ssblex

Description: A nested ball exists whose radius is less than any desired amount. (Contributed by NM, 20-Sep-2007) (Revised by Mario Carneiro, 12-Nov-2013)

		Ref	Expression
	Assertion	ssblex	$⊢ ((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{+} \land S \in ℝ^{+})) \to \exists x \in ℝ^{+} (x < R \land P ball (D) x \subseteq P ball (D) S)$

Proof

Step	Hyp	Ref	Expression
1		simprl	$⊢ ((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{+} \land S \in ℝ^{+})) \to R \in ℝ^{+}$
2	1	rphalfcld	$⊢ ((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{+} \land S \in ℝ^{+})) \to \frac{R}{2} \in ℝ^{+}$
3		simprr	$⊢ ((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{+} \land S \in ℝ^{+})) \to S \in ℝ^{+}$
4	2 3	ifcld	$⊢ ((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{+} \land S \in ℝ^{+})) \to if (\frac{R}{2} \leq S, \frac{R}{2}, S) \in ℝ^{+}$
5	4	rpred	$⊢ ((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{+} \land S \in ℝ^{+})) \to if (\frac{R}{2} \leq S, \frac{R}{2}, S) \in ℝ$
6	2	rpred	$⊢ ((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{+} \land S \in ℝ^{+})) \to \frac{R}{2} \in ℝ$
7	1	rpred	$⊢ ((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{+} \land S \in ℝ^{+})) \to R \in ℝ$
8	3	rpred	$⊢ ((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{+} \land S \in ℝ^{+})) \to S \in ℝ$
9		min1	$⊢ (\frac{R}{2} \in ℝ \land S \in ℝ) \to if (\frac{R}{2} \leq S, \frac{R}{2}, S) \leq \frac{R}{2}$
10	6 8 9	syl2anc	$⊢ ((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{+} \land S \in ℝ^{+})) \to if (\frac{R}{2} \leq S, \frac{R}{2}, S) \leq \frac{R}{2}$
11	1	rpgt0d	$⊢ ((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{+} \land S \in ℝ^{+})) \to 0 < R$
12		halfpos	$⊢ R \in ℝ \to (0 < R \leftrightarrow \frac{R}{2} < R)$
13	7 12	syl	$⊢ ((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{+} \land S \in ℝ^{+})) \to (0 < R \leftrightarrow \frac{R}{2} < R)$
14	11 13	mpbid	$⊢ ((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{+} \land S \in ℝ^{+})) \to \frac{R}{2} < R$
15	5 6 7 10 14	lelttrd	$⊢ ((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{+} \land S \in ℝ^{+})) \to if (\frac{R}{2} \leq S, \frac{R}{2}, S) < R$
16		simpl	$⊢ ((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{+} \land S \in ℝ^{+})) \to (D \in ∞Met (X) \land P \in X)$
17	4	rpxrd	$⊢ ((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{+} \land S \in ℝ^{+})) \to if (\frac{R}{2} \leq S, \frac{R}{2}, S) \in ℝ^{*}$
18	3	rpxrd	$⊢ ((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{+} \land S \in ℝ^{+})) \to S \in ℝ^{*}$
19		min2	$⊢ (\frac{R}{2} \in ℝ \land S \in ℝ) \to if (\frac{R}{2} \leq S, \frac{R}{2}, S) \leq S$
20	6 8 19	syl2anc	$⊢ ((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{+} \land S \in ℝ^{+})) \to if (\frac{R}{2} \leq S, \frac{R}{2}, S) \leq S$
21		ssbl	$⊢ ((D \in ∞Met (X) \land P \in X) \land (if (\frac{R}{2} \leq S, \frac{R}{2}, S) \in ℝ^{} \land S \in ℝ^{}) \land if (\frac{R}{2} \leq S, \frac{R}{2}, S) \leq S) \to P ball (D) if (\frac{R}{2} \leq S, \frac{R}{2}, S) \subseteq P ball (D) S$
22	16 17 18 20 21	syl121anc	$⊢ ((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{+} \land S \in ℝ^{+})) \to P ball (D) if (\frac{R}{2} \leq S, \frac{R}{2}, S) \subseteq P ball (D) S$
23		breq1	$⊢ x = if (\frac{R}{2} \leq S, \frac{R}{2}, S) \to (x < R \leftrightarrow if (\frac{R}{2} \leq S, \frac{R}{2}, S) < R)$
24		oveq2	$⊢ x = if (\frac{R}{2} \leq S, \frac{R}{2}, S) \to P ball (D) x = P ball (D) if (\frac{R}{2} \leq S, \frac{R}{2}, S)$
25	24	sseq1d	$⊢ x = if (\frac{R}{2} \leq S, \frac{R}{2}, S) \to (P ball (D) x \subseteq P ball (D) S \leftrightarrow P ball (D) if (\frac{R}{2} \leq S, \frac{R}{2}, S) \subseteq P ball (D) S)$
26	23 25	anbi12d	$⊢ x = if (\frac{R}{2} \leq S, \frac{R}{2}, S) \to ((x < R \land P ball (D) x \subseteq P ball (D) S) \leftrightarrow (if (\frac{R}{2} \leq S, \frac{R}{2}, S) < R \land P ball (D) if (\frac{R}{2} \leq S, \frac{R}{2}, S) \subseteq P ball (D) S))$
27	26	rspcev	$⊢ (if (\frac{R}{2} \leq S, \frac{R}{2}, S) \in ℝ^{+} \land (if (\frac{R}{2} \leq S, \frac{R}{2}, S) < R \land P ball (D) if (\frac{R}{2} \leq S, \frac{R}{2}, S) \subseteq P ball (D) S)) \to \exists x \in ℝ^{+} (x < R \land P ball (D) x \subseteq P ball (D) S)$
28	4 15 22 27	syl12anc	$⊢ ((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{+} \land S \in ℝ^{+})) \to \exists x \in ℝ^{+} (x < R \land P ball (D) x \subseteq P ball (D) S)$

Metamath Proof Explorer

Theorem ssblex

Proof