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 ⊢ ∀ n ∈ Odd 7 < n → n ∈ GoldbachOdd → ∀ n ∈ Odd 5 < n → n ∈ GoldbachOddW

Proof

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