A1: (2 |^ 5) |^ 68 = 2 |^ (5 * 68) by NEWTON:9;
A2: 1 mod 31 = 1 by NAT_D:24;
2 |^ 5 = (((2 * 2) * 2) * 2) * 2 by Th1
.= (31 * 1) + 1 ;
then (2 |^ 5) mod 31 = 1 by NAT_D:def 2;
then ((2 |^ 5) |^ 68) mod 31 = 1 by NEWTON05:15;
then A3: 2 |^ 340,1 are_congruent_mod 31 by A1, A2, NAT_D:64;
(2 |^ (340 + 1)) - 2 = ((2 |^ 340) * (2 |^ 1)) - (2 * 1) by NEWTON:8
.= 2 * ((2 |^ 340) - 1) ;
hence 31 divides (2 |^ 341) - 2 by A3, INT_2:2; :: thesis: verum