Metamath Proof Explorer
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 ) = ( ๐ด ยท ( โ โ ๐ด ) ) |