sqrtmul

Description: Square root distributes over multiplication. (Contributed by NM, 30-Jul-1999) (Revised by Mario Carneiro, 29-May-2016)

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

Proof

Step	Hyp	Ref	Expression
1		simpll	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to A \in ℝ$
2		simprl	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to B \in ℝ$
3	1 2	remulcld	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to A B \in ℝ$
4		mulge0	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to 0 \leq A B$
5		resqrtcl	$⊢ (A B \in ℝ \land 0 \leq A B) \to \sqrt{A B} \in ℝ$
6	3 4 5	syl2anc	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to \sqrt{A B} \in ℝ$
7		resqrtcl	$⊢ (A \in ℝ \land 0 \leq A) \to \sqrt{A} \in ℝ$
8	7	adantr	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to \sqrt{A} \in ℝ$
9		resqrtcl	$⊢ (B \in ℝ \land 0 \leq B) \to \sqrt{B} \in ℝ$
10	9	adantl	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to \sqrt{B} \in ℝ$
11	8 10	remulcld	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to \sqrt{A} \sqrt{B} \in ℝ$
12		sqrtge0	$⊢ (A B \in ℝ \land 0 \leq A B) \to 0 \leq \sqrt{A B}$
13	3 4 12	syl2anc	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to 0 \leq \sqrt{A B}$
14		sqrtge0	$⊢ (A \in ℝ \land 0 \leq A) \to 0 \leq \sqrt{A}$
15	14	adantr	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to 0 \leq \sqrt{A}$
16		sqrtge0	$⊢ (B \in ℝ \land 0 \leq B) \to 0 \leq \sqrt{B}$
17	16	adantl	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to 0 \leq \sqrt{B}$
18	8 10 15 17	mulge0d	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to 0 \leq \sqrt{A} \sqrt{B}$
19		resqrtth	$⊢ (A \in ℝ \land 0 \leq A) \to {\sqrt{A}}^{2} = A$
20		resqrtth	$⊢ (B \in ℝ \land 0 \leq B) \to {\sqrt{B}}^{2} = B$
21	19 20	oveqan12d	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to {\sqrt{A}}^{2} {\sqrt{B}}^{2} = A B$
22	8	recnd	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to \sqrt{A} \in ℂ$
23	10	recnd	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to \sqrt{B} \in ℂ$
24	22 23	sqmuld	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to {\sqrt{A} \sqrt{B}}^{2} = {\sqrt{A}}^{2} {\sqrt{B}}^{2}$
25		resqrtth	$⊢ (A B \in ℝ \land 0 \leq A B) \to {\sqrt{A B}}^{2} = A B$
26	3 4 25	syl2anc	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to {\sqrt{A B}}^{2} = A B$
27	21 24 26	3eqtr4rd	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to {\sqrt{A B}}^{2} = {\sqrt{A} \sqrt{B}}^{2}$
28	6 11 13 18 27	sq11d	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to \sqrt{A B} = \sqrt{A} \sqrt{B}$

Metamath Proof Explorer

Theorem sqrtmul

Proof