fzsplitnd

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

		Ref	Expression
	Hypothesis	fzsplitnd.1	$⊢ φ \to K \in (M \dots N)$
	Assertion	fzsplitnd	$⊢ φ \to (M \dots N) = (M \dots K - 1) \cup (K \dots N)$

Step	Hyp	Ref	Expression
1		fzsplitnd.1	$⊢ φ \to K \in (M \dots N)$
2		elfzuz	$⊢ K \in (M \dots N) \to K \in ℤ_{\geq M}$
3	1 2	syl	$⊢ φ \to K \in ℤ_{\geq M}$
4	1	elfzelzd	$⊢ φ \to K \in ℤ$
5	4	zcnd	$⊢ φ \to K \in ℂ$
6		1cnd	$⊢ φ \to 1 \in ℂ$
7	5 6	npcand	$⊢ φ \to K - 1 + 1 = K$
8	7	eleq1d	$⊢ φ \to (K - 1 + 1 \in ℤ_{\geq M} \leftrightarrow K \in ℤ_{\geq M})$
9	3 8	mpbird	$⊢ φ \to K - 1 + 1 \in ℤ_{\geq M}$
10		1zzd	$⊢ φ \to 1 \in ℤ$
11	4 10	zsubcld	$⊢ φ \to K - 1 \in ℤ$
12		elfzuz3	$⊢ K \in (M \dots N) \to N \in ℤ_{\geq K}$
13	1 12	syl	$⊢ φ \to N \in ℤ_{\geq K}$
14	7	fveq2d	$⊢ φ \to ℤ_{\geq (K - 1 + 1)} = ℤ_{\geq K}$
15	14	eleq2d	$⊢ φ \to (N \in ℤ_{\geq (K - 1 + 1)} \leftrightarrow N \in ℤ_{\geq K})$
16	13 15	mpbird	$⊢ φ \to N \in ℤ_{\geq (K - 1 + 1)}$
17		peano2uzr	$⊢ (K - 1 \in ℤ \land N \in ℤ_{\geq (K - 1 + 1)}) \to N \in ℤ_{\geq (K - 1)}$
18	11 16 17	syl2anc	$⊢ φ \to N \in ℤ_{\geq (K - 1)}$
19		fzsplit2	$⊢ (K - 1 + 1 \in ℤ_{\geq M} \land N \in ℤ_{\geq (K - 1)}) \to (M \dots N) = (M \dots K - 1) \cup (K - 1 + 1 \dots N)$
20	9 18 19	syl2anc	$⊢ φ \to (M \dots N) = (M \dots K - 1) \cup (K - 1 + 1 \dots N)$
21	7	oveq1d	$⊢ φ \to (K - 1 + 1 \dots N) = (K \dots N)$
22	21	uneq2d	$⊢ φ \to (M \dots K - 1) \cup (K - 1 + 1 \dots N) = (M \dots K - 1) \cup (K \dots N)$
23	20 22	eqtrd	$⊢ φ \to (M \dots N) = (M \dots K - 1) \cup (K \dots N)$

Metamath Proof Explorer