Metamath Proof Explorer


Theorem 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 o. - ) |` ( RR X. RR ) )
Assertion ioo2blex
|- ( ( A e. RR /\ B e. RR ) -> ( A (,) B ) e. ran ( ball ` D ) )

Proof

Step Hyp Ref Expression
1 remet.1
 |-  D = ( ( abs o. - ) |` ( RR X. RR ) )
2 1 ioo2bl
 |-  ( ( A e. RR /\ B e. RR ) -> ( A (,) B ) = ( ( ( A + B ) / 2 ) ( ball ` D ) ( ( B - A ) / 2 ) ) )
3 1 rexmet
 |-  D e. ( *Met ` RR )
4 readdcl
 |-  ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
5 4 rehalfcld
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A + B ) / 2 ) e. RR )
6 resubcl
 |-  ( ( B e. RR /\ A e. RR ) -> ( B - A ) e. RR )
7 6 ancoms
 |-  ( ( A e. RR /\ B e. RR ) -> ( B - A ) e. RR )
8 7 rehalfcld
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( B - A ) / 2 ) e. RR )
9 8 rexrd
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( B - A ) / 2 ) e. RR* )
10 blelrn
 |-  ( ( D e. ( *Met ` RR ) /\ ( ( A + B ) / 2 ) e. RR /\ ( ( B - A ) / 2 ) e. RR* ) -> ( ( ( A + B ) / 2 ) ( ball ` D ) ( ( B - A ) / 2 ) ) e. ran ( ball ` D ) )
11 3 5 9 10 mp3an2i
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( ( A + B ) / 2 ) ( ball ` D ) ( ( B - A ) / 2 ) ) e. ran ( ball ` D ) )
12 2 11 eqeltrd
 |-  ( ( A e. RR /\ B e. RR ) -> ( A (,) B ) e. ran ( ball ` D ) )