xblss2

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)

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

Proof

Step	Hyp	Ref	Expression
1		xblss2.1	$⊢ φ \to D \in ∞Met (X)$
2		xblss2.2	$⊢ φ \to P \in X$
3		xblss2.3	$⊢ φ \to Q \in X$
4		xblss2.4	$⊢ φ \to R \in ℝ^{*}$
5		xblss2.5	$⊢ φ \to S \in ℝ^{*}$
6		xblss2.6	$⊢ φ \to P D Q \in ℝ$
7		xblss2.7	$⊢ φ \to P D Q \leq S +_{𝑒} (- R)$
8		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))$
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 ∞Met (X)$
12	3	adantr	$⊢ (φ \land x \in (P ball (D) R)) \to Q \in X$
13		xmetcl	$⊢ (D \in ∞Met (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		xmetcl	$⊢ (D \in ∞Met (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		xmettri2	$⊢ (D \in ∞Met (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	28	adantr	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to P D x < R$
46	7	ad2antrr	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to P D Q \leq S +_{𝑒} (- R)$
47		0xr	$⊢ 0 \in ℝ^{*}$
48	47	a1i	$⊢ (φ \land x \in (P ball (D) R)) \to 0 \in ℝ^{*}$
49		xmetge0	$⊢ (D \in ∞Met (X) \land P \in X \land Q \in X) \to 0 \leq P D Q$
50	11 22 12 49	syl3anc	$⊢ (φ \land x \in (P ball (D) R)) \to 0 \leq P D Q$
51	48 17 36 50 37	xrletrd	$⊢ (φ \land x \in (P ball (D) R)) \to 0 \leq S +_{𝑒} (- R)$
52		ge0nemnf	$⊢ (S +_{𝑒} (- R) \in ℝ^{*} \land 0 \leq S +_{𝑒} (- R)) \to S +_{𝑒} (- R) \neq −∞$
53	36 51 52	syl2anc	$⊢ (φ \land x \in (P ball (D) R)) \to S +_{𝑒} (- R) \neq −∞$
54	53	adantr	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to S +_{𝑒} (- R) \neq −∞$
55	5	ad2antrr	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to S \in ℝ^{*}$
56		xaddmnf1	$⊢ (S \in ℝ^{*} \land S \neq +∞) \to S +_{𝑒} −∞ = −∞$
57	56	ex	$⊢ S \in ℝ^{*} \to (S \neq +∞ \to S +_{𝑒} −∞ = −∞)$
58	55 57	syl	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to (S \neq +∞ \to S +_{𝑒} −∞ = −∞)$
59		simpr	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to R = +∞$
60		xnegeq	$⊢ R = +∞ \to - R = - +∞$
61	59 60	syl	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to - R = - +∞$
62		xnegpnf	$⊢ - +∞ = −∞$
63	61 62	syl6eq	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to - R = −∞$
64	63	oveq2d	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to S +_{𝑒} (- R) = S +_{𝑒} −∞$
65	64	eqeq1d	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to (S +_{𝑒} (- R) = −∞ \leftrightarrow S +_{𝑒} −∞ = −∞)$
66	58 65	sylibrd	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to (S \neq +∞ \to S +_{𝑒} (- R) = −∞)$
67	66	necon1d	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to (S +_{𝑒} (- R) \neq −∞ \to S = +∞)$
68	54 67	mpd	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to S = +∞$
69	68 63	oveq12d	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to S +_{𝑒} (- R) = +∞ +_{𝑒} −∞$
70		pnfaddmnf	$⊢ +∞ +_{𝑒} −∞ = 0$
71	69 70	syl6eq	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to S +_{𝑒} (- R) = 0$
72	46 71	breqtrd	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to P D Q \leq 0$
73	50	biantrud	$⊢ (φ \land x \in (P ball (D) R)) \to (P D Q \leq 0 \leftrightarrow (P D Q \leq 0 \land 0 \leq P D Q))$
74		xrletri3	$⊢ (P D Q \in ℝ^{} \land 0 \in ℝ^{}) \to (P D Q = 0 \leftrightarrow (P D Q \leq 0 \land 0 \leq P D Q))$
75	17 47 74	sylancl	$⊢ (φ \land x \in (P ball (D) R)) \to (P D Q = 0 \leftrightarrow (P D Q \leq 0 \land 0 \leq P D Q))$
76		xmeteq0	$⊢ (D \in ∞Met (X) \land P \in X \land Q \in X) \to (P D Q = 0 \leftrightarrow P = Q)$
77	11 22 12 76	syl3anc	$⊢ (φ \land x \in (P ball (D) R)) \to (P D Q = 0 \leftrightarrow P = Q)$
78	73 75 77	3bitr2d	$⊢ (φ \land x \in (P ball (D) R)) \to (P D Q \leq 0 \leftrightarrow P = Q)$
79	78	adantr	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to (P D Q \leq 0 \leftrightarrow P = Q)$
80	72 79	mpbid	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to P = Q$
81	80	oveq1d	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to P D x = Q D x$
82	59 68	eqtr4d	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to R = S$
83	45 81 82	3brtr3d	$⊢ ((φ \land x \in (P ball (D) R)) \land R = +∞) \to Q D x < S$
84		xmetge0	$⊢ (D \in ∞Met (X) \land P \in X \land x \in X) \to 0 \leq P D x$
85	11 22 10 84	syl3anc	$⊢ (φ \land x \in (P ball (D) R)) \to 0 \leq P D x$
86	48 24 18 85 28	xrlelttrd	$⊢ (φ \land x \in (P ball (D) R)) \to 0 < R$
87	48 18 86	xrltled	$⊢ (φ \land x \in (P ball (D) R)) \to 0 \leq R$
88		ge0nemnf	$⊢ (R \in ℝ^{*} \land 0 \leq R) \to R \neq −∞$
89	18 87 88	syl2anc	$⊢ (φ \land x \in (P ball (D) R)) \to R \neq −∞$
90	18 89	jca	$⊢ (φ \land x \in (P ball (D) R)) \to (R \in ℝ^{*} \land R \neq −∞)$
91		xrnemnf	$⊢ (R \in ℝ^{*} \land R \neq −∞) \leftrightarrow (R \in ℝ \lor R = +∞)$
92	90 91	sylib	$⊢ (φ \land x \in (P ball (D) R)) \to (R \in ℝ \lor R = +∞)$
93	44 83 92	mpjaodan	$⊢ (φ \land x \in (P ball (D) R)) \to Q D x < S$
94		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))$
95	11 12 34 94	syl3anc	$⊢ (φ \land x \in (P ball (D) R)) \to (x \in (Q ball (D) S) \leftrightarrow (x \in X \land Q D x < S))$
96	10 93 95	mpbir2and	$⊢ (φ \land x \in (P ball (D) R)) \to x \in (Q ball (D) S)$
97	96	ex	$⊢ φ \to (x \in (P ball (D) R) \to x \in (Q ball (D) S))$
98	97	ssrdv	$⊢ φ \to P ball (D) R \subseteq Q ball (D) S$

Metamath Proof Explorer

Theorem xblss2

Proof