let a be Integer; :: thesis: for p being Prime st a mod p <> 0 holds
Lege ((a ^2),p) = 1
let p be Prime; :: thesis: ( a mod p <> 0 implies Lege ((a ^2),p) = 1 )
assume a mod p <> 0 ; :: thesis: Lege ((a ^2),p) = 1
then not p divides a by INT_1:62;
then not p divides a ^2 by Th7;
then A1: (a ^2) mod p <> 0 by INT_1:62;
a ^2 is_quadratic_residue_mod p by Th9;
hence Lege ((a ^2),p) = 1 by Def3, A1; :: thesis: verum