Metamath Proof Explorer

Theorem nnnle0

Description: A positive integer is not less than or equal to zero. (Contributed by AV, 13-May-2020)

Ref Expression
Assertion nnnle0 
|- ( A e. NN -> -. A <_ 0 )

Proof

Step Hyp Ref Expression
1 nngt0 
 |-  ( A e. NN -> 0 < A )
2 0re 
 |-  0 e. RR
3 nnre 
 |-  ( A e. NN -> A e. RR )
4 ltnle 
 |-  ( ( 0 e. RR /\ A e. RR ) -> ( 0 < A <-> -. A <_ 0 ) )
5 4 bicomd 
 |-  ( ( 0 e. RR /\ A e. RR ) -> ( -. A <_ 0 <-> 0 < A ) )
6 2 3 5 sylancr 
 |-  ( A e. NN -> ( -. A <_ 0 <-> 0 < A ) )
7 1 6 mpbird 
 |-  ( A e. NN -> -. A <_ 0 )