Metamath Proof Explorer

Theorem vmage0

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

Ref Expression
Assertion vmage0 
|- ( A e. NN -> 0 <_ ( Lam ` A ) )

Proof

Step Hyp Ref Expression
1 ef0 
 |-  ( exp ` 0 ) = 1
2 efvmacl 
 |-  ( A e. NN -> ( exp ` ( Lam ` A ) ) e. NN )
3 2 nnge1d 
 |-  ( A e. NN -> 1 <_ ( exp ` ( Lam ` A ) ) )
4 1 3 eqbrtrid 
 |-  ( A e. NN -> ( exp ` 0 ) <_ ( exp ` ( Lam ` A ) ) )
5 0re 
 |-  0 e. RR
6 vmacl 
 |-  ( A e. NN -> ( Lam ` A ) e. RR )
7 efle 
 |-  ( ( 0 e. RR /\ ( Lam ` A ) e. RR ) -> ( 0 <_ ( Lam ` A ) <-> ( exp ` 0 ) <_ ( exp ` ( Lam ` A ) ) ) )
8 5 6 7 sylancr 
 |-  ( A e. NN -> ( 0 <_ ( Lam ` A ) <-> ( exp ` 0 ) <_ ( exp ` ( Lam ` A ) ) ) )
9 4 8 mpbird 
 |-  ( A e. NN -> 0 <_ ( Lam ` A ) )