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∈ℝ→AB=A+B2ball⁡DB−A2

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+A2∈ℝ
5 resubcl ⊢B∈ℝ∧A∈ℝ→B−A∈ℝ
6 5 ancoms ⊢A∈ℝ∧B∈ℝ→B−A∈ℝ
7 6 rehalfcld ⊢A∈ℝ∧B∈ℝ→B−A2∈ℝ
8 1 bl2ioo ⊢B+A2∈ℝ∧B−A2∈ℝ→B+A2ball⁡DB−A2=B+A2−B−A2B+A2+B−A2
9 4 7 8 syl2anc ⊢A∈ℝ∧B∈ℝ→B+A2ball⁡DB−A2=B+A2−B−A2B+A2+B−A2
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+A2=A+B2
15 14 oveq1d ⊢A∈ℝ∧B∈ℝ→B+A2ball⁡DB−A2=A+B2ball⁡DB−A2
16 halfaddsub ⊢B∈ℂ∧A∈ℂ→B+A2+B−A2=B∧B+A2−B−A2=A
17 10 11 16 syl2anr ⊢A∈ℝ∧B∈ℝ→B+A2+B−A2=B∧B+A2−B−A2=A
18 17 simprd ⊢A∈ℝ∧B∈ℝ→B+A2−B−A2=A
19 17 simpld ⊢A∈ℝ∧B∈ℝ→B+A2+B−A2=B
20 18 19 oveq12d ⊢A∈ℝ∧B∈ℝ→B+A2−B−A2B+A2+B−A2=AB
21 9 15 20 3eqtr3rd ⊢A∈ℝ∧B∈ℝ→AB=A+B2ball⁡DB−A2