Metamath Proof Explorer

Theorem ssblps

Description: The size of a ball increases monotonically with its radius. (Contributed by NM, 20-Sep-2007) (Revised by Mario Carneiro, 24-Aug-2015) (Revised by Thierry Arnoux, 11-Mar-2018)

Ref Expression
Assertion ssblps 
|- ( ( ( D e. ( PsMet ` X ) /\ P e. X ) /\ ( R e. RR* /\ S e. RR* ) /\ R <_ S ) -> ( P ( ball ` D ) R ) C_ ( P ( ball ` D ) S ) )

Proof

Step Hyp Ref Expression
1 simp1l 
 |-  ( ( ( D e. ( PsMet ` X ) /\ P e. X ) /\ ( R e. RR* /\ S e. RR* ) /\ R <_ S ) -> D e. ( PsMet ` X ) )
2 simp1r 
 |-  ( ( ( D e. ( PsMet ` X ) /\ P e. X ) /\ ( R e. RR* /\ S e. RR* ) /\ R <_ S ) -> P e. X )
3 simp2l 
 |-  ( ( ( D e. ( PsMet ` X ) /\ P e. X ) /\ ( R e. RR* /\ S e. RR* ) /\ R <_ S ) -> R e. RR* )
4 simp2r 
 |-  ( ( ( D e. ( PsMet ` X ) /\ P e. X ) /\ ( R e. RR* /\ S e. RR* ) /\ R <_ S ) -> S e. RR* )
5 psmet0 
 |-  ( ( D e. ( PsMet ` X ) /\ P e. X ) -> ( P D P ) = 0 )
6 5 3ad2ant1 
 |-  ( ( ( D e. ( PsMet ` X ) /\ P e. X ) /\ ( R e. RR* /\ S e. RR* ) /\ R <_ S ) -> ( P D P ) = 0 )
7 0re 
 |-  0 e. RR
8 6 7 eqeltrdi 
 |-  ( ( ( D e. ( PsMet ` X ) /\ P e. X ) /\ ( R e. RR* /\ S e. RR* ) /\ R <_ S ) -> ( P D P ) e. RR )
9 simp3 
 |-  ( ( ( D e. ( PsMet ` X ) /\ P e. X ) /\ ( R e. RR* /\ S e. RR* ) /\ R <_ S ) -> R <_ S )
10 xsubge0 
 |-  ( ( S e. RR* /\ R e. RR* ) -> ( 0 <_ ( S +e -e R ) <-> R <_ S ) )
11 4 3 10 syl2anc 
 |-  ( ( ( D e. ( PsMet ` X ) /\ P e. X ) /\ ( R e. RR* /\ S e. RR* ) /\ R <_ S ) -> ( 0 <_ ( S +e -e R ) <-> R <_ S ) )
12 9 11 mpbird 
 |-  ( ( ( D e. ( PsMet ` X ) /\ P e. X ) /\ ( R e. RR* /\ S e. RR* ) /\ R <_ S ) -> 0 <_ ( S +e -e R ) )
13 6 12 eqbrtrd 
 |-  ( ( ( D e. ( PsMet ` X ) /\ P e. X ) /\ ( R e. RR* /\ S e. RR* ) /\ R <_ S ) -> ( P D P ) <_ ( S +e -e R ) )
14 1 2 2 3 4 8 13 xblss2ps 
 |-  ( ( ( D e. ( PsMet ` X ) /\ P e. X ) /\ ( R e. RR* /\ S e. RR* ) /\ R <_ S ) -> ( P ( ball ` D ) R ) C_ ( P ( ball ` D ) S ) )