fzouzsplit

Description: Split an upper integer set into a half-open integer range and another upper integer set. (Contributed by Mario Carneiro, 21-Sep-2016)

		Ref	Expression
	Assertion	fzouzsplit	$⊢ B \in ℤ_{\geq A} \to ℤ_{\geq A} = (A ..^B) \cup ℤ_{\geq B}$

Proof

Step	Hyp	Ref	Expression
1		eluzelre	$⊢ B \in ℤ_{\geq A} \to B \in ℝ$
2		eluzelre	$⊢ x \in ℤ_{\geq A} \to x \in ℝ$
3		lelttric	$⊢ (B \in ℝ \land x \in ℝ) \to (B \leq x \lor x < B)$
4	1 2 3	syl2an	$⊢ (B \in ℤ_{\geq A} \land x \in ℤ_{\geq A}) \to (B \leq x \lor x < B)$
5	4	orcomd	$⊢ (B \in ℤ_{\geq A} \land x \in ℤ_{\geq A}) \to (x < B \lor B \leq x)$
6		id	$⊢ x \in ℤ_{\geq A} \to x \in ℤ_{\geq A}$
7		eluzelz	$⊢ B \in ℤ_{\geq A} \to B \in ℤ$
8		elfzo2	$⊢ x \in (A ..^B) \leftrightarrow (x \in ℤ_{\geq A} \land B \in ℤ \land x < B)$
9		df-3an	$⊢ (x \in ℤ_{\geq A} \land B \in ℤ \land x < B) \leftrightarrow ((x \in ℤ_{\geq A} \land B \in ℤ) \land x < B)$
10	8 9	bitri	$⊢ x \in (A ..^B) \leftrightarrow ((x \in ℤ_{\geq A} \land B \in ℤ) \land x < B)$
11	10	baib	$⊢ (x \in ℤ_{\geq A} \land B \in ℤ) \to (x \in (A ..^B) \leftrightarrow x < B)$
12	6 7 11	syl2anr	$⊢ (B \in ℤ_{\geq A} \land x \in ℤ_{\geq A}) \to (x \in (A ..^B) \leftrightarrow x < B)$
13		eluzelz	$⊢ x \in ℤ_{\geq A} \to x \in ℤ$
14		eluz	$⊢ (B \in ℤ \land x \in ℤ) \to (x \in ℤ_{\geq B} \leftrightarrow B \leq x)$
15	7 13 14	syl2an	$⊢ (B \in ℤ_{\geq A} \land x \in ℤ_{\geq A}) \to (x \in ℤ_{\geq B} \leftrightarrow B \leq x)$
16	12 15	orbi12d	$⊢ (B \in ℤ_{\geq A} \land x \in ℤ_{\geq A}) \to ((x \in (A ..^B) \lor x \in ℤ_{\geq B}) \leftrightarrow (x < B \lor B \leq x))$
17	5 16	mpbird	$⊢ (B \in ℤ_{\geq A} \land x \in ℤ_{\geq A}) \to (x \in (A ..^B) \lor x \in ℤ_{\geq B})$
18	17	ex	$⊢ B \in ℤ_{\geq A} \to (x \in ℤ_{\geq A} \to (x \in (A ..^B) \lor x \in ℤ_{\geq B}))$
19		elun	$⊢ x \in ((A ..^B) \cup ℤ_{\geq B}) \leftrightarrow (x \in (A ..^B) \lor x \in ℤ_{\geq B})$
20	18 19	imbitrrdi	$⊢ B \in ℤ_{\geq A} \to (x \in ℤ_{\geq A} \to x \in ((A ..^B) \cup ℤ_{\geq B}))$
21	20	ssrdv	$⊢ B \in ℤ_{\geq A} \to ℤ_{\geq A} \subseteq (A ..^B) \cup ℤ_{\geq B}$
22		elfzouz	$⊢ x \in (A ..^B) \to x \in ℤ_{\geq A}$
23	22	ssriv	$⊢ (A ..^B) \subseteq ℤ_{\geq A}$
24	23	a1i	$⊢ B \in ℤ_{\geq A} \to (A ..^B) \subseteq ℤ_{\geq A}$
25		uzss	$⊢ B \in ℤ_{\geq A} \to ℤ_{\geq B} \subseteq ℤ_{\geq A}$
26	24 25	unssd	$⊢ B \in ℤ_{\geq A} \to (A ..^B) \cup ℤ_{\geq B} \subseteq ℤ_{\geq A}$
27	21 26	eqssd	$⊢ B \in ℤ_{\geq A} \to ℤ_{\geq A} = (A ..^B) \cup ℤ_{\geq B}$

Metamath Proof Explorer

Theorem fzouzsplit

Proof