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