Proof of Theorem efiatan2
Step | Hyp | Ref
| Expression |
1 | | ax-icn 10676 |
. . . . 5
⊢ i ∈
ℂ |
2 | | atancl 25621 |
. . . . 5
⊢ (𝐴 ∈ dom arctan →
(arctan‘𝐴) ∈
ℂ) |
3 | | mulcl 10701 |
. . . . 5
⊢ ((i
∈ ℂ ∧ (arctan‘𝐴) ∈ ℂ) → (i ·
(arctan‘𝐴)) ∈
ℂ) |
4 | 1, 2, 3 | sylancr 590 |
. . . 4
⊢ (𝐴 ∈ dom arctan → (i
· (arctan‘𝐴))
∈ ℂ) |
5 | | efcl 15530 |
. . . 4
⊢ ((i
· (arctan‘𝐴))
∈ ℂ → (exp‘(i · (arctan‘𝐴))) ∈ ℂ) |
6 | 4, 5 | syl 17 |
. . 3
⊢ (𝐴 ∈ dom arctan →
(exp‘(i · (arctan‘𝐴))) ∈ ℂ) |
7 | | ax-1cn 10675 |
. . . . 5
⊢ 1 ∈
ℂ |
8 | | atandm2 25617 |
. . . . . . 7
⊢ (𝐴 ∈ dom arctan ↔ (𝐴 ∈ ℂ ∧ (1 −
(i · 𝐴)) ≠ 0
∧ (1 + (i · 𝐴))
≠ 0)) |
9 | 8 | simp1bi 1146 |
. . . . . 6
⊢ (𝐴 ∈ dom arctan → 𝐴 ∈
ℂ) |
10 | 9 | sqcld 13602 |
. . . . 5
⊢ (𝐴 ∈ dom arctan → (𝐴↑2) ∈
ℂ) |
11 | | addcl 10699 |
. . . . 5
⊢ ((1
∈ ℂ ∧ (𝐴↑2) ∈ ℂ) → (1 + (𝐴↑2)) ∈
ℂ) |
12 | 7, 10, 11 | sylancr 590 |
. . . 4
⊢ (𝐴 ∈ dom arctan → (1 +
(𝐴↑2)) ∈
ℂ) |
13 | 12 | sqrtcld 14889 |
. . 3
⊢ (𝐴 ∈ dom arctan →
(√‘(1 + (𝐴↑2))) ∈ ℂ) |
14 | 12 | sqsqrtd 14891 |
. . . . 5
⊢ (𝐴 ∈ dom arctan →
((√‘(1 + (𝐴↑2)))↑2) = (1 + (𝐴↑2))) |
15 | | atandm4 25619 |
. . . . . 6
⊢ (𝐴 ∈ dom arctan ↔ (𝐴 ∈ ℂ ∧ (1 +
(𝐴↑2)) ≠
0)) |
16 | 15 | simprbi 500 |
. . . . 5
⊢ (𝐴 ∈ dom arctan → (1 +
(𝐴↑2)) ≠
0) |
17 | 14, 16 | eqnetrd 3001 |
. . . 4
⊢ (𝐴 ∈ dom arctan →
((√‘(1 + (𝐴↑2)))↑2) ≠ 0) |
18 | | sqne0 13583 |
. . . . 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 235 |
. . 3
⊢ (𝐴 ∈ dom arctan →
(√‘(1 + (𝐴↑2))) ≠ 0) |
21 | 6, 13, 20 | divcan4d 11502 |
. 2
⊢ (𝐴 ∈ dom arctan →
(((exp‘(i · (arctan‘𝐴))) · (√‘(1 + (𝐴↑2)))) / (√‘(1
+ (𝐴↑2)))) =
(exp‘(i · (arctan‘𝐴)))) |
22 | | halfcn 11933 |
. . . . . . 7
⊢ (1 / 2)
∈ ℂ |
23 | 12, 16 | logcld 25316 |
. . . . . . 7
⊢ (𝐴 ∈ dom arctan →
(log‘(1 + (𝐴↑2))) ∈ ℂ) |
24 | | mulcl 10701 |
. . . . . . 7
⊢ (((1 / 2)
∈ ℂ ∧ (log‘(1 + (𝐴↑2))) ∈ ℂ) → ((1 / 2)
· (log‘(1 + (𝐴↑2)))) ∈ ℂ) |
25 | 22, 23, 24 | sylancr 590 |
. . . . . 6
⊢ (𝐴 ∈ dom arctan → ((1 /
2) · (log‘(1 + (𝐴↑2)))) ∈ ℂ) |
26 | | efadd 15541 |
. . . . . 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 587 |
. . . . 5
⊢ (𝐴 ∈ dom arctan →
(exp‘((i · (arctan‘𝐴)) + ((1 / 2) · (log‘(1 +
(𝐴↑2)))))) =
((exp‘(i · (arctan‘𝐴))) · (exp‘((1 / 2) ·
(log‘(1 + (𝐴↑2))))))) |
28 | | 2cn 11793 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℂ |
29 | 28 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ dom arctan → 2
∈ ℂ) |
30 | | mulcl 10701 |
. . . . . . . . . . . . . 14
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i · 𝐴) ∈ ℂ) |
31 | 1, 9, 30 | sylancr 590 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ dom arctan → (i
· 𝐴) ∈
ℂ) |
32 | | addcl 10699 |
. . . . . . . . . . . . 13
⊢ ((1
∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (1 + (i ·
𝐴)) ∈
ℂ) |
33 | 7, 31, 32 | sylancr 590 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ dom arctan → (1 +
(i · 𝐴)) ∈
ℂ) |
34 | 8 | simp3bi 1148 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ dom arctan → (1 +
(i · 𝐴)) ≠
0) |
35 | 33, 34 | logcld 25316 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ dom arctan →
(log‘(1 + (i · 𝐴))) ∈ ℂ) |
36 | 29, 35, 4 | subdid 11176 |
. . . . . . . . . 10
⊢ (𝐴 ∈ dom arctan → (2
· ((log‘(1 + (i · 𝐴))) − (i · (arctan‘𝐴)))) = ((2 ·
(log‘(1 + (i · 𝐴)))) − (2 · (i ·
(arctan‘𝐴))))) |
37 | | atanval 25624 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ dom arctan →
(arctan‘𝐴) = ((i / 2)
· ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴)))))) |
38 | 37 | oveq2d 7188 |
. . . . . . . . . . . 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 10744 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ dom arctan → ((2
· i) · (arctan‘𝐴)) = (2 · (i ·
(arctan‘𝐴)))) |
41 | | halfcl 11943 |
. . . . . . . . . . . . . . . . . 18
⊢ (i ∈
ℂ → (i / 2) ∈ ℂ) |
42 | 1, 41 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ (i / 2)
∈ ℂ |
43 | 28, 1, 42 | mulassi 10732 |
. . . . . . . . . . . . . . . 16
⊢ ((2
· i) · (i / 2)) = (2 · (i · (i /
2))) |
44 | 28, 1, 42 | mul12i 10915 |
. . . . . . . . . . . . . . . 16
⊢ (2
· (i · (i / 2))) = (i · (2 · (i /
2))) |
45 | | 2ne0 11822 |
. . . . . . . . . . . . . . . . . . 19
⊢ 2 ≠
0 |
46 | 1, 28, 45 | divcan2i 11463 |
. . . . . . . . . . . . . . . . . 18
⊢ (2
· (i / 2)) = i |
47 | 46 | oveq2i 7183 |
. . . . . . . . . . . . . . . . 17
⊢ (i
· (2 · (i / 2))) = (i · i) |
48 | | ixi 11349 |
. . . . . . . . . . . . . . . . 17
⊢ (i
· i) = -1 |
49 | 47, 48 | eqtri 2761 |
. . . . . . . . . . . . . . . 16
⊢ (i
· (2 · (i / 2))) = -1 |
50 | 43, 44, 49 | 3eqtri 2765 |
. . . . . . . . . . . . . . 15
⊢ ((2
· i) · (i / 2)) = -1 |
51 | 50 | oveq1i 7182 |
. . . . . . . . . . . . . 14
⊢ (((2
· i) · (i / 2)) · ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i
· 𝐴))))) = (-1
· ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴))))) |
52 | | subcl 10965 |
. . . . . . . . . . . . . . . . . 18
⊢ ((1
∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (1 − (i
· 𝐴)) ∈
ℂ) |
53 | 7, 31, 52 | sylancr 590 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ dom arctan → (1
− (i · 𝐴))
∈ ℂ) |
54 | 8 | simp2bi 1147 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ dom arctan → (1
− (i · 𝐴))
≠ 0) |
55 | 53, 54 | logcld 25316 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ dom arctan →
(log‘(1 − (i · 𝐴))) ∈ ℂ) |
56 | 55, 35 | subcld 11077 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ dom arctan →
((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴)))) ∈
ℂ) |
57 | 56 | mulm1d 11172 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ dom arctan → (-1
· ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴))))) = -((log‘(1
− (i · 𝐴)))
− (log‘(1 + (i · 𝐴))))) |
58 | 51, 57 | syl5eq 2785 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ dom arctan → (((2
· i) · (i / 2)) · ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i
· 𝐴))))) =
-((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴))))) |
59 | | 2mulicn 11941 |
. . . . . . . . . . . . . . 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 10744 |
. . . . . . . . . . . . 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 11093 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ dom arctan →
-((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴)))) = ((log‘(1 + (i
· 𝐴))) −
(log‘(1 − (i · 𝐴))))) |
64 | 58, 62, 63 | 3eqtr3d 2781 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ dom arctan → ((2
· i) · ((i / 2) · ((log‘(1 − (i · 𝐴))) − (log‘(1 + (i
· 𝐴)))))) =
((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) |
65 | 38, 40, 64 | 3eqtr3d 2781 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ dom arctan → (2
· (i · (arctan‘𝐴))) = ((log‘(1 + (i · 𝐴))) − (log‘(1
− (i · 𝐴))))) |
66 | 65 | oveq2d 7188 |
. . . . . . . . . 10
⊢ (𝐴 ∈ dom arctan → ((2
· (log‘(1 + (i · 𝐴)))) − (2 · (i ·
(arctan‘𝐴)))) = ((2
· (log‘(1 + (i · 𝐴)))) − ((log‘(1 + (i ·
𝐴))) − (log‘(1
− (i · 𝐴)))))) |
67 | | mulcl 10701 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℂ ∧ (log‘(1 + (i · 𝐴))) ∈ ℂ) → (2 ·
(log‘(1 + (i · 𝐴)))) ∈ ℂ) |
68 | 28, 35, 67 | sylancr 590 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ dom arctan → (2
· (log‘(1 + (i · 𝐴)))) ∈ ℂ) |
69 | 68, 35, 55 | subsubd 11105 |
. . . . . . . . . . 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 11961 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ dom arctan → (2
· (log‘(1 + (i · 𝐴)))) = ((log‘(1 + (i · 𝐴))) + (log‘(1 + (i
· 𝐴))))) |
71 | 35, 35, 70 | mvrladdd 11133 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ dom arctan → ((2
· (log‘(1 + (i · 𝐴)))) − (log‘(1 + (i ·
𝐴)))) = (log‘(1 + (i
· 𝐴)))) |
72 | 71 | oveq1d 7187 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ dom arctan → (((2
· (log‘(1 + (i · 𝐴)))) − (log‘(1 + (i ·
𝐴)))) + (log‘(1
− (i · 𝐴)))) =
((log‘(1 + (i · 𝐴))) + (log‘(1 − (i ·
𝐴))))) |
73 | | atanlogadd 25654 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ dom arctan →
((log‘(1 + (i · 𝐴))) + (log‘(1 − (i ·
𝐴)))) ∈ ran
log) |
74 | | logef 25327 |
. . . . . . . . . . . . 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 15541 |
. . . . . . . . . . . . . . 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 587 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ dom arctan →
(exp‘((log‘(1 + (i · 𝐴))) + (log‘(1 − (i ·
𝐴))))) =
((exp‘(log‘(1 + (i · 𝐴)))) · (exp‘(log‘(1
− (i · 𝐴)))))) |
78 | | eflog 25322 |
. . . . . . . . . . . . . . . 16
⊢ (((1 + (i
· 𝐴)) ∈ ℂ
∧ (1 + (i · 𝐴))
≠ 0) → (exp‘(log‘(1 + (i · 𝐴)))) = (1 + (i · 𝐴))) |
79 | 33, 34, 78 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ dom arctan →
(exp‘(log‘(1 + (i · 𝐴)))) = (1 + (i · 𝐴))) |
80 | | eflog 25322 |
. . . . . . . . . . . . . . . 16
⊢ (((1
− (i · 𝐴))
∈ ℂ ∧ (1 − (i · 𝐴)) ≠ 0) → (exp‘(log‘(1
− (i · 𝐴)))) =
(1 − (i · 𝐴))) |
81 | 53, 54, 80 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ dom arctan →
(exp‘(log‘(1 − (i · 𝐴)))) = (1 − (i · 𝐴))) |
82 | 79, 81 | oveq12d 7190 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ dom arctan →
((exp‘(log‘(1 + (i · 𝐴)))) · (exp‘(log‘(1
− (i · 𝐴)))))
= ((1 + (i · 𝐴))
· (1 − (i · 𝐴)))) |
83 | | sq1 13652 |
. . . . . . . . . . . . . . . . 17
⊢
(1↑2) = 1 |
84 | 83 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ dom arctan →
(1↑2) = 1) |
85 | | sqmul 13579 |
. . . . . . . . . . . . . . . . . 18
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → ((i · 𝐴)↑2) = ((i↑2) · (𝐴↑2))) |
86 | 1, 9, 85 | sylancr 590 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ dom arctan → ((i
· 𝐴)↑2) =
((i↑2) · (𝐴↑2))) |
87 | | i2 13659 |
. . . . . . . . . . . . . . . . . . 19
⊢
(i↑2) = -1 |
88 | 87 | oveq1i 7182 |
. . . . . . . . . . . . . . . . . 18
⊢
((i↑2) · (𝐴↑2)) = (-1 · (𝐴↑2)) |
89 | 10 | mulm1d 11172 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ dom arctan → (-1
· (𝐴↑2)) =
-(𝐴↑2)) |
90 | 88, 89 | syl5eq 2785 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ dom arctan →
((i↑2) · (𝐴↑2)) = -(𝐴↑2)) |
91 | 86, 90 | eqtrd 2773 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ dom arctan → ((i
· 𝐴)↑2) =
-(𝐴↑2)) |
92 | 84, 91 | oveq12d 7190 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ dom arctan →
((1↑2) − ((i · 𝐴)↑2)) = (1 − -(𝐴↑2))) |
93 | | subsq 13666 |
. . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → ((1↑2) −
((i · 𝐴)↑2)) =
((1 + (i · 𝐴))
· (1 − (i · 𝐴)))) |
94 | 7, 31, 93 | sylancr 590 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ dom arctan →
((1↑2) − ((i · 𝐴)↑2)) = ((1 + (i · 𝐴)) · (1 − (i
· 𝐴)))) |
95 | | subneg 11015 |
. . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℂ ∧ (𝐴↑2) ∈ ℂ) → (1 −
-(𝐴↑2)) = (1 + (𝐴↑2))) |
96 | 7, 10, 95 | sylancr 590 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ dom arctan → (1
− -(𝐴↑2)) = (1 +
(𝐴↑2))) |
97 | 92, 94, 96 | 3eqtr3d 2781 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ dom arctan → ((1 +
(i · 𝐴)) · (1
− (i · 𝐴))) =
(1 + (𝐴↑2))) |
98 | 77, 82, 97 | 3eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ dom arctan →
(exp‘((log‘(1 + (i · 𝐴))) + (log‘(1 − (i ·
𝐴))))) = (1 + (𝐴↑2))) |
99 | 98 | fveq2d 6680 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ dom arctan →
(log‘(exp‘((log‘(1 + (i · 𝐴))) + (log‘(1 − (i ·
𝐴)))))) = (log‘(1 +
(𝐴↑2)))) |
100 | 75, 99 | eqtr3d 2775 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ dom arctan →
((log‘(1 + (i · 𝐴))) + (log‘(1 − (i ·
𝐴)))) = (log‘(1 +
(𝐴↑2)))) |
101 | 69, 72, 100 | 3eqtrd 2777 |
. . . . . . . . . 10
⊢ (𝐴 ∈ dom arctan → ((2
· (log‘(1 + (i · 𝐴)))) − ((log‘(1 + (i ·
𝐴))) − (log‘(1
− (i · 𝐴)))))
= (log‘(1 + (𝐴↑2)))) |
102 | 36, 66, 101 | 3eqtrd 2777 |
. . . . . . . . 9
⊢ (𝐴 ∈ dom arctan → (2
· ((log‘(1 + (i · 𝐴))) − (i · (arctan‘𝐴)))) = (log‘(1 + (𝐴↑2)))) |
103 | 102 | oveq1d 7187 |
. . . . . . . 8
⊢ (𝐴 ∈ dom arctan → ((2
· ((log‘(1 + (i · 𝐴))) − (i · (arctan‘𝐴)))) / 2) = ((log‘(1 +
(𝐴↑2))) /
2)) |
104 | 35, 4 | subcld 11077 |
. . . . . . . . 9
⊢ (𝐴 ∈ dom arctan →
((log‘(1 + (i · 𝐴))) − (i · (arctan‘𝐴))) ∈
ℂ) |
105 | 45 | a1i 11 |
. . . . . . . . 9
⊢ (𝐴 ∈ dom arctan → 2 ≠
0) |
106 | 104, 29, 105 | divcan3d 11501 |
. . . . . . . 8
⊢ (𝐴 ∈ dom arctan → ((2
· ((log‘(1 + (i · 𝐴))) − (i · (arctan‘𝐴)))) / 2) = ((log‘(1 + (i
· 𝐴))) − (i
· (arctan‘𝐴)))) |
107 | 23, 29, 105 | divrec2d 11500 |
. . . . . . . 8
⊢ (𝐴 ∈ dom arctan →
((log‘(1 + (𝐴↑2))) / 2) = ((1 / 2) ·
(log‘(1 + (𝐴↑2))))) |
108 | 103, 106,
107 | 3eqtr3d 2781 |
. . . . . . 7
⊢ (𝐴 ∈ dom arctan →
((log‘(1 + (i · 𝐴))) − (i · (arctan‘𝐴))) = ((1 / 2) ·
(log‘(1 + (𝐴↑2))))) |
109 | 35, 4, 25 | subaddd 11095 |
. . . . . . 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 235 |
. . . . . 6
⊢ (𝐴 ∈ dom arctan → ((i
· (arctan‘𝐴))
+ ((1 / 2) · (log‘(1 + (𝐴↑2))))) = (log‘(1 + (i ·
𝐴)))) |
111 | 110 | fveq2d 6680 |
. . . . 5
⊢ (𝐴 ∈ dom arctan →
(exp‘((i · (arctan‘𝐴)) + ((1 / 2) · (log‘(1 +
(𝐴↑2)))))) =
(exp‘(log‘(1 + (i · 𝐴))))) |
112 | 27, 111 | eqtr3d 2775 |
. . . 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 25457 |
. . . . . 6
⊢ (𝐴 ∈ dom arctan → ((1 +
(𝐴↑2))↑𝑐(1 / 2))
= (exp‘((1 / 2) · (log‘(1 + (𝐴↑2)))))) |
115 | | cxpsqrt 25448 |
. . . . . . 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 2775 |
. . . . 5
⊢ (𝐴 ∈ dom arctan →
(exp‘((1 / 2) · (log‘(1 + (𝐴↑2))))) = (√‘(1 + (𝐴↑2)))) |
118 | 117 | oveq2d 7188 |
. . . 4
⊢ (𝐴 ∈ dom arctan →
((exp‘(i · (arctan‘𝐴))) · (exp‘((1 / 2) ·
(log‘(1 + (𝐴↑2)))))) = ((exp‘(i ·
(arctan‘𝐴))) ·
(√‘(1 + (𝐴↑2))))) |
119 | 112, 118,
79 | 3eqtr3d 2781 |
. . 3
⊢ (𝐴 ∈ dom arctan →
((exp‘(i · (arctan‘𝐴))) · (√‘(1 + (𝐴↑2)))) = (1 + (i ·
𝐴))) |
120 | 119 | oveq1d 7187 |
. 2
⊢ (𝐴 ∈ dom arctan →
(((exp‘(i · (arctan‘𝐴))) · (√‘(1 + (𝐴↑2)))) / (√‘(1
+ (𝐴↑2)))) = ((1 + (i
· 𝐴)) /
(√‘(1 + (𝐴↑2))))) |
121 | 21, 120 | eqtr3d 2775 |
1
⊢ (𝐴 ∈ dom arctan →
(exp‘(i · (arctan‘𝐴))) = ((1 + (i · 𝐴)) / (√‘(1 + (𝐴↑2))))) |