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