Metamath Proof Explorer


Theorem znnsub

Description: The positive difference of unequal integers is a positive integer. (Generalization of nnsub .) (Contributed by NM, 11-May-2004)

Ref Expression
Assertion znnsub M N M < N N M

Proof

Step Hyp Ref Expression
1 zre M M
2 zre N N
3 posdif M N M < N 0 < N M
4 1 2 3 syl2an M N M < N 0 < N M
5 zsubcl N M N M
6 5 ancoms M N N M
7 6 biantrurd M N 0 < N M N M 0 < N M
8 4 7 bitrd M N M < N N M 0 < N M
9 elnnz N M N M 0 < N M
10 8 9 bitr4di M N M < N N M