This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xblcntrps

Description: A ball contains its center. (Contributed by NM, 2-Sep-2006) (Revised by Mario Carneiro, 12-Nov-2013) (Revised by Thierry Arnoux, 11-Mar-2018)

Ref Expression
Assertion xblcntrps ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X ∧ R ∈ ℝ * ∧ 0 < R → P ∈ P ball ⁡ D R

Proof

Step Hyp Ref Expression
1 simp2 ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X ∧ R ∈ ℝ * ∧ 0 < R → P ∈ X
2 psmet0 ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X → P D P = 0
3 2 3adant3 ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X ∧ R ∈ ℝ * ∧ 0 < R → P D P = 0
4 simp3r ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X ∧ R ∈ ℝ * ∧ 0 < R → 0 < R
5 3 4 eqbrtrd ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X ∧ R ∈ ℝ * ∧ 0 < R → P D P < R
6 elblps ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X ∧ R ∈ ℝ * → P ∈ P ball ⁡ D R ↔ P ∈ X ∧ P D P < R
7 6 3adant3r ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X ∧ R ∈ ℝ * ∧ 0 < R → P ∈ P ball ⁡ D R ↔ P ∈ X ∧ P D P < R
8 1 5 7 mpbir2and ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X ∧ R ∈ ℝ * ∧ 0 < R → P ∈ P ball ⁡ D R