let n be non zero Nat; :: thesis: 3 divides ((2 |^ (2 |^ (n + 1))) + (2 |^ (2 |^ n))) + 1
A1: (2 |^ (2 |^ (n + 1))) mod 3 = 1 by Th42;
A2: (2 |^ (2 |^ n)) mod 3 = 1 by Th42;
(((2 |^ (2 |^ (n + 1))) + (2 |^ (2 |^ n))) + 1) mod 3 = ((1 + 1) + 1) mod 3 by A1, A2, Lm8, NUMBER05:8
.= 0 ;
hence 3 divides ((2 |^ (2 |^ (n + 1))) + (2 |^ (2 |^ n))) + 1 by INT_1:62; :: thesis: verum