xbln0

Description: A ball is nonempty iff the radius is positive. (Contributed by Mario Carneiro, 23-Aug-2015)

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

Proof

Step	Hyp	Ref	Expression
1		n0	$⊢ P ball (D) R \neq \emptyset \leftrightarrow \exists x x \in (P ball (D) R)$
2		elbl	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \to (x \in (P ball (D) R) \leftrightarrow (x \in X \land P D x < R))$
3		xmetge0	$⊢ (D \in ∞Met (X) \land P \in X \land x \in X) \to 0 \leq P D x$
4	3	3expa	$⊢ ((D \in ∞Met (X) \land P \in X) \land x \in X) \to 0 \leq P D x$
5	4	3adantl3	$⊢ ((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land x \in X) \to 0 \leq P D x$
6		0xr	$⊢ 0 \in ℝ^{*}$
7		xmetcl	$⊢ (D \in ∞Met (X) \land P \in X \land x \in X) \to P D x \in ℝ^{*}$
8	7	3expa	$⊢ ((D \in ∞Met (X) \land P \in X) \land x \in X) \to P D x \in ℝ^{*}$
9	8	3adantl3	$⊢ ((D \in ∞Met (X) \land P \in X \land R \in ℝ^{}) \land x \in X) \to P D x \in ℝ^{}$
10		simpl3	$⊢ ((D \in ∞Met (X) \land P \in X \land R \in ℝ^{}) \land x \in X) \to R \in ℝ^{}$
11		xrlelttr	$⊢ (0 \in ℝ^{} \land P D x \in ℝ^{} \land R \in ℝ^{*}) \to ((0 \leq P D x \land P D x < R) \to 0 < R)$
12	6 9 10 11	mp3an2i	$⊢ ((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land x \in X) \to ((0 \leq P D x \land P D x < R) \to 0 < R)$
13	5 12	mpand	$⊢ ((D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \land x \in X) \to (P D x < R \to 0 < R)$
14	13	expimpd	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \to ((x \in X \land P D x < R) \to 0 < R)$
15	2 14	sylbid	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \to (x \in (P ball (D) R) \to 0 < R)$
16	15	exlimdv	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \to (\exists x x \in (P ball (D) R) \to 0 < R)$
17	1 16	syl5bi	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \to (P ball (D) R \neq \emptyset \to 0 < R)$
18		xblcntr	$⊢ (D \in ∞Met (X) \land P \in X \land (R \in ℝ^{*} \land 0 < R)) \to P \in (P ball (D) R)$
19	18	ne0d	$⊢ (D \in ∞Met (X) \land P \in X \land (R \in ℝ^{*} \land 0 < R)) \to P ball (D) R \neq \emptyset$
20	19	3expa	$⊢ ((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{*} \land 0 < R)) \to P ball (D) R \neq \emptyset$
21	20	expr	$⊢ ((D \in ∞Met (X) \land P \in X) \land R \in ℝ^{*}) \to (0 < R \to P ball (D) R \neq \emptyset)$
22	21	3impa	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \to (0 < R \to P ball (D) R \neq \emptyset)$
23	17 22	impbid	$⊢ (D \in ∞Met (X) \land P \in X \land R \in ℝ^{*}) \to (P ball (D) R \neq \emptyset \leftrightarrow 0 < R)$

Metamath Proof Explorer

Theorem xbln0

Proof