Metamath Proof Explorer

Theorem elfzolt2b

Description: A member in a half-open integer interval is less than the upper bound. (Contributed by Mario Carneiro, 29-Sep-2015)

Ref Expression
Assertion elfzolt2b 
|- ( K e. ( M ..^ N ) -> K e. ( K ..^ N ) )

Proof

Step Hyp Ref Expression
1 elfzoelz 
 |-  ( K e. ( M ..^ N ) -> K e. ZZ )
2 elfzoel2 
 |-  ( K e. ( M ..^ N ) -> N e. ZZ )
3 elfzolt2 
 |-  ( K e. ( M ..^ N ) -> K < N )
4 fzolb 
 |-  ( K e. ( K ..^ N ) <-> ( K e. ZZ /\ N e. ZZ /\ K < N ) )
5 1 2 3 4 syl3anbrc 
 |-  ( K e. ( M ..^ N ) -> K e. ( K ..^ N ) )