Metamath Proof Explorer

Theorem atanlogaddlem

Description: Lemma for atanlogadd . (Contributed by Mario Carneiro, 3-Apr-2015)

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

Proof

Step Hyp Ref Expression
1 0re 
 |-  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 leloe 
 |-  ( ( 0 e. RR /\ ( Re ` A ) e. RR ) -> ( 0 <_ ( Re ` A ) <-> ( 0 < ( Re ` A ) \/ 0 = ( Re ` A ) ) ) )
6 1 4 5 sylancr 
 |-  ( A e. dom arctan -> ( 0 <_ ( Re ` A ) <-> ( 0 < ( Re ` A ) \/ 0 = ( Re ` A ) ) ) )
7 6 biimpa 
 |-  ( ( A e. dom arctan /\ 0 <_ ( Re ` A ) ) -> ( 0 < ( Re ` A ) \/ 0 = ( Re ` A ) ) )
8 ax-1cn 
 |-  1 e. CC
9 ax-icn 
 |-  _i e. CC
10 mulcl 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC )
11 9 3 10 sylancr 
 |-  ( A e. dom arctan -> ( _i x. A ) e. CC )
12 addcl 
 |-  ( ( 1 e. CC /\ ( _i x. A ) e. CC ) -> ( 1 + ( _i x. A ) ) e. CC )
13 8 11 12 sylancr 
 |-  ( A e. dom arctan -> ( 1 + ( _i x. A ) ) e. CC )
14 2 simp3bi 
 |-  ( A e. dom arctan -> ( 1 + ( _i x. A ) ) =/= 0 )
15 13 14 logcld 
 |-  ( A e. dom arctan -> ( log ` ( 1 + ( _i x. A ) ) ) e. CC )
16 subcl 
 |-  ( ( 1 e. CC /\ ( _i x. A ) e. CC ) -> ( 1 - ( _i x. A ) ) e. CC )
17 8 11 16 sylancr 
 |-  ( A e. dom arctan -> ( 1 - ( _i x. A ) ) e. CC )
18 2 simp2bi 
 |-  ( A e. dom arctan -> ( 1 - ( _i x. A ) ) =/= 0 )
19 17 18 logcld 
 |-  ( A e. dom arctan -> ( log ` ( 1 - ( _i x. A ) ) ) e. CC )
20 15 19 addcld 
 |-  ( A e. dom arctan -> ( ( log ` ( 1 + ( _i x. A ) ) ) + ( log ` ( 1 - ( _i x. A ) ) ) ) e. CC )
21 20 adantr 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( ( log ` ( 1 + ( _i x. A ) ) ) + ( log ` ( 1 - ( _i x. A ) ) ) ) e. CC )
22 pire 
 |-  _pi e. RR
23 22 renegcli 
 |-  -u _pi e. RR
24 23 a1i 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> -u _pi e. RR )
25 19 adantr 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( log ` ( 1 - ( _i x. A ) ) ) e. CC )
26 25 imcld 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Im ` ( log ` ( 1 - ( _i x. A ) ) ) ) e. RR )
27 15 adantr 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( log ` ( 1 + ( _i x. A ) ) ) e. CC )
28 27 imcld 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Im ` ( log ` ( 1 + ( _i x. A ) ) ) ) e. RR )
29 28 26 readdcld 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( ( Im ` ( log ` ( 1 + ( _i x. A ) ) ) ) + ( Im ` ( log ` ( 1 - ( _i x. A ) ) ) ) ) e. RR )
30 17 adantr 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( 1 - ( _i x. A ) ) e. CC )
31 im1 
 |-  ( Im ` 1 ) = 0
32 31 oveq1i 
 |-  ( ( Im ` 1 ) - ( Im ` ( _i x. A ) ) ) = ( 0 - ( Im ` ( _i x. A ) ) )
33 df-neg 
 |-  -u ( Im ` ( _i x. A ) ) = ( 0 - ( Im ` ( _i x. A ) ) )
34 32 33 eqtr4i 
 |-  ( ( Im ` 1 ) - ( Im ` ( _i x. A ) ) ) = -u ( Im ` ( _i x. A ) )
35 11 adantr 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( _i x. A ) e. CC )
36 imsub 
 |-  ( ( 1 e. CC /\ ( _i x. A ) e. CC ) -> ( Im ` ( 1 - ( _i x. A ) ) ) = ( ( Im ` 1 ) - ( Im ` ( _i x. A ) ) ) )
37 8 35 36 sylancr 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Im ` ( 1 - ( _i x. A ) ) ) = ( ( Im ` 1 ) - ( Im ` ( _i x. A ) ) ) )
38 3 adantr 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> A e. CC )
39 reim 
 |-  ( A e. CC -> ( Re ` A ) = ( Im ` ( _i x. A ) ) )
40 38 39 syl 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Re ` A ) = ( Im ` ( _i x. A ) ) )
41 40 negeqd 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> -u ( Re ` A ) = -u ( Im ` ( _i x. A ) ) )
42 34 37 41 3eqtr4a 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Im ` ( 1 - ( _i x. A ) ) ) = -u ( Re ` A ) )
43 4 lt0neg2d 
 |-  ( A e. dom arctan -> ( 0 < ( Re ` A ) <-> -u ( Re ` A ) < 0 ) )
44 43 biimpa 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> -u ( Re ` A ) < 0 )
45 42 44 eqbrtrd 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Im ` ( 1 - ( _i x. A ) ) ) < 0 )
46 argimlt0 
 |-  ( ( ( 1 - ( _i x. A ) ) e. CC /\ ( Im ` ( 1 - ( _i x. A ) ) ) < 0 ) -> ( Im ` ( log ` ( 1 - ( _i x. A ) ) ) ) e. ( -u _pi (,) 0 ) )
47 30 45 46 syl2anc 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Im ` ( log ` ( 1 - ( _i x. A ) ) ) ) e. ( -u _pi (,) 0 ) )
48 eliooord 
 |-  ( ( Im ` ( log ` ( 1 - ( _i x. A ) ) ) ) e. ( -u _pi (,) 0 ) -> ( -u _pi < ( Im ` ( log ` ( 1 - ( _i x. A ) ) ) ) /\ ( Im ` ( log ` ( 1 - ( _i x. A ) ) ) ) < 0 ) )
49 47 48 syl 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( -u _pi < ( Im ` ( log ` ( 1 - ( _i x. A ) ) ) ) /\ ( Im ` ( log ` ( 1 - ( _i x. A ) ) ) ) < 0 ) )
50 49 simpld 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> -u _pi < ( Im ` ( log ` ( 1 - ( _i x. A ) ) ) ) )
51 13 adantr 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( 1 + ( _i x. A ) ) e. CC )
52 simpr 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> 0 < ( Re ` A ) )
53 imadd 
 |-  ( ( 1 e. CC /\ ( _i x. A ) e. CC ) -> ( Im ` ( 1 + ( _i x. A ) ) ) = ( ( Im ` 1 ) + ( Im ` ( _i x. A ) ) ) )
54 8 35 53 sylancr 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Im ` ( 1 + ( _i x. A ) ) ) = ( ( Im ` 1 ) + ( Im ` ( _i x. A ) ) ) )
55 40 oveq2d 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( ( Im ` 1 ) + ( Re ` A ) ) = ( ( Im ` 1 ) + ( Im ` ( _i x. A ) ) ) )
56 31 oveq1i 
 |-  ( ( Im ` 1 ) + ( Re ` A ) ) = ( 0 + ( Re ` A ) )
57 38 recld 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Re ` A ) e. RR )
58 57 recnd 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Re ` A ) e. CC )
59 58 addlidd 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( 0 + ( Re ` A ) ) = ( Re ` A ) )
60 56 59 eqtrid 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( ( Im ` 1 ) + ( Re ` A ) ) = ( Re ` A ) )
61 54 55 60 3eqtr2d 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Im ` ( 1 + ( _i x. A ) ) ) = ( Re ` A ) )
62 52 61 breqtrrd 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> 0 < ( Im ` ( 1 + ( _i x. A ) ) ) )
63 argimgt0 
 |-  ( ( ( 1 + ( _i x. A ) ) e. CC /\ 0 < ( Im ` ( 1 + ( _i x. A ) ) ) ) -> ( Im ` ( log ` ( 1 + ( _i x. A ) ) ) ) e. ( 0 (,) _pi ) )
64 51 62 63 syl2anc 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Im ` ( log ` ( 1 + ( _i x. A ) ) ) ) e. ( 0 (,) _pi ) )
65 eliooord 
 |-  ( ( Im ` ( log ` ( 1 + ( _i x. A ) ) ) ) e. ( 0 (,) _pi ) -> ( 0 < ( Im ` ( log ` ( 1 + ( _i x. A ) ) ) ) /\ ( Im ` ( log ` ( 1 + ( _i x. A ) ) ) ) < _pi ) )
66 64 65 syl 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( 0 < ( Im ` ( log ` ( 1 + ( _i x. A ) ) ) ) /\ ( Im ` ( log ` ( 1 + ( _i x. A ) ) ) ) < _pi ) )
67 66 simpld 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> 0 < ( Im ` ( log ` ( 1 + ( _i x. A ) ) ) ) )
68 28 26 ltaddpos2d 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( 0 < ( Im ` ( log ` ( 1 + ( _i x. A ) ) ) ) <-> ( Im ` ( log ` ( 1 - ( _i x. A ) ) ) ) < ( ( Im ` ( log ` ( 1 + ( _i x. A ) ) ) ) + ( Im ` ( log ` ( 1 - ( _i x. A ) ) ) ) ) ) )
69 67 68 mpbid 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Im ` ( log ` ( 1 - ( _i x. A ) ) ) ) < ( ( Im ` ( log ` ( 1 + ( _i x. A ) ) ) ) + ( Im ` ( log ` ( 1 - ( _i x. A ) ) ) ) ) )
70 24 26 29 50 69 lttrd 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> -u _pi < ( ( Im ` ( log ` ( 1 + ( _i x. A ) ) ) ) + ( Im ` ( log ` ( 1 - ( _i x. A ) ) ) ) ) )
71 27 25 imaddd 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Im ` ( ( log ` ( 1 + ( _i x. A ) ) ) + ( log ` ( 1 - ( _i x. A ) ) ) ) ) = ( ( Im ` ( log ` ( 1 + ( _i x. A ) ) ) ) + ( Im ` ( log ` ( 1 - ( _i x. A ) ) ) ) ) )
72 70 71 breqtrrd 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> -u _pi < ( Im ` ( ( log ` ( 1 + ( _i x. A ) ) ) + ( log ` ( 1 - ( _i x. A ) ) ) ) ) )
73 22 a1i 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> _pi e. RR )
74 0red 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> 0 e. RR )
75 49 simprd 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Im ` ( log ` ( 1 - ( _i x. A ) ) ) ) < 0 )
76 26 74 28 75 ltadd2dd 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( ( Im ` ( log ` ( 1 + ( _i x. A ) ) ) ) + ( Im ` ( log ` ( 1 - ( _i x. A ) ) ) ) ) < ( ( Im ` ( log ` ( 1 + ( _i x. A ) ) ) ) + 0 ) )
77 28 recnd 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Im ` ( log ` ( 1 + ( _i x. A ) ) ) ) e. CC )
78 77 addridd 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( ( Im ` ( log ` ( 1 + ( _i x. A ) ) ) ) + 0 ) = ( Im ` ( log ` ( 1 + ( _i x. A ) ) ) ) )
79 76 78 breqtrd 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( ( Im ` ( log ` ( 1 + ( _i x. A ) ) ) ) + ( Im ` ( log ` ( 1 - ( _i x. A ) ) ) ) ) < ( Im ` ( log ` ( 1 + ( _i x. A ) ) ) ) )
80 66 simprd 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Im ` ( log ` ( 1 + ( _i x. A ) ) ) ) < _pi )
81 29 28 73 79 80 lttrd 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( ( Im ` ( log ` ( 1 + ( _i x. A ) ) ) ) + ( Im ` ( log ` ( 1 - ( _i x. A ) ) ) ) ) < _pi )
82 29 73 81 ltled 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( ( Im ` ( log ` ( 1 + ( _i x. A ) ) ) ) + ( Im ` ( log ` ( 1 - ( _i x. A ) ) ) ) ) <_ _pi )
83 71 82 eqbrtrd 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( Im ` ( ( log ` ( 1 + ( _i x. A ) ) ) + ( log ` ( 1 - ( _i x. A ) ) ) ) ) <_ _pi )
84 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 ) )
85 21 72 83 84 syl3anbrc 
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( ( log ` ( 1 + ( _i x. A ) ) ) + ( log ` ( 1 - ( _i x. A ) ) ) ) e. ran log )
86 0red 
 |-  ( ( A e. dom arctan /\ 0 = ( Re ` A ) ) -> 0 e. RR )
87 11 adantr 
 |-  ( ( A e. dom arctan /\ 0 = ( Re ` A ) ) -> ( _i x. A ) e. CC )
88 simpr 
 |-  ( ( A e. dom arctan /\ 0 = ( Re ` A ) ) -> 0 = ( Re ` A ) )
89 3 adantr 
 |-  ( ( A e. dom arctan /\ 0 = ( Re ` A ) ) -> A e. CC )
90 89 39 syl 
 |-  ( ( A e. dom arctan /\ 0 = ( Re ` A ) ) -> ( Re ` A ) = ( Im ` ( _i x. A ) ) )
91 88 90 eqtr2d 
 |-  ( ( A e. dom arctan /\ 0 = ( Re ` A ) ) -> ( Im ` ( _i x. A ) ) = 0 )
92 87 91 reim0bd 
 |-  ( ( A e. dom arctan /\ 0 = ( Re ` A ) ) -> ( _i x. A ) e. RR )
93 15 19 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 ) ) ) ) )
94 93 ad2antrr 
 |-  ( ( ( A e. dom arctan /\ 0 = ( Re ` A ) ) /\ 0 <_ ( _i x. A ) ) -> ( ( log ` ( 1 + ( _i x. A ) ) ) + ( log ` ( 1 - ( _i x. A ) ) ) ) = ( ( log ` ( 1 - ( _i x. A ) ) ) + ( log ` ( 1 + ( _i x. A ) ) ) ) )
95 logrncl 
 |-  ( ( ( 1 - ( _i x. A ) ) e. CC /\ ( 1 - ( _i x. A ) ) =/= 0 ) -> ( log ` ( 1 - ( _i x. A ) ) ) e. ran log )
96 17 18 95 syl2anc 
 |-  ( A e. dom arctan -> ( log ` ( 1 - ( _i x. A ) ) ) e. ran log )
97 96 ad2antrr 
 |-  ( ( ( A e. dom arctan /\ 0 = ( Re ` A ) ) /\ 0 <_ ( _i x. A ) ) -> ( log ` ( 1 - ( _i x. A ) ) ) e. ran log )
98 1re 
 |-  1 e. RR
99 92 adantr 
 |-  ( ( ( A e. dom arctan /\ 0 = ( Re ` A ) ) /\ 0 <_ ( _i x. A ) ) -> ( _i x. A ) e. RR )
100 readdcl 
 |-  ( ( 1 e. RR /\ ( _i x. A ) e. RR ) -> ( 1 + ( _i x. A ) ) e. RR )
101 98 99 100 sylancr 
 |-  ( ( ( A e. dom arctan /\ 0 = ( Re ` A ) ) /\ 0 <_ ( _i x. A ) ) -> ( 1 + ( _i x. A ) ) e. RR )
102 0red 
 |-  ( ( ( A e. dom arctan /\ 0 = ( Re ` A ) ) /\ 0 <_ ( _i x. A ) ) -> 0 e. RR )
103 1red 
 |-  ( ( ( A e. dom arctan /\ 0 = ( Re ` A ) ) /\ 0 <_ ( _i x. A ) ) -> 1 e. RR )
104 0lt1 
 |-  0 < 1
105 104 a1i 
 |-  ( ( ( A e. dom arctan /\ 0 = ( Re ` A ) ) /\ 0 <_ ( _i x. A ) ) -> 0 < 1 )
106 addge01 
 |-  ( ( 1 e. RR /\ ( _i x. A ) e. RR ) -> ( 0 <_ ( _i x. A ) <-> 1 <_ ( 1 + ( _i x. A ) ) ) )
107 98 92 106 sylancr 
 |-  ( ( A e. dom arctan /\ 0 = ( Re ` A ) ) -> ( 0 <_ ( _i x. A ) <-> 1 <_ ( 1 + ( _i x. A ) ) ) )
108 107 biimpa 
 |-  ( ( ( A e. dom arctan /\ 0 = ( Re ` A ) ) /\ 0 <_ ( _i x. A ) ) -> 1 <_ ( 1 + ( _i x. A ) ) )
109 102 103 101 105 108 ltletrd 
 |-  ( ( ( A e. dom arctan /\ 0 = ( Re ` A ) ) /\ 0 <_ ( _i x. A ) ) -> 0 < ( 1 + ( _i x. A ) ) )
110 101 109 elrpd 
 |-  ( ( ( A e. dom arctan /\ 0 = ( Re ` A ) ) /\ 0 <_ ( _i x. A ) ) -> ( 1 + ( _i x. A ) ) e. RR+ )
111 110 relogcld 
 |-  ( ( ( A e. dom arctan /\ 0 = ( Re ` A ) ) /\ 0 <_ ( _i x. A ) ) -> ( log ` ( 1 + ( _i x. A ) ) ) e. RR )
112 logrnaddcl 
 |-  ( ( ( log ` ( 1 - ( _i x. A ) ) ) e. ran log /\ ( log ` ( 1 + ( _i x. A ) ) ) e. RR ) -> ( ( log ` ( 1 - ( _i x. A ) ) ) + ( log ` ( 1 + ( _i x. A ) ) ) ) e. ran log )
113 97 111 112 syl2anc 
 |-  ( ( ( A e. dom arctan /\ 0 = ( Re ` A ) ) /\ 0 <_ ( _i x. A ) ) -> ( ( log ` ( 1 - ( _i x. A ) ) ) + ( log ` ( 1 + ( _i x. A ) ) ) ) e. ran log )
114 94 113 eqeltrd 
 |-  ( ( ( A e. dom arctan /\ 0 = ( Re ` A ) ) /\ 0 <_ ( _i x. A ) ) -> ( ( log ` ( 1 + ( _i x. A ) ) ) + ( log ` ( 1 - ( _i x. A ) ) ) ) e. ran log )
115 logrncl 
 |-  ( ( ( 1 + ( _i x. A ) ) e. CC /\ ( 1 + ( _i x. A ) ) =/= 0 ) -> ( log ` ( 1 + ( _i x. A ) ) ) e. ran log )
116 13 14 115 syl2anc 
 |-  ( A e. dom arctan -> ( log ` ( 1 + ( _i x. A ) ) ) e. ran log )
117 116 ad2antrr 
 |-  ( ( ( A e. dom arctan /\ 0 = ( Re ` A ) ) /\ ( _i x. A ) <_ 0 ) -> ( log ` ( 1 + ( _i x. A ) ) ) e. ran log )
118 92 adantr 
 |-  ( ( ( A e. dom arctan /\ 0 = ( Re ` A ) ) /\ ( _i x. A ) <_ 0 ) -> ( _i x. A ) e. RR )
119 resubcl 
 |-  ( ( 1 e. RR /\ ( _i x. A ) e. RR ) -> ( 1 - ( _i x. A ) ) e. RR )
120 98 118 119 sylancr 
 |-  ( ( ( A e. dom arctan /\ 0 = ( Re ` A ) ) /\ ( _i x. A ) <_ 0 ) -> ( 1 - ( _i x. A ) ) e. RR )
121 0red 
 |-  ( ( ( A e. dom arctan /\ 0 = ( Re ` A ) ) /\ ( _i x. A ) <_ 0 ) -> 0 e. RR )
122 1red 
 |-  ( ( ( A e. dom arctan /\ 0 = ( Re ` A ) ) /\ ( _i x. A ) <_ 0 ) -> 1 e. RR )
123 104 a1i 
 |-  ( ( ( A e. dom arctan /\ 0 = ( Re ` A ) ) /\ ( _i x. A ) <_ 0 ) -> 0 < 1 )
124 1m0e1 
 |-  ( 1 - 0 ) = 1
125 1red 
 |-  ( ( A e. dom arctan /\ 0 = ( Re ` A ) ) -> 1 e. RR )
126 92 86 125 lesub2d 
 |-  ( ( A e. dom arctan /\ 0 = ( Re ` A ) ) -> ( ( _i x. A ) <_ 0 <-> ( 1 - 0 ) <_ ( 1 - ( _i x. A ) ) ) )
127 126 biimpa 
 |-  ( ( ( A e. dom arctan /\ 0 = ( Re ` A ) ) /\ ( _i x. A ) <_ 0 ) -> ( 1 - 0 ) <_ ( 1 - ( _i x. A ) ) )
128 124 127 eqbrtrrid 
 |-  ( ( ( A e. dom arctan /\ 0 = ( Re ` A ) ) /\ ( _i x. A ) <_ 0 ) -> 1 <_ ( 1 - ( _i x. A ) ) )
129 121 122 120 123 128 ltletrd 
 |-  ( ( ( A e. dom arctan /\ 0 = ( Re ` A ) ) /\ ( _i x. A ) <_ 0 ) -> 0 < ( 1 - ( _i x. A ) ) )
130 120 129 elrpd 
 |-  ( ( ( A e. dom arctan /\ 0 = ( Re ` A ) ) /\ ( _i x. A ) <_ 0 ) -> ( 1 - ( _i x. A ) ) e. RR+ )
131 130 relogcld 
 |-  ( ( ( A e. dom arctan /\ 0 = ( Re ` A ) ) /\ ( _i x. A ) <_ 0 ) -> ( log ` ( 1 - ( _i x. A ) ) ) e. RR )
132 logrnaddcl 
 |-  ( ( ( log ` ( 1 + ( _i x. A ) ) ) e. ran log /\ ( log ` ( 1 - ( _i x. A ) ) ) e. RR ) -> ( ( log ` ( 1 + ( _i x. A ) ) ) + ( log ` ( 1 - ( _i x. A ) ) ) ) e. ran log )
133 117 131 132 syl2anc 
 |-  ( ( ( A e. dom arctan /\ 0 = ( Re ` A ) ) /\ ( _i x. A ) <_ 0 ) -> ( ( log ` ( 1 + ( _i x. A ) ) ) + ( log ` ( 1 - ( _i x. A ) ) ) ) e. ran log )
134 86 92 114 133 lecasei 
 |-  ( ( A e. dom arctan /\ 0 = ( Re ` A ) ) -> ( ( log ` ( 1 + ( _i x. A ) ) ) + ( log ` ( 1 - ( _i x. A ) ) ) ) e. ran log )
135 85 134 jaodan 
 |-  ( ( A e. dom arctan /\ ( 0 < ( Re ` A ) \/ 0 = ( Re ` A ) ) ) -> ( ( log ` ( 1 + ( _i x. A ) ) ) + ( log ` ( 1 - ( _i x. A ) ) ) ) e. ran log )
136 7 135 syldan 
 |-  ( ( A e. dom arctan /\ 0 <_ ( Re ` A ) ) -> ( ( log ` ( 1 + ( _i x. A ) ) ) + ( log ` ( 1 - ( _i x. A ) ) ) ) e. ran log )