Metamath Proof Explorer

Theorem elbl2ps

Description: Membership in a ball. (Contributed by NM, 9-Mar-2007) (Revised by Thierry Arnoux, 11-Mar-2018)

Ref Expression
Assertion elbl2ps ⊢ D ∈ PsMet ⁡ X ∧ R ∈ ℝ * ∧ P ∈ X ∧ A ∈ X → A ∈ P ball ⁡ D R ↔ P D A < R

Proof

Step Hyp Ref Expression
1 simprr ⊢ D ∈ PsMet ⁡ X ∧ R ∈ ℝ * ∧ P ∈ X ∧ A ∈ X → A ∈ X
2 elblps ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X ∧ R ∈ ℝ * → A ∈ P ball ⁡ D R ↔ A ∈ X ∧ P D A < R
3 2 3expa ⊢ D ∈ PsMet ⁡ X ∧ P ∈ X ∧ R ∈ ℝ * → A ∈ P ball ⁡ D R ↔ A ∈ X ∧ P D A < R
4 3 an32s ⊢ D ∈ PsMet ⁡ X ∧ R ∈ ℝ * ∧ P ∈ X → A ∈ P ball ⁡ D R ↔ A ∈ X ∧ P D A < R
5 4 adantrr ⊢ D ∈ PsMet ⁡ X ∧ R ∈ ℝ * ∧ P ∈ X ∧ A ∈ X → A ∈ P ball ⁡ D R ↔ A ∈ X ∧ P D A < R
6 1 5 mpbirand ⊢ D ∈ PsMet ⁡ X ∧ R ∈ ℝ * ∧ P ∈ X ∧ A ∈ X → A ∈ P ball ⁡ D R ↔ P D A < R