Metamath Proof Explorer

Theorem blcntrps

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

Proof

Step	Hyp	Ref	Expression
1		rpxr	$⊢ R \in ℝ^{+} \to R \in ℝ^{*}$
2		rpgt0	$⊢ R \in ℝ^{+} \to 0 < R$
3	1 2	jca	$⊢ R \in ℝ^{+} \to (R \in ℝ^{*} \land 0 < R)$
4		xblcntrps	$⊢ (D \in PsMet (X) \land P \in X \land (R \in ℝ^{*} \land 0 < R)) \to P \in (P ball (D) R)$
5	3 4	syl3an3	$⊢ (D \in PsMet (X) \land P \in X \land R \in ℝ^{+}) \to P \in (P ball (D) R)$