Metamath Proof Explorer


Theorem absvalsq

Description: Square of value of absolute value function. (Contributed by NM, 16-Jan-2006)

Ref Expression
Assertion absvalsq ( 𝐴 ∈ ℂ → ( ( abs ‘ 𝐴 ) ↑ 2 ) = ( 𝐴 · ( ∗ ‘ 𝐴 ) ) )

Proof

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 ) = ( 𝐴 · ( ∗ ‘ 𝐴 ) ) )