Metamath Proof Explorer

Theorem ioo2bl

Description: An open interval of reals in terms of a ball. (Contributed by NM, 18-May-2007) (Revised by Mario Carneiro, 28-Aug-2015)

Ref Expression
Hypothesis remet.1 ⊢ D = abs ∘ − ↾ ℝ 2
Assertion ioo2bl ⊢ A ∈ ℝ ∧ B ∈ ℝ → A B = A + B 2 ball ⁡ D B − A 2

Proof

Step Hyp Ref Expression
1 remet.1 ⊢ D = abs ∘ − ↾ ℝ 2
2 readdcl ⊢ B ∈ ℝ ∧ A ∈ ℝ → B + A ∈ ℝ
3 2 ancoms ⊢ A ∈ ℝ ∧ B ∈ ℝ → B + A ∈ ℝ
4 3 rehalfcld ⊢ A ∈ ℝ ∧ B ∈ ℝ → B + A 2 ∈ ℝ
5 resubcl ⊢ B ∈ ℝ ∧ A ∈ ℝ → B − A ∈ ℝ
6 5 ancoms ⊢ A ∈ ℝ ∧ B ∈ ℝ → B − A ∈ ℝ
7 6 rehalfcld ⊢ A ∈ ℝ ∧ B ∈ ℝ → B − A 2 ∈ ℝ
8 1 bl2ioo ⊢ B + A 2 ∈ ℝ ∧ B − A 2 ∈ ℝ → B + A 2 ball ⁡ D B − A 2 = B + A 2 − B − A 2 B + A 2 + B − A 2
9 4 7 8 syl2anc ⊢ A ∈ ℝ ∧ B ∈ ℝ → B + A 2 ball ⁡ D B − A 2 = B + A 2 − B − A 2 B + A 2 + B − A 2
10 recn ⊢ B ∈ ℝ → B ∈ ℂ
11 recn ⊢ A ∈ ℝ → A ∈ ℂ
12 addcom ⊢ B ∈ ℂ ∧ A ∈ ℂ → B + A = A + B
13 10 11 12 syl2anr ⊢ A ∈ ℝ ∧ B ∈ ℝ → B + A = A + B
14 13 oveq1d ⊢ A ∈ ℝ ∧ B ∈ ℝ → B + A 2 = A + B 2
15 14 oveq1d ⊢ A ∈ ℝ ∧ B ∈ ℝ → B + A 2 ball ⁡ D B − A 2 = A + B 2 ball ⁡ D B − A 2
16 halfaddsub ⊢ B ∈ ℂ ∧ A ∈ ℂ → B + A 2 + B − A 2 = B ∧ B + A 2 − B − A 2 = A
17 10 11 16 syl2anr ⊢ A ∈ ℝ ∧ B ∈ ℝ → B + A 2 + B − A 2 = B ∧ B + A 2 − B − A 2 = A
18 17 simprd ⊢ A ∈ ℝ ∧ B ∈ ℝ → B + A 2 − B − A 2 = A
19 17 simpld ⊢ A ∈ ℝ ∧ B ∈ ℝ → B + A 2 + B − A 2 = B
20 18 19 oveq12d ⊢ A ∈ ℝ ∧ B ∈ ℝ → B + A 2 − B − A 2 B + A 2 + B − A 2 = A B
21 9 15 20 3eqtr3rd ⊢ A ∈ ℝ ∧ B ∈ ℝ → A B = A + B 2 ball ⁡ D B − A 2