Metamath Proof Explorer

Theorem bl2ioo

Description: A ball in terms of an open interval of reals. (Contributed by NM, 18-May-2007) (Revised by Mario Carneiro, 13-Nov-2013)

Ref Expression
Hypothesis remet.1 
|- D = ( ( abs o. - ) |` ( RR X. RR ) )
Assertion bl2ioo 
|- ( ( A e. RR /\ B e. RR ) -> ( A ( ball ` D ) B ) = ( ( A - B ) (,) ( A + B ) ) )

Proof

Step Hyp Ref Expression
1 remet.1 
 |-  D = ( ( abs o. - ) |` ( RR X. RR ) )
2 1 remetdval 
 |-  ( ( A e. RR /\ x e. RR ) -> ( A D x ) = ( abs ` ( A - x ) ) )
3 recn 
 |-  ( A e. RR -> A e. CC )
4 recn 
 |-  ( x e. RR -> x e. CC )
5 abssub 
 |-  ( ( A e. CC /\ x e. CC ) -> ( abs ` ( A - x ) ) = ( abs ` ( x - A ) ) )
6 3 4 5 syl2an 
 |-  ( ( A e. RR /\ x e. RR ) -> ( abs ` ( A - x ) ) = ( abs ` ( x - A ) ) )
7 2 6 eqtrd 
 |-  ( ( A e. RR /\ x e. RR ) -> ( A D x ) = ( abs ` ( x - A ) ) )
8 7 breq1d 
 |-  ( ( A e. RR /\ x e. RR ) -> ( ( A D x ) < B <-> ( abs ` ( x - A ) ) < B ) )
9 8 adantlr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ x e. RR ) -> ( ( A D x ) < B <-> ( abs ` ( x - A ) ) < B ) )
10 absdiflt 
 |-  ( ( x e. RR /\ A e. RR /\ B e. RR ) -> ( ( abs ` ( x - A ) ) < B <-> ( ( A - B ) < x /\ x < ( A + B ) ) ) )
11 10 3expb 
 |-  ( ( x e. RR /\ ( A e. RR /\ B e. RR ) ) -> ( ( abs ` ( x - A ) ) < B <-> ( ( A - B ) < x /\ x < ( A + B ) ) ) )
12 11 ancoms 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ x e. RR ) -> ( ( abs ` ( x - A ) ) < B <-> ( ( A - B ) < x /\ x < ( A + B ) ) ) )
13 9 12 bitrd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ x e. RR ) -> ( ( A D x ) < B <-> ( ( A - B ) < x /\ x < ( A + B ) ) ) )
14 13 pm5.32da 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( x e. RR /\ ( A D x ) < B ) <-> ( x e. RR /\ ( ( A - B ) < x /\ x < ( A + B ) ) ) ) )
15 3anass 
 |-  ( ( x e. RR /\ ( A - B ) < x /\ x < ( A + B ) ) <-> ( x e. RR /\ ( ( A - B ) < x /\ x < ( A + B ) ) ) )
16 14 15 bitr4di 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( x e. RR /\ ( A D x ) < B ) <-> ( x e. RR /\ ( A - B ) < x /\ x < ( A + B ) ) ) )
17 rexr 
 |-  ( B e. RR -> B e. RR* )
18 1 rexmet 
 |-  D e. ( *Met ` RR )
19 elbl 
 |-  ( ( D e. ( *Met ` RR ) /\ A e. RR /\ B e. RR* ) -> ( x e. ( A ( ball ` D ) B ) <-> ( x e. RR /\ ( A D x ) < B ) ) )
20 18 19 mp3an1 
 |-  ( ( A e. RR /\ B e. RR* ) -> ( x e. ( A ( ball ` D ) B ) <-> ( x e. RR /\ ( A D x ) < B ) ) )
21 17 20 sylan2 
 |-  ( ( A e. RR /\ B e. RR ) -> ( x e. ( A ( ball ` D ) B ) <-> ( x e. RR /\ ( A D x ) < B ) ) )
22 resubcl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A - B ) e. RR )
23 readdcl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
24 rexr 
 |-  ( ( A - B ) e. RR -> ( A - B ) e. RR* )
25 rexr 
 |-  ( ( A + B ) e. RR -> ( A + B ) e. RR* )
26 elioo2 
 |-  ( ( ( A - B ) e. RR* /\ ( A + B ) e. RR* ) -> ( x e. ( ( A - B ) (,) ( A + B ) ) <-> ( x e. RR /\ ( A - B ) < x /\ x < ( A + B ) ) ) )
27 24 25 26 syl2an 
 |-  ( ( ( A - B ) e. RR /\ ( A + B ) e. RR ) -> ( x e. ( ( A - B ) (,) ( A + B ) ) <-> ( x e. RR /\ ( A - B ) < x /\ x < ( A + B ) ) ) )
28 22 23 27 syl2anc 
 |-  ( ( A e. RR /\ B e. RR ) -> ( x e. ( ( A - B ) (,) ( A + B ) ) <-> ( x e. RR /\ ( A - B ) < x /\ x < ( A + B ) ) ) )
29 16 21 28 3bitr4d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( x e. ( A ( ball ` D ) B ) <-> x e. ( ( A - B ) (,) ( A + B ) ) ) )
30 29 eqrdv 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A ( ball ` D ) B ) = ( ( A - B ) (,) ( A + B ) ) )