Metamath Proof Explorer

Theorem nn0le0eq0

Description: A nonnegative integer is less than or equal to zero iff it is equal to zero. (Contributed by NM, 9-Dec-2005)

Ref Expression
Assertion nn0le0eq0 
|- ( N e. NN0 -> ( N <_ 0 <-> N = 0 ) )

Proof

Step Hyp Ref Expression
1 nn0ge0 
 |-  ( N e. NN0 -> 0 <_ N )
2 1 biantrud 
 |-  ( N e. NN0 -> ( N <_ 0 <-> ( N <_ 0 /\ 0 <_ N ) ) )
3 nn0re 
 |-  ( N e. NN0 -> N e. RR )
4 0re 
 |-  0 e. RR
5 letri3 
 |-  ( ( N e. RR /\ 0 e. RR ) -> ( N = 0 <-> ( N <_ 0 /\ 0 <_ N ) ) )
6 3 4 5 sylancl 
 |-  ( N e. NN0 -> ( N = 0 <-> ( N <_ 0 /\ 0 <_ N ) ) )
7 2 6 bitr4d 
 |-  ( N e. NN0 -> ( N <_ 0 <-> N = 0 ) )