(10 * 5904) + 8 = 11 * 5368 ;
then 3 |^ 10,1 are_congruent_mod 11 by Lm1113;
then (3 |^ 10) |^ 56,1 |^ 56 are_congruent_mod 11 by GR_CY_3:34;
then (3 |^ 560) * (3 |^ 1),1 * 3 are_congruent_mod 11 by Lm1135, INT_4:11;
hence 11 divides (3 |^ 561) - 3 by Lm1137; :: thesis: verum