sqrtdiv

Description: Square root distributes over division. (Contributed by Mario Carneiro, 5-May-2016)

		Ref	Expression
	Assertion	sqrtdiv	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ^{+}) \to \sqrt{\frac{A}{B}} = \frac{\sqrt{A}}{\sqrt{B}}$

Proof

Step	Hyp	Ref	Expression
1		rerpdivcl	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to \frac{A}{B} \in ℝ$
2	1	adantlr	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ^{+}) \to \frac{A}{B} \in ℝ$
3		elrp	$⊢ B \in ℝ^{+} \leftrightarrow (B \in ℝ \land 0 < B)$
4		divge0	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 < B)) \to 0 \leq \frac{A}{B}$
5	3 4	sylan2b	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ^{+}) \to 0 \leq \frac{A}{B}$
6		resqrtcl	$⊢ (\frac{A}{B} \in ℝ \land 0 \leq \frac{A}{B}) \to \sqrt{\frac{A}{B}} \in ℝ$
7	2 5 6	syl2anc	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ^{+}) \to \sqrt{\frac{A}{B}} \in ℝ$
8	7	recnd	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ^{+}) \to \sqrt{\frac{A}{B}} \in ℂ$
9		rpsqrtcl	$⊢ B \in ℝ^{+} \to \sqrt{B} \in ℝ^{+}$
10	9	adantl	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ^{+}) \to \sqrt{B} \in ℝ^{+}$
11	10	rpcnd	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ^{+}) \to \sqrt{B} \in ℂ$
12	10	rpne0d	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ^{+}) \to \sqrt{B} \neq 0$
13	8 11 12	divcan4d	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ^{+}) \to \frac{\sqrt{\frac{A}{B}} \sqrt{B}}{\sqrt{B}} = \sqrt{\frac{A}{B}}$
14		rprege0	$⊢ B \in ℝ^{+} \to (B \in ℝ \land 0 \leq B)$
15	14	adantl	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ^{+}) \to (B \in ℝ \land 0 \leq B)$
16		sqrtmul	$⊢ ((\frac{A}{B} \in ℝ \land 0 \leq \frac{A}{B}) \land (B \in ℝ \land 0 \leq B)) \to \sqrt{(\frac{A}{B}) B} = \sqrt{\frac{A}{B}} \sqrt{B}$
17	2 5 15 16	syl21anc	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ^{+}) \to \sqrt{(\frac{A}{B}) B} = \sqrt{\frac{A}{B}} \sqrt{B}$
18		simpll	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ^{+}) \to A \in ℝ$
19	18	recnd	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ^{+}) \to A \in ℂ$
20		rpcn	$⊢ B \in ℝ^{+} \to B \in ℂ$
21	20	adantl	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ^{+}) \to B \in ℂ$
22		rpne0	$⊢ B \in ℝ^{+} \to B \neq 0$
23	22	adantl	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ^{+}) \to B \neq 0$
24	19 21 23	divcan1d	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ^{+}) \to (\frac{A}{B}) B = A$
25	24	fveq2d	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ^{+}) \to \sqrt{(\frac{A}{B}) B} = \sqrt{A}$
26	17 25	eqtr3d	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ^{+}) \to \sqrt{\frac{A}{B}} \sqrt{B} = \sqrt{A}$
27	26	oveq1d	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ^{+}) \to \frac{\sqrt{\frac{A}{B}} \sqrt{B}}{\sqrt{B}} = \frac{\sqrt{A}}{\sqrt{B}}$
28	13 27	eqtr3d	$⊢ ((A \in ℝ \land 0 \leq A) \land B \in ℝ^{+}) \to \sqrt{\frac{A}{B}} = \frac{\sqrt{A}}{\sqrt{B}}$

Metamath Proof Explorer

Theorem sqrtdiv

Proof