fzosplitsn

Description: Extending a half-open range by a singleton on the end. (Contributed by Stefan O'Rear, 23-Aug-2015)

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

Step	Hyp	Ref	Expression
1		id	$⊢ B \in ℤ_{\geq A} \to B \in ℤ_{\geq A}$
2		eluzelz	$⊢ B \in ℤ_{\geq A} \to B \in ℤ$
3		uzid	$⊢ B \in ℤ \to B \in ℤ_{\geq B}$
4		peano2uz	$⊢ B \in ℤ_{\geq B} \to B + 1 \in ℤ_{\geq B}$
5	2 3 4	3syl	$⊢ B \in ℤ_{\geq A} \to B + 1 \in ℤ_{\geq B}$
6		elfzuzb	$⊢ B \in (A \dots B + 1) \leftrightarrow (B \in ℤ_{\geq A} \land B + 1 \in ℤ_{\geq B})$
7	1 5 6	sylanbrc	$⊢ B \in ℤ_{\geq A} \to B \in (A \dots B + 1)$
8		fzosplit	$⊢ B \in (A \dots B + 1) \to (A ..^B + 1) = (A ..^B) \cup (B ..^B + 1)$
9	7 8	syl	$⊢ B \in ℤ_{\geq A} \to (A ..^B + 1) = (A ..^B) \cup (B ..^B + 1)$
10		fzosn	$⊢ B \in ℤ \to (B ..^B + 1) = \{B\}$
11	2 10	syl	$⊢ B \in ℤ_{\geq A} \to (B ..^B + 1) = \{B\}$
12	11	uneq2d	$⊢ B \in ℤ_{\geq A} \to (A ..^B) \cup (B ..^B + 1) = (A ..^B) \cup \{B\}$
13	9 12	eqtrd	$⊢ B \in ℤ_{\geq A} \to (A ..^B + 1) = (A ..^B) \cup \{B\}$

Metamath Proof Explorer