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 \in PsMet (X) \land P \in X \land Q \in X) \land (R \in ℝ \land S \in ℝ \land P D Q \leq S - R)) \to P ball (D) R \subseteq Q ball (D) S$

Proof

Step	Hyp	Ref	Expression
1		simpl1	$⊢ ((D \in PsMet (X) \land P \in X \land Q \in X) \land (R \in ℝ \land S \in ℝ \land P D Q \leq S - R)) \to D \in PsMet (X)$
2		simpl2	$⊢ ((D \in PsMet (X) \land P \in X \land Q \in X) \land (R \in ℝ \land S \in ℝ \land P D Q \leq S - R)) \to P \in X$
3		simpl3	$⊢ ((D \in PsMet (X) \land P \in X \land Q \in X) \land (R \in ℝ \land S \in ℝ \land P D Q \leq S - R)) \to Q \in X$
4		simpr1	$⊢ ((D \in PsMet (X) \land P \in X \land Q \in X) \land (R \in ℝ \land S \in ℝ \land P D Q \leq S - R)) \to R \in ℝ$
5	4	rexrd	$⊢ ((D \in PsMet (X) \land P \in X \land Q \in X) \land (R \in ℝ \land S \in ℝ \land P D Q \leq S - R)) \to R \in ℝ^{*}$
6		simpr2	$⊢ ((D \in PsMet (X) \land P \in X \land Q \in X) \land (R \in ℝ \land S \in ℝ \land P D Q \leq S - R)) \to S \in ℝ$
7	6	rexrd	$⊢ ((D \in PsMet (X) \land P \in X \land Q \in X) \land (R \in ℝ \land S \in ℝ \land P D Q \leq S - R)) \to S \in ℝ^{*}$
8	6 4	resubcld	$⊢ ((D \in PsMet (X) \land P \in X \land Q \in X) \land (R \in ℝ \land S \in ℝ \land P D Q \leq S - R)) \to S - R \in ℝ$
9		simpr3	$⊢ ((D \in PsMet (X) \land P \in X \land Q \in X) \land (R \in ℝ \land S \in ℝ \land P D Q \leq S - R)) \to P D Q \leq S - R$
10		psmetlecl	$⊢ (D \in PsMet (X) \land (P \in X \land Q \in X) \land (S - R \in ℝ \land P D Q \leq S - R)) \to P D Q \in ℝ$
11	1 2 3 8 9 10	syl122anc	$⊢ ((D \in PsMet (X) \land P \in X \land Q \in X) \land (R \in ℝ \land S \in ℝ \land P D Q \leq S - R)) \to P D Q \in ℝ$
12		rexsub	$⊢ (S \in ℝ \land R \in ℝ) \to S +_{𝑒} (- R) = S - R$
13	6 4 12	syl2anc	$⊢ ((D \in PsMet (X) \land P \in X \land Q \in X) \land (R \in ℝ \land S \in ℝ \land P D Q \leq S - R)) \to S +_{𝑒} (- R) = S - R$
14	9 13	breqtrrd	$⊢ ((D \in PsMet (X) \land P \in X \land Q \in X) \land (R \in ℝ \land S \in ℝ \land P D Q \leq S - R)) \to P D Q \leq S +_{𝑒} (- R)$
15	1 2 3 5 7 11 14	xblss2ps	$⊢ ((D \in PsMet (X) \land P \in X \land Q \in X) \land (R \in ℝ \land S \in ℝ \land P D Q \leq S - R)) \to P ball (D) R \subseteq Q ball (D) S$

Metamath Proof Explorer

Theorem blss2ps

Proof