Metamath Proof Explorer


Theorem atanlogaddlem

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

Ref Expression
Assertion atanlogaddlem ( ( 𝐴 ∈ dom arctan ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) + ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ∈ ran log )

Proof

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