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

Metamath Proof Explorer

Theorem absvalsqi

Description: Square of value of absolute value function. (Contributed by NM, 2-Oct-1999)

Ref Expression
Hypothesis absvalsqi.1 ⊢ 𝐴 ∈ ℂ
Assertion absvalsqi ( ( abs ‘ 𝐴 ) ↑ 2 ) = ( 𝐴 · ( ∗ ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 absvalsqi.1 ⊢ 𝐴 ∈ ℂ
2 absvalsq ⊢ ( 𝐴 ∈ ℂ → ( ( abs ‘ 𝐴 ) ↑ 2 ) = ( 𝐴 · ( ∗ ‘ 𝐴 ) ) )
3 1 2 ax-mp ⊢ ( ( abs ‘ 𝐴 ) ↑ 2 ) = ( 𝐴 · ( ∗ ‘ 𝐴 ) )