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 mulridd โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ( 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 โˆ’ ๐ด ) ) ) ) )