Metamath Proof Explorer


Theorem zltlem1

Description: Integer ordering relation. (Contributed by NM, 13-Nov-2004)

Ref Expression
Assertion zltlem1 MNM<NMN1

Proof

Step Hyp Ref Expression
1 peano2zm NN1
2 zleltp1 MN1MN1M<N-1+1
3 1 2 sylan2 MNMN1M<N-1+1
4 zcn NN
5 ax-1cn 1
6 npcan N1N-1+1=N
7 4 5 6 sylancl NN-1+1=N
8 7 adantl MNN-1+1=N
9 8 breq2d MNM<N-1+1M<N
10 3 9 bitr2d MNM<NMN1