# Metamath Proof Explorer

## Theorem nnsum4primesodd

Description: If the (weak) ternary Goldbach conjecture is valid, then every odd integer greater than 5 is the sum of 3 primes. (Contributed by AV, 2-Jul-2020)

Ref Expression
Assertion nnsum4primesodd ${⊢}\forall {m}\in \mathrm{Odd}\phantom{\rule{.4em}{0ex}}\left(5<{m}\to {m}\in \mathrm{GoldbachOddW}\right)\to \left(\left({N}\in {ℤ}_{\ge 6}\wedge {N}\in \mathrm{Odd}\right)\to \exists {f}\in \left({ℙ}^{\left(1\dots 3\right)}\right)\phantom{\rule{.4em}{0ex}}{N}=\sum _{{k}=1}^{3}{f}\left({k}\right)\right)$

### Proof

Step Hyp Ref Expression
1 breq2 ${⊢}{m}={N}\to \left(5<{m}↔5<{N}\right)$
2 eleq1 ${⊢}{m}={N}\to \left({m}\in \mathrm{GoldbachOddW}↔{N}\in \mathrm{GoldbachOddW}\right)$
3 1 2 imbi12d ${⊢}{m}={N}\to \left(\left(5<{m}\to {m}\in \mathrm{GoldbachOddW}\right)↔\left(5<{N}\to {N}\in \mathrm{GoldbachOddW}\right)\right)$
4 3 rspcv ${⊢}{N}\in \mathrm{Odd}\to \left(\forall {m}\in \mathrm{Odd}\phantom{\rule{.4em}{0ex}}\left(5<{m}\to {m}\in \mathrm{GoldbachOddW}\right)\to \left(5<{N}\to {N}\in \mathrm{GoldbachOddW}\right)\right)$
5 4 adantl ${⊢}\left({N}\in {ℤ}_{\ge 6}\wedge {N}\in \mathrm{Odd}\right)\to \left(\forall {m}\in \mathrm{Odd}\phantom{\rule{.4em}{0ex}}\left(5<{m}\to {m}\in \mathrm{GoldbachOddW}\right)\to \left(5<{N}\to {N}\in \mathrm{GoldbachOddW}\right)\right)$
6 eluz2 ${⊢}{N}\in {ℤ}_{\ge 6}↔\left(6\in ℤ\wedge {N}\in ℤ\wedge 6\le {N}\right)$
7 5lt6 ${⊢}5<6$
8 5re ${⊢}5\in ℝ$
9 8 a1i ${⊢}{N}\in ℤ\to 5\in ℝ$
10 6re ${⊢}6\in ℝ$
11 10 a1i ${⊢}{N}\in ℤ\to 6\in ℝ$
12 zre ${⊢}{N}\in ℤ\to {N}\in ℝ$
13 ltletr ${⊢}\left(5\in ℝ\wedge 6\in ℝ\wedge {N}\in ℝ\right)\to \left(\left(5<6\wedge 6\le {N}\right)\to 5<{N}\right)$
14 9 11 12 13 syl3anc ${⊢}{N}\in ℤ\to \left(\left(5<6\wedge 6\le {N}\right)\to 5<{N}\right)$
15 7 14 mpani ${⊢}{N}\in ℤ\to \left(6\le {N}\to 5<{N}\right)$
16 15 imp ${⊢}\left({N}\in ℤ\wedge 6\le {N}\right)\to 5<{N}$
17 16 3adant1 ${⊢}\left(6\in ℤ\wedge {N}\in ℤ\wedge 6\le {N}\right)\to 5<{N}$
18 6 17 sylbi ${⊢}{N}\in {ℤ}_{\ge 6}\to 5<{N}$
19 18 adantr ${⊢}\left({N}\in {ℤ}_{\ge 6}\wedge {N}\in \mathrm{Odd}\right)\to 5<{N}$
20 pm2.27 ${⊢}5<{N}\to \left(\left(5<{N}\to {N}\in \mathrm{GoldbachOddW}\right)\to {N}\in \mathrm{GoldbachOddW}\right)$
21 19 20 syl ${⊢}\left({N}\in {ℤ}_{\ge 6}\wedge {N}\in \mathrm{Odd}\right)\to \left(\left(5<{N}\to {N}\in \mathrm{GoldbachOddW}\right)\to {N}\in \mathrm{GoldbachOddW}\right)$
22 isgbow ${⊢}{N}\in \mathrm{GoldbachOddW}↔\left({N}\in \mathrm{Odd}\wedge \exists {p}\in ℙ\phantom{\rule{.4em}{0ex}}\exists {q}\in ℙ\phantom{\rule{.4em}{0ex}}\exists {r}\in ℙ\phantom{\rule{.4em}{0ex}}{N}={p}+{q}+{r}\right)$
23 1ex ${⊢}1\in \mathrm{V}$
24 2ex ${⊢}2\in \mathrm{V}$
25 3ex ${⊢}3\in \mathrm{V}$
26 vex ${⊢}{p}\in \mathrm{V}$
27 vex ${⊢}{q}\in \mathrm{V}$
28 vex ${⊢}{r}\in \mathrm{V}$
29 1ne2 ${⊢}1\ne 2$
30 1re ${⊢}1\in ℝ$
31 1lt3 ${⊢}1<3$
32 30 31 ltneii ${⊢}1\ne 3$
33 2re ${⊢}2\in ℝ$
34 2lt3 ${⊢}2<3$
35 33 34 ltneii ${⊢}2\ne 3$
36 23 24 25 26 27 28 29 32 35 ftp ${⊢}\left\{⟨1,{p}⟩,⟨2,{q}⟩,⟨3,{r}⟩\right\}:\left\{1,2,3\right\}⟶\left\{{p},{q},{r}\right\}$
37 36 a1i ${⊢}\left(\left({p}\in ℙ\wedge {q}\in ℙ\right)\wedge {r}\in ℙ\right)\to \left\{⟨1,{p}⟩,⟨2,{q}⟩,⟨3,{r}⟩\right\}:\left\{1,2,3\right\}⟶\left\{{p},{q},{r}\right\}$
38 1p2e3 ${⊢}1+2=3$
39 38 eqcomi ${⊢}3=1+2$
40 39 oveq2i ${⊢}\left(1\dots 3\right)=\left(1\dots 1+2\right)$
41 1z ${⊢}1\in ℤ$
42 fztp ${⊢}1\in ℤ\to \left(1\dots 1+2\right)=\left\{1,1+1,1+2\right\}$
43 41 42 ax-mp ${⊢}\left(1\dots 1+2\right)=\left\{1,1+1,1+2\right\}$
44 eqid ${⊢}1=1$
45 id ${⊢}1=1\to 1=1$
46 1p1e2 ${⊢}1+1=2$
47 46 a1i ${⊢}1=1\to 1+1=2$
48 38 a1i ${⊢}1=1\to 1+2=3$
49 45 47 48 tpeq123d ${⊢}1=1\to \left\{1,1+1,1+2\right\}=\left\{1,2,3\right\}$
50 44 49 ax-mp ${⊢}\left\{1,1+1,1+2\right\}=\left\{1,2,3\right\}$
51 40 43 50 3eqtri ${⊢}\left(1\dots 3\right)=\left\{1,2,3\right\}$
52 51 feq2i ${⊢}\left\{⟨1,{p}⟩,⟨2,{q}⟩,⟨3,{r}⟩\right\}:\left(1\dots 3\right)⟶\left\{{p},{q},{r}\right\}↔\left\{⟨1,{p}⟩,⟨2,{q}⟩,⟨3,{r}⟩\right\}:\left\{1,2,3\right\}⟶\left\{{p},{q},{r}\right\}$
53 37 52 sylibr ${⊢}\left(\left({p}\in ℙ\wedge {q}\in ℙ\right)\wedge {r}\in ℙ\right)\to \left\{⟨1,{p}⟩,⟨2,{q}⟩,⟨3,{r}⟩\right\}:\left(1\dots 3\right)⟶\left\{{p},{q},{r}\right\}$
54 df-3an ${⊢}\left({p}\in ℙ\wedge {q}\in ℙ\wedge {r}\in ℙ\right)↔\left(\left({p}\in ℙ\wedge {q}\in ℙ\right)\wedge {r}\in ℙ\right)$
55 26 27 28 tpss ${⊢}\left({p}\in ℙ\wedge {q}\in ℙ\wedge {r}\in ℙ\right)↔\left\{{p},{q},{r}\right\}\subseteq ℙ$
56 54 55 sylbb1 ${⊢}\left(\left({p}\in ℙ\wedge {q}\in ℙ\right)\wedge {r}\in ℙ\right)\to \left\{{p},{q},{r}\right\}\subseteq ℙ$
57 53 56 fssd ${⊢}\left(\left({p}\in ℙ\wedge {q}\in ℙ\right)\wedge {r}\in ℙ\right)\to \left\{⟨1,{p}⟩,⟨2,{q}⟩,⟨3,{r}⟩\right\}:\left(1\dots 3\right)⟶ℙ$
58 prmex ${⊢}ℙ\in \mathrm{V}$
59 ovex ${⊢}\left(1\dots 3\right)\in \mathrm{V}$
60 58 59 pm3.2i ${⊢}\left(ℙ\in \mathrm{V}\wedge \left(1\dots 3\right)\in \mathrm{V}\right)$
61 elmapg ${⊢}\left(ℙ\in \mathrm{V}\wedge \left(1\dots 3\right)\in \mathrm{V}\right)\to \left(\left\{⟨1,{p}⟩,⟨2,{q}⟩,⟨3,{r}⟩\right\}\in \left({ℙ}^{\left(1\dots 3\right)}\right)↔\left\{⟨1,{p}⟩,⟨2,{q}⟩,⟨3,{r}⟩\right\}:\left(1\dots 3\right)⟶ℙ\right)$
62 60 61 mp1i ${⊢}\left(\left({p}\in ℙ\wedge {q}\in ℙ\right)\wedge {r}\in ℙ\right)\to \left(\left\{⟨1,{p}⟩,⟨2,{q}⟩,⟨3,{r}⟩\right\}\in \left({ℙ}^{\left(1\dots 3\right)}\right)↔\left\{⟨1,{p}⟩,⟨2,{q}⟩,⟨3,{r}⟩\right\}:\left(1\dots 3\right)⟶ℙ\right)$
63 57 62 mpbird ${⊢}\left(\left({p}\in ℙ\wedge {q}\in ℙ\right)\wedge {r}\in ℙ\right)\to \left\{⟨1,{p}⟩,⟨2,{q}⟩,⟨3,{r}⟩\right\}\in \left({ℙ}^{\left(1\dots 3\right)}\right)$
64 fveq1 ${⊢}{f}=\left\{⟨1,{p}⟩,⟨2,{q}⟩,⟨3,{r}⟩\right\}\to {f}\left({k}\right)=\left\{⟨1,{p}⟩,⟨2,{q}⟩,⟨3,{r}⟩\right\}\left({k}\right)$
65 64 sumeq2sdv ${⊢}{f}=\left\{⟨1,{p}⟩,⟨2,{q}⟩,⟨3,{r}⟩\right\}\to \sum _{{k}=1}^{3}{f}\left({k}\right)=\sum _{{k}=1}^{3}\left\{⟨1,{p}⟩,⟨2,{q}⟩,⟨3,{r}⟩\right\}\left({k}\right)$
66 65 eqeq2d ${⊢}{f}=\left\{⟨1,{p}⟩,⟨2,{q}⟩,⟨3,{r}⟩\right\}\to \left({p}+{q}+{r}=\sum _{{k}=1}^{3}{f}\left({k}\right)↔{p}+{q}+{r}=\sum _{{k}=1}^{3}\left\{⟨1,{p}⟩,⟨2,{q}⟩,⟨3,{r}⟩\right\}\left({k}\right)\right)$
67 66 adantl ${⊢}\left(\left(\left({p}\in ℙ\wedge {q}\in ℙ\right)\wedge {r}\in ℙ\right)\wedge {f}=\left\{⟨1,{p}⟩,⟨2,{q}⟩,⟨3,{r}⟩\right\}\right)\to \left({p}+{q}+{r}=\sum _{{k}=1}^{3}{f}\left({k}\right)↔{p}+{q}+{r}=\sum _{{k}=1}^{3}\left\{⟨1,{p}⟩,⟨2,{q}⟩,⟨3,{r}⟩\right\}\left({k}\right)\right)$
68 51 a1i ${⊢}\left(\left({p}\in ℙ\wedge {q}\in ℙ\right)\wedge {r}\in ℙ\right)\to \left(1\dots 3\right)=\left\{1,2,3\right\}$
69 68 sumeq1d ${⊢}\left(\left({p}\in ℙ\wedge {q}\in ℙ\right)\wedge {r}\in ℙ\right)\to \sum _{{k}=1}^{3}\left\{⟨1,{p}⟩,⟨2,{q}⟩,⟨3,{r}⟩\right\}\left({k}\right)=\sum _{{k}\in \left\{1,2,3\right\}}\left\{⟨1,{p}⟩,⟨2,{q}⟩,⟨3,{r}⟩\right\}\left({k}\right)$
70 fveq2 ${⊢}{k}=1\to \left\{⟨1,{p}⟩,⟨2,{q}⟩,⟨3,{r}⟩\right\}\left({k}\right)=\left\{⟨1,{p}⟩,⟨2,{q}⟩,⟨3,{r}⟩\right\}\left(1\right)$
71 23 26 fvtp1 ${⊢}\left(1\ne 2\wedge 1\ne 3\right)\to \left\{⟨1,{p}⟩,⟨2,{q}⟩,⟨3,{r}⟩\right\}\left(1\right)={p}$
72 29 32 71 mp2an ${⊢}\left\{⟨1,{p}⟩,⟨2,{q}⟩,⟨3,{r}⟩\right\}\left(1\right)={p}$
73 70 72 syl6eq ${⊢}{k}=1\to \left\{⟨1,{p}⟩,⟨2,{q}⟩,⟨3,{r}⟩\right\}\left({k}\right)={p}$
74 fveq2 ${⊢}{k}=2\to \left\{⟨1,{p}⟩,⟨2,{q}⟩,⟨3,{r}⟩\right\}\left({k}\right)=\left\{⟨1,{p}⟩,⟨2,{q}⟩,⟨3,{r}⟩\right\}\left(2\right)$
75 24 27 fvtp2 ${⊢}\left(1\ne 2\wedge 2\ne 3\right)\to \left\{⟨1,{p}⟩,⟨2,{q}⟩,⟨3,{r}⟩\right\}\left(2\right)={q}$
76 29 35 75 mp2an ${⊢}\left\{⟨1,{p}⟩,⟨2,{q}⟩,⟨3,{r}⟩\right\}\left(2\right)={q}$
77 74 76 syl6eq ${⊢}{k}=2\to \left\{⟨1,{p}⟩,⟨2,{q}⟩,⟨3,{r}⟩\right\}\left({k}\right)={q}$
78 fveq2 ${⊢}{k}=3\to \left\{⟨1,{p}⟩,⟨2,{q}⟩,⟨3,{r}⟩\right\}\left({k}\right)=\left\{⟨1,{p}⟩,⟨2,{q}⟩,⟨3,{r}⟩\right\}\left(3\right)$
79 25 28 fvtp3 ${⊢}\left(1\ne 3\wedge 2\ne 3\right)\to \left\{⟨1,{p}⟩,⟨2,{q}⟩,⟨3,{r}⟩\right\}\left(3\right)={r}$
80 32 35 79 mp2an ${⊢}\left\{⟨1,{p}⟩,⟨2,{q}⟩,⟨3,{r}⟩\right\}\left(3\right)={r}$
81 78 80 syl6eq ${⊢}{k}=3\to \left\{⟨1,{p}⟩,⟨2,{q}⟩,⟨3,{r}⟩\right\}\left({k}\right)={r}$
82 prmz ${⊢}{p}\in ℙ\to {p}\in ℤ$
83 82 zcnd ${⊢}{p}\in ℙ\to {p}\in ℂ$
84 prmz ${⊢}{q}\in ℙ\to {q}\in ℤ$
85 84 zcnd ${⊢}{q}\in ℙ\to {q}\in ℂ$
86 prmz ${⊢}{r}\in ℙ\to {r}\in ℤ$
87 86 zcnd ${⊢}{r}\in ℙ\to {r}\in ℂ$
88 83 85 87 3anim123i ${⊢}\left({p}\in ℙ\wedge {q}\in ℙ\wedge {r}\in ℙ\right)\to \left({p}\in ℂ\wedge {q}\in ℂ\wedge {r}\in ℂ\right)$
89 88 3expa ${⊢}\left(\left({p}\in ℙ\wedge {q}\in ℙ\right)\wedge {r}\in ℙ\right)\to \left({p}\in ℂ\wedge {q}\in ℂ\wedge {r}\in ℂ\right)$
90 2z ${⊢}2\in ℤ$
91 3z ${⊢}3\in ℤ$
92 41 90 91 3pm3.2i ${⊢}\left(1\in ℤ\wedge 2\in ℤ\wedge 3\in ℤ\right)$
93 92 a1i ${⊢}\left(\left({p}\in ℙ\wedge {q}\in ℙ\right)\wedge {r}\in ℙ\right)\to \left(1\in ℤ\wedge 2\in ℤ\wedge 3\in ℤ\right)$
94 29 a1i ${⊢}\left(\left({p}\in ℙ\wedge {q}\in ℙ\right)\wedge {r}\in ℙ\right)\to 1\ne 2$
95 32 a1i ${⊢}\left(\left({p}\in ℙ\wedge {q}\in ℙ\right)\wedge {r}\in ℙ\right)\to 1\ne 3$
96 35 a1i ${⊢}\left(\left({p}\in ℙ\wedge {q}\in ℙ\right)\wedge {r}\in ℙ\right)\to 2\ne 3$
97 73 77 81 89 93 94 95 96 sumtp ${⊢}\left(\left({p}\in ℙ\wedge {q}\in ℙ\right)\wedge {r}\in ℙ\right)\to \sum _{{k}\in \left\{1,2,3\right\}}\left\{⟨1,{p}⟩,⟨2,{q}⟩,⟨3,{r}⟩\right\}\left({k}\right)={p}+{q}+{r}$
98 69 97 eqtr2d ${⊢}\left(\left({p}\in ℙ\wedge {q}\in ℙ\right)\wedge {r}\in ℙ\right)\to {p}+{q}+{r}=\sum _{{k}=1}^{3}\left\{⟨1,{p}⟩,⟨2,{q}⟩,⟨3,{r}⟩\right\}\left({k}\right)$
99 63 67 98 rspcedvd ${⊢}\left(\left({p}\in ℙ\wedge {q}\in ℙ\right)\wedge {r}\in ℙ\right)\to \exists {f}\in \left({ℙ}^{\left(1\dots 3\right)}\right)\phantom{\rule{.4em}{0ex}}{p}+{q}+{r}=\sum _{{k}=1}^{3}{f}\left({k}\right)$
100 eqeq1 ${⊢}{N}={p}+{q}+{r}\to \left({N}=\sum _{{k}=1}^{3}{f}\left({k}\right)↔{p}+{q}+{r}=\sum _{{k}=1}^{3}{f}\left({k}\right)\right)$
101 100 rexbidv ${⊢}{N}={p}+{q}+{r}\to \left(\exists {f}\in \left({ℙ}^{\left(1\dots 3\right)}\right)\phantom{\rule{.4em}{0ex}}{N}=\sum _{{k}=1}^{3}{f}\left({k}\right)↔\exists {f}\in \left({ℙ}^{\left(1\dots 3\right)}\right)\phantom{\rule{.4em}{0ex}}{p}+{q}+{r}=\sum _{{k}=1}^{3}{f}\left({k}\right)\right)$
102 99 101 syl5ibrcom ${⊢}\left(\left({p}\in ℙ\wedge {q}\in ℙ\right)\wedge {r}\in ℙ\right)\to \left({N}={p}+{q}+{r}\to \exists {f}\in \left({ℙ}^{\left(1\dots 3\right)}\right)\phantom{\rule{.4em}{0ex}}{N}=\sum _{{k}=1}^{3}{f}\left({k}\right)\right)$
103 102 rexlimdva ${⊢}\left({p}\in ℙ\wedge {q}\in ℙ\right)\to \left(\exists {r}\in ℙ\phantom{\rule{.4em}{0ex}}{N}={p}+{q}+{r}\to \exists {f}\in \left({ℙ}^{\left(1\dots 3\right)}\right)\phantom{\rule{.4em}{0ex}}{N}=\sum _{{k}=1}^{3}{f}\left({k}\right)\right)$
104 103 rexlimivv ${⊢}\exists {p}\in ℙ\phantom{\rule{.4em}{0ex}}\exists {q}\in ℙ\phantom{\rule{.4em}{0ex}}\exists {r}\in ℙ\phantom{\rule{.4em}{0ex}}{N}={p}+{q}+{r}\to \exists {f}\in \left({ℙ}^{\left(1\dots 3\right)}\right)\phantom{\rule{.4em}{0ex}}{N}=\sum _{{k}=1}^{3}{f}\left({k}\right)$
105 104 adantl ${⊢}\left({N}\in \mathrm{Odd}\wedge \exists {p}\in ℙ\phantom{\rule{.4em}{0ex}}\exists {q}\in ℙ\phantom{\rule{.4em}{0ex}}\exists {r}\in ℙ\phantom{\rule{.4em}{0ex}}{N}={p}+{q}+{r}\right)\to \exists {f}\in \left({ℙ}^{\left(1\dots 3\right)}\right)\phantom{\rule{.4em}{0ex}}{N}=\sum _{{k}=1}^{3}{f}\left({k}\right)$
106 22 105 sylbi ${⊢}{N}\in \mathrm{GoldbachOddW}\to \exists {f}\in \left({ℙ}^{\left(1\dots 3\right)}\right)\phantom{\rule{.4em}{0ex}}{N}=\sum _{{k}=1}^{3}{f}\left({k}\right)$
107 106 a1i ${⊢}\left({N}\in {ℤ}_{\ge 6}\wedge {N}\in \mathrm{Odd}\right)\to \left({N}\in \mathrm{GoldbachOddW}\to \exists {f}\in \left({ℙ}^{\left(1\dots 3\right)}\right)\phantom{\rule{.4em}{0ex}}{N}=\sum _{{k}=1}^{3}{f}\left({k}\right)\right)$
108 5 21 107 3syld ${⊢}\left({N}\in {ℤ}_{\ge 6}\wedge {N}\in \mathrm{Odd}\right)\to \left(\forall {m}\in \mathrm{Odd}\phantom{\rule{.4em}{0ex}}\left(5<{m}\to {m}\in \mathrm{GoldbachOddW}\right)\to \exists {f}\in \left({ℙ}^{\left(1\dots 3\right)}\right)\phantom{\rule{.4em}{0ex}}{N}=\sum _{{k}=1}^{3}{f}\left({k}\right)\right)$
109 108 com12 ${⊢}\forall {m}\in \mathrm{Odd}\phantom{\rule{.4em}{0ex}}\left(5<{m}\to {m}\in \mathrm{GoldbachOddW}\right)\to \left(\left({N}\in {ℤ}_{\ge 6}\wedge {N}\in \mathrm{Odd}\right)\to \exists {f}\in \left({ℙ}^{\left(1\dots 3\right)}\right)\phantom{\rule{.4em}{0ex}}{N}=\sum _{{k}=1}^{3}{f}\left({k}\right)\right)$