let a be non zero Nat; :: thesis: ex n being non prime Nat st n divides (a |^ n) - a
per cases ( not a is prime or ( a is prime & a > 2 ) or ( a is prime & a <= 2 ) ) ;
suppose not a is prime ; :: thesis: ex n being non prime Nat st n divides (a |^ n) - a
then reconsider n = a as non zero non prime Nat ;
take n ; :: thesis: n divides (a |^ n) - a
a divides (a |^ n) - (a |^ 1) by Th18;
hence n divides (a |^ n) - a ; :: thesis: verum
end;
suppose that A1: a is prime and
A2: a > 2 ; :: thesis: ex n being non prime Nat st n divides (a |^ n) - a
reconsider a = a as odd Nat by ;
2 * a > 1 * a by XREAL_1:68;
then 2 * a > 2 * 1 by ;
then reconsider n = 2 * a as non prime Nat by PEPIN:17;
take n ; :: thesis: n divides (a |^ n) - a
A3: 2 = 2 |^ 1 ;
A4: (a |^ n) - a is even ;
a divides (a |^ n) - (a |^ 1) by Th18;
hence n divides (a |^ n) - a by ; :: thesis: verum
end;
suppose that A5: a is prime and
A6: a <= 2 ; :: thesis: ex n being non prime Nat st n divides (a |^ n) - a
a >= 1 + 1 by ;
then A7: a = 2 by ;
A8: 341 = 11 * 31 ;
then reconsider n = 341 as non prime Nat by ;
take n ; :: thesis: n divides (a |^ n) - a
thus n divides (a |^ n) - a by ; :: thesis: verum
end;
end;