Step |
Hyp |
Ref |
Expression |
1 |
|
absval |
⊢ ( 𝐴 ∈ ℂ → ( abs ‘ 𝐴 ) = ( √ ‘ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) ) |
2 |
1
|
oveq1d |
⊢ ( 𝐴 ∈ ℂ → ( ( abs ‘ 𝐴 ) ↑ 2 ) = ( ( √ ‘ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) ↑ 2 ) ) |
3 |
|
cjmulrcl |
⊢ ( 𝐴 ∈ ℂ → ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ∈ ℝ ) |
4 |
|
cjmulge0 |
⊢ ( 𝐴 ∈ ℂ → 0 ≤ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) |
5 |
|
resqrtth |
⊢ ( ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) → ( ( √ ‘ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) ↑ 2 ) = ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) |
6 |
3 4 5
|
syl2anc |
⊢ ( 𝐴 ∈ ℂ → ( ( √ ‘ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) ↑ 2 ) = ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) |
7 |
2 6
|
eqtrd |
⊢ ( 𝐴 ∈ ℂ → ( ( abs ‘ 𝐴 ) ↑ 2 ) = ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) |