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 ) ) )