Step |
Hyp |
Ref |
Expression |
1 |
|
df-cht |
⊢ θ = ( 𝑥 ∈ ℝ ↦ Σ 𝑝 ∈ ( ( 0 [,] 𝑥 ) ∩ ℙ ) ( log ‘ 𝑝 ) ) |
2 |
|
ppifi |
⊢ ( 𝑥 ∈ ℝ → ( ( 0 [,] 𝑥 ) ∩ ℙ ) ∈ Fin ) |
3 |
|
simpr |
⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝑥 ) ∩ ℙ ) ) → 𝑝 ∈ ( ( 0 [,] 𝑥 ) ∩ ℙ ) ) |
4 |
3
|
elin2d |
⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝑥 ) ∩ ℙ ) ) → 𝑝 ∈ ℙ ) |
5 |
|
prmnn |
⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℕ ) |
6 |
4 5
|
syl |
⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝑥 ) ∩ ℙ ) ) → 𝑝 ∈ ℕ ) |
7 |
6
|
nnrpd |
⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝑥 ) ∩ ℙ ) ) → 𝑝 ∈ ℝ+ ) |
8 |
7
|
relogcld |
⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝑥 ) ∩ ℙ ) ) → ( log ‘ 𝑝 ) ∈ ℝ ) |
9 |
2 8
|
fsumrecl |
⊢ ( 𝑥 ∈ ℝ → Σ 𝑝 ∈ ( ( 0 [,] 𝑥 ) ∩ ℙ ) ( log ‘ 𝑝 ) ∈ ℝ ) |
10 |
1 9
|
fmpti |
⊢ θ : ℝ ⟶ ℝ |