dvasin - Mathbox for Brendan Leahy

	Mathbox for Brendan Leahy		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > dvasin		Structured version Visualization version GIF version

Theorem dvasin 33626

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

**Hypothesis**
Ref	Expression
dvasin.d	⊢ 𝐷 = (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞)))

**Assertion**
Ref	Expression
dvasin	⊢ (ℂ D (arcsin ↾ 𝐷)) = (𝑥 ∈ 𝐷 ↦ (1 / (√‘(1 − (𝑥↑2)))))

Distinct variable group: 𝑥,𝐷

Proof of Theorem dvasin Dummy variables 𝑦 𝑧 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-asin 24637	. . . . 5 ⊢ arcsin = (𝑥 ∈ ℂ ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))
2	1	reseq1i 5424	. . . 4 ⊢ (arcsin ↾ 𝐷) = ((𝑥 ∈ ℂ ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))) ↾ 𝐷)
3		dvasin.d	. . . . . 6 ⊢ 𝐷 = (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞)))
4		difss 3770	. . . . . 6 ⊢ (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞))) ⊆ ℂ
5	3, 4	eqsstri 3668	. . . . 5 ⊢ 𝐷 ⊆ ℂ
6		resmpt 5484	. . . . 5 ⊢ (𝐷 ⊆ ℂ → ((𝑥 ∈ ℂ ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))) ↾ 𝐷) = (𝑥 ∈ 𝐷 ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))))
7	5, 6	ax-mp 5	. . . 4 ⊢ ((𝑥 ∈ ℂ ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))) ↾ 𝐷) = (𝑥 ∈ 𝐷 ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))
8	2, 7	eqtri 2673	. . 3 ⊢ (arcsin ↾ 𝐷) = (𝑥 ∈ 𝐷 ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))
9	8	oveq2i 6701	. 2 ⊢ (ℂ D (arcsin ↾ 𝐷)) = (ℂ D (𝑥 ∈ 𝐷 ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))))
10		cnelprrecn 10067	. . . . 5 ⊢ ℂ ∈ {ℝ, ℂ}
11	10	a1i 11	. . . 4 ⊢ (⊤ → ℂ ∈ {ℝ, ℂ})
12	5	sseli 3632	. . . . . . 7 ⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ ℂ)
13		ax-icn 10033	. . . . . . . . 9 ⊢ i ∈ ℂ
14		mulcl 10058	. . . . . . . . 9 ⊢ ((i ∈ ℂ ∧ 𝑥 ∈ ℂ) → (i · 𝑥) ∈ ℂ)
15	13, 14	mpan 706	. . . . . . . 8 ⊢ (𝑥 ∈ ℂ → (i · 𝑥) ∈ ℂ)
16		ax-1cn 10032	. . . . . . . . . 10 ⊢ 1 ∈ ℂ
17		sqcl 12965	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℂ → (𝑥↑2) ∈ ℂ)
18		subcl 10318	. . . . . . . . . 10 ⊢ ((1 ∈ ℂ ∧ (𝑥↑2) ∈ ℂ) → (1 − (𝑥↑2)) ∈ ℂ)
19	16, 17, 18	sylancr 696	. . . . . . . . 9 ⊢ (𝑥 ∈ ℂ → (1 − (𝑥↑2)) ∈ ℂ)
20	19	sqrtcld 14220	. . . . . . . 8 ⊢ (𝑥 ∈ ℂ → (√‘(1 − (𝑥↑2))) ∈ ℂ)
21	15, 20	addcld 10097	. . . . . . 7 ⊢ (𝑥 ∈ ℂ → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℂ)
22	12, 21	syl 17	. . . . . 6 ⊢ (𝑥 ∈ 𝐷 → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℂ)
23		asinlem 24640	. . . . . . 7 ⊢ (𝑥 ∈ ℂ → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≠ 0)
24	12, 23	syl 17	. . . . . 6 ⊢ (𝑥 ∈ 𝐷 → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≠ 0)
25	22, 24	logcld 24362	. . . . 5 ⊢ (𝑥 ∈ 𝐷 → (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
26	25	adantl 481	. . . 4 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
27		ovexd 6720	. . . 4 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → (i / (√‘(1 − (𝑥↑2)))) ∈ V)
28		simpr 476	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ)
29		asinlem3 24643	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℂ → 0 ≤ (ℜ‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
30		rere 13906	. . . . . . . . . . . . . . . . . . 19 ⊢ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → (ℜ‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) = ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))
31	30	breq2d 4697	. . . . . . . . . . . . . . . . . 18 ⊢ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → (0 ≤ (ℜ‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ↔ 0 ≤ ((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
32	31	biimpac 502	. . . . . . . . . . . . . . . . 17 ⊢ ((0 ≤ (ℜ‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → 0 ≤ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))
33	29, 32	sylan 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → 0 ≤ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))
34	23	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≠ 0)
35	28, 33, 34	ne0gt0d 10212	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → 0 < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))
36		0re 10078	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ ℝ
37		ltnle 10155	. . . . . . . . . . . . . . . . 17 ⊢ ((0 ∈ ℝ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → (0 < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ↔ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
38	36, 37	mpan 706	. . . . . . . . . . . . . . . 16 ⊢ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → (0 < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ↔ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
39	38	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → (0 < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ↔ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
40	35, 39	mpbid 222	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0)
41	40	ex 449	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℂ → (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
42	12, 41	syl 17	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐷 → (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
43		imor 427	. . . . . . . . . . . 12 ⊢ ((((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0) ↔ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
44	42, 43	sylib 208	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐷 → (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
45	44	orcomd 402	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐷 → (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ))
46	45	olcd 407	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → (¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ)))
47		3ianor 1074	. . . . . . . . . . 11 ⊢ (¬ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∧ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0) ↔ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∨ ¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
48		3orrot 1061	. . . . . . . . . . 11 ⊢ ((¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∨ ¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0) ↔ (¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ))
49		3orass 1057	. . . . . . . . . . 11 ⊢ ((¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) ↔ (¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ)))
50	47, 48, 49	3bitrri 287	. . . . . . . . . 10 ⊢ ((¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ)) ↔ ¬ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∧ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
51		mnfxr 10134	. . . . . . . . . . 11 ⊢ -∞ ∈ ℝ^*
52		elioc2 12274	. . . . . . . . . . 11 ⊢ ((-∞ ∈ ℝ^* ∧ 0 ∈ ℝ) → (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (-∞(,]0) ↔ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∧ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0)))
53	51, 36, 52	mp2an 708	. . . . . . . . . 10 ⊢ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (-∞(,]0) ↔ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∧ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
54	50, 53	xchbinxr 324	. . . . . . . . 9 ⊢ ((¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ)) ↔ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (-∞(,]0))
55	46, 54	sylib 208	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐷 → ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (-∞(,]0))
56	22, 55	eldifd 3618	. . . . . . 7 ⊢ (𝑥 ∈ 𝐷 → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (ℂ ∖ (-∞(,]0)))
57	56	adantl 481	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (ℂ ∖ (-∞(,]0)))
58		ovexd 6720	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))) ∈ V)
59		eldifi 3765	. . . . . . . 8 ⊢ (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → 𝑦 ∈ ℂ)
60		eldifn 3766	. . . . . . . . 9 ⊢ (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → ¬ 𝑦 ∈ (-∞(,]0))
61		0xr 10124	. . . . . . . . . . . 12 ⊢ 0 ∈ ℝ^*
62		mnflt0 11997	. . . . . . . . . . . 12 ⊢ -∞ < 0
63		ubioc1 12265	. . . . . . . . . . . 12 ⊢ ((-∞ ∈ ℝ^* ∧ 0 ∈ ℝ^* ∧ -∞ < 0) → 0 ∈ (-∞(,]0))
64	51, 61, 62, 63	mp3an 1464	. . . . . . . . . . 11 ⊢ 0 ∈ (-∞(,]0)
65		eleq1 2718	. . . . . . . . . . 11 ⊢ (𝑦 = 0 → (𝑦 ∈ (-∞(,]0) ↔ 0 ∈ (-∞(,]0)))
66	64, 65	mpbiri 248	. . . . . . . . . 10 ⊢ (𝑦 = 0 → 𝑦 ∈ (-∞(,]0))
67	66	necon3bi 2849	. . . . . . . . 9 ⊢ (¬ 𝑦 ∈ (-∞(,]0) → 𝑦 ≠ 0)
68	60, 67	syl 17	. . . . . . . 8 ⊢ (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → 𝑦 ≠ 0)
69	59, 68	logcld 24362	. . . . . . 7 ⊢ (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → (log‘𝑦) ∈ ℂ)
70	69	adantl 481	. . . . . 6 ⊢ ((⊤ ∧ 𝑦 ∈ (ℂ ∖ (-∞(,]0))) → (log‘𝑦) ∈ ℂ)
71		ovexd 6720	. . . . . 6 ⊢ ((⊤ ∧ 𝑦 ∈ (ℂ ∖ (-∞(,]0))) → (1 / 𝑦) ∈ V)
72	13	a1i 11	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐷 → i ∈ ℂ)
73	72, 12	mulcld 10098	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → (i · 𝑥) ∈ ℂ)
74	73	adantl 481	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → (i · 𝑥) ∈ ℂ)
75	13	a1i 11	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → i ∈ ℂ)
76	12	adantl 481	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ ℂ)
77		1cnd 10094	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → 1 ∈ ℂ)
78		simpr 476	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → 𝑥 ∈ ℂ)
79		1cnd 10094	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → 1 ∈ ℂ)
80	11	dvmptid 23765	. . . . . . . . . . 11 ⊢ (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ 𝑥)) = (𝑥 ∈ ℂ ↦ 1))
81	5	a1i 11	. . . . . . . . . . 11 ⊢ (⊤ → 𝐷 ⊆ ℂ)
82		eqid 2651	. . . . . . . . . . . . . 14 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
83	82	cnfldtopon 22633	. . . . . . . . . . . . 13 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
84	83	toponunii 20769	. . . . . . . . . . . . . 14 ⊢ ℂ = ∪ (TopOpen‘ℂ_fld)
85	84	restid 16141	. . . . . . . . . . . . 13 ⊢ ((TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ) → ((TopOpen‘ℂ_fld) ↾_t ℂ) = (TopOpen‘ℂ_fld))
86	83, 85	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((TopOpen‘ℂ_fld) ↾_t ℂ) = (TopOpen‘ℂ_fld)
87	86	eqcomi 2660	. . . . . . . . . . 11 ⊢ (TopOpen‘ℂ_fld) = ((TopOpen‘ℂ_fld) ↾_t ℂ)
88	82	recld2 22664	. . . . . . . . . . . . . . 15 ⊢ ℝ ∈ (Clsd‘(TopOpen‘ℂ_fld))
89		neg1rr 11163	. . . . . . . . . . . . . . . . . 18 ⊢ -1 ∈ ℝ
90		iocmnfcld 22619	. . . . . . . . . . . . . . . . . 18 ⊢ (-1 ∈ ℝ → (-∞(,]-1) ∈ (Clsd‘(topGen‘ran (,))))
91	89, 90	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (-∞(,]-1) ∈ (Clsd‘(topGen‘ran (,)))
92		1re 10077	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℝ
93		icopnfcld 22618	. . . . . . . . . . . . . . . . . 18 ⊢ (1 ∈ ℝ → (1[,)+∞) ∈ (Clsd‘(topGen‘ran (,))))
94	92, 93	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (1[,)+∞) ∈ (Clsd‘(topGen‘ran (,)))
95		uncld 20893	. . . . . . . . . . . . . . . . 17 ⊢ (((-∞(,]-1) ∈ (Clsd‘(topGen‘ran (,))) ∧ (1[,)+∞) ∈ (Clsd‘(topGen‘ran (,)))) → ((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘(topGen‘ran (,))))
96	91, 94, 95	mp2an 708	. . . . . . . . . . . . . . . 16 ⊢ ((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘(topGen‘ran (,)))
97	82	tgioo2 22653	. . . . . . . . . . . . . . . . 17 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
98	97	fveq2i 6232	. . . . . . . . . . . . . . . 16 ⊢ (Clsd‘(topGen‘ran (,))) = (Clsd‘((TopOpen‘ℂ_fld) ↾_t ℝ))
99	96, 98	eleqtri 2728	. . . . . . . . . . . . . . 15 ⊢ ((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘((TopOpen‘ℂ_fld) ↾_t ℝ))
100		restcldr 21026	. . . . . . . . . . . . . . 15 ⊢ ((ℝ ∈ (Clsd‘(TopOpen‘ℂ_fld)) ∧ ((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘((TopOpen‘ℂ_fld) ↾_t ℝ))) → ((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘(TopOpen‘ℂ_fld)))
101	88, 99, 100	mp2an 708	. . . . . . . . . . . . . 14 ⊢ ((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘(TopOpen‘ℂ_fld))
102	84	cldopn 20883	. . . . . . . . . . . . . 14 ⊢ (((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘(TopOpen‘ℂ_fld)) → (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞))) ∈ (TopOpen‘ℂ_fld))
103	101, 102	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞))) ∈ (TopOpen‘ℂ_fld)
104	3, 103	eqeltri 2726	. . . . . . . . . . . 12 ⊢ 𝐷 ∈ (TopOpen‘ℂ_fld)
105	104	a1i 11	. . . . . . . . . . 11 ⊢ (⊤ → 𝐷 ∈ (TopOpen‘ℂ_fld))
106	11, 78, 79, 80, 81, 87, 82, 105	dvmptres 23771	. . . . . . . . . 10 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ 𝑥)) = (𝑥 ∈ 𝐷 ↦ 1))
107	13	a1i 11	. . . . . . . . . 10 ⊢ (⊤ → i ∈ ℂ)
108	11, 76, 77, 106, 107	dvmptcmul 23772	. . . . . . . . 9 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ (i · 𝑥))) = (𝑥 ∈ 𝐷 ↦ (i · 1)))
109	13	mulid1i 10080	. . . . . . . . . 10 ⊢ (i · 1) = i
110	109	mpteq2i 4774	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 ↦ (i · 1)) = (𝑥 ∈ 𝐷 ↦ i)
111	108, 110	syl6eq 2701	. . . . . . . 8 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ (i · 𝑥))) = (𝑥 ∈ 𝐷 ↦ i))
112	12	sqcld 13046	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐷 → (𝑥↑2) ∈ ℂ)
113	16, 112, 18	sylancr 696	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐷 → (1 − (𝑥↑2)) ∈ ℂ)
114	113	sqrtcld 14220	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → (√‘(1 − (𝑥↑2))) ∈ ℂ)
115	114	adantl 481	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → (√‘(1 − (𝑥↑2))) ∈ ℂ)
116		ovexd 6720	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → (-𝑥 / (√‘(1 − (𝑥↑2)))) ∈ V)
117		elin 3829	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐷 ∩ ℝ) ↔ (𝑥 ∈ 𝐷 ∧ 𝑥 ∈ ℝ))
118	3	asindmre 33625	. . . . . . . . . . . . . . . . 17 ⊢ (𝐷 ∩ ℝ) = (-1(,)1)
119	118	eqimssi 3692	. . . . . . . . . . . . . . . 16 ⊢ (𝐷 ∩ ℝ) ⊆ (-1(,)1)
120	119	sseli 3632	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐷 ∩ ℝ) → 𝑥 ∈ (-1(,)1))
121	117, 120	sylbir 225	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ 𝐷 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ (-1(,)1))
122		incom 3838	. . . . . . . . . . . . . . . 16 ⊢ ((0(,)+∞) ∩ (-∞(,]0)) = ((-∞(,]0) ∩ (0(,)+∞))
123		pnfxr 10130	. . . . . . . . . . . . . . . . 17 ⊢ +∞ ∈ ℝ^*
124		df-ioc 12218	. . . . . . . . . . . . . . . . . 18 ⊢ (,] = (𝑥 ∈ ℝ^, 𝑦 ∈ ℝ^ ↦ {𝑧 ∈ ℝ^* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})
125		df-ioo 12217	. . . . . . . . . . . . . . . . . 18 ⊢ (,) = (𝑥 ∈ ℝ^, 𝑦 ∈ ℝ^ ↦ {𝑧 ∈ ℝ^* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
126		xrltnle 10143	. . . . . . . . . . . . . . . . . 18 ⊢ ((0 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) → (0 < 𝑤 ↔ ¬ 𝑤 ≤ 0))
127	124, 125, 126	ixxdisj 12228	. . . . . . . . . . . . . . . . 17 ⊢ ((-∞ ∈ ℝ^* ∧ 0 ∈ ℝ^* ∧ +∞ ∈ ℝ^*) → ((-∞(,]0) ∩ (0(,)+∞)) = ∅)
128	51, 61, 123, 127	mp3an 1464	. . . . . . . . . . . . . . . 16 ⊢ ((-∞(,]0) ∩ (0(,)+∞)) = ∅
129	122, 128	eqtri 2673	. . . . . . . . . . . . . . 15 ⊢ ((0(,)+∞) ∩ (-∞(,]0)) = ∅
130		elioore 12243	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (-1(,)1) → 𝑥 ∈ ℝ)
131	130	resqcld 13075	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (-1(,)1) → (𝑥↑2) ∈ ℝ)
132		resubcl 10383	. . . . . . . . . . . . . . . . . 18 ⊢ ((1 ∈ ℝ ∧ (𝑥↑2) ∈ ℝ) → (1 − (𝑥↑2)) ∈ ℝ)
133	92, 131, 132	sylancr 696	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (-1(,)1) → (1 − (𝑥↑2)) ∈ ℝ)
134	89	rexri 10135	. . . . . . . . . . . . . . . . . . 19 ⊢ -1 ∈ ℝ^*
135	92	rexri 10135	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℝ^*
136		elioo2 12254	. . . . . . . . . . . . . . . . . . 19 ⊢ ((-1 ∈ ℝ^* ∧ 1 ∈ ℝ^*) → (𝑥 ∈ (-1(,)1) ↔ (𝑥 ∈ ℝ ∧ -1 < 𝑥 ∧ 𝑥 < 1)))
137	134, 135, 136	mp2an 708	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (-1(,)1) ↔ (𝑥 ∈ ℝ ∧ -1 < 𝑥 ∧ 𝑥 < 1))
138		recn 10064	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
139	138	abscld 14219	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℝ → (abs‘𝑥) ∈ ℝ)
140	138	absge0d 14227	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℝ → 0 ≤ (abs‘𝑥))
141		0le1 10589	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 ≤ 1
142		lt2sq 12977	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((abs‘𝑥) ∈ ℝ ∧ 0 ≤ (abs‘𝑥)) ∧ (1 ∈ ℝ ∧ 0 ≤ 1)) → ((abs‘𝑥) < 1 ↔ ((abs‘𝑥)↑2) < (1↑2)))
143	92, 141, 142	mpanr12 721	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((abs‘𝑥) ∈ ℝ ∧ 0 ≤ (abs‘𝑥)) → ((abs‘𝑥) < 1 ↔ ((abs‘𝑥)↑2) < (1↑2)))
144	139, 140, 143	syl2anc 694	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℝ → ((abs‘𝑥) < 1 ↔ ((abs‘𝑥)↑2) < (1↑2)))
145		abslt 14098	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑥) < 1 ↔ (-1 < 𝑥 ∧ 𝑥 < 1)))
146	92, 145	mpan2 707	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℝ → ((abs‘𝑥) < 1 ↔ (-1 < 𝑥 ∧ 𝑥 < 1)))
147		absresq 14086	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℝ → ((abs‘𝑥)↑2) = (𝑥↑2))
148		sq1 12998	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1↑2) = 1
149	148	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℝ → (1↑2) = 1)
150	147, 149	breq12d 4698	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℝ → (((abs‘𝑥)↑2) < (1↑2) ↔ (𝑥↑2) < 1))
151		resqcl 12971	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℝ → (𝑥↑2) ∈ ℝ)
152		posdif 10559	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑥↑2) ∈ ℝ ∧ 1 ∈ ℝ) → ((𝑥↑2) < 1 ↔ 0 < (1 − (𝑥↑2))))
153	151, 92, 152	sylancl 695	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℝ → ((𝑥↑2) < 1 ↔ 0 < (1 − (𝑥↑2))))
154	150, 153	bitrd 268	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℝ → (((abs‘𝑥)↑2) < (1↑2) ↔ 0 < (1 − (𝑥↑2))))
155	144, 146, 154	3bitr3d 298	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ → ((-1 < 𝑥 ∧ 𝑥 < 1) ↔ 0 < (1 − (𝑥↑2))))
156	155	biimpd 219	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℝ → ((-1 < 𝑥 ∧ 𝑥 < 1) → 0 < (1 − (𝑥↑2))))
157	156	3impib 1281	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℝ ∧ -1 < 𝑥 ∧ 𝑥 < 1) → 0 < (1 − (𝑥↑2)))
158	137, 157	sylbi 207	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (-1(,)1) → 0 < (1 − (𝑥↑2)))
159	133, 158	elrpd 11907	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (-1(,)1) → (1 − (𝑥↑2)) ∈ ℝ⁺)
160		ioorp 12289	. . . . . . . . . . . . . . . 16 ⊢ (0(,)+∞) = ℝ⁺
161	159, 160	syl6eleqr 2741	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (-1(,)1) → (1 − (𝑥↑2)) ∈ (0(,)+∞))
162		disjel 4056	. . . . . . . . . . . . . . 15 ⊢ ((((0(,)+∞) ∩ (-∞(,]0)) = ∅ ∧ (1 − (𝑥↑2)) ∈ (0(,)+∞)) → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
163	129, 161, 162	sylancr 696	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (-1(,)1) → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
164	121, 163	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝐷 ∧ 𝑥 ∈ ℝ) → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
165		elioc2 12274	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((-∞ ∈ ℝ^* ∧ 0 ∈ ℝ) → ((1 − (𝑥↑2)) ∈ (-∞(,]0) ↔ ((1 − (𝑥↑2)) ∈ ℝ ∧ -∞ < (1 − (𝑥↑2)) ∧ (1 − (𝑥↑2)) ≤ 0)))
166	51, 36, 165	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1 − (𝑥↑2)) ∈ (-∞(,]0) ↔ ((1 − (𝑥↑2)) ∈ ℝ ∧ -∞ < (1 − (𝑥↑2)) ∧ (1 − (𝑥↑2)) ≤ 0))
167	166	biimpi 206	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1 − (𝑥↑2)) ∈ (-∞(,]0) → ((1 − (𝑥↑2)) ∈ ℝ ∧ -∞ < (1 − (𝑥↑2)) ∧ (1 − (𝑥↑2)) ≤ 0))
168	167	simp1d 1093	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1 − (𝑥↑2)) ∈ (-∞(,]0) → (1 − (𝑥↑2)) ∈ ℝ)
169		resubcl 10383	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1 ∈ ℝ ∧ (1 − (𝑥↑2)) ∈ ℝ) → (1 − (1 − (𝑥↑2))) ∈ ℝ)
170	92, 168, 169	sylancr 696	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 − (𝑥↑2)) ∈ (-∞(,]0) → (1 − (1 − (𝑥↑2))) ∈ ℝ)
171		nncan 10348	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1 ∈ ℂ ∧ (𝑥↑2) ∈ ℂ) → (1 − (1 − (𝑥↑2))) = (𝑥↑2))
172	16, 171	mpan 706	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥↑2) ∈ ℂ → (1 − (1 − (𝑥↑2))) = (𝑥↑2))
173	172	eleq1d 2715	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥↑2) ∈ ℂ → ((1 − (1 − (𝑥↑2))) ∈ ℝ ↔ (𝑥↑2) ∈ ℝ))
174	173	biimpa 500	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥↑2) ∈ ℂ ∧ (1 − (1 − (𝑥↑2))) ∈ ℝ) → (𝑥↑2) ∈ ℝ)
175	170, 174	sylan2 490	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (𝑥↑2) ∈ ℝ)
176	168	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (1 − (𝑥↑2)) ∈ ℝ)
177	167	simp3d 1095	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1 − (𝑥↑2)) ∈ (-∞(,]0) → (1 − (𝑥↑2)) ≤ 0)
178	177	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (1 − (𝑥↑2)) ≤ 0)
179		letr 10169	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((1 − (𝑥↑2)) ∈ ℝ ∧ 0 ∈ ℝ ∧ 1 ∈ ℝ) → (((1 − (𝑥↑2)) ≤ 0 ∧ 0 ≤ 1) → (1 − (𝑥↑2)) ≤ 1))
180	36, 92, 179	mp3an23 1456	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1 − (𝑥↑2)) ∈ ℝ → (((1 − (𝑥↑2)) ≤ 0 ∧ 0 ≤ 1) → (1 − (𝑥↑2)) ≤ 1))
181	141, 180	mpan2i 713	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1 − (𝑥↑2)) ∈ ℝ → ((1 − (𝑥↑2)) ≤ 0 → (1 − (𝑥↑2)) ≤ 1))
182	176, 178, 181	sylc 65	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (1 − (𝑥↑2)) ≤ 1)
183		subge0 10579	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1 ∈ ℝ ∧ (1 − (𝑥↑2)) ∈ ℝ) → (0 ≤ (1 − (1 − (𝑥↑2))) ↔ (1 − (𝑥↑2)) ≤ 1))
184	92, 176, 183	sylancr 696	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (0 ≤ (1 − (1 − (𝑥↑2))) ↔ (1 − (𝑥↑2)) ≤ 1))
185	182, 184	mpbird 247	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → 0 ≤ (1 − (1 − (𝑥↑2))))
186	172	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (1 − (1 − (𝑥↑2))) = (𝑥↑2))
187	185, 186	breqtrd 4711	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → 0 ≤ (𝑥↑2))
188	175, 187	resqrtcld 14200	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (√‘(𝑥↑2)) ∈ ℝ)
189	17, 188	sylan 487	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (√‘(𝑥↑2)) ∈ ℝ)
190		eleq1 2718	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (√‘(𝑥↑2)) → (𝑥 ∈ ℝ ↔ (√‘(𝑥↑2)) ∈ ℝ))
191	189, 190	syl5ibrcom 237	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (𝑥 = (√‘(𝑥↑2)) → 𝑥 ∈ ℝ))
192	189	renegcld 10495	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → -(√‘(𝑥↑2)) ∈ ℝ)
193		eleq1 2718	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = -(√‘(𝑥↑2)) → (𝑥 ∈ ℝ ↔ -(√‘(𝑥↑2)) ∈ ℝ))
194	192, 193	syl5ibrcom 237	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (𝑥 = -(√‘(𝑥↑2)) → 𝑥 ∈ ℝ))
195		eqid 2651	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥↑2) = (𝑥↑2)
196		eqsqrtor 14150	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℂ ∧ (𝑥↑2) ∈ ℂ) → ((𝑥↑2) = (𝑥↑2) ↔ (𝑥 = (√‘(𝑥↑2)) ∨ 𝑥 = -(√‘(𝑥↑2)))))
197	17, 196	mpdan 703	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℂ → ((𝑥↑2) = (𝑥↑2) ↔ (𝑥 = (√‘(𝑥↑2)) ∨ 𝑥 = -(√‘(𝑥↑2)))))
198	195, 197	mpbii 223	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℂ → (𝑥 = (√‘(𝑥↑2)) ∨ 𝑥 = -(√‘(𝑥↑2))))
199	198	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (𝑥 = (√‘(𝑥↑2)) ∨ 𝑥 = -(√‘(𝑥↑2))))
200	191, 194, 199	mpjaod 395	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → 𝑥 ∈ ℝ)
201	200	stoic1a 1737	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℂ ∧ ¬ 𝑥 ∈ ℝ) → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
202	12, 201	sylan 487	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝐷 ∧ ¬ 𝑥 ∈ ℝ) → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
203	164, 202	pm2.61dan 849	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐷 → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
204	113, 203	eldifd 3618	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐷 → (1 − (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0)))
205	204	adantl 481	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → (1 − (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0)))
206		2cnd 11131	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℂ → 2 ∈ ℂ)
207		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℂ → 𝑥 ∈ ℂ)
208	206, 207	mulcld 10098	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℂ → (2 · 𝑥) ∈ ℂ)
209	208	negcld 10417	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℂ → -(2 · 𝑥) ∈ ℂ)
210	209	adantl 481	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → -(2 · 𝑥) ∈ ℂ)
211	12, 210	sylan2 490	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → -(2 · 𝑥) ∈ ℂ)
212	59	sqrtcld 14220	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → (√‘𝑦) ∈ ℂ)
213	212	adantl 481	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑦 ∈ (ℂ ∖ (-∞(,]0))) → (√‘𝑦) ∈ ℂ)
214		ovexd 6720	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑦 ∈ (ℂ ∖ (-∞(,]0))) → (1 / (2 · (√‘𝑦))) ∈ V)
215	19	adantl 481	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → (1 − (𝑥↑2)) ∈ ℂ)
216	36	a1i 11	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → 0 ∈ ℝ)
217		1cnd 10094	. . . . . . . . . . . . . 14 ⊢ (⊤ → 1 ∈ ℂ)
218	11, 217	dvmptc 23766	. . . . . . . . . . . . 13 ⊢ (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ 1)) = (𝑥 ∈ ℂ ↦ 0))
219	17	adantl 481	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → (𝑥↑2) ∈ ℂ)
220		2cn 11129	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℂ
221		mulcl 10058	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (2 · 𝑥) ∈ ℂ)
222	220, 221	mpan 706	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℂ → (2 · 𝑥) ∈ ℂ)
223	222	adantl 481	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → (2 · 𝑥) ∈ ℂ)
224		2nn 11223	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℕ
225		dvexp 23761	. . . . . . . . . . . . . . . 16 ⊢ (2 ∈ ℕ → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · (𝑥↑(2 − 1)))))
226	224, 225	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · (𝑥↑(2 − 1))))
227		2m1e1 11173	. . . . . . . . . . . . . . . . . . 19 ⊢ (2 − 1) = 1
228	227	oveq2i 6701	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥↑(2 − 1)) = (𝑥↑1)
229		exp1 12906	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℂ → (𝑥↑1) = 𝑥)
230	228, 229	syl5eq 2697	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℂ → (𝑥↑(2 − 1)) = 𝑥)
231	230	oveq2d 6706	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℂ → (2 · (𝑥↑(2 − 1))) = (2 · 𝑥))
232	231	mpteq2ia 4773	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℂ ↦ (2 · (𝑥↑(2 − 1)))) = (𝑥 ∈ ℂ ↦ (2 · 𝑥))
233	226, 232	eqtri 2673	. . . . . . . . . . . . . 14 ⊢ (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · 𝑥))
234	233	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · 𝑥)))
235	11, 79, 216, 218, 219, 223, 234	dvmptsub 23775	. . . . . . . . . . . 12 ⊢ (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (1 − (𝑥↑2)))) = (𝑥 ∈ ℂ ↦ (0 − (2 · 𝑥))))
236		df-neg 10307	. . . . . . . . . . . . 13 ⊢ -(2 · 𝑥) = (0 − (2 · 𝑥))
237	236	mpteq2i 4774	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℂ ↦ -(2 · 𝑥)) = (𝑥 ∈ ℂ ↦ (0 − (2 · 𝑥)))
238	235, 237	syl6eqr 2703	. . . . . . . . . . 11 ⊢ (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (1 − (𝑥↑2)))) = (𝑥 ∈ ℂ ↦ -(2 · 𝑥)))
239	11, 215, 210, 238, 81, 87, 82, 105	dvmptres 23771	. . . . . . . . . 10 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ (1 − (𝑥↑2)))) = (𝑥 ∈ 𝐷 ↦ -(2 · 𝑥)))
240		eqid 2651	. . . . . . . . . . . 12 ⊢ (ℂ ∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0))
241	240	dvcnsqrt 24530	. . . . . . . . . . 11 ⊢ (ℂ D (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (√‘𝑦))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (1 / (2 · (√‘𝑦))))
242	241	a1i 11	. . . . . . . . . 10 ⊢ (⊤ → (ℂ D (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (√‘𝑦))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (1 / (2 · (√‘𝑦)))))
243		fveq2 6229	. . . . . . . . . 10 ⊢ (𝑦 = (1 − (𝑥↑2)) → (√‘𝑦) = (√‘(1 − (𝑥↑2))))
244	243	oveq2d 6706	. . . . . . . . . . 11 ⊢ (𝑦 = (1 − (𝑥↑2)) → (2 · (√‘𝑦)) = (2 · (√‘(1 − (𝑥↑2)))))
245	244	oveq2d 6706	. . . . . . . . . 10 ⊢ (𝑦 = (1 − (𝑥↑2)) → (1 / (2 · (√‘𝑦))) = (1 / (2 · (√‘(1 − (𝑥↑2))))))
246	11, 11, 205, 211, 213, 214, 239, 242, 243, 245	dvmptco 23780	. . . . . . . . 9 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ (√‘(1 − (𝑥↑2))))) = (𝑥 ∈ 𝐷 ↦ ((1 / (2 · (√‘(1 − (𝑥↑2))))) · -(2 · 𝑥))))
247		mulneg2 10505	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (2 · -𝑥) = -(2 · 𝑥))
248	220, 12, 247	sylancr 696	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐷 → (2 · -𝑥) = -(2 · 𝑥))
249	248	oveq1d 6705	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐷 → ((2 · -𝑥) / (2 · (√‘(1 − (𝑥↑2))))) = (-(2 · 𝑥) / (2 · (√‘(1 − (𝑥↑2))))))
250	12	negcld 10417	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐷 → -𝑥 ∈ ℂ)
251		eldifn 3766	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞))) → ¬ 𝑥 ∈ ((-∞(,]-1) ∪ (1[,)+∞)))
252	251, 3	eleq2s 2748	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐷 → ¬ 𝑥 ∈ ((-∞(,]-1) ∪ (1[,)+∞)))
253		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = -1 → 𝑥 = -1)
254		mnflt 11995	. . . . . . . . . . . . . . . . . . . 20 ⊢ (-1 ∈ ℝ → -∞ < -1)
255	89, 254	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ -∞ < -1
256		ubioc1 12265	. . . . . . . . . . . . . . . . . . 19 ⊢ ((-∞ ∈ ℝ^* ∧ -1 ∈ ℝ^* ∧ -∞ < -1) → -1 ∈ (-∞(,]-1))
257	51, 134, 255, 256	mp3an 1464	. . . . . . . . . . . . . . . . . 18 ⊢ -1 ∈ (-∞(,]-1)
258	253, 257	syl6eqel 2738	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = -1 → 𝑥 ∈ (-∞(,]-1))
259		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 1 → 𝑥 = 1)
260		ltpnf 11992	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 ∈ ℝ → 1 < +∞)
261	92, 260	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 < +∞
262		lbico1 12266	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ ℝ^* ∧ +∞ ∈ ℝ^* ∧ 1 < +∞) → 1 ∈ (1[,)+∞))
263	135, 123, 261, 262	mp3an 1464	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ (1[,)+∞)
264	259, 263	syl6eqel 2738	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 1 → 𝑥 ∈ (1[,)+∞))
265	258, 264	orim12i 537	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = -1 ∨ 𝑥 = 1) → (𝑥 ∈ (-∞(,]-1) ∨ 𝑥 ∈ (1[,)+∞)))
266	265	orcoms 403	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = 1 ∨ 𝑥 = -1) → (𝑥 ∈ (-∞(,]-1) ∨ 𝑥 ∈ (1[,)+∞)))
267		elun 3786	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ((-∞(,]-1) ∪ (1[,)+∞)) ↔ (𝑥 ∈ (-∞(,]-1) ∨ 𝑥 ∈ (1[,)+∞)))
268	266, 267	sylibr 224	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 1 ∨ 𝑥 = -1) → 𝑥 ∈ ((-∞(,]-1) ∪ (1[,)+∞)))
269	252, 268	nsyl 135	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐷 → ¬ (𝑥 = 1 ∨ 𝑥 = -1))
270		1cnd 10094	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → 1 ∈ ℂ)
271	17	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → (𝑥↑2) ∈ ℂ)
272	19	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → (1 − (𝑥↑2)) ∈ ℂ)
273		simpr 476	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → (√‘(1 − (𝑥↑2))) = 0)
274	272, 273	sqr00d 14224	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → (1 − (𝑥↑2)) = 0)
275	270, 271, 274	subeq0d 10438	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → 1 = (𝑥↑2))
276	148, 275	syl5req 2698	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → (𝑥↑2) = (1↑2))
277	276	ex 449	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℂ → ((√‘(1 − (𝑥↑2))) = 0 → (𝑥↑2) = (1↑2)))
278		sqeqor 13018	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑥↑2) = (1↑2) ↔ (𝑥 = 1 ∨ 𝑥 = -1)))
279	16, 278	mpan2 707	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℂ → ((𝑥↑2) = (1↑2) ↔ (𝑥 = 1 ∨ 𝑥 = -1)))
280	277, 279	sylibd 229	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℂ → ((√‘(1 − (𝑥↑2))) = 0 → (𝑥 = 1 ∨ 𝑥 = -1)))
281	280	necon3bd 2837	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℂ → (¬ (𝑥 = 1 ∨ 𝑥 = -1) → (√‘(1 − (𝑥↑2))) ≠ 0))
282	12, 269, 281	sylc 65	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐷 → (√‘(1 − (𝑥↑2))) ≠ 0)
283		2cnne0 11280	. . . . . . . . . . . . 13 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
284		divcan5 10765	. . . . . . . . . . . . 13 ⊢ ((-𝑥 ∈ ℂ ∧ ((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · -𝑥) / (2 · (√‘(1 − (𝑥↑2))))) = (-𝑥 / (√‘(1 − (𝑥↑2)))))
285	283, 284	mp3an3 1453	. . . . . . . . . . . 12 ⊢ ((-𝑥 ∈ ℂ ∧ ((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0)) → ((2 · -𝑥) / (2 · (√‘(1 − (𝑥↑2))))) = (-𝑥 / (√‘(1 − (𝑥↑2)))))
286	250, 114, 282, 285	syl12anc 1364	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐷 → ((2 · -𝑥) / (2 · (√‘(1 − (𝑥↑2))))) = (-𝑥 / (√‘(1 − (𝑥↑2)))))
287	220, 12, 221	sylancr 696	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐷 → (2 · 𝑥) ∈ ℂ)
288	287	negcld 10417	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐷 → -(2 · 𝑥) ∈ ℂ)
289		mulcl 10058	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ∈ ℂ) → (2 · (√‘(1 − (𝑥↑2)))) ∈ ℂ)
290	220, 114, 289	sylancr 696	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐷 → (2 · (√‘(1 − (𝑥↑2)))) ∈ ℂ)
291		mulne0 10707	. . . . . . . . . . . . . 14 ⊢ (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ ((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0)) → (2 · (√‘(1 − (𝑥↑2)))) ≠ 0)
292	283, 291	mpan 706	. . . . . . . . . . . . 13 ⊢ (((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0) → (2 · (√‘(1 − (𝑥↑2)))) ≠ 0)
293	114, 282, 292	syl2anc 694	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐷 → (2 · (√‘(1 − (𝑥↑2)))) ≠ 0)
294	288, 290, 293	divrec2d 10843	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐷 → (-(2 · 𝑥) / (2 · (√‘(1 − (𝑥↑2))))) = ((1 / (2 · (√‘(1 − (𝑥↑2))))) · -(2 · 𝑥)))
295	249, 286, 294	3eqtr3rd 2694	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐷 → ((1 / (2 · (√‘(1 − (𝑥↑2))))) · -(2 · 𝑥)) = (-𝑥 / (√‘(1 − (𝑥↑2)))))
296	295	mpteq2ia 4773	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 ↦ ((1 / (2 · (√‘(1 − (𝑥↑2))))) · -(2 · 𝑥))) = (𝑥 ∈ 𝐷 ↦ (-𝑥 / (√‘(1 − (𝑥↑2)))))
297	246, 296	syl6eq 2701	. . . . . . . 8 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ (√‘(1 − (𝑥↑2))))) = (𝑥 ∈ 𝐷 ↦ (-𝑥 / (√‘(1 − (𝑥↑2))))))
298	11, 74, 75, 111, 115, 116, 297	dvmptadd 23768	. . . . . . 7 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))) = (𝑥 ∈ 𝐷 ↦ (i + (-𝑥 / (√‘(1 − (𝑥↑2)))))))
299		mulcl 10058	. . . . . . . . . . . 12 ⊢ ((i ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ∈ ℂ) → (i · (√‘(1 − (𝑥↑2)))) ∈ ℂ)
300	13, 20, 299	sylancr 696	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℂ → (i · (√‘(1 − (𝑥↑2)))) ∈ ℂ)
301	12, 300	syl 17	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐷 → (i · (√‘(1 − (𝑥↑2)))) ∈ ℂ)
302	301, 250, 114, 282	divdird 10877	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → (((i · (√‘(1 − (𝑥↑2)))) + -𝑥) / (√‘(1 − (𝑥↑2)))) = (((i · (√‘(1 − (𝑥↑2)))) / (√‘(1 − (𝑥↑2)))) + (-𝑥 / (√‘(1 − (𝑥↑2))))))
303		ixi 10694	. . . . . . . . . . . . . . . 16 ⊢ (i · i) = -1
304	303	eqcomi 2660	. . . . . . . . . . . . . . 15 ⊢ -1 = (i · i)
305	304	oveq1i 6700	. . . . . . . . . . . . . 14 ⊢ (-1 · 𝑥) = ((i · i) · 𝑥)
306		mulm1 10509	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℂ → (-1 · 𝑥) = -𝑥)
307		mulass 10062	. . . . . . . . . . . . . . 15 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ ∧ 𝑥 ∈ ℂ) → ((i · i) · 𝑥) = (i · (i · 𝑥)))
308	13, 13, 307	mp3an12 1454	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℂ → ((i · i) · 𝑥) = (i · (i · 𝑥)))
309	305, 306, 308	3eqtr3a 2709	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℂ → -𝑥 = (i · (i · 𝑥)))
310	309	oveq1d 6705	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℂ → (-𝑥 + (i · (√‘(1 − (𝑥↑2))))) = ((i · (i · 𝑥)) + (i · (√‘(1 − (𝑥↑2))))))
311		negcl 10319	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℂ → -𝑥 ∈ ℂ)
312	300, 311	addcomd 10276	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℂ → ((i · (√‘(1 − (𝑥↑2)))) + -𝑥) = (-𝑥 + (i · (√‘(1 − (𝑥↑2))))))
313	13	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℂ → i ∈ ℂ)
314	313, 15, 20	adddid 10102	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℂ → (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) = ((i · (i · 𝑥)) + (i · (√‘(1 − (𝑥↑2))))))
315	310, 312, 314	3eqtr4d 2695	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℂ → ((i · (√‘(1 − (𝑥↑2)))) + -𝑥) = (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
316	12, 315	syl 17	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐷 → ((i · (√‘(1 − (𝑥↑2)))) + -𝑥) = (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
317	316	oveq1d 6705	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → (((i · (√‘(1 − (𝑥↑2)))) + -𝑥) / (√‘(1 − (𝑥↑2)))) = ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))))
318	72, 114, 282	divcan4d 10845	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐷 → ((i · (√‘(1 − (𝑥↑2)))) / (√‘(1 − (𝑥↑2)))) = i)
319	318	oveq1d 6705	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → (((i · (√‘(1 − (𝑥↑2)))) / (√‘(1 − (𝑥↑2)))) + (-𝑥 / (√‘(1 − (𝑥↑2))))) = (i + (-𝑥 / (√‘(1 − (𝑥↑2))))))
320	302, 317, 319	3eqtr3rd 2694	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐷 → (i + (-𝑥 / (√‘(1 − (𝑥↑2))))) = ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))))
321	320	mpteq2ia 4773	. . . . . . 7 ⊢ (𝑥 ∈ 𝐷 ↦ (i + (-𝑥 / (√‘(1 − (𝑥↑2)))))) = (𝑥 ∈ 𝐷 ↦ ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))))
322	298, 321	syl6eq 2701	. . . . . 6 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))) = (𝑥 ∈ 𝐷 ↦ ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2))))))
323	240	dvlog 24442	. . . . . . 7 ⊢ (ℂ D (log ↾ (ℂ ∖ (-∞(,]0)))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (1 / 𝑦))
324		logf1o 24356	. . . . . . . . . 10 ⊢ log:(ℂ ∖ {0})–1-1-onto→ran log
325		f1of 6175	. . . . . . . . . 10 ⊢ (log:(ℂ ∖ {0})–1-1-onto→ran log → log:(ℂ ∖ {0})⟶ran log)
326	324, 325	mp1i 13	. . . . . . . . 9 ⊢ (⊤ → log:(ℂ ∖ {0})⟶ran log)
327		snssi 4371	. . . . . . . . . . 11 ⊢ (0 ∈ (-∞(,]0) → {0} ⊆ (-∞(,]0))
328	64, 327	ax-mp 5	. . . . . . . . . 10 ⊢ {0} ⊆ (-∞(,]0)
329		sscon 3777	. . . . . . . . . 10 ⊢ ({0} ⊆ (-∞(,]0) → (ℂ ∖ (-∞(,]0)) ⊆ (ℂ ∖ {0}))
330	328, 329	mp1i 13	. . . . . . . . 9 ⊢ (⊤ → (ℂ ∖ (-∞(,]0)) ⊆ (ℂ ∖ {0}))
331	326, 330	feqresmpt 6289	. . . . . . . 8 ⊢ (⊤ → (log ↾ (ℂ ∖ (-∞(,]0))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (log‘𝑦)))
332	331	oveq2d 6706	. . . . . . 7 ⊢ (⊤ → (ℂ D (log ↾ (ℂ ∖ (-∞(,]0)))) = (ℂ D (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (log‘𝑦))))
333	323, 332	syl5reqr 2700	. . . . . 6 ⊢ (⊤ → (ℂ D (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (log‘𝑦))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (1 / 𝑦)))
334		fveq2 6229	. . . . . 6 ⊢ (𝑦 = ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) → (log‘𝑦) = (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
335		oveq2 6698	. . . . . 6 ⊢ (𝑦 = ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) → (1 / 𝑦) = (1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
336	11, 11, 57, 58, 70, 71, 322, 333, 334, 335	dvmptco 23780	. . . . 5 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))) = (𝑥 ∈ 𝐷 ↦ ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))))))
337	22, 24	reccld 10832	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐷 → (1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
338		mulcl 10058	. . . . . . . . . 10 ⊢ ((i ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℂ) → (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
339	13, 21, 338	sylancr 696	. . . . . . . . 9 ⊢ (𝑥 ∈ ℂ → (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
340	12, 339	syl 17	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐷 → (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
341	337, 340, 114, 282	divassd 10874	. . . . . . 7 ⊢ (𝑥 ∈ 𝐷 → (((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))) / (√‘(1 − (𝑥↑2)))) = ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2))))))
342	340, 22, 24	divrec2d 10843	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) = ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))
343	72, 22, 24	divcan4d 10845	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) = i)
344	342, 343	eqtr3d 2687	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐷 → ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))) = i)
345	344	oveq1d 6705	. . . . . . 7 ⊢ (𝑥 ∈ 𝐷 → (((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))) / (√‘(1 − (𝑥↑2)))) = (i / (√‘(1 − (𝑥↑2)))))
346	341, 345	eqtr3d 2687	. . . . . 6 ⊢ (𝑥 ∈ 𝐷 → ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2))))) = (i / (√‘(1 − (𝑥↑2)))))
347	346	mpteq2ia 4773	. . . . 5 ⊢ (𝑥 ∈ 𝐷 ↦ ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))))) = (𝑥 ∈ 𝐷 ↦ (i / (√‘(1 − (𝑥↑2)))))
348	336, 347	syl6eq 2701	. . . 4 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))) = (𝑥 ∈ 𝐷 ↦ (i / (√‘(1 − (𝑥↑2))))))
349		negicn 10320	. . . . 5 ⊢ -i ∈ ℂ
350	349	a1i 11	. . . 4 ⊢ (⊤ → -i ∈ ℂ)
351	11, 26, 27, 348, 350	dvmptcmul 23772	. . 3 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))) = (𝑥 ∈ 𝐷 ↦ (-i · (i / (√‘(1 − (𝑥↑2)))))))
352	351	trud 1533	. 2 ⊢ (ℂ D (𝑥 ∈ 𝐷 ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))) = (𝑥 ∈ 𝐷 ↦ (-i · (i / (√‘(1 − (𝑥↑2))))))
353	13, 13	mulneg1i 10514	. . . . . 6 ⊢ (-i · i) = -(i · i)
354	303	negeqi 10312	. . . . . 6 ⊢ -(i · i) = --1
355		negneg1e1 11166	. . . . . 6 ⊢ --1 = 1
356	353, 354, 355	3eqtri 2677	. . . . 5 ⊢ (-i · i) = 1
357	356	oveq1i 6700	. . . 4 ⊢ ((-i · i) / (√‘(1 − (𝑥↑2)))) = (1 / (√‘(1 − (𝑥↑2))))
358		divass 10741	. . . . . 6 ⊢ ((-i ∈ ℂ ∧ i ∈ ℂ ∧ ((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0)) → ((-i · i) / (√‘(1 − (𝑥↑2)))) = (-i · (i / (√‘(1 − (𝑥↑2))))))
359	349, 13, 358	mp3an12 1454	. . . . 5 ⊢ (((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0) → ((-i · i) / (√‘(1 − (𝑥↑2)))) = (-i · (i / (√‘(1 − (𝑥↑2))))))
360	114, 282, 359	syl2anc 694	. . . 4 ⊢ (𝑥 ∈ 𝐷 → ((-i · i) / (√‘(1 − (𝑥↑2)))) = (-i · (i / (√‘(1 − (𝑥↑2))))))
361	357, 360	syl5reqr 2700	. . 3 ⊢ (𝑥 ∈ 𝐷 → (-i · (i / (√‘(1 − (𝑥↑2))))) = (1 / (√‘(1 − (𝑥↑2)))))
362	361	mpteq2ia 4773	. 2 ⊢ (𝑥 ∈ 𝐷 ↦ (-i · (i / (√‘(1 − (𝑥↑2)))))) = (𝑥 ∈ 𝐷 ↦ (1 / (√‘(1 − (𝑥↑2)))))
363	9, 352, 362	3eqtri 2677	1 ⊢ (ℂ D (arcsin ↾ 𝐷)) = (𝑥 ∈ 𝐷 ↦ (1 / (√‘(1 − (𝑥↑2)))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∨ wo 382 ∧ wa 383 ∨ w3o 1053 ∧ w3a 1054 = wceq 1523 ⊤wtru 1524 ∈ wcel 2030 ≠ wne 2823 Vcvv 3231 ∖ cdif 3604 ∪ cun 3605 ∩ cin 3606 ⊆ wss 3607 ∅c0 3948 {csn 4210 {cpr 4212 class class class wbr 4685 ↦ cmpt 4762 ran crn 5144 ↾ cres 5145 ⟶wf 5922 –1-1-onto→wf1o 5925 ‘cfv 5926 (class class class)co 6690 ℂcc 9972 ℝcr 9973 0cc0 9974 1c1 9975 ici 9976 + caddc 9977 · cmul 9979 +∞cpnf 10109 -∞cmnf 10110 ℝ^*cxr 10111 < clt 10112 ≤ cle 10113 − cmin 10304 -cneg 10305 / cdiv 10722 ℕcn 11058 2c2 11108 ℝ⁺crp 11870 (,)cioo 12213 (,]cioc 12214 [,)cico 12215 ↑cexp 12900 ℜcre 13881 √csqrt 14017 abscabs 14018 ↾_t crest 16128 TopOpenctopn 16129 topGenctg 16145 ℂ_fldccnfld 19794 TopOnctopon 20763 Clsdccld 20868 D cdv 23672 logclog 24346 arcsincasin 24634

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-8 2032 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 ax-rep 4804 ax-sep 4814 ax-nul 4822 ax-pow 4873 ax-pr 4936 ax-un 6991 ax-inf2 8576 ax-cnex 10030 ax-resscn 10031 ax-1cn 10032 ax-icn 10033 ax-addcl 10034 ax-addrcl 10035 ax-mulcl 10036 ax-mulrcl 10037 ax-mulcom 10038 ax-addass 10039 ax-mulass 10040 ax-distr 10041 ax-i2m1 10042 ax-1ne0 10043 ax-1rid 10044 ax-rnegex 10045 ax-rrecex 10046 ax-cnre 10047 ax-pre-lttri 10048 ax-pre-lttrn 10049 ax-pre-ltadd 10050 ax-pre-mulgt0 10051 ax-pre-sup 10052 ax-addf 10053 ax-mulf 10054

This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1055 df-3an 1056 df-tru 1526 df-fal 1529 df-ex 1745 df-nf 1750 df-sb 1938 df-eu 2502 df-mo 2503 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-ne 2824 df-nel 2927 df-ral 2946 df-rex 2947 df-reu 2948 df-rmo 2949 df-rab 2950 df-v 3233 df-sbc 3469 df-csb 3567 df-dif 3610 df-un 3612 df-in 3614 df-ss 3621 df-pss 3623 df-nul 3949 df-if 4120 df-pw 4193 df-sn 4211 df-pr 4213 df-tp 4215 df-op 4217 df-uni 4469 df-int 4508 df-iun 4554 df-iin 4555 df-br 4686 df-opab 4746 df-mpt 4763 df-tr 4786 df-id 5053 df-eprel 5058 df-po 5064 df-so 5065 df-fr 5102 df-se 5103 df-we 5104 df-xp 5149 df-rel 5150 df-cnv 5151 df-co 5152 df-dm 5153 df-rn 5154 df-res 5155 df-ima 5156 df-pred 5718 df-ord 5764 df-on 5765 df-lim 5766 df-suc 5767 df-iota 5889 df-fun 5928 df-fn 5929 df-f 5930 df-f1 5931 df-fo 5932 df-f1o 5933 df-fv 5934 df-isom 5935 df-riota 6651 df-ov 6693 df-oprab 6694 df-mpt2 6695 df-of 6939 df-om 7108 df-1st 7210 df-2nd 7211 df-supp 7341 df-wrecs 7452 df-recs 7513 df-rdg 7551 df-1o 7605 df-2o 7606 df-oadd 7609 df-er 7787 df-map 7901 df-pm 7902 df-ixp 7951 df-en 7998 df-dom 7999 df-sdom 8000 df-fin 8001 df-fsupp 8317 df-fi 8358 df-sup 8389 df-inf 8390 df-oi 8456 df-card 8803 df-cda 9028 df-pnf 10114 df-mnf 10115 df-xr 10116 df-ltxr 10117 df-le 10118 df-sub 10306 df-neg 10307 df-div 10723 df-nn 11059 df-2 11117 df-3 11118 df-4 11119 df-5 11120 df-6 11121 df-7 11122 df-8 11123 df-9 11124 df-n0 11331 df-z 11416 df-dec 11532 df-uz 11726 df-q 11827 df-rp 11871 df-xneg 11984 df-xadd 11985 df-xmul 11986 df-ioo 12217 df-ioc 12218 df-ico 12219 df-icc 12220 df-fz 12365 df-fzo 12505 df-fl 12633 df-mod 12709 df-seq 12842 df-exp 12901 df-fac 13101 df-bc 13130 df-hash 13158 df-shft 13851 df-cj 13883 df-re 13884 df-im 13885 df-sqrt 14019 df-abs 14020 df-limsup 14246 df-clim 14263 df-rlim 14264 df-sum 14461 df-ef 14842 df-sin 14844 df-cos 14845 df-tan 14846 df-pi 14847 df-struct 15906 df-ndx 15907 df-slot 15908 df-base 15910 df-sets 15911 df-ress 15912 df-plusg 16001 df-mulr 16002 df-starv 16003 df-sca 16004 df-vsca 16005 df-ip 16006 df-tset 16007 df-ple 16008 df-ds 16011 df-unif 16012 df-hom 16013 df-cco 16014 df-rest 16130 df-topn 16131 df-0g 16149 df-gsum 16150 df-topgen 16151 df-pt 16152 df-prds 16155 df-xrs 16209 df-qtop 16214 df-imas 16215 df-xps 16217 df-mre 16293 df-mrc 16294 df-acs 16296 df-mgm 17289 df-sgrp 17331 df-mnd 17342 df-submnd 17383 df-mulg 17588 df-cntz 17796 df-cmn 18241 df-psmet 19786 df-xmet 19787 df-met 19788 df-bl 19789 df-mopn 19790 df-fbas 19791 df-fg 19792 df-cnfld 19795 df-top 20747 df-topon 20764 df-topsp 20785 df-bases 20798 df-cld 20871 df-ntr 20872 df-cls 20873 df-nei 20950 df-lp 20988 df-perf 20989 df-cn 21079 df-cnp 21080 df-haus 21167 df-cmp 21238 df-tx 21413 df-hmeo 21606 df-fil 21697 df-fm 21789 df-flim 21790 df-flf 21791 df-xms 22172 df-ms 22173 df-tms 22174 df-cncf 22728 df-limc 23675 df-dv 23676 df-log 24348 df-cxp 24349 df-asin 24637

This theorem is referenced by: dvacos 33627 dvreasin 33628

W3C validator