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 } ) )