# Metamath Proof Explorer

## Theorem gbogbow

Description: A (strong) odd Goldbach number is a weak Goldbach number. (Contributed by AV, 26-Jul-2020)

Ref Expression
Assertion gbogbow ${⊢}{Z}\in \mathrm{GoldbachOdd}\to {Z}\in \mathrm{GoldbachOddW}$

### Proof

Step Hyp Ref Expression
1 simpr ${⊢}\left(\left({p}\in \mathrm{Odd}\wedge {q}\in \mathrm{Odd}\wedge {r}\in \mathrm{Odd}\right)\wedge {Z}={p}+{q}+{r}\right)\to {Z}={p}+{q}+{r}$
2 1 reximi ${⊢}\exists {r}\in ℙ\phantom{\rule{.4em}{0ex}}\left(\left({p}\in \mathrm{Odd}\wedge {q}\in \mathrm{Odd}\wedge {r}\in \mathrm{Odd}\right)\wedge {Z}={p}+{q}+{r}\right)\to \exists {r}\in ℙ\phantom{\rule{.4em}{0ex}}{Z}={p}+{q}+{r}$
3 2 reximi ${⊢}\exists {q}\in ℙ\phantom{\rule{.4em}{0ex}}\exists {r}\in ℙ\phantom{\rule{.4em}{0ex}}\left(\left({p}\in \mathrm{Odd}\wedge {q}\in \mathrm{Odd}\wedge {r}\in \mathrm{Odd}\right)\wedge {Z}={p}+{q}+{r}\right)\to \exists {q}\in ℙ\phantom{\rule{.4em}{0ex}}\exists {r}\in ℙ\phantom{\rule{.4em}{0ex}}{Z}={p}+{q}+{r}$
4 3 reximi ${⊢}\exists {p}\in ℙ\phantom{\rule{.4em}{0ex}}\exists {q}\in ℙ\phantom{\rule{.4em}{0ex}}\exists {r}\in ℙ\phantom{\rule{.4em}{0ex}}\left(\left({p}\in \mathrm{Odd}\wedge {q}\in \mathrm{Odd}\wedge {r}\in \mathrm{Odd}\right)\wedge {Z}={p}+{q}+{r}\right)\to \exists {p}\in ℙ\phantom{\rule{.4em}{0ex}}\exists {q}\in ℙ\phantom{\rule{.4em}{0ex}}\exists {r}\in ℙ\phantom{\rule{.4em}{0ex}}{Z}={p}+{q}+{r}$
5 4 anim2i ${⊢}\left({Z}\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}}\left(\left({p}\in \mathrm{Odd}\wedge {q}\in \mathrm{Odd}\wedge {r}\in \mathrm{Odd}\right)\wedge {Z}={p}+{q}+{r}\right)\right)\to \left({Z}\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}}{Z}={p}+{q}+{r}\right)$
6 isgbo ${⊢}{Z}\in \mathrm{GoldbachOdd}↔\left({Z}\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}}\left(\left({p}\in \mathrm{Odd}\wedge {q}\in \mathrm{Odd}\wedge {r}\in \mathrm{Odd}\right)\wedge {Z}={p}+{q}+{r}\right)\right)$
7 isgbow ${⊢}{Z}\in \mathrm{GoldbachOddW}↔\left({Z}\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}}{Z}={p}+{q}+{r}\right)$
8 5 6 7 3imtr4i ${⊢}{Z}\in \mathrm{GoldbachOdd}\to {Z}\in \mathrm{GoldbachOddW}$