This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem blss2ps

Description: One ball is contained in another if the center-to-center distance is less than the difference of the radii. (Contributed by Mario Carneiro, 15-Jan-2014) (Revised by Mario Carneiro, 23-Aug-2015) (Revised by Thierry Arnoux, 11-Mar-2018)

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

Proof

Step Hyp Ref Expression
1 simpl1 
 |-  ( ( ( D e. ( PsMet ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR /\ S e. RR /\ ( P D Q ) <_ ( S - R ) ) ) -> D e. ( PsMet ` X ) )
2 simpl2 
 |-  ( ( ( D e. ( PsMet ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR /\ S e. RR /\ ( P D Q ) <_ ( S - R ) ) ) -> P e. X )
3 simpl3 
 |-  ( ( ( D e. ( PsMet ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR /\ S e. RR /\ ( P D Q ) <_ ( S - R ) ) ) -> Q e. X )
4 simpr1 
 |-  ( ( ( D e. ( PsMet ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR /\ S e. RR /\ ( P D Q ) <_ ( S - R ) ) ) -> R e. RR )
5 4 rexrd 
 |-  ( ( ( D e. ( PsMet ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR /\ S e. RR /\ ( P D Q ) <_ ( S - R ) ) ) -> R e. RR* )
6 simpr2 
 |-  ( ( ( D e. ( PsMet ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR /\ S e. RR /\ ( P D Q ) <_ ( S - R ) ) ) -> S e. RR )
7 6 rexrd 
 |-  ( ( ( D e. ( PsMet ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR /\ S e. RR /\ ( P D Q ) <_ ( S - R ) ) ) -> S e. RR* )
8 6 4 resubcld 
 |-  ( ( ( D e. ( PsMet ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR /\ S e. RR /\ ( P D Q ) <_ ( S - R ) ) ) -> ( S - R ) e. RR )
9 simpr3 
 |-  ( ( ( D e. ( PsMet ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR /\ S e. RR /\ ( P D Q ) <_ ( S - R ) ) ) -> ( P D Q ) <_ ( S - R ) )
10 psmetlecl 
 |-  ( ( D e. ( PsMet ` X ) /\ ( P e. X /\ Q e. X ) /\ ( ( S - R ) e. RR /\ ( P D Q ) <_ ( S - R ) ) ) -> ( P D Q ) e. RR )
11 1 2 3 8 9 10 syl122anc 
 |-  ( ( ( D e. ( PsMet ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR /\ S e. RR /\ ( P D Q ) <_ ( S - R ) ) ) -> ( P D Q ) e. RR )
12 rexsub 
 |-  ( ( S e. RR /\ R e. RR ) -> ( S +e -e R ) = ( S - R ) )
13 6 4 12 syl2anc 
 |-  ( ( ( D e. ( PsMet ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR /\ S e. RR /\ ( P D Q ) <_ ( S - R ) ) ) -> ( S +e -e R ) = ( S - R ) )
14 9 13 breqtrrd 
 |-  ( ( ( D e. ( PsMet ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR /\ S e. RR /\ ( P D Q ) <_ ( S - R ) ) ) -> ( P D Q ) <_ ( S +e -e R ) )
15 1 2 3 5 7 11 14 xblss2ps 
 |-  ( ( ( D e. ( PsMet ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR /\ S e. RR /\ ( P D Q ) <_ ( S - R ) ) ) -> ( P ( ball ` D ) R ) C_ ( Q ( ball ` D ) S ) )