let n be Nat; :: thesis: 11 divides (2 |^ (10 * n)) - 1
(93 * 11) + 1,1 are_congruent_mod 11 ;
then (2 |^ 10) |^ n,1 |^ n are_congruent_mod 11 by Lm7, GR_CY_3:34;
hence 11 divides (2 |^ (10 * n)) - 1 by NEWTON:9; :: thesis: verum