(3 |^ 16) |^ 69,1 |^ 69 are_congruent_mod 17 by Lm1133, Lm1108, Lm1146, GR_CY_3:34;
then (3 |^ 1104) * 3,1 * 3 are_congruent_mod 17 by Lm1140, INT_4:11;
then 3 |^ (1104 + 1),3 are_congruent_mod 17 by NEWTON:6;
hence 17 divides (3 |^ 1105) - 3 ; :: thesis: verum