Metamath Proof Explorer


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