Step |
Hyp |
Ref |
Expression |
1 |
|
cjcl |
|- ( A e. CC -> ( * ` A ) e. CC ) |
2 |
|
absval |
|- ( ( * ` A ) e. CC -> ( abs ` ( * ` A ) ) = ( sqrt ` ( ( * ` A ) x. ( * ` ( * ` A ) ) ) ) ) |
3 |
1 2
|
syl |
|- ( A e. CC -> ( abs ` ( * ` A ) ) = ( sqrt ` ( ( * ` A ) x. ( * ` ( * ` A ) ) ) ) ) |
4 |
|
mulcom |
|- ( ( A e. CC /\ ( * ` A ) e. CC ) -> ( A x. ( * ` A ) ) = ( ( * ` A ) x. A ) ) |
5 |
1 4
|
mpdan |
|- ( A e. CC -> ( A x. ( * ` A ) ) = ( ( * ` A ) x. A ) ) |
6 |
|
cjcj |
|- ( A e. CC -> ( * ` ( * ` A ) ) = A ) |
7 |
6
|
oveq2d |
|- ( A e. CC -> ( ( * ` A ) x. ( * ` ( * ` A ) ) ) = ( ( * ` A ) x. A ) ) |
8 |
5 7
|
eqtr4d |
|- ( A e. CC -> ( A x. ( * ` A ) ) = ( ( * ` A ) x. ( * ` ( * ` A ) ) ) ) |
9 |
8
|
fveq2d |
|- ( A e. CC -> ( sqrt ` ( A x. ( * ` A ) ) ) = ( sqrt ` ( ( * ` A ) x. ( * ` ( * ` A ) ) ) ) ) |
10 |
3 9
|
eqtr4d |
|- ( A e. CC -> ( abs ` ( * ` A ) ) = ( sqrt ` ( A x. ( * ` A ) ) ) ) |
11 |
|
absval |
|- ( A e. CC -> ( abs ` A ) = ( sqrt ` ( A x. ( * ` A ) ) ) ) |
12 |
10 11
|
eqtr4d |
|- ( A e. CC -> ( abs ` ( * ` A ) ) = ( abs ` A ) ) |