Metamath Proof Explorer


Theorem bl2in

Description: Two balls are disjoint if they don't overlap. (Contributed by NM, 11-Mar-2007) (Revised by Mario Carneiro, 23-Aug-2015)

Ref Expression
Assertion bl2in D Met X P X Q X R R P D Q 2 P ball D R Q ball D R =

Proof

Step Hyp Ref Expression
1 simpl1 D Met X P X Q X R R P D Q 2 D Met X
2 metxmet D Met X D ∞Met X
3 1 2 syl D Met X P X Q X R R P D Q 2 D ∞Met X
4 simpl2 D Met X P X Q X R R P D Q 2 P X
5 simpl3 D Met X P X Q X R R P D Q 2 Q X
6 rexr R R *
7 6 ad2antrl D Met X P X Q X R R P D Q 2 R *
8 simprl D Met X P X Q X R R P D Q 2 R
9 8 8 rexaddd D Met X P X Q X R R P D Q 2 R + 𝑒 R = R + R
10 8 recnd D Met X P X Q X R R P D Q 2 R
11 10 2timesd D Met X P X Q X R R P D Q 2 2 R = R + R
12 9 11 eqtr4d D Met X P X Q X R R P D Q 2 R + 𝑒 R = 2 R
13 id R R
14 metcl D Met X P X Q X P D Q
15 2re 2
16 2pos 0 < 2
17 15 16 pm3.2i 2 0 < 2
18 lemuldiv2 R P D Q 2 0 < 2 2 R P D Q R P D Q 2
19 17 18 mp3an3 R P D Q 2 R P D Q R P D Q 2
20 13 14 19 syl2anr D Met X P X Q X R 2 R P D Q R P D Q 2
21 20 biimprd D Met X P X Q X R R P D Q 2 2 R P D Q
22 21 impr D Met X P X Q X R R P D Q 2 2 R P D Q
23 12 22 eqbrtrd D Met X P X Q X R R P D Q 2 R + 𝑒 R P D Q
24 bldisj D ∞Met X P X Q X R * R * R + 𝑒 R P D Q P ball D R Q ball D R =
25 3 4 5 7 7 23 24 syl33anc D Met X P X Q X R R P D Q 2 P ball D R Q ball D R =