let n be Nat; :: thesis: not Fermat n is even
A1: (Fermat n) - 1 = (Fermat n) -' 1 by XREAL_0:def 2;
((Fermat n) -' 1) mod 2 = 0 by Lm17;
then (Fermat n) -' 1 is even by NAT_2:23;
hence not Fermat n is even by A1; :: thesis: verum