Metamath Proof Explorer


Theorem znn0sub

Description: The nonnegative difference of integers is a nonnegative integer. (Generalization of nn0sub .) (Contributed by NM, 14-Jul-2005)

Ref Expression
Assertion znn0sub M N M N N M 0

Proof

Step Hyp Ref Expression
1 zre N N
2 zre M M
3 subge0 N M 0 N M M N
4 1 2 3 syl2an N M 0 N M M N
5 zsubcl N M N M
6 5 biantrurd N M 0 N M N M 0 N M
7 4 6 bitr3d N M M N N M 0 N M
8 7 ancoms M N M N N M 0 N M
9 elnn0z N M 0 N M 0 N M
10 8 9 bitr4di M N M N N M 0