Metamath Proof Explorer


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 ≤ 𝐵 ) ) → ( √ ‘ ( 𝐴 · 𝐵 ) ) = ( ( √ ‘ 𝐴 ) · ( √ ‘ 𝐵 ) ) )