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 addid2d
 |-  ( ( A e. dom arctan /\ 0 < ( Re ` A ) ) -> ( 0 + ( Re ` A ) ) = ( Re ` A ) )
60 56 59 syl5eq
 |-  ( ( 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 addid1d
 |-  ( ( 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 )