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 ) )