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

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 ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∩ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) ) = ∅ )

Proof

Step Hyp Ref Expression
1 simpr3 ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) )
2 simpr1 ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → 𝑅 ∈ ℝ* )
3 simpr2 ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → 𝑆 ∈ ℝ* )
4 2 3 xaddcld ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → ( 𝑅 +𝑒 𝑆 ) ∈ ℝ* )
5 xmetcl ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) → ( 𝑃 𝐷 𝑄 ) ∈ ℝ* )
6 5 adantr ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → ( 𝑃 𝐷 𝑄 ) ∈ ℝ* )
7 4 6 xrlenltd ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → ( ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ↔ ¬ ( 𝑃 𝐷 𝑄 ) < ( 𝑅 +𝑒 𝑆 ) ) )
8 1 7 mpbid ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → ¬ ( 𝑃 𝐷 𝑄 ) < ( 𝑅 +𝑒 𝑆 ) )
9 elin ⊢ ( 𝑥 ∈ ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∩ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) ) ↔ ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∧ 𝑥 ∈ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) ) )
10 simpl1 ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
11 simpl2 ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → 𝑃 ∈ 𝑋 )
12 elbl ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ) )
13 10 11 2 12 syl3anc ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ) )
14 simpl3 ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → 𝑄 ∈ 𝑋 )
15 elbl ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑄 ∈ 𝑋 ∧ 𝑆 ∈ ℝ* ) → ( 𝑥 ∈ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑄 𝐷 𝑥 ) < 𝑆 ) ) )
16 10 14 3 15 syl3anc ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → ( 𝑥 ∈ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑄 𝐷 𝑥 ) < 𝑆 ) ) )
17 13 16 anbi12d ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → ( ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∧ 𝑥 ∈ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) ) ↔ ( ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑄 𝐷 𝑥 ) < 𝑆 ) ) ) )
18 anandi ⊢ ( ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑃 𝐷 𝑥 ) < 𝑅 ∧ ( 𝑄 𝐷 𝑥 ) < 𝑆 ) ) ↔ ( ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑄 𝐷 𝑥 ) < 𝑆 ) ) )
19 17 18 bitr4di ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → ( ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∧ 𝑥 ∈ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑃 𝐷 𝑥 ) < 𝑅 ∧ ( 𝑄 𝐷 𝑥 ) < 𝑆 ) ) ) )
20 10 adantr ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
21 11 adantr ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝑃 ∈ 𝑋 )
22 simpr ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
23 xmetcl ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑃 𝐷 𝑥 ) ∈ ℝ* )
24 20 21 22 23 syl3anc ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑃 𝐷 𝑥 ) ∈ ℝ* )
25 14 adantr ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝑄 ∈ 𝑋 )
26 xmetcl ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑄 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑄 𝐷 𝑥 ) ∈ ℝ* )
27 20 25 22 26 syl3anc ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑄 𝐷 𝑥 ) ∈ ℝ* )
28 2 adantr ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝑅 ∈ ℝ* )
29 3 adantr ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) ∧ 𝑥 ∈ 𝑋 ) → 𝑆 ∈ ℝ* )
30 xlt2add ⊢ ( ( ( ( 𝑃 𝐷 𝑥 ) ∈ ℝ* ∧ ( 𝑄 𝐷 𝑥 ) ∈ ℝ* ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) ) → ( ( ( 𝑃 𝐷 𝑥 ) < 𝑅 ∧ ( 𝑄 𝐷 𝑥 ) < 𝑆 ) → ( ( 𝑃 𝐷 𝑥 ) +𝑒 ( 𝑄 𝐷 𝑥 ) ) < ( 𝑅 +𝑒 𝑆 ) ) )
31 24 27 28 29 30 syl22anc ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝑃 𝐷 𝑥 ) < 𝑅 ∧ ( 𝑄 𝐷 𝑥 ) < 𝑆 ) → ( ( 𝑃 𝐷 𝑥 ) +𝑒 ( 𝑄 𝐷 𝑥 ) ) < ( 𝑅 +𝑒 𝑆 ) ) )
32 xmettri3 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → ( 𝑃 𝐷 𝑄 ) ≤ ( ( 𝑃 𝐷 𝑥 ) +𝑒 ( 𝑄 𝐷 𝑥 ) ) )
33 20 21 25 22 32 syl13anc ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑃 𝐷 𝑄 ) ≤ ( ( 𝑃 𝐷 𝑥 ) +𝑒 ( 𝑄 𝐷 𝑥 ) ) )
34 6 adantr ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑃 𝐷 𝑄 ) ∈ ℝ* )
35 24 27 xaddcld ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑃 𝐷 𝑥 ) +𝑒 ( 𝑄 𝐷 𝑥 ) ) ∈ ℝ* )
36 4 adantr ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑅 +𝑒 𝑆 ) ∈ ℝ* )
37 xrlelttr ⊢ ( ( ( 𝑃 𝐷 𝑄 ) ∈ ℝ* ∧ ( ( 𝑃 𝐷 𝑥 ) +𝑒 ( 𝑄 𝐷 𝑥 ) ) ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ∈ ℝ* ) → ( ( ( 𝑃 𝐷 𝑄 ) ≤ ( ( 𝑃 𝐷 𝑥 ) +𝑒 ( 𝑄 𝐷 𝑥 ) ) ∧ ( ( 𝑃 𝐷 𝑥 ) +𝑒 ( 𝑄 𝐷 𝑥 ) ) < ( 𝑅 +𝑒 𝑆 ) ) → ( 𝑃 𝐷 𝑄 ) < ( 𝑅 +𝑒 𝑆 ) ) )
38 34 35 36 37 syl3anc ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝑃 𝐷 𝑄 ) ≤ ( ( 𝑃 𝐷 𝑥 ) +𝑒 ( 𝑄 𝐷 𝑥 ) ) ∧ ( ( 𝑃 𝐷 𝑥 ) +𝑒 ( 𝑄 𝐷 𝑥 ) ) < ( 𝑅 +𝑒 𝑆 ) ) → ( 𝑃 𝐷 𝑄 ) < ( 𝑅 +𝑒 𝑆 ) ) )
39 33 38 mpand ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝑃 𝐷 𝑥 ) +𝑒 ( 𝑄 𝐷 𝑥 ) ) < ( 𝑅 +𝑒 𝑆 ) → ( 𝑃 𝐷 𝑄 ) < ( 𝑅 +𝑒 𝑆 ) ) )
40 31 39 syld ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝑃 𝐷 𝑥 ) < 𝑅 ∧ ( 𝑄 𝐷 𝑥 ) < 𝑆 ) → ( 𝑃 𝐷 𝑄 ) < ( 𝑅 +𝑒 𝑆 ) ) )
41 40 expimpd ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → ( ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑃 𝐷 𝑥 ) < 𝑅 ∧ ( 𝑄 𝐷 𝑥 ) < 𝑆 ) ) → ( 𝑃 𝐷 𝑄 ) < ( 𝑅 +𝑒 𝑆 ) ) )
42 19 41 sylbid ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → ( ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∧ 𝑥 ∈ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) ) → ( 𝑃 𝐷 𝑄 ) < ( 𝑅 +𝑒 𝑆 ) ) )
43 9 42 biimtrid ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → ( 𝑥 ∈ ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∩ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) ) → ( 𝑃 𝐷 𝑄 ) < ( 𝑅 +𝑒 𝑆 ) ) )
44 8 43 mtod ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → ¬ 𝑥 ∈ ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∩ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) ) )
45 44 eq0rdv ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑆 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∩ ( 𝑄 ( ball ‘ 𝐷 ) 𝑆 ) ) = ∅ )