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 (a ^2) mod p <> 0 by INT_1:62;
hence Lege ((a ^2),p) = 1 by Def3, Th9; :: thesis: verum