This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elfzr

Description: A member of a finite interval of integers is either a member of the corresponding half-open integer range or the upper bound of the interval. (Contributed by AV, 5-Feb-2021)

Ref Expression
Assertion elfzr 
|- ( K e. ( M ... N ) -> ( K e. ( M ..^ N ) \/ K = N ) )

Proof

Step Hyp Ref Expression
1 elfzuz2 
 |-  ( K e. ( M ... N ) -> N e. ( ZZ>= ` M ) )
2 fzisfzounsn 
 |-  ( N e. ( ZZ>= ` M ) -> ( M ... N ) = ( ( M ..^ N ) u. { N } ) )
3 2 eleq2d 
 |-  ( N e. ( ZZ>= ` M ) -> ( K e. ( M ... N ) <-> K e. ( ( M ..^ N ) u. { N } ) ) )
4 elun 
 |-  ( K e. ( ( M ..^ N ) u. { N } ) <-> ( K e. ( M ..^ N ) \/ K e. { N } ) )
5 elsni 
 |-  ( K e. { N } -> K = N )
6 5 orim2i 
 |-  ( ( K e. ( M ..^ N ) \/ K e. { N } ) -> ( K e. ( M ..^ N ) \/ K = N ) )
7 4 6 sylbi 
 |-  ( K e. ( ( M ..^ N ) u. { N } ) -> ( K e. ( M ..^ N ) \/ K = N ) )
8 3 7 biimtrdi 
 |-  ( N e. ( ZZ>= ` M ) -> ( K e. ( M ... N ) -> ( K e. ( M ..^ N ) \/ K = N ) ) )
9 1 8 mpcom 
 |-  ( K e. ( M ... N ) -> ( K e. ( M ..^ N ) \/ K = N ) )