Step |
Hyp |
Ref |
Expression |
1 |
|
ax-icn |
|- _i e. CC |
2 |
|
mulcl |
|- ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC ) |
3 |
1 2
|
mpan |
|- ( A e. CC -> ( _i x. A ) e. CC ) |
4 |
|
imval |
|- ( ( _i x. A ) e. CC -> ( Im ` ( _i x. A ) ) = ( Re ` ( ( _i x. A ) / _i ) ) ) |
5 |
3 4
|
syl |
|- ( A e. CC -> ( Im ` ( _i x. A ) ) = ( Re ` ( ( _i x. A ) / _i ) ) ) |
6 |
|
ine0 |
|- _i =/= 0 |
7 |
|
divcan3 |
|- ( ( A e. CC /\ _i e. CC /\ _i =/= 0 ) -> ( ( _i x. A ) / _i ) = A ) |
8 |
1 6 7
|
mp3an23 |
|- ( A e. CC -> ( ( _i x. A ) / _i ) = A ) |
9 |
8
|
fveq2d |
|- ( A e. CC -> ( Re ` ( ( _i x. A ) / _i ) ) = ( Re ` A ) ) |
10 |
5 9
|
eqtr2d |
|- ( A e. CC -> ( Re ` A ) = ( Im ` ( _i x. A ) ) ) |