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

Metamath Proof Explorer

Theorem elfzolem1

Description: A member in a half-open integer interval is less than or equal to the upper bound minus 1 . (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Assertion elfzolem1 
|- ( K e. ( M ..^ N ) -> K <_ ( N - 1 ) )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( K e. ( M ..^ N ) -> K e. ( M ..^ N ) )
2 elfzoel2 
 |-  ( K e. ( M ..^ N ) -> N e. ZZ )
3 simpl 
 |-  ( ( K e. ( M ..^ N ) /\ N e. ZZ ) -> K e. ( M ..^ N ) )
4 fzoval 
 |-  ( N e. ZZ -> ( M ..^ N ) = ( M ... ( N - 1 ) ) )
5 4 adantl 
 |-  ( ( K e. ( M ..^ N ) /\ N e. ZZ ) -> ( M ..^ N ) = ( M ... ( N - 1 ) ) )
6 3 5 eleqtrd 
 |-  ( ( K e. ( M ..^ N ) /\ N e. ZZ ) -> K e. ( M ... ( N - 1 ) ) )
7 elfzle2 
 |-  ( K e. ( M ... ( N - 1 ) ) -> K <_ ( N - 1 ) )
8 6 7 syl 
 |-  ( ( K e. ( M ..^ N ) /\ N e. ZZ ) -> K <_ ( N - 1 ) )
9 1 2 8 syl2anc 
 |-  ( K e. ( M ..^ N ) -> K <_ ( N - 1 ) )