Metamath Proof Explorer


Theorem absval2i

Description: Value of absolute value function. Definition 10.36 of Gleason p. 133. (Contributed by NM, 2-Oct-1999)

Ref Expression
Hypothesis absvalsqi.1 𝐴 ∈ ℂ
Assertion absval2i ( abs ‘ 𝐴 ) = ( √ ‘ ( ( ( ℜ ‘ 𝐴 ) ↑ 2 ) + ( ( ℑ ‘ 𝐴 ) ↑ 2 ) ) )

Proof

Step Hyp Ref Expression
1 absvalsqi.1 𝐴 ∈ ℂ
2 absval2 ( 𝐴 ∈ ℂ → ( abs ‘ 𝐴 ) = ( √ ‘ ( ( ( ℜ ‘ 𝐴 ) ↑ 2 ) + ( ( ℑ ‘ 𝐴 ) ↑ 2 ) ) ) )
3 1 2 ax-mp ( abs ‘ 𝐴 ) = ( √ ‘ ( ( ( ℜ ‘ 𝐴 ) ↑ 2 ) + ( ( ℑ ‘ 𝐴 ) ↑ 2 ) ) )