Metamath Proof Explorer

Theorem rei

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

Ref Expression
Assertion rei 
|- ( Re ` _i ) = 0

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 fveq2i 
 |-  ( Re ` ( 0 + ( _i x. 1 ) ) ) = ( Re ` ( _i x. 1 ) )
6 0re 
 |-  0 e. RR
7 1re 
 |-  1 e. RR
8 crre 
 |-  ( ( 0 e. RR /\ 1 e. RR ) -> ( Re ` ( 0 + ( _i x. 1 ) ) ) = 0 )
9 6 7 8 mp2an 
 |-  ( Re ` ( 0 + ( _i x. 1 ) ) ) = 0
10 1 mulid1i 
 |-  ( _i x. 1 ) = _i
11 10 fveq2i 
 |-  ( Re ` ( _i x. 1 ) ) = ( Re ` _i )
12 5 9 11 3eqtr3ri 
 |-  ( Re ` _i ) = 0