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