let n be Nat; :: thesis: (Fermat n) mod (2 |^ (2 |^ n)) = 1
set 2N = 2 |^ (2 |^ n);
(Fermat n) mod (2 |^ (2 |^ n)) = (((2 |^ (2 |^ n)) * 1) + 1) mod (2 |^ (2 |^ n))
.= 1 mod (2 |^ (2 |^ n)) by NAT_D:21
.= 1 by Lm2, NAT_D:14 ;
hence (Fermat n) mod (2 |^ (2 |^ n)) = 1 ; :: thesis: verum