let a be Nat; 6 divides (a |^ 3) - a
( 3 divides a * 1 or 3 divides (a + 1) * (a - 1) )
by Th50;
then A1:
3 divides ((a - 1) * (a + 1)) * (a * 1)
by INT_2:2;
( a is even or a + 1 is even )
;
then A2:
(a * (a + 1)) * (a - 1) is even
;
(2 * 1) + 1 is odd
;
then A3:
3,2 |^ 1 are_coprime
by NAT_5:3;
(a |^ (2 + 1)) - a =
((a |^ 2) * a) - a
by NEWTON:6
.=
(((a |^ 2) - (1 |^ 2)) * a) * 1
.=
(((a - 1) * (a + 1)) * a) * 1
by NEWTON01:1
;
then
( |.3.| divides |.((a |^ 3) - a).| & |.2.| divides |.((a |^ 3) - a).| )
by A1, A2, INT_2:16;
then
|.(3 * 2).| divides |.((a |^ 3) - a).|
by PEPIN:4, A3;
hence
6 divides (a |^ 3) - a
by INT_2:16; verum