Metamath Proof Explorer


Theorem dvacos

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

Ref Expression
Hypothesis dvasin.d D = −∞ 1 1 +∞
Assertion dvacos D arccos D = x D 1 1 x 2

Proof

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