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

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 addlidd ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( 0 + ( ℜ ‘ 𝐴 ) ) = ( ℜ ‘ 𝐴 ) )
60 56 59 eqtrid ⊢ ( ( 𝐴 ∈ 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 addridd ⊢ ( ( 𝐴 ∈ 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 )