Theorem sqrtmulii

Description: Square root distributes over multiplication. (Contributed by NM, 30-Jul-1999)

	Ref	Expression
Hypotheses	sqrtthi.1	$$⊢A\in ℝ$$
	sqr11.1	$$⊢B\in ℝ$$
	sqrmuli.1	$$⊢0\le A$$
	sqrmuli.2	$$⊢0\le B$$
Assertion	sqrtmulii	$$⊢\sqrt{AB}=\sqrt{A}\sqrt{B}$$

Proof

Step	Hyp	Ref	Expression
1		sqrtthi.1	$$⊢A\in ℝ$$
2		sqr11.1	$$⊢B\in ℝ$$
3		sqrmuli.1	$$⊢0\le A$$
4		sqrmuli.2	$$⊢0\le B$$
5	1 2	sqrtmuli	$$⊢\left(0\le A\wedge 0\le B\right)\to \sqrt{AB}=\sqrt{A}\sqrt{B}$$
6	3 4 5	mp2an	$$⊢\sqrt{AB}=\sqrt{A}\sqrt{B}$$