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 )