Metamath Proof Explorer

Theorem goldbachth

Description: Goldbach's theorem: Two different Fermat numbers are coprime. See ProofWiki "Goldbach's theorem", 31-Jul-2021, https://proofwiki.org/wiki/Goldbach%27s_Theorem or Wikipedia "Fermat number", 31-Jul-2021, https://en.wikipedia.org/wiki/Fermat_number#Basic_properties . (Contributed by AV, 1-Aug-2021)

Ref Expression
Assertion goldbachth 
|- ( ( N e. NN0 /\ M e. NN0 /\ N =/= M ) -> ( ( FermatNo ` N ) gcd ( FermatNo ` M ) ) = 1 )

Proof

Step Hyp Ref Expression
1 nn0re 
 |-  ( N e. NN0 -> N e. RR )
2 nn0re 
 |-  ( M e. NN0 -> M e. RR )
3 lttri4 
 |-  ( ( N e. RR /\ M e. RR ) -> ( N < M \/ N = M \/ M < N ) )
4 1 2 3 syl2an 
 |-  ( ( N e. NN0 /\ M e. NN0 ) -> ( N < M \/ N = M \/ M < N ) )
5 4 3adant3 
 |-  ( ( N e. NN0 /\ M e. NN0 /\ N =/= M ) -> ( N < M \/ N = M \/ M < N ) )
6 fmtnonn 
 |-  ( N e. NN0 -> ( FermatNo ` N ) e. NN )
7 6 nnzd 
 |-  ( N e. NN0 -> ( FermatNo ` N ) e. ZZ )
8 fmtnonn 
 |-  ( M e. NN0 -> ( FermatNo ` M ) e. NN )
9 8 nnzd 
 |-  ( M e. NN0 -> ( FermatNo ` M ) e. ZZ )
10 gcdcom 
 |-  ( ( ( FermatNo ` N ) e. ZZ /\ ( FermatNo ` M ) e. ZZ ) -> ( ( FermatNo ` N ) gcd ( FermatNo ` M ) ) = ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) )
11 7 9 10 syl2anr 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( ( FermatNo ` N ) gcd ( FermatNo ` M ) ) = ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) )
12 11 3adant3 
 |-  ( ( M e. NN0 /\ N e. NN0 /\ N < M ) -> ( ( FermatNo ` N ) gcd ( FermatNo ` M ) ) = ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) )
13 goldbachthlem2 
 |-  ( ( M e. NN0 /\ N e. NN0 /\ N < M ) -> ( ( FermatNo ` M ) gcd ( FermatNo ` N ) ) = 1 )
14 12 13 eqtrd 
 |-  ( ( M e. NN0 /\ N e. NN0 /\ N < M ) -> ( ( FermatNo ` N ) gcd ( FermatNo ` M ) ) = 1 )
15 14 3exp 
 |-  ( M e. NN0 -> ( N e. NN0 -> ( N < M -> ( ( FermatNo ` N ) gcd ( FermatNo ` M ) ) = 1 ) ) )
16 15 impcom 
 |-  ( ( N e. NN0 /\ M e. NN0 ) -> ( N < M -> ( ( FermatNo ` N ) gcd ( FermatNo ` M ) ) = 1 ) )
17 16 3adant3 
 |-  ( ( N e. NN0 /\ M e. NN0 /\ N =/= M ) -> ( N < M -> ( ( FermatNo ` N ) gcd ( FermatNo ` M ) ) = 1 ) )
18 eqneqall 
 |-  ( N = M -> ( N =/= M -> ( ( FermatNo ` N ) gcd ( FermatNo ` M ) ) = 1 ) )
19 18 com12 
 |-  ( N =/= M -> ( N = M -> ( ( FermatNo ` N ) gcd ( FermatNo ` M ) ) = 1 ) )
20 19 3ad2ant3 
 |-  ( ( N e. NN0 /\ M e. NN0 /\ N =/= M ) -> ( N = M -> ( ( FermatNo ` N ) gcd ( FermatNo ` M ) ) = 1 ) )
21 goldbachthlem2 
 |-  ( ( N e. NN0 /\ M e. NN0 /\ M < N ) -> ( ( FermatNo ` N ) gcd ( FermatNo ` M ) ) = 1 )
22 21 3expia 
 |-  ( ( N e. NN0 /\ M e. NN0 ) -> ( M < N -> ( ( FermatNo ` N ) gcd ( FermatNo ` M ) ) = 1 ) )
23 22 3adant3 
 |-  ( ( N e. NN0 /\ M e. NN0 /\ N =/= M ) -> ( M < N -> ( ( FermatNo ` N ) gcd ( FermatNo ` M ) ) = 1 ) )
24 17 20 23 3jaod 
 |-  ( ( N e. NN0 /\ M e. NN0 /\ N =/= M ) -> ( ( N < M \/ N = M \/ M < N ) -> ( ( FermatNo ` N ) gcd ( FermatNo ` M ) ) = 1 ) )
25 5 24 mpd 
 |-  ( ( N e. NN0 /\ M e. NN0 /\ N =/= M ) -> ( ( FermatNo ` N ) gcd ( FermatNo ` M ) ) = 1 )