Metamath Proof Explorer


Theorem fzssfzo

Description: Condition for an integer interval to be a subset of a half-open integer interval. (Contributed by Thierry Arnoux, 8-Oct-2018)

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

Proof

Step Hyp Ref Expression
1 elfzoel2
 |-  ( K e. ( M ..^ N ) -> N e. ZZ )
2 fzoval
 |-  ( N e. ZZ -> ( M ..^ N ) = ( M ... ( N - 1 ) ) )
3 1 2 syl
 |-  ( K e. ( M ..^ N ) -> ( M ..^ N ) = ( M ... ( N - 1 ) ) )
4 3 eleq2d
 |-  ( K e. ( M ..^ N ) -> ( K e. ( M ..^ N ) <-> K e. ( M ... ( N - 1 ) ) ) )
5 4 ibi
 |-  ( K e. ( M ..^ N ) -> K e. ( M ... ( N - 1 ) ) )
6 elfzuz3
 |-  ( K e. ( M ... ( N - 1 ) ) -> ( N - 1 ) e. ( ZZ>= ` K ) )
7 fzss2
 |-  ( ( N - 1 ) e. ( ZZ>= ` K ) -> ( M ... K ) C_ ( M ... ( N - 1 ) ) )
8 5 6 7 3syl
 |-  ( K e. ( M ..^ N ) -> ( M ... K ) C_ ( M ... ( N - 1 ) ) )
9 8 3 sseqtrrd
 |-  ( K e. ( M ..^ N ) -> ( M ... K ) C_ ( M ..^ N ) )