dvasin

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

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

Proof

Step	Hyp	Ref	Expression
1		dvasin.d	$⊢ D = ℂ ∖ ((−∞, - 1] \cup [1, +∞))$
2		df-asin	$⊢ arcsin = (x \in ℂ ⟼ (- i) \log (i x + \sqrt{1 - x^{2}}))$
3	2	reseq1i	$⊢ {arcsin ↾}_{D} = {(x \in ℂ ⟼ (- i) \log (i x + \sqrt{1 - x^{2}})) ↾}_{D}$
4		difss	$⊢ ℂ ∖ ((−∞, - 1] \cup [1, +∞)) \subseteq ℂ$
5	1 4	eqsstri	$⊢ D \subseteq ℂ$
6		resmpt	$⊢ D \subseteq ℂ \to {(x \in ℂ ⟼ (- i) \log (i x + \sqrt{1 - x^{2}})) ↾}_{D} = (x \in D ⟼ (- i) \log (i x + \sqrt{1 - x^{2}}))$
7	5 6	ax-mp	$⊢ {(x \in ℂ ⟼ (- i) \log (i x + \sqrt{1 - x^{2}})) ↾}_{D} = (x \in D ⟼ (- i) \log (i x + \sqrt{1 - x^{2}}))$
8	3 7	eqtri	$⊢ {arcsin ↾}_{D} = (x \in D ⟼ (- i) \log (i x + \sqrt{1 - x^{2}}))$
9	8	oveq2i	$⊢ ℂ D ({arcsin ↾}_{D}) = \frac{d (x \in D⟼ (- i) \log (i x + \sqrt{1 - x^{2}}))}{d_{ℂ} x}$
10		cnelprrecn	$⊢ ℂ \in \{ℝ, ℂ\}$
11	10	a1i	$⊢ ⊤ \to ℂ \in \{ℝ, ℂ\}$
12	5	sseli	$⊢ x \in D \to x \in ℂ$
13		ax-icn	$⊢ i \in ℂ$
14		mulcl	$⊢ (i \in ℂ \land x \in ℂ) \to i x \in ℂ$
15	13 14	mpan	$⊢ x \in ℂ \to i x \in ℂ$
16		ax-1cn	$⊢ 1 \in ℂ$
17		sqcl	$⊢ x \in ℂ \to x^{2} \in ℂ$
18		subcl	$⊢ (1 \in ℂ \land x^{2} \in ℂ) \to 1 - x^{2} \in ℂ$
19	16 17 18	sylancr	$⊢ x \in ℂ \to 1 - x^{2} \in ℂ$
20	19	sqrtcld	$⊢ x \in ℂ \to \sqrt{1 - x^{2}} \in ℂ$
21	15 20	addcld	$⊢ x \in ℂ \to i x + \sqrt{1 - x^{2}} \in ℂ$
22	12 21	syl	$⊢ x \in D \to i x + \sqrt{1 - x^{2}} \in ℂ$
23		asinlem	$⊢ x \in ℂ \to i x + \sqrt{1 - x^{2}} \neq 0$
24	12 23	syl	$⊢ x \in D \to i x + \sqrt{1 - x^{2}} \neq 0$
25	22 24	logcld	$⊢ x \in D \to \log (i x + \sqrt{1 - x^{2}}) \in ℂ$
26	25	adantl	$⊢ (⊤ \land x \in D) \to \log (i x + \sqrt{1 - x^{2}}) \in ℂ$
27		ovexd	$⊢ (⊤ \land x \in D) \to \frac{i}{\sqrt{1 - x^{2}}} \in V$
28		simpr	$⊢ (x \in ℂ \land i x + \sqrt{1 - x^{2}} \in ℝ) \to i x + \sqrt{1 - x^{2}} \in ℝ$
29		asinlem3	$⊢ x \in ℂ \to 0 \leq ℜ (i x + \sqrt{1 - x^{2}})$
30		rere	$⊢ i x + \sqrt{1 - x^{2}} \in ℝ \to ℜ (i x + \sqrt{1 - x^{2}}) = i x + \sqrt{1 - x^{2}}$
31	30	breq2d	$⊢ i x + \sqrt{1 - x^{2}} \in ℝ \to (0 \leq ℜ (i x + \sqrt{1 - x^{2}}) \leftrightarrow 0 \leq i x + \sqrt{1 - x^{2}})$
32	31	biimpac	$⊢ (0 \leq ℜ (i x + \sqrt{1 - x^{2}}) \land i x + \sqrt{1 - x^{2}} \in ℝ) \to 0 \leq i x + \sqrt{1 - x^{2}}$
33	29 32	sylan	$⊢ (x \in ℂ \land i x + \sqrt{1 - x^{2}} \in ℝ) \to 0 \leq i x + \sqrt{1 - x^{2}}$
34	23	adantr	$⊢ (x \in ℂ \land i x + \sqrt{1 - x^{2}} \in ℝ) \to i x + \sqrt{1 - x^{2}} \neq 0$
35	28 33 34	ne0gt0d	$⊢ (x \in ℂ \land i x + \sqrt{1 - x^{2}} \in ℝ) \to 0 < i x + \sqrt{1 - x^{2}}$
36		0re	$⊢ 0 \in ℝ$
37		ltnle	$⊢ (0 \in ℝ \land i x + \sqrt{1 - x^{2}} \in ℝ) \to (0 < i x + \sqrt{1 - x^{2}} \leftrightarrow \neg i x + \sqrt{1 - x^{2}} \leq 0)$
38	36 37	mpan	$⊢ i x + \sqrt{1 - x^{2}} \in ℝ \to (0 < i x + \sqrt{1 - x^{2}} \leftrightarrow \neg i x + \sqrt{1 - x^{2}} \leq 0)$
39	38	adantl	$⊢ (x \in ℂ \land i x + \sqrt{1 - x^{2}} \in ℝ) \to (0 < i x + \sqrt{1 - x^{2}} \leftrightarrow \neg i x + \sqrt{1 - x^{2}} \leq 0)$
40	35 39	mpbid	$⊢ (x \in ℂ \land i x + \sqrt{1 - x^{2}} \in ℝ) \to \neg i x + \sqrt{1 - x^{2}} \leq 0$
41	40	ex	$⊢ x \in ℂ \to (i x + \sqrt{1 - x^{2}} \in ℝ \to \neg i x + \sqrt{1 - x^{2}} \leq 0)$
42	12 41	syl	$⊢ x \in D \to (i x + \sqrt{1 - x^{2}} \in ℝ \to \neg i x + \sqrt{1 - x^{2}} \leq 0)$
43		imor	$⊢ (i x + \sqrt{1 - x^{2}} \in ℝ \to \neg i x + \sqrt{1 - x^{2}} \leq 0) \leftrightarrow (\neg i x + \sqrt{1 - x^{2}} \in ℝ \lor \neg i x + \sqrt{1 - x^{2}} \leq 0)$
44	42 43	sylib	$⊢ x \in D \to (\neg i x + \sqrt{1 - x^{2}} \in ℝ \lor \neg i x + \sqrt{1 - x^{2}} \leq 0)$
45	44	orcomd	$⊢ x \in D \to (\neg i x + \sqrt{1 - x^{2}} \leq 0 \lor \neg i x + \sqrt{1 - x^{2}} \in ℝ)$
46	45	olcd	$⊢ x \in D \to (\neg −∞ < i x + \sqrt{1 - x^{2}} \lor (\neg i x + \sqrt{1 - x^{2}} \leq 0 \lor \neg i x + \sqrt{1 - x^{2}} \in ℝ))$
47		3ianor	$⊢ \neg (i x + \sqrt{1 - x^{2}} \in ℝ \land −∞ < i x + \sqrt{1 - x^{2}} \land i x + \sqrt{1 - x^{2}} \leq 0) \leftrightarrow (\neg i x + \sqrt{1 - x^{2}} \in ℝ \lor \neg −∞ < i x + \sqrt{1 - x^{2}} \lor \neg i x + \sqrt{1 - x^{2}} \leq 0)$
48		3orrot	$⊢ (\neg i x + \sqrt{1 - x^{2}} \in ℝ \lor \neg −∞ < i x + \sqrt{1 - x^{2}} \lor \neg i x + \sqrt{1 - x^{2}} \leq 0) \leftrightarrow (\neg −∞ < i x + \sqrt{1 - x^{2}} \lor \neg i x + \sqrt{1 - x^{2}} \leq 0 \lor \neg i x + \sqrt{1 - x^{2}} \in ℝ)$
49		3orass	$⊢ (\neg −∞ < i x + \sqrt{1 - x^{2}} \lor \neg i x + \sqrt{1 - x^{2}} \leq 0 \lor \neg i x + \sqrt{1 - x^{2}} \in ℝ) \leftrightarrow (\neg −∞ < i x + \sqrt{1 - x^{2}} \lor (\neg i x + \sqrt{1 - x^{2}} \leq 0 \lor \neg i x + \sqrt{1 - x^{2}} \in ℝ))$
50	47 48 49	3bitrri	$⊢ (\neg −∞ < i x + \sqrt{1 - x^{2}} \lor (\neg i x + \sqrt{1 - x^{2}} \leq 0 \lor \neg i x + \sqrt{1 - x^{2}} \in ℝ)) \leftrightarrow \neg (i x + \sqrt{1 - x^{2}} \in ℝ \land −∞ < i x + \sqrt{1 - x^{2}} \land i x + \sqrt{1 - x^{2}} \leq 0)$
51		mnfxr	$⊢ −∞ \in ℝ^{*}$
52		elioc2	$⊢ (−∞ \in ℝ^{*} \land 0 \in ℝ) \to (i x + \sqrt{1 - x^{2}} \in (−∞, 0] \leftrightarrow (i x + \sqrt{1 - x^{2}} \in ℝ \land −∞ < i x + \sqrt{1 - x^{2}} \land i x + \sqrt{1 - x^{2}} \leq 0))$
53	51 36 52	mp2an	$⊢ i x + \sqrt{1 - x^{2}} \in (−∞, 0] \leftrightarrow (i x + \sqrt{1 - x^{2}} \in ℝ \land −∞ < i x + \sqrt{1 - x^{2}} \land i x + \sqrt{1 - x^{2}} \leq 0)$
54	50 53	xchbinxr	$⊢ (\neg −∞ < i x + \sqrt{1 - x^{2}} \lor (\neg i x + \sqrt{1 - x^{2}} \leq 0 \lor \neg i x + \sqrt{1 - x^{2}} \in ℝ)) \leftrightarrow \neg i x + \sqrt{1 - x^{2}} \in (−∞, 0]$
55	46 54	sylib	$⊢ x \in D \to \neg i x + \sqrt{1 - x^{2}} \in (−∞, 0]$
56	22 55	eldifd	$⊢ x \in D \to i x + \sqrt{1 - x^{2}} \in (ℂ ∖ (−∞, 0])$
57	56	adantl	$⊢ (⊤ \land x \in D) \to i x + \sqrt{1 - x^{2}} \in (ℂ ∖ (−∞, 0])$
58		ovexd	$⊢ (⊤ \land x \in D) \to \frac{i (i x + \sqrt{1 - x^{2}})}{\sqrt{1 - x^{2}}} \in V$
59		eldifi	$⊢ y \in (ℂ ∖ (−∞, 0]) \to y \in ℂ$
60		eldifn	$⊢ y \in (ℂ ∖ (−∞, 0]) \to \neg y \in (−∞, 0]$
61		0xr	$⊢ 0 \in ℝ^{*}$
62		mnflt0	$⊢ −∞ < 0$
63		ubioc1	$⊢ (−∞ \in ℝ^{} \land 0 \in ℝ^{} \land −∞ < 0) \to 0 \in (−∞, 0]$
64	51 61 62 63	mp3an	$⊢ 0 \in (−∞, 0]$
65		eleq1	$⊢ y = 0 \to (y \in (−∞, 0] \leftrightarrow 0 \in (−∞, 0])$
66	64 65	mpbiri	$⊢ y = 0 \to y \in (−∞, 0]$
67	66	necon3bi	$⊢ \neg y \in (−∞, 0] \to y \neq 0$
68	60 67	syl	$⊢ y \in (ℂ ∖ (−∞, 0]) \to y \neq 0$
69	59 68	logcld	$⊢ y \in (ℂ ∖ (−∞, 0]) \to \log y \in ℂ$
70	69	adantl	$⊢ (⊤ \land y \in (ℂ ∖ (−∞, 0])) \to \log y \in ℂ$
71		ovexd	$⊢ (⊤ \land y \in (ℂ ∖ (−∞, 0])) \to \frac{1}{y} \in V$
72	13	a1i	$⊢ x \in D \to i \in ℂ$
73	72 12	mulcld	$⊢ x \in D \to i x \in ℂ$
74	73	adantl	$⊢ (⊤ \land x \in D) \to i x \in ℂ$
75	13	a1i	$⊢ (⊤ \land x \in D) \to i \in ℂ$
76	12	adantl	$⊢ (⊤ \land x \in D) \to x \in ℂ$
77		1cnd	$⊢ (⊤ \land x \in D) \to 1 \in ℂ$
78		simpr	$⊢ (⊤ \land x \in ℂ) \to x \in ℂ$
79		1cnd	$⊢ (⊤ \land x \in ℂ) \to 1 \in ℂ$
80	11	dvmptid	$⊢ ⊤ \to \frac{d (x \in ℂ⟼ x)}{d_{ℂ} x} = (x \in ℂ ⟼ 1)$
81	5	a1i	$⊢ ⊤ \to D \subseteq ℂ$
82		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
83	82	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
84	83	toponrestid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ$
85	82	recld2	$⊢ ℝ \in Clsd (TopOpen (ℂ_{fld}))$
86		neg1rr	$⊢ - 1 \in ℝ$
87		iocmnfcld	$⊢ - 1 \in ℝ \to (−∞, - 1] \in Clsd (topGen (ran (.)))$
88	86 87	ax-mp	$⊢ (−∞, - 1] \in Clsd (topGen (ran (.)))$
89		1re	$⊢ 1 \in ℝ$
90		icopnfcld	$⊢ 1 \in ℝ \to [1, +∞) \in Clsd (topGen (ran (.)))$
91	89 90	ax-mp	$⊢ [1, +∞) \in Clsd (topGen (ran (.)))$
92		uncld	$⊢ ((−∞, - 1] \in Clsd (topGen (ran (.))) \land [1, +∞) \in Clsd (topGen (ran (.)))) \to (−∞, - 1] \cup [1, +∞) \in Clsd (topGen (ran (.)))$
93	88 91 92	mp2an	$⊢ (−∞, - 1] \cup [1, +∞) \in Clsd (topGen (ran (.)))$
94		tgioo4	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
95	94	fveq2i	$⊢ Clsd (topGen (ran (.))) = Clsd (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
96	93 95	eleqtri	$⊢ (−∞, - 1] \cup [1, +∞) \in Clsd (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
97		restcldr	$⊢ (ℝ \in Clsd (TopOpen (ℂ_{fld})) \land (−∞, - 1] \cup [1, +∞) \in Clsd (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)) \to (−∞, - 1] \cup [1, +∞) \in Clsd (TopOpen (ℂ_{fld}))$
98	85 96 97	mp2an	$⊢ (−∞, - 1] \cup [1, +∞) \in Clsd (TopOpen (ℂ_{fld}))$
99	83	toponunii	$⊢ ℂ = ⋃ TopOpen (ℂ_{fld})$
100	99	cldopn	$⊢ (−∞, - 1] \cup [1, +∞) \in Clsd (TopOpen (ℂ_{fld})) \to ℂ ∖ ((−∞, - 1] \cup [1, +∞)) \in TopOpen (ℂ_{fld})$
101	98 100	ax-mp	$⊢ ℂ ∖ ((−∞, - 1] \cup [1, +∞)) \in TopOpen (ℂ_{fld})$
102	1 101	eqeltri	$⊢ D \in TopOpen (ℂ_{fld})$
103	102	a1i	$⊢ ⊤ \to D \in TopOpen (ℂ_{fld})$
104	11 78 79 80 81 84 82 103	dvmptres	$⊢ ⊤ \to \frac{d (x \in D⟼ x)}{d_{ℂ} x} = (x \in D ⟼ 1)$
105	13	a1i	$⊢ ⊤ \to i \in ℂ$
106	11 76 77 104 105	dvmptcmul	$⊢ ⊤ \to \frac{d (x \in D⟼ i x)}{d_{ℂ} x} = (x \in D ⟼ i \cdot 1)$
107	13	mulridi	$⊢ i \cdot 1 = i$
108	107	mpteq2i	$⊢ (x \in D ⟼ i \cdot 1) = (x \in D ⟼ i)$
109	106 108	eqtrdi	$⊢ ⊤ \to \frac{d (x \in D⟼ i x)}{d_{ℂ} x} = (x \in D ⟼ i)$
110	12	sqcld	$⊢ x \in D \to x^{2} \in ℂ$
111	16 110 18	sylancr	$⊢ x \in D \to 1 - x^{2} \in ℂ$
112	111	sqrtcld	$⊢ x \in D \to \sqrt{1 - x^{2}} \in ℂ$
113	112	adantl	$⊢ (⊤ \land x \in D) \to \sqrt{1 - x^{2}} \in ℂ$
114		ovexd	$⊢ (⊤ \land x \in D) \to \frac{- x}{\sqrt{1 - x^{2}}} \in V$
115		elin	$⊢ x \in (D \cap ℝ) \leftrightarrow (x \in D \land x \in ℝ)$
116	1	asindmre	$⊢ D \cap ℝ = (- 1, 1)$
117	116	eqimssi	$⊢ D \cap ℝ \subseteq (- 1, 1)$
118	117	sseli	$⊢ x \in (D \cap ℝ) \to x \in (- 1, 1)$
119	115 118	sylbir	$⊢ (x \in D \land x \in ℝ) \to x \in (- 1, 1)$
120		incom	$⊢ (0, +∞) \cap (−∞, 0] = (−∞, 0] \cap (0, +∞)$
121		pnfxr	$⊢ +∞ \in ℝ^{*}$
122		df-ioc	$⊢ (.] = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x < z \land z \leq y)\})$
123		df-ioo	$⊢ (.) = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x < z \land z < y)\})$
124		xrltnle	$⊢ (0 \in ℝ^{} \land w \in ℝ^{}) \to (0 < w \leftrightarrow \neg w \leq 0)$
125	122 123 124	ixxdisj	$⊢ (−∞ \in ℝ^{} \land 0 \in ℝ^{} \land +∞ \in ℝ^{*}) \to (−∞, 0] \cap (0, +∞) = \emptyset$
126	51 61 121 125	mp3an	$⊢ (−∞, 0] \cap (0, +∞) = \emptyset$
127	120 126	eqtri	$⊢ (0, +∞) \cap (−∞, 0] = \emptyset$
128		elioore	$⊢ x \in (- 1, 1) \to x \in ℝ$
129	128	resqcld	$⊢ x \in (- 1, 1) \to x^{2} \in ℝ$
130		resubcl	$⊢ (1 \in ℝ \land x^{2} \in ℝ) \to 1 - x^{2} \in ℝ$
131	89 129 130	sylancr	$⊢ x \in (- 1, 1) \to 1 - x^{2} \in ℝ$
132	86	rexri	$⊢ - 1 \in ℝ^{*}$
133		1xr	$⊢ 1 \in ℝ^{*}$
134		elioo2	$⊢ (- 1 \in ℝ^{} \land 1 \in ℝ^{}) \to (x \in (- 1, 1) \leftrightarrow (x \in ℝ \land - 1 < x \land x < 1))$
135	132 133 134	mp2an	$⊢ x \in (- 1, 1) \leftrightarrow (x \in ℝ \land - 1 < x \land x < 1)$
136		recn	$⊢ x \in ℝ \to x \in ℂ$
137	136	abscld	$⊢ x \in ℝ \to \|x\| \in ℝ$
138	136	absge0d	$⊢ x \in ℝ \to 0 \leq \|x\|$
139		0le1	$⊢ 0 \leq 1$
140		lt2sq	$⊢ ((\|x\| \in ℝ \land 0 \leq \|x\|) \land (1 \in ℝ \land 0 \leq 1)) \to (\|x\| < 1 \leftrightarrow {\|x\|}^{2} < 1^{2})$
141	89 139 140	mpanr12	$⊢ (\|x\| \in ℝ \land 0 \leq \|x\|) \to (\|x\| < 1 \leftrightarrow {\|x\|}^{2} < 1^{2})$
142	137 138 141	syl2anc	$⊢ x \in ℝ \to (\|x\| < 1 \leftrightarrow {\|x\|}^{2} < 1^{2})$
143		abslt	$⊢ (x \in ℝ \land 1 \in ℝ) \to (\|x\| < 1 \leftrightarrow (- 1 < x \land x < 1))$
144	89 143	mpan2	$⊢ x \in ℝ \to (\|x\| < 1 \leftrightarrow (- 1 < x \land x < 1))$
145		absresq	$⊢ x \in ℝ \to {\|x\|}^{2} = x^{2}$
146		sq1	$⊢ 1^{2} = 1$
147	146	a1i	$⊢ x \in ℝ \to 1^{2} = 1$
148	145 147	breq12d	$⊢ x \in ℝ \to ({\|x\|}^{2} < 1^{2} \leftrightarrow x^{2} < 1)$
149		resqcl	$⊢ x \in ℝ \to x^{2} \in ℝ$
150		posdif	$⊢ (x^{2} \in ℝ \land 1 \in ℝ) \to (x^{2} < 1 \leftrightarrow 0 < 1 - x^{2})$
151	149 89 150	sylancl	$⊢ x \in ℝ \to (x^{2} < 1 \leftrightarrow 0 < 1 - x^{2})$
152	148 151	bitrd	$⊢ x \in ℝ \to ({\|x\|}^{2} < 1^{2} \leftrightarrow 0 < 1 - x^{2})$
153	142 144 152	3bitr3d	$⊢ x \in ℝ \to ((- 1 < x \land x < 1) \leftrightarrow 0 < 1 - x^{2})$
154	153	biimpd	$⊢ x \in ℝ \to ((- 1 < x \land x < 1) \to 0 < 1 - x^{2})$
155	154	3impib	$⊢ (x \in ℝ \land - 1 < x \land x < 1) \to 0 < 1 - x^{2}$
156	135 155	sylbi	$⊢ x \in (- 1, 1) \to 0 < 1 - x^{2}$
157	131 156	elrpd	$⊢ x \in (- 1, 1) \to 1 - x^{2} \in ℝ^{+}$
158		ioorp	$⊢ (0, +∞) = ℝ^{+}$
159	157 158	eleqtrrdi	$⊢ x \in (- 1, 1) \to 1 - x^{2} \in (0, +∞)$
160		disjel	$⊢ ((0, +∞) \cap (−∞, 0] = \emptyset \land 1 - x^{2} \in (0, +∞)) \to \neg 1 - x^{2} \in (−∞, 0]$
161	127 159 160	sylancr	$⊢ x \in (- 1, 1) \to \neg 1 - x^{2} \in (−∞, 0]$
162	119 161	syl	$⊢ (x \in D \land x \in ℝ) \to \neg 1 - x^{2} \in (−∞, 0]$
163		elioc2	$⊢ (−∞ \in ℝ^{*} \land 0 \in ℝ) \to (1 - x^{2} \in (−∞, 0] \leftrightarrow (1 - x^{2} \in ℝ \land −∞ < 1 - x^{2} \land 1 - x^{2} \leq 0))$
164	51 36 163	mp2an	$⊢ 1 - x^{2} \in (−∞, 0] \leftrightarrow (1 - x^{2} \in ℝ \land −∞ < 1 - x^{2} \land 1 - x^{2} \leq 0)$
165	164	biimpi	$⊢ 1 - x^{2} \in (−∞, 0] \to (1 - x^{2} \in ℝ \land −∞ < 1 - x^{2} \land 1 - x^{2} \leq 0)$
166	165	simp1d	$⊢ 1 - x^{2} \in (−∞, 0] \to 1 - x^{2} \in ℝ$
167		resubcl	$⊢ (1 \in ℝ \land 1 - x^{2} \in ℝ) \to 1 - (1 - x^{2}) \in ℝ$
168	89 166 167	sylancr	$⊢ 1 - x^{2} \in (−∞, 0] \to 1 - (1 - x^{2}) \in ℝ$
169		nncan	$⊢ (1 \in ℂ \land x^{2} \in ℂ) \to 1 - (1 - x^{2}) = x^{2}$
170	16 169	mpan	$⊢ x^{2} \in ℂ \to 1 - (1 - x^{2}) = x^{2}$
171	170	eleq1d	$⊢ x^{2} \in ℂ \to (1 - (1 - x^{2}) \in ℝ \leftrightarrow x^{2} \in ℝ)$
172	171	biimpa	$⊢ (x^{2} \in ℂ \land 1 - (1 - x^{2}) \in ℝ) \to x^{2} \in ℝ$
173	168 172	sylan2	$⊢ (x^{2} \in ℂ \land 1 - x^{2} \in (−∞, 0]) \to x^{2} \in ℝ$
174	166	adantl	$⊢ (x^{2} \in ℂ \land 1 - x^{2} \in (−∞, 0]) \to 1 - x^{2} \in ℝ$
175	165	simp3d	$⊢ 1 - x^{2} \in (−∞, 0] \to 1 - x^{2} \leq 0$
176	175	adantl	$⊢ (x^{2} \in ℂ \land 1 - x^{2} \in (−∞, 0]) \to 1 - x^{2} \leq 0$
177		letr	$⊢ (1 - x^{2} \in ℝ \land 0 \in ℝ \land 1 \in ℝ) \to ((1 - x^{2} \leq 0 \land 0 \leq 1) \to 1 - x^{2} \leq 1)$
178	36 89 177	mp3an23	$⊢ 1 - x^{2} \in ℝ \to ((1 - x^{2} \leq 0 \land 0 \leq 1) \to 1 - x^{2} \leq 1)$
179	139 178	mpan2i	$⊢ 1 - x^{2} \in ℝ \to (1 - x^{2} \leq 0 \to 1 - x^{2} \leq 1)$
180	174 176 179	sylc	$⊢ (x^{2} \in ℂ \land 1 - x^{2} \in (−∞, 0]) \to 1 - x^{2} \leq 1$
181		subge0	$⊢ (1 \in ℝ \land 1 - x^{2} \in ℝ) \to (0 \leq 1 - (1 - x^{2}) \leftrightarrow 1 - x^{2} \leq 1)$
182	89 174 181	sylancr	$⊢ (x^{2} \in ℂ \land 1 - x^{2} \in (−∞, 0]) \to (0 \leq 1 - (1 - x^{2}) \leftrightarrow 1 - x^{2} \leq 1)$
183	180 182	mpbird	$⊢ (x^{2} \in ℂ \land 1 - x^{2} \in (−∞, 0]) \to 0 \leq 1 - (1 - x^{2})$
184	170	adantr	$⊢ (x^{2} \in ℂ \land 1 - x^{2} \in (−∞, 0]) \to 1 - (1 - x^{2}) = x^{2}$
185	183 184	breqtrd	$⊢ (x^{2} \in ℂ \land 1 - x^{2} \in (−∞, 0]) \to 0 \leq x^{2}$
186	173 185	resqrtcld	$⊢ (x^{2} \in ℂ \land 1 - x^{2} \in (−∞, 0]) \to \sqrt{x^{2}} \in ℝ$
187	17 186	sylan	$⊢ (x \in ℂ \land 1 - x^{2} \in (−∞, 0]) \to \sqrt{x^{2}} \in ℝ$
188		eleq1	$⊢ x = \sqrt{x^{2}} \to (x \in ℝ \leftrightarrow \sqrt{x^{2}} \in ℝ)$
189	187 188	syl5ibrcom	$⊢ (x \in ℂ \land 1 - x^{2} \in (−∞, 0]) \to (x = \sqrt{x^{2}} \to x \in ℝ)$
190	187	renegcld	$⊢ (x \in ℂ \land 1 - x^{2} \in (−∞, 0]) \to - \sqrt{x^{2}} \in ℝ$
191		eleq1	$⊢ x = - \sqrt{x^{2}} \to (x \in ℝ \leftrightarrow - \sqrt{x^{2}} \in ℝ)$
192	190 191	syl5ibrcom	$⊢ (x \in ℂ \land 1 - x^{2} \in (−∞, 0]) \to (x = - \sqrt{x^{2}} \to x \in ℝ)$
193		eqid	$⊢ x^{2} = x^{2}$
194		eqsqrtor	$⊢ (x \in ℂ \land x^{2} \in ℂ) \to (x^{2} = x^{2} \leftrightarrow (x = \sqrt{x^{2}} \lor x = - \sqrt{x^{2}}))$
195	17 194	mpdan	$⊢ x \in ℂ \to (x^{2} = x^{2} \leftrightarrow (x = \sqrt{x^{2}} \lor x = - \sqrt{x^{2}}))$
196	193 195	mpbii	$⊢ x \in ℂ \to (x = \sqrt{x^{2}} \lor x = - \sqrt{x^{2}})$
197	196	adantr	$⊢ (x \in ℂ \land 1 - x^{2} \in (−∞, 0]) \to (x = \sqrt{x^{2}} \lor x = - \sqrt{x^{2}})$
198	189 192 197	mpjaod	$⊢ (x \in ℂ \land 1 - x^{2} \in (−∞, 0]) \to x \in ℝ$
199	198	stoic1a	$⊢ (x \in ℂ \land \neg x \in ℝ) \to \neg 1 - x^{2} \in (−∞, 0]$
200	12 199	sylan	$⊢ (x \in D \land \neg x \in ℝ) \to \neg 1 - x^{2} \in (−∞, 0]$
201	162 200	pm2.61dan	$⊢ x \in D \to \neg 1 - x^{2} \in (−∞, 0]$
202	111 201	eldifd	$⊢ x \in D \to 1 - x^{2} \in (ℂ ∖ (−∞, 0])$
203	202	adantl	$⊢ (⊤ \land x \in D) \to 1 - x^{2} \in (ℂ ∖ (−∞, 0])$
204		2cnd	$⊢ x \in ℂ \to 2 \in ℂ$
205		id	$⊢ x \in ℂ \to x \in ℂ$
206	204 205	mulcld	$⊢ x \in ℂ \to 2 x \in ℂ$
207	206	negcld	$⊢ x \in ℂ \to - 2 x \in ℂ$
208	207	adantl	$⊢ (⊤ \land x \in ℂ) \to - 2 x \in ℂ$
209	12 208	sylan2	$⊢ (⊤ \land x \in D) \to - 2 x \in ℂ$
210	59	sqrtcld	$⊢ y \in (ℂ ∖ (−∞, 0]) \to \sqrt{y} \in ℂ$
211	210	adantl	$⊢ (⊤ \land y \in (ℂ ∖ (−∞, 0])) \to \sqrt{y} \in ℂ$
212		ovexd	$⊢ (⊤ \land y \in (ℂ ∖ (−∞, 0])) \to \frac{1}{2 \sqrt{y}} \in V$
213	19	adantl	$⊢ (⊤ \land x \in ℂ) \to 1 - x^{2} \in ℂ$
214	36	a1i	$⊢ (⊤ \land x \in ℂ) \to 0 \in ℝ$
215		1cnd	$⊢ ⊤ \to 1 \in ℂ$
216	11 215	dvmptc	$⊢ ⊤ \to \frac{d (x \in ℂ⟼ 1)}{d_{ℂ} x} = (x \in ℂ ⟼ 0)$
217	17	adantl	$⊢ (⊤ \land x \in ℂ) \to x^{2} \in ℂ$
218		2cn	$⊢ 2 \in ℂ$
219		mulcl	$⊢ (2 \in ℂ \land x \in ℂ) \to 2 x \in ℂ$
220	218 219	mpan	$⊢ x \in ℂ \to 2 x \in ℂ$
221	220	adantl	$⊢ (⊤ \land x \in ℂ) \to 2 x \in ℂ$
222		2nn	$⊢ 2 \in ℕ$
223		dvexp	$⊢ 2 \in ℕ \to \frac{d (x \in ℂ⟼ x^{2})}{d_{ℂ} x} = (x \in ℂ ⟼ 2 x^{2 - 1})$
224	222 223	ax-mp	$⊢ \frac{d (x \in ℂ⟼ x^{2})}{d_{ℂ} x} = (x \in ℂ ⟼ 2 x^{2 - 1})$
225		2m1e1	$⊢ 2 - 1 = 1$
226	225	oveq2i	$⊢ x^{2 - 1} = x^{1}$
227		exp1	$⊢ x \in ℂ \to x^{1} = x$
228	226 227	eqtrid	$⊢ x \in ℂ \to x^{2 - 1} = x$
229	228	oveq2d	$⊢ x \in ℂ \to 2 x^{2 - 1} = 2 x$
230	229	mpteq2ia	$⊢ (x \in ℂ ⟼ 2 x^{2 - 1}) = (x \in ℂ ⟼ 2 x)$
231	224 230	eqtri	$⊢ \frac{d (x \in ℂ⟼ x^{2})}{d_{ℂ} x} = (x \in ℂ ⟼ 2 x)$
232	231	a1i	$⊢ ⊤ \to \frac{d (x \in ℂ⟼ x^{2})}{d_{ℂ} x} = (x \in ℂ ⟼ 2 x)$
233	11 79 214 216 217 221 232	dvmptsub	$⊢ ⊤ \to \frac{d (x \in ℂ⟼ 1 - x^{2})}{d_{ℂ} x} = (x \in ℂ ⟼ 0 - 2 x)$
234		df-neg	$⊢ - 2 x = 0 - 2 x$
235	234	mpteq2i	$⊢ (x \in ℂ ⟼ - 2 x) = (x \in ℂ ⟼ 0 - 2 x)$
236	233 235	eqtr4di	$⊢ ⊤ \to \frac{d (x \in ℂ⟼ 1 - x^{2})}{d_{ℂ} x} = (x \in ℂ ⟼ - 2 x)$
237	11 213 208 236 81 84 82 103	dvmptres	$⊢ ⊤ \to \frac{d (x \in D⟼ 1 - x^{2})}{d_{ℂ} x} = (x \in D ⟼ - 2 x)$
238		eqid	$⊢ ℂ ∖ (−∞, 0] = ℂ ∖ (−∞, 0]$
239	238	dvcnsqrt	$⊢ \frac{d (y \in (ℂ ∖ (−∞, 0])⟼ \sqrt{y})}{d_{ℂ} y} = (y \in (ℂ ∖ (−∞, 0]) ⟼ \frac{1}{2 \sqrt{y}})$
240	239	a1i	$⊢ ⊤ \to \frac{d (y \in (ℂ ∖ (−∞, 0])⟼ \sqrt{y})}{d_{ℂ} y} = (y \in (ℂ ∖ (−∞, 0]) ⟼ \frac{1}{2 \sqrt{y}})$
241		fveq2	$⊢ y = 1 - x^{2} \to \sqrt{y} = \sqrt{1 - x^{2}}$
242	241	oveq2d	$⊢ y = 1 - x^{2} \to 2 \sqrt{y} = 2 \sqrt{1 - x^{2}}$
243	242	oveq2d	$⊢ y = 1 - x^{2} \to \frac{1}{2 \sqrt{y}} = \frac{1}{2 \sqrt{1 - x^{2}}}$
244	11 11 203 209 211 212 237 240 241 243	dvmptco	$⊢ ⊤ \to \frac{d (x \in D⟼ \sqrt{1 - x^{2}})}{d_{ℂ} x} = (x \in D ⟼ (\frac{1}{2 \sqrt{1 - x^{2}}}) (- 2 x))$
245		mulneg2	$⊢ (2 \in ℂ \land x \in ℂ) \to 2 (- x) = - 2 x$
246	218 12 245	sylancr	$⊢ x \in D \to 2 (- x) = - 2 x$
247	246	oveq1d	$⊢ x \in D \to \frac{2 (- x)}{2 \sqrt{1 - x^{2}}} = \frac{- 2 x}{2 \sqrt{1 - x^{2}}}$
248	12	negcld	$⊢ x \in D \to - x \in ℂ$
249		eldifn	$⊢ x \in (ℂ ∖ ((−∞, - 1] \cup [1, +∞))) \to \neg x \in ((−∞, - 1] \cup [1, +∞))$
250	249 1	eleq2s	$⊢ x \in D \to \neg x \in ((−∞, - 1] \cup [1, +∞))$
251		id	$⊢ x = - 1 \to x = - 1$
252		mnflt	$⊢ - 1 \in ℝ \to −∞ < - 1$
253	86 252	ax-mp	$⊢ −∞ < - 1$
254		ubioc1	$⊢ (−∞ \in ℝ^{} \land - 1 \in ℝ^{} \land −∞ < - 1) \to - 1 \in (−∞, - 1]$
255	51 132 253 254	mp3an	$⊢ - 1 \in (−∞, - 1]$
256	251 255	eqeltrdi	$⊢ x = - 1 \to x \in (−∞, - 1]$
257		id	$⊢ x = 1 \to x = 1$
258		ltpnf	$⊢ 1 \in ℝ \to 1 < +∞$
259	89 258	ax-mp	$⊢ 1 < +∞$
260		lbico1	$⊢ (1 \in ℝ^{} \land +∞ \in ℝ^{} \land 1 < +∞) \to 1 \in [1, +∞)$
261	133 121 259 260	mp3an	$⊢ 1 \in [1, +∞)$
262	257 261	eqeltrdi	$⊢ x = 1 \to x \in [1, +∞)$
263	256 262	orim12i	$⊢ (x = - 1 \lor x = 1) \to (x \in (−∞, - 1] \lor x \in [1, +∞))$
264	263	orcoms	$⊢ (x = 1 \lor x = - 1) \to (x \in (−∞, - 1] \lor x \in [1, +∞))$
265		elun	$⊢ x \in ((−∞, - 1] \cup [1, +∞)) \leftrightarrow (x \in (−∞, - 1] \lor x \in [1, +∞))$
266	264 265	sylibr	$⊢ (x = 1 \lor x = - 1) \to x \in ((−∞, - 1] \cup [1, +∞))$
267	250 266	nsyl	$⊢ x \in D \to \neg (x = 1 \lor x = - 1)$
268		1cnd	$⊢ (x \in ℂ \land \sqrt{1 - x^{2}} = 0) \to 1 \in ℂ$
269	17	adantr	$⊢ (x \in ℂ \land \sqrt{1 - x^{2}} = 0) \to x^{2} \in ℂ$
270	19	adantr	$⊢ (x \in ℂ \land \sqrt{1 - x^{2}} = 0) \to 1 - x^{2} \in ℂ$
271		simpr	$⊢ (x \in ℂ \land \sqrt{1 - x^{2}} = 0) \to \sqrt{1 - x^{2}} = 0$
272	270 271	sqr00d	$⊢ (x \in ℂ \land \sqrt{1 - x^{2}} = 0) \to 1 - x^{2} = 0$
273	268 269 272	subeq0d	$⊢ (x \in ℂ \land \sqrt{1 - x^{2}} = 0) \to 1 = x^{2}$
274	146 273	eqtr2id	$⊢ (x \in ℂ \land \sqrt{1 - x^{2}} = 0) \to x^{2} = 1^{2}$
275	274	ex	$⊢ x \in ℂ \to (\sqrt{1 - x^{2}} = 0 \to x^{2} = 1^{2})$
276		sqeqor	$⊢ (x \in ℂ \land 1 \in ℂ) \to (x^{2} = 1^{2} \leftrightarrow (x = 1 \lor x = - 1))$
277	16 276	mpan2	$⊢ x \in ℂ \to (x^{2} = 1^{2} \leftrightarrow (x = 1 \lor x = - 1))$
278	275 277	sylibd	$⊢ x \in ℂ \to (\sqrt{1 - x^{2}} = 0 \to (x = 1 \lor x = - 1))$
279	278	necon3bd	$⊢ x \in ℂ \to (\neg (x = 1 \lor x = - 1) \to \sqrt{1 - x^{2}} \neq 0)$
280	12 267 279	sylc	$⊢ x \in D \to \sqrt{1 - x^{2}} \neq 0$
281		2cnne0	$⊢ (2 \in ℂ \land 2 \neq 0)$
282		divcan5	$⊢ (- x \in ℂ \land (\sqrt{1 - x^{2}} \in ℂ \land \sqrt{1 - x^{2}} \neq 0) \land (2 \in ℂ \land 2 \neq 0)) \to \frac{2 (- x)}{2 \sqrt{1 - x^{2}}} = \frac{- x}{\sqrt{1 - x^{2}}}$
283	281 282	mp3an3	$⊢ (- x \in ℂ \land (\sqrt{1 - x^{2}} \in ℂ \land \sqrt{1 - x^{2}} \neq 0)) \to \frac{2 (- x)}{2 \sqrt{1 - x^{2}}} = \frac{- x}{\sqrt{1 - x^{2}}}$
284	248 112 280 283	syl12anc	$⊢ x \in D \to \frac{2 (- x)}{2 \sqrt{1 - x^{2}}} = \frac{- x}{\sqrt{1 - x^{2}}}$
285	218 12 219	sylancr	$⊢ x \in D \to 2 x \in ℂ$
286	285	negcld	$⊢ x \in D \to - 2 x \in ℂ$
287		mulcl	$⊢ (2 \in ℂ \land \sqrt{1 - x^{2}} \in ℂ) \to 2 \sqrt{1 - x^{2}} \in ℂ$
288	218 112 287	sylancr	$⊢ x \in D \to 2 \sqrt{1 - x^{2}} \in ℂ$
289		mulne0	$⊢ ((2 \in ℂ \land 2 \neq 0) \land (\sqrt{1 - x^{2}} \in ℂ \land \sqrt{1 - x^{2}} \neq 0)) \to 2 \sqrt{1 - x^{2}} \neq 0$
290	281 289	mpan	$⊢ (\sqrt{1 - x^{2}} \in ℂ \land \sqrt{1 - x^{2}} \neq 0) \to 2 \sqrt{1 - x^{2}} \neq 0$
291	112 280 290	syl2anc	$⊢ x \in D \to 2 \sqrt{1 - x^{2}} \neq 0$
292	286 288 291	divrec2d	$⊢ x \in D \to \frac{- 2 x}{2 \sqrt{1 - x^{2}}} = (\frac{1}{2 \sqrt{1 - x^{2}}}) (- 2 x)$
293	247 284 292	3eqtr3rd	$⊢ x \in D \to (\frac{1}{2 \sqrt{1 - x^{2}}}) (- 2 x) = \frac{- x}{\sqrt{1 - x^{2}}}$
294	293	mpteq2ia	$⊢ (x \in D ⟼ (\frac{1}{2 \sqrt{1 - x^{2}}}) (- 2 x)) = (x \in D ⟼ \frac{- x}{\sqrt{1 - x^{2}}})$
295	244 294	eqtrdi	$⊢ ⊤ \to \frac{d (x \in D⟼ \sqrt{1 - x^{2}})}{d_{ℂ} x} = (x \in D ⟼ \frac{- x}{\sqrt{1 - x^{2}}})$
296	11 74 75 109 113 114 295	dvmptadd	$⊢ ⊤ \to \frac{d (x \in D⟼ i x + \sqrt{1 - x^{2}})}{d_{ℂ} x} = (x \in D ⟼ i + (\frac{- x}{\sqrt{1 - x^{2}}}))$
297		mulcl	$⊢ (i \in ℂ \land \sqrt{1 - x^{2}} \in ℂ) \to i \sqrt{1 - x^{2}} \in ℂ$
298	13 20 297	sylancr	$⊢ x \in ℂ \to i \sqrt{1 - x^{2}} \in ℂ$
299	12 298	syl	$⊢ x \in D \to i \sqrt{1 - x^{2}} \in ℂ$
300	299 248 112 280	divdird	$⊢ x \in D \to \frac{i \sqrt{1 - x^{2}} + (- x)}{\sqrt{1 - x^{2}}} = (\frac{i \sqrt{1 - x^{2}}}{\sqrt{1 - x^{2}}}) + (\frac{- x}{\sqrt{1 - x^{2}}})$
301		ixi	$⊢ i i = - 1$
302	301	eqcomi	$⊢ - 1 = i i$
303	302	oveq1i	$⊢ -1 x = i i x$
304		mulm1	$⊢ x \in ℂ \to -1 x = - x$
305		mulass	$⊢ (i \in ℂ \land i \in ℂ \land x \in ℂ) \to i i x = i i x$
306	13 13 305	mp3an12	$⊢ x \in ℂ \to i i x = i i x$
307	303 304 306	3eqtr3a	$⊢ x \in ℂ \to - x = i i x$
308	307	oveq1d	$⊢ x \in ℂ \to - x + i \sqrt{1 - x^{2}} = i i x + i \sqrt{1 - x^{2}}$
309		negcl	$⊢ x \in ℂ \to - x \in ℂ$
310	298 309	addcomd	$⊢ x \in ℂ \to i \sqrt{1 - x^{2}} + (- x) = - x + i \sqrt{1 - x^{2}}$
311	13	a1i	$⊢ x \in ℂ \to i \in ℂ$
312	311 15 20	adddid	$⊢ x \in ℂ \to i (i x + \sqrt{1 - x^{2}}) = i i x + i \sqrt{1 - x^{2}}$
313	308 310 312	3eqtr4d	$⊢ x \in ℂ \to i \sqrt{1 - x^{2}} + (- x) = i (i x + \sqrt{1 - x^{2}})$
314	12 313	syl	$⊢ x \in D \to i \sqrt{1 - x^{2}} + (- x) = i (i x + \sqrt{1 - x^{2}})$
315	314	oveq1d	$⊢ x \in D \to \frac{i \sqrt{1 - x^{2}} + (- x)}{\sqrt{1 - x^{2}}} = \frac{i (i x + \sqrt{1 - x^{2}})}{\sqrt{1 - x^{2}}}$
316	72 112 280	divcan4d	$⊢ x \in D \to \frac{i \sqrt{1 - x^{2}}}{\sqrt{1 - x^{2}}} = i$
317	316	oveq1d	$⊢ x \in D \to (\frac{i \sqrt{1 - x^{2}}}{\sqrt{1 - x^{2}}}) + (\frac{- x}{\sqrt{1 - x^{2}}}) = i + (\frac{- x}{\sqrt{1 - x^{2}}})$
318	300 315 317	3eqtr3rd	$⊢ x \in D \to i + (\frac{- x}{\sqrt{1 - x^{2}}}) = \frac{i (i x + \sqrt{1 - x^{2}})}{\sqrt{1 - x^{2}}}$
319	318	mpteq2ia	$⊢ (x \in D ⟼ i + (\frac{- x}{\sqrt{1 - x^{2}}})) = (x \in D ⟼ \frac{i (i x + \sqrt{1 - x^{2}})}{\sqrt{1 - x^{2}}})$
320	296 319	eqtrdi	$⊢ ⊤ \to \frac{d (x \in D⟼ i x + \sqrt{1 - x^{2}})}{d_{ℂ} x} = (x \in D ⟼ \frac{i (i x + \sqrt{1 - x^{2}})}{\sqrt{1 - x^{2}}})$
321		logf1o	$⊢ log : ℂ ∖ \{0\} \underset{1-1 onto}{⟶} ran log$
322		f1of	$⊢ log : ℂ ∖ \{0\} \underset{1-1 onto}{⟶} ran log \to log : ℂ ∖ \{0\} ⟶ ran log$
323	321 322	mp1i	$⊢ ⊤ \to log : ℂ ∖ \{0\} ⟶ ran log$
324		snssi	$⊢ 0 \in (−∞, 0] \to \{0\} \subseteq (−∞, 0]$
325	64 324	ax-mp	$⊢ \{0\} \subseteq (−∞, 0]$
326		sscon	$⊢ \{0\} \subseteq (−∞, 0] \to ℂ ∖ (−∞, 0] \subseteq ℂ ∖ \{0\}$
327	325 326	mp1i	$⊢ ⊤ \to ℂ ∖ (−∞, 0] \subseteq ℂ ∖ \{0\}$
328	323 327	feqresmpt	$⊢ ⊤ \to {log ↾}_{(ℂ ∖ (−∞, 0])} = (y \in (ℂ ∖ (−∞, 0]) ⟼ \log y)$
329	328	oveq2d	$⊢ ⊤ \to ℂ D ({log ↾}_{(ℂ ∖ (−∞, 0])}) = \frac{d (y \in (ℂ ∖ (−∞, 0])⟼ \log y)}{d_{ℂ} y}$
330	238	dvlog	$⊢ ℂ D ({log ↾}_{(ℂ ∖ (−∞, 0])}) = (y \in (ℂ ∖ (−∞, 0]) ⟼ \frac{1}{y})$
331	329 330	eqtr3di	$⊢ ⊤ \to \frac{d (y \in (ℂ ∖ (−∞, 0])⟼ \log y)}{d_{ℂ} y} = (y \in (ℂ ∖ (−∞, 0]) ⟼ \frac{1}{y})$
332		fveq2	$⊢ y = i x + \sqrt{1 - x^{2}} \to \log y = \log (i x + \sqrt{1 - x^{2}})$
333		oveq2	$⊢ y = i x + \sqrt{1 - x^{2}} \to \frac{1}{y} = \frac{1}{i x + \sqrt{1 - x^{2}}}$
334	11 11 57 58 70 71 320 331 332 333	dvmptco	$⊢ ⊤ \to \frac{d (x \in D⟼ \log (i x + \sqrt{1 - x^{2}}))}{d_{ℂ} x} = (x \in D ⟼ (\frac{1}{i x + \sqrt{1 - x^{2}}}) (\frac{i (i x + \sqrt{1 - x^{2}})}{\sqrt{1 - x^{2}}}))$
335	22 24	reccld	$⊢ x \in D \to \frac{1}{i x + \sqrt{1 - x^{2}}} \in ℂ$
336		mulcl	$⊢ (i \in ℂ \land i x + \sqrt{1 - x^{2}} \in ℂ) \to i (i x + \sqrt{1 - x^{2}}) \in ℂ$
337	13 21 336	sylancr	$⊢ x \in ℂ \to i (i x + \sqrt{1 - x^{2}}) \in ℂ$
338	12 337	syl	$⊢ x \in D \to i (i x + \sqrt{1 - x^{2}}) \in ℂ$
339	335 338 112 280	divassd	$⊢ x \in D \to \frac{(\frac{1}{i x + \sqrt{1 - x^{2}}}) i (i x + \sqrt{1 - x^{2}})}{\sqrt{1 - x^{2}}} = (\frac{1}{i x + \sqrt{1 - x^{2}}}) (\frac{i (i x + \sqrt{1 - x^{2}})}{\sqrt{1 - x^{2}}})$
340	338 22 24	divrec2d	$⊢ x \in D \to \frac{i (i x + \sqrt{1 - x^{2}})}{i x + \sqrt{1 - x^{2}}} = (\frac{1}{i x + \sqrt{1 - x^{2}}}) i (i x + \sqrt{1 - x^{2}})$
341	72 22 24	divcan4d	$⊢ x \in D \to \frac{i (i x + \sqrt{1 - x^{2}})}{i x + \sqrt{1 - x^{2}}} = i$
342	340 341	eqtr3d	$⊢ x \in D \to (\frac{1}{i x + \sqrt{1 - x^{2}}}) i (i x + \sqrt{1 - x^{2}}) = i$
343	342	oveq1d	$⊢ x \in D \to \frac{(\frac{1}{i x + \sqrt{1 - x^{2}}}) i (i x + \sqrt{1 - x^{2}})}{\sqrt{1 - x^{2}}} = \frac{i}{\sqrt{1 - x^{2}}}$
344	339 343	eqtr3d	$⊢ x \in D \to (\frac{1}{i x + \sqrt{1 - x^{2}}}) (\frac{i (i x + \sqrt{1 - x^{2}})}{\sqrt{1 - x^{2}}}) = \frac{i}{\sqrt{1 - x^{2}}}$
345	344	mpteq2ia	$⊢ (x \in D ⟼ (\frac{1}{i x + \sqrt{1 - x^{2}}}) (\frac{i (i x + \sqrt{1 - x^{2}})}{\sqrt{1 - x^{2}}})) = (x \in D ⟼ \frac{i}{\sqrt{1 - x^{2}}})$
346	334 345	eqtrdi	$⊢ ⊤ \to \frac{d (x \in D⟼ \log (i x + \sqrt{1 - x^{2}}))}{d_{ℂ} x} = (x \in D ⟼ \frac{i}{\sqrt{1 - x^{2}}})$
347		negicn	$⊢ - i \in ℂ$
348	347	a1i	$⊢ ⊤ \to - i \in ℂ$
349	11 26 27 346 348	dvmptcmul	$⊢ ⊤ \to \frac{d (x \in D⟼ (- i) \log (i x + \sqrt{1 - x^{2}}))}{d_{ℂ} x} = (x \in D ⟼ (- i) (\frac{i}{\sqrt{1 - x^{2}}}))$
350	349	mptru	$⊢ \frac{d (x \in D⟼ (- i) \log (i x + \sqrt{1 - x^{2}}))}{d_{ℂ} x} = (x \in D ⟼ (- i) (\frac{i}{\sqrt{1 - x^{2}}}))$
351		divass	$⊢ (- i \in ℂ \land i \in ℂ \land (\sqrt{1 - x^{2}} \in ℂ \land \sqrt{1 - x^{2}} \neq 0)) \to \frac{(- i) i}{\sqrt{1 - x^{2}}} = (- i) (\frac{i}{\sqrt{1 - x^{2}}})$
352	347 13 351	mp3an12	$⊢ (\sqrt{1 - x^{2}} \in ℂ \land \sqrt{1 - x^{2}} \neq 0) \to \frac{(- i) i}{\sqrt{1 - x^{2}}} = (- i) (\frac{i}{\sqrt{1 - x^{2}}})$
353	112 280 352	syl2anc	$⊢ x \in D \to \frac{(- i) i}{\sqrt{1 - x^{2}}} = (- i) (\frac{i}{\sqrt{1 - x^{2}}})$
354	13 13	mulneg1i	$⊢ (- i) i = - i i$
355	301	negeqi	$⊢ - i i = - -1$
356		negneg1e1	$⊢ - -1 = 1$
357	354 355 356	3eqtri	$⊢ (- i) i = 1$
358	357	oveq1i	$⊢ \frac{(- i) i}{\sqrt{1 - x^{2}}} = \frac{1}{\sqrt{1 - x^{2}}}$
359	353 358	eqtr3di	$⊢ x \in D \to (- i) (\frac{i}{\sqrt{1 - x^{2}}}) = \frac{1}{\sqrt{1 - x^{2}}}$
360	359	mpteq2ia	$⊢ (x \in D ⟼ (- i) (\frac{i}{\sqrt{1 - x^{2}}})) = (x \in D ⟼ \frac{1}{\sqrt{1 - x^{2}}})$
361	9 350 360	3eqtri	$⊢ ℂ D ({arcsin ↾}_{D}) = (x \in D ⟼ \frac{1}{\sqrt{1 - x^{2}}})$

Metamath Proof Explorer

Theorem dvasin

Proof