Theorem elfzofz

Description: A half-open range is contained in the corresponding closed range. (Contributed by Stefan O'Rear, 23-Aug-2015)

	Ref	Expression
Assertion	elfzofz	⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝐾 ∈ ( 𝑀 ... 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		elfzouz	⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) )
2		elfzouz2	⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) )
3		elfzuzb	⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) )
4	1 2 3	sylanbrc	⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝐾 ∈ ( 𝑀 ... 𝑁 ) )