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