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 ( ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑅 ≤ ( ( 𝑃 𝐷 𝑄 ) / 2 ) ) ) → ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∩ ( 𝑄 ( ball ‘ 𝐷 ) 𝑅 ) ) = ∅ )

Proof

Step Hyp Ref Expression
1 simpl1 ⊢ ( ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑅 ≤ ( ( 𝑃 𝐷 𝑄 ) / 2 ) ) ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
2 metxmet ⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
3 1 2 syl ⊢ ( ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑅 ≤ ( ( 𝑃 𝐷 𝑄 ) / 2 ) ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
4 simpl2 ⊢ ( ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑅 ≤ ( ( 𝑃 𝐷 𝑄 ) / 2 ) ) ) → 𝑃 ∈ 𝑋 )
5 simpl3 ⊢ ( ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑅 ≤ ( ( 𝑃 𝐷 𝑄 ) / 2 ) ) ) → 𝑄 ∈ 𝑋 )
6 rexr ⊢ ( 𝑅 ∈ ℝ → 𝑅 ∈ ℝ* )
7 6 ad2antrl ⊢ ( ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑅 ≤ ( ( 𝑃 𝐷 𝑄 ) / 2 ) ) ) → 𝑅 ∈ ℝ* )
8 simprl ⊢ ( ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑅 ≤ ( ( 𝑃 𝐷 𝑄 ) / 2 ) ) ) → 𝑅 ∈ ℝ )
9 8 8 rexaddd ⊢ ( ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑅 ≤ ( ( 𝑃 𝐷 𝑄 ) / 2 ) ) ) → ( 𝑅 +𝑒 𝑅 ) = ( 𝑅 + 𝑅 ) )
10 8 recnd ⊢ ( ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑅 ≤ ( ( 𝑃 𝐷 𝑄 ) / 2 ) ) ) → 𝑅 ∈ ℂ )
11 10 2timesd ⊢ ( ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑅 ≤ ( ( 𝑃 𝐷 𝑄 ) / 2 ) ) ) → ( 2 · 𝑅 ) = ( 𝑅 + 𝑅 ) )
12 9 11 eqtr4d ⊢ ( ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑅 ≤ ( ( 𝑃 𝐷 𝑄 ) / 2 ) ) ) → ( 𝑅 +𝑒 𝑅 ) = ( 2 · 𝑅 ) )
13 id ⊢ ( 𝑅 ∈ ℝ → 𝑅 ∈ ℝ )
14 metcl ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) → ( 𝑃 𝐷 𝑄 ) ∈ ℝ )
15 2re ⊢ 2 ∈ ℝ
16 2pos ⊢ 0 < 2
17 15 16 pm3.2i ⊢ ( 2 ∈ ℝ ∧ 0 < 2 )
18 lemuldiv2 ⊢ ( ( 𝑅 ∈ ℝ ∧ ( 𝑃 𝐷 𝑄 ) ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( 2 · 𝑅 ) ≤ ( 𝑃 𝐷 𝑄 ) ↔ 𝑅 ≤ ( ( 𝑃 𝐷 𝑄 ) / 2 ) ) )
19 17 18 mp3an3 ⊢ ( ( 𝑅 ∈ ℝ ∧ ( 𝑃 𝐷 𝑄 ) ∈ ℝ ) → ( ( 2 · 𝑅 ) ≤ ( 𝑃 𝐷 𝑄 ) ↔ 𝑅 ≤ ( ( 𝑃 𝐷 𝑄 ) / 2 ) ) )
20 13 14 19 syl2anr ⊢ ( ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ 𝑅 ∈ ℝ ) → ( ( 2 · 𝑅 ) ≤ ( 𝑃 𝐷 𝑄 ) ↔ 𝑅 ≤ ( ( 𝑃 𝐷 𝑄 ) / 2 ) ) )
21 20 biimprd ⊢ ( ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ 𝑅 ∈ ℝ ) → ( 𝑅 ≤ ( ( 𝑃 𝐷 𝑄 ) / 2 ) → ( 2 · 𝑅 ) ≤ ( 𝑃 𝐷 𝑄 ) ) )
22 21 impr ⊢ ( ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑅 ≤ ( ( 𝑃 𝐷 𝑄 ) / 2 ) ) ) → ( 2 · 𝑅 ) ≤ ( 𝑃 𝐷 𝑄 ) )
23 12 22 eqbrtrd ⊢ ( ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑅 ≤ ( ( 𝑃 𝐷 𝑄 ) / 2 ) ) ) → ( 𝑅 +𝑒 𝑅 ) ≤ ( 𝑃 𝐷 𝑄 ) )
24 bldisj ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑅 ∈ ℝ* ∧ ( 𝑅 +𝑒 𝑅 ) ≤ ( 𝑃 𝐷 𝑄 ) ) ) → ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∩ ( 𝑄 ( ball ‘ 𝐷 ) 𝑅 ) ) = ∅ )
25 3 4 5 7 7 23 24 syl33anc ⊢ ( ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ ∧ 𝑅 ≤ ( ( 𝑃 𝐷 𝑄 ) / 2 ) ) ) → ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∩ ( 𝑄 ( ball ‘ 𝐷 ) 𝑅 ) ) = ∅ )