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

Metamath Proof Explorer

Theorem asinneg

Description: The arcsine function is odd. (Contributed by Mario Carneiro, 1-Apr-2015)

Ref Expression
Assertion asinneg 
|- ( A e. CC -> ( arcsin ` -u A ) = -u ( arcsin ` A ) )

Proof

Step Hyp Ref Expression
1 ax-icn 
 |-  _i e. CC
2 mulcl 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC )
3 1 2 mpan 
 |-  ( A e. CC -> ( _i x. A ) e. CC )
4 ax-1cn 
 |-  1 e. CC
5 sqcl 
 |-  ( A e. CC -> ( A ^ 2 ) e. CC )
6 subcl 
 |-  ( ( 1 e. CC /\ ( A ^ 2 ) e. CC ) -> ( 1 - ( A ^ 2 ) ) e. CC )
7 4 5 6 sylancr 
 |-  ( A e. CC -> ( 1 - ( A ^ 2 ) ) e. CC )
8 7 sqrtcld 
 |-  ( A e. CC -> ( sqrt ` ( 1 - ( A ^ 2 ) ) ) e. CC )
9 3 8 addcld 
 |-  ( A e. CC -> ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) e. CC )
10 asinlem 
 |-  ( A e. CC -> ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) =/= 0 )
11 9 10 logcld 
 |-  ( A e. CC -> ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) e. CC )
12 efneg 
 |-  ( ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) e. CC -> ( exp ` -u ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) = ( 1 / ( exp ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) ) )
13 11 12 syl 
 |-  ( A e. CC -> ( exp ` -u ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) = ( 1 / ( exp ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) ) )
14 eflog 
 |-  ( ( ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) e. CC /\ ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) =/= 0 ) -> ( exp ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) = ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) )
15 9 10 14 syl2anc 
 |-  ( A e. CC -> ( exp ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) = ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) )
16 15 oveq2d 
 |-  ( A e. CC -> ( 1 / ( exp ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) ) = ( 1 / ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) )
17 asinlem2 
 |-  ( A e. CC -> ( ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) x. ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) = 1 )
18 4 a1i 
 |-  ( A e. CC -> 1 e. CC )
19 negcl 
 |-  ( A e. CC -> -u A e. CC )
20 mulcl 
 |-  ( ( _i e. CC /\ -u A e. CC ) -> ( _i x. -u A ) e. CC )
21 1 19 20 sylancr 
 |-  ( A e. CC -> ( _i x. -u A ) e. CC )
22 19 sqcld 
 |-  ( A e. CC -> ( -u A ^ 2 ) e. CC )
23 subcl 
 |-  ( ( 1 e. CC /\ ( -u A ^ 2 ) e. CC ) -> ( 1 - ( -u A ^ 2 ) ) e. CC )
24 4 22 23 sylancr 
 |-  ( A e. CC -> ( 1 - ( -u A ^ 2 ) ) e. CC )
25 24 sqrtcld 
 |-  ( A e. CC -> ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) e. CC )
26 21 25 addcld 
 |-  ( A e. CC -> ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) e. CC )
27 18 9 26 10 divmuld 
 |-  ( A e. CC -> ( ( 1 / ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) = ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) <-> ( ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) x. ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) = 1 ) )
28 17 27 mpbird 
 |-  ( A e. CC -> ( 1 / ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) = ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) )
29 13 16 28 3eqtrd 
 |-  ( A e. CC -> ( exp ` -u ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) = ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) )
30 asinlem 
 |-  ( -u A e. CC -> ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) =/= 0 )
31 19 30 syl 
 |-  ( A e. CC -> ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) =/= 0 )
32 11 negcld 
 |-  ( A e. CC -> -u ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) e. CC )
33 11 imnegd 
 |-  ( A e. CC -> ( Im ` -u ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) = -u ( Im ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) )
34 11 imcld 
 |-  ( A e. CC -> ( Im ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) e. RR )
35 34 renegcld 
 |-  ( A e. CC -> -u ( Im ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) e. RR )
36 pire 
 |-  _pi e. RR
37 36 a1i 
 |-  ( A e. CC -> _pi e. RR )
38 9 10 logimcld 
 |-  ( A e. CC -> ( -u _pi < ( Im ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) /\ ( Im ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) <_ _pi ) )
39 38 simprd 
 |-  ( A e. CC -> ( Im ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) <_ _pi )
40 9 renegd 
 |-  ( A e. CC -> ( Re ` -u ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) = -u ( Re ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) )
41 asinlem3 
 |-  ( A e. CC -> 0 <_ ( Re ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) )
42 9 recld 
 |-  ( A e. CC -> ( Re ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) e. RR )
43 42 le0neg2d 
 |-  ( A e. CC -> ( 0 <_ ( Re ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) <-> -u ( Re ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) <_ 0 ) )
44 41 43 mpbid 
 |-  ( A e. CC -> -u ( Re ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) <_ 0 )
45 40 44 eqbrtrd 
 |-  ( A e. CC -> ( Re ` -u ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) <_ 0 )
46 9 negcld 
 |-  ( A e. CC -> -u ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) e. CC )
47 46 recld 
 |-  ( A e. CC -> ( Re ` -u ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) e. RR )
48 0re 
 |-  0 e. RR
49 lenlt 
 |-  ( ( ( Re ` -u ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) e. RR /\ 0 e. RR ) -> ( ( Re ` -u ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) <_ 0 <-> -. 0 < ( Re ` -u ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) )
50 47 48 49 sylancl 
 |-  ( A e. CC -> ( ( Re ` -u ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) <_ 0 <-> -. 0 < ( Re ` -u ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) )
51 45 50 mpbid 
 |-  ( A e. CC -> -. 0 < ( Re ` -u ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) )
52 lognegb 
 |-  ( ( ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) e. CC /\ ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) =/= 0 ) -> ( -u ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) e. RR+ <-> ( Im ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) = _pi ) )
53 9 10 52 syl2anc 
 |-  ( A e. CC -> ( -u ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) e. RR+ <-> ( Im ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) = _pi ) )
54 rpgt0 
 |-  ( -u ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) e. RR+ -> 0 < -u ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) )
55 rpre 
 |-  ( -u ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) e. RR+ -> -u ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) e. RR )
56 55 rered 
 |-  ( -u ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) e. RR+ -> ( Re ` -u ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) = -u ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) )
57 54 56 breqtrrd 
 |-  ( -u ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) e. RR+ -> 0 < ( Re ` -u ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) )
58 53 57 biimtrrdi 
 |-  ( A e. CC -> ( ( Im ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) = _pi -> 0 < ( Re ` -u ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) )
59 58 necon3bd 
 |-  ( A e. CC -> ( -. 0 < ( Re ` -u ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) -> ( Im ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) =/= _pi ) )
60 51 59 mpd 
 |-  ( A e. CC -> ( Im ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) =/= _pi )
61 60 necomd 
 |-  ( A e. CC -> _pi =/= ( Im ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) )
62 34 37 39 61 leneltd 
 |-  ( A e. CC -> ( Im ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) < _pi )
63 ltneg 
 |-  ( ( ( Im ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) e. RR /\ _pi e. RR ) -> ( ( Im ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) < _pi <-> -u _pi < -u ( Im ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) ) )
64 34 36 63 sylancl 
 |-  ( A e. CC -> ( ( Im ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) < _pi <-> -u _pi < -u ( Im ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) ) )
65 62 64 mpbid 
 |-  ( A e. CC -> -u _pi < -u ( Im ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) )
66 38 simpld 
 |-  ( A e. CC -> -u _pi < ( Im ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) )
67 36 renegcli 
 |-  -u _pi e. RR
68 ltle 
 |-  ( ( -u _pi e. RR /\ ( Im ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) e. RR ) -> ( -u _pi < ( Im ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) -> -u _pi <_ ( Im ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) ) )
69 67 34 68 sylancr 
 |-  ( A e. CC -> ( -u _pi < ( Im ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) -> -u _pi <_ ( Im ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) ) )
70 66 69 mpd 
 |-  ( A e. CC -> -u _pi <_ ( Im ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) )
71 lenegcon1 
 |-  ( ( _pi e. RR /\ ( Im ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) e. RR ) -> ( -u _pi <_ ( Im ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) <-> -u ( Im ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) <_ _pi ) )
72 36 34 71 sylancr 
 |-  ( A e. CC -> ( -u _pi <_ ( Im ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) <-> -u ( Im ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) <_ _pi ) )
73 70 72 mpbid 
 |-  ( A e. CC -> -u ( Im ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) <_ _pi )
74 67 rexri 
 |-  -u _pi e. RR*
75 elioc2 
 |-  ( ( -u _pi e. RR* /\ _pi e. RR ) -> ( -u ( Im ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) e. ( -u _pi (,] _pi ) <-> ( -u ( Im ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) e. RR /\ -u _pi < -u ( Im ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) /\ -u ( Im ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) <_ _pi ) ) )
76 74 36 75 mp2an 
 |-  ( -u ( Im ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) e. ( -u _pi (,] _pi ) <-> ( -u ( Im ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) e. RR /\ -u _pi < -u ( Im ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) /\ -u ( Im ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) <_ _pi ) )
77 35 65 73 76 syl3anbrc 
 |-  ( A e. CC -> -u ( Im ` ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) e. ( -u _pi (,] _pi ) )
78 33 77 eqeltrd 
 |-  ( A e. CC -> ( Im ` -u ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) e. ( -u _pi (,] _pi ) )
79 imf 
 |-  Im : CC --> RR
80 ffn 
 |-  ( Im : CC --> RR -> Im Fn CC )
81 elpreima 
 |-  ( Im Fn CC -> ( -u ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) e. ( `' Im " ( -u _pi (,] _pi ) ) <-> ( -u ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) e. CC /\ ( Im ` -u ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) e. ( -u _pi (,] _pi ) ) ) )
82 79 80 81 mp2b 
 |-  ( -u ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) e. ( `' Im " ( -u _pi (,] _pi ) ) <-> ( -u ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) e. CC /\ ( Im ` -u ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) e. ( -u _pi (,] _pi ) ) )
83 32 78 82 sylanbrc 
 |-  ( A e. CC -> -u ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) e. ( `' Im " ( -u _pi (,] _pi ) ) )
84 logrn 
 |-  ran log = ( `' Im " ( -u _pi (,] _pi ) )
85 83 84 eleqtrrdi 
 |-  ( A e. CC -> -u ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) e. ran log )
86 logeftb 
 |-  ( ( ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) e. CC /\ ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) =/= 0 /\ -u ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) e. ran log ) -> ( ( log ` ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) = -u ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) <-> ( exp ` -u ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) = ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) )
87 26 31 85 86 syl3anc 
 |-  ( A e. CC -> ( ( log ` ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) = -u ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) <-> ( exp ` -u ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) = ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) )
88 29 87 mpbird 
 |-  ( A e. CC -> ( log ` ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) = -u ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) )
89 88 oveq2d 
 |-  ( A e. CC -> ( -u _i x. ( log ` ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) ) = ( -u _i x. -u ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) )
90 negicn 
 |-  -u _i e. CC
91 mulneg2 
 |-  ( ( -u _i e. CC /\ ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) e. CC ) -> ( -u _i x. -u ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) = -u ( -u _i x. ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) )
92 90 11 91 sylancr 
 |-  ( A e. CC -> ( -u _i x. -u ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) = -u ( -u _i x. ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) )
93 89 92 eqtrd 
 |-  ( A e. CC -> ( -u _i x. ( log ` ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) ) = -u ( -u _i x. ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) )
94 asinval 
 |-  ( -u A e. CC -> ( arcsin ` -u A ) = ( -u _i x. ( log ` ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) ) )
95 19 94 syl 
 |-  ( A e. CC -> ( arcsin ` -u A ) = ( -u _i x. ( log ` ( ( _i x. -u A ) + ( sqrt ` ( 1 - ( -u A ^ 2 ) ) ) ) ) ) )
96 asinval 
 |-  ( A e. CC -> ( arcsin ` A ) = ( -u _i x. ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) )
97 96 negeqd 
 |-  ( A e. CC -> -u ( arcsin ` A ) = -u ( -u _i x. ( log ` ( ( _i x. A ) + ( sqrt ` ( 1 - ( A ^ 2 ) ) ) ) ) ) )
98 93 95 97 3eqtr4d 
 |-  ( A e. CC -> ( arcsin ` -u A ) = -u ( arcsin ` A ) )