Metamath Proof Explorer

Theorem elfzolt3b

Description: Membership in a half-open integer interval implies that the bounds are unequal. (Contributed by Mario Carneiro, 29-Sep-2015)

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

Proof

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