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+ )