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 tgioo4 ⊢ 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