Metamath Proof Explorer

Theorem bldisj

Description: Two balls are disjoint if the center-to-center distance is more than the sum of the radii. (Contributed by Mario Carneiro, 30-Dec-2013)

Ref Expression
Assertion bldisj 
|- ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) -> ( ( P ( ball ` D ) R ) i^i ( Q ( ball ` D ) S ) ) = (/) )

Proof

Step Hyp Ref Expression
1 simpr3 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) -> ( R +e S ) <_ ( P D Q ) )
2 simpr1 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) -> R e. RR* )
3 simpr2 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) -> S e. RR* )
4 2 3 xaddcld 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) -> ( R +e S ) e. RR* )
5 xmetcl 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) -> ( P D Q ) e. RR* )
6 5 adantr 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) -> ( P D Q ) e. RR* )
7 4 6 xrlenltd 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) -> ( ( R +e S ) <_ ( P D Q ) <-> -. ( P D Q ) < ( R +e S ) ) )
8 1 7 mpbid 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) -> -. ( P D Q ) < ( R +e S ) )
9 elin 
 |-  ( x e. ( ( P ( ball ` D ) R ) i^i ( Q ( ball ` D ) S ) ) <-> ( x e. ( P ( ball ` D ) R ) /\ x e. ( Q ( ball ` D ) S ) ) )
10 simpl1 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) -> D e. ( *Met ` X ) )
11 simpl2 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) -> P e. X )
12 elbl 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( x e. ( P ( ball ` D ) R ) <-> ( x e. X /\ ( P D x ) < R ) ) )
13 10 11 2 12 syl3anc 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) -> ( x e. ( P ( ball ` D ) R ) <-> ( x e. X /\ ( P D x ) < R ) ) )
14 simpl3 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) -> Q e. X )
15 elbl 
 |-  ( ( D e. ( *Met ` X ) /\ Q e. X /\ S e. RR* ) -> ( x e. ( Q ( ball ` D ) S ) <-> ( x e. X /\ ( Q D x ) < S ) ) )
16 10 14 3 15 syl3anc 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) -> ( x e. ( Q ( ball ` D ) S ) <-> ( x e. X /\ ( Q D x ) < S ) ) )
17 13 16 anbi12d 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) -> ( ( x e. ( P ( ball ` D ) R ) /\ x e. ( Q ( ball ` D ) S ) ) <-> ( ( x e. X /\ ( P D x ) < R ) /\ ( x e. X /\ ( Q D x ) < S ) ) ) )
18 anandi 
 |-  ( ( x e. X /\ ( ( P D x ) < R /\ ( Q D x ) < S ) ) <-> ( ( x e. X /\ ( P D x ) < R ) /\ ( x e. X /\ ( Q D x ) < S ) ) )
19 17 18 bitr4di 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) -> ( ( x e. ( P ( ball ` D ) R ) /\ x e. ( Q ( ball ` D ) S ) ) <-> ( x e. X /\ ( ( P D x ) < R /\ ( Q D x ) < S ) ) ) )
20 10 adantr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) /\ x e. X ) -> D e. ( *Met ` X ) )
21 11 adantr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) /\ x e. X ) -> P e. X )
22 simpr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) /\ x e. X ) -> x e. X )
23 xmetcl 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ x e. X ) -> ( P D x ) e. RR* )
24 20 21 22 23 syl3anc 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) /\ x e. X ) -> ( P D x ) e. RR* )
25 14 adantr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) /\ x e. X ) -> Q e. X )
26 xmetcl 
 |-  ( ( D e. ( *Met ` X ) /\ Q e. X /\ x e. X ) -> ( Q D x ) e. RR* )
27 20 25 22 26 syl3anc 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) /\ x e. X ) -> ( Q D x ) e. RR* )
28 2 adantr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) /\ x e. X ) -> R e. RR* )
29 3 adantr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) /\ x e. X ) -> S e. RR* )
30 xlt2add 
 |-  ( ( ( ( P D x ) e. RR* /\ ( Q D x ) e. RR* ) /\ ( R e. RR* /\ S e. RR* ) ) -> ( ( ( P D x ) < R /\ ( Q D x ) < S ) -> ( ( P D x ) +e ( Q D x ) ) < ( R +e S ) ) )
31 24 27 28 29 30 syl22anc 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) /\ x e. X ) -> ( ( ( P D x ) < R /\ ( Q D x ) < S ) -> ( ( P D x ) +e ( Q D x ) ) < ( R +e S ) ) )
32 xmettri3 
 |-  ( ( D e. ( *Met ` X ) /\ ( P e. X /\ Q e. X /\ x e. X ) ) -> ( P D Q ) <_ ( ( P D x ) +e ( Q D x ) ) )
33 20 21 25 22 32 syl13anc 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) /\ x e. X ) -> ( P D Q ) <_ ( ( P D x ) +e ( Q D x ) ) )
34 6 adantr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) /\ x e. X ) -> ( P D Q ) e. RR* )
35 24 27 xaddcld 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) /\ x e. X ) -> ( ( P D x ) +e ( Q D x ) ) e. RR* )
36 4 adantr 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) /\ x e. X ) -> ( R +e S ) e. RR* )
37 xrlelttr 
 |-  ( ( ( P D Q ) e. RR* /\ ( ( P D x ) +e ( Q D x ) ) e. RR* /\ ( R +e S ) e. RR* ) -> ( ( ( P D Q ) <_ ( ( P D x ) +e ( Q D x ) ) /\ ( ( P D x ) +e ( Q D x ) ) < ( R +e S ) ) -> ( P D Q ) < ( R +e S ) ) )
38 34 35 36 37 syl3anc 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) /\ x e. X ) -> ( ( ( P D Q ) <_ ( ( P D x ) +e ( Q D x ) ) /\ ( ( P D x ) +e ( Q D x ) ) < ( R +e S ) ) -> ( P D Q ) < ( R +e S ) ) )
39 33 38 mpand 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) /\ x e. X ) -> ( ( ( P D x ) +e ( Q D x ) ) < ( R +e S ) -> ( P D Q ) < ( R +e S ) ) )
40 31 39 syld 
 |-  ( ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) /\ x e. X ) -> ( ( ( P D x ) < R /\ ( Q D x ) < S ) -> ( P D Q ) < ( R +e S ) ) )
41 40 expimpd 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) -> ( ( x e. X /\ ( ( P D x ) < R /\ ( Q D x ) < S ) ) -> ( P D Q ) < ( R +e S ) ) )
42 19 41 sylbid 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) -> ( ( x e. ( P ( ball ` D ) R ) /\ x e. ( Q ( ball ` D ) S ) ) -> ( P D Q ) < ( R +e S ) ) )
43 9 42 syl5bi 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) -> ( x e. ( ( P ( ball ` D ) R ) i^i ( Q ( ball ` D ) S ) ) -> ( P D Q ) < ( R +e S ) ) )
44 8 43 mtod 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) -> -. x e. ( ( P ( ball ` D ) R ) i^i ( Q ( ball ` D ) S ) ) )
45 44 eq0rdv 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X /\ Q e. X ) /\ ( R e. RR* /\ S e. RR* /\ ( R +e S ) <_ ( P D Q ) ) ) -> ( ( P ( ball ` D ) R ) i^i ( Q ( ball ` D ) S ) ) = (/) )