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 e. ZZ /\ N e. ZZ ) -> ( M < N <-> ( M + 1 ) <_ N ) )

Proof

Step Hyp Ref Expression
1 nnge1 
 |-  ( ( N - M ) e. NN -> 1 <_ ( N - M ) )
2 1 a1i 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( N - M ) e. NN -> 1 <_ ( N - M ) ) )
3 znnsub 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M < N <-> ( N - M ) e. NN ) )
4 zre 
 |-  ( M e. ZZ -> M e. RR )
5 zre 
 |-  ( N e. ZZ -> N e. RR )
6 1re 
 |-  1 e. RR
7 leaddsub2 
 |-  ( ( M e. RR /\ 1 e. RR /\ N e. RR ) -> ( ( M + 1 ) <_ N <-> 1 <_ ( N - M ) ) )
8 6 7 mp3an2 
 |-  ( ( M e. RR /\ N e. RR ) -> ( ( M + 1 ) <_ N <-> 1 <_ ( N - M ) ) )
9 4 5 8 syl2an 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M + 1 ) <_ N <-> 1 <_ ( N - M ) ) )
10 2 3 9 3imtr4d 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M < N -> ( M + 1 ) <_ N ) )
11 4 adantr 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> M e. RR )
12 11 ltp1d 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> M < ( M + 1 ) )
13 peano2re 
 |-  ( M e. RR -> ( M + 1 ) e. RR )
14 11 13 syl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M + 1 ) e. RR )
15 5 adantl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> N e. RR )
16 ltletr 
 |-  ( ( M e. RR /\ ( M + 1 ) e. RR /\ N e. RR ) -> ( ( M < ( M + 1 ) /\ ( M + 1 ) <_ N ) -> M < N ) )
17 11 14 15 16 syl3anc 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M < ( M + 1 ) /\ ( M + 1 ) <_ N ) -> M < N ) )
18 12 17 mpand 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M + 1 ) <_ N -> M < N ) )
19 10 18 impbid 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M < N <-> ( M + 1 ) <_ N ) )