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∈Even4<n→n∈GoldbachEven→∀m∈Odd5<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∈Even4<n→n∈GoldbachEven→4<m−3→m−3∈GoldbachEven
31 25 26 30 3syl ⊢7<m∧m∈ℤ∧m∈Odd→∀n∈Even4<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 rspcedeq2vd ⊢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 syl6ibr ⊢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∈Even4<n→n∈GoldbachEven→m∈GoldbachOddW
75 74 ex ⊢7<m∧m∈ℤ→m∈Odd→∀n∈Even4<n→n∈GoldbachEven→m∈GoldbachOddW
76 75 com23 ⊢7<m∧m∈ℤ→∀n∈Even4<n→n∈GoldbachEven→m∈Odd→m∈GoldbachOddW
77 76 ex ⊢7<m→m∈ℤ→∀n∈Even4<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∈Even4<n→n∈GoldbachEven→m∈Odd→m∈GoldbachOddW
83 82 a1d ⊢7=m→m∈ℤ→∀n∈Even4<n→n∈GoldbachEven→m∈Odd→m∈GoldbachOddW
84 77 83 jaoi ⊢7<m∨7=m→m∈ℤ→∀n∈Even4<n→n∈GoldbachEven→m∈Odd→m∈GoldbachOddW
85 84 com12 ⊢m∈ℤ→7<m∨7=m→∀n∈Even4<n→n∈GoldbachEven→m∈Odd→m∈GoldbachOddW
86 22 85 sylbid ⊢m∈ℤ→6+1≤m→∀n∈Even4<n→n∈GoldbachEven→m∈Odd→m∈GoldbachOddW
87 16 86 sylbid ⊢m∈ℤ→6<m→∀n∈Even4<n→n∈GoldbachEven→m∈Odd→m∈GoldbachOddW
88 87 com12 ⊢6<m→m∈ℤ→∀n∈Even4<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 syl6bir ⊢6=m→m∈Odd→m∈GoldbachOddW
95 94 a1d ⊢6=m→∀n∈Even4<n→n∈GoldbachEven→m∈Odd→m∈GoldbachOddW
96 95 a1d ⊢6=m→m∈ℤ→∀n∈Even4<n→n∈GoldbachEven→m∈Odd→m∈GoldbachOddW
97 88 96 jaoi ⊢6<m∨6=m→m∈ℤ→∀n∈Even4<n→n∈GoldbachEven→m∈Odd→m∈GoldbachOddW
98 97 com12 ⊢m∈ℤ→6<m∨6=m→∀n∈Even4<n→n∈GoldbachEven→m∈Odd→m∈GoldbachOddW
99 12 98 sylbid ⊢m∈ℤ→5+1≤m→∀n∈Even4<n→n∈GoldbachEven→m∈Odd→m∈GoldbachOddW
100 5 99 sylbid ⊢m∈ℤ→5<m→∀n∈Even4<n→n∈GoldbachEven→m∈Odd→m∈GoldbachOddW
101 100 com24 ⊢m∈ℤ→m∈Odd→∀n∈Even4<n→n∈GoldbachEven→5<m→m∈GoldbachOddW
102 1 101 mpcom ⊢m∈Odd→∀n∈Even4<n→n∈GoldbachEven→5<m→m∈GoldbachOddW
103 102 impcom ⊢∀n∈Even4<n→n∈GoldbachEven∧m∈Odd→5<m→m∈GoldbachOddW
104 103 ralrimiva ⊢∀n∈Even4<n→n∈GoldbachEven→∀m∈Odd5<m→m∈GoldbachOddW