(10000 * 4304) + 6720 = 17 * ((100 * 25321) + 60) ;
then 3 |^ 16,1 are_congruent_mod 17 by Lm1108, Lm1143, Lm1133;
then (3 |^ 16) |^ 35,1 |^ 35 are_congruent_mod 17 by GR_CY_3:34;
then (3 |^ 560) * (3 |^ 1),1 * 3 are_congruent_mod 17 by Lm1136, INT_4:11;
then 3 |^ (560 + 1),3 are_congruent_mod 17 by NEWTON:8;
hence 17 divides (3 |^ 561) - 3 ; :: thesis: verum