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 N0N0N=0

Proof

Step Hyp Ref Expression
1 nn0ge0 N00N
2 1 biantrud N0N0N00N
3 nn0re N0N
4 0re 0
5 letri3 N0N=0N00N
6 3 4 5 sylancl N0N=0N00N
7 2 6 bitr4d N0N0N=0