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 4;
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 NAT_D:67;
then cLa * cLa,1 are_congruent_mod n by A1, NAT_D:64;
then n divides (cLa * cLa) - 1 by INT_2:15;
then A3: n divides (cLa + 1) * (cLa - 1) ;
0 = n * 0 ;
then A4: n divides 0 by INT_1:def 3;
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 NAT_D:67
.= 0 by A4, A6, INT_1:62 ;
hence contradiction by A2; :: thesis: verum

end;

cLa >= 0 by NAT_D:62;
then 0 + 1 <= cLa by A5, INT_1:7;
then A7: cLa - 1 is Element of NAT by INT_1:5;
cLa mod n = a mod n by NAT_D:65;
then A8: a,cLa are_congruent_mod n by NAT_D:64;
a mod n >= 0 by NAT_D:62;
then cLa + 1 is Element of NAT by INT_1:3;
then ( n divides cLa - (- 1) or n divides cLa - 1 ) by A7, A3, NEWTON:80;
then ( cLa, - 1 are_congruent_mod n or cLa,1 are_congruent_mod n ) by INT_2:15;
hence ( a,1 are_congruent_mod n or a, - 1 are_congruent_mod n ) by A8, INT_1:15; :: thesis: verum