let i, j be Integer; :: thesis: for m being Nat st i is_quadratic_residue_mod m & i,j are_congruent_mod m holds
j is_quadratic_residue_mod m
let m be Nat; :: thesis: ( i is_quadratic_residue_mod m & i,j are_congruent_mod m implies j is_quadratic_residue_mod m )
assume that
A1: i is_quadratic_residue_mod m and
A2: i,j are_congruent_mod m ; :: thesis: j is_quadratic_residue_mod m
consider x being Integer such that
A3: ((x ^2) - i) mod m = 0 by A1, Def2;
m divides i - j by A2, INT_2:15;
then A4: (i - j) mod m = 0 by Lm1;
((x ^2) - j) mod m = (((x ^2) - i) + (i - j)) mod m
.= ((((x ^2) - i) mod m) + ((i - j) mod m)) mod m by NAT_D:66
.= 0 by A3, A4, NAT_D:65 ;
hence j is_quadratic_residue_mod m by Def2; :: thesis: verum