let a be Nat; :: thesis: ( 5 divides (a |^ 3) - 1 iff 5 divides a - 1 )
L1: ( 5 divides (a |^ 3) - 1 implies 5 divides a - 1 )

proof

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

end;

a - 1 divides (a |^ 3) - (1 |^ 3) by NEWTON01:33;
hence ( 5 divides (a |^ 3) - 1 iff 5 divides a - 1 ) by L1, INT_2:9; :: thesis: verum