This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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