Proof of Theorem nnsum3primesle9
Step | Hyp | Ref
| Expression |
1 | | eluzelre 12335 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈ ℝ) |
2 | | 8re 11812 |
. . . . . 6
⊢ 8 ∈
ℝ |
3 | 2 | a1i 11 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) → 8 ∈ ℝ) |
4 | 1, 3 | leloed 10861 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 ≤ 8 ↔ (𝑁 < 8 ∨ 𝑁 = 8))) |
5 | | eluzelz 12334 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈ ℤ) |
6 | | 7nn 11808 |
. . . . . . . . . 10
⊢ 7 ∈
ℕ |
7 | 6 | nnzi 12087 |
. . . . . . . . 9
⊢ 7 ∈
ℤ |
8 | | zleltp1 12114 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 7 ∈
ℤ) → (𝑁 ≤ 7
↔ 𝑁 < (7 +
1))) |
9 | 5, 7, 8 | sylancl 589 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 ≤ 7 ↔ 𝑁 < (7 + 1))) |
10 | | 7re 11809 |
. . . . . . . . . 10
⊢ 7 ∈
ℝ |
11 | 10 | a1i 11 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘2) → 7 ∈ ℝ) |
12 | 1, 11 | leloed 10861 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 ≤ 7 ↔ (𝑁 < 7 ∨ 𝑁 = 7))) |
13 | | 7p1e8 11865 |
. . . . . . . . . 10
⊢ (7 + 1) =
8 |
14 | 13 | breq2i 5038 |
. . . . . . . . 9
⊢ (𝑁 < (7 + 1) ↔ 𝑁 < 8) |
15 | 14 | a1i 11 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 < (7 + 1) ↔ 𝑁 < 8)) |
16 | 9, 12, 15 | 3bitr3rd 313 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 < 8 ↔ (𝑁 < 7 ∨ 𝑁 = 7))) |
17 | | 6nn 11805 |
. . . . . . . . . . . 12
⊢ 6 ∈
ℕ |
18 | 17 | nnzi 12087 |
. . . . . . . . . . 11
⊢ 6 ∈
ℤ |
19 | | zleltp1 12114 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ 6 ∈
ℤ) → (𝑁 ≤ 6
↔ 𝑁 < (6 +
1))) |
20 | 5, 18, 19 | sylancl 589 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 ≤ 6 ↔ 𝑁 < (6 + 1))) |
21 | | 6re 11806 |
. . . . . . . . . . . 12
⊢ 6 ∈
ℝ |
22 | 21 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘2) → 6 ∈ ℝ) |
23 | 1, 22 | leloed 10861 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 ≤ 6 ↔ (𝑁 < 6 ∨ 𝑁 = 6))) |
24 | | 6p1e7 11864 |
. . . . . . . . . . . 12
⊢ (6 + 1) =
7 |
25 | 24 | breq2i 5038 |
. . . . . . . . . . 11
⊢ (𝑁 < (6 + 1) ↔ 𝑁 < 7) |
26 | 25 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 < (6 + 1) ↔ 𝑁 < 7)) |
27 | 20, 23, 26 | 3bitr3rd 313 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 < 7 ↔ (𝑁 < 6 ∨ 𝑁 = 6))) |
28 | | 5nn 11802 |
. . . . . . . . . . . . . 14
⊢ 5 ∈
ℕ |
29 | 28 | nnzi 12087 |
. . . . . . . . . . . . 13
⊢ 5 ∈
ℤ |
30 | | zleltp1 12114 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℤ ∧ 5 ∈
ℤ) → (𝑁 ≤ 5
↔ 𝑁 < (5 +
1))) |
31 | 5, 29, 30 | sylancl 589 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 ≤ 5 ↔ 𝑁 < (5 + 1))) |
32 | | 5re 11803 |
. . . . . . . . . . . . . 14
⊢ 5 ∈
ℝ |
33 | 32 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈
(ℤ≥‘2) → 5 ∈ ℝ) |
34 | 1, 33 | leloed 10861 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 ≤ 5 ↔ (𝑁 < 5 ∨ 𝑁 = 5))) |
35 | | 5p1e6 11863 |
. . . . . . . . . . . . . 14
⊢ (5 + 1) =
6 |
36 | 35 | breq2i 5038 |
. . . . . . . . . . . . 13
⊢ (𝑁 < (5 + 1) ↔ 𝑁 < 6) |
37 | 36 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 < (5 + 1) ↔ 𝑁 < 6)) |
38 | 31, 34, 37 | 3bitr3rd 313 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 < 6 ↔ (𝑁 < 5 ∨ 𝑁 = 5))) |
39 | | 4z 12097 |
. . . . . . . . . . . . . . 15
⊢ 4 ∈
ℤ |
40 | | zleltp1 12114 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℤ ∧ 4 ∈
ℤ) → (𝑁 ≤ 4
↔ 𝑁 < (4 +
1))) |
41 | 5, 39, 40 | sylancl 589 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 ≤ 4 ↔ 𝑁 < (4 + 1))) |
42 | | 4re 11800 |
. . . . . . . . . . . . . . . 16
⊢ 4 ∈
ℝ |
43 | 42 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈
(ℤ≥‘2) → 4 ∈ ℝ) |
44 | 1, 43 | leloed 10861 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 ≤ 4 ↔ (𝑁 < 4 ∨ 𝑁 = 4))) |
45 | | 4p1e5 11862 |
. . . . . . . . . . . . . . . 16
⊢ (4 + 1) =
5 |
46 | 45 | breq2i 5038 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 < (4 + 1) ↔ 𝑁 < 5) |
47 | 46 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 < (4 + 1) ↔ 𝑁 < 5)) |
48 | 41, 44, 47 | 3bitr3rd 313 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 < 5 ↔ (𝑁 < 4 ∨ 𝑁 = 4))) |
49 | | 3z 12096 |
. . . . . . . . . . . . . . . . 17
⊢ 3 ∈
ℤ |
50 | | zleltp1 12114 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℤ ∧ 3 ∈
ℤ) → (𝑁 ≤ 3
↔ 𝑁 < (3 +
1))) |
51 | 5, 49, 50 | sylancl 589 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 ≤ 3 ↔ 𝑁 < (3 + 1))) |
52 | | 3re 11796 |
. . . . . . . . . . . . . . . . . 18
⊢ 3 ∈
ℝ |
53 | 52 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈
(ℤ≥‘2) → 3 ∈ ℝ) |
54 | 1, 53 | leloed 10861 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 ≤ 3 ↔ (𝑁 < 3 ∨ 𝑁 = 3))) |
55 | | 3p1e4 11861 |
. . . . . . . . . . . . . . . . . 18
⊢ (3 + 1) =
4 |
56 | 55 | breq2i 5038 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 < (3 + 1) ↔ 𝑁 < 4) |
57 | 56 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 < (3 + 1) ↔ 𝑁 < 4)) |
58 | 51, 54, 57 | 3bitr3rd 313 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 < 4 ↔ (𝑁 < 3 ∨ 𝑁 = 3))) |
59 | | eluz2 12330 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈
(ℤ≥‘2) ↔ (2 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 2 ≤
𝑁)) |
60 | | 2re 11790 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 2 ∈
ℝ |
61 | 60 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ ℤ → 2 ∈
ℝ) |
62 | | zre 12066 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
63 | 61, 62 | leloed 10861 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℤ → (2 ≤
𝑁 ↔ (2 < 𝑁 ∨ 2 = 𝑁))) |
64 | | 3m1e2 11844 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (3
− 1) = 2 |
65 | 64 | eqcomi 2747 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 2 = (3
− 1) |
66 | 65 | breq1i 5037 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (2 <
𝑁 ↔ (3 − 1) <
𝑁) |
67 | | zlem1lt 12115 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((3
∈ ℤ ∧ 𝑁
∈ ℤ) → (3 ≤ 𝑁 ↔ (3 − 1) < 𝑁)) |
68 | 49, 67 | mpan 690 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℤ → (3 ≤
𝑁 ↔ (3 − 1) <
𝑁)) |
69 | 68 | biimprd 251 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℤ → ((3
− 1) < 𝑁 → 3
≤ 𝑁)) |
70 | 66, 69 | syl5bi 245 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℤ → (2 <
𝑁 → 3 ≤ 𝑁)) |
71 | 52 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℤ → 3 ∈
ℝ) |
72 | 71, 62 | lenltd 10864 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℤ → (3 ≤
𝑁 ↔ ¬ 𝑁 < 3)) |
73 | | pm2.21 123 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (¬
𝑁 < 3 → (𝑁 < 3 → 𝑁 = 2)) |
74 | 72, 73 | syl6bi 256 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℤ → (3 ≤
𝑁 → (𝑁 < 3 → 𝑁 = 2))) |
75 | 70, 74 | syldc 48 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (2 <
𝑁 → (𝑁 ∈ ℤ → (𝑁 < 3 → 𝑁 = 2))) |
76 | | eqcom 2745 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (2 =
𝑁 ↔ 𝑁 = 2) |
77 | 76 | biimpi 219 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (2 =
𝑁 → 𝑁 = 2) |
78 | 77 | 2a1d 26 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (2 =
𝑁 → (𝑁 ∈ ℤ → (𝑁 < 3 → 𝑁 = 2))) |
79 | 75, 78 | jaoi 856 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((2 <
𝑁 ∨ 2 = 𝑁) → (𝑁 ∈ ℤ → (𝑁 < 3 → 𝑁 = 2))) |
80 | 79 | com12 32 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℤ → ((2 <
𝑁 ∨ 2 = 𝑁) → (𝑁 < 3 → 𝑁 = 2))) |
81 | 63, 80 | sylbid 243 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℤ → (2 ≤
𝑁 → (𝑁 < 3 → 𝑁 = 2))) |
82 | 81 | imp 410 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈ ℤ ∧ 2 ≤
𝑁) → (𝑁 < 3 → 𝑁 = 2)) |
83 | | 2lt3 11888 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 <
3 |
84 | | breq1 5033 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 = 2 → (𝑁 < 3 ↔ 2 < 3)) |
85 | 83, 84 | mpbiri 261 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 = 2 → 𝑁 < 3) |
86 | 82, 85 | impbid1 228 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℤ ∧ 2 ≤
𝑁) → (𝑁 < 3 ↔ 𝑁 = 2)) |
87 | 86 | 3adant1 1131 |
. . . . . . . . . . . . . . . . 17
⊢ ((2
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 2 ≤ 𝑁) → (𝑁 < 3 ↔ 𝑁 = 2)) |
88 | 59, 87 | sylbi 220 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 < 3 ↔ 𝑁 = 2)) |
89 | 88 | orbi1d 916 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈
(ℤ≥‘2) → ((𝑁 < 3 ∨ 𝑁 = 3) ↔ (𝑁 = 2 ∨ 𝑁 = 3))) |
90 | 58, 89 | bitrd 282 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 < 4 ↔ (𝑁 = 2 ∨ 𝑁 = 3))) |
91 | 90 | orbi1d 916 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈
(ℤ≥‘2) → ((𝑁 < 4 ∨ 𝑁 = 4) ↔ ((𝑁 = 2 ∨ 𝑁 = 3) ∨ 𝑁 = 4))) |
92 | 48, 91 | bitrd 282 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 < 5 ↔ ((𝑁 = 2 ∨ 𝑁 = 3) ∨ 𝑁 = 4))) |
93 | 92 | orbi1d 916 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘2) → ((𝑁 < 5 ∨ 𝑁 = 5) ↔ (((𝑁 = 2 ∨ 𝑁 = 3) ∨ 𝑁 = 4) ∨ 𝑁 = 5))) |
94 | 38, 93 | bitrd 282 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 < 6 ↔ (((𝑁 = 2 ∨ 𝑁 = 3) ∨ 𝑁 = 4) ∨ 𝑁 = 5))) |
95 | 94 | orbi1d 916 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘2) → ((𝑁 < 6 ∨ 𝑁 = 6) ↔ ((((𝑁 = 2 ∨ 𝑁 = 3) ∨ 𝑁 = 4) ∨ 𝑁 = 5) ∨ 𝑁 = 6))) |
96 | 27, 95 | bitrd 282 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 < 7 ↔ ((((𝑁 = 2 ∨ 𝑁 = 3) ∨ 𝑁 = 4) ∨ 𝑁 = 5) ∨ 𝑁 = 6))) |
97 | 96 | orbi1d 916 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → ((𝑁 < 7 ∨ 𝑁 = 7) ↔ (((((𝑁 = 2 ∨ 𝑁 = 3) ∨ 𝑁 = 4) ∨ 𝑁 = 5) ∨ 𝑁 = 6) ∨ 𝑁 = 7))) |
98 | 16, 97 | bitrd 282 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 < 8 ↔ (((((𝑁 = 2 ∨ 𝑁 = 3) ∨ 𝑁 = 4) ∨ 𝑁 = 5) ∨ 𝑁 = 6) ∨ 𝑁 = 7))) |
99 | 98 | orbi1d 916 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) → ((𝑁 < 8 ∨ 𝑁 = 8) ↔ ((((((𝑁 = 2 ∨ 𝑁 = 3) ∨ 𝑁 = 4) ∨ 𝑁 = 5) ∨ 𝑁 = 6) ∨ 𝑁 = 7) ∨ 𝑁 = 8))) |
100 | 99 | biimpd 232 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → ((𝑁 < 8 ∨ 𝑁 = 8) → ((((((𝑁 = 2 ∨ 𝑁 = 3) ∨ 𝑁 = 4) ∨ 𝑁 = 5) ∨ 𝑁 = 6) ∨ 𝑁 = 7) ∨ 𝑁 = 8))) |
101 | 4, 100 | sylbid 243 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 ≤ 8 → ((((((𝑁 = 2 ∨ 𝑁 = 3) ∨ 𝑁 = 4) ∨ 𝑁 = 5) ∨ 𝑁 = 6) ∨ 𝑁 = 7) ∨ 𝑁 = 8))) |
102 | 101 | imp 410 |
. 2
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑁 ≤ 8) → ((((((𝑁 = 2 ∨ 𝑁 = 3) ∨ 𝑁 = 4) ∨ 𝑁 = 5) ∨ 𝑁 = 6) ∨ 𝑁 = 7) ∨ 𝑁 = 8)) |
103 | | 2prm 16133 |
. . . . . . . . . 10
⊢ 2 ∈
ℙ |
104 | | eleq1 2820 |
. . . . . . . . . 10
⊢ (𝑁 = 2 → (𝑁 ∈ ℙ ↔ 2 ∈
ℙ)) |
105 | 103, 104 | mpbiri 261 |
. . . . . . . . 9
⊢ (𝑁 = 2 → 𝑁 ∈ ℙ) |
106 | | nnsum3primesprm 44776 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℙ →
∃𝑑 ∈ ℕ
∃𝑓 ∈ (ℙ
↑m (1...𝑑))(𝑑 ≤ 3 ∧ 𝑁 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) |
107 | 105, 106 | syl 17 |
. . . . . . . 8
⊢ (𝑁 = 2 → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ
↑m (1...𝑑))(𝑑 ≤ 3 ∧ 𝑁 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) |
108 | | 3prm 16135 |
. . . . . . . . . 10
⊢ 3 ∈
ℙ |
109 | | eleq1 2820 |
. . . . . . . . . 10
⊢ (𝑁 = 3 → (𝑁 ∈ ℙ ↔ 3 ∈
ℙ)) |
110 | 108, 109 | mpbiri 261 |
. . . . . . . . 9
⊢ (𝑁 = 3 → 𝑁 ∈ ℙ) |
111 | 110, 106 | syl 17 |
. . . . . . . 8
⊢ (𝑁 = 3 → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ
↑m (1...𝑑))(𝑑 ≤ 3 ∧ 𝑁 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) |
112 | 107, 111 | jaoi 856 |
. . . . . . 7
⊢ ((𝑁 = 2 ∨ 𝑁 = 3) → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑m
(1...𝑑))(𝑑 ≤ 3 ∧ 𝑁 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) |
113 | | nnsum3primes4 44774 |
. . . . . . . 8
⊢
∃𝑑 ∈
ℕ ∃𝑓 ∈
(ℙ ↑m (1...𝑑))(𝑑 ≤ 3 ∧ 4 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘)) |
114 | | eqeq1 2742 |
. . . . . . . . . 10
⊢ (𝑁 = 4 → (𝑁 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘) ↔ 4 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) |
115 | 114 | anbi2d 632 |
. . . . . . . . 9
⊢ (𝑁 = 4 → ((𝑑 ≤ 3 ∧ 𝑁 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘)) ↔ (𝑑 ≤ 3 ∧ 4 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘)))) |
116 | 115 | 2rexbidv 3210 |
. . . . . . . 8
⊢ (𝑁 = 4 → (∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ
↑m (1...𝑑))(𝑑 ≤ 3 ∧ 𝑁 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘)) ↔ ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑m
(1...𝑑))(𝑑 ≤ 3 ∧ 4 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘)))) |
117 | 113, 116 | mpbiri 261 |
. . . . . . 7
⊢ (𝑁 = 4 → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ
↑m (1...𝑑))(𝑑 ≤ 3 ∧ 𝑁 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) |
118 | 112, 117 | jaoi 856 |
. . . . . 6
⊢ (((𝑁 = 2 ∨ 𝑁 = 3) ∨ 𝑁 = 4) → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑m
(1...𝑑))(𝑑 ≤ 3 ∧ 𝑁 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) |
119 | | 5prm 16545 |
. . . . . . . 8
⊢ 5 ∈
ℙ |
120 | | eleq1 2820 |
. . . . . . . 8
⊢ (𝑁 = 5 → (𝑁 ∈ ℙ ↔ 5 ∈
ℙ)) |
121 | 119, 120 | mpbiri 261 |
. . . . . . 7
⊢ (𝑁 = 5 → 𝑁 ∈ ℙ) |
122 | 121, 106 | syl 17 |
. . . . . 6
⊢ (𝑁 = 5 → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ
↑m (1...𝑑))(𝑑 ≤ 3 ∧ 𝑁 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) |
123 | 118, 122 | jaoi 856 |
. . . . 5
⊢ ((((𝑁 = 2 ∨ 𝑁 = 3) ∨ 𝑁 = 4) ∨ 𝑁 = 5) → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑m
(1...𝑑))(𝑑 ≤ 3 ∧ 𝑁 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) |
124 | | 6gbe 44757 |
. . . . . . 7
⊢ 6 ∈
GoldbachEven |
125 | | eleq1 2820 |
. . . . . . 7
⊢ (𝑁 = 6 → (𝑁 ∈ GoldbachEven ↔ 6 ∈
GoldbachEven )) |
126 | 124, 125 | mpbiri 261 |
. . . . . 6
⊢ (𝑁 = 6 → 𝑁 ∈ GoldbachEven ) |
127 | | nnsum3primesgbe 44778 |
. . . . . 6
⊢ (𝑁 ∈ GoldbachEven →
∃𝑑 ∈ ℕ
∃𝑓 ∈ (ℙ
↑m (1...𝑑))(𝑑 ≤ 3 ∧ 𝑁 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) |
128 | 126, 127 | syl 17 |
. . . . 5
⊢ (𝑁 = 6 → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ
↑m (1...𝑑))(𝑑 ≤ 3 ∧ 𝑁 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) |
129 | 123, 128 | jaoi 856 |
. . . 4
⊢
(((((𝑁 = 2 ∨
𝑁 = 3) ∨ 𝑁 = 4) ∨ 𝑁 = 5) ∨ 𝑁 = 6) → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑m
(1...𝑑))(𝑑 ≤ 3 ∧ 𝑁 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) |
130 | | 7prm 16547 |
. . . . . 6
⊢ 7 ∈
ℙ |
131 | | eleq1 2820 |
. . . . . 6
⊢ (𝑁 = 7 → (𝑁 ∈ ℙ ↔ 7 ∈
ℙ)) |
132 | 130, 131 | mpbiri 261 |
. . . . 5
⊢ (𝑁 = 7 → 𝑁 ∈ ℙ) |
133 | 132, 106 | syl 17 |
. . . 4
⊢ (𝑁 = 7 → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ
↑m (1...𝑑))(𝑑 ≤ 3 ∧ 𝑁 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) |
134 | 129, 133 | jaoi 856 |
. . 3
⊢
((((((𝑁 = 2 ∨
𝑁 = 3) ∨ 𝑁 = 4) ∨ 𝑁 = 5) ∨ 𝑁 = 6) ∨ 𝑁 = 7) → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑m
(1...𝑑))(𝑑 ≤ 3 ∧ 𝑁 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) |
135 | | 8gbe 44759 |
. . . . 5
⊢ 8 ∈
GoldbachEven |
136 | | eleq1 2820 |
. . . . 5
⊢ (𝑁 = 8 → (𝑁 ∈ GoldbachEven ↔ 8 ∈
GoldbachEven )) |
137 | 135, 136 | mpbiri 261 |
. . . 4
⊢ (𝑁 = 8 → 𝑁 ∈ GoldbachEven ) |
138 | 137, 127 | syl 17 |
. . 3
⊢ (𝑁 = 8 → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ
↑m (1...𝑑))(𝑑 ≤ 3 ∧ 𝑁 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) |
139 | 134, 138 | jaoi 856 |
. 2
⊢
(((((((𝑁 = 2 ∨
𝑁 = 3) ∨ 𝑁 = 4) ∨ 𝑁 = 5) ∨ 𝑁 = 6) ∨ 𝑁 = 7) ∨ 𝑁 = 8) → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑m
(1...𝑑))(𝑑 ≤ 3 ∧ 𝑁 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) |
140 | 102, 139 | syl 17 |
1
⊢ ((𝑁 ∈
(ℤ≥‘2) ∧ 𝑁 ≤ 8) → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑m
(1...𝑑))(𝑑 ≤ 3 ∧ 𝑁 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) |