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 22 tgioo2
 |-  ( 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 ) ) ) ) )