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 ( 𝑁 ∈ ( ℤ𝑀 ) → ( 𝑀 ... 𝑁 ) = ( ( 𝑀 ... ( 𝑁 − 1 ) ) ∪ { 𝑁 } ) )

Proof

Step Hyp Ref Expression
1 eluzelz ( 𝑁 ∈ ( ℤ𝑀 ) → 𝑁 ∈ ℤ )
2 1 zcnd ( 𝑁 ∈ ( ℤ𝑀 ) → 𝑁 ∈ ℂ )
3 1zzd ( 𝑁 ∈ ( ℤ𝑀 ) → 1 ∈ ℤ )
4 3 zcnd ( 𝑁 ∈ ( ℤ𝑀 ) → 1 ∈ ℂ )
5 2 4 npcand ( 𝑁 ∈ ( ℤ𝑀 ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
6 5 eleq1d ( 𝑁 ∈ ( ℤ𝑀 ) → ( ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ𝑀 ) ↔ 𝑁 ∈ ( ℤ𝑀 ) ) )
7 6 ibir ( 𝑁 ∈ ( ℤ𝑀 ) → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ𝑀 ) )
8 eluzelre ( 𝑁 ∈ ( ℤ𝑀 ) → 𝑁 ∈ ℝ )
9 8 lem1d ( 𝑁 ∈ ( ℤ𝑀 ) → ( 𝑁 − 1 ) ≤ 𝑁 )
10 1 3 zsubcld ( 𝑁 ∈ ( ℤ𝑀 ) → ( 𝑁 − 1 ) ∈ ℤ )
11 eluz1 ( ( 𝑁 − 1 ) ∈ ℤ → ( 𝑁 ∈ ( ℤ ‘ ( 𝑁 − 1 ) ) ↔ ( 𝑁 ∈ ℤ ∧ ( 𝑁 − 1 ) ≤ 𝑁 ) ) )
12 10 11 syl ( 𝑁 ∈ ( ℤ𝑀 ) → ( 𝑁 ∈ ( ℤ ‘ ( 𝑁 − 1 ) ) ↔ ( 𝑁 ∈ ℤ ∧ ( 𝑁 − 1 ) ≤ 𝑁 ) ) )
13 1 9 12 mpbir2and ( 𝑁 ∈ ( ℤ𝑀 ) → 𝑁 ∈ ( ℤ ‘ ( 𝑁 − 1 ) ) )
14 fzsplit2 ( ( ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ𝑀 ) ∧ 𝑁 ∈ ( ℤ ‘ ( 𝑁 − 1 ) ) ) → ( 𝑀 ... 𝑁 ) = ( ( 𝑀 ... ( 𝑁 − 1 ) ) ∪ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) )
15 7 13 14 syl2anc ( 𝑁 ∈ ( ℤ𝑀 ) → ( 𝑀 ... 𝑁 ) = ( ( 𝑀 ... ( 𝑁 − 1 ) ) ∪ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) )
16 5 oveq1d ( 𝑁 ∈ ( ℤ𝑀 ) → ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) = ( 𝑁 ... 𝑁 ) )
17 fzsn ( 𝑁 ∈ ℤ → ( 𝑁 ... 𝑁 ) = { 𝑁 } )
18 1 17 syl ( 𝑁 ∈ ( ℤ𝑀 ) → ( 𝑁 ... 𝑁 ) = { 𝑁 } )
19 16 18 eqtrd ( 𝑁 ∈ ( ℤ𝑀 ) → ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) = { 𝑁 } )
20 19 uneq2d ( 𝑁 ∈ ( ℤ𝑀 ) → ( ( 𝑀 ... ( 𝑁 − 1 ) ) ∪ ( ( ( 𝑁 − 1 ) + 1 ) ... 𝑁 ) ) = ( ( 𝑀 ... ( 𝑁 − 1 ) ) ∪ { 𝑁 } ) )
21 15 20 eqtrd ( 𝑁 ∈ ( ℤ𝑀 ) → ( 𝑀 ... 𝑁 ) = ( ( 𝑀 ... ( 𝑁 − 1 ) ) ∪ { 𝑁 } ) )