let a be Integer; :: thesis: for n being Prime holds
( not (a * a) mod n = 1 or a,1 are_congruent_mod n or a, - 1 are_congruent_mod n )
let n be Prime; :: thesis: ( not (a * a) mod n = 1 or a,1 are_congruent_mod n or a, - 1 are_congruent_mod n )
reconsider cLa = a mod n as Integer ;
n > 1 by INT_2:def 5;
then A1: 1 mod n = 1 by PEPIN:5;
assume A2: (a * a) mod n = 1 ; :: thesis: ( a,1 are_congruent_mod n or a, - 1 are_congruent_mod n )
then (cLa * cLa) mod n = 1 by INT_3:15;
then cLa * cLa,1 are_congruent_mod n by A1, INT_3:12;
then n divides (cLa * cLa) - 1 by INT_2:19;
then A3: n divides (cLa + 1) * (cLa - 1) ;
0 = n * 0 ;
then A4: n divides 0 by INT_1:def 9;
A5: a mod n <> 0

proof

assume A6: a mod n = 0 ; :: thesis: contradiction
(a * a) mod n = ((a mod n) * (a mod n)) mod n by INT_3:15
.= 0 by A4, A6, INT_1:89 ;
hence contradiction by A2; :: thesis: verum

end;

cLa >= 0 by INT_3:9;
then 0 + 1 <= cLa by A5, INT_1:20;
then A7: cLa - 1 is Element of NAT by INT_1:18;
cLa mod n = a mod n by INT_3:13;
then A8: a,cLa are_congruent_mod n by INT_3:12;
a mod n >= 0 by INT_3:9;
then cLa + 1 is Element of NAT by INT_1:16;
then ( n divides cLa - (- 1) or n divides cLa - 1 ) by A7, A3, NEWTON:98;
then ( cLa, - 1 are_congruent_mod n or cLa,1 are_congruent_mod n ) by INT_2:19;
hence ( a,1 are_congruent_mod n or a, - 1 are_congruent_mod n ) by A8, INT_1:36; :: thesis: verum