Metamath Proof Explorer

Theorem efiatan

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

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

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 -> ( _i x. ( arctan ` A ) ) = ( _i x. ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) ) )
3 ax-icn 
 |-  _i e. CC
4 3 a1i 
 |-  ( A e. dom arctan -> _i e. CC )
5 halfcl 
 |-  ( _i e. CC -> ( _i / 2 ) e. CC )
6 3 5 mp1i 
 |-  ( A e. dom arctan -> ( _i / 2 ) 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 mulcl 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC )
11 3 9 10 sylancr 
 |-  ( A e. dom arctan -> ( _i x. A ) e. CC )
12 subcl 
 |-  ( ( 1 e. CC /\ ( _i x. A ) e. CC ) -> ( 1 - ( _i x. A ) ) e. CC )
13 7 11 12 sylancr 
 |-  ( A e. dom arctan -> ( 1 - ( _i x. A ) ) e. CC )
14 8 simp2bi 
 |-  ( A e. dom arctan -> ( 1 - ( _i x. A ) ) =/= 0 )
15 13 14 logcld 
 |-  ( A e. dom arctan -> ( log ` ( 1 - ( _i x. A ) ) ) e. CC )
16 addcl 
 |-  ( ( 1 e. CC /\ ( _i x. A ) e. CC ) -> ( 1 + ( _i x. A ) ) e. CC )
17 7 11 16 sylancr 
 |-  ( A e. dom arctan -> ( 1 + ( _i x. A ) ) e. CC )
18 8 simp3bi 
 |-  ( A e. dom arctan -> ( 1 + ( _i x. A ) ) =/= 0 )
19 17 18 logcld 
 |-  ( A e. dom arctan -> ( log ` ( 1 + ( _i x. A ) ) ) e. CC )
20 15 19 subcld 
 |-  ( A e. dom arctan -> ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) e. CC )
21 4 6 20 mulassd 
 |-  ( A e. dom arctan -> ( ( _i x. ( _i / 2 ) ) x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) = ( _i x. ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) ) )
22 2cn 
 |-  2 e. CC
23 2ne0 
 |-  2 =/= 0
24 divneg 
 |-  ( ( 1 e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> -u ( 1 / 2 ) = ( -u 1 / 2 ) )
25 7 22 23 24 mp3an 
 |-  -u ( 1 / 2 ) = ( -u 1 / 2 )
26 ixi 
 |-  ( _i x. _i ) = -u 1
27 26 oveq1i 
 |-  ( ( _i x. _i ) / 2 ) = ( -u 1 / 2 )
28 3 3 22 23 divassi 
 |-  ( ( _i x. _i ) / 2 ) = ( _i x. ( _i / 2 ) )
29 25 27 28 3eqtr2i 
 |-  -u ( 1 / 2 ) = ( _i x. ( _i / 2 ) )
30 29 oveq1i 
 |-  ( -u ( 1 / 2 ) x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) = ( ( _i x. ( _i / 2 ) ) x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) )
31 halfcn 
 |-  ( 1 / 2 ) e. CC
32 mulneg12 
 |-  ( ( ( 1 / 2 ) e. CC /\ ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) e. CC ) -> ( -u ( 1 / 2 ) x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) = ( ( 1 / 2 ) x. -u ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) )
33 31 20 32 sylancr 
 |-  ( A e. dom arctan -> ( -u ( 1 / 2 ) x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) = ( ( 1 / 2 ) x. -u ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) )
34 15 19 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 ) ) ) ) )
35 34 oveq2d 
 |-  ( A e. dom arctan -> ( ( 1 / 2 ) x. -u ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) = ( ( 1 / 2 ) x. ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) )
36 31 a1i 
 |-  ( A e. dom arctan -> ( 1 / 2 ) e. CC )
37 36 19 15 subdid 
 |-  ( A e. dom arctan -> ( ( 1 / 2 ) x. ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) = ( ( ( 1 / 2 ) x. ( log ` ( 1 + ( _i x. A ) ) ) ) - ( ( 1 / 2 ) x. ( log ` ( 1 - ( _i x. A ) ) ) ) ) )
38 33 35 37 3eqtrd 
 |-  ( A e. dom arctan -> ( -u ( 1 / 2 ) x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) = ( ( ( 1 / 2 ) x. ( log ` ( 1 + ( _i x. A ) ) ) ) - ( ( 1 / 2 ) x. ( log ` ( 1 - ( _i x. A ) ) ) ) ) )
39 30 38 eqtr3id 
 |-  ( A e. dom arctan -> ( ( _i x. ( _i / 2 ) ) x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) = ( ( ( 1 / 2 ) x. ( log ` ( 1 + ( _i x. A ) ) ) ) - ( ( 1 / 2 ) x. ( log ` ( 1 - ( _i x. A ) ) ) ) ) )
40 2 21 39 3eqtr2d 
 |-  ( A e. dom arctan -> ( _i x. ( arctan ` A ) ) = ( ( ( 1 / 2 ) x. ( log ` ( 1 + ( _i x. A ) ) ) ) - ( ( 1 / 2 ) x. ( log ` ( 1 - ( _i x. A ) ) ) ) ) )
41 40 fveq2d 
 |-  ( A e. dom arctan -> ( exp ` ( _i x. ( arctan ` A ) ) ) = ( exp ` ( ( ( 1 / 2 ) x. ( log ` ( 1 + ( _i x. A ) ) ) ) - ( ( 1 / 2 ) x. ( log ` ( 1 - ( _i x. A ) ) ) ) ) ) )
42 mulcl 
 |-  ( ( ( 1 / 2 ) e. CC /\ ( log ` ( 1 + ( _i x. A ) ) ) e. CC ) -> ( ( 1 / 2 ) x. ( log ` ( 1 + ( _i x. A ) ) ) ) e. CC )
43 31 19 42 sylancr 
 |-  ( A e. dom arctan -> ( ( 1 / 2 ) x. ( log ` ( 1 + ( _i x. A ) ) ) ) e. CC )
44 mulcl 
 |-  ( ( ( 1 / 2 ) e. CC /\ ( log ` ( 1 - ( _i x. A ) ) ) e. CC ) -> ( ( 1 / 2 ) x. ( log ` ( 1 - ( _i x. A ) ) ) ) e. CC )
45 31 15 44 sylancr 
 |-  ( A e. dom arctan -> ( ( 1 / 2 ) x. ( log ` ( 1 - ( _i x. A ) ) ) ) e. CC )
46 efsub 
 |-  ( ( ( ( 1 / 2 ) x. ( log ` ( 1 + ( _i x. A ) ) ) ) e. CC /\ ( ( 1 / 2 ) x. ( log ` ( 1 - ( _i x. A ) ) ) ) e. CC ) -> ( exp ` ( ( ( 1 / 2 ) x. ( log ` ( 1 + ( _i x. A ) ) ) ) - ( ( 1 / 2 ) x. ( log ` ( 1 - ( _i x. A ) ) ) ) ) ) = ( ( exp ` ( ( 1 / 2 ) x. ( log ` ( 1 + ( _i x. A ) ) ) ) ) / ( exp ` ( ( 1 / 2 ) x. ( log ` ( 1 - ( _i x. A ) ) ) ) ) ) )
47 43 45 46 syl2anc 
 |-  ( A e. dom arctan -> ( exp ` ( ( ( 1 / 2 ) x. ( log ` ( 1 + ( _i x. A ) ) ) ) - ( ( 1 / 2 ) x. ( log ` ( 1 - ( _i x. A ) ) ) ) ) ) = ( ( exp ` ( ( 1 / 2 ) x. ( log ` ( 1 + ( _i x. A ) ) ) ) ) / ( exp ` ( ( 1 / 2 ) x. ( log ` ( 1 - ( _i x. A ) ) ) ) ) ) )
48 17 18 36 cxpefd 
 |-  ( A e. dom arctan -> ( ( 1 + ( _i x. A ) ) ^c ( 1 / 2 ) ) = ( exp ` ( ( 1 / 2 ) x. ( log ` ( 1 + ( _i x. A ) ) ) ) ) )
49 cxpsqrt 
 |-  ( ( 1 + ( _i x. A ) ) e. CC -> ( ( 1 + ( _i x. A ) ) ^c ( 1 / 2 ) ) = ( sqrt ` ( 1 + ( _i x. A ) ) ) )
50 17 49 syl 
 |-  ( A e. dom arctan -> ( ( 1 + ( _i x. A ) ) ^c ( 1 / 2 ) ) = ( sqrt ` ( 1 + ( _i x. A ) ) ) )
51 48 50 eqtr3d 
 |-  ( A e. dom arctan -> ( exp ` ( ( 1 / 2 ) x. ( log ` ( 1 + ( _i x. A ) ) ) ) ) = ( sqrt ` ( 1 + ( _i x. A ) ) ) )
52 13 14 36 cxpefd 
 |-  ( A e. dom arctan -> ( ( 1 - ( _i x. A ) ) ^c ( 1 / 2 ) ) = ( exp ` ( ( 1 / 2 ) x. ( log ` ( 1 - ( _i x. A ) ) ) ) ) )
53 cxpsqrt 
 |-  ( ( 1 - ( _i x. A ) ) e. CC -> ( ( 1 - ( _i x. A ) ) ^c ( 1 / 2 ) ) = ( sqrt ` ( 1 - ( _i x. A ) ) ) )
54 13 53 syl 
 |-  ( A e. dom arctan -> ( ( 1 - ( _i x. A ) ) ^c ( 1 / 2 ) ) = ( sqrt ` ( 1 - ( _i x. A ) ) ) )
55 52 54 eqtr3d 
 |-  ( A e. dom arctan -> ( exp ` ( ( 1 / 2 ) x. ( log ` ( 1 - ( _i x. A ) ) ) ) ) = ( sqrt ` ( 1 - ( _i x. A ) ) ) )
56 51 55 oveq12d 
 |-  ( A e. dom arctan -> ( ( exp ` ( ( 1 / 2 ) x. ( log ` ( 1 + ( _i x. A ) ) ) ) ) / ( exp ` ( ( 1 / 2 ) x. ( log ` ( 1 - ( _i x. A ) ) ) ) ) ) = ( ( sqrt ` ( 1 + ( _i x. A ) ) ) / ( sqrt ` ( 1 - ( _i x. A ) ) ) ) )
57 41 47 56 3eqtrd 
 |-  ( A e. dom arctan -> ( exp ` ( _i x. ( arctan ` A ) ) ) = ( ( sqrt ` ( 1 + ( _i x. A ) ) ) / ( sqrt ` ( 1 - ( _i x. A ) ) ) ) )