Proof of Theorem isosctrlem2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 1cnd 11257 | . . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) → 1
∈ ℂ) | 
| 2 |  | simpl1 1191 | . . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
𝐴 ∈
ℂ) | 
| 3 | 1, 2 | negsubd 11627 | . . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) → (1
+ -𝐴) = (1 − 𝐴)) | 
| 4 |  | 1rp 13039 | . . . . . . . 8
⊢ 1 ∈
ℝ+ | 
| 5 | 4 | a1i 11 | . . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) → 1
∈ ℝ+) | 
| 6 |  | simpl3 1193 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
¬ 1 = 𝐴) | 
| 7 |  | simpl2 1192 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
(abs‘𝐴) =
1) | 
| 8 | 1, 2, 1 | sub32d 11653 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
((1 − 𝐴) − 1) =
((1 − 1) − 𝐴)) | 
| 9 |  | 1m1e0 12339 | . . . . . . . . . . . . . . . . 17
⊢ (1
− 1) = 0 | 
| 10 | 9 | oveq1i 7442 | . . . . . . . . . . . . . . . 16
⊢ ((1
− 1) − 𝐴) = (0
− 𝐴) | 
| 11 |  | df-neg 11496 | . . . . . . . . . . . . . . . 16
⊢ -𝐴 = (0 − 𝐴) | 
| 12 | 10, 11 | eqtr4i 2767 | . . . . . . . . . . . . . . 15
⊢ ((1
− 1) − 𝐴) =
-𝐴 | 
| 13 | 8, 12 | eqtrdi 2792 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
((1 − 𝐴) − 1) =
-𝐴) | 
| 14 |  | 1cnd 11257 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → 1
∈ ℂ) | 
| 15 |  | simp1 1136 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → 𝐴 ∈
ℂ) | 
| 16 | 14, 15 | subcld 11621 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (1
− 𝐴) ∈
ℂ) | 
| 17 | 16 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) → (1
− 𝐴) ∈
ℂ) | 
| 18 |  | ax-1cn 11214 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ 1 ∈
ℂ | 
| 19 |  | subeq0 11536 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((1
∈ ℂ ∧ 𝐴
∈ ℂ) → ((1 − 𝐴) = 0 ↔ 1 = 𝐴)) | 
| 20 | 18, 19 | mpan 690 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐴 ∈ ℂ → ((1
− 𝐴) = 0 ↔ 1 =
𝐴)) | 
| 21 | 20 | biimpd 229 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐴 ∈ ℂ → ((1
− 𝐴) = 0 → 1 =
𝐴)) | 
| 22 | 21 | con3dimp 408 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ ℂ ∧ ¬ 1 =
𝐴) → ¬ (1 −
𝐴) = 0) | 
| 23 | 22 | neqned 2946 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℂ ∧ ¬ 1 =
𝐴) → (1 − 𝐴) ≠ 0) | 
| 24 | 23 | 3adant2 1131 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (1
− 𝐴) ≠
0) | 
| 25 | 24 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) → (1
− 𝐴) ≠
0) | 
| 26 | 17, 25 | recrecd 12041 | . . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) → (1
/ (1 / (1 − 𝐴))) = (1
− 𝐴)) | 
| 27 | 14, 16, 24 | div2negd 12059 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (-1 /
-(1 − 𝐴)) = (1 / (1
− 𝐴))) | 
| 28 | 27 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
(-1 / -(1 − 𝐴)) = (1
/ (1 − 𝐴))) | 
| 29 | 15 | negcld 11608 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → -𝐴 ∈
ℂ) | 
| 30 | 29, 16, 24 | cjdivd 15263 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
(∗‘(-𝐴 / (1
− 𝐴))) =
((∗‘-𝐴) /
(∗‘(1 − 𝐴)))) | 
| 31 | 15 | cjnegd 15251 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
(∗‘-𝐴) =
-(∗‘𝐴)) | 
| 32 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝐴 = 0 → (abs‘𝐴) =
(abs‘0)) | 
| 33 |  | abs0 15325 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(abs‘0) = 0 | 
| 34 | 32, 33 | eqtrdi 2792 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝐴 = 0 → (abs‘𝐴) = 0) | 
| 35 |  | eqtr2 2760 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((abs‘𝐴) = 1
∧ (abs‘𝐴) = 0)
→ 1 = 0) | 
| 36 | 34, 35 | sylan2 593 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((abs‘𝐴) = 1
∧ 𝐴 = 0) → 1 =
0) | 
| 37 |  | ax-1ne0 11225 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ 1 ≠
0 | 
| 38 |  | neneq 2945 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (1 ≠ 0
→ ¬ 1 = 0) | 
| 39 | 37, 38 | mp1i 13 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((abs‘𝐴) = 1
∧ 𝐴 = 0) → ¬ 1
= 0) | 
| 40 | 36, 39 | pm2.65da 816 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((abs‘𝐴) = 1
→ ¬ 𝐴 =
0) | 
| 41 | 40 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1) →
¬ 𝐴 =
0) | 
| 42 |  | df-ne 2940 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝐴 ≠ 0 ↔ ¬ 𝐴 = 0) | 
| 43 |  | oveq1 7439 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
((abs‘𝐴) = 1
→ ((abs‘𝐴)↑2) = (1↑2)) | 
| 44 |  | sq1 14235 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
(1↑2) = 1 | 
| 45 | 43, 44 | eqtrdi 2792 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
((abs‘𝐴) = 1
→ ((abs‘𝐴)↑2) = 1) | 
| 46 | 45 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1) →
((abs‘𝐴)↑2) =
1) | 
| 47 |  | absvalsq 15320 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝐴 ∈ ℂ →
((abs‘𝐴)↑2) =
(𝐴 ·
(∗‘𝐴))) | 
| 48 | 47 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1) →
((abs‘𝐴)↑2) =
(𝐴 ·
(∗‘𝐴))) | 
| 49 | 46, 48 | eqtr3d 2778 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1) → 1
= (𝐴 ·
(∗‘𝐴))) | 
| 50 | 49 | 3adant3 1132 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
𝐴 ≠ 0) → 1 = (𝐴 · (∗‘𝐴))) | 
| 51 | 50 | oveq1d 7447 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
𝐴 ≠ 0) → (1 / 𝐴) = ((𝐴 · (∗‘𝐴)) / 𝐴)) | 
| 52 |  | simp1 1136 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
𝐴 ≠ 0) → 𝐴 ∈
ℂ) | 
| 53 | 52 | cjcld 15236 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
𝐴 ≠ 0) →
(∗‘𝐴) ∈
ℂ) | 
| 54 |  | simp3 1138 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
𝐴 ≠ 0) → 𝐴 ≠ 0) | 
| 55 | 53, 52, 54 | divcan3d 12049 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
𝐴 ≠ 0) → ((𝐴 · (∗‘𝐴)) / 𝐴) = (∗‘𝐴)) | 
| 56 | 51, 55 | eqtrd 2776 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2742 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1) →
(∗‘𝐴) = (1 /
𝐴)) | 
| 60 | 59 | 3adant3 1132 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
(∗‘𝐴) = (1 /
𝐴)) | 
| 61 | 60 | negeqd 11503 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
-(∗‘𝐴) = -(1 /
𝐴)) | 
| 62 | 31, 61 | eqtrd 2776 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
(∗‘-𝐴) = -(1 /
𝐴)) | 
| 63 | 62 | oveq1d 7447 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
((∗‘-𝐴) /
(∗‘(1 − 𝐴))) = (-(1 / 𝐴) / (∗‘(1 − 𝐴)))) | 
| 64 |  | cjsub 15189 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((1
∈ ℂ ∧ 𝐴
∈ ℂ) → (∗‘(1 − 𝐴)) = ((∗‘1) −
(∗‘𝐴))) | 
| 65 | 18, 64 | mpan 690 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐴 ∈ ℂ →
(∗‘(1 − 𝐴)) = ((∗‘1) −
(∗‘𝐴))) | 
| 66 |  | 1red 11263 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝐴 ∈ ℂ → 1 ∈
ℝ) | 
| 67 | 66 | cjred 15266 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐴 ∈ ℂ →
(∗‘1) = 1) | 
| 68 | 67 | oveq1d 7447 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐴 ∈ ℂ →
((∗‘1) − (∗‘𝐴)) = (1 − (∗‘𝐴))) | 
| 69 | 65, 68 | eqtrd 2776 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐴 ∈ ℂ →
(∗‘(1 − 𝐴)) = (1 − (∗‘𝐴))) | 
| 70 | 69 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1) →
(∗‘(1 − 𝐴)) = (1 − (∗‘𝐴))) | 
| 71 | 59 | oveq2d 7448 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1) →
(1 − (∗‘𝐴)) = (1 − (1 / 𝐴))) | 
| 72 | 70, 71 | eqtrd 2776 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1) →
(∗‘(1 − 𝐴)) = (1 − (1 / 𝐴))) | 
| 73 | 72 | 3adant3 1132 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
(∗‘(1 − 𝐴)) = (1 − (1 / 𝐴))) | 
| 74 | 73 | oveq2d 7448 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (-(1 /
𝐴) / (∗‘(1
− 𝐴))) = (-(1 / 𝐴) / (1 − (1 / 𝐴)))) | 
| 75 | 30, 63, 74 | 3eqtrd 2780 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
(∗‘(-𝐴 / (1
− 𝐴))) = (-(1 / 𝐴) / (1 − (1 / 𝐴)))) | 
| 76 | 40 | 3ad2ant2 1134 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → ¬
𝐴 = 0) | 
| 77 | 76 | neqned 2946 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → 𝐴 ≠ 0) | 
| 78 |  | 1cnd 11257 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → 1 ∈
ℂ) | 
| 79 |  | simpl 482 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → 𝐴 ∈
ℂ) | 
| 80 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → 𝐴 ≠ 0) | 
| 81 | 78, 79, 80 | divnegd 12057 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → -(1 / 𝐴) = (-1 / 𝐴)) | 
| 82 | 81 | oveq1d 7447 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (-(1 / 𝐴) / (1 − (1 / 𝐴))) = ((-1 / 𝐴) / (1 − (1 / 𝐴)))) | 
| 83 | 15, 77, 82 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (-(1 /
𝐴) / (1 − (1 / 𝐴))) = ((-1 / 𝐴) / (1 − (1 / 𝐴)))) | 
| 84 | 14 | negcld 11608 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → -1
∈ ℂ) | 
| 85 | 84, 15, 77 | divcld 12044 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (-1 /
𝐴) ∈
ℂ) | 
| 86 | 15, 77 | reccld 12037 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (1 /
𝐴) ∈
ℂ) | 
| 87 | 14, 86 | subcld 11621 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (1
− (1 / 𝐴)) ∈
ℂ) | 
| 88 | 16, 24 | cjne0d 15243 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
(∗‘(1 − 𝐴)) ≠ 0) | 
| 89 | 73, 88 | eqnetrrd 3008 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (1
− (1 / 𝐴)) ≠
0) | 
| 90 | 85, 87, 15, 89, 77 | divcan5d 12070 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → ((𝐴 · (-1 / 𝐴)) / (𝐴 · (1 − (1 / 𝐴)))) = ((-1 / 𝐴) / (1 − (1 / 𝐴)))) | 
| 91 | 84, 15, 77 | divcan2d 12046 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (𝐴 · (-1 / 𝐴)) = -1) | 
| 92 | 15, 14, 86 | subdid 11720 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (𝐴 · (1 − (1 / 𝐴))) = ((𝐴 · 1) − (𝐴 · (1 / 𝐴)))) | 
| 93 | 15 | mulridd 11279 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (𝐴 · 1) = 𝐴) | 
| 94 | 15, 77 | recidd 12039 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (𝐴 · (1 / 𝐴)) = 1) | 
| 95 | 93, 94 | oveq12d 7450 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → ((𝐴 · 1) − (𝐴 · (1 / 𝐴))) = (𝐴 − 1)) | 
| 96 | 92, 95 | eqtrd 2776 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (𝐴 · (1 − (1 / 𝐴))) = (𝐴 − 1)) | 
| 97 | 91, 96 | oveq12d 7450 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → ((𝐴 · (-1 / 𝐴)) / (𝐴 · (1 − (1 / 𝐴)))) = (-1 / (𝐴 − 1))) | 
| 98 | 83, 90, 97 | 3eqtr2d 2782 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (-(1 /
𝐴) / (1 − (1 / 𝐴))) = (-1 / (𝐴 − 1))) | 
| 99 |  | subcl 11508 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → (𝐴 −
1) ∈ ℂ) | 
| 100 | 99 | negnegd 11612 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → --(𝐴
− 1) = (𝐴 −
1)) | 
| 101 |  | negsubdi2 11569 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → -(𝐴 −
1) = (1 − 𝐴)) | 
| 102 | 101 | negeqd 11503 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → --(𝐴
− 1) = -(1 − 𝐴)) | 
| 103 | 100, 102 | eqtr3d 2778 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → (𝐴 −
1) = -(1 − 𝐴)) | 
| 104 | 15, 14, 103 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (𝐴 − 1) = -(1 − 𝐴)) | 
| 105 | 104 | oveq2d 7448 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (-1 /
(𝐴 − 1)) = (-1 / -(1
− 𝐴))) | 
| 106 | 75, 98, 105 | 3eqtrd 2780 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
(∗‘(-𝐴 / (1
− 𝐴))) = (-1 / -(1
− 𝐴))) | 
| 107 | 106 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
(∗‘(-𝐴 / (1
− 𝐴))) = (-1 / -(1
− 𝐴))) | 
| 108 | 29, 16, 24 | divcld 12044 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (-𝐴 / (1 − 𝐴)) ∈ ℂ) | 
| 109 | 108 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
(-𝐴 / (1 − 𝐴)) ∈
ℂ) | 
| 110 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
(ℑ‘(-𝐴 / (1
− 𝐴))) =
0) | 
| 111 | 109, 110 | reim0bd 15240 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
(-𝐴 / (1 − 𝐴)) ∈
ℝ) | 
| 112 | 111 | cjred 15266 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
(∗‘(-𝐴 / (1
− 𝐴))) = (-𝐴 / (1 − 𝐴))) | 
| 113 | 112, 111 | eqeltrd 2840 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
(∗‘(-𝐴 / (1
− 𝐴))) ∈
ℝ) | 
| 114 | 107, 113 | eqeltrrd 2841 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
(-1 / -(1 − 𝐴))
∈ ℝ) | 
| 115 | 28, 114 | eqeltrrd 2841 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) → (1
/ (1 − 𝐴)) ∈
ℝ) | 
| 116 | 16, 24 | recne0d 12038 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (1 / (1
− 𝐴)) ≠
0) | 
| 117 | 116 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) → (1
/ (1 − 𝐴)) ≠
0) | 
| 118 | 115, 117 | rereccld 12095 | . . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) → (1
/ (1 / (1 − 𝐴)))
∈ ℝ) | 
| 119 | 26, 118 | eqeltrrd 2841 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) → (1
− 𝐴) ∈
ℝ) | 
| 120 |  | 1red 11263 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) → 1
∈ ℝ) | 
| 121 | 119, 120 | resubcld 11692 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
((1 − 𝐴) − 1)
∈ ℝ) | 
| 122 | 13, 121 | eqeltrrd 2841 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
-𝐴 ∈
ℝ) | 
| 123 | 2, 122 | negrebd 11620 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
𝐴 ∈
ℝ) | 
| 124 | 123 | absord 15455 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
((abs‘𝐴) = 𝐴 ∨ (abs‘𝐴) = -𝐴)) | 
| 125 |  | eqeq1 2740 | . . . . . . . . . . . . 13
⊢
((abs‘𝐴) = 1
→ ((abs‘𝐴) =
𝐴 ↔ 1 = 𝐴)) | 
| 126 | 125 | biimpd 229 | . . . . . . . . . . . 12
⊢
((abs‘𝐴) = 1
→ ((abs‘𝐴) =
𝐴 → 1 = 𝐴)) | 
| 127 |  | eqeq1 2740 | . . . . . . . . . . . . 13
⊢
((abs‘𝐴) = 1
→ ((abs‘𝐴) =
-𝐴 ↔ 1 = -𝐴)) | 
| 128 | 127 | biimpd 229 | . . . . . . . . . . . 12
⊢
((abs‘𝐴) = 1
→ ((abs‘𝐴) =
-𝐴 → 1 = -𝐴)) | 
| 129 | 126, 128 | orim12d 966 | . . . . . . . . . . 11
⊢
((abs‘𝐴) = 1
→ (((abs‘𝐴) =
𝐴 ∨ (abs‘𝐴) = -𝐴) → (1 = 𝐴 ∨ 1 = -𝐴))) | 
| 130 | 7, 124, 129 | sylc 65 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) → (1
= 𝐴 ∨ 1 = -𝐴)) | 
| 131 | 130 | ord 864 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
(¬ 1 = 𝐴 → 1 =
-𝐴)) | 
| 132 | 6, 131 | mpd 15 | . . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) → 1
= -𝐴) | 
| 133 | 132, 5 | eqeltrrd 2841 | . . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
-𝐴 ∈
ℝ+) | 
| 134 | 5, 133 | rpaddcld 13093 | . . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) → (1
+ -𝐴) ∈
ℝ+) | 
| 135 | 3, 134 | eqeltrrd 2841 | . . . . 5
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) → (1
− 𝐴) ∈
ℝ+) | 
| 136 | 135 | relogcld 26666 | . . . 4
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
(log‘(1 − 𝐴))
∈ ℝ) | 
| 137 | 136 | reim0d 15265 | . . 3
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
(ℑ‘(log‘(1 − 𝐴))) = 0) | 
| 138 | 133, 135 | rpdivcld 13095 | . . . . 5
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
(-𝐴 / (1 − 𝐴)) ∈
ℝ+) | 
| 139 | 138 | relogcld 26666 | . . . 4
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
(log‘(-𝐴 / (1 −
𝐴))) ∈
ℝ) | 
| 140 | 139 | reim0d 15265 | . . 3
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
(ℑ‘(log‘(-𝐴 / (1 − 𝐴)))) = 0) | 
| 141 | 137, 140 | eqtr4d 2779 | . 2
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) = 0) →
(ℑ‘(log‘(1 − 𝐴))) = (ℑ‘(log‘(-𝐴 / (1 − 𝐴))))) | 
| 142 | 16, 24 | logcld 26613 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
(log‘(1 − 𝐴))
∈ ℂ) | 
| 143 | 142 | adantr 480 | . . . . 5
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
(log‘(1 − 𝐴))
∈ ℂ) | 
| 144 | 143 | imcld 15235 | . . . 4
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
(ℑ‘(log‘(1 − 𝐴))) ∈ ℝ) | 
| 145 | 144 | recnd 11290 | . . 3
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
(ℑ‘(log‘(1 − 𝐴))) ∈ ℂ) | 
| 146 | 108 | adantr 480 | . . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
(-𝐴 / (1 − 𝐴)) ∈
ℂ) | 
| 147 | 15, 77 | negne0d 11619 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → -𝐴 ≠ 0) | 
| 148 | 29, 16, 147, 24 | divne0d 12060 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (-𝐴 / (1 − 𝐴)) ≠ 0) | 
| 149 | 148 | adantr 480 | . . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
(-𝐴 / (1 − 𝐴)) ≠ 0) | 
| 150 | 146, 149 | logcld 26613 | . . . . 5
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
(log‘(-𝐴 / (1 −
𝐴))) ∈
ℂ) | 
| 151 | 150 | imcld 15235 | . . . 4
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
(ℑ‘(log‘(-𝐴 / (1 − 𝐴)))) ∈ ℝ) | 
| 152 | 151 | recnd 11290 | . . 3
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
(ℑ‘(log‘(-𝐴 / (1 − 𝐴)))) ∈ ℂ) | 
| 153 | 106 | fveq2d 6909 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
(log‘(∗‘(-𝐴 / (1 − 𝐴)))) = (log‘(-1 / -(1 − 𝐴)))) | 
| 154 | 153 | adantr 480 | . . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
(log‘(∗‘(-𝐴 / (1 − 𝐴)))) = (log‘(-1 / -(1 − 𝐴)))) | 
| 155 |  | logcj 26649 | . . . . . . 7
⊢ (((-𝐴 / (1 − 𝐴)) ∈ ℂ ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
(log‘(∗‘(-𝐴 / (1 − 𝐴)))) = (∗‘(log‘(-𝐴 / (1 − 𝐴))))) | 
| 156 | 108, 155 | sylan 580 | . . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
(log‘(∗‘(-𝐴 / (1 − 𝐴)))) = (∗‘(log‘(-𝐴 / (1 − 𝐴))))) | 
| 157 | 16, 24 | reccld 12037 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) → (1 / (1
− 𝐴)) ∈
ℂ) | 
| 158 | 157, 116 | logcld 26613 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
(log‘(1 / (1 − 𝐴))) ∈ ℂ) | 
| 159 | 158 | negnegd 11612 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
--(log‘(1 / (1 − 𝐴))) = (log‘(1 / (1 − 𝐴)))) | 
| 160 |  | isosctrlem1 26862 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
(ℑ‘(log‘(1 − 𝐴))) ≠ π) | 
| 161 |  | logrec 26807 | . . . . . . . . . 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 11503 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
-(log‘(1 − 𝐴))
= --(log‘(1 / (1 − 𝐴)))) | 
| 164 | 27 | fveq2d 6909 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
(log‘(-1 / -(1 − 𝐴))) = (log‘(1 / (1 − 𝐴)))) | 
| 165 | 159, 163,
164 | 3eqtr4rd 2787 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
(log‘(-1 / -(1 − 𝐴))) = -(log‘(1 − 𝐴))) | 
| 166 | 165 | adantr 480 | . . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
(log‘(-1 / -(1 − 𝐴))) = -(log‘(1 − 𝐴))) | 
| 167 | 154, 156,
166 | 3eqtr3rd 2785 | . . . . 5
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
-(log‘(1 − 𝐴))
= (∗‘(log‘(-𝐴 / (1 − 𝐴))))) | 
| 168 | 167 | fveq2d 6909 | . . . 4
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
(ℑ‘-(log‘(1 − 𝐴))) =
(ℑ‘(∗‘(log‘(-𝐴 / (1 − 𝐴)))))) | 
| 169 | 143 | imnegd 15250 | . . . 4
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
(ℑ‘-(log‘(1 − 𝐴))) = -(ℑ‘(log‘(1 −
𝐴)))) | 
| 170 | 150 | imcjd 15245 | . . . 4
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
(ℑ‘(∗‘(log‘(-𝐴 / (1 − 𝐴))))) = -(ℑ‘(log‘(-𝐴 / (1 − 𝐴))))) | 
| 171 | 168, 169,
170 | 3eqtr3d 2784 | . . 3
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
-(ℑ‘(log‘(1 − 𝐴))) = -(ℑ‘(log‘(-𝐴 / (1 − 𝐴))))) | 
| 172 | 145, 152,
171 | neg11d 11633 | . 2
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) ∧
(ℑ‘(-𝐴 / (1
− 𝐴))) ≠ 0) →
(ℑ‘(log‘(1 − 𝐴))) = (ℑ‘(log‘(-𝐴 / (1 − 𝐴))))) | 
| 173 | 141, 172 | pm2.61dane 3028 | 1
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) = 1 ∧
¬ 1 = 𝐴) →
(ℑ‘(log‘(1 − 𝐴))) = (ℑ‘(log‘(-𝐴 / (1 − 𝐴))))) |