This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rennim

Description: A real number does not lie on the negative imaginary axis. (Contributed by Mario Carneiro, 8-Jul-2013)

Ref Expression
Assertion rennim 
|- ( A e. RR -> ( _i x. A ) e/ RR+ )

Proof

Step Hyp Ref Expression
1 ax-icn 
 |-  _i e. CC
2 recn 
 |-  ( A e. RR -> A e. CC )
3 mulcl 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC )
4 1 2 3 sylancr 
 |-  ( A e. RR -> ( _i x. A ) e. CC )
5 rpre 
 |-  ( ( _i x. A ) e. RR+ -> ( _i x. A ) e. RR )
6 rereb 
 |-  ( ( _i x. A ) e. CC -> ( ( _i x. A ) e. RR <-> ( Re ` ( _i x. A ) ) = ( _i x. A ) ) )
7 5 6 imbitrid 
 |-  ( ( _i x. A ) e. CC -> ( ( _i x. A ) e. RR+ -> ( Re ` ( _i x. A ) ) = ( _i x. A ) ) )
8 4 7 syl 
 |-  ( A e. RR -> ( ( _i x. A ) e. RR+ -> ( Re ` ( _i x. A ) ) = ( _i x. A ) ) )
9 4 addlidd 
 |-  ( A e. RR -> ( 0 + ( _i x. A ) ) = ( _i x. A ) )
10 9 fveq2d 
 |-  ( A e. RR -> ( Re ` ( 0 + ( _i x. A ) ) ) = ( Re ` ( _i x. A ) ) )
11 0re 
 |-  0 e. RR
12 crre 
 |-  ( ( 0 e. RR /\ A e. RR ) -> ( Re ` ( 0 + ( _i x. A ) ) ) = 0 )
13 11 12 mpan 
 |-  ( A e. RR -> ( Re ` ( 0 + ( _i x. A ) ) ) = 0 )
14 10 13 eqtr3d 
 |-  ( A e. RR -> ( Re ` ( _i x. A ) ) = 0 )
15 14 eqeq1d 
 |-  ( A e. RR -> ( ( Re ` ( _i x. A ) ) = ( _i x. A ) <-> 0 = ( _i x. A ) ) )
16 8 15 sylibd 
 |-  ( A e. RR -> ( ( _i x. A ) e. RR+ -> 0 = ( _i x. A ) ) )
17 rpne0 
 |-  ( ( _i x. A ) e. RR+ -> ( _i x. A ) =/= 0 )
18 17 necon2bi 
 |-  ( ( _i x. A ) = 0 -> -. ( _i x. A ) e. RR+ )
19 18 eqcoms 
 |-  ( 0 = ( _i x. A ) -> -. ( _i x. A ) e. RR+ )
20 16 19 syl6 
 |-  ( A e. RR -> ( ( _i x. A ) e. RR+ -> -. ( _i x. A ) e. RR+ ) )
21 20 pm2.01d 
 |-  ( A e. RR -> -. ( _i x. A ) e. RR+ )
22 df-nel 
 |-  ( ( _i x. A ) e/ RR+ <-> -. ( _i x. A ) e. RR+ )
23 21 22 sylibr 
 |-  ( A e. RR -> ( _i x. A ) e/ RR+ )