Proof of Theorem 2efiatan
| Step | Hyp | Ref
| Expression |
| 1 | | atanval 26927 |
. . . . 5
⊢ (𝐴 ∈ dom arctan →
(arctan‘𝐴) = ((i / 2)
· ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴)))))) |
| 2 | 1 | oveq2d 7447 |
. . . 4
⊢ (𝐴 ∈ dom arctan → ((2
· i) · (arctan‘𝐴)) = ((2 · i) · ((i / 2)
· ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴))))))) |
| 3 | | 2cn 12341 |
. . . . . 6
⊢ 2 ∈
ℂ |
| 4 | 3 | a1i 11 |
. . . . 5
⊢ (𝐴 ∈ dom arctan → 2
∈ ℂ) |
| 5 | | ax-icn 11214 |
. . . . . 6
⊢ i ∈
ℂ |
| 6 | 5 | a1i 11 |
. . . . 5
⊢ (𝐴 ∈ dom arctan → i
∈ ℂ) |
| 7 | | atancl 26924 |
. . . . 5
⊢ (𝐴 ∈ dom arctan →
(arctan‘𝐴) ∈
ℂ) |
| 8 | 4, 6, 7 | mulassd 11284 |
. . . 4
⊢ (𝐴 ∈ dom arctan → ((2
· i) · (arctan‘𝐴)) = (2 · (i ·
(arctan‘𝐴)))) |
| 9 | | halfcl 12491 |
. . . . . . . . . 10
⊢ (i ∈
ℂ → (i / 2) ∈ ℂ) |
| 10 | 5, 9 | ax-mp 5 |
. . . . . . . . 9
⊢ (i / 2)
∈ ℂ |
| 11 | 3, 5, 10 | mulassi 11272 |
. . . . . . . 8
⊢ ((2
· i) · (i / 2)) = (2 · (i · (i /
2))) |
| 12 | 3, 5, 10 | mul12i 11456 |
. . . . . . . 8
⊢ (2
· (i · (i / 2))) = (i · (2 · (i /
2))) |
| 13 | | 2ne0 12370 |
. . . . . . . . . . 11
⊢ 2 ≠
0 |
| 14 | 5, 3, 13 | divcan2i 12010 |
. . . . . . . . . 10
⊢ (2
· (i / 2)) = i |
| 15 | 14 | oveq2i 7442 |
. . . . . . . . 9
⊢ (i
· (2 · (i / 2))) = (i · i) |
| 16 | | ixi 11892 |
. . . . . . . . 9
⊢ (i
· i) = -1 |
| 17 | 15, 16 | eqtri 2765 |
. . . . . . . 8
⊢ (i
· (2 · (i / 2))) = -1 |
| 18 | 11, 12, 17 | 3eqtri 2769 |
. . . . . . 7
⊢ ((2
· i) · (i / 2)) = -1 |
| 19 | 18 | oveq1i 7441 |
. . . . . 6
⊢ (((2
· i) · (i / 2)) · ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i
· 𝐴))))) = (-1
· ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴))))) |
| 20 | | ax-1cn 11213 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
| 21 | | atandm2 26920 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ dom arctan ↔ (𝐴 ∈ ℂ ∧ (1 −
(i · 𝐴)) ≠ 0
∧ (1 + (i · 𝐴))
≠ 0)) |
| 22 | 21 | simp1bi 1146 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ dom arctan → 𝐴 ∈
ℂ) |
| 23 | | mulcl 11239 |
. . . . . . . . . . 11
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i · 𝐴) ∈ ℂ) |
| 24 | 5, 22, 23 | sylancr 587 |
. . . . . . . . . 10
⊢ (𝐴 ∈ dom arctan → (i
· 𝐴) ∈
ℂ) |
| 25 | | subcl 11507 |
. . . . . . . . . 10
⊢ ((1
∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (1 − (i
· 𝐴)) ∈
ℂ) |
| 26 | 20, 24, 25 | sylancr 587 |
. . . . . . . . 9
⊢ (𝐴 ∈ dom arctan → (1
− (i · 𝐴))
∈ ℂ) |
| 27 | 21 | simp2bi 1147 |
. . . . . . . . 9
⊢ (𝐴 ∈ dom arctan → (1
− (i · 𝐴))
≠ 0) |
| 28 | 26, 27 | logcld 26612 |
. . . . . . . 8
⊢ (𝐴 ∈ dom arctan →
(log‘(1 − (i · 𝐴))) ∈ ℂ) |
| 29 | | addcl 11237 |
. . . . . . . . . 10
⊢ ((1
∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (1 + (i ·
𝐴)) ∈
ℂ) |
| 30 | 20, 24, 29 | sylancr 587 |
. . . . . . . . 9
⊢ (𝐴 ∈ dom arctan → (1 +
(i · 𝐴)) ∈
ℂ) |
| 31 | 21 | simp3bi 1148 |
. . . . . . . . 9
⊢ (𝐴 ∈ dom arctan → (1 +
(i · 𝐴)) ≠
0) |
| 32 | 30, 31 | logcld 26612 |
. . . . . . . 8
⊢ (𝐴 ∈ dom arctan →
(log‘(1 + (i · 𝐴))) ∈ ℂ) |
| 33 | 28, 32 | subcld 11620 |
. . . . . . 7
⊢ (𝐴 ∈ dom arctan →
((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴)))) ∈
ℂ) |
| 34 | 33 | mulm1d 11715 |
. . . . . 6
⊢ (𝐴 ∈ dom arctan → (-1
· ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴))))) = -((log‘(1
− (i · 𝐴)))
− (log‘(1 + (i · 𝐴))))) |
| 35 | 19, 34 | eqtrid 2789 |
. . . . 5
⊢ (𝐴 ∈ dom arctan → (((2
· i) · (i / 2)) · ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i
· 𝐴))))) =
-((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴))))) |
| 36 | | 2mulicn 12489 |
. . . . . . 7
⊢ (2
· i) ∈ ℂ |
| 37 | 36 | a1i 11 |
. . . . . 6
⊢ (𝐴 ∈ dom arctan → (2
· i) ∈ ℂ) |
| 38 | 10 | a1i 11 |
. . . . . 6
⊢ (𝐴 ∈ dom arctan → (i /
2) ∈ ℂ) |
| 39 | 37, 38, 33 | mulassd 11284 |
. . . . 5
⊢ (𝐴 ∈ dom arctan → (((2
· i) · (i / 2)) · ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i
· 𝐴))))) = ((2
· i) · ((i / 2) · ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i
· 𝐴))))))) |
| 40 | 28, 32 | negsubdi2d 11636 |
. . . . 5
⊢ (𝐴 ∈ dom arctan →
-((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴)))) = ((log‘(1 + (i
· 𝐴))) −
(log‘(1 − (i · 𝐴))))) |
| 41 | 35, 39, 40 | 3eqtr3d 2785 |
. . . 4
⊢ (𝐴 ∈ dom arctan → ((2
· i) · ((i / 2) · ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i
· 𝐴)))))) =
((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) |
| 42 | 2, 8, 41 | 3eqtr3d 2785 |
. . 3
⊢ (𝐴 ∈ dom arctan → (2
· (i · (arctan‘𝐴))) = ((log‘(1 + (i · 𝐴))) − (log‘(1
− (i · 𝐴))))) |
| 43 | 42 | fveq2d 6910 |
. 2
⊢ (𝐴 ∈ dom arctan →
(exp‘(2 · (i · (arctan‘𝐴)))) = (exp‘((log‘(1 + (i
· 𝐴))) −
(log‘(1 − (i · 𝐴)))))) |
| 44 | | efsub 16136 |
. . 3
⊢
(((log‘(1 + (i · 𝐴))) ∈ ℂ ∧ (log‘(1
− (i · 𝐴)))
∈ ℂ) → (exp‘((log‘(1 + (i · 𝐴))) − (log‘(1
− (i · 𝐴)))))
= ((exp‘(log‘(1 + (i · 𝐴)))) / (exp‘(log‘(1 − (i
· 𝐴)))))) |
| 45 | 32, 28, 44 | syl2anc 584 |
. 2
⊢ (𝐴 ∈ dom arctan →
(exp‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) =
((exp‘(log‘(1 + (i · 𝐴)))) / (exp‘(log‘(1 − (i
· 𝐴)))))) |
| 46 | | eflog 26618 |
. . . . 5
⊢ (((1 + (i
· 𝐴)) ∈ ℂ
∧ (1 + (i · 𝐴))
≠ 0) → (exp‘(log‘(1 + (i · 𝐴)))) = (1 + (i · 𝐴))) |
| 47 | 30, 31, 46 | syl2anc 584 |
. . . 4
⊢ (𝐴 ∈ dom arctan →
(exp‘(log‘(1 + (i · 𝐴)))) = (1 + (i · 𝐴))) |
| 48 | | eflog 26618 |
. . . . 5
⊢ (((1
− (i · 𝐴))
∈ ℂ ∧ (1 − (i · 𝐴)) ≠ 0) → (exp‘(log‘(1
− (i · 𝐴)))) =
(1 − (i · 𝐴))) |
| 49 | 26, 27, 48 | syl2anc 584 |
. . . 4
⊢ (𝐴 ∈ dom arctan →
(exp‘(log‘(1 − (i · 𝐴)))) = (1 − (i · 𝐴))) |
| 50 | 47, 49 | oveq12d 7449 |
. . 3
⊢ (𝐴 ∈ dom arctan →
((exp‘(log‘(1 + (i · 𝐴)))) / (exp‘(log‘(1 − (i
· 𝐴))))) = ((1 + (i
· 𝐴)) / (1 −
(i · 𝐴)))) |
| 51 | | negsub 11557 |
. . . . . . . 8
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i + -𝐴) = (i − 𝐴)) |
| 52 | 5, 22, 51 | sylancr 587 |
. . . . . . 7
⊢ (𝐴 ∈ dom arctan → (i +
-𝐴) = (i − 𝐴)) |
| 53 | 6 | mulridd 11278 |
. . . . . . . 8
⊢ (𝐴 ∈ dom arctan → (i
· 1) = i) |
| 54 | 16 | oveq1i 7441 |
. . . . . . . . 9
⊢ ((i
· i) · 𝐴) =
(-1 · 𝐴) |
| 55 | 6, 6, 22 | mulassd 11284 |
. . . . . . . . 9
⊢ (𝐴 ∈ dom arctan → ((i
· i) · 𝐴) =
(i · (i · 𝐴))) |
| 56 | 22 | mulm1d 11715 |
. . . . . . . . 9
⊢ (𝐴 ∈ dom arctan → (-1
· 𝐴) = -𝐴) |
| 57 | 54, 55, 56 | 3eqtr3a 2801 |
. . . . . . . 8
⊢ (𝐴 ∈ dom arctan → (i
· (i · 𝐴)) =
-𝐴) |
| 58 | 53, 57 | oveq12d 7449 |
. . . . . . 7
⊢ (𝐴 ∈ dom arctan → ((i
· 1) + (i · (i · 𝐴))) = (i + -𝐴)) |
| 59 | 6, 22, 6 | pnpcan2d 11658 |
. . . . . . 7
⊢ (𝐴 ∈ dom arctan → ((i +
i) − (𝐴 + i)) = (i
− 𝐴)) |
| 60 | 52, 58, 59 | 3eqtr4d 2787 |
. . . . . 6
⊢ (𝐴 ∈ dom arctan → ((i
· 1) + (i · (i · 𝐴))) = ((i + i) − (𝐴 + i))) |
| 61 | 20 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ dom arctan → 1
∈ ℂ) |
| 62 | 6, 61, 24 | adddid 11285 |
. . . . . 6
⊢ (𝐴 ∈ dom arctan → (i
· (1 + (i · 𝐴))) = ((i · 1) + (i · (i
· 𝐴)))) |
| 63 | 6 | 2timesd 12509 |
. . . . . . 7
⊢ (𝐴 ∈ dom arctan → (2
· i) = (i + i)) |
| 64 | 63 | oveq1d 7446 |
. . . . . 6
⊢ (𝐴 ∈ dom arctan → ((2
· i) − (𝐴 +
i)) = ((i + i) − (𝐴 +
i))) |
| 65 | 60, 62, 64 | 3eqtr4d 2787 |
. . . . 5
⊢ (𝐴 ∈ dom arctan → (i
· (1 + (i · 𝐴))) = ((2 · i) − (𝐴 + i))) |
| 66 | 6, 61, 24 | subdid 11719 |
. . . . . 6
⊢ (𝐴 ∈ dom arctan → (i
· (1 − (i · 𝐴))) = ((i · 1) − (i · (i
· 𝐴)))) |
| 67 | 53, 57 | oveq12d 7449 |
. . . . . . 7
⊢ (𝐴 ∈ dom arctan → ((i
· 1) − (i · (i · 𝐴))) = (i − -𝐴)) |
| 68 | | subneg 11558 |
. . . . . . . 8
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i − -𝐴) = (i + 𝐴)) |
| 69 | 5, 22, 68 | sylancr 587 |
. . . . . . 7
⊢ (𝐴 ∈ dom arctan → (i
− -𝐴) = (i + 𝐴)) |
| 70 | 67, 69 | eqtrd 2777 |
. . . . . 6
⊢ (𝐴 ∈ dom arctan → ((i
· 1) − (i · (i · 𝐴))) = (i + 𝐴)) |
| 71 | | addcom 11447 |
. . . . . . 7
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i + 𝐴) = (𝐴 + i)) |
| 72 | 5, 22, 71 | sylancr 587 |
. . . . . 6
⊢ (𝐴 ∈ dom arctan → (i +
𝐴) = (𝐴 + i)) |
| 73 | 66, 70, 72 | 3eqtrd 2781 |
. . . . 5
⊢ (𝐴 ∈ dom arctan → (i
· (1 − (i · 𝐴))) = (𝐴 + i)) |
| 74 | 65, 73 | oveq12d 7449 |
. . . 4
⊢ (𝐴 ∈ dom arctan → ((i
· (1 + (i · 𝐴))) / (i · (1 − (i ·
𝐴)))) = (((2 · i)
− (𝐴 + i)) / (𝐴 + i))) |
| 75 | | ine0 11698 |
. . . . . 6
⊢ i ≠
0 |
| 76 | 75 | a1i 11 |
. . . . 5
⊢ (𝐴 ∈ dom arctan → i ≠
0) |
| 77 | 30, 26, 6, 27, 76 | divcan5d 12069 |
. . . 4
⊢ (𝐴 ∈ dom arctan → ((i
· (1 + (i · 𝐴))) / (i · (1 − (i ·
𝐴)))) = ((1 + (i ·
𝐴)) / (1 − (i
· 𝐴)))) |
| 78 | | addcl 11237 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ i ∈
ℂ) → (𝐴 + i)
∈ ℂ) |
| 79 | 22, 5, 78 | sylancl 586 |
. . . . 5
⊢ (𝐴 ∈ dom arctan → (𝐴 + i) ∈
ℂ) |
| 80 | | subneg 11558 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ i ∈
ℂ) → (𝐴 −
-i) = (𝐴 +
i)) |
| 81 | 22, 5, 80 | sylancl 586 |
. . . . . 6
⊢ (𝐴 ∈ dom arctan → (𝐴 − -i) = (𝐴 + i)) |
| 82 | | atandm 26919 |
. . . . . . . 8
⊢ (𝐴 ∈ dom arctan ↔ (𝐴 ∈ ℂ ∧ 𝐴 ≠ -i ∧ 𝐴 ≠ i)) |
| 83 | 82 | simp2bi 1147 |
. . . . . . 7
⊢ (𝐴 ∈ dom arctan → 𝐴 ≠ -i) |
| 84 | | negicn 11509 |
. . . . . . . 8
⊢ -i ∈
ℂ |
| 85 | | subeq0 11535 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ -i ∈
ℂ) → ((𝐴 −
-i) = 0 ↔ 𝐴 =
-i)) |
| 86 | 85 | necon3bid 2985 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ -i ∈
ℂ) → ((𝐴 −
-i) ≠ 0 ↔ 𝐴 ≠
-i)) |
| 87 | 22, 84, 86 | sylancl 586 |
. . . . . . 7
⊢ (𝐴 ∈ dom arctan →
((𝐴 − -i) ≠ 0
↔ 𝐴 ≠
-i)) |
| 88 | 83, 87 | mpbird 257 |
. . . . . 6
⊢ (𝐴 ∈ dom arctan → (𝐴 − -i) ≠
0) |
| 89 | 81, 88 | eqnetrrd 3009 |
. . . . 5
⊢ (𝐴 ∈ dom arctan → (𝐴 + i) ≠ 0) |
| 90 | 37, 79, 79, 89 | divsubdird 12082 |
. . . 4
⊢ (𝐴 ∈ dom arctan → (((2
· i) − (𝐴 +
i)) / (𝐴 + i)) = (((2
· i) / (𝐴 + i))
− ((𝐴 + i) / (𝐴 + i)))) |
| 91 | 74, 77, 90 | 3eqtr3d 2785 |
. . 3
⊢ (𝐴 ∈ dom arctan → ((1 +
(i · 𝐴)) / (1
− (i · 𝐴))) =
(((2 · i) / (𝐴 + i))
− ((𝐴 + i) / (𝐴 + i)))) |
| 92 | 79, 89 | dividd 12041 |
. . . 4
⊢ (𝐴 ∈ dom arctan →
((𝐴 + i) / (𝐴 + i)) = 1) |
| 93 | 92 | oveq2d 7447 |
. . 3
⊢ (𝐴 ∈ dom arctan → (((2
· i) / (𝐴 + i))
− ((𝐴 + i) / (𝐴 + i))) = (((2 · i) /
(𝐴 + i)) −
1)) |
| 94 | 50, 91, 93 | 3eqtrd 2781 |
. 2
⊢ (𝐴 ∈ dom arctan →
((exp‘(log‘(1 + (i · 𝐴)))) / (exp‘(log‘(1 − (i
· 𝐴))))) = (((2
· i) / (𝐴 + i))
− 1)) |
| 95 | 43, 45, 94 | 3eqtrd 2781 |
1
⊢ (𝐴 ∈ dom arctan →
(exp‘(2 · (i · (arctan‘𝐴)))) = (((2 · i) / (𝐴 + i)) − 1)) |