Description: A half-open range is contained in the corresponding closed range. (Contributed by Stefan O'Rear, 23-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | elfzofz | |- ( K e. ( M ..^ N ) -> K e. ( M ... N ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elfzouz | |- ( K e. ( M ..^ N ) -> K e. ( ZZ>= ` M ) ) |
|
2 | elfzouz2 | |- ( K e. ( M ..^ N ) -> N e. ( ZZ>= ` K ) ) |
|
3 | elfzuzb | |- ( K e. ( M ... N ) <-> ( K e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) ) |
|
4 | 1 2 3 | sylanbrc | |- ( K e. ( M ..^ N ) -> K e. ( M ... N ) ) |