let a be Nat; :: thesis: 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; :: thesis: verum

( 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; :: thesis: verum