Metamath Proof Explorer

Theorem stgoldbnnsum4prm

Description: If the (strong) ternary Goldbach conjecture is valid, then every integer greater than 1 is the sum of at most 4 primes. (Contributed by AV, 27-Jul-2020)

Ref Expression
Assertion stgoldbnnsum4prm ${⊢}\forall {m}\in \mathrm{Odd}\phantom{\rule{.4em}{0ex}}\left(7<{m}\to {m}\in \mathrm{GoldbachOdd}\right)\to \forall {n}\in {ℤ}_{\ge 2}\phantom{\rule{.4em}{0ex}}\exists {d}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {f}\in \left({ℙ}^{\left(1\dots {d}\right)}\right)\phantom{\rule{.4em}{0ex}}\left({d}\le 4\wedge {n}=\sum _{{k}=1}^{{d}}{f}\left({k}\right)\right)$

Proof

Step Hyp Ref Expression
1 stgoldbwt ${⊢}\forall {m}\in \mathrm{Odd}\phantom{\rule{.4em}{0ex}}\left(7<{m}\to {m}\in \mathrm{GoldbachOdd}\right)\to \forall {m}\in \mathrm{Odd}\phantom{\rule{.4em}{0ex}}\left(5<{m}\to {m}\in \mathrm{GoldbachOddW}\right)$
2 wtgoldbnnsum4prm ${⊢}\forall {m}\in \mathrm{Odd}\phantom{\rule{.4em}{0ex}}\left(5<{m}\to {m}\in \mathrm{GoldbachOddW}\right)\to \forall {n}\in {ℤ}_{\ge 2}\phantom{\rule{.4em}{0ex}}\exists {d}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {f}\in \left({ℙ}^{\left(1\dots {d}\right)}\right)\phantom{\rule{.4em}{0ex}}\left({d}\le 4\wedge {n}=\sum _{{k}=1}^{{d}}{f}\left({k}\right)\right)$
3 1 2 syl ${⊢}\forall {m}\in \mathrm{Odd}\phantom{\rule{.4em}{0ex}}\left(7<{m}\to {m}\in \mathrm{GoldbachOdd}\right)\to \forall {n}\in {ℤ}_{\ge 2}\phantom{\rule{.4em}{0ex}}\exists {d}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {f}\in \left({ℙ}^{\left(1\dots {d}\right)}\right)\phantom{\rule{.4em}{0ex}}\left({d}\le 4\wedge {n}=\sum _{{k}=1}^{{d}}{f}\left({k}\right)\right)$