let n be Nat; :: thesis: ((Fermat n) -' 1) mod 2 = 0
2 mod 2 = 0 by NAT_D:25;
then ( (Fermat n) -' 1 = 2 |^ (2 |^ n) & 2 is even ) by NAT_2:21, NAT_D:34;
then (Fermat n) -' 1 is even by Th21, PREPOWER:6;
hence ((Fermat n) -' 1) mod 2 = 0 by NAT_2:21; :: thesis: verum