Metamath Proof Explorer

Theorem wtgoldbnnsum4prm

Description: If the (weak) ternary Goldbach conjecture is valid, then every integer greater than 1 is the sum of at most 4 primes, showing that Schnirelmann's constant would be less than or equal to 4. See corollary 1.1 in Helfgott p. 4. (Contributed by AV, 25-Jul-2020)

Ref Expression
Assertion wtgoldbnnsum4prm ( ∀ 𝑚 ∈ Odd ( 5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) → ∀ 𝑛 ∈ ( ℤ≥ ‘ 2 ) ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 4 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) )

Proof

Step Hyp Ref Expression
1 2z ⊢ 2 ∈ ℤ
2 9nn ⊢ 9 ∈ ℕ
3 2 nnzi ⊢ 9 ∈ ℤ
4 2re ⊢ 2 ∈ ℝ
5 9re ⊢ 9 ∈ ℝ
6 2lt9 ⊢ 2 < 9
7 4 5 6 ltleii ⊢ 2 ≤ 9
8 eluz2 ⊢ ( 9 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ 9 ∈ ℤ ∧ 2 ≤ 9 ) )
9 1 3 7 8 mpbir3an ⊢ 9 ∈ ( ℤ≥ ‘ 2 )
10 fzouzsplit ⊢ ( 9 ∈ ( ℤ≥ ‘ 2 ) → ( ℤ≥ ‘ 2 ) = ( ( 2 ..^ 9 ) ∪ ( ℤ≥ ‘ 9 ) ) )
11 10 eleq2d ⊢ ( 9 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↔ 𝑛 ∈ ( ( 2 ..^ 9 ) ∪ ( ℤ≥ ‘ 9 ) ) ) )
12 9 11 ax-mp ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↔ 𝑛 ∈ ( ( 2 ..^ 9 ) ∪ ( ℤ≥ ‘ 9 ) ) )
13 elun ⊢ ( 𝑛 ∈ ( ( 2 ..^ 9 ) ∪ ( ℤ≥ ‘ 9 ) ) ↔ ( 𝑛 ∈ ( 2 ..^ 9 ) ∨ 𝑛 ∈ ( ℤ≥ ‘ 9 ) ) )
14 12 13 bitri ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑛 ∈ ( 2 ..^ 9 ) ∨ 𝑛 ∈ ( ℤ≥ ‘ 9 ) ) )
15 elfzo2 ⊢ ( 𝑛 ∈ ( 2 ..^ 9 ) ↔ ( 𝑛 ∈ ( ℤ≥ ‘ 2 ) ∧ 9 ∈ ℤ ∧ 𝑛 < 9 ) )
16 simp1 ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 2 ) ∧ 9 ∈ ℤ ∧ 𝑛 < 9 ) → 𝑛 ∈ ( ℤ≥ ‘ 2 ) )
17 df-9 ⊢ 9 = ( 8 + 1 )
18 17 breq2i ⊢ ( 𝑛 < 9 ↔ 𝑛 < ( 8 + 1 ) )
19 eluz2nn ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 2 ) → 𝑛 ∈ ℕ )
20 8nn ⊢ 8 ∈ ℕ
21 19 20 jctir ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑛 ∈ ℕ ∧ 8 ∈ ℕ ) )
22 21 adantr ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 2 ) ∧ 9 ∈ ℤ ) → ( 𝑛 ∈ ℕ ∧ 8 ∈ ℕ ) )
23 nnleltp1 ⊢ ( ( 𝑛 ∈ ℕ ∧ 8 ∈ ℕ ) → ( 𝑛 ≤ 8 ↔ 𝑛 < ( 8 + 1 ) ) )
24 22 23 syl ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 2 ) ∧ 9 ∈ ℤ ) → ( 𝑛 ≤ 8 ↔ 𝑛 < ( 8 + 1 ) ) )
25 24 biimprd ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 2 ) ∧ 9 ∈ ℤ ) → ( 𝑛 < ( 8 + 1 ) → 𝑛 ≤ 8 ) )
26 18 25 biimtrid ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 2 ) ∧ 9 ∈ ℤ ) → ( 𝑛 < 9 → 𝑛 ≤ 8 ) )
27 26 3impia ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 2 ) ∧ 9 ∈ ℤ ∧ 𝑛 < 9 ) → 𝑛 ≤ 8 )
28 16 27 jca ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 2 ) ∧ 9 ∈ ℤ ∧ 𝑛 < 9 ) → ( 𝑛 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑛 ≤ 8 ) )
29 15 28 sylbi ⊢ ( 𝑛 ∈ ( 2 ..^ 9 ) → ( 𝑛 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑛 ≤ 8 ) )
30 nnsum4primesle9 ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑛 ≤ 8 ) → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 4 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) )
31 29 30 syl ⊢ ( 𝑛 ∈ ( 2 ..^ 9 ) → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 4 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) )
32 31 a1d ⊢ ( 𝑛 ∈ ( 2 ..^ 9 ) → ( ∀ 𝑚 ∈ Odd ( 5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 4 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) ) )
33 4nn ⊢ 4 ∈ ℕ
34 33 a1i ⊢ ( ( ( 𝑛 ∈ ( ℤ≥ ‘ 9 ) ∧ 𝑛 ∈ Even ) ∧ ∀ 𝑚 ∈ Odd ( 5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) ) → 4 ∈ ℕ )
35 oveq2 ⊢ ( 𝑑 = 4 → ( 1 ... 𝑑 ) = ( 1 ... 4 ) )
36 35 oveq2d ⊢ ( 𝑑 = 4 → ( ℙ ↑m ( 1 ... 𝑑 ) ) = ( ℙ ↑m ( 1 ... 4 ) ) )
37 breq1 ⊢ ( 𝑑 = 4 → ( 𝑑 ≤ 4 ↔ 4 ≤ 4 ) )
38 35 sumeq1d ⊢ ( 𝑑 = 4 → Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) = Σ 𝑘 ∈ ( 1 ... 4 ) ( 𝑓 ‘ 𝑘 ) )
39 38 eqeq2d ⊢ ( 𝑑 = 4 → ( 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ↔ 𝑛 = Σ 𝑘 ∈ ( 1 ... 4 ) ( 𝑓 ‘ 𝑘 ) ) )
40 37 39 anbi12d ⊢ ( 𝑑 = 4 → ( ( 𝑑 ≤ 4 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) ↔ ( 4 ≤ 4 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 4 ) ( 𝑓 ‘ 𝑘 ) ) ) )
41 36 40 rexeqbidv ⊢ ( 𝑑 = 4 → ( ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 4 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) ↔ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 4 ) ) ( 4 ≤ 4 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 4 ) ( 𝑓 ‘ 𝑘 ) ) ) )
42 41 adantl ⊢ ( ( ( ( 𝑛 ∈ ( ℤ≥ ‘ 9 ) ∧ 𝑛 ∈ Even ) ∧ ∀ 𝑚 ∈ Odd ( 5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) ) ∧ 𝑑 = 4 ) → ( ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 4 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) ↔ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 4 ) ) ( 4 ≤ 4 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 4 ) ( 𝑓 ‘ 𝑘 ) ) ) )
43 4re ⊢ 4 ∈ ℝ
44 43 leidi ⊢ 4 ≤ 4
45 44 a1i ⊢ ( ( ( 𝑛 ∈ ( ℤ≥ ‘ 9 ) ∧ 𝑛 ∈ Even ) ∧ ∀ 𝑚 ∈ Odd ( 5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) ) → 4 ≤ 4 )
46 nnsum4primeseven ⊢ ( ∀ 𝑚 ∈ Odd ( 5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) → ( ( 𝑛 ∈ ( ℤ≥ ‘ 9 ) ∧ 𝑛 ∈ Even ) → ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 4 ) ) 𝑛 = Σ 𝑘 ∈ ( 1 ... 4 ) ( 𝑓 ‘ 𝑘 ) ) )
47 46 impcom ⊢ ( ( ( 𝑛 ∈ ( ℤ≥ ‘ 9 ) ∧ 𝑛 ∈ Even ) ∧ ∀ 𝑚 ∈ Odd ( 5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) ) → ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 4 ) ) 𝑛 = Σ 𝑘 ∈ ( 1 ... 4 ) ( 𝑓 ‘ 𝑘 ) )
48 r19.42v ⊢ ( ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 4 ) ) ( 4 ≤ 4 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 4 ) ( 𝑓 ‘ 𝑘 ) ) ↔ ( 4 ≤ 4 ∧ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 4 ) ) 𝑛 = Σ 𝑘 ∈ ( 1 ... 4 ) ( 𝑓 ‘ 𝑘 ) ) )
49 45 47 48 sylanbrc ⊢ ( ( ( 𝑛 ∈ ( ℤ≥ ‘ 9 ) ∧ 𝑛 ∈ Even ) ∧ ∀ 𝑚 ∈ Odd ( 5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) ) → ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 4 ) ) ( 4 ≤ 4 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 4 ) ( 𝑓 ‘ 𝑘 ) ) )
50 34 42 49 rspcedvd ⊢ ( ( ( 𝑛 ∈ ( ℤ≥ ‘ 9 ) ∧ 𝑛 ∈ Even ) ∧ ∀ 𝑚 ∈ Odd ( 5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) ) → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 4 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) )
51 50 ex ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 9 ) ∧ 𝑛 ∈ Even ) → ( ∀ 𝑚 ∈ Odd ( 5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 4 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) ) )
52 3nn ⊢ 3 ∈ ℕ
53 52 a1i ⊢ ( ( ( 𝑛 ∈ ( ℤ≥ ‘ 9 ) ∧ 𝑛 ∈ Odd ) ∧ ∀ 𝑚 ∈ Odd ( 5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) ) → 3 ∈ ℕ )
54 oveq2 ⊢ ( 𝑑 = 3 → ( 1 ... 𝑑 ) = ( 1 ... 3 ) )
55 54 oveq2d ⊢ ( 𝑑 = 3 → ( ℙ ↑m ( 1 ... 𝑑 ) ) = ( ℙ ↑m ( 1 ... 3 ) ) )
56 breq1 ⊢ ( 𝑑 = 3 → ( 𝑑 ≤ 4 ↔ 3 ≤ 4 ) )
57 54 sumeq1d ⊢ ( 𝑑 = 3 → Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑓 ‘ 𝑘 ) )
58 57 eqeq2d ⊢ ( 𝑑 = 3 → ( 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ↔ 𝑛 = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑓 ‘ 𝑘 ) ) )
59 56 58 anbi12d ⊢ ( 𝑑 = 3 → ( ( 𝑑 ≤ 4 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) ↔ ( 3 ≤ 4 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑓 ‘ 𝑘 ) ) ) )
60 55 59 rexeqbidv ⊢ ( 𝑑 = 3 → ( ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 4 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) ↔ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 3 ) ) ( 3 ≤ 4 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑓 ‘ 𝑘 ) ) ) )
61 60 adantl ⊢ ( ( ( ( 𝑛 ∈ ( ℤ≥ ‘ 9 ) ∧ 𝑛 ∈ Odd ) ∧ ∀ 𝑚 ∈ Odd ( 5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) ) ∧ 𝑑 = 3 ) → ( ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 4 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) ↔ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 3 ) ) ( 3 ≤ 4 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑓 ‘ 𝑘 ) ) ) )
62 3re ⊢ 3 ∈ ℝ
63 3lt4 ⊢ 3 < 4
64 62 43 63 ltleii ⊢ 3 ≤ 4
65 64 a1i ⊢ ( ( ( 𝑛 ∈ ( ℤ≥ ‘ 9 ) ∧ 𝑛 ∈ Odd ) ∧ ∀ 𝑚 ∈ Odd ( 5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) ) → 3 ≤ 4 )
66 6nn ⊢ 6 ∈ ℕ
67 66 nnzi ⊢ 6 ∈ ℤ
68 6re ⊢ 6 ∈ ℝ
69 6lt9 ⊢ 6 < 9
70 68 5 69 ltleii ⊢ 6 ≤ 9
71 eluzuzle ⊢ ( ( 6 ∈ ℤ ∧ 6 ≤ 9 ) → ( 𝑛 ∈ ( ℤ≥ ‘ 9 ) → 𝑛 ∈ ( ℤ≥ ‘ 6 ) ) )
72 67 70 71 mp2an ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 9 ) → 𝑛 ∈ ( ℤ≥ ‘ 6 ) )
73 72 anim1i ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 9 ) ∧ 𝑛 ∈ Odd ) → ( 𝑛 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝑛 ∈ Odd ) )
74 nnsum4primesodd ⊢ ( ∀ 𝑚 ∈ Odd ( 5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) → ( ( 𝑛 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝑛 ∈ Odd ) → ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 3 ) ) 𝑛 = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑓 ‘ 𝑘 ) ) )
75 73 74 mpan9 ⊢ ( ( ( 𝑛 ∈ ( ℤ≥ ‘ 9 ) ∧ 𝑛 ∈ Odd ) ∧ ∀ 𝑚 ∈ Odd ( 5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) ) → ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 3 ) ) 𝑛 = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑓 ‘ 𝑘 ) )
76 r19.42v ⊢ ( ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 3 ) ) ( 3 ≤ 4 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑓 ‘ 𝑘 ) ) ↔ ( 3 ≤ 4 ∧ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 3 ) ) 𝑛 = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑓 ‘ 𝑘 ) ) )
77 65 75 76 sylanbrc ⊢ ( ( ( 𝑛 ∈ ( ℤ≥ ‘ 9 ) ∧ 𝑛 ∈ Odd ) ∧ ∀ 𝑚 ∈ Odd ( 5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) ) → ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 3 ) ) ( 3 ≤ 4 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑓 ‘ 𝑘 ) ) )
78 53 61 77 rspcedvd ⊢ ( ( ( 𝑛 ∈ ( ℤ≥ ‘ 9 ) ∧ 𝑛 ∈ Odd ) ∧ ∀ 𝑚 ∈ Odd ( 5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) ) → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 4 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) )
79 78 ex ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 9 ) ∧ 𝑛 ∈ Odd ) → ( ∀ 𝑚 ∈ Odd ( 5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 4 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) ) )
80 eluzelz ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 9 ) → 𝑛 ∈ ℤ )
81 zeoALTV ⊢ ( 𝑛 ∈ ℤ → ( 𝑛 ∈ Even ∨ 𝑛 ∈ Odd ) )
82 80 81 syl ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 9 ) → ( 𝑛 ∈ Even ∨ 𝑛 ∈ Odd ) )
83 51 79 82 mpjaodan ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 9 ) → ( ∀ 𝑚 ∈ Odd ( 5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 4 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) ) )
84 32 83 jaoi ⊢ ( ( 𝑛 ∈ ( 2 ..^ 9 ) ∨ 𝑛 ∈ ( ℤ≥ ‘ 9 ) ) → ( ∀ 𝑚 ∈ Odd ( 5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 4 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) ) )
85 14 84 sylbi ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 2 ) → ( ∀ 𝑚 ∈ Odd ( 5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 4 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) ) )
86 85 impcom ⊢ ( ( ∀ 𝑚 ∈ Odd ( 5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 2 ) ) → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 4 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) )
87 86 ralrimiva ⊢ ( ∀ 𝑚 ∈ Odd ( 5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) → ∀ 𝑛 ∈ ( ℤ≥ ‘ 2 ) ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 4 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) )