Metamath Proof Explorer

Theorem atanlogsub

Description: A variation on atanlogadd , to show that sqrt ( 1 +i z ) / sqrt ( 1 - i z ) = sqrt ( ( 1 +i z ) / ( 1 - i z ) ) under more limited conditions. (Contributed by Mario Carneiro, 4-Apr-2015)

Ref Expression
Assertion atanlogsub 
|- ( ( A e. dom arctan /\ ( Re ` A ) =/= 0 ) -> ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) e. ran log )

Proof

Step Hyp Ref Expression
1 ax-1cn 
 |-  1 e. CC
2 ax-icn 
 |-  _i e. CC
3 atandm2 
 |-  ( A e. dom arctan <-> ( A e. CC /\ ( 1 - ( _i x. A ) ) =/= 0 /\ ( 1 + ( _i x. A ) ) =/= 0 ) )
4 3 simp1bi 
 |-  ( A e. dom arctan -> A e. CC )
5 mulcl 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC )
6 2 4 5 sylancr 
 |-  ( A e. dom arctan -> ( _i x. A ) e. CC )
7 addcl 
 |-  ( ( 1 e. CC /\ ( _i x. A ) e. CC ) -> ( 1 + ( _i x. A ) ) e. CC )
8 1 6 7 sylancr 
 |-  ( A e. dom arctan -> ( 1 + ( _i x. A ) ) e. CC )
9 3 simp3bi 
 |-  ( A e. dom arctan -> ( 1 + ( _i x. A ) ) =/= 0 )
10 8 9 logcld 
 |-  ( A e. dom arctan -> ( log ` ( 1 + ( _i x. A ) ) ) e. CC )
11 subcl 
 |-  ( ( 1 e. CC /\ ( _i x. A ) e. CC ) -> ( 1 - ( _i x. A ) ) e. CC )
12 1 6 11 sylancr 
 |-  ( A e. dom arctan -> ( 1 - ( _i x. A ) ) e. CC )
13 3 simp2bi 
 |-  ( A e. dom arctan -> ( 1 - ( _i x. A ) ) =/= 0 )
14 12 13 logcld 
 |-  ( A e. dom arctan -> ( log ` ( 1 - ( _i x. A ) ) ) e. CC )
15 10 14 subcld 
 |-  ( A e. dom arctan -> ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) e. CC )
16 15 adantr 
 |-  ( ( A e. dom arctan /\ ( Re ` A ) =/= 0 ) -> ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) e. CC )
17 4 recld 
 |-  ( A e. dom arctan -> ( Re ` A ) e. RR )
18 0re 
 |-  0 e. RR
19 lttri2 
 |-  ( ( ( Re ` A ) e. RR /\ 0 e. RR ) -> ( ( Re ` A ) =/= 0 <-> ( ( Re ` A ) < 0 \/ 0 < ( Re ` A ) ) ) )
20 17 18 19 sylancl 
 |-  ( A e. dom arctan -> ( ( Re ` A ) =/= 0 <-> ( ( Re ` A ) < 0 \/ 0 < ( Re ` A ) ) ) )
21 20 biimpa 
 |-  ( ( A e. dom arctan /\ ( Re ` A ) =/= 0 ) -> ( ( Re ` A ) < 0 \/ 0 < ( Re ` A ) ) )
22 15 imnegd 
 |-  ( A e. dom arctan -> ( Im ` -u ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) = -u ( Im ` ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) )
23 10 14 negsubdi2d 
 |-  ( A e. dom arctan -> -u ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) = ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) )
24 mulneg2 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( _i x. -u A ) = -u ( _i x. A ) )
25 2 4 24 sylancr 
 |-  ( A e. dom arctan -> ( _i x. -u A ) = -u ( _i x. A ) )
26 25 oveq2d 
 |-  ( A e. dom arctan -> ( 1 + ( _i x. -u A ) ) = ( 1 + -u ( _i x. A ) ) )
27 negsub 
 |-  ( ( 1 e. CC /\ ( _i x. A ) e. CC ) -> ( 1 + -u ( _i x. A ) ) = ( 1 - ( _i x. A ) ) )
28 1 6 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 oveq2d 
 |-  ( A e. dom arctan -> ( 1 - ( _i x. -u A ) ) = ( 1 - -u ( _i x. A ) ) )
32 subneg 
 |-  ( ( 1 e. CC /\ ( _i x. A ) e. CC ) -> ( 1 - -u ( _i x. A ) ) = ( 1 + ( _i x. A ) ) )
33 1 6 32 sylancr 
 |-  ( A e. dom arctan -> ( 1 - -u ( _i x. A ) ) = ( 1 + ( _i x. A ) ) )
34 31 33 eqtrd 
 |-  ( A e. dom arctan -> ( 1 - ( _i x. -u A ) ) = ( 1 + ( _i x. A ) ) )
35 34 fveq2d 
 |-  ( A e. dom arctan -> ( log ` ( 1 - ( _i x. -u A ) ) ) = ( log ` ( 1 + ( _i x. A ) ) ) )
36 30 35 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 ) ) ) ) )
37 23 36 eqtr4d 
 |-  ( A e. dom arctan -> -u ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) = ( ( log ` ( 1 + ( _i x. -u A ) ) ) - ( log ` ( 1 - ( _i x. -u A ) ) ) ) )
38 37 fveq2d 
 |-  ( A e. dom arctan -> ( Im ` -u ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) = ( Im ` ( ( log ` ( 1 + ( _i x. -u A ) ) ) - ( log ` ( 1 - ( _i x. -u A ) ) ) ) ) )
39 22 38 eqtr3d 
 |-  ( A e. dom arctan -> -u ( Im ` ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) = ( Im ` ( ( log ` ( 1 + ( _i x. -u A ) ) ) - ( log ` ( 1 - ( _i x. -u A ) ) ) ) ) )
40 39 adantr 
 |-  ( ( A e. dom arctan /\ ( Re ` A ) < 0 ) -> -u ( Im ` ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) = ( Im ` ( ( log ` ( 1 + ( _i x. -u A ) ) ) - ( log ` ( 1 - ( _i x. -u A ) ) ) ) ) )
41 atandmneg 
 |-  ( A e. dom arctan -> -u A e. dom arctan )
42 17 lt0neg1d 
 |-  ( A e. dom arctan -> ( ( Re ` A ) < 0 <-> 0 < -u ( Re ` A ) ) )
43 42 biimpa 
 |-  ( ( A e. dom arctan /\ ( Re ` A ) < 0 ) -> 0 < -u ( Re ` A ) )
44 4 adantr 
 |-  ( ( A e. dom arctan /\ ( Re ` A ) < 0 ) -> A e. CC )
45 44 renegd 
 |-  ( ( A e. dom arctan /\ ( Re ` A ) < 0 ) -> ( Re ` -u A ) = -u ( Re ` A ) )
46 43 45 breqtrrd 
 |-  ( ( A e. dom arctan /\ ( Re ` A ) < 0 ) -> 0 < ( Re ` -u A ) )
47 atanlogsublem 
 |-  ( ( -u A e. dom arctan /\ 0 < ( Re ` -u A ) ) -> ( Im ` ( ( log ` ( 1 + ( _i x. -u A ) ) ) - ( log ` ( 1 - ( _i x. -u A ) ) ) ) ) e. ( -u _pi (,) _pi ) )
48 41 46 47 syl2an2r 
 |-  ( ( A e. dom arctan /\ ( Re ` A ) < 0 ) -> ( Im ` ( ( log ` ( 1 + ( _i x. -u A ) ) ) - ( log ` ( 1 - ( _i x. -u A ) ) ) ) ) e. ( -u _pi (,) _pi ) )
49 picn 
 |-  _pi e. CC
50 49 negnegi 
 |-  -u -u _pi = _pi
51 50 oveq2i 
 |-  ( -u _pi (,) -u -u _pi ) = ( -u _pi (,) _pi )
52 48 51 eleqtrrdi 
 |-  ( ( A e. dom arctan /\ ( Re ` A ) < 0 ) -> ( Im ` ( ( log ` ( 1 + ( _i x. -u A ) ) ) - ( log ` ( 1 - ( _i x. -u A ) ) ) ) ) e. ( -u _pi (,) -u -u _pi ) )
53 40 52 eqeltrd 
 |-  ( ( A e. dom arctan /\ ( Re ` A ) < 0 ) -> -u ( Im ` ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) e. ( -u _pi (,) -u -u _pi ) )
54 pire 
 |-  _pi e. RR
55 54 renegcli 
 |-  -u _pi e. RR
56 15 adantr 
 |-  ( ( A e. dom arctan /\ ( Re ` A ) < 0 ) -> ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) e. CC )
57 56 imcld 
 |-  ( ( A e. dom arctan /\ ( Re ` A ) < 0 ) -> ( Im ` ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) e. RR )
58 iooneg 
 |-  ( ( -u _pi e. RR /\ _pi e. RR /\ ( Im ` ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) e. RR ) -> ( ( Im ` ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) e. ( -u _pi (,) _pi ) <-> -u ( Im ` ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) e. ( -u _pi (,) -u -u _pi ) ) )
59 55 54 57 58 mp3an12i 
 |-  ( ( A e. dom arctan /\ ( Re ` A ) < 0 ) -> ( ( Im ` ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) e. ( -u _pi (,) _pi ) <-> -u ( Im ` ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) e. ( -u _pi (,) -u -u _pi ) ) )
60 53 59 mpbird 
 |-  ( ( A e. dom arctan /\ ( Re ` A ) < 0 ) -> ( Im ` ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) e. ( -u _pi (,) _pi ) )
61 atanlogsublem 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Im ` ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) e. ( -u _pi (,) _pi ) )
62 60 61 jaodan 
 |-  ( ( A e. dom arctan /\ ( ( Re ` A ) < 0 \/ 0 < ( Re ` A ) ) ) -> ( Im ` ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) e. ( -u _pi (,) _pi ) )
63 21 62 syldan 
 |-  ( ( A e. dom arctan /\ ( Re ` A ) =/= 0 ) -> ( Im ` ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) e. ( -u _pi (,) _pi ) )
64 eliooord 
 |-  ( ( Im ` ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) e. ( -u _pi (,) _pi ) -> ( -u _pi < ( Im ` ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) /\ ( Im ` ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) < _pi ) )
65 63 64 syl 
 |-  ( ( A e. dom arctan /\ ( Re ` A ) =/= 0 ) -> ( -u _pi < ( Im ` ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) /\ ( Im ` ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) < _pi ) )
66 65 simpld 
 |-  ( ( A e. dom arctan /\ ( Re ` A ) =/= 0 ) -> -u _pi < ( Im ` ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) )
67 65 simprd 
 |-  ( ( A e. dom arctan /\ ( Re ` A ) =/= 0 ) -> ( Im ` ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) < _pi )
68 16 imcld 
 |-  ( ( A e. dom arctan /\ ( Re ` A ) =/= 0 ) -> ( Im ` ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) e. RR )
69 ltle 
 |-  ( ( ( Im ` ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) e. RR /\ _pi e. RR ) -> ( ( Im ` ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) < _pi -> ( Im ` ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) <_ _pi ) )
70 68 54 69 sylancl 
 |-  ( ( A e. dom arctan /\ ( Re ` A ) =/= 0 ) -> ( ( Im ` ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) < _pi -> ( Im ` ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) <_ _pi ) )
71 67 70 mpd 
 |-  ( ( A e. dom arctan /\ ( Re ` A ) =/= 0 ) -> ( Im ` ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) <_ _pi )
72 ellogrn 
 |-  ( ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) e. ran log <-> ( ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) e. CC /\ -u _pi < ( Im ` ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) /\ ( Im ` ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) <_ _pi ) )
73 16 66 71 72 syl3anbrc 
 |-  ( ( A e. dom arctan /\ ( Re ` A ) =/= 0 ) -> ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) e. ran log )