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