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 ⊢ ∀ n ∈ Even 4 < n → n ∈ GoldbachEven → N ∈ Even ∧ 6 ≤ N → ∃ p ∈ ℙ ∃ q ∈ ℙ ∃ r ∈ ℙ N = p + q + r

Proof

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