Metamath Proof Explorer

Theorem fzspl

Description: Split the last element of a finite set of sequential integers. More generic than fzsuc . (Contributed by Thierry Arnoux, 7-Nov-2016)

Ref Expression
Assertion fzspl 
|- ( N e. ( ZZ>= ` M ) -> ( M ... N ) = ( ( M ... ( N - 1 ) ) u. { N } ) )

Proof

Step Hyp Ref Expression
1 eluzelz 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )
2 1 zcnd 
 |-  ( N e. ( ZZ>= ` M ) -> N e. CC )
3 1zzd 
 |-  ( N e. ( ZZ>= ` M ) -> 1 e. ZZ )
4 3 zcnd 
 |-  ( N e. ( ZZ>= ` M ) -> 1 e. CC )
5 2 4 npcand 
 |-  ( N e. ( ZZ>= ` M ) -> ( ( N - 1 ) + 1 ) = N )
6 5 eleq1d 
 |-  ( N e. ( ZZ>= ` M ) -> ( ( ( N - 1 ) + 1 ) e. ( ZZ>= ` M ) <-> N e. ( ZZ>= ` M ) ) )
7 6 ibir 
 |-  ( N e. ( ZZ>= ` M ) -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` M ) )
8 eluzelre 
 |-  ( N e. ( ZZ>= ` M ) -> N e. RR )
9 8 lem1d 
 |-  ( N e. ( ZZ>= ` M ) -> ( N - 1 ) <_ N )
10 1 3 zsubcld 
 |-  ( N e. ( ZZ>= ` M ) -> ( N - 1 ) e. ZZ )
11 eluz1 
 |-  ( ( N - 1 ) e. ZZ -> ( N e. ( ZZ>= ` ( N - 1 ) ) <-> ( N e. ZZ /\ ( N - 1 ) <_ N ) ) )
12 10 11 syl 
 |-  ( N e. ( ZZ>= ` M ) -> ( N e. ( ZZ>= ` ( N - 1 ) ) <-> ( N e. ZZ /\ ( N - 1 ) <_ N ) ) )
13 1 9 12 mpbir2and 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ( ZZ>= ` ( N - 1 ) ) )
14 fzsplit2 
 |-  ( ( ( ( N - 1 ) + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` ( N - 1 ) ) ) -> ( M ... N ) = ( ( M ... ( N - 1 ) ) u. ( ( ( N - 1 ) + 1 ) ... N ) ) )
15 7 13 14 syl2anc 
 |-  ( N e. ( ZZ>= ` M ) -> ( M ... N ) = ( ( M ... ( N - 1 ) ) u. ( ( ( N - 1 ) + 1 ) ... N ) ) )
16 5 oveq1d 
 |-  ( N e. ( ZZ>= ` M ) -> ( ( ( N - 1 ) + 1 ) ... N ) = ( N ... N ) )
17 fzsn 
 |-  ( N e. ZZ -> ( N ... N ) = { N } )
18 1 17 syl 
 |-  ( N e. ( ZZ>= ` M ) -> ( N ... N ) = { N } )
19 16 18 eqtrd 
 |-  ( N e. ( ZZ>= ` M ) -> ( ( ( N - 1 ) + 1 ) ... N ) = { N } )
20 19 uneq2d 
 |-  ( N e. ( ZZ>= ` M ) -> ( ( M ... ( N - 1 ) ) u. ( ( ( N - 1 ) + 1 ) ... N ) ) = ( ( M ... ( N - 1 ) ) u. { N } ) )
21 15 20 eqtrd 
 |-  ( N e. ( ZZ>= ` M ) -> ( M ... N ) = ( ( M ... ( N - 1 ) ) u. { N } ) )