bl2in

Description: Two balls are disjoint if they don't overlap. (Contributed by NM, 11-Mar-2007) (Revised by Mario Carneiro, 23-Aug-2015)

		Ref	Expression
	Assertion	bl2in	$⊢ ((D \in Met (X) \land P \in X \land Q \in X) \land (R \in ℝ \land R \leq \frac{P D Q}{2})) \to (P ball (D) R) \cap (Q ball (D) R) = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		simpl1	$⊢ ((D \in Met (X) \land P \in X \land Q \in X) \land (R \in ℝ \land R \leq \frac{P D Q}{2})) \to D \in Met (X)$
2		metxmet	$⊢ D \in Met (X) \to D \in ∞Met (X)$
3	1 2	syl	$⊢ ((D \in Met (X) \land P \in X \land Q \in X) \land (R \in ℝ \land R \leq \frac{P D Q}{2})) \to D \in ∞Met (X)$
4		simpl2	$⊢ ((D \in Met (X) \land P \in X \land Q \in X) \land (R \in ℝ \land R \leq \frac{P D Q}{2})) \to P \in X$
5		simpl3	$⊢ ((D \in Met (X) \land P \in X \land Q \in X) \land (R \in ℝ \land R \leq \frac{P D Q}{2})) \to Q \in X$
6		rexr	$⊢ R \in ℝ \to R \in ℝ^{*}$
7	6	ad2antrl	$⊢ ((D \in Met (X) \land P \in X \land Q \in X) \land (R \in ℝ \land R \leq \frac{P D Q}{2})) \to R \in ℝ^{*}$
8		simprl	$⊢ ((D \in Met (X) \land P \in X \land Q \in X) \land (R \in ℝ \land R \leq \frac{P D Q}{2})) \to R \in ℝ$
9	8 8	rexaddd	$⊢ ((D \in Met (X) \land P \in X \land Q \in X) \land (R \in ℝ \land R \leq \frac{P D Q}{2})) \to R +_{𝑒} R = R + R$
10	8	recnd	$⊢ ((D \in Met (X) \land P \in X \land Q \in X) \land (R \in ℝ \land R \leq \frac{P D Q}{2})) \to R \in ℂ$
11	10	2timesd	$⊢ ((D \in Met (X) \land P \in X \land Q \in X) \land (R \in ℝ \land R \leq \frac{P D Q}{2})) \to 2 R = R + R$
12	9 11	eqtr4d	$⊢ ((D \in Met (X) \land P \in X \land Q \in X) \land (R \in ℝ \land R \leq \frac{P D Q}{2})) \to R +_{𝑒} R = 2 R$
13		id	$⊢ R \in ℝ \to R \in ℝ$
14		metcl	$⊢ (D \in Met (X) \land P \in X \land Q \in X) \to P D Q \in ℝ$
15		2re	$⊢ 2 \in ℝ$
16		2pos	$⊢ 0 < 2$
17	15 16	pm3.2i	$⊢ (2 \in ℝ \land 0 < 2)$
18		lemuldiv2	$⊢ (R \in ℝ \land P D Q \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (2 R \leq P D Q \leftrightarrow R \leq \frac{P D Q}{2})$
19	17 18	mp3an3	$⊢ (R \in ℝ \land P D Q \in ℝ) \to (2 R \leq P D Q \leftrightarrow R \leq \frac{P D Q}{2})$
20	13 14 19	syl2anr	$⊢ ((D \in Met (X) \land P \in X \land Q \in X) \land R \in ℝ) \to (2 R \leq P D Q \leftrightarrow R \leq \frac{P D Q}{2})$
21	20	biimprd	$⊢ ((D \in Met (X) \land P \in X \land Q \in X) \land R \in ℝ) \to (R \leq \frac{P D Q}{2} \to 2 R \leq P D Q)$
22	21	impr	$⊢ ((D \in Met (X) \land P \in X \land Q \in X) \land (R \in ℝ \land R \leq \frac{P D Q}{2})) \to 2 R \leq P D Q$
23	12 22	eqbrtrd	$⊢ ((D \in Met (X) \land P \in X \land Q \in X) \land (R \in ℝ \land R \leq \frac{P D Q}{2})) \to R +_{𝑒} R \leq P D Q$
24		bldisj	$⊢ ((D \in ∞Met (X) \land P \in X \land Q \in X) \land (R \in ℝ^{} \land R \in ℝ^{} \land R +_{𝑒} R \leq P D Q)) \to (P ball (D) R) \cap (Q ball (D) R) = \emptyset$
25	3 4 5 7 7 23 24	syl33anc	$⊢ ((D \in Met (X) \land P \in X \land Q \in X) \land (R \in ℝ \land R \leq \frac{P D Q}{2})) \to (P ball (D) R) \cap (Q ball (D) R) = \emptyset$

Metamath Proof Explorer

Theorem bl2in

Proof