let a, n be Nat; :: thesis: 6 divides (a |^ ((2 * n) + 1)) - a
A1: 2 divides (a |^ ((2 * n) + 1)) - a by Th74;
3 divides (a |^ ((2 * n) + 1)) - a by Th75;
then 2 * 3 divides (a |^ ((2 * n) + 1)) - a by INT_2:28, INT_2:30, PEPIN:41, A1, PEPIN:4;
hence 6 divides (a |^ ((2 * n) + 1)) - a ; :: thesis: verum