Metamath Proof Explorer


Theorem chpge0

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

Ref Expression
Assertion chpge0 A0ψA

Proof

Step Hyp Ref Expression
1 ef0 e0=1
2 efchpcl AeψA
3 2 nnge1d A1eψA
4 1 3 eqbrtrid Ae0eψA
5 0re 0
6 chpcl AψA
7 efle 0ψA0ψAe0eψA
8 5 6 7 sylancr A0ψAe0eψA
9 4 8 mpbird A0ψA