blgt0

Description: A nonempty ball implies that the radius is positive. (Contributed by NM, 11-Mar-2007) (Revised by Mario Carneiro, 23-Aug-2015)

		Ref	Expression
	Assertion	blgt0	$⊢ ((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land A \in (P ball (D) R)) \to 0 < R$

Step	Hyp	Ref	Expression
1		0xr	$⊢ 0 \in ℝ^{*}$
2	1	a1i	$⊢ ((D \in ∞Met (X) \land P \in X \land R \in ℝ^{}) \land A \in (P ball (D) R)) \to 0 \in ℝ^{}$
3		simpl1	$⊢ ((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land A \in (P ball (D) R)) \to D \in ∞Met (X)$
4		simpl2	$⊢ ((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land A \in (P ball (D) R)) \to P \in X$
5		elbl	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \to (A \in (P ball (D) R) \leftrightarrow (A \in X \land P D A < R))$
6	5	simprbda	$⊢ ((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land A \in (P ball (D) R)) \to A \in X$
7		xmetcl	$⊢ (D \in ∞Met (X) \land P \in X \land A \in X) \to P D A \in ℝ^{*}$
8	3 4 6 7	syl3anc	$⊢ ((D \in ∞Met (X) \land P \in X \land R \in ℝ^{}) \land A \in (P ball (D) R)) \to P D A \in ℝ^{}$
9		simpl3	$⊢ ((D \in ∞Met (X) \land P \in X \land R \in ℝ^{}) \land A \in (P ball (D) R)) \to R \in ℝ^{}$
10		xmetge0	$⊢ (D \in ∞Met (X) \land P \in X \land A \in X) \to 0 \leq P D A$
11	3 4 6 10	syl3anc	$⊢ ((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land A \in (P ball (D) R)) \to 0 \leq P D A$
12	5	simplbda	$⊢ ((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land A \in (P ball (D) R)) \to P D A < R$
13	2 8 9 11 12	xrlelttrd	$⊢ ((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land A \in (P ball (D) R)) \to 0 < R$

Metamath Proof Explorer