# Metamath Proof Explorer

## Theorem stgoldbwt

Description: If the strong ternary Goldbach conjecture is valid, then the weak ternary Goldbach conjecture holds, too. (Contributed by AV, 27-Jul-2020)

Ref Expression
Assertion stgoldbwt ${⊢}\forall {n}\in \mathrm{Odd}\phantom{\rule{.4em}{0ex}}\left(7<{n}\to {n}\in \mathrm{GoldbachOdd}\right)\to \forall {n}\in \mathrm{Odd}\phantom{\rule{.4em}{0ex}}\left(5<{n}\to {n}\in \mathrm{GoldbachOddW}\right)$

### Proof

Step Hyp Ref Expression
1 pm3.35 ${⊢}\left(7<{n}\wedge \left(7<{n}\to {n}\in \mathrm{GoldbachOdd}\right)\right)\to {n}\in \mathrm{GoldbachOdd}$
2 gbogbow ${⊢}{n}\in \mathrm{GoldbachOdd}\to {n}\in \mathrm{GoldbachOddW}$
3 2 a1d ${⊢}{n}\in \mathrm{GoldbachOdd}\to \left(5<{n}\to {n}\in \mathrm{GoldbachOddW}\right)$
4 1 3 syl ${⊢}\left(7<{n}\wedge \left(7<{n}\to {n}\in \mathrm{GoldbachOdd}\right)\right)\to \left(5<{n}\to {n}\in \mathrm{GoldbachOddW}\right)$
5 4 ex ${⊢}7<{n}\to \left(\left(7<{n}\to {n}\in \mathrm{GoldbachOdd}\right)\to \left(5<{n}\to {n}\in \mathrm{GoldbachOddW}\right)\right)$
6 5 a1d ${⊢}7<{n}\to \left({n}\in \mathrm{Odd}\to \left(\left(7<{n}\to {n}\in \mathrm{GoldbachOdd}\right)\to \left(5<{n}\to {n}\in \mathrm{GoldbachOddW}\right)\right)\right)$
7 oddz ${⊢}{n}\in \mathrm{Odd}\to {n}\in ℤ$
8 7 zred ${⊢}{n}\in \mathrm{Odd}\to {n}\in ℝ$
9 7re ${⊢}7\in ℝ$
10 9 a1i ${⊢}{n}\in \mathrm{Odd}\to 7\in ℝ$
11 8 10 lenltd ${⊢}{n}\in \mathrm{Odd}\to \left({n}\le 7↔¬7<{n}\right)$
12 8 10 leloed ${⊢}{n}\in \mathrm{Odd}\to \left({n}\le 7↔\left({n}<7\vee {n}=7\right)\right)$
13 7 adantr ${⊢}\left({n}\in \mathrm{Odd}\wedge 5<{n}\right)\to {n}\in ℤ$
14 6nn ${⊢}6\in ℕ$
15 14 nnzi ${⊢}6\in ℤ$
16 13 15 jctir ${⊢}\left({n}\in \mathrm{Odd}\wedge 5<{n}\right)\to \left({n}\in ℤ\wedge 6\in ℤ\right)$
17 16 adantl ${⊢}\left({n}<7\wedge \left({n}\in \mathrm{Odd}\wedge 5<{n}\right)\right)\to \left({n}\in ℤ\wedge 6\in ℤ\right)$
18 df-7 ${⊢}7=6+1$
19 18 breq2i ${⊢}{n}<7↔{n}<6+1$
20 19 biimpi ${⊢}{n}<7\to {n}<6+1$
21 df-6 ${⊢}6=5+1$
22 5nn ${⊢}5\in ℕ$
23 22 nnzi ${⊢}5\in ℤ$
24 zltp1le ${⊢}\left(5\in ℤ\wedge {n}\in ℤ\right)\to \left(5<{n}↔5+1\le {n}\right)$
25 23 7 24 sylancr ${⊢}{n}\in \mathrm{Odd}\to \left(5<{n}↔5+1\le {n}\right)$
26 25 biimpa ${⊢}\left({n}\in \mathrm{Odd}\wedge 5<{n}\right)\to 5+1\le {n}$
27 21 26 eqbrtrid ${⊢}\left({n}\in \mathrm{Odd}\wedge 5<{n}\right)\to 6\le {n}$
28 20 27 anim12ci ${⊢}\left({n}<7\wedge \left({n}\in \mathrm{Odd}\wedge 5<{n}\right)\right)\to \left(6\le {n}\wedge {n}<6+1\right)$
29 zgeltp1eq ${⊢}\left({n}\in ℤ\wedge 6\in ℤ\right)\to \left(\left(6\le {n}\wedge {n}<6+1\right)\to {n}=6\right)$
30 17 28 29 sylc ${⊢}\left({n}<7\wedge \left({n}\in \mathrm{Odd}\wedge 5<{n}\right)\right)\to {n}=6$
31 30 orcd ${⊢}\left({n}<7\wedge \left({n}\in \mathrm{Odd}\wedge 5<{n}\right)\right)\to \left({n}=6\vee {n}=7\right)$
32 31 ex ${⊢}{n}<7\to \left(\left({n}\in \mathrm{Odd}\wedge 5<{n}\right)\to \left({n}=6\vee {n}=7\right)\right)$
33 olc ${⊢}{n}=7\to \left({n}=6\vee {n}=7\right)$
34 33 a1d ${⊢}{n}=7\to \left(\left({n}\in \mathrm{Odd}\wedge 5<{n}\right)\to \left({n}=6\vee {n}=7\right)\right)$
35 32 34 jaoi ${⊢}\left({n}<7\vee {n}=7\right)\to \left(\left({n}\in \mathrm{Odd}\wedge 5<{n}\right)\to \left({n}=6\vee {n}=7\right)\right)$
36 35 expd ${⊢}\left({n}<7\vee {n}=7\right)\to \left({n}\in \mathrm{Odd}\to \left(5<{n}\to \left({n}=6\vee {n}=7\right)\right)\right)$
37 36 com12 ${⊢}{n}\in \mathrm{Odd}\to \left(\left({n}<7\vee {n}=7\right)\to \left(5<{n}\to \left({n}=6\vee {n}=7\right)\right)\right)$
38 12 37 sylbid ${⊢}{n}\in \mathrm{Odd}\to \left({n}\le 7\to \left(5<{n}\to \left({n}=6\vee {n}=7\right)\right)\right)$
39 eleq1 ${⊢}{n}=6\to \left({n}\in \mathrm{Odd}↔6\in \mathrm{Odd}\right)$
40 6even ${⊢}6\in \mathrm{Even}$
41 evennodd ${⊢}6\in \mathrm{Even}\to ¬6\in \mathrm{Odd}$
42 41 pm2.21d ${⊢}6\in \mathrm{Even}\to \left(6\in \mathrm{Odd}\to {n}\in \mathrm{GoldbachOddW}\right)$
43 40 42 mp1i ${⊢}{n}=6\to \left(6\in \mathrm{Odd}\to {n}\in \mathrm{GoldbachOddW}\right)$
44 39 43 sylbid ${⊢}{n}=6\to \left({n}\in \mathrm{Odd}\to {n}\in \mathrm{GoldbachOddW}\right)$
45 7gbow ${⊢}7\in \mathrm{GoldbachOddW}$
46 eleq1 ${⊢}{n}=7\to \left({n}\in \mathrm{GoldbachOddW}↔7\in \mathrm{GoldbachOddW}\right)$
47 45 46 mpbiri ${⊢}{n}=7\to {n}\in \mathrm{GoldbachOddW}$
48 47 a1d ${⊢}{n}=7\to \left({n}\in \mathrm{Odd}\to {n}\in \mathrm{GoldbachOddW}\right)$
49 44 48 jaoi ${⊢}\left({n}=6\vee {n}=7\right)\to \left({n}\in \mathrm{Odd}\to {n}\in \mathrm{GoldbachOddW}\right)$
50 49 com12 ${⊢}{n}\in \mathrm{Odd}\to \left(\left({n}=6\vee {n}=7\right)\to {n}\in \mathrm{GoldbachOddW}\right)$
51 38 50 syl6d ${⊢}{n}\in \mathrm{Odd}\to \left({n}\le 7\to \left(5<{n}\to {n}\in \mathrm{GoldbachOddW}\right)\right)$
52 11 51 sylbird ${⊢}{n}\in \mathrm{Odd}\to \left(¬7<{n}\to \left(5<{n}\to {n}\in \mathrm{GoldbachOddW}\right)\right)$
53 52 com12 ${⊢}¬7<{n}\to \left({n}\in \mathrm{Odd}\to \left(5<{n}\to {n}\in \mathrm{GoldbachOddW}\right)\right)$
54 53 a1dd ${⊢}¬7<{n}\to \left({n}\in \mathrm{Odd}\to \left(\left(7<{n}\to {n}\in \mathrm{GoldbachOdd}\right)\to \left(5<{n}\to {n}\in \mathrm{GoldbachOddW}\right)\right)\right)$
55 6 54 pm2.61i ${⊢}{n}\in \mathrm{Odd}\to \left(\left(7<{n}\to {n}\in \mathrm{GoldbachOdd}\right)\to \left(5<{n}\to {n}\in \mathrm{GoldbachOddW}\right)\right)$
56 55 ralimia ${⊢}\forall {n}\in \mathrm{Odd}\phantom{\rule{.4em}{0ex}}\left(7<{n}\to {n}\in \mathrm{GoldbachOdd}\right)\to \forall {n}\in \mathrm{Odd}\phantom{\rule{.4em}{0ex}}\left(5<{n}\to {n}\in \mathrm{GoldbachOddW}\right)$