fzsplit1nn0

Description: Split a finite 1-based set of integers in the middle, allowing either end to be empty ( ( 1 ... 0 ) ). (Contributed by Stefan O'Rear, 8-Oct-2014)

		Ref	Expression
	Assertion	fzsplit1nn0	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0} \land A \leq B) \to (1 \dots B) = (1 \dots A) \cup (A + 1 \dots B)$

Proof

Step	Hyp	Ref	Expression
1		elnn0	$⊢ A \in ℕ_{0} \leftrightarrow (A \in ℕ \lor A = 0)$
2		1zzd	$⊢ (A \in ℕ \land (B \in ℕ_{0} \land A \leq B)) \to 1 \in ℤ$
3		nn0z	$⊢ B \in ℕ_{0} \to B \in ℤ$
4	3	ad2antrl	$⊢ (A \in ℕ \land (B \in ℕ_{0} \land A \leq B)) \to B \in ℤ$
5		nnz	$⊢ A \in ℕ \to A \in ℤ$
6	5	adantr	$⊢ (A \in ℕ \land (B \in ℕ_{0} \land A \leq B)) \to A \in ℤ$
7		nnge1	$⊢ A \in ℕ \to 1 \leq A$
8	7	adantr	$⊢ (A \in ℕ \land (B \in ℕ_{0} \land A \leq B)) \to 1 \leq A$
9		simprr	$⊢ (A \in ℕ \land (B \in ℕ_{0} \land A \leq B)) \to A \leq B$
10	2 4 6 8 9	elfzd	$⊢ (A \in ℕ \land (B \in ℕ_{0} \land A \leq B)) \to A \in (1 \dots B)$
11		fzsplit	$⊢ A \in (1 \dots B) \to (1 \dots B) = (1 \dots A) \cup (A + 1 \dots B)$
12	10 11	syl	$⊢ (A \in ℕ \land (B \in ℕ_{0} \land A \leq B)) \to (1 \dots B) = (1 \dots A) \cup (A + 1 \dots B)$
13		uncom	$⊢ (1 \dots A) \cup (A + 1 \dots B) = (A + 1 \dots B) \cup (1 \dots A)$
14		oveq1	$⊢ A = 0 \to A + 1 = 0 + 1$
15	14	adantr	$⊢ (A = 0 \land (B \in ℕ_{0} \land A \leq B)) \to A + 1 = 0 + 1$
16		0p1e1	$⊢ 0 + 1 = 1$
17	15 16	eqtrdi	$⊢ (A = 0 \land (B \in ℕ_{0} \land A \leq B)) \to A + 1 = 1$
18	17	oveq1d	$⊢ (A = 0 \land (B \in ℕ_{0} \land A \leq B)) \to (A + 1 \dots B) = (1 \dots B)$
19		oveq2	$⊢ A = 0 \to (1 \dots A) = (1 \dots 0)$
20	19	adantr	$⊢ (A = 0 \land (B \in ℕ_{0} \land A \leq B)) \to (1 \dots A) = (1 \dots 0)$
21		fz10	$⊢ (1 \dots 0) = \emptyset$
22	20 21	eqtrdi	$⊢ (A = 0 \land (B \in ℕ_{0} \land A \leq B)) \to (1 \dots A) = \emptyset$
23	18 22	uneq12d	$⊢ (A = 0 \land (B \in ℕ_{0} \land A \leq B)) \to (A + 1 \dots B) \cup (1 \dots A) = (1 \dots B) \cup \emptyset$
24		un0	$⊢ (1 \dots B) \cup \emptyset = (1 \dots B)$
25	23 24	eqtrdi	$⊢ (A = 0 \land (B \in ℕ_{0} \land A \leq B)) \to (A + 1 \dots B) \cup (1 \dots A) = (1 \dots B)$
26	13 25	eqtr2id	$⊢ (A = 0 \land (B \in ℕ_{0} \land A \leq B)) \to (1 \dots B) = (1 \dots A) \cup (A + 1 \dots B)$
27	12 26	jaoian	$⊢ ((A \in ℕ \lor A = 0) \land (B \in ℕ_{0} \land A \leq B)) \to (1 \dots B) = (1 \dots A) \cup (A + 1 \dots B)$
28	27	ex	$⊢ (A \in ℕ \lor A = 0) \to ((B \in ℕ_{0} \land A \leq B) \to (1 \dots B) = (1 \dots A) \cup (A + 1 \dots B))$
29	1 28	sylbi	$⊢ A \in ℕ_{0} \to ((B \in ℕ_{0} \land A \leq B) \to (1 \dots B) = (1 \dots A) \cup (A + 1 \dots B))$
30	29	3impib	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0} \land A \leq B) \to (1 \dots B) = (1 \dots A) \cup (A + 1 \dots B)$

Metamath Proof Explorer

Theorem fzsplit1nn0

Proof