Proof of Theorem isosctrlem2
Step | Hyp | Ref
| Expression |
1 | | 1cnd 10371 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) → 1
∈ ℂ) |
2 | | simpl1 1199 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
𝐴 ∈
ℂ) |
3 | 1, 2 | negsubd 10740 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) → (1
+ -𝐴) = (1 − 𝐴)) |
4 | | 1rp 12141 |
. . . . . . . 8
⊢ 1 ∈
ℝ+ |
5 | 4 | a1i 11 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) → 1
∈ ℝ+) |
6 | | simpl3 1203 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
¬ 1 = 𝐴) |
7 | | simpl2 1201 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
(abs‘𝐴) =
1) |
8 | 1, 2, 1 | sub32d 10766 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
((1 − 𝐴) − 1) =
((1 − 1) − 𝐴)) |
9 | | 1m1e0 11447 |
. . . . . . . . . . . . . . . . 17
⊢ (1
− 1) = 0 |
10 | 9 | oveq1i 6932 |
. . . . . . . . . . . . . . . 16
⊢ ((1
− 1) − 𝐴) = (0
− 𝐴) |
11 | | df-neg 10609 |
. . . . . . . . . . . . . . . 16
⊢ -𝐴 = (0 − 𝐴) |
12 | 10, 11 | eqtr4i 2805 |
. . . . . . . . . . . . . . 15
⊢ ((1
− 1) − 𝐴) =
-𝐴 |
13 | 8, 12 | syl6eq 2830 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
((1 − 𝐴) − 1) =
-𝐴) |
14 | | 1cnd 10371 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → 1
∈ ℂ) |
15 | | simp1 1127 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → 𝐴 ∈
ℂ) |
16 | 14, 15 | subcld 10734 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (1
− 𝐴) ∈
ℂ) |
17 | 16 | adantr 474 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) → (1
− 𝐴) ∈
ℂ) |
18 | | ax-1cn 10330 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 1 ∈
ℂ |
19 | | subeq0 10649 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((1
∈ ℂ ∧ 𝐴
∈ ℂ) → ((1 − 𝐴) = 0 ↔ 1 = 𝐴)) |
20 | 18, 19 | mpan 680 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐴 ∈ ℂ → ((1
− 𝐴) = 0 ↔ 1 =
𝐴)) |
21 | 20 | biimpd 221 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐴 ∈ ℂ → ((1
− 𝐴) = 0 → 1 =
𝐴)) |
22 | 21 | con3dimp 399 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ ℂ ∧ ¬ 1 =
𝐴) → ¬ (1 −
𝐴) = 0) |
23 | 22 | neqned 2976 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℂ ∧ ¬ 1 =
𝐴) → (1 − 𝐴) ≠ 0) |
24 | 23 | 3adant2 1122 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (1
− 𝐴) ≠
0) |
25 | 24 | adantr 474 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) → (1
− 𝐴) ≠
0) |
26 | 17, 25 | recrecd 11148 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) → (1
/ (1 / (1 − 𝐴))) = (1
− 𝐴)) |
27 | 14, 16, 24 | div2negd 11166 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (-1 /
-(1 − 𝐴)) = (1 / (1
− 𝐴))) |
28 | 27 | adantr 474 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
(-1 / -(1 − 𝐴)) = (1
/ (1 − 𝐴))) |
29 | 15 | negcld 10721 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → -𝐴 ∈
ℂ) |
30 | 29, 16, 24 | cjdivd 14370 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
(∗‘(-𝐴 / (1
− 𝐴))) =
((∗‘-𝐴) /
(∗‘(1 − 𝐴)))) |
31 | 15 | cjnegd 14358 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
(∗‘-𝐴) =
-(∗‘𝐴)) |
32 | | fveq2 6446 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝐴 = 0 → (abs‘𝐴) =
(abs‘0)) |
33 | | abs0 14432 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(abs‘0) = 0 |
34 | 32, 33 | syl6eq 2830 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝐴 = 0 → (abs‘𝐴) = 0) |
35 | | eqtr2 2800 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((abs‘𝐴) = 1
∧ (abs‘𝐴) = 0)
→ 1 = 0) |
36 | 34, 35 | sylan2 586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((abs‘𝐴) = 1
∧ 𝐴 = 0) → 1 =
0) |
37 | | ax-1ne0 10341 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ 1 ≠
0 |
38 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (1 ≠ 0
→ 1 ≠ 0) |
39 | 38 | neneqd 2974 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (1 ≠ 0
→ ¬ 1 = 0) |
40 | 37, 39 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((abs‘𝐴) = 1
∧ 𝐴 = 0) → ¬ 1
= 0) |
41 | 36, 40 | pm2.65da 807 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((abs‘𝐴) = 1
→ ¬ 𝐴 =
0) |
42 | 41 | adantl 475 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1) →
¬ 𝐴 =
0) |
43 | | df-ne 2970 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝐴 ≠ 0 ↔ ¬ 𝐴 = 0) |
44 | | oveq1 6929 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
((abs‘𝐴) = 1
→ ((abs‘𝐴)↑2) = (1↑2)) |
45 | | sq1 13277 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
(1↑2) = 1 |
46 | 44, 45 | syl6eq 2830 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
((abs‘𝐴) = 1
→ ((abs‘𝐴)↑2) = 1) |
47 | 46 | adantl 475 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1) →
((abs‘𝐴)↑2) =
1) |
48 | | absvalsq 14427 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝐴 ∈ ℂ →
((abs‘𝐴)↑2) =
(𝐴 ·
(∗‘𝐴))) |
49 | 48 | adantr 474 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1) →
((abs‘𝐴)↑2) =
(𝐴 ·
(∗‘𝐴))) |
50 | 47, 49 | eqtr3d 2816 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1) → 1
= (𝐴 ·
(∗‘𝐴))) |
51 | 50 | 3adant3 1123 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
𝐴 ≠ 0) → 1 = (𝐴 · (∗‘𝐴))) |
52 | 51 | oveq1d 6937 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
𝐴 ≠ 0) → (1 / 𝐴) = ((𝐴 · (∗‘𝐴)) / 𝐴)) |
53 | | simp1 1127 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
𝐴 ≠ 0) → 𝐴 ∈
ℂ) |
54 | 53 | cjcld 14343 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
𝐴 ≠ 0) →
(∗‘𝐴) ∈
ℂ) |
55 | | simp3 1129 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
𝐴 ≠ 0) → 𝐴 ≠ 0) |
56 | 54, 53, 55 | divcan3d 11156 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
𝐴 ≠ 0) → ((𝐴 · (∗‘𝐴)) / 𝐴) = (∗‘𝐴)) |
57 | 52, 56 | eqtrd 2814 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
𝐴 ≠ 0) → (1 / 𝐴) = (∗‘𝐴)) |
58 | 43, 57 | syl3an3br 1476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 𝐴 = 0) → (1 /
𝐴) = (∗‘𝐴)) |
59 | 42, 58 | mpd3an3 1535 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1) →
(1 / 𝐴) =
(∗‘𝐴)) |
60 | 59 | eqcomd 2784 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1) →
(∗‘𝐴) = (1 /
𝐴)) |
61 | 60 | 3adant3 1123 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
(∗‘𝐴) = (1 /
𝐴)) |
62 | 61 | negeqd 10616 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
-(∗‘𝐴) = -(1 /
𝐴)) |
63 | 31, 62 | eqtrd 2814 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
(∗‘-𝐴) = -(1 /
𝐴)) |
64 | 63 | oveq1d 6937 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
((∗‘-𝐴) /
(∗‘(1 − 𝐴))) = (-(1 / 𝐴) / (∗‘(1 − 𝐴)))) |
65 | | cjsub 14296 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((1
∈ ℂ ∧ 𝐴
∈ ℂ) → (∗‘(1 − 𝐴)) = ((∗‘1) −
(∗‘𝐴))) |
66 | 18, 65 | mpan 680 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐴 ∈ ℂ →
(∗‘(1 − 𝐴)) = ((∗‘1) −
(∗‘𝐴))) |
67 | | 1red 10377 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝐴 ∈ ℂ → 1 ∈
ℝ) |
68 | 67 | cjred 14373 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐴 ∈ ℂ →
(∗‘1) = 1) |
69 | 68 | oveq1d 6937 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐴 ∈ ℂ →
((∗‘1) − (∗‘𝐴)) = (1 − (∗‘𝐴))) |
70 | 66, 69 | eqtrd 2814 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐴 ∈ ℂ →
(∗‘(1 − 𝐴)) = (1 − (∗‘𝐴))) |
71 | 70 | adantr 474 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1) →
(∗‘(1 − 𝐴)) = (1 − (∗‘𝐴))) |
72 | 60 | oveq2d 6938 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1) →
(1 − (∗‘𝐴)) = (1 − (1 / 𝐴))) |
73 | 71, 72 | eqtrd 2814 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1) →
(∗‘(1 − 𝐴)) = (1 − (1 / 𝐴))) |
74 | 73 | 3adant3 1123 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
(∗‘(1 − 𝐴)) = (1 − (1 / 𝐴))) |
75 | 74 | oveq2d 6938 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (-(1 /
𝐴) / (∗‘(1
− 𝐴))) = (-(1 / 𝐴) / (1 − (1 / 𝐴)))) |
76 | 30, 64, 75 | 3eqtrd 2818 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
(∗‘(-𝐴 / (1
− 𝐴))) = (-(1 / 𝐴) / (1 − (1 / 𝐴)))) |
77 | 41 | 3ad2ant2 1125 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → ¬
𝐴 = 0) |
78 | 77 | neqned 2976 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → 𝐴 ≠ 0) |
79 | | 1cnd 10371 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → 1 ∈
ℂ) |
80 | | simpl 476 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → 𝐴 ∈
ℂ) |
81 | | simpr 479 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → 𝐴 ≠ 0) |
82 | 79, 80, 81 | divnegd 11164 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → -(1 / 𝐴) = (-1 / 𝐴)) |
83 | 82 | oveq1d 6937 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (-(1 / 𝐴) / (1 − (1 / 𝐴))) = ((-1 / 𝐴) / (1 − (1 / 𝐴)))) |
84 | 15, 78, 83 | syl2anc 579 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (-(1 /
𝐴) / (1 − (1 / 𝐴))) = ((-1 / 𝐴) / (1 − (1 / 𝐴)))) |
85 | 14 | negcld 10721 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → -1
∈ ℂ) |
86 | 85, 15, 78 | divcld 11151 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (-1 /
𝐴) ∈
ℂ) |
87 | 15, 78 | reccld 11144 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (1 /
𝐴) ∈
ℂ) |
88 | 14, 87 | subcld 10734 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (1
− (1 / 𝐴)) ∈
ℂ) |
89 | 16, 24 | cjne0d 14350 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
(∗‘(1 − 𝐴)) ≠ 0) |
90 | 74, 89 | eqnetrrd 3037 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (1
− (1 / 𝐴)) ≠
0) |
91 | 86, 88, 15, 90, 78 | divcan5d 11177 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → ((𝐴 · (-1 / 𝐴)) / (𝐴 · (1 − (1 / 𝐴)))) = ((-1 / 𝐴) / (1 − (1 / 𝐴)))) |
92 | 85, 15, 78 | divcan2d 11153 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (𝐴 · (-1 / 𝐴)) = -1) |
93 | 15, 14, 87 | subdid 10831 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (𝐴 · (1 − (1 / 𝐴))) = ((𝐴 · 1) − (𝐴 · (1 / 𝐴)))) |
94 | 15 | mulid1d 10394 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (𝐴 · 1) = 𝐴) |
95 | 15, 78 | recidd 11146 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (𝐴 · (1 / 𝐴)) = 1) |
96 | 94, 95 | oveq12d 6940 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → ((𝐴 · 1) − (𝐴 · (1 / 𝐴))) = (𝐴 − 1)) |
97 | 93, 96 | eqtrd 2814 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (𝐴 · (1 − (1 / 𝐴))) = (𝐴 − 1)) |
98 | 92, 97 | oveq12d 6940 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → ((𝐴 · (-1 / 𝐴)) / (𝐴 · (1 − (1 / 𝐴)))) = (-1 / (𝐴 − 1))) |
99 | 84, 91, 98 | 3eqtr2d 2820 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (-(1 /
𝐴) / (1 − (1 / 𝐴))) = (-1 / (𝐴 − 1))) |
100 | | subcl 10621 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → (𝐴 −
1) ∈ ℂ) |
101 | 100 | negnegd 10725 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → --(𝐴
− 1) = (𝐴 −
1)) |
102 | | negsubdi2 10682 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → -(𝐴 −
1) = (1 − 𝐴)) |
103 | 102 | negeqd 10616 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → --(𝐴
− 1) = -(1 − 𝐴)) |
104 | 101, 103 | eqtr3d 2816 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → (𝐴 −
1) = -(1 − 𝐴)) |
105 | 15, 14, 104 | syl2anc 579 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (𝐴 − 1) = -(1 − 𝐴)) |
106 | 105 | oveq2d 6938 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (-1 /
(𝐴 − 1)) = (-1 / -(1
− 𝐴))) |
107 | 76, 99, 106 | 3eqtrd 2818 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
(∗‘(-𝐴 / (1
− 𝐴))) = (-1 / -(1
− 𝐴))) |
108 | 107 | adantr 474 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
(∗‘(-𝐴 / (1
− 𝐴))) = (-1 / -(1
− 𝐴))) |
109 | 29, 16, 24 | divcld 11151 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (-𝐴 / (1 − 𝐴)) ∈ ℂ) |
110 | 109 | adantr 474 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
(-𝐴 / (1 − 𝐴)) ∈
ℂ) |
111 | | simpr 479 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
(ℑ‘(-𝐴 / (1
− 𝐴))) =
0) |
112 | 110, 111 | reim0bd 14347 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
(-𝐴 / (1 − 𝐴)) ∈
ℝ) |
113 | 112 | cjred 14373 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
(∗‘(-𝐴 / (1
− 𝐴))) = (-𝐴 / (1 − 𝐴))) |
114 | 113, 112 | eqeltrd 2859 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
(∗‘(-𝐴 / (1
− 𝐴))) ∈
ℝ) |
115 | 108, 114 | eqeltrrd 2860 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
(-1 / -(1 − 𝐴))
∈ ℝ) |
116 | 28, 115 | eqeltrrd 2860 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) → (1
/ (1 − 𝐴)) ∈
ℝ) |
117 | 16, 24 | recne0d 11145 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (1 / (1
− 𝐴)) ≠
0) |
118 | 117 | adantr 474 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) → (1
/ (1 − 𝐴)) ≠
0) |
119 | 116, 118 | rereccld 11202 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) → (1
/ (1 / (1 − 𝐴)))
∈ ℝ) |
120 | 26, 119 | eqeltrrd 2860 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) → (1
− 𝐴) ∈
ℝ) |
121 | | 1red 10377 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) → 1
∈ ℝ) |
122 | 120, 121 | resubcld 10803 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
((1 − 𝐴) − 1)
∈ ℝ) |
123 | 13, 122 | eqeltrrd 2860 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
-𝐴 ∈
ℝ) |
124 | 2, 123 | negrebd 10733 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
𝐴 ∈
ℝ) |
125 | 124 | absord 14562 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
((abs‘𝐴) = 𝐴 ∨ (abs‘𝐴) = -𝐴)) |
126 | | eqeq1 2782 |
. . . . . . . . . . . . 13
⊢
((abs‘𝐴) = 1
→ ((abs‘𝐴) =
𝐴 ↔ 1 = 𝐴)) |
127 | 126 | biimpd 221 |
. . . . . . . . . . . 12
⊢
((abs‘𝐴) = 1
→ ((abs‘𝐴) =
𝐴 → 1 = 𝐴)) |
128 | | eqeq1 2782 |
. . . . . . . . . . . . 13
⊢
((abs‘𝐴) = 1
→ ((abs‘𝐴) =
-𝐴 ↔ 1 = -𝐴)) |
129 | 128 | biimpd 221 |
. . . . . . . . . . . 12
⊢
((abs‘𝐴) = 1
→ ((abs‘𝐴) =
-𝐴 → 1 = -𝐴)) |
130 | 127, 129 | orim12d 950 |
. . . . . . . . . . 11
⊢
((abs‘𝐴) = 1
→ (((abs‘𝐴) =
𝐴 ∨ (abs‘𝐴) = -𝐴) → (1 = 𝐴 ∨ 1 = -𝐴))) |
131 | 7, 125, 130 | sylc 65 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) → (1
= 𝐴 ∨ 1 = -𝐴)) |
132 | 131 | ord 853 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
(¬ 1 = 𝐴 → 1 =
-𝐴)) |
133 | 6, 132 | mpd 15 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) → 1
= -𝐴) |
134 | 133, 5 | eqeltrrd 2860 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
-𝐴 ∈
ℝ+) |
135 | 5, 134 | rpaddcld 12196 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) → (1
+ -𝐴) ∈
ℝ+) |
136 | 3, 135 | eqeltrrd 2860 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) → (1
− 𝐴) ∈
ℝ+) |
137 | 136 | relogcld 24806 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
(log‘(1 − 𝐴))
∈ ℝ) |
138 | 137 | reim0d 14372 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
(ℑ‘(log‘(1 − 𝐴))) = 0) |
139 | 134, 136 | rpdivcld 12198 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
(-𝐴 / (1 − 𝐴)) ∈
ℝ+) |
140 | 139 | relogcld 24806 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
(log‘(-𝐴 / (1 −
𝐴))) ∈
ℝ) |
141 | 140 | reim0d 14372 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
(ℑ‘(log‘(-𝐴 / (1 − 𝐴)))) = 0) |
142 | 138, 141 | eqtr4d 2817 |
. 2
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
(ℑ‘(log‘(1 − 𝐴))) = (ℑ‘(log‘(-𝐴 / (1 − 𝐴))))) |
143 | 16, 24 | logcld 24754 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
(log‘(1 − 𝐴))
∈ ℂ) |
144 | 143 | adantr 474 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
(log‘(1 − 𝐴))
∈ ℂ) |
145 | 144 | imcld 14342 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
(ℑ‘(log‘(1 − 𝐴))) ∈ ℝ) |
146 | 145 | recnd 10405 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
(ℑ‘(log‘(1 − 𝐴))) ∈ ℂ) |
147 | 109 | adantr 474 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
(-𝐴 / (1 − 𝐴)) ∈
ℂ) |
148 | 15, 78 | negne0d 10732 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → -𝐴 ≠ 0) |
149 | 29, 16, 148, 24 | divne0d 11167 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (-𝐴 / (1 − 𝐴)) ≠ 0) |
150 | 149 | adantr 474 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
(-𝐴 / (1 − 𝐴)) ≠ 0) |
151 | 147, 150 | logcld 24754 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
(log‘(-𝐴 / (1 −
𝐴))) ∈
ℂ) |
152 | 151 | imcld 14342 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
(ℑ‘(log‘(-𝐴 / (1 − 𝐴)))) ∈ ℝ) |
153 | 152 | recnd 10405 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
(ℑ‘(log‘(-𝐴 / (1 − 𝐴)))) ∈ ℂ) |
154 | 107 | fveq2d 6450 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
(log‘(∗‘(-𝐴 / (1 − 𝐴)))) = (log‘(-1 / -(1 − 𝐴)))) |
155 | 154 | adantr 474 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
(log‘(∗‘(-𝐴 / (1 − 𝐴)))) = (log‘(-1 / -(1 − 𝐴)))) |
156 | | logcj 24789 |
. . . . . . 7
⊢ (((-𝐴 / (1 − 𝐴)) ∈ ℂ ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
(log‘(∗‘(-𝐴 / (1 − 𝐴)))) = (∗‘(log‘(-𝐴 / (1 − 𝐴))))) |
157 | 109, 156 | sylan 575 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
(log‘(∗‘(-𝐴 / (1 − 𝐴)))) = (∗‘(log‘(-𝐴 / (1 − 𝐴))))) |
158 | 16, 24 | reccld 11144 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (1 / (1
− 𝐴)) ∈
ℂ) |
159 | 158, 117 | logcld 24754 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
(log‘(1 / (1 − 𝐴))) ∈ ℂ) |
160 | 159 | negnegd 10725 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
--(log‘(1 / (1 − 𝐴))) = (log‘(1 / (1 − 𝐴)))) |
161 | | isosctrlem1 24996 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
(ℑ‘(log‘(1 − 𝐴))) ≠ π) |
162 | | logrec 24941 |
. . . . . . . . . 10
⊢ (((1
− 𝐴) ∈ ℂ
∧ (1 − 𝐴) ≠ 0
∧ (ℑ‘(log‘(1 − 𝐴))) ≠ π) → (log‘(1 −
𝐴)) = -(log‘(1 / (1
− 𝐴)))) |
163 | 16, 24, 161, 162 | syl3anc 1439 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
(log‘(1 − 𝐴)) =
-(log‘(1 / (1 − 𝐴)))) |
164 | 163 | negeqd 10616 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
-(log‘(1 − 𝐴))
= --(log‘(1 / (1 − 𝐴)))) |
165 | 27 | fveq2d 6450 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
(log‘(-1 / -(1 − 𝐴))) = (log‘(1 / (1 − 𝐴)))) |
166 | 160, 164,
165 | 3eqtr4rd 2825 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
(log‘(-1 / -(1 − 𝐴))) = -(log‘(1 − 𝐴))) |
167 | 166 | adantr 474 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
(log‘(-1 / -(1 − 𝐴))) = -(log‘(1 − 𝐴))) |
168 | 155, 157,
167 | 3eqtr3rd 2823 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
-(log‘(1 − 𝐴))
= (∗‘(log‘(-𝐴 / (1 − 𝐴))))) |
169 | 168 | fveq2d 6450 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
(ℑ‘-(log‘(1 − 𝐴))) =
(ℑ‘(∗‘(log‘(-𝐴 / (1 − 𝐴)))))) |
170 | 144 | imnegd 14357 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
(ℑ‘-(log‘(1 − 𝐴))) = -(ℑ‘(log‘(1 −
𝐴)))) |
171 | 151 | imcjd 14352 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
(ℑ‘(∗‘(log‘(-𝐴 / (1 − 𝐴))))) = -(ℑ‘(log‘(-𝐴 / (1 − 𝐴))))) |
172 | 169, 170,
171 | 3eqtr3d 2822 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
-(ℑ‘(log‘(1 − 𝐴))) = -(ℑ‘(log‘(-𝐴 / (1 − 𝐴))))) |
173 | 146, 153,
172 | neg11d 10746 |
. 2
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
(ℑ‘(log‘(1 − 𝐴))) = (ℑ‘(log‘(-𝐴 / (1 − 𝐴))))) |
174 | 142, 173 | pm2.61dane 3057 |
1
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
(ℑ‘(log‘(1 − 𝐴))) = (ℑ‘(log‘(-𝐴 / (1 − 𝐴))))) |