Metamath Proof Explorer

Theorem fzoss1

Description: Subset relationship for half-open sequences of integers. (Contributed by Stefan O'Rear, 15-Aug-2015) (Revised by Mario Carneiro, 29-Sep-2015)

Ref Expression
Assertion fzoss1 
|- ( K e. ( ZZ>= ` M ) -> ( K ..^ N ) C_ ( M ..^ N ) )

Proof

Step Hyp Ref Expression
1 sseq1 
 |-  ( ( K ..^ N ) = (/) -> ( ( K ..^ N ) C_ ( M ..^ N ) <-> (/) C_ ( M ..^ N ) ) )
2 fzon0 
 |-  ( ( K ..^ N ) =/= (/) <-> K e. ( K ..^ N ) )
3 elfzoel2 
 |-  ( K e. ( K ..^ N ) -> N e. ZZ )
4 2 3 sylbi 
 |-  ( ( K ..^ N ) =/= (/) -> N e. ZZ )
5 fzss1 
 |-  ( K e. ( ZZ>= ` M ) -> ( K ... ( N - 1 ) ) C_ ( M ... ( N - 1 ) ) )
6 5 adantr 
 |-  ( ( K e. ( ZZ>= ` M ) /\ N e. ZZ ) -> ( K ... ( N - 1 ) ) C_ ( M ... ( N - 1 ) ) )
7 fzoval 
 |-  ( N e. ZZ -> ( K ..^ N ) = ( K ... ( N - 1 ) ) )
8 7 adantl 
 |-  ( ( K e. ( ZZ>= ` M ) /\ N e. ZZ ) -> ( K ..^ N ) = ( K ... ( N - 1 ) ) )
9 fzoval 
 |-  ( N e. ZZ -> ( M ..^ N ) = ( M ... ( N - 1 ) ) )
10 9 adantl 
 |-  ( ( K e. ( ZZ>= ` M ) /\ N e. ZZ ) -> ( M ..^ N ) = ( M ... ( N - 1 ) ) )
11 6 8 10 3sstr4d 
 |-  ( ( K e. ( ZZ>= ` M ) /\ N e. ZZ ) -> ( K ..^ N ) C_ ( M ..^ N ) )
12 4 11 sylan2 
 |-  ( ( K e. ( ZZ>= ` M ) /\ ( K ..^ N ) =/= (/) ) -> ( K ..^ N ) C_ ( M ..^ N ) )
13 0ss 
 |-  (/) C_ ( M ..^ N )
14 13 a1i 
 |-  ( K e. ( ZZ>= ` M ) -> (/) C_ ( M ..^ N ) )
15 1 12 14 pm2.61ne 
 |-  ( K e. ( ZZ>= ` M ) -> ( K ..^ N ) C_ ( M ..^ N ) )