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

Metamath Proof Explorer

Theorem blss2

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)

Ref Expression
Assertion blss2 ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X ∧ Q ∈ X ∧ R ∈ ℝ ∧ S ∈ ℝ ∧ P D Q ≤ S − R → P ball ⁡ D R ⊆ Q ball ⁡ D S

Proof

Step Hyp Ref Expression
1 simpl1 ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X ∧ Q ∈ X ∧ R ∈ ℝ ∧ S ∈ ℝ ∧ P D Q ≤ S − R → D ∈ ∞Met ⁡ X
2 simpl2 ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X ∧ Q ∈ X ∧ R ∈ ℝ ∧ S ∈ ℝ ∧ P D Q ≤ S − R → P ∈ X
3 simpl3 ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X ∧ Q ∈ X ∧ R ∈ ℝ ∧ S ∈ ℝ ∧ P D Q ≤ S − R → Q ∈ X
4 simpr1 ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X ∧ Q ∈ X ∧ R ∈ ℝ ∧ S ∈ ℝ ∧ P D Q ≤ S − R → R ∈ ℝ
5 4 rexrd ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X ∧ Q ∈ X ∧ R ∈ ℝ ∧ S ∈ ℝ ∧ P D Q ≤ S − R → R ∈ ℝ *
6 simpr2 ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X ∧ Q ∈ X ∧ R ∈ ℝ ∧ S ∈ ℝ ∧ P D Q ≤ S − R → S ∈ ℝ
7 6 rexrd ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X ∧ Q ∈ X ∧ R ∈ ℝ ∧ S ∈ ℝ ∧ P D Q ≤ S − R → S ∈ ℝ *
8 6 4 resubcld ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X ∧ Q ∈ X ∧ R ∈ ℝ ∧ S ∈ ℝ ∧ P D Q ≤ S − R → S − R ∈ ℝ
9 simpr3 ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X ∧ Q ∈ X ∧ R ∈ ℝ ∧ S ∈ ℝ ∧ P D Q ≤ S − R → P D Q ≤ S − R
10 xmetlecl ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X ∧ Q ∈ X ∧ S − R ∈ ℝ ∧ P D Q ≤ S − R → P D Q ∈ ℝ
11 1 2 3 8 9 10 syl122anc ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X ∧ Q ∈ X ∧ R ∈ ℝ ∧ S ∈ ℝ ∧ P D Q ≤ S − R → P D Q ∈ ℝ
12 rexsub ⊢ S ∈ ℝ ∧ R ∈ ℝ → S + 𝑒 − R = S − R
13 6 4 12 syl2anc ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X ∧ Q ∈ X ∧ R ∈ ℝ ∧ S ∈ ℝ ∧ P D Q ≤ S − R → S + 𝑒 − R = S − R
14 9 13 breqtrrd ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X ∧ Q ∈ X ∧ R ∈ ℝ ∧ S ∈ ℝ ∧ P D Q ≤ S − R → P D Q ≤ S + 𝑒 − R
15 1 2 3 5 7 11 14 xblss2 ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X ∧ Q ∈ X ∧ R ∈ ℝ ∧ S ∈ ℝ ∧ P D Q ≤ S − R → P ball ⁡ D R ⊆ Q ball ⁡ D S