let i, j be Integer; :: thesis: for m being Nat st i gcd m = 1 & 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 gcd m = 1 & i is_quadratic_residue_mod m & i,j are_congruent_mod m implies j is_quadratic_residue_mod m )
assume A1: ( i gcd m = 1 & i is_quadratic_residue_mod m & i,j are_congruent_mod m ) ; :: thesis: j is_quadratic_residue_mod m
then consider x being Integer such that
A2: ((x ^2 ) - i) mod m = 0 by Def2;
m divides i - j by A1, INT_2:19;
then A3: (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 INT_3:14
.= 0 by A2, A3, INT_3:13 ;
hence j is_quadratic_residue_mod m by Def2; :: thesis: verum