Metamath Proof Explorer

Theorem xbln0

Description: A ball is nonempty iff the radius is positive. (Contributed by Mario Carneiro, 23-Aug-2015)

Ref Expression
Assertion xbln0 
|- ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( ( P ( ball ` D ) R ) =/= (/) <-> 0 < R ) )

Proof

Step Hyp Ref Expression
1 n0 
 |-  ( ( P ( ball ` D ) R ) =/= (/) <-> E. x x e. ( P ( ball ` D ) R ) )
2 elbl 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( x e. ( P ( ball ` D ) R ) <-> ( x e. X /\ ( P D x ) < R ) ) )
3 xmetge0 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ x e. X ) -> 0 <_ ( P D x ) )
4 3 3expa 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ x e. X ) -> 0 <_ ( P D x ) )
5 4 3adantl3 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ x e. X ) -> 0 <_ ( P D x ) )
6 0xr 
 |-  0 e. RR*
7 xmetcl 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ x e. X ) -> ( P D x ) e. RR* )
8 7 3expa 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ x e. X ) -> ( P D x ) e. RR* )
9 8 3adantl3 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ x e. X ) -> ( P D x ) e. RR* )
10 simpl3 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ x e. X ) -> R e. RR* )
11 xrlelttr 
 |-  ( ( 0 e. RR* /\ ( P D x ) e. RR* /\ R e. RR* ) -> ( ( 0 <_ ( P D x ) /\ ( P D x ) < R ) -> 0 < R ) )
12 6 9 10 11 mp3an2i 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ x e. X ) -> ( ( 0 <_ ( P D x ) /\ ( P D x ) < R ) -> 0 < R ) )
13 5 12 mpand 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ x e. X ) -> ( ( P D x ) < R -> 0 < R ) )
14 13 expimpd 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( ( x e. X /\ ( P D x ) < R ) -> 0 < R ) )
15 2 14 sylbid 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( x e. ( P ( ball ` D ) R ) -> 0 < R ) )
16 15 exlimdv 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( E. x x e. ( P ( ball ` D ) R ) -> 0 < R ) )
17 1 16 biimtrid 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( ( P ( ball ` D ) R ) =/= (/) -> 0 < R ) )
18 xblcntr 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ ( R e. RR* /\ 0 < R ) ) -> P e. ( P ( ball ` D ) R ) )
19 18 ne0d 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ ( R e. RR* /\ 0 < R ) ) -> ( P ( ball ` D ) R ) =/= (/) )
20 19 3expa 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( R e. RR* /\ 0 < R ) ) -> ( P ( ball ` D ) R ) =/= (/) )
21 20 expr 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ R e. RR* ) -> ( 0 < R -> ( P ( ball ` D ) R ) =/= (/) ) )
22 21 3impa 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( 0 < R -> ( P ( ball ` D ) R ) =/= (/) ) )
23 17 22 impbid 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( ( P ( ball ` D ) R ) =/= (/) <-> 0 < R ) )