Metamath Proof Explorer


Theorem nnsum4primesoddALTV

Description: If the (strong) ternary Goldbach conjecture is valid, then every odd integer greater than 7 is the sum of 3 primes. (Contributed by AV, 26-Jul-2020)

Ref Expression
Assertion nnsum4primesoddALTV ( ∀ 𝑚 ∈ Odd ( 7 < 𝑚𝑚 ∈ GoldbachOdd ) → ( ( 𝑁 ∈ ( ℤ ‘ 8 ) ∧ 𝑁 ∈ Odd ) → ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 3 ) ) 𝑁 = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑓𝑘 ) ) )

Proof

Step Hyp Ref Expression
1 breq2 ( 𝑚 = 𝑁 → ( 7 < 𝑚 ↔ 7 < 𝑁 ) )
2 eleq1 ( 𝑚 = 𝑁 → ( 𝑚 ∈ GoldbachOdd ↔ 𝑁 ∈ GoldbachOdd ) )
3 1 2 imbi12d ( 𝑚 = 𝑁 → ( ( 7 < 𝑚𝑚 ∈ GoldbachOdd ) ↔ ( 7 < 𝑁𝑁 ∈ GoldbachOdd ) ) )
4 3 rspcv ( 𝑁 ∈ Odd → ( ∀ 𝑚 ∈ Odd ( 7 < 𝑚𝑚 ∈ GoldbachOdd ) → ( 7 < 𝑁𝑁 ∈ GoldbachOdd ) ) )
5 4 adantl ( ( 𝑁 ∈ ( ℤ ‘ 8 ) ∧ 𝑁 ∈ Odd ) → ( ∀ 𝑚 ∈ Odd ( 7 < 𝑚𝑚 ∈ GoldbachOdd ) → ( 7 < 𝑁𝑁 ∈ GoldbachOdd ) ) )
6 eluz2 ( 𝑁 ∈ ( ℤ ‘ 8 ) ↔ ( 8 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 8 ≤ 𝑁 ) )
7 7lt8 7 < 8
8 7re 7 ∈ ℝ
9 8 a1i ( 𝑁 ∈ ℤ → 7 ∈ ℝ )
10 8re 8 ∈ ℝ
11 10 a1i ( 𝑁 ∈ ℤ → 8 ∈ ℝ )
12 zre ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
13 ltletr ( ( 7 ∈ ℝ ∧ 8 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 7 < 8 ∧ 8 ≤ 𝑁 ) → 7 < 𝑁 ) )
14 9 11 12 13 syl3anc ( 𝑁 ∈ ℤ → ( ( 7 < 8 ∧ 8 ≤ 𝑁 ) → 7 < 𝑁 ) )
15 7 14 mpani ( 𝑁 ∈ ℤ → ( 8 ≤ 𝑁 → 7 < 𝑁 ) )
16 15 imp ( ( 𝑁 ∈ ℤ ∧ 8 ≤ 𝑁 ) → 7 < 𝑁 )
17 16 3adant1 ( ( 8 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 8 ≤ 𝑁 ) → 7 < 𝑁 )
18 6 17 sylbi ( 𝑁 ∈ ( ℤ ‘ 8 ) → 7 < 𝑁 )
19 18 adantr ( ( 𝑁 ∈ ( ℤ ‘ 8 ) ∧ 𝑁 ∈ Odd ) → 7 < 𝑁 )
20 pm2.27 ( 7 < 𝑁 → ( ( 7 < 𝑁𝑁 ∈ GoldbachOdd ) → 𝑁 ∈ GoldbachOdd ) )
21 19 20 syl ( ( 𝑁 ∈ ( ℤ ‘ 8 ) ∧ 𝑁 ∈ Odd ) → ( ( 7 < 𝑁𝑁 ∈ GoldbachOdd ) → 𝑁 ∈ GoldbachOdd ) )
22 isgbo ( 𝑁 ∈ GoldbachOdd ↔ ( 𝑁 ∈ Odd ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑁 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) )
23 1ex 1 ∈ V
24 2ex 2 ∈ V
25 3ex 3 ∈ V
26 vex 𝑝 ∈ V
27 vex 𝑞 ∈ V
28 vex 𝑟 ∈ V
29 1ne2 1 ≠ 2
30 1re 1 ∈ ℝ
31 1lt3 1 < 3
32 30 31 ltneii 1 ≠ 3
33 2re 2 ∈ ℝ
34 2lt3 2 < 3
35 33 34 ltneii 2 ≠ 3
36 23 24 25 26 27 28 29 32 35 ftp { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ , ⟨ 3 , 𝑟 ⟩ } : { 1 , 2 , 3 } ⟶ { 𝑝 , 𝑞 , 𝑟 }
37 36 a1i ( ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ∧ 𝑟 ∈ ℙ ) → { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ , ⟨ 3 , 𝑟 ⟩ } : { 1 , 2 , 3 } ⟶ { 𝑝 , 𝑞 , 𝑟 } )
38 1p2e3 ( 1 + 2 ) = 3
39 38 eqcomi 3 = ( 1 + 2 )
40 39 oveq2i ( 1 ... 3 ) = ( 1 ... ( 1 + 2 ) )
41 1z 1 ∈ ℤ
42 fztp ( 1 ∈ ℤ → ( 1 ... ( 1 + 2 ) ) = { 1 , ( 1 + 1 ) , ( 1 + 2 ) } )
43 41 42 ax-mp ( 1 ... ( 1 + 2 ) ) = { 1 , ( 1 + 1 ) , ( 1 + 2 ) }
44 eqid 1 = 1
45 id ( 1 = 1 → 1 = 1 )
46 1p1e2 ( 1 + 1 ) = 2
47 46 a1i ( 1 = 1 → ( 1 + 1 ) = 2 )
48 38 a1i ( 1 = 1 → ( 1 + 2 ) = 3 )
49 45 47 48 tpeq123d ( 1 = 1 → { 1 , ( 1 + 1 ) , ( 1 + 2 ) } = { 1 , 2 , 3 } )
50 44 49 ax-mp { 1 , ( 1 + 1 ) , ( 1 + 2 ) } = { 1 , 2 , 3 }
51 40 43 50 3eqtri ( 1 ... 3 ) = { 1 , 2 , 3 }
52 51 feq2i ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ , ⟨ 3 , 𝑟 ⟩ } : ( 1 ... 3 ) ⟶ { 𝑝 , 𝑞 , 𝑟 } ↔ { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ , ⟨ 3 , 𝑟 ⟩ } : { 1 , 2 , 3 } ⟶ { 𝑝 , 𝑞 , 𝑟 } )
53 37 52 sylibr ( ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ∧ 𝑟 ∈ ℙ ) → { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ , ⟨ 3 , 𝑟 ⟩ } : ( 1 ... 3 ) ⟶ { 𝑝 , 𝑞 , 𝑟 } )
54 df-3an ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ∧ 𝑟 ∈ ℙ ) ↔ ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ∧ 𝑟 ∈ ℙ ) )
55 26 27 28 tpss ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ∧ 𝑟 ∈ ℙ ) ↔ { 𝑝 , 𝑞 , 𝑟 } ⊆ ℙ )
56 54 55 sylbb1 ( ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ∧ 𝑟 ∈ ℙ ) → { 𝑝 , 𝑞 , 𝑟 } ⊆ ℙ )
57 53 56 fssd ( ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ∧ 𝑟 ∈ ℙ ) → { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ , ⟨ 3 , 𝑟 ⟩ } : ( 1 ... 3 ) ⟶ ℙ )
58 prmex ℙ ∈ V
59 ovex ( 1 ... 3 ) ∈ V
60 58 59 pm3.2i ( ℙ ∈ V ∧ ( 1 ... 3 ) ∈ V )
61 elmapg ( ( ℙ ∈ V ∧ ( 1 ... 3 ) ∈ V ) → ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ , ⟨ 3 , 𝑟 ⟩ } ∈ ( ℙ ↑m ( 1 ... 3 ) ) ↔ { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ , ⟨ 3 , 𝑟 ⟩ } : ( 1 ... 3 ) ⟶ ℙ ) )
62 60 61 mp1i ( ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ∧ 𝑟 ∈ ℙ ) → ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ , ⟨ 3 , 𝑟 ⟩ } ∈ ( ℙ ↑m ( 1 ... 3 ) ) ↔ { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ , ⟨ 3 , 𝑟 ⟩ } : ( 1 ... 3 ) ⟶ ℙ ) )
63 57 62 mpbird ( ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ∧ 𝑟 ∈ ℙ ) → { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ , ⟨ 3 , 𝑟 ⟩ } ∈ ( ℙ ↑m ( 1 ... 3 ) ) )
64 fveq1 ( 𝑓 = { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ , ⟨ 3 , 𝑟 ⟩ } → ( 𝑓𝑘 ) = ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ , ⟨ 3 , 𝑟 ⟩ } ‘ 𝑘 ) )
65 64 sumeq2sdv ( 𝑓 = { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ , ⟨ 3 , 𝑟 ⟩ } → Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑓𝑘 ) = Σ 𝑘 ∈ ( 1 ... 3 ) ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ , ⟨ 3 , 𝑟 ⟩ } ‘ 𝑘 ) )
66 65 eqeq2d ( 𝑓 = { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ , ⟨ 3 , 𝑟 ⟩ } → ( ( ( 𝑝 + 𝑞 ) + 𝑟 ) = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑓𝑘 ) ↔ ( ( 𝑝 + 𝑞 ) + 𝑟 ) = Σ 𝑘 ∈ ( 1 ... 3 ) ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ , ⟨ 3 , 𝑟 ⟩ } ‘ 𝑘 ) ) )
67 66 adantl ( ( ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ∧ 𝑟 ∈ ℙ ) ∧ 𝑓 = { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ , ⟨ 3 , 𝑟 ⟩ } ) → ( ( ( 𝑝 + 𝑞 ) + 𝑟 ) = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑓𝑘 ) ↔ ( ( 𝑝 + 𝑞 ) + 𝑟 ) = Σ 𝑘 ∈ ( 1 ... 3 ) ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ , ⟨ 3 , 𝑟 ⟩ } ‘ 𝑘 ) ) )
68 51 a1i ( ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ∧ 𝑟 ∈ ℙ ) → ( 1 ... 3 ) = { 1 , 2 , 3 } )
69 68 sumeq1d ( ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ∧ 𝑟 ∈ ℙ ) → Σ 𝑘 ∈ ( 1 ... 3 ) ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ , ⟨ 3 , 𝑟 ⟩ } ‘ 𝑘 ) = Σ 𝑘 ∈ { 1 , 2 , 3 } ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ , ⟨ 3 , 𝑟 ⟩ } ‘ 𝑘 ) )
70 fveq2 ( 𝑘 = 1 → ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ , ⟨ 3 , 𝑟 ⟩ } ‘ 𝑘 ) = ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ , ⟨ 3 , 𝑟 ⟩ } ‘ 1 ) )
71 23 26 fvtp1 ( ( 1 ≠ 2 ∧ 1 ≠ 3 ) → ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ , ⟨ 3 , 𝑟 ⟩ } ‘ 1 ) = 𝑝 )
72 29 32 71 mp2an ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ , ⟨ 3 , 𝑟 ⟩ } ‘ 1 ) = 𝑝
73 70 72 eqtrdi ( 𝑘 = 1 → ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ , ⟨ 3 , 𝑟 ⟩ } ‘ 𝑘 ) = 𝑝 )
74 fveq2 ( 𝑘 = 2 → ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ , ⟨ 3 , 𝑟 ⟩ } ‘ 𝑘 ) = ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ , ⟨ 3 , 𝑟 ⟩ } ‘ 2 ) )
75 24 27 fvtp2 ( ( 1 ≠ 2 ∧ 2 ≠ 3 ) → ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ , ⟨ 3 , 𝑟 ⟩ } ‘ 2 ) = 𝑞 )
76 29 35 75 mp2an ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ , ⟨ 3 , 𝑟 ⟩ } ‘ 2 ) = 𝑞
77 74 76 eqtrdi ( 𝑘 = 2 → ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ , ⟨ 3 , 𝑟 ⟩ } ‘ 𝑘 ) = 𝑞 )
78 fveq2 ( 𝑘 = 3 → ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ , ⟨ 3 , 𝑟 ⟩ } ‘ 𝑘 ) = ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ , ⟨ 3 , 𝑟 ⟩ } ‘ 3 ) )
79 25 28 fvtp3 ( ( 1 ≠ 3 ∧ 2 ≠ 3 ) → ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ , ⟨ 3 , 𝑟 ⟩ } ‘ 3 ) = 𝑟 )
80 32 35 79 mp2an ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ , ⟨ 3 , 𝑟 ⟩ } ‘ 3 ) = 𝑟
81 78 80 eqtrdi ( 𝑘 = 3 → ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ , ⟨ 3 , 𝑟 ⟩ } ‘ 𝑘 ) = 𝑟 )
82 prmz ( 𝑝 ∈ ℙ → 𝑝 ∈ ℤ )
83 82 zcnd ( 𝑝 ∈ ℙ → 𝑝 ∈ ℂ )
84 prmz ( 𝑞 ∈ ℙ → 𝑞 ∈ ℤ )
85 84 zcnd ( 𝑞 ∈ ℙ → 𝑞 ∈ ℂ )
86 prmz ( 𝑟 ∈ ℙ → 𝑟 ∈ ℤ )
87 86 zcnd ( 𝑟 ∈ ℙ → 𝑟 ∈ ℂ )
88 83 85 87 3anim123i ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ∧ 𝑟 ∈ ℙ ) → ( 𝑝 ∈ ℂ ∧ 𝑞 ∈ ℂ ∧ 𝑟 ∈ ℂ ) )
89 88 3expa ( ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ∧ 𝑟 ∈ ℙ ) → ( 𝑝 ∈ ℂ ∧ 𝑞 ∈ ℂ ∧ 𝑟 ∈ ℂ ) )
90 2z 2 ∈ ℤ
91 3z 3 ∈ ℤ
92 41 90 91 3pm3.2i ( 1 ∈ ℤ ∧ 2 ∈ ℤ ∧ 3 ∈ ℤ )
93 92 a1i ( ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ∧ 𝑟 ∈ ℙ ) → ( 1 ∈ ℤ ∧ 2 ∈ ℤ ∧ 3 ∈ ℤ ) )
94 29 a1i ( ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ∧ 𝑟 ∈ ℙ ) → 1 ≠ 2 )
95 32 a1i ( ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ∧ 𝑟 ∈ ℙ ) → 1 ≠ 3 )
96 35 a1i ( ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ∧ 𝑟 ∈ ℙ ) → 2 ≠ 3 )
97 73 77 81 89 93 94 95 96 sumtp ( ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ∧ 𝑟 ∈ ℙ ) → Σ 𝑘 ∈ { 1 , 2 , 3 } ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ , ⟨ 3 , 𝑟 ⟩ } ‘ 𝑘 ) = ( ( 𝑝 + 𝑞 ) + 𝑟 ) )
98 69 97 eqtr2d ( ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ∧ 𝑟 ∈ ℙ ) → ( ( 𝑝 + 𝑞 ) + 𝑟 ) = Σ 𝑘 ∈ ( 1 ... 3 ) ( { ⟨ 1 , 𝑝 ⟩ , ⟨ 2 , 𝑞 ⟩ , ⟨ 3 , 𝑟 ⟩ } ‘ 𝑘 ) )
99 63 67 98 rspcedvd ( ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ∧ 𝑟 ∈ ℙ ) → ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 3 ) ) ( ( 𝑝 + 𝑞 ) + 𝑟 ) = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑓𝑘 ) )
100 eqeq1 ( 𝑁 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) → ( 𝑁 = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑓𝑘 ) ↔ ( ( 𝑝 + 𝑞 ) + 𝑟 ) = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑓𝑘 ) ) )
101 100 rexbidv ( 𝑁 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) → ( ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 3 ) ) 𝑁 = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑓𝑘 ) ↔ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 3 ) ) ( ( 𝑝 + 𝑞 ) + 𝑟 ) = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑓𝑘 ) ) )
102 99 101 syl5ibrcom ( ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ∧ 𝑟 ∈ ℙ ) → ( 𝑁 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) → ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 3 ) ) 𝑁 = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑓𝑘 ) ) )
103 102 adantld ( ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) ∧ 𝑟 ∈ ℙ ) → ( ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑁 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) → ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 3 ) ) 𝑁 = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑓𝑘 ) ) )
104 103 rexlimdva ( ( 𝑝 ∈ ℙ ∧ 𝑞 ∈ ℙ ) → ( ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑁 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) → ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 3 ) ) 𝑁 = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑓𝑘 ) ) )
105 104 rexlimivv ( ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑁 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) → ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 3 ) ) 𝑁 = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑓𝑘 ) )
106 105 adantl ( ( 𝑁 ∈ Odd ∧ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑁 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) ) → ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 3 ) ) 𝑁 = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑓𝑘 ) )
107 22 106 sylbi ( 𝑁 ∈ GoldbachOdd → ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 3 ) ) 𝑁 = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑓𝑘 ) )
108 107 a1i ( ( 𝑁 ∈ ( ℤ ‘ 8 ) ∧ 𝑁 ∈ Odd ) → ( 𝑁 ∈ GoldbachOdd → ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 3 ) ) 𝑁 = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑓𝑘 ) ) )
109 5 21 108 3syld ( ( 𝑁 ∈ ( ℤ ‘ 8 ) ∧ 𝑁 ∈ Odd ) → ( ∀ 𝑚 ∈ Odd ( 7 < 𝑚𝑚 ∈ GoldbachOdd ) → ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 3 ) ) 𝑁 = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑓𝑘 ) ) )
110 109 com12 ( ∀ 𝑚 ∈ Odd ( 7 < 𝑚𝑚 ∈ GoldbachOdd ) → ( ( 𝑁 ∈ ( ℤ ‘ 8 ) ∧ 𝑁 ∈ Odd ) → ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 3 ) ) 𝑁 = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑓𝑘 ) ) )