This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ∀ 𝑛 ∈ Odd ( 7 < 𝑛 → 𝑛 ∈ GoldbachOdd ) → ∀ 𝑛 ∈ Odd ( 5 < 𝑛 → 𝑛 ∈ GoldbachOddW ) )

Proof

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