Theorem chpge0

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

	Ref	Expression
Assertion	chpge0	⊢ ( 𝐴 ∈ ℝ → 0 ≤ ( ψ ‘ 𝐴 ) )

Proof

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