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

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