let n be Nat; :: thesis: ((2 |^ n) - 1) ^2 divides (2 |^ (((2 |^ n) - 1) * n)) - 1
set m = (2 |^ n) - 1;
(((2 |^ n) - 1) + 1) |^ ((2 |^ n) - 1) = 2 |^ (((2 |^ n) - 1) * n) by NEWTON:9;
hence ((2 |^ n) - 1) ^2 divides (2 |^ (((2 |^ n) - 1) * n)) - 1 by Th42; :: thesis: verum