Metamath Proof Explorer

Theorem nnsum4primesevenALTV

Description: If the (strong) ternary Goldbach conjecture is valid, then every even integer greater than 10 is the sum of 4 primes. (Contributed by AV, 27-Jul-2020)

Ref Expression
Assertion nnsum4primesevenALTV ( ∀ 𝑚 ∈ Odd ( 7 < 𝑚 → 𝑚 ∈ GoldbachOdd ) → ( ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑁 ∈ Even ) → ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 4 ) ) 𝑁 = Σ 𝑘 ∈ ( 1 ... 4 ) ( 𝑓 ‘ 𝑘 ) ) )

Proof

Step Hyp Ref Expression
1 simplll ⊢ ( ( ( ( ∀ 𝑚 ∈ Odd ( 7 < 𝑚 → 𝑚 ∈ GoldbachOdd ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑁 ∈ Even ) ) ∧ 𝑜 ∈ GoldbachOdd ) ∧ 𝑁 = ( 𝑜 + 3 ) ) → ∀ 𝑚 ∈ Odd ( 7 < 𝑚 → 𝑚 ∈ GoldbachOdd ) )
2 8nn ⊢ 8 ∈ ℕ
3 2 nnzi ⊢ 8 ∈ ℤ
4 3 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) → 8 ∈ ℤ )
5 3z ⊢ 3 ∈ ℤ
6 5 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) → 3 ∈ ℤ )
7 4 6 zaddcld ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) → ( 8 + 3 ) ∈ ℤ )
8 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) → 𝑁 ∈ ℤ )
9 eluz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ↔ ( 1 2 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 1 2 ≤ 𝑁 ) )
10 8p4e12 ⊢ ( 8 + 4 ) = 1 2
11 10 breq1i ⊢ ( ( 8 + 4 ) ≤ 𝑁 ↔ 1 2 ≤ 𝑁 )
12 1nn0 ⊢ 1 ∈ ℕ0
13 2nn ⊢ 2 ∈ ℕ
14 1lt2 ⊢ 1 < 2
15 12 12 13 14 declt ⊢ 1 1 < 1 2
16 8p3e11 ⊢ ( 8 + 3 ) = 1 1
17 15 16 10 3brtr4i ⊢ ( 8 + 3 ) < ( 8 + 4 )
18 8re ⊢ 8 ∈ ℝ
19 18 a1i ⊢ ( 𝑁 ∈ ℤ → 8 ∈ ℝ )
20 3re ⊢ 3 ∈ ℝ
21 20 a1i ⊢ ( 𝑁 ∈ ℤ → 3 ∈ ℝ )
22 19 21 readdcld ⊢ ( 𝑁 ∈ ℤ → ( 8 + 3 ) ∈ ℝ )
23 4re ⊢ 4 ∈ ℝ
24 23 a1i ⊢ ( 𝑁 ∈ ℤ → 4 ∈ ℝ )
25 19 24 readdcld ⊢ ( 𝑁 ∈ ℤ → ( 8 + 4 ) ∈ ℝ )
26 zre ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
27 ltleletr ⊢ ( ( ( 8 + 3 ) ∈ ℝ ∧ ( 8 + 4 ) ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( ( 8 + 3 ) < ( 8 + 4 ) ∧ ( 8 + 4 ) ≤ 𝑁 ) → ( 8 + 3 ) ≤ 𝑁 ) )
28 22 25 26 27 syl3anc ⊢ ( 𝑁 ∈ ℤ → ( ( ( 8 + 3 ) < ( 8 + 4 ) ∧ ( 8 + 4 ) ≤ 𝑁 ) → ( 8 + 3 ) ≤ 𝑁 ) )
29 17 28 mpani ⊢ ( 𝑁 ∈ ℤ → ( ( 8 + 4 ) ≤ 𝑁 → ( 8 + 3 ) ≤ 𝑁 ) )
30 11 29 biimtrrid ⊢ ( 𝑁 ∈ ℤ → ( 1 2 ≤ 𝑁 → ( 8 + 3 ) ≤ 𝑁 ) )
31 30 imp ⊢ ( ( 𝑁 ∈ ℤ ∧ 1 2 ≤ 𝑁 ) → ( 8 + 3 ) ≤ 𝑁 )
32 31 3adant1 ⊢ ( ( 1 2 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 1 2 ≤ 𝑁 ) → ( 8 + 3 ) ≤ 𝑁 )
33 9 32 sylbi ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) → ( 8 + 3 ) ≤ 𝑁 )
34 eluz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 8 + 3 ) ) ↔ ( ( 8 + 3 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 8 + 3 ) ≤ 𝑁 ) )
35 7 8 33 34 syl3anbrc ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) → 𝑁 ∈ ( ℤ≥ ‘ ( 8 + 3 ) ) )
36 eluzsub ⊢ ( ( 8 ∈ ℤ ∧ 3 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 8 + 3 ) ) ) → ( 𝑁 − 3 ) ∈ ( ℤ≥ ‘ 8 ) )
37 4 6 35 36 syl3anc ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) → ( 𝑁 − 3 ) ∈ ( ℤ≥ ‘ 8 ) )
38 37 adantr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑁 ∈ Even ) → ( 𝑁 − 3 ) ∈ ( ℤ≥ ‘ 8 ) )
39 38 ad3antlr ⊢ ( ( ( ( ∀ 𝑚 ∈ Odd ( 7 < 𝑚 → 𝑚 ∈ GoldbachOdd ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑁 ∈ Even ) ) ∧ 𝑜 ∈ GoldbachOdd ) ∧ 𝑁 = ( 𝑜 + 3 ) ) → ( 𝑁 − 3 ) ∈ ( ℤ≥ ‘ 8 ) )
40 3odd ⊢ 3 ∈ Odd
41 40 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) → 3 ∈ Odd )
42 41 anim1i ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑁 ∈ Even ) → ( 3 ∈ Odd ∧ 𝑁 ∈ Even ) )
43 42 adantl ⊢ ( ( ∀ 𝑚 ∈ Odd ( 7 < 𝑚 → 𝑚 ∈ GoldbachOdd ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑁 ∈ Even ) ) → ( 3 ∈ Odd ∧ 𝑁 ∈ Even ) )
44 43 ancomd ⊢ ( ( ∀ 𝑚 ∈ Odd ( 7 < 𝑚 → 𝑚 ∈ GoldbachOdd ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑁 ∈ Even ) ) → ( 𝑁 ∈ Even ∧ 3 ∈ Odd ) )
45 44 adantr ⊢ ( ( ( ∀ 𝑚 ∈ Odd ( 7 < 𝑚 → 𝑚 ∈ GoldbachOdd ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑁 ∈ Even ) ) ∧ 𝑜 ∈ GoldbachOdd ) → ( 𝑁 ∈ Even ∧ 3 ∈ Odd ) )
46 45 adantr ⊢ ( ( ( ( ∀ 𝑚 ∈ Odd ( 7 < 𝑚 → 𝑚 ∈ GoldbachOdd ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑁 ∈ Even ) ) ∧ 𝑜 ∈ GoldbachOdd ) ∧ 𝑁 = ( 𝑜 + 3 ) ) → ( 𝑁 ∈ Even ∧ 3 ∈ Odd ) )
47 emoo ⊢ ( ( 𝑁 ∈ Even ∧ 3 ∈ Odd ) → ( 𝑁 − 3 ) ∈ Odd )
48 46 47 syl ⊢ ( ( ( ( ∀ 𝑚 ∈ Odd ( 7 < 𝑚 → 𝑚 ∈ GoldbachOdd ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑁 ∈ Even ) ) ∧ 𝑜 ∈ GoldbachOdd ) ∧ 𝑁 = ( 𝑜 + 3 ) ) → ( 𝑁 − 3 ) ∈ Odd )
49 nnsum4primesoddALTV ⊢ ( ∀ 𝑚 ∈ Odd ( 7 < 𝑚 → 𝑚 ∈ GoldbachOdd ) → ( ( ( 𝑁 − 3 ) ∈ ( ℤ≥ ‘ 8 ) ∧ ( 𝑁 − 3 ) ∈ Odd ) → ∃ 𝑔 ∈ ( ℙ ↑m ( 1 ... 3 ) ) ( 𝑁 − 3 ) = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑔 ‘ 𝑘 ) ) )
50 49 imp ⊢ ( ( ∀ 𝑚 ∈ Odd ( 7 < 𝑚 → 𝑚 ∈ GoldbachOdd ) ∧ ( ( 𝑁 − 3 ) ∈ ( ℤ≥ ‘ 8 ) ∧ ( 𝑁 − 3 ) ∈ Odd ) ) → ∃ 𝑔 ∈ ( ℙ ↑m ( 1 ... 3 ) ) ( 𝑁 − 3 ) = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑔 ‘ 𝑘 ) )
51 1 39 48 50 syl12anc ⊢ ( ( ( ( ∀ 𝑚 ∈ Odd ( 7 < 𝑚 → 𝑚 ∈ GoldbachOdd ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑁 ∈ Even ) ) ∧ 𝑜 ∈ GoldbachOdd ) ∧ 𝑁 = ( 𝑜 + 3 ) ) → ∃ 𝑔 ∈ ( ℙ ↑m ( 1 ... 3 ) ) ( 𝑁 − 3 ) = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑔 ‘ 𝑘 ) )
52 simpr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑔 : ( 1 ... 3 ) ⟶ ℙ ) → 𝑔 : ( 1 ... 3 ) ⟶ ℙ )
53 4z ⊢ 4 ∈ ℤ
54 fzonel ⊢ ¬ 4 ∈ ( 1 ..^ 4 )
55 fzoval ⊢ ( 4 ∈ ℤ → ( 1 ..^ 4 ) = ( 1 ... ( 4 − 1 ) ) )
56 53 55 ax-mp ⊢ ( 1 ..^ 4 ) = ( 1 ... ( 4 − 1 ) )
57 4cn ⊢ 4 ∈ ℂ
58 ax-1cn ⊢ 1 ∈ ℂ
59 3cn ⊢ 3 ∈ ℂ
60 3p1e4 ⊢ ( 3 + 1 ) = 4
61 subadd2 ⊢ ( ( 4 ∈ ℂ ∧ 1 ∈ ℂ ∧ 3 ∈ ℂ ) → ( ( 4 − 1 ) = 3 ↔ ( 3 + 1 ) = 4 ) )
62 60 61 mpbiri ⊢ ( ( 4 ∈ ℂ ∧ 1 ∈ ℂ ∧ 3 ∈ ℂ ) → ( 4 − 1 ) = 3 )
63 57 58 59 62 mp3an ⊢ ( 4 − 1 ) = 3
64 63 oveq2i ⊢ ( 1 ... ( 4 − 1 ) ) = ( 1 ... 3 )
65 56 64 eqtri ⊢ ( 1 ..^ 4 ) = ( 1 ... 3 )
66 65 eqcomi ⊢ ( 1 ... 3 ) = ( 1 ..^ 4 )
67 66 eleq2i ⊢ ( 4 ∈ ( 1 ... 3 ) ↔ 4 ∈ ( 1 ..^ 4 ) )
68 54 67 mtbir ⊢ ¬ 4 ∈ ( 1 ... 3 )
69 53 68 pm3.2i ⊢ ( 4 ∈ ℤ ∧ ¬ 4 ∈ ( 1 ... 3 ) )
70 69 a1i ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑔 : ( 1 ... 3 ) ⟶ ℙ ) → ( 4 ∈ ℤ ∧ ¬ 4 ∈ ( 1 ... 3 ) ) )
71 3prm ⊢ 3 ∈ ℙ
72 71 a1i ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑔 : ( 1 ... 3 ) ⟶ ℙ ) → 3 ∈ ℙ )
73 fsnunf ⊢ ( ( 𝑔 : ( 1 ... 3 ) ⟶ ℙ ∧ ( 4 ∈ ℤ ∧ ¬ 4 ∈ ( 1 ... 3 ) ) ∧ 3 ∈ ℙ ) → ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) : ( ( 1 ... 3 ) ∪ { 4 } ) ⟶ ℙ )
74 52 70 72 73 syl3anc ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑔 : ( 1 ... 3 ) ⟶ ℙ ) → ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) : ( ( 1 ... 3 ) ∪ { 4 } ) ⟶ ℙ )
75 fzval3 ⊢ ( 4 ∈ ℤ → ( 1 ... 4 ) = ( 1 ..^ ( 4 + 1 ) ) )
76 53 75 ax-mp ⊢ ( 1 ... 4 ) = ( 1 ..^ ( 4 + 1 ) )
77 1z ⊢ 1 ∈ ℤ
78 1re ⊢ 1 ∈ ℝ
79 1lt4 ⊢ 1 < 4
80 78 23 79 ltleii ⊢ 1 ≤ 4
81 eluz2 ⊢ ( 4 ∈ ( ℤ≥ ‘ 1 ) ↔ ( 1 ∈ ℤ ∧ 4 ∈ ℤ ∧ 1 ≤ 4 ) )
82 77 53 80 81 mpbir3an ⊢ 4 ∈ ( ℤ≥ ‘ 1 )
83 fzosplitsn ⊢ ( 4 ∈ ( ℤ≥ ‘ 1 ) → ( 1 ..^ ( 4 + 1 ) ) = ( ( 1 ..^ 4 ) ∪ { 4 } ) )
84 82 83 ax-mp ⊢ ( 1 ..^ ( 4 + 1 ) ) = ( ( 1 ..^ 4 ) ∪ { 4 } )
85 65 uneq1i ⊢ ( ( 1 ..^ 4 ) ∪ { 4 } ) = ( ( 1 ... 3 ) ∪ { 4 } )
86 76 84 85 3eqtri ⊢ ( 1 ... 4 ) = ( ( 1 ... 3 ) ∪ { 4 } )
87 86 feq2i ⊢ ( ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) : ( 1 ... 4 ) ⟶ ℙ ↔ ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) : ( ( 1 ... 3 ) ∪ { 4 } ) ⟶ ℙ )
88 74 87 sylibr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑔 : ( 1 ... 3 ) ⟶ ℙ ) → ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) : ( 1 ... 4 ) ⟶ ℙ )
89 prmex ⊢ ℙ ∈ V
90 ovex ⊢ ( 1 ... 4 ) ∈ V
91 89 90 pm3.2i ⊢ ( ℙ ∈ V ∧ ( 1 ... 4 ) ∈ V )
92 elmapg ⊢ ( ( ℙ ∈ V ∧ ( 1 ... 4 ) ∈ V ) → ( ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) ∈ ( ℙ ↑m ( 1 ... 4 ) ) ↔ ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) : ( 1 ... 4 ) ⟶ ℙ ) )
93 91 92 mp1i ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑔 : ( 1 ... 3 ) ⟶ ℙ ) → ( ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) ∈ ( ℙ ↑m ( 1 ... 4 ) ) ↔ ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) : ( 1 ... 4 ) ⟶ ℙ ) )
94 88 93 mpbird ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑔 : ( 1 ... 3 ) ⟶ ℙ ) → ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) ∈ ( ℙ ↑m ( 1 ... 4 ) ) )
95 94 adantr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑔 : ( 1 ... 3 ) ⟶ ℙ ) ∧ ( 𝑁 − 3 ) = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑔 ‘ 𝑘 ) ) → ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) ∈ ( ℙ ↑m ( 1 ... 4 ) ) )
96 fveq1 ⊢ ( 𝑓 = ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) → ( 𝑓 ‘ 𝑘 ) = ( ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) ‘ 𝑘 ) )
97 96 sumeq2sdv ⊢ ( 𝑓 = ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) → Σ 𝑘 ∈ ( 1 ... 4 ) ( 𝑓 ‘ 𝑘 ) = Σ 𝑘 ∈ ( 1 ... 4 ) ( ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) ‘ 𝑘 ) )
98 97 eqeq2d ⊢ ( 𝑓 = ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) → ( 𝑁 = Σ 𝑘 ∈ ( 1 ... 4 ) ( 𝑓 ‘ 𝑘 ) ↔ 𝑁 = Σ 𝑘 ∈ ( 1 ... 4 ) ( ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) ‘ 𝑘 ) ) )
99 98 adantl ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑔 : ( 1 ... 3 ) ⟶ ℙ ) ∧ ( 𝑁 − 3 ) = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑔 ‘ 𝑘 ) ) ∧ 𝑓 = ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) ) → ( 𝑁 = Σ 𝑘 ∈ ( 1 ... 4 ) ( 𝑓 ‘ 𝑘 ) ↔ 𝑁 = Σ 𝑘 ∈ ( 1 ... 4 ) ( ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) ‘ 𝑘 ) ) )
100 82 a1i ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑔 : ( 1 ... 3 ) ⟶ ℙ ) → 4 ∈ ( ℤ≥ ‘ 1 ) )
101 86 eleq2i ⊢ ( 𝑘 ∈ ( 1 ... 4 ) ↔ 𝑘 ∈ ( ( 1 ... 3 ) ∪ { 4 } ) )
102 elun ⊢ ( 𝑘 ∈ ( ( 1 ... 3 ) ∪ { 4 } ) ↔ ( 𝑘 ∈ ( 1 ... 3 ) ∨ 𝑘 ∈ { 4 } ) )
103 velsn ⊢ ( 𝑘 ∈ { 4 } ↔ 𝑘 = 4 )
104 103 orbi2i ⊢ ( ( 𝑘 ∈ ( 1 ... 3 ) ∨ 𝑘 ∈ { 4 } ) ↔ ( 𝑘 ∈ ( 1 ... 3 ) ∨ 𝑘 = 4 ) )
105 101 102 104 3bitri ⊢ ( 𝑘 ∈ ( 1 ... 4 ) ↔ ( 𝑘 ∈ ( 1 ... 3 ) ∨ 𝑘 = 4 ) )
106 elfz2 ⊢ ( 𝑘 ∈ ( 1 ... 3 ) ↔ ( ( 1 ∈ ℤ ∧ 3 ∈ ℤ ∧ 𝑘 ∈ ℤ ) ∧ ( 1 ≤ 𝑘 ∧ 𝑘 ≤ 3 ) ) )
107 20 23 pm3.2i ⊢ ( 3 ∈ ℝ ∧ 4 ∈ ℝ )
108 3lt4 ⊢ 3 < 4
109 ltnle ⊢ ( ( 3 ∈ ℝ ∧ 4 ∈ ℝ ) → ( 3 < 4 ↔ ¬ 4 ≤ 3 ) )
110 108 109 mpbii ⊢ ( ( 3 ∈ ℝ ∧ 4 ∈ ℝ ) → ¬ 4 ≤ 3 )
111 107 110 ax-mp ⊢ ¬ 4 ≤ 3
112 breq1 ⊢ ( 𝑘 = 4 → ( 𝑘 ≤ 3 ↔ 4 ≤ 3 ) )
113 112 eqcoms ⊢ ( 4 = 𝑘 → ( 𝑘 ≤ 3 ↔ 4 ≤ 3 ) )
114 111 113 mtbiri ⊢ ( 4 = 𝑘 → ¬ 𝑘 ≤ 3 )
115 114 a1i ⊢ ( 𝑘 ∈ ℤ → ( 4 = 𝑘 → ¬ 𝑘 ≤ 3 ) )
116 115 necon2ad ⊢ ( 𝑘 ∈ ℤ → ( 𝑘 ≤ 3 → 4 ≠ 𝑘 ) )
117 116 adantld ⊢ ( 𝑘 ∈ ℤ → ( ( 1 ≤ 𝑘 ∧ 𝑘 ≤ 3 ) → 4 ≠ 𝑘 ) )
118 117 3ad2ant3 ⊢ ( ( 1 ∈ ℤ ∧ 3 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( ( 1 ≤ 𝑘 ∧ 𝑘 ≤ 3 ) → 4 ≠ 𝑘 ) )
119 118 imp ⊢ ( ( ( 1 ∈ ℤ ∧ 3 ∈ ℤ ∧ 𝑘 ∈ ℤ ) ∧ ( 1 ≤ 𝑘 ∧ 𝑘 ≤ 3 ) ) → 4 ≠ 𝑘 )
120 106 119 sylbi ⊢ ( 𝑘 ∈ ( 1 ... 3 ) → 4 ≠ 𝑘 )
121 120 adantr ⊢ ( ( 𝑘 ∈ ( 1 ... 3 ) ∧ 𝑔 : ( 1 ... 3 ) ⟶ ℙ ) → 4 ≠ 𝑘 )
122 fvunsn ⊢ ( 4 ≠ 𝑘 → ( ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) ‘ 𝑘 ) = ( 𝑔 ‘ 𝑘 ) )
123 121 122 syl ⊢ ( ( 𝑘 ∈ ( 1 ... 3 ) ∧ 𝑔 : ( 1 ... 3 ) ⟶ ℙ ) → ( ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) ‘ 𝑘 ) = ( 𝑔 ‘ 𝑘 ) )
124 ffvelcdm ⊢ ( ( 𝑔 : ( 1 ... 3 ) ⟶ ℙ ∧ 𝑘 ∈ ( 1 ... 3 ) ) → ( 𝑔 ‘ 𝑘 ) ∈ ℙ )
125 124 ancoms ⊢ ( ( 𝑘 ∈ ( 1 ... 3 ) ∧ 𝑔 : ( 1 ... 3 ) ⟶ ℙ ) → ( 𝑔 ‘ 𝑘 ) ∈ ℙ )
126 prmz ⊢ ( ( 𝑔 ‘ 𝑘 ) ∈ ℙ → ( 𝑔 ‘ 𝑘 ) ∈ ℤ )
127 125 126 syl ⊢ ( ( 𝑘 ∈ ( 1 ... 3 ) ∧ 𝑔 : ( 1 ... 3 ) ⟶ ℙ ) → ( 𝑔 ‘ 𝑘 ) ∈ ℤ )
128 127 zcnd ⊢ ( ( 𝑘 ∈ ( 1 ... 3 ) ∧ 𝑔 : ( 1 ... 3 ) ⟶ ℙ ) → ( 𝑔 ‘ 𝑘 ) ∈ ℂ )
129 123 128 eqeltrd ⊢ ( ( 𝑘 ∈ ( 1 ... 3 ) ∧ 𝑔 : ( 1 ... 3 ) ⟶ ℙ ) → ( ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) ‘ 𝑘 ) ∈ ℂ )
130 129 ex ⊢ ( 𝑘 ∈ ( 1 ... 3 ) → ( 𝑔 : ( 1 ... 3 ) ⟶ ℙ → ( ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) ‘ 𝑘 ) ∈ ℂ ) )
131 130 adantld ⊢ ( 𝑘 ∈ ( 1 ... 3 ) → ( ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑔 : ( 1 ... 3 ) ⟶ ℙ ) → ( ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) ‘ 𝑘 ) ∈ ℂ ) )
132 fveq2 ⊢ ( 𝑘 = 4 → ( ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) ‘ 𝑘 ) = ( ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) ‘ 4 ) )
133 53 a1i ⊢ ( 𝑔 : ( 1 ... 3 ) ⟶ ℙ → 4 ∈ ℤ )
134 5 a1i ⊢ ( 𝑔 : ( 1 ... 3 ) ⟶ ℙ → 3 ∈ ℤ )
135 fdm ⊢ ( 𝑔 : ( 1 ... 3 ) ⟶ ℙ → dom 𝑔 = ( 1 ... 3 ) )
136 eleq2 ⊢ ( dom 𝑔 = ( 1 ... 3 ) → ( 4 ∈ dom 𝑔 ↔ 4 ∈ ( 1 ... 3 ) ) )
137 68 136 mtbiri ⊢ ( dom 𝑔 = ( 1 ... 3 ) → ¬ 4 ∈ dom 𝑔 )
138 135 137 syl ⊢ ( 𝑔 : ( 1 ... 3 ) ⟶ ℙ → ¬ 4 ∈ dom 𝑔 )
139 fsnunfv ⊢ ( ( 4 ∈ ℤ ∧ 3 ∈ ℤ ∧ ¬ 4 ∈ dom 𝑔 ) → ( ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) ‘ 4 ) = 3 )
140 133 134 138 139 syl3anc ⊢ ( 𝑔 : ( 1 ... 3 ) ⟶ ℙ → ( ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) ‘ 4 ) = 3 )
141 140 adantl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑔 : ( 1 ... 3 ) ⟶ ℙ ) → ( ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) ‘ 4 ) = 3 )
142 132 141 sylan9eq ⊢ ( ( 𝑘 = 4 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑔 : ( 1 ... 3 ) ⟶ ℙ ) ) → ( ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) ‘ 𝑘 ) = 3 )
143 142 59 eqeltrdi ⊢ ( ( 𝑘 = 4 ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑔 : ( 1 ... 3 ) ⟶ ℙ ) ) → ( ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) ‘ 𝑘 ) ∈ ℂ )
144 143 ex ⊢ ( 𝑘 = 4 → ( ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑔 : ( 1 ... 3 ) ⟶ ℙ ) → ( ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) ‘ 𝑘 ) ∈ ℂ ) )
145 131 144 jaoi ⊢ ( ( 𝑘 ∈ ( 1 ... 3 ) ∨ 𝑘 = 4 ) → ( ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑔 : ( 1 ... 3 ) ⟶ ℙ ) → ( ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) ‘ 𝑘 ) ∈ ℂ ) )
146 145 com12 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑔 : ( 1 ... 3 ) ⟶ ℙ ) → ( ( 𝑘 ∈ ( 1 ... 3 ) ∨ 𝑘 = 4 ) → ( ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) ‘ 𝑘 ) ∈ ℂ ) )
147 105 146 biimtrid ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑔 : ( 1 ... 3 ) ⟶ ℙ ) → ( 𝑘 ∈ ( 1 ... 4 ) → ( ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) ‘ 𝑘 ) ∈ ℂ ) )
148 147 imp ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑔 : ( 1 ... 3 ) ⟶ ℙ ) ∧ 𝑘 ∈ ( 1 ... 4 ) ) → ( ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) ‘ 𝑘 ) ∈ ℂ )
149 100 148 132 fsumm1 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑔 : ( 1 ... 3 ) ⟶ ℙ ) → Σ 𝑘 ∈ ( 1 ... 4 ) ( ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) ‘ 𝑘 ) = ( Σ 𝑘 ∈ ( 1 ... ( 4 − 1 ) ) ( ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) ‘ 𝑘 ) + ( ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) ‘ 4 ) ) )
150 149 adantr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑔 : ( 1 ... 3 ) ⟶ ℙ ) ∧ ( 𝑁 − 3 ) = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑔 ‘ 𝑘 ) ) → Σ 𝑘 ∈ ( 1 ... 4 ) ( ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) ‘ 𝑘 ) = ( Σ 𝑘 ∈ ( 1 ... ( 4 − 1 ) ) ( ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) ‘ 𝑘 ) + ( ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) ‘ 4 ) ) )
151 63 eqcomi ⊢ 3 = ( 4 − 1 )
152 151 oveq2i ⊢ ( 1 ... 3 ) = ( 1 ... ( 4 − 1 ) )
153 152 a1i ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑔 : ( 1 ... 3 ) ⟶ ℙ ) → ( 1 ... 3 ) = ( 1 ... ( 4 − 1 ) ) )
154 120 adantl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑔 : ( 1 ... 3 ) ⟶ ℙ ) ∧ 𝑘 ∈ ( 1 ... 3 ) ) → 4 ≠ 𝑘 )
155 154 122 syl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑔 : ( 1 ... 3 ) ⟶ ℙ ) ∧ 𝑘 ∈ ( 1 ... 3 ) ) → ( ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) ‘ 𝑘 ) = ( 𝑔 ‘ 𝑘 ) )
156 155 eqcomd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑔 : ( 1 ... 3 ) ⟶ ℙ ) ∧ 𝑘 ∈ ( 1 ... 3 ) ) → ( 𝑔 ‘ 𝑘 ) = ( ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) ‘ 𝑘 ) )
157 153 156 sumeq12dv ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑔 : ( 1 ... 3 ) ⟶ ℙ ) → Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑔 ‘ 𝑘 ) = Σ 𝑘 ∈ ( 1 ... ( 4 − 1 ) ) ( ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) ‘ 𝑘 ) )
158 157 eqeq2d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑔 : ( 1 ... 3 ) ⟶ ℙ ) → ( ( 𝑁 − 3 ) = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑔 ‘ 𝑘 ) ↔ ( 𝑁 − 3 ) = Σ 𝑘 ∈ ( 1 ... ( 4 − 1 ) ) ( ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) ‘ 𝑘 ) ) )
159 158 biimpa ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑔 : ( 1 ... 3 ) ⟶ ℙ ) ∧ ( 𝑁 − 3 ) = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑔 ‘ 𝑘 ) ) → ( 𝑁 − 3 ) = Σ 𝑘 ∈ ( 1 ... ( 4 − 1 ) ) ( ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) ‘ 𝑘 ) )
160 159 eqcomd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑔 : ( 1 ... 3 ) ⟶ ℙ ) ∧ ( 𝑁 − 3 ) = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑔 ‘ 𝑘 ) ) → Σ 𝑘 ∈ ( 1 ... ( 4 − 1 ) ) ( ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) ‘ 𝑘 ) = ( 𝑁 − 3 ) )
161 160 oveq1d ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑔 : ( 1 ... 3 ) ⟶ ℙ ) ∧ ( 𝑁 − 3 ) = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑔 ‘ 𝑘 ) ) → ( Σ 𝑘 ∈ ( 1 ... ( 4 − 1 ) ) ( ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) ‘ 𝑘 ) + ( ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) ‘ 4 ) ) = ( ( 𝑁 − 3 ) + ( ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) ‘ 4 ) ) )
162 53 a1i ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑔 : ( 1 ... 3 ) ⟶ ℙ ) → 4 ∈ ℤ )
163 5 a1i ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑔 : ( 1 ... 3 ) ⟶ ℙ ) → 3 ∈ ℤ )
164 138 adantl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑔 : ( 1 ... 3 ) ⟶ ℙ ) → ¬ 4 ∈ dom 𝑔 )
165 162 163 164 139 syl3anc ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑔 : ( 1 ... 3 ) ⟶ ℙ ) → ( ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) ‘ 4 ) = 3 )
166 165 oveq2d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑔 : ( 1 ... 3 ) ⟶ ℙ ) → ( ( 𝑁 − 3 ) + ( ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) ‘ 4 ) ) = ( ( 𝑁 − 3 ) + 3 ) )
167 eluzelcn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) → 𝑁 ∈ ℂ )
168 59 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) → 3 ∈ ℂ )
169 167 168 npcand ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) → ( ( 𝑁 − 3 ) + 3 ) = 𝑁 )
170 169 adantr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑔 : ( 1 ... 3 ) ⟶ ℙ ) → ( ( 𝑁 − 3 ) + 3 ) = 𝑁 )
171 166 170 eqtrd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑔 : ( 1 ... 3 ) ⟶ ℙ ) → ( ( 𝑁 − 3 ) + ( ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) ‘ 4 ) ) = 𝑁 )
172 171 adantr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑔 : ( 1 ... 3 ) ⟶ ℙ ) ∧ ( 𝑁 − 3 ) = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑔 ‘ 𝑘 ) ) → ( ( 𝑁 − 3 ) + ( ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) ‘ 4 ) ) = 𝑁 )
173 150 161 172 3eqtrrd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑔 : ( 1 ... 3 ) ⟶ ℙ ) ∧ ( 𝑁 − 3 ) = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑔 ‘ 𝑘 ) ) → 𝑁 = Σ 𝑘 ∈ ( 1 ... 4 ) ( ( 𝑔 ∪ { ⟨ 4 , 3 ⟩ } ) ‘ 𝑘 ) )
174 95 99 173 rspcedvd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑔 : ( 1 ... 3 ) ⟶ ℙ ) ∧ ( 𝑁 − 3 ) = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑔 ‘ 𝑘 ) ) → ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 4 ) ) 𝑁 = Σ 𝑘 ∈ ( 1 ... 4 ) ( 𝑓 ‘ 𝑘 ) )
175 174 ex ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑔 : ( 1 ... 3 ) ⟶ ℙ ) → ( ( 𝑁 − 3 ) = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑔 ‘ 𝑘 ) → ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 4 ) ) 𝑁 = Σ 𝑘 ∈ ( 1 ... 4 ) ( 𝑓 ‘ 𝑘 ) ) )
176 175 expcom ⊢ ( 𝑔 : ( 1 ... 3 ) ⟶ ℙ → ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) → ( ( 𝑁 − 3 ) = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑔 ‘ 𝑘 ) → ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 4 ) ) 𝑁 = Σ 𝑘 ∈ ( 1 ... 4 ) ( 𝑓 ‘ 𝑘 ) ) ) )
177 elmapi ⊢ ( 𝑔 ∈ ( ℙ ↑m ( 1 ... 3 ) ) → 𝑔 : ( 1 ... 3 ) ⟶ ℙ )
178 176 177 syl11 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) → ( 𝑔 ∈ ( ℙ ↑m ( 1 ... 3 ) ) → ( ( 𝑁 − 3 ) = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑔 ‘ 𝑘 ) → ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 4 ) ) 𝑁 = Σ 𝑘 ∈ ( 1 ... 4 ) ( 𝑓 ‘ 𝑘 ) ) ) )
179 178 rexlimdv ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) → ( ∃ 𝑔 ∈ ( ℙ ↑m ( 1 ... 3 ) ) ( 𝑁 − 3 ) = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑔 ‘ 𝑘 ) → ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 4 ) ) 𝑁 = Σ 𝑘 ∈ ( 1 ... 4 ) ( 𝑓 ‘ 𝑘 ) ) )
180 179 adantr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑁 ∈ Even ) → ( ∃ 𝑔 ∈ ( ℙ ↑m ( 1 ... 3 ) ) ( 𝑁 − 3 ) = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑔 ‘ 𝑘 ) → ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 4 ) ) 𝑁 = Σ 𝑘 ∈ ( 1 ... 4 ) ( 𝑓 ‘ 𝑘 ) ) )
181 180 ad3antlr ⊢ ( ( ( ( ∀ 𝑚 ∈ Odd ( 7 < 𝑚 → 𝑚 ∈ GoldbachOdd ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑁 ∈ Even ) ) ∧ 𝑜 ∈ GoldbachOdd ) ∧ 𝑁 = ( 𝑜 + 3 ) ) → ( ∃ 𝑔 ∈ ( ℙ ↑m ( 1 ... 3 ) ) ( 𝑁 − 3 ) = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑔 ‘ 𝑘 ) → ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 4 ) ) 𝑁 = Σ 𝑘 ∈ ( 1 ... 4 ) ( 𝑓 ‘ 𝑘 ) ) )
182 51 181 mpd ⊢ ( ( ( ( ∀ 𝑚 ∈ Odd ( 7 < 𝑚 → 𝑚 ∈ GoldbachOdd ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑁 ∈ Even ) ) ∧ 𝑜 ∈ GoldbachOdd ) ∧ 𝑁 = ( 𝑜 + 3 ) ) → ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 4 ) ) 𝑁 = Σ 𝑘 ∈ ( 1 ... 4 ) ( 𝑓 ‘ 𝑘 ) )
183 evengpoap3 ⊢ ( ∀ 𝑚 ∈ Odd ( 7 < 𝑚 → 𝑚 ∈ GoldbachOdd ) → ( ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑁 ∈ Even ) → ∃ 𝑜 ∈ GoldbachOdd 𝑁 = ( 𝑜 + 3 ) ) )
184 183 imp ⊢ ( ( ∀ 𝑚 ∈ Odd ( 7 < 𝑚 → 𝑚 ∈ GoldbachOdd ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑁 ∈ Even ) ) → ∃ 𝑜 ∈ GoldbachOdd 𝑁 = ( 𝑜 + 3 ) )
185 182 184 r19.29a ⊢ ( ( ∀ 𝑚 ∈ Odd ( 7 < 𝑚 → 𝑚 ∈ GoldbachOdd ) ∧ ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑁 ∈ Even ) ) → ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 4 ) ) 𝑁 = Σ 𝑘 ∈ ( 1 ... 4 ) ( 𝑓 ‘ 𝑘 ) )
186 185 ex ⊢ ( ∀ 𝑚 ∈ Odd ( 7 < 𝑚 → 𝑚 ∈ GoldbachOdd ) → ( ( 𝑁 ∈ ( ℤ≥ ‘ 1 2 ) ∧ 𝑁 ∈ Even ) → ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 4 ) ) 𝑁 = Σ 𝑘 ∈ ( 1 ... 4 ) ( 𝑓 ‘ 𝑘 ) ) )