Theorem atanlogadd

Description: The rule sqrt ( z w ) = ( sqrt z ) ( sqrt w ) is not always true on the complex numbers, but it is true when the arguments of z and w sum to within the interval ( -upi , pi ] , so there are some cases such as this one with z = 1 +i A and w = 1 - i A which are true unconditionally. This result can also be stated as " sqrt ( 1 + z ) + sqrt ( 1 - z ) is analytic". (Contributed by Mario Carneiro, 3-Apr-2015)

	Ref	Expression
Assertion	atanlogadd	|- ( A e. dom arctan -> ( ( log ` ( 1 + ( _i x. A ) ) ) + ( log ` ( 1 - ( _i x. A ) ) ) ) e. ran log )

Proof

Step	Hyp	Ref	Expression
1		0red	|- ( A e. dom arctan -> 0 e. RR )
2		atandm2	|- ( A e. dom arctan <-> ( A e. CC /\ ( 1 - ( _i x. A ) ) =/= 0 /\ ( 1 + ( _i x. A ) ) =/= 0 ) )
3	2	simp1bi	|- ( A e. dom arctan -> A e. CC )
4	3	recld	|- ( A e. dom arctan -> ( Re ` A ) e. RR )
5		atanlogaddlem	|- ( ( A e. dom arctan /\ 0 <_ ( Re ` A ) ) -> ( ( log ` ( 1 + ( _i x. A ) ) ) + ( log ` ( 1 - ( _i x. A ) ) ) ) e. ran log )
6		ax-1cn	|- 1 e. CC
7		ax-icn	|- _i e. CC
8		mulcl	|- ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC )
9	7 3 8	sylancr	|- ( A e. dom arctan -> ( _i x. A ) e. CC )
10		addcl	|- ( ( 1 e. CC /\ ( _i x. A ) e. CC ) -> ( 1 + ( _i x. A ) ) e. CC )
11	6 9 10	sylancr	|- ( A e. dom arctan -> ( 1 + ( _i x. A ) ) e. CC )
12	2	simp3bi	|- ( A e. dom arctan -> ( 1 + ( _i x. A ) ) =/= 0 )
13	11 12	logcld	|- ( A e. dom arctan -> ( log ` ( 1 + ( _i x. A ) ) ) e. CC )
14		subcl	|- ( ( 1 e. CC /\ ( _i x. A ) e. CC ) -> ( 1 - ( _i x. A ) ) e. CC )
15	6 9 14	sylancr	|- ( A e. dom arctan -> ( 1 - ( _i x. A ) ) e. CC )
16	2	simp2bi	|- ( A e. dom arctan -> ( 1 - ( _i x. A ) ) =/= 0 )
17	15 16	logcld	|- ( A e. dom arctan -> ( log ` ( 1 - ( _i x. A ) ) ) e. CC )
18	13 17	addcomd	|- ( A e. dom arctan -> ( ( log ` ( 1 + ( _i x. A ) ) ) + ( log ` ( 1 - ( _i x. A ) ) ) ) = ( ( log ` ( 1 - ( _i x. A ) ) ) + ( log ` ( 1 + ( _i x. A ) ) ) ) )
19		mulneg2	|- ( ( _i e. CC /\ A e. CC ) -> ( _i x. -u A ) = -u ( _i x. A ) )
20	7 3 19	sylancr	|- ( A e. dom arctan -> ( _i x. -u A ) = -u ( _i x. A ) )
21	20	oveq2d	|- ( A e. dom arctan -> ( 1 + ( _i x. -u A ) ) = ( 1 + -u ( _i x. A ) ) )
22		negsub	|- ( ( 1 e. CC /\ ( _i x. A ) e. CC ) -> ( 1 + -u ( _i x. A ) ) = ( 1 - ( _i x. A ) ) )
23	6 9 22	sylancr	|- ( A e. dom arctan -> ( 1 + -u ( _i x. A ) ) = ( 1 - ( _i x. A ) ) )
24	21 23	eqtrd	|- ( A e. dom arctan -> ( 1 + ( _i x. -u A ) ) = ( 1 - ( _i x. A ) ) )
25	24	fveq2d	|- ( A e. dom arctan -> ( log ` ( 1 + ( _i x. -u A ) ) ) = ( log ` ( 1 - ( _i x. A ) ) ) )
26	20	oveq2d	|- ( A e. dom arctan -> ( 1 - ( _i x. -u A ) ) = ( 1 - -u ( _i x. A ) ) )
27		subneg	|- ( ( 1 e. CC /\ ( _i x. A ) e. CC ) -> ( 1 - -u ( _i x. A ) ) = ( 1 + ( _i x. A ) ) )
28	6 9 27	sylancr	|- ( A e. dom arctan -> ( 1 - -u ( _i x. A ) ) = ( 1 + ( _i x. A ) ) )
29	26 28	eqtrd	|- ( A e. dom arctan -> ( 1 - ( _i x. -u A ) ) = ( 1 + ( _i x. A ) ) )
30	29	fveq2d	|- ( A e. dom arctan -> ( log ` ( 1 - ( _i x. -u A ) ) ) = ( log ` ( 1 + ( _i x. A ) ) ) )
31	25 30	oveq12d	|- ( A e. dom arctan -> ( ( log ` ( 1 + ( _i x. -u A ) ) ) + ( log ` ( 1 - ( _i x. -u A ) ) ) ) = ( ( log ` ( 1 - ( _i x. A ) ) ) + ( log ` ( 1 + ( _i x. A ) ) ) ) )
32	18 31	eqtr4d	|- ( A e. dom arctan -> ( ( log ` ( 1 + ( _i x. A ) ) ) + ( log ` ( 1 - ( _i x. A ) ) ) ) = ( ( log ` ( 1 + ( _i x. -u A ) ) ) + ( log ` ( 1 - ( _i x. -u A ) ) ) ) )
33	32	adantr	|- ( ( A e. dom arctan /\ ( Re ` A ) <_ 0 ) -> ( ( log ` ( 1 + ( _i x. A ) ) ) + ( log ` ( 1 - ( _i x. A ) ) ) ) = ( ( log ` ( 1 + ( _i x. -u A ) ) ) + ( log ` ( 1 - ( _i x. -u A ) ) ) ) )
34		atandmneg	|- ( A e. dom arctan -> -u A e. dom arctan )
35	4	le0neg1d	|- ( A e. dom arctan -> ( ( Re ` A ) <_ 0 <-> 0 <_ -u ( Re ` A ) ) )
36	35	biimpa	|- ( ( A e. dom arctan /\ ( Re ` A ) <_ 0 ) -> 0 <_ -u ( Re ` A ) )
37	3	renegd	|- ( A e. dom arctan -> ( Re ` -u A ) = -u ( Re ` A ) )
38	37	adantr	|- ( ( A e. dom arctan /\ ( Re ` A ) <_ 0 ) -> ( Re ` -u A ) = -u ( Re ` A ) )
39	36 38	breqtrrd	|- ( ( A e. dom arctan /\ ( Re ` A ) <_ 0 ) -> 0 <_ ( Re ` -u A ) )
40		atanlogaddlem	|- ( ( -u A e. dom arctan /\ 0 <_ ( Re ` -u A ) ) -> ( ( log ` ( 1 + ( _i x. -u A ) ) ) + ( log ` ( 1 - ( _i x. -u A ) ) ) ) e. ran log )
41	34 39 40	syl2an2r	|- ( ( A e. dom arctan /\ ( Re ` A ) <_ 0 ) -> ( ( log ` ( 1 + ( _i x. -u A ) ) ) + ( log ` ( 1 - ( _i x. -u A ) ) ) ) e. ran log )
42	33 41	eqeltrd	|- ( ( A e. dom arctan /\ ( Re ` A ) <_ 0 ) -> ( ( log ` ( 1 + ( _i x. A ) ) ) + ( log ` ( 1 - ( _i x. A ) ) ) ) e. ran log )
43	1 4 5 42	lecasei	|- ( A e. dom arctan -> ( ( log ` ( 1 + ( _i x. A ) ) ) + ( log ` ( 1 - ( _i x. A ) ) ) ) e. ran log )