Theorem vmage0

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

	Ref	Expression
Assertion	vmage0	$$⊢A\in \mathbb{N}\to 0\le \Lambda \left(A\right)$$

Proof

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