Metamath Proof Explorer

Theorem xrsblre

Description: Any ball of the metric of the extended reals centered on an element of RR is entirely contained in RR . (Contributed by Mario Carneiro, 4-Sep-2015)

Ref Expression
Hypothesis xrsxmet.1 
|- D = ( dist ` RR*s )
Assertion xrsblre 
|- ( ( P e. RR /\ R e. RR* ) -> ( P ( ball ` D ) R ) C_ RR )

Proof

Step Hyp Ref Expression
1 xrsxmet.1 
 |-  D = ( dist ` RR*s )
2 rexr 
 |-  ( P e. RR -> P e. RR* )
3 1 xrsxmet 
 |-  D e. ( *Met ` RR* )
4 eqid 
 |-  ( `' D " RR ) = ( `' D " RR )
5 4 blssec 
 |-  ( ( D e. ( *Met ` RR* ) /\ P e. RR* /\ R e. RR* ) -> ( P ( ball ` D ) R ) C_ [ P ] ( `' D " RR ) )
6 3 5 mp3an1 
 |-  ( ( P e. RR* /\ R e. RR* ) -> ( P ( ball ` D ) R ) C_ [ P ] ( `' D " RR ) )
7 2 6 sylan 
 |-  ( ( P e. RR /\ R e. RR* ) -> ( P ( ball ` D ) R ) C_ [ P ] ( `' D " RR ) )
8 vex 
 |-  x e. _V
9 simpl 
 |-  ( ( P e. RR /\ R e. RR* ) -> P e. RR )
10 elecg 
 |-  ( ( x e. _V /\ P e. RR ) -> ( x e. [ P ] ( `' D " RR ) <-> P ( `' D " RR ) x ) )
11 8 9 10 sylancr 
 |-  ( ( P e. RR /\ R e. RR* ) -> ( x e. [ P ] ( `' D " RR ) <-> P ( `' D " RR ) x ) )
12 4 xmeterval 
 |-  ( D e. ( *Met ` RR* ) -> ( P ( `' D " RR ) x <-> ( P e. RR* /\ x e. RR* /\ ( P D x ) e. RR ) ) )
13 3 12 ax-mp 
 |-  ( P ( `' D " RR ) x <-> ( P e. RR* /\ x e. RR* /\ ( P D x ) e. RR ) )
14 simpr 
 |-  ( ( ( ( P e. RR /\ R e. RR* ) /\ ( P e. RR* /\ x e. RR* /\ ( P D x ) e. RR ) ) /\ P = x ) -> P = x )
15 simplll 
 |-  ( ( ( ( P e. RR /\ R e. RR* ) /\ ( P e. RR* /\ x e. RR* /\ ( P D x ) e. RR ) ) /\ P = x ) -> P e. RR )
16 14 15 eqeltrrd 
 |-  ( ( ( ( P e. RR /\ R e. RR* ) /\ ( P e. RR* /\ x e. RR* /\ ( P D x ) e. RR ) ) /\ P = x ) -> x e. RR )
17 simplr3 
 |-  ( ( ( ( P e. RR /\ R e. RR* ) /\ ( P e. RR* /\ x e. RR* /\ ( P D x ) e. RR ) ) /\ P =/= x ) -> ( P D x ) e. RR )
18 simplr1 
 |-  ( ( ( ( P e. RR /\ R e. RR* ) /\ ( P e. RR* /\ x e. RR* /\ ( P D x ) e. RR ) ) /\ P =/= x ) -> P e. RR* )
19 simplr2 
 |-  ( ( ( ( P e. RR /\ R e. RR* ) /\ ( P e. RR* /\ x e. RR* /\ ( P D x ) e. RR ) ) /\ P =/= x ) -> x e. RR* )
20 simpr 
 |-  ( ( ( ( P e. RR /\ R e. RR* ) /\ ( P e. RR* /\ x e. RR* /\ ( P D x ) e. RR ) ) /\ P =/= x ) -> P =/= x )
21 1 xrsdsreclb 
 |-  ( ( P e. RR* /\ x e. RR* /\ P =/= x ) -> ( ( P D x ) e. RR <-> ( P e. RR /\ x e. RR ) ) )
22 18 19 20 21 syl3anc 
 |-  ( ( ( ( P e. RR /\ R e. RR* ) /\ ( P e. RR* /\ x e. RR* /\ ( P D x ) e. RR ) ) /\ P =/= x ) -> ( ( P D x ) e. RR <-> ( P e. RR /\ x e. RR ) ) )
23 17 22 mpbid 
 |-  ( ( ( ( P e. RR /\ R e. RR* ) /\ ( P e. RR* /\ x e. RR* /\ ( P D x ) e. RR ) ) /\ P =/= x ) -> ( P e. RR /\ x e. RR ) )
24 23 simprd 
 |-  ( ( ( ( P e. RR /\ R e. RR* ) /\ ( P e. RR* /\ x e. RR* /\ ( P D x ) e. RR ) ) /\ P =/= x ) -> x e. RR )
25 16 24 pm2.61dane 
 |-  ( ( ( P e. RR /\ R e. RR* ) /\ ( P e. RR* /\ x e. RR* /\ ( P D x ) e. RR ) ) -> x e. RR )
26 25 ex 
 |-  ( ( P e. RR /\ R e. RR* ) -> ( ( P e. RR* /\ x e. RR* /\ ( P D x ) e. RR ) -> x e. RR ) )
27 13 26 syl5bi 
 |-  ( ( P e. RR /\ R e. RR* ) -> ( P ( `' D " RR ) x -> x e. RR ) )
28 11 27 sylbid 
 |-  ( ( P e. RR /\ R e. RR* ) -> ( x e. [ P ] ( `' D " RR ) -> x e. RR ) )
29 28 ssrdv 
 |-  ( ( P e. RR /\ R e. RR* ) -> [ P ] ( `' D " RR ) C_ RR )
30 7 29 sstrd 
 |-  ( ( P e. RR /\ R e. RR* ) -> ( P ( ball ` D ) R ) C_ RR )