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 ⊢ℂDarccos↾D=x∈D⟼−11−x2

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 ⊢ℂDarccos↾D=dx∈Dπ2−arcsin⁡xdℂ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∈ℂπ2dℂ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π2dℂ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→11−x2∈V
53 asinf ⊢arcsin:ℂ⟶ℂ
54 53 a1i ⊢⊤→arcsin:ℂ⟶ℂ
55 54 21 feqresmpt ⊢⊤→arcsin↾D=x∈D⟼arcsin⁡x
56 55 oveq2d ⊢⊤→ℂDarcsin↾D=dx∈Darcsin⁡xdℂx
57 1 dvasin ⊢ℂDarcsin↾D=x∈D⟼11−x2
58 56 57 eqtr3di ⊢⊤→dx∈Darcsin⁡xdℂx=x∈D⟼11−x2
59 11 14 16 47 51 52 58 dvmptsub ⊢⊤→dx∈Dπ2−arcsin⁡xdℂx=x∈D⟼0−11−x2
60 59 mptru ⊢dx∈Dπ2−arcsin⁡xdℂx=x∈D⟼0−11−x2
61 df-neg ⊢−11−x2=0−11−x2
62 1cnd ⊢x∈D→1∈ℂ
63 ax-1cn ⊢1∈ℂ
64 48 sqcld ⊢x∈D→x2∈ℂ
65 subcl ⊢1∈ℂ∧x2∈ℂ→1−x2∈ℂ
66 63 64 65 sylancr ⊢x∈D→1−x2∈ℂ
67 66 sqrtcld ⊢x∈D→1−x2∈ℂ
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 ⊢12=1
92 1cnd ⊢x∈ℂ∧1−x2=0→1∈ℂ
93 sqcl ⊢x∈ℂ→x2∈ℂ
94 93 adantr ⊢x∈ℂ∧1−x2=0→x2∈ℂ
95 63 93 65 sylancr ⊢x∈ℂ→1−x2∈ℂ
96 95 adantr ⊢x∈ℂ∧1−x2=0→1−x2∈ℂ
97 simpr ⊢x∈ℂ∧1−x2=0→1−x2=0
98 96 97 sqr00d ⊢x∈ℂ∧1−x2=0→1−x2=0
99 92 94 98 subeq0d ⊢x∈ℂ∧1−x2=0→1=x2
100 91 99 eqtr2id ⊢x∈ℂ∧1−x2=0→x2=12
101 100 ex ⊢x∈ℂ→1−x2=0→x2=12
102 sqeqor ⊢x∈ℂ∧1∈ℂ→x2=12↔x=1∨x=−1
103 63 102 mpan2 ⊢x∈ℂ→x2=12↔x=1∨x=−1
104 101 103 sylibd ⊢x∈ℂ→1−x2=0→x=1∨x=−1
105 104 necon3bd ⊢x∈ℂ→¬x=1∨x=−1→1−x2≠0
106 48 90 105 sylc ⊢x∈D→1−x2≠0
107 62 67 106 divnegd ⊢x∈D→−11−x2=−11−x2
108 61 107 eqtr3id ⊢x∈D→0−11−x2=−11−x2
109 108 mpteq2ia ⊢x∈D⟼0−11−x2=x∈D⟼−11−x2
110 9 60 109 3eqtri ⊢ℂDarccos↾D=x∈D⟼−11−x2