fzosplit

Description: Split a half-open integer range in half. (Contributed by Stefan O'Rear, 14-Aug-2015)

		Ref	Expression
	Assertion	fzosplit	$⊢ D \in (B \dots C) \to (B ..^C) = (B ..^D) \cup (D ..^C)$

Step	Hyp	Ref	Expression
1		simpr	$⊢ (D \in (B \dots C) \land x \in (B ..^C)) \to x \in (B ..^C)$
2		elfzelz	$⊢ D \in (B \dots C) \to D \in ℤ$
3	2	adantr	$⊢ (D \in (B \dots C) \land x \in (B ..^C)) \to D \in ℤ$
4		fzospliti	$⊢ (x \in (B ..^C) \land D \in ℤ) \to (x \in (B ..^D) \lor x \in (D ..^C))$
5	1 3 4	syl2anc	$⊢ (D \in (B \dots C) \land x \in (B ..^C)) \to (x \in (B ..^D) \lor x \in (D ..^C))$
6		elun	$⊢ x \in ((B ..^D) \cup (D ..^C)) \leftrightarrow (x \in (B ..^D) \lor x \in (D ..^C))$
7	5 6	sylibr	$⊢ (D \in (B \dots C) \land x \in (B ..^C)) \to x \in ((B ..^D) \cup (D ..^C))$
8	7	ex	$⊢ D \in (B \dots C) \to (x \in (B ..^C) \to x \in ((B ..^D) \cup (D ..^C)))$
9	8	ssrdv	$⊢ D \in (B \dots C) \to (B ..^C) \subseteq (B ..^D) \cup (D ..^C)$
10		elfzuz3	$⊢ D \in (B \dots C) \to C \in ℤ_{\geq D}$
11		fzoss2	$⊢ C \in ℤ_{\geq D} \to (B ..^D) \subseteq (B ..^C)$
12	10 11	syl	$⊢ D \in (B \dots C) \to (B ..^D) \subseteq (B ..^C)$
13		elfzuz	$⊢ D \in (B \dots C) \to D \in ℤ_{\geq B}$
14		fzoss1	$⊢ D \in ℤ_{\geq B} \to (D ..^C) \subseteq (B ..^C)$
15	13 14	syl	$⊢ D \in (B \dots C) \to (D ..^C) \subseteq (B ..^C)$
16	12 15	unssd	$⊢ D \in (B \dots C) \to (B ..^D) \cup (D ..^C) \subseteq (B ..^C)$
17	9 16	eqssd	$⊢ D \in (B \dots C) \to (B ..^C) = (B ..^D) \cup (D ..^C)$

Metamath Proof Explorer