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 ) )
;

end;

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;take n ; :: thesis: n divides (a |^ n) - a

a divides (a |^ n) - (a |^ 1) by Th18;

hence n divides (a |^ n) - a ; :: thesis: verum

suppose that A1:
a is prime
and

A2: a > 2 ; :: thesis: ex n being non prime Nat st n divides (a |^ n) - a

A2: a > 2 ; :: thesis: ex n being non prime Nat st n divides (a |^ n) - a

reconsider a = a as odd Nat by A1, A2, PEPIN:17;

2 * a > 1 * a by XREAL_1:68;

then 2 * a > 2 * 1 by A2, XXREAL_0:2;

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 A3, A4, PEPIN:4, NAT_5:3; :: thesis: verum

end;2 * a > 1 * a by XREAL_1:68;

then 2 * a > 2 * 1 by A2, XXREAL_0:2;

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 A3, A4, PEPIN:4, NAT_5:3; :: thesis: verum

suppose that A5:
a is prime
and

A6: a <= 2 ; :: thesis: ex n being non prime Nat st n divides (a |^ n) - a

A6: a <= 2 ; :: thesis: ex n being non prime Nat st n divides (a |^ n) - a

a >= 1 + 1
by A5, NAT_1:13;

then A7: a = 2 by A6, XXREAL_0:1;

A8: 341 = 11 * 31 ;

then reconsider n = 341 as non prime Nat by NAT_4:27, NUMERAL2:24;

take n ; :: thesis: n divides (a |^ n) - a

thus n divides (a |^ n) - a by A7, A8, Th20, Th21, PEPIN:4, INT_2:30, NAT_4:27, NUMERAL2:24; :: thesis: verum

end;then A7: a = 2 by A6, XXREAL_0:1;

A8: 341 = 11 * 31 ;

then reconsider n = 341 as non prime Nat by NAT_4:27, NUMERAL2:24;

take n ; :: thesis: n divides (a |^ n) - a

thus n divides (a |^ n) - a by A7, A8, Th20, Th21, PEPIN:4, INT_2:30, NAT_4:27, NUMERAL2:24; :: thesis: verum