This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 biimtrdi ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐾 = 𝑀 ∨ 𝐾 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∨ 𝐾 = 𝑁 ) ) )
11 1 10 mpcom ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐾 = 𝑀 ∨ 𝐾 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∨ 𝐾 = 𝑁 ) )