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 − 𝐴 ) ) ) ) )