Proof of Theorem nnsum3primesle9
| Step | Hyp | Ref
| Expression |
| 1 | | eluzelre 12889 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈ ℝ) |
| 2 | | 8re 12362 |
. . . . . 6
⊢ 8 ∈
ℝ |
| 3 | 2 | a1i 11 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) → 8 ∈ ℝ) |
| 4 | 1, 3 | leloed 11404 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 ≤ 8 ↔ (𝑁 < 8 ∨ 𝑁 = 8))) |
| 5 | | eluzelz 12888 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈ ℤ) |
| 6 | | 7nn 12358 |
. . . . . . . . . 10
⊢ 7 ∈
ℕ |
| 7 | 6 | nnzi 12641 |
. . . . . . . . 9
⊢ 7 ∈
ℤ |
| 8 | | zleltp1 12668 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 7 ∈
ℤ) → (𝑁 ≤ 7
↔ 𝑁 < (7 +
1))) |
| 9 | 5, 7, 8 | sylancl 586 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 ≤ 7 ↔ 𝑁 < (7 + 1))) |
| 10 | | 7re 12359 |
. . . . . . . . . 10
⊢ 7 ∈
ℝ |
| 11 | 10 | a1i 11 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘2) → 7 ∈ ℝ) |
| 12 | 1, 11 | leloed 11404 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 ≤ 7 ↔ (𝑁 < 7 ∨ 𝑁 = 7))) |
| 13 | | 7p1e8 12415 |
. . . . . . . . . 10
⊢ (7 + 1) =
8 |
| 14 | 13 | breq2i 5151 |
. . . . . . . . 9
⊢ (𝑁 < (7 + 1) ↔ 𝑁 < 8) |
| 15 | 14 | a1i 11 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 < (7 + 1) ↔ 𝑁 < 8)) |
| 16 | 9, 12, 15 | 3bitr3rd 310 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 < 8 ↔ (𝑁 < 7 ∨ 𝑁 = 7))) |
| 17 | | 6nn 12355 |
. . . . . . . . . . . 12
⊢ 6 ∈
ℕ |
| 18 | 17 | nnzi 12641 |
. . . . . . . . . . 11
⊢ 6 ∈
ℤ |
| 19 | | zleltp1 12668 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ 6 ∈
ℤ) → (𝑁 ≤ 6
↔ 𝑁 < (6 +
1))) |
| 20 | 5, 18, 19 | sylancl 586 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 ≤ 6 ↔ 𝑁 < (6 + 1))) |
| 21 | | 6re 12356 |
. . . . . . . . . . . 12
⊢ 6 ∈
ℝ |
| 22 | 21 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘2) → 6 ∈ ℝ) |
| 23 | 1, 22 | leloed 11404 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 ≤ 6 ↔ (𝑁 < 6 ∨ 𝑁 = 6))) |
| 24 | | 6p1e7 12414 |
. . . . . . . . . . . 12
⊢ (6 + 1) =
7 |
| 25 | 24 | breq2i 5151 |
. . . . . . . . . . 11
⊢ (𝑁 < (6 + 1) ↔ 𝑁 < 7) |
| 26 | 25 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 < (6 + 1) ↔ 𝑁 < 7)) |
| 27 | 20, 23, 26 | 3bitr3rd 310 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 < 7 ↔ (𝑁 < 6 ∨ 𝑁 = 6))) |
| 28 | | 5nn 12352 |
. . . . . . . . . . . . . 14
⊢ 5 ∈
ℕ |
| 29 | 28 | nnzi 12641 |
. . . . . . . . . . . . 13
⊢ 5 ∈
ℤ |
| 30 | | zleltp1 12668 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℤ ∧ 5 ∈
ℤ) → (𝑁 ≤ 5
↔ 𝑁 < (5 +
1))) |
| 31 | 5, 29, 30 | sylancl 586 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 ≤ 5 ↔ 𝑁 < (5 + 1))) |
| 32 | | 5re 12353 |
. . . . . . . . . . . . . 14
⊢ 5 ∈
ℝ |
| 33 | 32 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈
(ℤ≥‘2) → 5 ∈ ℝ) |
| 34 | 1, 33 | leloed 11404 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 ≤ 5 ↔ (𝑁 < 5 ∨ 𝑁 = 5))) |
| 35 | | 5p1e6 12413 |
. . . . . . . . . . . . . 14
⊢ (5 + 1) =
6 |
| 36 | 35 | breq2i 5151 |
. . . . . . . . . . . . 13
⊢ (𝑁 < (5 + 1) ↔ 𝑁 < 6) |
| 37 | 36 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 < (5 + 1) ↔ 𝑁 < 6)) |
| 38 | 31, 34, 37 | 3bitr3rd 310 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 < 6 ↔ (𝑁 < 5 ∨ 𝑁 = 5))) |
| 39 | | 4z 12651 |
. . . . . . . . . . . . . . 15
⊢ 4 ∈
ℤ |
| 40 | | zleltp1 12668 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℤ ∧ 4 ∈
ℤ) → (𝑁 ≤ 4
↔ 𝑁 < (4 +
1))) |
| 41 | 5, 39, 40 | sylancl 586 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 ≤ 4 ↔ 𝑁 < (4 + 1))) |
| 42 | | 4re 12350 |
. . . . . . . . . . . . . . . 16
⊢ 4 ∈
ℝ |
| 43 | 42 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈
(ℤ≥‘2) → 4 ∈ ℝ) |
| 44 | 1, 43 | leloed 11404 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 ≤ 4 ↔ (𝑁 < 4 ∨ 𝑁 = 4))) |
| 45 | | 4p1e5 12412 |
. . . . . . . . . . . . . . . 16
⊢ (4 + 1) =
5 |
| 46 | 45 | breq2i 5151 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 < (4 + 1) ↔ 𝑁 < 5) |
| 47 | 46 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 < (4 + 1) ↔ 𝑁 < 5)) |
| 48 | 41, 44, 47 | 3bitr3rd 310 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 < 5 ↔ (𝑁 < 4 ∨ 𝑁 = 4))) |
| 49 | | 3z 12650 |
. . . . . . . . . . . . . . . . 17
⊢ 3 ∈
ℤ |
| 50 | | zleltp1 12668 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℤ ∧ 3 ∈
ℤ) → (𝑁 ≤ 3
↔ 𝑁 < (3 +
1))) |
| 51 | 5, 49, 50 | sylancl 586 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 ≤ 3 ↔ 𝑁 < (3 + 1))) |
| 52 | | 3re 12346 |
. . . . . . . . . . . . . . . . . 18
⊢ 3 ∈
ℝ |
| 53 | 52 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈
(ℤ≥‘2) → 3 ∈ ℝ) |
| 54 | 1, 53 | leloed 11404 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 ≤ 3 ↔ (𝑁 < 3 ∨ 𝑁 = 3))) |
| 55 | | 3p1e4 12411 |
. . . . . . . . . . . . . . . . . 18
⊢ (3 + 1) =
4 |
| 56 | 55 | breq2i 5151 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 < (3 + 1) ↔ 𝑁 < 4) |
| 57 | 56 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 < (3 + 1) ↔ 𝑁 < 4)) |
| 58 | 51, 54, 57 | 3bitr3rd 310 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 < 4 ↔ (𝑁 < 3 ∨ 𝑁 = 3))) |
| 59 | | eluz2 12884 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈
(ℤ≥‘2) ↔ (2 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 2 ≤
𝑁)) |
| 60 | | 2re 12340 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 2 ∈
ℝ |
| 61 | 60 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ ℤ → 2 ∈
ℝ) |
| 62 | | zre 12617 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
| 63 | 61, 62 | leloed 11404 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℤ → (2 ≤
𝑁 ↔ (2 < 𝑁 ∨ 2 = 𝑁))) |
| 64 | | 3m1e2 12394 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (3
− 1) = 2 |
| 65 | 64 | eqcomi 2746 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 2 = (3
− 1) |
| 66 | 65 | breq1i 5150 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (2 <
𝑁 ↔ (3 − 1) <
𝑁) |
| 67 | | zlem1lt 12669 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((3
∈ ℤ ∧ 𝑁
∈ ℤ) → (3 ≤ 𝑁 ↔ (3 − 1) < 𝑁)) |
| 68 | 49, 67 | mpan 690 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℤ → (3 ≤
𝑁 ↔ (3 − 1) <
𝑁)) |
| 69 | 68 | biimprd 248 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℤ → ((3
− 1) < 𝑁 → 3
≤ 𝑁)) |
| 70 | 66, 69 | biimtrid 242 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℤ → (2 <
𝑁 → 3 ≤ 𝑁)) |
| 71 | 52 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℤ → 3 ∈
ℝ) |
| 72 | 71, 62 | lenltd 11407 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℤ → (3 ≤
𝑁 ↔ ¬ 𝑁 < 3)) |
| 73 | | pm2.21 123 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (¬
𝑁 < 3 → (𝑁 < 3 → 𝑁 = 2)) |
| 74 | 72, 73 | biimtrdi 253 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℤ → (3 ≤
𝑁 → (𝑁 < 3 → 𝑁 = 2))) |
| 75 | 70, 74 | syldc 48 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (2 <
𝑁 → (𝑁 ∈ ℤ → (𝑁 < 3 → 𝑁 = 2))) |
| 76 | | eqcom 2744 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (2 =
𝑁 ↔ 𝑁 = 2) |
| 77 | 76 | biimpi 216 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (2 =
𝑁 → 𝑁 = 2) |
| 78 | 77 | 2a1d 26 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (2 =
𝑁 → (𝑁 ∈ ℤ → (𝑁 < 3 → 𝑁 = 2))) |
| 79 | 75, 78 | jaoi 858 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((2 <
𝑁 ∨ 2 = 𝑁) → (𝑁 ∈ ℤ → (𝑁 < 3 → 𝑁 = 2))) |
| 80 | 79 | com12 32 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℤ → ((2 <
𝑁 ∨ 2 = 𝑁) → (𝑁 < 3 → 𝑁 = 2))) |
| 81 | 63, 80 | sylbid 240 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℤ → (2 ≤
𝑁 → (𝑁 < 3 → 𝑁 = 2))) |
| 82 | 81 | imp 406 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℤ ∧ 2 ≤
𝑁) → (𝑁 < 3 → 𝑁 = 2)) |
| 83 | | 2lt3 12438 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 <
3 |
| 84 | | breq1 5146 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 = 2 → (𝑁 < 3 ↔ 2 < 3)) |
| 85 | 83, 84 | mpbiri 258 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 = 2 → 𝑁 < 3) |
| 86 | 82, 85 | impbid1 225 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℤ ∧ 2 ≤
𝑁) → (𝑁 < 3 ↔ 𝑁 = 2)) |
| 87 | 86 | 3adant1 1131 |
. . . . . . . . . . . . . . . . 17
⊢ ((2
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 2 ≤ 𝑁) → (𝑁 < 3 ↔ 𝑁 = 2)) |
| 88 | 59, 87 | sylbi 217 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 < 3 ↔ 𝑁 = 2)) |
| 89 | 88 | orbi1d 917 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈
(ℤ≥‘2) → ((𝑁 < 3 ∨ 𝑁 = 3) ↔ (𝑁 = 2 ∨ 𝑁 = 3))) |
| 90 | 58, 89 | bitrd 279 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 < 4 ↔ (𝑁 = 2 ∨ 𝑁 = 3))) |
| 91 | 90 | orbi1d 917 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈
(ℤ≥‘2) → ((𝑁 < 4 ∨ 𝑁 = 4) ↔ ((𝑁 = 2 ∨ 𝑁 = 3) ∨ 𝑁 = 4))) |
| 92 | 48, 91 | bitrd 279 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 < 5 ↔ ((𝑁 = 2 ∨ 𝑁 = 3) ∨ 𝑁 = 4))) |
| 93 | 92 | orbi1d 917 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘2) → ((𝑁 < 5 ∨ 𝑁 = 5) ↔ (((𝑁 = 2 ∨ 𝑁 = 3) ∨ 𝑁 = 4) ∨ 𝑁 = 5))) |
| 94 | 38, 93 | bitrd 279 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 < 6 ↔ (((𝑁 = 2 ∨ 𝑁 = 3) ∨ 𝑁 = 4) ∨ 𝑁 = 5))) |
| 95 | 94 | orbi1d 917 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘2) → ((𝑁 < 6 ∨ 𝑁 = 6) ↔ ((((𝑁 = 2 ∨ 𝑁 = 3) ∨ 𝑁 = 4) ∨ 𝑁 = 5) ∨ 𝑁 = 6))) |
| 96 | 27, 95 | bitrd 279 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 < 7 ↔ ((((𝑁 = 2 ∨ 𝑁 = 3) ∨ 𝑁 = 4) ∨ 𝑁 = 5) ∨ 𝑁 = 6))) |
| 97 | 96 | orbi1d 917 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → ((𝑁 < 7 ∨ 𝑁 = 7) ↔ (((((𝑁 = 2 ∨ 𝑁 = 3) ∨ 𝑁 = 4) ∨ 𝑁 = 5) ∨ 𝑁 = 6) ∨ 𝑁 = 7))) |
| 98 | 16, 97 | bitrd 279 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 < 8 ↔ (((((𝑁 = 2 ∨ 𝑁 = 3) ∨ 𝑁 = 4) ∨ 𝑁 = 5) ∨ 𝑁 = 6) ∨ 𝑁 = 7))) |
| 99 | 98 | orbi1d 917 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) → ((𝑁 < 8 ∨ 𝑁 = 8) ↔ ((((((𝑁 = 2 ∨ 𝑁 = 3) ∨ 𝑁 = 4) ∨ 𝑁 = 5) ∨ 𝑁 = 6) ∨ 𝑁 = 7) ∨ 𝑁 = 8))) |
| 100 | 99 | biimpd 229 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → ((𝑁 < 8 ∨ 𝑁 = 8) → ((((((𝑁 = 2 ∨ 𝑁 = 3) ∨ 𝑁 = 4) ∨ 𝑁 = 5) ∨ 𝑁 = 6) ∨ 𝑁 = 7) ∨ 𝑁 = 8))) |
| 101 | 4, 100 | sylbid 240 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 ≤ 8 → ((((((𝑁 = 2 ∨ 𝑁 = 3) ∨ 𝑁 = 4) ∨ 𝑁 = 5) ∨ 𝑁 = 6) ∨ 𝑁 = 7) ∨ 𝑁 = 8))) |
| 102 | 101 | imp 406 |
. 2
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑁 ≤ 8) → ((((((𝑁 = 2 ∨ 𝑁 = 3) ∨ 𝑁 = 4) ∨ 𝑁 = 5) ∨ 𝑁 = 6) ∨ 𝑁 = 7) ∨ 𝑁 = 8)) |
| 103 | | 2prm 16729 |
. . . . . . . . . 10
⊢ 2 ∈
ℙ |
| 104 | | eleq1 2829 |
. . . . . . . . . 10
⊢ (𝑁 = 2 → (𝑁 ∈ ℙ ↔ 2 ∈
ℙ)) |
| 105 | 103, 104 | mpbiri 258 |
. . . . . . . . 9
⊢ (𝑁 = 2 → 𝑁 ∈ ℙ) |
| 106 | | nnsum3primesprm 47777 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℙ →
∃𝑑 ∈ ℕ
∃𝑓 ∈ (ℙ
↑m (1...𝑑))(𝑑 ≤ 3 ∧ 𝑁 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) |
| 107 | 105, 106 | syl 17 |
. . . . . . . 8
⊢ (𝑁 = 2 → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ
↑m (1...𝑑))(𝑑 ≤ 3 ∧ 𝑁 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) |
| 108 | | 3prm 16731 |
. . . . . . . . . 10
⊢ 3 ∈
ℙ |
| 109 | | eleq1 2829 |
. . . . . . . . . 10
⊢ (𝑁 = 3 → (𝑁 ∈ ℙ ↔ 3 ∈
ℙ)) |
| 110 | 108, 109 | mpbiri 258 |
. . . . . . . . 9
⊢ (𝑁 = 3 → 𝑁 ∈ ℙ) |
| 111 | 110, 106 | syl 17 |
. . . . . . . 8
⊢ (𝑁 = 3 → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ
↑m (1...𝑑))(𝑑 ≤ 3 ∧ 𝑁 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) |
| 112 | 107, 111 | jaoi 858 |
. . . . . . 7
⊢ ((𝑁 = 2 ∨ 𝑁 = 3) → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑m
(1...𝑑))(𝑑 ≤ 3 ∧ 𝑁 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) |
| 113 | | nnsum3primes4 47775 |
. . . . . . . 8
⊢
∃𝑑 ∈
ℕ ∃𝑓 ∈
(ℙ ↑m (1...𝑑))(𝑑 ≤ 3 ∧ 4 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘)) |
| 114 | | eqeq1 2741 |
. . . . . . . . . 10
⊢ (𝑁 = 4 → (𝑁 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘) ↔ 4 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) |
| 115 | 114 | anbi2d 630 |
. . . . . . . . 9
⊢ (𝑁 = 4 → ((𝑑 ≤ 3 ∧ 𝑁 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘)) ↔ (𝑑 ≤ 3 ∧ 4 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘)))) |
| 116 | 115 | 2rexbidv 3222 |
. . . . . . . 8
⊢ (𝑁 = 4 → (∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ
↑m (1...𝑑))(𝑑 ≤ 3 ∧ 𝑁 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘)) ↔ ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑m
(1...𝑑))(𝑑 ≤ 3 ∧ 4 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘)))) |
| 117 | 113, 116 | mpbiri 258 |
. . . . . . 7
⊢ (𝑁 = 4 → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ
↑m (1...𝑑))(𝑑 ≤ 3 ∧ 𝑁 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) |
| 118 | 112, 117 | jaoi 858 |
. . . . . 6
⊢ (((𝑁 = 2 ∨ 𝑁 = 3) ∨ 𝑁 = 4) → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑m
(1...𝑑))(𝑑 ≤ 3 ∧ 𝑁 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) |
| 119 | | 5prm 17146 |
. . . . . . . 8
⊢ 5 ∈
ℙ |
| 120 | | eleq1 2829 |
. . . . . . . 8
⊢ (𝑁 = 5 → (𝑁 ∈ ℙ ↔ 5 ∈
ℙ)) |
| 121 | 119, 120 | mpbiri 258 |
. . . . . . 7
⊢ (𝑁 = 5 → 𝑁 ∈ ℙ) |
| 122 | 121, 106 | syl 17 |
. . . . . 6
⊢ (𝑁 = 5 → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ
↑m (1...𝑑))(𝑑 ≤ 3 ∧ 𝑁 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) |
| 123 | 118, 122 | jaoi 858 |
. . . . 5
⊢ ((((𝑁 = 2 ∨ 𝑁 = 3) ∨ 𝑁 = 4) ∨ 𝑁 = 5) → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑m
(1...𝑑))(𝑑 ≤ 3 ∧ 𝑁 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) |
| 124 | | 6gbe 47758 |
. . . . . . 7
⊢ 6 ∈
GoldbachEven |
| 125 | | eleq1 2829 |
. . . . . . 7
⊢ (𝑁 = 6 → (𝑁 ∈ GoldbachEven ↔ 6 ∈
GoldbachEven )) |
| 126 | 124, 125 | mpbiri 258 |
. . . . . 6
⊢ (𝑁 = 6 → 𝑁 ∈ GoldbachEven ) |
| 127 | | nnsum3primesgbe 47779 |
. . . . . 6
⊢ (𝑁 ∈ GoldbachEven →
∃𝑑 ∈ ℕ
∃𝑓 ∈ (ℙ
↑m (1...𝑑))(𝑑 ≤ 3 ∧ 𝑁 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) |
| 128 | 126, 127 | syl 17 |
. . . . 5
⊢ (𝑁 = 6 → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ
↑m (1...𝑑))(𝑑 ≤ 3 ∧ 𝑁 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) |
| 129 | 123, 128 | jaoi 858 |
. . . 4
⊢
(((((𝑁 = 2 ∨
𝑁 = 3) ∨ 𝑁 = 4) ∨ 𝑁 = 5) ∨ 𝑁 = 6) → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑m
(1...𝑑))(𝑑 ≤ 3 ∧ 𝑁 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) |
| 130 | | 7prm 17148 |
. . . . . 6
⊢ 7 ∈
ℙ |
| 131 | | eleq1 2829 |
. . . . . 6
⊢ (𝑁 = 7 → (𝑁 ∈ ℙ ↔ 7 ∈
ℙ)) |
| 132 | 130, 131 | mpbiri 258 |
. . . . 5
⊢ (𝑁 = 7 → 𝑁 ∈ ℙ) |
| 133 | 132, 106 | syl 17 |
. . . 4
⊢ (𝑁 = 7 → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ
↑m (1...𝑑))(𝑑 ≤ 3 ∧ 𝑁 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) |
| 134 | 129, 133 | jaoi 858 |
. . 3
⊢
((((((𝑁 = 2 ∨
𝑁 = 3) ∨ 𝑁 = 4) ∨ 𝑁 = 5) ∨ 𝑁 = 6) ∨ 𝑁 = 7) → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑m
(1...𝑑))(𝑑 ≤ 3 ∧ 𝑁 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) |
| 135 | | 8gbe 47760 |
. . . . 5
⊢ 8 ∈
GoldbachEven |
| 136 | | eleq1 2829 |
. . . . 5
⊢ (𝑁 = 8 → (𝑁 ∈ GoldbachEven ↔ 8 ∈
GoldbachEven )) |
| 137 | 135, 136 | mpbiri 258 |
. . . 4
⊢ (𝑁 = 8 → 𝑁 ∈ GoldbachEven ) |
| 138 | 137, 127 | syl 17 |
. . 3
⊢ (𝑁 = 8 → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ
↑m (1...𝑑))(𝑑 ≤ 3 ∧ 𝑁 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) |
| 139 | 134, 138 | jaoi 858 |
. 2
⊢
(((((((𝑁 = 2 ∨
𝑁 = 3) ∨ 𝑁 = 4) ∨ 𝑁 = 5) ∨ 𝑁 = 6) ∨ 𝑁 = 7) ∨ 𝑁 = 8) → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑m
(1...𝑑))(𝑑 ≤ 3 ∧ 𝑁 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) |
| 140 | 102, 139 | syl 17 |
1
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑁 ≤ 8) → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑m
(1...𝑑))(𝑑 ≤ 3 ∧ 𝑁 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) |