Theorem fzsplitnr

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

	Ref	Expression
Hypotheses	fzsplitnr.1	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	fzsplitnr.2	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
	fzsplitnr.3	⊢ ( 𝜑 → 𝐾 ∈ ℤ )
	fzsplitnr.4	⊢ ( 𝜑 → 𝑀 ≤ 𝐾 )
	fzsplitnr.5	⊢ ( 𝜑 → 𝐾 ≤ 𝑁 )
Assertion	fzsplitnr	⊢ ( 𝜑 → ( 𝑀 ... 𝑁 ) = ( ( 𝑀 ... ( 𝐾 − 1 ) ) ∪ ( 𝐾 ... 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fzsplitnr.1	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2		fzsplitnr.2	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
3		fzsplitnr.3	⊢ ( 𝜑 → 𝐾 ∈ ℤ )
4		fzsplitnr.4	⊢ ( 𝜑 → 𝑀 ≤ 𝐾 )
5		fzsplitnr.5	⊢ ( 𝜑 → 𝐾 ≤ 𝑁 )
6	1 2 3 4 5	elfzd	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑀 ... 𝑁 ) )
7	6	fzsplitnd	⊢ ( 𝜑 → ( 𝑀 ... 𝑁 ) = ( ( 𝑀 ... ( 𝐾 − 1 ) ) ∪ ( 𝐾 ... 𝑁 ) ) )