Theorem fzsplitnd

Description: Split a finite interval of integers into two parts. (Contributed by metakunt, 28-May-2024)

	Ref	Expression
Hypothesis	fzsplitnd.1	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑀 ... 𝑁 ) )
Assertion	fzsplitnd	⊢ ( 𝜑 → ( 𝑀 ... 𝑁 ) = ( ( 𝑀 ... ( 𝐾 − 1 ) ) ∪ ( 𝐾 ... 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fzsplitnd.1	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑀 ... 𝑁 ) )
2		elfzuz	⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) )
3	1 2	syl	⊢ ( 𝜑 → 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) )
4	1	elfzelzd	⊢ ( 𝜑 → 𝐾 ∈ ℤ )
5	4	zcnd	⊢ ( 𝜑 → 𝐾 ∈ ℂ )
6		1cnd	⊢ ( 𝜑 → 1 ∈ ℂ )
7	5 6	npcand	⊢ ( 𝜑 → ( ( 𝐾 − 1 ) + 1 ) = 𝐾 )
8	7	eleq1d	⊢ ( 𝜑 → ( ( ( 𝐾 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ↔ 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ) )
9	3 8	mpbird	⊢ ( 𝜑 → ( ( 𝐾 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
10		1zzd	⊢ ( 𝜑 → 1 ∈ ℤ )
11	4 10	zsubcld	⊢ ( 𝜑 → ( 𝐾 − 1 ) ∈ ℤ )
12		elfzuz3	⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) )
13	1 12	syl	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) )
14	7	fveq2d	⊢ ( 𝜑 → ( ℤ≥ ‘ ( ( 𝐾 − 1 ) + 1 ) ) = ( ℤ≥ ‘ 𝐾 ) )
15	14	eleq2d	⊢ ( 𝜑 → ( 𝑁 ∈ ( ℤ≥ ‘ ( ( 𝐾 − 1 ) + 1 ) ) ↔ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) )
16	13 15	mpbird	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ ( ( 𝐾 − 1 ) + 1 ) ) )
17		peano2uzr	⊢ ( ( ( 𝐾 − 1 ) ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( ( 𝐾 − 1 ) + 1 ) ) ) → 𝑁 ∈ ( ℤ≥ ‘ ( 𝐾 − 1 ) ) )
18	11 16 17	syl2anc	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ ( 𝐾 − 1 ) ) )
19		fzsplit2	⊢ ( ( ( ( 𝐾 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐾 − 1 ) ) ) → ( 𝑀 ... 𝑁 ) = ( ( 𝑀 ... ( 𝐾 − 1 ) ) ∪ ( ( ( 𝐾 − 1 ) + 1 ) ... 𝑁 ) ) )
20	9 18 19	syl2anc	⊢ ( 𝜑 → ( 𝑀 ... 𝑁 ) = ( ( 𝑀 ... ( 𝐾 − 1 ) ) ∪ ( ( ( 𝐾 − 1 ) + 1 ) ... 𝑁 ) ) )
21	7	oveq1d	⊢ ( 𝜑 → ( ( ( 𝐾 − 1 ) + 1 ) ... 𝑁 ) = ( 𝐾 ... 𝑁 ) )
22	21	uneq2d	⊢ ( 𝜑 → ( ( 𝑀 ... ( 𝐾 − 1 ) ) ∪ ( ( ( 𝐾 − 1 ) + 1 ) ... 𝑁 ) ) = ( ( 𝑀 ... ( 𝐾 − 1 ) ) ∪ ( 𝐾 ... 𝑁 ) ) )
23	20 22	eqtrd	⊢ ( 𝜑 → ( 𝑀 ... 𝑁 ) = ( ( 𝑀 ... ( 𝐾 − 1 ) ) ∪ ( 𝐾 ... 𝑁 ) ) )