Metamath Proof Explorer

Theorem sbgoldbst

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

Ref Expression
Assertion sbgoldbst ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∀ 𝑚 ∈ Odd ( 7 < 𝑚 → 𝑚 ∈ GoldbachOdd ) )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝑚 ∈ Odd ∧ 7 < 𝑚 ) → 𝑚 ∈ Odd )
2 3odd ⊢ 3 ∈ Odd
3 1 2 jctir ⊢ ( ( 𝑚 ∈ Odd ∧ 7 < 𝑚 ) → ( 𝑚 ∈ Odd ∧ 3 ∈ Odd ) )
4 omoeALTV ⊢ ( ( 𝑚 ∈ Odd ∧ 3 ∈ Odd ) → ( 𝑚 − 3 ) ∈ Even )
5 breq2 ⊢ ( 𝑛 = ( 𝑚 − 3 ) → ( 4 < 𝑛 ↔ 4 < ( 𝑚 − 3 ) ) )
6 eleq1 ⊢ ( 𝑛 = ( 𝑚 − 3 ) → ( 𝑛 ∈ GoldbachEven ↔ ( 𝑚 − 3 ) ∈ GoldbachEven ) )
7 5 6 imbi12d ⊢ ( 𝑛 = ( 𝑚 − 3 ) → ( ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) ↔ ( 4 < ( 𝑚 − 3 ) → ( 𝑚 − 3 ) ∈ GoldbachEven ) ) )
8 7 rspcv ⊢ ( ( 𝑚 − 3 ) ∈ Even → ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ( 4 < ( 𝑚 − 3 ) → ( 𝑚 − 3 ) ∈ GoldbachEven ) ) )
9 3 4 8 3syl ⊢ ( ( 𝑚 ∈ Odd ∧ 7 < 𝑚 ) → ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ( 4 < ( 𝑚 − 3 ) → ( 𝑚 − 3 ) ∈ GoldbachEven ) ) )
10 4p3e7 ⊢ ( 4 + 3 ) = 7
11 10 breq1i ⊢ ( ( 4 + 3 ) < 𝑚 ↔ 7 < 𝑚 )
12 4re ⊢ 4 ∈ ℝ
13 12 a1i ⊢ ( 𝑚 ∈ Odd → 4 ∈ ℝ )
14 3re ⊢ 3 ∈ ℝ
15 14 a1i ⊢ ( 𝑚 ∈ Odd → 3 ∈ ℝ )
16 oddz ⊢ ( 𝑚 ∈ Odd → 𝑚 ∈ ℤ )
17 16 zred ⊢ ( 𝑚 ∈ Odd → 𝑚 ∈ ℝ )
18 13 15 17 ltaddsubd ⊢ ( 𝑚 ∈ Odd → ( ( 4 + 3 ) < 𝑚 ↔ 4 < ( 𝑚 − 3 ) ) )
19 18 biimpd ⊢ ( 𝑚 ∈ Odd → ( ( 4 + 3 ) < 𝑚 → 4 < ( 𝑚 − 3 ) ) )
20 11 19 biimtrrid ⊢ ( 𝑚 ∈ Odd → ( 7 < 𝑚 → 4 < ( 𝑚 − 3 ) ) )
21 20 imp ⊢ ( ( 𝑚 ∈ Odd ∧ 7 < 𝑚 ) → 4 < ( 𝑚 − 3 ) )
22 pm2.27 ⊢ ( 4 < ( 𝑚 − 3 ) → ( ( 4 < ( 𝑚 − 3 ) → ( 𝑚 − 3 ) ∈ GoldbachEven ) → ( 𝑚 − 3 ) ∈ GoldbachEven ) )
23 21 22 syl ⊢ ( ( 𝑚 ∈ Odd ∧ 7 < 𝑚 ) → ( ( 4 < ( 𝑚 − 3 ) → ( 𝑚 − 3 ) ∈ GoldbachEven ) → ( 𝑚 − 3 ) ∈ GoldbachEven ) )
24 isgbe ⊢ ( ( 𝑚 − 3 ) ∈ GoldbachEven ↔ ( ( 𝑚 − 3 ) ∈ Even ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ ( 𝑚 − 3 ) = ( 𝑝 + 𝑞 ) ) ) )
25 3prm ⊢ 3 ∈ ℙ
26 25 a1i ⊢ ( ( ( ( ( 𝑚 ∈ Odd ∧ 7 < 𝑚 ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) ∧ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ ( 𝑚 − 3 ) = ( 𝑝 + 𝑞 ) ) ) → 3 ∈ ℙ )
27 eleq1 ⊢ ( 𝑟 = 3 → ( 𝑟 ∈ Odd ↔ 3 ∈ Odd ) )
28 27 3anbi3d ⊢ ( 𝑟 = 3 → ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ↔ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 3 ∈ Odd ) ) )
29 oveq2 ⊢ ( 𝑟 = 3 → ( ( 𝑝 + 𝑞 ) + 𝑟 ) = ( ( 𝑝 + 𝑞 ) + 3 ) )
30 29 eqeq2d ⊢ ( 𝑟 = 3 → ( 𝑚 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ↔ 𝑚 = ( ( 𝑝 + 𝑞 ) + 3 ) ) )
31 28 30 anbi12d ⊢ ( 𝑟 = 3 → ( ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑚 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ↔ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 3 ∈ Odd ) ∧ 𝑚 = ( ( 𝑝 + 𝑞 ) + 3 ) ) ) )
32 31 adantl ⊢ ( ( ( ( ( ( 𝑚 ∈ Odd ∧ 7 < 𝑚 ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) ∧ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ ( 𝑚 − 3 ) = ( 𝑝 + 𝑞 ) ) ) ∧ 𝑟 = 3 ) → ( ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑚 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ↔ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 3 ∈ Odd ) ∧ 𝑚 = ( ( 𝑝 + 𝑞 ) + 3 ) ) ) )
33 simp1 ⊢ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ ( 𝑚 − 3 ) = ( 𝑝 + 𝑞 ) ) → 𝑝 ∈ Odd )
34 simp2 ⊢ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ ( 𝑚 − 3 ) = ( 𝑝 + 𝑞 ) ) → 𝑞 ∈ Odd )
35 2 a1i ⊢ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ ( 𝑚 − 3 ) = ( 𝑝 + 𝑞 ) ) → 3 ∈ Odd )
36 33 34 35 3jca ⊢ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ ( 𝑚 − 3 ) = ( 𝑝 + 𝑞 ) ) → ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 3 ∈ Odd ) )
37 36 adantl ⊢ ( ( ( ( ( 𝑚 ∈ Odd ∧ 7 < 𝑚 ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) ∧ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ ( 𝑚 − 3 ) = ( 𝑝 + 𝑞 ) ) ) → ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 3 ∈ Odd ) )
38 16 zcnd ⊢ ( 𝑚 ∈ Odd → 𝑚 ∈ ℂ )
39 38 ad3antrrr ⊢ ( ( ( ( 𝑚 ∈ Odd ∧ 7 < 𝑚 ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) → 𝑚 ∈ ℂ )
40 3cn ⊢ 3 ∈ ℂ
41 40 a1i ⊢ ( ( ( ( 𝑚 ∈ Odd ∧ 7 < 𝑚 ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) → 3 ∈ ℂ )
42 prmz ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℤ )
43 prmz ⊢ ( 𝑞 ∈ ℙ → 𝑞 ∈ ℤ )
44 zaddcl ⊢ ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℤ ) → ( 𝑝 + 𝑞 ) ∈ ℤ )
45 42 43 44 syl2an ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) → ( 𝑝 + 𝑞 ) ∈ ℤ )
46 45 zcnd ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) → ( 𝑝 + 𝑞 ) ∈ ℂ )
47 46 adantll ⊢ ( ( ( ( 𝑚 ∈ Odd ∧ 7 < 𝑚 ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) → ( 𝑝 + 𝑞 ) ∈ ℂ )
48 39 41 47 subadd2d ⊢ ( ( ( ( 𝑚 ∈ Odd ∧ 7 < 𝑚 ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) → ( ( 𝑚 − 3 ) = ( 𝑝 + 𝑞 ) ↔ ( ( 𝑝 + 𝑞 ) + 3 ) = 𝑚 ) )
49 48 biimpa ⊢ ( ( ( ( ( 𝑚 ∈ Odd ∧ 7 < 𝑚 ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) ∧ ( 𝑚 − 3 ) = ( 𝑝 + 𝑞 ) ) → ( ( 𝑝 + 𝑞 ) + 3 ) = 𝑚 )
50 49 eqcomd ⊢ ( ( ( ( ( 𝑚 ∈ Odd ∧ 7 < 𝑚 ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) ∧ ( 𝑚 − 3 ) = ( 𝑝 + 𝑞 ) ) → 𝑚 = ( ( 𝑝 + 𝑞 ) + 3 ) )
51 50 3ad2antr3 ⊢ ( ( ( ( ( 𝑚 ∈ Odd ∧ 7 < 𝑚 ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) ∧ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ ( 𝑚 − 3 ) = ( 𝑝 + 𝑞 ) ) ) → 𝑚 = ( ( 𝑝 + 𝑞 ) + 3 ) )
52 37 51 jca ⊢ ( ( ( ( ( 𝑚 ∈ Odd ∧ 7 < 𝑚 ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) ∧ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ ( 𝑚 − 3 ) = ( 𝑝 + 𝑞 ) ) ) → ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 3 ∈ Odd ) ∧ 𝑚 = ( ( 𝑝 + 𝑞 ) + 3 ) ) )
53 26 32 52 rspcedvd ⊢ ( ( ( ( ( 𝑚 ∈ Odd ∧ 7 < 𝑚 ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) ∧ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ ( 𝑚 − 3 ) = ( 𝑝 + 𝑞 ) ) ) → ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑚 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
54 53 ex ⊢ ( ( ( ( 𝑚 ∈ Odd ∧ 7 < 𝑚 ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑞 ∈ ℙ ) → ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ ( 𝑚 − 3 ) = ( 𝑝 + 𝑞 ) ) → ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑚 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) )
55 54 reximdva ⊢ ( ( ( 𝑚 ∈ Odd ∧ 7 < 𝑚 ) ∧ 𝑝 ∈ ℙ ) → ( ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ ( 𝑚 − 3 ) = ( 𝑝 + 𝑞 ) ) → ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑚 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) )
56 55 reximdva ⊢ ( ( 𝑚 ∈ Odd ∧ 7 < 𝑚 ) → ( ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ ( 𝑚 − 3 ) = ( 𝑝 + 𝑞 ) ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑚 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) )
57 56 1 jctild ⊢ ( ( 𝑚 ∈ Odd ∧ 7 < 𝑚 ) → ( ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ ( 𝑚 − 3 ) = ( 𝑝 + 𝑞 ) ) → ( 𝑚 ∈ Odd ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑚 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) ) )
58 isgbo ⊢ ( 𝑚 ∈ GoldbachOdd ↔ ( 𝑚 ∈ Odd ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑚 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) )
59 57 58 imbitrrdi ⊢ ( ( 𝑚 ∈ Odd ∧ 7 < 𝑚 ) → ( ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ ( 𝑚 − 3 ) = ( 𝑝 + 𝑞 ) ) → 𝑚 ∈ GoldbachOdd ) )
60 59 adantld ⊢ ( ( 𝑚 ∈ Odd ∧ 7 < 𝑚 ) → ( ( ( 𝑚 − 3 ) ∈ Even ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ ( 𝑚 − 3 ) = ( 𝑝 + 𝑞 ) ) ) → 𝑚 ∈ GoldbachOdd ) )
61 24 60 biimtrid ⊢ ( ( 𝑚 ∈ Odd ∧ 7 < 𝑚 ) → ( ( 𝑚 − 3 ) ∈ GoldbachEven → 𝑚 ∈ GoldbachOdd ) )
62 9 23 61 3syld ⊢ ( ( 𝑚 ∈ Odd ∧ 7 < 𝑚 ) → ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → 𝑚 ∈ GoldbachOdd ) )
63 62 com12 ⊢ ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ( ( 𝑚 ∈ Odd ∧ 7 < 𝑚 ) → 𝑚 ∈ GoldbachOdd ) )
64 63 expd ⊢ ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ( 𝑚 ∈ Odd → ( 7 < 𝑚 → 𝑚 ∈ GoldbachOdd ) ) )
65 64 ralrimiv ⊢ ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∀ 𝑚 ∈ Odd ( 7 < 𝑚 → 𝑚 ∈ GoldbachOdd ) )