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

Metamath Proof Explorer

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 )