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 ) = ( ๐ด ยท ( โˆ— โ€˜ ๐ด ) )