Description: Implication of membership in a finite set of sequential integers. (Contributed by NM, 20-Sep-2005) (Revised by Mario Carneiro, 28-Apr-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | elfzuz2 | |- ( K e. ( M ... N ) -> N e. ( ZZ>= ` M ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elfzuzb | |- ( K e. ( M ... N ) <-> ( K e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) ) |
|
2 | eqid | |- ( ZZ>= ` M ) = ( ZZ>= ` M ) |
|
3 | 2 | uztrn2 | |- ( ( K e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) -> N e. ( ZZ>= ` M ) ) |
4 | 1 3 | sylbi | |- ( K e. ( M ... N ) -> N e. ( ZZ>= ` M ) ) |