Metamath Proof Explorer

Theorem dvreacos

Description: Real derivative of arccosine. (Contributed by Brendan Leahy, 3-Aug-2017) (Proof shortened by Brendan Leahy, 18-Dec-2018)

Ref Expression
Assertion dvreacos 
|- ( RR _D ( arccos |` ( -u 1 (,) 1 ) ) ) = ( x e. ( -u 1 (,) 1 ) |-> ( -u 1 / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 acosf 
 |-  arccos : CC --> CC
2 1 a1i 
 |-  ( T. -> arccos : CC --> CC )
3 ioossre 
 |-  ( -u 1 (,) 1 ) C_ RR
4 ax-resscn 
 |-  RR C_ CC
5 3 4 sstri 
 |-  ( -u 1 (,) 1 ) C_ CC
6 5 a1i 
 |-  ( T. -> ( -u 1 (,) 1 ) C_ CC )
7 2 6 feqresmpt 
 |-  ( T. -> ( arccos |` ( -u 1 (,) 1 ) ) = ( x e. ( -u 1 (,) 1 ) |-> ( arccos ` x ) ) )
8 7 oveq2d 
 |-  ( T. -> ( RR _D ( arccos |` ( -u 1 (,) 1 ) ) ) = ( RR _D ( x e. ( -u 1 (,) 1 ) |-> ( arccos ` x ) ) ) )
9 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
10 reelprrecn 
 |-  RR e. { RR , CC }
11 10 a1i 
 |-  ( T. -> RR e. { RR , CC } )
12 9 recld2 
 |-  RR e. ( Clsd ` ( TopOpen ` CCfld ) )
13 neg1rr 
 |-  -u 1 e. RR
14 iocmnfcld 
 |-  ( -u 1 e. RR -> ( -oo (,] -u 1 ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
15 13 14 ax-mp 
 |-  ( -oo (,] -u 1 ) e. ( Clsd ` ( topGen ` ran (,) ) )
16 1re 
 |-  1 e. RR
17 icopnfcld 
 |-  ( 1 e. RR -> ( 1 [,) +oo ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
18 16 17 ax-mp 
 |-  ( 1 [,) +oo ) e. ( Clsd ` ( topGen ` ran (,) ) )
19 uncld 
 |-  ( ( ( -oo (,] -u 1 ) e. ( Clsd ` ( topGen ` ran (,) ) ) /\ ( 1 [,) +oo ) e. ( Clsd ` ( topGen ` ran (,) ) ) ) -> ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
20 15 18 19 mp2an 
 |-  ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) e. ( Clsd ` ( topGen ` ran (,) ) )
21 9 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
22 21 fveq2i 
 |-  ( Clsd ` ( topGen ` ran (,) ) ) = ( Clsd ` ( ( TopOpen ` CCfld ) |`t RR ) )
23 20 22 eleqtri 
 |-  ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) e. ( Clsd ` ( ( TopOpen ` CCfld ) |`t RR ) )
24 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 ) ) )
25 12 23 24 mp2an 
 |-  ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) e. ( Clsd ` ( TopOpen ` CCfld ) )
26 9 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
27 26 toponunii 
 |-  CC = U. ( TopOpen ` CCfld )
28 27 cldopn 
 |-  ( ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) e. ( Clsd ` ( TopOpen ` CCfld ) ) -> ( CC \ ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) ) e. ( TopOpen ` CCfld ) )
29 25 28 mp1i 
 |-  ( T. -> ( CC \ ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) ) e. ( TopOpen ` CCfld ) )
30 incom 
 |-  ( RR i^i ( CC \ ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) ) ) = ( ( CC \ ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) ) i^i RR )
31 eqid 
 |-  ( CC \ ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) ) = ( CC \ ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) )
32 31 asindmre 
 |-  ( ( CC \ ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) ) i^i RR ) = ( -u 1 (,) 1 )
33 30 32 eqtri 
 |-  ( RR i^i ( CC \ ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) ) ) = ( -u 1 (,) 1 )
34 33 a1i 
 |-  ( T. -> ( RR i^i ( CC \ ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) ) ) = ( -u 1 (,) 1 ) )
35 eldifi 
 |-  ( x e. ( CC \ ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) ) -> x e. CC )
36 acoscl 
 |-  ( x e. CC -> ( arccos ` x ) e. CC )
37 35 36 syl 
 |-  ( x e. ( CC \ ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) ) -> ( arccos ` x ) e. CC )
38 37 adantl 
 |-  ( ( T. /\ x e. ( CC \ ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) ) ) -> ( arccos ` x ) e. CC )
39 ovexd 
 |-  ( ( T. /\ x e. ( CC \ ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) ) ) -> ( -u 1 / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) e. _V )
40 difssd 
 |-  ( T. -> ( CC \ ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) ) C_ CC )
41 2 40 feqresmpt 
 |-  ( T. -> ( arccos |` ( CC \ ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) ) ) = ( x e. ( CC \ ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) ) |-> ( arccos ` x ) ) )
42 41 oveq2d 
 |-  ( T. -> ( CC _D ( arccos |` ( CC \ ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) ) ) ) = ( CC _D ( x e. ( CC \ ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) ) |-> ( arccos ` x ) ) ) )
43 31 dvacos 
 |-  ( CC _D ( arccos |` ( CC \ ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) ) ) ) = ( x e. ( CC \ ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) ) |-> ( -u 1 / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) )
44 42 43 eqtr3di 
 |-  ( T. -> ( CC _D ( x e. ( CC \ ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) ) |-> ( arccos ` x ) ) ) = ( x e. ( CC \ ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) ) |-> ( -u 1 / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) )
45 9 11 29 34 38 39 44 dvmptres3 
 |-  ( T. -> ( RR _D ( x e. ( -u 1 (,) 1 ) |-> ( arccos ` x ) ) ) = ( x e. ( -u 1 (,) 1 ) |-> ( -u 1 / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) )
46 8 45 eqtrd 
 |-  ( T. -> ( RR _D ( arccos |` ( -u 1 (,) 1 ) ) ) = ( x e. ( -u 1 (,) 1 ) |-> ( -u 1 / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) )
47 46 mptru 
 |-  ( RR _D ( arccos |` ( -u 1 (,) 1 ) ) ) = ( x e. ( -u 1 (,) 1 ) |-> ( -u 1 / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) )