Metamath Proof Explorer

Theorem fzoss2

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 fzoss2 
|- ( N e. ( ZZ>= ` K ) -> ( M ..^ K ) C_ ( M ..^ N ) )

Proof

Step Hyp Ref Expression
1 eluzel2 
 |-  ( N e. ( ZZ>= ` K ) -> K e. ZZ )
2 peano2zm 
 |-  ( K e. ZZ -> ( K - 1 ) e. ZZ )
3 1 2 syl 
 |-  ( N e. ( ZZ>= ` K ) -> ( K - 1 ) e. ZZ )
4 1zzd 
 |-  ( N e. ( ZZ>= ` K ) -> 1 e. ZZ )
5 id 
 |-  ( N e. ( ZZ>= ` K ) -> N e. ( ZZ>= ` K ) )
6 1 zcnd 
 |-  ( N e. ( ZZ>= ` K ) -> K e. CC )
7 ax-1cn 
 |-  1 e. CC
8 npcan 
 |-  ( ( K e. CC /\ 1 e. CC ) -> ( ( K - 1 ) + 1 ) = K )
9 6 7 8 sylancl 
 |-  ( N e. ( ZZ>= ` K ) -> ( ( K - 1 ) + 1 ) = K )
10 9 fveq2d 
 |-  ( N e. ( ZZ>= ` K ) -> ( ZZ>= ` ( ( K - 1 ) + 1 ) ) = ( ZZ>= ` K ) )
11 5 10 eleqtrrd 
 |-  ( N e. ( ZZ>= ` K ) -> N e. ( ZZ>= ` ( ( K - 1 ) + 1 ) ) )
12 eluzsub 
 |-  ( ( ( K - 1 ) e. ZZ /\ 1 e. ZZ /\ N e. ( ZZ>= ` ( ( K - 1 ) + 1 ) ) ) -> ( N - 1 ) e. ( ZZ>= ` ( K - 1 ) ) )
13 3 4 11 12 syl3anc 
 |-  ( N e. ( ZZ>= ` K ) -> ( N - 1 ) e. ( ZZ>= ` ( K - 1 ) ) )
14 fzss2 
 |-  ( ( N - 1 ) e. ( ZZ>= ` ( K - 1 ) ) -> ( M ... ( K - 1 ) ) C_ ( M ... ( N - 1 ) ) )
15 13 14 syl 
 |-  ( N e. ( ZZ>= ` K ) -> ( M ... ( K - 1 ) ) C_ ( M ... ( N - 1 ) ) )
16 fzoval 
 |-  ( K e. ZZ -> ( M ..^ K ) = ( M ... ( K - 1 ) ) )
17 1 16 syl 
 |-  ( N e. ( ZZ>= ` K ) -> ( M ..^ K ) = ( M ... ( K - 1 ) ) )
18 eluzelz 
 |-  ( N e. ( ZZ>= ` K ) -> N e. ZZ )
19 fzoval 
 |-  ( N e. ZZ -> ( M ..^ N ) = ( M ... ( N - 1 ) ) )
20 18 19 syl 
 |-  ( N e. ( ZZ>= ` K ) -> ( M ..^ N ) = ( M ... ( N - 1 ) ) )
21 15 17 20 3sstr4d 
 |-  ( N e. ( ZZ>= ` K ) -> ( M ..^ K ) C_ ( M ..^ N ) )