Metamath Proof Explorer

Theorem ssblex

Description: A nested ball exists whose radius is less than any desired amount. (Contributed by NM, 20-Sep-2007) (Revised by Mario Carneiro, 12-Nov-2013)

Ref Expression
Assertion ssblex 
|- ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( R e. RR+ /\ S e. RR+ ) ) -> E. x e. RR+ ( x < R /\ ( P ( ball ` D ) x ) C_ ( P ( ball ` D ) S ) ) )

Proof

Step Hyp Ref Expression
1 simprl 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( R e. RR+ /\ S e. RR+ ) ) -> R e. RR+ )
2 1 rphalfcld 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( R e. RR+ /\ S e. RR+ ) ) -> ( R / 2 ) e. RR+ )
3 simprr 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( R e. RR+ /\ S e. RR+ ) ) -> S e. RR+ )
4 2 3 ifcld 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( R e. RR+ /\ S e. RR+ ) ) -> if ( ( R / 2 ) <_ S , ( R / 2 ) , S ) e. RR+ )
5 4 rpred 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( R e. RR+ /\ S e. RR+ ) ) -> if ( ( R / 2 ) <_ S , ( R / 2 ) , S ) e. RR )
6 2 rpred 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( R e. RR+ /\ S e. RR+ ) ) -> ( R / 2 ) e. RR )
7 1 rpred 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( R e. RR+ /\ S e. RR+ ) ) -> R e. RR )
8 3 rpred 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( R e. RR+ /\ S e. RR+ ) ) -> S e. RR )
9 min1 
 |-  ( ( ( R / 2 ) e. RR /\ S e. RR ) -> if ( ( R / 2 ) <_ S , ( R / 2 ) , S ) <_ ( R / 2 ) )
10 6 8 9 syl2anc 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( R e. RR+ /\ S e. RR+ ) ) -> if ( ( R / 2 ) <_ S , ( R / 2 ) , S ) <_ ( R / 2 ) )
11 1 rpgt0d 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( R e. RR+ /\ S e. RR+ ) ) -> 0 < R )
12 halfpos 
 |-  ( R e. RR -> ( 0 < R <-> ( R / 2 ) < R ) )
13 7 12 syl 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( R e. RR+ /\ S e. RR+ ) ) -> ( 0 < R <-> ( R / 2 ) < R ) )
14 11 13 mpbid 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( R e. RR+ /\ S e. RR+ ) ) -> ( R / 2 ) < R )
15 5 6 7 10 14 lelttrd 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( R e. RR+ /\ S e. RR+ ) ) -> if ( ( R / 2 ) <_ S , ( R / 2 ) , S ) < R )
16 simpl 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( R e. RR+ /\ S e. RR+ ) ) -> ( D e. ( *Met ` X ) /\ P e. X ) )
17 4 rpxrd 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( R e. RR+ /\ S e. RR+ ) ) -> if ( ( R / 2 ) <_ S , ( R / 2 ) , S ) e. RR* )
18 3 rpxrd 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( R e. RR+ /\ S e. RR+ ) ) -> S e. RR* )
19 min2 
 |-  ( ( ( R / 2 ) e. RR /\ S e. RR ) -> if ( ( R / 2 ) <_ S , ( R / 2 ) , S ) <_ S )
20 6 8 19 syl2anc 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( R e. RR+ /\ S e. RR+ ) ) -> if ( ( R / 2 ) <_ S , ( R / 2 ) , S ) <_ S )
21 ssbl 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( if ( ( R / 2 ) <_ S , ( R / 2 ) , S ) e. RR* /\ S e. RR* ) /\ if ( ( R / 2 ) <_ S , ( R / 2 ) , S ) <_ S ) -> ( P ( ball ` D ) if ( ( R / 2 ) <_ S , ( R / 2 ) , S ) ) C_ ( P ( ball ` D ) S ) )
22 16 17 18 20 21 syl121anc 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( R e. RR+ /\ S e. RR+ ) ) -> ( P ( ball ` D ) if ( ( R / 2 ) <_ S , ( R / 2 ) , S ) ) C_ ( P ( ball ` D ) S ) )
23 breq1 
 |-  ( x = if ( ( R / 2 ) <_ S , ( R / 2 ) , S ) -> ( x < R <-> if ( ( R / 2 ) <_ S , ( R / 2 ) , S ) < R ) )
24 oveq2 
 |-  ( x = if ( ( R / 2 ) <_ S , ( R / 2 ) , S ) -> ( P ( ball ` D ) x ) = ( P ( ball ` D ) if ( ( R / 2 ) <_ S , ( R / 2 ) , S ) ) )
25 24 sseq1d 
 |-  ( x = if ( ( R / 2 ) <_ S , ( R / 2 ) , S ) -> ( ( P ( ball ` D ) x ) C_ ( P ( ball ` D ) S ) <-> ( P ( ball ` D ) if ( ( R / 2 ) <_ S , ( R / 2 ) , S ) ) C_ ( P ( ball ` D ) S ) ) )
26 23 25 anbi12d 
 |-  ( x = if ( ( R / 2 ) <_ S , ( R / 2 ) , S ) -> ( ( x < R /\ ( P ( ball ` D ) x ) C_ ( P ( ball ` D ) S ) ) <-> ( if ( ( R / 2 ) <_ S , ( R / 2 ) , S ) < R /\ ( P ( ball ` D ) if ( ( R / 2 ) <_ S , ( R / 2 ) , S ) ) C_ ( P ( ball ` D ) S ) ) ) )
27 26 rspcev 
 |-  ( ( if ( ( R / 2 ) <_ S , ( R / 2 ) , S ) e. RR+ /\ ( if ( ( R / 2 ) <_ S , ( R / 2 ) , S ) < R /\ ( P ( ball ` D ) if ( ( R / 2 ) <_ S , ( R / 2 ) , S ) ) C_ ( P ( ball ` D ) S ) ) ) -> E. x e. RR+ ( x < R /\ ( P ( ball ` D ) x ) C_ ( P ( ball ` D ) S ) ) )
28 4 15 22 27 syl12anc 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( R e. RR+ /\ S e. RR+ ) ) -> E. x e. RR+ ( x < R /\ ( P ( ball ` D ) x ) C_ ( P ( ball ` D ) S ) ) )