Metamath Proof Explorer


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

Proof

Step Hyp Ref Expression
1 xblss2ps.1 φ D PsMet X
2 xblss2ps.2 φ P X
3 xblss2ps.3 φ Q X
4 xblss2ps.4 φ R *
5 xblss2ps.5 φ S *
6 xblss2ps.6 φ P D Q
7 xblss2ps.7 φ P D Q S + 𝑒 R
8 elblps D PsMet 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 PsMet X
12 3 adantr φ x P ball D R Q X
13 psmetcl D PsMet 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 psmetcl D PsMet 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 psmettri2 D PsMet 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 14 adantr φ x P ball D R R = +∞ Q D x *
46 6 ad2antrr φ x P ball D R R = +∞ P D Q
47 simpll φ x P ball D R R = +∞ φ
48 simplr φ x P ball D R R = +∞ x P ball D R
49 simpr φ x P ball D R R = +∞ R = +∞
50 49 oveq2d φ x P ball D R R = +∞ P ball D R = P ball D +∞
51 48 50 eleqtrd φ x P ball D R R = +∞ x P ball D +∞
52 xblpnfps D PsMet X P X x P ball D +∞ x X P D x
53 1 2 52 syl2anc φ x P ball D +∞ x X P D x
54 53 simplbda φ x P ball D +∞ P D x
55 47 51 54 syl2anc φ x P ball D R R = +∞ P D x
56 46 55 readdcld φ x P ball D R R = +∞ P D Q + P D x
57 56 rexrd φ x P ball D R R = +∞ P D Q + P D x *
58 pnfxr +∞ *
59 58 a1i φ x P ball D R R = +∞ +∞ *
60 1 ad2antrr φ x P ball D R R = +∞ D PsMet X
61 2 ad2antrr φ x P ball D R R = +∞ P X
62 3 ad2antrr φ x P ball D R R = +∞ Q X
63 10 adantr φ x P ball D R R = +∞ x X
64 60 61 62 63 26 syl13anc φ x P ball D R R = +∞ Q D x P D Q + 𝑒 P D x
65 46 55 rexaddd φ x P ball D R R = +∞ P D Q + 𝑒 P D x = P D Q + P D x
66 64 65 breqtrd φ x P ball D R R = +∞ Q D x P D Q + P D x
67 56 ltpnfd φ x P ball D R R = +∞ P D Q + P D x < +∞
68 45 57 59 66 67 xrlelttrd φ x P ball D R R = +∞ Q D x < +∞
69 0xr 0 *
70 69 a1i φ x P ball D R 0 *
71 psmetge0 D PsMet X P X Q X 0 P D Q
72 11 22 12 71 syl3anc φ x P ball D R 0 P D Q
73 70 17 36 72 37 xrletrd φ x P ball D R 0 S + 𝑒 R
74 ge0nemnf S + 𝑒 R * 0 S + 𝑒 R S + 𝑒 R −∞
75 36 73 74 syl2anc φ x P ball D R S + 𝑒 R −∞
76 75 adantr φ x P ball D R R = +∞ S + 𝑒 R −∞
77 5 ad2antrr φ x P ball D R R = +∞ S *
78 xaddmnf1 S * S +∞ S + 𝑒 −∞ = −∞
79 78 ex S * S +∞ S + 𝑒 −∞ = −∞
80 77 79 syl φ x P ball D R R = +∞ S +∞ S + 𝑒 −∞ = −∞
81 xnegeq R = +∞ R = +∞
82 49 81 syl φ x P ball D R R = +∞ R = +∞
83 xnegpnf +∞ = −∞
84 82 83 eqtrdi φ x P ball D R R = +∞ R = −∞
85 84 oveq2d φ x P ball D R R = +∞ S + 𝑒 R = S + 𝑒 −∞
86 85 eqeq1d φ x P ball D R R = +∞ S + 𝑒 R = −∞ S + 𝑒 −∞ = −∞
87 80 86 sylibrd φ x P ball D R R = +∞ S +∞ S + 𝑒 R = −∞
88 87 necon1d φ x P ball D R R = +∞ S + 𝑒 R −∞ S = +∞
89 76 88 mpd φ x P ball D R R = +∞ S = +∞
90 68 89 breqtrrd φ x P ball D R R = +∞ Q D x < S
91 psmetge0 D PsMet X P X x X 0 P D x
92 11 22 10 91 syl3anc φ x P ball D R 0 P D x
93 70 24 18 92 28 xrlelttrd φ x P ball D R 0 < R
94 70 18 93 xrltled φ x P ball D R 0 R
95 ge0nemnf R * 0 R R −∞
96 18 94 95 syl2anc φ x P ball D R R −∞
97 18 96 jca φ x P ball D R R * R −∞
98 xrnemnf R * R −∞ R R = +∞
99 97 98 sylib φ x P ball D R R R = +∞
100 44 90 99 mpjaodan φ x P ball D R Q D x < S
101 elblps D PsMet X Q X S * x Q ball D S x X Q D x < S
102 11 12 34 101 syl3anc φ x P ball D R x Q ball D S x X Q D x < S
103 10 100 102 mpbir2and φ x P ball D R x Q ball D S
104 103 ex φ x P ball D R x Q ball D S
105 104 ssrdv φ P ball D R Q ball D S