Metamath Proof Explorer


Theorem nnleltp1

Description: Positive integer ordering relation. (Contributed by NM, 13-Aug-2001) (Proof shortened by Mario Carneiro, 16-May-2014)

Ref Expression
Assertion nnleltp1 ABABA<B+1

Proof

Step Hyp Ref Expression
1 nnz AA
2 nnz BB
3 zleltp1 ABABA<B+1
4 1 2 3 syl2an ABABA<B+1