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 \in ∞Met (X) \land P \in X \land Q \in X) \land (R \in ℝ^{} \land S \in ℝ^{} \land R +_{𝑒} S \leq P D Q)) \to (P ball (D) R) \cap (Q ball (D) S) = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		simpr3	$⊢ ((D \in ∞Met (X) \land P \in X \land Q \in X) \land (R \in ℝ^{} \land S \in ℝ^{} \land R +_{𝑒} S \leq P D Q)) \to R +_{𝑒} S \leq P D Q$
2		simpr1	$⊢ ((D \in ∞Met (X) \land P \in X \land Q \in X) \land (R \in ℝ^{} \land S \in ℝ^{} \land R +_{𝑒} S \leq P D Q)) \to R \in ℝ^{*}$
3		simpr2	$⊢ ((D \in ∞Met (X) \land P \in X \land Q \in X) \land (R \in ℝ^{} \land S \in ℝ^{} \land R +_{𝑒} S \leq P D Q)) \to S \in ℝ^{*}$
4	2 3	xaddcld	$⊢ ((D \in ∞Met (X) \land P \in X \land Q \in X) \land (R \in ℝ^{} \land S \in ℝ^{} \land R +_{𝑒} S \leq P D Q)) \to R +_{𝑒} S \in ℝ^{*}$
5		xmetcl	$⊢ (D \in ∞Met (X) \land P \in X \land Q \in X) \to P D Q \in ℝ^{*}$
6	5	adantr	$⊢ ((D \in ∞Met (X) \land P \in X \land Q \in X) \land (R \in ℝ^{} \land S \in ℝ^{} \land R +_{𝑒} S \leq P D Q)) \to P D Q \in ℝ^{*}$
7	4 6	xrlenltd	$⊢ ((D \in ∞Met (X) \land P \in X \land Q \in X) \land (R \in ℝ^{} \land S \in ℝ^{} \land R +_{𝑒} S \leq P D Q)) \to (R +_{𝑒} S \leq P D Q \leftrightarrow \neg P D Q < R +_{𝑒} S)$
8	1 7	mpbid	$⊢ ((D \in ∞Met (X) \land P \in X \land Q \in X) \land (R \in ℝ^{} \land S \in ℝ^{} \land R +_{𝑒} S \leq P D Q)) \to \neg P D Q < R +_{𝑒} S$
9		elin	$⊢ x \in ((P ball (D) R) \cap (Q ball (D) S)) \leftrightarrow (x \in (P ball (D) R) \land x \in (Q ball (D) S))$
10		simpl1	$⊢ ((D \in ∞Met (X) \land P \in X \land Q \in X) \land (R \in ℝ^{} \land S \in ℝ^{} \land R +_{𝑒} S \leq P D Q)) \to D \in ∞Met (X)$
11		simpl2	$⊢ ((D \in ∞Met (X) \land P \in X \land Q \in X) \land (R \in ℝ^{} \land S \in ℝ^{} \land R +_{𝑒} S \leq P D Q)) \to P \in X$
12		elbl	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \to (x \in (P ball (D) R) \leftrightarrow (x \in X \land P D x < R))$
13	10 11 2 12	syl3anc	$⊢ ((D \in ∞Met (X) \land P \in X \land Q \in X) \land (R \in ℝ^{} \land S \in ℝ^{} \land R +_{𝑒} S \leq P D Q)) \to (x \in (P ball (D) R) \leftrightarrow (x \in X \land P D x < R))$
14		simpl3	$⊢ ((D \in ∞Met (X) \land P \in X \land Q \in X) \land (R \in ℝ^{} \land S \in ℝ^{} \land R +_{𝑒} S \leq P D Q)) \to Q \in X$
15		elbl	$⊢ (D \in ∞Met (X) \land Q \in X \land S \in ℝ^{*}) \to (x \in (Q ball (D) S) \leftrightarrow (x \in X \land Q D x < S))$
16	10 14 3 15	syl3anc	$⊢ ((D \in ∞Met (X) \land P \in X \land Q \in X) \land (R \in ℝ^{} \land S \in ℝ^{} \land R +_{𝑒} S \leq P D Q)) \to (x \in (Q ball (D) S) \leftrightarrow (x \in X \land Q D x < S))$
17	13 16	anbi12d	$⊢ ((D \in ∞Met (X) \land P \in X \land Q \in X) \land (R \in ℝ^{} \land S \in ℝ^{} \land R +_{𝑒} S \leq P D Q)) \to ((x \in (P ball (D) R) \land x \in (Q ball (D) S)) \leftrightarrow ((x \in X \land P D x < R) \land (x \in X \land Q D x < S)))$
18		anandi	$⊢ (x \in X \land (P D x < R \land Q D x < S)) \leftrightarrow ((x \in X \land P D x < R) \land (x \in X \land Q D x < S))$
19	17 18	bitr4di	$⊢ ((D \in ∞Met (X) \land P \in X \land Q \in X) \land (R \in ℝ^{} \land S \in ℝ^{} \land R +_{𝑒} S \leq P D Q)) \to ((x \in (P ball (D) R) \land x \in (Q ball (D) S)) \leftrightarrow (x \in X \land (P D x < R \land Q D x < S)))$
20	10	adantr	$⊢ (((D \in ∞Met (X) \land P \in X \land Q \in X) \land (R \in ℝ^{} \land S \in ℝ^{} \land R +_{𝑒} S \leq P D Q)) \land x \in X) \to D \in ∞Met (X)$
21	11	adantr	$⊢ (((D \in ∞Met (X) \land P \in X \land Q \in X) \land (R \in ℝ^{} \land S \in ℝ^{} \land R +_{𝑒} S \leq P D Q)) \land x \in X) \to P \in X$
22		simpr	$⊢ (((D \in ∞Met (X) \land P \in X \land Q \in X) \land (R \in ℝ^{} \land S \in ℝ^{} \land R +_{𝑒} S \leq P D Q)) \land x \in X) \to x \in X$
23		xmetcl	$⊢ (D \in ∞Met (X) \land P \in X \land x \in X) \to P D x \in ℝ^{*}$
24	20 21 22 23	syl3anc	$⊢ (((D \in ∞Met (X) \land P \in X \land Q \in X) \land (R \in ℝ^{} \land S \in ℝ^{} \land R +_{𝑒} S \leq P D Q)) \land x \in X) \to P D x \in ℝ^{*}$
25	14	adantr	$⊢ (((D \in ∞Met (X) \land P \in X \land Q \in X) \land (R \in ℝ^{} \land S \in ℝ^{} \land R +_{𝑒} S \leq P D Q)) \land x \in X) \to Q \in X$
26		xmetcl	$⊢ (D \in ∞Met (X) \land Q \in X \land x \in X) \to Q D x \in ℝ^{*}$
27	20 25 22 26	syl3anc	$⊢ (((D \in ∞Met (X) \land P \in X \land Q \in X) \land (R \in ℝ^{} \land S \in ℝ^{} \land R +_{𝑒} S \leq P D Q)) \land x \in X) \to Q D x \in ℝ^{*}$
28	2	adantr	$⊢ (((D \in ∞Met (X) \land P \in X \land Q \in X) \land (R \in ℝ^{} \land S \in ℝ^{} \land R +_{𝑒} S \leq P D Q)) \land x \in X) \to R \in ℝ^{*}$
29	3	adantr	$⊢ (((D \in ∞Met (X) \land P \in X \land Q \in X) \land (R \in ℝ^{} \land S \in ℝ^{} \land R +_{𝑒} S \leq P D Q)) \land x \in X) \to S \in ℝ^{*}$
30		xlt2add	$⊢ ((P D x \in ℝ^{} \land Q D x \in ℝ^{}) \land (R \in ℝ^{} \land S \in ℝ^{})) \to ((P D x < R \land Q D x < S) \to (P D x) +_{𝑒} (Q D x) < R +_{𝑒} S)$
31	24 27 28 29 30	syl22anc	$⊢ (((D \in ∞Met (X) \land P \in X \land Q \in X) \land (R \in ℝ^{} \land S \in ℝ^{} \land R +_{𝑒} S \leq P D Q)) \land x \in X) \to ((P D x < R \land Q D x < S) \to (P D x) +_{𝑒} (Q D x) < R +_{𝑒} S)$
32		xmettri3	$⊢ (D \in ∞Met (X) \land (P \in X \land Q \in X \land x \in X)) \to P D Q \leq (P D x) +_{𝑒} (Q D x)$
33	20 21 25 22 32	syl13anc	$⊢ (((D \in ∞Met (X) \land P \in X \land Q \in X) \land (R \in ℝ^{} \land S \in ℝ^{} \land R +_{𝑒} S \leq P D Q)) \land x \in X) \to P D Q \leq (P D x) +_{𝑒} (Q D x)$
34	6	adantr	$⊢ (((D \in ∞Met (X) \land P \in X \land Q \in X) \land (R \in ℝ^{} \land S \in ℝ^{} \land R +_{𝑒} S \leq P D Q)) \land x \in X) \to P D Q \in ℝ^{*}$
35	24 27	xaddcld	$⊢ (((D \in ∞Met (X) \land P \in X \land Q \in X) \land (R \in ℝ^{} \land S \in ℝ^{} \land R +_{𝑒} S \leq P D Q)) \land x \in X) \to (P D x) +_{𝑒} (Q D x) \in ℝ^{*}$
36	4	adantr	$⊢ (((D \in ∞Met (X) \land P \in X \land Q \in X) \land (R \in ℝ^{} \land S \in ℝ^{} \land R +_{𝑒} S \leq P D Q)) \land x \in X) \to R +_{𝑒} S \in ℝ^{*}$
37		xrlelttr	$⊢ (P D Q \in ℝ^{} \land (P D x) +_{𝑒} (Q D x) \in ℝ^{} \land R +_{𝑒} S \in ℝ^{*}) \to ((P D Q \leq (P D x) +_{𝑒} (Q D x) \land (P D x) +_{𝑒} (Q D x) < R +_{𝑒} S) \to P D Q < R +_{𝑒} S)$
38	34 35 36 37	syl3anc	$⊢ (((D \in ∞Met (X) \land P \in X \land Q \in X) \land (R \in ℝ^{} \land S \in ℝ^{} \land R +_{𝑒} S \leq P D Q)) \land x \in X) \to ((P D Q \leq (P D x) +_{𝑒} (Q D x) \land (P D x) +_{𝑒} (Q D x) < R +_{𝑒} S) \to P D Q < R +_{𝑒} S)$
39	33 38	mpand	$⊢ (((D \in ∞Met (X) \land P \in X \land Q \in X) \land (R \in ℝ^{} \land S \in ℝ^{} \land R +_{𝑒} S \leq P D Q)) \land x \in X) \to ((P D x) +_{𝑒} (Q D x) < R +_{𝑒} S \to P D Q < R +_{𝑒} S)$
40	31 39	syld	$⊢ (((D \in ∞Met (X) \land P \in X \land Q \in X) \land (R \in ℝ^{} \land S \in ℝ^{} \land R +_{𝑒} S \leq P D Q)) \land x \in X) \to ((P D x < R \land Q D x < S) \to P D Q < R +_{𝑒} S)$
41	40	expimpd	$⊢ ((D \in ∞Met (X) \land P \in X \land Q \in X) \land (R \in ℝ^{} \land S \in ℝ^{} \land R +_{𝑒} S \leq P D Q)) \to ((x \in X \land (P D x < R \land Q D x < S)) \to P D Q < R +_{𝑒} S)$
42	19 41	sylbid	$⊢ ((D \in ∞Met (X) \land P \in X \land Q \in X) \land (R \in ℝ^{} \land S \in ℝ^{} \land R +_{𝑒} S \leq P D Q)) \to ((x \in (P ball (D) R) \land x \in (Q ball (D) S)) \to P D Q < R +_{𝑒} S)$
43	9 42	syl5bi	$⊢ ((D \in ∞Met (X) \land P \in X \land Q \in X) \land (R \in ℝ^{} \land S \in ℝ^{} \land R +_{𝑒} S \leq P D Q)) \to (x \in ((P ball (D) R) \cap (Q ball (D) S)) \to P D Q < R +_{𝑒} S)$
44	8 43	mtod	$⊢ ((D \in ∞Met (X) \land P \in X \land Q \in X) \land (R \in ℝ^{} \land S \in ℝ^{} \land R +_{𝑒} S \leq P D Q)) \to \neg x \in ((P ball (D) R) \cap (Q ball (D) S))$
45	44	eq0rdv	$⊢ ((D \in ∞Met (X) \land P \in X \land Q \in X) \land (R \in ℝ^{} \land S \in ℝ^{} \land R +_{𝑒} S \leq P D Q)) \to (P ball (D) R) \cap (Q ball (D) S) = \emptyset$

Metamath Proof Explorer

Theorem bldisj

Proof