Metamath Proof Explorer


Theorem chtf

Description: Domain and range of the Chebyshev function. (Contributed by Mario Carneiro, 15-Sep-2014)

Ref Expression
Assertion chtf θ : ℝ ⟶ ℝ

Proof

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 θ : ℝ ⟶ ℝ