Proof of Theorem isosctrlem2
Step | Hyp | Ref
| Expression |
1 | | 1cnd 10056 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) → 1
∈ ℂ) |
2 | | simpl1 1064 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
𝐴 ∈
ℂ) |
3 | 1, 2 | negsubd 10398 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) → (1
+ -𝐴) = (1 − 𝐴)) |
4 | | 1rp 11836 |
. . . . . . . 8
⊢ 1 ∈
ℝ+ |
5 | 4 | a1i 11 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) → 1
∈ ℝ+) |
6 | | simpl3 1066 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
¬ 1 = 𝐴) |
7 | | simpl2 1065 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
(abs‘𝐴) =
1) |
8 | 1, 2, 1 | sub32d 10424 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
((1 − 𝐴) − 1) =
((1 − 1) − 𝐴)) |
9 | | 1m1e0 11089 |
. . . . . . . . . . . . . . . . 17
⊢ (1
− 1) = 0 |
10 | 9 | oveq1i 6660 |
. . . . . . . . . . . . . . . 16
⊢ ((1
− 1) − 𝐴) = (0
− 𝐴) |
11 | | df-neg 10269 |
. . . . . . . . . . . . . . . 16
⊢ -𝐴 = (0 − 𝐴) |
12 | 10, 11 | eqtr4i 2647 |
. . . . . . . . . . . . . . 15
⊢ ((1
− 1) − 𝐴) =
-𝐴 |
13 | 8, 12 | syl6eq 2672 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
((1 − 𝐴) − 1) =
-𝐴) |
14 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → 1
∈ ℂ) |
15 | | simp1 1061 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → 𝐴 ∈
ℂ) |
16 | 14, 15 | subcld 10392 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (1
− 𝐴) ∈
ℂ) |
17 | 16 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) → (1
− 𝐴) ∈
ℂ) |
18 | | ax-1cn 9994 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 1 ∈
ℂ |
19 | | subeq0 10307 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((1
∈ ℂ ∧ 𝐴
∈ ℂ) → ((1 − 𝐴) = 0 ↔ 1 = 𝐴)) |
20 | 18, 19 | mpan 706 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐴 ∈ ℂ → ((1
− 𝐴) = 0 ↔ 1 =
𝐴)) |
21 | 20 | biimpd 219 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐴 ∈ ℂ → ((1
− 𝐴) = 0 → 1 =
𝐴)) |
22 | 21 | con3dimp 457 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ ℂ ∧ ¬ 1 =
𝐴) → ¬ (1 −
𝐴) = 0) |
23 | 22 | neqned 2801 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℂ ∧ ¬ 1 =
𝐴) → (1 − 𝐴) ≠ 0) |
24 | 23 | 3adant2 1080 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (1
− 𝐴) ≠
0) |
25 | 24 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) → (1
− 𝐴) ≠
0) |
26 | 17, 25 | recrecd 10798 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) → (1
/ (1 / (1 − 𝐴))) = (1
− 𝐴)) |
27 | 14, 16, 24 | div2negd 10816 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (-1 /
-(1 − 𝐴)) = (1 / (1
− 𝐴))) |
28 | 27 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
(-1 / -(1 − 𝐴)) = (1
/ (1 − 𝐴))) |
29 | 15 | negcld 10379 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → -𝐴 ∈
ℂ) |
30 | 29, 16, 24 | cjdivd 13963 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
(∗‘(-𝐴 / (1
− 𝐴))) =
((∗‘-𝐴) /
(∗‘(1 − 𝐴)))) |
31 | 15 | cjnegd 13951 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
(∗‘-𝐴) =
-(∗‘𝐴)) |
32 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝐴 = 0 → (abs‘𝐴) =
(abs‘0)) |
33 | | abs0 14025 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(abs‘0) = 0 |
34 | 32, 33 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝐴 = 0 → (abs‘𝐴) = 0) |
35 | | eqtr2 2642 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((abs‘𝐴) = 1
∧ (abs‘𝐴) = 0)
→ 1 = 0) |
36 | 34, 35 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((abs‘𝐴) = 1
∧ 𝐴 = 0) → 1 =
0) |
37 | | ax-1ne0 10005 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ 1 ≠
0 |
38 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (1 ≠ 0
→ 1 ≠ 0) |
39 | 38 | neneqd 2799 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (1 ≠ 0
→ ¬ 1 = 0) |
40 | 37, 39 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((abs‘𝐴) = 1
∧ 𝐴 = 0) → ¬ 1
= 0) |
41 | 36, 40 | pm2.65da 600 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((abs‘𝐴) = 1
→ ¬ 𝐴 =
0) |
42 | 41 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1) →
¬ 𝐴 =
0) |
43 | | df-ne 2795 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝐴 ≠ 0 ↔ ¬ 𝐴 = 0) |
44 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
((abs‘𝐴) = 1
→ ((abs‘𝐴)↑2) = (1↑2)) |
45 | | sq1 12958 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
(1↑2) = 1 |
46 | 44, 45 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
((abs‘𝐴) = 1
→ ((abs‘𝐴)↑2) = 1) |
47 | 46 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1) →
((abs‘𝐴)↑2) =
1) |
48 | | absvalsq 14020 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝐴 ∈ ℂ →
((abs‘𝐴)↑2) =
(𝐴 ·
(∗‘𝐴))) |
49 | 48 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1) →
((abs‘𝐴)↑2) =
(𝐴 ·
(∗‘𝐴))) |
50 | 47, 49 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1) → 1
= (𝐴 ·
(∗‘𝐴))) |
51 | 50 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
𝐴 ≠ 0) → 1 = (𝐴 · (∗‘𝐴))) |
52 | 51 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
𝐴 ≠ 0) → (1 / 𝐴) = ((𝐴 · (∗‘𝐴)) / 𝐴)) |
53 | | simp1 1061 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
𝐴 ≠ 0) → 𝐴 ∈
ℂ) |
54 | 53 | cjcld 13936 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
𝐴 ≠ 0) →
(∗‘𝐴) ∈
ℂ) |
55 | | simp3 1063 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
𝐴 ≠ 0) → 𝐴 ≠ 0) |
56 | 54, 53, 55 | divcan3d 10806 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
𝐴 ≠ 0) → ((𝐴 · (∗‘𝐴)) / 𝐴) = (∗‘𝐴)) |
57 | 52, 56 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
𝐴 ≠ 0) → (1 / 𝐴) = (∗‘𝐴)) |
58 | 43, 57 | syl3an3br 1367 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 𝐴 = 0) → (1 /
𝐴) = (∗‘𝐴)) |
59 | 42, 58 | mpd3an3 1425 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1) →
(1 / 𝐴) =
(∗‘𝐴)) |
60 | 59 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1) →
(∗‘𝐴) = (1 /
𝐴)) |
61 | 60 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
(∗‘𝐴) = (1 /
𝐴)) |
62 | 61 | negeqd 10275 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
-(∗‘𝐴) = -(1 /
𝐴)) |
63 | 31, 62 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
(∗‘-𝐴) = -(1 /
𝐴)) |
64 | 63 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
((∗‘-𝐴) /
(∗‘(1 − 𝐴))) = (-(1 / 𝐴) / (∗‘(1 − 𝐴)))) |
65 | | cjsub 13889 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((1
∈ ℂ ∧ 𝐴
∈ ℂ) → (∗‘(1 − 𝐴)) = ((∗‘1) −
(∗‘𝐴))) |
66 | 18, 65 | mpan 706 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐴 ∈ ℂ →
(∗‘(1 − 𝐴)) = ((∗‘1) −
(∗‘𝐴))) |
67 | | 1red 10055 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝐴 ∈ ℂ → 1 ∈
ℝ) |
68 | 67 | cjred 13966 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐴 ∈ ℂ →
(∗‘1) = 1) |
69 | 68 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐴 ∈ ℂ →
((∗‘1) − (∗‘𝐴)) = (1 − (∗‘𝐴))) |
70 | 66, 69 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐴 ∈ ℂ →
(∗‘(1 − 𝐴)) = (1 − (∗‘𝐴))) |
71 | 70 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1) →
(∗‘(1 − 𝐴)) = (1 − (∗‘𝐴))) |
72 | 60 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1) →
(1 − (∗‘𝐴)) = (1 − (1 / 𝐴))) |
73 | 71, 72 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1) →
(∗‘(1 − 𝐴)) = (1 − (1 / 𝐴))) |
74 | 73 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
(∗‘(1 − 𝐴)) = (1 − (1 / 𝐴))) |
75 | 74 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (-(1 /
𝐴) / (∗‘(1
− 𝐴))) = (-(1 / 𝐴) / (1 − (1 / 𝐴)))) |
76 | 30, 64, 75 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
(∗‘(-𝐴 / (1
− 𝐴))) = (-(1 / 𝐴) / (1 − (1 / 𝐴)))) |
77 | 41 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → ¬
𝐴 = 0) |
78 | 77 | neqned 2801 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → 𝐴 ≠ 0) |
79 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → 1 ∈
ℂ) |
80 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → 𝐴 ∈
ℂ) |
81 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → 𝐴 ≠ 0) |
82 | 79, 80, 81 | divnegd 10814 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → -(1 / 𝐴) = (-1 / 𝐴)) |
83 | 82 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (-(1 / 𝐴) / (1 − (1 / 𝐴))) = ((-1 / 𝐴) / (1 − (1 / 𝐴)))) |
84 | 15, 78, 83 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (-(1 /
𝐴) / (1 − (1 / 𝐴))) = ((-1 / 𝐴) / (1 − (1 / 𝐴)))) |
85 | 14 | negcld 10379 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → -1
∈ ℂ) |
86 | 85, 15, 78 | divcld 10801 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (-1 /
𝐴) ∈
ℂ) |
87 | 15, 78 | reccld 10794 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (1 /
𝐴) ∈
ℂ) |
88 | 14, 87 | subcld 10392 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (1
− (1 / 𝐴)) ∈
ℂ) |
89 | 16, 24 | cjne0d 13943 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
(∗‘(1 − 𝐴)) ≠ 0) |
90 | 74, 89 | eqnetrrd 2862 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (1
− (1 / 𝐴)) ≠
0) |
91 | 86, 88, 15, 90, 78 | divcan5d 10827 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → ((𝐴 · (-1 / 𝐴)) / (𝐴 · (1 − (1 / 𝐴)))) = ((-1 / 𝐴) / (1 − (1 / 𝐴)))) |
92 | 85, 15, 78 | divcan2d 10803 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (𝐴 · (-1 / 𝐴)) = -1) |
93 | 15, 14, 87 | subdid 10486 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (𝐴 · (1 − (1 / 𝐴))) = ((𝐴 · 1) − (𝐴 · (1 / 𝐴)))) |
94 | 15 | mulid1d 10057 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (𝐴 · 1) = 𝐴) |
95 | 15, 78 | recidd 10796 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (𝐴 · (1 / 𝐴)) = 1) |
96 | 94, 95 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → ((𝐴 · 1) − (𝐴 · (1 / 𝐴))) = (𝐴 − 1)) |
97 | 93, 96 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (𝐴 · (1 − (1 / 𝐴))) = (𝐴 − 1)) |
98 | 92, 97 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → ((𝐴 · (-1 / 𝐴)) / (𝐴 · (1 − (1 / 𝐴)))) = (-1 / (𝐴 − 1))) |
99 | 84, 91, 98 | 3eqtr2d 2662 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (-(1 /
𝐴) / (1 − (1 / 𝐴))) = (-1 / (𝐴 − 1))) |
100 | | subcl 10280 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → (𝐴 −
1) ∈ ℂ) |
101 | 100 | negnegd 10383 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → --(𝐴
− 1) = (𝐴 −
1)) |
102 | | negsubdi2 10340 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → -(𝐴 −
1) = (1 − 𝐴)) |
103 | 102 | negeqd 10275 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → --(𝐴
− 1) = -(1 − 𝐴)) |
104 | 101, 103 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → (𝐴 −
1) = -(1 − 𝐴)) |
105 | 15, 14, 104 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (𝐴 − 1) = -(1 − 𝐴)) |
106 | 105 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (-1 /
(𝐴 − 1)) = (-1 / -(1
− 𝐴))) |
107 | 76, 99, 106 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
(∗‘(-𝐴 / (1
− 𝐴))) = (-1 / -(1
− 𝐴))) |
108 | 107 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
(∗‘(-𝐴 / (1
− 𝐴))) = (-1 / -(1
− 𝐴))) |
109 | 29, 16, 24 | divcld 10801 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (-𝐴 / (1 − 𝐴)) ∈ ℂ) |
110 | 109 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
(-𝐴 / (1 − 𝐴)) ∈
ℂ) |
111 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
(ℑ‘(-𝐴 / (1
− 𝐴))) =
0) |
112 | 110, 111 | reim0bd 13940 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
(-𝐴 / (1 − 𝐴)) ∈
ℝ) |
113 | 112 | cjred 13966 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
(∗‘(-𝐴 / (1
− 𝐴))) = (-𝐴 / (1 − 𝐴))) |
114 | 113, 112 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
(∗‘(-𝐴 / (1
− 𝐴))) ∈
ℝ) |
115 | 108, 114 | eqeltrrd 2702 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
(-1 / -(1 − 𝐴))
∈ ℝ) |
116 | 28, 115 | eqeltrrd 2702 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) → (1
/ (1 − 𝐴)) ∈
ℝ) |
117 | 16, 24 | recne0d 10795 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (1 / (1
− 𝐴)) ≠
0) |
118 | 117 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) → (1
/ (1 − 𝐴)) ≠
0) |
119 | 116, 118 | rereccld 10852 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) → (1
/ (1 / (1 − 𝐴)))
∈ ℝ) |
120 | 26, 119 | eqeltrrd 2702 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) → (1
− 𝐴) ∈
ℝ) |
121 | | 1red 10055 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) → 1
∈ ℝ) |
122 | 120, 121 | resubcld 10458 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
((1 − 𝐴) − 1)
∈ ℝ) |
123 | 13, 122 | eqeltrrd 2702 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
-𝐴 ∈
ℝ) |
124 | 2, 123 | negrebd 10391 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
𝐴 ∈
ℝ) |
125 | 124 | absord 14154 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
((abs‘𝐴) = 𝐴 ∨ (abs‘𝐴) = -𝐴)) |
126 | | eqeq1 2626 |
. . . . . . . . . . . . 13
⊢
((abs‘𝐴) = 1
→ ((abs‘𝐴) =
𝐴 ↔ 1 = 𝐴)) |
127 | 126 | biimpd 219 |
. . . . . . . . . . . 12
⊢
((abs‘𝐴) = 1
→ ((abs‘𝐴) =
𝐴 → 1 = 𝐴)) |
128 | | eqeq1 2626 |
. . . . . . . . . . . . 13
⊢
((abs‘𝐴) = 1
→ ((abs‘𝐴) =
-𝐴 ↔ 1 = -𝐴)) |
129 | 128 | biimpd 219 |
. . . . . . . . . . . 12
⊢
((abs‘𝐴) = 1
→ ((abs‘𝐴) =
-𝐴 → 1 = -𝐴)) |
130 | 127, 129 | orim12d 883 |
. . . . . . . . . . 11
⊢
((abs‘𝐴) = 1
→ (((abs‘𝐴) =
𝐴 ∨ (abs‘𝐴) = -𝐴) → (1 = 𝐴 ∨ 1 = -𝐴))) |
131 | 7, 125, 130 | sylc 65 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) → (1
= 𝐴 ∨ 1 = -𝐴)) |
132 | 131 | ord 392 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
(¬ 1 = 𝐴 → 1 =
-𝐴)) |
133 | 6, 132 | mpd 15 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) → 1
= -𝐴) |
134 | 133, 5 | eqeltrrd 2702 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
-𝐴 ∈
ℝ+) |
135 | 5, 134 | rpaddcld 11887 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) → (1
+ -𝐴) ∈
ℝ+) |
136 | 3, 135 | eqeltrrd 2702 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) → (1
− 𝐴) ∈
ℝ+) |
137 | 136 | relogcld 24369 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
(log‘(1 − 𝐴))
∈ ℝ) |
138 | 137 | reim0d 13965 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
(ℑ‘(log‘(1 − 𝐴))) = 0) |
139 | 134, 136 | rpdivcld 11889 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
(-𝐴 / (1 − 𝐴)) ∈
ℝ+) |
140 | 139 | relogcld 24369 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
(log‘(-𝐴 / (1 −
𝐴))) ∈
ℝ) |
141 | 140 | reim0d 13965 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
(ℑ‘(log‘(-𝐴 / (1 − 𝐴)))) = 0) |
142 | 138, 141 | eqtr4d 2659 |
. 2
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
(ℑ‘(log‘(1 − 𝐴))) = (ℑ‘(log‘(-𝐴 / (1 − 𝐴))))) |
143 | 16, 24 | logcld 24317 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
(log‘(1 − 𝐴))
∈ ℂ) |
144 | 143 | adantr 481 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
(log‘(1 − 𝐴))
∈ ℂ) |
145 | 144 | imcld 13935 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
(ℑ‘(log‘(1 − 𝐴))) ∈ ℝ) |
146 | 145 | recnd 10068 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
(ℑ‘(log‘(1 − 𝐴))) ∈ ℂ) |
147 | 109 | adantr 481 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
(-𝐴 / (1 − 𝐴)) ∈
ℂ) |
148 | 15, 78 | negne0d 10390 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → -𝐴 ≠ 0) |
149 | 29, 16, 148, 24 | divne0d 10817 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (-𝐴 / (1 − 𝐴)) ≠ 0) |
150 | 149 | adantr 481 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
(-𝐴 / (1 − 𝐴)) ≠ 0) |
151 | 147, 150 | logcld 24317 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
(log‘(-𝐴 / (1 −
𝐴))) ∈
ℂ) |
152 | 151 | imcld 13935 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
(ℑ‘(log‘(-𝐴 / (1 − 𝐴)))) ∈ ℝ) |
153 | 152 | recnd 10068 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
(ℑ‘(log‘(-𝐴 / (1 − 𝐴)))) ∈ ℂ) |
154 | 107 | fveq2d 6195 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
(log‘(∗‘(-𝐴 / (1 − 𝐴)))) = (log‘(-1 / -(1 − 𝐴)))) |
155 | 154 | adantr 481 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
(log‘(∗‘(-𝐴 / (1 − 𝐴)))) = (log‘(-1 / -(1 − 𝐴)))) |
156 | | logcj 24352 |
. . . . . . 7
⊢ (((-𝐴 / (1 − 𝐴)) ∈ ℂ ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
(log‘(∗‘(-𝐴 / (1 − 𝐴)))) = (∗‘(log‘(-𝐴 / (1 − 𝐴))))) |
157 | 109, 156 | sylan 488 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
(log‘(∗‘(-𝐴 / (1 − 𝐴)))) = (∗‘(log‘(-𝐴 / (1 − 𝐴))))) |
158 | 16, 24 | reccld 10794 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (1 / (1
− 𝐴)) ∈
ℂ) |
159 | 158, 117 | logcld 24317 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
(log‘(1 / (1 − 𝐴))) ∈ ℂ) |
160 | 159 | negnegd 10383 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
--(log‘(1 / (1 − 𝐴))) = (log‘(1 / (1 − 𝐴)))) |
161 | | isosctrlem1 24548 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
(ℑ‘(log‘(1 − 𝐴))) ≠ π) |
162 | | logrec 24501 |
. . . . . . . . . 10
⊢ (((1
− 𝐴) ∈ ℂ
∧ (1 − 𝐴) ≠ 0
∧ (ℑ‘(log‘(1 − 𝐴))) ≠ π) → (log‘(1 −
𝐴)) = -(log‘(1 / (1
− 𝐴)))) |
163 | 16, 24, 161, 162 | syl3anc 1326 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
(log‘(1 − 𝐴)) =
-(log‘(1 / (1 − 𝐴)))) |
164 | 163 | negeqd 10275 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
-(log‘(1 − 𝐴))
= --(log‘(1 / (1 − 𝐴)))) |
165 | 27 | fveq2d 6195 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
(log‘(-1 / -(1 − 𝐴))) = (log‘(1 / (1 − 𝐴)))) |
166 | 160, 164,
165 | 3eqtr4rd 2667 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
(log‘(-1 / -(1 − 𝐴))) = -(log‘(1 − 𝐴))) |
167 | 166 | adantr 481 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
(log‘(-1 / -(1 − 𝐴))) = -(log‘(1 − 𝐴))) |
168 | 155, 157,
167 | 3eqtr3rd 2665 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
-(log‘(1 − 𝐴))
= (∗‘(log‘(-𝐴 / (1 − 𝐴))))) |
169 | 168 | fveq2d 6195 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
(ℑ‘-(log‘(1 − 𝐴))) =
(ℑ‘(∗‘(log‘(-𝐴 / (1 − 𝐴)))))) |
170 | 144 | imnegd 13950 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
(ℑ‘-(log‘(1 − 𝐴))) = -(ℑ‘(log‘(1 −
𝐴)))) |
171 | 151 | imcjd 13945 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
(ℑ‘(∗‘(log‘(-𝐴 / (1 − 𝐴))))) = -(ℑ‘(log‘(-𝐴 / (1 − 𝐴))))) |
172 | 169, 170,
171 | 3eqtr3d 2664 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
-(ℑ‘(log‘(1 − 𝐴))) = -(ℑ‘(log‘(-𝐴 / (1 − 𝐴))))) |
173 | 146, 153,
172 | neg11d 10404 |
. 2
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
(ℑ‘(log‘(1 − 𝐴))) = (ℑ‘(log‘(-𝐴 / (1 − 𝐴))))) |
174 | 142, 173 | pm2.61dane 2881 |
1
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
(ℑ‘(log‘(1 − 𝐴))) = (ℑ‘(log‘(-𝐴 / (1 − 𝐴))))) |