Metamath Proof Explorer

Theorem 2efiatan

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

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

Proof

Step Hyp Ref Expression
1 atanval 
 |-  ( A e. dom arctan -> ( arctan ` A ) = ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) )
2 1 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 ) ) ) ) ) ) )
3 2cn 
 |-  2 e. CC
4 3 a1i 
 |-  ( A e. dom arctan -> 2 e. CC )
5 ax-icn 
 |-  _i e. CC
6 5 a1i 
 |-  ( A e. dom arctan -> _i e. CC )
7 atancl 
 |-  ( A e. dom arctan -> ( arctan ` A ) e. CC )
8 4 6 7 mulassd 
 |-  ( A e. dom arctan -> ( ( 2 x. _i ) x. ( arctan ` A ) ) = ( 2 x. ( _i x. ( arctan ` A ) ) ) )
9 halfcl 
 |-  ( _i e. CC -> ( _i / 2 ) e. CC )
10 5 9 ax-mp 
 |-  ( _i / 2 ) e. CC
11 3 5 10 mulassi 
 |-  ( ( 2 x. _i ) x. ( _i / 2 ) ) = ( 2 x. ( _i x. ( _i / 2 ) ) )
12 3 5 10 mul12i 
 |-  ( 2 x. ( _i x. ( _i / 2 ) ) ) = ( _i x. ( 2 x. ( _i / 2 ) ) )
13 2ne0 
 |-  2 =/= 0
14 5 3 13 divcan2i 
 |-  ( 2 x. ( _i / 2 ) ) = _i
15 14 oveq2i 
 |-  ( _i x. ( 2 x. ( _i / 2 ) ) ) = ( _i x. _i )
16 ixi 
 |-  ( _i x. _i ) = -u 1
17 15 16 eqtri 
 |-  ( _i x. ( 2 x. ( _i / 2 ) ) ) = -u 1
18 11 12 17 3eqtri 
 |-  ( ( 2 x. _i ) x. ( _i / 2 ) ) = -u 1
19 18 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 ) ) ) ) )
20 ax-1cn 
 |-  1 e. CC
21 atandm2 
 |-  ( A e. dom arctan <-> ( A e. CC /\ ( 1 - ( _i x. A ) ) =/= 0 /\ ( 1 + ( _i x. A ) ) =/= 0 ) )
22 21 simp1bi 
 |-  ( A e. dom arctan -> A e. CC )
23 mulcl 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC )
24 5 22 23 sylancr 
 |-  ( A e. dom arctan -> ( _i x. A ) e. CC )
25 subcl 
 |-  ( ( 1 e. CC /\ ( _i x. A ) e. CC ) -> ( 1 - ( _i x. A ) ) e. CC )
26 20 24 25 sylancr 
 |-  ( A e. dom arctan -> ( 1 - ( _i x. A ) ) e. CC )
27 21 simp2bi 
 |-  ( A e. dom arctan -> ( 1 - ( _i x. A ) ) =/= 0 )
28 26 27 logcld 
 |-  ( A e. dom arctan -> ( log ` ( 1 - ( _i x. A ) ) ) e. CC )
29 addcl 
 |-  ( ( 1 e. CC /\ ( _i x. A ) e. CC ) -> ( 1 + ( _i x. A ) ) e. CC )
30 20 24 29 sylancr 
 |-  ( A e. dom arctan -> ( 1 + ( _i x. A ) ) e. CC )
31 21 simp3bi 
 |-  ( A e. dom arctan -> ( 1 + ( _i x. A ) ) =/= 0 )
32 30 31 logcld 
 |-  ( A e. dom arctan -> ( log ` ( 1 + ( _i x. A ) ) ) e. CC )
33 28 32 subcld 
 |-  ( A e. dom arctan -> ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) e. CC )
34 33 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 ) ) ) ) )
35 19 34 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 ) ) ) ) )
36 2mulicn 
 |-  ( 2 x. _i ) e. CC
37 36 a1i 
 |-  ( A e. dom arctan -> ( 2 x. _i ) e. CC )
38 10 a1i 
 |-  ( A e. dom arctan -> ( _i / 2 ) e. CC )
39 37 38 33 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 ) ) ) ) ) ) )
40 28 32 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 ) ) ) ) )
41 35 39 40 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 ) ) ) ) )
42 2 8 41 3eqtr3d 
 |-  ( A e. dom arctan -> ( 2 x. ( _i x. ( arctan ` A ) ) ) = ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) )
43 42 fveq2d 
 |-  ( A e. dom arctan -> ( exp ` ( 2 x. ( _i x. ( arctan ` A ) ) ) ) = ( exp ` ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) )
44 efsub 
 |-  ( ( ( 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 ) ) ) ) / ( exp ` ( log ` ( 1 - ( _i x. A ) ) ) ) ) )
45 32 28 44 syl2anc 
 |-  ( A e. dom arctan -> ( exp ` ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) = ( ( exp ` ( log ` ( 1 + ( _i x. A ) ) ) ) / ( exp ` ( log ` ( 1 - ( _i x. A ) ) ) ) ) )
46 eflog 
 |-  ( ( ( 1 + ( _i x. A ) ) e. CC /\ ( 1 + ( _i x. A ) ) =/= 0 ) -> ( exp ` ( log ` ( 1 + ( _i x. A ) ) ) ) = ( 1 + ( _i x. A ) ) )
47 30 31 46 syl2anc 
 |-  ( A e. dom arctan -> ( exp ` ( log ` ( 1 + ( _i x. A ) ) ) ) = ( 1 + ( _i x. A ) ) )
48 eflog 
 |-  ( ( ( 1 - ( _i x. A ) ) e. CC /\ ( 1 - ( _i x. A ) ) =/= 0 ) -> ( exp ` ( log ` ( 1 - ( _i x. A ) ) ) ) = ( 1 - ( _i x. A ) ) )
49 26 27 48 syl2anc 
 |-  ( A e. dom arctan -> ( exp ` ( log ` ( 1 - ( _i x. A ) ) ) ) = ( 1 - ( _i x. A ) ) )
50 47 49 oveq12d 
 |-  ( A e. dom arctan -> ( ( exp ` ( log ` ( 1 + ( _i x. A ) ) ) ) / ( exp ` ( log ` ( 1 - ( _i x. A ) ) ) ) ) = ( ( 1 + ( _i x. A ) ) / ( 1 - ( _i x. A ) ) ) )
51 negsub 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( _i + -u A ) = ( _i - A ) )
52 5 22 51 sylancr 
 |-  ( A e. dom arctan -> ( _i + -u A ) = ( _i - A ) )
53 6 mulid1d 
 |-  ( A e. dom arctan -> ( _i x. 1 ) = _i )
54 16 oveq1i 
 |-  ( ( _i x. _i ) x. A ) = ( -u 1 x. A )
55 6 6 22 mulassd 
 |-  ( A e. dom arctan -> ( ( _i x. _i ) x. A ) = ( _i x. ( _i x. A ) ) )
56 22 mulm1d 
 |-  ( A e. dom arctan -> ( -u 1 x. A ) = -u A )
57 54 55 56 3eqtr3a 
 |-  ( A e. dom arctan -> ( _i x. ( _i x. A ) ) = -u A )
58 53 57 oveq12d 
 |-  ( A e. dom arctan -> ( ( _i x. 1 ) + ( _i x. ( _i x. A ) ) ) = ( _i + -u A ) )
59 6 22 6 pnpcan2d 
 |-  ( A e. dom arctan -> ( ( _i + _i ) - ( A + _i ) ) = ( _i - A ) )
60 52 58 59 3eqtr4d 
 |-  ( A e. dom arctan -> ( ( _i x. 1 ) + ( _i x. ( _i x. A ) ) ) = ( ( _i + _i ) - ( A + _i ) ) )
61 20 a1i 
 |-  ( A e. dom arctan -> 1 e. CC )
62 6 61 24 adddid 
 |-  ( A e. dom arctan -> ( _i x. ( 1 + ( _i x. A ) ) ) = ( ( _i x. 1 ) + ( _i x. ( _i x. A ) ) ) )
63 6 2timesd 
 |-  ( A e. dom arctan -> ( 2 x. _i ) = ( _i + _i ) )
64 63 oveq1d 
 |-  ( A e. dom arctan -> ( ( 2 x. _i ) - ( A + _i ) ) = ( ( _i + _i ) - ( A + _i ) ) )
65 60 62 64 3eqtr4d 
 |-  ( A e. dom arctan -> ( _i x. ( 1 + ( _i x. A ) ) ) = ( ( 2 x. _i ) - ( A + _i ) ) )
66 6 61 24 subdid 
 |-  ( A e. dom arctan -> ( _i x. ( 1 - ( _i x. A ) ) ) = ( ( _i x. 1 ) - ( _i x. ( _i x. A ) ) ) )
67 53 57 oveq12d 
 |-  ( A e. dom arctan -> ( ( _i x. 1 ) - ( _i x. ( _i x. A ) ) ) = ( _i - -u A ) )
68 subneg 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( _i - -u A ) = ( _i + A ) )
69 5 22 68 sylancr 
 |-  ( A e. dom arctan -> ( _i - -u A ) = ( _i + A ) )
70 67 69 eqtrd 
 |-  ( A e. dom arctan -> ( ( _i x. 1 ) - ( _i x. ( _i x. A ) ) ) = ( _i + A ) )
71 addcom 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( _i + A ) = ( A + _i ) )
72 5 22 71 sylancr 
 |-  ( A e. dom arctan -> ( _i + A ) = ( A + _i ) )
73 66 70 72 3eqtrd 
 |-  ( A e. dom arctan -> ( _i x. ( 1 - ( _i x. A ) ) ) = ( A + _i ) )
74 65 73 oveq12d 
 |-  ( A e. dom arctan -> ( ( _i x. ( 1 + ( _i x. A ) ) ) / ( _i x. ( 1 - ( _i x. A ) ) ) ) = ( ( ( 2 x. _i ) - ( A + _i ) ) / ( A + _i ) ) )
75 ine0 
 |-  _i =/= 0
76 75 a1i 
 |-  ( A e. dom arctan -> _i =/= 0 )
77 30 26 6 27 76 divcan5d 
 |-  ( A e. dom arctan -> ( ( _i x. ( 1 + ( _i x. A ) ) ) / ( _i x. ( 1 - ( _i x. A ) ) ) ) = ( ( 1 + ( _i x. A ) ) / ( 1 - ( _i x. A ) ) ) )
78 addcl 
 |-  ( ( A e. CC /\ _i e. CC ) -> ( A + _i ) e. CC )
79 22 5 78 sylancl 
 |-  ( A e. dom arctan -> ( A + _i ) e. CC )
80 subneg 
 |-  ( ( A e. CC /\ _i e. CC ) -> ( A - -u _i ) = ( A + _i ) )
81 22 5 80 sylancl 
 |-  ( A e. dom arctan -> ( A - -u _i ) = ( A + _i ) )
82 atandm 
 |-  ( A e. dom arctan <-> ( A e. CC /\ A =/= -u _i /\ A =/= _i ) )
83 82 simp2bi 
 |-  ( A e. dom arctan -> A =/= -u _i )
84 negicn 
 |-  -u _i e. CC
85 subeq0 
 |-  ( ( A e. CC /\ -u _i e. CC ) -> ( ( A - -u _i ) = 0 <-> A = -u _i ) )
86 85 necon3bid 
 |-  ( ( A e. CC /\ -u _i e. CC ) -> ( ( A - -u _i ) =/= 0 <-> A =/= -u _i ) )
87 22 84 86 sylancl 
 |-  ( A e. dom arctan -> ( ( A - -u _i ) =/= 0 <-> A =/= -u _i ) )
88 83 87 mpbird 
 |-  ( A e. dom arctan -> ( A - -u _i ) =/= 0 )
89 81 88 eqnetrrd 
 |-  ( A e. dom arctan -> ( A + _i ) =/= 0 )
90 37 79 79 89 divsubdird 
 |-  ( A e. dom arctan -> ( ( ( 2 x. _i ) - ( A + _i ) ) / ( A + _i ) ) = ( ( ( 2 x. _i ) / ( A + _i ) ) - ( ( A + _i ) / ( A + _i ) ) ) )
91 74 77 90 3eqtr3d 
 |-  ( A e. dom arctan -> ( ( 1 + ( _i x. A ) ) / ( 1 - ( _i x. A ) ) ) = ( ( ( 2 x. _i ) / ( A + _i ) ) - ( ( A + _i ) / ( A + _i ) ) ) )
92 79 89 dividd 
 |-  ( A e. dom arctan -> ( ( A + _i ) / ( A + _i ) ) = 1 )
93 92 oveq2d 
 |-  ( A e. dom arctan -> ( ( ( 2 x. _i ) / ( A + _i ) ) - ( ( A + _i ) / ( A + _i ) ) ) = ( ( ( 2 x. _i ) / ( A + _i ) ) - 1 ) )
94 50 91 93 3eqtrd 
 |-  ( A e. dom arctan -> ( ( exp ` ( log ` ( 1 + ( _i x. A ) ) ) ) / ( exp ` ( log ` ( 1 - ( _i x. A ) ) ) ) ) = ( ( ( 2 x. _i ) / ( A + _i ) ) - 1 ) )
95 43 45 94 3eqtrd 
 |-  ( A e. dom arctan -> ( exp ` ( 2 x. ( _i x. ( arctan ` A ) ) ) ) = ( ( ( 2 x. _i ) / ( A + _i ) ) - 1 ) )