chtge0

Description: The Chebyshev function is always positive. (Contributed by Mario Carneiro, 15-Sep-2014)

		Ref	Expression
	Assertion	chtge0	$⊢ A \in ℝ \to 0 \leq θ (A)$

Step	Hyp	Ref	Expression
1		ppifi	$⊢ A \in ℝ \to [0, A] \cap ℙ \in Fin$
2		simpr	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to p \in ([0, A] \cap ℙ)$
3	2	elin2d	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to p \in ℙ$
4		prmuz2	$⊢ p \in ℙ \to p \in ℤ_{\geq 2}$
5	3 4	syl	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to p \in ℤ_{\geq 2}$
6		eluz2b2	$⊢ p \in ℤ_{\geq 2} \leftrightarrow (p \in ℕ \land 1 < p)$
7	5 6	sylib	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to (p \in ℕ \land 1 < p)$
8	7	simpld	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to p \in ℕ$
9	8	nnrpd	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to p \in ℝ^{+}$
10	9	relogcld	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to \log p \in ℝ$
11	8	nnred	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to p \in ℝ$
12	7	simprd	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to 1 < p$
13	11 12	rplogcld	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to \log p \in ℝ^{+}$
14	13	rpge0d	$⊢ (A \in ℝ \land p \in ([0, A] \cap ℙ)) \to 0 \leq \log p$
15	1 10 14	fsumge0	$⊢ A \in ℝ \to 0 \leq \sum_{p \in [0, A] \cap ℙ} \log p$
16		chtval	$⊢ A \in ℝ \to θ (A) = \sum_{p \in [0, A] \cap ℙ} \log p$
17	15 16	breqtrrd	$⊢ A \in ℝ \to 0 \leq θ (A)$

Metamath Proof Explorer