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