Metamath Proof Explorer


Theorem elfzouz

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

Ref Expression
Assertion elfzouz
|- ( K e. ( M ..^ N ) -> K e. ( ZZ>= ` M ) )

Proof

Step Hyp Ref Expression
1 elfzo2
 |-  ( K e. ( M ..^ N ) <-> ( K e. ( ZZ>= ` M ) /\ N e. ZZ /\ K < N ) )
2 1 simp1bi
 |-  ( K e. ( M ..^ N ) -> K e. ( ZZ>= ` M ) )