Metamath Proof Explorer


Theorem nn0leltp1

Description: Nonnegative integer ordering relation. (Contributed by Raph Levien, 10-Apr-2004)

Ref Expression
Assertion nn0leltp1 M 0 N 0 M N M < N + 1

Proof

Step Hyp Ref Expression
1 nn0z M 0 M
2 nn0z N 0 N
3 zleltp1 M N M N M < N + 1
4 1 2 3 syl2an M 0 N 0 M N M < N + 1