Theorem bl2in 7840

Description: Two balls are disjoint if they don't overlap.

Hypothesis

Ref	Expression
blval.1	|- X = dom dom D

Assertion

Ref	Expression
bl2in	|- (((D e. Met /\ P e. X /\ Q e. X) /\ (R e. RR /\ 0 < R /\ R <_ ((PDQ) / 2))) -> ((P( ball ` D)R) i^i (Q( ball ` D)R)) = (/))

Proof of Theorem bl2in

Step	Hyp	Ref	Expression
1		blval.1	. . . . . 6 |- X = dom dom D
2	1	elbl 7835	. . . . 5 |- (((D e. Met /\ P e. X) /\ (R e. RR /\ 0 < R)) -> (x e. (P( ball ` D)R) <-> (x e. X /\ (PDx) < R)))
3		3simpa 787	. . . . 5 |- ((D e. Met /\ P e. X /\ Q e. X) -> (D e. Met /\ P e. X))
4		3simpa 787	. . . . 5 |- ((R e. RR /\ 0 < R /\ R <_ ((PDQ) / 2)) -> (R e. RR /\ 0 < R))
5	2, 3, 4	syl2an 456	. . . 4 |- (((D e. Met /\ P e. X /\ Q e. X) /\ (R e. RR /\ 0 < R /\ R <_ ((PDQ) / 2))) -> (x e. (P( ball ` D)R) <-> (x e. X /\ (PDx) < R)))
6		axaddrcl 5284	. . . . . . . . . . . . . 14 |- (((PDx) e. RR /\ (QDx) e. RR) -> ((PDx) + (QDx)) e. RR)
7	1	metcl 7808	. . . . . . . . . . . . . . . 16 |- ((D e. Met /\ P e. X /\ x e. X) -> (PDx) e. RR)
8	7	3expa 835	. . . . . . . . . . . . . . 15 |- (((D e. Met /\ P e. X) /\ x e. X) -> (PDx) e. RR)
9	8	3adantl3 807	. . . . . . . . . . . . . 14 |- (((D e. Met /\ P e. X /\ Q e. X) /\ x e. X) -> (PDx) e. RR)
10	1	metcl 7808	. . . . . . . . . . . . . . . 16 |- ((D e. Met /\ Q e. X /\ x e. X) -> (QDx) e. RR)
11	10	3expa 835	. . . . . . . . . . . . . . 15 |- (((D e. Met /\ Q e. X) /\ x e. X) -> (QDx) e. RR)
12	11	3adantl2 806	. . . . . . . . . . . . . 14 |- (((D e. Met /\ P e. X /\ Q e. X) /\ x e. X) -> (QDx) e. RR)
13	6, 9, 12	sylanc 473	. . . . . . . . . . . . 13 |- (((D e. Met /\ P e. X /\ Q e. X) /\ x e. X) -> ((PDx) + (QDx)) e. RR)
14	13	adantr 391	. . . . . . . . . . . 12 |- ((((D e. Met /\ P e. X /\ Q e. X) /\ x e. X) /\ (R e. RR /\ 0 < R /\ R <_ ((PDQ) / 2))) -> ((PDx) + (QDx)) e. RR)
15	14	ad2antrr 406	. . . . . . . . . . 11 |- ((((((D e. Met /\ P e. X /\ Q e. X) /\ x e. X) /\ (R e. RR /\ 0 < R /\ R <_ ((PDQ) / 2))) /\ (PDx) < R) /\ (QDx) < R) -> ((PDx) + (QDx)) e. RR)
16		2re 5981	. . . . . . . . . . . . . . 15 |- 2 e. RR
17		axmulrcl 5286	. . . . . . . . . . . . . . 15 |- ((2 e. RR /\ R e. RR) -> (2 x. R) e. RR)
18	16, 17	mpan 697	. . . . . . . . . . . . . 14 |- (R e. RR -> (2 x. R) e. RR)
19	18	3ad2ant1 802	. . . . . . . . . . . . 13 |- ((R e. RR /\ 0 < R /\ R <_ ((PDQ) / 2)) -> (2 x. R) e. RR)
20	19	adantl 390	. . . . . . . . . . . 12 |- ((((D e. Met /\ P e. X /\ Q e. X) /\ x e. X) /\ (R e. RR /\ 0 < R /\ R <_ ((PDQ) / 2))) -> (2 x. R) e. RR)
21	20	ad2antrr 406	. . . . . . . . . . 11 |- ((((((D e. Met /\ P e. X /\ Q e. X) /\ x e. X) /\ (R e. RR /\ 0 < R /\ R <_ ((PDQ) / 2))) /\ (PDx) < R) /\ (QDx) < R) -> (2 x. R) e. RR)
22	1	metcl 7808	. . . . . . . . . . . . 13 |- ((D e. Met /\ P e. X /\ Q e. X) -> (PDQ) e. RR)
23	22	ad2antrr 406	. . . . . . . . . . . 12 |- ((((D e. Met /\ P e. X /\ Q e. X) /\ x e. X) /\ (R e. RR /\ 0 < R /\ R <_ ((PDQ) / 2))) -> (PDQ) e. RR)
24	23	ad2antrr 406	. . . . . . . . . . 11 |- ((((((D e. Met /\ P e. X /\ Q e. X) /\ x e. X) /\ (R e. RR /\ 0 < R /\ R <_ ((PDQ) / 2))) /\ (PDx) < R) /\ (QDx) < R) -> (PDQ) e. RR)
25		lt2addt 5655	. . . . . . . . . . . . . . 15 |- ((((PDx) e. RR /\ (QDx) e. RR) /\ (R e. RR /\ R e. RR)) -> (((PDx) < R /\ (QDx) < R) -> ((PDx) + (QDx)) < (R + R)))
26	9, 12	jca 288	. . . . . . . . . . . . . . 15 |- (((D e. Met /\ P e. X /\ Q e. X) /\ x e. X) -> ((PDx) e. RR /\ (QDx) e. RR))
27		3simp1 790	. . . . . . . . . . . . . . . 16 |- ((R e. RR /\ 0 < R /\ R <_ ((PDQ) / 2)) -> R e. RR)
28	27, 27	jca 288	. . . . . . . . . . . . . . 15 |- ((R e. RR /\ 0 < R /\ R <_ ((PDQ) / 2)) -> (R e. RR /\ R e. RR))
29	25, 26, 28	syl2an 456	. . . . . . . . . . . . . 14 |- ((((D e. Met /\ P e. X /\ Q e. X) /\ x e. X) /\ (R e. RR /\ 0 < R /\ R <_ ((PDQ) / 2))) -> (((PDx) < R /\ (QDx) < R) -> ((PDx) + (QDx)) < (R + R)))
30	29	exp3a 376	. . . . . . . . . . . . 13 |- ((((D e. Met /\ P e. X /\ Q e. X) /\ x e. X) /\ (R e. RR /\ 0 < R /\ R <_ ((PDQ) / 2))) -> ((PDx) < R -> ((QDx) < R -> ((PDx) + (QDx)) < (R + R))))
31	30	imp31 362	. . . . . . . . . . . 12 |- ((((((D e. Met /\ P e. X /\ Q e. X) /\ x e. X) /\ (R e. RR /\ 0 < R /\ R <_ ((PDQ) / 2))) /\ (PDx) < R) /\ (QDx) < R) -> ((PDx) + (QDx)) < (R + R))
32		recnt 5325	. . . . . . . . . . . . . . . 16 |- (R e. RR -> R e. CC)
33		2timest 6006	. . . . . . . . . . . . . . . 16 |- (R e. CC -> (2 x. R) = (R + R))
34	32, 33	syl 10	. . . . . . . . . . . . . . 15 |- (R e. RR -> (2 x. R) = (R + R))
35	34	3ad2ant1 802	. . . . . . . . . . . . . 14 |- ((R e. RR /\ 0 < R /\ R <_ ((PDQ) / 2)) -> (2 x. R) = (R + R))
36	35	adantl 390	. . . . . . . . . . . . 13 |- ((((D e. Met /\ P e. X /\ Q e. X) /\ x e. X) /\ (R e. RR /\ 0 < R /\ R <_ ((PDQ) / 2))) -> (2 x. R) = (R + R))
37	36	ad2antrr 406	. . . . . . . . . . . 12 |- ((((((D e. Met /\ P e. X /\ Q e. X) /\ x e. X) /\ (R e. RR /\ 0 < R /\ R <_ ((PDQ) / 2))) /\ (PDx) < R) /\ (QDx) < R) -> (2 x. R) = (R + R))
38	31, 37	breqtrrd 2646	. . . . . . . . . . 11 |- ((((((D e. Met /\ P e. X /\ Q e. X) /\ x e. X) /\ (R e. RR /\ 0 < R /\ R <_ ((PDQ) / 2))) /\ (PDx) < R) /\ (QDx) < R) -> ((PDx) + (QDx)) < (2 x. R))
39		2pos 5991	. . . . . . . . . . . . . . . . . . . 20 |- 0 < 2
40		lemuldiv2tOLD 5879	. . . . . . . . . . . . . . . . . . . 20 |- (((2 e. RR /\ R e. RR /\ (PDQ) e. RR) /\ 0 < 2) -> ((2 x. R) <_ (PDQ) <-> R <_ ((PDQ) / 2)))
41	39, 40	mpan2 698	. . . . . . . . . . . . . . . . . . 19 |- ((2 e. RR /\ R e. RR /\ (PDQ) e. RR) -> ((2 x. R) <_ (PDQ) <-> R <_ ((PDQ) / 2)))
42	16, 41	mp3an1 905	. . . . . . . . . . . . . . . . . 18 |- ((R e. RR /\ (PDQ) e. RR) -> ((2 x. R) <_ (PDQ) <-> R <_ ((PDQ) / 2)))
43	42	biimpar 419	. . . . . . . . . . . . . . . . 17 |- (((R e. RR /\ (PDQ) e. RR) /\ R <_ ((PDQ) / 2)) -> (2 x. R) <_ (PDQ))
44	43	ancom1s 492	. . . . . . . . . . . . . . . 16 |- ((((PDQ) e. RR /\ R e. RR) /\ R <_ ((PDQ) / 2)) -> (2 x. R) <_ (PDQ))
45	44	anasss 442	. . . . . . . . . . . . . . 15 |- (((PDQ) e. RR /\ (R e. RR /\ R <_ ((PDQ) / 2))) -> (2 x. R) <_ (PDQ))
46	45, 22	sylan 450	. . . . . . . . . . . . . 14 |- (((D e. Met /\ P e. X /\ Q e. X) /\ (R e. RR /\ R <_ ((PDQ) / 2))) -> (2 x. R) <_ (PDQ))
47	46	3adantr2 809	. . . . . . . . . . . . 13 |- (((D e. Met /\ P e. X /\ Q e. X) /\ (R e. RR /\ 0 < R /\ R <_ ((PDQ) / 2))) -> (2 x. R) <_ (PDQ))
48	47	adantlr 395	. . . . . . . . . . . 12 |- ((