Metamath Proof Explorer

Theorem dvacos

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

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

Proof

Step Hyp Ref Expression
1 dvasin.d 
 |-  D = ( CC \ ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) )
2 df-acos 
 |-  arccos = ( x e. CC |-> ( ( _pi / 2 ) - ( arcsin ` x ) ) )
3 2 reseq1i 
 |-  ( arccos |` D ) = ( ( x e. CC |-> ( ( _pi / 2 ) - ( arcsin ` x ) ) ) |` 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 |-> ( ( _pi / 2 ) - ( arcsin ` x ) ) ) |` D ) = ( x e. D |-> ( ( _pi / 2 ) - ( arcsin ` x ) ) ) )
7 5 6 ax-mp 
 |-  ( ( x e. CC |-> ( ( _pi / 2 ) - ( arcsin ` x ) ) ) |` D ) = ( x e. D |-> ( ( _pi / 2 ) - ( arcsin ` x ) ) )
8 3 7 eqtri 
 |-  ( arccos |` D ) = ( x e. D |-> ( ( _pi / 2 ) - ( arcsin ` x ) ) )
9 8 oveq2i 
 |-  ( CC _D ( arccos |` D ) ) = ( CC _D ( x e. D |-> ( ( _pi / 2 ) - ( arcsin ` x ) ) ) )
10 cnelprrecn 
 |-  CC e. { RR , CC }
11 10 a1i 
 |-  ( T. -> CC e. { RR , CC } )
12 halfpire 
 |-  ( _pi / 2 ) e. RR
13 12 recni 
 |-  ( _pi / 2 ) e. CC
14 13 a1i 
 |-  ( ( T. /\ x e. D ) -> ( _pi / 2 ) e. CC )
15 c0ex 
 |-  0 e. _V
16 15 a1i 
 |-  ( ( T. /\ x e. D ) -> 0 e. _V )
17 13 a1i 
 |-  ( ( T. /\ x e. CC ) -> ( _pi / 2 ) e. CC )
18 15 a1i 
 |-  ( ( T. /\ x e. CC ) -> 0 e. _V )
19 13 a1i 
 |-  ( T. -> ( _pi / 2 ) e. CC )
20 11 19 dvmptc 
 |-  ( T. -> ( CC _D ( x e. CC |-> ( _pi / 2 ) ) ) = ( x e. CC |-> 0 ) )
21 5 a1i 
 |-  ( T. -> D C_ CC )
22 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
23 22 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
24 23 toponrestid 
 |-  ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
25 22 recld2 
 |-  RR e. ( Clsd ` ( TopOpen ` CCfld ) )
26 neg1rr 
 |-  -u 1 e. RR
27 iocmnfcld 
 |-  ( -u 1 e. RR -> ( -oo (,] -u 1 ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
28 26 27 ax-mp 
 |-  ( -oo (,] -u 1 ) e. ( Clsd ` ( topGen ` ran (,) ) )
29 tgioo4 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
30 29 fveq2i 
 |-  ( Clsd ` ( topGen ` ran (,) ) ) = ( Clsd ` ( ( TopOpen ` CCfld ) |`t RR ) )
31 28 30 eleqtri 
 |-  ( -oo (,] -u 1 ) e. ( Clsd ` ( ( TopOpen ` CCfld ) |`t RR ) )
32 restcldr 
 |-  ( ( RR e. ( Clsd ` ( TopOpen ` CCfld ) ) /\ ( -oo (,] -u 1 ) e. ( Clsd ` ( ( TopOpen ` CCfld ) |`t RR ) ) ) -> ( -oo (,] -u 1 ) e. ( Clsd ` ( TopOpen ` CCfld ) ) )
33 25 31 32 mp2an 
 |-  ( -oo (,] -u 1 ) e. ( Clsd ` ( TopOpen ` CCfld ) )
34 1re 
 |-  1 e. RR
35 icopnfcld 
 |-  ( 1 e. RR -> ( 1 [,) +oo ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
36 34 35 ax-mp 
 |-  ( 1 [,) +oo ) e. ( Clsd ` ( topGen ` ran (,) ) )
37 36 30 eleqtri 
 |-  ( 1 [,) +oo ) e. ( Clsd ` ( ( TopOpen ` CCfld ) |`t RR ) )
38 restcldr 
 |-  ( ( RR e. ( Clsd ` ( TopOpen ` CCfld ) ) /\ ( 1 [,) +oo ) e. ( Clsd ` ( ( TopOpen ` CCfld ) |`t RR ) ) ) -> ( 1 [,) +oo ) e. ( Clsd ` ( TopOpen ` CCfld ) ) )
39 25 37 38 mp2an 
 |-  ( 1 [,) +oo ) e. ( Clsd ` ( TopOpen ` CCfld ) )
40 uncld 
 |-  ( ( ( -oo (,] -u 1 ) e. ( Clsd ` ( TopOpen ` CCfld ) ) /\ ( 1 [,) +oo ) e. ( Clsd ` ( TopOpen ` CCfld ) ) ) -> ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) e. ( Clsd ` ( TopOpen ` CCfld ) ) )
41 33 39 40 mp2an 
 |-  ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) e. ( Clsd ` ( TopOpen ` CCfld ) )
42 23 toponunii 
 |-  CC = U. ( TopOpen ` CCfld )
43 42 cldopn 
 |-  ( ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) e. ( Clsd ` ( TopOpen ` CCfld ) ) -> ( CC \ ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) ) e. ( TopOpen ` CCfld ) )
44 41 43 ax-mp 
 |-  ( CC \ ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) ) e. ( TopOpen ` CCfld )
45 1 44 eqeltri 
 |-  D e. ( TopOpen ` CCfld )
46 45 a1i 
 |-  ( T. -> D e. ( TopOpen ` CCfld ) )
47 11 17 18 20 21 24 22 46 dvmptres 
 |-  ( T. -> ( CC _D ( x e. D |-> ( _pi / 2 ) ) ) = ( x e. D |-> 0 ) )
48 5 sseli 
 |-  ( x e. D -> x e. CC )
49 asincl 
 |-  ( x e. CC -> ( arcsin ` x ) e. CC )
50 48 49 syl 
 |-  ( x e. D -> ( arcsin ` x ) e. CC )
51 50 adantl 
 |-  ( ( T. /\ x e. D ) -> ( arcsin ` x ) e. CC )
52 ovexd 
 |-  ( ( T. /\ x e. D ) -> ( 1 / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) e. _V )
53 asinf 
 |-  arcsin : CC --> CC
54 53 a1i 
 |-  ( T. -> arcsin : CC --> CC )
55 54 21 feqresmpt 
 |-  ( T. -> ( arcsin |` D ) = ( x e. D |-> ( arcsin ` x ) ) )
56 55 oveq2d 
 |-  ( T. -> ( CC _D ( arcsin |` D ) ) = ( CC _D ( x e. D |-> ( arcsin ` x ) ) ) )
57 1 dvasin 
 |-  ( CC _D ( arcsin |` D ) ) = ( x e. D |-> ( 1 / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) )
58 56 57 eqtr3di 
 |-  ( T. -> ( CC _D ( x e. D |-> ( arcsin ` x ) ) ) = ( x e. D |-> ( 1 / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) )
59 11 14 16 47 51 52 58 dvmptsub 
 |-  ( T. -> ( CC _D ( x e. D |-> ( ( _pi / 2 ) - ( arcsin ` x ) ) ) ) = ( x e. D |-> ( 0 - ( 1 / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) ) )
60 59 mptru 
 |-  ( CC _D ( x e. D |-> ( ( _pi / 2 ) - ( arcsin ` x ) ) ) ) = ( x e. D |-> ( 0 - ( 1 / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) )
61 df-neg 
 |-  -u ( 1 / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) = ( 0 - ( 1 / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) )
62 1cnd 
 |-  ( x e. D -> 1 e. CC )
63 ax-1cn 
 |-  1 e. CC
64 48 sqcld 
 |-  ( x e. D -> ( x ^ 2 ) e. CC )
65 subcl 
 |-  ( ( 1 e. CC /\ ( x ^ 2 ) e. CC ) -> ( 1 - ( x ^ 2 ) ) e. CC )
66 63 64 65 sylancr 
 |-  ( x e. D -> ( 1 - ( x ^ 2 ) ) e. CC )
67 66 sqrtcld 
 |-  ( x e. D -> ( sqrt ` ( 1 - ( x ^ 2 ) ) ) e. CC )
68 eldifn 
 |-  ( x e. ( CC \ ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) ) -> -. x e. ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) )
69 68 1 eleq2s 
 |-  ( x e. D -> -. x e. ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) )
70 mnfxr 
 |-  -oo e. RR*
71 26 rexri 
 |-  -u 1 e. RR*
72 mnflt 
 |-  ( -u 1 e. RR -> -oo < -u 1 )
73 26 72 ax-mp 
 |-  -oo < -u 1
74 ubioc1 
 |-  ( ( -oo e. RR* /\ -u 1 e. RR* /\ -oo < -u 1 ) -> -u 1 e. ( -oo (,] -u 1 ) )
75 70 71 73 74 mp3an 
 |-  -u 1 e. ( -oo (,] -u 1 )
76 eleq1 
 |-  ( x = -u 1 -> ( x e. ( -oo (,] -u 1 ) <-> -u 1 e. ( -oo (,] -u 1 ) ) )
77 75 76 mpbiri 
 |-  ( x = -u 1 -> x e. ( -oo (,] -u 1 ) )
78 34 rexri 
 |-  1 e. RR*
79 pnfxr 
 |-  +oo e. RR*
80 ltpnf 
 |-  ( 1 e. RR -> 1 < +oo )
81 34 80 ax-mp 
 |-  1 < +oo
82 lbico1 
 |-  ( ( 1 e. RR* /\ +oo e. RR* /\ 1 < +oo ) -> 1 e. ( 1 [,) +oo ) )
83 78 79 81 82 mp3an 
 |-  1 e. ( 1 [,) +oo )
84 eleq1 
 |-  ( x = 1 -> ( x e. ( 1 [,) +oo ) <-> 1 e. ( 1 [,) +oo ) ) )
85 83 84 mpbiri 
 |-  ( x = 1 -> x e. ( 1 [,) +oo ) )
86 77 85 orim12i 
 |-  ( ( x = -u 1 \/ x = 1 ) -> ( x e. ( -oo (,] -u 1 ) \/ x e. ( 1 [,) +oo ) ) )
87 86 orcoms 
 |-  ( ( x = 1 \/ x = -u 1 ) -> ( x e. ( -oo (,] -u 1 ) \/ x e. ( 1 [,) +oo ) ) )
88 elun 
 |-  ( x e. ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) <-> ( x e. ( -oo (,] -u 1 ) \/ x e. ( 1 [,) +oo ) ) )
89 87 88 sylibr 
 |-  ( ( x = 1 \/ x = -u 1 ) -> x e. ( ( -oo (,] -u 1 ) u. ( 1 [,) +oo ) ) )
90 69 89 nsyl 
 |-  ( x e. D -> -. ( x = 1 \/ x = -u 1 ) )
91 sq1 
 |-  ( 1 ^ 2 ) = 1
92 1cnd 
 |-  ( ( x e. CC /\ ( sqrt ` ( 1 - ( x ^ 2 ) ) ) = 0 ) -> 1 e. CC )
93 sqcl 
 |-  ( x e. CC -> ( x ^ 2 ) e. CC )
94 93 adantr 
 |-  ( ( x e. CC /\ ( sqrt ` ( 1 - ( x ^ 2 ) ) ) = 0 ) -> ( x ^ 2 ) e. CC )
95 63 93 65 sylancr 
 |-  ( x e. CC -> ( 1 - ( x ^ 2 ) ) e. CC )
96 95 adantr 
 |-  ( ( x e. CC /\ ( sqrt ` ( 1 - ( x ^ 2 ) ) ) = 0 ) -> ( 1 - ( x ^ 2 ) ) e. CC )
97 simpr 
 |-  ( ( x e. CC /\ ( sqrt ` ( 1 - ( x ^ 2 ) ) ) = 0 ) -> ( sqrt ` ( 1 - ( x ^ 2 ) ) ) = 0 )
98 96 97 sqr00d 
 |-  ( ( x e. CC /\ ( sqrt ` ( 1 - ( x ^ 2 ) ) ) = 0 ) -> ( 1 - ( x ^ 2 ) ) = 0 )
99 92 94 98 subeq0d 
 |-  ( ( x e. CC /\ ( sqrt ` ( 1 - ( x ^ 2 ) ) ) = 0 ) -> 1 = ( x ^ 2 ) )
100 91 99 eqtr2id 
 |-  ( ( x e. CC /\ ( sqrt ` ( 1 - ( x ^ 2 ) ) ) = 0 ) -> ( x ^ 2 ) = ( 1 ^ 2 ) )
101 100 ex 
 |-  ( x e. CC -> ( ( sqrt ` ( 1 - ( x ^ 2 ) ) ) = 0 -> ( x ^ 2 ) = ( 1 ^ 2 ) ) )
102 sqeqor 
 |-  ( ( x e. CC /\ 1 e. CC ) -> ( ( x ^ 2 ) = ( 1 ^ 2 ) <-> ( x = 1 \/ x = -u 1 ) ) )
103 63 102 mpan2 
 |-  ( x e. CC -> ( ( x ^ 2 ) = ( 1 ^ 2 ) <-> ( x = 1 \/ x = -u 1 ) ) )
104 101 103 sylibd 
 |-  ( x e. CC -> ( ( sqrt ` ( 1 - ( x ^ 2 ) ) ) = 0 -> ( x = 1 \/ x = -u 1 ) ) )
105 104 necon3bd 
 |-  ( x e. CC -> ( -. ( x = 1 \/ x = -u 1 ) -> ( sqrt ` ( 1 - ( x ^ 2 ) ) ) =/= 0 ) )
106 48 90 105 sylc 
 |-  ( x e. D -> ( sqrt ` ( 1 - ( x ^ 2 ) ) ) =/= 0 )
107 62 67 106 divnegd 
 |-  ( x e. D -> -u ( 1 / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) = ( -u 1 / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) )
108 61 107 eqtr3id 
 |-  ( x e. D -> ( 0 - ( 1 / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) = ( -u 1 / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) )
109 108 mpteq2ia 
 |-  ( x e. D |-> ( 0 - ( 1 / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) ) ) = ( x e. D |-> ( -u 1 / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) )
110 9 60 109 3eqtri 
 |-  ( CC _D ( arccos |` D ) ) = ( x e. D |-> ( -u 1 / ( sqrt ` ( 1 - ( x ^ 2 ) ) ) ) )