Metamath Proof Explorer

Theorem zleltp1

Description: Integer ordering relation. (Contributed by NM, 10-May-2004)

Ref Expression
Assertion zleltp1 
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M <_ N <-> M < ( N + 1 ) ) )

Proof

Step Hyp Ref Expression
1 zre 
 |-  ( M e. ZZ -> M e. RR )
2 zre 
 |-  ( N e. ZZ -> N e. RR )
3 1re 
 |-  1 e. RR
4 leadd1 
 |-  ( ( M e. RR /\ N e. RR /\ 1 e. RR ) -> ( M <_ N <-> ( M + 1 ) <_ ( N + 1 ) ) )
5 3 4 mp3an3 
 |-  ( ( M e. RR /\ N e. RR ) -> ( M <_ N <-> ( M + 1 ) <_ ( N + 1 ) ) )
6 1 2 5 syl2an 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M <_ N <-> ( M + 1 ) <_ ( N + 1 ) ) )
7 peano2z 
 |-  ( N e. ZZ -> ( N + 1 ) e. ZZ )
8 zltp1le 
 |-  ( ( M e. ZZ /\ ( N + 1 ) e. ZZ ) -> ( M < ( N + 1 ) <-> ( M + 1 ) <_ ( N + 1 ) ) )
9 7 8 sylan2 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M < ( N + 1 ) <-> ( M + 1 ) <_ ( N + 1 ) ) )
10 6 9 bitr4d 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M <_ N <-> M < ( N + 1 ) ) )