let a, n be Nat; 42 divides (a |^ ((6 * n) + 1)) - a
A0:
( 2,7 are_coprime & 3,7 are_coprime )
by INT_2:28, INT_2:30, PEPIN:41, NAT_4:26;
A1:
2 divides (a |^ ((6 * n) + 1)) - a
by Th74;
3 divides (a |^ ((2 * (3 * n)) + 1)) - a
by Th75;
then A2:
2 * 3 divides (a |^ ((6 * n) + 1)) - a
by INT_2:28, INT_2:30, PEPIN:41, A1, PEPIN:4;
7 divides (a |^ ((6 * n) + 1)) - a
by Th77;
then
7 * (2 * 3) divides (a |^ ((6 * n) + 1)) - a
by A0, EULER_1:14, A2, PEPIN:4;
hence
42 divides (a |^ ((6 * n) + 1)) - a
; verum