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