Metamath Proof Explorer


Theorem zltp1le

Description: Integer ordering relation. (Contributed by NM, 10-May-2004) (Proof shortened by Mario Carneiro, 16-May-2014)

Ref Expression
Assertion zltp1le M N M < N M + 1 N

Proof

Step Hyp Ref Expression
1 nnge1 N M 1 N M
2 1 a1i M N N M 1 N M
3 znnsub M N M < N N M
4 zre M M
5 zre N N
6 1re 1
7 leaddsub2 M 1 N M + 1 N 1 N M
8 6 7 mp3an2 M N M + 1 N 1 N M
9 4 5 8 syl2an M N M + 1 N 1 N M
10 2 3 9 3imtr4d M N M < N M + 1 N
11 4 adantr M N M
12 11 ltp1d M N M < M + 1
13 peano2re M M + 1
14 11 13 syl M N M + 1
15 5 adantl M N N
16 ltletr M M + 1 N M < M + 1 M + 1 N M < N
17 11 14 15 16 syl3anc M N M < M + 1 M + 1 N M < N
18 12 17 mpand M N M + 1 N M < N
19 10 18 impbid M N M < N M + 1 N