Metamath Proof Explorer

Theorem sbgoldbwt

Description: If the strong binary Goldbach conjecture is valid, then the (weak) ternary Goldbach conjecture holds, too. (Contributed by AV, 20-Jul-2020)

Ref Expression
Assertion sbgoldbwt ⊢ ∀ n ∈ Even 4 < n → n ∈ GoldbachEven → ∀ m ∈ Odd 5 < m → m ∈ GoldbachOddW

Proof

Step Hyp Ref Expression
1 oddz ⊢ m ∈ Odd → m ∈ ℤ
2 5nn ⊢ 5 ∈ ℕ
3 2 nnzi ⊢ 5 ∈ ℤ
4 zltp1le ⊢ 5 ∈ ℤ ∧ m ∈ ℤ → 5 < m ↔ 5 + 1 ≤ m
5 3 4 mpan ⊢ m ∈ ℤ → 5 < m ↔ 5 + 1 ≤ m
6 5p1e6 ⊢ 5 + 1 = 6
7 6 breq1i ⊢ 5 + 1 ≤ m ↔ 6 ≤ m
8 6re ⊢ 6 ∈ ℝ
9 8 a1i ⊢ m ∈ ℤ → 6 ∈ ℝ
10 zre ⊢ m ∈ ℤ → m ∈ ℝ
11 9 10 leloed ⊢ m ∈ ℤ → 6 ≤ m ↔ 6 < m ∨ 6 = m
12 7 11 bitrid ⊢ m ∈ ℤ → 5 + 1 ≤ m ↔ 6 < m ∨ 6 = m
13 6nn ⊢ 6 ∈ ℕ
14 13 nnzi ⊢ 6 ∈ ℤ
15 zltp1le ⊢ 6 ∈ ℤ ∧ m ∈ ℤ → 6 < m ↔ 6 + 1 ≤ m
16 14 15 mpan ⊢ m ∈ ℤ → 6 < m ↔ 6 + 1 ≤ m
17 6p1e7 ⊢ 6 + 1 = 7
18 17 breq1i ⊢ 6 + 1 ≤ m ↔ 7 ≤ m
19 7re ⊢ 7 ∈ ℝ
20 19 a1i ⊢ m ∈ ℤ → 7 ∈ ℝ
21 20 10 leloed ⊢ m ∈ ℤ → 7 ≤ m ↔ 7 < m ∨ 7 = m
22 18 21 bitrid ⊢ m ∈ ℤ → 6 + 1 ≤ m ↔ 7 < m ∨ 7 = m
23 simpr ⊢ 7 < m ∧ m ∈ ℤ ∧ m ∈ Odd → m ∈ Odd
24 3odd ⊢ 3 ∈ Odd
25 23 24 jctir ⊢ 7 < m ∧ m ∈ ℤ ∧ m ∈ Odd → m ∈ Odd ∧ 3 ∈ Odd
26 omoeALTV ⊢ m ∈ Odd ∧ 3 ∈ Odd → m − 3 ∈ Even
27 breq2 ⊢ n = m − 3 → 4 < n ↔ 4 < m − 3
28 eleq1 ⊢ n = m − 3 → n ∈ GoldbachEven ↔ m − 3 ∈ GoldbachEven
29 27 28 imbi12d ⊢ n = m − 3 → 4 < n → n ∈ GoldbachEven ↔ 4 < m − 3 → m − 3 ∈ GoldbachEven
30 29 rspcv ⊢ m − 3 ∈ Even → ∀ n ∈ Even 4 < n → n ∈ GoldbachEven → 4 < m − 3 → m − 3 ∈ GoldbachEven
31 25 26 30 3syl ⊢ 7 < m ∧ m ∈ ℤ ∧ m ∈ Odd → ∀ n ∈ Even 4 < n → n ∈ GoldbachEven → 4 < m − 3 → m − 3 ∈ GoldbachEven
32 4p3e7 ⊢ 4 + 3 = 7
33 32 eqcomi ⊢ 7 = 4 + 3
34 33 breq1i ⊢ 7 < m ↔ 4 + 3 < m
35 4re ⊢ 4 ∈ ℝ
36 35 a1i ⊢ m ∈ ℤ → 4 ∈ ℝ
37 3re ⊢ 3 ∈ ℝ
38 37 a1i ⊢ m ∈ ℤ → 3 ∈ ℝ
39 ltaddsub ⊢ 4 ∈ ℝ ∧ 3 ∈ ℝ ∧ m ∈ ℝ → 4 + 3 < m ↔ 4 < m − 3
40 39 biimpd ⊢ 4 ∈ ℝ ∧ 3 ∈ ℝ ∧ m ∈ ℝ → 4 + 3 < m → 4 < m − 3
41 36 38 10 40 syl3anc ⊢ m ∈ ℤ → 4 + 3 < m → 4 < m − 3
42 34 41 biimtrid ⊢ m ∈ ℤ → 7 < m → 4 < m − 3
43 42 impcom ⊢ 7 < m ∧ m ∈ ℤ → 4 < m − 3
44 43 adantr ⊢ 7 < m ∧ m ∈ ℤ ∧ m ∈ Odd → 4 < m − 3
45 pm2.27 ⊢ 4 < m − 3 → 4 < m − 3 → m − 3 ∈ GoldbachEven → m − 3 ∈ GoldbachEven
46 44 45 syl ⊢ 7 < m ∧ m ∈ ℤ ∧ m ∈ Odd → 4 < m − 3 → m − 3 ∈ GoldbachEven → m − 3 ∈ GoldbachEven
47 isgbe ⊢ m − 3 ∈ GoldbachEven ↔ m − 3 ∈ Even ∧ ∃ p ∈ ℙ ∃ q ∈ ℙ p ∈ Odd ∧ q ∈ Odd ∧ m − 3 = p + q
48 3prm ⊢ 3 ∈ ℙ
49 48 a1i ⊢ m ∈ ℤ → 3 ∈ ℙ
50 zcn ⊢ m ∈ ℤ → m ∈ ℂ
51 3cn ⊢ 3 ∈ ℂ
52 50 51 jctir ⊢ m ∈ ℤ → m ∈ ℂ ∧ 3 ∈ ℂ
53 npcan ⊢ m ∈ ℂ ∧ 3 ∈ ℂ → m - 3 + 3 = m
54 53 eqcomd ⊢ m ∈ ℂ ∧ 3 ∈ ℂ → m = m - 3 + 3
55 52 54 syl ⊢ m ∈ ℤ → m = m - 3 + 3
56 oveq2 ⊢ 3 = r → m - 3 + 3 = m - 3 + r
57 56 eqcoms ⊢ r = 3 → m - 3 + 3 = m - 3 + r
58 55 57 sylan9eq ⊢ m ∈ ℤ ∧ r = 3 → m = m - 3 + r
59 49 58 rspcedeqvd ⊢ m ∈ ℤ → ∃ r ∈ ℙ m = m - 3 + r
60 oveq1 ⊢ m − 3 = p + q → m - 3 + r = p + q + r
61 60 eqeq2d ⊢ m − 3 = p + q → m = m - 3 + r ↔ m = p + q + r
62 61 rexbidv ⊢ m − 3 = p + q → ∃ r ∈ ℙ m = m - 3 + r ↔ ∃ r ∈ ℙ m = p + q + r
63 59 62 imbitrid ⊢ m − 3 = p + q → m ∈ ℤ → ∃ r ∈ ℙ m = p + q + r
64 63 3ad2ant3 ⊢ p ∈ Odd ∧ q ∈ Odd ∧ m − 3 = p + q → m ∈ ℤ → ∃ r ∈ ℙ m = p + q + r
65 64 com12 ⊢ m ∈ ℤ → p ∈ Odd ∧ q ∈ Odd ∧ m − 3 = p + q → ∃ r ∈ ℙ m = p + q + r
66 65 ad4antlr ⊢ 7 < m ∧ m ∈ ℤ ∧ m ∈ Odd ∧ p ∈ ℙ ∧ q ∈ ℙ → p ∈ Odd ∧ q ∈ Odd ∧ m − 3 = p + q → ∃ r ∈ ℙ m = p + q + r
67 66 reximdva ⊢ 7 < m ∧ m ∈ ℤ ∧ m ∈ Odd ∧ p ∈ ℙ → ∃ q ∈ ℙ p ∈ Odd ∧ q ∈ Odd ∧ m − 3 = p + q → ∃ q ∈ ℙ ∃ r ∈ ℙ m = p + q + r
68 67 reximdva ⊢ 7 < m ∧ m ∈ ℤ ∧ m ∈ Odd → ∃ p ∈ ℙ ∃ q ∈ ℙ p ∈ Odd ∧ q ∈ Odd ∧ m − 3 = p + q → ∃ p ∈ ℙ ∃ q ∈ ℙ ∃ r ∈ ℙ m = p + q + r
69 68 23 jctild ⊢ 7 < m ∧ m ∈ ℤ ∧ m ∈ Odd → ∃ p ∈ ℙ ∃ q ∈ ℙ p ∈ Odd ∧ q ∈ Odd ∧ m − 3 = p + q → m ∈ Odd ∧ ∃ p ∈ ℙ ∃ q ∈ ℙ ∃ r ∈ ℙ m = p + q + r
70 isgbow ⊢ m ∈ GoldbachOddW ↔ m ∈ Odd ∧ ∃ p ∈ ℙ ∃ q ∈ ℙ ∃ r ∈ ℙ m = p + q + r
71 69 70 imbitrrdi ⊢ 7 < m ∧ m ∈ ℤ ∧ m ∈ Odd → ∃ p ∈ ℙ ∃ q ∈ ℙ p ∈ Odd ∧ q ∈ Odd ∧ m − 3 = p + q → m ∈ GoldbachOddW
72 71 adantld ⊢ 7 < m ∧ m ∈ ℤ ∧ m ∈ Odd → m − 3 ∈ Even ∧ ∃ p ∈ ℙ ∃ q ∈ ℙ p ∈ Odd ∧ q ∈ Odd ∧ m − 3 = p + q → m ∈ GoldbachOddW
73 47 72 biimtrid ⊢ 7 < m ∧ m ∈ ℤ ∧ m ∈ Odd → m − 3 ∈ GoldbachEven → m ∈ GoldbachOddW
74 31 46 73 3syld ⊢ 7 < m ∧ m ∈ ℤ ∧ m ∈ Odd → ∀ n ∈ Even 4 < n → n ∈ GoldbachEven → m ∈ GoldbachOddW
75 74 ex ⊢ 7 < m ∧ m ∈ ℤ → m ∈ Odd → ∀ n ∈ Even 4 < n → n ∈ GoldbachEven → m ∈ GoldbachOddW
76 75 com23 ⊢ 7 < m ∧ m ∈ ℤ → ∀ n ∈ Even 4 < n → n ∈ GoldbachEven → m ∈ Odd → m ∈ GoldbachOddW
77 76 ex ⊢ 7 < m → m ∈ ℤ → ∀ n ∈ Even 4 < n → n ∈ GoldbachEven → m ∈ Odd → m ∈ GoldbachOddW
78 7gbow ⊢ 7 ∈ GoldbachOddW
79 eleq1 ⊢ 7 = m → 7 ∈ GoldbachOddW ↔ m ∈ GoldbachOddW
80 78 79 mpbii ⊢ 7 = m → m ∈ GoldbachOddW
81 80 a1d ⊢ 7 = m → m ∈ Odd → m ∈ GoldbachOddW
82 81 a1d ⊢ 7 = m → ∀ n ∈ Even 4 < n → n ∈ GoldbachEven → m ∈ Odd → m ∈ GoldbachOddW
83 82 a1d ⊢ 7 = m → m ∈ ℤ → ∀ n ∈ Even 4 < n → n ∈ GoldbachEven → m ∈ Odd → m ∈ GoldbachOddW
84 77 83 jaoi ⊢ 7 < m ∨ 7 = m → m ∈ ℤ → ∀ n ∈ Even 4 < n → n ∈ GoldbachEven → m ∈ Odd → m ∈ GoldbachOddW
85 84 com12 ⊢ m ∈ ℤ → 7 < m ∨ 7 = m → ∀ n ∈ Even 4 < n → n ∈ GoldbachEven → m ∈ Odd → m ∈ GoldbachOddW
86 22 85 sylbid ⊢ m ∈ ℤ → 6 + 1 ≤ m → ∀ n ∈ Even 4 < n → n ∈ GoldbachEven → m ∈ Odd → m ∈ GoldbachOddW
87 16 86 sylbid ⊢ m ∈ ℤ → 6 < m → ∀ n ∈ Even 4 < n → n ∈ GoldbachEven → m ∈ Odd → m ∈ GoldbachOddW
88 87 com12 ⊢ 6 < m → m ∈ ℤ → ∀ n ∈ Even 4 < n → n ∈ GoldbachEven → m ∈ Odd → m ∈ GoldbachOddW
89 eleq1 ⊢ 6 = m → 6 ∈ Odd ↔ m ∈ Odd
90 6even ⊢ 6 ∈ Even
91 evennodd ⊢ 6 ∈ Even → ¬ 6 ∈ Odd
92 91 pm2.21d ⊢ 6 ∈ Even → 6 ∈ Odd → m ∈ GoldbachOddW
93 90 92 ax-mp ⊢ 6 ∈ Odd → m ∈ GoldbachOddW
94 89 93 biimtrrdi ⊢ 6 = m → m ∈ Odd → m ∈ GoldbachOddW
95 94 a1d ⊢ 6 = m → ∀ n ∈ Even 4 < n → n ∈ GoldbachEven → m ∈ Odd → m ∈ GoldbachOddW
96 95 a1d ⊢ 6 = m → m ∈ ℤ → ∀ n ∈ Even 4 < n → n ∈ GoldbachEven → m ∈ Odd → m ∈ GoldbachOddW
97 88 96 jaoi ⊢ 6 < m ∨ 6 = m → m ∈ ℤ → ∀ n ∈ Even 4 < n → n ∈ GoldbachEven → m ∈ Odd → m ∈ GoldbachOddW
98 97 com12 ⊢ m ∈ ℤ → 6 < m ∨ 6 = m → ∀ n ∈ Even 4 < n → n ∈ GoldbachEven → m ∈ Odd → m ∈ GoldbachOddW
99 12 98 sylbid ⊢ m ∈ ℤ → 5 + 1 ≤ m → ∀ n ∈ Even 4 < n → n ∈ GoldbachEven → m ∈ Odd → m ∈ GoldbachOddW
100 5 99 sylbid ⊢ m ∈ ℤ → 5 < m → ∀ n ∈ Even 4 < n → n ∈ GoldbachEven → m ∈ Odd → m ∈ GoldbachOddW
101 100 com24 ⊢ m ∈ ℤ → m ∈ Odd → ∀ n ∈ Even 4 < n → n ∈ GoldbachEven → 5 < m → m ∈ GoldbachOddW
102 1 101 mpcom ⊢ m ∈ Odd → ∀ n ∈ Even 4 < n → n ∈ GoldbachEven → 5 < m → m ∈ GoldbachOddW
103 102 impcom ⊢ ∀ n ∈ Even 4 < n → n ∈ GoldbachEven ∧ m ∈ Odd → 5 < m → m ∈ GoldbachOddW
104 103 ralrimiva ⊢ ∀ n ∈ Even 4 < n → n ∈ GoldbachEven → ∀ m ∈ Odd 5 < m → m ∈ GoldbachOddW