Theorem chtf

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

	Ref	Expression
Assertion	chtf	$$⊢\theta :ℝ⟶ℝ$$

Proof

Step	Hyp	Ref	Expression
1		df-cht	$$⊢\theta =\left(x\in ℝ⟼\sum _{p\in \left[0,x\right]\cap \mathbb{P}}\log p\right)$$
2		ppifi	$$⊢x\in ℝ\to \left[0,x\right]\cap \mathbb{P}\in \mathrm{Fin}$$
3		simpr	$$⊢\left(x\in ℝ\wedge p\in \left(\left[0,x\right]\cap \mathbb{P}\right)\right)\to p\in \left(\left[0,x\right]\cap \mathbb{P}\right)$$
4	3	elin2d	$$⊢\left(x\in ℝ\wedge p\in \left(\left[0,x\right]\cap \mathbb{P}\right)\right)\to p\in \mathbb{P}$$
5		prmnn	$$⊢p\in \mathbb{P}\to p\in \mathbb{N}$$
6	4 5	syl	$$⊢\left(x\in ℝ\wedge p\in \left(\left[0,x\right]\cap \mathbb{P}\right)\right)\to p\in \mathbb{N}$$
7	6	nnrpd	$$⊢\left(x\in ℝ\wedge p\in \left(\left[0,x\right]\cap \mathbb{P}\right)\right)\to p\in {ℝ}^{+}$$
8	7	relogcld	$$⊢\left(x\in ℝ\wedge p\in \left(\left[0,x\right]\cap \mathbb{P}\right)\right)\to \log p\in ℝ$$
9	2 8	fsumrecl	$$⊢x\in ℝ\to \sum _{p\in \left[0,x\right]\cap \mathbb{P}}\log p\in ℝ$$
10	1 9	fmpti	$$⊢\theta :ℝ⟶ℝ$$