Step |
Hyp |
Ref |
Expression |
1 |
|
ax-icn |
|- _i e. CC |
2 |
|
ax-1cn |
|- 1 e. CC |
3 |
1 2
|
mulcli |
|- ( _i x. 1 ) e. CC |
4 |
3
|
addid2i |
|- ( 0 + ( _i x. 1 ) ) = ( _i x. 1 ) |
5 |
4
|
eqcomi |
|- ( _i x. 1 ) = ( 0 + ( _i x. 1 ) ) |
6 |
5
|
fveq2i |
|- ( Im ` ( _i x. 1 ) ) = ( Im ` ( 0 + ( _i x. 1 ) ) ) |
7 |
1
|
mulid1i |
|- ( _i x. 1 ) = _i |
8 |
7
|
fveq2i |
|- ( Im ` ( _i x. 1 ) ) = ( Im ` _i ) |
9 |
|
0re |
|- 0 e. RR |
10 |
|
1re |
|- 1 e. RR |
11 |
|
crim |
|- ( ( 0 e. RR /\ 1 e. RR ) -> ( Im ` ( 0 + ( _i x. 1 ) ) ) = 1 ) |
12 |
9 10 11
|
mp2an |
|- ( Im ` ( 0 + ( _i x. 1 ) ) ) = 1 |
13 |
6 8 12
|
3eqtr3i |
|- ( Im ` _i ) = 1 |