Description: The real part of _i . (Contributed by Scott Fenton, 9-Jun-2006)
Ref | Expression | ||
---|---|---|---|
Assertion | rei | |- ( Re ` _i ) = 0 |
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 |