Metamath Proof Explorer


Theorem nn0leltp1

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

Ref Expression
Assertion nn0leltp1 M0N0MNM<N+1

Proof

Step Hyp Ref Expression
1 nn0z M0M
2 nn0z N0N
3 zleltp1 MNMNM<N+1
4 1 2 3 syl2an M0N0MNM<N+1