Step | Hyp | Ref
| Expression |
1 | | eleq1w 2842 |
. . . . 5
⊢ (𝑚 = 𝑘 → (𝑚 ∈ ℙ ↔ 𝑘 ∈ ℙ)) |
2 | | oveq2 6930 |
. . . . 5
⊢ (𝑚 = 𝑘 → (1 / 𝑚) = (1 / 𝑘)) |
3 | 1, 2 | ifbieq1d 4330 |
. . . 4
⊢ (𝑚 = 𝑘 → if(𝑚 ∈ ℙ, (1 / 𝑚), 0) = if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) |
4 | 3 | cbvmptv 4985 |
. . 3
⊢ (𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, (1 / 𝑚), 0)) = (𝑘 ∈ ℕ ↦ if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) |
5 | 4 | prmreclem6 16029 |
. 2
⊢ ¬
seq1( + , (𝑚 ∈ ℕ
↦ if(𝑚 ∈
ℙ, (1 / 𝑚), 0)))
∈ dom ⇝ |
6 | | inss2 4054 |
. . . . . . . . 9
⊢ (ℙ
∩ (1...𝑛)) ⊆
(1...𝑛) |
7 | | elinel2 4023 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (ℙ ∩
(1...𝑛)) → 𝑘 ∈ (1...𝑛)) |
8 | | elfznn 12687 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (1...𝑛) → 𝑘 ∈ ℕ) |
9 | | nnrecre 11417 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → (1 /
𝑘) ∈
ℝ) |
10 | 9 | recnd 10405 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → (1 /
𝑘) ∈
ℂ) |
11 | 7, 8, 10 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (ℙ ∩
(1...𝑛)) → (1 / 𝑘) ∈
ℂ) |
12 | 11 | rgen 3104 |
. . . . . . . . 9
⊢
∀𝑘 ∈
(ℙ ∩ (1...𝑛))(1 /
𝑘) ∈
ℂ |
13 | 6, 12 | pm3.2i 464 |
. . . . . . . 8
⊢ ((ℙ
∩ (1...𝑛)) ⊆
(1...𝑛) ∧ ∀𝑘 ∈ (ℙ ∩
(1...𝑛))(1 / 𝑘) ∈
ℂ) |
14 | | fzfi 13090 |
. . . . . . . . 9
⊢
(1...𝑛) ∈
Fin |
15 | 14 | olci 855 |
. . . . . . . 8
⊢
((1...𝑛) ⊆
(ℤ≥‘1) ∨ (1...𝑛) ∈ Fin) |
16 | | sumss2 14864 |
. . . . . . . 8
⊢
((((ℙ ∩ (1...𝑛)) ⊆ (1...𝑛) ∧ ∀𝑘 ∈ (ℙ ∩ (1...𝑛))(1 / 𝑘) ∈ ℂ) ∧ ((1...𝑛) ⊆
(ℤ≥‘1) ∨ (1...𝑛) ∈ Fin)) → Σ𝑘 ∈ (ℙ ∩
(1...𝑛))(1 / 𝑘) = Σ𝑘 ∈ (1...𝑛)if(𝑘 ∈ (ℙ ∩ (1...𝑛)), (1 / 𝑘), 0)) |
17 | 13, 15, 16 | mp2an 682 |
. . . . . . 7
⊢
Σ𝑘 ∈
(ℙ ∩ (1...𝑛))(1 /
𝑘) = Σ𝑘 ∈ (1...𝑛)if(𝑘 ∈ (ℙ ∩ (1...𝑛)), (1 / 𝑘), 0) |
18 | | elin 4019 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (ℙ ∩
(1...𝑛)) ↔ (𝑘 ∈ ℙ ∧ 𝑘 ∈ (1...𝑛))) |
19 | 18 | rbaib 534 |
. . . . . . . . 9
⊢ (𝑘 ∈ (1...𝑛) → (𝑘 ∈ (ℙ ∩ (1...𝑛)) ↔ 𝑘 ∈ ℙ)) |
20 | 19 | ifbid 4329 |
. . . . . . . 8
⊢ (𝑘 ∈ (1...𝑛) → if(𝑘 ∈ (ℙ ∩ (1...𝑛)), (1 / 𝑘), 0) = if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) |
21 | 20 | sumeq2i 14837 |
. . . . . . 7
⊢
Σ𝑘 ∈
(1...𝑛)if(𝑘 ∈ (ℙ ∩
(1...𝑛)), (1 / 𝑘), 0) = Σ𝑘 ∈ (1...𝑛)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) |
22 | 17, 21 | eqtri 2802 |
. . . . . 6
⊢
Σ𝑘 ∈
(ℙ ∩ (1...𝑛))(1 /
𝑘) = Σ𝑘 ∈ (1...𝑛)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) |
23 | 8 | adantl 475 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℕ) |
24 | | prmnn 15793 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℙ → 𝑘 ∈
ℕ) |
25 | 24, 10 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℙ → (1 /
𝑘) ∈
ℂ) |
26 | 25 | adantl 475 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑘
∈ ℙ) → (1 / 𝑘) ∈ ℂ) |
27 | | 0cnd 10369 |
. . . . . . . . . 10
⊢
((⊤ ∧ ¬ 𝑘 ∈ ℙ) → 0 ∈
ℂ) |
28 | 26, 27 | ifclda 4341 |
. . . . . . . . 9
⊢ (⊤
→ if(𝑘 ∈ ℙ,
(1 / 𝑘), 0) ∈
ℂ) |
29 | 28 | mptru 1609 |
. . . . . . . 8
⊢ if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈
ℂ |
30 | 4 | fvmpt2 6552 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℕ ∧ if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℂ) →
((𝑚 ∈ ℕ ↦
if(𝑚 ∈ ℙ, (1 /
𝑚), 0))‘𝑘) = if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) |
31 | 23, 29, 30 | sylancl 580 |
. . . . . . 7
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (1...𝑛)) → ((𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, (1 / 𝑚), 0))‘𝑘) = if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) |
32 | | id 22 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ) |
33 | | nnuz 12029 |
. . . . . . . 8
⊢ ℕ =
(ℤ≥‘1) |
34 | 32, 33 | syl6eleq 2869 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
(ℤ≥‘1)) |
35 | 29 | a1i 11 |
. . . . . . 7
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈ (1...𝑛)) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℂ) |
36 | 31, 34, 35 | fsumser 14868 |
. . . . . 6
⊢ (𝑛 ∈ ℕ →
Σ𝑘 ∈ (1...𝑛)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = (seq1( + , (𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, (1 / 𝑚), 0)))‘𝑛)) |
37 | 22, 36 | syl5eq 2826 |
. . . . 5
⊢ (𝑛 ∈ ℕ →
Σ𝑘 ∈ (ℙ
∩ (1...𝑛))(1 / 𝑘) = (seq1( + , (𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, (1 / 𝑚), 0)))‘𝑛)) |
38 | 37 | mpteq2ia 4975 |
. . . 4
⊢ (𝑛 ∈ ℕ ↦
Σ𝑘 ∈ (ℙ
∩ (1...𝑛))(1 / 𝑘)) = (𝑛 ∈ ℕ ↦ (seq1( + , (𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, (1 / 𝑚), 0)))‘𝑛)) |
39 | | prmrec.f |
. . . 4
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (ℙ ∩
(1...𝑛))(1 / 𝑘)) |
40 | | 1z 11759 |
. . . . . . 7
⊢ 1 ∈
ℤ |
41 | | seqfn 13131 |
. . . . . . 7
⊢ (1 ∈
ℤ → seq1( + , (𝑚
∈ ℕ ↦ if(𝑚
∈ ℙ, (1 / 𝑚),
0))) Fn (ℤ≥‘1)) |
42 | 40, 41 | ax-mp 5 |
. . . . . 6
⊢ seq1( + ,
(𝑚 ∈ ℕ ↦
if(𝑚 ∈ ℙ, (1 /
𝑚), 0))) Fn
(ℤ≥‘1) |
43 | 33 | fneq2i 6231 |
. . . . . 6
⊢ (seq1( +
, (𝑚 ∈ ℕ ↦
if(𝑚 ∈ ℙ, (1 /
𝑚), 0))) Fn ℕ ↔
seq1( + , (𝑚 ∈ ℕ
↦ if(𝑚 ∈
ℙ, (1 / 𝑚), 0))) Fn
(ℤ≥‘1)) |
44 | 42, 43 | mpbir 223 |
. . . . 5
⊢ seq1( + ,
(𝑚 ∈ ℕ ↦
if(𝑚 ∈ ℙ, (1 /
𝑚), 0))) Fn
ℕ |
45 | | dffn5 6501 |
. . . . 5
⊢ (seq1( +
, (𝑚 ∈ ℕ ↦
if(𝑚 ∈ ℙ, (1 /
𝑚), 0))) Fn ℕ ↔
seq1( + , (𝑚 ∈ ℕ
↦ if(𝑚 ∈
ℙ, (1 / 𝑚), 0))) =
(𝑛 ∈ ℕ ↦
(seq1( + , (𝑚 ∈
ℕ ↦ if(𝑚 ∈
ℙ, (1 / 𝑚),
0)))‘𝑛))) |
46 | 44, 45 | mpbi 222 |
. . . 4
⊢ seq1( + ,
(𝑚 ∈ ℕ ↦
if(𝑚 ∈ ℙ, (1 /
𝑚), 0))) = (𝑛 ∈ ℕ ↦ (seq1( +
, (𝑚 ∈ ℕ ↦
if(𝑚 ∈ ℙ, (1 /
𝑚), 0)))‘𝑛)) |
47 | 38, 39, 46 | 3eqtr4i 2812 |
. . 3
⊢ 𝐹 = seq1( + , (𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, (1 / 𝑚), 0))) |
48 | 47 | eleq1i 2850 |
. 2
⊢ (𝐹 ∈ dom ⇝ ↔ seq1(
+ , (𝑚 ∈ ℕ
↦ if(𝑚 ∈
ℙ, (1 / 𝑚), 0)))
∈ dom ⇝ ) |
49 | 5, 48 | mtbir 315 |
1
⊢ ¬
𝐹 ∈ dom
⇝ |