Metamath Proof Explorer


Theorem elbl3ps

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

Ref Expression
Assertion elbl3ps D PsMet X R * P X A X A P ball D R A D P < R

Proof

Step Hyp Ref Expression
1 elbl2ps D PsMet X R * P X A X A P ball D R P D A < R
2 psmetsym D PsMet X P X A X P D A = A D P
3 2 3expb D PsMet X P X A X P D A = A D P
4 3 adantlr D PsMet X R * P X A X P D A = A D P
5 4 breq1d D PsMet X R * P X A X P D A < R A D P < R
6 1 5 bitrd D PsMet X R * P X A X A P ball D R A D P < R