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