Description: The von Mangoldt function is nonnegative. (Contributed by Mario Carneiro, 7-Apr-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | vmage0 | ⊢ ( 𝐴 ∈ ℕ → 0 ≤ ( Λ ‘ 𝐴 ) ) |
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 ≤ ( Λ ‘ 𝐴 ) ) |