ioo2blex

Description: An open interval of reals in terms of a ball. (Contributed by Mario Carneiro, 14-Nov-2013)

		Ref	Expression
	Hypothesis	remet.1	$⊢ D = {(abs \circ -) ↾}_{ℝ^{2}}$
	Assertion	ioo2blex	$⊢ (A \in ℝ \land B \in ℝ) \to (A, B) \in ran ball (D)$

Step	Hyp	Ref	Expression
1		remet.1	$⊢ D = {(abs \circ -) ↾}_{ℝ^{2}}$
2	1	ioo2bl	$⊢ (A \in ℝ \land B \in ℝ) \to (A, B) = (\frac{A + B}{2}) ball (D) (\frac{B - A}{2})$
3	1	rexmet	$⊢ D \in ∞Met (ℝ)$
4		readdcl	$⊢ (A \in ℝ \land B \in ℝ) \to A + B \in ℝ$
5	4	rehalfcld	$⊢ (A \in ℝ \land B \in ℝ) \to \frac{A + B}{2} \in ℝ$
6		resubcl	$⊢ (B \in ℝ \land A \in ℝ) \to B - A \in ℝ$
7	6	ancoms	$⊢ (A \in ℝ \land B \in ℝ) \to B - A \in ℝ$
8	7	rehalfcld	$⊢ (A \in ℝ \land B \in ℝ) \to \frac{B - A}{2} \in ℝ$
9	8	rexrd	$⊢ (A \in ℝ \land B \in ℝ) \to \frac{B - A}{2} \in ℝ^{*}$
10		blelrn	$⊢ (D \in ∞Met (ℝ) \land \frac{A + B}{2} \in ℝ \land \frac{B - A}{2} \in ℝ^{*}) \to (\frac{A + B}{2}) ball (D) (\frac{B - A}{2}) \in ran ball (D)$
11	3 5 9 10	mp3an2i	$⊢ (A \in ℝ \land B \in ℝ) \to (\frac{A + B}{2}) ball (D) (\frac{B - A}{2}) \in ran ball (D)$
12	2 11	eqeltrd	$⊢ (A \in ℝ \land B \in ℝ) \to (A, B) \in ran ball (D)$

Metamath Proof Explorer