Metamath Proof Explorer


Theorem 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 φ D ∞Met X
xblss2.2 φ P X
xblss2.3 φ Q X
xblss2.4 φ R *
xblss2.5 φ S *
xblss2.6 φ P D Q
xblss2.7 φ P D Q S + 𝑒 R
Assertion xblss2 φ P ball D R Q ball D S

Proof

Step Hyp Ref Expression
1 xblss2.1 φ D ∞Met X
2 xblss2.2 φ P X
3 xblss2.3 φ Q X
4 xblss2.4 φ R *
5 xblss2.5 φ S *
6 xblss2.6 φ P D Q
7 xblss2.7 φ P D Q S + 𝑒 R
8 elbl D ∞Met X P X R * x P ball D R x X P D x < R
9 1 2 4 8 syl3anc φ x P ball D R x X P D x < R
10 9 simprbda φ x P ball D R x X
11 1 adantr φ x P ball D R D ∞Met X
12 3 adantr φ x P ball D R Q X
13 xmetcl D ∞Met X Q X x X Q D x *
14 11 12 10 13 syl3anc φ x P ball D R Q D x *
15 14 adantr φ x P ball D R R Q D x *
16 6 adantr φ x P ball D R P D Q
17 16 rexrd φ x P ball D R P D Q *
18 4 adantr φ x P ball D R R *
19 17 18 xaddcld φ x P ball D R P D Q + 𝑒 R *
20 19 adantr φ x P ball D R R P D Q + 𝑒 R *
21 5 ad2antrr φ x P ball D R R S *
22 2 adantr φ x P ball D R P X
23 xmetcl D ∞Met X P X x X P D x *
24 11 22 10 23 syl3anc φ x P ball D R P D x *
25 17 24 xaddcld φ x P ball D R P D Q + 𝑒 P D x *
26 xmettri2 D ∞Met X P X Q X x X Q D x P D Q + 𝑒 P D x
27 11 22 12 10 26 syl13anc φ x P ball D R Q D x P D Q + 𝑒 P D x
28 9 simplbda φ x P ball D R P D x < R
29 xltadd2 P D x * R * P D Q P D x < R P D Q + 𝑒 P D x < P D Q + 𝑒 R
30 24 18 16 29 syl3anc φ x P ball D R P D x < R P D Q + 𝑒 P D x < P D Q + 𝑒 R
31 28 30 mpbid φ x P ball D R P D Q + 𝑒 P D x < P D Q + 𝑒 R
32 14 25 19 27 31 xrlelttrd φ x P ball D R Q D x < P D Q + 𝑒 R
33 32 adantr φ x P ball D R R Q D x < P D Q + 𝑒 R
34 5 adantr φ x P ball D R S *
35 18 xnegcld φ x P ball D R R *
36 34 35 xaddcld φ x P ball D R S + 𝑒 R *
37 7 adantr φ x P ball D R P D Q S + 𝑒 R
38 xleadd1a P D Q * S + 𝑒 R * R * P D Q S + 𝑒 R P D Q + 𝑒 R S + 𝑒 R + 𝑒 R
39 17 36 18 37 38 syl31anc φ x P ball D R P D Q + 𝑒 R S + 𝑒 R + 𝑒 R
40 39 adantr φ x P ball D R R P D Q + 𝑒 R S + 𝑒 R + 𝑒 R
41 xnpcan S * R S + 𝑒 R + 𝑒 R = S
42 34 41 sylan φ x P ball D R R S + 𝑒 R + 𝑒 R = S
43 40 42 breqtrd φ x P ball D R R P D Q + 𝑒 R S
44 15 20 21 33 43 xrltletrd φ x P ball D R R Q D x < S
45 28 adantr φ x P ball D R R = +∞ P D x < R
46 7 ad2antrr φ x P ball D R R = +∞ P D Q S + 𝑒 R
47 0xr 0 *
48 47 a1i φ x P ball D R 0 *
49 xmetge0 D ∞Met X P X Q X 0 P D Q
50 11 22 12 49 syl3anc φ x P ball D R 0 P D Q
51 48 17 36 50 37 xrletrd φ x P ball D R 0 S + 𝑒 R
52 ge0nemnf S + 𝑒 R * 0 S + 𝑒 R S + 𝑒 R −∞
53 36 51 52 syl2anc φ x P ball D R S + 𝑒 R −∞
54 53 adantr φ x P ball D R R = +∞ S + 𝑒 R −∞
55 5 ad2antrr φ x P ball D R R = +∞ S *
56 xaddmnf1 S * S +∞ S + 𝑒 −∞ = −∞
57 56 ex S * S +∞ S + 𝑒 −∞ = −∞
58 55 57 syl φ x P ball D R R = +∞ S +∞ S + 𝑒 −∞ = −∞
59 simpr φ x P ball D R R = +∞ R = +∞
60 xnegeq R = +∞ R = +∞
61 59 60 syl φ x P ball D R R = +∞ R = +∞
62 xnegpnf +∞ = −∞
63 61 62 eqtrdi φ x P ball D R R = +∞ R = −∞
64 63 oveq2d φ x P ball D R R = +∞ S + 𝑒 R = S + 𝑒 −∞
65 64 eqeq1d φ x P ball D R R = +∞ S + 𝑒 R = −∞ S + 𝑒 −∞ = −∞
66 58 65 sylibrd φ x P ball D R R = +∞ S +∞ S + 𝑒 R = −∞
67 66 necon1d φ x P ball D R R = +∞ S + 𝑒 R −∞ S = +∞
68 54 67 mpd φ x P ball D R R = +∞ S = +∞
69 68 63 oveq12d φ x P ball D R R = +∞ S + 𝑒 R = +∞ + 𝑒 −∞
70 pnfaddmnf +∞ + 𝑒 −∞ = 0
71 69 70 eqtrdi φ x P ball D R R = +∞ S + 𝑒 R = 0
72 46 71 breqtrd φ x P ball D R R = +∞ P D Q 0
73 50 biantrud φ x P ball D R P D Q 0 P D Q 0 0 P D Q
74 xrletri3 P D Q * 0 * P D Q = 0 P D Q 0 0 P D Q
75 17 47 74 sylancl φ x P ball D R P D Q = 0 P D Q 0 0 P D Q
76 xmeteq0 D ∞Met X P X Q X P D Q = 0 P = Q
77 11 22 12 76 syl3anc φ x P ball D R P D Q = 0 P = Q
78 73 75 77 3bitr2d φ x P ball D R P D Q 0 P = Q
79 78 adantr φ x P ball D R R = +∞ P D Q 0 P = Q
80 72 79 mpbid φ x P ball D R R = +∞ P = Q
81 80 oveq1d φ x P ball D R R = +∞ P D x = Q D x
82 59 68 eqtr4d φ x P ball D R R = +∞ R = S
83 45 81 82 3brtr3d φ x P ball D R R = +∞ Q D x < S
84 xmetge0 D ∞Met X P X x X 0 P D x
85 11 22 10 84 syl3anc φ x P ball D R 0 P D x
86 48 24 18 85 28 xrlelttrd φ x P ball D R 0 < R
87 48 18 86 xrltled φ x P ball D R 0 R
88 ge0nemnf R * 0 R R −∞
89 18 87 88 syl2anc φ x P ball D R R −∞
90 18 89 jca φ x P ball D R R * R −∞
91 xrnemnf R * R −∞ R R = +∞
92 90 91 sylib φ x P ball D R R R = +∞
93 44 83 92 mpjaodan φ x P ball D R Q D x < S
94 elbl D ∞Met X Q X S * x Q ball D S x X Q D x < S
95 11 12 34 94 syl3anc φ x P ball D R x Q ball D S x X Q D x < S
96 10 93 95 mpbir2and φ x P ball D R x Q ball D S
97 96 ex φ x P ball D R x Q ball D S
98 97 ssrdv φ P ball D R Q ball D S