Metamath Proof Explorer

Theorem dvasin

Description: Derivative of arcsine. (Contributed by Brendan Leahy, 18-Dec-2018)

Ref Expression
Hypothesis dvasin.d 
|- D = ( CC \ ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) )
Assertion dvasin 
|- ( CC _D ( arcsin |` D ) ) = ( x e. D |-> ( 1 / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dvasin.d 
 |-  D = ( CC \ ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) )
2 df-asin 
 |-  arcsin = ( x e. CC |-> ( -u _i x. ( log ` ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) ) )
3 2 reseq1i 
 |-  ( arcsin |` D ) = ( ( x e. CC |-> ( -u _i x. ( log ` ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) ) ) |` D )
4 difss 
 |-  ( CC \ ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) ) C_ CC
5 1 4 eqsstri 
 |-  D C_ CC
6 resmpt 
 |-  ( D C_ CC -> ( ( x e. CC |-> ( -u _i x. ( log ` ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) ) ) |` D ) = ( x e. D |-> ( -u _i x. ( log ` ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) ) ) )
7 5 6 ax-mp 
 |-  ( ( x e. CC |-> ( -u _i x. ( log ` ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) ) ) |` D ) = ( x e. D |-> ( -u _i x. ( log ` ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) ) )
8 3 7 eqtri 
 |-  ( arcsin |` D ) = ( x e. D |-> ( -u _i x. ( log ` ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) ) )
9 8 oveq2i 
 |-  ( CC _D ( arcsin |` D ) ) = ( CC _D ( x e. D |-> ( -u _i x. ( log ` ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) ) ) )
10 cnelprrecn 
 |-  CC e. { RR , CC }
11 10 a1i 
 |-  ( T. -> CC e. { RR , CC } )
12 5 sseli 
 |-  ( x e. D -> x e. CC )
13 ax-icn 
 |-  _i e. CC
14 mulcl 
 |-  ( ( _i e. CC /\ x e. CC ) -> ( _i x. x ) e. CC )
15 13 14 mpan 
 |-  ( x e. CC -> ( _i x. x ) e. CC )
16 ax-1cn 
 |-  1 e. CC
17 sqcl 
 |-  ( x e. CC -> ( x ^ 2 ) e. CC )
18 subcl 
 |-  ( ( 1 e. CC /\ ( x ^ 2 ) e. CC ) -> ( 1 - ( x ^ 2 ) ) e. CC )
19 16 17 18 sylancr 
 |-  ( x e. CC -> ( 1 - ( x ^ 2 ) ) e. CC )
20 19 sqrtcld 
 |-  ( x e. CC -> ( sqrt ` ( 1 - ( x ^ 2 ) ) ) e. CC )
21 15 20 addcld 
 |-  ( x e. CC -> ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) e. CC )
22 12 21 syl 
 |-  ( x e. D -> ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) e. CC )
23 asinlem 
 |-  ( x e. CC -> ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) =/= 0 )
24 12 23 syl 
 |-  ( x e. D -> ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) =/= 0 )
25 22 24 logcld 
 |-  ( x e. D -> ( log ` ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) e. CC )
26 25 adantl 
 |-  ( ( T. /\ x e. D ) -> ( log ` ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) e. CC )
27 ovexd 
 |-  ( ( T. /\ x e. D ) -> ( _i / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) e. _V )
28 simpr 
 |-  ( ( x e. CC /\ ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) e. RR ) -> ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) e. RR )
29 asinlem3 
 |-  ( x e. CC -> 0 <_ ( Re ` ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) )
30 rere 
 |-  ( ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) e. RR -> ( Re ` ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) = ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) )
31 30 breq2d 
 |-  ( ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) e. RR -> ( 0 <_ ( Re ` ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) <-> 0 <_ ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) )
32 31 biimpac 
 |-  ( ( 0 <_ ( Re ` ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) /\ ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) e. RR ) -> 0 <_ ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) )
33 29 32 sylan 
 |-  ( ( x e. CC /\ ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) e. RR ) -> 0 <_ ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) )
34 23 adantr 
 |-  ( ( x e. CC /\ ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) e. RR ) -> ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) =/= 0 )
35 28 33 34 ne0gt0d 
 |-  ( ( x e. CC /\ ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) e. RR ) -> 0 < ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) )
36 0re 
 |-  0 e. RR
37 ltnle 
 |-  ( ( 0 e. RR /\ ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) e. RR ) -> ( 0 < ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) <-> -. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) <_ 0 ) )
38 36 37 mpan 
 |-  ( ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) e. RR -> ( 0 < ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) <-> -. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) <_ 0 ) )
39 38 adantl 
 |-  ( ( x e. CC /\ ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) e. RR ) -> ( 0 < ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) <-> -. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) <_ 0 ) )
40 35 39 mpbid 
 |-  ( ( x e. CC /\ ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) e. RR ) -> -. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) <_ 0 )
41 40 ex 
 |-  ( x e. CC -> ( ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) e. RR -> -. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) <_ 0 ) )
42 12 41 syl 
 |-  ( x e. D -> ( ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) e. RR -> -. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) <_ 0 ) )
43 imor 
 |-  ( ( ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) e. RR -> -. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) <_ 0 ) <-> ( -. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) e. RR \/ -. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) <_ 0 ) )
44 42 43 sylib 
 |-  ( x e. D -> ( -. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) e. RR \/ -. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) <_ 0 ) )
45 44 orcomd 
 |-  ( x e. D -> ( -. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) <_ 0 \/ -. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) e. RR ) )
46 45 olcd 
 |-  ( x e. D -> ( -. -oo < ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) \/ ( -. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) <_ 0 \/ -. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) e. RR ) ) )
47 3ianor 
 |-  ( -. ( ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) e. RR /\ -oo < ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) /\ ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) <_ 0 ) <-> ( -. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) e. RR \/ -. -oo < ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) \/ -. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) <_ 0 ) )
48 3orrot 
 |-  ( ( -. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) e. RR \/ -. -oo < ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) \/ -. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) <_ 0 ) <-> ( -. -oo < ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) \/ -. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) <_ 0 \/ -. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) e. RR ) )
49 3orass 
 |-  ( ( -. -oo < ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) \/ -. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) <_ 0 \/ -. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) e. RR ) <-> ( -. -oo < ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) \/ ( -. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) <_ 0 \/ -. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) e. RR ) ) )
50 47 48 49 3bitrri 
 |-  ( ( -. -oo < ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) \/ ( -. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) <_ 0 \/ -. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) e. RR ) ) <-> -. ( ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) e. RR /\ -oo < ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) /\ ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) <_ 0 ) )
51 mnfxr 
 |-  -oo e. RR*
52 elioc2 
 |-  ( ( -oo e. RR* /\ 0 e. RR ) -> ( ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) e. ( -oo (,] 0 ) <-> ( ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) e. RR /\ -oo < ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) /\ ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) <_ 0 ) ) )
53 51 36 52 mp2an 
 |-  ( ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) e. ( -oo (,] 0 ) <-> ( ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) e. RR /\ -oo < ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) /\ ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) <_ 0 ) )
54 50 53 xchbinxr 
 |-  ( ( -. -oo < ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) \/ ( -. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) <_ 0 \/ -. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) e. RR ) ) <-> -. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) e. ( -oo (,] 0 ) )
55 46 54 sylib 
 |-  ( x e. D -> -. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) e. ( -oo (,] 0 ) )
56 22 55 eldifd 
 |-  ( x e. D -> ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) e. ( CC \ ( -oo (,] 0 ) ) )
57 56 adantl 
 |-  ( ( T. /\ x e. D ) -> ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) e. ( CC \ ( -oo (,] 0 ) ) )
58 ovexd 
 |-  ( ( T. /\ x e. D ) -> ( ( _i x. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) e. _V )
59 eldifi 
 |-  ( y e. ( CC \ ( -oo (,] 0 ) ) -> y e. CC )
60 eldifn 
 |-  ( y e. ( CC \ ( -oo (,] 0 ) ) -> -. y e. ( -oo (,] 0 ) )
61 0xr 
 |-  0 e. RR*
62 mnflt0 
 |-  -oo < 0
63 ubioc1 
 |-  ( ( -oo e. RR* /\ 0 e. RR* /\ -oo < 0 ) -> 0 e. ( -oo (,] 0 ) )
64 51 61 62 63 mp3an 
 |-  0 e. ( -oo (,] 0 )
65 eleq1 
 |-  ( y = 0 -> ( y e. ( -oo (,] 0 ) <-> 0 e. ( -oo (,] 0 ) ) )
66 64 65 mpbiri 
 |-  ( y = 0 -> y e. ( -oo (,] 0 ) )
67 66 necon3bi 
 |-  ( -. y e. ( -oo (,] 0 ) -> y =/= 0 )
68 60 67 syl 
 |-  ( y e. ( CC \ ( -oo (,] 0 ) ) -> y =/= 0 )
69 59 68 logcld 
 |-  ( y e. ( CC \ ( -oo (,] 0 ) ) -> ( log ` y ) e. CC )
70 69 adantl 
 |-  ( ( T. /\ y e. ( CC \ ( -oo (,] 0 ) ) ) -> ( log ` y ) e. CC )
71 ovexd 
 |-  ( ( T. /\ y e. ( CC \ ( -oo (,] 0 ) ) ) -> ( 1 / y ) e. _V )
72 13 a1i 
 |-  ( x e. D -> _i e. CC )
73 72 12 mulcld 
 |-  ( x e. D -> ( _i x. x ) e. CC )
74 73 adantl 
 |-  ( ( T. /\ x e. D ) -> ( _i x. x ) e. CC )
75 13 a1i 
 |-  ( ( T. /\ x e. D ) -> _i e. CC )
76 12 adantl 
 |-  ( ( T. /\ x e. D ) -> x e. CC )
77 1cnd 
 |-  ( ( T. /\ x e. D ) -> 1 e. CC )
78 simpr 
 |-  ( ( T. /\ x e. CC ) -> x e. CC )
79 1cnd 
 |-  ( ( T. /\ x e. CC ) -> 1 e. CC )
80 11 dvmptid 
 |-  ( T. -> ( CC _D ( x e. CC |-> x ) ) = ( x e. CC |-> 1 ) )
81 5 a1i 
 |-  ( T. -> D C_ CC )
82 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
83 82 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
84 83 toponrestid 
 |-  ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
85 82 recld2 
 |-  RR e. ( Clsd ` ( TopOpen ` CCfld ) )
86 neg1rr 
 |-  -u 1 e. RR
87 iocmnfcld 
 |-  ( -u 1 e. RR -> ( -oo (,] -u 1 ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
88 86 87 ax-mp 
 |-  ( -oo (,] -u 1 ) e. ( Clsd ` ( topGen ` ran (,) ) )
89 1re 
 |-  1 e. RR
90 icopnfcld 
 |-  ( 1 e. RR -> ( 1 [,) +oo ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
91 89 90 ax-mp 
 |-  ( 1 [,) +oo ) e. ( Clsd ` ( topGen ` ran (,) ) )
92 uncld 
 |-  ( ( ( -oo (,] -u 1 ) e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( 1 [,) +oo ) e. ( Clsd ` ( topGen ` ran (,) ) ) ) -> ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
93 88 91 92 mp2an 
 |-  ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) e. ( Clsd ` ( topGen ` ran (,) ) )
94 82 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
95 94 fveq2i 
 |-  ( Clsd ` ( topGen ` ran (,) ) ) = ( Clsd ` ( ( TopOpen ` CCfld ) |`t RR ) )
96 93 95 eleqtri 
 |-  ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) e. ( Clsd ` ( ( TopOpen ` CCfld ) |`t RR ) )
97 restcldr 
 |-  ( ( RR e. ( Clsd ` ( TopOpen ` CCfld ) ) /\ ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) e. ( Clsd ` ( ( TopOpen ` CCfld ) |`t RR ) ) ) -> ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) e. ( Clsd ` ( TopOpen ` CCfld ) ) )
98 85 96 97 mp2an 
 |-  ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) e. ( Clsd ` ( TopOpen ` CCfld ) )
99 83 toponunii 
 |-  CC = U. ( TopOpen ` CCfld )
100 99 cldopn 
 |-  ( ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) e. ( Clsd ` ( TopOpen ` CCfld ) ) -> ( CC \ ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) ) e. ( TopOpen ` CCfld ) )
101 98 100 ax-mp 
 |-  ( CC \ ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) ) e. ( TopOpen ` CCfld )
102 1 101 eqeltri 
 |-  D e. ( TopOpen ` CCfld )
103 102 a1i 
 |-  ( T. -> D e. ( TopOpen ` CCfld ) )
104 11 78 79 80 81 84 82 103 dvmptres 
 |-  ( T. -> ( CC _D ( x e. D |-> x ) ) = ( x e. D |-> 1 ) )
105 13 a1i 
 |-  ( T. -> _i e. CC )
106 11 76 77 104 105 dvmptcmul 
 |-  ( T. -> ( CC _D ( x e. D |-> ( _i x. x ) ) ) = ( x e. D |-> ( _i x. 1 ) ) )
107 13 mulid1i 
 |-  ( _i x. 1 ) = _i
108 107 mpteq2i 
 |-  ( x e. D |-> ( _i x. 1 ) ) = ( x e. D |-> _i )
109 106 108 eqtrdi 
 |-  ( T. -> ( CC _D ( x e. D |-> ( _i x. x ) ) ) = ( x e. D |-> _i ) )
110 12 sqcld 
 |-  ( x e. D -> ( x ^ 2 ) e. CC )
111 16 110 18 sylancr 
 |-  ( x e. D -> ( 1 - ( x ^ 2 ) ) e. CC )
112 111 sqrtcld 
 |-  ( x e. D -> ( sqrt ` ( 1 - ( x ^ 2 ) ) ) e. CC )
113 112 adantl 
 |-  ( ( T. /\ x e. D ) -> ( sqrt ` ( 1 - ( x ^ 2 ) ) ) e. CC )
114 ovexd 
 |-  ( ( T. /\ x e. D ) -> ( -u x / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) e. _V )
115 elin 
 |-  ( x e. ( D i^i RR ) <-> ( x e. D /\ x e. RR ) )
116 1 asindmre 
 |-  ( D i^i RR ) = ( -u 1 (,) 1 )
117 116 eqimssi 
 |-  ( D i^i RR ) C_ ( -u 1 (,) 1 )
118 117 sseli 
 |-  ( x e. ( D i^i RR ) -> x e. ( -u 1 (,) 1 ) )
119 115 118 sylbir 
 |-  ( ( x e. D /\ x e. RR ) -> x e. ( -u 1 (,) 1 ) )
120 incom 
 |-  ( ( 0 (,) +oo ) i^i ( -oo (,] 0 ) ) = ( ( -oo (,] 0 ) i^i ( 0 (,) +oo ) )
121 pnfxr 
 |-  +oo e. RR*
122 df-ioc 
 |-  (,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )
123 df-ioo 
 |-  (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } )
124 xrltnle 
 |-  ( ( 0 e. RR* /\ w e. RR* ) -> ( 0 < w <-> -. w <_ 0 ) )
125 122 123 124 ixxdisj 
 |-  ( ( -oo e. RR* /\ 0 e. RR* /\ +oo e. RR* ) -> ( ( -oo (,] 0 ) i^i ( 0 (,) +oo ) ) = (/) )
126 51 61 121 125 mp3an 
 |-  ( ( -oo (,] 0 ) i^i ( 0 (,) +oo ) ) = (/)
127 120 126 eqtri 
 |-  ( ( 0 (,) +oo ) i^i ( -oo (,] 0 ) ) = (/)
128 elioore 
 |-  ( x e. ( -u 1 (,) 1 ) -> x e. RR )
129 128 resqcld 
 |-  ( x e. ( -u 1 (,) 1 ) -> ( x ^ 2 ) e. RR )
130 resubcl 
 |-  ( ( 1 e. RR /\ ( x ^ 2 ) e. RR ) -> ( 1 - ( x ^ 2 ) ) e. RR )
131 89 129 130 sylancr 
 |-  ( x e. ( -u 1 (,) 1 ) -> ( 1 - ( x ^ 2 ) ) e. RR )
132 86 rexri 
 |-  -u 1 e. RR*
133 1xr 
 |-  1 e. RR*
134 elioo2 
 |-  ( ( -u 1 e. RR* /\ 1 e. RR* ) -> ( x e. ( -u 1 (,) 1 ) <-> ( x e. RR /\ -u 1 < x /\ x < 1 ) ) )
135 132 133 134 mp2an 
 |-  ( x e. ( -u 1 (,) 1 ) <-> ( x e. RR /\ -u 1 < x /\ x < 1 ) )
136 recn 
 |-  ( x e. RR -> x e. CC )
137 136 abscld 
 |-  ( x e. RR -> ( abs ` x ) e. RR )
138 136 absge0d 
 |-  ( x e. RR -> 0 <_ ( abs ` x ) )
139 0le1 
 |-  0 <_ 1
140 lt2sq 
 |-  ( ( ( ( abs ` x ) e. RR /\ 0 <_ ( abs ` x ) ) /\ ( 1 e. RR /\ 0 <_ 1 ) ) -> ( ( abs ` x ) < 1 <-> ( ( abs ` x ) ^ 2 ) < ( 1 ^ 2 ) ) )
141 89 139 140 mpanr12 
 |-  ( ( ( abs ` x ) e. RR /\ 0 <_ ( abs ` x ) ) -> ( ( abs ` x ) < 1 <-> ( ( abs ` x ) ^ 2 ) < ( 1 ^ 2 ) ) )
142 137 138 141 syl2anc 
 |-  ( x e. RR -> ( ( abs ` x ) < 1 <-> ( ( abs ` x ) ^ 2 ) < ( 1 ^ 2 ) ) )
143 abslt 
 |-  ( ( x e. RR /\ 1 e. RR ) -> ( ( abs ` x ) < 1 <-> ( -u 1 < x /\ x < 1 ) ) )
144 89 143 mpan2 
 |-  ( x e. RR -> ( ( abs ` x ) < 1 <-> ( -u 1 < x /\ x < 1 ) ) )
145 absresq 
 |-  ( x e. RR -> ( ( abs ` x ) ^ 2 ) = ( x ^ 2 ) )
146 sq1 
 |-  ( 1 ^ 2 ) = 1
147 146 a1i 
 |-  ( x e. RR -> ( 1 ^ 2 ) = 1 )
148 145 147 breq12d 
 |-  ( x e. RR -> ( ( ( abs ` x ) ^ 2 ) < ( 1 ^ 2 ) <-> ( x ^ 2 ) < 1 ) )
149 resqcl 
 |-  ( x e. RR -> ( x ^ 2 ) e. RR )
150 posdif 
 |-  ( ( ( x ^ 2 ) e. RR /\ 1 e. RR ) -> ( ( x ^ 2 ) < 1 <-> 0 < ( 1 - ( x ^ 2 ) ) ) )
151 149 89 150 sylancl 
 |-  ( x e. RR -> ( ( x ^ 2 ) < 1 <-> 0 < ( 1 - ( x ^ 2 ) ) ) )
152 148 151 bitrd 
 |-  ( x e. RR -> ( ( ( abs ` x ) ^ 2 ) < ( 1 ^ 2 ) <-> 0 < ( 1 - ( x ^ 2 ) ) ) )
153 142 144 152 3bitr3d 
 |-  ( x e. RR -> ( ( -u 1 < x /\ x < 1 ) <-> 0 < ( 1 - ( x ^ 2 ) ) ) )
154 153 biimpd 
 |-  ( x e. RR -> ( ( -u 1 < x /\ x < 1 ) -> 0 < ( 1 - ( x ^ 2 ) ) ) )
155 154 3impib 
 |-  ( ( x e. RR /\ -u 1 < x /\ x < 1 ) -> 0 < ( 1 - ( x ^ 2 ) ) )
156 135 155 sylbi 
 |-  ( x e. ( -u 1 (,) 1 ) -> 0 < ( 1 - ( x ^ 2 ) ) )
157 131 156 elrpd 
 |-  ( x e. ( -u 1 (,) 1 ) -> ( 1 - ( x ^ 2 ) ) e. RR+ )
158 ioorp 
 |-  ( 0 (,) +oo ) = RR+
159 157 158 eleqtrrdi 
 |-  ( x e. ( -u 1 (,) 1 ) -> ( 1 - ( x ^ 2 ) ) e. ( 0 (,) +oo ) )
160 disjel 
 |-  ( ( ( ( 0 (,) +oo ) i^i ( -oo (,] 0 ) ) = (/) /\ ( 1 - ( x ^ 2 ) ) e. ( 0 (,) +oo ) ) -> -. ( 1 - ( x ^ 2 ) ) e. ( -oo (,] 0 ) )
161 127 159 160 sylancr 
 |-  ( x e. ( -u 1 (,) 1 ) -> -. ( 1 - ( x ^ 2 ) ) e. ( -oo (,] 0 ) )
162 119 161 syl 
 |-  ( ( x e. D /\ x e. RR ) -> -. ( 1 - ( x ^ 2 ) ) e. ( -oo (,] 0 ) )
163 elioc2 
 |-  ( ( -oo e. RR* /\ 0 e. RR ) -> ( ( 1 - ( x ^ 2 ) ) e. ( -oo (,] 0 ) <-> ( ( 1 - ( x ^ 2 ) ) e. RR /\ -oo < ( 1 - ( x ^ 2 ) ) /\ ( 1 - ( x ^ 2 ) ) <_ 0 ) ) )
164 51 36 163 mp2an 
 |-  ( ( 1 - ( x ^ 2 ) ) e. ( -oo (,] 0 ) <-> ( ( 1 - ( x ^ 2 ) ) e. RR /\ -oo < ( 1 - ( x ^ 2 ) ) /\ ( 1 - ( x ^ 2 ) ) <_ 0 ) )
165 164 biimpi 
 |-  ( ( 1 - ( x ^ 2 ) ) e. ( -oo (,] 0 ) -> ( ( 1 - ( x ^ 2 ) ) e. RR /\ -oo < ( 1 - ( x ^ 2 ) ) /\ ( 1 - ( x ^ 2 ) ) <_ 0 ) )
166 165 simp1d 
 |-  ( ( 1 - ( x ^ 2 ) ) e. ( -oo (,] 0 ) -> ( 1 - ( x ^ 2 ) ) e. RR )
167 resubcl 
 |-  ( ( 1 e. RR /\ ( 1 - ( x ^ 2 ) ) e. RR ) -> ( 1 - ( 1 - ( x ^ 2 ) ) ) e. RR )
168 89 166 167 sylancr 
 |-  ( ( 1 - ( x ^ 2 ) ) e. ( -oo (,] 0 ) -> ( 1 - ( 1 - ( x ^ 2 ) ) ) e. RR )
169 nncan 
 |-  ( ( 1 e. CC /\ ( x ^ 2 ) e. CC ) -> ( 1 - ( 1 - ( x ^ 2 ) ) ) = ( x ^ 2 ) )
170 16 169 mpan 
 |-  ( ( x ^ 2 ) e. CC -> ( 1 - ( 1 - ( x ^ 2 ) ) ) = ( x ^ 2 ) )
171 170 eleq1d 
 |-  ( ( x ^ 2 ) e. CC -> ( ( 1 - ( 1 - ( x ^ 2 ) ) ) e. RR <-> ( x ^ 2 ) e. RR ) )
172 171 biimpa 
 |-  ( ( ( x ^ 2 ) e. CC /\ ( 1 - ( 1 - ( x ^ 2 ) ) ) e. RR ) -> ( x ^ 2 ) e. RR )
173 168 172 sylan2 
 |-  ( ( ( x ^ 2 ) e. CC /\ ( 1 - ( x ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( x ^ 2 ) e. RR )
174 166 adantl 
 |-  ( ( ( x ^ 2 ) e. CC /\ ( 1 - ( x ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( 1 - ( x ^ 2 ) ) e. RR )
175 165 simp3d 
 |-  ( ( 1 - ( x ^ 2 ) ) e. ( -oo (,] 0 ) -> ( 1 - ( x ^ 2 ) ) <_ 0 )
176 175 adantl 
 |-  ( ( ( x ^ 2 ) e. CC /\ ( 1 - ( x ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( 1 - ( x ^ 2 ) ) <_ 0 )
177 letr 
 |-  ( ( ( 1 - ( x ^ 2 ) ) e. RR /\ 0 e. RR /\ 1 e. RR ) -> ( ( ( 1 - ( x ^ 2 ) ) <_ 0 /\ 0 <_ 1 ) -> ( 1 - ( x ^ 2 ) ) <_ 1 ) )
178 36 89 177 mp3an23 
 |-  ( ( 1 - ( x ^ 2 ) ) e. RR -> ( ( ( 1 - ( x ^ 2 ) ) <_ 0 /\ 0 <_ 1 ) -> ( 1 - ( x ^ 2 ) ) <_ 1 ) )
179 139 178 mpan2i 
 |-  ( ( 1 - ( x ^ 2 ) ) e. RR -> ( ( 1 - ( x ^ 2 ) ) <_ 0 -> ( 1 - ( x ^ 2 ) ) <_ 1 ) )
180 174 176 179 sylc 
 |-  ( ( ( x ^ 2 ) e. CC /\ ( 1 - ( x ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( 1 - ( x ^ 2 ) ) <_ 1 )
181 subge0 
 |-  ( ( 1 e. RR /\ ( 1 - ( x ^ 2 ) ) e. RR ) -> ( 0 <_ ( 1 - ( 1 - ( x ^ 2 ) ) ) <-> ( 1 - ( x ^ 2 ) ) <_ 1 ) )
182 89 174 181 sylancr 
 |-  ( ( ( x ^ 2 ) e. CC /\ ( 1 - ( x ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( 0 <_ ( 1 - ( 1 - ( x ^ 2 ) ) ) <-> ( 1 - ( x ^ 2 ) ) <_ 1 ) )
183 180 182 mpbird 
 |-  ( ( ( x ^ 2 ) e. CC /\ ( 1 - ( x ^ 2 ) ) e. ( -oo (,] 0 ) ) -> 0 <_ ( 1 - ( 1 - ( x ^ 2 ) ) ) )
184 170 adantr 
 |-  ( ( ( x ^ 2 ) e. CC /\ ( 1 - ( x ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( 1 - ( 1 - ( x ^ 2 ) ) ) = ( x ^ 2 ) )
185 183 184 breqtrd 
 |-  ( ( ( x ^ 2 ) e. CC /\ ( 1 - ( x ^ 2 ) ) e. ( -oo (,] 0 ) ) -> 0 <_ ( x ^ 2 ) )
186 173 185 resqrtcld 
 |-  ( ( ( x ^ 2 ) e. CC /\ ( 1 - ( x ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( sqrt ` ( x ^ 2 ) ) e. RR )
187 17 186 sylan 
 |-  ( ( x e. CC /\ ( 1 - ( x ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( sqrt ` ( x ^ 2 ) ) e. RR )
188 eleq1 
 |-  ( x = ( sqrt ` ( x ^ 2 ) ) -> ( x e. RR <-> ( sqrt ` ( x ^ 2 ) ) e. RR ) )
189 187 188 syl5ibrcom 
 |-  ( ( x e. CC /\ ( 1 - ( x ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( x = ( sqrt ` ( x ^ 2 ) ) -> x e. RR ) )
190 187 renegcld 
 |-  ( ( x e. CC /\ ( 1 - ( x ^ 2 ) ) e. ( -oo (,] 0 ) ) -> -u ( sqrt ` ( x ^ 2 ) ) e. RR )
191 eleq1 
 |-  ( x = -u ( sqrt ` ( x ^ 2 ) ) -> ( x e. RR <-> -u ( sqrt ` ( x ^ 2 ) ) e. RR ) )
192 190 191 syl5ibrcom 
 |-  ( ( x e. CC /\ ( 1 - ( x ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( x = -u ( sqrt ` ( x ^ 2 ) ) -> x e. RR ) )
193 eqid 
 |-  ( x ^ 2 ) = ( x ^ 2 )
194 eqsqrtor 
 |-  ( ( x e. CC /\ ( x ^ 2 ) e. CC ) -> ( ( x ^ 2 ) = ( x ^ 2 ) <-> ( x = ( sqrt ` ( x ^ 2 ) ) \/ x = -u ( sqrt ` ( x ^ 2 ) ) ) ) )
195 17 194 mpdan 
 |-  ( x e. CC -> ( ( x ^ 2 ) = ( x ^ 2 ) <-> ( x = ( sqrt ` ( x ^ 2 ) ) \/ x = -u ( sqrt ` ( x ^ 2 ) ) ) ) )
196 193 195 mpbii 
 |-  ( x e. CC -> ( x = ( sqrt ` ( x ^ 2 ) ) \/ x = -u ( sqrt ` ( x ^ 2 ) ) ) )
197 196 adantr 
 |-  ( ( x e. CC /\ ( 1 - ( x ^ 2 ) ) e. ( -oo (,] 0 ) ) -> ( x = ( sqrt ` ( x ^ 2 ) ) \/ x = -u ( sqrt ` ( x ^ 2 ) ) ) )
198 189 192 197 mpjaod 
 |-  ( ( x e. CC /\ ( 1 - ( x ^ 2 ) ) e. ( -oo (,] 0 ) ) -> x e. RR )
199 198 stoic1a 
 |-  ( ( x e. CC /\ -. x e. RR ) -> -. ( 1 - ( x ^ 2 ) ) e. ( -oo (,] 0 ) )
200 12 199 sylan 
 |-  ( ( x e. D /\ -. x e. RR ) -> -. ( 1 - ( x ^ 2 ) ) e. ( -oo (,] 0 ) )
201 162 200 pm2.61dan 
 |-  ( x e. D -> -. ( 1 - ( x ^ 2 ) ) e. ( -oo (,] 0 ) )
202 111 201 eldifd 
 |-  ( x e. D -> ( 1 - ( x ^ 2 ) ) e. ( CC \ ( -oo (,] 0 ) ) )
203 202 adantl 
 |-  ( ( T. /\ x e. D ) -> ( 1 - ( x ^ 2 ) ) e. ( CC \ ( -oo (,] 0 ) ) )
204 2cnd 
 |-  ( x e. CC -> 2 e. CC )
205 id 
 |-  ( x e. CC -> x e. CC )
206 204 205 mulcld 
 |-  ( x e. CC -> ( 2 x. x ) e. CC )
207 206 negcld 
 |-  ( x e. CC -> -u ( 2 x. x ) e. CC )
208 207 adantl 
 |-  ( ( T. /\ x e. CC ) -> -u ( 2 x. x ) e. CC )
209 12 208 sylan2 
 |-  ( ( T. /\ x e. D ) -> -u ( 2 x. x ) e. CC )
210 59 sqrtcld 
 |-  ( y e. ( CC \ ( -oo (,] 0 ) ) -> ( sqrt ` y ) e. CC )
211 210 adantl 
 |-  ( ( T. /\ y e. ( CC \ ( -oo (,] 0 ) ) ) -> ( sqrt ` y ) e. CC )
212 ovexd 
 |-  ( ( T. /\ y e. ( CC \ ( -oo (,] 0 ) ) ) -> ( 1 / ( 2 x. ( sqrt ` y ) ) ) e. _V )
213 19 adantl 
 |-  ( ( T. /\ x e. CC ) -> ( 1 - ( x ^ 2 ) ) e. CC )
214 36 a1i 
 |-  ( ( T. /\ x e. CC ) -> 0 e. RR )
215 1cnd 
 |-  ( T. -> 1 e. CC )
216 11 215 dvmptc 
 |-  ( T. -> ( CC _D ( x e. CC |-> 1 ) ) = ( x e. CC |-> 0 ) )
217 17 adantl 
 |-  ( ( T. /\ x e. CC ) -> ( x ^ 2 ) e. CC )
218 2cn 
 |-  2 e. CC
219 mulcl 
 |-  ( ( 2 e. CC /\ x e. CC ) -> ( 2 x. x ) e. CC )
220 218 219 mpan 
 |-  ( x e. CC -> ( 2 x. x ) e. CC )
221 220 adantl 
 |-  ( ( T. /\ x e. CC ) -> ( 2 x. x ) e. CC )
222 2nn 
 |-  2 e. NN
223 dvexp 
 |-  ( 2 e. NN -> ( CC _D ( x e. CC |-> ( x ^ 2 ) ) ) = ( x e. CC |-> ( 2 x. ( x ^ ( 2 - 1 ) ) ) ) )
224 222 223 ax-mp 
 |-  ( CC _D ( x e. CC |-> ( x ^ 2 ) ) ) = ( x e. CC |-> ( 2 x. ( x ^ ( 2 - 1 ) ) ) )
225 2m1e1 
 |-  ( 2 - 1 ) = 1
226 225 oveq2i 
 |-  ( x ^ ( 2 - 1 ) ) = ( x ^ 1 )
227 exp1 
 |-  ( x e. CC -> ( x ^ 1 ) = x )
228 226 227 syl5eq 
 |-  ( x e. CC -> ( x ^ ( 2 - 1 ) ) = x )
229 228 oveq2d 
 |-  ( x e. CC -> ( 2 x. ( x ^ ( 2 - 1 ) ) ) = ( 2 x. x ) )
230 229 mpteq2ia 
 |-  ( x e. CC |-> ( 2 x. ( x ^ ( 2 - 1 ) ) ) ) = ( x e. CC |-> ( 2 x. x ) )
231 224 230 eqtri 
 |-  ( CC _D ( x e. CC |-> ( x ^ 2 ) ) ) = ( x e. CC |-> ( 2 x. x ) )
232 231 a1i 
 |-  ( T. -> ( CC _D ( x e. CC |-> ( x ^ 2 ) ) ) = ( x e. CC |-> ( 2 x. x ) ) )
233 11 79 214 216 217 221 232 dvmptsub 
 |-  ( T. -> ( CC _D ( x e. CC |-> ( 1 - ( x ^ 2 ) ) ) ) = ( x e. CC |-> ( 0 - ( 2 x. x ) ) ) )
234 df-neg 
 |-  -u ( 2 x. x ) = ( 0 - ( 2 x. x ) )
235 234 mpteq2i 
 |-  ( x e. CC |-> -u ( 2 x. x ) ) = ( x e. CC |-> ( 0 - ( 2 x. x ) ) )
236 233 235 eqtr4di 
 |-  ( T. -> ( CC _D ( x e. CC |-> ( 1 - ( x ^ 2 ) ) ) ) = ( x e. CC |-> -u ( 2 x. x ) ) )
237 11 213 208 236 81 84 82 103 dvmptres 
 |-  ( T. -> ( CC _D ( x e. D |-> ( 1 - ( x ^ 2 ) ) ) ) = ( x e. D |-> -u ( 2 x. x ) ) )
238 eqid 
 |-  ( CC \ ( -oo (,] 0 ) ) = ( CC \ ( -oo (,] 0 ) )
239 238 dvcnsqrt 
 |-  ( CC _D ( y e. ( CC \ ( -oo (,] 0 ) ) |-> ( sqrt ` y ) ) ) = ( y e. ( CC \ ( -oo (,] 0 ) ) |-> ( 1 / ( 2 x. ( sqrt ` y ) ) ) )
240 239 a1i 
 |-  ( T. -> ( CC _D ( y e. ( CC \ ( -oo (,] 0 ) ) |-> ( sqrt ` y ) ) ) = ( y e. ( CC \ ( -oo (,] 0 ) ) |-> ( 1 / ( 2 x. ( sqrt ` y ) ) ) ) )
241 fveq2 
 |-  ( y = ( 1 - ( x ^ 2 ) ) -> ( sqrt ` y ) = ( sqrt ` ( 1 - ( x ^ 2 ) ) ) )
242 241 oveq2d 
 |-  ( y = ( 1 - ( x ^ 2 ) ) -> ( 2 x. ( sqrt ` y ) ) = ( 2 x. ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) )
243 242 oveq2d 
 |-  ( y = ( 1 - ( x ^ 2 ) ) -> ( 1 / ( 2 x. ( sqrt ` y ) ) ) = ( 1 / ( 2 x. ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) )
244 11 11 203 209 211 212 237 240 241 243 dvmptco 
 |-  ( T. -> ( CC _D ( x e. D |-> ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) = ( x e. D |-> ( ( 1 / ( 2 x. ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) x. -u ( 2 x. x ) ) ) )
245 mulneg2 
 |-  ( ( 2 e. CC /\ x e. CC ) -> ( 2 x. -u x ) = -u ( 2 x. x ) )
246 218 12 245 sylancr 
 |-  ( x e. D -> ( 2 x. -u x ) = -u ( 2 x. x ) )
247 246 oveq1d 
 |-  ( x e. D -> ( ( 2 x. -u x ) / ( 2 x. ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) = ( -u ( 2 x. x ) / ( 2 x. ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) )
248 12 negcld 
 |-  ( x e. D -> -u x e. CC )
249 eldifn 
 |-  ( x e. ( CC \ ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) ) -> -. x e. ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) )
250 249 1 eleq2s 
 |-  ( x e. D -> -. x e. ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) )
251 id 
 |-  ( x = -u 1 -> x = -u 1 )
252 mnflt 
 |-  ( -u 1 e. RR -> -oo < -u 1 )
253 86 252 ax-mp 
 |-  -oo < -u 1
254 ubioc1 
 |-  ( ( -oo e. RR* /\ -u 1 e. RR* /\ -oo < -u 1 ) -> -u 1 e. ( -oo (,] -u 1 ) )
255 51 132 253 254 mp3an 
 |-  -u 1 e. ( -oo (,] -u 1 )
256 251 255 eqeltrdi 
 |-  ( x = -u 1 -> x e. ( -oo (,] -u 1 ) )
257 id 
 |-  ( x = 1 -> x = 1 )
258 ltpnf 
 |-  ( 1 e. RR -> 1 < +oo )
259 89 258 ax-mp 
 |-  1 < +oo
260 lbico1 
 |-  ( ( 1 e. RR* /\ +oo e. RR* /\ 1 < +oo ) -> 1 e. ( 1 [,) +oo ) )
261 133 121 259 260 mp3an 
 |-  1 e. ( 1 [,) +oo )
262 257 261 eqeltrdi 
 |-  ( x = 1 -> x e. ( 1 [,) +oo ) )
263 256 262 orim12i 
 |-  ( ( x = -u 1 \/ x = 1 ) -> ( x e. ( -oo (,] -u 1 ) \/ x e. ( 1 [,) +oo ) ) )
264 263 orcoms 
 |-  ( ( x = 1 \/ x = -u 1 ) -> ( x e. ( -oo (,] -u 1 ) \/ x e. ( 1 [,) +oo ) ) )
265 elun 
 |-  ( x e. ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) <-> ( x e. ( -oo (,] -u 1 ) \/ x e. ( 1 [,) +oo ) ) )
266 264 265 sylibr 
 |-  ( ( x = 1 \/ x = -u 1 ) -> x e. ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) )
267 250 266 nsyl 
 |-  ( x e. D -> -. ( x = 1 \/ x = -u 1 ) )
268 1cnd 
 |-  ( ( x e. CC /\ ( sqrt ` ( 1 - ( x ^ 2 ) ) ) = 0 ) -> 1 e. CC )
269 17 adantr 
 |-  ( ( x e. CC /\ ( sqrt ` ( 1 - ( x ^ 2 ) ) ) = 0 ) -> ( x ^ 2 ) e. CC )
270 19 adantr 
 |-  ( ( x e. CC /\ ( sqrt ` ( 1 - ( x ^ 2 ) ) ) = 0 ) -> ( 1 - ( x ^ 2 ) ) e. CC )
271 simpr 
 |-  ( ( x e. CC /\ ( sqrt ` ( 1 - ( x ^ 2 ) ) ) = 0 ) -> ( sqrt ` ( 1 - ( x ^ 2 ) ) ) = 0 )
272 270 271 sqr00d 
 |-  ( ( x e. CC /\ ( sqrt ` ( 1 - ( x ^ 2 ) ) ) = 0 ) -> ( 1 - ( x ^ 2 ) ) = 0 )
273 268 269 272 subeq0d 
 |-  ( ( x e. CC /\ ( sqrt ` ( 1 - ( x ^ 2 ) ) ) = 0 ) -> 1 = ( x ^ 2 ) )
274 146 273 eqtr2id 
 |-  ( ( x e. CC /\ ( sqrt ` ( 1 - ( x ^ 2 ) ) ) = 0 ) -> ( x ^ 2 ) = ( 1 ^ 2 ) )
275 274 ex 
 |-  ( x e. CC -> ( ( sqrt ` ( 1 - ( x ^ 2 ) ) ) = 0 -> ( x ^ 2 ) = ( 1 ^ 2 ) ) )
276 sqeqor 
 |-  ( ( x e. CC /\ 1 e. CC ) -> ( ( x ^ 2 ) = ( 1 ^ 2 ) <-> ( x = 1 \/ x = -u 1 ) ) )
277 16 276 mpan2 
 |-  ( x e. CC -> ( ( x ^ 2 ) = ( 1 ^ 2 ) <-> ( x = 1 \/ x = -u 1 ) ) )
278 275 277 sylibd 
 |-  ( x e. CC -> ( ( sqrt ` ( 1 - ( x ^ 2 ) ) ) = 0 -> ( x = 1 \/ x = -u 1 ) ) )
279 278 necon3bd 
 |-  ( x e. CC -> ( -. ( x = 1 \/ x = -u 1 ) -> ( sqrt ` ( 1 - ( x ^ 2 ) ) ) =/= 0 ) )
280 12 267 279 sylc 
 |-  ( x e. D -> ( sqrt ` ( 1 - ( x ^ 2 ) ) ) =/= 0 )
281 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
282 divcan5 
 |-  ( ( -u x e. CC /\ ( ( sqrt ` ( 1 - ( x ^ 2 ) ) ) e. CC /\ ( sqrt ` ( 1 - ( x ^ 2 ) ) ) =/= 0 ) /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( 2 x. -u x ) / ( 2 x. ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) = ( -u x / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) )
283 281 282 mp3an3 
 |-  ( ( -u x e. CC /\ ( ( sqrt ` ( 1 - ( x ^ 2 ) ) ) e. CC /\ ( sqrt ` ( 1 - ( x ^ 2 ) ) ) =/= 0 ) ) -> ( ( 2 x. -u x ) / ( 2 x. ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) = ( -u x / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) )
284 248 112 280 283 syl12anc 
 |-  ( x e. D -> ( ( 2 x. -u x ) / ( 2 x. ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) = ( -u x / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) )
285 218 12 219 sylancr 
 |-  ( x e. D -> ( 2 x. x ) e. CC )
286 285 negcld 
 |-  ( x e. D -> -u ( 2 x. x ) e. CC )
287 mulcl 
 |-  ( ( 2 e. CC /\ ( sqrt ` ( 1 - ( x ^ 2 ) ) ) e. CC ) -> ( 2 x. ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) e. CC )
288 218 112 287 sylancr 
 |-  ( x e. D -> ( 2 x. ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) e. CC )
289 mulne0 
 |-  ( ( ( 2 e. CC /\ 2 =/= 0 ) /\ ( ( sqrt ` ( 1 - ( x ^ 2 ) ) ) e. CC /\ ( sqrt ` ( 1 - ( x ^ 2 ) ) ) =/= 0 ) ) -> ( 2 x. ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) =/= 0 )
290 281 289 mpan 
 |-  ( ( ( sqrt ` ( 1 - ( x ^ 2 ) ) ) e. CC /\ ( sqrt ` ( 1 - ( x ^ 2 ) ) ) =/= 0 ) -> ( 2 x. ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) =/= 0 )
291 112 280 290 syl2anc 
 |-  ( x e. D -> ( 2 x. ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) =/= 0 )
292 286 288 291 divrec2d 
 |-  ( x e. D -> ( -u ( 2 x. x ) / ( 2 x. ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) = ( ( 1 / ( 2 x. ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) x. -u ( 2 x. x ) ) )
293 247 284 292 3eqtr3rd 
 |-  ( x e. D -> ( ( 1 / ( 2 x. ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) x. -u ( 2 x. x ) ) = ( -u x / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) )
294 293 mpteq2ia 
 |-  ( x e. D |-> ( ( 1 / ( 2 x. ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) x. -u ( 2 x. x ) ) ) = ( x e. D |-> ( -u x / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) )
295 244 294 eqtrdi 
 |-  ( T. -> ( CC _D ( x e. D |-> ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) = ( x e. D |-> ( -u x / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) )
296 11 74 75 109 113 114 295 dvmptadd 
 |-  ( T. -> ( CC _D ( x e. D |-> ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) ) = ( x e. D |-> ( _i + ( -u x / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) ) )
297 mulcl 
 |-  ( ( _i e. CC /\ ( sqrt ` ( 1 - ( x ^ 2 ) ) ) e. CC ) -> ( _i x. ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) e. CC )
298 13 20 297 sylancr 
 |-  ( x e. CC -> ( _i x. ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) e. CC )
299 12 298 syl 
 |-  ( x e. D -> ( _i x. ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) e. CC )
300 299 248 112 280 divdird 
 |-  ( x e. D -> ( ( ( _i x. ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) + -u x ) / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) = ( ( ( _i x. ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) + ( -u x / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) )
301 ixi 
 |-  ( _i x. _i ) = -u 1
302 301 eqcomi 
 |-  -u 1 = ( _i x. _i )
303 302 oveq1i 
 |-  ( -u 1 x. x ) = ( ( _i x. _i ) x. x )
304 mulm1 
 |-  ( x e. CC -> ( -u 1 x. x ) = -u x )
305 mulass 
 |-  ( ( _i e. CC /\ _i e. CC /\ x e. CC ) -> ( ( _i x. _i ) x. x ) = ( _i x. ( _i x. x ) ) )
306 13 13 305 mp3an12 
 |-  ( x e. CC -> ( ( _i x. _i ) x. x ) = ( _i x. ( _i x. x ) ) )
307 303 304 306 3eqtr3a 
 |-  ( x e. CC -> -u x = ( _i x. ( _i x. x ) ) )
308 307 oveq1d 
 |-  ( x e. CC -> ( -u x + ( _i x. ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) = ( ( _i x. ( _i x. x ) ) + ( _i x. ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) )
309 negcl 
 |-  ( x e. CC -> -u x e. CC )
310 298 309 addcomd 
 |-  ( x e. CC -> ( ( _i x. ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) + -u x ) = ( -u x + ( _i x. ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) )
311 13 a1i 
 |-  ( x e. CC -> _i e. CC )
312 311 15 20 adddid 
 |-  ( x e. CC -> ( _i x. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) = ( ( _i x. ( _i x. x ) ) + ( _i x. ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) )
313 308 310 312 3eqtr4d 
 |-  ( x e. CC -> ( ( _i x. ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) + -u x ) = ( _i x. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) )
314 12 313 syl 
 |-  ( x e. D -> ( ( _i x. ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) + -u x ) = ( _i x. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) )
315 314 oveq1d 
 |-  ( x e. D -> ( ( ( _i x. ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) + -u x ) / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) = ( ( _i x. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) )
316 72 112 280 divcan4d 
 |-  ( x e. D -> ( ( _i x. ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) = _i )
317 316 oveq1d 
 |-  ( x e. D -> ( ( ( _i x. ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) + ( -u x / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) = ( _i + ( -u x / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) )
318 300 315 317 3eqtr3rd 
 |-  ( x e. D -> ( _i + ( -u x / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) = ( ( _i x. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) )
319 318 mpteq2ia 
 |-  ( x e. D |-> ( _i + ( -u x / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) ) = ( x e. D |-> ( ( _i x. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) )
320 296 319 eqtrdi 
 |-  ( T. -> ( CC _D ( x e. D |-> ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) ) = ( x e. D |-> ( ( _i x. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) )
321 logf1o 
 |-  log : ( CC \ { 0 } ) -1-1-onto-> ran log
322 f1of 
 |-  ( log : ( CC \ { 0 } ) -1-1-onto-> ran log -> log : ( CC \ { 0 } ) --> ran log )
323 321 322 mp1i 
 |-  ( T. -> log : ( CC \ { 0 } ) --> ran log )
324 snssi 
 |-  ( 0 e. ( -oo (,] 0 ) -> { 0 } C_ ( -oo (,] 0 ) )
325 64 324 ax-mp 
 |-  { 0 } C_ ( -oo (,] 0 )
326 sscon 
 |-  ( { 0 } C_ ( -oo (,] 0 ) -> ( CC \ ( -oo (,] 0 ) ) C_ ( CC \ { 0 } ) )
327 325 326 mp1i 
 |-  ( T. -> ( CC \ ( -oo (,] 0 ) ) C_ ( CC \ { 0 } ) )
328 323 327 feqresmpt 
 |-  ( T. -> ( log |` ( CC \ ( -oo (,] 0 ) ) ) = ( y e. ( CC \ ( -oo (,] 0 ) ) |-> ( log ` y ) ) )
329 328 oveq2d 
 |-  ( T. -> ( CC _D ( log |` ( CC \ ( -oo (,] 0 ) ) ) ) = ( CC _D ( y e. ( CC \ ( -oo (,] 0 ) ) |-> ( log ` y ) ) ) )
330 238 dvlog 
 |-  ( CC _D ( log |` ( CC \ ( -oo (,] 0 ) ) ) ) = ( y e. ( CC \ ( -oo (,] 0 ) ) |-> ( 1 / y ) )
331 329 330 eqtr3di 
 |-  ( T. -> ( CC _D ( y e. ( CC \ ( -oo (,] 0 ) ) |-> ( log ` y ) ) ) = ( y e. ( CC \ ( -oo (,] 0 ) ) |-> ( 1 / y ) ) )
332 fveq2 
 |-  ( y = ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) -> ( log ` y ) = ( log ` ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) )
333 oveq2 
 |-  ( y = ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) -> ( 1 / y ) = ( 1 / ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) )
334 11 11 57 58 70 71 320 331 332 333 dvmptco 
 |-  ( T. -> ( CC _D ( x e. D |-> ( log ` ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) ) ) = ( x e. D |-> ( ( 1 / ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) x. ( ( _i x. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) ) )
335 22 24 reccld 
 |-  ( x e. D -> ( 1 / ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) e. CC )
336 mulcl 
 |-  ( ( _i e. CC /\ ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) e. CC ) -> ( _i x. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) e. CC )
337 13 21 336 sylancr 
 |-  ( x e. CC -> ( _i x. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) e. CC )
338 12 337 syl 
 |-  ( x e. D -> ( _i x. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) e. CC )
339 335 338 112 280 divassd 
 |-  ( x e. D -> ( ( ( 1 / ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) x. ( _i x. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) ) / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) = ( ( 1 / ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) x. ( ( _i x. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) )
340 338 22 24 divrec2d 
 |-  ( x e. D -> ( ( _i x. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) / ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) = ( ( 1 / ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) x. ( _i x. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) ) )
341 72 22 24 divcan4d 
 |-  ( x e. D -> ( ( _i x. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) / ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) = _i )
342 340 341 eqtr3d 
 |-  ( x e. D -> ( ( 1 / ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) x. ( _i x. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) ) = _i )
343 342 oveq1d 
 |-  ( x e. D -> ( ( ( 1 / ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) x. ( _i x. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) ) / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) = ( _i / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) )
344 339 343 eqtr3d 
 |-  ( x e. D -> ( ( 1 / ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) x. ( ( _i x. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) = ( _i / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) )
345 344 mpteq2ia 
 |-  ( x e. D |-> ( ( 1 / ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) x. ( ( _i x. ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) ) = ( x e. D |-> ( _i / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) )
346 334 345 eqtrdi 
 |-  ( T. -> ( CC _D ( x e. D |-> ( log ` ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) ) ) = ( x e. D |-> ( _i / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) )
347 negicn 
 |-  -u _i e. CC
348 347 a1i 
 |-  ( T. -> -u _i e. CC )
349 11 26 27 346 348 dvmptcmul 
 |-  ( T. -> ( CC _D ( x e. D |-> ( -u _i x. ( log ` ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) ) ) ) = ( x e. D |-> ( -u _i x. ( _i / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) ) )
350 349 mptru 
 |-  ( CC _D ( x e. D |-> ( -u _i x. ( log ` ( ( _i x. x ) + ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) ) ) ) = ( x e. D |-> ( -u _i x. ( _i / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) )
351 divass 
 |-  ( ( -u _i e. CC /\ _i e. CC /\ ( ( sqrt ` ( 1 - ( x ^ 2 ) ) ) e. CC /\ ( sqrt ` ( 1 - ( x ^ 2 ) ) ) =/= 0 ) ) -> ( ( -u _i x. _i ) / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) = ( -u _i x. ( _i / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) )
352 347 13 351 mp3an12 
 |-  ( ( ( sqrt ` ( 1 - ( x ^ 2 ) ) ) e. CC /\ ( sqrt ` ( 1 - ( x ^ 2 ) ) ) =/= 0 ) -> ( ( -u _i x. _i ) / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) = ( -u _i x. ( _i / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) )
353 112 280 352 syl2anc 
 |-  ( x e. D -> ( ( -u _i x. _i ) / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) = ( -u _i x. ( _i / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) )
354 13 13 mulneg1i 
 |-  ( -u _i x. _i ) = -u ( _i x. _i )
355 301 negeqi 
 |-  -u ( _i x. _i ) = -u -u 1
356 negneg1e1 
 |-  -u -u 1 = 1
357 354 355 356 3eqtri 
 |-  ( -u _i x. _i ) = 1
358 357 oveq1i 
 |-  ( ( -u _i x. _i ) / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) = ( 1 / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) )
359 353 358 eqtr3di 
 |-  ( x e. D -> ( -u _i x. ( _i / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) = ( 1 / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) )
360 359 mpteq2ia 
 |-  ( x e. D |-> ( -u _i x. ( _i / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) ) = ( x e. D |-> ( 1 / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) )
361 9 350 360 3eqtri 
 |-  ( CC _D ( arcsin |` D ) ) = ( x e. D |-> ( 1 / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) )