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 ) )