Metamath Proof Explorer


Theorem uznn0sub

Description: The nonnegative difference of integers is a nonnegative integer. (Contributed by NM, 4-Sep-2005)

Ref Expression
Assertion uznn0sub N M N M 0

Proof

Step Hyp Ref Expression
1 eluz2 N M M N M N
2 znn0sub M N M N N M 0
3 2 biimp3a M N M N N M 0
4 1 3 sylbi N M N M 0