Metamath Proof Explorer

Theorem elbl3

Description: Membership in a ball, with reversed distance function arguments. (Contributed by NM, 10-Nov-2007)

Ref Expression
Assertion elbl3 ⊢ D ∈ ∞Met ⁡ X ∧ R ∈ ℝ * ∧ P ∈ X ∧ A ∈ X → A ∈ P ball ⁡ D R ↔ A D P < R

Proof

Step Hyp Ref Expression
1 elbl2 ⊢ D ∈ ∞Met ⁡ X ∧ R ∈ ℝ * ∧ P ∈ X ∧ A ∈ X → A ∈ P ball ⁡ D R ↔ P D A < R
2 xmetsym ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X ∧ A ∈ X → P D A = A D P
3 2 3expb ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X ∧ A ∈ X → P D A = A D P
4 3 adantlr ⊢ D ∈ ∞Met ⁡ X ∧ R ∈ ℝ * ∧ P ∈ X ∧ A ∈ X → P D A = A D P
5 4 breq1d ⊢ D ∈ ∞Met ⁡ X ∧ R ∈ ℝ * ∧ P ∈ X ∧ A ∈ X → P D A < R ↔ A D P < R
6 1 5 bitrd ⊢ D ∈ ∞Met ⁡ X ∧ R ∈ ℝ * ∧ P ∈ X ∧ A ∈ X → A ∈ P ball ⁡ D R ↔ A D P < R