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	$⊢ N \in ℤ_{\geq M} \to (M \dots N) = (M \dots N - 1) \cup \{N\}$

Proof

Step	Hyp	Ref	Expression
1		eluzelz	$⊢ N \in ℤ_{\geq M} \to N \in ℤ$
2	1	zcnd	$⊢ N \in ℤ_{\geq M} \to N \in ℂ$
3		1zzd	$⊢ N \in ℤ_{\geq M} \to 1 \in ℤ$
4	3	zcnd	$⊢ N \in ℤ_{\geq M} \to 1 \in ℂ$
5	2 4	npcand	$⊢ N \in ℤ_{\geq M} \to N - 1 + 1 = N$
6	5	eleq1d	$⊢ N \in ℤ_{\geq M} \to (N - 1 + 1 \in ℤ_{\geq M} \leftrightarrow N \in ℤ_{\geq M})$
7	6	ibir	$⊢ N \in ℤ_{\geq M} \to N - 1 + 1 \in ℤ_{\geq M}$
8		eluzelre	$⊢ N \in ℤ_{\geq M} \to N \in ℝ$
9	8	lem1d	$⊢ N \in ℤ_{\geq M} \to N - 1 \leq N$
10	1 3	zsubcld	$⊢ N \in ℤ_{\geq M} \to N - 1 \in ℤ$
11		eluz1	$⊢ N - 1 \in ℤ \to (N \in ℤ_{\geq (N - 1)} \leftrightarrow (N \in ℤ \land N - 1 \leq N))$
12	10 11	syl	$⊢ N \in ℤ_{\geq M} \to (N \in ℤ_{\geq (N - 1)} \leftrightarrow (N \in ℤ \land N - 1 \leq N))$
13	1 9 12	mpbir2and	$⊢ N \in ℤ_{\geq M} \to N \in ℤ_{\geq (N - 1)}$
14		fzsplit2	$⊢ (N - 1 + 1 \in ℤ_{\geq M} \land N \in ℤ_{\geq (N - 1)}) \to (M \dots N) = (M \dots N - 1) \cup (N - 1 + 1 \dots N)$
15	7 13 14	syl2anc	$⊢ N \in ℤ_{\geq M} \to (M \dots N) = (M \dots N - 1) \cup (N - 1 + 1 \dots N)$
16	5	oveq1d	$⊢ N \in ℤ_{\geq M} \to (N - 1 + 1 \dots N) = (N \dots N)$
17		fzsn	$⊢ N \in ℤ \to (N \dots N) = \{N\}$
18	1 17	syl	$⊢ N \in ℤ_{\geq M} \to (N \dots N) = \{N\}$
19	16 18	eqtrd	$⊢ N \in ℤ_{\geq M} \to (N - 1 + 1 \dots N) = \{N\}$
20	19	uneq2d	$⊢ N \in ℤ_{\geq M} \to (M \dots N - 1) \cup (N - 1 + 1 \dots N) = (M \dots N - 1) \cup \{N\}$
21	15 20	eqtrd	$⊢ N \in ℤ_{\geq M} \to (M \dots N) = (M \dots N - 1) \cup \{N\}$

Metamath Proof Explorer

Theorem fzspl

Proof