fzoun

Description: A half-open integer range as union of two half-open integer ranges. (Contributed by AV, 23-Apr-2022)

		Ref	Expression
	Assertion	fzoun	$⊢ (B \in ℤ_{\geq A} \land C \in ℕ_{0}) \to (A ..^B + C) = (A ..^B) \cup (B ..^B + C)$

Step	Hyp	Ref	Expression
1		eluzel2	$⊢ B \in ℤ_{\geq A} \to A \in ℤ$
2	1	adantr	$⊢ (B \in ℤ_{\geq A} \land C \in ℕ_{0}) \to A \in ℤ$
3		eluzelz	$⊢ B \in ℤ_{\geq A} \to B \in ℤ$
4		nn0z	$⊢ C \in ℕ_{0} \to C \in ℤ$
5		zaddcl	$⊢ (B \in ℤ \land C \in ℤ) \to B + C \in ℤ$
6	3 4 5	syl2an	$⊢ (B \in ℤ_{\geq A} \land C \in ℕ_{0}) \to B + C \in ℤ$
7	3	adantr	$⊢ (B \in ℤ_{\geq A} \land C \in ℕ_{0}) \to B \in ℤ$
8		eluzle	$⊢ B \in ℤ_{\geq A} \to A \leq B$
9	8	adantr	$⊢ (B \in ℤ_{\geq A} \land C \in ℕ_{0}) \to A \leq B$
10		nn0ge0	$⊢ C \in ℕ_{0} \to 0 \leq C$
11	10	adantl	$⊢ (B \in ℤ_{\geq A} \land C \in ℕ_{0}) \to 0 \leq C$
12		eluzelre	$⊢ B \in ℤ_{\geq A} \to B \in ℝ$
13		nn0re	$⊢ C \in ℕ_{0} \to C \in ℝ$
14		addge01	$⊢ (B \in ℝ \land C \in ℝ) \to (0 \leq C \leftrightarrow B \leq B + C)$
15	12 13 14	syl2an	$⊢ (B \in ℤ_{\geq A} \land C \in ℕ_{0}) \to (0 \leq C \leftrightarrow B \leq B + C)$
16	11 15	mpbid	$⊢ (B \in ℤ_{\geq A} \land C \in ℕ_{0}) \to B \leq B + C$
17	2 6 7 9 16	elfzd	$⊢ (B \in ℤ_{\geq A} \land C \in ℕ_{0}) \to B \in (A \dots B + C)$
18		fzosplit	$⊢ B \in (A \dots B + C) \to (A ..^B + C) = (A ..^B) \cup (B ..^B + C)$
19	17 18	syl	$⊢ (B \in ℤ_{\geq A} \land C \in ℕ_{0}) \to (A ..^B + C) = (A ..^B) \cup (B ..^B + C)$

Metamath Proof Explorer