Metamath Proof Explorer

Theorem mogoldbb

Description: If the modern version of the original formulation of the Goldbach conjecture is valid, the (weak) binary Goldbach conjecture also holds. (Contributed by AV, 26-Dec-2021)

Ref Expression
Assertion mogoldbb ( ∀ 𝑛 ∈ ( ℤ≥ ‘ 6 ) ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) → ∀ 𝑛 ∈ Even ( 2 < 𝑛 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) )

Proof

Step Hyp Ref Expression
1 nfra1 ⊢ Ⅎ 𝑛 ∀ 𝑛 ∈ ( ℤ≥ ‘ 6 ) ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 )
2 eqeq1 ⊢ ( 𝑛 = 𝑚 → ( 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ↔ 𝑚 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
3 2 rexbidv ⊢ ( 𝑛 = 𝑚 → ( ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ↔ ∃ 𝑟 ∈ ℙ 𝑚 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
4 3 2rexbidv ⊢ ( 𝑛 = 𝑚 → ( ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ↔ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑚 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
5 4 cbvralvw ⊢ ( ∀ 𝑛 ∈ ( ℤ≥ ‘ 6 ) ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ↔ ∀ 𝑚 ∈ ( ℤ≥ ‘ 6 ) ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑚 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) )
6 6nn ⊢ 6 ∈ ℕ
7 6 nnzi ⊢ 6 ∈ ℤ
8 7 a1i ⊢ ( ( 𝑛 ∈ Even ∧ 2 < 𝑛 ) → 6 ∈ ℤ )
9 evenz ⊢ ( 𝑛 ∈ Even → 𝑛 ∈ ℤ )
10 2z ⊢ 2 ∈ ℤ
11 10 a1i ⊢ ( 𝑛 ∈ Even → 2 ∈ ℤ )
12 9 11 zaddcld ⊢ ( 𝑛 ∈ Even → ( 𝑛 + 2 ) ∈ ℤ )
13 12 adantr ⊢ ( ( 𝑛 ∈ Even ∧ 2 < 𝑛 ) → ( 𝑛 + 2 ) ∈ ℤ )
14 4cn ⊢ 4 ∈ ℂ
15 2cn ⊢ 2 ∈ ℂ
16 4p2e6 ⊢ ( 4 + 2 ) = 6
17 16 eqcomi ⊢ 6 = ( 4 + 2 )
18 14 15 17 mvrraddi ⊢ ( 6 − 2 ) = 4
19 2p2e4 ⊢ ( 2 + 2 ) = 4
20 2evenALTV ⊢ 2 ∈ Even
21 evenltle ⊢ ( ( 𝑛 ∈ Even ∧ 2 ∈ Even ∧ 2 < 𝑛 ) → ( 2 + 2 ) ≤ 𝑛 )
22 20 21 mp3an2 ⊢ ( ( 𝑛 ∈ Even ∧ 2 < 𝑛 ) → ( 2 + 2 ) ≤ 𝑛 )
23 19 22 eqbrtrrid ⊢ ( ( 𝑛 ∈ Even ∧ 2 < 𝑛 ) → 4 ≤ 𝑛 )
24 18 23 eqbrtrid ⊢ ( ( 𝑛 ∈ Even ∧ 2 < 𝑛 ) → ( 6 − 2 ) ≤ 𝑛 )
25 6re ⊢ 6 ∈ ℝ
26 25 a1i ⊢ ( 𝑛 ∈ Even → 6 ∈ ℝ )
27 2re ⊢ 2 ∈ ℝ
28 27 a1i ⊢ ( 𝑛 ∈ Even → 2 ∈ ℝ )
29 9 zred ⊢ ( 𝑛 ∈ Even → 𝑛 ∈ ℝ )
30 26 28 29 3jca ⊢ ( 𝑛 ∈ Even → ( 6 ∈ ℝ ∧ 2 ∈ ℝ ∧ 𝑛 ∈ ℝ ) )
31 30 adantr ⊢ ( ( 𝑛 ∈ Even ∧ 2 < 𝑛 ) → ( 6 ∈ ℝ ∧ 2 ∈ ℝ ∧ 𝑛 ∈ ℝ ) )
32 lesubadd ⊢ ( ( 6 ∈ ℝ ∧ 2 ∈ ℝ ∧ 𝑛 ∈ ℝ ) → ( ( 6 − 2 ) ≤ 𝑛 ↔ 6 ≤ ( 𝑛 + 2 ) ) )
33 31 32 syl ⊢ ( ( 𝑛 ∈ Even ∧ 2 < 𝑛 ) → ( ( 6 − 2 ) ≤ 𝑛 ↔ 6 ≤ ( 𝑛 + 2 ) ) )
34 24 33 mpbid ⊢ ( ( 𝑛 ∈ Even ∧ 2 < 𝑛 ) → 6 ≤ ( 𝑛 + 2 ) )
35 eluz2 ⊢ ( ( 𝑛 + 2 ) ∈ ( ℤ≥ ‘ 6 ) ↔ ( 6 ∈ ℤ ∧ ( 𝑛 + 2 ) ∈ ℤ ∧ 6 ≤ ( 𝑛 + 2 ) ) )
36 8 13 34 35 syl3anbrc ⊢ ( ( 𝑛 ∈ Even ∧ 2 < 𝑛 ) → ( 𝑛 + 2 ) ∈ ( ℤ≥ ‘ 6 ) )
37 eqeq1 ⊢ ( 𝑚 = ( 𝑛 + 2 ) → ( 𝑚 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ↔ ( 𝑛 + 2 ) = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
38 37 rexbidv ⊢ ( 𝑚 = ( 𝑛 + 2 ) → ( ∃ 𝑟 ∈ ℙ 𝑚 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ↔ ∃ 𝑟 ∈ ℙ ( 𝑛 + 2 ) = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
39 38 2rexbidv ⊢ ( 𝑚 = ( 𝑛 + 2 ) → ( ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑚 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ↔ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( 𝑛 + 2 ) = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
40 39 rspcv ⊢ ( ( 𝑛 + 2 ) ∈ ( ℤ≥ ‘ 6 ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 6 ) ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑚 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( 𝑛 + 2 ) = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
41 36 40 syl ⊢ ( ( 𝑛 ∈ Even ∧ 2 < 𝑛 ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 6 ) ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑚 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( 𝑛 + 2 ) = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
42 5 41 biimtrid ⊢ ( ( 𝑛 ∈ Even ∧ 2 < 𝑛 ) → ( ∀ 𝑛 ∈ ( ℤ≥ ‘ 6 ) ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( 𝑛 + 2 ) = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
43 nfv ⊢ Ⅎ 𝑝 ( 𝑛 ∈ Even ∧ 2 < 𝑛 )
44 nfre1 ⊢ Ⅎ 𝑝 ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 )
45 nfv ⊢ Ⅎ 𝑞 ( ( 𝑛 ∈ Even ∧ 2 < 𝑛 ) ∧ 𝑝 ∈ ℙ )
46 nfcv ⊢ Ⅎ 𝑞 ℙ
47 nfre1 ⊢ Ⅎ 𝑞 ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 )
48 46 47 nfrexw ⊢ Ⅎ 𝑞 ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 )
49 simplrl ⊢ ( ( ( ( 𝑛 ∈ Even ∧ 2 < 𝑛 ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ) ∧ 𝑟 ∈ ℙ ) → 𝑝 ∈ ℙ )
50 simplrr ⊢ ( ( ( ( 𝑛 ∈ Even ∧ 2 < 𝑛 ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ) ∧ 𝑟 ∈ ℙ ) → 𝑞 ∈ ℙ )
51 simpr ⊢ ( ( ( ( 𝑛 ∈ Even ∧ 2 < 𝑛 ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ) ∧ 𝑟 ∈ ℙ ) → 𝑟 ∈ ℙ )
52 49 50 51 3jca ⊢ ( ( ( ( 𝑛 ∈ Even ∧ 2 < 𝑛 ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ) ∧ 𝑟 ∈ ℙ ) → ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ∧ 𝑟 ∈ ℙ ) )
53 52 adantr ⊢ ( ( ( ( ( 𝑛 ∈ Even ∧ 2 < 𝑛 ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ) ∧ 𝑟 ∈ ℙ ) ∧ ( 𝑛 + 2 ) = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) → ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ∧ 𝑟 ∈ ℙ ) )
54 simp-4l ⊢ ( ( ( ( ( 𝑛 ∈ Even ∧ 2 < 𝑛 ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ) ∧ 𝑟 ∈ ℙ ) ∧ ( 𝑛 + 2 ) = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) → 𝑛 ∈ Even )
55 simpr ⊢ ( ( ( ( ( 𝑛 ∈ Even ∧ 2 < 𝑛 ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ) ∧ 𝑟 ∈ ℙ ) ∧ ( 𝑛 + 2 ) = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) → ( 𝑛 + 2 ) = ( ( 𝑝 + 𝑞 ) + 𝑟 ) )
56 mogoldbblem ⊢ ( ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ∧ 𝑟 ∈ ℙ ) ∧ 𝑛 ∈ Even ∧ ( 𝑛 + 2 ) = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) → ∃ 𝑦 ∈ ℙ ∃ 𝑥 ∈ ℙ 𝑛 = ( 𝑦 + 𝑥 ) )
57 oveq1 ⊢ ( 𝑝 = 𝑦 → ( 𝑝 + 𝑞 ) = ( 𝑦 + 𝑞 ) )
58 57 eqeq2d ⊢ ( 𝑝 = 𝑦 → ( 𝑛 = ( 𝑝 + 𝑞 ) ↔ 𝑛 = ( 𝑦 + 𝑞 ) ) )
59 oveq2 ⊢ ( 𝑞 = 𝑥 → ( 𝑦 + 𝑞 ) = ( 𝑦 + 𝑥 ) )
60 59 eqeq2d ⊢ ( 𝑞 = 𝑥 → ( 𝑛 = ( 𝑦 + 𝑞 ) ↔ 𝑛 = ( 𝑦 + 𝑥 ) ) )
61 58 60 cbvrex2vw ⊢ ( ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ↔ ∃ 𝑦 ∈ ℙ ∃ 𝑥 ∈ ℙ 𝑛 = ( 𝑦 + 𝑥 ) )
62 56 61 sylibr ⊢ ( ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ∧ 𝑟 ∈ ℙ ) ∧ 𝑛 ∈ Even ∧ ( 𝑛 + 2 ) = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) )
63 53 54 55 62 syl3anc ⊢ ( ( ( ( ( 𝑛 ∈ Even ∧ 2 < 𝑛 ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ) ∧ 𝑟 ∈ ℙ ) ∧ ( 𝑛 + 2 ) = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) )
64 63 rexlimdva2 ⊢ ( ( ( 𝑛 ∈ Even ∧ 2 < 𝑛 ) ∧ ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ) → ( ∃ 𝑟 ∈ ℙ ( 𝑛 + 2 ) = ( ( 𝑝 + 𝑞 ) + 𝑟 ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) )
65 64 expr ⊢ ( ( ( 𝑛 ∈ Even ∧ 2 < 𝑛 ) ∧ 𝑝 ∈ ℙ ) → ( 𝑞 ∈ ℙ → ( ∃ 𝑟 ∈ ℙ ( 𝑛 + 2 ) = ( ( 𝑝 + 𝑞 ) + 𝑟 ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) ) )
66 45 48 65 rexlimd ⊢ ( ( ( 𝑛 ∈ Even ∧ 2 < 𝑛 ) ∧ 𝑝 ∈ ℙ ) → ( ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( 𝑛 + 2 ) = ( ( 𝑝 + 𝑞 ) + 𝑟 ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) )
67 66 ex ⊢ ( ( 𝑛 ∈ Even ∧ 2 < 𝑛 ) → ( 𝑝 ∈ ℙ → ( ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( 𝑛 + 2 ) = ( ( 𝑝 + 𝑞 ) + 𝑟 ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) ) )
68 43 44 67 rexlimd ⊢ ( ( 𝑛 ∈ Even ∧ 2 < 𝑛 ) → ( ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( 𝑛 + 2 ) = ( ( 𝑝 + 𝑞 ) + 𝑟 ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) )
69 42 68 syldc ⊢ ( ∀ 𝑛 ∈ ( ℤ≥ ‘ 6 ) ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) → ( ( 𝑛 ∈ Even ∧ 2 < 𝑛 ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) )
70 69 expd ⊢ ( ∀ 𝑛 ∈ ( ℤ≥ ‘ 6 ) ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) → ( 𝑛 ∈ Even → ( 2 < 𝑛 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) ) )
71 1 70 ralrimi ⊢ ( ∀ 𝑛 ∈ ( ℤ≥ ‘ 6 ) ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) → ∀ 𝑛 ∈ Even ( 2 < 𝑛 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) )