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 ) ) ∪ { 𝑁 } ) )