Metamath Proof Explorer


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 ≤ ( Λ ‘ 𝐴 ) )