Metamath Proof Explorer

Theorem nnsum4primeseven

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

Ref Expression
Assertion nnsum4primeseven ( ∀ 𝑚 ∈ Odd ( 5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) → ( ( 𝑁 ∈ ( ℤ≥ ‘ 9 ) ∧ 𝑁 ∈ Even ) → ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 4 ) ) 𝑁 = Σ 𝑘 ∈ ( 1 ... 4 ) ( 𝑓 ‘ 𝑘 ) ) )

Proof

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