HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem bl2in 7795
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
StepHypRef Expression
1 blval.1 . . . . . 6 |- X = dom dom D
21elbl 7790 . . . . 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 784 . . . . 5 |- ((D e. Met /\ P e. X /\ Q e. X) -> (D e. Met /\ P e. X))
4 3simpa 784 . . . . 5 |- ((R e. RR /\ 0 < R /\ R <_ ((PDQ) / 2)) -> (R e. RR /\ 0 < R))
52, 3, 4syl2an 454 . . . 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 5252 . . . . . . . . . . . . . . 15 |- (((PDx) e. RR /\ (QDx) e. RR) -> ((PDx) + (QDx)) e. RR)
71metcl 7761 . . . . . . . . . . . . . . . . 17 |- ((D e. Met /\ P e. X /\ x e. X) -> (PDx) e. RR)
873expa 832 . . . . . . . . . . . . . . . 16 |- (((D e. Met /\ P e. X) /\ x e. X) -> (PDx) e. RR)
983adantl3 804 . . . . . . . . . . . . . . 15 |- (((D e. Met /\ P e. X /\ Q e. X) /\ x e. X) -> (PDx) e. RR)
101metcl 7761 . . . . . . . . . . . . . . . . 17 |- ((D e. Met /\ Q e. X /\ x e. X) -> (QDx) e. RR)
11103expa 832 . . . . . . . . . . . . . . . 16 |- (((D e. Met /\ Q e. X) /\ x e. X) -> (QDx) e. RR)
12113adantl2 803 . . . . . . . . . . . . . . 15 |- (((D e. Met /\ P e. X /\ Q e. X) /\ x e. X) -> (QDx) e. RR)
136, 9, 12sylanc 471 . . . . . . . . . . . . . 14 |- (((D e. Met /\ P e. X /\ Q e. X) /\ x e. X) -> ((PDx) + (QDx)) e. RR)
1413adantr 389 . . . . . . . . . . . . 13 |- ((((D e. Met /\ P e. X /\ Q e. X) /\ x e. X) /\ (R e. RR /\ 0 < R /\ R <_ ((PDQ) / 2))) -> ((PDx) + (QDx)) e. RR)
1514ad2antrr 404 . . . . . . . . . . . 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)) e. RR)
16 2re 5934 . . . . . . . . . . . . . . . 16 |- 2 e. RR
17 axmulrcl 5254 . . . . . . . . . . . . . . . 16 |- ((2 e. RR /\ R e. RR) -> (2 x. R) e. RR)
1816, 17mpan 694 . . . . . . . . . . . . . . 15 |- (R e. RR -> (2 x. R) e. RR)
19183ad2ant1 799 . . . . . . . . . . . . . 14 |- ((R e. RR /\ 0 < R /\ R <_ ((PDQ) / 2)) -> (2 x. R) e. RR)
2019adantl 388 . . . . . . . . . . . . 13 |- ((((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)
2120ad2antrr 404 . . . . . . . . . . . 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) e. RR)
221metcl 7761 . . . . . . . . . . . . . 14 |- ((D e. Met /\ P e. X /\ Q e. X) -> (PDQ) e. RR)
2322ad2antrr 404 . . . . . . . . . . . . 13 |- ((((D e. Met /\ P e. X /\ Q e. X) /\ x e. X) /\ (R e. RR /\ 0 < R /\ R <_ ((PDQ) / 2))) -> (PDQ) e. RR)
2423ad2antrr 404 . . . . . . . . . . . 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) -> (PDQ) e. RR)
25 lt2addt 5625 . . . . . . . . . . . . . . . 16 |- ((((PDx) e. RR /\ (QDx) e. RR) /\ (R e. RR /\ R e. RR)) -> (((PDx) < R /\ (QDx) < R) -> ((PDx) + (QDx)) < (R + R)))
269, 12jca 288 . . . . . . . . . . . . . . . 16 |- (((D e. Met /\ P e. X /\ Q e. X) /\ x e. X) -> ((PDx) e. RR /\ (QDx) e. RR))
27 3simp1 787 . . . . . . . . . . . . . . . . 17 |- ((R e. RR /\ 0 < R /\ R <_ ((PDQ) / 2)) -> R e. RR)
2827, 27jca 288 . . . . . . . . . . . . . . . 16 |- ((R e. RR /\ 0 < R /\ R <_ ((PDQ) / 2)) -> (R e. RR /\ R e. RR))
2925, 26, 28syl2an 454 . . . . . . . . . . . . . . 15 |- ((((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)))
3029exp3a 375 . . . . . . . . . . . . . 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))))
3130imp31 362 . . . . . . . . . . . . 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))
32 recnt 5293 . . . . . . . . . . . . . . . . 17 |- (R e. RR -> R e. CC)
33 2timest 5959 . . . . . . . . . . . . . . . . 17 |- (R e. CC -> (2 x. R) = (R + R))
3432, 33syl 10 . . . . . . . . . . . . . . . 16 |- (R e. RR -> (2 x. R) = (R + R))
35343ad2ant1 799 . . . . . . . . . . . . . . 15 |- ((R e. RR /\ 0 < R /\ R <_ ((PDQ) / 2)) -> (2 x. R) = (R + R))
3635adantl 388 . . . . . . . . . . . . . 14 |- ((((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))
3736ad2antrr 404 . . . . . . . . . . . . 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) -> (2 x. R) = (R + R))
3831, 37breqtrrd 2636 . . . . . . . . . . . 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)) < (2 x. R))
39 2pos 5944 . . . . . . . . . . . . . . . . . . . . 21 |- 0 < 2
40 lemuldiv2t 5833 . . . . . . . . . . . . . . . . . . . . 21 |- (((2 e. RR /\ R e. RR /\ (PDQ) e. RR) /\ 0 < 2) -> ((2 x. R) <_ (PDQ) <-> R <_ ((PDQ) / 2)))
4139, 40mpan2 695 . . . . . . . . . . . . . . . . . . . 20 |- ((2 e. RR /\ R e. RR /\ (PDQ) e. RR) -> ((2 x. R) <_ (PDQ) <-> R <_ ((PDQ) / 2)))
4216, 41mp3an1 901 . . . . . . . . . . . . . . . . . . 19 |- ((R e. RR /\ (PDQ) e. RR) -> ((2 x. R) <_ (PDQ) <-> R <_ ((PDQ) / 2)))
4342biimpar 417 . . . . . . . . . . . . . . . . . 18 |- (((R e. RR /\ (PDQ) e. RR) /\ R <_ ((PDQ) / 2)) -> (2 x. R) <_ (PDQ))
4443ancom1s 490 . . . . . . . . . . . . . . . . 17 |- ((((PDQ) e. RR /\ R e. RR) /\ R <_ ((PDQ) / 2)) -> (2 x. R) <_ (PDQ))
4544anasss 440 . . . . . . . . . . . . . . . 16 |- (((PDQ) e. RR /\ (R e. RR /\ R <_ ((PDQ) / 2))) -> (2 x. R) <_ (PDQ))
4645, 22sylan 448 . . . . . . . . . . . . . . 15 |- (((D e. Met /\ P e. X /\ Q e. X) /\ (R e. RR /\ R <_ ((PDQ) / 2))) -> (2 x. R) <_ (PDQ))
47463adantr2 806 . . . . . . . . . . . . . 14 |- (((D e. Met /\ P e. X /\ Q e. X) /\ (R e. RR /\ 0 < R /\ R <_ ((PDQ) / 2))) -> (2 x. R) <_ (PDQ))
4847adantlr 393 . . . . . . . . . . . . 13 |- ((