Step | Hyp | Ref
| Expression |
1 | | 2z 11286 |
. . . . . . 7
⊢ 2 ∈
ℤ |
2 | | 9nn 11069 |
. . . . . . . 8
⊢ 9 ∈
ℕ |
3 | 2 | nnzi 11278 |
. . . . . . 7
⊢ 9 ∈
ℤ |
4 | | 2re 10967 |
. . . . . . . 8
⊢ 2 ∈
ℝ |
5 | | 9re 10984 |
. . . . . . . 8
⊢ 9 ∈
ℝ |
6 | | 2lt9 11105 |
. . . . . . . 8
⊢ 2 <
9 |
7 | 4, 5, 6 | ltleii 10039 |
. . . . . . 7
⊢ 2 ≤
9 |
8 | | eluz2 11569 |
. . . . . . 7
⊢ (9 ∈
(ℤ≥‘2) ↔ (2 ∈ ℤ ∧ 9 ∈
ℤ ∧ 2 ≤ 9)) |
9 | 1, 3, 7, 8 | mpbir3an 1237 |
. . . . . 6
⊢ 9 ∈
(ℤ≥‘2) |
10 | | fzouzsplit 12372 |
. . . . . . 7
⊢ (9 ∈
(ℤ≥‘2) → (ℤ≥‘2) =
((2..^9) ∪ (ℤ≥‘9))) |
11 | 10 | eleq2d 2673 |
. . . . . 6
⊢ (9 ∈
(ℤ≥‘2) → (𝑛 ∈ (ℤ≥‘2)
↔ 𝑛 ∈ ((2..^9)
∪ (ℤ≥‘9)))) |
12 | 9, 11 | ax-mp 5 |
. . . . 5
⊢ (𝑛 ∈
(ℤ≥‘2) ↔ 𝑛 ∈ ((2..^9) ∪
(ℤ≥‘9))) |
13 | | elun 3715 |
. . . . 5
⊢ (𝑛 ∈ ((2..^9) ∪
(ℤ≥‘9)) ↔ (𝑛 ∈ (2..^9) ∨ 𝑛 ∈
(ℤ≥‘9))) |
14 | 12, 13 | bitri 263 |
. . . 4
⊢ (𝑛 ∈
(ℤ≥‘2) ↔ (𝑛 ∈ (2..^9) ∨ 𝑛 ∈
(ℤ≥‘9))) |
15 | | elfzo2 12342 |
. . . . . . . 8
⊢ (𝑛 ∈ (2..^9) ↔ (𝑛 ∈
(ℤ≥‘2) ∧ 9 ∈ ℤ ∧ 𝑛 < 9)) |
16 | | simp1 1054 |
. . . . . . . . 9
⊢ ((𝑛 ∈
(ℤ≥‘2) ∧ 9 ∈ ℤ ∧ 𝑛 < 9) → 𝑛 ∈
(ℤ≥‘2)) |
17 | | df-9 10963 |
. . . . . . . . . . . 12
⊢ 9 = (8 +
1) |
18 | 17 | breq2i 4591 |
. . . . . . . . . . 11
⊢ (𝑛 < 9 ↔ 𝑛 < (8 + 1)) |
19 | | eluz2nn 11602 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈
(ℤ≥‘2) → 𝑛 ∈ ℕ) |
20 | | 8nn 11068 |
. . . . . . . . . . . . . . 15
⊢ 8 ∈
ℕ |
21 | 19, 20 | jctir 559 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈
(ℤ≥‘2) → (𝑛 ∈ ℕ ∧ 8 ∈
ℕ)) |
22 | 21 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈
(ℤ≥‘2) ∧ 9 ∈ ℤ) → (𝑛 ∈ ℕ ∧ 8 ∈
ℕ)) |
23 | | nnleltp1 11309 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℕ ∧ 8 ∈
ℕ) → (𝑛 ≤ 8
↔ 𝑛 < (8 +
1))) |
24 | 22, 23 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈
(ℤ≥‘2) ∧ 9 ∈ ℤ) → (𝑛 ≤ 8 ↔ 𝑛 < (8 + 1))) |
25 | 24 | biimprd 237 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈
(ℤ≥‘2) ∧ 9 ∈ ℤ) → (𝑛 < (8 + 1) → 𝑛 ≤ 8)) |
26 | 18, 25 | syl5bi 231 |
. . . . . . . . . 10
⊢ ((𝑛 ∈
(ℤ≥‘2) ∧ 9 ∈ ℤ) → (𝑛 < 9 → 𝑛 ≤ 8)) |
27 | 26 | 3impia 1253 |
. . . . . . . . 9
⊢ ((𝑛 ∈
(ℤ≥‘2) ∧ 9 ∈ ℤ ∧ 𝑛 < 9) → 𝑛 ≤ 8) |
28 | 16, 27 | jca 553 |
. . . . . . . 8
⊢ ((𝑛 ∈
(ℤ≥‘2) ∧ 9 ∈ ℤ ∧ 𝑛 < 9) → (𝑛 ∈
(ℤ≥‘2) ∧ 𝑛 ≤ 8)) |
29 | 15, 28 | sylbi 206 |
. . . . . . 7
⊢ (𝑛 ∈ (2..^9) → (𝑛 ∈
(ℤ≥‘2) ∧ 𝑛 ≤ 8)) |
30 | | nnsum3primesle9 40210 |
. . . . . . 7
⊢ ((𝑛 ∈
(ℤ≥‘2) ∧ 𝑛 ≤ 8) → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑𝑚
(1...𝑑))(𝑑 ≤ 3 ∧ 𝑛 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) |
31 | 29, 30 | syl 17 |
. . . . . 6
⊢ (𝑛 ∈ (2..^9) →
∃𝑑 ∈ ℕ
∃𝑓 ∈ (ℙ
↑𝑚 (1...𝑑))(𝑑 ≤ 3 ∧ 𝑛 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) |
32 | 31 | a1d 25 |
. . . . 5
⊢ (𝑛 ∈ (2..^9) →
(∀𝑚 ∈ Even (4
< 𝑚 → 𝑚 ∈ GoldbachEven ) →
∃𝑑 ∈ ℕ
∃𝑓 ∈ (ℙ
↑𝑚 (1...𝑑))(𝑑 ≤ 3 ∧ 𝑛 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘)))) |
33 | | breq2 4587 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → (4 < 𝑚 ↔ 4 < 𝑛)) |
34 | | eleq1 2676 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → (𝑚 ∈ GoldbachEven ↔ 𝑛 ∈ GoldbachEven
)) |
35 | 33, 34 | imbi12d 333 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑛 → ((4 < 𝑚 → 𝑚 ∈ GoldbachEven ) ↔ (4 < 𝑛 → 𝑛 ∈ GoldbachEven ))) |
36 | 35 | rspcv 3278 |
. . . . . . . . 9
⊢ (𝑛 ∈ Even →
(∀𝑚 ∈ Even (4
< 𝑚 → 𝑚 ∈ GoldbachEven ) → (4
< 𝑛 → 𝑛 ∈ GoldbachEven
))) |
37 | | 4re 10974 |
. . . . . . . . . . . . . . 15
⊢ 4 ∈
ℝ |
38 | 37 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈
(ℤ≥‘9) → 4 ∈ ℝ) |
39 | 5 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈
(ℤ≥‘9) → 9 ∈ ℝ) |
40 | | eluzelre 11574 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈
(ℤ≥‘9) → 𝑛 ∈ ℝ) |
41 | 38, 39, 40 | 3jca 1235 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈
(ℤ≥‘9) → (4 ∈ ℝ ∧ 9 ∈
ℝ ∧ 𝑛 ∈
ℝ)) |
42 | 41 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ Even ∧ 𝑛 ∈
(ℤ≥‘9)) → (4 ∈ ℝ ∧ 9 ∈
ℝ ∧ 𝑛 ∈
ℝ)) |
43 | | eluzle 11576 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈
(ℤ≥‘9) → 9 ≤ 𝑛) |
44 | 43 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ Even ∧ 𝑛 ∈
(ℤ≥‘9)) → 9 ≤ 𝑛) |
45 | | 4lt9 11103 |
. . . . . . . . . . . . 13
⊢ 4 <
9 |
46 | 44, 45 | jctil 558 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ Even ∧ 𝑛 ∈
(ℤ≥‘9)) → (4 < 9 ∧ 9 ≤ 𝑛)) |
47 | | ltletr 10008 |
. . . . . . . . . . . 12
⊢ ((4
∈ ℝ ∧ 9 ∈ ℝ ∧ 𝑛 ∈ ℝ) → ((4 < 9 ∧ 9
≤ 𝑛) → 4 < 𝑛)) |
48 | 42, 46, 47 | sylc 63 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ Even ∧ 𝑛 ∈
(ℤ≥‘9)) → 4 < 𝑛) |
49 | | pm2.27 41 |
. . . . . . . . . . 11
⊢ (4 <
𝑛 → ((4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → 𝑛 ∈ GoldbachEven
)) |
50 | 48, 49 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ Even ∧ 𝑛 ∈
(ℤ≥‘9)) → ((4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → 𝑛 ∈ GoldbachEven
)) |
51 | 50 | ex 449 |
. . . . . . . . 9
⊢ (𝑛 ∈ Even → (𝑛 ∈
(ℤ≥‘9) → ((4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → 𝑛 ∈ GoldbachEven
))) |
52 | 36, 51 | syl5d 71 |
. . . . . . . 8
⊢ (𝑛 ∈ Even → (𝑛 ∈
(ℤ≥‘9) → (∀𝑚 ∈ Even (4 < 𝑚 → 𝑚 ∈ GoldbachEven ) → 𝑛 ∈ GoldbachEven
))) |
53 | 52 | impcom 445 |
. . . . . . 7
⊢ ((𝑛 ∈
(ℤ≥‘9) ∧ 𝑛 ∈ Even ) → (∀𝑚 ∈ Even (4 < 𝑚 → 𝑚 ∈ GoldbachEven ) → 𝑛 ∈ GoldbachEven
)) |
54 | | nnsum3primesgbe 40208 |
. . . . . . 7
⊢ (𝑛 ∈ GoldbachEven →
∃𝑑 ∈ ℕ
∃𝑓 ∈ (ℙ
↑𝑚 (1...𝑑))(𝑑 ≤ 3 ∧ 𝑛 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) |
55 | 53, 54 | syl6 34 |
. . . . . 6
⊢ ((𝑛 ∈
(ℤ≥‘9) ∧ 𝑛 ∈ Even ) → (∀𝑚 ∈ Even (4 < 𝑚 → 𝑚 ∈ GoldbachEven ) → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ
↑𝑚 (1...𝑑))(𝑑 ≤ 3 ∧ 𝑛 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘)))) |
56 | | bgoldbwt 40199 |
. . . . . . . 8
⊢
(∀𝑚 ∈
Even (4 < 𝑚 → 𝑚 ∈ GoldbachEven ) →
∀𝑜 ∈ Odd (5
< 𝑜 → 𝑜 ∈ GoldbachOdd
)) |
57 | | 3nn 11063 |
. . . . . . . . . . 11
⊢ 3 ∈
ℕ |
58 | 57 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝑛 ∈
(ℤ≥‘9) ∧ 𝑛 ∈ Odd ) ∧ ∀𝑜 ∈ Odd (5 < 𝑜 → 𝑜 ∈ GoldbachOdd )) → 3 ∈
ℕ) |
59 | | oveq2 6557 |
. . . . . . . . . . . . 13
⊢ (𝑑 = 3 → (1...𝑑) = (1...3)) |
60 | 59 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (𝑑 = 3 → (ℙ
↑𝑚 (1...𝑑)) = (ℙ ↑𝑚
(1...3))) |
61 | | breq1 4586 |
. . . . . . . . . . . . 13
⊢ (𝑑 = 3 → (𝑑 ≤ 3 ↔ 3 ≤ 3)) |
62 | 59 | sumeq1d 14279 |
. . . . . . . . . . . . . 14
⊢ (𝑑 = 3 → Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘) = Σ𝑘 ∈ (1...3)(𝑓‘𝑘)) |
63 | 62 | eqeq2d 2620 |
. . . . . . . . . . . . 13
⊢ (𝑑 = 3 → (𝑛 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘) ↔ 𝑛 = Σ𝑘 ∈ (1...3)(𝑓‘𝑘))) |
64 | 61, 63 | anbi12d 743 |
. . . . . . . . . . . 12
⊢ (𝑑 = 3 → ((𝑑 ≤ 3 ∧ 𝑛 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘)) ↔ (3 ≤ 3 ∧ 𝑛 = Σ𝑘 ∈ (1...3)(𝑓‘𝑘)))) |
65 | 60, 64 | rexeqbidv 3130 |
. . . . . . . . . . 11
⊢ (𝑑 = 3 → (∃𝑓 ∈ (ℙ
↑𝑚 (1...𝑑))(𝑑 ≤ 3 ∧ 𝑛 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘)) ↔ ∃𝑓 ∈ (ℙ ↑𝑚
(1...3))(3 ≤ 3 ∧ 𝑛 =
Σ𝑘 ∈
(1...3)(𝑓‘𝑘)))) |
66 | 65 | adantl 481 |
. . . . . . . . . 10
⊢ ((((𝑛 ∈
(ℤ≥‘9) ∧ 𝑛 ∈ Odd ) ∧ ∀𝑜 ∈ Odd (5 < 𝑜 → 𝑜 ∈ GoldbachOdd )) ∧ 𝑑 = 3) → (∃𝑓 ∈ (ℙ
↑𝑚 (1...𝑑))(𝑑 ≤ 3 ∧ 𝑛 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘)) ↔ ∃𝑓 ∈ (ℙ ↑𝑚
(1...3))(3 ≤ 3 ∧ 𝑛 =
Σ𝑘 ∈
(1...3)(𝑓‘𝑘)))) |
67 | | 3re 10971 |
. . . . . . . . . . . . 13
⊢ 3 ∈
ℝ |
68 | 67 | leidi 10441 |
. . . . . . . . . . . 12
⊢ 3 ≤
3 |
69 | 68 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝑛 ∈
(ℤ≥‘9) ∧ 𝑛 ∈ Odd ) ∧ ∀𝑜 ∈ Odd (5 < 𝑜 → 𝑜 ∈ GoldbachOdd )) → 3 ≤
3) |
70 | | 6nn 11066 |
. . . . . . . . . . . . . . 15
⊢ 6 ∈
ℕ |
71 | 70 | nnzi 11278 |
. . . . . . . . . . . . . 14
⊢ 6 ∈
ℤ |
72 | | 6re 10978 |
. . . . . . . . . . . . . . 15
⊢ 6 ∈
ℝ |
73 | | 6lt9 11101 |
. . . . . . . . . . . . . . 15
⊢ 6 <
9 |
74 | 72, 5, 73 | ltleii 10039 |
. . . . . . . . . . . . . 14
⊢ 6 ≤
9 |
75 | | eluzuzle 11572 |
. . . . . . . . . . . . . 14
⊢ ((6
∈ ℤ ∧ 6 ≤ 9) → (𝑛 ∈ (ℤ≥‘9)
→ 𝑛 ∈
(ℤ≥‘6))) |
76 | 71, 74, 75 | mp2an 704 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈
(ℤ≥‘9) → 𝑛 ∈
(ℤ≥‘6)) |
77 | 76 | anim1i 590 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈
(ℤ≥‘9) ∧ 𝑛 ∈ Odd ) → (𝑛 ∈ (ℤ≥‘6)
∧ 𝑛 ∈ Odd
)) |
78 | | nnsum4primesodd 40212 |
. . . . . . . . . . . 12
⊢
(∀𝑜 ∈
Odd (5 < 𝑜 → 𝑜 ∈ GoldbachOdd ) →
((𝑛 ∈
(ℤ≥‘6) ∧ 𝑛 ∈ Odd ) → ∃𝑓 ∈ (ℙ
↑𝑚 (1...3))𝑛 = Σ𝑘 ∈ (1...3)(𝑓‘𝑘))) |
79 | 77, 78 | mpan9 485 |
. . . . . . . . . . 11
⊢ (((𝑛 ∈
(ℤ≥‘9) ∧ 𝑛 ∈ Odd ) ∧ ∀𝑜 ∈ Odd (5 < 𝑜 → 𝑜 ∈ GoldbachOdd )) → ∃𝑓 ∈ (ℙ
↑𝑚 (1...3))𝑛 = Σ𝑘 ∈ (1...3)(𝑓‘𝑘)) |
80 | | r19.42v 3073 |
. . . . . . . . . . 11
⊢
(∃𝑓 ∈
(ℙ ↑𝑚 (1...3))(3 ≤ 3 ∧ 𝑛 = Σ𝑘 ∈ (1...3)(𝑓‘𝑘)) ↔ (3 ≤ 3 ∧ ∃𝑓 ∈ (ℙ
↑𝑚 (1...3))𝑛 = Σ𝑘 ∈ (1...3)(𝑓‘𝑘))) |
81 | 69, 79, 80 | sylanbrc 695 |
. . . . . . . . . 10
⊢ (((𝑛 ∈
(ℤ≥‘9) ∧ 𝑛 ∈ Odd ) ∧ ∀𝑜 ∈ Odd (5 < 𝑜 → 𝑜 ∈ GoldbachOdd )) → ∃𝑓 ∈ (ℙ
↑𝑚 (1...3))(3 ≤ 3 ∧ 𝑛 = Σ𝑘 ∈ (1...3)(𝑓‘𝑘))) |
82 | 58, 66, 81 | rspcedvd 3289 |
. . . . . . . . 9
⊢ (((𝑛 ∈
(ℤ≥‘9) ∧ 𝑛 ∈ Odd ) ∧ ∀𝑜 ∈ Odd (5 < 𝑜 → 𝑜 ∈ GoldbachOdd )) → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ
↑𝑚 (1...𝑑))(𝑑 ≤ 3 ∧ 𝑛 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) |
83 | 82 | expcom 450 |
. . . . . . . 8
⊢
(∀𝑜 ∈
Odd (5 < 𝑜 → 𝑜 ∈ GoldbachOdd ) →
((𝑛 ∈
(ℤ≥‘9) ∧ 𝑛 ∈ Odd ) → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ
↑𝑚 (1...𝑑))(𝑑 ≤ 3 ∧ 𝑛 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘)))) |
84 | 56, 83 | syl 17 |
. . . . . . 7
⊢
(∀𝑚 ∈
Even (4 < 𝑚 → 𝑚 ∈ GoldbachEven ) →
((𝑛 ∈
(ℤ≥‘9) ∧ 𝑛 ∈ Odd ) → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ
↑𝑚 (1...𝑑))(𝑑 ≤ 3 ∧ 𝑛 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘)))) |
85 | 84 | com12 32 |
. . . . . 6
⊢ ((𝑛 ∈
(ℤ≥‘9) ∧ 𝑛 ∈ Odd ) → (∀𝑚 ∈ Even (4 < 𝑚 → 𝑚 ∈ GoldbachEven ) → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ
↑𝑚 (1...𝑑))(𝑑 ≤ 3 ∧ 𝑛 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘)))) |
86 | | eluzelz 11573 |
. . . . . . 7
⊢ (𝑛 ∈
(ℤ≥‘9) → 𝑛 ∈ ℤ) |
87 | | zeoALTV 40119 |
. . . . . . 7
⊢ (𝑛 ∈ ℤ → (𝑛 ∈ Even ∨ 𝑛 ∈ Odd )) |
88 | 86, 87 | syl 17 |
. . . . . 6
⊢ (𝑛 ∈
(ℤ≥‘9) → (𝑛 ∈ Even ∨ 𝑛 ∈ Odd )) |
89 | 55, 85, 88 | mpjaodan 823 |
. . . . 5
⊢ (𝑛 ∈
(ℤ≥‘9) → (∀𝑚 ∈ Even (4 < 𝑚 → 𝑚 ∈ GoldbachEven ) → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ
↑𝑚 (1...𝑑))(𝑑 ≤ 3 ∧ 𝑛 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘)))) |
90 | 32, 89 | jaoi 393 |
. . . 4
⊢ ((𝑛 ∈ (2..^9) ∨ 𝑛 ∈
(ℤ≥‘9)) → (∀𝑚 ∈ Even (4 < 𝑚 → 𝑚 ∈ GoldbachEven ) → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ
↑𝑚 (1...𝑑))(𝑑 ≤ 3 ∧ 𝑛 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘)))) |
91 | 14, 90 | sylbi 206 |
. . 3
⊢ (𝑛 ∈
(ℤ≥‘2) → (∀𝑚 ∈ Even (4 < 𝑚 → 𝑚 ∈ GoldbachEven ) → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ
↑𝑚 (1...𝑑))(𝑑 ≤ 3 ∧ 𝑛 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘)))) |
92 | 91 | impcom 445 |
. 2
⊢
((∀𝑚 ∈
Even (4 < 𝑚 → 𝑚 ∈ GoldbachEven ) ∧
𝑛 ∈
(ℤ≥‘2)) → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑𝑚
(1...𝑑))(𝑑 ≤ 3 ∧ 𝑛 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) |
93 | 92 | ralrimiva 2949 |
1
⊢
(∀𝑚 ∈
Even (4 < 𝑚 → 𝑚 ∈ GoldbachEven ) →
∀𝑛 ∈
(ℤ≥‘2)∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑𝑚
(1...𝑑))(𝑑 ≤ 3 ∧ 𝑛 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) |