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

Metamath Proof Explorer

Theorem elfzr

Description: A member of a finite interval of integers is either a member of the corresponding half-open integer range or the upper bound of the interval. (Contributed by AV, 5-Feb-2021)

Ref Expression
Assertion elfzr ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ∨ 𝐾 = 𝑁 ) )

Proof

Step Hyp Ref Expression
1 elfzuz2 ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
2 fzisfzounsn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 ... 𝑁 ) = ( ( 𝑀 ..^ 𝑁 ) ∪ { 𝑁 } ) )
3 2 eleq2d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ↔ 𝐾 ∈ ( ( 𝑀 ..^ 𝑁 ) ∪ { 𝑁 } ) ) )
4 elun ⊢ ( 𝐾 ∈ ( ( 𝑀 ..^ 𝑁 ) ∪ { 𝑁 } ) ↔ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ∨ 𝐾 ∈ { 𝑁 } ) )
5 elsni ⊢ ( 𝐾 ∈ { 𝑁 } → 𝐾 = 𝑁 )
6 5 orim2i ⊢ ( ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ∨ 𝐾 ∈ { 𝑁 } ) → ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ∨ 𝐾 = 𝑁 ) )
7 4 6 sylbi ⊢ ( 𝐾 ∈ ( ( 𝑀 ..^ 𝑁 ) ∪ { 𝑁 } ) → ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ∨ 𝐾 = 𝑁 ) )
8 3 7 biimtrdi ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ∨ 𝐾 = 𝑁 ) ) )
9 1 8 mpcom ⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ∨ 𝐾 = 𝑁 ) )