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 ) ) = (/) )