let n be Nat; :: thesis: ( n <> 0 implies 3, Fermat n are_relative_prime )
assume A1: n <> 0 ; :: thesis: 3, Fermat n are_relative_prime
(Fermat n) gcd 3 <> 3

proof

assume (Fermat n) gcd 3 = 3 ; :: thesis: contradiction
then 3 divides Fermat n by NAT_D:def 5;
then consider k being Element of NAT such that
A2: 3 = (k * (2 |^ (n + 1))) + 1 by Th44, Th61;
1 = (k * (2 |^ (n + 1))) div 2 by A2, NAT_2:5;
then 1 = k * (2 |^ n) by Lm5;
then ( k = 1 & 2 |^ n = 1 ) by NAT_1:15;
then 2 |^ n = 2 |^ 0 by NEWTON:9;
hence contradiction by A1, Th31; :: thesis: verum

end;

hence 3, Fermat n are_relative_prime by Th2, Th44; :: thesis: verum