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

Metamath Proof Explorer

Theorem asinsin

Description: The arcsine function composed with sin is equal to the identity. This plus sinasin allow to view sin and arcsin as inverse operations to each other. For ease of use, we have not defined precisely the correct domain of correctness of this identity; in addition to the main region described here it is also true forsome points on the branch cuts, namely when A = (pi / 2 ) - i y for nonnegative real y and also symmetrically at A =i y - ( pi / 2 ) . In particular, when restricted to reals this identity extends to the closed interval [ -u (pi / 2 ) , ( pi / 2 ) ] , not just the open interval (see reasinsin ). (Contributed by Mario Carneiro, 2-Apr-2015)

Ref Expression
Assertion asinsin 
|- ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( arcsin ` ( sin ` A ) ) = A )

Proof

Step Hyp Ref Expression
1 sincl 
 |-  ( A e. CC -> ( sin ` A ) e. CC )
2 1 adantr 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( sin ` A ) e. CC )
3 asinval 
 |-  ( ( sin ` A ) e. CC -> ( arcsin ` ( sin ` A ) ) = ( -u _i x. ( log ` ( ( _i x. ( sin ` A ) ) + ( sqrt ` ( 1 - ( ( sin ` A ) ^ 2 ) ) ) ) ) ) )
4 2 3 syl 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( arcsin ` ( sin ` A ) ) = ( -u _i x. ( log ` ( ( _i x. ( sin ` A ) ) + ( sqrt ` ( 1 - ( ( sin ` A ) ^ 2 ) ) ) ) ) ) )
5 ax-icn 
 |-  _i e. CC
6 mulcl 
 |-  ( ( _i e. CC /\ ( sin ` A ) e. CC ) -> ( _i x. ( sin ` A ) ) e. CC )
7 5 2 6 sylancr 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( _i x. ( sin ` A ) ) e. CC )
8 simpl 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> A e. CC )
9 mulcl 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC )
10 5 8 9 sylancr 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( _i x. A ) e. CC )
11 efcl 
 |-  ( ( _i x. A ) e. CC -> ( exp ` ( _i x. A ) ) e. CC )
12 10 11 syl 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( exp ` ( _i x. A ) ) e. CC )
13 7 12 pncan3d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( _i x. ( sin ` A ) ) + ( ( exp ` ( _i x. A ) ) - ( _i x. ( sin ` A ) ) ) ) = ( exp ` ( _i x. A ) ) )
14 12 7 subcld 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( exp ` ( _i x. A ) ) - ( _i x. ( sin ` A ) ) ) e. CC )
15 ax-1cn 
 |-  1 e. CC
16 2 sqcld 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( sin ` A ) ^ 2 ) e. CC )
17 subcl 
 |-  ( ( 1 e. CC /\ ( ( sin ` A ) ^ 2 ) e. CC ) -> ( 1 - ( ( sin ` A ) ^ 2 ) ) e. CC )
18 15 16 17 sylancr 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( 1 - ( ( sin ` A ) ^ 2 ) ) e. CC )
19 binom2sub 
 |-  ( ( ( exp ` ( _i x. A ) ) e. CC /\ ( _i x. ( sin ` A ) ) e. CC ) -> ( ( ( exp ` ( _i x. A ) ) - ( _i x. ( sin ` A ) ) ) ^ 2 ) = ( ( ( ( exp ` ( _i x. A ) ) ^ 2 ) - ( 2 x. ( ( exp ` ( _i x. A ) ) x. ( _i x. ( sin ` A ) ) ) ) ) + ( ( _i x. ( sin ` A ) ) ^ 2 ) ) )
20 12 7 19 syl2anc 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( ( exp ` ( _i x. A ) ) - ( _i x. ( sin ` A ) ) ) ^ 2 ) = ( ( ( ( exp ` ( _i x. A ) ) ^ 2 ) - ( 2 x. ( ( exp ` ( _i x. A ) ) x. ( _i x. ( sin ` A ) ) ) ) ) + ( ( _i x. ( sin ` A ) ) ^ 2 ) ) )
21 12 sqvald 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( exp ` ( _i x. A ) ) ^ 2 ) = ( ( exp ` ( _i x. A ) ) x. ( exp ` ( _i x. A ) ) ) )
22 2cn 
 |-  2 e. CC
23 22 a1i 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> 2 e. CC )
24 23 12 7 mul12d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( 2 x. ( ( exp ` ( _i x. A ) ) x. ( _i x. ( sin ` A ) ) ) ) = ( ( exp ` ( _i x. A ) ) x. ( 2 x. ( _i x. ( sin ` A ) ) ) ) )
25 21 24 oveq12d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( ( exp ` ( _i x. A ) ) ^ 2 ) - ( 2 x. ( ( exp ` ( _i x. A ) ) x. ( _i x. ( sin ` A ) ) ) ) ) = ( ( ( exp ` ( _i x. A ) ) x. ( exp ` ( _i x. A ) ) ) - ( ( exp ` ( _i x. A ) ) x. ( 2 x. ( _i x. ( sin ` A ) ) ) ) ) )
26 coscl 
 |-  ( A e. CC -> ( cos ` A ) e. CC )
27 26 adantr 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( cos ` A ) e. CC )
28 subsq 
 |-  ( ( ( cos ` A ) e. CC /\ ( _i x. ( sin ` A ) ) e. CC ) -> ( ( ( cos ` A ) ^ 2 ) - ( ( _i x. ( sin ` A ) ) ^ 2 ) ) = ( ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) x. ( ( cos ` A ) - ( _i x. ( sin ` A ) ) ) ) )
29 27 7 28 syl2anc 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( ( cos ` A ) ^ 2 ) - ( ( _i x. ( sin ` A ) ) ^ 2 ) ) = ( ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) x. ( ( cos ` A ) - ( _i x. ( sin ` A ) ) ) ) )
30 sqmul 
 |-  ( ( _i e. CC /\ ( sin ` A ) e. CC ) -> ( ( _i x. ( sin ` A ) ) ^ 2 ) = ( ( _i ^ 2 ) x. ( ( sin ` A ) ^ 2 ) ) )
31 5 2 30 sylancr 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( _i x. ( sin ` A ) ) ^ 2 ) = ( ( _i ^ 2 ) x. ( ( sin ` A ) ^ 2 ) ) )
32 i2 
 |-  ( _i ^ 2 ) = -u 1
33 32 oveq1i 
 |-  ( ( _i ^ 2 ) x. ( ( sin ` A ) ^ 2 ) ) = ( -u 1 x. ( ( sin ` A ) ^ 2 ) )
34 16 mulm1d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( -u 1 x. ( ( sin ` A ) ^ 2 ) ) = -u ( ( sin ` A ) ^ 2 ) )
35 33 34 eqtrid 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( _i ^ 2 ) x. ( ( sin ` A ) ^ 2 ) ) = -u ( ( sin ` A ) ^ 2 ) )
36 31 35 eqtrd 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( _i x. ( sin ` A ) ) ^ 2 ) = -u ( ( sin ` A ) ^ 2 ) )
37 36 oveq2d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( ( cos ` A ) ^ 2 ) - ( ( _i x. ( sin ` A ) ) ^ 2 ) ) = ( ( ( cos ` A ) ^ 2 ) - -u ( ( sin ` A ) ^ 2 ) ) )
38 27 sqcld 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( cos ` A ) ^ 2 ) e. CC )
39 38 16 subnegd 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( ( cos ` A ) ^ 2 ) - -u ( ( sin ` A ) ^ 2 ) ) = ( ( ( cos ` A ) ^ 2 ) + ( ( sin ` A ) ^ 2 ) ) )
40 38 16 addcomd 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( ( cos ` A ) ^ 2 ) + ( ( sin ` A ) ^ 2 ) ) = ( ( ( sin ` A ) ^ 2 ) + ( ( cos ` A ) ^ 2 ) ) )
41 37 39 40 3eqtrd 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( ( cos ` A ) ^ 2 ) - ( ( _i x. ( sin ` A ) ) ^ 2 ) ) = ( ( ( sin ` A ) ^ 2 ) + ( ( cos ` A ) ^ 2 ) ) )
42 efival 
 |-  ( A e. CC -> ( exp ` ( _i x. A ) ) = ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) )
43 42 adantr 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( exp ` ( _i x. A ) ) = ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) )
44 7 2timesd 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( 2 x. ( _i x. ( sin ` A ) ) ) = ( ( _i x. ( sin ` A ) ) + ( _i x. ( sin ` A ) ) ) )
45 43 44 oveq12d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( exp ` ( _i x. A ) ) - ( 2 x. ( _i x. ( sin ` A ) ) ) ) = ( ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) - ( ( _i x. ( sin ` A ) ) + ( _i x. ( sin ` A ) ) ) ) )
46 27 7 7 pnpcan2d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) - ( ( _i x. ( sin ` A ) ) + ( _i x. ( sin ` A ) ) ) ) = ( ( cos ` A ) - ( _i x. ( sin ` A ) ) ) )
47 45 46 eqtrd 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( exp ` ( _i x. A ) ) - ( 2 x. ( _i x. ( sin ` A ) ) ) ) = ( ( cos ` A ) - ( _i x. ( sin ` A ) ) ) )
48 43 47 oveq12d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( exp ` ( _i x. A ) ) x. ( ( exp ` ( _i x. A ) ) - ( 2 x. ( _i x. ( sin ` A ) ) ) ) ) = ( ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) x. ( ( cos ` A ) - ( _i x. ( sin ` A ) ) ) ) )
49 mulcl 
 |-  ( ( 2 e. CC /\ ( _i x. ( sin ` A ) ) e. CC ) -> ( 2 x. ( _i x. ( sin ` A ) ) ) e. CC )
50 22 7 49 sylancr 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( 2 x. ( _i x. ( sin ` A ) ) ) e. CC )
51 12 12 50 subdid 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( exp ` ( _i x. A ) ) x. ( ( exp ` ( _i x. A ) ) - ( 2 x. ( _i x. ( sin ` A ) ) ) ) ) = ( ( ( exp ` ( _i x. A ) ) x. ( exp ` ( _i x. A ) ) ) - ( ( exp ` ( _i x. A ) ) x. ( 2 x. ( _i x. ( sin ` A ) ) ) ) ) )
52 48 51 eqtr3d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) x. ( ( cos ` A ) - ( _i x. ( sin ` A ) ) ) ) = ( ( ( exp ` ( _i x. A ) ) x. ( exp ` ( _i x. A ) ) ) - ( ( exp ` ( _i x. A ) ) x. ( 2 x. ( _i x. ( sin ` A ) ) ) ) ) )
53 29 41 52 3eqtr3d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( ( sin ` A ) ^ 2 ) + ( ( cos ` A ) ^ 2 ) ) = ( ( ( exp ` ( _i x. A ) ) x. ( exp ` ( _i x. A ) ) ) - ( ( exp ` ( _i x. A ) ) x. ( 2 x. ( _i x. ( sin ` A ) ) ) ) ) )
54 sincossq 
 |-  ( A e. CC -> ( ( ( sin ` A ) ^ 2 ) + ( ( cos ` A ) ^ 2 ) ) = 1 )
55 54 adantr 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( ( sin ` A ) ^ 2 ) + ( ( cos ` A ) ^ 2 ) ) = 1 )
56 25 53 55 3eqtr2d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( ( exp ` ( _i x. A ) ) ^ 2 ) - ( 2 x. ( ( exp ` ( _i x. A ) ) x. ( _i x. ( sin ` A ) ) ) ) ) = 1 )
57 56 36 oveq12d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( ( ( exp ` ( _i x. A ) ) ^ 2 ) - ( 2 x. ( ( exp ` ( _i x. A ) ) x. ( _i x. ( sin ` A ) ) ) ) ) + ( ( _i x. ( sin ` A ) ) ^ 2 ) ) = ( 1 + -u ( ( sin ` A ) ^ 2 ) ) )
58 negsub 
 |-  ( ( 1 e. CC /\ ( ( sin ` A ) ^ 2 ) e. CC ) -> ( 1 + -u ( ( sin ` A ) ^ 2 ) ) = ( 1 - ( ( sin ` A ) ^ 2 ) ) )
59 15 16 58 sylancr 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( 1 + -u ( ( sin ` A ) ^ 2 ) ) = ( 1 - ( ( sin ` A ) ^ 2 ) ) )
60 20 57 59 3eqtrd 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( ( exp ` ( _i x. A ) ) - ( _i x. ( sin ` A ) ) ) ^ 2 ) = ( 1 - ( ( sin ` A ) ^ 2 ) ) )
61 halfre 
 |-  ( 1 / 2 ) e. RR
62 61 a1i 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( 1 / 2 ) e. RR )
63 negicn 
 |-  -u _i e. CC
64 mulcl 
 |-  ( ( -u _i e. CC /\ A e. CC ) -> ( -u _i x. A ) e. CC )
65 63 8 64 sylancr 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( -u _i x. A ) e. CC )
66 efcl 
 |-  ( ( -u _i x. A ) e. CC -> ( exp ` ( -u _i x. A ) ) e. CC )
67 65 66 syl 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( exp ` ( -u _i x. A ) ) e. CC )
68 12 67 addcld 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) e. CC )
69 68 recld 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( Re ` ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) ) e. RR )
70 halfgt0 
 |-  0 < ( 1 / 2 )
71 70 a1i 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> 0 < ( 1 / 2 ) )
72 12 recld 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( Re ` ( exp ` ( _i x. A ) ) ) e. RR )
73 67 recld 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( Re ` ( exp ` ( -u _i x. A ) ) ) e. RR )
74 asinsinlem 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> 0 < ( Re ` ( exp ` ( _i x. A ) ) ) )
75 negcl 
 |-  ( A e. CC -> -u A e. CC )
76 75 adantr 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> -u A e. CC )
77 reneg 
 |-  ( A e. CC -> ( Re ` -u A ) = -u ( Re ` A ) )
78 77 adantr 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( Re ` -u A ) = -u ( Re ` A ) )
79 halfpire 
 |-  ( _pi / 2 ) e. RR
80 79 renegcli 
 |-  -u ( _pi / 2 ) e. RR
81 recl 
 |-  ( A e. CC -> ( Re ` A ) e. RR )
82 iooneg 
 |-  ( ( -u ( _pi / 2 ) e. RR /\ ( _pi / 2 ) e. RR /\ ( Re ` A ) e. RR ) -> ( ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) <-> -u ( Re ` A ) e. ( -u ( _pi / 2 ) (,) -u -u ( _pi / 2 ) ) ) )
83 80 79 81 82 mp3an12i 
 |-  ( A e. CC -> ( ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) <-> -u ( Re ` A ) e. ( -u ( _pi / 2 ) (,) -u -u ( _pi / 2 ) ) ) )
84 83 biimpa 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> -u ( Re ` A ) e. ( -u ( _pi / 2 ) (,) -u -u ( _pi / 2 ) ) )
85 79 recni 
 |-  ( _pi / 2 ) e. CC
86 85 negnegi 
 |-  -u -u ( _pi / 2 ) = ( _pi / 2 )
87 86 oveq2i 
 |-  ( -u ( _pi / 2 ) (,) -u -u ( _pi / 2 ) ) = ( -u ( _pi / 2 ) (,) ( _pi / 2 ) )
88 84 87 eleqtrdi 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> -u ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) )
89 78 88 eqeltrd 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( Re ` -u A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) )
90 asinsinlem 
 |-  ( ( -u A e. CC /\ ( Re ` -u A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> 0 < ( Re ` ( exp ` ( _i x. -u A ) ) ) )
91 76 89 90 syl2anc 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> 0 < ( Re ` ( exp ` ( _i x. -u A ) ) ) )
92 mulneg12 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( -u _i x. A ) = ( _i x. -u A ) )
93 5 8 92 sylancr 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( -u _i x. A ) = ( _i x. -u A ) )
94 93 fveq2d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( exp ` ( -u _i x. A ) ) = ( exp ` ( _i x. -u A ) ) )
95 94 fveq2d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( Re ` ( exp ` ( -u _i x. A ) ) ) = ( Re ` ( exp ` ( _i x. -u A ) ) ) )
96 91 95 breqtrrd 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> 0 < ( Re ` ( exp ` ( -u _i x. A ) ) ) )
97 72 73 74 96 addgt0d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> 0 < ( ( Re ` ( exp ` ( _i x. A ) ) ) + ( Re ` ( exp ` ( -u _i x. A ) ) ) ) )
98 12 67 readdd 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( Re ` ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) ) = ( ( Re ` ( exp ` ( _i x. A ) ) ) + ( Re ` ( exp ` ( -u _i x. A ) ) ) ) )
99 97 98 breqtrrd 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> 0 < ( Re ` ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) ) )
100 62 69 71 99 mulgt0d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> 0 < ( ( 1 / 2 ) x. ( Re ` ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) ) ) )
101 cosval 
 |-  ( A e. CC -> ( cos ` A ) = ( ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) / 2 ) )
102 101 adantr 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( cos ` A ) = ( ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) / 2 ) )
103 2ne0 
 |-  2 =/= 0
104 103 a1i 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> 2 =/= 0 )
105 68 23 104 divrec2d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) / 2 ) = ( ( 1 / 2 ) x. ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) ) )
106 102 105 eqtrd 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( cos ` A ) = ( ( 1 / 2 ) x. ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) ) )
107 106 fveq2d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( Re ` ( cos ` A ) ) = ( Re ` ( ( 1 / 2 ) x. ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) ) ) )
108 remul2 
 |-  ( ( ( 1 / 2 ) e. RR /\ ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) e. CC ) -> ( Re ` ( ( 1 / 2 ) x. ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) ) ) = ( ( 1 / 2 ) x. ( Re ` ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) ) ) )
109 61 68 108 sylancr 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( Re ` ( ( 1 / 2 ) x. ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) ) ) = ( ( 1 / 2 ) x. ( Re ` ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) ) ) )
110 107 109 eqtrd 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( Re ` ( cos ` A ) ) = ( ( 1 / 2 ) x. ( Re ` ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) ) ) )
111 100 110 breqtrrd 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> 0 < ( Re ` ( cos ` A ) ) )
112 27 7 43 mvrraddd 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( exp ` ( _i x. A ) ) - ( _i x. ( sin ` A ) ) ) = ( cos ` A ) )
113 112 fveq2d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( Re ` ( ( exp ` ( _i x. A ) ) - ( _i x. ( sin ` A ) ) ) ) = ( Re ` ( cos ` A ) ) )
114 111 113 breqtrrd 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> 0 < ( Re ` ( ( exp ` ( _i x. A ) ) - ( _i x. ( sin ` A ) ) ) ) )
115 14 18 60 114 eqsqrt2d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( exp ` ( _i x. A ) ) - ( _i x. ( sin ` A ) ) ) = ( sqrt ` ( 1 - ( ( sin ` A ) ^ 2 ) ) ) )
116 115 oveq2d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( _i x. ( sin ` A ) ) + ( ( exp ` ( _i x. A ) ) - ( _i x. ( sin ` A ) ) ) ) = ( ( _i x. ( sin ` A ) ) + ( sqrt ` ( 1 - ( ( sin ` A ) ^ 2 ) ) ) ) )
117 13 116 eqtr3d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( exp ` ( _i x. A ) ) = ( ( _i x. ( sin ` A ) ) + ( sqrt ` ( 1 - ( ( sin ` A ) ^ 2 ) ) ) ) )
118 117 fveq2d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( log ` ( exp ` ( _i x. A ) ) ) = ( log ` ( ( _i x. ( sin ` A ) ) + ( sqrt ` ( 1 - ( ( sin ` A ) ^ 2 ) ) ) ) ) )
119 pire 
 |-  _pi e. RR
120 119 renegcli 
 |-  -u _pi e. RR
121 120 a1i 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> -u _pi e. RR )
122 80 a1i 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> -u ( _pi / 2 ) e. RR )
123 elioore 
 |-  ( ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> ( Re ` A ) e. RR )
124 123 adantl 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( Re ` A ) e. RR )
125 pirp 
 |-  _pi e. RR+
126 rphalflt 
 |-  ( _pi e. RR+ -> ( _pi / 2 ) < _pi )
127 125 126 ax-mp 
 |-  ( _pi / 2 ) < _pi
128 79 119 ltnegi 
 |-  ( ( _pi / 2 ) < _pi <-> -u _pi < -u ( _pi / 2 ) )
129 127 128 mpbi 
 |-  -u _pi < -u ( _pi / 2 )
130 129 a1i 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> -u _pi < -u ( _pi / 2 ) )
131 eliooord 
 |-  ( ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> ( -u ( _pi / 2 ) < ( Re ` A ) /\ ( Re ` A ) < ( _pi / 2 ) ) )
132 131 adantl 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( -u ( _pi / 2 ) < ( Re ` A ) /\ ( Re ` A ) < ( _pi / 2 ) ) )
133 132 simpld 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> -u ( _pi / 2 ) < ( Re ` A ) )
134 121 122 124 130 133 lttrd 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> -u _pi < ( Re ` A ) )
135 imre 
 |-  ( ( _i x. A ) e. CC -> ( Im ` ( _i x. A ) ) = ( Re ` ( -u _i x. ( _i x. A ) ) ) )
136 10 135 syl 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( Im ` ( _i x. A ) ) = ( Re ` ( -u _i x. ( _i x. A ) ) ) )
137 5 5 mulneg1i 
 |-  ( -u _i x. _i ) = -u ( _i x. _i )
138 ixi 
 |-  ( _i x. _i ) = -u 1
139 138 negeqi 
 |-  -u ( _i x. _i ) = -u -u 1
140 15 negnegi 
 |-  -u -u 1 = 1
141 137 139 140 3eqtri 
 |-  ( -u _i x. _i ) = 1
142 141 oveq1i 
 |-  ( ( -u _i x. _i ) x. A ) = ( 1 x. A )
143 63 a1i 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> -u _i e. CC )
144 5 a1i 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> _i e. CC )
145 143 144 8 mulassd 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( -u _i x. _i ) x. A ) = ( -u _i x. ( _i x. A ) ) )
146 mullid 
 |-  ( A e. CC -> ( 1 x. A ) = A )
147 146 adantr 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( 1 x. A ) = A )
148 142 145 147 3eqtr3a 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( -u _i x. ( _i x. A ) ) = A )
149 148 fveq2d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( Re ` ( -u _i x. ( _i x. A ) ) ) = ( Re ` A ) )
150 136 149 eqtrd 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( Im ` ( _i x. A ) ) = ( Re ` A ) )
151 134 150 breqtrrd 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> -u _pi < ( Im ` ( _i x. A ) ) )
152 119 a1i 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> _pi e. RR )
153 79 a1i 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( _pi / 2 ) e. RR )
154 132 simprd 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( Re ` A ) < ( _pi / 2 ) )
155 127 a1i 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( _pi / 2 ) < _pi )
156 124 153 152 154 155 lttrd 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( Re ` A ) < _pi )
157 124 152 156 ltled 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( Re ` A ) <_ _pi )
158 150 157 eqbrtrd 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( Im ` ( _i x. A ) ) <_ _pi )
159 ellogrn 
 |-  ( ( _i x. A ) e. ran log <-> ( ( _i x. A ) e. CC /\ -u _pi < ( Im ` ( _i x. A ) ) /\ ( Im ` ( _i x. A ) ) <_ _pi ) )
160 10 151 158 159 syl3anbrc 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( _i x. A ) e. ran log )
161 logef 
 |-  ( ( _i x. A ) e. ran log -> ( log ` ( exp ` ( _i x. A ) ) ) = ( _i x. A ) )
162 160 161 syl 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( log ` ( exp ` ( _i x. A ) ) ) = ( _i x. A ) )
163 118 162 eqtr3d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( log ` ( ( _i x. ( sin ` A ) ) + ( sqrt ` ( 1 - ( ( sin ` A ) ^ 2 ) ) ) ) ) = ( _i x. A ) )
164 163 oveq2d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( -u _i x. ( log ` ( ( _i x. ( sin ` A ) ) + ( sqrt ` ( 1 - ( ( sin ` A ) ^ 2 ) ) ) ) ) ) = ( -u _i x. ( _i x. A ) ) )
165 4 164 148 3eqtrd 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( arcsin ` ( sin ` A ) ) = A )