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

Metamath Proof Explorer

Theorem sbgoldbo

Description: If the strong binary Goldbach conjecture is valid, the original formulation of the Goldbach conjecture also holds: Every integer greater than 2 can be expressed as the sum of three "primes" with regarding 1 to be a prime (as Goldbach did). Original text: "Es scheint wenigstens, dass eine jede Zahl, die groesser ist als 2, ein aggregatum trium numerorum primorum sey." (Goldbach, 1742). (Contributed by AV, 25-Dec-2021)

Ref Expression
Hypothesis sbgoldbo.p ⊢ 𝑃 = ( { 1 } ∪ ℙ )
Assertion sbgoldbo ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∀ 𝑛 ∈ ( ℤ≥ ‘ 3 ) ∃ 𝑝 ∈ 𝑃 ∃ 𝑞 ∈ 𝑃 ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) )

Proof

Step Hyp Ref Expression
1 sbgoldbo.p ⊢ 𝑃 = ( { 1 } ∪ ℙ )
2 nfra1 ⊢ Ⅎ 𝑛 ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven )
3 3z ⊢ 3 ∈ ℤ
4 6nn ⊢ 6 ∈ ℕ
5 4 nnzi ⊢ 6 ∈ ℤ
6 3re ⊢ 3 ∈ ℝ
7 6re ⊢ 6 ∈ ℝ
8 3lt6 ⊢ 3 < 6
9 6 7 8 ltleii ⊢ 3 ≤ 6
10 eluz2 ⊢ ( 6 ∈ ( ℤ≥ ‘ 3 ) ↔ ( 3 ∈ ℤ ∧ 6 ∈ ℤ ∧ 3 ≤ 6 ) )
11 3 5 9 10 mpbir3an ⊢ 6 ∈ ( ℤ≥ ‘ 3 )
12 uzsplit ⊢ ( 6 ∈ ( ℤ≥ ‘ 3 ) → ( ℤ≥ ‘ 3 ) = ( ( 3 ... ( 6 − 1 ) ) ∪ ( ℤ≥ ‘ 6 ) ) )
13 12 eleq2d ⊢ ( 6 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑛 ∈ ( ℤ≥ ‘ 3 ) ↔ 𝑛 ∈ ( ( 3 ... ( 6 − 1 ) ) ∪ ( ℤ≥ ‘ 6 ) ) ) )
14 11 13 ax-mp ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 3 ) ↔ 𝑛 ∈ ( ( 3 ... ( 6 − 1 ) ) ∪ ( ℤ≥ ‘ 6 ) ) )
15 elun ⊢ ( 𝑛 ∈ ( ( 3 ... ( 6 − 1 ) ) ∪ ( ℤ≥ ‘ 6 ) ) ↔ ( 𝑛 ∈ ( 3 ... ( 6 − 1 ) ) ∨ 𝑛 ∈ ( ℤ≥ ‘ 6 ) ) )
16 6m1e5 ⊢ ( 6 − 1 ) = 5
17 16 oveq2i ⊢ ( 3 ... ( 6 − 1 ) ) = ( 3 ... 5 )
18 5nn ⊢ 5 ∈ ℕ
19 18 nnzi ⊢ 5 ∈ ℤ
20 5re ⊢ 5 ∈ ℝ
21 3lt5 ⊢ 3 < 5
22 6 20 21 ltleii ⊢ 3 ≤ 5
23 eluz2 ⊢ ( 5 ∈ ( ℤ≥ ‘ 3 ) ↔ ( 3 ∈ ℤ ∧ 5 ∈ ℤ ∧ 3 ≤ 5 ) )
24 3 19 22 23 mpbir3an ⊢ 5 ∈ ( ℤ≥ ‘ 3 )
25 fzopredsuc ⊢ ( 5 ∈ ( ℤ≥ ‘ 3 ) → ( 3 ... 5 ) = ( ( { 3 } ∪ ( ( 3 + 1 ) ..^ 5 ) ) ∪ { 5 } ) )
26 24 25 ax-mp ⊢ ( 3 ... 5 ) = ( ( { 3 } ∪ ( ( 3 + 1 ) ..^ 5 ) ) ∪ { 5 } )
27 17 26 eqtri ⊢ ( 3 ... ( 6 − 1 ) ) = ( ( { 3 } ∪ ( ( 3 + 1 ) ..^ 5 ) ) ∪ { 5 } )
28 27 eleq2i ⊢ ( 𝑛 ∈ ( 3 ... ( 6 − 1 ) ) ↔ 𝑛 ∈ ( ( { 3 } ∪ ( ( 3 + 1 ) ..^ 5 ) ) ∪ { 5 } ) )
29 elun ⊢ ( 𝑛 ∈ ( ( { 3 } ∪ ( ( 3 + 1 ) ..^ 5 ) ) ∪ { 5 } ) ↔ ( 𝑛 ∈ ( { 3 } ∪ ( ( 3 + 1 ) ..^ 5 ) ) ∨ 𝑛 ∈ { 5 } ) )
30 elun ⊢ ( 𝑛 ∈ ( { 3 } ∪ ( ( 3 + 1 ) ..^ 5 ) ) ↔ ( 𝑛 ∈ { 3 } ∨ 𝑛 ∈ ( ( 3 + 1 ) ..^ 5 ) ) )
31 elsni ⊢ ( 𝑛 ∈ { 3 } → 𝑛 = 3 )
32 1ex ⊢ 1 ∈ V
33 32 snid ⊢ 1 ∈ { 1 }
34 33 orci ⊢ ( 1 ∈ { 1 } ∨ 1 ∈ ℙ )
35 elun ⊢ ( 1 ∈ ( { 1 } ∪ ℙ ) ↔ ( 1 ∈ { 1 } ∨ 1 ∈ ℙ ) )
36 34 35 mpbir ⊢ 1 ∈ ( { 1 } ∪ ℙ )
37 36 1 eleqtrri ⊢ 1 ∈ 𝑃
38 37 a1i ⊢ ( 𝑛 = 3 → 1 ∈ 𝑃 )
39 simpl ⊢ ( ( 𝑛 = 3 ∧ 𝑝 = 1 ) → 𝑛 = 3 )
40 oveq1 ⊢ ( 𝑝 = 1 → ( 𝑝 + 𝑞 ) = ( 1 + 𝑞 ) )
41 40 oveq1d ⊢ ( 𝑝 = 1 → ( ( 𝑝 + 𝑞 ) + 𝑟 ) = ( ( 1 + 𝑞 ) + 𝑟 ) )
42 41 adantl ⊢ ( ( 𝑛 = 3 ∧ 𝑝 = 1 ) → ( ( 𝑝 + 𝑞 ) + 𝑟 ) = ( ( 1 + 𝑞 ) + 𝑟 ) )
43 39 42 eqeq12d ⊢ ( ( 𝑛 = 3 ∧ 𝑝 = 1 ) → ( 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ↔ 3 = ( ( 1 + 𝑞 ) + 𝑟 ) ) )
44 43 2rexbidv ⊢ ( ( 𝑛 = 3 ∧ 𝑝 = 1 ) → ( ∃ 𝑞 ∈ 𝑃 ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ↔ ∃ 𝑞 ∈ 𝑃 ∃ 𝑟 ∈ 𝑃 3 = ( ( 1 + 𝑞 ) + 𝑟 ) ) )
45 oveq2 ⊢ ( 𝑞 = 1 → ( 1 + 𝑞 ) = ( 1 + 1 ) )
46 45 oveq1d ⊢ ( 𝑞 = 1 → ( ( 1 + 𝑞 ) + 𝑟 ) = ( ( 1 + 1 ) + 𝑟 ) )
47 46 eqeq2d ⊢ ( 𝑞 = 1 → ( 3 = ( ( 1 + 𝑞 ) + 𝑟 ) ↔ 3 = ( ( 1 + 1 ) + 𝑟 ) ) )
48 47 rexbidv ⊢ ( 𝑞 = 1 → ( ∃ 𝑟 ∈ 𝑃 3 = ( ( 1 + 𝑞 ) + 𝑟 ) ↔ ∃ 𝑟 ∈ 𝑃 3 = ( ( 1 + 1 ) + 𝑟 ) ) )
49 48 adantl ⊢ ( ( 𝑛 = 3 ∧ 𝑞 = 1 ) → ( ∃ 𝑟 ∈ 𝑃 3 = ( ( 1 + 𝑞 ) + 𝑟 ) ↔ ∃ 𝑟 ∈ 𝑃 3 = ( ( 1 + 1 ) + 𝑟 ) ) )
50 df-3 ⊢ 3 = ( 2 + 1 )
51 df-2 ⊢ 2 = ( 1 + 1 )
52 51 oveq1i ⊢ ( 2 + 1 ) = ( ( 1 + 1 ) + 1 )
53 50 52 eqtri ⊢ 3 = ( ( 1 + 1 ) + 1 )
54 oveq2 ⊢ ( 𝑟 = 1 → ( ( 1 + 1 ) + 𝑟 ) = ( ( 1 + 1 ) + 1 ) )
55 53 54 eqtr4id ⊢ ( 𝑟 = 1 → 3 = ( ( 1 + 1 ) + 𝑟 ) )
56 55 adantl ⊢ ( ( 𝑛 = 3 ∧ 𝑟 = 1 ) → 3 = ( ( 1 + 1 ) + 𝑟 ) )
57 38 56 rspcedeq2vd ⊢ ( 𝑛 = 3 → ∃ 𝑟 ∈ 𝑃 3 = ( ( 1 + 1 ) + 𝑟 ) )
58 38 49 57 rspcedvd ⊢ ( 𝑛 = 3 → ∃ 𝑞 ∈ 𝑃 ∃ 𝑟 ∈ 𝑃 3 = ( ( 1 + 𝑞 ) + 𝑟 ) )
59 38 44 58 rspcedvd ⊢ ( 𝑛 = 3 → ∃ 𝑝 ∈ 𝑃 ∃ 𝑞 ∈ 𝑃 ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) )
60 31 59 syl ⊢ ( 𝑛 ∈ { 3 } → ∃ 𝑝 ∈ 𝑃 ∃ 𝑞 ∈ 𝑃 ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) )
61 3p1e4 ⊢ ( 3 + 1 ) = 4
62 df-5 ⊢ 5 = ( 4 + 1 )
63 61 62 oveq12i ⊢ ( ( 3 + 1 ) ..^ 5 ) = ( 4 ..^ ( 4 + 1 ) )
64 4z ⊢ 4 ∈ ℤ
65 fzval3 ⊢ ( 4 ∈ ℤ → ( 4 ... 4 ) = ( 4 ..^ ( 4 + 1 ) ) )
66 64 65 ax-mp ⊢ ( 4 ... 4 ) = ( 4 ..^ ( 4 + 1 ) )
67 63 66 eqtr4i ⊢ ( ( 3 + 1 ) ..^ 5 ) = ( 4 ... 4 )
68 67 eleq2i ⊢ ( 𝑛 ∈ ( ( 3 + 1 ) ..^ 5 ) ↔ 𝑛 ∈ ( 4 ... 4 ) )
69 fzsn ⊢ ( 4 ∈ ℤ → ( 4 ... 4 ) = { 4 } )
70 64 69 ax-mp ⊢ ( 4 ... 4 ) = { 4 }
71 70 eleq2i ⊢ ( 𝑛 ∈ ( 4 ... 4 ) ↔ 𝑛 ∈ { 4 } )
72 68 71 bitri ⊢ ( 𝑛 ∈ ( ( 3 + 1 ) ..^ 5 ) ↔ 𝑛 ∈ { 4 } )
73 elsni ⊢ ( 𝑛 ∈ { 4 } → 𝑛 = 4 )
74 2prm ⊢ 2 ∈ ℙ
75 74 olci ⊢ ( 2 ∈ { 1 } ∨ 2 ∈ ℙ )
76 elun ⊢ ( 2 ∈ ( { 1 } ∪ ℙ ) ↔ ( 2 ∈ { 1 } ∨ 2 ∈ ℙ ) )
77 75 76 mpbir ⊢ 2 ∈ ( { 1 } ∪ ℙ )
78 77 1 eleqtrri ⊢ 2 ∈ 𝑃
79 78 a1i ⊢ ( 𝑛 = 4 → 2 ∈ 𝑃 )
80 oveq1 ⊢ ( 𝑝 = 2 → ( 𝑝 + 𝑞 ) = ( 2 + 𝑞 ) )
81 80 oveq1d ⊢ ( 𝑝 = 2 → ( ( 𝑝 + 𝑞 ) + 𝑟 ) = ( ( 2 + 𝑞 ) + 𝑟 ) )
82 81 eqeq2d ⊢ ( 𝑝 = 2 → ( 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ↔ 𝑛 = ( ( 2 + 𝑞 ) + 𝑟 ) ) )
83 82 2rexbidv ⊢ ( 𝑝 = 2 → ( ∃ 𝑞 ∈ 𝑃 ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ↔ ∃ 𝑞 ∈ 𝑃 ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 2 + 𝑞 ) + 𝑟 ) ) )
84 83 adantl ⊢ ( ( 𝑛 = 4 ∧ 𝑝 = 2 ) → ( ∃ 𝑞 ∈ 𝑃 ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ↔ ∃ 𝑞 ∈ 𝑃 ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 2 + 𝑞 ) + 𝑟 ) ) )
85 37 a1i ⊢ ( 𝑛 = 4 → 1 ∈ 𝑃 )
86 oveq2 ⊢ ( 𝑞 = 1 → ( 2 + 𝑞 ) = ( 2 + 1 ) )
87 86 oveq1d ⊢ ( 𝑞 = 1 → ( ( 2 + 𝑞 ) + 𝑟 ) = ( ( 2 + 1 ) + 𝑟 ) )
88 87 eqeq2d ⊢ ( 𝑞 = 1 → ( 𝑛 = ( ( 2 + 𝑞 ) + 𝑟 ) ↔ 𝑛 = ( ( 2 + 1 ) + 𝑟 ) ) )
89 88 rexbidv ⊢ ( 𝑞 = 1 → ( ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 2 + 𝑞 ) + 𝑟 ) ↔ ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 2 + 1 ) + 𝑟 ) ) )
90 89 adantl ⊢ ( ( 𝑛 = 4 ∧ 𝑞 = 1 ) → ( ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 2 + 𝑞 ) + 𝑟 ) ↔ ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 2 + 1 ) + 𝑟 ) ) )
91 simpl ⊢ ( ( 𝑛 = 4 ∧ 𝑟 = 1 ) → 𝑛 = 4 )
92 df-4 ⊢ 4 = ( 3 + 1 )
93 50 oveq1i ⊢ ( 3 + 1 ) = ( ( 2 + 1 ) + 1 )
94 92 93 eqtri ⊢ 4 = ( ( 2 + 1 ) + 1 )
95 94 a1i ⊢ ( ( 𝑛 = 4 ∧ 𝑟 = 1 ) → 4 = ( ( 2 + 1 ) + 1 ) )
96 oveq2 ⊢ ( 𝑟 = 1 → ( ( 2 + 1 ) + 𝑟 ) = ( ( 2 + 1 ) + 1 ) )
97 96 eqcomd ⊢ ( 𝑟 = 1 → ( ( 2 + 1 ) + 1 ) = ( ( 2 + 1 ) + 𝑟 ) )
98 97 adantl ⊢ ( ( 𝑛 = 4 ∧ 𝑟 = 1 ) → ( ( 2 + 1 ) + 1 ) = ( ( 2 + 1 ) + 𝑟 ) )
99 95 98 eqtrd ⊢ ( ( 𝑛 = 4 ∧ 𝑟 = 1 ) → 4 = ( ( 2 + 1 ) + 𝑟 ) )
100 91 99 eqtrd ⊢ ( ( 𝑛 = 4 ∧ 𝑟 = 1 ) → 𝑛 = ( ( 2 + 1 ) + 𝑟 ) )
101 85 100 rspcedeq2vd ⊢ ( 𝑛 = 4 → ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 2 + 1 ) + 𝑟 ) )
102 85 90 101 rspcedvd ⊢ ( 𝑛 = 4 → ∃ 𝑞 ∈ 𝑃 ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 2 + 𝑞 ) + 𝑟 ) )
103 79 84 102 rspcedvd ⊢ ( 𝑛 = 4 → ∃ 𝑝 ∈ 𝑃 ∃ 𝑞 ∈ 𝑃 ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) )
104 73 103 syl ⊢ ( 𝑛 ∈ { 4 } → ∃ 𝑝 ∈ 𝑃 ∃ 𝑞 ∈ 𝑃 ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) )
105 72 104 sylbi ⊢ ( 𝑛 ∈ ( ( 3 + 1 ) ..^ 5 ) → ∃ 𝑝 ∈ 𝑃 ∃ 𝑞 ∈ 𝑃 ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) )
106 60 105 jaoi ⊢ ( ( 𝑛 ∈ { 3 } ∨ 𝑛 ∈ ( ( 3 + 1 ) ..^ 5 ) ) → ∃ 𝑝 ∈ 𝑃 ∃ 𝑞 ∈ 𝑃 ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) )
107 30 106 sylbi ⊢ ( 𝑛 ∈ ( { 3 } ∪ ( ( 3 + 1 ) ..^ 5 ) ) → ∃ 𝑝 ∈ 𝑃 ∃ 𝑞 ∈ 𝑃 ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) )
108 elsni ⊢ ( 𝑛 ∈ { 5 } → 𝑛 = 5 )
109 3prm ⊢ 3 ∈ ℙ
110 109 olci ⊢ ( 3 ∈ { 1 } ∨ 3 ∈ ℙ )
111 elun ⊢ ( 3 ∈ ( { 1 } ∪ ℙ ) ↔ ( 3 ∈ { 1 } ∨ 3 ∈ ℙ ) )
112 110 111 mpbir ⊢ 3 ∈ ( { 1 } ∪ ℙ )
113 112 1 eleqtrri ⊢ 3 ∈ 𝑃
114 113 a1i ⊢ ( 𝑛 = 5 → 3 ∈ 𝑃 )
115 oveq1 ⊢ ( 𝑝 = 3 → ( 𝑝 + 𝑞 ) = ( 3 + 𝑞 ) )
116 115 oveq1d ⊢ ( 𝑝 = 3 → ( ( 𝑝 + 𝑞 ) + 𝑟 ) = ( ( 3 + 𝑞 ) + 𝑟 ) )
117 116 eqeq2d ⊢ ( 𝑝 = 3 → ( 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ↔ 𝑛 = ( ( 3 + 𝑞 ) + 𝑟 ) ) )
118 117 2rexbidv ⊢ ( 𝑝 = 3 → ( ∃ 𝑞 ∈ 𝑃 ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ↔ ∃ 𝑞 ∈ 𝑃 ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 3 + 𝑞 ) + 𝑟 ) ) )
119 118 adantl ⊢ ( ( 𝑛 = 5 ∧ 𝑝 = 3 ) → ( ∃ 𝑞 ∈ 𝑃 ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ↔ ∃ 𝑞 ∈ 𝑃 ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 3 + 𝑞 ) + 𝑟 ) ) )
120 37 a1i ⊢ ( 𝑛 = 5 → 1 ∈ 𝑃 )
121 oveq2 ⊢ ( 𝑞 = 1 → ( 3 + 𝑞 ) = ( 3 + 1 ) )
122 121 oveq1d ⊢ ( 𝑞 = 1 → ( ( 3 + 𝑞 ) + 𝑟 ) = ( ( 3 + 1 ) + 𝑟 ) )
123 122 eqeq2d ⊢ ( 𝑞 = 1 → ( 𝑛 = ( ( 3 + 𝑞 ) + 𝑟 ) ↔ 𝑛 = ( ( 3 + 1 ) + 𝑟 ) ) )
124 123 rexbidv ⊢ ( 𝑞 = 1 → ( ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 3 + 𝑞 ) + 𝑟 ) ↔ ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 3 + 1 ) + 𝑟 ) ) )
125 124 adantl ⊢ ( ( 𝑛 = 5 ∧ 𝑞 = 1 ) → ( ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 3 + 𝑞 ) + 𝑟 ) ↔ ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 3 + 1 ) + 𝑟 ) ) )
126 simpl ⊢ ( ( 𝑛 = 5 ∧ 𝑟 = 1 ) → 𝑛 = 5 )
127 92 oveq1i ⊢ ( 4 + 1 ) = ( ( 3 + 1 ) + 1 )
128 62 127 eqtri ⊢ 5 = ( ( 3 + 1 ) + 1 )
129 oveq2 ⊢ ( 𝑟 = 1 → ( ( 3 + 1 ) + 𝑟 ) = ( ( 3 + 1 ) + 1 ) )
130 128 129 eqtr4id ⊢ ( 𝑟 = 1 → 5 = ( ( 3 + 1 ) + 𝑟 ) )
131 130 adantl ⊢ ( ( 𝑛 = 5 ∧ 𝑟 = 1 ) → 5 = ( ( 3 + 1 ) + 𝑟 ) )
132 126 131 eqtrd ⊢ ( ( 𝑛 = 5 ∧ 𝑟 = 1 ) → 𝑛 = ( ( 3 + 1 ) + 𝑟 ) )
133 120 132 rspcedeq2vd ⊢ ( 𝑛 = 5 → ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 3 + 1 ) + 𝑟 ) )
134 120 125 133 rspcedvd ⊢ ( 𝑛 = 5 → ∃ 𝑞 ∈ 𝑃 ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 3 + 𝑞 ) + 𝑟 ) )
135 114 119 134 rspcedvd ⊢ ( 𝑛 = 5 → ∃ 𝑝 ∈ 𝑃 ∃ 𝑞 ∈ 𝑃 ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) )
136 108 135 syl ⊢ ( 𝑛 ∈ { 5 } → ∃ 𝑝 ∈ 𝑃 ∃ 𝑞 ∈ 𝑃 ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) )
137 107 136 jaoi ⊢ ( ( 𝑛 ∈ ( { 3 } ∪ ( ( 3 + 1 ) ..^ 5 ) ) ∨ 𝑛 ∈ { 5 } ) → ∃ 𝑝 ∈ 𝑃 ∃ 𝑞 ∈ 𝑃 ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) )
138 29 137 sylbi ⊢ ( 𝑛 ∈ ( ( { 3 } ∪ ( ( 3 + 1 ) ..^ 5 ) ) ∪ { 5 } ) → ∃ 𝑝 ∈ 𝑃 ∃ 𝑞 ∈ 𝑃 ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) )
139 138 a1d ⊢ ( 𝑛 ∈ ( ( { 3 } ∪ ( ( 3 + 1 ) ..^ 5 ) ) ∪ { 5 } ) → ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∃ 𝑝 ∈ 𝑃 ∃ 𝑞 ∈ 𝑃 ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
140 28 139 sylbi ⊢ ( 𝑛 ∈ ( 3 ... ( 6 − 1 ) ) → ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∃ 𝑝 ∈ 𝑃 ∃ 𝑞 ∈ 𝑃 ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
141 sbgoldbm ⊢ ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∀ 𝑛 ∈ ( ℤ≥ ‘ 6 ) ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) )
142 rspa ⊢ ( ( ∀ 𝑛 ∈ ( ℤ≥ ‘ 6 ) ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 6 ) ) → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) )
143 ssun2 ⊢ ℙ ⊆ ( { 1 } ∪ ℙ )
144 143 1 sseqtrri ⊢ ℙ ⊆ 𝑃
145 rexss ⊢ ( ℙ ⊆ 𝑃 → ( ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ↔ ∃ 𝑝 ∈ 𝑃 ( 𝑝 ∈ ℙ ∧ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) )
146 144 145 ax-mp ⊢ ( ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ↔ ∃ 𝑝 ∈ 𝑃 ( 𝑝 ∈ ℙ ∧ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
147 rexss ⊢ ( ℙ ⊆ 𝑃 → ( ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ↔ ∃ 𝑞 ∈ 𝑃 ( 𝑞 ∈ ℙ ∧ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) )
148 144 147 ax-mp ⊢ ( ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ↔ ∃ 𝑞 ∈ 𝑃 ( 𝑞 ∈ ℙ ∧ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
149 rexss ⊢ ( ℙ ⊆ 𝑃 → ( ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ↔ ∃ 𝑟 ∈ 𝑃 ( 𝑟 ∈ ℙ ∧ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) )
150 144 149 ax-mp ⊢ ( ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ↔ ∃ 𝑟 ∈ 𝑃 ( 𝑟 ∈ ℙ ∧ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
151 simpr ⊢ ( ( 𝑟 ∈ ℙ ∧ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) → 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) )
152 151 reximi ⊢ ( ∃ 𝑟 ∈ 𝑃 ( 𝑟 ∈ ℙ ∧ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) → ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) )
153 150 152 sylbi ⊢ ( ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) → ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) )
154 153 adantl ⊢ ( ( 𝑞 ∈ ℙ ∧ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) → ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) )
155 154 reximi ⊢ ( ∃ 𝑞 ∈ 𝑃 ( 𝑞 ∈ ℙ ∧ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) → ∃ 𝑞 ∈ 𝑃 ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) )
156 148 155 sylbi ⊢ ( ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) → ∃ 𝑞 ∈ 𝑃 ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) )
157 156 adantl ⊢ ( ( 𝑝 ∈ ℙ ∧ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) → ∃ 𝑞 ∈ 𝑃 ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) )
158 157 reximi ⊢ ( ∃ 𝑝 ∈ 𝑃 ( 𝑝 ∈ ℙ ∧ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) → ∃ 𝑝 ∈ 𝑃 ∃ 𝑞 ∈ 𝑃 ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) )
159 146 158 sylbi ⊢ ( ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) → ∃ 𝑝 ∈ 𝑃 ∃ 𝑞 ∈ 𝑃 ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) )
160 142 159 syl ⊢ ( ( ∀ 𝑛 ∈ ( ℤ≥ ‘ 6 ) ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 6 ) ) → ∃ 𝑝 ∈ 𝑃 ∃ 𝑞 ∈ 𝑃 ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) )
161 160 ex ⊢ ( ∀ 𝑛 ∈ ( ℤ≥ ‘ 6 ) ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) → ( 𝑛 ∈ ( ℤ≥ ‘ 6 ) → ∃ 𝑝 ∈ 𝑃 ∃ 𝑞 ∈ 𝑃 ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
162 141 161 syl ⊢ ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ( 𝑛 ∈ ( ℤ≥ ‘ 6 ) → ∃ 𝑝 ∈ 𝑃 ∃ 𝑞 ∈ 𝑃 ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
163 162 com12 ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 6 ) → ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∃ 𝑝 ∈ 𝑃 ∃ 𝑞 ∈ 𝑃 ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
164 140 163 jaoi ⊢ ( ( 𝑛 ∈ ( 3 ... ( 6 − 1 ) ) ∨ 𝑛 ∈ ( ℤ≥ ‘ 6 ) ) → ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∃ 𝑝 ∈ 𝑃 ∃ 𝑞 ∈ 𝑃 ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
165 15 164 sylbi ⊢ ( 𝑛 ∈ ( ( 3 ... ( 6 − 1 ) ) ∪ ( ℤ≥ ‘ 6 ) ) → ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∃ 𝑝 ∈ 𝑃 ∃ 𝑞 ∈ 𝑃 ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
166 165 com12 ⊢ ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ( 𝑛 ∈ ( ( 3 ... ( 6 − 1 ) ) ∪ ( ℤ≥ ‘ 6 ) ) → ∃ 𝑝 ∈ 𝑃 ∃ 𝑞 ∈ 𝑃 ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
167 14 166 biimtrid ⊢ ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ( 𝑛 ∈ ( ℤ≥ ‘ 3 ) → ∃ 𝑝 ∈ 𝑃 ∃ 𝑞 ∈ 𝑃 ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) )
168 2 167 ralrimi ⊢ ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∀ 𝑛 ∈ ( ℤ≥ ‘ 3 ) ∃ 𝑝 ∈ 𝑃 ∃ 𝑞 ∈ 𝑃 ∃ 𝑟 ∈ 𝑃 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) )