Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  xblss2 Unicode version

Theorem xblss2 12600
 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 12602 for extended metrics, we have to assume the balls are a finite distance apart, or else will not even be in the infinity ball around . (Contributed by Mario Carneiro, 23-Aug-2015.)
Hypotheses
Ref Expression
xblss2.1
xblss2.2
xblss2.3
xblss2.4
xblss2.5
xblss2.6
xblss2.7
Assertion
Ref Expression
xblss2

Proof of Theorem xblss2
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 xblss2.1 . . . . . 6
2 xblss2.2 . . . . . 6
3 xblss2.4 . . . . . 6
4 elbl 12586 . . . . . 6
51, 2, 3, 4syl3anc 1216 . . . . 5
65simprbda 380 . . . 4
71adantr 274 . . . . . . . 8
8 xblss2.3 . . . . . . . . 9
98adantr 274 . . . . . . . 8
10 xmetcl 12547 . . . . . . . 8
117, 9, 6, 10syl3anc 1216 . . . . . . 7
1211adantr 274 . . . . . 6
13 xblss2.6 . . . . . . . . . 10
1413adantr 274 . . . . . . . . 9
1514rexrd 7834 . . . . . . . 8
163adantr 274 . . . . . . . 8
1715, 16xaddcld 9690 . . . . . . 7
1817adantr 274 . . . . . 6
19 xblss2.5 . . . . . . 7
2019ad2antrr 479 . . . . . 6
212adantr 274 . . . . . . . . . 10
22 xmetcl 12547 . . . . . . . . . 10
237, 21, 6, 22syl3anc 1216 . . . . . . . . 9
2415, 23xaddcld 9690 . . . . . . . 8
25 xmettri2 12556 . . . . . . . . 9
267, 21, 9, 6, 25syl13anc 1218 . . . . . . . 8
275simplbda 381 . . . . . . . . 9
28 xltadd2 9683 . . . . . . . . . 10
2923, 16, 14, 28syl3anc 1216 . . . . . . . . 9
3027, 29mpbid 146 . . . . . . . 8
3111, 24, 17, 26, 30xrlelttrd 9616 . . . . . . 7
3231adantr 274 . . . . . 6
3319adantr 274 . . . . . . . . . 10
3416xnegcld 9661 . . . . . . . . . 10
3533, 34xaddcld 9690 . . . . . . . . 9
36 xblss2.7 . . . . . . . . . 10
3736adantr 274 . . . . . . . . 9
38 xleadd1a 9679 . . . . . . . . 9
3915, 35, 16, 37, 38syl31anc 1219 . . . . . . . 8
4039adantr 274 . . . . . . 7
41 xnpcan 9678 . . . . . . . 8
4233, 41sylan 281 . . . . . . 7
4340, 42breqtrd 3957 . . . . . 6
4412, 18, 20, 32, 43xrltletrd 9617 . . . . 5
4527adantr 274 . . . . . 6
4636ad2antrr 479 . . . . . . . . 9
4719ad2antrr 479 . . . . . . . . . . . . 13
48 xrpnfdc 9648 . . . . . . . . . . . . 13 DECID
4947, 48syl 14 . . . . . . . . . . . 12 DECID
50 0xr 7831 . . . . . . . . . . . . . . . 16
5150a1i 9 . . . . . . . . . . . . . . 15
52 xmetge0 12560 . . . . . . . . . . . . . . . 16
537, 21, 9, 52syl3anc 1216 . . . . . . . . . . . . . . 15
5451, 15, 35, 53, 37xrletrd 9618 . . . . . . . . . . . . . 14
55 ge0nemnf 9630 . . . . . . . . . . . . . 14
5635, 54, 55syl2anc 408 . . . . . . . . . . . . 13
5756adantr 274 . . . . . . . . . . . 12
58 xaddmnf1 9654 . . . . . . . . . . . . . . . . 17
5958ex 114 . . . . . . . . . . . . . . . 16
6047, 59syl 14 . . . . . . . . . . . . . . 15
61 simpr 109 . . . . . . . . . . . . . . . . . . 19
62 xnegeq 9633 . . . . . . . . . . . . . . . . . . 19
6361, 62syl 14 . . . . . . . . . . . . . . . . . 18
64 xnegpnf 9634 . . . . . . . . . . . . . . . . . 18
6563, 64eqtrdi 2188 . . . . . . . . . . . . . . . . 17
6665oveq2d 5793 . . . . . . . . . . . . . . . 16
6766eqeq1d 2148 . . . . . . . . . . . . . . 15
6860, 67sylibrd 168 . . . . . . . . . . . . . 14
6968a1d 22 . . . . . . . . . . . . 13 DECID
7069necon1ddc 2386 . . . . . . . . . . . 12 DECID
7149, 57, 70mp2d 47 . . . . . . . . . . 11
7271, 65oveq12d 5795 . . . . . . . . . 10
73 pnfaddmnf 9656 . . . . . . . . . 10
7472, 73eqtrdi 2188 . . . . . . . . 9
7546, 74breqtrd 3957 . . . . . . . 8
7653biantrud 302 . . . . . . . . . 10
77 xrletri3 9611 . . . . . . . . . . 11
7815, 50, 77sylancl 409 . . . . . . . . . 10
79 xmeteq0 12554 . . . . . . . . . . 11
807, 21, 9, 79syl3anc 1216 . . . . . . . . . 10
8176, 78, 803bitr2d 215 . . . . . . . . 9
8281adantr 274 . . . . . . . 8
8375, 82mpbid 146 . . . . . . 7
8483oveq1d 5792 . . . . . 6
8561, 71eqtr4d 2175 . . . . . 6
8645, 84, 853brtr3d 3962 . . . . 5
87 xmetge0 12560 . . . . . . . . . . 11
887, 21, 6, 87syl3anc 1216 . . . . . . . . . 10
8951, 23, 16, 88, 27xrlelttrd 9616 . . . . . . . . 9
9051, 16, 89xrltled 9608 . . . . . . . 8
91 ge0nemnf 9630 . . . . . . . 8
9216, 90, 91syl2anc 408 . . . . . . 7
9316, 92jca 304 . . . . . 6
94 xrnemnf 9587 . . . . . 6
9593, 94sylib 121 . . . . 5
9644, 86, 95mpjaodan 787 . . . 4
97 elbl 12586 . . . . 5
987, 9, 33, 97syl3anc 1216 . . . 4
996, 96, 98mpbir2and 928 . . 3
10099ex 114 . 2
101100ssrdv 3103 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 103   wb 104   wo 697  DECID wdc 819   wceq 1331   wcel 1480   wne 2308   wss 3071   class class class wbr 3932  cfv 5126  (class class class)co 5777  cr 7638  cc0 7639   cpnf 7816   cmnf 7817  cxr 7818   clt 7819   cle 7820   cxne 9579  cxad 9580  cxmet 12175  cbl 12177 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-sep 4049  ax-pow 4101  ax-pr 4134  ax-un 4358  ax-setind 4455  ax-cnex 7730  ax-resscn 7731  ax-1cn 7732  ax-1re 7733  ax-icn 7734  ax-addcl 7735  ax-addrcl 7736  ax-mulcl 7737  ax-mulrcl 7738  ax-addcom 7739  ax-mulcom 7740  ax-addass 7741  ax-mulass 7742  ax-distr 7743  ax-i2m1 7744  ax-0lt1 7745  ax-1rid 7746  ax-0id 7747  ax-rnegex 7748  ax-precex 7749  ax-cnre 7750  ax-pre-ltirr 7751  ax-pre-ltwlin 7752  ax-pre-lttrn 7753  ax-pre-apti 7754  ax-pre-ltadd 7755  ax-pre-mulgt0 7756 This theorem depends on definitions:  df-bi 116  df-stab 816  df-dc 820  df-3or 963  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ne 2309  df-nel 2404  df-ral 2421  df-rex 2422  df-reu 2423  df-rab 2425  df-v 2688  df-sbc 2910  df-csb 3004  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-if 3475  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3740  df-iun 3818  df-br 3933  df-opab 3993  df-mpt 3994  df-id 4218  df-po 4221  df-iso 4222  df-xp 4548  df-rel 4549  df-cnv 4550  df-co 4551  df-dm 4552  df-rn 4553  df-res 4554  df-ima 4555  df-iota 5091  df-fun 5128  df-fn 5129  df-f 5130  df-fv 5134  df-riota 5733  df-ov 5780  df-oprab 5781  df-mpo 5782  df-1st 6041  df-2nd 6042  df-map 6547  df-pnf 7821  df-mnf 7822  df-xr 7823  df-ltxr 7824  df-le 7825  df-sub 7954  df-neg 7955  df-2 8798  df-xneg 9582  df-xadd 9583  df-psmet 12182  df-xmet 12183  df-bl 12185 This theorem is referenced by:  blss2  12602  ssbl  12621
 Copyright terms: Public domain W3C validator