Theorem isosctrlem2 25557

Description: Lemma for isosctr 25559. 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.)

Assertion

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

Proof of Theorem isosctrlem2

Step	Hyp	Ref	Expression
1		1cnd 10714	. . . . . . 7 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) = 0) → 1 ∈ ℂ)
2		simpl1 1192	. . . . . . 7 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) = 0) → 𝐴 ∈ ℂ)
3	1, 2	negsubd 11081	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) = 0) → (1 + -𝐴) = (1 − 𝐴))
4		1rp 12476	. . . . . . . 8 ⊢ 1 ∈ ℝ+
5	4	a1i 11	. . . . . . 7 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) = 0) → 1 ∈ ℝ+)
6		simpl3 1194	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) = 0) → ¬ 1 = 𝐴)
7		simpl2 1193	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) = 0) → (abs‘𝐴) = 1)
8	1, 2, 1	sub32d 11107	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) = 0) → ((1 − 𝐴) − 1) = ((1 − 1) − 𝐴))
9		1m1e0 11788	. . . . . . . . . . . . . . . . 17 ⊢ (1 − 1) = 0
10	9	oveq1i 7180	. . . . . . . . . . . . . . . 16 ⊢ ((1 − 1) − 𝐴) = (0 − 𝐴)
11		df-neg 10951	. . . . . . . . . . . . . . . 16 ⊢ -𝐴 = (0 − 𝐴)
12	10, 11	eqtr4i 2764	. . . . . . . . . . . . . . 15 ⊢ ((1 − 1) − 𝐴) = -𝐴
13	8, 12	eqtrdi 2789	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) = 0) → ((1 − 𝐴) − 1) = -𝐴)
14		1cnd 10714	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → 1 ∈ ℂ)
15		simp1 1137	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → 𝐴 ∈ ℂ)
16	14, 15	subcld 11075	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (1 − 𝐴) ∈ ℂ)
17	16	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) = 0) → (1 − 𝐴) ∈ ℂ)
18		ax-1cn 10673	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 ∈ ℂ
19		subeq0 10990	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((1 − 𝐴) = 0 ↔ 1 = 𝐴))
20	18, 19	mpan 690	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐴 ∈ ℂ → ((1 − 𝐴) = 0 ↔ 1 = 𝐴))
21	20	biimpd 232	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐴 ∈ ℂ → ((1 − 𝐴) = 0 → 1 = 𝐴))
22	21	con3dimp 412	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ ℂ ∧ ¬ 1 = 𝐴) → ¬ (1 − 𝐴) = 0)
23	22	neqned 2941	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℂ ∧ ¬ 1 = 𝐴) → (1 − 𝐴) ≠ 0)
24	23	3adant2 1132	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (1 − 𝐴) ≠ 0)
25	24	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) = 0) → (1 − 𝐴) ≠ 0)
26	17, 25	recrecd 11491	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) = 0) → (1 / (1 / (1 − 𝐴))) = (1 − 𝐴))
27	14, 16, 24	div2negd 11509	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (-1 / -(1 − 𝐴)) = (1 / (1 − 𝐴)))
28	27	adantr 484	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) = 0) → (-1 / -(1 − 𝐴)) = (1 / (1 − 𝐴)))
29	15	negcld 11062	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → -𝐴 ∈ ℂ)
30	29, 16, 24	cjdivd 14672	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (∗‘(-𝐴 / (1 − 𝐴))) = ((∗‘-𝐴) / (∗‘(1 − 𝐴))))
31	15	cjnegd 14660	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (∗‘-𝐴) = -(∗‘𝐴))
32		fveq2 6674	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝐴 = 0 → (abs‘𝐴) = (abs‘0))
33		abs0 14735	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (abs‘0) = 0
34	32, 33	eqtrdi 2789	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝐴 = 0 → (abs‘𝐴) = 0)
35		eqtr2 2759	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((abs‘𝐴) = 1 ∧ (abs‘𝐴) = 0) → 1 = 0)
36	34, 35	sylan2 596	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((abs‘𝐴) = 1 ∧ 𝐴 = 0) → 1 = 0)
37		ax-1ne0 10684	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 1 ≠ 0
38		neneq 2940	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (1 ≠ 0 → ¬ 1 = 0)
39	37, 38	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((abs‘𝐴) = 1 ∧ 𝐴 = 0) → ¬ 1 = 0)
40	36, 39	pm2.65da 817	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((abs‘𝐴) = 1 → ¬ 𝐴 = 0)
41	40	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1) → ¬ 𝐴 = 0)
42		df-ne 2935	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝐴 ≠ 0 ↔ ¬ 𝐴 = 0)
43		oveq1 7177	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((abs‘𝐴) = 1 → ((abs‘𝐴)↑2) = (1↑2))
44		sq1 13650	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (1↑2) = 1
45	43, 44	eqtrdi 2789	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((abs‘𝐴) = 1 → ((abs‘𝐴)↑2) = 1)
46	45	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1) → ((abs‘𝐴)↑2) = 1)
47		absvalsq 14730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝐴 ∈ ℂ → ((abs‘𝐴)↑2) = (𝐴 · (∗‘𝐴)))
48	47	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1) → ((abs‘𝐴)↑2) = (𝐴 · (∗‘𝐴)))
49	46, 48	eqtr3d 2775	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1) → 1 = (𝐴 · (∗‘𝐴)))
50	49	3adant3 1133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ 𝐴 ≠ 0) → 1 = (𝐴 · (∗‘𝐴)))
51	50	oveq1d 7185	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ 𝐴 ≠ 0) → (1 / 𝐴) = ((𝐴 · (∗‘𝐴)) / 𝐴))
52		simp1 1137	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ 𝐴 ≠ 0) → 𝐴 ∈ ℂ)
53	52	cjcld 14645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ 𝐴 ≠ 0) → (∗‘𝐴) ∈ ℂ)
54		simp3 1139	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ 𝐴 ≠ 0) → 𝐴 ≠ 0)
55	53, 52, 54	divcan3d 11499	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ 𝐴 ≠ 0) → ((𝐴 · (∗‘𝐴)) / 𝐴) = (∗‘𝐴))
56	51, 55	eqtrd 2773	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ 𝐴 ≠ 0) → (1 / 𝐴) = (∗‘𝐴))
57	42, 56	syl3an3br 1409	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 𝐴 = 0) → (1 / 𝐴) = (∗‘𝐴))
58	41, 57	mpd3an3 1463	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1) → (1 / 𝐴) = (∗‘𝐴))
59	58	eqcomd 2744	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1) → (∗‘𝐴) = (1 / 𝐴))
60	59	3adant3 1133	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (∗‘𝐴) = (1 / 𝐴))
61	60	negeqd 10958	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → -(∗‘𝐴) = -(1 / 𝐴))
62	31, 61	eqtrd 2773	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (∗‘-𝐴) = -(1 / 𝐴))
63	62	oveq1d 7185	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → ((∗‘-𝐴) / (∗‘(1 − 𝐴))) = (-(1 / 𝐴) / (∗‘(1 − 𝐴))))
64		cjsub 14598	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (∗‘(1 − 𝐴)) = ((∗‘1) − (∗‘𝐴)))
65	18, 64	mpan 690	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐴 ∈ ℂ → (∗‘(1 − 𝐴)) = ((∗‘1) − (∗‘𝐴)))
66		1red 10720	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝐴 ∈ ℂ → 1 ∈ ℝ)
67	66	cjred 14675	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐴 ∈ ℂ → (∗‘1) = 1)
68	67	oveq1d 7185	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐴 ∈ ℂ → ((∗‘1) − (∗‘𝐴)) = (1 − (∗‘𝐴)))
69	65, 68	eqtrd 2773	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐴 ∈ ℂ → (∗‘(1 − 𝐴)) = (1 − (∗‘𝐴)))
70	69	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1) → (∗‘(1 − 𝐴)) = (1 − (∗‘𝐴)))
71	59	oveq2d 7186	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1) → (1 − (∗‘𝐴)) = (1 − (1 / 𝐴)))
72	70, 71	eqtrd 2773	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1) → (∗‘(1 − 𝐴)) = (1 − (1 / 𝐴)))
73	72	3adant3 1133	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (∗‘(1 − 𝐴)) = (1 − (1 / 𝐴)))
74	73	oveq2d 7186	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (-(1 / 𝐴) / (∗‘(1 − 𝐴))) = (-(1 / 𝐴) / (1 − (1 / 𝐴))))
75	30, 63, 74	3eqtrd 2777	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (∗‘(-𝐴 / (1 − 𝐴))) = (-(1 / 𝐴) / (1 − (1 / 𝐴))))
76	40	3ad2ant2 1135	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → ¬ 𝐴 = 0)
77	76	neqned 2941	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → 𝐴 ≠ 0)
78		1cnd 10714	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → 1 ∈ ℂ)
79		simpl 486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → 𝐴 ∈ ℂ)
80		simpr 488	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → 𝐴 ≠ 0)
81	78, 79, 80	divnegd 11507	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → -(1 / 𝐴) = (-1 / 𝐴))
82	81	oveq1d 7185	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (-(1 / 𝐴) / (1 − (1 / 𝐴))) = ((-1 / 𝐴) / (1 − (1 / 𝐴))))
83	15, 77, 82	syl2anc 587	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (-(1 / 𝐴) / (1 − (1 / 𝐴))) = ((-1 / 𝐴) / (1 − (1 / 𝐴))))
84	14	negcld 11062	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → -1 ∈ ℂ)
85	84, 15, 77	divcld 11494	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (-1 / 𝐴) ∈ ℂ)
86	15, 77	reccld 11487	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (1 / 𝐴) ∈ ℂ)
87	14, 86	subcld 11075	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (1 − (1 / 𝐴)) ∈ ℂ)
88	16, 24	cjne0d 14652	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (∗‘(1 − 𝐴)) ≠ 0)
89	73, 88	eqnetrrd 3002	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (1 − (1 / 𝐴)) ≠ 0)
90	85, 87, 15, 89, 77	divcan5d 11520	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → ((𝐴 · (-1 / 𝐴)) / (𝐴 · (1 − (1 / 𝐴)))) = ((-1 / 𝐴) / (1 − (1 / 𝐴))))
91	84, 15, 77	divcan2d 11496	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (𝐴 · (-1 / 𝐴)) = -1)
92	15, 14, 86	subdid 11174	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (𝐴 · (1 − (1 / 𝐴))) = ((𝐴 · 1) − (𝐴 · (1 / 𝐴))))
93	15	mulid1d 10736	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (𝐴 · 1) = 𝐴)
94	15, 77	recidd 11489	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (𝐴 · (1 / 𝐴)) = 1)
95	93, 94	oveq12d 7188	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → ((𝐴 · 1) − (𝐴 · (1 / 𝐴))) = (𝐴 − 1))
96	92, 95	eqtrd 2773	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (𝐴 · (1 − (1 / 𝐴))) = (𝐴 − 1))
97	91, 96	oveq12d 7188	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → ((𝐴 · (-1 / 𝐴)) / (𝐴 · (1 − (1 / 𝐴)))) = (-1 / (𝐴 − 1)))
98	83, 90, 97	3eqtr2d 2779	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (-(1 / 𝐴) / (1 − (1 / 𝐴))) = (-1 / (𝐴 − 1)))
99		subcl 10963	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) → (𝐴 − 1) ∈ ℂ)
100	99	negnegd 11066	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) → --(𝐴 − 1) = (𝐴 − 1))
101		negsubdi2 11023	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) → -(𝐴 − 1) = (1 − 𝐴))
102	101	negeqd 10958	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) → --(𝐴 − 1) = -(1 − 𝐴))
103	100, 102	eqtr3d 2775	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) → (𝐴 − 1) = -(1 − 𝐴))
104	15, 14, 103	syl2anc 587	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (𝐴 − 1) = -(1 − 𝐴))
105	104	oveq2d 7186	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (-1 / (𝐴 − 1)) = (-1 / -(1 − 𝐴)))
106	75, 98, 105	3eqtrd 2777	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (∗‘(-𝐴 / (1 − 𝐴))) = (-1 / -(1 − 𝐴)))
107	106	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) = 0) → (∗‘(-𝐴 / (1 − 𝐴))) = (-1 / -(1 − 𝐴)))
108	29, 16, 24	divcld 11494	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (-𝐴 / (1 − 𝐴)) ∈ ℂ)
109	108	adantr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) = 0) → (-𝐴 / (1 − 𝐴)) ∈ ℂ)
110		simpr 488	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) = 0) → (ℑ‘(-𝐴 / (1 − 𝐴))) = 0)
111	109, 110	reim0bd 14649	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) = 0) → (-𝐴 / (1 − 𝐴)) ∈ ℝ)
112	111	cjred 14675	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) = 0) → (∗‘(-𝐴 / (1 − 𝐴))) = (-𝐴 / (1 − 𝐴)))
113	112, 111	eqeltrd 2833	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) = 0) → (∗‘(-𝐴 / (1 − 𝐴))) ∈ ℝ)
114	107, 113	eqeltrrd 2834	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) = 0) → (-1 / -(1 − 𝐴)) ∈ ℝ)
115	28, 114	eqeltrrd 2834	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) = 0) → (1 / (1 − 𝐴)) ∈ ℝ)
116	16, 24	recne0d 11488	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (1 / (1 − 𝐴)) ≠ 0)
117	116	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) = 0) → (1 / (1 − 𝐴)) ≠ 0)
118	115, 117	rereccld 11545	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) = 0) → (1 / (1 / (1 − 𝐴))) ∈ ℝ)
119	26, 118	eqeltrrd 2834	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) = 0) → (1 − 𝐴) ∈ ℝ)
120		1red 10720	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) = 0) → 1 ∈ ℝ)
121	119, 120	resubcld 11146	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) = 0) → ((1 − 𝐴) − 1) ∈ ℝ)
122	13, 121	eqeltrrd 2834	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) = 0) → -𝐴 ∈ ℝ)
123	2, 122	negrebd 11074	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) = 0) → 𝐴 ∈ ℝ)
124	123	absord 14865	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) = 0) → ((abs‘𝐴) = 𝐴 ∨ (abs‘𝐴) = -𝐴))
125		eqeq1 2742	. . . . . . . . . . . . 13 ⊢ ((abs‘𝐴) = 1 → ((abs‘𝐴) = 𝐴 ↔ 1 = 𝐴))
126	125	biimpd 232	. . . . . . . . . . . 12 ⊢ ((abs‘𝐴) = 1 → ((abs‘𝐴) = 𝐴 → 1 = 𝐴))
127		eqeq1 2742	. . . . . . . . . . . . 13 ⊢ ((abs‘𝐴) = 1 → ((abs‘𝐴) = -𝐴 ↔ 1 = -𝐴))
128	127	biimpd 232	. . . . . . . . . . . 12 ⊢ ((abs‘𝐴) = 1 → ((abs‘𝐴) = -𝐴 → 1 = -𝐴))
129	126, 128	orim12d 964	. . . . . . . . . . 11 ⊢ ((abs‘𝐴) = 1 → (((abs‘𝐴) = 𝐴 ∨ (abs‘𝐴) = -𝐴) → (1 = 𝐴 ∨ 1 = -𝐴)))
130	7, 124, 129	sylc 65	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) = 0) → (1 = 𝐴 ∨ 1 = -𝐴))
131	130	ord 863	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) = 0) → (¬ 1 = 𝐴 → 1 = -𝐴))
132	6, 131	mpd 15	. . . . . . . 8 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) = 0) → 1 = -𝐴)
133	132, 5	eqeltrrd 2834	. . . . . . 7 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) = 0) → -𝐴 ∈ ℝ+)
134	5, 133	rpaddcld 12529	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) = 0) → (1 + -𝐴) ∈ ℝ+)
135	3, 134	eqeltrrd 2834	. . . . 5 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) = 0) → (1 − 𝐴) ∈ ℝ+)
136	135	relogcld 25366	. . . 4 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) = 0) → (log‘(1 − 𝐴)) ∈ ℝ)
137	136	reim0d 14674	. . 3 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) = 0) → (ℑ‘(log‘(1 − 𝐴))) = 0)
138	133, 135	rpdivcld 12531	. . . . 5 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) = 0) → (-𝐴 / (1 − 𝐴)) ∈ ℝ+)
139	138	relogcld 25366	. . . 4 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) = 0) → (log‘(-𝐴 / (1 − 𝐴))) ∈ ℝ)
140	139	reim0d 14674	. . 3 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) = 0) → (ℑ‘(log‘(-𝐴 / (1 − 𝐴)))) = 0)
141	137, 140	eqtr4d 2776	. 2 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) = 0) → (ℑ‘(log‘(1 − 𝐴))) = (ℑ‘(log‘(-𝐴 / (1 − 𝐴)))))
142	16, 24	logcld 25314	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (log‘(1 − 𝐴)) ∈ ℂ)
143	142	adantr 484	. . . . 5 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) ≠ 0) → (log‘(1 − 𝐴)) ∈ ℂ)
144	143	imcld 14644	. . . 4 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) ≠ 0) → (ℑ‘(log‘(1 − 𝐴))) ∈ ℝ)
145	144	recnd 10747	. . 3 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) ≠ 0) → (ℑ‘(log‘(1 − 𝐴))) ∈ ℂ)
146	108	adantr 484	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) ≠ 0) → (-𝐴 / (1 − 𝐴)) ∈ ℂ)
147	15, 77	negne0d 11073	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → -𝐴 ≠ 0)
148	29, 16, 147, 24	divne0d 11510	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (-𝐴 / (1 − 𝐴)) ≠ 0)
149	148	adantr 484	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) ≠ 0) → (-𝐴 / (1 − 𝐴)) ≠ 0)
150	146, 149	logcld 25314	. . . . 5 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) ≠ 0) → (log‘(-𝐴 / (1 − 𝐴))) ∈ ℂ)
151	150	imcld 14644	. . . 4 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) ≠ 0) → (ℑ‘(log‘(-𝐴 / (1 − 𝐴)))) ∈ ℝ)
152	151	recnd 10747	. . 3 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) ≠ 0) → (ℑ‘(log‘(-𝐴 / (1 − 𝐴)))) ∈ ℂ)
153	106	fveq2d 6678	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (log‘(∗‘(-𝐴 / (1 − 𝐴)))) = (log‘(-1 / -(1 − 𝐴))))
154	153	adantr 484	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) ≠ 0) → (log‘(∗‘(-𝐴 / (1 − 𝐴)))) = (log‘(-1 / -(1 − 𝐴))))
155		logcj 25349	. . . . . . 7 ⊢ (((-𝐴 / (1 − 𝐴)) ∈ ℂ ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) ≠ 0) → (log‘(∗‘(-𝐴 / (1 − 𝐴)))) = (∗‘(log‘(-𝐴 / (1 − 𝐴)))))
156	108, 155	sylan 583	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) ≠ 0) → (log‘(∗‘(-𝐴 / (1 − 𝐴)))) = (∗‘(log‘(-𝐴 / (1 − 𝐴)))))
157	16, 24	reccld 11487	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (1 / (1 − 𝐴)) ∈ ℂ)
158	157, 116	logcld 25314	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (log‘(1 / (1 − 𝐴))) ∈ ℂ)
159	158	negnegd 11066	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → --(log‘(1 / (1 − 𝐴))) = (log‘(1 / (1 − 𝐴))))
160		isosctrlem1 25556	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (ℑ‘(log‘(1 − 𝐴))) ≠ π)
161		logrec 25501	. . . . . . . . . 10 ⊢ (((1 − 𝐴) ∈ ℂ ∧ (1 − 𝐴) ≠ 0 ∧ (ℑ‘(log‘(1 − 𝐴))) ≠ π) → (log‘(1 − 𝐴)) = -(log‘(1 / (1 − 𝐴))))
162	16, 24, 160, 161	syl3anc 1372	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (log‘(1 − 𝐴)) = -(log‘(1 / (1 − 𝐴))))
163	162	negeqd 10958	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → -(log‘(1 − 𝐴)) = --(log‘(1 / (1 − 𝐴))))
164	27	fveq2d 6678	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (log‘(-1 / -(1 − 𝐴))) = (log‘(1 / (1 − 𝐴))))
165	159, 163, 164	3eqtr4rd 2784	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (log‘(-1 / -(1 − 𝐴))) = -(log‘(1 − 𝐴)))
166	165	adantr 484	. . . . . 6 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) ≠ 0) → (log‘(-1 / -(1 − 𝐴))) = -(log‘(1 − 𝐴)))
167	154, 156, 166	3eqtr3rd 2782	. . . . 5 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) ≠ 0) → -(log‘(1 − 𝐴)) = (∗‘(log‘(-𝐴 / (1 − 𝐴)))))
168	167	fveq2d 6678	. . . 4 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) ≠ 0) → (ℑ‘-(log‘(1 − 𝐴))) = (ℑ‘(∗‘(log‘(-𝐴 / (1 − 𝐴))))))
169	143	imnegd 14659	. . . 4 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) ≠ 0) → (ℑ‘-(log‘(1 − 𝐴))) = -(ℑ‘(log‘(1 − 𝐴))))
170	150	imcjd 14654	. . . 4 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) ≠ 0) → (ℑ‘(∗‘(log‘(-𝐴 / (1 − 𝐴))))) = -(ℑ‘(log‘(-𝐴 / (1 − 𝐴)))))
171	168, 169, 170	3eqtr3d 2781	. . 3 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) ≠ 0) → -(ℑ‘(log‘(1 − 𝐴))) = -(ℑ‘(log‘(-𝐴 / (1 − 𝐴)))))
172	145, 152, 171	neg11d 11087	. 2 ⊢ (((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) ∧ (ℑ‘(-𝐴 / (1 − 𝐴))) ≠ 0) → (ℑ‘(log‘(1 − 𝐴))) = (ℑ‘(log‘(-𝐴 / (1 − 𝐴)))))
173	141, 172	pm2.61dane 3021	1 ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (ℑ‘(log‘(1 − 𝐴))) = (ℑ‘(log‘(-𝐴 / (1 − 𝐴)))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 846   ∧ w3a 1088   = wceq 1542   ∈ wcel 2114   ≠ wne 2934  ‘cfv 6339  (class class class)co 7170  ℂcc 10613  ℝcr 10614  0cc0 10615  1c1 10616   + caddc 10618   · cmul 10620   − cmin 10948  -cneg 10949   / cdiv 11375  2c2 11771  ℝ⁺crp 12472  ↑cexp 13521  ∗ccj 14545  ℑcim 14547  abscabs 14683  πcpi 15512  logclog 25298

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2710  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5232  ax-pr 5296  ax-un 7479  ax-inf2 9177  ax-cnex 10671  ax-resscn 10672  ax-1cn 10673  ax-icn 10674  ax-addcl 10675  ax-addrcl 10676  ax-mulcl 10677  ax-mulrcl 10678  ax-mulcom 10679  ax-addass 10680  ax-mulass 10681  ax-distr 10682  ax-i2m1 10683  ax-1ne0 10684  ax-1rid 10685  ax-rnegex 10686  ax-rrecex 10687  ax-cnre 10688  ax-pre-lttri 10689  ax-pre-lttrn 10690  ax-pre-ltadd 10691  ax-pre-mulgt0 10692  ax-pre-sup 10693  ax-addf 10694  ax-mulf 10695

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-nel 3039  df-ral 3058  df-rex 3059  df-reu 3060  df-rmo 3061  df-rab 3062  df-v 3400  df-sbc 3681  df-csb 3791  df-dif 3846  df-un 3848  df-in 3850  df-ss 3860  df-pss 3862  df-nul 4212  df-if 4415  df-pw 4490  df-sn 4517  df-pr 4519  df-tp 4521  df-op 4523  df-uni 4797  df-int 4837  df-iun 4883  df-iin 4884  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5429  df-eprel 5434  df-po 5442  df-so 5443  df-fr 5483  df-se 5484  df-we 5485  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-pred 6129  df-ord 6175  df-on 6176  df-lim 6177  df-suc 6178  df-iota 6297  df-fun 6341  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346  df-fv 6347  df-isom 6348  df-riota 7127  df-ov 7173  df-oprab 7174  df-mpo 7175  df-of 7425  df-om 7600  df-1st 7714  df-2nd 7715  df-supp 7857  df-wrecs 7976  df-recs 8037  df-rdg 8075  df-1o 8131  df-2o 8132  df-er 8320  df-map 8439  df-pm 8440  df-ixp 8508  df-en 8556  df-dom 8557  df-sdom 8558  df-fin 8559  df-fsupp 8907  df-fi 8948  df-sup 8979  df-inf 8980  df-oi 9047  df-card 9441  df-pnf 10755  df-mnf 10756  df-xr 10757  df-ltxr 10758  df-le 10759  df-sub 10950  df-neg 10951  df-div 11376  df-nn 11717  df-2 11779  df-3 11780  df-4 11781  df-5 11782  df-6 11783  df-7 11784  df-8 11785  df-9 11786  df-n0 11977  df-z 12063  df-dec 12180  df-uz 12325  df-q 12431  df-rp 12473  df-xneg 12590  df-xadd 12591  df-xmul 12592  df-ioo 12825  df-ioc 12826  df-ico 12827  df-icc 12828  df-fz 12982  df-fzo 13125  df-fl 13253  df-mod 13329  df-seq 13461  df-exp 13522  df-fac 13726  df-bc 13755  df-hash 13783  df-shft 14516  df-cj 14548  df-re 14549  df-im 14550  df-sqrt 14684  df-abs 14685  df-limsup 14918  df-clim 14935  df-rlim 14936  df-sum 15136  df-ef 15513  df-sin 15515  df-cos 15516  df-pi 15518  df-struct 16588  df-ndx 16589  df-slot 16590  df-base 16592  df-sets 16593  df-ress 16594  df-plusg 16681  df-mulr 16682  df-starv 16683  df-sca 16684  df-vsca 16685  df-ip 16686  df-tset 16687  df-ple 16688  df-ds 16690  df-unif 16691  df-hom 16692  df-cco 16693  df-rest 16799  df-topn 16800  df-0g 16818  df-gsum 16819  df-topgen 16820  df-pt 16821  df-prds 16824  df-xrs 16878  df-qtop 16883  df-imas 16884  df-xps 16886  df-mre 16960  df-mrc 16961  df-acs 16963  df-mgm 17968  df-sgrp 18017  df-mnd 18028  df-submnd 18073  df-mulg 18343  df-cntz 18565  df-cmn 19026  df-psmet 20209  df-xmet 20210  df-met 20211  df-bl 20212  df-mopn 20213  df-fbas 20214  df-fg 20215  df-cnfld 20218  df-top 21645  df-topon 21662  df-topsp 21684  df-bases 21697  df-cld 21770  df-ntr 21771  df-cls 21772  df-nei 21849  df-lp 21887  df-perf 21888  df-cn 21978  df-cnp 21979  df-haus 22066  df-tx 22313  df-hmeo 22506  df-fil 22597  df-fm 22689  df-flim 22690  df-flf 22691  df-xms 23073  df-ms 23074  df-tms 23075  df-cncf 23630  df-limc 24618  df-dv 24619  df-log 25300

This theorem is referenced by:  isosctrlem3  25558