Theorem elfzofz

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

Proof

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