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 D arccos 1 1 = x 1 1 1 1 x 2

Proof

Step Hyp Ref Expression
1 acosf arccos :
2 1 a1i arccos :
3 ioossre 1 1
4 ax-resscn
5 3 4 sstri 1 1
6 5 a1i 1 1
7 2 6 feqresmpt arccos 1 1 = x 1 1 arccos x
8 7 oveq2d D arccos 1 1 = dx 1 1 arccos x d x
9 eqid TopOpen fld = TopOpen fld
10 reelprrecn
11 10 a1i
12 9 recld2 Clsd TopOpen fld
13 neg1rr 1
14 iocmnfcld 1 −∞ 1 Clsd topGen ran .
15 13 14 ax-mp −∞ 1 Clsd topGen ran .
16 1re 1
17 icopnfcld 1 1 +∞ Clsd topGen ran .
18 16 17 ax-mp 1 +∞ Clsd topGen ran .
19 uncld −∞ 1 Clsd topGen ran . 1 +∞ Clsd topGen ran . −∞ 1 1 +∞ Clsd topGen ran .
20 15 18 19 mp2an −∞ 1 1 +∞ Clsd topGen ran .
21 9 tgioo2 topGen ran . = TopOpen fld 𝑡
22 21 fveq2i Clsd topGen ran . = Clsd TopOpen fld 𝑡
23 20 22 eleqtri −∞ 1 1 +∞ Clsd TopOpen fld 𝑡
24 restcldr Clsd TopOpen fld −∞ 1 1 +∞ Clsd TopOpen fld 𝑡 −∞ 1 1 +∞ Clsd TopOpen fld
25 12 23 24 mp2an −∞ 1 1 +∞ Clsd TopOpen fld
26 9 cnfldtopon TopOpen fld TopOn
27 26 toponunii = TopOpen fld
28 27 cldopn −∞ 1 1 +∞ Clsd TopOpen fld −∞ 1 1 +∞ TopOpen fld
29 25 28 mp1i −∞ 1 1 +∞ TopOpen fld
30 incom −∞ 1 1 +∞ = −∞ 1 1 +∞
31 eqid −∞ 1 1 +∞ = −∞ 1 1 +∞
32 31 asindmre −∞ 1 1 +∞ = 1 1
33 30 32 eqtri −∞ 1 1 +∞ = 1 1
34 33 a1i −∞ 1 1 +∞ = 1 1
35 eldifi x −∞ 1 1 +∞ x
36 acoscl x arccos x
37 35 36 syl x −∞ 1 1 +∞ arccos x
38 37 adantl x −∞ 1 1 +∞ arccos x
39 ovexd x −∞ 1 1 +∞ 1 1 x 2 V
40 difssd −∞ 1 1 +∞
41 2 40 feqresmpt arccos −∞ 1 1 +∞ = x −∞ 1 1 +∞ arccos x
42 41 oveq2d D arccos −∞ 1 1 +∞ = dx −∞ 1 1 +∞ arccos x d x
43 31 dvacos D arccos −∞ 1 1 +∞ = x −∞ 1 1 +∞ 1 1 x 2
44 42 43 eqtr3di dx −∞ 1 1 +∞ arccos x d x = x −∞ 1 1 +∞ 1 1 x 2
45 9 11 29 34 38 39 44 dvmptres3 dx 1 1 arccos x d x = x 1 1 1 1 x 2
46 8 45 eqtrd D arccos 1 1 = x 1 1 1 1 x 2
47 46 mptru D arccos 1 1 = x 1 1 1 1 x 2