Metamath Proof Explorer

Theorem efiatan2

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

Ref Expression
Assertion efiatan2 
|- ( A e. dom arctan -> ( exp ` ( _i x. ( arctan ` A ) ) ) = ( ( 1 + ( _i x. A ) ) / ( sqrt ` ( 1 + ( A ^ 2 ) ) ) ) )

Proof

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