xblss2ps

Description: One ball is contained in another if the center-to-center distance is less than the difference of the radii. In this version of blss2 for extended metrics, we have to assume the balls are a finite distance apart, or else P will not even be in the infinity ball around Q . (Contributed by Mario Carneiro, 23-Aug-2015) (Revised by Thierry Arnoux, 11-Mar-2018)

	Ref	Expression
Hypotheses	xblss2ps.1	$⊢ φ \to D \in PsMet (X)$
	xblss2ps.2	$⊢ φ \to P \in X$
	xblss2ps.3	$⊢ φ \to Q \in X$
	xblss2ps.4	$⊢ φ \to R \in ℝ^{*}$
	xblss2ps.5	$⊢ φ \to S \in ℝ^{*}$
	xblss2ps.6	$⊢ φ \to P D Q \in ℝ$
	xblss2ps.7	$⊢ φ \to P D Q \leq S +_{𝑒} (- R)$
Assertion	xblss2ps	$⊢ φ \to P ball (D) R \subseteq Q ball (D) S$

Proof

Step	Hyp	Ref	Expression
1		xblss2ps.1	$⊢ φ \to D \in PsMet (X)$
2		xblss2ps.2	$⊢ φ \to P \in X$
3		xblss2ps.3	$⊢ φ \to Q \in X$
4		xblss2ps.4	$⊢ φ \to R \in ℝ^{*}$
5		xblss2ps.5	$⊢ φ \to S \in ℝ^{*}$
6		xblss2ps.6	$⊢ φ \to P D Q \in ℝ$
7		xblss2ps.7	$⊢ φ \to P D Q \leq S +_{𝑒} (- R)$
8		elblps	$⊢ (D \in PsMet (X) \land P \in X \land R \in ℝ^{*}) \to (x \in (P ball (D) R) \leftrightarrow (x \in X \land P D x < R))$
9	1 2 4 8	syl3anc	$⊢ φ \to (x \in (P ball (D) R) \leftrightarrow (x \in X \land P D x < R))$
10	9	simprbda	$⊢ (φ \land x \in (P ball (D) R)) \to x \in X$
11	1	adantr	$⊢ (φ \land x \in (P ball (D) R)) \to D \in PsMet (X)$
12	3	adantr	$⊢ (φ \land x \in (P ball (D) R)) \to Q \in X$
13		psmetcl	$⊢ (D \in PsMet (X) \land Q \in X \land x \in X) \to Q D x \in ℝ^{*}$
14	11 12 10 13	syl3anc	$⊢ (φ \land x \in (P ball (D) R)) \to Q D x \in ℝ^{*}$
15	14	adantr	$⊢ ((φ \land x \in (P ball (D) R)) \land R \in ℝ) \to Q D x \in ℝ^{*}$
16	6	adantr	$⊢ (φ \land x \in (P ball (D) R)) \to P D Q \in ℝ$
17	16	rexrd	$⊢ (φ \land x \in (P ball (D) R)) \to P D Q \in ℝ^{*}$
18	4	adantr	$⊢ (φ \land x \in (P ball (D) R)) \to R \in ℝ^{*}$
19	17 18	xaddcld	$⊢ (φ \land x \in (P ball (D) R)) \to (P D Q) +_{𝑒} R \in ℝ^{*}$
20	19	adantr	$⊢ ((φ \land x \in (P ball (D) R)) \land R \in ℝ) \to (P D Q) +_{𝑒} R \in ℝ^{*}$
21	5	ad2antrr	$⊢ ((φ \land x \in (P ball (D) R)) \land R \in ℝ) \to S \in ℝ^{*}$
22	2	adantr	$⊢ (φ \land x \in (P ball (D) R)) \to P \in X$
23		psmetcl	$⊢ (D \in PsMet (X) \land P \in X \land x \in X) \to P D x \in ℝ^{*}$
24	11 22 10 23	syl3anc	$⊢ (φ \land x \in (P ball (D) R)) \to P D x \in ℝ^{*}$
25	17 24	xaddcld	$⊢ (φ \land x \in (P ball (D) R)) \to (P D Q) +_{𝑒} (P D x) \in ℝ^{*}$
26		psmettri2	$⊢ (D \in PsMet (X) \land (P \in X \land Q \in X \land x \in X)) \to Q D x \leq (P D Q) +_{𝑒} (P D x)$
27	11 22 12 10 26	syl13anc	$⊢ (φ \land x \in (P ball (D) R)) \to Q D x \leq (P D Q) +_{𝑒} (P D x)$
28	9	simplbda	$⊢ (φ \land x \in (P ball (D) R)) \to P D x < R$
29		xltadd2	$⊢ (P D x \in ℝ^{} \land R \in ℝ^{} \land P D Q \in ℝ) \to (P D x < R \leftrightarrow (P D Q) +_{𝑒} (P D x) < (P D Q) +_{𝑒} R)$
30	24 18 16 29	syl3anc	$⊢ (φ \land x \in (P ball (D) R)) \to (P D x < R \leftrightarrow (P D Q) +_{𝑒} (P D x) < (P D Q) +_{𝑒} R)$
31	28 30	mpbid	$⊢ (φ \land x \in (P ball (D) R)) \to (P D Q) +_{𝑒} (P D x) < (P D Q) +_{𝑒} R$
32	14 25 19 27 31	xrlelttrd	$⊢ (φ \land x \in (P ball (D) R)) \to Q D x < (P D Q) +_{𝑒} R$
33	32	adantr	$⊢ ((φ \land x \in (P ball (D) R)) \land R \in ℝ) \to Q D x < (P D Q) +_{𝑒} R$
34	5	adantr	$⊢ (φ \land x \in (P ball (D) R)) \to S \in ℝ^{*}$
35	18	xnegcld	$⊢ (φ \land x \in (P ball (D) R)) \to - R \in ℝ^{*}$
36	34 35	xaddcld	$⊢ (φ \land x \in (P ball (D) R)) \to S +_{𝑒} (- R) \in ℝ^{*}$
37	7	adantr	$⊢ (φ \land x \in (P ball (D) R)) \to P D Q \leq S +_{𝑒} (- R)$
38		xleadd1a	$⊢ ((P D Q \in ℝ^{} \land S +_{𝑒} (- R) \in ℝ^{} \land R \in ℝ^{*}) \land P D Q \leq S +_{𝑒} (- R)) \to (P D Q) +_{𝑒} R \leq (S +_{𝑒} (- R)) +_{𝑒} R$
39	17 36 18 37 38	syl31anc	$⊢ (φ \land x \in (P ball (D) R)) \to (P D Q) +_{𝑒} R \leq (S +_{𝑒} (- R)) +_{𝑒} R$
40	39	adantr	$⊢ ((φ \land x \in (P ball (D) R)) \land R \in ℝ) \to (P D Q) +_{𝑒} R \leq (S +_{𝑒} (- R)) +_{𝑒} R$
41		xnpcan	$⊢ (S \in ℝ^{*} \land R \in ℝ) \to (S +_{𝑒} (- R)) +_{𝑒} R = S$
42	34 41	sylan	$⊢ ((φ \land x \in (P ball (D) R)) \land R \in ℝ) \to (S +_{𝑒} (- R)) +_{𝑒} R = S$
43	40 42	breqtrd	$⊢ ((φ \land x \in (P ball (D) R)) \land R \in ℝ) \to (P D Q) +_{𝑒} R \leq S$
44	15 20 21 33 43	xrltletrd	$⊢ ((φ \land x \in (P ball (D) R)) \land R \in ℝ) \to Q D x < S$
45	14	adantr	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to Q D x \in ℝ^{*}$
46	6	ad2antrr	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to P D Q \in ℝ$
47		simpll	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to φ$
48		simplr	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to x \in (P ball (D) R)$
49		simpr	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to R = +∞$
50	49	oveq2d	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to P ball (D) R = P ball (D) +∞$
51	48 50	eleqtrd	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to x \in (P ball (D) +∞)$
52		xblpnfps	$⊢ (D \in PsMet (X) \land P \in X) \to (x \in (P ball (D) +∞) \leftrightarrow (x \in X \land P D x \in ℝ))$
53	1 2 52	syl2anc	$⊢ φ \to (x \in (P ball (D) +∞) \leftrightarrow (x \in X \land P D x \in ℝ))$
54	53	simplbda	$⊢ (φ \land x \in (P ball (D) +∞)) \to P D x \in ℝ$
55	47 51 54	syl2anc	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to P D x \in ℝ$
56	46 55	readdcld	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to (P D Q) + (P D x) \in ℝ$
57	56	rexrd	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to (P D Q) + (P D x) \in ℝ^{*}$
58		pnfxr	$⊢ +∞ \in ℝ^{*}$
59	58	a1i	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to +∞ \in ℝ^{*}$
60	1	ad2antrr	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to D \in PsMet (X)$
61	2	ad2antrr	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to P \in X$
62	3	ad2antrr	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to Q \in X$
63	10	adantr	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to x \in X$
64	60 61 62 63 26	syl13anc	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to Q D x \leq (P D Q) +_{𝑒} (P D x)$
65	46 55	rexaddd	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to (P D Q) +_{𝑒} (P D x) = (P D Q) + (P D x)$
66	64 65	breqtrd	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to Q D x \leq (P D Q) + (P D x)$
67	56	ltpnfd	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to (P D Q) + (P D x) < +∞$
68	45 57 59 66 67	xrlelttrd	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to Q D x < +∞$
69		0xr	$⊢ 0 \in ℝ^{*}$
70	69	a1i	$⊢ (φ \land x \in (P ball (D) R)) \to 0 \in ℝ^{*}$
71		psmetge0	$⊢ (D \in PsMet (X) \land P \in X \land Q \in X) \to 0 \leq P D Q$
72	11 22 12 71	syl3anc	$⊢ (φ \land x \in (P ball (D) R)) \to 0 \leq P D Q$
73	70 17 36 72 37	xrletrd	$⊢ (φ \land x \in (P ball (D) R)) \to 0 \leq S +_{𝑒} (- R)$
74		ge0nemnf	$⊢ (S +_{𝑒} (- R) \in ℝ^{*} \land 0 \leq S +_{𝑒} (- R)) \to S +_{𝑒} (- R) \neq −∞$
75	36 73 74	syl2anc	$⊢ (φ \land x \in (P ball (D) R)) \to S +_{𝑒} (- R) \neq −∞$
76	75	adantr	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to S +_{𝑒} (- R) \neq −∞$
77	5	ad2antrr	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to S \in ℝ^{*}$
78		xaddmnf1	$⊢ (S \in ℝ^{*} \land S \neq +∞) \to S +_{𝑒} −∞ = −∞$
79	78	ex	$⊢ S \in ℝ^{*} \to (S \neq +∞ \to S +_{𝑒} −∞ = −∞)$
80	77 79	syl	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to (S \neq +∞ \to S +_{𝑒} −∞ = −∞)$
81		xnegeq	$⊢ R = +∞ \to - R = - +∞$
82	49 81	syl	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to - R = - +∞$
83		xnegpnf	$⊢ - +∞ = −∞$
84	82 83	syl6eq	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to - R = −∞$
85	84	oveq2d	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to S +_{𝑒} (- R) = S +_{𝑒} −∞$
86	85	eqeq1d	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to (S +_{𝑒} (- R) = −∞ \leftrightarrow S +_{𝑒} −∞ = −∞)$
87	80 86	sylibrd	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to (S \neq +∞ \to S +_{𝑒} (- R) = −∞)$
88	87	necon1d	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to (S +_{𝑒} (- R) \neq −∞ \to S = +∞)$
89	76 88	mpd	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to S = +∞$
90	68 89	breqtrrd	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to Q D x < S$
91		psmetge0	$⊢ (D \in PsMet (X) \land P \in X \land x \in X) \to 0 \leq P D x$
92	11 22 10 91	syl3anc	$⊢ (φ \land x \in (P ball (D) R)) \to 0 \leq P D x$
93	70 24 18 92 28	xrlelttrd	$⊢ (φ \land x \in (P ball (D) R)) \to 0 < R$
94	70 18 93	xrltled	$⊢ (φ \land x \in (P ball (D) R)) \to 0 \leq R$
95		ge0nemnf	$⊢ (R \in ℝ^{*} \land 0 \leq R) \to R \neq −∞$
96	18 94 95	syl2anc	$⊢ (φ \land x \in (P ball (D) R)) \to R \neq −∞$
97	18 96	jca	$⊢ (φ \land x \in (P ball (D) R)) \to (R \in ℝ^{*} \land R \neq −∞)$
98		xrnemnf	$⊢ (R \in ℝ^{*} \land R \neq −∞) \leftrightarrow (R \in ℝ \lor R = +∞)$
99	97 98	sylib	$⊢ (φ \land x \in (P ball (D) R)) \to (R \in ℝ \lor R = +∞)$
100	44 90 99	mpjaodan	$⊢ (φ \land x \in (P ball (D) R)) \to Q D x < S$
101		elblps	$⊢ (D \in PsMet (X) \land Q \in X \land S \in ℝ^{*}) \to (x \in (Q ball (D) S) \leftrightarrow (x \in X \land Q D x < S))$
102	11 12 34 101	syl3anc	$⊢ (φ \land x \in (P ball (D) R)) \to (x \in (Q ball (D) S) \leftrightarrow (x \in X \land Q D x < S))$
103	10 100 102	mpbir2and	$⊢ (φ \land x \in (P ball (D) R)) \to x \in (Q ball (D) S)$
104	103	ex	$⊢ φ \to (x \in (P ball (D) R) \to x \in (Q ball (D) S))$
105	104	ssrdv	$⊢ φ \to P ball (D) R \subseteq Q ball (D) S$

Metamath Proof Explorer

Theorem xblss2ps

Proof