let a be Nat; :: thesis: for p being Prime holds
( (a |^ (p - 1)) mod p = 0 or (a |^ (p - 1)) mod p = 1 )
let p be Prime; :: thesis: ( (a |^ (p - 1)) mod p = 0 or (a |^ (p - 1)) mod p = 1 )
reconsider k = p - 1 as non zero Nat ;

per cases ( k + 1 divides a or not k + 1 divides a ) ;

suppose B1: k + 1 divides a ; :: thesis: ( (a |^ (p - 1)) mod p = 0 or (a |^ (p - 1)) mod p = 1 )

a |^ 1 divides a |^ k by NEWTON:89, NAT_1:14;
then p divides a |^ k by B1, INT_2:9;
hence ( (a |^ (p - 1)) mod p = 0 or (a |^ (p - 1)) mod p = 1 ) by INT_1:62; :: thesis: verum

end;

suppose B1: not k + 1 divides a ; :: thesis: ( (a |^ (p - 1)) mod p = 0 or (a |^ (p - 1)) mod p = 1 )

then reconsider a = a as non zero Nat by INT_2:12;
k + 1 divides (a |^ k) - 1 by B1, NEWTON02:157;
then B2: ((a |^ k) - 1) mod p = 0 by INT_1:62;
then (((a |^ k) - 1) + 1) mod p = (((a |^ k) - 1) mod p) + 1 by NAT_D:70;
hence ( (a |^ (p - 1)) mod p = 0 or (a |^ (p - 1)) mod p = 1 ) by B2; :: thesis: verum

end;

end;