chtf

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

		Ref	Expression
	Assertion	chtf	$⊢ θ : ℝ ⟶ ℝ$

Step	Hyp	Ref	Expression
1		df-cht	$⊢ θ = (x \in ℝ ⟼ \sum_{p \in [0, x] \cap ℙ} \log p)$
2		ppifi	$⊢ x \in ℝ \to [0, x] \cap ℙ \in Fin$
3		simpr	$⊢ (x \in ℝ \land p \in ([0, x] \cap ℙ)) \to p \in ([0, x] \cap ℙ)$
4	3	elin2d	$⊢ (x \in ℝ \land p \in ([0, x] \cap ℙ)) \to p \in ℙ$
5		prmnn	$⊢ p \in ℙ \to p \in ℕ$
6	4 5	syl	$⊢ (x \in ℝ \land p \in ([0, x] \cap ℙ)) \to p \in ℕ$
7	6	nnrpd	$⊢ (x \in ℝ \land p \in ([0, x] \cap ℙ)) \to p \in ℝ^{+}$
8	7	relogcld	$⊢ (x \in ℝ \land p \in ([0, x] \cap ℙ)) \to \log p \in ℝ$
9	2 8	fsumrecl	$⊢ x \in ℝ \to \sum_{p \in [0, x] \cap ℙ} \log p \in ℝ$
10	1 9	fmpti	$⊢ θ : ℝ ⟶ ℝ$

Metamath Proof Explorer