Theorem zltp1led

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

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

Proof

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