Metamath Proof Explorer


Theorem nnsum4primeseven

Description: If the (weak) ternary Goldbach conjecture is valid, then every even integer greater than 8 is the sum of 4 primes. (Contributed by AV, 25-Jul-2020)

Ref Expression
Assertion nnsum4primeseven mOdd5<mmGoldbachOddWN9NEvenf14N=k=14fk

Proof

Step Hyp Ref Expression
1 evengpop3 mOdd5<mmGoldbachOddWN9NEvenoGoldbachOddWN=o+3
2 1 imp mOdd5<mmGoldbachOddWN9NEvenoGoldbachOddWN=o+3
3 simplll mOdd5<mmGoldbachOddWN9NEvenoGoldbachOddWN=o+3mOdd5<mmGoldbachOddW
4 6nn 6
5 4 nnzi 6
6 5 a1i N96
7 3z 3
8 7 a1i N93
9 6p3e9 6+3=9
10 9 eqcomi 9=6+3
11 10 fveq2i 9=6+3
12 11 eleq2i N9N6+3
13 12 biimpi N9N6+3
14 eluzsub 63N6+3N36
15 6 8 13 14 syl3anc N9N36
16 15 adantr N9NEvenN36
17 16 ad3antlr mOdd5<mmGoldbachOddWN9NEvenoGoldbachOddWN=o+3N36
18 3odd 3Odd
19 18 a1i N93Odd
20 19 anim1i N9NEven3OddNEven
21 20 adantl mOdd5<mmGoldbachOddWN9NEven3OddNEven
22 21 ancomd mOdd5<mmGoldbachOddWN9NEvenNEven3Odd
23 22 adantr mOdd5<mmGoldbachOddWN9NEvenoGoldbachOddWNEven3Odd
24 23 adantr mOdd5<mmGoldbachOddWN9NEvenoGoldbachOddWN=o+3NEven3Odd
25 emoo NEven3OddN3Odd
26 24 25 syl mOdd5<mmGoldbachOddWN9NEvenoGoldbachOddWN=o+3N3Odd
27 nnsum4primesodd mOdd5<mmGoldbachOddWN36N3Oddg13N3=k=13gk
28 27 imp mOdd5<mmGoldbachOddWN36N3Oddg13N3=k=13gk
29 3 17 26 28 syl12anc mOdd5<mmGoldbachOddWN9NEvenoGoldbachOddWN=o+3g13N3=k=13gk
30 simpr N9g:13g:13
31 4z 4
32 fzonel ¬41..^4
33 fzoval 41..^4=141
34 31 33 ax-mp 1..^4=141
35 4cn 4
36 ax-1cn 1
37 3cn 3
38 35 36 37 3pm3.2i 413
39 3p1e4 3+1=4
40 subadd2 41341=33+1=4
41 39 40 mpbiri 41341=3
42 38 41 ax-mp 41=3
43 42 oveq2i 141=13
44 34 43 eqtri 1..^4=13
45 44 eqcomi 13=1..^4
46 45 eleq2i 41341..^4
47 32 46 mtbir ¬413
48 31 47 pm3.2i 4¬413
49 48 a1i N9g:134¬413
50 3prm 3
51 50 a1i N9g:133
52 fsnunf g:134¬4133g43:134
53 30 49 51 52 syl3anc N9g:13g43:134
54 fzval3 414=1..^4+1
55 31 54 ax-mp 14=1..^4+1
56 1z 1
57 1re 1
58 4re 4
59 1lt4 1<4
60 57 58 59 ltleii 14
61 eluz2 411414
62 56 31 60 61 mpbir3an 41
63 fzosplitsn 411..^4+1=1..^44
64 62 63 ax-mp 1..^4+1=1..^44
65 44 uneq1i 1..^44=134
66 55 64 65 3eqtri 14=134
67 66 feq2i g43:14g43:134
68 53 67 sylibr N9g:13g43:14
69 prmex V
70 ovex 14V
71 69 70 pm3.2i V14V
72 elmapg V14Vg4314g43:14
73 71 72 mp1i N9g:13g4314g43:14
74 68 73 mpbird N9g:13g4314
75 74 adantr N9g:13N3=k=13gkg4314
76 fveq1 f=g43fk=g43k
77 76 adantr f=g43k14fk=g43k
78 77 sumeq2dv f=g43k=14fk=k=14g43k
79 78 eqeq2d f=g43N=k=14fkN=k=14g43k
80 79 adantl N9g:13N3=k=13gkf=g43N=k=14fkN=k=14g43k
81 62 a1i N9g:1341
82 66 eleq2i k14k134
83 elun k134k13k4
84 velsn k4k=4
85 84 orbi2i k13k4k13k=4
86 82 83 85 3bitri k14k13k=4
87 elfz2 k1313k1kk3
88 3re 3
89 88 58 pm3.2i 34
90 3lt4 3<4
91 ltnle 343<4¬43
92 90 91 mpbii 34¬43
93 89 92 ax-mp ¬43
94 breq1 k=4k343
95 94 eqcoms 4=kk343
96 93 95 mtbiri 4=k¬k3
97 96 a1i k4=k¬k3
98 97 necon2ad kk34k
99 98 adantld k1kk34k
100 99 3ad2ant3 13k1kk34k
101 100 imp 13k1kk34k
102 87 101 sylbi k134k
103 102 adantr k13g:134k
104 fvunsn 4kg43k=gk
105 103 104 syl k13g:13g43k=gk
106 ffvelrn g:13k13gk
107 106 ancoms k13g:13gk
108 prmz gkgk
109 107 108 syl k13g:13gk
110 109 zcnd k13g:13gk
111 105 110 eqeltrd k13g:13g43k
112 111 ex k13g:13g43k
113 112 adantld k13N9g:13g43k
114 fveq2 k=4g43k=g434
115 31 a1i g:134
116 7 a1i g:133
117 fdm g:13domg=13
118 eleq2 domg=134domg413
119 47 118 mtbiri domg=13¬4domg
120 117 119 syl g:13¬4domg
121 fsnunfv 43¬4domgg434=3
122 115 116 120 121 syl3anc g:13g434=3
123 122 adantl N9g:13g434=3
124 114 123 sylan9eq k=4N9g:13g43k=3
125 124 37 eqeltrdi k=4N9g:13g43k
126 125 ex k=4N9g:13g43k
127 113 126 jaoi k13k=4N9g:13g43k
128 127 com12 N9g:13k13k=4g43k
129 86 128 syl5bi N9g:13k14g43k
130 129 imp N9g:13k14g43k
131 81 130 114 fsumm1 N9g:13k=14g43k=k=141g43k+g434
132 131 adantr N9g:13N3=k=13gkk=14g43k=k=141g43k+g434
133 42 eqcomi 3=41
134 133 oveq2i 13=141
135 134 a1i N9g:1313=141
136 102 adantl N9g:13k134k
137 136 104 syl N9g:13k13g43k=gk
138 137 eqcomd N9g:13k13gk=g43k
139 135 138 sumeq12dv N9g:13k=13gk=k=141g43k
140 139 eqeq2d N9g:13N3=k=13gkN3=k=141g43k
141 140 biimpa N9g:13N3=k=13gkN3=k=141g43k
142 141 eqcomd N9g:13N3=k=13gkk=141g43k=N3
143 142 oveq1d N9g:13N3=k=13gkk=141g43k+g434=N-3+g434
144 31 a1i N9g:134
145 7 a1i N9g:133
146 120 adantl N9g:13¬4domg
147 144 145 146 121 syl3anc N9g:13g434=3
148 147 oveq2d N9g:13N-3+g434=N-3+3
149 eluzelcn N9N
150 37 a1i N93
151 149 150 npcand N9N-3+3=N
152 151 adantr N9g:13N-3+3=N
153 148 152 eqtrd N9g:13N-3+g434=N
154 153 adantr N9g:13N3=k=13gkN-3+g434=N
155 132 143 154 3eqtrrd N9g:13N3=k=13gkN=k=14g43k
156 75 80 155 rspcedvd N9g:13N3=k=13gkf14N=k=14fk
157 156 ex N9g:13N3=k=13gkf14N=k=14fk
158 157 expcom g:13N9N3=k=13gkf14N=k=14fk
159 elmapi g13g:13
160 158 159 syl11 N9g13N3=k=13gkf14N=k=14fk
161 160 rexlimdv N9g13N3=k=13gkf14N=k=14fk
162 161 adantr N9NEveng13N3=k=13gkf14N=k=14fk
163 162 ad3antlr mOdd5<mmGoldbachOddWN9NEvenoGoldbachOddWN=o+3g13N3=k=13gkf14N=k=14fk
164 29 163 mpd mOdd5<mmGoldbachOddWN9NEvenoGoldbachOddWN=o+3f14N=k=14fk
165 164 rexlimdva2 mOdd5<mmGoldbachOddWN9NEvenoGoldbachOddWN=o+3f14N=k=14fk
166 2 165 mpd mOdd5<mmGoldbachOddWN9NEvenf14N=k=14fk
167 166 ex mOdd5<mmGoldbachOddWN9NEvenf14N=k=14fk