Metamath Proof Explorer

Theorem sgoldbeven3prm

Description: If the binary Goldbach conjecture is valid, then an even integer greater than 5 can be expressed as the sum of three primes: Since ( N - 2 ) is even iff N is even, there would be primes p and q with ( N - 2 ) = ( p + q ) , and therefore N = ( ( p + q ) + 2 ) . (Contributed by AV, 24-Dec-2021)

Ref Expression
Assertion sgoldbeven3prm ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ( ( 𝑁 ∈ Even ∧ 6 ≤ 𝑁 ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑁 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )

Proof

Step Hyp Ref Expression
1 sbgoldbb ⊢ ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∀ 𝑛 ∈ Even ( 2 < 𝑛 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) )
2 2p2e4 ⊢ ( 2 + 2 ) = 4
3 evenz ⊢ ( 𝑁 ∈ Even → 𝑁 ∈ ℤ )
4 3 zred ⊢ ( 𝑁 ∈ Even → 𝑁 ∈ ℝ )
5 4lt6 ⊢ 4 < 6
6 4re ⊢ 4 ∈ ℝ
7 6re ⊢ 6 ∈ ℝ
8 ltletr ⊢ ( ( 4 ∈ ℝ ∧ 6 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 4 < 6 ∧ 6 ≤ 𝑁 ) → 4 < 𝑁 ) )
9 6 7 8 mp3an12 ⊢ ( 𝑁 ∈ ℝ → ( ( 4 < 6 ∧ 6 ≤ 𝑁 ) → 4 < 𝑁 ) )
10 5 9 mpani ⊢ ( 𝑁 ∈ ℝ → ( 6 ≤ 𝑁 → 4 < 𝑁 ) )
11 4 10 syl ⊢ ( 𝑁 ∈ Even → ( 6 ≤ 𝑁 → 4 < 𝑁 ) )
12 11 imp ⊢ ( ( 𝑁 ∈ Even ∧ 6 ≤ 𝑁 ) → 4 < 𝑁 )
13 2 12 eqbrtrid ⊢ ( ( 𝑁 ∈ Even ∧ 6 ≤ 𝑁 ) → ( 2 + 2 ) < 𝑁 )
14 2re ⊢ 2 ∈ ℝ
15 14 a1i ⊢ ( ( 𝑁 ∈ Even ∧ 6 ≤ 𝑁 ) → 2 ∈ ℝ )
16 4 adantr ⊢ ( ( 𝑁 ∈ Even ∧ 6 ≤ 𝑁 ) → 𝑁 ∈ ℝ )
17 15 15 16 ltaddsub2d ⊢ ( ( 𝑁 ∈ Even ∧ 6 ≤ 𝑁 ) → ( ( 2 + 2 ) < 𝑁 ↔ 2 < ( 𝑁 − 2 ) ) )
18 13 17 mpbid ⊢ ( ( 𝑁 ∈ Even ∧ 6 ≤ 𝑁 ) → 2 < ( 𝑁 − 2 ) )
19 2evenALTV ⊢ 2 ∈ Even
20 emee ⊢ ( ( 𝑁 ∈ Even ∧ 2 ∈ Even ) → ( 𝑁 − 2 ) ∈ Even )
21 19 20 mpan2 ⊢ ( 𝑁 ∈ Even → ( 𝑁 − 2 ) ∈ Even )
22 breq2 ⊢ ( 𝑛 = ( 𝑁 − 2 ) → ( 2 < 𝑛 ↔ 2 < ( 𝑁 − 2 ) ) )
23 eqeq1 ⊢ ( 𝑛 = ( 𝑁 − 2 ) → ( 𝑛 = ( 𝑝 + 𝑞 ) ↔ ( 𝑁 − 2 ) = ( 𝑝 + 𝑞 ) ) )
24 23 2rexbidv ⊢ ( 𝑛 = ( 𝑁 − 2 ) → ( ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ↔ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑁 − 2 ) = ( 𝑝 + 𝑞 ) ) )
25 22 24 imbi12d ⊢ ( 𝑛 = ( 𝑁 − 2 ) → ( ( 2 < 𝑛 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) ↔ ( 2 < ( 𝑁 − 2 ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑁 − 2 ) = ( 𝑝 + 𝑞 ) ) ) )
26 25 rspcv ⊢ ( ( 𝑁 − 2 ) ∈ Even → ( ∀ 𝑛 ∈ Even ( 2 < 𝑛 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) → ( 2 < ( 𝑁 − 2 ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑁 − 2 ) = ( 𝑝 + 𝑞 ) ) ) )
27 2prm ⊢ 2 ∈ ℙ
28 27 a1i ⊢ ( ( 𝑁 ∈ Even ∧ ( 𝑁 − 2 ) = ( 𝑝 + 𝑞 ) ) → 2 ∈ ℙ )
29 oveq2 ⊢ ( 𝑟 = 2 → ( ( 𝑝 + 𝑞 ) + 𝑟 ) = ( ( 𝑝 + 𝑞 ) + 2 ) )
30 29 eqeq2d ⊢ ( 𝑟 = 2 → ( 𝑁 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ↔ 𝑁 = ( ( 𝑝 + 𝑞 ) + 2 ) ) )
31 30 adantl ⊢ ( ( ( 𝑁 ∈ Even ∧ ( 𝑁 − 2 ) = ( 𝑝 + 𝑞 ) ) ∧ 𝑟 = 2 ) → ( 𝑁 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ↔ 𝑁 = ( ( 𝑝 + 𝑞 ) + 2 ) ) )
32 3 zcnd ⊢ ( 𝑁 ∈ Even → 𝑁 ∈ ℂ )
33 2cnd ⊢ ( 𝑁 ∈ Even → 2 ∈ ℂ )
34 npcan ⊢ ( ( 𝑁 ∈ ℂ ∧ 2 ∈ ℂ ) → ( ( 𝑁 − 2 ) + 2 ) = 𝑁 )
35 34 eqcomd ⊢ ( ( 𝑁 ∈ ℂ ∧ 2 ∈ ℂ ) → 𝑁 = ( ( 𝑁 − 2 ) + 2 ) )
36 32 33 35 syl2anc ⊢ ( 𝑁 ∈ Even → 𝑁 = ( ( 𝑁 − 2 ) + 2 ) )
37 36 adantr ⊢ ( ( 𝑁 ∈ Even ∧ ( 𝑁 − 2 ) = ( 𝑝 + 𝑞 ) ) → 𝑁 = ( ( 𝑁 − 2 ) + 2 ) )
38 simpr ⊢ ( ( 𝑁 ∈ Even ∧ ( 𝑁 − 2 ) = ( 𝑝 + 𝑞 ) ) → ( 𝑁 − 2 ) = ( 𝑝 + 𝑞 ) )
39 38 oveq1d ⊢ ( ( 𝑁 ∈ Even ∧ ( 𝑁 − 2 ) = ( 𝑝 + 𝑞 ) ) → ( ( 𝑁 − 2 ) + 2 ) = ( ( 𝑝 + 𝑞 ) + 2 ) )
40 37 39 eqtrd ⊢ ( ( 𝑁 ∈ Even ∧ ( 𝑁 − 2 ) = ( 𝑝 + 𝑞 ) ) → 𝑁 = ( ( 𝑝 + 𝑞 ) + 2 ) )
41 28 31 40 rspcedvd ⊢ ( ( 𝑁 ∈ Even ∧ ( 𝑁 − 2 ) = ( 𝑝 + 𝑞 ) ) → ∃ 𝑟 ∈ ℙ 𝑁 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) )
42 41 ex ⊢ ( 𝑁 ∈ Even → ( ( 𝑁 − 2 ) = ( 𝑝 + 𝑞 ) → ∃ 𝑟 ∈ ℙ 𝑁 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
43 42 reximdv ⊢ ( 𝑁 ∈ Even → ( ∃ 𝑞 ∈ ℙ ( 𝑁 − 2 ) = ( 𝑝 + 𝑞 ) → ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑁 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
44 43 reximdv ⊢ ( 𝑁 ∈ Even → ( ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑁 − 2 ) = ( 𝑝 + 𝑞 ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑁 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
45 44 imim2d ⊢ ( 𝑁 ∈ Even → ( ( 2 < ( 𝑁 − 2 ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑁 − 2 ) = ( 𝑝 + 𝑞 ) ) → ( 2 < ( 𝑁 − 2 ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑁 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) )
46 26 45 syl9r ⊢ ( 𝑁 ∈ Even → ( ( 𝑁 − 2 ) ∈ Even → ( ∀ 𝑛 ∈ Even ( 2 < 𝑛 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) → ( 2 < ( 𝑁 − 2 ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑁 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) ) )
47 21 46 mpd ⊢ ( 𝑁 ∈ Even → ( ∀ 𝑛 ∈ Even ( 2 < 𝑛 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) → ( 2 < ( 𝑁 − 2 ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑁 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) )
48 47 adantr ⊢ ( ( 𝑁 ∈ Even ∧ 6 ≤ 𝑁 ) → ( ∀ 𝑛 ∈ Even ( 2 < 𝑛 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) → ( 2 < ( 𝑁 − 2 ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑁 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) )
49 18 48 mpid ⊢ ( ( 𝑁 ∈ Even ∧ 6 ≤ 𝑁 ) → ( ∀ 𝑛 ∈ Even ( 2 < 𝑛 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑁 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
50 1 49 syl5com ⊢ ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ( ( 𝑁 ∈ Even ∧ 6 ≤ 𝑁 ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑁 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )