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 ( ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0𝑁𝑀 ) → ( ( FermatNo ‘ 𝑁 ) gcd ( FermatNo ‘ 𝑀 ) ) = 1 )

Proof

Step Hyp Ref Expression
1 nn0re ( 𝑁 ∈ ℕ0𝑁 ∈ ℝ )
2 nn0re ( 𝑀 ∈ ℕ0𝑀 ∈ ℝ )
3 lttri4 ( ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( 𝑁 < 𝑀𝑁 = 𝑀𝑀 < 𝑁 ) )
4 1 2 3 syl2an ( ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0 ) → ( 𝑁 < 𝑀𝑁 = 𝑀𝑀 < 𝑁 ) )
5 4 3adant3 ( ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0𝑁𝑀 ) → ( 𝑁 < 𝑀𝑁 = 𝑀𝑀 < 𝑁 ) )
6 fmtnonn ( 𝑁 ∈ ℕ0 → ( FermatNo ‘ 𝑁 ) ∈ ℕ )
7 6 nnzd ( 𝑁 ∈ ℕ0 → ( FermatNo ‘ 𝑁 ) ∈ ℤ )
8 fmtnonn ( 𝑀 ∈ ℕ0 → ( FermatNo ‘ 𝑀 ) ∈ ℕ )
9 8 nnzd ( 𝑀 ∈ ℕ0 → ( FermatNo ‘ 𝑀 ) ∈ ℤ )
10 gcdcom ( ( ( FermatNo ‘ 𝑁 ) ∈ ℤ ∧ ( FermatNo ‘ 𝑀 ) ∈ ℤ ) → ( ( FermatNo ‘ 𝑁 ) gcd ( FermatNo ‘ 𝑀 ) ) = ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) )
11 7 9 10 syl2anr ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) → ( ( FermatNo ‘ 𝑁 ) gcd ( FermatNo ‘ 𝑀 ) ) = ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) )
12 11 3adant3 ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0𝑁 < 𝑀 ) → ( ( FermatNo ‘ 𝑁 ) gcd ( FermatNo ‘ 𝑀 ) ) = ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) )
13 goldbachthlem2 ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0𝑁 < 𝑀 ) → ( ( FermatNo ‘ 𝑀 ) gcd ( FermatNo ‘ 𝑁 ) ) = 1 )
14 12 13 eqtrd ( ( 𝑀 ∈ ℕ0𝑁 ∈ ℕ0𝑁 < 𝑀 ) → ( ( FermatNo ‘ 𝑁 ) gcd ( FermatNo ‘ 𝑀 ) ) = 1 )
15 14 3exp ( 𝑀 ∈ ℕ0 → ( 𝑁 ∈ ℕ0 → ( 𝑁 < 𝑀 → ( ( FermatNo ‘ 𝑁 ) gcd ( FermatNo ‘ 𝑀 ) ) = 1 ) ) )
16 15 impcom ( ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0 ) → ( 𝑁 < 𝑀 → ( ( FermatNo ‘ 𝑁 ) gcd ( FermatNo ‘ 𝑀 ) ) = 1 ) )
17 16 3adant3 ( ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0𝑁𝑀 ) → ( 𝑁 < 𝑀 → ( ( FermatNo ‘ 𝑁 ) gcd ( FermatNo ‘ 𝑀 ) ) = 1 ) )
18 eqneqall ( 𝑁 = 𝑀 → ( 𝑁𝑀 → ( ( FermatNo ‘ 𝑁 ) gcd ( FermatNo ‘ 𝑀 ) ) = 1 ) )
19 18 com12 ( 𝑁𝑀 → ( 𝑁 = 𝑀 → ( ( FermatNo ‘ 𝑁 ) gcd ( FermatNo ‘ 𝑀 ) ) = 1 ) )
20 19 3ad2ant3 ( ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0𝑁𝑀 ) → ( 𝑁 = 𝑀 → ( ( FermatNo ‘ 𝑁 ) gcd ( FermatNo ‘ 𝑀 ) ) = 1 ) )
21 goldbachthlem2 ( ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0𝑀 < 𝑁 ) → ( ( FermatNo ‘ 𝑁 ) gcd ( FermatNo ‘ 𝑀 ) ) = 1 )
22 21 3expia ( ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0 ) → ( 𝑀 < 𝑁 → ( ( FermatNo ‘ 𝑁 ) gcd ( FermatNo ‘ 𝑀 ) ) = 1 ) )
23 22 3adant3 ( ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0𝑁𝑀 ) → ( 𝑀 < 𝑁 → ( ( FermatNo ‘ 𝑁 ) gcd ( FermatNo ‘ 𝑀 ) ) = 1 ) )
24 17 20 23 3jaod ( ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0𝑁𝑀 ) → ( ( 𝑁 < 𝑀𝑁 = 𝑀𝑀 < 𝑁 ) → ( ( FermatNo ‘ 𝑁 ) gcd ( FermatNo ‘ 𝑀 ) ) = 1 ) )
25 5 24 mpd ( ( 𝑁 ∈ ℕ0𝑀 ∈ ℕ0𝑁𝑀 ) → ( ( FermatNo ‘ 𝑁 ) gcd ( FermatNo ‘ 𝑀 ) ) = 1 )