Step |
Hyp |
Ref |
Expression |
1 |
|
absval |
โข ( ๐ด โ โ โ ( abs โ ๐ด ) = ( โ โ ( ๐ด ยท ( โ โ ๐ด ) ) ) ) |
2 |
|
cjmulrcl |
โข ( ๐ด โ โ โ ( ๐ด ยท ( โ โ ๐ด ) ) โ โ ) |
3 |
|
cjmulge0 |
โข ( ๐ด โ โ โ 0 โค ( ๐ด ยท ( โ โ ๐ด ) ) ) |
4 |
|
resqrtcl |
โข ( ( ( ๐ด ยท ( โ โ ๐ด ) ) โ โ โง 0 โค ( ๐ด ยท ( โ โ ๐ด ) ) ) โ ( โ โ ( ๐ด ยท ( โ โ ๐ด ) ) ) โ โ ) |
5 |
2 3 4
|
syl2anc |
โข ( ๐ด โ โ โ ( โ โ ( ๐ด ยท ( โ โ ๐ด ) ) ) โ โ ) |
6 |
1 5
|
eqeltrd |
โข ( ๐ด โ โ โ ( abs โ ๐ด ) โ โ ) |