Theorem elfzlmr

Description: A member of a finite interval of integers is either its lower bound or its upper bound or an element of its interior. (Contributed by AV, 5-Feb-2021)

	Ref	Expression
Assertion	elfzlmr	|- ( K e. ( M ... N ) -> ( K = M \/ K e. ( ( M + 1 ) ..^ N ) \/ K = N ) )

Proof

Step	Hyp	Ref	Expression
1		elfzuz2	|- ( K e. ( M ... N ) -> N e. ( ZZ>= ` M ) )
2		fzpred	|- ( N e. ( ZZ>= ` M ) -> ( M ... N ) = ( { M } u. ( ( M + 1 ) ... N ) ) )
3	2	eleq2d	|- ( N e. ( ZZ>= ` M ) -> ( K e. ( M ... N ) <-> K e. ( { M } u. ( ( M + 1 ) ... N ) ) ) )
4		elsni	|- ( K e. { M } -> K = M )
5		elfzr	|- ( K e. ( ( M + 1 ) ... N ) -> ( K e. ( ( M + 1 ) ..^ N ) \/ K = N ) )
6	4 5	orim12i	|- ( ( K e. { M } \/ K e. ( ( M + 1 ) ... N ) ) -> ( K = M \/ ( K e. ( ( M + 1 ) ..^ N ) \/ K = N ) ) )
7		elun	|- ( K e. ( { M } u. ( ( M + 1 ) ... N ) ) <-> ( K e. { M } \/ K e. ( ( M + 1 ) ... N ) ) )
8		3orass	|- ( ( K = M \/ K e. ( ( M + 1 ) ..^ N ) \/ K = N ) <-> ( K = M \/ ( K e. ( ( M + 1 ) ..^ N ) \/ K = N ) ) )
9	6 7 8	3imtr4i	|- ( K e. ( { M } u. ( ( M + 1 ) ... N ) ) -> ( K = M \/ K e. ( ( M + 1 ) ..^ N ) \/ K = N ) )
10	3 9	biimtrdi	|- ( N e. ( ZZ>= ` M ) -> ( K e. ( M ... N ) -> ( K = M \/ K e. ( ( M + 1 ) ..^ N ) \/ K = N ) ) )
11	1 10	mpcom	|- ( K e. ( M ... N ) -> ( K = M \/ K e. ( ( M + 1 ) ..^ N ) \/ K = N ) )