Theorem elfzouz

Description: Membership in a half-open integer interval. (Contributed by Mario Carneiro, 29-Sep-2015)

	Ref	Expression
Assertion	elfzouz	⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		elfzo2	⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ↔ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁 ) )
2	1	simp1bi	⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) )