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	⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐾 = 𝑀 ∨ 𝐾 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∨ 𝐾 = 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		elfzuz2	⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
2		fzpred	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 ... 𝑁 ) = ( { 𝑀 } ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
3	2	eleq2d	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ↔ 𝐾 ∈ ( { 𝑀 } ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ) )
4		elsni	⊢ ( 𝐾 ∈ { 𝑀 } → 𝐾 = 𝑀 )
5		elfzr	⊢ ( 𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) → ( 𝐾 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∨ 𝐾 = 𝑁 ) )
6	4 5	orim12i	⊢ ( ( 𝐾 ∈ { 𝑀 } ∨ 𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → ( 𝐾 = 𝑀 ∨ ( 𝐾 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∨ 𝐾 = 𝑁 ) ) )
7		elun	⊢ ( 𝐾 ∈ ( { 𝑀 } ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) ↔ ( 𝐾 ∈ { 𝑀 } ∨ 𝐾 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) )
8		3orass	⊢ ( ( 𝐾 = 𝑀 ∨ 𝐾 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∨ 𝐾 = 𝑁 ) ↔ ( 𝐾 = 𝑀 ∨ ( 𝐾 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∨ 𝐾 = 𝑁 ) ) )
9	6 7 8	3imtr4i	⊢ ( 𝐾 ∈ ( { 𝑀 } ∪ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → ( 𝐾 = 𝑀 ∨ 𝐾 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∨ 𝐾 = 𝑁 ) )
10	3 9	syl6bi	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐾 = 𝑀 ∨ 𝐾 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∨ 𝐾 = 𝑁 ) ) )
11	1 10	mpcom	⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐾 = 𝑀 ∨ 𝐾 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∨ 𝐾 = 𝑁 ) )