Metamath Proof Explorer

Theorem ssbl

Description: The size of a ball increases monotonically with its radius. (Contributed by NM, 20-Sep-2007) (Revised by Mario Carneiro, 24-Aug-2015)

		Ref	Expression
	Assertion	ssbl	$⊢ ((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{} \land S \in ℝ^{}) \land R \leq S) \to P ball (D) R \subseteq P ball (D) S$

Proof

Step	Hyp	Ref	Expression
1		simp1l	$⊢ ((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{} \land S \in ℝ^{}) \land R \leq S) \to D \in ∞Met (X)$
2		simp1r	$⊢ ((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{} \land S \in ℝ^{}) \land R \leq S) \to P \in X$
3		simp2l	$⊢ ((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{} \land S \in ℝ^{}) \land R \leq S) \to R \in ℝ^{*}$
4		simp2r	$⊢ ((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{} \land S \in ℝ^{}) \land R \leq S) \to S \in ℝ^{*}$
5		xmet0	$⊢ (D \in ∞Met (X) \land P \in X) \to P D P = 0$
6	5	3ad2ant1	$⊢ ((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{} \land S \in ℝ^{}) \land R \leq S) \to P D P = 0$
7		0re	$⊢ 0 \in ℝ$
8	6 7	eqeltrdi	$⊢ ((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{} \land S \in ℝ^{}) \land R \leq S) \to P D P \in ℝ$
9		simp3	$⊢ ((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{} \land S \in ℝ^{}) \land R \leq S) \to R \leq S$
10		xsubge0	$⊢ (S \in ℝ^{} \land R \in ℝ^{}) \to (0 \leq S +_{𝑒} (- R) \leftrightarrow R \leq S)$
11	4 3 10	syl2anc	$⊢ ((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{} \land S \in ℝ^{}) \land R \leq S) \to (0 \leq S +_{𝑒} (- R) \leftrightarrow R \leq S)$
12	9 11	mpbird	$⊢ ((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{} \land S \in ℝ^{}) \land R \leq S) \to 0 \leq S +_{𝑒} (- R)$
13	6 12	eqbrtrd	$⊢ ((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{} \land S \in ℝ^{}) \land R \leq S) \to P D P \leq S +_{𝑒} (- R)$
14	1 2 2 3 4 8 13	xblss2	$⊢ ((D \in ∞Met (X) \land P \in X) \land (R \in ℝ^{} \land S \in ℝ^{}) \land R \leq S) \to P ball (D) R \subseteq P ball (D) S$