Theorem chpge0

Description: The second Chebyshev function is nonnegative. (Contributed by Mario Carneiro, 7-Apr-2016)

	Ref	Expression
Assertion	chpge0	$$⊢A\in ℝ\to 0\le \psi \left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		ef0	$$⊢{\mathrm{e}}^0=1$$
2		efchpcl	$$⊢A\in ℝ\to {\mathrm{e}}^{\psi \left(A\right)}\in \mathbb{N}$$
3	2	nnge1d	$$⊢A\in ℝ\to 1\le {\mathrm{e}}^{\psi \left(A\right)}$$
4	1 3	eqbrtrid	$$⊢A\in ℝ\to {\mathrm{e}}^0\le {\mathrm{e}}^{\psi \left(A\right)}$$
5		0re	$$⊢0\in ℝ$$
6		chpcl	$$⊢A\in ℝ\to \psi \left(A\right)\in ℝ$$
7		efle	$$⊢\left(0\in ℝ\wedge \psi \left(A\right)\in ℝ\right)\to \left(0\le \psi \left(A\right)\leftrightarrow {\mathrm{e}}^0\le {\mathrm{e}}^{\psi \left(A\right)}\right)$$
8	5 6 7	sylancr	$$⊢A\in ℝ\to \left(0\le \psi \left(A\right)\leftrightarrow {\mathrm{e}}^0\le {\mathrm{e}}^{\psi \left(A\right)}\right)$$
9	4 8	mpbird	$$⊢A\in ℝ\to 0\le \psi \left(A\right)$$