A1:
(2 |^ 10) |^ 34 = 2 |^ (10 * 34)
by NEWTON:9;
A2:
1 mod 11 = 1
by NAT_D:24;
2 |^ 10 =
((((((((2 * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2) * 2
by Th6
.=
(11 * 93) + 1
;
then
(2 |^ 10) mod 11 = 1
by NAT_D:def 2;
then
((2 |^ 10) |^ 34) mod 11 = 1
by NEWTON05:15;
then A3:
2 |^ 340,1 are_congruent_mod 11
by A1, A2, NAT_D:64;
(2 |^ (340 + 1)) - 2 =
((2 |^ 340) * (2 |^ 1)) - (2 * 1)
by NEWTON:8
.=
2 * ((2 |^ 340) - 1)
;
hence
11 divides (2 |^ 341) - 2
by A3, INT_2:2; verum