| Step | Hyp | Ref
| Expression |
| 1 | | nnre 12273 |
. . . . . . 7
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℝ) |
| 2 | | chtval 27153 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(θ‘𝐴) =
Σ𝑘 ∈ ((0[,]𝐴) ∩ ℙ)(log‘𝑘)) |
| 3 | 1, 2 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ ℕ →
(θ‘𝐴) =
Σ𝑘 ∈ ((0[,]𝐴) ∩ ℙ)(log‘𝑘)) |
| 4 | | 2eluzge1 12936 |
. . . . . . . . . 10
⊢ 2 ∈
(ℤ≥‘1) |
| 5 | | ppisval2 27148 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 2 ∈
(ℤ≥‘1)) → ((0[,]𝐴) ∩ ℙ) =
((1...(⌊‘𝐴))
∩ ℙ)) |
| 6 | 1, 4, 5 | sylancl 586 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℕ →
((0[,]𝐴) ∩ ℙ) =
((1...(⌊‘𝐴))
∩ ℙ)) |
| 7 | | nnz 12634 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℤ) |
| 8 | | flid 13848 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℤ →
(⌊‘𝐴) = 𝐴) |
| 9 | 7, 8 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℕ →
(⌊‘𝐴) = 𝐴) |
| 10 | 9 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℕ →
(1...(⌊‘𝐴)) =
(1...𝐴)) |
| 11 | 10 | ineq1d 4219 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℕ →
((1...(⌊‘𝐴))
∩ ℙ) = ((1...𝐴)
∩ ℙ)) |
| 12 | 6, 11 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝐴 ∈ ℕ →
((0[,]𝐴) ∩ ℙ) =
((1...𝐴) ∩
ℙ)) |
| 13 | 12 | sumeq1d 15736 |
. . . . . . 7
⊢ (𝐴 ∈ ℕ →
Σ𝑘 ∈ ((0[,]𝐴) ∩ ℙ)(log‘𝑘) = Σ𝑘 ∈ ((1...𝐴) ∩ ℙ)(log‘𝑘)) |
| 14 | | inss1 4237 |
. . . . . . . 8
⊢
((1...𝐴) ∩
ℙ) ⊆ (1...𝐴) |
| 15 | | elinel1 4201 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ((1...𝐴) ∩ ℙ) → 𝑘 ∈ (1...𝐴)) |
| 16 | | elfznn 13593 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (1...𝐴) → 𝑘 ∈ ℕ) |
| 17 | 16 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℕ ∧ 𝑘 ∈ (1...𝐴)) → 𝑘 ∈ ℕ) |
| 18 | 17 | nnrpd 13075 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℕ ∧ 𝑘 ∈ (1...𝐴)) → 𝑘 ∈ ℝ+) |
| 19 | 18 | relogcld 26665 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ ∧ 𝑘 ∈ (1...𝐴)) → (log‘𝑘) ∈ ℝ) |
| 20 | 19 | recnd 11289 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑘 ∈ (1...𝐴)) → (log‘𝑘) ∈ ℂ) |
| 21 | 15, 20 | sylan2 593 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝑘 ∈ ((1...𝐴) ∩ ℙ)) → (log‘𝑘) ∈
ℂ) |
| 22 | 21 | ralrimiva 3146 |
. . . . . . . 8
⊢ (𝐴 ∈ ℕ →
∀𝑘 ∈
((1...𝐴) ∩
ℙ)(log‘𝑘)
∈ ℂ) |
| 23 | | fzfi 14013 |
. . . . . . . . . 10
⊢
(1...𝐴) ∈
Fin |
| 24 | 23 | olci 867 |
. . . . . . . . 9
⊢
((1...𝐴) ⊆
(ℤ≥‘1) ∨ (1...𝐴) ∈ Fin) |
| 25 | | sumss2 15762 |
. . . . . . . . 9
⊢
(((((1...𝐴) ∩
ℙ) ⊆ (1...𝐴)
∧ ∀𝑘 ∈
((1...𝐴) ∩
ℙ)(log‘𝑘)
∈ ℂ) ∧ ((1...𝐴) ⊆ (ℤ≥‘1)
∨ (1...𝐴) ∈ Fin))
→ Σ𝑘 ∈
((1...𝐴) ∩
ℙ)(log‘𝑘) =
Σ𝑘 ∈ (1...𝐴)if(𝑘 ∈ ((1...𝐴) ∩ ℙ), (log‘𝑘), 0)) |
| 26 | 24, 25 | mpan2 691 |
. . . . . . . 8
⊢
((((1...𝐴) ∩
ℙ) ⊆ (1...𝐴)
∧ ∀𝑘 ∈
((1...𝐴) ∩
ℙ)(log‘𝑘)
∈ ℂ) → Σ𝑘 ∈ ((1...𝐴) ∩ ℙ)(log‘𝑘) = Σ𝑘 ∈ (1...𝐴)if(𝑘 ∈ ((1...𝐴) ∩ ℙ), (log‘𝑘), 0)) |
| 27 | 14, 22, 26 | sylancr 587 |
. . . . . . 7
⊢ (𝐴 ∈ ℕ →
Σ𝑘 ∈ ((1...𝐴) ∩ ℙ)(log‘𝑘) = Σ𝑘 ∈ (1...𝐴)if(𝑘 ∈ ((1...𝐴) ∩ ℙ), (log‘𝑘), 0)) |
| 28 | 13, 27 | eqtrd 2777 |
. . . . . 6
⊢ (𝐴 ∈ ℕ →
Σ𝑘 ∈ ((0[,]𝐴) ∩ ℙ)(log‘𝑘) = Σ𝑘 ∈ (1...𝐴)if(𝑘 ∈ ((1...𝐴) ∩ ℙ), (log‘𝑘), 0)) |
| 29 | 3, 28 | eqtrd 2777 |
. . . . 5
⊢ (𝐴 ∈ ℕ →
(θ‘𝐴) =
Σ𝑘 ∈ (1...𝐴)if(𝑘 ∈ ((1...𝐴) ∩ ℙ), (log‘𝑘), 0)) |
| 30 | | elin 3967 |
. . . . . . . 8
⊢ (𝑘 ∈ ((1...𝐴) ∩ ℙ) ↔ (𝑘 ∈ (1...𝐴) ∧ 𝑘 ∈ ℙ)) |
| 31 | 30 | baibr 536 |
. . . . . . 7
⊢ (𝑘 ∈ (1...𝐴) → (𝑘 ∈ ℙ ↔ 𝑘 ∈ ((1...𝐴) ∩ ℙ))) |
| 32 | 31 | ifbid 4549 |
. . . . . 6
⊢ (𝑘 ∈ (1...𝐴) → if(𝑘 ∈ ℙ, (log‘𝑘), 0) = if(𝑘 ∈ ((1...𝐴) ∩ ℙ), (log‘𝑘), 0)) |
| 33 | 32 | sumeq2i 15734 |
. . . . 5
⊢
Σ𝑘 ∈
(1...𝐴)if(𝑘 ∈ ℙ,
(log‘𝑘), 0) =
Σ𝑘 ∈ (1...𝐴)if(𝑘 ∈ ((1...𝐴) ∩ ℙ), (log‘𝑘), 0) |
| 34 | 29, 33 | eqtr4di 2795 |
. . . 4
⊢ (𝐴 ∈ ℕ →
(θ‘𝐴) =
Σ𝑘 ∈ (1...𝐴)if(𝑘 ∈ ℙ, (log‘𝑘), 0)) |
| 35 | | eleq1w 2824 |
. . . . . . . 8
⊢ (𝑛 = 𝑘 → (𝑛 ∈ ℙ ↔ 𝑘 ∈ ℙ)) |
| 36 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑛 = 𝑘 → (log‘𝑛) = (log‘𝑘)) |
| 37 | 35, 36 | ifbieq1d 4550 |
. . . . . . 7
⊢ (𝑛 = 𝑘 → if(𝑛 ∈ ℙ, (log‘𝑛), 0) = if(𝑘 ∈ ℙ, (log‘𝑘), 0)) |
| 38 | | eqid 2737 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ,
(log‘𝑛), 0)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ,
(log‘𝑛),
0)) |
| 39 | | fvex 6919 |
. . . . . . . 8
⊢
(log‘𝑘) ∈
V |
| 40 | | 0cn 11253 |
. . . . . . . . 9
⊢ 0 ∈
ℂ |
| 41 | 40 | elexi 3503 |
. . . . . . . 8
⊢ 0 ∈
V |
| 42 | 39, 41 | ifex 4576 |
. . . . . . 7
⊢ if(𝑘 ∈ ℙ,
(log‘𝑘), 0) ∈
V |
| 43 | 37, 38, 42 | fvmpt 7016 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ,
(log‘𝑛),
0))‘𝑘) = if(𝑘 ∈ ℙ,
(log‘𝑘),
0)) |
| 44 | 17, 43 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑘 ∈ (1...𝐴)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (log‘𝑛), 0))‘𝑘) = if(𝑘 ∈ ℙ, (log‘𝑘), 0)) |
| 45 | | elnnuz 12922 |
. . . . . 6
⊢ (𝐴 ∈ ℕ ↔ 𝐴 ∈
(ℤ≥‘1)) |
| 46 | 45 | biimpi 216 |
. . . . 5
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
(ℤ≥‘1)) |
| 47 | | ifcl 4571 |
. . . . . 6
⊢
(((log‘𝑘)
∈ ℂ ∧ 0 ∈ ℂ) → if(𝑘 ∈ ℙ, (log‘𝑘), 0) ∈
ℂ) |
| 48 | 20, 40, 47 | sylancl 586 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑘 ∈ (1...𝐴)) → if(𝑘 ∈ ℙ, (log‘𝑘), 0) ∈
ℂ) |
| 49 | 44, 46, 48 | fsumser 15766 |
. . . 4
⊢ (𝐴 ∈ ℕ →
Σ𝑘 ∈ (1...𝐴)if(𝑘 ∈ ℙ, (log‘𝑘), 0) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ,
(log‘𝑛),
0)))‘𝐴)) |
| 50 | 34, 49 | eqtrd 2777 |
. . 3
⊢ (𝐴 ∈ ℕ →
(θ‘𝐴) = (seq1(
+ , (𝑛 ∈ ℕ
↦ if(𝑛 ∈
ℙ, (log‘𝑛),
0)))‘𝐴)) |
| 51 | 50 | fveq2d 6910 |
. 2
⊢ (𝐴 ∈ ℕ →
(exp‘(θ‘𝐴)) = (exp‘(seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ,
(log‘𝑛),
0)))‘𝐴))) |
| 52 | | addcl 11237 |
. . . 4
⊢ ((𝑘 ∈ ℂ ∧ 𝑝 ∈ ℂ) → (𝑘 + 𝑝) ∈ ℂ) |
| 53 | 52 | adantl 481 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ (𝑘 ∈ ℂ ∧ 𝑝 ∈ ℂ)) → (𝑘 + 𝑝) ∈ ℂ) |
| 54 | 44, 48 | eqeltrd 2841 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝑘 ∈ (1...𝐴)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (log‘𝑛), 0))‘𝑘) ∈ ℂ) |
| 55 | | efadd 16130 |
. . . 4
⊢ ((𝑘 ∈ ℂ ∧ 𝑝 ∈ ℂ) →
(exp‘(𝑘 + 𝑝)) = ((exp‘𝑘) · (exp‘𝑝))) |
| 56 | 55 | adantl 481 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ (𝑘 ∈ ℂ ∧ 𝑝 ∈ ℂ)) →
(exp‘(𝑘 + 𝑝)) = ((exp‘𝑘) · (exp‘𝑝))) |
| 57 | | 1nn 12277 |
. . . . . . 7
⊢ 1 ∈
ℕ |
| 58 | | ifcl 4571 |
. . . . . . 7
⊢ ((𝑘 ∈ ℕ ∧ 1 ∈
ℕ) → if(𝑘 ∈
ℙ, 𝑘, 1) ∈
ℕ) |
| 59 | 17, 57, 58 | sylancl 586 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝑘 ∈ (1...𝐴)) → if(𝑘 ∈ ℙ, 𝑘, 1) ∈ ℕ) |
| 60 | 59 | nnrpd 13075 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑘 ∈ (1...𝐴)) → if(𝑘 ∈ ℙ, 𝑘, 1) ∈
ℝ+) |
| 61 | 60 | reeflogd 26666 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝑘 ∈ (1...𝐴)) → (exp‘(log‘if(𝑘 ∈ ℙ, 𝑘, 1))) = if(𝑘 ∈ ℙ, 𝑘, 1)) |
| 62 | | fvif 6922 |
. . . . . . 7
⊢
(log‘if(𝑘
∈ ℙ, 𝑘, 1)) =
if(𝑘 ∈ ℙ,
(log‘𝑘),
(log‘1)) |
| 63 | | log1 26627 |
. . . . . . . 8
⊢
(log‘1) = 0 |
| 64 | | ifeq2 4530 |
. . . . . . . 8
⊢
((log‘1) = 0 → if(𝑘 ∈ ℙ, (log‘𝑘), (log‘1)) = if(𝑘 ∈ ℙ,
(log‘𝑘),
0)) |
| 65 | 63, 64 | ax-mp 5 |
. . . . . . 7
⊢ if(𝑘 ∈ ℙ,
(log‘𝑘),
(log‘1)) = if(𝑘
∈ ℙ, (log‘𝑘), 0) |
| 66 | 62, 65 | eqtri 2765 |
. . . . . 6
⊢
(log‘if(𝑘
∈ ℙ, 𝑘, 1)) =
if(𝑘 ∈ ℙ,
(log‘𝑘),
0) |
| 67 | 44, 66 | eqtr4di 2795 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑘 ∈ (1...𝐴)) → ((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (log‘𝑛), 0))‘𝑘) = (log‘if(𝑘 ∈ ℙ, 𝑘, 1))) |
| 68 | 67 | fveq2d 6910 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝑘 ∈ (1...𝐴)) → (exp‘((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (log‘𝑛), 0))‘𝑘)) = (exp‘(log‘if(𝑘 ∈ ℙ, 𝑘, 1)))) |
| 69 | | id 22 |
. . . . . . 7
⊢ (𝑛 = 𝑘 → 𝑛 = 𝑘) |
| 70 | 35, 69 | ifbieq1d 4550 |
. . . . . 6
⊢ (𝑛 = 𝑘 → if(𝑛 ∈ ℙ, 𝑛, 1) = if(𝑘 ∈ ℙ, 𝑘, 1)) |
| 71 | | prmorcht.1 |
. . . . . 6
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)) |
| 72 | | vex 3484 |
. . . . . . 7
⊢ 𝑘 ∈ V |
| 73 | 57 | elexi 3503 |
. . . . . . 7
⊢ 1 ∈
V |
| 74 | 72, 73 | ifex 4576 |
. . . . . 6
⊢ if(𝑘 ∈ ℙ, 𝑘, 1) ∈ V |
| 75 | 70, 71, 74 | fvmpt 7016 |
. . . . 5
⊢ (𝑘 ∈ ℕ → (𝐹‘𝑘) = if(𝑘 ∈ ℙ, 𝑘, 1)) |
| 76 | 17, 75 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝑘 ∈ (1...𝐴)) → (𝐹‘𝑘) = if(𝑘 ∈ ℙ, 𝑘, 1)) |
| 77 | 61, 68, 76 | 3eqtr4d 2787 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝑘 ∈ (1...𝐴)) → (exp‘((𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (log‘𝑛), 0))‘𝑘)) = (𝐹‘𝑘)) |
| 78 | 53, 54, 46, 56, 77 | seqhomo 14090 |
. 2
⊢ (𝐴 ∈ ℕ →
(exp‘(seq1( + , (𝑛
∈ ℕ ↦ if(𝑛
∈ ℙ, (log‘𝑛), 0)))‘𝐴)) = (seq1( · , 𝐹)‘𝐴)) |
| 79 | 51, 78 | eqtrd 2777 |
1
⊢ (𝐴 ∈ ℕ →
(exp‘(θ‘𝐴)) = (seq1( · , 𝐹)‘𝐴)) |