Metamath Proof Explorer


Theorem isosctrlem2

Description: Lemma for isosctr . Corresponds to the case where one vertex is at 0, another at 1 and the third lies on the unit circle. (Contributed by Saveliy Skresanov, 31-Dec-2016)

Ref Expression
Assertion isosctrlem2 ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ( ℑ ‘ ( log ‘ ( 1 − 𝐴 ) ) ) = ( ℑ ‘ ( log ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 1cnd ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) = 0 ) → 1 ∈ ℂ )
2 simpl1 ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) = 0 ) → 𝐴 ∈ ℂ )
3 1 2 negsubd ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) = 0 ) → ( 1 + - 𝐴 ) = ( 1 − 𝐴 ) )
4 1rp 1 ∈ ℝ+
5 4 a1i ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) = 0 ) → 1 ∈ ℝ+ )
6 simpl3 ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) = 0 ) → ¬ 1 = 𝐴 )
7 simpl2 ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) = 0 ) → ( abs ‘ 𝐴 ) = 1 )
8 1 2 1 sub32d ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) = 0 ) → ( ( 1 − 𝐴 ) − 1 ) = ( ( 1 − 1 ) − 𝐴 ) )
9 1m1e0 ( 1 − 1 ) = 0
10 9 oveq1i ( ( 1 − 1 ) − 𝐴 ) = ( 0 − 𝐴 )
11 df-neg - 𝐴 = ( 0 − 𝐴 )
12 10 11 eqtr4i ( ( 1 − 1 ) − 𝐴 ) = - 𝐴
13 8 12 eqtrdi ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) = 0 ) → ( ( 1 − 𝐴 ) − 1 ) = - 𝐴 )
14 1cnd ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → 1 ∈ ℂ )
15 simp1 ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → 𝐴 ∈ ℂ )
16 14 15 subcld ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ( 1 − 𝐴 ) ∈ ℂ )
17 16 adantr ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) = 0 ) → ( 1 − 𝐴 ) ∈ ℂ )
18 ax-1cn 1 ∈ ℂ
19 subeq0 ( ( 1 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( 1 − 𝐴 ) = 0 ↔ 1 = 𝐴 ) )
20 18 19 mpan ( 𝐴 ∈ ℂ → ( ( 1 − 𝐴 ) = 0 ↔ 1 = 𝐴 ) )
21 20 biimpd ( 𝐴 ∈ ℂ → ( ( 1 − 𝐴 ) = 0 → 1 = 𝐴 ) )
22 21 con3dimp ( ( 𝐴 ∈ ℂ ∧ ¬ 1 = 𝐴 ) → ¬ ( 1 − 𝐴 ) = 0 )
23 22 neqned ( ( 𝐴 ∈ ℂ ∧ ¬ 1 = 𝐴 ) → ( 1 − 𝐴 ) ≠ 0 )
24 23 3adant2 ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ( 1 − 𝐴 ) ≠ 0 )
25 24 adantr ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) = 0 ) → ( 1 − 𝐴 ) ≠ 0 )
26 17 25 recrecd ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) = 0 ) → ( 1 / ( 1 / ( 1 − 𝐴 ) ) ) = ( 1 − 𝐴 ) )
27 14 16 24 div2negd ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ( - 1 / - ( 1 − 𝐴 ) ) = ( 1 / ( 1 − 𝐴 ) ) )
28 27 adantr ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) = 0 ) → ( - 1 / - ( 1 − 𝐴 ) ) = ( 1 / ( 1 − 𝐴 ) ) )
29 15 negcld ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → - 𝐴 ∈ ℂ )
30 29 16 24 cjdivd ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ( ∗ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) = ( ( ∗ ‘ - 𝐴 ) / ( ∗ ‘ ( 1 − 𝐴 ) ) ) )
31 15 cjnegd ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ( ∗ ‘ - 𝐴 ) = - ( ∗ ‘ 𝐴 ) )
32 fveq2 ( 𝐴 = 0 → ( abs ‘ 𝐴 ) = ( abs ‘ 0 ) )
33 abs0 ( abs ‘ 0 ) = 0
34 32 33 eqtrdi ( 𝐴 = 0 → ( abs ‘ 𝐴 ) = 0 )
35 eqtr2 ( ( ( abs ‘ 𝐴 ) = 1 ∧ ( abs ‘ 𝐴 ) = 0 ) → 1 = 0 )
36 34 35 sylan2 ( ( ( abs ‘ 𝐴 ) = 1 ∧ 𝐴 = 0 ) → 1 = 0 )
37 ax-1ne0 1 ≠ 0
38 neneq ( 1 ≠ 0 → ¬ 1 = 0 )
39 37 38 mp1i ( ( ( abs ‘ 𝐴 ) = 1 ∧ 𝐴 = 0 ) → ¬ 1 = 0 )
40 36 39 pm2.65da ( ( abs ‘ 𝐴 ) = 1 → ¬ 𝐴 = 0 )
41 40 adantl ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ) → ¬ 𝐴 = 0 )
42 df-ne ( 𝐴 ≠ 0 ↔ ¬ 𝐴 = 0 )
43 oveq1 ( ( abs ‘ 𝐴 ) = 1 → ( ( abs ‘ 𝐴 ) ↑ 2 ) = ( 1 ↑ 2 ) )
44 sq1 ( 1 ↑ 2 ) = 1
45 43 44 eqtrdi ( ( abs ‘ 𝐴 ) = 1 → ( ( abs ‘ 𝐴 ) ↑ 2 ) = 1 )
46 45 adantl ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ) → ( ( abs ‘ 𝐴 ) ↑ 2 ) = 1 )
47 absvalsq ( 𝐴 ∈ ℂ → ( ( abs ‘ 𝐴 ) ↑ 2 ) = ( 𝐴 · ( ∗ ‘ 𝐴 ) ) )
48 47 adantr ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ) → ( ( abs ‘ 𝐴 ) ↑ 2 ) = ( 𝐴 · ( ∗ ‘ 𝐴 ) ) )
49 46 48 eqtr3d ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ) → 1 = ( 𝐴 · ( ∗ ‘ 𝐴 ) ) )
50 49 3adant3 ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ 𝐴 ≠ 0 ) → 1 = ( 𝐴 · ( ∗ ‘ 𝐴 ) ) )
51 50 oveq1d ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ 𝐴 ≠ 0 ) → ( 1 / 𝐴 ) = ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) / 𝐴 ) )
52 simp1 ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ 𝐴 ≠ 0 ) → 𝐴 ∈ ℂ )
53 52 cjcld ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ 𝐴 ≠ 0 ) → ( ∗ ‘ 𝐴 ) ∈ ℂ )
54 simp3 ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ 𝐴 ≠ 0 ) → 𝐴 ≠ 0 )
55 53 52 54 divcan3d ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ 𝐴 ≠ 0 ) → ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) / 𝐴 ) = ( ∗ ‘ 𝐴 ) )
56 51 55 eqtrd ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ 𝐴 ≠ 0 ) → ( 1 / 𝐴 ) = ( ∗ ‘ 𝐴 ) )
57 42 56 syl3an3br ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 𝐴 = 0 ) → ( 1 / 𝐴 ) = ( ∗ ‘ 𝐴 ) )
58 41 57 mpd3an3 ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ) → ( 1 / 𝐴 ) = ( ∗ ‘ 𝐴 ) )
59 58 eqcomd ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ) → ( ∗ ‘ 𝐴 ) = ( 1 / 𝐴 ) )
60 59 3adant3 ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ( ∗ ‘ 𝐴 ) = ( 1 / 𝐴 ) )
61 60 negeqd ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → - ( ∗ ‘ 𝐴 ) = - ( 1 / 𝐴 ) )
62 31 61 eqtrd ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ( ∗ ‘ - 𝐴 ) = - ( 1 / 𝐴 ) )
63 62 oveq1d ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ( ( ∗ ‘ - 𝐴 ) / ( ∗ ‘ ( 1 − 𝐴 ) ) ) = ( - ( 1 / 𝐴 ) / ( ∗ ‘ ( 1 − 𝐴 ) ) ) )
64 cjsub ( ( 1 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ∗ ‘ ( 1 − 𝐴 ) ) = ( ( ∗ ‘ 1 ) − ( ∗ ‘ 𝐴 ) ) )
65 18 64 mpan ( 𝐴 ∈ ℂ → ( ∗ ‘ ( 1 − 𝐴 ) ) = ( ( ∗ ‘ 1 ) − ( ∗ ‘ 𝐴 ) ) )
66 1red ( 𝐴 ∈ ℂ → 1 ∈ ℝ )
67 66 cjred ( 𝐴 ∈ ℂ → ( ∗ ‘ 1 ) = 1 )
68 67 oveq1d ( 𝐴 ∈ ℂ → ( ( ∗ ‘ 1 ) − ( ∗ ‘ 𝐴 ) ) = ( 1 − ( ∗ ‘ 𝐴 ) ) )
69 65 68 eqtrd ( 𝐴 ∈ ℂ → ( ∗ ‘ ( 1 − 𝐴 ) ) = ( 1 − ( ∗ ‘ 𝐴 ) ) )
70 69 adantr ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ) → ( ∗ ‘ ( 1 − 𝐴 ) ) = ( 1 − ( ∗ ‘ 𝐴 ) ) )
71 59 oveq2d ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ) → ( 1 − ( ∗ ‘ 𝐴 ) ) = ( 1 − ( 1 / 𝐴 ) ) )
72 70 71 eqtrd ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ) → ( ∗ ‘ ( 1 − 𝐴 ) ) = ( 1 − ( 1 / 𝐴 ) ) )
73 72 3adant3 ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ( ∗ ‘ ( 1 − 𝐴 ) ) = ( 1 − ( 1 / 𝐴 ) ) )
74 73 oveq2d ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ( - ( 1 / 𝐴 ) / ( ∗ ‘ ( 1 − 𝐴 ) ) ) = ( - ( 1 / 𝐴 ) / ( 1 − ( 1 / 𝐴 ) ) ) )
75 30 63 74 3eqtrd ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ( ∗ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) = ( - ( 1 / 𝐴 ) / ( 1 − ( 1 / 𝐴 ) ) ) )
76 40 3ad2ant2 ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ¬ 𝐴 = 0 )
77 76 neqned ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → 𝐴 ≠ 0 )
78 1cnd ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → 1 ∈ ℂ )
79 simpl ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → 𝐴 ∈ ℂ )
80 simpr ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → 𝐴 ≠ 0 )
81 78 79 80 divnegd ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → - ( 1 / 𝐴 ) = ( - 1 / 𝐴 ) )
82 81 oveq1d ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( - ( 1 / 𝐴 ) / ( 1 − ( 1 / 𝐴 ) ) ) = ( ( - 1 / 𝐴 ) / ( 1 − ( 1 / 𝐴 ) ) ) )
83 15 77 82 syl2anc ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ( - ( 1 / 𝐴 ) / ( 1 − ( 1 / 𝐴 ) ) ) = ( ( - 1 / 𝐴 ) / ( 1 − ( 1 / 𝐴 ) ) ) )
84 14 negcld ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → - 1 ∈ ℂ )
85 84 15 77 divcld ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ( - 1 / 𝐴 ) ∈ ℂ )
86 15 77 reccld ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ( 1 / 𝐴 ) ∈ ℂ )
87 14 86 subcld ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ( 1 − ( 1 / 𝐴 ) ) ∈ ℂ )
88 16 24 cjne0d ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ( ∗ ‘ ( 1 − 𝐴 ) ) ≠ 0 )
89 73 88 eqnetrrd ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ( 1 − ( 1 / 𝐴 ) ) ≠ 0 )
90 85 87 15 89 77 divcan5d ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ( ( 𝐴 · ( - 1 / 𝐴 ) ) / ( 𝐴 · ( 1 − ( 1 / 𝐴 ) ) ) ) = ( ( - 1 / 𝐴 ) / ( 1 − ( 1 / 𝐴 ) ) ) )
91 84 15 77 divcan2d ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ( 𝐴 · ( - 1 / 𝐴 ) ) = - 1 )
92 15 14 86 subdid ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ( 𝐴 · ( 1 − ( 1 / 𝐴 ) ) ) = ( ( 𝐴 · 1 ) − ( 𝐴 · ( 1 / 𝐴 ) ) ) )
93 15 mulid1d ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ( 𝐴 · 1 ) = 𝐴 )
94 15 77 recidd ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ( 𝐴 · ( 1 / 𝐴 ) ) = 1 )
95 93 94 oveq12d ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ( ( 𝐴 · 1 ) − ( 𝐴 · ( 1 / 𝐴 ) ) ) = ( 𝐴 − 1 ) )
96 92 95 eqtrd ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ( 𝐴 · ( 1 − ( 1 / 𝐴 ) ) ) = ( 𝐴 − 1 ) )
97 91 96 oveq12d ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ( ( 𝐴 · ( - 1 / 𝐴 ) ) / ( 𝐴 · ( 1 − ( 1 / 𝐴 ) ) ) ) = ( - 1 / ( 𝐴 − 1 ) ) )
98 83 90 97 3eqtr2d ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ( - ( 1 / 𝐴 ) / ( 1 − ( 1 / 𝐴 ) ) ) = ( - 1 / ( 𝐴 − 1 ) ) )
99 subcl ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝐴 − 1 ) ∈ ℂ )
100 99 negnegd ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ) → - - ( 𝐴 − 1 ) = ( 𝐴 − 1 ) )
101 negsubdi2 ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ) → - ( 𝐴 − 1 ) = ( 1 − 𝐴 ) )
102 101 negeqd ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ) → - - ( 𝐴 − 1 ) = - ( 1 − 𝐴 ) )
103 100 102 eqtr3d ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝐴 − 1 ) = - ( 1 − 𝐴 ) )
104 15 14 103 syl2anc ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ( 𝐴 − 1 ) = - ( 1 − 𝐴 ) )
105 104 oveq2d ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ( - 1 / ( 𝐴 − 1 ) ) = ( - 1 / - ( 1 − 𝐴 ) ) )
106 75 98 105 3eqtrd ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ( ∗ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) = ( - 1 / - ( 1 − 𝐴 ) ) )
107 106 adantr ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) = 0 ) → ( ∗ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) = ( - 1 / - ( 1 − 𝐴 ) ) )
108 29 16 24 divcld ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ( - 𝐴 / ( 1 − 𝐴 ) ) ∈ ℂ )
109 108 adantr ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) = 0 ) → ( - 𝐴 / ( 1 − 𝐴 ) ) ∈ ℂ )
110 simpr ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) = 0 ) → ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) = 0 )
111 109 110 reim0bd ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) = 0 ) → ( - 𝐴 / ( 1 − 𝐴 ) ) ∈ ℝ )
112 111 cjred ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) = 0 ) → ( ∗ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) = ( - 𝐴 / ( 1 − 𝐴 ) ) )
113 112 111 eqeltrd ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) = 0 ) → ( ∗ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) ∈ ℝ )
114 107 113 eqeltrrd ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) = 0 ) → ( - 1 / - ( 1 − 𝐴 ) ) ∈ ℝ )
115 28 114 eqeltrrd ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) = 0 ) → ( 1 / ( 1 − 𝐴 ) ) ∈ ℝ )
116 16 24 recne0d ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ( 1 / ( 1 − 𝐴 ) ) ≠ 0 )
117 116 adantr ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) = 0 ) → ( 1 / ( 1 − 𝐴 ) ) ≠ 0 )
118 115 117 rereccld ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) = 0 ) → ( 1 / ( 1 / ( 1 − 𝐴 ) ) ) ∈ ℝ )
119 26 118 eqeltrrd ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) = 0 ) → ( 1 − 𝐴 ) ∈ ℝ )
120 1red ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) = 0 ) → 1 ∈ ℝ )
121 119 120 resubcld ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) = 0 ) → ( ( 1 − 𝐴 ) − 1 ) ∈ ℝ )
122 13 121 eqeltrrd ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) = 0 ) → - 𝐴 ∈ ℝ )
123 2 122 negrebd ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) = 0 ) → 𝐴 ∈ ℝ )
124 123 absord ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) = 0 ) → ( ( abs ‘ 𝐴 ) = 𝐴 ∨ ( abs ‘ 𝐴 ) = - 𝐴 ) )
125 eqeq1 ( ( abs ‘ 𝐴 ) = 1 → ( ( abs ‘ 𝐴 ) = 𝐴 ↔ 1 = 𝐴 ) )
126 125 biimpd ( ( abs ‘ 𝐴 ) = 1 → ( ( abs ‘ 𝐴 ) = 𝐴 → 1 = 𝐴 ) )
127 eqeq1 ( ( abs ‘ 𝐴 ) = 1 → ( ( abs ‘ 𝐴 ) = - 𝐴 ↔ 1 = - 𝐴 ) )
128 127 biimpd ( ( abs ‘ 𝐴 ) = 1 → ( ( abs ‘ 𝐴 ) = - 𝐴 → 1 = - 𝐴 ) )
129 126 128 orim12d ( ( abs ‘ 𝐴 ) = 1 → ( ( ( abs ‘ 𝐴 ) = 𝐴 ∨ ( abs ‘ 𝐴 ) = - 𝐴 ) → ( 1 = 𝐴 ∨ 1 = - 𝐴 ) ) )
130 7 124 129 sylc ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) = 0 ) → ( 1 = 𝐴 ∨ 1 = - 𝐴 ) )
131 130 ord ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) = 0 ) → ( ¬ 1 = 𝐴 → 1 = - 𝐴 ) )
132 6 131 mpd ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) = 0 ) → 1 = - 𝐴 )
133 132 5 eqeltrrd ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) = 0 ) → - 𝐴 ∈ ℝ+ )
134 5 133 rpaddcld ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) = 0 ) → ( 1 + - 𝐴 ) ∈ ℝ+ )
135 3 134 eqeltrrd ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) = 0 ) → ( 1 − 𝐴 ) ∈ ℝ+ )
136 135 relogcld ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) = 0 ) → ( log ‘ ( 1 − 𝐴 ) ) ∈ ℝ )
137 136 reim0d ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) = 0 ) → ( ℑ ‘ ( log ‘ ( 1 − 𝐴 ) ) ) = 0 )
138 133 135 rpdivcld ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) = 0 ) → ( - 𝐴 / ( 1 − 𝐴 ) ) ∈ ℝ+ )
139 138 relogcld ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) = 0 ) → ( log ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) ∈ ℝ )
140 139 reim0d ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) = 0 ) → ( ℑ ‘ ( log ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) ) = 0 )
141 137 140 eqtr4d ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) = 0 ) → ( ℑ ‘ ( log ‘ ( 1 − 𝐴 ) ) ) = ( ℑ ‘ ( log ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) ) )
142 16 24 logcld ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ( log ‘ ( 1 − 𝐴 ) ) ∈ ℂ )
143 142 adantr ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) ≠ 0 ) → ( log ‘ ( 1 − 𝐴 ) ) ∈ ℂ )
144 143 imcld ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) ≠ 0 ) → ( ℑ ‘ ( log ‘ ( 1 − 𝐴 ) ) ) ∈ ℝ )
145 144 recnd ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) ≠ 0 ) → ( ℑ ‘ ( log ‘ ( 1 − 𝐴 ) ) ) ∈ ℂ )
146 108 adantr ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) ≠ 0 ) → ( - 𝐴 / ( 1 − 𝐴 ) ) ∈ ℂ )
147 15 77 negne0d ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → - 𝐴 ≠ 0 )
148 29 16 147 24 divne0d ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ( - 𝐴 / ( 1 − 𝐴 ) ) ≠ 0 )
149 148 adantr ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) ≠ 0 ) → ( - 𝐴 / ( 1 − 𝐴 ) ) ≠ 0 )
150 146 149 logcld ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) ≠ 0 ) → ( log ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) ∈ ℂ )
151 150 imcld ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) ≠ 0 ) → ( ℑ ‘ ( log ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) ) ∈ ℝ )
152 151 recnd ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) ≠ 0 ) → ( ℑ ‘ ( log ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) ) ∈ ℂ )
153 106 fveq2d ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ( log ‘ ( ∗ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) ) = ( log ‘ ( - 1 / - ( 1 − 𝐴 ) ) ) )
154 153 adantr ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) ≠ 0 ) → ( log ‘ ( ∗ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) ) = ( log ‘ ( - 1 / - ( 1 − 𝐴 ) ) ) )
155 logcj ( ( ( - 𝐴 / ( 1 − 𝐴 ) ) ∈ ℂ ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) ≠ 0 ) → ( log ‘ ( ∗ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) ) = ( ∗ ‘ ( log ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) ) )
156 108 155 sylan ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) ≠ 0 ) → ( log ‘ ( ∗ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) ) = ( ∗ ‘ ( log ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) ) )
157 16 24 reccld ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ( 1 / ( 1 − 𝐴 ) ) ∈ ℂ )
158 157 116 logcld ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) ∈ ℂ )
159 158 negnegd ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → - - ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) = ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) )
160 isosctrlem1 ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ( ℑ ‘ ( log ‘ ( 1 − 𝐴 ) ) ) ≠ π )
161 logrec ( ( ( 1 − 𝐴 ) ∈ ℂ ∧ ( 1 − 𝐴 ) ≠ 0 ∧ ( ℑ ‘ ( log ‘ ( 1 − 𝐴 ) ) ) ≠ π ) → ( log ‘ ( 1 − 𝐴 ) ) = - ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) )
162 16 24 160 161 syl3anc ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ( log ‘ ( 1 − 𝐴 ) ) = - ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) )
163 162 negeqd ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → - ( log ‘ ( 1 − 𝐴 ) ) = - - ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) )
164 27 fveq2d ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ( log ‘ ( - 1 / - ( 1 − 𝐴 ) ) ) = ( log ‘ ( 1 / ( 1 − 𝐴 ) ) ) )
165 159 163 164 3eqtr4rd ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ( log ‘ ( - 1 / - ( 1 − 𝐴 ) ) ) = - ( log ‘ ( 1 − 𝐴 ) ) )
166 165 adantr ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) ≠ 0 ) → ( log ‘ ( - 1 / - ( 1 − 𝐴 ) ) ) = - ( log ‘ ( 1 − 𝐴 ) ) )
167 154 156 166 3eqtr3rd ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) ≠ 0 ) → - ( log ‘ ( 1 − 𝐴 ) ) = ( ∗ ‘ ( log ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) ) )
168 167 fveq2d ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) ≠ 0 ) → ( ℑ ‘ - ( log ‘ ( 1 − 𝐴 ) ) ) = ( ℑ ‘ ( ∗ ‘ ( log ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) ) ) )
169 143 imnegd ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) ≠ 0 ) → ( ℑ ‘ - ( log ‘ ( 1 − 𝐴 ) ) ) = - ( ℑ ‘ ( log ‘ ( 1 − 𝐴 ) ) ) )
170 150 imcjd ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) ≠ 0 ) → ( ℑ ‘ ( ∗ ‘ ( log ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) ) ) = - ( ℑ ‘ ( log ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) ) )
171 168 169 170 3eqtr3d ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) ≠ 0 ) → - ( ℑ ‘ ( log ‘ ( 1 − 𝐴 ) ) ) = - ( ℑ ‘ ( log ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) ) )
172 145 152 171 neg11d ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) ∧ ( ℑ ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) ≠ 0 ) → ( ℑ ‘ ( log ‘ ( 1 − 𝐴 ) ) ) = ( ℑ ‘ ( log ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) ) )
173 141 172 pm2.61dane ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) = 1 ∧ ¬ 1 = 𝐴 ) → ( ℑ ‘ ( log ‘ ( 1 − 𝐴 ) ) ) = ( ℑ ‘ ( log ‘ ( - 𝐴 / ( 1 − 𝐴 ) ) ) ) )