Theorem sqrtdivd

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

	Ref	Expression
Hypotheses	resqrcld.1	$$⊢\phi \to A\in ℝ$$
	resqrcld.2	$$⊢\phi \to 0\le A$$
	sqrdivd.3	$$⊢\phi \to B\in {ℝ}^{+}$$
Assertion	sqrtdivd	$$⊢\phi \to \sqrt{\frac{A}{B}}=\frac{\sqrt{A}}{\sqrt{B}}$$

Proof

Step	Hyp	Ref	Expression
1		resqrcld.1	$$⊢\phi \to A\in ℝ$$
2		resqrcld.2	$$⊢\phi \to 0\le A$$
3		sqrdivd.3	$$⊢\phi \to B\in {ℝ}^{+}$$
4		sqrtdiv	$$⊢\left(\left(A\in ℝ\wedge 0\le A\right)\wedge B\in {ℝ}^{+}\right)\to \sqrt{\frac{A}{B}}=\frac{\sqrt{A}}{\sqrt{B}}$$
5	1 2 3 4	syl21anc	$$⊢\phi \to \sqrt{\frac{A}{B}}=\frac{\sqrt{A}}{\sqrt{B}}$$