dvacos

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

		Ref	Expression
	Hypothesis	dvasin.d	$⊢ D = ℂ ∖ ((−∞, - 1] \cup [1, +∞))$
	Assertion	dvacos	$⊢ ℂ D ({arccos ↾}_{D}) = (x \in D ⟼ \frac{- 1}{\sqrt{1 - x^{2}}})$

Proof

Step	Hyp	Ref	Expression
1		dvasin.d	$⊢ D = ℂ ∖ ((−∞, - 1] \cup [1, +∞))$
2		df-acos	$⊢ arccos = (x \in ℂ ⟼ (\frac{π}{2}) - arcsin (x))$
3	2	reseq1i	$⊢ {arccos ↾}_{D} = {(x \in ℂ ⟼ (\frac{π}{2}) - arcsin (x)) ↾}_{D}$
4		difss	$⊢ ℂ ∖ ((−∞, - 1] \cup [1, +∞)) \subseteq ℂ$
5	1 4	eqsstri	$⊢ D \subseteq ℂ$
6		resmpt	$⊢ D \subseteq ℂ \to {(x \in ℂ ⟼ (\frac{π}{2}) - arcsin (x)) ↾}_{D} = (x \in D ⟼ (\frac{π}{2}) - arcsin (x))$
7	5 6	ax-mp	$⊢ {(x \in ℂ ⟼ (\frac{π}{2}) - arcsin (x)) ↾}_{D} = (x \in D ⟼ (\frac{π}{2}) - arcsin (x))$
8	3 7	eqtri	$⊢ {arccos ↾}_{D} = (x \in D ⟼ (\frac{π}{2}) - arcsin (x))$
9	8	oveq2i	$⊢ ℂ D ({arccos ↾}_{D}) = \frac{d (x \in D⟼ (\frac{π}{2}) - arcsin (x))}{d_{ℂ} x}$
10		cnelprrecn	$⊢ ℂ \in \{ℝ, ℂ\}$
11	10	a1i	$⊢ ⊤ \to ℂ \in \{ℝ, ℂ\}$
12		halfpire	$⊢ \frac{π}{2} \in ℝ$
13	12	recni	$⊢ \frac{π}{2} \in ℂ$
14	13	a1i	$⊢ (⊤ \land x \in D) \to \frac{π}{2} \in ℂ$
15		c0ex	$⊢ 0 \in V$
16	15	a1i	$⊢ (⊤ \land x \in D) \to 0 \in V$
17	13	a1i	$⊢ (⊤ \land x \in ℂ) \to \frac{π}{2} \in ℂ$
18	15	a1i	$⊢ (⊤ \land x \in ℂ) \to 0 \in V$
19	13	a1i	$⊢ ⊤ \to \frac{π}{2} \in ℂ$
20	11 19	dvmptc	$⊢ ⊤ \to \frac{d (x \in ℂ⟼ \frac{π}{2})}{d_{ℂ} x} = (x \in ℂ ⟼ 0)$
21	5	a1i	$⊢ ⊤ \to D \subseteq ℂ$
22		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
23	22	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
24	23	toponrestid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ$
25	22	recld2	$⊢ ℝ \in Clsd (TopOpen (ℂ_{fld}))$
26		neg1rr	$⊢ - 1 \in ℝ$
27		iocmnfcld	$⊢ - 1 \in ℝ \to (−∞, - 1] \in Clsd (topGen (ran (.)))$
28	26 27	ax-mp	$⊢ (−∞, - 1] \in Clsd (topGen (ran (.)))$
29	22	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
30	29	fveq2i	$⊢ Clsd (topGen (ran (.))) = Clsd (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
31	28 30	eleqtri	$⊢ (−∞, - 1] \in Clsd (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
32		restcldr	$⊢ (ℝ \in Clsd (TopOpen (ℂ_{fld})) \land (−∞, - 1] \in Clsd (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)) \to (−∞, - 1] \in Clsd (TopOpen (ℂ_{fld}))$
33	25 31 32	mp2an	$⊢ (−∞, - 1] \in Clsd (TopOpen (ℂ_{fld}))$
34		1re	$⊢ 1 \in ℝ$
35		icopnfcld	$⊢ 1 \in ℝ \to [1, +∞) \in Clsd (topGen (ran (.)))$
36	34 35	ax-mp	$⊢ [1, +∞) \in Clsd (topGen (ran (.)))$
37	36 30	eleqtri	$⊢ [1, +∞) \in Clsd (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
38		restcldr	$⊢ (ℝ \in Clsd (TopOpen (ℂ_{fld})) \land [1, +∞) \in Clsd (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)) \to [1, +∞) \in Clsd (TopOpen (ℂ_{fld}))$
39	25 37 38	mp2an	$⊢ [1, +∞) \in Clsd (TopOpen (ℂ_{fld}))$
40		uncld	$⊢ ((−∞, - 1] \in Clsd (TopOpen (ℂ_{fld})) \land [1, +∞) \in Clsd (TopOpen (ℂ_{fld}))) \to (−∞, - 1] \cup [1, +∞) \in Clsd (TopOpen (ℂ_{fld}))$
41	33 39 40	mp2an	$⊢ (−∞, - 1] \cup [1, +∞) \in Clsd (TopOpen (ℂ_{fld}))$
42	23	toponunii	$⊢ ℂ = ⋃ TopOpen (ℂ_{fld})$
43	42	cldopn	$⊢ (−∞, - 1] \cup [1, +∞) \in Clsd (TopOpen (ℂ_{fld})) \to ℂ ∖ ((−∞, - 1] \cup [1, +∞)) \in TopOpen (ℂ_{fld})$
44	41 43	ax-mp	$⊢ ℂ ∖ ((−∞, - 1] \cup [1, +∞)) \in TopOpen (ℂ_{fld})$
45	1 44	eqeltri	$⊢ D \in TopOpen (ℂ_{fld})$
46	45	a1i	$⊢ ⊤ \to D \in TopOpen (ℂ_{fld})$
47	11 17 18 20 21 24 22 46	dvmptres	$⊢ ⊤ \to \frac{d (x \in D⟼ \frac{π}{2})}{d_{ℂ} x} = (x \in D ⟼ 0)$
48	5	sseli	$⊢ x \in D \to x \in ℂ$
49		asincl	$⊢ x \in ℂ \to arcsin (x) \in ℂ$
50	48 49	syl	$⊢ x \in D \to arcsin (x) \in ℂ$
51	50	adantl	$⊢ (⊤ \land x \in D) \to arcsin (x) \in ℂ$
52		ovexd	$⊢ (⊤ \land x \in D) \to \frac{1}{\sqrt{1 - x^{2}}} \in V$
53	1	dvasin	$⊢ ℂ D ({arcsin ↾}_{D}) = (x \in D ⟼ \frac{1}{\sqrt{1 - x^{2}}})$
54		asinf	$⊢ arcsin : ℂ ⟶ ℂ$
55	54	a1i	$⊢ ⊤ \to arcsin : ℂ ⟶ ℂ$
56	55 21	feqresmpt	$⊢ ⊤ \to {arcsin ↾}_{D} = (x \in D ⟼ arcsin (x))$
57	56	oveq2d	$⊢ ⊤ \to ℂ D ({arcsin ↾}_{D}) = \frac{d (x \in D⟼ arcsin (x))}{d_{ℂ} x}$
58	53 57	syl5reqr	$⊢ ⊤ \to \frac{d (x \in D⟼ arcsin (x))}{d_{ℂ} x} = (x \in D ⟼ \frac{1}{\sqrt{1 - x^{2}}})$
59	11 14 16 47 51 52 58	dvmptsub	$⊢ ⊤ \to \frac{d (x \in D⟼ (\frac{π}{2}) - arcsin (x))}{d_{ℂ} x} = (x \in D ⟼ 0 - (\frac{1}{\sqrt{1 - x^{2}}}))$
60	59	mptru	$⊢ \frac{d (x \in D⟼ (\frac{π}{2}) - arcsin (x))}{d_{ℂ} x} = (x \in D ⟼ 0 - (\frac{1}{\sqrt{1 - x^{2}}}))$
61		df-neg	$⊢ - \frac{1}{\sqrt{1 - x^{2}}} = 0 - (\frac{1}{\sqrt{1 - x^{2}}})$
62		1cnd	$⊢ x \in D \to 1 \in ℂ$
63		ax-1cn	$⊢ 1 \in ℂ$
64	48	sqcld	$⊢ x \in D \to x^{2} \in ℂ$
65		subcl	$⊢ (1 \in ℂ \land x^{2} \in ℂ) \to 1 - x^{2} \in ℂ$
66	63 64 65	sylancr	$⊢ x \in D \to 1 - x^{2} \in ℂ$
67	66	sqrtcld	$⊢ x \in D \to \sqrt{1 - x^{2}} \in ℂ$
68		eldifn	$⊢ x \in (ℂ ∖ ((−∞, - 1] \cup [1, +∞))) \to \neg x \in ((−∞, - 1] \cup [1, +∞))$
69	68 1	eleq2s	$⊢ x \in D \to \neg x \in ((−∞, - 1] \cup [1, +∞))$
70		mnfxr	$⊢ −∞ \in ℝ^{*}$
71	26	rexri	$⊢ - 1 \in ℝ^{*}$
72		mnflt	$⊢ - 1 \in ℝ \to −∞ < - 1$
73	26 72	ax-mp	$⊢ −∞ < - 1$
74		ubioc1	$⊢ (−∞ \in ℝ^{} \land - 1 \in ℝ^{} \land −∞ < - 1) \to - 1 \in (−∞, - 1]$
75	70 71 73 74	mp3an	$⊢ - 1 \in (−∞, - 1]$
76		eleq1	$⊢ x = - 1 \to (x \in (−∞, - 1] \leftrightarrow - 1 \in (−∞, - 1])$
77	75 76	mpbiri	$⊢ x = - 1 \to x \in (−∞, - 1]$
78	34	rexri	$⊢ 1 \in ℝ^{*}$
79		pnfxr	$⊢ +∞ \in ℝ^{*}$
80		ltpnf	$⊢ 1 \in ℝ \to 1 < +∞$
81	34 80	ax-mp	$⊢ 1 < +∞$
82		lbico1	$⊢ (1 \in ℝ^{} \land +∞ \in ℝ^{} \land 1 < +∞) \to 1 \in [1, +∞)$
83	78 79 81 82	mp3an	$⊢ 1 \in [1, +∞)$
84		eleq1	$⊢ x = 1 \to (x \in [1, +∞) \leftrightarrow 1 \in [1, +∞))$
85	83 84	mpbiri	$⊢ x = 1 \to x \in [1, +∞)$
86	77 85	orim12i	$⊢ (x = - 1 \lor x = 1) \to (x \in (−∞, - 1] \lor x \in [1, +∞))$
87	86	orcoms	$⊢ (x = 1 \lor x = - 1) \to (x \in (−∞, - 1] \lor x \in [1, +∞))$
88		elun	$⊢ x \in ((−∞, - 1] \cup [1, +∞)) \leftrightarrow (x \in (−∞, - 1] \lor x \in [1, +∞))$
89	87 88	sylibr	$⊢ (x = 1 \lor x = - 1) \to x \in ((−∞, - 1] \cup [1, +∞))$
90	69 89	nsyl	$⊢ x \in D \to \neg (x = 1 \lor x = - 1)$
91		sq1	$⊢ 1^{2} = 1$
92		1cnd	$⊢ (x \in ℂ \land \sqrt{1 - x^{2}} = 0) \to 1 \in ℂ$
93		sqcl	$⊢ x \in ℂ \to x^{2} \in ℂ$
94	93	adantr	$⊢ (x \in ℂ \land \sqrt{1 - x^{2}} = 0) \to x^{2} \in ℂ$
95	63 93 65	sylancr	$⊢ x \in ℂ \to 1 - x^{2} \in ℂ$
96	95	adantr	$⊢ (x \in ℂ \land \sqrt{1 - x^{2}} = 0) \to 1 - x^{2} \in ℂ$
97		simpr	$⊢ (x \in ℂ \land \sqrt{1 - x^{2}} = 0) \to \sqrt{1 - x^{2}} = 0$
98	96 97	sqr00d	$⊢ (x \in ℂ \land \sqrt{1 - x^{2}} = 0) \to 1 - x^{2} = 0$
99	92 94 98	subeq0d	$⊢ (x \in ℂ \land \sqrt{1 - x^{2}} = 0) \to 1 = x^{2}$
100	91 99	syl5req	$⊢ (x \in ℂ \land \sqrt{1 - x^{2}} = 0) \to x^{2} = 1^{2}$
101	100	ex	$⊢ x \in ℂ \to (\sqrt{1 - x^{2}} = 0 \to x^{2} = 1^{2})$
102		sqeqor	$⊢ (x \in ℂ \land 1 \in ℂ) \to (x^{2} = 1^{2} \leftrightarrow (x = 1 \lor x = - 1))$
103	63 102	mpan2	$⊢ x \in ℂ \to (x^{2} = 1^{2} \leftrightarrow (x = 1 \lor x = - 1))$
104	101 103	sylibd	$⊢ x \in ℂ \to (\sqrt{1 - x^{2}} = 0 \to (x = 1 \lor x = - 1))$
105	104	necon3bd	$⊢ x \in ℂ \to (\neg (x = 1 \lor x = - 1) \to \sqrt{1 - x^{2}} \neq 0)$
106	48 90 105	sylc	$⊢ x \in D \to \sqrt{1 - x^{2}} \neq 0$
107	62 67 106	divnegd	$⊢ x \in D \to - \frac{1}{\sqrt{1 - x^{2}}} = \frac{- 1}{\sqrt{1 - x^{2}}}$
108	61 107	syl5eqr	$⊢ x \in D \to 0 - (\frac{1}{\sqrt{1 - x^{2}}}) = \frac{- 1}{\sqrt{1 - x^{2}}}$
109	108	mpteq2ia	$⊢ (x \in D ⟼ 0 - (\frac{1}{\sqrt{1 - x^{2}}})) = (x \in D ⟼ \frac{- 1}{\sqrt{1 - x^{2}}})$
110	9 60 109	3eqtri	$⊢ ℂ D ({arccos ↾}_{D}) = (x \in D ⟼ \frac{- 1}{\sqrt{1 - x^{2}}})$

Metamath Proof Explorer

Theorem dvacos

Proof