bldisj - Intuitionistic Logic Explorer

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

Theorem bldisj 14569

Description: Two balls are disjoint if the center-to-center distance is more than the sum of the radii. (Contributed by Mario Carneiro, 30-Dec-2013.)

**Assertion**
Ref	Expression
bldisj	$/\$ $/\$ $/\$ $/\$ $/\$

Proof of Theorem bldisj Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpr3 1007	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
2		simpr1 1005	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
3		simpr2 1006	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
4	2, 3	xaddcld 9950	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
5		xmetcl 14520	. . . . . 6 $/\$ $/\$
6	5	adantr 276	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
7		xrlenlt 8084	. . . . 5 $/\$
8	4, 6, 7	syl2anc 411	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
9	1, 8	mpbid 147	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
10		elin 3342	. . . 4 $/\$
11		simpl1 1002	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
12		simpl2 1003	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
13		elbl 14559	. . . . . . . 8 $/\$ $/\$ $/\$
14	11, 12, 2, 13	syl3anc 1249	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
15		simpl3 1004	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
16		elbl 14559	. . . . . . . 8 $/\$ $/\$ $/\$
17	11, 15, 3, 16	syl3anc 1249	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
18	14, 17	anbi12d 473	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
19		anandi 590	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
20	18, 19	bitr4di 198	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
21	11	adantr 276	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
22	12	adantr 276	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
23		simpr 110	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
24		xmetcl 14520	. . . . . . . . 9 $/\$ $/\$
25	21, 22, 23, 24	syl3anc 1249	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
26	15	adantr 276	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
27		xmetcl 14520	. . . . . . . . 9 $/\$ $/\$
28	21, 26, 23, 27	syl3anc 1249	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
29	2	adantr 276	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
30	3	adantr 276	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
31		xlt2add 9946	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
32	25, 28, 29, 30, 31	syl22anc 1250	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
33		xmettri3 14542	. . . . . . . . 9 $/\$ $/\$ $/\$
34	21, 22, 26, 23, 33	syl13anc 1251	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
35	6	adantr 276	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
36	25, 28	xaddcld 9950	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
37	4	adantr 276	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
38		xrlelttr 9872	. . . . . . . . 9 $/\$ $/\$ $/\$
39	35, 36, 37, 38	syl3anc 1249	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
40	34, 39	mpand 429	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
41	32, 40	syld 45	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
42	41	expimpd 363	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
43	20, 42	sylbid 150	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
44	10, 43	biimtrid 152	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
45	9, 44	mtod 664	. 2 $/\$ $/\$ $/\$ $/\$ $/\$
46	45	eq0rdv 3491	1 $/\$ $/\$ $/\$ $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104

wb 105 $/\$ w3a 980

wceq 1364

wcel 2164

cin 3152

c0 3446 class class class wbr 4029

cfv 5254 (class class class)co 5918

cxr 8053

clt 8054

cle 8055

cxad 9836

cxmet 14032

cbl 14034

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-13 2166 ax-14 2167 ax-ext 2175 ax-sep 4147 ax-pow 4203 ax-pr 4238 ax-un 4464 ax-setind 4569 ax-cnex 7963 ax-resscn 7964 ax-1cn 7965 ax-1re 7966 ax-icn 7967 ax-addcl 7968 ax-addrcl 7969 ax-mulcl 7970 ax-addcom 7972 ax-addass 7974 ax-i2m1 7977 ax-0id 7980 ax-rnegex 7981 ax-pre-ltirr 7984 ax-pre-ltwlin 7985 ax-pre-lttrn 7986 ax-pre-apti 7987 ax-pre-ltadd 7988

This theorem depends on definitions: df-bi 117 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1472 df-sb 1774 df-eu 2045 df-mo 2046 df-clab 2180 df-cleq 2186 df-clel 2189 df-nfc 2325 df-ne 2365 df-nel 2460 df-ral 2477 df-rex 2478 df-rab 2481 df-v 2762 df-sbc 2986 df-csb 3081 df-dif 3155 df-un 3157 df-in 3159 df-ss 3166 df-nul 3447 df-if 3558 df-pw 3603 df-sn 3624 df-pr 3625 df-op 3627 df-uni 3836 df-iun 3914 df-br 4030 df-opab 4091 df-mpt 4092 df-id 4324 df-po 4327 df-iso 4328 df-xp 4665 df-rel 4666 df-cnv 4667 df-co 4668 df-dm 4669 df-rn 4670 df-res 4671 df-ima 4672 df-iota 5215 df-fun 5256 df-fn 5257 df-f 5258 df-fv 5262 df-ov 5921 df-oprab 5922 df-mpo 5923 df-1st 6193 df-2nd 6194 df-map 6704 df-pnf 8056 df-mnf 8057 df-xr 8058 df-ltxr 8059 df-le 8060 df-xadd 9839 df-psmet 14039 df-xmet 14040 df-bl 14042

This theorem is referenced by: bl2in 14571

W3C validator