let n, t be Nat; :: thesis: Fermat n divides (2 |^ ((2 |^ n) * ((2 * t) + 1))) + 1
set T = 2 |^ (2 |^ n);
( (2 |^ ((2 |^ n) * ((2 * t) + 1))) + 1 = ((2 |^ (2 |^ n)) |^ ((2 * t) + 1)) + (1 |^ ((2 * t) + 1)) & Fermat n = (2 |^ (2 |^ n)) + 1 ) by PEPIN:def 3, NEWTON:9;
hence Fermat n divides (2 |^ ((2 |^ n) * ((2 * t) + 1))) + 1 by NEWTON01:35; :: thesis: verum