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

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