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 
|- ( ( A e. CC /\ ( abs ` A ) = 1 /\ -. 1 = A ) -> ( Im ` ( log ` ( 1 - A ) ) ) = ( Im ` ( log ` ( -u A / ( 1 - A ) ) ) ) )

Proof

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