Theorem sqrtmul

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

	Ref	Expression
Assertion	sqrtmul	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( √ ‘ ( 𝐴 · 𝐵 ) ) = ( ( √ ‘ 𝐴 ) · ( √ ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpll	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → 𝐴 ∈ ℝ )
2		simprl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → 𝐵 ∈ ℝ )
3	1 2	remulcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( 𝐴 · 𝐵 ) ∈ ℝ )
4		mulge0	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → 0 ≤ ( 𝐴 · 𝐵 ) )
5		resqrtcl	⊢ ( ( ( 𝐴 · 𝐵 ) ∈ ℝ ∧ 0 ≤ ( 𝐴 · 𝐵 ) ) → ( √ ‘ ( 𝐴 · 𝐵 ) ) ∈ ℝ )
6	3 4 5	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( √ ‘ ( 𝐴 · 𝐵 ) ) ∈ ℝ )
7		resqrtcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( √ ‘ 𝐴 ) ∈ ℝ )
8	7	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( √ ‘ 𝐴 ) ∈ ℝ )
9		resqrtcl	⊢ ( ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) → ( √ ‘ 𝐵 ) ∈ ℝ )
10	9	adantl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( √ ‘ 𝐵 ) ∈ ℝ )
11	8 10	remulcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( ( √ ‘ 𝐴 ) · ( √ ‘ 𝐵 ) ) ∈ ℝ )
12		sqrtge0	⊢ ( ( ( 𝐴 · 𝐵 ) ∈ ℝ ∧ 0 ≤ ( 𝐴 · 𝐵 ) ) → 0 ≤ ( √ ‘ ( 𝐴 · 𝐵 ) ) )
13	3 4 12	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → 0 ≤ ( √ ‘ ( 𝐴 · 𝐵 ) ) )
14		sqrtge0	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → 0 ≤ ( √ ‘ 𝐴 ) )
15	14	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → 0 ≤ ( √ ‘ 𝐴 ) )
16		sqrtge0	⊢ ( ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) → 0 ≤ ( √ ‘ 𝐵 ) )
17	16	adantl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → 0 ≤ ( √ ‘ 𝐵 ) )
18	8 10 15 17	mulge0d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → 0 ≤ ( ( √ ‘ 𝐴 ) · ( √ ‘ 𝐵 ) ) )
19		resqrtth	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ( √ ‘ 𝐴 ) ↑ 2 ) = 𝐴 )
20		resqrtth	⊢ ( ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) → ( ( √ ‘ 𝐵 ) ↑ 2 ) = 𝐵 )
21	19 20	oveqan12d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( ( ( √ ‘ 𝐴 ) ↑ 2 ) · ( ( √ ‘ 𝐵 ) ↑ 2 ) ) = ( 𝐴 · 𝐵 ) )
22	8	recnd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( √ ‘ 𝐴 ) ∈ ℂ )
23	10	recnd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( √ ‘ 𝐵 ) ∈ ℂ )
24	22 23	sqmuld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( ( ( √ ‘ 𝐴 ) · ( √ ‘ 𝐵 ) ) ↑ 2 ) = ( ( ( √ ‘ 𝐴 ) ↑ 2 ) · ( ( √ ‘ 𝐵 ) ↑ 2 ) ) )
25		resqrtth	⊢ ( ( ( 𝐴 · 𝐵 ) ∈ ℝ ∧ 0 ≤ ( 𝐴 · 𝐵 ) ) → ( ( √ ‘ ( 𝐴 · 𝐵 ) ) ↑ 2 ) = ( 𝐴 · 𝐵 ) )
26	3 4 25	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( ( √ ‘ ( 𝐴 · 𝐵 ) ) ↑ 2 ) = ( 𝐴 · 𝐵 ) )
27	21 24 26	3eqtr4rd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( ( √ ‘ ( 𝐴 · 𝐵 ) ) ↑ 2 ) = ( ( ( √ ‘ 𝐴 ) · ( √ ‘ 𝐵 ) ) ↑ 2 ) )
28	6 11 13 18 27	sq11d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( √ ‘ ( 𝐴 · 𝐵 ) ) = ( ( √ ‘ 𝐴 ) · ( √ ‘ 𝐵 ) ) )