Metamath Proof Explorer

Theorem dvacos

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

Ref Expression
Hypothesis dvasin.d ⊢ 𝐷 = ( ℂ ∖ ( ( -∞ (,] - 1 ) ∪ ( 1 [,) +∞ ) ) )
Assertion dvacos ( ℂ D ( arccos ↾ 𝐷 ) ) = ( 𝑥 ∈ 𝐷 ↦ ( - 1 / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dvasin.d ⊢ 𝐷 = ( ℂ ∖ ( ( -∞ (,] - 1 ) ∪ ( 1 [,) +∞ ) ) )
2 df-acos ⊢ arccos = ( 𝑥 ∈ ℂ ↦ ( ( π / 2 ) − ( arcsin ‘ 𝑥 ) ) )
3 2 reseq1i ⊢ ( arccos ↾ 𝐷 ) = ( ( 𝑥 ∈ ℂ ↦ ( ( π / 2 ) − ( arcsin ‘ 𝑥 ) ) ) ↾ 𝐷 )
4 difss ⊢ ( ℂ ∖ ( ( -∞ (,] - 1 ) ∪ ( 1 [,) +∞ ) ) ) ⊆ ℂ
5 1 4 eqsstri ⊢ 𝐷 ⊆ ℂ
6 resmpt ⊢ ( 𝐷 ⊆ ℂ → ( ( 𝑥 ∈ ℂ ↦ ( ( π / 2 ) − ( arcsin ‘ 𝑥 ) ) ) ↾ 𝐷 ) = ( 𝑥 ∈ 𝐷 ↦ ( ( π / 2 ) − ( arcsin ‘ 𝑥 ) ) ) )
7 5 6 ax-mp ⊢ ( ( 𝑥 ∈ ℂ ↦ ( ( π / 2 ) − ( arcsin ‘ 𝑥 ) ) ) ↾ 𝐷 ) = ( 𝑥 ∈ 𝐷 ↦ ( ( π / 2 ) − ( arcsin ‘ 𝑥 ) ) )
8 3 7 eqtri ⊢ ( arccos ↾ 𝐷 ) = ( 𝑥 ∈ 𝐷 ↦ ( ( π / 2 ) − ( arcsin ‘ 𝑥 ) ) )
9 8 oveq2i ⊢ ( ℂ D ( arccos ↾ 𝐷 ) ) = ( ℂ D ( 𝑥 ∈ 𝐷 ↦ ( ( π / 2 ) − ( arcsin ‘ 𝑥 ) ) ) )
10 cnelprrecn ⊢ ℂ ∈ { ℝ , ℂ }
11 10 a1i ⊢ ( ⊤ → ℂ ∈ { ℝ , ℂ } )
12 halfpire ⊢ ( π / 2 ) ∈ ℝ
13 12 recni ⊢ ( π / 2 ) ∈ ℂ
14 13 a1i ⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐷 ) → ( π / 2 ) ∈ ℂ )
15 c0ex ⊢ 0 ∈ V
16 15 a1i ⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐷 ) → 0 ∈ V )
17 13 a1i ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( π / 2 ) ∈ ℂ )
18 15 a1i ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → 0 ∈ V )
19 13 a1i ⊢ ( ⊤ → ( π / 2 ) ∈ ℂ )
20 11 19 dvmptc ⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( π / 2 ) ) ) = ( 𝑥 ∈ ℂ ↦ 0 ) )
21 5 a1i ⊢ ( ⊤ → 𝐷 ⊆ ℂ )
22 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
23 22 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
24 23 toponrestid ⊢ ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
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 ) ↾t ℝ )
30 29 fveq2i ⊢ ( Clsd ‘ ( topGen ‘ ran (,) ) ) = ( Clsd ‘ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) )
31 28 30 eleqtri ⊢ ( -∞ (,] - 1 ) ∈ ( Clsd ‘ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) )
32 restcldr ⊢ ( ( ℝ ∈ ( Clsd ‘ ( TopOpen ‘ ℂfld ) ) ∧ ( -∞ (,] - 1 ) ∈ ( Clsd ‘ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ) → ( -∞ (,] - 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 ) ↾t ℝ ) )
38 restcldr ⊢ ( ( ℝ ∈ ( Clsd ‘ ( TopOpen ‘ ℂfld ) ) ∧ ( 1 [,) +∞ ) ∈ ( Clsd ‘ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ) → ( 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 ⊢ 𝐷 ∈ ( TopOpen ‘ ℂfld )
46 45 a1i ⊢ ( ⊤ → 𝐷 ∈ ( TopOpen ‘ ℂfld ) )
47 11 17 18 20 21 24 22 46 dvmptres ⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ 𝐷 ↦ ( π / 2 ) ) ) = ( 𝑥 ∈ 𝐷 ↦ 0 ) )
48 5 sseli ⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ∈ ℂ )
49 asincl ⊢ ( 𝑥 ∈ ℂ → ( arcsin ‘ 𝑥 ) ∈ ℂ )
50 48 49 syl ⊢ ( 𝑥 ∈ 𝐷 → ( arcsin ‘ 𝑥 ) ∈ ℂ )
51 50 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐷 ) → ( arcsin ‘ 𝑥 ) ∈ ℂ )
52 ovexd ⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐷 ) → ( 1 / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∈ V )
53 asinf ⊢ arcsin : ℂ ⟶ ℂ
54 53 a1i ⊢ ( ⊤ → arcsin : ℂ ⟶ ℂ )
55 54 21 feqresmpt ⊢ ( ⊤ → ( arcsin ↾ 𝐷 ) = ( 𝑥 ∈ 𝐷 ↦ ( arcsin ‘ 𝑥 ) ) )
56 55 oveq2d ⊢ ( ⊤ → ( ℂ D ( arcsin ↾ 𝐷 ) ) = ( ℂ D ( 𝑥 ∈ 𝐷 ↦ ( arcsin ‘ 𝑥 ) ) ) )
57 1 dvasin ⊢ ( ℂ D ( arcsin ↾ 𝐷 ) ) = ( 𝑥 ∈ 𝐷 ↦ ( 1 / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) )
58 56 57 eqtr3di ⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ 𝐷 ↦ ( arcsin ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( 1 / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) )
59 11 14 16 47 51 52 58 dvmptsub ⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ 𝐷 ↦ ( ( π / 2 ) − ( arcsin ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( 0 − ( 1 / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ) )
60 59 mptru ⊢ ( ℂ D ( 𝑥 ∈ 𝐷 ↦ ( ( π / 2 ) − ( arcsin ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( 0 − ( 1 / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) )
61 df-neg ⊢ - ( 1 / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) = ( 0 − ( 1 / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) )
62 1cnd ⊢ ( 𝑥 ∈ 𝐷 → 1 ∈ ℂ )
63 ax-1cn ⊢ 1 ∈ ℂ
64 48 sqcld ⊢ ( 𝑥 ∈ 𝐷 → ( 𝑥 ↑ 2 ) ∈ ℂ )
65 subcl ⊢ ( ( 1 ∈ ℂ ∧ ( 𝑥 ↑ 2 ) ∈ ℂ ) → ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ℂ )
66 63 64 65 sylancr ⊢ ( 𝑥 ∈ 𝐷 → ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ℂ )
67 66 sqrtcld ⊢ ( 𝑥 ∈ 𝐷 → ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ∈ ℂ )
68 eldifn ⊢ ( 𝑥 ∈ ( ℂ ∖ ( ( -∞ (,] - 1 ) ∪ ( 1 [,) +∞ ) ) ) → ¬ 𝑥 ∈ ( ( -∞ (,] - 1 ) ∪ ( 1 [,) +∞ ) ) )
69 68 1 eleq2s ⊢ ( 𝑥 ∈ 𝐷 → ¬ 𝑥 ∈ ( ( -∞ (,] - 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 ⊢ ( 𝑥 = - 1 → ( 𝑥 ∈ ( -∞ (,] - 1 ) ↔ - 1 ∈ ( -∞ (,] - 1 ) ) )
77 75 76 mpbiri ⊢ ( 𝑥 = - 1 → 𝑥 ∈ ( -∞ (,] - 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 ⊢ ( 𝑥 = 1 → ( 𝑥 ∈ ( 1 [,) +∞ ) ↔ 1 ∈ ( 1 [,) +∞ ) ) )
85 83 84 mpbiri ⊢ ( 𝑥 = 1 → 𝑥 ∈ ( 1 [,) +∞ ) )
86 77 85 orim12i ⊢ ( ( 𝑥 = - 1 ∨ 𝑥 = 1 ) → ( 𝑥 ∈ ( -∞ (,] - 1 ) ∨ 𝑥 ∈ ( 1 [,) +∞ ) ) )
87 86 orcoms ⊢ ( ( 𝑥 = 1 ∨ 𝑥 = - 1 ) → ( 𝑥 ∈ ( -∞ (,] - 1 ) ∨ 𝑥 ∈ ( 1 [,) +∞ ) ) )
88 elun ⊢ ( 𝑥 ∈ ( ( -∞ (,] - 1 ) ∪ ( 1 [,) +∞ ) ) ↔ ( 𝑥 ∈ ( -∞ (,] - 1 ) ∨ 𝑥 ∈ ( 1 [,) +∞ ) ) )
89 87 88 sylibr ⊢ ( ( 𝑥 = 1 ∨ 𝑥 = - 1 ) → 𝑥 ∈ ( ( -∞ (,] - 1 ) ∪ ( 1 [,) +∞ ) ) )
90 69 89 nsyl ⊢ ( 𝑥 ∈ 𝐷 → ¬ ( 𝑥 = 1 ∨ 𝑥 = - 1 ) )
91 sq1 ⊢ ( 1 ↑ 2 ) = 1
92 1cnd ⊢ ( ( 𝑥 ∈ ℂ ∧ ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) = 0 ) → 1 ∈ ℂ )
93 sqcl ⊢ ( 𝑥 ∈ ℂ → ( 𝑥 ↑ 2 ) ∈ ℂ )
94 93 adantr ⊢ ( ( 𝑥 ∈ ℂ ∧ ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) = 0 ) → ( 𝑥 ↑ 2 ) ∈ ℂ )
95 63 93 65 sylancr ⊢ ( 𝑥 ∈ ℂ → ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ℂ )
96 95 adantr ⊢ ( ( 𝑥 ∈ ℂ ∧ ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) = 0 ) → ( 1 − ( 𝑥 ↑ 2 ) ) ∈ ℂ )
97 simpr ⊢ ( ( 𝑥 ∈ ℂ ∧ ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) = 0 ) → ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) = 0 )
98 96 97 sqr00d ⊢ ( ( 𝑥 ∈ ℂ ∧ ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) = 0 ) → ( 1 − ( 𝑥 ↑ 2 ) ) = 0 )
99 92 94 98 subeq0d ⊢ ( ( 𝑥 ∈ ℂ ∧ ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) = 0 ) → 1 = ( 𝑥 ↑ 2 ) )
100 91 99 eqtr2id ⊢ ( ( 𝑥 ∈ ℂ ∧ ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) = 0 ) → ( 𝑥 ↑ 2 ) = ( 1 ↑ 2 ) )
101 100 ex ⊢ ( 𝑥 ∈ ℂ → ( ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) = 0 → ( 𝑥 ↑ 2 ) = ( 1 ↑ 2 ) ) )
102 sqeqor ⊢ ( ( 𝑥 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑥 ↑ 2 ) = ( 1 ↑ 2 ) ↔ ( 𝑥 = 1 ∨ 𝑥 = - 1 ) ) )
103 63 102 mpan2 ⊢ ( 𝑥 ∈ ℂ → ( ( 𝑥 ↑ 2 ) = ( 1 ↑ 2 ) ↔ ( 𝑥 = 1 ∨ 𝑥 = - 1 ) ) )
104 101 103 sylibd ⊢ ( 𝑥 ∈ ℂ → ( ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) = 0 → ( 𝑥 = 1 ∨ 𝑥 = - 1 ) ) )
105 104 necon3bd ⊢ ( 𝑥 ∈ ℂ → ( ¬ ( 𝑥 = 1 ∨ 𝑥 = - 1 ) → ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ≠ 0 ) )
106 48 90 105 sylc ⊢ ( 𝑥 ∈ 𝐷 → ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ≠ 0 )
107 62 67 106 divnegd ⊢ ( 𝑥 ∈ 𝐷 → - ( 1 / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) = ( - 1 / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) )
108 61 107 eqtr3id ⊢ ( 𝑥 ∈ 𝐷 → ( 0 − ( 1 / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) = ( - 1 / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) )
109 108 mpteq2ia ⊢ ( 𝑥 ∈ 𝐷 ↦ ( 0 − ( 1 / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) ) = ( 𝑥 ∈ 𝐷 ↦ ( - 1 / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) )
110 9 60 109 3eqtri ⊢ ( ℂ D ( arccos ↾ 𝐷 ) ) = ( 𝑥 ∈ 𝐷 ↦ ( - 1 / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) )