let a be Integer; :: thesis: for m being Nat holds a ^2 is_quadratic_residue_mod m

let m be Nat; :: thesis: a ^2 is_quadratic_residue_mod m

((a ^2) - (a ^2)) mod m = 0 by INT_1:73;

hence a ^2 is_quadratic_residue_mod m ; :: thesis: verum

let m be Nat; :: thesis: a ^2 is_quadratic_residue_mod m

((a ^2) - (a ^2)) mod m = 0 by INT_1:73;

hence a ^2 is_quadratic_residue_mod m ; :: thesis: verum