Metamath Proof Explorer


Theorem imi

Description: The imaginary part of _i . (Contributed by Scott Fenton, 9-Jun-2006)

Ref Expression
Assertion imi
|- ( Im ` _i ) = 1

Proof

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