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 ⊢ 𝐷 = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
Assertion ioo2bl ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 (,) 𝐵 ) = ( ( ( 𝐴 + 𝐵 ) / 2 ) ( ball ‘ 𝐷 ) ( ( 𝐵 − 𝐴 ) / 2 ) ) )

Proof

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