This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sqrtdivd

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

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

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