Proof of Theorem efiatan2
Step | Hyp | Ref
| Expression |
1 | | ax-icn 10033 |
. . . . 5
⊢ i ∈
ℂ |
2 | | atancl 24653 |
. . . . 5
⊢ (𝐴 ∈ dom arctan →
(arctan‘𝐴) ∈
ℂ) |
3 | | mulcl 10058 |
. . . . 5
⊢ ((i
∈ ℂ ∧ (arctan‘𝐴) ∈ ℂ) → (i ·
(arctan‘𝐴)) ∈
ℂ) |
4 | 1, 2, 3 | sylancr 696 |
. . . 4
⊢ (𝐴 ∈ dom arctan → (i
· (arctan‘𝐴))
∈ ℂ) |
5 | | efcl 14857 |
. . . 4
⊢ ((i
· (arctan‘𝐴))
∈ ℂ → (exp‘(i · (arctan‘𝐴))) ∈ ℂ) |
6 | 4, 5 | syl 17 |
. . 3
⊢ (𝐴 ∈ dom arctan →
(exp‘(i · (arctan‘𝐴))) ∈ ℂ) |
7 | | ax-1cn 10032 |
. . . . 5
⊢ 1 ∈
ℂ |
8 | | atandm2 24649 |
. . . . . . 7
⊢ (𝐴 ∈ dom arctan ↔ (𝐴 ∈ ℂ ∧ (1 −
(i · 𝐴)) ≠ 0
∧ (1 + (i · 𝐴))
≠ 0)) |
9 | 8 | simp1bi 1096 |
. . . . . 6
⊢ (𝐴 ∈ dom arctan → 𝐴 ∈
ℂ) |
10 | 9 | sqcld 13046 |
. . . . 5
⊢ (𝐴 ∈ dom arctan → (𝐴↑2) ∈
ℂ) |
11 | | addcl 10056 |
. . . . 5
⊢ ((1
∈ ℂ ∧ (𝐴↑2) ∈ ℂ) → (1 + (𝐴↑2)) ∈
ℂ) |
12 | 7, 10, 11 | sylancr 696 |
. . . 4
⊢ (𝐴 ∈ dom arctan → (1 +
(𝐴↑2)) ∈
ℂ) |
13 | 12 | sqrtcld 14220 |
. . 3
⊢ (𝐴 ∈ dom arctan →
(√‘(1 + (𝐴↑2))) ∈ ℂ) |
14 | 12 | sqsqrtd 14222 |
. . . . 5
⊢ (𝐴 ∈ dom arctan →
((√‘(1 + (𝐴↑2)))↑2) = (1 + (𝐴↑2))) |
15 | | atandm4 24651 |
. . . . . 6
⊢ (𝐴 ∈ dom arctan ↔ (𝐴 ∈ ℂ ∧ (1 +
(𝐴↑2)) ≠
0)) |
16 | 15 | simprbi 479 |
. . . . 5
⊢ (𝐴 ∈ dom arctan → (1 +
(𝐴↑2)) ≠
0) |
17 | 14, 16 | eqnetrd 2890 |
. . . 4
⊢ (𝐴 ∈ dom arctan →
((√‘(1 + (𝐴↑2)))↑2) ≠ 0) |
18 | | sqne0 12970 |
. . . . 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 222 |
. . 3
⊢ (𝐴 ∈ dom arctan →
(√‘(1 + (𝐴↑2))) ≠ 0) |
21 | 6, 13, 20 | divcan4d 10845 |
. 2
⊢ (𝐴 ∈ dom arctan →
(((exp‘(i · (arctan‘𝐴))) · (√‘(1 + (𝐴↑2)))) / (√‘(1
+ (𝐴↑2)))) =
(exp‘(i · (arctan‘𝐴)))) |
22 | | halfcn 11285 |
. . . . . . 7
⊢ (1 / 2)
∈ ℂ |
23 | 12, 16 | logcld 24362 |
. . . . . . 7
⊢ (𝐴 ∈ dom arctan →
(log‘(1 + (𝐴↑2))) ∈ ℂ) |
24 | | mulcl 10058 |
. . . . . . 7
⊢ (((1 / 2)
∈ ℂ ∧ (log‘(1 + (𝐴↑2))) ∈ ℂ) → ((1 / 2)
· (log‘(1 + (𝐴↑2)))) ∈ ℂ) |
25 | 22, 23, 24 | sylancr 696 |
. . . . . 6
⊢ (𝐴 ∈ dom arctan → ((1 /
2) · (log‘(1 + (𝐴↑2)))) ∈ ℂ) |
26 | | efadd 14868 |
. . . . . 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 694 |
. . . . 5
⊢ (𝐴 ∈ dom arctan →
(exp‘((i · (arctan‘𝐴)) + ((1 / 2) · (log‘(1 +
(𝐴↑2)))))) =
((exp‘(i · (arctan‘𝐴))) · (exp‘((1 / 2) ·
(log‘(1 + (𝐴↑2))))))) |
28 | | 2cn 11129 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℂ |
29 | 28 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ dom arctan → 2
∈ ℂ) |
30 | | mulcl 10058 |
. . . . . . . . . . . . . 14
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i · 𝐴) ∈ ℂ) |
31 | 1, 9, 30 | sylancr 696 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ dom arctan → (i
· 𝐴) ∈
ℂ) |
32 | | addcl 10056 |
. . . . . . . . . . . . 13
⊢ ((1
∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (1 + (i ·
𝐴)) ∈
ℂ) |
33 | 7, 31, 32 | sylancr 696 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ dom arctan → (1 +
(i · 𝐴)) ∈
ℂ) |
34 | 8 | simp3bi 1098 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ dom arctan → (1 +
(i · 𝐴)) ≠
0) |
35 | 33, 34 | logcld 24362 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ dom arctan →
(log‘(1 + (i · 𝐴))) ∈ ℂ) |
36 | 29, 35, 4 | subdid 10524 |
. . . . . . . . . 10
⊢ (𝐴 ∈ dom arctan → (2
· ((log‘(1 + (i · 𝐴))) − (i · (arctan‘𝐴)))) = ((2 ·
(log‘(1 + (i · 𝐴)))) − (2 · (i ·
(arctan‘𝐴))))) |
37 | | atanval 24656 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ dom arctan →
(arctan‘𝐴) = ((i / 2)
· ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴)))))) |
38 | 37 | oveq2d 6706 |
. . . . . . . . . . . 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 10101 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ dom arctan → ((2
· i) · (arctan‘𝐴)) = (2 · (i ·
(arctan‘𝐴)))) |
41 | | halfcl 11295 |
. . . . . . . . . . . . . . . . . 18
⊢ (i ∈
ℂ → (i / 2) ∈ ℂ) |
42 | 1, 41 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ (i / 2)
∈ ℂ |
43 | 28, 1, 42 | mulassi 10087 |
. . . . . . . . . . . . . . . 16
⊢ ((2
· i) · (i / 2)) = (2 · (i · (i /
2))) |
44 | 28, 1, 42 | mul12i 10269 |
. . . . . . . . . . . . . . . 16
⊢ (2
· (i · (i / 2))) = (i · (2 · (i /
2))) |
45 | | 2ne0 11151 |
. . . . . . . . . . . . . . . . . . 19
⊢ 2 ≠
0 |
46 | 1, 28, 45 | divcan2i 10806 |
. . . . . . . . . . . . . . . . . 18
⊢ (2
· (i / 2)) = i |
47 | 46 | oveq2i 6701 |
. . . . . . . . . . . . . . . . 17
⊢ (i
· (2 · (i / 2))) = (i · i) |
48 | | ixi 10694 |
. . . . . . . . . . . . . . . . 17
⊢ (i
· i) = -1 |
49 | 47, 48 | eqtri 2673 |
. . . . . . . . . . . . . . . 16
⊢ (i
· (2 · (i / 2))) = -1 |
50 | 43, 44, 49 | 3eqtri 2677 |
. . . . . . . . . . . . . . 15
⊢ ((2
· i) · (i / 2)) = -1 |
51 | 50 | oveq1i 6700 |
. . . . . . . . . . . . . 14
⊢ (((2
· i) · (i / 2)) · ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i
· 𝐴))))) = (-1
· ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴))))) |
52 | | subcl 10318 |
. . . . . . . . . . . . . . . . . 18
⊢ ((1
∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (1 − (i
· 𝐴)) ∈
ℂ) |
53 | 7, 31, 52 | sylancr 696 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ dom arctan → (1
− (i · 𝐴))
∈ ℂ) |
54 | 8 | simp2bi 1097 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ dom arctan → (1
− (i · 𝐴))
≠ 0) |
55 | 53, 54 | logcld 24362 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ dom arctan →
(log‘(1 − (i · 𝐴))) ∈ ℂ) |
56 | 55, 35 | subcld 10430 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ dom arctan →
((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴)))) ∈
ℂ) |
57 | 56 | mulm1d 10520 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ dom arctan → (-1
· ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴))))) = -((log‘(1
− (i · 𝐴)))
− (log‘(1 + (i · 𝐴))))) |
58 | 51, 57 | syl5eq 2697 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ dom arctan → (((2
· i) · (i / 2)) · ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i
· 𝐴))))) =
-((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴))))) |
59 | | 2mulicn 11293 |
. . . . . . . . . . . . . . 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 10101 |
. . . . . . . . . . . . 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 10446 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ dom arctan →
-((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴)))) = ((log‘(1 + (i
· 𝐴))) −
(log‘(1 − (i · 𝐴))))) |
64 | 58, 62, 63 | 3eqtr3d 2693 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ dom arctan → ((2
· i) · ((i / 2) · ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i
· 𝐴)))))) =
((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) |
65 | 38, 40, 64 | 3eqtr3d 2693 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ dom arctan → (2
· (i · (arctan‘𝐴))) = ((log‘(1 + (i · 𝐴))) − (log‘(1
− (i · 𝐴))))) |
66 | 65 | oveq2d 6706 |
. . . . . . . . . 10
⊢ (𝐴 ∈ dom arctan → ((2
· (log‘(1 + (i · 𝐴)))) − (2 · (i ·
(arctan‘𝐴)))) = ((2
· (log‘(1 + (i · 𝐴)))) − ((log‘(1 + (i ·
𝐴))) − (log‘(1
− (i · 𝐴)))))) |
67 | | mulcl 10058 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℂ ∧ (log‘(1 + (i · 𝐴))) ∈ ℂ) → (2 ·
(log‘(1 + (i · 𝐴)))) ∈ ℂ) |
68 | 28, 35, 67 | sylancr 696 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ dom arctan → (2
· (log‘(1 + (i · 𝐴)))) ∈ ℂ) |
69 | 68, 35, 55 | subsubd 10458 |
. . . . . . . . . . 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 11313 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ dom arctan → (2
· (log‘(1 + (i · 𝐴)))) = ((log‘(1 + (i · 𝐴))) + (log‘(1 + (i
· 𝐴))))) |
71 | 70 | oveq1d 6705 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ dom arctan → ((2
· (log‘(1 + (i · 𝐴)))) − (log‘(1 + (i ·
𝐴)))) = (((log‘(1 +
(i · 𝐴))) +
(log‘(1 + (i · 𝐴)))) − (log‘(1 + (i ·
𝐴))))) |
72 | 35, 35 | pncand 10431 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ dom arctan →
(((log‘(1 + (i · 𝐴))) + (log‘(1 + (i · 𝐴)))) − (log‘(1 + (i
· 𝐴)))) =
(log‘(1 + (i · 𝐴)))) |
73 | 71, 72 | eqtrd 2685 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ dom arctan → ((2
· (log‘(1 + (i · 𝐴)))) − (log‘(1 + (i ·
𝐴)))) = (log‘(1 + (i
· 𝐴)))) |
74 | 73 | oveq1d 6705 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ dom arctan → (((2
· (log‘(1 + (i · 𝐴)))) − (log‘(1 + (i ·
𝐴)))) + (log‘(1
− (i · 𝐴)))) =
((log‘(1 + (i · 𝐴))) + (log‘(1 − (i ·
𝐴))))) |
75 | | atanlogadd 24686 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ dom arctan →
((log‘(1 + (i · 𝐴))) + (log‘(1 − (i ·
𝐴)))) ∈ ran
log) |
76 | | logef 24373 |
. . . . . . . . . . . . 13
⊢
(((log‘(1 + (i · 𝐴))) + (log‘(1 − (i ·
𝐴)))) ∈ ran log →
(log‘(exp‘((log‘(1 + (i · 𝐴))) + (log‘(1 − (i ·
𝐴)))))) = ((log‘(1 +
(i · 𝐴))) +
(log‘(1 − (i · 𝐴))))) |
77 | 75, 76 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ dom arctan →
(log‘(exp‘((log‘(1 + (i · 𝐴))) + (log‘(1 − (i ·
𝐴)))))) = ((log‘(1 +
(i · 𝐴))) +
(log‘(1 − (i · 𝐴))))) |
78 | | efadd 14868 |
. . . . . . . . . . . . . . 15
⊢
(((log‘(1 + (i · 𝐴))) ∈ ℂ ∧ (log‘(1
− (i · 𝐴)))
∈ ℂ) → (exp‘((log‘(1 + (i · 𝐴))) + (log‘(1 − (i
· 𝐴))))) =
((exp‘(log‘(1 + (i · 𝐴)))) · (exp‘(log‘(1
− (i · 𝐴)))))) |
79 | 35, 55, 78 | syl2anc 694 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ dom arctan →
(exp‘((log‘(1 + (i · 𝐴))) + (log‘(1 − (i ·
𝐴))))) =
((exp‘(log‘(1 + (i · 𝐴)))) · (exp‘(log‘(1
− (i · 𝐴)))))) |
80 | | eflog 24368 |
. . . . . . . . . . . . . . . 16
⊢ (((1 + (i
· 𝐴)) ∈ ℂ
∧ (1 + (i · 𝐴))
≠ 0) → (exp‘(log‘(1 + (i · 𝐴)))) = (1 + (i · 𝐴))) |
81 | 33, 34, 80 | syl2anc 694 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ dom arctan →
(exp‘(log‘(1 + (i · 𝐴)))) = (1 + (i · 𝐴))) |
82 | | eflog 24368 |
. . . . . . . . . . . . . . . 16
⊢ (((1
− (i · 𝐴))
∈ ℂ ∧ (1 − (i · 𝐴)) ≠ 0) → (exp‘(log‘(1
− (i · 𝐴)))) =
(1 − (i · 𝐴))) |
83 | 53, 54, 82 | syl2anc 694 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ dom arctan →
(exp‘(log‘(1 − (i · 𝐴)))) = (1 − (i · 𝐴))) |
84 | 81, 83 | oveq12d 6708 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ dom arctan →
((exp‘(log‘(1 + (i · 𝐴)))) · (exp‘(log‘(1
− (i · 𝐴)))))
= ((1 + (i · 𝐴))
· (1 − (i · 𝐴)))) |
85 | | sq1 12998 |
. . . . . . . . . . . . . . . . 17
⊢
(1↑2) = 1 |
86 | 85 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ dom arctan →
(1↑2) = 1) |
87 | | sqmul 12966 |
. . . . . . . . . . . . . . . . . 18
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → ((i · 𝐴)↑2) = ((i↑2) · (𝐴↑2))) |
88 | 1, 9, 87 | sylancr 696 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ dom arctan → ((i
· 𝐴)↑2) =
((i↑2) · (𝐴↑2))) |
89 | | i2 13005 |
. . . . . . . . . . . . . . . . . . 19
⊢
(i↑2) = -1 |
90 | 89 | oveq1i 6700 |
. . . . . . . . . . . . . . . . . 18
⊢
((i↑2) · (𝐴↑2)) = (-1 · (𝐴↑2)) |
91 | 10 | mulm1d 10520 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ dom arctan → (-1
· (𝐴↑2)) =
-(𝐴↑2)) |
92 | 90, 91 | syl5eq 2697 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ dom arctan →
((i↑2) · (𝐴↑2)) = -(𝐴↑2)) |
93 | 88, 92 | eqtrd 2685 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ dom arctan → ((i
· 𝐴)↑2) =
-(𝐴↑2)) |
94 | 86, 93 | oveq12d 6708 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ dom arctan →
((1↑2) − ((i · 𝐴)↑2)) = (1 − -(𝐴↑2))) |
95 | | subsq 13012 |
. . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → ((1↑2) −
((i · 𝐴)↑2)) =
((1 + (i · 𝐴))
· (1 − (i · 𝐴)))) |
96 | 7, 31, 95 | sylancr 696 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ dom arctan →
((1↑2) − ((i · 𝐴)↑2)) = ((1 + (i · 𝐴)) · (1 − (i
· 𝐴)))) |
97 | | subneg 10368 |
. . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℂ ∧ (𝐴↑2) ∈ ℂ) → (1 −
-(𝐴↑2)) = (1 + (𝐴↑2))) |
98 | 7, 10, 97 | sylancr 696 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ dom arctan → (1
− -(𝐴↑2)) = (1 +
(𝐴↑2))) |
99 | 94, 96, 98 | 3eqtr3d 2693 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ dom arctan → ((1 +
(i · 𝐴)) · (1
− (i · 𝐴))) =
(1 + (𝐴↑2))) |
100 | 79, 84, 99 | 3eqtrd 2689 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ dom arctan →
(exp‘((log‘(1 + (i · 𝐴))) + (log‘(1 − (i ·
𝐴))))) = (1 + (𝐴↑2))) |
101 | 100 | fveq2d 6233 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ dom arctan →
(log‘(exp‘((log‘(1 + (i · 𝐴))) + (log‘(1 − (i ·
𝐴)))))) = (log‘(1 +
(𝐴↑2)))) |
102 | 77, 101 | eqtr3d 2687 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ dom arctan →
((log‘(1 + (i · 𝐴))) + (log‘(1 − (i ·
𝐴)))) = (log‘(1 +
(𝐴↑2)))) |
103 | 69, 74, 102 | 3eqtrd 2689 |
. . . . . . . . . 10
⊢ (𝐴 ∈ dom arctan → ((2
· (log‘(1 + (i · 𝐴)))) − ((log‘(1 + (i ·
𝐴))) − (log‘(1
− (i · 𝐴)))))
= (log‘(1 + (𝐴↑2)))) |
104 | 36, 66, 103 | 3eqtrd 2689 |
. . . . . . . . 9
⊢ (𝐴 ∈ dom arctan → (2
· ((log‘(1 + (i · 𝐴))) − (i · (arctan‘𝐴)))) = (log‘(1 + (𝐴↑2)))) |
105 | 104 | oveq1d 6705 |
. . . . . . . 8
⊢ (𝐴 ∈ dom arctan → ((2
· ((log‘(1 + (i · 𝐴))) − (i · (arctan‘𝐴)))) / 2) = ((log‘(1 +
(𝐴↑2))) /
2)) |
106 | 35, 4 | subcld 10430 |
. . . . . . . . 9
⊢ (𝐴 ∈ dom arctan →
((log‘(1 + (i · 𝐴))) − (i · (arctan‘𝐴))) ∈
ℂ) |
107 | 45 | a1i 11 |
. . . . . . . . 9
⊢ (𝐴 ∈ dom arctan → 2 ≠
0) |
108 | 106, 29, 107 | divcan3d 10844 |
. . . . . . . 8
⊢ (𝐴 ∈ dom arctan → ((2
· ((log‘(1 + (i · 𝐴))) − (i · (arctan‘𝐴)))) / 2) = ((log‘(1 + (i
· 𝐴))) − (i
· (arctan‘𝐴)))) |
109 | 23, 29, 107 | divrec2d 10843 |
. . . . . . . 8
⊢ (𝐴 ∈ dom arctan →
((log‘(1 + (𝐴↑2))) / 2) = ((1 / 2) ·
(log‘(1 + (𝐴↑2))))) |
110 | 105, 108,
109 | 3eqtr3d 2693 |
. . . . . . 7
⊢ (𝐴 ∈ dom arctan →
((log‘(1 + (i · 𝐴))) − (i · (arctan‘𝐴))) = ((1 / 2) ·
(log‘(1 + (𝐴↑2))))) |
111 | 35, 4, 25 | subaddd 10448 |
. . . . . . 7
⊢ (𝐴 ∈ dom arctan →
(((log‘(1 + (i · 𝐴))) − (i · (arctan‘𝐴))) = ((1 / 2) ·
(log‘(1 + (𝐴↑2)))) ↔ ((i ·
(arctan‘𝐴)) + ((1 /
2) · (log‘(1 + (𝐴↑2))))) = (log‘(1 + (i ·
𝐴))))) |
112 | 110, 111 | mpbid 222 |
. . . . . 6
⊢ (𝐴 ∈ dom arctan → ((i
· (arctan‘𝐴))
+ ((1 / 2) · (log‘(1 + (𝐴↑2))))) = (log‘(1 + (i ·
𝐴)))) |
113 | 112 | fveq2d 6233 |
. . . . 5
⊢ (𝐴 ∈ dom arctan →
(exp‘((i · (arctan‘𝐴)) + ((1 / 2) · (log‘(1 +
(𝐴↑2)))))) =
(exp‘(log‘(1 + (i · 𝐴))))) |
114 | 27, 113 | eqtr3d 2687 |
. . . 4
⊢ (𝐴 ∈ dom arctan →
((exp‘(i · (arctan‘𝐴))) · (exp‘((1 / 2) ·
(log‘(1 + (𝐴↑2)))))) = (exp‘(log‘(1 +
(i · 𝐴))))) |
115 | 22 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ dom arctan → (1 /
2) ∈ ℂ) |
116 | 12, 16, 115 | cxpefd 24503 |
. . . . . 6
⊢ (𝐴 ∈ dom arctan → ((1 +
(𝐴↑2))↑𝑐(1 / 2))
= (exp‘((1 / 2) · (log‘(1 + (𝐴↑2)))))) |
117 | | cxpsqrt 24494 |
. . . . . . 7
⊢ ((1 +
(𝐴↑2)) ∈ ℂ
→ ((1 + (𝐴↑2))↑𝑐(1 / 2))
= (√‘(1 + (𝐴↑2)))) |
118 | 12, 117 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ dom arctan → ((1 +
(𝐴↑2))↑𝑐(1 / 2))
= (√‘(1 + (𝐴↑2)))) |
119 | 116, 118 | eqtr3d 2687 |
. . . . 5
⊢ (𝐴 ∈ dom arctan →
(exp‘((1 / 2) · (log‘(1 + (𝐴↑2))))) = (√‘(1 + (𝐴↑2)))) |
120 | 119 | oveq2d 6706 |
. . . 4
⊢ (𝐴 ∈ dom arctan →
((exp‘(i · (arctan‘𝐴))) · (exp‘((1 / 2) ·
(log‘(1 + (𝐴↑2)))))) = ((exp‘(i ·
(arctan‘𝐴))) ·
(√‘(1 + (𝐴↑2))))) |
121 | 114, 120,
81 | 3eqtr3d 2693 |
. . 3
⊢ (𝐴 ∈ dom arctan →
((exp‘(i · (arctan‘𝐴))) · (√‘(1 + (𝐴↑2)))) = (1 + (i ·
𝐴))) |
122 | 121 | oveq1d 6705 |
. 2
⊢ (𝐴 ∈ dom arctan →
(((exp‘(i · (arctan‘𝐴))) · (√‘(1 + (𝐴↑2)))) / (√‘(1
+ (𝐴↑2)))) = ((1 + (i
· 𝐴)) /
(√‘(1 + (𝐴↑2))))) |
123 | 21, 122 | eqtr3d 2687 |
1
⊢ (𝐴 ∈ dom arctan →
(exp‘(i · (arctan‘𝐴))) = ((1 + (i · 𝐴)) / (√‘(1 + (𝐴↑2))))) |