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 ) ( 𝑓 ‘ 𝑘 ) ) )