let a be non trivial Nat; :: thesis: for x, y being Integer holds Px (a,|.((4 * x) + y).|), Px (a,|.y.|) are_congruent_mod Px (a,|.x.|)
let x, y be Integer; :: thesis: Px (a,|.((4 * x) + y).|), Px (a,|.y.|) are_congruent_mod Px (a,|.x.|)
A1: (Px (a,|.((2 * x) + y).|)) * (- 1),(- (Px (a,|.y.|))) * (- 1) are_congruent_mod Px (a,|.x.|) by Th17, INT_4:11;
Px (a,|.((2 * x) + ((2 * x) + y)).|), - (Px (a,|.((2 * x) + y).|)) are_congruent_mod Px (a,|.x.|) by Th17;
hence Px (a,|.((4 * x) + y).|), Px (a,|.y.|) are_congruent_mod Px (a,|.x.|) by A1, INT_1:15; :: thesis: verum