Theorem zltlem1d

Description: Integer ordering relation, a deduction version. (Contributed by metakunt, 23-May-2024)

	Ref	Expression
Hypotheses	zltlem1d.1	|- ( ph -> M e. ZZ )
	zltlem1d.2	|- ( ph -> N e. ZZ )
Assertion	zltlem1d	|- ( ph -> ( M < N <-> M <_ ( N - 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		zltlem1d.1	|- ( ph -> M e. ZZ )
2		zltlem1d.2	|- ( ph -> N e. ZZ )
3		zltlem1	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M < N <-> M <_ ( N - 1 ) ) )
4	1 2 3	syl2anc	|- ( ph -> ( M < N <-> M <_ ( N - 1 ) ) )