A1: 5 divides (a |^ 5) - a by PEPIN:59, Th58;
assume A2: 5 divides (a |^ 3) - 1 ; :: thesis: 5 divides a - 1
then a2b: a |^ 3 <> 0 by INT_2:13;
A3: a divides a |^ 3 by NAT_3:3;
5 divides (- (a |^ 2)) * ((a |^ 3) - 1) by A2, INT_2:2;
then 5 divides (- ((a |^ 2) * (a |^ 3))) + (a |^ 2) ;
then 5 divides (- (a |^ (2 + 3))) + (a |^ 2) by NEWTON:8;
then 5 divides ((- (a |^ 5)) + (a |^ 2)) + ((a |^ 5) - a) by WSIERP_1:4, A1;
then 5 divides (a |^ 2) - a ;
then 5 divides (a * a) - a by NEWTON:81;
then A4: 5 divides a * (a - 1) ;
not 5 divides ((a |^ 3) - 1) + 1 by A2, a2b, NEWTON:39;
then not 5 divides a by A3, INT_2:9;
hence 5 divides a - 1 by A4, PEPIN:59, INT_5:7; :: thesis: verum