Step |
Hyp |
Ref |
Expression |
1 |
|
recn |
|- ( A e. RR -> A e. CC ) |
2 |
|
absval |
|- ( A e. CC -> ( abs ` A ) = ( sqrt ` ( A x. ( * ` A ) ) ) ) |
3 |
1 2
|
syl |
|- ( A e. RR -> ( abs ` A ) = ( sqrt ` ( A x. ( * ` A ) ) ) ) |
4 |
1
|
sqvald |
|- ( A e. RR -> ( A ^ 2 ) = ( A x. A ) ) |
5 |
|
cjre |
|- ( A e. RR -> ( * ` A ) = A ) |
6 |
5
|
oveq2d |
|- ( A e. RR -> ( A x. ( * ` A ) ) = ( A x. A ) ) |
7 |
4 6
|
eqtr4d |
|- ( A e. RR -> ( A ^ 2 ) = ( A x. ( * ` A ) ) ) |
8 |
7
|
fveq2d |
|- ( A e. RR -> ( sqrt ` ( A ^ 2 ) ) = ( sqrt ` ( A x. ( * ` A ) ) ) ) |
9 |
3 8
|
eqtr4d |
|- ( A e. RR -> ( abs ` A ) = ( sqrt ` ( A ^ 2 ) ) ) |