Theorem vmage0

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

	Ref	Expression
Assertion	vmage0	⊢ ( 𝐴 ∈ ℕ → 0 ≤ ( Λ ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		ef0	⊢ ( exp ‘ 0 ) = 1
2		efvmacl	⊢ ( 𝐴 ∈ ℕ → ( exp ‘ ( Λ ‘ 𝐴 ) ) ∈ ℕ )
3	2	nnge1d	⊢ ( 𝐴 ∈ ℕ → 1 ≤ ( exp ‘ ( Λ ‘ 𝐴 ) ) )
4	1 3	eqbrtrid	⊢ ( 𝐴 ∈ ℕ → ( exp ‘ 0 ) ≤ ( exp ‘ ( Λ ‘ 𝐴 ) ) )
5		0re	⊢ 0 ∈ ℝ
6		vmacl	⊢ ( 𝐴 ∈ ℕ → ( Λ ‘ 𝐴 ) ∈ ℝ )
7		efle	⊢ ( ( 0 ∈ ℝ ∧ ( Λ ‘ 𝐴 ) ∈ ℝ ) → ( 0 ≤ ( Λ ‘ 𝐴 ) ↔ ( exp ‘ 0 ) ≤ ( exp ‘ ( Λ ‘ 𝐴 ) ) ) )
8	5 6 7	sylancr	⊢ ( 𝐴 ∈ ℕ → ( 0 ≤ ( Λ ‘ 𝐴 ) ↔ ( exp ‘ 0 ) ≤ ( exp ‘ ( Λ ‘ 𝐴 ) ) ) )
9	4 8	mpbird	⊢ ( 𝐴 ∈ ℕ → 0 ≤ ( Λ ‘ 𝐴 ) )