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

Metamath Proof Explorer

Theorem sqrtmuli

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

	Ref	Expression
Hypotheses	sqrtthi.1	$⊢ A \in ℝ$
	sqr11.1	$⊢ B \in ℝ$
Assertion	sqrtmuli	$⊢ (0 \leq A \land 0 \leq B) \to \sqrt{A B} = \sqrt{A} \sqrt{B}$

Step	Hyp	Ref	Expression
1		sqrtthi.1	$⊢ A \in ℝ$
2		sqr11.1	$⊢ B \in ℝ$
3		sqrtmul	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to \sqrt{A B} = \sqrt{A} \sqrt{B}$
4	2 3	mpanr1	$⊢ ((A \in ℝ \land 0 \leq A) \land 0 \leq B) \to \sqrt{A B} = \sqrt{A} \sqrt{B}$
5	1 4	mpanl1	$⊢ (0 \leq A \land 0 \leq B) \to \sqrt{A B} = \sqrt{A} \sqrt{B}$