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

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

( 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

cLa >= 0
by NAT_D:62;
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;(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

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