let a be Nat; :: thesis: for p being prime Nat st not p divides a holds
ex n being Nat st
( p divides (a |^ n) - 1 & 0 < n & n < p )
let p be prime Nat; :: thesis: ( not p divides a implies ex n being Nat st
( p divides (a |^ n) - 1 & 0 < n & n < p ) )
assume A0: not p divides a ; :: thesis: ex n being Nat st
( p divides (a |^ n) - 1 & 0 < n & n < p )
p > 1 by INT_2:def 4;
then p >= 1 + 1 by NAT_1:13;
then consider k being Nat such that
A1: p = 2 + k by NAT_1:10;
p = (k + 1) + 1 by A1;
then p divides (a |^ (k + 1)) - 1 by A0, Th59;
hence ex n being Nat st
( p divides (a |^ n) - 1 & 0 < n & n < p ) by A1, XREAL_1:6; :: thesis: verum