This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 eqtrid ⊢ ( 𝐴 ∈ 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 eqtrid ⊢ ( 𝐴 ∈ 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 ) ) ) ) )