Metamath Proof Explorer

Theorem zlem1lt

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

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

Proof

Step Hyp Ref Expression
1 peano2zm 
 |-  ( M e. ZZ -> ( M - 1 ) e. ZZ )
2 zltp1le 
 |-  ( ( ( M - 1 ) e. ZZ /\ N e. ZZ ) -> ( ( M - 1 ) < N <-> ( ( M - 1 ) + 1 ) <_ N ) )
3 1 2 sylan 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M - 1 ) < N <-> ( ( M - 1 ) + 1 ) <_ N ) )
4 zcn 
 |-  ( M e. ZZ -> M e. CC )
5 ax-1cn 
 |-  1 e. CC
6 npcan 
 |-  ( ( M e. CC /\ 1 e. CC ) -> ( ( M - 1 ) + 1 ) = M )
7 4 5 6 sylancl 
 |-  ( M e. ZZ -> ( ( M - 1 ) + 1 ) = M )
8 7 adantr 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M - 1 ) + 1 ) = M )
9 8 breq1d 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( ( M - 1 ) + 1 ) <_ N <-> M <_ N ) )
10 3 9 bitr2d 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M <_ N <-> ( M - 1 ) < N ) )