Theorem logneg

Description: The natural logarithm of a negative real number. (Contributed by Mario Carneiro, 13-May-2014) (Revised by Mario Carneiro, 3-Apr-2015)

	Ref	Expression
Assertion	logneg	|- ( A e. RR+ -> ( log ` -u A ) = ( ( log ` A ) + ( _i x. _pi ) ) )

Proof

Step	Hyp	Ref	Expression
1		relogcl	|- ( A e. RR+ -> ( log ` A ) e. RR )
2	1	recnd	|- ( A e. RR+ -> ( log ` A ) e. CC )
3		ax-icn	|- _i e. CC
4		picn	|- _pi e. CC
5	3 4	mulcli	|- ( _i x. _pi ) e. CC
6		efadd	|- ( ( ( log ` A ) e. CC /\ ( _i x. _pi ) e. CC ) -> ( exp ` ( ( log ` A ) + ( _i x. _pi ) ) ) = ( ( exp ` ( log ` A ) ) x. ( exp ` ( _i x. _pi ) ) ) )
7	2 5 6	sylancl	|- ( A e. RR+ -> ( exp ` ( ( log ` A ) + ( _i x. _pi ) ) ) = ( ( exp ` ( log ` A ) ) x. ( exp ` ( _i x. _pi ) ) ) )
8		efipi	|- ( exp ` ( _i x. _pi ) ) = -u 1
9	8	oveq2i	|- ( ( exp ` ( log ` A ) ) x. ( exp ` ( _i x. _pi ) ) ) = ( ( exp ` ( log ` A ) ) x. -u 1 )
10		reeflog	|- ( A e. RR+ -> ( exp ` ( log ` A ) ) = A )
11	10	oveq1d	|- ( A e. RR+ -> ( ( exp ` ( log ` A ) ) x. -u 1 ) = ( A x. -u 1 ) )
12	9 11	syl5eq	|- ( A e. RR+ -> ( ( exp ` ( log ` A ) ) x. ( exp ` ( _i x. _pi ) ) ) = ( A x. -u 1 ) )
13		rpcn	|- ( A e. RR+ -> A e. CC )
14		neg1cn	|- -u 1 e. CC
15		mulcom	|- ( ( A e. CC /\ -u 1 e. CC ) -> ( A x. -u 1 ) = ( -u 1 x. A ) )
16	13 14 15	sylancl	|- ( A e. RR+ -> ( A x. -u 1 ) = ( -u 1 x. A ) )
17	13	mulm1d	|- ( A e. RR+ -> ( -u 1 x. A ) = -u A )
18	16 17	eqtrd	|- ( A e. RR+ -> ( A x. -u 1 ) = -u A )
19	7 12 18	3eqtrd	|- ( A e. RR+ -> ( exp ` ( ( log ` A ) + ( _i x. _pi ) ) ) = -u A )
20	19	fveq2d	|- ( A e. RR+ -> ( log ` ( exp ` ( ( log ` A ) + ( _i x. _pi ) ) ) ) = ( log ` -u A ) )
21		addcl	|- ( ( ( log ` A ) e. CC /\ ( _i x. _pi ) e. CC ) -> ( ( log ` A ) + ( _i x. _pi ) ) e. CC )
22	2 5 21	sylancl	|- ( A e. RR+ -> ( ( log ` A ) + ( _i x. _pi ) ) e. CC )
23		pipos	|- 0 < _pi
24		pire	|- _pi e. RR
25		lt0neg2	|- ( _pi e. RR -> ( 0 < _pi <-> -u _pi < 0 ) )
26	24 25	ax-mp	|- ( 0 < _pi <-> -u _pi < 0 )
27	23 26	mpbi	|- -u _pi < 0
28	24	renegcli	|- -u _pi e. RR
29		0re	|- 0 e. RR
30	28 29 24	lttri	|- ( ( -u _pi < 0 /\ 0 < _pi ) -> -u _pi < _pi )
31	27 23 30	mp2an	|- -u _pi < _pi
32		crim	|- ( ( ( log ` A ) e. RR /\ _pi e. RR ) -> ( Im ` ( ( log ` A ) + ( _i x. _pi ) ) ) = _pi )
33	1 24 32	sylancl	|- ( A e. RR+ -> ( Im ` ( ( log ` A ) + ( _i x. _pi ) ) ) = _pi )
34	31 33	breqtrrid	|- ( A e. RR+ -> -u _pi < ( Im ` ( ( log ` A ) + ( _i x. _pi ) ) ) )
35	24	leidi	|- _pi <_ _pi
36	33 35	eqbrtrdi	|- ( A e. RR+ -> ( Im ` ( ( log ` A ) + ( _i x. _pi ) ) ) <_ _pi )
37		ellogrn	|- ( ( ( log ` A ) + ( _i x. _pi ) ) e. ran log <-> ( ( ( log ` A ) + ( _i x. _pi ) ) e. CC /\ -u _pi < ( Im ` ( ( log ` A ) + ( _i x. _pi ) ) ) /\ ( Im ` ( ( log ` A ) + ( _i x. _pi ) ) ) <_ _pi ) )
38	22 34 36 37	syl3anbrc	|- ( A e. RR+ -> ( ( log ` A ) + ( _i x. _pi ) ) e. ran log )
39		logef	|- ( ( ( log ` A ) + ( _i x. _pi ) ) e. ran log -> ( log ` ( exp ` ( ( log ` A ) + ( _i x. _pi ) ) ) ) = ( ( log ` A ) + ( _i x. _pi ) ) )
40	38 39	syl	|- ( A e. RR+ -> ( log ` ( exp ` ( ( log ` A ) + ( _i x. _pi ) ) ) ) = ( ( log ` A ) + ( _i x. _pi ) ) )
41	20 40	eqtr3d	|- ( A e. RR+ -> ( log ` -u A ) = ( ( log ` A ) + ( _i x. _pi ) ) )