This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem chtf

Description: Domain and codoamin 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 ⊢ θ : ℝ ⟶ ℝ