2 |^ 56,1 |^ 7 are_congruent_mod 17 by Lm1144, Lm1145, Lm1146, INT_1:15;
then (2 |^ 56) |^ 10,1 |^ 10 are_congruent_mod 17 by GR_CY_3:34;
then (2 |^ 560) * (2 |^ 1),1 * 2 are_congruent_mod 17 by Lm1120, INT_4:11;
then 2 |^ (560 + 1),2 are_congruent_mod 17 by NEWTON:8;
hence 17 divides (2 |^ 561) - 2 ; :: thesis: verum