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 \in (- 1, 1) ⟼ \frac{- 1}{\sqrt{1 - x^{2}}})$

Proof

Step	Hyp	Ref	Expression
1		acosf	$⊢ arccos : ℂ ⟶ ℂ$
2	1	a1i	$⊢ ⊤ \to arccos : ℂ ⟶ ℂ$
3		ioossre	$⊢ (- 1, 1) \subseteq ℝ$
4		ax-resscn	$⊢ ℝ \subseteq ℂ$
5	3 4	sstri	$⊢ (- 1, 1) \subseteq ℂ$
6	5	a1i	$⊢ ⊤ \to (- 1, 1) \subseteq ℂ$
7	2 6	feqresmpt	$⊢ ⊤ \to {arccos ↾}_{(- 1, 1)} = (x \in (- 1, 1) ⟼ arccos (x))$
8	7	oveq2d	$⊢ ⊤ \to ℝ D ({arccos ↾}_{(- 1, 1)}) = \frac{d (x \in (- 1, 1)⟼ arccos (x))}{d_{ℝ} x}$
9		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
10		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
11	10	a1i	$⊢ ⊤ \to ℝ \in \{ℝ, ℂ\}$
12	9	recld2	$⊢ ℝ \in Clsd (TopOpen (ℂ_{fld}))$
13		neg1rr	$⊢ - 1 \in ℝ$
14		iocmnfcld	$⊢ - 1 \in ℝ \to (−∞, - 1] \in Clsd (topGen (ran (.)))$
15	13 14	ax-mp	$⊢ (−∞, - 1] \in Clsd (topGen (ran (.)))$
16		1re	$⊢ 1 \in ℝ$
17		icopnfcld	$⊢ 1 \in ℝ \to [1, +∞) \in Clsd (topGen (ran (.)))$
18	16 17	ax-mp	$⊢ [1, +∞) \in Clsd (topGen (ran (.)))$
19		uncld	$⊢ ((−∞, - 1] \in Clsd (topGen (ran (.))) \land [1, +∞) \in Clsd (topGen (ran (.)))) \to (−∞, - 1] \cup [1, +∞) \in Clsd (topGen (ran (.)))$
20	15 18 19	mp2an	$⊢ (−∞, - 1] \cup [1, +∞) \in Clsd (topGen (ran (.)))$
21	9	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
22	21	fveq2i	$⊢ Clsd (topGen (ran (.))) = Clsd (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
23	20 22	eleqtri	$⊢ (−∞, - 1] \cup [1, +∞) \in Clsd (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
24		restcldr	$⊢ (ℝ \in Clsd (TopOpen (ℂ_{fld})) \land (−∞, - 1] \cup [1, +∞) \in Clsd (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)) \to (−∞, - 1] \cup [1, +∞) \in Clsd (TopOpen (ℂ_{fld}))$
25	12 23 24	mp2an	$⊢ (−∞, - 1] \cup [1, +∞) \in Clsd (TopOpen (ℂ_{fld}))$
26	9	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
27	26	toponunii	$⊢ ℂ = ⋃ TopOpen (ℂ_{fld})$
28	27	cldopn	$⊢ (−∞, - 1] \cup [1, +∞) \in Clsd (TopOpen (ℂ_{fld})) \to ℂ ∖ ((−∞, - 1] \cup [1, +∞)) \in TopOpen (ℂ_{fld})$
29	25 28	mp1i	$⊢ ⊤ \to ℂ ∖ ((−∞, - 1] \cup [1, +∞)) \in TopOpen (ℂ_{fld})$
30		incom	$⊢ ℝ \cap (ℂ ∖ ((−∞, - 1] \cup [1, +∞))) = (ℂ ∖ ((−∞, - 1] \cup [1, +∞))) \cap ℝ$
31		eqid	$⊢ ℂ ∖ ((−∞, - 1] \cup [1, +∞)) = ℂ ∖ ((−∞, - 1] \cup [1, +∞))$
32	31	asindmre	$⊢ (ℂ ∖ ((−∞, - 1] \cup [1, +∞))) \cap ℝ = (- 1, 1)$
33	30 32	eqtri	$⊢ ℝ \cap (ℂ ∖ ((−∞, - 1] \cup [1, +∞))) = (- 1, 1)$
34	33	a1i	$⊢ ⊤ \to ℝ \cap (ℂ ∖ ((−∞, - 1] \cup [1, +∞))) = (- 1, 1)$
35		eldifi	$⊢ x \in (ℂ ∖ ((−∞, - 1] \cup [1, +∞))) \to x \in ℂ$
36		acoscl	$⊢ x \in ℂ \to arccos (x) \in ℂ$
37	35 36	syl	$⊢ x \in (ℂ ∖ ((−∞, - 1] \cup [1, +∞))) \to arccos (x) \in ℂ$
38	37	adantl	$⊢ (⊤ \land x \in (ℂ ∖ ((−∞, - 1] \cup [1, +∞)))) \to arccos (x) \in ℂ$
39		ovexd	$⊢ (⊤ \land x \in (ℂ ∖ ((−∞, - 1] \cup [1, +∞)))) \to \frac{- 1}{\sqrt{1 - x^{2}}} \in V$
40		difssd	$⊢ ⊤ \to ℂ ∖ ((−∞, - 1] \cup [1, +∞)) \subseteq ℂ$
41	2 40	feqresmpt	$⊢ ⊤ \to {arccos ↾}_{(ℂ ∖ ((−∞, - 1] \cup [1, +∞)))} = (x \in (ℂ ∖ ((−∞, - 1] \cup [1, +∞))) ⟼ arccos (x))$
42	41	oveq2d	$⊢ ⊤ \to ℂ D ({arccos ↾}_{(ℂ ∖ ((−∞, - 1] \cup [1, +∞)))}) = \frac{d (x \in (ℂ ∖ ((−∞, - 1] \cup [1, +∞)))⟼ arccos (x))}{d_{ℂ} x}$
43	31	dvacos	$⊢ ℂ D ({arccos ↾}_{(ℂ ∖ ((−∞, - 1] \cup [1, +∞)))}) = (x \in (ℂ ∖ ((−∞, - 1] \cup [1, +∞))) ⟼ \frac{- 1}{\sqrt{1 - x^{2}}})$
44	42 43	eqtr3di	$⊢ ⊤ \to \frac{d (x \in (ℂ ∖ ((−∞, - 1] \cup [1, +∞)))⟼ arccos (x))}{d_{ℂ} x} = (x \in (ℂ ∖ ((−∞, - 1] \cup [1, +∞))) ⟼ \frac{- 1}{\sqrt{1 - x^{2}}})$
45	9 11 29 34 38 39 44	dvmptres3	$⊢ ⊤ \to \frac{d (x \in (- 1, 1)⟼ arccos (x))}{d_{ℝ} x} = (x \in (- 1, 1) ⟼ \frac{- 1}{\sqrt{1 - x^{2}}})$
46	8 45	eqtrd	$⊢ ⊤ \to ℝ D ({arccos ↾}_{(- 1, 1)}) = (x \in (- 1, 1) ⟼ \frac{- 1}{\sqrt{1 - x^{2}}})$
47	46	mptru	$⊢ ℝ D ({arccos ↾}_{(- 1, 1)}) = (x \in (- 1, 1) ⟼ \frac{- 1}{\sqrt{1 - x^{2}}})$

Metamath Proof Explorer

Theorem dvreacos

Proof