Metamath Proof Explorer

Theorem blgt0

Description: A nonempty ball implies that the radius is positive. (Contributed by NM, 11-Mar-2007) (Revised by Mario Carneiro, 23-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 0xr 
 |-  0 e. RR*
2 1 a1i 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ A e. ( P ( ball ` D ) R ) ) -> 0 e. RR* )
3 simpl1 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ A e. ( P ( ball ` D ) R ) ) -> D e. ( *Met ` X ) )
4 simpl2 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ A e. ( P ( ball ` D ) R ) ) -> P e. X )
5 elbl 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( A e. ( P ( ball ` D ) R ) <-> ( A e. X /\ ( P D A ) < R ) ) )
6 5 simprbda 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ A e. ( P ( ball ` D ) R ) ) -> A e. X )
7 xmetcl 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ A e. X ) -> ( P D A ) e. RR* )
8 3 4 6 7 syl3anc 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ A e. ( P ( ball ` D ) R ) ) -> ( P D A ) e. RR* )
9 simpl3 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ A e. ( P ( ball ` D ) R ) ) -> R e. RR* )
10 xmetge0 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ A e. X ) -> 0 <_ ( P D A ) )
11 3 4 6 10 syl3anc 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ A e. ( P ( ball ` D ) R ) ) -> 0 <_ ( P D A ) )
12 5 simplbda 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ A e. ( P ( ball ` D ) R ) ) -> ( P D A ) < R )
13 2 8 9 11 12 xrlelttrd 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) /\ A e. ( P ( ball ` D ) R ) ) -> 0 < R )