let a be Nat; :: thesis: 154 divides (a |^ 61) - a
( 6 + 1 is odd & 6 + 1 is prime & 10 + 1 is odd & 10 + 1 is prime ) by NAT_4:26, NAT_4:27;
then (2 * (6 + 1)) * (10 + 1) divides (a |^ ((6 * 10) + 1)) - a by Th78;
hence 154 divides (a |^ 61) - a ; :: thesis: verum