Metamath Proof Explorer

Theorem sbgoldbwt

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

Ref Expression
Assertion sbgoldbwt ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∀ 𝑚 ∈ Odd ( 5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) )

Proof

Step Hyp Ref Expression
1 oddz ⊢ ( 𝑚 ∈ Odd → 𝑚 ∈ ℤ )
2 5nn ⊢ 5 ∈ ℕ
3 2 nnzi ⊢ 5 ∈ ℤ
4 zltp1le ⊢ ( ( 5 ∈ ℤ ∧ 𝑚 ∈ ℤ ) → ( 5 < 𝑚 ↔ ( 5 + 1 ) ≤ 𝑚 ) )
5 3 4 mpan ⊢ ( 𝑚 ∈ ℤ → ( 5 < 𝑚 ↔ ( 5 + 1 ) ≤ 𝑚 ) )
6 5p1e6 ⊢ ( 5 + 1 ) = 6
7 6 breq1i ⊢ ( ( 5 + 1 ) ≤ 𝑚 ↔ 6 ≤ 𝑚 )
8 6re ⊢ 6 ∈ ℝ
9 8 a1i ⊢ ( 𝑚 ∈ ℤ → 6 ∈ ℝ )
10 zre ⊢ ( 𝑚 ∈ ℤ → 𝑚 ∈ ℝ )
11 9 10 leloed ⊢ ( 𝑚 ∈ ℤ → ( 6 ≤ 𝑚 ↔ ( 6 < 𝑚 ∨ 6 = 𝑚 ) ) )
12 7 11 bitrid ⊢ ( 𝑚 ∈ ℤ → ( ( 5 + 1 ) ≤ 𝑚 ↔ ( 6 < 𝑚 ∨ 6 = 𝑚 ) ) )
13 6nn ⊢ 6 ∈ ℕ
14 13 nnzi ⊢ 6 ∈ ℤ
15 zltp1le ⊢ ( ( 6 ∈ ℤ ∧ 𝑚 ∈ ℤ ) → ( 6 < 𝑚 ↔ ( 6 + 1 ) ≤ 𝑚 ) )
16 14 15 mpan ⊢ ( 𝑚 ∈ ℤ → ( 6 < 𝑚 ↔ ( 6 + 1 ) ≤ 𝑚 ) )
17 6p1e7 ⊢ ( 6 + 1 ) = 7
18 17 breq1i ⊢ ( ( 6 + 1 ) ≤ 𝑚 ↔ 7 ≤ 𝑚 )
19 7re ⊢ 7 ∈ ℝ
20 19 a1i ⊢ ( 𝑚 ∈ ℤ → 7 ∈ ℝ )
21 20 10 leloed ⊢ ( 𝑚 ∈ ℤ → ( 7 ≤ 𝑚 ↔ ( 7 < 𝑚 ∨ 7 = 𝑚 ) ) )
22 18 21 bitrid ⊢ ( 𝑚 ∈ ℤ → ( ( 6 + 1 ) ≤ 𝑚 ↔ ( 7 < 𝑚 ∨ 7 = 𝑚 ) ) )
23 simpr ⊢ ( ( ( 7 < 𝑚 ∧ 𝑚 ∈ ℤ ) ∧ 𝑚 ∈ Odd ) → 𝑚 ∈ Odd )
24 3odd ⊢ 3 ∈ Odd
25 23 24 jctir ⊢ ( ( ( 7 < 𝑚 ∧ 𝑚 ∈ ℤ ) ∧ 𝑚 ∈ Odd ) → ( 𝑚 ∈ Odd ∧ 3 ∈ Odd ) )
26 omoeALTV ⊢ ( ( 𝑚 ∈ Odd ∧ 3 ∈ Odd ) → ( 𝑚 − 3 ) ∈ Even )
27 breq2 ⊢ ( 𝑛 = ( 𝑚 − 3 ) → ( 4 < 𝑛 ↔ 4 < ( 𝑚 − 3 ) ) )
28 eleq1 ⊢ ( 𝑛 = ( 𝑚 − 3 ) → ( 𝑛 ∈ GoldbachEven ↔ ( 𝑚 − 3 ) ∈ GoldbachEven ) )
29 27 28 imbi12d ⊢ ( 𝑛 = ( 𝑚 − 3 ) → ( ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) ↔ ( 4 < ( 𝑚 − 3 ) → ( 𝑚 − 3 ) ∈ GoldbachEven ) ) )
30 29 rspcv ⊢ ( ( 𝑚 − 3 ) ∈ Even → ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ( 4 < ( 𝑚 − 3 ) → ( 𝑚 − 3 ) ∈ GoldbachEven ) ) )
31 25 26 30 3syl ⊢ ( ( ( 7 < 𝑚 ∧ 𝑚 ∈ ℤ ) ∧ 𝑚 ∈ Odd ) → ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ( 4 < ( 𝑚 − 3 ) → ( 𝑚 − 3 ) ∈ GoldbachEven ) ) )
32 4p3e7 ⊢ ( 4 + 3 ) = 7
33 32 eqcomi ⊢ 7 = ( 4 + 3 )
34 33 breq1i ⊢ ( 7 < 𝑚 ↔ ( 4 + 3 ) < 𝑚 )
35 4re ⊢ 4 ∈ ℝ
36 35 a1i ⊢ ( 𝑚 ∈ ℤ → 4 ∈ ℝ )
37 3re ⊢ 3 ∈ ℝ
38 37 a1i ⊢ ( 𝑚 ∈ ℤ → 3 ∈ ℝ )
39 ltaddsub ⊢ ( ( 4 ∈ ℝ ∧ 3 ∈ ℝ ∧ 𝑚 ∈ ℝ ) → ( ( 4 + 3 ) < 𝑚 ↔ 4 < ( 𝑚 − 3 ) ) )
40 39 biimpd ⊢ ( ( 4 ∈ ℝ ∧ 3 ∈ ℝ ∧ 𝑚 ∈ ℝ ) → ( ( 4 + 3 ) < 𝑚 → 4 < ( 𝑚 − 3 ) ) )
41 36 38 10 40 syl3anc ⊢ ( 𝑚 ∈ ℤ → ( ( 4 + 3 ) < 𝑚 → 4 < ( 𝑚 − 3 ) ) )
42 34 41 biimtrid ⊢ ( 𝑚 ∈ ℤ → ( 7 < 𝑚 → 4 < ( 𝑚 − 3 ) ) )
43 42 impcom ⊢ ( ( 7 < 𝑚 ∧ 𝑚 ∈ ℤ ) → 4 < ( 𝑚 − 3 ) )
44 43 adantr ⊢ ( ( ( 7 < 𝑚 ∧ 𝑚 ∈ ℤ ) ∧ 𝑚 ∈ Odd ) → 4 < ( 𝑚 − 3 ) )
45 pm2.27 ⊢ ( 4 < ( 𝑚 − 3 ) → ( ( 4 < ( 𝑚 − 3 ) → ( 𝑚 − 3 ) ∈ GoldbachEven ) → ( 𝑚 − 3 ) ∈ GoldbachEven ) )
46 44 45 syl ⊢ ( ( ( 7 < 𝑚 ∧ 𝑚 ∈ ℤ ) ∧ 𝑚 ∈ Odd ) → ( ( 4 < ( 𝑚 − 3 ) → ( 𝑚 − 3 ) ∈ GoldbachEven ) → ( 𝑚 − 3 ) ∈ GoldbachEven ) )
47 isgbe ⊢ ( ( 𝑚 − 3 ) ∈ GoldbachEven ↔ ( ( 𝑚 − 3 ) ∈ Even ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ ( 𝑚 − 3 ) = ( 𝑝 + 𝑞 ) ) ) )
48 3prm ⊢ 3 ∈ ℙ
49 48 a1i ⊢ ( 𝑚 ∈ ℤ → 3 ∈ ℙ )
50 zcn ⊢ ( 𝑚 ∈ ℤ → 𝑚 ∈ ℂ )
51 3cn ⊢ 3 ∈ ℂ
52 50 51 jctir ⊢ ( 𝑚 ∈ ℤ → ( 𝑚 ∈ ℂ ∧ 3 ∈ ℂ ) )
53 npcan ⊢ ( ( 𝑚 ∈ ℂ ∧ 3 ∈ ℂ ) → ( ( 𝑚 − 3 ) + 3 ) = 𝑚 )
54 53 eqcomd ⊢ ( ( 𝑚 ∈ ℂ ∧ 3 ∈ ℂ ) → 𝑚 = ( ( 𝑚 − 3 ) + 3 ) )
55 52 54 syl ⊢ ( 𝑚 ∈ ℤ → 𝑚 = ( ( 𝑚 − 3 ) + 3 ) )
56 oveq2 ⊢ ( 3 = 𝑟 → ( ( 𝑚 − 3 ) + 3 ) = ( ( 𝑚 − 3 ) + 𝑟 ) )
57 56 eqcoms ⊢ ( 𝑟 = 3 → ( ( 𝑚 − 3 ) + 3 ) = ( ( 𝑚 − 3 ) + 𝑟 ) )
58 55 57 sylan9eq ⊢ ( ( 𝑚 ∈ ℤ ∧ 𝑟 = 3 ) → 𝑚 = ( ( 𝑚 − 3 ) + 𝑟 ) )
59 49 58 rspcedeq2vd ⊢ ( 𝑚 ∈ ℤ → ∃ 𝑟 ∈ ℙ 𝑚 = ( ( 𝑚 − 3 ) + 𝑟 ) )
60 oveq1 ⊢ ( ( 𝑚 − 3 ) = ( 𝑝 + 𝑞 ) → ( ( 𝑚 − 3 ) + 𝑟 ) = ( ( 𝑝 + 𝑞 ) + 𝑟 ) )
61 60 eqeq2d ⊢ ( ( 𝑚 − 3 ) = ( 𝑝 + 𝑞 ) → ( 𝑚 = ( ( 𝑚 − 3 ) + 𝑟 ) ↔ 𝑚 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
62 61 rexbidv ⊢ ( ( 𝑚 − 3 ) = ( 𝑝 + 𝑞 ) → ( ∃ 𝑟 ∈ ℙ 𝑚 = ( ( 𝑚 − 3 ) + 𝑟 ) ↔ ∃ 𝑟 ∈ ℙ 𝑚 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
63 59 62 imbitrid ⊢ ( ( 𝑚 − 3 ) = ( 𝑝 + 𝑞 ) → ( 𝑚 ∈ ℤ → ∃ 𝑟 ∈ ℙ 𝑚 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
64 63 3ad2ant3 ⊢ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ ( 𝑚 − 3 ) = ( 𝑝 + 𝑞 ) ) → ( 𝑚 ∈ ℤ → ∃ 𝑟 ∈ ℙ 𝑚 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
65 64 com12 ⊢ ( 𝑚 ∈ ℤ → ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ ( 𝑚 − 3 ) = ( 𝑝 + 𝑞 ) ) → ∃ 𝑟 ∈ ℙ 𝑚 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
66 65 ad4antlr ⊢ ( ( ( ( ( 7 < 𝑚 ∧ 𝑚 ∈ ℤ ) ∧ 𝑚 ∈ Odd ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) → ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ ( 𝑚 − 3 ) = ( 𝑝 + 𝑞 ) ) → ∃ 𝑟 ∈ ℙ 𝑚 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
67 66 reximdva ⊢ ( ( ( ( 7 < 𝑚 ∧ 𝑚 ∈ ℤ ) ∧ 𝑚 ∈ Odd ) ∧ 𝑝 ∈ ℙ ) → ( ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ ( 𝑚 − 3 ) = ( 𝑝 + 𝑞 ) ) → ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑚 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
68 67 reximdva ⊢ ( ( ( 7 < 𝑚 ∧ 𝑚 ∈ ℤ ) ∧ 𝑚 ∈ Odd ) → ( ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ ( 𝑚 − 3 ) = ( 𝑝 + 𝑞 ) ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑚 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
69 68 23 jctild ⊢ ( ( ( 7 < 𝑚 ∧ 𝑚 ∈ ℤ ) ∧ 𝑚 ∈ Odd ) → ( ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ ( 𝑚 − 3 ) = ( 𝑝 + 𝑞 ) ) → ( 𝑚 ∈ Odd ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑚 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) )
70 isgbow ⊢ ( 𝑚 ∈ GoldbachOddW ↔ ( 𝑚 ∈ Odd ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑚 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
71 69 70 imbitrrdi ⊢ ( ( ( 7 < 𝑚 ∧ 𝑚 ∈ ℤ ) ∧ 𝑚 ∈ Odd ) → ( ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ ( 𝑚 − 3 ) = ( 𝑝 + 𝑞 ) ) → 𝑚 ∈ GoldbachOddW ) )
72 71 adantld ⊢ ( ( ( 7 < 𝑚 ∧ 𝑚 ∈ ℤ ) ∧ 𝑚 ∈ Odd ) → ( ( ( 𝑚 − 3 ) ∈ Even ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ ( 𝑚 − 3 ) = ( 𝑝 + 𝑞 ) ) ) → 𝑚 ∈ GoldbachOddW ) )
73 47 72 biimtrid ⊢ ( ( ( 7 < 𝑚 ∧ 𝑚 ∈ ℤ ) ∧ 𝑚 ∈ Odd ) → ( ( 𝑚 − 3 ) ∈ GoldbachEven → 𝑚 ∈ GoldbachOddW ) )
74 31 46 73 3syld ⊢ ( ( ( 7 < 𝑚 ∧ 𝑚 ∈ ℤ ) ∧ 𝑚 ∈ Odd ) → ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → 𝑚 ∈ GoldbachOddW ) )
75 74 ex ⊢ ( ( 7 < 𝑚 ∧ 𝑚 ∈ ℤ ) → ( 𝑚 ∈ Odd → ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → 𝑚 ∈ GoldbachOddW ) ) )
76 75 com23 ⊢ ( ( 7 < 𝑚 ∧ 𝑚 ∈ ℤ ) → ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ( 𝑚 ∈ Odd → 𝑚 ∈ GoldbachOddW ) ) )
77 76 ex ⊢ ( 7 < 𝑚 → ( 𝑚 ∈ ℤ → ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ( 𝑚 ∈ Odd → 𝑚 ∈ GoldbachOddW ) ) ) )
78 7gbow ⊢ 7 ∈ GoldbachOddW
79 eleq1 ⊢ ( 7 = 𝑚 → ( 7 ∈ GoldbachOddW ↔ 𝑚 ∈ GoldbachOddW ) )
80 78 79 mpbii ⊢ ( 7 = 𝑚 → 𝑚 ∈ GoldbachOddW )
81 80 a1d ⊢ ( 7 = 𝑚 → ( 𝑚 ∈ Odd → 𝑚 ∈ GoldbachOddW ) )
82 81 a1d ⊢ ( 7 = 𝑚 → ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ( 𝑚 ∈ Odd → 𝑚 ∈ GoldbachOddW ) ) )
83 82 a1d ⊢ ( 7 = 𝑚 → ( 𝑚 ∈ ℤ → ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ( 𝑚 ∈ Odd → 𝑚 ∈ GoldbachOddW ) ) ) )
84 77 83 jaoi ⊢ ( ( 7 < 𝑚 ∨ 7 = 𝑚 ) → ( 𝑚 ∈ ℤ → ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ( 𝑚 ∈ Odd → 𝑚 ∈ GoldbachOddW ) ) ) )
85 84 com12 ⊢ ( 𝑚 ∈ ℤ → ( ( 7 < 𝑚 ∨ 7 = 𝑚 ) → ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ( 𝑚 ∈ Odd → 𝑚 ∈ GoldbachOddW ) ) ) )
86 22 85 sylbid ⊢ ( 𝑚 ∈ ℤ → ( ( 6 + 1 ) ≤ 𝑚 → ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ( 𝑚 ∈ Odd → 𝑚 ∈ GoldbachOddW ) ) ) )
87 16 86 sylbid ⊢ ( 𝑚 ∈ ℤ → ( 6 < 𝑚 → ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ( 𝑚 ∈ Odd → 𝑚 ∈ GoldbachOddW ) ) ) )
88 87 com12 ⊢ ( 6 < 𝑚 → ( 𝑚 ∈ ℤ → ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ( 𝑚 ∈ Odd → 𝑚 ∈ GoldbachOddW ) ) ) )
89 eleq1 ⊢ ( 6 = 𝑚 → ( 6 ∈ Odd ↔ 𝑚 ∈ Odd ) )
90 6even ⊢ 6 ∈ Even
91 evennodd ⊢ ( 6 ∈ Even → ¬ 6 ∈ Odd )
92 91 pm2.21d ⊢ ( 6 ∈ Even → ( 6 ∈ Odd → 𝑚 ∈ GoldbachOddW ) )
93 90 92 ax-mp ⊢ ( 6 ∈ Odd → 𝑚 ∈ GoldbachOddW )
94 89 93 biimtrrdi ⊢ ( 6 = 𝑚 → ( 𝑚 ∈ Odd → 𝑚 ∈ GoldbachOddW ) )
95 94 a1d ⊢ ( 6 = 𝑚 → ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ( 𝑚 ∈ Odd → 𝑚 ∈ GoldbachOddW ) ) )
96 95 a1d ⊢ ( 6 = 𝑚 → ( 𝑚 ∈ ℤ → ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ( 𝑚 ∈ Odd → 𝑚 ∈ GoldbachOddW ) ) ) )
97 88 96 jaoi ⊢ ( ( 6 < 𝑚 ∨ 6 = 𝑚 ) → ( 𝑚 ∈ ℤ → ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ( 𝑚 ∈ Odd → 𝑚 ∈ GoldbachOddW ) ) ) )
98 97 com12 ⊢ ( 𝑚 ∈ ℤ → ( ( 6 < 𝑚 ∨ 6 = 𝑚 ) → ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ( 𝑚 ∈ Odd → 𝑚 ∈ GoldbachOddW ) ) ) )
99 12 98 sylbid ⊢ ( 𝑚 ∈ ℤ → ( ( 5 + 1 ) ≤ 𝑚 → ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ( 𝑚 ∈ Odd → 𝑚 ∈ GoldbachOddW ) ) ) )
100 5 99 sylbid ⊢ ( 𝑚 ∈ ℤ → ( 5 < 𝑚 → ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ( 𝑚 ∈ Odd → 𝑚 ∈ GoldbachOddW ) ) ) )
101 100 com24 ⊢ ( 𝑚 ∈ ℤ → ( 𝑚 ∈ Odd → ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ( 5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) ) ) )
102 1 101 mpcom ⊢ ( 𝑚 ∈ Odd → ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ( 5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) ) )
103 102 impcom ⊢ ( ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) ∧ 𝑚 ∈ Odd ) → ( 5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) )
104 103 ralrimiva ⊢ ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∀ 𝑚 ∈ Odd ( 5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) )