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 \in PsMet (X) \land P \in X \land (R \in ℝ^{*} \land 0 < R)) \to P \in (P ball (D) R)$

Proof

Step	Hyp	Ref	Expression
1		simp2	$⊢ (D \in PsMet (X) \land P \in X \land (R \in ℝ^{*} \land 0 < R)) \to P \in X$
2		psmet0	$⊢ (D \in PsMet (X) \land P \in X) \to P D P = 0$
3	2	3adant3	$⊢ (D \in PsMet (X) \land P \in X \land (R \in ℝ^{*} \land 0 < R)) \to P D P = 0$
4		simp3r	$⊢ (D \in PsMet (X) \land P \in X \land (R \in ℝ^{*} \land 0 < R)) \to 0 < R$
5	3 4	eqbrtrd	$⊢ (D \in PsMet (X) \land P \in X \land (R \in ℝ^{*} \land 0 < R)) \to P D P < R$
6		elblps	$⊢ (D \in PsMet (X) \land P \in X \land R \in ℝ^{*}) \to (P \in (P ball (D) R) \leftrightarrow (P \in X \land P D P < R))$
7	6	3adant3r	$⊢ (D \in PsMet (X) \land P \in X \land (R \in ℝ^{*} \land 0 < R)) \to (P \in (P ball (D) R) \leftrightarrow (P \in X \land P D P < R))$
8	1 5 7	mpbir2and	$⊢ (D \in PsMet (X) \land P \in X \land (R \in ℝ^{*} \land 0 < R)) \to P \in (P ball (D) R)$