Metamath Proof Explorer

Theorem tgoldbachgt

Description: Odd integers greater than ( ; 1 0 ^ ; 2 7 ) have at least a representation as a sum of three odd primes. Final statement in section 7.4 of Helfgott p. 70 , expressed using the set G of odd numbers which can be written as a sum of three odd primes. (Contributed by Thierry Arnoux, 22-Dec-2021)

Ref Expression
Hypotheses tgoldbachgt.o ⊢O=z∈ℤ|¬2∥z
tgoldbachgt.g ⊢G=z∈O|∃p∈ℙ∃q∈ℙ∃r∈ℙp∈O∧q∈O∧r∈O∧z=p+q+r
Assertion tgoldbachgt ⊢∃m∈ℕm≤1027∧∀n∈Om<n→n∈G

Proof

Step Hyp Ref Expression
1 tgoldbachgt.o ⊢O=z∈ℤ|¬2∥z
2 tgoldbachgt.g ⊢G=z∈O|∃p∈ℙ∃q∈ℙ∃r∈ℙp∈O∧q∈O∧r∈O∧z=p+q+r
3 10nn ⊢10∈ℕ
4 2nn0 ⊢2∈ℕ0
5 7nn0 ⊢7∈ℕ0
6 4 5 deccl ⊢27∈ℕ0
7 nnexpcl ⊢10∈ℕ∧27∈ℕ0→1027∈ℕ
8 3 6 7 mp2an ⊢1027∈ℕ
9 8 nnrei ⊢1027∈ℝ
10 9 leidi ⊢1027≤1027
11 simpl ⊢n∈O∧1027<n→n∈O
12 inss2 ⊢O∩ℙ⊆ℙ
13 prmssnn ⊢ℙ⊆ℕ
14 12 13 sstri ⊢O∩ℙ⊆ℕ
15 14 a1i ⊢n∈O∧1027<n∧c∈O∩ℙrepr⁡3n→O∩ℙ⊆ℕ
16 1 eleq2i ⊢n∈O↔n∈z∈ℤ|¬2∥z
17 elrabi ⊢n∈z∈ℤ|¬2∥z→n∈ℤ
18 16 17 sylbi ⊢n∈O→n∈ℤ
19 18 ad2antrr ⊢n∈O∧1027<n∧c∈O∩ℙrepr⁡3n→n∈ℤ
20 3nn0 ⊢3∈ℕ0
21 20 a1i ⊢n∈O∧1027<n∧c∈O∩ℙrepr⁡3n→3∈ℕ0
22 simpr ⊢n∈O∧1027<n∧c∈O∩ℙrepr⁡3n→c∈O∩ℙrepr⁡3n
23 15 19 21 22 reprf ⊢n∈O∧1027<n∧c∈O∩ℙrepr⁡3n→c:0..^3⟶O∩ℙ
24 c0ex ⊢0∈V
25 24 tpid1 ⊢0∈012
26 fzo0to3tp ⊢0..^3=012
27 25 26 eleqtrri ⊢0∈0..^3
28 27 a1i ⊢n∈O∧1027<n∧c∈O∩ℙrepr⁡3n→0∈0..^3
29 23 28 ffvelcdmd ⊢n∈O∧1027<n∧c∈O∩ℙrepr⁡3n→c⁡0∈O∩ℙ
30 29 elin2d ⊢n∈O∧1027<n∧c∈O∩ℙrepr⁡3n→c⁡0∈ℙ
31 1ex ⊢1∈V
32 31 tpid2 ⊢1∈012
33 32 26 eleqtrri ⊢1∈0..^3
34 33 a1i ⊢n∈O∧1027<n∧c∈O∩ℙrepr⁡3n→1∈0..^3
35 23 34 ffvelcdmd ⊢n∈O∧1027<n∧c∈O∩ℙrepr⁡3n→c⁡1∈O∩ℙ
36 35 elin2d ⊢n∈O∧1027<n∧c∈O∩ℙrepr⁡3n→c⁡1∈ℙ
37 2ex ⊢2∈V
38 37 tpid3 ⊢2∈012
39 38 26 eleqtrri ⊢2∈0..^3
40 39 a1i ⊢n∈O∧1027<n∧c∈O∩ℙrepr⁡3n→2∈0..^3
41 23 40 ffvelcdmd ⊢n∈O∧1027<n∧c∈O∩ℙrepr⁡3n→c⁡2∈O∩ℙ
42 41 elin2d ⊢n∈O∧1027<n∧c∈O∩ℙrepr⁡3n→c⁡2∈ℙ
43 29 elin1d ⊢n∈O∧1027<n∧c∈O∩ℙrepr⁡3n→c⁡0∈O
44 35 elin1d ⊢n∈O∧1027<n∧c∈O∩ℙrepr⁡3n→c⁡1∈O
45 41 elin1d ⊢n∈O∧1027<n∧c∈O∩ℙrepr⁡3n→c⁡2∈O
46 43 44 45 3jca ⊢n∈O∧1027<n∧c∈O∩ℙrepr⁡3n→c⁡0∈O∧c⁡1∈O∧c⁡2∈O
47 26 a1i ⊢n∈O∧1027<n∧c∈O∩ℙrepr⁡3n→0..^3=012
48 47 sumeq1d ⊢n∈O∧1027<n∧c∈O∩ℙrepr⁡3n→∑i∈0..^3c⁡i=∑i∈012c⁡i
49 15 19 21 22 reprsum ⊢n∈O∧1027<n∧c∈O∩ℙrepr⁡3n→∑i∈0..^3c⁡i=n
50 fveq2 ⊢i=0→c⁡i=c⁡0
51 fveq2 ⊢i=1→c⁡i=c⁡1
52 fveq2 ⊢i=2→c⁡i=c⁡2
53 14 29 sselid ⊢n∈O∧1027<n∧c∈O∩ℙrepr⁡3n→c⁡0∈ℕ
54 53 nncnd ⊢n∈O∧1027<n∧c∈O∩ℙrepr⁡3n→c⁡0∈ℂ
55 14 35 sselid ⊢n∈O∧1027<n∧c∈O∩ℙrepr⁡3n→c⁡1∈ℕ
56 55 nncnd ⊢n∈O∧1027<n∧c∈O∩ℙrepr⁡3n→c⁡1∈ℂ
57 14 41 sselid ⊢n∈O∧1027<n∧c∈O∩ℙrepr⁡3n→c⁡2∈ℕ
58 57 nncnd ⊢n∈O∧1027<n∧c∈O∩ℙrepr⁡3n→c⁡2∈ℂ
59 54 56 58 3jca ⊢n∈O∧1027<n∧c∈O∩ℙrepr⁡3n→c⁡0∈ℂ∧c⁡1∈ℂ∧c⁡2∈ℂ
60 24 a1i ⊢n∈O∧1027<n∧c∈O∩ℙrepr⁡3n→0∈V
61 31 a1i ⊢n∈O∧1027<n∧c∈O∩ℙrepr⁡3n→1∈V
62 37 a1i ⊢n∈O∧1027<n∧c∈O∩ℙrepr⁡3n→2∈V
63 60 61 62 3jca ⊢n∈O∧1027<n∧c∈O∩ℙrepr⁡3n→0∈V∧1∈V∧2∈V
64 0ne1 ⊢0≠1
65 64 a1i ⊢n∈O∧1027<n∧c∈O∩ℙrepr⁡3n→0≠1
66 0ne2 ⊢0≠2
67 66 a1i ⊢n∈O∧1027<n∧c∈O∩ℙrepr⁡3n→0≠2
68 1ne2 ⊢1≠2
69 68 a1i ⊢n∈O∧1027<n∧c∈O∩ℙrepr⁡3n→1≠2
70 50 51 52 59 63 65 67 69 sumtp ⊢n∈O∧1027<n∧c∈O∩ℙrepr⁡3n→∑i∈012c⁡i=c⁡0+c⁡1+c⁡2
71 48 49 70 3eqtr3d ⊢n∈O∧1027<n∧c∈O∩ℙrepr⁡3n→n=c⁡0+c⁡1+c⁡2
72 46 71 jca ⊢n∈O∧1027<n∧c∈O∩ℙrepr⁡3n→c⁡0∈O∧c⁡1∈O∧c⁡2∈O∧n=c⁡0+c⁡1+c⁡2
73 eleq1 ⊢p=c⁡0→p∈O↔c⁡0∈O
74 73 3anbi1d ⊢p=c⁡0→p∈O∧q∈O∧r∈O↔c⁡0∈O∧q∈O∧r∈O
75 oveq1 ⊢p=c⁡0→p+q=c⁡0+q
76 75 oveq1d ⊢p=c⁡0→p+q+r=c⁡0+q+r
77 76 eqeq2d ⊢p=c⁡0→n=p+q+r↔n=c⁡0+q+r
78 74 77 anbi12d ⊢p=c⁡0→p∈O∧q∈O∧r∈O∧n=p+q+r↔c⁡0∈O∧q∈O∧r∈O∧n=c⁡0+q+r
79 eleq1 ⊢q=c⁡1→q∈O↔c⁡1∈O
80 79 3anbi2d ⊢q=c⁡1→c⁡0∈O∧q∈O∧r∈O↔c⁡0∈O∧c⁡1∈O∧r∈O
81 oveq2 ⊢q=c⁡1→c⁡0+q=c⁡0+c⁡1
82 81 oveq1d ⊢q=c⁡1→c⁡0+q+r=c⁡0+c⁡1+r
83 82 eqeq2d ⊢q=c⁡1→n=c⁡0+q+r↔n=c⁡0+c⁡1+r
84 80 83 anbi12d ⊢q=c⁡1→c⁡0∈O∧q∈O∧r∈O∧n=c⁡0+q+r↔c⁡0∈O∧c⁡1∈O∧r∈O∧n=c⁡0+c⁡1+r
85 eleq1 ⊢r=c⁡2→r∈O↔c⁡2∈O
86 85 3anbi3d ⊢r=c⁡2→c⁡0∈O∧c⁡1∈O∧r∈O↔c⁡0∈O∧c⁡1∈O∧c⁡2∈O
87 oveq2 ⊢r=c⁡2→c⁡0+c⁡1+r=c⁡0+c⁡1+c⁡2
88 87 eqeq2d ⊢r=c⁡2→n=c⁡0+c⁡1+r↔n=c⁡0+c⁡1+c⁡2
89 86 88 anbi12d ⊢r=c⁡2→c⁡0∈O∧c⁡1∈O∧r∈O∧n=c⁡0+c⁡1+r↔c⁡0∈O∧c⁡1∈O∧c⁡2∈O∧n=c⁡0+c⁡1+c⁡2
90 78 84 89 rspc3ev ⊢c⁡0∈ℙ∧c⁡1∈ℙ∧c⁡2∈ℙ∧c⁡0∈O∧c⁡1∈O∧c⁡2∈O∧n=c⁡0+c⁡1+c⁡2→∃p∈ℙ∃q∈ℙ∃r∈ℙp∈O∧q∈O∧r∈O∧n=p+q+r
91 30 36 42 72 90 syl31anc ⊢n∈O∧1027<n∧c∈O∩ℙrepr⁡3n→∃p∈ℙ∃q∈ℙ∃r∈ℙp∈O∧q∈O∧r∈O∧n=p+q+r
92 91 adantr ⊢n∈O∧1027<n∧c∈O∩ℙrepr⁡3n∧⊤→∃p∈ℙ∃q∈ℙ∃r∈ℙp∈O∧q∈O∧r∈O∧n=p+q+r
93 8 a1i ⊢n∈O∧1027<n→1027∈ℕ
94 93 nnred ⊢n∈O∧1027<n→1027∈ℝ
95 18 zred ⊢n∈O→n∈ℝ
96 95 adantr ⊢n∈O∧1027<n→n∈ℝ
97 simpr ⊢n∈O∧1027<n→1027<n
98 94 96 97 ltled ⊢n∈O∧1027<n→1027≤n
99 1 11 98 tgoldbachgtd ⊢n∈O∧1027<n→0<O∩ℙrepr⁡3n
100 ovex ⊢O∩ℙrepr⁡3n∈V
101 hashneq0 ⊢O∩ℙrepr⁡3n∈V→0<O∩ℙrepr⁡3n↔O∩ℙrepr⁡3n≠∅
102 100 101 ax-mp ⊢0<O∩ℙrepr⁡3n↔O∩ℙrepr⁡3n≠∅
103 99 102 sylib ⊢n∈O∧1027<n→O∩ℙrepr⁡3n≠∅
104 103 neneqd ⊢n∈O∧1027<n→¬O∩ℙrepr⁡3n=∅
105 neq0 ⊢¬O∩ℙrepr⁡3n=∅↔∃cc∈O∩ℙrepr⁡3n
106 104 105 sylib ⊢n∈O∧1027<n→∃cc∈O∩ℙrepr⁡3n
107 tru ⊢⊤
108 106 107 jctil ⊢n∈O∧1027<n→⊤∧∃cc∈O∩ℙrepr⁡3n
109 19.42v ⊢∃c⊤∧c∈O∩ℙrepr⁡3n↔⊤∧∃cc∈O∩ℙrepr⁡3n
110 108 109 sylibr ⊢n∈O∧1027<n→∃c⊤∧c∈O∩ℙrepr⁡3n
111 exancom ⊢∃c⊤∧c∈O∩ℙrepr⁡3n↔∃cc∈O∩ℙrepr⁡3n∧⊤
112 110 111 sylib ⊢n∈O∧1027<n→∃cc∈O∩ℙrepr⁡3n∧⊤
113 df-rex ⊢∃c∈O∩ℙrepr⁡3n⊤↔∃cc∈O∩ℙrepr⁡3n∧⊤
114 112 113 sylibr ⊢n∈O∧1027<n→∃c∈O∩ℙrepr⁡3n⊤
115 92 114 r19.29a ⊢n∈O∧1027<n→∃p∈ℙ∃q∈ℙ∃r∈ℙp∈O∧q∈O∧r∈O∧n=p+q+r
116 2 eleq2i ⊢n∈G↔n∈z∈O|∃p∈ℙ∃q∈ℙ∃r∈ℙp∈O∧q∈O∧r∈O∧z=p+q+r
117 eqeq1 ⊢z=n→z=p+q+r↔n=p+q+r
118 117 anbi2d ⊢z=n→p∈O∧q∈O∧r∈O∧z=p+q+r↔p∈O∧q∈O∧r∈O∧n=p+q+r
119 118 rexbidv ⊢z=n→∃r∈ℙp∈O∧q∈O∧r∈O∧z=p+q+r↔∃r∈ℙp∈O∧q∈O∧r∈O∧n=p+q+r
120 119 rexbidv ⊢z=n→∃q∈ℙ∃r∈ℙp∈O∧q∈O∧r∈O∧z=p+q+r↔∃q∈ℙ∃r∈ℙp∈O∧q∈O∧r∈O∧n=p+q+r
121 120 rexbidv ⊢z=n→∃p∈ℙ∃q∈ℙ∃r∈ℙp∈O∧q∈O∧r∈O∧z=p+q+r↔∃p∈ℙ∃q∈ℙ∃r∈ℙp∈O∧q∈O∧r∈O∧n=p+q+r
122 121 elrab3 ⊢n∈O→n∈z∈O|∃p∈ℙ∃q∈ℙ∃r∈ℙp∈O∧q∈O∧r∈O∧z=p+q+r↔∃p∈ℙ∃q∈ℙ∃r∈ℙp∈O∧q∈O∧r∈O∧n=p+q+r
123 116 122 bitrid ⊢n∈O→n∈G↔∃p∈ℙ∃q∈ℙ∃r∈ℙp∈O∧q∈O∧r∈O∧n=p+q+r
124 123 biimpar ⊢n∈O∧∃p∈ℙ∃q∈ℙ∃r∈ℙp∈O∧q∈O∧r∈O∧n=p+q+r→n∈G
125 11 115 124 syl2anc ⊢n∈O∧1027<n→n∈G
126 125 ex ⊢n∈O→1027<n→n∈G
127 126 rgen ⊢∀n∈O1027<n→n∈G
128 10 127 pm3.2i ⊢1027≤1027∧∀n∈O1027<n→n∈G
129 breq1 ⊢m=1027→m≤1027↔1027≤1027
130 breq1 ⊢m=1027→m<n↔1027<n
131 130 imbi1d ⊢m=1027→m<n→n∈G↔1027<n→n∈G
132 131 ralbidv ⊢m=1027→∀n∈Om<n→n∈G↔∀n∈O1027<n→n∈G
133 129 132 anbi12d ⊢m=1027→m≤1027∧∀n∈Om<n→n∈G↔1027≤1027∧∀n∈O1027<n→n∈G
134 133 rspcev ⊢1027∈ℕ∧1027≤1027∧∀n∈O1027<n→n∈G→∃m∈ℕm≤1027∧∀n∈Om<n→n∈G
135 8 128 134 mp2an ⊢∃m∈ℕm≤1027∧∀n∈Om<n→n∈G