Metamath Proof Explorer

Theorem dvreasin

Description: Real derivative of arcsine. (Contributed by Brendan Leahy, 3-Aug-2017) (Proof shortened by Brendan Leahy, 18-Dec-2018)

Ref Expression
Assertion dvreasin ( ℝ D ( arcsin ↾ ( - 1 (,) 1 ) ) ) = ( 𝑥 ∈ ( - 1 (,) 1 ) ↦ ( 1 / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 asinf ⊢ arcsin : ℂ ⟶ ℂ
2 1 a1i ⊢ ( ⊤ → arcsin : ℂ ⟶ ℂ )
3 ioossre ⊢ ( - 1 (,) 1 ) ⊆ ℝ
4 ax-resscn ⊢ ℝ ⊆ ℂ
5 3 4 sstri ⊢ ( - 1 (,) 1 ) ⊆ ℂ
6 5 a1i ⊢ ( ⊤ → ( - 1 (,) 1 ) ⊆ ℂ )
7 2 6 feqresmpt ⊢ ( ⊤ → ( arcsin ↾ ( - 1 (,) 1 ) ) = ( 𝑥 ∈ ( - 1 (,) 1 ) ↦ ( arcsin ‘ 𝑥 ) ) )
8 7 oveq2d ⊢ ( ⊤ → ( ℝ D ( arcsin ↾ ( - 1 (,) 1 ) ) ) = ( ℝ D ( 𝑥 ∈ ( - 1 (,) 1 ) ↦ ( arcsin ‘ 𝑥 ) ) ) )
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 ) ↾t ℝ )
22 21 fveq2i ⊢ ( Clsd ‘ ( topGen ‘ ran (,) ) ) = ( Clsd ‘ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) )
23 20 22 eleqtri ⊢ ( ( -∞ (,] - 1 ) ∪ ( 1 [,) +∞ ) ) ∈ ( Clsd ‘ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) )
24 restcldr ⊢ ( ( ℝ ∈ ( Clsd ‘ ( TopOpen ‘ ℂfld ) ) ∧ ( ( -∞ (,] - 1 ) ∪ ( 1 [,) +∞ ) ) ∈ ( Clsd ‘ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) ) ) → ( ( -∞ (,] - 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 ⊢ ( 𝑥 ∈ ( ℂ ∖ ( ( -∞ (,] - 1 ) ∪ ( 1 [,) +∞ ) ) ) → 𝑥 ∈ ℂ )
36 asincl ⊢ ( 𝑥 ∈ ℂ → ( arcsin ‘ 𝑥 ) ∈ ℂ )
37 35 36 syl ⊢ ( 𝑥 ∈ ( ℂ ∖ ( ( -∞ (,] - 1 ) ∪ ( 1 [,) +∞ ) ) ) → ( arcsin ‘ 𝑥 ) ∈ ℂ )
38 37 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( ℂ ∖ ( ( -∞ (,] - 1 ) ∪ ( 1 [,) +∞ ) ) ) ) → ( arcsin ‘ 𝑥 ) ∈ ℂ )
39 ovexd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( ℂ ∖ ( ( -∞ (,] - 1 ) ∪ ( 1 [,) +∞ ) ) ) ) → ( 1 / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ∈ V )
40 difssd ⊢ ( ⊤ → ( ℂ ∖ ( ( -∞ (,] - 1 ) ∪ ( 1 [,) +∞ ) ) ) ⊆ ℂ )
41 2 40 feqresmpt ⊢ ( ⊤ → ( arcsin ↾ ( ℂ ∖ ( ( -∞ (,] - 1 ) ∪ ( 1 [,) +∞ ) ) ) ) = ( 𝑥 ∈ ( ℂ ∖ ( ( -∞ (,] - 1 ) ∪ ( 1 [,) +∞ ) ) ) ↦ ( arcsin ‘ 𝑥 ) ) )
42 41 oveq2d ⊢ ( ⊤ → ( ℂ D ( arcsin ↾ ( ℂ ∖ ( ( -∞ (,] - 1 ) ∪ ( 1 [,) +∞ ) ) ) ) ) = ( ℂ D ( 𝑥 ∈ ( ℂ ∖ ( ( -∞ (,] - 1 ) ∪ ( 1 [,) +∞ ) ) ) ↦ ( arcsin ‘ 𝑥 ) ) ) )
43 31 dvasin ⊢ ( ℂ D ( arcsin ↾ ( ℂ ∖ ( ( -∞ (,] - 1 ) ∪ ( 1 [,) +∞ ) ) ) ) ) = ( 𝑥 ∈ ( ℂ ∖ ( ( -∞ (,] - 1 ) ∪ ( 1 [,) +∞ ) ) ) ↦ ( 1 / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) )
44 42 43 eqtr3di ⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ ( ℂ ∖ ( ( -∞ (,] - 1 ) ∪ ( 1 [,) +∞ ) ) ) ↦ ( arcsin ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( ℂ ∖ ( ( -∞ (,] - 1 ) ∪ ( 1 [,) +∞ ) ) ) ↦ ( 1 / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) )
45 9 11 29 34 38 39 44 dvmptres3 ⊢ ( ⊤ → ( ℝ D ( 𝑥 ∈ ( - 1 (,) 1 ) ↦ ( arcsin ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( - 1 (,) 1 ) ↦ ( 1 / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) )
46 8 45 eqtrd ⊢ ( ⊤ → ( ℝ D ( arcsin ↾ ( - 1 (,) 1 ) ) ) = ( 𝑥 ∈ ( - 1 (,) 1 ) ↦ ( 1 / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) ) )
47 46 mptru ⊢ ( ℝ D ( arcsin ↾ ( - 1 (,) 1 ) ) ) = ( 𝑥 ∈ ( - 1 (,) 1 ) ↦ ( 1 / ( √ ‘ ( 1 − ( 𝑥 ↑ 2 ) ) ) ) )