blhalf

Description: A ball of radius R / 2 is contained in a ball of radius R centered at any point inside the smaller ball. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 14-Jan-2014)

		Ref	Expression
	Assertion	blhalf	$⊢ ((M \in ∞Met (X) \land Y \in X) \land (R \in ℝ \land Z \in (Y ball (M) (\frac{R}{2})))) \to Y ball (M) (\frac{R}{2}) \subseteq Z ball (M) R$

Proof

Step	Hyp	Ref	Expression
1		simpll	$⊢ ((M \in ∞Met (X) \land Y \in X) \land (R \in ℝ \land Z \in (Y ball (M) (\frac{R}{2})))) \to M \in ∞Met (X)$
2		simplr	$⊢ ((M \in ∞Met (X) \land Y \in X) \land (R \in ℝ \land Z \in (Y ball (M) (\frac{R}{2})))) \to Y \in X$
3		simprr	$⊢ ((M \in ∞Met (X) \land Y \in X) \land (R \in ℝ \land Z \in (Y ball (M) (\frac{R}{2})))) \to Z \in (Y ball (M) (\frac{R}{2}))$
4		simprl	$⊢ ((M \in ∞Met (X) \land Y \in X) \land (R \in ℝ \land Z \in (Y ball (M) (\frac{R}{2})))) \to R \in ℝ$
5	4	rehalfcld	$⊢ ((M \in ∞Met (X) \land Y \in X) \land (R \in ℝ \land Z \in (Y ball (M) (\frac{R}{2})))) \to \frac{R}{2} \in ℝ$
6	5	rexrd	$⊢ ((M \in ∞Met (X) \land Y \in X) \land (R \in ℝ \land Z \in (Y ball (M) (\frac{R}{2})))) \to \frac{R}{2} \in ℝ^{*}$
7		elbl	$⊢ (M \in ∞Met (X) \land Y \in X \land \frac{R}{2} \in ℝ^{*}) \to (Z \in (Y ball (M) (\frac{R}{2})) \leftrightarrow (Z \in X \land Y M Z < \frac{R}{2}))$
8	1 2 6 7	syl3anc	$⊢ ((M \in ∞Met (X) \land Y \in X) \land (R \in ℝ \land Z \in (Y ball (M) (\frac{R}{2})))) \to (Z \in (Y ball (M) (\frac{R}{2})) \leftrightarrow (Z \in X \land Y M Z < \frac{R}{2}))$
9	3 8	mpbid	$⊢ ((M \in ∞Met (X) \land Y \in X) \land (R \in ℝ \land Z \in (Y ball (M) (\frac{R}{2})))) \to (Z \in X \land Y M Z < \frac{R}{2})$
10	9	simpld	$⊢ ((M \in ∞Met (X) \land Y \in X) \land (R \in ℝ \land Z \in (Y ball (M) (\frac{R}{2})))) \to Z \in X$
11		xmetcl	$⊢ (M \in ∞Met (X) \land Y \in X \land Z \in X) \to Y M Z \in ℝ^{*}$
12	1 2 10 11	syl3anc	$⊢ ((M \in ∞Met (X) \land Y \in X) \land (R \in ℝ \land Z \in (Y ball (M) (\frac{R}{2})))) \to Y M Z \in ℝ^{*}$
13	9	simprd	$⊢ ((M \in ∞Met (X) \land Y \in X) \land (R \in ℝ \land Z \in (Y ball (M) (\frac{R}{2})))) \to Y M Z < \frac{R}{2}$
14	12 6 13	xrltled	$⊢ ((M \in ∞Met (X) \land Y \in X) \land (R \in ℝ \land Z \in (Y ball (M) (\frac{R}{2})))) \to Y M Z \leq \frac{R}{2}$
15	5	recnd	$⊢ ((M \in ∞Met (X) \land Y \in X) \land (R \in ℝ \land Z \in (Y ball (M) (\frac{R}{2})))) \to \frac{R}{2} \in ℂ$
16	4	recnd	$⊢ ((M \in ∞Met (X) \land Y \in X) \land (R \in ℝ \land Z \in (Y ball (M) (\frac{R}{2})))) \to R \in ℂ$
17	16	2halvesd	$⊢ ((M \in ∞Met (X) \land Y \in X) \land (R \in ℝ \land Z \in (Y ball (M) (\frac{R}{2})))) \to (\frac{R}{2}) + (\frac{R}{2}) = R$
18	15 15 17	mvlraddd	$⊢ ((M \in ∞Met (X) \land Y \in X) \land (R \in ℝ \land Z \in (Y ball (M) (\frac{R}{2})))) \to \frac{R}{2} = R - (\frac{R}{2})$
19	14 18	breqtrd	$⊢ ((M \in ∞Met (X) \land Y \in X) \land (R \in ℝ \land Z \in (Y ball (M) (\frac{R}{2})))) \to Y M Z \leq R - (\frac{R}{2})$
20		blss2	$⊢ ((M \in ∞Met (X) \land Y \in X \land Z \in X) \land (\frac{R}{2} \in ℝ \land R \in ℝ \land Y M Z \leq R - (\frac{R}{2}))) \to Y ball (M) (\frac{R}{2}) \subseteq Z ball (M) R$
21	1 2 10 5 4 19 20	syl33anc	$⊢ ((M \in ∞Met (X) \land Y \in X) \land (R \in ℝ \land Z \in (Y ball (M) (\frac{R}{2})))) \to Y ball (M) (\frac{R}{2}) \subseteq Z ball (M) R$

Metamath Proof Explorer

Theorem blhalf

Proof