This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fzsplit

Description: Split a finite interval of integers into two parts. (Contributed by Jeff Madsen, 17-Jun-2010) (Revised by Mario Carneiro, 13-Apr-2016)

		Ref	Expression
	Assertion	fzsplit	$⊢ K \in (M \dots N) \to (M \dots N) = (M \dots K) \cup (K + 1 \dots N)$

Proof

Step	Hyp	Ref	Expression
1		elfzuz	$⊢ K \in (M \dots N) \to K \in ℤ_{\geq M}$
2		peano2uz	$⊢ K \in ℤ_{\geq M} \to K + 1 \in ℤ_{\geq M}$
3	1 2	syl	$⊢ K \in (M \dots N) \to K + 1 \in ℤ_{\geq M}$
4		elfzuz3	$⊢ K \in (M \dots N) \to N \in ℤ_{\geq K}$
5		fzsplit2	$⊢ (K + 1 \in ℤ_{\geq M} \land N \in ℤ_{\geq K}) \to (M \dots N) = (M \dots K) \cup (K + 1 \dots N)$
6	3 4 5	syl2anc	$⊢ K \in (M \dots N) \to (M \dots N) = (M \dots K) \cup (K + 1 \dots N)$