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 38167

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 26907	. . . . 5 ⊢ arcsin = (𝑥 ∈ ℂ ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))
2	1	reseq1i 5959	. . . 4 ⊢ (arcsin ↾ 𝐷) = ((𝑥 ∈ ℂ ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))) ↾ 𝐷)
3		dvasin.d	. . . . . 6 ⊢ 𝐷 = (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞)))
4		difss 4089	. . . . . 6 ⊢ (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞))) ⊆ ℂ
5	3, 4	eqsstri 3982	. . . . 5 ⊢ 𝐷 ⊆ ℂ
6		resmpt 6023	. . . . 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 2784	. . 3 ⊢ (arcsin ↾ 𝐷) = (𝑥 ∈ 𝐷 ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))
9	8	oveq2i 7403	. 2 ⊢ (ℂ D (arcsin ↾ 𝐷)) = (ℂ D (𝑥 ∈ 𝐷 ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))))
10		cnelprrecn 11163	. . . . 5 ⊢ ℂ ∈ {ℝ, ℂ}
11	10	a1i 11	. . . 4 ⊢ (⊤ → ℂ ∈ {ℝ, ℂ})
12	5	sseli 3932	. . . . . . 7 ⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ ℂ)
13		ax-icn 11129	. . . . . . . . 9 ⊢ i ∈ ℂ
14		mulcl 11154	. . . . . . . . 9 ⊢ ((i ∈ ℂ ∧ 𝑥 ∈ ℂ) → (i · 𝑥) ∈ ℂ)
15	13, 14	mpan 700	. . . . . . . 8 ⊢ (𝑥 ∈ ℂ → (i · 𝑥) ∈ ℂ)
16		ax-1cn 11128	. . . . . . . . . 10 ⊢ 1 ∈ ℂ
17		sqcl 14128	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℂ → (𝑥↑2) ∈ ℂ)
18		subcl 11426	. . . . . . . . . 10 ⊢ ((1 ∈ ℂ ∧ (𝑥↑2) ∈ ℂ) → (1 − (𝑥↑2)) ∈ ℂ)
19	16, 17, 18	sylancr 596	. . . . . . . . 9 ⊢ (𝑥 ∈ ℂ → (1 − (𝑥↑2)) ∈ ℂ)
20	19	sqrtcld 15450	. . . . . . . 8 ⊢ (𝑥 ∈ ℂ → (√‘(1 − (𝑥↑2))) ∈ ℂ)
21	15, 20	addcld 11198	. . . . . . 7 ⊢ (𝑥 ∈ ℂ → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℂ)
22	12, 21	syl 17	. . . . . 6 ⊢ (𝑥 ∈ 𝐷 → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℂ)
23		asinlem 26910	. . . . . . 7 ⊢ (𝑥 ∈ ℂ → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≠ 0)
24	12, 23	syl 17	. . . . . 6 ⊢ (𝑥 ∈ 𝐷 → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≠ 0)
25	22, 24	logcld 26612	. . . . 5 ⊢ (𝑥 ∈ 𝐷 → (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
26	25	adantl 485	. . . 4 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
27		ovexd 7427	. . . 4 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → (i / (√‘(1 − (𝑥↑2)))) ∈ V)
28		simpr 488	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ)
29		asinlem3 26913	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℂ → 0 ≤ (ℜ‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
30		rere 15132	. . . . . . . . . . . . . . . . . . 19 ⊢ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → (ℜ‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) = ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))
31	30	breq2d 5111	. . . . . . . . . . . . . . . . . 18 ⊢ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → (0 ≤ (ℜ‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ↔ 0 ≤ ((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
32	31	biimpac 482	. . . . . . . . . . . . . . . . 17 ⊢ ((0 ≤ (ℜ‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → 0 ≤ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))
33	29, 32	sylan 589	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → 0 ≤ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))
34	23	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≠ 0)
35	28, 33, 34	ne0gt0d 11317	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → 0 < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))
36		0re 11180	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ ℝ
37		ltnle 11259	. . . . . . . . . . . . . . . . 17 ⊢ ((0 ∈ ℝ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → (0 < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ↔ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
38	36, 37	mpan 700	. . . . . . . . . . . . . . . 16 ⊢ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → (0 < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ↔ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
39	38	adantl 485	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → (0 < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ↔ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
40	35, 39	mpbid 234	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0)
41	40	ex 416	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℂ → (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
42	12, 41	syl 17	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐷 → (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
43		imor 864	. . . . . . . . . . . 12 ⊢ ((((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0) ↔ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
44	42, 43	sylib 220	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐷 → (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
45	44	orcomd 882	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐷 → (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ))
46	45	olcd 885	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → (¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ)))
47		3ianor 1118	. . . . . . . . . . 11 ⊢ (¬ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∧ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0) ↔ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∨ ¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
48		3orrot 1102	. . . . . . . . . . 11 ⊢ ((¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∨ ¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0) ↔ (¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ))
49		3orass 1100	. . . . . . . . . . 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 300	. . . . . . . . . 10 ⊢ ((¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ)) ↔ ¬ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∧ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
51		mnfxr 11236	. . . . . . . . . . 11 ⊢ -∞ ∈ ℝ^*
52		elioc2 13410	. . . . . . . . . . 11 ⊢ ((-∞ ∈ ℝ^* ∧ 0 ∈ ℝ) → (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (-∞(,]0) ↔ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∧ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0)))
53	51, 36, 52	mp2an 702	. . . . . . . . . 10 ⊢ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (-∞(,]0) ↔ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∧ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
54	50, 53	xchbinxr 337	. . . . . . . . 9 ⊢ ((¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ)) ↔ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (-∞(,]0))
55	46, 54	sylib 220	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐷 → ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (-∞(,]0))
56	22, 55	eldifd 3915	. . . . . . 7 ⊢ (𝑥 ∈ 𝐷 → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (ℂ ∖ (-∞(,]0)))
57	56	adantl 485	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (ℂ ∖ (-∞(,]0)))
58		ovexd 7427	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))) ∈ V)
59		eldifi 4084	. . . . . . . 8 ⊢ (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → 𝑦 ∈ ℂ)
60		eldifn 4085	. . . . . . . . 9 ⊢ (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → ¬ 𝑦 ∈ (-∞(,]0))
61		0xr 11226	. . . . . . . . . . . 12 ⊢ 0 ∈ ℝ^*
62		mnflt0 13124	. . . . . . . . . . . 12 ⊢ -∞ < 0
63		ubioc1 13400	. . . . . . . . . . . 12 ⊢ ((-∞ ∈ ℝ^* ∧ 0 ∈ ℝ^* ∧ -∞ < 0) → 0 ∈ (-∞(,]0))
64	51, 61, 62, 63	mp3an 1481	. . . . . . . . . . 11 ⊢ 0 ∈ (-∞(,]0)
65		eleq1 2849	. . . . . . . . . . 11 ⊢ (𝑦 = 0 → (𝑦 ∈ (-∞(,]0) ↔ 0 ∈ (-∞(,]0)))
66	64, 65	mpbiri 260	. . . . . . . . . 10 ⊢ (𝑦 = 0 → 𝑦 ∈ (-∞(,]0))
67	66	necon3bi 2982	. . . . . . . . 9 ⊢ (¬ 𝑦 ∈ (-∞(,]0) → 𝑦 ≠ 0)
68	60, 67	syl 17	. . . . . . . 8 ⊢ (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → 𝑦 ≠ 0)
69	59, 68	logcld 26612	. . . . . . 7 ⊢ (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → (log‘𝑦) ∈ ℂ)
70	69	adantl 485	. . . . . 6 ⊢ ((⊤ ∧ 𝑦 ∈ (ℂ ∖ (-∞(,]0))) → (log‘𝑦) ∈ ℂ)
71		ovexd 7427	. . . . . 6 ⊢ ((⊤ ∧ 𝑦 ∈ (ℂ ∖ (-∞(,]0))) → (1 / 𝑦) ∈ V)
72	13	a1i 11	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐷 → i ∈ ℂ)
73	72, 12	mulcld 11199	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → (i · 𝑥) ∈ ℂ)
74	73	adantl 485	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → (i · 𝑥) ∈ ℂ)
75	13	a1i 11	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → i ∈ ℂ)
76	12	adantl 485	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ ℂ)
77		1cnd 11172	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → 1 ∈ ℂ)
78		simpr 488	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → 𝑥 ∈ ℂ)
79		1cnd 11172	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → 1 ∈ ℂ)
80	11	dvmptid 25999	. . . . . . . . . . 11 ⊢ (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ 𝑥)) = (𝑥 ∈ ℂ ↦ 1))
81	5	a1i 11	. . . . . . . . . . 11 ⊢ (⊤ → 𝐷 ⊆ ℂ)
82		eqid 2761	. . . . . . . . . . . . 13 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
83	82	cnfldtopon 24822	. . . . . . . . . . . 12 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
84	83	toponrestid 22961	. . . . . . . . . . 11 ⊢ (TopOpen‘ℂ_fld) = ((TopOpen‘ℂ_fld) ↾_t ℂ)
85	82	recld2 24855	. . . . . . . . . . . . . . 15 ⊢ ℝ ∈ (Clsd‘(TopOpen‘ℂ_fld))
86		neg1rr 12178	. . . . . . . . . . . . . . . . . 18 ⊢ -1 ∈ ℝ
87		iocmnfcld 24808	. . . . . . . . . . . . . . . . . 18 ⊢ (-1 ∈ ℝ → (-∞(,]-1) ∈ (Clsd‘(topGen‘ran (,))))
88	86, 87	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (-∞(,]-1) ∈ (Clsd‘(topGen‘ran (,)))
89		1re 11178	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℝ
90		icopnfcld 24807	. . . . . . . . . . . . . . . . . 18 ⊢ (1 ∈ ℝ → (1[,)+∞) ∈ (Clsd‘(topGen‘ran (,))))
91	89, 90	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (1[,)+∞) ∈ (Clsd‘(topGen‘ran (,)))
92		uncld 23081	. . . . . . . . . . . . . . . . 17 ⊢ (((-∞(,]-1) ∈ (Clsd‘(topGen‘ran (,))) ∧ (1[,)+∞) ∈ (Clsd‘(topGen‘ran (,)))) → ((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘(topGen‘ran (,))))
93	88, 91, 92	mp2an 702	. . . . . . . . . . . . . . . 16 ⊢ ((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘(topGen‘ran (,)))
94		tgioo4 24845	. . . . . . . . . . . . . . . . 17 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
95	94	fveq2i 6866	. . . . . . . . . . . . . . . 16 ⊢ (Clsd‘(topGen‘ran (,))) = (Clsd‘((TopOpen‘ℂ_fld) ↾_t ℝ))
96	93, 95	eleqtri 2859	. . . . . . . . . . . . . . 15 ⊢ ((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘((TopOpen‘ℂ_fld) ↾_t ℝ))
97		restcldr 23214	. . . . . . . . . . . . . . 15 ⊢ ((ℝ ∈ (Clsd‘(TopOpen‘ℂ_fld)) ∧ ((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘((TopOpen‘ℂ_fld) ↾_t ℝ))) → ((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘(TopOpen‘ℂ_fld)))
98	85, 96, 97	mp2an 702	. . . . . . . . . . . . . 14 ⊢ ((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘(TopOpen‘ℂ_fld))
99	83	toponunii 22956	. . . . . . . . . . . . . . 15 ⊢ ℂ = ∪ (TopOpen‘ℂ_fld)
100	99	cldopn 23071	. . . . . . . . . . . . . 14 ⊢ (((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘(TopOpen‘ℂ_fld)) → (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞))) ∈ (TopOpen‘ℂ_fld))
101	98, 100	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞))) ∈ (TopOpen‘ℂ_fld)
102	3, 101	eqeltri 2857	. . . . . . . . . . . 12 ⊢ 𝐷 ∈ (TopOpen‘ℂ_fld)
103	102	a1i 11	. . . . . . . . . . 11 ⊢ (⊤ → 𝐷 ∈ (TopOpen‘ℂ_fld))
104	11, 78, 79, 80, 81, 84, 82, 103	dvmptres 26005	. . . . . . . . . 10 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ 𝑥)) = (𝑥 ∈ 𝐷 ↦ 1))
105	13	a1i 11	. . . . . . . . . 10 ⊢ (⊤ → i ∈ ℂ)
106	11, 76, 77, 104, 105	dvmptcmul 26006	. . . . . . . . 9 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ (i · 𝑥))) = (𝑥 ∈ 𝐷 ↦ (i · 1)))
107	13	mulridi 11183	. . . . . . . . . 10 ⊢ (i · 1) = i
108	107	mpteq2i 5195	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 ↦ (i · 1)) = (𝑥 ∈ 𝐷 ↦ i)
109	106, 108	eqtrdi 2812	. . . . . . . 8 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ (i · 𝑥))) = (𝑥 ∈ 𝐷 ↦ i))
110	12	sqcld 14154	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐷 → (𝑥↑2) ∈ ℂ)
111	16, 110, 18	sylancr 596	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐷 → (1 − (𝑥↑2)) ∈ ℂ)
112	111	sqrtcld 15450	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → (√‘(1 − (𝑥↑2))) ∈ ℂ)
113	112	adantl 485	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → (√‘(1 − (𝑥↑2))) ∈ ℂ)
114		ovexd 7427	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → (-𝑥 / (√‘(1 − (𝑥↑2)))) ∈ V)
115		elin 3920	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐷 ∩ ℝ) ↔ (𝑥 ∈ 𝐷 ∧ 𝑥 ∈ ℝ))
116	3	asindmre 38166	. . . . . . . . . . . . . . . . 17 ⊢ (𝐷 ∩ ℝ) = (-1(,)1)
117	116	eqimssi 3996	. . . . . . . . . . . . . . . 16 ⊢ (𝐷 ∩ ℝ) ⊆ (-1(,)1)
118	117	sseli 3932	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐷 ∩ ℝ) → 𝑥 ∈ (-1(,)1))
119	115, 118	sylbir 237	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ 𝐷 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ (-1(,)1))
120		incom 4161	. . . . . . . . . . . . . . . 16 ⊢ ((0(,)+∞) ∩ (-∞(,]0)) = ((-∞(,]0) ∩ (0(,)+∞))
121		pnfxr 11233	. . . . . . . . . . . . . . . . 17 ⊢ +∞ ∈ ℝ^*
122		df-ioc 13351	. . . . . . . . . . . . . . . . . 18 ⊢ (,] = (𝑥 ∈ ℝ^, 𝑦 ∈ ℝ^ ↦ {𝑧 ∈ ℝ^* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})
123		df-ioo 13350	. . . . . . . . . . . . . . . . . 18 ⊢ (,) = (𝑥 ∈ ℝ^, 𝑦 ∈ ℝ^ ↦ {𝑧 ∈ ℝ^* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
124		xrltnle 11246	. . . . . . . . . . . . . . . . . 18 ⊢ ((0 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) → (0 < 𝑤 ↔ ¬ 𝑤 ≤ 0))
125	122, 123, 124	ixxdisj 13361	. . . . . . . . . . . . . . . . 17 ⊢ ((-∞ ∈ ℝ^* ∧ 0 ∈ ℝ^* ∧ +∞ ∈ ℝ^*) → ((-∞(,]0) ∩ (0(,)+∞)) = ∅)
126	51, 61, 121, 125	mp3an 1481	. . . . . . . . . . . . . . . 16 ⊢ ((-∞(,]0) ∩ (0(,)+∞)) = ∅
127	120, 126	eqtri 2784	. . . . . . . . . . . . . . 15 ⊢ ((0(,)+∞) ∩ (-∞(,]0)) = ∅
128		elioore 13376	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (-1(,)1) → 𝑥 ∈ ℝ)
129	128	resqcld 14135	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (-1(,)1) → (𝑥↑2) ∈ ℝ)
130		resubcl 11492	. . . . . . . . . . . . . . . . . 18 ⊢ ((1 ∈ ℝ ∧ (𝑥↑2) ∈ ℝ) → (1 − (𝑥↑2)) ∈ ℝ)
131	89, 129, 130	sylancr 596	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (-1(,)1) → (1 − (𝑥↑2)) ∈ ℝ)
132	86	rexri 11237	. . . . . . . . . . . . . . . . . . 19 ⊢ -1 ∈ ℝ^*
133		1xr 11238	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℝ^*
134		elioo2 13387	. . . . . . . . . . . . . . . . . . 19 ⊢ ((-1 ∈ ℝ^* ∧ 1 ∈ ℝ^*) → (𝑥 ∈ (-1(,)1) ↔ (𝑥 ∈ ℝ ∧ -1 < 𝑥 ∧ 𝑥 < 1)))
135	132, 133, 134	mp2an 702	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (-1(,)1) ↔ (𝑥 ∈ ℝ ∧ -1 < 𝑥 ∧ 𝑥 < 1))
136		recn 11160	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
137	136	abscld 15449	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℝ → (abs‘𝑥) ∈ ℝ)
138	136	absge0d 15457	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℝ → 0 ≤ (abs‘𝑥))
139		0le1 11707	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 ≤ 1
140		lt2sq 14143	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((abs‘𝑥) ∈ ℝ ∧ 0 ≤ (abs‘𝑥)) ∧ (1 ∈ ℝ ∧ 0 ≤ 1)) → ((abs‘𝑥) < 1 ↔ ((abs‘𝑥)↑2) < (1↑2)))
141	89, 139, 140	mpanr12 715	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((abs‘𝑥) ∈ ℝ ∧ 0 ≤ (abs‘𝑥)) → ((abs‘𝑥) < 1 ↔ ((abs‘𝑥)↑2) < (1↑2)))
142	137, 138, 141	syl2anc 593	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℝ → ((abs‘𝑥) < 1 ↔ ((abs‘𝑥)↑2) < (1↑2)))
143		abslt 15325	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑥) < 1 ↔ (-1 < 𝑥 ∧ 𝑥 < 1)))
144	89, 143	mpan2 701	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℝ → ((abs‘𝑥) < 1 ↔ (-1 < 𝑥 ∧ 𝑥 < 1)))
145		absresq 15312	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℝ → ((abs‘𝑥)↑2) = (𝑥↑2))
146		sq1 14205	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1↑2) = 1
147	146	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℝ → (1↑2) = 1)
148	145, 147	breq12d 5112	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℝ → (((abs‘𝑥)↑2) < (1↑2) ↔ (𝑥↑2) < 1))
149		resqcl 14134	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℝ → (𝑥↑2) ∈ ℝ)
150		posdif 11677	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑥↑2) ∈ ℝ ∧ 1 ∈ ℝ) → ((𝑥↑2) < 1 ↔ 0 < (1 − (𝑥↑2))))
151	149, 89, 150	sylancl 595	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℝ → ((𝑥↑2) < 1 ↔ 0 < (1 − (𝑥↑2))))
152	148, 151	bitrd 281	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℝ → (((abs‘𝑥)↑2) < (1↑2) ↔ 0 < (1 − (𝑥↑2))))
153	142, 144, 152	3bitr3d 311	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ → ((-1 < 𝑥 ∧ 𝑥 < 1) ↔ 0 < (1 − (𝑥↑2))))
154	153	biimpd 231	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℝ → ((-1 < 𝑥 ∧ 𝑥 < 1) → 0 < (1 − (𝑥↑2))))
155	154	3impib 1128	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℝ ∧ -1 < 𝑥 ∧ 𝑥 < 1) → 0 < (1 − (𝑥↑2)))
156	135, 155	sylbi 219	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (-1(,)1) → 0 < (1 − (𝑥↑2)))
157	131, 156	elrpd 13031	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (-1(,)1) → (1 − (𝑥↑2)) ∈ ℝ⁺)
158		ioorp 13426	. . . . . . . . . . . . . . . 16 ⊢ (0(,)+∞) = ℝ⁺
159	157, 158	eleqtrrdi 2872	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (-1(,)1) → (1 − (𝑥↑2)) ∈ (0(,)+∞))
160		disjel 4410	. . . . . . . . . . . . . . 15 ⊢ ((((0(,)+∞) ∩ (-∞(,]0)) = ∅ ∧ (1 − (𝑥↑2)) ∈ (0(,)+∞)) → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
161	127, 159, 160	sylancr 596	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (-1(,)1) → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
162	119, 161	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝐷 ∧ 𝑥 ∈ ℝ) → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
163		elioc2 13410	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((-∞ ∈ ℝ^* ∧ 0 ∈ ℝ) → ((1 − (𝑥↑2)) ∈ (-∞(,]0) ↔ ((1 − (𝑥↑2)) ∈ ℝ ∧ -∞ < (1 − (𝑥↑2)) ∧ (1 − (𝑥↑2)) ≤ 0)))
164	51, 36, 163	mp2an 702	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1 − (𝑥↑2)) ∈ (-∞(,]0) ↔ ((1 − (𝑥↑2)) ∈ ℝ ∧ -∞ < (1 − (𝑥↑2)) ∧ (1 − (𝑥↑2)) ≤ 0))
165	164	biimpi 218	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1 − (𝑥↑2)) ∈ (-∞(,]0) → ((1 − (𝑥↑2)) ∈ ℝ ∧ -∞ < (1 − (𝑥↑2)) ∧ (1 − (𝑥↑2)) ≤ 0))
166	165	simp1d 1154	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1 − (𝑥↑2)) ∈ (-∞(,]0) → (1 − (𝑥↑2)) ∈ ℝ)
167		resubcl 11492	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1 ∈ ℝ ∧ (1 − (𝑥↑2)) ∈ ℝ) → (1 − (1 − (𝑥↑2))) ∈ ℝ)
168	89, 166, 167	sylancr 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 − (𝑥↑2)) ∈ (-∞(,]0) → (1 − (1 − (𝑥↑2))) ∈ ℝ)
169		nncan 11457	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1 ∈ ℂ ∧ (𝑥↑2) ∈ ℂ) → (1 − (1 − (𝑥↑2))) = (𝑥↑2))
170	16, 169	mpan 700	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥↑2) ∈ ℂ → (1 − (1 − (𝑥↑2))) = (𝑥↑2))
171	170	eleq1d 2846	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥↑2) ∈ ℂ → ((1 − (1 − (𝑥↑2))) ∈ ℝ ↔ (𝑥↑2) ∈ ℝ))
172	171	biimpa 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥↑2) ∈ ℂ ∧ (1 − (1 − (𝑥↑2))) ∈ ℝ) → (𝑥↑2) ∈ ℝ)
173	168, 172	sylan2 602	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (𝑥↑2) ∈ ℝ)
174	166	adantl 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (1 − (𝑥↑2)) ∈ ℝ)
175	165	simp3d 1156	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1 − (𝑥↑2)) ∈ (-∞(,]0) → (1 − (𝑥↑2)) ≤ 0)
176	175	adantl 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (1 − (𝑥↑2)) ≤ 0)
177		letr 11274	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((1 − (𝑥↑2)) ∈ ℝ ∧ 0 ∈ ℝ ∧ 1 ∈ ℝ) → (((1 − (𝑥↑2)) ≤ 0 ∧ 0 ≤ 1) → (1 − (𝑥↑2)) ≤ 1))
178	36, 89, 177	mp3an23 1473	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1 − (𝑥↑2)) ∈ ℝ → (((1 − (𝑥↑2)) ≤ 0 ∧ 0 ≤ 1) → (1 − (𝑥↑2)) ≤ 1))
179	139, 178	mpan2i 707	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1 − (𝑥↑2)) ∈ ℝ → ((1 − (𝑥↑2)) ≤ 0 → (1 − (𝑥↑2)) ≤ 1))
180	174, 176, 179	sylc 65	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (1 − (𝑥↑2)) ≤ 1)
181		subge0 11697	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1 ∈ ℝ ∧ (1 − (𝑥↑2)) ∈ ℝ) → (0 ≤ (1 − (1 − (𝑥↑2))) ↔ (1 − (𝑥↑2)) ≤ 1))
182	89, 174, 181	sylancr 596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (0 ≤ (1 − (1 − (𝑥↑2))) ↔ (1 − (𝑥↑2)) ≤ 1))
183	180, 182	mpbird 259	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → 0 ≤ (1 − (1 − (𝑥↑2))))
184	170	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (1 − (1 − (𝑥↑2))) = (𝑥↑2))
185	183, 184	breqtrd 5125	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → 0 ≤ (𝑥↑2))
186	173, 185	resqrtcld 15428	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (√‘(𝑥↑2)) ∈ ℝ)
187	17, 186	sylan 589	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (√‘(𝑥↑2)) ∈ ℝ)
188		eleq1 2849	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (√‘(𝑥↑2)) → (𝑥 ∈ ℝ ↔ (√‘(𝑥↑2)) ∈ ℝ))
189	187, 188	syl5ibrcom 249	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (𝑥 = (√‘(𝑥↑2)) → 𝑥 ∈ ℝ))
190	187	renegcld 11611	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → -(√‘(𝑥↑2)) ∈ ℝ)
191		eleq1 2849	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = -(√‘(𝑥↑2)) → (𝑥 ∈ ℝ ↔ -(√‘(𝑥↑2)) ∈ ℝ))
192	190, 191	syl5ibrcom 249	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (𝑥 = -(√‘(𝑥↑2)) → 𝑥 ∈ ℝ))
193		eqid 2761	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥↑2) = (𝑥↑2)
194		eqsqrtor 15377	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℂ ∧ (𝑥↑2) ∈ ℂ) → ((𝑥↑2) = (𝑥↑2) ↔ (𝑥 = (√‘(𝑥↑2)) ∨ 𝑥 = -(√‘(𝑥↑2)))))
195	17, 194	mpdan 697	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℂ → ((𝑥↑2) = (𝑥↑2) ↔ (𝑥 = (√‘(𝑥↑2)) ∨ 𝑥 = -(√‘(𝑥↑2)))))
196	193, 195	mpbii 235	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℂ → (𝑥 = (√‘(𝑥↑2)) ∨ 𝑥 = -(√‘(𝑥↑2))))
197	196	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (𝑥 = (√‘(𝑥↑2)) ∨ 𝑥 = -(√‘(𝑥↑2))))
198	189, 192, 197	mpjaod 871	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → 𝑥 ∈ ℝ)
199	198	stoic1a 1791	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℂ ∧ ¬ 𝑥 ∈ ℝ) → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
200	12, 199	sylan 589	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝐷 ∧ ¬ 𝑥 ∈ ℝ) → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
201	162, 200	pm2.61dan 822	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐷 → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
202	111, 201	eldifd 3915	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐷 → (1 − (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0)))
203	202	adantl 485	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → (1 − (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0)))
204		2cnd 12293	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℂ → 2 ∈ ℂ)
205		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℂ → 𝑥 ∈ ℂ)
206	204, 205	mulcld 11199	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℂ → (2 · 𝑥) ∈ ℂ)
207	206	negcld 11526	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℂ → -(2 · 𝑥) ∈ ℂ)
208	207	adantl 485	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → -(2 · 𝑥) ∈ ℂ)
209	12, 208	sylan2 602	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → -(2 · 𝑥) ∈ ℂ)
210	59	sqrtcld 15450	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → (√‘𝑦) ∈ ℂ)
211	210	adantl 485	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑦 ∈ (ℂ ∖ (-∞(,]0))) → (√‘𝑦) ∈ ℂ)
212		ovexd 7427	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑦 ∈ (ℂ ∖ (-∞(,]0))) → (1 / (2 · (√‘𝑦))) ∈ V)
213	19	adantl 485	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → (1 − (𝑥↑2)) ∈ ℂ)
214	36	a1i 11	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → 0 ∈ ℝ)
215		1cnd 11172	. . . . . . . . . . . . . 14 ⊢ (⊤ → 1 ∈ ℂ)
216	11, 215	dvmptc 26000	. . . . . . . . . . . . 13 ⊢ (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ 1)) = (𝑥 ∈ ℂ ↦ 0))
217	17	adantl 485	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → (𝑥↑2) ∈ ℂ)
218		2cn 12290	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℂ
219		mulcl 11154	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (2 · 𝑥) ∈ ℂ)
220	218, 219	mpan 700	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℂ → (2 · 𝑥) ∈ ℂ)
221	220	adantl 485	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → (2 · 𝑥) ∈ ℂ)
222		2nn 12288	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℕ
223		dvexp 25995	. . . . . . . . . . . . . . . 16 ⊢ (2 ∈ ℕ → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · (𝑥↑(2 − 1)))))
224	222, 223	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · (𝑥↑(2 − 1))))
225		2m1e1 12339	. . . . . . . . . . . . . . . . . . 19 ⊢ (2 − 1) = 1
226	225	oveq2i 7403	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥↑(2 − 1)) = (𝑥↑1)
227		exp1 14077	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℂ → (𝑥↑1) = 𝑥)
228	226, 227	eqtrid 2808	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℂ → (𝑥↑(2 − 1)) = 𝑥)
229	228	oveq2d 7408	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℂ → (2 · (𝑥↑(2 − 1))) = (2 · 𝑥))
230	229	mpteq2ia 5194	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℂ ↦ (2 · (𝑥↑(2 − 1)))) = (𝑥 ∈ ℂ ↦ (2 · 𝑥))
231	224, 230	eqtri 2784	. . . . . . . . . . . . . 14 ⊢ (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · 𝑥))
232	231	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · 𝑥)))
233	11, 79, 214, 216, 217, 221, 232	dvmptsub 26009	. . . . . . . . . . . 12 ⊢ (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (1 − (𝑥↑2)))) = (𝑥 ∈ ℂ ↦ (0 − (2 · 𝑥))))
234		df-neg 11414	. . . . . . . . . . . . 13 ⊢ -(2 · 𝑥) = (0 − (2 · 𝑥))
235	234	mpteq2i 5195	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℂ ↦ -(2 · 𝑥)) = (𝑥 ∈ ℂ ↦ (0 − (2 · 𝑥)))
236	233, 235	eqtr4di 2814	. . . . . . . . . . 11 ⊢ (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (1 − (𝑥↑2)))) = (𝑥 ∈ ℂ ↦ -(2 · 𝑥)))
237	11, 213, 208, 236, 81, 84, 82, 103	dvmptres 26005	. . . . . . . . . 10 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ (1 − (𝑥↑2)))) = (𝑥 ∈ 𝐷 ↦ -(2 · 𝑥)))
238		eqid 2761	. . . . . . . . . . . 12 ⊢ (ℂ ∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0))
239	238	dvcnsqrt 26786	. . . . . . . . . . 11 ⊢ (ℂ D (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (√‘𝑦))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (1 / (2 · (√‘𝑦))))
240	239	a1i 11	. . . . . . . . . 10 ⊢ (⊤ → (ℂ D (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (√‘𝑦))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (1 / (2 · (√‘𝑦)))))
241		fveq2 6863	. . . . . . . . . 10 ⊢ (𝑦 = (1 − (𝑥↑2)) → (√‘𝑦) = (√‘(1 − (𝑥↑2))))
242	241	oveq2d 7408	. . . . . . . . . . 11 ⊢ (𝑦 = (1 − (𝑥↑2)) → (2 · (√‘𝑦)) = (2 · (√‘(1 − (𝑥↑2)))))
243	242	oveq2d 7408	. . . . . . . . . 10 ⊢ (𝑦 = (1 − (𝑥↑2)) → (1 / (2 · (√‘𝑦))) = (1 / (2 · (√‘(1 − (𝑥↑2))))))
244	11, 11, 203, 209, 211, 212, 237, 240, 241, 243	dvmptco 26014	. . . . . . . . 9 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ (√‘(1 − (𝑥↑2))))) = (𝑥 ∈ 𝐷 ↦ ((1 / (2 · (√‘(1 − (𝑥↑2))))) · -(2 · 𝑥))))
245		mulneg2 11621	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (2 · -𝑥) = -(2 · 𝑥))
246	218, 12, 245	sylancr 596	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐷 → (2 · -𝑥) = -(2 · 𝑥))
247	246	oveq1d 7407	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐷 → ((2 · -𝑥) / (2 · (√‘(1 − (𝑥↑2))))) = (-(2 · 𝑥) / (2 · (√‘(1 − (𝑥↑2))))))
248	12	negcld 11526	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐷 → -𝑥 ∈ ℂ)
249		eldifn 4085	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞))) → ¬ 𝑥 ∈ ((-∞(,]-1) ∪ (1[,)+∞)))
250	249, 3	eleq2s 2879	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐷 → ¬ 𝑥 ∈ ((-∞(,]-1) ∪ (1[,)+∞)))
251		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = -1 → 𝑥 = -1)
252		mnflt 13122	. . . . . . . . . . . . . . . . . . . 20 ⊢ (-1 ∈ ℝ → -∞ < -1)
253	86, 252	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ -∞ < -1
254		ubioc1 13400	. . . . . . . . . . . . . . . . . . 19 ⊢ ((-∞ ∈ ℝ^* ∧ -1 ∈ ℝ^* ∧ -∞ < -1) → -1 ∈ (-∞(,]-1))
255	51, 132, 253, 254	mp3an 1481	. . . . . . . . . . . . . . . . . 18 ⊢ -1 ∈ (-∞(,]-1)
256	251, 255	eqeltrdi 2869	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = -1 → 𝑥 ∈ (-∞(,]-1))
257		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 1 → 𝑥 = 1)
258		ltpnf 13119	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 ∈ ℝ → 1 < +∞)
259	89, 258	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 < +∞
260		lbico1 13401	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ ℝ^* ∧ +∞ ∈ ℝ^* ∧ 1 < +∞) → 1 ∈ (1[,)+∞))
261	133, 121, 259, 260	mp3an 1481	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ (1[,)+∞)
262	257, 261	eqeltrdi 2869	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 1 → 𝑥 ∈ (1[,)+∞))
263	256, 262	orim12i 919	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = -1 ∨ 𝑥 = 1) → (𝑥 ∈ (-∞(,]-1) ∨ 𝑥 ∈ (1[,)+∞)))
264	263	orcoms 883	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = 1 ∨ 𝑥 = -1) → (𝑥 ∈ (-∞(,]-1) ∨ 𝑥 ∈ (1[,)+∞)))
265		elun 4106	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ((-∞(,]-1) ∪ (1[,)+∞)) ↔ (𝑥 ∈ (-∞(,]-1) ∨ 𝑥 ∈ (1[,)+∞)))
266	264, 265	sylibr 236	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 1 ∨ 𝑥 = -1) → 𝑥 ∈ ((-∞(,]-1) ∪ (1[,)+∞)))
267	250, 266	nsyl 140	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐷 → ¬ (𝑥 = 1 ∨ 𝑥 = -1))
268		1cnd 11172	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → 1 ∈ ℂ)
269	17	adantr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → (𝑥↑2) ∈ ℂ)
270	19	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → (1 − (𝑥↑2)) ∈ ℂ)
271		simpr 488	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → (√‘(1 − (𝑥↑2))) = 0)
272	270, 271	sqr00d 15454	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → (1 − (𝑥↑2)) = 0)
273	268, 269, 272	subeq0d 11547	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → 1 = (𝑥↑2))
274	146, 273	eqtr2id 2809	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → (𝑥↑2) = (1↑2))
275	274	ex 416	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℂ → ((√‘(1 − (𝑥↑2))) = 0 → (𝑥↑2) = (1↑2)))
276		sqeqor 14226	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑥↑2) = (1↑2) ↔ (𝑥 = 1 ∨ 𝑥 = -1)))
277	16, 276	mpan2 701	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℂ → ((𝑥↑2) = (1↑2) ↔ (𝑥 = 1 ∨ 𝑥 = -1)))
278	275, 277	sylibd 241	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℂ → ((√‘(1 − (𝑥↑2))) = 0 → (𝑥 = 1 ∨ 𝑥 = -1)))
279	278	necon3bd 2970	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℂ → (¬ (𝑥 = 1 ∨ 𝑥 = -1) → (√‘(1 − (𝑥↑2))) ≠ 0))
280	12, 267, 279	sylc 65	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐷 → (√‘(1 − (𝑥↑2))) ≠ 0)
281		2cnne0 12427	. . . . . . . . . . . . 13 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
282		divcan5 11890	. . . . . . . . . . . . 13 ⊢ ((-𝑥 ∈ ℂ ∧ ((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · -𝑥) / (2 · (√‘(1 − (𝑥↑2))))) = (-𝑥 / (√‘(1 − (𝑥↑2)))))
283	281, 282	mp3an3 1470	. . . . . . . . . . . 12 ⊢ ((-𝑥 ∈ ℂ ∧ ((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0)) → ((2 · -𝑥) / (2 · (√‘(1 − (𝑥↑2))))) = (-𝑥 / (√‘(1 − (𝑥↑2)))))
284	248, 112, 280, 283	syl12anc 847	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐷 → ((2 · -𝑥) / (2 · (√‘(1 − (𝑥↑2))))) = (-𝑥 / (√‘(1 − (𝑥↑2)))))
285	218, 12, 219	sylancr 596	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐷 → (2 · 𝑥) ∈ ℂ)
286	285	negcld 11526	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐷 → -(2 · 𝑥) ∈ ℂ)
287		mulcl 11154	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ∈ ℂ) → (2 · (√‘(1 − (𝑥↑2)))) ∈ ℂ)
288	218, 112, 287	sylancr 596	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐷 → (2 · (√‘(1 − (𝑥↑2)))) ∈ ℂ)
289		mulne0 11826	. . . . . . . . . . . . . 14 ⊢ (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ ((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0)) → (2 · (√‘(1 − (𝑥↑2)))) ≠ 0)
290	281, 289	mpan 700	. . . . . . . . . . . . 13 ⊢ (((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0) → (2 · (√‘(1 − (𝑥↑2)))) ≠ 0)
291	112, 280, 290	syl2anc 593	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐷 → (2 · (√‘(1 − (𝑥↑2)))) ≠ 0)
292	286, 288, 291	divrec2d 11968	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐷 → (-(2 · 𝑥) / (2 · (√‘(1 − (𝑥↑2))))) = ((1 / (2 · (√‘(1 − (𝑥↑2))))) · -(2 · 𝑥)))
293	247, 284, 292	3eqtr3rd 2805	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐷 → ((1 / (2 · (√‘(1 − (𝑥↑2))))) · -(2 · 𝑥)) = (-𝑥 / (√‘(1 − (𝑥↑2)))))
294	293	mpteq2ia 5194	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 ↦ ((1 / (2 · (√‘(1 − (𝑥↑2))))) · -(2 · 𝑥))) = (𝑥 ∈ 𝐷 ↦ (-𝑥 / (√‘(1 − (𝑥↑2)))))
295	244, 294	eqtrdi 2812	. . . . . . . 8 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ (√‘(1 − (𝑥↑2))))) = (𝑥 ∈ 𝐷 ↦ (-𝑥 / (√‘(1 − (𝑥↑2))))))
296	11, 74, 75, 109, 113, 114, 295	dvmptadd 26002	. . . . . . 7 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))) = (𝑥 ∈ 𝐷 ↦ (i + (-𝑥 / (√‘(1 − (𝑥↑2)))))))
297		mulcl 11154	. . . . . . . . . . . 12 ⊢ ((i ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ∈ ℂ) → (i · (√‘(1 − (𝑥↑2)))) ∈ ℂ)
298	13, 20, 297	sylancr 596	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℂ → (i · (√‘(1 − (𝑥↑2)))) ∈ ℂ)
299	12, 298	syl 17	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐷 → (i · (√‘(1 − (𝑥↑2)))) ∈ ℂ)
300	299, 248, 112, 280	divdird 12002	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → (((i · (√‘(1 − (𝑥↑2)))) + -𝑥) / (√‘(1 − (𝑥↑2)))) = (((i · (√‘(1 − (𝑥↑2)))) / (√‘(1 − (𝑥↑2)))) + (-𝑥 / (√‘(1 − (𝑥↑2))))))
301		ixi 11813	. . . . . . . . . . . . . . . 16 ⊢ (i · i) = -1
302	301	eqcomi 2770	. . . . . . . . . . . . . . 15 ⊢ -1 = (i · i)
303	302	oveq1i 7402	. . . . . . . . . . . . . 14 ⊢ (-1 · 𝑥) = ((i · i) · 𝑥)
304		mulm1 11625	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℂ → (-1 · 𝑥) = -𝑥)
305		mulass 11158	. . . . . . . . . . . . . . 15 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ ∧ 𝑥 ∈ ℂ) → ((i · i) · 𝑥) = (i · (i · 𝑥)))
306	13, 13, 305	mp3an12 1471	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℂ → ((i · i) · 𝑥) = (i · (i · 𝑥)))
307	303, 304, 306	3eqtr3a 2820	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℂ → -𝑥 = (i · (i · 𝑥)))
308	307	oveq1d 7407	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℂ → (-𝑥 + (i · (√‘(1 − (𝑥↑2))))) = ((i · (i · 𝑥)) + (i · (√‘(1 − (𝑥↑2))))))
309		negcl 11427	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℂ → -𝑥 ∈ ℂ)
310	298, 309	addcomd 11382	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℂ → ((i · (√‘(1 − (𝑥↑2)))) + -𝑥) = (-𝑥 + (i · (√‘(1 − (𝑥↑2))))))
311	13	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℂ → i ∈ ℂ)
312	311, 15, 20	adddid 11203	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℂ → (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) = ((i · (i · 𝑥)) + (i · (√‘(1 − (𝑥↑2))))))
313	308, 310, 312	3eqtr4d 2806	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℂ → ((i · (√‘(1 − (𝑥↑2)))) + -𝑥) = (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
314	12, 313	syl 17	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐷 → ((i · (√‘(1 − (𝑥↑2)))) + -𝑥) = (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
315	314	oveq1d 7407	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → (((i · (√‘(1 − (𝑥↑2)))) + -𝑥) / (√‘(1 − (𝑥↑2)))) = ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))))
316	72, 112, 280	divcan4d 11970	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐷 → ((i · (√‘(1 − (𝑥↑2)))) / (√‘(1 − (𝑥↑2)))) = i)
317	316	oveq1d 7407	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → (((i · (√‘(1 − (𝑥↑2)))) / (√‘(1 − (𝑥↑2)))) + (-𝑥 / (√‘(1 − (𝑥↑2))))) = (i + (-𝑥 / (√‘(1 − (𝑥↑2))))))
318	300, 315, 317	3eqtr3rd 2805	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐷 → (i + (-𝑥 / (√‘(1 − (𝑥↑2))))) = ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))))
319	318	mpteq2ia 5194	. . . . . . 7 ⊢ (𝑥 ∈ 𝐷 ↦ (i + (-𝑥 / (√‘(1 − (𝑥↑2)))))) = (𝑥 ∈ 𝐷 ↦ ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))))
320	296, 319	eqtrdi 2812	. . . . . 6 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))) = (𝑥 ∈ 𝐷 ↦ ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2))))))
321		logf1o 26606	. . . . . . . . . 10 ⊢ log:(ℂ ∖ {0})–1-1-onto→ran log
322		f1of 6802	. . . . . . . . . 10 ⊢ (log:(ℂ ∖ {0})–1-1-onto→ran log → log:(ℂ ∖ {0})⟶ran log)
323	321, 322	mp1i 13	. . . . . . . . 9 ⊢ (⊤ → log:(ℂ ∖ {0})⟶ran log)
324		snssi 4743	. . . . . . . . . . 11 ⊢ (0 ∈ (-∞(,]0) → {0} ⊆ (-∞(,]0))
325	64, 324	ax-mp 5	. . . . . . . . . 10 ⊢ {0} ⊆ (-∞(,]0)
326		sscon 4096	. . . . . . . . . 10 ⊢ ({0} ⊆ (-∞(,]0) → (ℂ ∖ (-∞(,]0)) ⊆ (ℂ ∖ {0}))
327	325, 326	mp1i 13	. . . . . . . . 9 ⊢ (⊤ → (ℂ ∖ (-∞(,]0)) ⊆ (ℂ ∖ {0}))
328	323, 327	feqresmpt 6932	. . . . . . . 8 ⊢ (⊤ → (log ↾ (ℂ ∖ (-∞(,]0))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (log‘𝑦)))
329	328	oveq2d 7408	. . . . . . 7 ⊢ (⊤ → (ℂ D (log ↾ (ℂ ∖ (-∞(,]0)))) = (ℂ D (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (log‘𝑦))))
330	238	dvlog 26693	. . . . . . 7 ⊢ (ℂ D (log ↾ (ℂ ∖ (-∞(,]0)))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (1 / 𝑦))
331	329, 330	eqtr3di 2811	. . . . . 6 ⊢ (⊤ → (ℂ D (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (log‘𝑦))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (1 / 𝑦)))
332		fveq2 6863	. . . . . 6 ⊢ (𝑦 = ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) → (log‘𝑦) = (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
333		oveq2 7400	. . . . . 6 ⊢ (𝑦 = ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) → (1 / 𝑦) = (1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
334	11, 11, 57, 58, 70, 71, 320, 331, 332, 333	dvmptco 26014	. . . . 5 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))) = (𝑥 ∈ 𝐷 ↦ ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))))))
335	22, 24	reccld 11957	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐷 → (1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
336		mulcl 11154	. . . . . . . . . 10 ⊢ ((i ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℂ) → (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
337	13, 21, 336	sylancr 596	. . . . . . . . 9 ⊢ (𝑥 ∈ ℂ → (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
338	12, 337	syl 17	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐷 → (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
339	335, 338, 112, 280	divassd 11999	. . . . . . 7 ⊢ (𝑥 ∈ 𝐷 → (((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))) / (√‘(1 − (𝑥↑2)))) = ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2))))))
340	338, 22, 24	divrec2d 11968	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) = ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))
341	72, 22, 24	divcan4d 11970	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) = i)
342	340, 341	eqtr3d 2798	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐷 → ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))) = i)
343	342	oveq1d 7407	. . . . . . 7 ⊢ (𝑥 ∈ 𝐷 → (((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))) / (√‘(1 − (𝑥↑2)))) = (i / (√‘(1 − (𝑥↑2)))))
344	339, 343	eqtr3d 2798	. . . . . 6 ⊢ (𝑥 ∈ 𝐷 → ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2))))) = (i / (√‘(1 − (𝑥↑2)))))
345	344	mpteq2ia 5194	. . . . 5 ⊢ (𝑥 ∈ 𝐷 ↦ ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))))) = (𝑥 ∈ 𝐷 ↦ (i / (√‘(1 − (𝑥↑2)))))
346	334, 345	eqtrdi 2812	. . . 4 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))) = (𝑥 ∈ 𝐷 ↦ (i / (√‘(1 − (𝑥↑2))))))
347		negicn 11428	. . . . 5 ⊢ -i ∈ ℂ
348	347	a1i 11	. . . 4 ⊢ (⊤ → -i ∈ ℂ)
349	11, 26, 27, 346, 348	dvmptcmul 26006	. . 3 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))) = (𝑥 ∈ 𝐷 ↦ (-i · (i / (√‘(1 − (𝑥↑2)))))))
350	349	mptru 1566	. 2 ⊢ (ℂ D (𝑥 ∈ 𝐷 ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))) = (𝑥 ∈ 𝐷 ↦ (-i · (i / (√‘(1 − (𝑥↑2))))))
351		divass 11860	. . . . . 6 ⊢ ((-i ∈ ℂ ∧ i ∈ ℂ ∧ ((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0)) → ((-i · i) / (√‘(1 − (𝑥↑2)))) = (-i · (i / (√‘(1 − (𝑥↑2))))))
352	347, 13, 351	mp3an12 1471	. . . . 5 ⊢ (((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0) → ((-i · i) / (√‘(1 − (𝑥↑2)))) = (-i · (i / (√‘(1 − (𝑥↑2))))))
353	112, 280, 352	syl2anc 593	. . . 4 ⊢ (𝑥 ∈ 𝐷 → ((-i · i) / (√‘(1 − (𝑥↑2)))) = (-i · (i / (√‘(1 − (𝑥↑2))))))
354	13, 13	mulneg1i 11630	. . . . . 6 ⊢ (-i · i) = -(i · i)
355	301	negeqi 11420	. . . . . 6 ⊢ -(i · i) = --1
356		negneg1e1 12181	. . . . . 6 ⊢ --1 = 1
357	354, 355, 356	3eqtri 2788	. . . . 5 ⊢ (-i · i) = 1
358	357	oveq1i 7402	. . . 4 ⊢ ((-i · i) / (√‘(1 − (𝑥↑2)))) = (1 / (√‘(1 − (𝑥↑2))))
359	353, 358	eqtr3di 2811	. . 3 ⊢ (𝑥 ∈ 𝐷 → (-i · (i / (√‘(1 − (𝑥↑2))))) = (1 / (√‘(1 − (𝑥↑2)))))
360	359	mpteq2ia 5194	. 2 ⊢ (𝑥 ∈ 𝐷 ↦ (-i · (i / (√‘(1 − (𝑥↑2)))))) = (𝑥 ∈ 𝐷 ↦ (1 / (√‘(1 − (𝑥↑2)))))
361	9, 350, 360	3eqtri 2788	1 ⊢ (ℂ D (arcsin ↾ 𝐷)) = (𝑥 ∈ 𝐷 ↦ (1 / (√‘(1 − (𝑥↑2)))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 399 ∨ wo 858 ∨ w3o 1096 ∧ w3a 1097 = wceq 1559 ⊤wtru 1560 ∈ wcel 2141 ≠ wne 2956 Vcvv 3453 ∖ cdif 3901 ∪ cun 3902 ∩ cin 3903 ⊆ wss 3904 ∅c0 4285 {csn 4581 {cpr 4583 class class class wbr 5099 ↦ cmpt 5180 ran crn 5646 ↾ cres 5647 ⟶wf 6513 –1-1-onto→wf1o 6516 ‘cfv 6517 (class class class)co 7392 ℂcc 11068 ℝcr 11069 0cc0 11070 1c1 11071 ici 11072 + caddc 11073 · cmul 11075 +∞cpnf 11210 -∞cmnf 11211 ℝ^*cxr 11212 < clt 11213 ≤ cle 11214 − cmin 11411 -cneg 11412 / cdiv 11841 ℕcn 12207 2c2 12269 ℝ⁺crp 12990 (,)cioo 13346 (,]cioc 13347 [,)cico 13348 ↑cexp 14071 ℜcre 15107 √csqrt 15243 abscabs 15244 ↾_t crest 17432 TopOpenctopn 17433 topGenctg 17449 ℂ_fldccnfld 21404 Clsdccld 23056 D cdv 25905 logclog 26596 arcsincasin 26904

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5226 ax-sep 5245 ax-nul 5255 ax-pow 5321 ax-pr 5389 ax-un 7714 ax-inf2 9593 ax-cnex 11126 ax-resscn 11127 ax-1cn 11128 ax-icn 11129 ax-addcl 11130 ax-addrcl 11131 ax-mulcl 11132 ax-mulrcl 11133 ax-mulcom 11134 ax-addass 11135 ax-mulass 11136 ax-distr 11137 ax-i2m1 11138 ax-1ne0 11139 ax-1rid 11140 ax-rnegex 11141 ax-rrecex 11142 ax-cnre 11143 ax-pre-lttri 11144 ax-pre-lttrn 11145 ax-pre-ltadd 11146 ax-pre-mulgt0 11147 ax-pre-sup 11148 ax-addf 11149

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1098 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3061 df-ral 3076 df-rex 3086 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3455 df-sbc 3745 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4582 df-pr 4584 df-tp 4586 df-op 4588 df-uni 4865 df-int 4905 df-iun 4950 df-iin 4951 df-br 5100 df-opab 5162 df-mpt 5181 df-tr 5207 df-id 5540 df-eprel 5545 df-po 5553 df-so 5554 df-fr 5598 df-se 5599 df-we 5600 df-xp 5651 df-rel 5652 df-cnv 5653 df-co 5654 df-dm 5655 df-rn 5656 df-res 5657 df-ima 5658 df-pred 6284 df-ord 6345 df-on 6346 df-lim 6347 df-suc 6348 df-iota 6473 df-fun 6519 df-fn 6520 df-f 6521 df-f1 6522 df-fo 6523 df-f1o 6524 df-fv 6525 df-isom 6526 df-riota 7349 df-ov 7395 df-oprab 7396 df-mpo 7397 df-of 7656 df-om 7843 df-1st 7966 df-2nd 7967 df-supp 8136 df-frecs 8257 df-wrecs 8288 df-recs 8337 df-rdg 8376 df-1o 8432 df-2o 8433 df-er 8673 df-map 8805 df-pm 8806 df-ixp 8876 df-en 8924 df-dom 8925 df-sdom 8926 df-fin 8927 df-fsupp 9305 df-fi 9354 df-sup 9385 df-inf 9386 df-oi 9455 df-card 9894 df-pnf 11215 df-mnf 11216 df-xr 11217 df-ltxr 11218 df-le 11219 df-sub 11413 df-neg 11414 df-div 11842 df-nn 12208 df-2 12277 df-3 12278 df-4 12279 df-5 12280 df-6 12281 df-7 12282 df-8 12283 df-9 12284 df-n0 12479 df-z 12566 df-dec 12686 df-uz 12837 df-q 12947 df-rp 12991 df-xneg 13111 df-xadd 13112 df-xmul 13113 df-ioo 13350 df-ioc 13351 df-ico 13352 df-icc 13353 df-fz 13510 df-fzo 13657 df-fl 13799 df-mod 13877 df-seq 14012 df-exp 14072 df-fac 14284 df-bc 14313 df-hash 14341 df-shft 15077 df-cj 15109 df-re 15110 df-im 15111 df-sqrt 15245 df-abs 15246 df-limsup 15481 df-clim 15498 df-rlim 15499 df-sum 15697 df-ef 16080 df-sin 16082 df-cos 16083 df-tan 16084 df-pi 16085 df-struct 17166 df-sets 17183 df-slot 17201 df-ndx 17213 df-base 17229 df-ress 17250 df-plusg 17282 df-mulr 17283 df-starv 17284 df-sca 17285 df-vsca 17286 df-ip 17287 df-tset 17288 df-ple 17289 df-ds 17291 df-unif 17292 df-hom 17293 df-cco 17294 df-rest 17434 df-topn 17435 df-0g 17453 df-gsum 17454 df-topgen 17455 df-pt 17456 df-prds 17459 df-xrs 17515 df-qtop 17520 df-imas 17521 df-xps 17523 df-mre 17597 df-mrc 17598 df-acs 17600 df-mgm 18657 df-sgrp 18736 df-mnd 18752 df-submnd 18801 df-mulg 19093 df-cntz 19340 df-cmn 19805 df-psmet 21396 df-xmet 21397 df-met 21398 df-bl 21399 df-mopn 21400 df-fbas 21401 df-fg 21402 df-cnfld 21405 df-top 22934 df-topon 22951 df-topsp 22973 df-bases 22986 df-cld 23059 df-ntr 23060 df-cls 23061 df-nei 23138 df-lp 23176 df-perf 23177 df-cn 23267 df-cnp 23268 df-haus 23355 df-cmp 23427 df-tx 23602 df-hmeo 23795 df-fil 23886 df-fm 23978 df-flim 23979 df-flf 23980 df-xms 24360 df-ms 24361 df-tms 24362 df-cncf 24920 df-limc 25908 df-dv 25909 df-log 26598 df-cxp 26599 df-asin 26907

This theorem is referenced by: dvacos 38168 dvreasin 38169

W3C validator