Metamath Proof Explorer

Theorem sbgoldbm

Description: If the strong binary Goldbach conjecture is valid, the modern version of the original formulation of the Goldbach conjecture also holds: Every integer greater than 5 can be expressed as the sum of three primes. (Contributed by AV, 24-Dec-2021)

Ref Expression
Assertion sbgoldbm ⊢ ∀ n ∈ Even 4 < n → n ∈ GoldbachEven → ∀ n ∈ ℤ ≥ 6 ∃ p ∈ ℙ ∃ q ∈ ℙ ∃ r ∈ ℙ n = p + q + r

Proof

Step Hyp Ref Expression
1 breq2 ⊢ n = m → 4 < n ↔ 4 < m
2 eleq1w ⊢ n = m → n ∈ GoldbachEven ↔ m ∈ GoldbachEven
3 1 2 imbi12d ⊢ n = m → 4 < n → n ∈ GoldbachEven ↔ 4 < m → m ∈ GoldbachEven
4 3 cbvralvw ⊢ ∀ n ∈ Even 4 < n → n ∈ GoldbachEven ↔ ∀ m ∈ Even 4 < m → m ∈ GoldbachEven
5 eluz2 ⊢ n ∈ ℤ ≥ 6 ↔ 6 ∈ ℤ ∧ n ∈ ℤ ∧ 6 ≤ n
6 zeoALTV ⊢ n ∈ ℤ → n ∈ Even ∨ n ∈ Odd
7 sgoldbeven3prm ⊢ ∀ m ∈ Even 4 < m → m ∈ GoldbachEven → n ∈ Even ∧ 6 ≤ n → ∃ p ∈ ℙ ∃ q ∈ ℙ ∃ r ∈ ℙ n = p + q + r
8 7 expdcom ⊢ n ∈ Even → 6 ≤ n → ∀ m ∈ Even 4 < m → m ∈ GoldbachEven → ∃ p ∈ ℙ ∃ q ∈ ℙ ∃ r ∈ ℙ n = p + q + r
9 sbgoldbwt ⊢ ∀ m ∈ Even 4 < m → m ∈ GoldbachEven → ∀ n ∈ Odd 5 < n → n ∈ GoldbachOddW
10 rspa ⊢ ∀ n ∈ Odd 5 < n → n ∈ GoldbachOddW ∧ n ∈ Odd → 5 < n → n ∈ GoldbachOddW
11 df-6 ⊢ 6 = 5 + 1
12 11 breq1i ⊢ 6 ≤ n ↔ 5 + 1 ≤ n
13 5nn ⊢ 5 ∈ ℕ
14 13 nnzi ⊢ 5 ∈ ℤ
15 oddz ⊢ n ∈ Odd → n ∈ ℤ
16 zltp1le ⊢ 5 ∈ ℤ ∧ n ∈ ℤ → 5 < n ↔ 5 + 1 ≤ n
17 14 15 16 sylancr ⊢ n ∈ Odd → 5 < n ↔ 5 + 1 ≤ n
18 17 biimprd ⊢ n ∈ Odd → 5 + 1 ≤ n → 5 < n
19 12 18 biimtrid ⊢ n ∈ Odd → 6 ≤ n → 5 < n
20 19 imp ⊢ n ∈ Odd ∧ 6 ≤ n → 5 < n
21 isgbow ⊢ n ∈ GoldbachOddW ↔ n ∈ Odd ∧ ∃ p ∈ ℙ ∃ q ∈ ℙ ∃ r ∈ ℙ n = p + q + r
22 21 simprbi ⊢ n ∈ GoldbachOddW → ∃ p ∈ ℙ ∃ q ∈ ℙ ∃ r ∈ ℙ n = p + q + r
23 22 a1i ⊢ n ∈ Odd ∧ 6 ≤ n → n ∈ GoldbachOddW → ∃ p ∈ ℙ ∃ q ∈ ℙ ∃ r ∈ ℙ n = p + q + r
24 20 23 embantd ⊢ n ∈ Odd ∧ 6 ≤ n → 5 < n → n ∈ GoldbachOddW → ∃ p ∈ ℙ ∃ q ∈ ℙ ∃ r ∈ ℙ n = p + q + r
25 24 ex ⊢ n ∈ Odd → 6 ≤ n → 5 < n → n ∈ GoldbachOddW → ∃ p ∈ ℙ ∃ q ∈ ℙ ∃ r ∈ ℙ n = p + q + r
26 25 com23 ⊢ n ∈ Odd → 5 < n → n ∈ GoldbachOddW → 6 ≤ n → ∃ p ∈ ℙ ∃ q ∈ ℙ ∃ r ∈ ℙ n = p + q + r
27 26 adantl ⊢ ∀ n ∈ Odd 5 < n → n ∈ GoldbachOddW ∧ n ∈ Odd → 5 < n → n ∈ GoldbachOddW → 6 ≤ n → ∃ p ∈ ℙ ∃ q ∈ ℙ ∃ r ∈ ℙ n = p + q + r
28 10 27 mpd ⊢ ∀ n ∈ Odd 5 < n → n ∈ GoldbachOddW ∧ n ∈ Odd → 6 ≤ n → ∃ p ∈ ℙ ∃ q ∈ ℙ ∃ r ∈ ℙ n = p + q + r
29 28 ex ⊢ ∀ n ∈ Odd 5 < n → n ∈ GoldbachOddW → n ∈ Odd → 6 ≤ n → ∃ p ∈ ℙ ∃ q ∈ ℙ ∃ r ∈ ℙ n = p + q + r
30 29 com23 ⊢ ∀ n ∈ Odd 5 < n → n ∈ GoldbachOddW → 6 ≤ n → n ∈ Odd → ∃ p ∈ ℙ ∃ q ∈ ℙ ∃ r ∈ ℙ n = p + q + r
31 9 30 syl ⊢ ∀ m ∈ Even 4 < m → m ∈ GoldbachEven → 6 ≤ n → n ∈ Odd → ∃ p ∈ ℙ ∃ q ∈ ℙ ∃ r ∈ ℙ n = p + q + r
32 31 com13 ⊢ n ∈ Odd → 6 ≤ n → ∀ m ∈ Even 4 < m → m ∈ GoldbachEven → ∃ p ∈ ℙ ∃ q ∈ ℙ ∃ r ∈ ℙ n = p + q + r
33 8 32 jaoi ⊢ n ∈ Even ∨ n ∈ Odd → 6 ≤ n → ∀ m ∈ Even 4 < m → m ∈ GoldbachEven → ∃ p ∈ ℙ ∃ q ∈ ℙ ∃ r ∈ ℙ n = p + q + r
34 6 33 syl ⊢ n ∈ ℤ → 6 ≤ n → ∀ m ∈ Even 4 < m → m ∈ GoldbachEven → ∃ p ∈ ℙ ∃ q ∈ ℙ ∃ r ∈ ℙ n = p + q + r
35 34 imp ⊢ n ∈ ℤ ∧ 6 ≤ n → ∀ m ∈ Even 4 < m → m ∈ GoldbachEven → ∃ p ∈ ℙ ∃ q ∈ ℙ ∃ r ∈ ℙ n = p + q + r
36 35 3adant1 ⊢ 6 ∈ ℤ ∧ n ∈ ℤ ∧ 6 ≤ n → ∀ m ∈ Even 4 < m → m ∈ GoldbachEven → ∃ p ∈ ℙ ∃ q ∈ ℙ ∃ r ∈ ℙ n = p + q + r
37 5 36 sylbi ⊢ n ∈ ℤ ≥ 6 → ∀ m ∈ Even 4 < m → m ∈ GoldbachEven → ∃ p ∈ ℙ ∃ q ∈ ℙ ∃ r ∈ ℙ n = p + q + r
38 37 impcom ⊢ ∀ m ∈ Even 4 < m → m ∈ GoldbachEven ∧ n ∈ ℤ ≥ 6 → ∃ p ∈ ℙ ∃ q ∈ ℙ ∃ r ∈ ℙ n = p + q + r
39 38 ralrimiva ⊢ ∀ m ∈ Even 4 < m → m ∈ GoldbachEven → ∀ n ∈ ℤ ≥ 6 ∃ p ∈ ℙ ∃ q ∈ ℙ ∃ r ∈ ℙ n = p + q + r
40 4 39 sylbi ⊢ ∀ n ∈ Even 4 < n → n ∈ GoldbachEven → ∀ n ∈ ℤ ≥ 6 ∃ p ∈ ℙ ∃ q ∈ ℙ ∃ r ∈ ℙ n = p + q + r