let n be Nat; :: thesis: ( n <> 0 implies 3, Fermat n are_coprime )
assume A1: n <> 0 ; :: thesis: 3, Fermat n are_coprime
(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 Th41, Th56;
1 = (k * (2 |^ (n + 1))) div 2 by A2, NAT_2:3;
then 1 = k * (2 |^ n) by Lm5;
then 2 |^ n = 1 by NAT_1:15;
then 2 |^ n = 2 |^ 0 by NEWTON:4;
hence contradiction by A1, Th30; :: thesis: verum
end;
hence 3, Fermat n are_coprime by Th2, Th41; :: thesis: verum