Proof of Theorem efiatan2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ax-icn 11214 | . . . . 5
⊢ i ∈
ℂ | 
| 2 |  | atancl 26924 | . . . . 5
⊢ (𝐴 ∈ dom arctan →
(arctan‘𝐴) ∈
ℂ) | 
| 3 |  | mulcl 11239 | . . . . 5
⊢ ((i
∈ ℂ ∧ (arctan‘𝐴) ∈ ℂ) → (i ·
(arctan‘𝐴)) ∈
ℂ) | 
| 4 | 1, 2, 3 | sylancr 587 | . . . 4
⊢ (𝐴 ∈ dom arctan → (i
· (arctan‘𝐴))
∈ ℂ) | 
| 5 |  | efcl 16118 | . . . 4
⊢ ((i
· (arctan‘𝐴))
∈ ℂ → (exp‘(i · (arctan‘𝐴))) ∈ ℂ) | 
| 6 | 4, 5 | syl 17 | . . 3
⊢ (𝐴 ∈ dom arctan →
(exp‘(i · (arctan‘𝐴))) ∈ ℂ) | 
| 7 |  | ax-1cn 11213 | . . . . 5
⊢ 1 ∈
ℂ | 
| 8 |  | atandm2 26920 | . . . . . . 7
⊢ (𝐴 ∈ dom arctan ↔ (𝐴 ∈ ℂ ∧ (1 −
(i · 𝐴)) ≠ 0
∧ (1 + (i · 𝐴))
≠ 0)) | 
| 9 | 8 | simp1bi 1146 | . . . . . 6
⊢ (𝐴 ∈ dom arctan → 𝐴 ∈
ℂ) | 
| 10 | 9 | sqcld 14184 | . . . . 5
⊢ (𝐴 ∈ dom arctan → (𝐴↑2) ∈
ℂ) | 
| 11 |  | addcl 11237 | . . . . 5
⊢ ((1
∈ ℂ ∧ (𝐴↑2) ∈ ℂ) → (1 + (𝐴↑2)) ∈
ℂ) | 
| 12 | 7, 10, 11 | sylancr 587 | . . . 4
⊢ (𝐴 ∈ dom arctan → (1 +
(𝐴↑2)) ∈
ℂ) | 
| 13 | 12 | sqrtcld 15476 | . . 3
⊢ (𝐴 ∈ dom arctan →
(√‘(1 + (𝐴↑2))) ∈ ℂ) | 
| 14 | 12 | sqsqrtd 15478 | . . . . 5
⊢ (𝐴 ∈ dom arctan →
((√‘(1 + (𝐴↑2)))↑2) = (1 + (𝐴↑2))) | 
| 15 |  | atandm4 26922 | . . . . . 6
⊢ (𝐴 ∈ dom arctan ↔ (𝐴 ∈ ℂ ∧ (1 +
(𝐴↑2)) ≠
0)) | 
| 16 | 15 | simprbi 496 | . . . . 5
⊢ (𝐴 ∈ dom arctan → (1 +
(𝐴↑2)) ≠
0) | 
| 17 | 14, 16 | eqnetrd 3008 | . . . 4
⊢ (𝐴 ∈ dom arctan →
((√‘(1 + (𝐴↑2)))↑2) ≠ 0) | 
| 18 |  | sqne0 14163 | . . . . 5
⊢
((√‘(1 + (𝐴↑2))) ∈ ℂ →
(((√‘(1 + (𝐴↑2)))↑2) ≠ 0 ↔
(√‘(1 + (𝐴↑2))) ≠ 0)) | 
| 19 | 13, 18 | syl 17 | . . . 4
⊢ (𝐴 ∈ dom arctan →
(((√‘(1 + (𝐴↑2)))↑2) ≠ 0 ↔
(√‘(1 + (𝐴↑2))) ≠ 0)) | 
| 20 | 17, 19 | mpbid 232 | . . 3
⊢ (𝐴 ∈ dom arctan →
(√‘(1 + (𝐴↑2))) ≠ 0) | 
| 21 | 6, 13, 20 | divcan4d 12049 | . 2
⊢ (𝐴 ∈ dom arctan →
(((exp‘(i · (arctan‘𝐴))) · (√‘(1 + (𝐴↑2)))) / (√‘(1
+ (𝐴↑2)))) =
(exp‘(i · (arctan‘𝐴)))) | 
| 22 |  | halfcn 12481 | . . . . . . 7
⊢ (1 / 2)
∈ ℂ | 
| 23 | 12, 16 | logcld 26612 | . . . . . . 7
⊢ (𝐴 ∈ dom arctan →
(log‘(1 + (𝐴↑2))) ∈ ℂ) | 
| 24 |  | mulcl 11239 | . . . . . . 7
⊢ (((1 / 2)
∈ ℂ ∧ (log‘(1 + (𝐴↑2))) ∈ ℂ) → ((1 / 2)
· (log‘(1 + (𝐴↑2)))) ∈ ℂ) | 
| 25 | 22, 23, 24 | sylancr 587 | . . . . . 6
⊢ (𝐴 ∈ dom arctan → ((1 /
2) · (log‘(1 + (𝐴↑2)))) ∈ ℂ) | 
| 26 |  | efadd 16130 | . . . . . 6
⊢ (((i
· (arctan‘𝐴))
∈ ℂ ∧ ((1 / 2) · (log‘(1 + (𝐴↑2)))) ∈ ℂ) →
(exp‘((i · (arctan‘𝐴)) + ((1 / 2) · (log‘(1 +
(𝐴↑2)))))) =
((exp‘(i · (arctan‘𝐴))) · (exp‘((1 / 2) ·
(log‘(1 + (𝐴↑2))))))) | 
| 27 | 4, 25, 26 | syl2anc 584 | . . . . 5
⊢ (𝐴 ∈ dom arctan →
(exp‘((i · (arctan‘𝐴)) + ((1 / 2) · (log‘(1 +
(𝐴↑2)))))) =
((exp‘(i · (arctan‘𝐴))) · (exp‘((1 / 2) ·
(log‘(1 + (𝐴↑2))))))) | 
| 28 |  | 2cn 12341 | . . . . . . . . . . . 12
⊢ 2 ∈
ℂ | 
| 29 | 28 | a1i 11 | . . . . . . . . . . 11
⊢ (𝐴 ∈ dom arctan → 2
∈ ℂ) | 
| 30 |  | mulcl 11239 | . . . . . . . . . . . . . 14
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i · 𝐴) ∈ ℂ) | 
| 31 | 1, 9, 30 | sylancr 587 | . . . . . . . . . . . . 13
⊢ (𝐴 ∈ dom arctan → (i
· 𝐴) ∈
ℂ) | 
| 32 |  | addcl 11237 | . . . . . . . . . . . . 13
⊢ ((1
∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (1 + (i ·
𝐴)) ∈
ℂ) | 
| 33 | 7, 31, 32 | sylancr 587 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ dom arctan → (1 +
(i · 𝐴)) ∈
ℂ) | 
| 34 | 8 | simp3bi 1148 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ dom arctan → (1 +
(i · 𝐴)) ≠
0) | 
| 35 | 33, 34 | logcld 26612 | . . . . . . . . . . 11
⊢ (𝐴 ∈ dom arctan →
(log‘(1 + (i · 𝐴))) ∈ ℂ) | 
| 36 | 29, 35, 4 | subdid 11719 | . . . . . . . . . 10
⊢ (𝐴 ∈ dom arctan → (2
· ((log‘(1 + (i · 𝐴))) − (i · (arctan‘𝐴)))) = ((2 ·
(log‘(1 + (i · 𝐴)))) − (2 · (i ·
(arctan‘𝐴))))) | 
| 37 |  | atanval 26927 | . . . . . . . . . . . . 13
⊢ (𝐴 ∈ dom arctan →
(arctan‘𝐴) = ((i / 2)
· ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴)))))) | 
| 38 | 37 | oveq2d 7447 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ dom arctan → ((2
· i) · (arctan‘𝐴)) = ((2 · i) · ((i / 2)
· ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴))))))) | 
| 39 | 1 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝐴 ∈ dom arctan → i
∈ ℂ) | 
| 40 | 29, 39, 2 | mulassd 11284 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ dom arctan → ((2
· i) · (arctan‘𝐴)) = (2 · (i ·
(arctan‘𝐴)))) | 
| 41 |  | halfcl 12491 | . . . . . . . . . . . . . . . . . 18
⊢ (i ∈
ℂ → (i / 2) ∈ ℂ) | 
| 42 | 1, 41 | ax-mp 5 | . . . . . . . . . . . . . . . . 17
⊢ (i / 2)
∈ ℂ | 
| 43 | 28, 1, 42 | mulassi 11272 | . . . . . . . . . . . . . . . 16
⊢ ((2
· i) · (i / 2)) = (2 · (i · (i /
2))) | 
| 44 | 28, 1, 42 | mul12i 11456 | . . . . . . . . . . . . . . . 16
⊢ (2
· (i · (i / 2))) = (i · (2 · (i /
2))) | 
| 45 |  | 2ne0 12370 | . . . . . . . . . . . . . . . . . . 19
⊢ 2 ≠
0 | 
| 46 | 1, 28, 45 | divcan2i 12010 | . . . . . . . . . . . . . . . . . 18
⊢ (2
· (i / 2)) = i | 
| 47 | 46 | oveq2i 7442 | . . . . . . . . . . . . . . . . 17
⊢ (i
· (2 · (i / 2))) = (i · i) | 
| 48 |  | ixi 11892 | . . . . . . . . . . . . . . . . 17
⊢ (i
· i) = -1 | 
| 49 | 47, 48 | eqtri 2765 | . . . . . . . . . . . . . . . 16
⊢ (i
· (2 · (i / 2))) = -1 | 
| 50 | 43, 44, 49 | 3eqtri 2769 | . . . . . . . . . . . . . . 15
⊢ ((2
· i) · (i / 2)) = -1 | 
| 51 | 50 | oveq1i 7441 | . . . . . . . . . . . . . 14
⊢ (((2
· i) · (i / 2)) · ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i
· 𝐴))))) = (-1
· ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴))))) | 
| 52 |  | subcl 11507 | . . . . . . . . . . . . . . . . . 18
⊢ ((1
∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (1 − (i
· 𝐴)) ∈
ℂ) | 
| 53 | 7, 31, 52 | sylancr 587 | . . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ dom arctan → (1
− (i · 𝐴))
∈ ℂ) | 
| 54 | 8 | simp2bi 1147 | . . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ dom arctan → (1
− (i · 𝐴))
≠ 0) | 
| 55 | 53, 54 | logcld 26612 | . . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ dom arctan →
(log‘(1 − (i · 𝐴))) ∈ ℂ) | 
| 56 | 55, 35 | subcld 11620 | . . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ dom arctan →
((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴)))) ∈
ℂ) | 
| 57 | 56 | mulm1d 11715 | . . . . . . . . . . . . . 14
⊢ (𝐴 ∈ dom arctan → (-1
· ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴))))) = -((log‘(1
− (i · 𝐴)))
− (log‘(1 + (i · 𝐴))))) | 
| 58 | 51, 57 | eqtrid 2789 | . . . . . . . . . . . . 13
⊢ (𝐴 ∈ dom arctan → (((2
· i) · (i / 2)) · ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i
· 𝐴))))) =
-((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴))))) | 
| 59 |  | 2mulicn 12489 | . . . . . . . . . . . . . . 15
⊢ (2
· i) ∈ ℂ | 
| 60 | 59 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (𝐴 ∈ dom arctan → (2
· i) ∈ ℂ) | 
| 61 | 42 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (𝐴 ∈ dom arctan → (i /
2) ∈ ℂ) | 
| 62 | 60, 61, 56 | mulassd 11284 | . . . . . . . . . . . . 13
⊢ (𝐴 ∈ dom arctan → (((2
· i) · (i / 2)) · ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i
· 𝐴))))) = ((2
· i) · ((i / 2) · ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i
· 𝐴))))))) | 
| 63 | 55, 35 | negsubdi2d 11636 | . . . . . . . . . . . . 13
⊢ (𝐴 ∈ dom arctan →
-((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴)))) = ((log‘(1 + (i
· 𝐴))) −
(log‘(1 − (i · 𝐴))))) | 
| 64 | 58, 62, 63 | 3eqtr3d 2785 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ dom arctan → ((2
· i) · ((i / 2) · ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i
· 𝐴)))))) =
((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) | 
| 65 | 38, 40, 64 | 3eqtr3d 2785 | . . . . . . . . . . 11
⊢ (𝐴 ∈ dom arctan → (2
· (i · (arctan‘𝐴))) = ((log‘(1 + (i · 𝐴))) − (log‘(1
− (i · 𝐴))))) | 
| 66 | 65 | oveq2d 7447 | . . . . . . . . . 10
⊢ (𝐴 ∈ dom arctan → ((2
· (log‘(1 + (i · 𝐴)))) − (2 · (i ·
(arctan‘𝐴)))) = ((2
· (log‘(1 + (i · 𝐴)))) − ((log‘(1 + (i ·
𝐴))) − (log‘(1
− (i · 𝐴)))))) | 
| 67 |  | mulcl 11239 | . . . . . . . . . . . . 13
⊢ ((2
∈ ℂ ∧ (log‘(1 + (i · 𝐴))) ∈ ℂ) → (2 ·
(log‘(1 + (i · 𝐴)))) ∈ ℂ) | 
| 68 | 28, 35, 67 | sylancr 587 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ dom arctan → (2
· (log‘(1 + (i · 𝐴)))) ∈ ℂ) | 
| 69 | 68, 35, 55 | subsubd 11648 | . . . . . . . . . . 11
⊢ (𝐴 ∈ dom arctan → ((2
· (log‘(1 + (i · 𝐴)))) − ((log‘(1 + (i ·
𝐴))) − (log‘(1
− (i · 𝐴)))))
= (((2 · (log‘(1 + (i · 𝐴)))) − (log‘(1 + (i ·
𝐴)))) + (log‘(1
− (i · 𝐴))))) | 
| 70 | 35 | 2timesd 12509 | . . . . . . . . . . . . 13
⊢ (𝐴 ∈ dom arctan → (2
· (log‘(1 + (i · 𝐴)))) = ((log‘(1 + (i · 𝐴))) + (log‘(1 + (i
· 𝐴))))) | 
| 71 | 35, 35, 70 | mvrladdd 11676 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ dom arctan → ((2
· (log‘(1 + (i · 𝐴)))) − (log‘(1 + (i ·
𝐴)))) = (log‘(1 + (i
· 𝐴)))) | 
| 72 | 71 | oveq1d 7446 | . . . . . . . . . . 11
⊢ (𝐴 ∈ dom arctan → (((2
· (log‘(1 + (i · 𝐴)))) − (log‘(1 + (i ·
𝐴)))) + (log‘(1
− (i · 𝐴)))) =
((log‘(1 + (i · 𝐴))) + (log‘(1 − (i ·
𝐴))))) | 
| 73 |  | atanlogadd 26957 | . . . . . . . . . . . . 13
⊢ (𝐴 ∈ dom arctan →
((log‘(1 + (i · 𝐴))) + (log‘(1 − (i ·
𝐴)))) ∈ ran
log) | 
| 74 |  | logef 26623 | . . . . . . . . . . . . 13
⊢
(((log‘(1 + (i · 𝐴))) + (log‘(1 − (i ·
𝐴)))) ∈ ran log →
(log‘(exp‘((log‘(1 + (i · 𝐴))) + (log‘(1 − (i ·
𝐴)))))) = ((log‘(1 +
(i · 𝐴))) +
(log‘(1 − (i · 𝐴))))) | 
| 75 | 73, 74 | syl 17 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ dom arctan →
(log‘(exp‘((log‘(1 + (i · 𝐴))) + (log‘(1 − (i ·
𝐴)))))) = ((log‘(1 +
(i · 𝐴))) +
(log‘(1 − (i · 𝐴))))) | 
| 76 |  | efadd 16130 | . . . . . . . . . . . . . . 15
⊢
(((log‘(1 + (i · 𝐴))) ∈ ℂ ∧ (log‘(1
− (i · 𝐴)))
∈ ℂ) → (exp‘((log‘(1 + (i · 𝐴))) + (log‘(1 − (i
· 𝐴))))) =
((exp‘(log‘(1 + (i · 𝐴)))) · (exp‘(log‘(1
− (i · 𝐴)))))) | 
| 77 | 35, 55, 76 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (𝐴 ∈ dom arctan →
(exp‘((log‘(1 + (i · 𝐴))) + (log‘(1 − (i ·
𝐴))))) =
((exp‘(log‘(1 + (i · 𝐴)))) · (exp‘(log‘(1
− (i · 𝐴)))))) | 
| 78 |  | eflog 26618 | . . . . . . . . . . . . . . . 16
⊢ (((1 + (i
· 𝐴)) ∈ ℂ
∧ (1 + (i · 𝐴))
≠ 0) → (exp‘(log‘(1 + (i · 𝐴)))) = (1 + (i · 𝐴))) | 
| 79 | 33, 34, 78 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ dom arctan →
(exp‘(log‘(1 + (i · 𝐴)))) = (1 + (i · 𝐴))) | 
| 80 |  | eflog 26618 | . . . . . . . . . . . . . . . 16
⊢ (((1
− (i · 𝐴))
∈ ℂ ∧ (1 − (i · 𝐴)) ≠ 0) → (exp‘(log‘(1
− (i · 𝐴)))) =
(1 − (i · 𝐴))) | 
| 81 | 53, 54, 80 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ dom arctan →
(exp‘(log‘(1 − (i · 𝐴)))) = (1 − (i · 𝐴))) | 
| 82 | 79, 81 | oveq12d 7449 | . . . . . . . . . . . . . 14
⊢ (𝐴 ∈ dom arctan →
((exp‘(log‘(1 + (i · 𝐴)))) · (exp‘(log‘(1
− (i · 𝐴)))))
= ((1 + (i · 𝐴))
· (1 − (i · 𝐴)))) | 
| 83 |  | sq1 14234 | . . . . . . . . . . . . . . . . 17
⊢
(1↑2) = 1 | 
| 84 | 83 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ dom arctan →
(1↑2) = 1) | 
| 85 |  | sqmul 14159 | . . . . . . . . . . . . . . . . . 18
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → ((i · 𝐴)↑2) = ((i↑2) · (𝐴↑2))) | 
| 86 | 1, 9, 85 | sylancr 587 | . . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ dom arctan → ((i
· 𝐴)↑2) =
((i↑2) · (𝐴↑2))) | 
| 87 |  | i2 14241 | . . . . . . . . . . . . . . . . . . 19
⊢
(i↑2) = -1 | 
| 88 | 87 | oveq1i 7441 | . . . . . . . . . . . . . . . . . 18
⊢
((i↑2) · (𝐴↑2)) = (-1 · (𝐴↑2)) | 
| 89 | 10 | mulm1d 11715 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ dom arctan → (-1
· (𝐴↑2)) =
-(𝐴↑2)) | 
| 90 | 88, 89 | eqtrid 2789 | . . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ dom arctan →
((i↑2) · (𝐴↑2)) = -(𝐴↑2)) | 
| 91 | 86, 90 | eqtrd 2777 | . . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ dom arctan → ((i
· 𝐴)↑2) =
-(𝐴↑2)) | 
| 92 | 84, 91 | oveq12d 7449 | . . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ dom arctan →
((1↑2) − ((i · 𝐴)↑2)) = (1 − -(𝐴↑2))) | 
| 93 |  | subsq 14249 | . . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → ((1↑2) −
((i · 𝐴)↑2)) =
((1 + (i · 𝐴))
· (1 − (i · 𝐴)))) | 
| 94 | 7, 31, 93 | sylancr 587 | . . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ dom arctan →
((1↑2) − ((i · 𝐴)↑2)) = ((1 + (i · 𝐴)) · (1 − (i
· 𝐴)))) | 
| 95 |  | subneg 11558 | . . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℂ ∧ (𝐴↑2) ∈ ℂ) → (1 −
-(𝐴↑2)) = (1 + (𝐴↑2))) | 
| 96 | 7, 10, 95 | sylancr 587 | . . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ dom arctan → (1
− -(𝐴↑2)) = (1 +
(𝐴↑2))) | 
| 97 | 92, 94, 96 | 3eqtr3d 2785 | . . . . . . . . . . . . . 14
⊢ (𝐴 ∈ dom arctan → ((1 +
(i · 𝐴)) · (1
− (i · 𝐴))) =
(1 + (𝐴↑2))) | 
| 98 | 77, 82, 97 | 3eqtrd 2781 | . . . . . . . . . . . . 13
⊢ (𝐴 ∈ dom arctan →
(exp‘((log‘(1 + (i · 𝐴))) + (log‘(1 − (i ·
𝐴))))) = (1 + (𝐴↑2))) | 
| 99 | 98 | fveq2d 6910 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ dom arctan →
(log‘(exp‘((log‘(1 + (i · 𝐴))) + (log‘(1 − (i ·
𝐴)))))) = (log‘(1 +
(𝐴↑2)))) | 
| 100 | 75, 99 | eqtr3d 2779 | . . . . . . . . . . 11
⊢ (𝐴 ∈ dom arctan →
((log‘(1 + (i · 𝐴))) + (log‘(1 − (i ·
𝐴)))) = (log‘(1 +
(𝐴↑2)))) | 
| 101 | 69, 72, 100 | 3eqtrd 2781 | . . . . . . . . . 10
⊢ (𝐴 ∈ dom arctan → ((2
· (log‘(1 + (i · 𝐴)))) − ((log‘(1 + (i ·
𝐴))) − (log‘(1
− (i · 𝐴)))))
= (log‘(1 + (𝐴↑2)))) | 
| 102 | 36, 66, 101 | 3eqtrd 2781 | . . . . . . . . 9
⊢ (𝐴 ∈ dom arctan → (2
· ((log‘(1 + (i · 𝐴))) − (i · (arctan‘𝐴)))) = (log‘(1 + (𝐴↑2)))) | 
| 103 | 102 | oveq1d 7446 | . . . . . . . 8
⊢ (𝐴 ∈ dom arctan → ((2
· ((log‘(1 + (i · 𝐴))) − (i · (arctan‘𝐴)))) / 2) = ((log‘(1 +
(𝐴↑2))) /
2)) | 
| 104 | 35, 4 | subcld 11620 | . . . . . . . . 9
⊢ (𝐴 ∈ dom arctan →
((log‘(1 + (i · 𝐴))) − (i · (arctan‘𝐴))) ∈
ℂ) | 
| 105 | 45 | a1i 11 | . . . . . . . . 9
⊢ (𝐴 ∈ dom arctan → 2 ≠
0) | 
| 106 | 104, 29, 105 | divcan3d 12048 | . . . . . . . 8
⊢ (𝐴 ∈ dom arctan → ((2
· ((log‘(1 + (i · 𝐴))) − (i · (arctan‘𝐴)))) / 2) = ((log‘(1 + (i
· 𝐴))) − (i
· (arctan‘𝐴)))) | 
| 107 | 23, 29, 105 | divrec2d 12047 | . . . . . . . 8
⊢ (𝐴 ∈ dom arctan →
((log‘(1 + (𝐴↑2))) / 2) = ((1 / 2) ·
(log‘(1 + (𝐴↑2))))) | 
| 108 | 103, 106,
107 | 3eqtr3d 2785 | . . . . . . 7
⊢ (𝐴 ∈ dom arctan →
((log‘(1 + (i · 𝐴))) − (i · (arctan‘𝐴))) = ((1 / 2) ·
(log‘(1 + (𝐴↑2))))) | 
| 109 | 35, 4, 25 | subaddd 11638 | . . . . . . 7
⊢ (𝐴 ∈ dom arctan →
(((log‘(1 + (i · 𝐴))) − (i · (arctan‘𝐴))) = ((1 / 2) ·
(log‘(1 + (𝐴↑2)))) ↔ ((i ·
(arctan‘𝐴)) + ((1 /
2) · (log‘(1 + (𝐴↑2))))) = (log‘(1 + (i ·
𝐴))))) | 
| 110 | 108, 109 | mpbid 232 | . . . . . 6
⊢ (𝐴 ∈ dom arctan → ((i
· (arctan‘𝐴))
+ ((1 / 2) · (log‘(1 + (𝐴↑2))))) = (log‘(1 + (i ·
𝐴)))) | 
| 111 | 110 | fveq2d 6910 | . . . . 5
⊢ (𝐴 ∈ dom arctan →
(exp‘((i · (arctan‘𝐴)) + ((1 / 2) · (log‘(1 +
(𝐴↑2)))))) =
(exp‘(log‘(1 + (i · 𝐴))))) | 
| 112 | 27, 111 | eqtr3d 2779 | . . . 4
⊢ (𝐴 ∈ dom arctan →
((exp‘(i · (arctan‘𝐴))) · (exp‘((1 / 2) ·
(log‘(1 + (𝐴↑2)))))) = (exp‘(log‘(1 +
(i · 𝐴))))) | 
| 113 | 22 | a1i 11 | . . . . . . 7
⊢ (𝐴 ∈ dom arctan → (1 /
2) ∈ ℂ) | 
| 114 | 12, 16, 113 | cxpefd 26754 | . . . . . 6
⊢ (𝐴 ∈ dom arctan → ((1 +
(𝐴↑2))↑𝑐(1 / 2))
= (exp‘((1 / 2) · (log‘(1 + (𝐴↑2)))))) | 
| 115 |  | cxpsqrt 26745 | . . . . . . 7
⊢ ((1 +
(𝐴↑2)) ∈ ℂ
→ ((1 + (𝐴↑2))↑𝑐(1 / 2))
= (√‘(1 + (𝐴↑2)))) | 
| 116 | 12, 115 | syl 17 | . . . . . 6
⊢ (𝐴 ∈ dom arctan → ((1 +
(𝐴↑2))↑𝑐(1 / 2))
= (√‘(1 + (𝐴↑2)))) | 
| 117 | 114, 116 | eqtr3d 2779 | . . . . 5
⊢ (𝐴 ∈ dom arctan →
(exp‘((1 / 2) · (log‘(1 + (𝐴↑2))))) = (√‘(1 + (𝐴↑2)))) | 
| 118 | 117 | oveq2d 7447 | . . . 4
⊢ (𝐴 ∈ dom arctan →
((exp‘(i · (arctan‘𝐴))) · (exp‘((1 / 2) ·
(log‘(1 + (𝐴↑2)))))) = ((exp‘(i ·
(arctan‘𝐴))) ·
(√‘(1 + (𝐴↑2))))) | 
| 119 | 112, 118,
79 | 3eqtr3d 2785 | . . 3
⊢ (𝐴 ∈ dom arctan →
((exp‘(i · (arctan‘𝐴))) · (√‘(1 + (𝐴↑2)))) = (1 + (i ·
𝐴))) | 
| 120 | 119 | oveq1d 7446 | . 2
⊢ (𝐴 ∈ dom arctan →
(((exp‘(i · (arctan‘𝐴))) · (√‘(1 + (𝐴↑2)))) / (√‘(1
+ (𝐴↑2)))) = ((1 + (i
· 𝐴)) /
(√‘(1 + (𝐴↑2))))) | 
| 121 | 21, 120 | eqtr3d 2779 | 1
⊢ (𝐴 ∈ dom arctan →
(exp‘(i · (arctan‘𝐴))) = ((1 + (i · 𝐴)) / (√‘(1 + (𝐴↑2))))) |