Metamath Proof Explorer

Theorem tgblthelfgott

Description: The ternary Goldbach conjecture is valid for all odd numbers less than 8.8 x 10^30 (actually 8.875694 x 10^30, see section 1.2.2 in Helfgott p. 4, using bgoldbachlt , ax-hgprmladder and bgoldbtbnd . (Contributed by AV, 4-Aug-2020) (Revised by AV, 9-Sep-2021)

Ref Expression
Assertion tgblthelfgott ⊢N∈Odd∧7<N∧N<88⁢1029→N∈GoldbachOdd

Proof

Step Hyp Ref Expression
1 ax-hgprmladder ⊢∃d∈ℤ≥3∃f∈RePart⁡df⁡0=7∧f⁡1=13∧f⁡d=89⁢1029∧∀i∈0..^df⁡i∈ℙ∖2∧f⁡i+1−f⁡i<4⁢1018−4∧4<f⁡i+1−f⁡i
2 1nn0 ⊢1∈ℕ0
3 1nn ⊢1∈ℕ
4 2 3 decnncl ⊢11∈ℕ
5 4 nnzi ⊢11∈ℤ
6 8nn0 ⊢8∈ℕ0
7 8nn ⊢8∈ℕ
8 6 7 decnncl ⊢88∈ℕ
9 10nn ⊢10∈ℕ
10 2nn0 ⊢2∈ℕ0
11 9nn ⊢9∈ℕ
12 10 11 decnncl ⊢29∈ℕ
13 12 nnnn0i ⊢29∈ℕ0
14 nnexpcl ⊢10∈ℕ∧29∈ℕ0→1029∈ℕ
15 9 13 14 mp2an ⊢1029∈ℕ
16 8 15 nnmulcli ⊢88⁢1029∈ℕ
17 16 nnzi ⊢88⁢1029∈ℤ
18 1re ⊢1∈ℝ
19 8 nnrei ⊢88∈ℝ
20 18 19 pm3.2i ⊢1∈ℝ∧88∈ℝ
21 0le1 ⊢0≤1
22 1lt10 ⊢1<10
23 7 6 2 22 declti ⊢1<88
24 21 23 pm3.2i ⊢0≤1∧1<88
25 nnexpcl ⊢10∈ℕ∧1∈ℕ0→101∈ℕ
26 9 2 25 mp2an ⊢101∈ℕ
27 26 nnrei ⊢101∈ℝ
28 15 nnrei ⊢1029∈ℝ
29 27 28 pm3.2i ⊢101∈ℝ∧1029∈ℝ
30 0re ⊢0∈ℝ
31 10re ⊢10∈ℝ
32 10pos ⊢0<10
33 30 31 32 ltleii ⊢0≤10
34 9 nncni ⊢10∈ℂ
35 exp1 ⊢10∈ℂ→101=10
36 34 35 ax-mp ⊢101=10
37 33 36 breqtrri ⊢0≤101
38 1z ⊢1∈ℤ
39 12 nnzi ⊢29∈ℤ
40 31 38 39 3pm3.2i ⊢10∈ℝ∧1∈ℤ∧29∈ℤ
41 2nn ⊢2∈ℕ
42 9nn0 ⊢9∈ℕ0
43 41 42 2 22 declti ⊢1<29
44 22 43 pm3.2i ⊢1<10∧1<29
45 ltexp2a ⊢10∈ℝ∧1∈ℤ∧29∈ℤ∧1<10∧1<29→101<1029
46 40 44 45 mp2an ⊢101<1029
47 37 46 pm3.2i ⊢0≤101∧101<1029
48 ltmul12a ⊢1∈ℝ∧88∈ℝ∧0≤1∧1<88∧101∈ℝ∧1029∈ℝ∧0≤101∧101<1029→1⁢101<88⁢1029
49 20 24 29 47 48 mp4an ⊢1⁢101<88⁢1029
50 26 nnzi ⊢101∈ℤ
51 zmulcl ⊢1∈ℤ∧101∈ℤ→1⁢101∈ℤ
52 38 50 51 mp2an ⊢1⁢101∈ℤ
53 zltp1le ⊢1⁢101∈ℤ∧88⁢1029∈ℤ→1⁢101<88⁢1029↔1⁢101+1≤88⁢1029
54 52 17 53 mp2an ⊢1⁢101<88⁢1029↔1⁢101+1≤88⁢1029
55 1t10e1p1e11 ⊢11=1⁢101+1
56 55 eqcomi ⊢1⁢101+1=11
57 56 breq1i ⊢1⁢101+1≤88⁢1029↔11≤88⁢1029
58 54 57 bitri ⊢1⁢101<88⁢1029↔11≤88⁢1029
59 49 58 mpbi ⊢11≤88⁢1029
60 eluz2 ⊢88⁢1029∈ℤ≥11↔11∈ℤ∧88⁢1029∈ℤ∧11≤88⁢1029
61 5 17 59 60 mpbir3an ⊢88⁢1029∈ℤ≥11
62 61 a1i ⊢d∈ℤ≥3∧f∈RePart⁡d∧f⁡0=7∧f⁡1=13∧f⁡d=89⁢1029∧∀i∈0..^df⁡i∈ℙ∖2∧f⁡i+1−f⁡i<4⁢1018−4∧4<f⁡i+1−f⁡i∧N∈Odd∧7<N∧N<88⁢1029→88⁢1029∈ℤ≥11
63 4nn ⊢4∈ℕ
64 2 7 decnncl ⊢18∈ℕ
65 64 nnnn0i ⊢18∈ℕ0
66 nnexpcl ⊢10∈ℕ∧18∈ℕ0→1018∈ℕ
67 9 65 66 mp2an ⊢1018∈ℕ
68 63 67 nnmulcli ⊢4⁢1018∈ℕ
69 68 nnzi ⊢4⁢1018∈ℤ
70 4re ⊢4∈ℝ
71 18 70 pm3.2i ⊢1∈ℝ∧4∈ℝ
72 1lt4 ⊢1<4
73 21 72 pm3.2i ⊢0≤1∧1<4
74 67 nnrei ⊢1018∈ℝ
75 27 74 pm3.2i ⊢101∈ℝ∧1018∈ℝ
76 64 nnzi ⊢18∈ℤ
77 31 38 76 3pm3.2i ⊢10∈ℝ∧1∈ℤ∧18∈ℤ
78 3 6 2 22 declti ⊢1<18
79 22 78 pm3.2i ⊢1<10∧1<18
80 ltexp2a ⊢10∈ℝ∧1∈ℤ∧18∈ℤ∧1<10∧1<18→101<1018
81 77 79 80 mp2an ⊢101<1018
82 37 81 pm3.2i ⊢0≤101∧101<1018
83 ltmul12a ⊢1∈ℝ∧4∈ℝ∧0≤1∧1<4∧101∈ℝ∧1018∈ℝ∧0≤101∧101<1018→1⁢101<4⁢1018
84 71 73 75 82 83 mp4an ⊢1⁢101<4⁢1018
85 4z ⊢4∈ℤ
86 67 nnzi ⊢1018∈ℤ
87 zmulcl ⊢4∈ℤ∧1018∈ℤ→4⁢1018∈ℤ
88 85 86 87 mp2an ⊢4⁢1018∈ℤ
89 zltp1le ⊢1⁢101∈ℤ∧4⁢1018∈ℤ→1⁢101<4⁢1018↔1⁢101+1≤4⁢1018
90 52 88 89 mp2an ⊢1⁢101<4⁢1018↔1⁢101+1≤4⁢1018
91 56 breq1i ⊢1⁢101+1≤4⁢1018↔11≤4⁢1018
92 90 91 bitri ⊢1⁢101<4⁢1018↔11≤4⁢1018
93 84 92 mpbi ⊢11≤4⁢1018
94 eluz2 ⊢4⁢1018∈ℤ≥11↔11∈ℤ∧4⁢1018∈ℤ∧11≤4⁢1018
95 5 69 93 94 mpbir3an ⊢4⁢1018∈ℤ≥11
96 95 a1i ⊢d∈ℤ≥3∧f∈RePart⁡d∧f⁡0=7∧f⁡1=13∧f⁡d=89⁢1029∧∀i∈0..^df⁡i∈ℙ∖2∧f⁡i+1−f⁡i<4⁢1018−4∧4<f⁡i+1−f⁡i∧N∈Odd∧7<N∧N<88⁢1029→4⁢1018∈ℤ≥11
97 simpl ⊢n∈Even∧4<n∧n<4⁢1018→n∈Even
98 simprl ⊢n∈Even∧4<n∧n<4⁢1018→4<n
99 evenz ⊢n∈Even→n∈ℤ
100 99 zred ⊢n∈Even→n∈ℝ
101 68 nnrei ⊢4⁢1018∈ℝ
102 ltle ⊢n∈ℝ∧4⁢1018∈ℝ→n<4⁢1018→n≤4⁢1018
103 100 101 102 sylancl ⊢n∈Even→n<4⁢1018→n≤4⁢1018
104 103 a1d ⊢n∈Even→4<n→n<4⁢1018→n≤4⁢1018
105 104 imp32 ⊢n∈Even∧4<n∧n<4⁢1018→n≤4⁢1018
106 ax-bgbltosilva ⊢n∈Even∧4<n∧n≤4⁢1018→n∈GoldbachEven
107 97 98 105 106 syl3anc ⊢n∈Even∧4<n∧n<4⁢1018→n∈GoldbachEven
108 107 ex ⊢n∈Even→4<n∧n<4⁢1018→n∈GoldbachEven
109 108 a1i ⊢d∈ℤ≥3∧f∈RePart⁡d∧f⁡0=7∧f⁡1=13∧f⁡d=89⁢1029∧∀i∈0..^df⁡i∈ℙ∖2∧f⁡i+1−f⁡i<4⁢1018−4∧4<f⁡i+1−f⁡i∧N∈Odd∧7<N∧N<88⁢1029→n∈Even→4<n∧n<4⁢1018→n∈GoldbachEven
110 109 ralrimiv ⊢d∈ℤ≥3∧f∈RePart⁡d∧f⁡0=7∧f⁡1=13∧f⁡d=89⁢1029∧∀i∈0..^df⁡i∈ℙ∖2∧f⁡i+1−f⁡i<4⁢1018−4∧4<f⁡i+1−f⁡i∧N∈Odd∧7<N∧N<88⁢1029→∀n∈Even4<n∧n<4⁢1018→n∈GoldbachEven
111 simpl ⊢d∈ℤ≥3∧f∈RePart⁡d→d∈ℤ≥3
112 111 ad2antrr ⊢d∈ℤ≥3∧f∈RePart⁡d∧f⁡0=7∧f⁡1=13∧f⁡d=89⁢1029∧∀i∈0..^df⁡i∈ℙ∖2∧f⁡i+1−f⁡i<4⁢1018−4∧4<f⁡i+1−f⁡i∧N∈Odd∧7<N∧N<88⁢1029→d∈ℤ≥3
113 simpr ⊢d∈ℤ≥3∧f∈RePart⁡d→f∈RePart⁡d
114 113 ad2antrr ⊢d∈ℤ≥3∧f∈RePart⁡d∧f⁡0=7∧f⁡1=13∧f⁡d=89⁢1029∧∀i∈0..^df⁡i∈ℙ∖2∧f⁡i+1−f⁡i<4⁢1018−4∧4<f⁡i+1−f⁡i∧N∈Odd∧7<N∧N<88⁢1029→f∈RePart⁡d
115 simpr ⊢f⁡0=7∧f⁡1=13∧f⁡d=89⁢1029∧∀i∈0..^df⁡i∈ℙ∖2∧f⁡i+1−f⁡i<4⁢1018−4∧4<f⁡i+1−f⁡i→∀i∈0..^df⁡i∈ℙ∖2∧f⁡i+1−f⁡i<4⁢1018−4∧4<f⁡i+1−f⁡i
116 115 ad2antlr ⊢d∈ℤ≥3∧f∈RePart⁡d∧f⁡0=7∧f⁡1=13∧f⁡d=89⁢1029∧∀i∈0..^df⁡i∈ℙ∖2∧f⁡i+1−f⁡i<4⁢1018−4∧4<f⁡i+1−f⁡i∧N∈Odd∧7<N∧N<88⁢1029→∀i∈0..^df⁡i∈ℙ∖2∧f⁡i+1−f⁡i<4⁢1018−4∧4<f⁡i+1−f⁡i
117 simpl1 ⊢f⁡0=7∧f⁡1=13∧f⁡d=89⁢1029∧∀i∈0..^df⁡i∈ℙ∖2∧f⁡i+1−f⁡i<4⁢1018−4∧4<f⁡i+1−f⁡i→f⁡0=7
118 117 ad2antlr ⊢d∈ℤ≥3∧f∈RePart⁡d∧f⁡0=7∧f⁡1=13∧f⁡d=89⁢1029∧∀i∈0..^df⁡i∈ℙ∖2∧f⁡i+1−f⁡i<4⁢1018−4∧4<f⁡i+1−f⁡i∧N∈Odd∧7<N∧N<88⁢1029→f⁡0=7
119 simpl2 ⊢f⁡0=7∧f⁡1=13∧f⁡d=89⁢1029∧∀i∈0..^df⁡i∈ℙ∖2∧f⁡i+1−f⁡i<4⁢1018−4∧4<f⁡i+1−f⁡i→f⁡1=13
120 119 ad2antlr ⊢d∈ℤ≥3∧f∈RePart⁡d∧f⁡0=7∧f⁡1=13∧f⁡d=89⁢1029∧∀i∈0..^df⁡i∈ℙ∖2∧f⁡i+1−f⁡i<4⁢1018−4∧4<f⁡i+1−f⁡i∧N∈Odd∧7<N∧N<88⁢1029→f⁡1=13
121 6 11 decnncl ⊢89∈ℕ
122 121 nnrei ⊢89∈ℝ
123 15 nngt0i ⊢0<1029
124 28 123 pm3.2i ⊢1029∈ℝ∧0<1029
125 19 122 124 3pm3.2i ⊢88∈ℝ∧89∈ℝ∧1029∈ℝ∧0<1029
126 8lt9 ⊢8<9
127 6 6 11 126 declt ⊢88<89
128 ltmul1a ⊢88∈ℝ∧89∈ℝ∧1029∈ℝ∧0<1029∧88<89→88⁢1029<89⁢1029
129 125 127 128 mp2an ⊢88⁢1029<89⁢1029
130 breq2 ⊢f⁡d=89⁢1029→88⁢1029<f⁡d↔88⁢1029<89⁢1029
131 129 130 mpbiri ⊢f⁡d=89⁢1029→88⁢1029<f⁡d
132 131 3ad2ant3 ⊢f⁡0=7∧f⁡1=13∧f⁡d=89⁢1029→88⁢1029<f⁡d
133 132 adantr ⊢f⁡0=7∧f⁡1=13∧f⁡d=89⁢1029∧∀i∈0..^df⁡i∈ℙ∖2∧f⁡i+1−f⁡i<4⁢1018−4∧4<f⁡i+1−f⁡i→88⁢1029<f⁡d
134 133 ad2antlr ⊢d∈ℤ≥3∧f∈RePart⁡d∧f⁡0=7∧f⁡1=13∧f⁡d=89⁢1029∧∀i∈0..^df⁡i∈ℙ∖2∧f⁡i+1−f⁡i<4⁢1018−4∧4<f⁡i+1−f⁡i∧N∈Odd∧7<N∧N<88⁢1029→88⁢1029<f⁡d
135 121 15 nnmulcli ⊢89⁢1029∈ℕ
136 135 nnrei ⊢89⁢1029∈ℝ
137 eleq1 ⊢f⁡d=89⁢1029→f⁡d∈ℝ↔89⁢1029∈ℝ
138 136 137 mpbiri ⊢f⁡d=89⁢1029→f⁡d∈ℝ
139 138 3ad2ant3 ⊢f⁡0=7∧f⁡1=13∧f⁡d=89⁢1029→f⁡d∈ℝ
140 139 adantr ⊢f⁡0=7∧f⁡1=13∧f⁡d=89⁢1029∧∀i∈0..^df⁡i∈ℙ∖2∧f⁡i+1−f⁡i<4⁢1018−4∧4<f⁡i+1−f⁡i→f⁡d∈ℝ
141 140 ad2antlr ⊢d∈ℤ≥3∧f∈RePart⁡d∧f⁡0=7∧f⁡1=13∧f⁡d=89⁢1029∧∀i∈0..^df⁡i∈ℙ∖2∧f⁡i+1−f⁡i<4⁢1018−4∧4<f⁡i+1−f⁡i∧N∈Odd∧7<N∧N<88⁢1029→f⁡d∈ℝ
142 62 96 110 112 114 116 118 120 134 141 bgoldbtbnd ⊢d∈ℤ≥3∧f∈RePart⁡d∧f⁡0=7∧f⁡1=13∧f⁡d=89⁢1029∧∀i∈0..^df⁡i∈ℙ∖2∧f⁡i+1−f⁡i<4⁢1018−4∧4<f⁡i+1−f⁡i∧N∈Odd∧7<N∧N<88⁢1029→∀n∈Odd7<n∧n<88⁢1029→n∈GoldbachOdd
143 142 exp31 ⊢d∈ℤ≥3∧f∈RePart⁡d→f⁡0=7∧f⁡1=13∧f⁡d=89⁢1029∧∀i∈0..^df⁡i∈ℙ∖2∧f⁡i+1−f⁡i<4⁢1018−4∧4<f⁡i+1−f⁡i→N∈Odd∧7<N∧N<88⁢1029→∀n∈Odd7<n∧n<88⁢1029→n∈GoldbachOdd
144 143 rexlimivv ⊢∃d∈ℤ≥3∃f∈RePart⁡df⁡0=7∧f⁡1=13∧f⁡d=89⁢1029∧∀i∈0..^df⁡i∈ℙ∖2∧f⁡i+1−f⁡i<4⁢1018−4∧4<f⁡i+1−f⁡i→N∈Odd∧7<N∧N<88⁢1029→∀n∈Odd7<n∧n<88⁢1029→n∈GoldbachOdd
145 breq2 ⊢n=N→7<n↔7<N
146 breq1 ⊢n=N→n<88⁢1029↔N<88⁢1029
147 145 146 anbi12d ⊢n=N→7<n∧n<88⁢1029↔7<N∧N<88⁢1029
148 eleq1 ⊢n=N→n∈GoldbachOdd↔N∈GoldbachOdd
149 147 148 imbi12d ⊢n=N→7<n∧n<88⁢1029→n∈GoldbachOdd↔7<N∧N<88⁢1029→N∈GoldbachOdd
150 149 rspcv ⊢N∈Odd→∀n∈Odd7<n∧n<88⁢1029→n∈GoldbachOdd→7<N∧N<88⁢1029→N∈GoldbachOdd
151 150 com23 ⊢N∈Odd→7<N∧N<88⁢1029→∀n∈Odd7<n∧n<88⁢1029→n∈GoldbachOdd→N∈GoldbachOdd
152 151 3impib ⊢N∈Odd∧7<N∧N<88⁢1029→∀n∈Odd7<n∧n<88⁢1029→n∈GoldbachOdd→N∈GoldbachOdd
153 144 152 sylcom ⊢∃d∈ℤ≥3∃f∈RePart⁡df⁡0=7∧f⁡1=13∧f⁡d=89⁢1029∧∀i∈0..^df⁡i∈ℙ∖2∧f⁡i+1−f⁡i<4⁢1018−4∧4<f⁡i+1−f⁡i→N∈Odd∧7<N∧N<88⁢1029→N∈GoldbachOdd
154 1 153 ax-mp ⊢N∈Odd∧7<N∧N<88⁢1029→N∈GoldbachOdd