This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem zltlem1

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

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

Proof

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