Metamath Proof Explorer


Theorem efiatan2

Description: Value of the exponential of an artcangent. (Contributed by Mario Carneiro, 3-Apr-2015)

Ref Expression
Assertion efiatan2 ( 𝐴 ∈ dom arctan → ( exp ‘ ( i · ( arctan ‘ 𝐴 ) ) ) = ( ( 1 + ( i · 𝐴 ) ) / ( √ ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ax-icn i ∈ ℂ
2 atancl ( 𝐴 ∈ dom arctan → ( arctan ‘ 𝐴 ) ∈ ℂ )
3 mulcl ( ( i ∈ ℂ ∧ ( arctan ‘ 𝐴 ) ∈ ℂ ) → ( i · ( arctan ‘ 𝐴 ) ) ∈ ℂ )
4 1 2 3 sylancr ( 𝐴 ∈ dom arctan → ( i · ( arctan ‘ 𝐴 ) ) ∈ ℂ )
5 efcl ( ( i · ( arctan ‘ 𝐴 ) ) ∈ ℂ → ( exp ‘ ( i · ( arctan ‘ 𝐴 ) ) ) ∈ ℂ )
6 4 5 syl ( 𝐴 ∈ dom arctan → ( exp ‘ ( i · ( arctan ‘ 𝐴 ) ) ) ∈ ℂ )
7 ax-1cn 1 ∈ ℂ
8 atandm2 ( 𝐴 ∈ dom arctan ↔ ( 𝐴 ∈ ℂ ∧ ( 1 − ( i · 𝐴 ) ) ≠ 0 ∧ ( 1 + ( i · 𝐴 ) ) ≠ 0 ) )
9 8 simp1bi ( 𝐴 ∈ dom arctan → 𝐴 ∈ ℂ )
10 9 sqcld ( 𝐴 ∈ dom arctan → ( 𝐴 ↑ 2 ) ∈ ℂ )
11 addcl ( ( 1 ∈ ℂ ∧ ( 𝐴 ↑ 2 ) ∈ ℂ ) → ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ℂ )
12 7 10 11 sylancr ( 𝐴 ∈ dom arctan → ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ℂ )
13 12 sqrtcld ( 𝐴 ∈ dom arctan → ( √ ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) ∈ ℂ )
14 12 sqsqrtd ( 𝐴 ∈ dom arctan → ( ( √ ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) ↑ 2 ) = ( 1 + ( 𝐴 ↑ 2 ) ) )
15 atandm4 ( 𝐴 ∈ dom arctan ↔ ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ≠ 0 ) )
16 15 simprbi ( 𝐴 ∈ dom arctan → ( 1 + ( 𝐴 ↑ 2 ) ) ≠ 0 )
17 14 16 eqnetrd ( 𝐴 ∈ dom arctan → ( ( √ ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) ↑ 2 ) ≠ 0 )
18 sqne0 ( ( √ ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) ∈ ℂ → ( ( ( √ ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) ↑ 2 ) ≠ 0 ↔ ( √ ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) ≠ 0 ) )
19 13 18 syl ( 𝐴 ∈ dom arctan → ( ( ( √ ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) ↑ 2 ) ≠ 0 ↔ ( √ ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) ≠ 0 ) )
20 17 19 mpbid ( 𝐴 ∈ dom arctan → ( √ ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) ≠ 0 )
21 6 13 20 divcan4d ( 𝐴 ∈ dom arctan → ( ( ( exp ‘ ( i · ( arctan ‘ 𝐴 ) ) ) · ( √ ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) ) / ( √ ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) ) = ( exp ‘ ( i · ( arctan ‘ 𝐴 ) ) ) )
22 halfcn ( 1 / 2 ) ∈ ℂ
23 12 16 logcld ( 𝐴 ∈ dom arctan → ( log ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) ∈ ℂ )
24 mulcl ( ( ( 1 / 2 ) ∈ ℂ ∧ ( log ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) ∈ ℂ ) → ( ( 1 / 2 ) · ( log ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) ) ∈ ℂ )
25 22 23 24 sylancr ( 𝐴 ∈ dom arctan → ( ( 1 / 2 ) · ( log ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) ) ∈ ℂ )
26 efadd ( ( ( 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 ( 𝐴 ∈ dom arctan → ( exp ‘ ( ( i · ( arctan ‘ 𝐴 ) ) + ( ( 1 / 2 ) · ( log ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) ) ) ) = ( ( exp ‘ ( i · ( arctan ‘ 𝐴 ) ) ) · ( exp ‘ ( ( 1 / 2 ) · ( log ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) ) ) ) )
28 2cn 2 ∈ ℂ
29 28 a1i ( 𝐴 ∈ dom arctan → 2 ∈ ℂ )
30 mulcl ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
31 1 9 30 sylancr ( 𝐴 ∈ dom arctan → ( i · 𝐴 ) ∈ ℂ )
32 addcl ( ( 1 ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( 1 + ( i · 𝐴 ) ) ∈ ℂ )
33 7 31 32 sylancr ( 𝐴 ∈ dom arctan → ( 1 + ( i · 𝐴 ) ) ∈ ℂ )
34 8 simp3bi ( 𝐴 ∈ dom arctan → ( 1 + ( i · 𝐴 ) ) ≠ 0 )
35 33 34 logcld ( 𝐴 ∈ dom arctan → ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ∈ ℂ )
36 29 35 4 subdid ( 𝐴 ∈ dom arctan → ( 2 · ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( i · ( arctan ‘ 𝐴 ) ) ) ) = ( ( 2 · ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) − ( 2 · ( i · ( arctan ‘ 𝐴 ) ) ) ) )
37 atanval ( 𝐴 ∈ dom arctan → ( arctan ‘ 𝐴 ) = ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) )
38 37 oveq2d ( 𝐴 ∈ dom arctan → ( ( 2 · i ) · ( arctan ‘ 𝐴 ) ) = ( ( 2 · i ) · ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) ) )
39 1 a1i ( 𝐴 ∈ dom arctan → i ∈ ℂ )
40 29 39 2 mulassd ( 𝐴 ∈ dom arctan → ( ( 2 · i ) · ( arctan ‘ 𝐴 ) ) = ( 2 · ( i · ( arctan ‘ 𝐴 ) ) ) )
41 halfcl ( i ∈ ℂ → ( i / 2 ) ∈ ℂ )
42 1 41 ax-mp ( i / 2 ) ∈ ℂ
43 28 1 42 mulassi ( ( 2 · i ) · ( i / 2 ) ) = ( 2 · ( i · ( i / 2 ) ) )
44 28 1 42 mul12i ( 2 · ( i · ( i / 2 ) ) ) = ( i · ( 2 · ( i / 2 ) ) )
45 2ne0 2 ≠ 0
46 1 28 45 divcan2i ( 2 · ( i / 2 ) ) = i
47 46 oveq2i ( i · ( 2 · ( i / 2 ) ) ) = ( i · i )
48 ixi ( i · i ) = - 1
49 47 48 eqtri ( i · ( 2 · ( i / 2 ) ) ) = - 1
50 43 44 49 3eqtri ( ( 2 · i ) · ( i / 2 ) ) = - 1
51 50 oveq1i ( ( ( 2 · i ) · ( i / 2 ) ) · ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) = ( - 1 · ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) )
52 subcl ( ( 1 ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( 1 − ( i · 𝐴 ) ) ∈ ℂ )
53 7 31 52 sylancr ( 𝐴 ∈ dom arctan → ( 1 − ( i · 𝐴 ) ) ∈ ℂ )
54 8 simp2bi ( 𝐴 ∈ dom arctan → ( 1 − ( i · 𝐴 ) ) ≠ 0 )
55 53 54 logcld ( 𝐴 ∈ dom arctan → ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ∈ ℂ )
56 55 35 subcld ( 𝐴 ∈ dom arctan → ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ∈ ℂ )
57 56 mulm1d ( 𝐴 ∈ dom arctan → ( - 1 · ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) = - ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) )
58 51 57 syl5eq ( 𝐴 ∈ dom arctan → ( ( ( 2 · i ) · ( i / 2 ) ) · ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) = - ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) )
59 2mulicn ( 2 · i ) ∈ ℂ
60 59 a1i ( 𝐴 ∈ dom arctan → ( 2 · i ) ∈ ℂ )
61 42 a1i ( 𝐴 ∈ dom arctan → ( i / 2 ) ∈ ℂ )
62 60 61 56 mulassd ( 𝐴 ∈ 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 ( 𝐴 ∈ dom arctan → - ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) = ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) )
64 58 62 63 3eqtr3d ( 𝐴 ∈ dom arctan → ( ( 2 · i ) · ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) ) = ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) )
65 38 40 64 3eqtr3d ( 𝐴 ∈ dom arctan → ( 2 · ( i · ( arctan ‘ 𝐴 ) ) ) = ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) )
66 65 oveq2d ( 𝐴 ∈ dom arctan → ( ( 2 · ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) − ( 2 · ( i · ( arctan ‘ 𝐴 ) ) ) ) = ( ( 2 · ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) − ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) )
67 mulcl ( ( 2 ∈ ℂ ∧ ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ∈ ℂ ) → ( 2 · ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ∈ ℂ )
68 28 35 67 sylancr ( 𝐴 ∈ dom arctan → ( 2 · ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ∈ ℂ )
69 68 35 55 subsubd ( 𝐴 ∈ 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 ( 𝐴 ∈ dom arctan → ( 2 · ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) = ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) + ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) )
71 35 35 70 mvrladdd ( 𝐴 ∈ dom arctan → ( ( 2 · ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) = ( log ‘ ( 1 + ( i · 𝐴 ) ) ) )
72 71 oveq1d ( 𝐴 ∈ dom arctan → ( ( ( 2 · ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) + ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) = ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) + ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) )
73 atanlogadd ( 𝐴 ∈ dom arctan → ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) + ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ∈ ran log )
74 logef ( ( ( 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 ( 𝐴 ∈ dom arctan → ( log ‘ ( exp ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) + ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ) = ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) + ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) )
76 efadd ( ( ( 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 ( 𝐴 ∈ dom arctan → ( exp ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) + ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) = ( ( exp ‘ ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) · ( exp ‘ ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) )
78 eflog ( ( ( 1 + ( i · 𝐴 ) ) ∈ ℂ ∧ ( 1 + ( i · 𝐴 ) ) ≠ 0 ) → ( exp ‘ ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) = ( 1 + ( i · 𝐴 ) ) )
79 33 34 78 syl2anc ( 𝐴 ∈ dom arctan → ( exp ‘ ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) = ( 1 + ( i · 𝐴 ) ) )
80 eflog ( ( ( 1 − ( i · 𝐴 ) ) ∈ ℂ ∧ ( 1 − ( i · 𝐴 ) ) ≠ 0 ) → ( exp ‘ ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) = ( 1 − ( i · 𝐴 ) ) )
81 53 54 80 syl2anc ( 𝐴 ∈ dom arctan → ( exp ‘ ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) = ( 1 − ( i · 𝐴 ) ) )
82 79 81 oveq12d ( 𝐴 ∈ dom arctan → ( ( exp ‘ ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) · ( exp ‘ ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) = ( ( 1 + ( i · 𝐴 ) ) · ( 1 − ( i · 𝐴 ) ) ) )
83 sq1 ( 1 ↑ 2 ) = 1
84 83 a1i ( 𝐴 ∈ dom arctan → ( 1 ↑ 2 ) = 1 )
85 sqmul ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( i · 𝐴 ) ↑ 2 ) = ( ( i ↑ 2 ) · ( 𝐴 ↑ 2 ) ) )
86 1 9 85 sylancr ( 𝐴 ∈ dom arctan → ( ( i · 𝐴 ) ↑ 2 ) = ( ( i ↑ 2 ) · ( 𝐴 ↑ 2 ) ) )
87 i2 ( i ↑ 2 ) = - 1
88 87 oveq1i ( ( i ↑ 2 ) · ( 𝐴 ↑ 2 ) ) = ( - 1 · ( 𝐴 ↑ 2 ) )
89 10 mulm1d ( 𝐴 ∈ dom arctan → ( - 1 · ( 𝐴 ↑ 2 ) ) = - ( 𝐴 ↑ 2 ) )
90 88 89 syl5eq ( 𝐴 ∈ dom arctan → ( ( i ↑ 2 ) · ( 𝐴 ↑ 2 ) ) = - ( 𝐴 ↑ 2 ) )
91 86 90 eqtrd ( 𝐴 ∈ dom arctan → ( ( i · 𝐴 ) ↑ 2 ) = - ( 𝐴 ↑ 2 ) )
92 84 91 oveq12d ( 𝐴 ∈ dom arctan → ( ( 1 ↑ 2 ) − ( ( i · 𝐴 ) ↑ 2 ) ) = ( 1 − - ( 𝐴 ↑ 2 ) ) )
93 subsq ( ( 1 ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( ( 1 ↑ 2 ) − ( ( i · 𝐴 ) ↑ 2 ) ) = ( ( 1 + ( i · 𝐴 ) ) · ( 1 − ( i · 𝐴 ) ) ) )
94 7 31 93 sylancr ( 𝐴 ∈ dom arctan → ( ( 1 ↑ 2 ) − ( ( i · 𝐴 ) ↑ 2 ) ) = ( ( 1 + ( i · 𝐴 ) ) · ( 1 − ( i · 𝐴 ) ) ) )
95 subneg ( ( 1 ∈ ℂ ∧ ( 𝐴 ↑ 2 ) ∈ ℂ ) → ( 1 − - ( 𝐴 ↑ 2 ) ) = ( 1 + ( 𝐴 ↑ 2 ) ) )
96 7 10 95 sylancr ( 𝐴 ∈ dom arctan → ( 1 − - ( 𝐴 ↑ 2 ) ) = ( 1 + ( 𝐴 ↑ 2 ) ) )
97 92 94 96 3eqtr3d ( 𝐴 ∈ dom arctan → ( ( 1 + ( i · 𝐴 ) ) · ( 1 − ( i · 𝐴 ) ) ) = ( 1 + ( 𝐴 ↑ 2 ) ) )
98 77 82 97 3eqtrd ( 𝐴 ∈ dom arctan → ( exp ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) + ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) = ( 1 + ( 𝐴 ↑ 2 ) ) )
99 98 fveq2d ( 𝐴 ∈ dom arctan → ( log ‘ ( exp ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) + ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ) = ( log ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) )
100 75 99 eqtr3d ( 𝐴 ∈ dom arctan → ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) + ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) = ( log ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) )
101 69 72 100 3eqtrd ( 𝐴 ∈ dom arctan → ( ( 2 · ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) − ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) = ( log ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) )
102 36 66 101 3eqtrd ( 𝐴 ∈ dom arctan → ( 2 · ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( i · ( arctan ‘ 𝐴 ) ) ) ) = ( log ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) )
103 102 oveq1d ( 𝐴 ∈ dom arctan → ( ( 2 · ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( i · ( arctan ‘ 𝐴 ) ) ) ) / 2 ) = ( ( log ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) / 2 ) )
104 35 4 subcld ( 𝐴 ∈ dom arctan → ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( i · ( arctan ‘ 𝐴 ) ) ) ∈ ℂ )
105 45 a1i ( 𝐴 ∈ dom arctan → 2 ≠ 0 )
106 104 29 105 divcan3d ( 𝐴 ∈ dom arctan → ( ( 2 · ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( i · ( arctan ‘ 𝐴 ) ) ) ) / 2 ) = ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( i · ( arctan ‘ 𝐴 ) ) ) )
107 23 29 105 divrec2d ( 𝐴 ∈ dom arctan → ( ( log ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) / 2 ) = ( ( 1 / 2 ) · ( log ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) ) )
108 103 106 107 3eqtr3d ( 𝐴 ∈ dom arctan → ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( i · ( arctan ‘ 𝐴 ) ) ) = ( ( 1 / 2 ) · ( log ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) ) )
109 35 4 25 subaddd ( 𝐴 ∈ 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 ( 𝐴 ∈ dom arctan → ( ( i · ( arctan ‘ 𝐴 ) ) + ( ( 1 / 2 ) · ( log ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) ) ) = ( log ‘ ( 1 + ( i · 𝐴 ) ) ) )
111 110 fveq2d ( 𝐴 ∈ dom arctan → ( exp ‘ ( ( i · ( arctan ‘ 𝐴 ) ) + ( ( 1 / 2 ) · ( log ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) ) ) ) = ( exp ‘ ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) )
112 27 111 eqtr3d ( 𝐴 ∈ dom arctan → ( ( exp ‘ ( i · ( arctan ‘ 𝐴 ) ) ) · ( exp ‘ ( ( 1 / 2 ) · ( log ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) ) ) ) = ( exp ‘ ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) )
113 22 a1i ( 𝐴 ∈ dom arctan → ( 1 / 2 ) ∈ ℂ )
114 12 16 113 cxpefd ( 𝐴 ∈ dom arctan → ( ( 1 + ( 𝐴 ↑ 2 ) ) ↑𝑐 ( 1 / 2 ) ) = ( exp ‘ ( ( 1 / 2 ) · ( log ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) ) ) )
115 cxpsqrt ( ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ℂ → ( ( 1 + ( 𝐴 ↑ 2 ) ) ↑𝑐 ( 1 / 2 ) ) = ( √ ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) )
116 12 115 syl ( 𝐴 ∈ dom arctan → ( ( 1 + ( 𝐴 ↑ 2 ) ) ↑𝑐 ( 1 / 2 ) ) = ( √ ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) )
117 114 116 eqtr3d ( 𝐴 ∈ dom arctan → ( exp ‘ ( ( 1 / 2 ) · ( log ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) ) ) = ( √ ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) )
118 117 oveq2d ( 𝐴 ∈ dom arctan → ( ( exp ‘ ( i · ( arctan ‘ 𝐴 ) ) ) · ( exp ‘ ( ( 1 / 2 ) · ( log ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) ) ) ) = ( ( exp ‘ ( i · ( arctan ‘ 𝐴 ) ) ) · ( √ ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) ) )
119 112 118 79 3eqtr3d ( 𝐴 ∈ dom arctan → ( ( exp ‘ ( i · ( arctan ‘ 𝐴 ) ) ) · ( √ ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) ) = ( 1 + ( i · 𝐴 ) ) )
120 119 oveq1d ( 𝐴 ∈ dom arctan → ( ( ( exp ‘ ( i · ( arctan ‘ 𝐴 ) ) ) · ( √ ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) ) / ( √ ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) ) = ( ( 1 + ( i · 𝐴 ) ) / ( √ ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) ) )
121 21 120 eqtr3d ( 𝐴 ∈ dom arctan → ( exp ‘ ( i · ( arctan ‘ 𝐴 ) ) ) = ( ( 1 + ( i · 𝐴 ) ) / ( √ ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) ) )