Metamath Proof Explorer

Theorem bgoldbnnsum3prm

Description: If the binary Goldbach conjecture is valid, then every integer greater than 1 is the sum of at most 3 primes, showing that Schnirelmann's constant would be equal to 3. (Contributed by AV, 2-Aug-2020)

Ref Expression
Assertion bgoldbnnsum3prm ( ∀ 𝑚 ∈ Even ( 4 < 𝑚 → 𝑚 ∈ GoldbachEven ) → ∀ 𝑛 ∈ ( ℤ≥ ‘ 2 ) ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑛 = Σ 𝑘 ∈ ( 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 syl5bi ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 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 nnsum3primesle9 ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑛 ≤ 8 ) → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) )
31 29 30 syl ⊢ ( 𝑛 ∈ ( 2 ..^ 9 ) → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) )
32 31 a1d ⊢ ( 𝑛 ∈ ( 2 ..^ 9 ) → ( ∀ 𝑚 ∈ Even ( 4 < 𝑚 → 𝑚 ∈ GoldbachEven ) → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) ) )
33 breq2 ⊢ ( 𝑚 = 𝑛 → ( 4 < 𝑚 ↔ 4 < 𝑛 ) )
34 eleq1w ⊢ ( 𝑚 = 𝑛 → ( 𝑚 ∈ GoldbachEven ↔ 𝑛 ∈ GoldbachEven ) )
35 33 34 imbi12d ⊢ ( 𝑚 = 𝑛 → ( ( 4 < 𝑚 → 𝑚 ∈ GoldbachEven ) ↔ ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) ) )
36 35 rspcv ⊢ ( 𝑛 ∈ Even → ( ∀ 𝑚 ∈ Even ( 4 < 𝑚 → 𝑚 ∈ GoldbachEven ) → ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) ) )
37 4re ⊢ 4 ∈ ℝ
38 37 a1i ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 9 ) → 4 ∈ ℝ )
39 5 a1i ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 9 ) → 9 ∈ ℝ )
40 eluzelre ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 9 ) → 𝑛 ∈ ℝ )
41 38 39 40 3jca ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 9 ) → ( 4 ∈ ℝ ∧ 9 ∈ ℝ ∧ 𝑛 ∈ ℝ ) )
42 41 adantl ⊢ ( ( 𝑛 ∈ Even ∧ 𝑛 ∈ ( ℤ≥ ‘ 9 ) ) → ( 4 ∈ ℝ ∧ 9 ∈ ℝ ∧ 𝑛 ∈ ℝ ) )
43 eluzle ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 9 ) → 9 ≤ 𝑛 )
44 43 adantl ⊢ ( ( 𝑛 ∈ Even ∧ 𝑛 ∈ ( ℤ≥ ‘ 9 ) ) → 9 ≤ 𝑛 )
45 4lt9 ⊢ 4 < 9
46 44 45 jctil ⊢ ( ( 𝑛 ∈ Even ∧ 𝑛 ∈ ( ℤ≥ ‘ 9 ) ) → ( 4 < 9 ∧ 9 ≤ 𝑛 ) )
47 ltletr ⊢ ( ( 4 ∈ ℝ ∧ 9 ∈ ℝ ∧ 𝑛 ∈ ℝ ) → ( ( 4 < 9 ∧ 9 ≤ 𝑛 ) → 4 < 𝑛 ) )
48 42 46 47 sylc ⊢ ( ( 𝑛 ∈ Even ∧ 𝑛 ∈ ( ℤ≥ ‘ 9 ) ) → 4 < 𝑛 )
49 pm2.27 ⊢ ( 4 < 𝑛 → ( ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → 𝑛 ∈ GoldbachEven ) )
50 48 49 syl ⊢ ( ( 𝑛 ∈ Even ∧ 𝑛 ∈ ( ℤ≥ ‘ 9 ) ) → ( ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → 𝑛 ∈ GoldbachEven ) )
51 50 ex ⊢ ( 𝑛 ∈ Even → ( 𝑛 ∈ ( ℤ≥ ‘ 9 ) → ( ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → 𝑛 ∈ GoldbachEven ) ) )
52 36 51 syl5d ⊢ ( 𝑛 ∈ Even → ( 𝑛 ∈ ( ℤ≥ ‘ 9 ) → ( ∀ 𝑚 ∈ Even ( 4 < 𝑚 → 𝑚 ∈ GoldbachEven ) → 𝑛 ∈ GoldbachEven ) ) )
53 52 impcom ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 9 ) ∧ 𝑛 ∈ Even ) → ( ∀ 𝑚 ∈ Even ( 4 < 𝑚 → 𝑚 ∈ GoldbachEven ) → 𝑛 ∈ GoldbachEven ) )
54 nnsum3primesgbe ⊢ ( 𝑛 ∈ GoldbachEven → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) )
55 53 54 syl6 ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 9 ) ∧ 𝑛 ∈ Even ) → ( ∀ 𝑚 ∈ Even ( 4 < 𝑚 → 𝑚 ∈ GoldbachEven ) → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) ) )
56 3nn ⊢ 3 ∈ ℕ
57 56 a1i ⊢ ( ( ( 𝑛 ∈ ( ℤ≥ ‘ 9 ) ∧ 𝑛 ∈ Odd ) ∧ ∀ 𝑜 ∈ Odd ( 5 < 𝑜 → 𝑜 ∈ GoldbachOddW ) ) → 3 ∈ ℕ )
58 oveq2 ⊢ ( 𝑑 = 3 → ( 1 ... 𝑑 ) = ( 1 ... 3 ) )
59 58 oveq2d ⊢ ( 𝑑 = 3 → ( ℙ ↑m ( 1 ... 𝑑 ) ) = ( ℙ ↑m ( 1 ... 3 ) ) )
60 breq1 ⊢ ( 𝑑 = 3 → ( 𝑑 ≤ 3 ↔ 3 ≤ 3 ) )
61 58 sumeq1d ⊢ ( 𝑑 = 3 → Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑓 ‘ 𝑘 ) )
62 61 eqeq2d ⊢ ( 𝑑 = 3 → ( 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ↔ 𝑛 = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑓 ‘ 𝑘 ) ) )
63 60 62 anbi12d ⊢ ( 𝑑 = 3 → ( ( 𝑑 ≤ 3 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) ↔ ( 3 ≤ 3 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑓 ‘ 𝑘 ) ) ) )
64 59 63 rexeqbidv ⊢ ( 𝑑 = 3 → ( ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) ↔ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 3 ) ) ( 3 ≤ 3 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑓 ‘ 𝑘 ) ) ) )
65 64 adantl ⊢ ( ( ( ( 𝑛 ∈ ( ℤ≥ ‘ 9 ) ∧ 𝑛 ∈ Odd ) ∧ ∀ 𝑜 ∈ Odd ( 5 < 𝑜 → 𝑜 ∈ GoldbachOddW ) ) ∧ 𝑑 = 3 ) → ( ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) ↔ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 3 ) ) ( 3 ≤ 3 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑓 ‘ 𝑘 ) ) ) )
66 3re ⊢ 3 ∈ ℝ
67 66 leidi ⊢ 3 ≤ 3
68 67 a1i ⊢ ( ( ( 𝑛 ∈ ( ℤ≥ ‘ 9 ) ∧ 𝑛 ∈ Odd ) ∧ ∀ 𝑜 ∈ Odd ( 5 < 𝑜 → 𝑜 ∈ GoldbachOddW ) ) → 3 ≤ 3 )
69 6nn ⊢ 6 ∈ ℕ
70 69 nnzi ⊢ 6 ∈ ℤ
71 6re ⊢ 6 ∈ ℝ
72 6lt9 ⊢ 6 < 9
73 71 5 72 ltleii ⊢ 6 ≤ 9
74 eluzuzle ⊢ ( ( 6 ∈ ℤ ∧ 6 ≤ 9 ) → ( 𝑛 ∈ ( ℤ≥ ‘ 9 ) → 𝑛 ∈ ( ℤ≥ ‘ 6 ) ) )
75 70 73 74 mp2an ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 9 ) → 𝑛 ∈ ( ℤ≥ ‘ 6 ) )
76 75 anim1i ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 9 ) ∧ 𝑛 ∈ Odd ) → ( 𝑛 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝑛 ∈ Odd ) )
77 nnsum4primesodd ⊢ ( ∀ 𝑜 ∈ Odd ( 5 < 𝑜 → 𝑜 ∈ GoldbachOddW ) → ( ( 𝑛 ∈ ( ℤ≥ ‘ 6 ) ∧ 𝑛 ∈ Odd ) → ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 3 ) ) 𝑛 = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑓 ‘ 𝑘 ) ) )
78 76 77 mpan9 ⊢ ( ( ( 𝑛 ∈ ( ℤ≥ ‘ 9 ) ∧ 𝑛 ∈ Odd ) ∧ ∀ 𝑜 ∈ Odd ( 5 < 𝑜 → 𝑜 ∈ GoldbachOddW ) ) → ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 3 ) ) 𝑛 = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑓 ‘ 𝑘 ) )
79 r19.42v ⊢ ( ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 3 ) ) ( 3 ≤ 3 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑓 ‘ 𝑘 ) ) ↔ ( 3 ≤ 3 ∧ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 3 ) ) 𝑛 = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑓 ‘ 𝑘 ) ) )
80 68 78 79 sylanbrc ⊢ ( ( ( 𝑛 ∈ ( ℤ≥ ‘ 9 ) ∧ 𝑛 ∈ Odd ) ∧ ∀ 𝑜 ∈ Odd ( 5 < 𝑜 → 𝑜 ∈ GoldbachOddW ) ) → ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 3 ) ) ( 3 ≤ 3 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 3 ) ( 𝑓 ‘ 𝑘 ) ) )
81 57 65 80 rspcedvd ⊢ ( ( ( 𝑛 ∈ ( ℤ≥ ‘ 9 ) ∧ 𝑛 ∈ Odd ) ∧ ∀ 𝑜 ∈ Odd ( 5 < 𝑜 → 𝑜 ∈ GoldbachOddW ) ) → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) )
82 81 expcom ⊢ ( ∀ 𝑜 ∈ Odd ( 5 < 𝑜 → 𝑜 ∈ GoldbachOddW ) → ( ( 𝑛 ∈ ( ℤ≥ ‘ 9 ) ∧ 𝑛 ∈ Odd ) → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) ) )
83 sbgoldbwt ⊢ ( ∀ 𝑚 ∈ Even ( 4 < 𝑚 → 𝑚 ∈ GoldbachEven ) → ∀ 𝑜 ∈ Odd ( 5 < 𝑜 → 𝑜 ∈ GoldbachOddW ) )
84 82 83 syl11 ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 9 ) ∧ 𝑛 ∈ Odd ) → ( ∀ 𝑚 ∈ Even ( 4 < 𝑚 → 𝑚 ∈ GoldbachEven ) → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) ) )
85 eluzelz ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 9 ) → 𝑛 ∈ ℤ )
86 zeoALTV ⊢ ( 𝑛 ∈ ℤ → ( 𝑛 ∈ Even ∨ 𝑛 ∈ Odd ) )
87 85 86 syl ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 9 ) → ( 𝑛 ∈ Even ∨ 𝑛 ∈ Odd ) )
88 55 84 87 mpjaodan ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 9 ) → ( ∀ 𝑚 ∈ Even ( 4 < 𝑚 → 𝑚 ∈ GoldbachEven ) → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) ) )
89 32 88 jaoi ⊢ ( ( 𝑛 ∈ ( 2 ..^ 9 ) ∨ 𝑛 ∈ ( ℤ≥ ‘ 9 ) ) → ( ∀ 𝑚 ∈ Even ( 4 < 𝑚 → 𝑚 ∈ GoldbachEven ) → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) ) )
90 14 89 sylbi ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 2 ) → ( ∀ 𝑚 ∈ Even ( 4 < 𝑚 → 𝑚 ∈ GoldbachEven ) → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) ) )
91 90 impcom ⊢ ( ( ∀ 𝑚 ∈ Even ( 4 < 𝑚 → 𝑚 ∈ GoldbachEven ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 2 ) ) → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) )
92 91 ralrimiva ⊢ ( ∀ 𝑚 ∈ Even ( 4 < 𝑚 → 𝑚 ∈ GoldbachEven ) → ∀ 𝑛 ∈ ( ℤ≥ ‘ 2 ) ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) )