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