Theorem elfzop1le2

Description: A member in a half-open integer interval plus 1 is less than or equal to the upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Assertion	elfzop1le2	|- ( K e. ( M ..^ N ) -> ( K + 1 ) <_ N )

Proof

Step	Hyp	Ref	Expression
1		elfzolt2	|- ( K e. ( M ..^ N ) -> K < N )
2		elfzoelz	|- ( K e. ( M ..^ N ) -> K e. ZZ )
3		elfzoel2	|- ( K e. ( M ..^ N ) -> N e. ZZ )
4		zltp1le	|- ( ( K e. ZZ /\ N e. ZZ ) -> ( K < N <-> ( K + 1 ) <_ N ) )
5	2 3 4	syl2anc	|- ( K e. ( M ..^ N ) -> ( K < N <-> ( K + 1 ) <_ N ) )
6	1 5	mpbid	|- ( K e. ( M ..^ N ) -> ( K + 1 ) <_ N )