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 36561

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 26360	. . . . 5 ⊢ arcsin = (𝑥 ∈ ℂ ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))
2	1	reseq1i 5976	. . . 4 ⊢ (arcsin ↾ 𝐷) = ((𝑥 ∈ ℂ ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))) ↾ 𝐷)
3		dvasin.d	. . . . . 6 ⊢ 𝐷 = (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞)))
4		difss 4131	. . . . . 6 ⊢ (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞))) ⊆ ℂ
5	3, 4	eqsstri 4016	. . . . 5 ⊢ 𝐷 ⊆ ℂ
6		resmpt 6036	. . . . 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 2761	. . 3 ⊢ (arcsin ↾ 𝐷) = (𝑥 ∈ 𝐷 ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))
9	8	oveq2i 7417	. 2 ⊢ (ℂ D (arcsin ↾ 𝐷)) = (ℂ D (𝑥 ∈ 𝐷 ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))))
10		cnelprrecn 11200	. . . . 5 ⊢ ℂ ∈ {ℝ, ℂ}
11	10	a1i 11	. . . 4 ⊢ (⊤ → ℂ ∈ {ℝ, ℂ})
12	5	sseli 3978	. . . . . . 7 ⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ ℂ)
13		ax-icn 11166	. . . . . . . . 9 ⊢ i ∈ ℂ
14		mulcl 11191	. . . . . . . . 9 ⊢ ((i ∈ ℂ ∧ 𝑥 ∈ ℂ) → (i · 𝑥) ∈ ℂ)
15	13, 14	mpan 689	. . . . . . . 8 ⊢ (𝑥 ∈ ℂ → (i · 𝑥) ∈ ℂ)
16		ax-1cn 11165	. . . . . . . . . 10 ⊢ 1 ∈ ℂ
17		sqcl 14080	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℂ → (𝑥↑2) ∈ ℂ)
18		subcl 11456	. . . . . . . . . 10 ⊢ ((1 ∈ ℂ ∧ (𝑥↑2) ∈ ℂ) → (1 − (𝑥↑2)) ∈ ℂ)
19	16, 17, 18	sylancr 588	. . . . . . . . 9 ⊢ (𝑥 ∈ ℂ → (1 − (𝑥↑2)) ∈ ℂ)
20	19	sqrtcld 15381	. . . . . . . 8 ⊢ (𝑥 ∈ ℂ → (√‘(1 − (𝑥↑2))) ∈ ℂ)
21	15, 20	addcld 11230	. . . . . . 7 ⊢ (𝑥 ∈ ℂ → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℂ)
22	12, 21	syl 17	. . . . . 6 ⊢ (𝑥 ∈ 𝐷 → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℂ)
23		asinlem 26363	. . . . . . 7 ⊢ (𝑥 ∈ ℂ → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≠ 0)
24	12, 23	syl 17	. . . . . 6 ⊢ (𝑥 ∈ 𝐷 → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≠ 0)
25	22, 24	logcld 26071	. . . . 5 ⊢ (𝑥 ∈ 𝐷 → (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
26	25	adantl 483	. . . 4 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
27		ovexd 7441	. . . 4 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → (i / (√‘(1 − (𝑥↑2)))) ∈ V)
28		simpr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ)
29		asinlem3 26366	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℂ → 0 ≤ (ℜ‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
30		rere 15066	. . . . . . . . . . . . . . . . . . 19 ⊢ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → (ℜ‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) = ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))
31	30	breq2d 5160	. . . . . . . . . . . . . . . . . 18 ⊢ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → (0 ≤ (ℜ‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ↔ 0 ≤ ((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
32	31	biimpac 480	. . . . . . . . . . . . . . . . 17 ⊢ ((0 ≤ (ℜ‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → 0 ≤ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))
33	29, 32	sylan 581	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → 0 ≤ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))
34	23	adantr 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≠ 0)
35	28, 33, 34	ne0gt0d 11348	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → 0 < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))
36		0re 11213	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ ℝ
37		ltnle 11290	. . . . . . . . . . . . . . . . 17 ⊢ ((0 ∈ ℝ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → (0 < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ↔ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
38	36, 37	mpan 689	. . . . . . . . . . . . . . . 16 ⊢ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → (0 < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ↔ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
39	38	adantl 483	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → (0 < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ↔ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
40	35, 39	mpbid 231	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0)
41	40	ex 414	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℂ → (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
42	12, 41	syl 17	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐷 → (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
43		imor 852	. . . . . . . . . . . 12 ⊢ ((((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0) ↔ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
44	42, 43	sylib 217	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐷 → (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
45	44	orcomd 870	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐷 → (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ))
46	45	olcd 873	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → (¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ)))
47		3ianor 1108	. . . . . . . . . . 11 ⊢ (¬ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∧ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0) ↔ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∨ ¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
48		3orrot 1093	. . . . . . . . . . 11 ⊢ ((¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∨ ¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0) ↔ (¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ))
49		3orass 1091	. . . . . . . . . . 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 298	. . . . . . . . . 10 ⊢ ((¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ)) ↔ ¬ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∧ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
51		mnfxr 11268	. . . . . . . . . . 11 ⊢ -∞ ∈ ℝ^*
52		elioc2 13384	. . . . . . . . . . 11 ⊢ ((-∞ ∈ ℝ^* ∧ 0 ∈ ℝ) → (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (-∞(,]0) ↔ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∧ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0)))
53	51, 36, 52	mp2an 691	. . . . . . . . . 10 ⊢ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (-∞(,]0) ↔ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∧ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
54	50, 53	xchbinxr 335	. . . . . . . . 9 ⊢ ((¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ)) ↔ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (-∞(,]0))
55	46, 54	sylib 217	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐷 → ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (-∞(,]0))
56	22, 55	eldifd 3959	. . . . . . 7 ⊢ (𝑥 ∈ 𝐷 → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (ℂ ∖ (-∞(,]0)))
57	56	adantl 483	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (ℂ ∖ (-∞(,]0)))
58		ovexd 7441	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))) ∈ V)
59		eldifi 4126	. . . . . . . 8 ⊢ (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → 𝑦 ∈ ℂ)
60		eldifn 4127	. . . . . . . . 9 ⊢ (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → ¬ 𝑦 ∈ (-∞(,]0))
61		0xr 11258	. . . . . . . . . . . 12 ⊢ 0 ∈ ℝ^*
62		mnflt0 13102	. . . . . . . . . . . 12 ⊢ -∞ < 0
63		ubioc1 13374	. . . . . . . . . . . 12 ⊢ ((-∞ ∈ ℝ^* ∧ 0 ∈ ℝ^* ∧ -∞ < 0) → 0 ∈ (-∞(,]0))
64	51, 61, 62, 63	mp3an 1462	. . . . . . . . . . 11 ⊢ 0 ∈ (-∞(,]0)
65		eleq1 2822	. . . . . . . . . . 11 ⊢ (𝑦 = 0 → (𝑦 ∈ (-∞(,]0) ↔ 0 ∈ (-∞(,]0)))
66	64, 65	mpbiri 258	. . . . . . . . . 10 ⊢ (𝑦 = 0 → 𝑦 ∈ (-∞(,]0))
67	66	necon3bi 2968	. . . . . . . . 9 ⊢ (¬ 𝑦 ∈ (-∞(,]0) → 𝑦 ≠ 0)
68	60, 67	syl 17	. . . . . . . 8 ⊢ (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → 𝑦 ≠ 0)
69	59, 68	logcld 26071	. . . . . . 7 ⊢ (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → (log‘𝑦) ∈ ℂ)
70	69	adantl 483	. . . . . 6 ⊢ ((⊤ ∧ 𝑦 ∈ (ℂ ∖ (-∞(,]0))) → (log‘𝑦) ∈ ℂ)
71		ovexd 7441	. . . . . 6 ⊢ ((⊤ ∧ 𝑦 ∈ (ℂ ∖ (-∞(,]0))) → (1 / 𝑦) ∈ V)
72	13	a1i 11	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐷 → i ∈ ℂ)
73	72, 12	mulcld 11231	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → (i · 𝑥) ∈ ℂ)
74	73	adantl 483	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → (i · 𝑥) ∈ ℂ)
75	13	a1i 11	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → i ∈ ℂ)
76	12	adantl 483	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ ℂ)
77		1cnd 11206	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → 1 ∈ ℂ)
78		simpr 486	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → 𝑥 ∈ ℂ)
79		1cnd 11206	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → 1 ∈ ℂ)
80	11	dvmptid 25466	. . . . . . . . . . 11 ⊢ (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ 𝑥)) = (𝑥 ∈ ℂ ↦ 1))
81	5	a1i 11	. . . . . . . . . . 11 ⊢ (⊤ → 𝐷 ⊆ ℂ)
82		eqid 2733	. . . . . . . . . . . . 13 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
83	82	cnfldtopon 24291	. . . . . . . . . . . 12 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
84	83	toponrestid 22415	. . . . . . . . . . 11 ⊢ (TopOpen‘ℂ_fld) = ((TopOpen‘ℂ_fld) ↾_t ℂ)
85	82	recld2 24322	. . . . . . . . . . . . . . 15 ⊢ ℝ ∈ (Clsd‘(TopOpen‘ℂ_fld))
86		neg1rr 12324	. . . . . . . . . . . . . . . . . 18 ⊢ -1 ∈ ℝ
87		iocmnfcld 24277	. . . . . . . . . . . . . . . . . 18 ⊢ (-1 ∈ ℝ → (-∞(,]-1) ∈ (Clsd‘(topGen‘ran (,))))
88	86, 87	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (-∞(,]-1) ∈ (Clsd‘(topGen‘ran (,)))
89		1re 11211	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℝ
90		icopnfcld 24276	. . . . . . . . . . . . . . . . . 18 ⊢ (1 ∈ ℝ → (1[,)+∞) ∈ (Clsd‘(topGen‘ran (,))))
91	89, 90	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (1[,)+∞) ∈ (Clsd‘(topGen‘ran (,)))
92		uncld 22537	. . . . . . . . . . . . . . . . 17 ⊢ (((-∞(,]-1) ∈ (Clsd‘(topGen‘ran (,))) ∧ (1[,)+∞) ∈ (Clsd‘(topGen‘ran (,)))) → ((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘(topGen‘ran (,))))
93	88, 91, 92	mp2an 691	. . . . . . . . . . . . . . . 16 ⊢ ((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘(topGen‘ran (,)))
94	82	tgioo2 24311	. . . . . . . . . . . . . . . . 17 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
95	94	fveq2i 6892	. . . . . . . . . . . . . . . 16 ⊢ (Clsd‘(topGen‘ran (,))) = (Clsd‘((TopOpen‘ℂ_fld) ↾_t ℝ))
96	93, 95	eleqtri 2832	. . . . . . . . . . . . . . 15 ⊢ ((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘((TopOpen‘ℂ_fld) ↾_t ℝ))
97		restcldr 22670	. . . . . . . . . . . . . . 15 ⊢ ((ℝ ∈ (Clsd‘(TopOpen‘ℂ_fld)) ∧ ((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘((TopOpen‘ℂ_fld) ↾_t ℝ))) → ((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘(TopOpen‘ℂ_fld)))
98	85, 96, 97	mp2an 691	. . . . . . . . . . . . . 14 ⊢ ((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘(TopOpen‘ℂ_fld))
99	83	toponunii 22410	. . . . . . . . . . . . . . 15 ⊢ ℂ = ∪ (TopOpen‘ℂ_fld)
100	99	cldopn 22527	. . . . . . . . . . . . . 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 2830	. . . . . . . . . . . 12 ⊢ 𝐷 ∈ (TopOpen‘ℂ_fld)
103	102	a1i 11	. . . . . . . . . . 11 ⊢ (⊤ → 𝐷 ∈ (TopOpen‘ℂ_fld))
104	11, 78, 79, 80, 81, 84, 82, 103	dvmptres 25472	. . . . . . . . . 10 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ 𝑥)) = (𝑥 ∈ 𝐷 ↦ 1))
105	13	a1i 11	. . . . . . . . . 10 ⊢ (⊤ → i ∈ ℂ)
106	11, 76, 77, 104, 105	dvmptcmul 25473	. . . . . . . . 9 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ (i · 𝑥))) = (𝑥 ∈ 𝐷 ↦ (i · 1)))
107	13	mulridi 11215	. . . . . . . . . 10 ⊢ (i · 1) = i
108	107	mpteq2i 5253	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 ↦ (i · 1)) = (𝑥 ∈ 𝐷 ↦ i)
109	106, 108	eqtrdi 2789	. . . . . . . 8 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ (i · 𝑥))) = (𝑥 ∈ 𝐷 ↦ i))
110	12	sqcld 14106	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐷 → (𝑥↑2) ∈ ℂ)
111	16, 110, 18	sylancr 588	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐷 → (1 − (𝑥↑2)) ∈ ℂ)
112	111	sqrtcld 15381	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → (√‘(1 − (𝑥↑2))) ∈ ℂ)
113	112	adantl 483	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → (√‘(1 − (𝑥↑2))) ∈ ℂ)
114		ovexd 7441	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → (-𝑥 / (√‘(1 − (𝑥↑2)))) ∈ V)
115		elin 3964	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐷 ∩ ℝ) ↔ (𝑥 ∈ 𝐷 ∧ 𝑥 ∈ ℝ))
116	3	asindmre 36560	. . . . . . . . . . . . . . . . 17 ⊢ (𝐷 ∩ ℝ) = (-1(,)1)
117	116	eqimssi 4042	. . . . . . . . . . . . . . . 16 ⊢ (𝐷 ∩ ℝ) ⊆ (-1(,)1)
118	117	sseli 3978	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐷 ∩ ℝ) → 𝑥 ∈ (-1(,)1))
119	115, 118	sylbir 234	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ 𝐷 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ (-1(,)1))
120		incom 4201	. . . . . . . . . . . . . . . 16 ⊢ ((0(,)+∞) ∩ (-∞(,]0)) = ((-∞(,]0) ∩ (0(,)+∞))
121		pnfxr 11265	. . . . . . . . . . . . . . . . 17 ⊢ +∞ ∈ ℝ^*
122		df-ioc 13326	. . . . . . . . . . . . . . . . . 18 ⊢ (,] = (𝑥 ∈ ℝ^, 𝑦 ∈ ℝ^ ↦ {𝑧 ∈ ℝ^* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})
123		df-ioo 13325	. . . . . . . . . . . . . . . . . 18 ⊢ (,) = (𝑥 ∈ ℝ^, 𝑦 ∈ ℝ^ ↦ {𝑧 ∈ ℝ^* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
124		xrltnle 11278	. . . . . . . . . . . . . . . . . 18 ⊢ ((0 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) → (0 < 𝑤 ↔ ¬ 𝑤 ≤ 0))
125	122, 123, 124	ixxdisj 13336	. . . . . . . . . . . . . . . . 17 ⊢ ((-∞ ∈ ℝ^* ∧ 0 ∈ ℝ^* ∧ +∞ ∈ ℝ^*) → ((-∞(,]0) ∩ (0(,)+∞)) = ∅)
126	51, 61, 121, 125	mp3an 1462	. . . . . . . . . . . . . . . 16 ⊢ ((-∞(,]0) ∩ (0(,)+∞)) = ∅
127	120, 126	eqtri 2761	. . . . . . . . . . . . . . 15 ⊢ ((0(,)+∞) ∩ (-∞(,]0)) = ∅
128		elioore 13351	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (-1(,)1) → 𝑥 ∈ ℝ)
129	128	resqcld 14087	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (-1(,)1) → (𝑥↑2) ∈ ℝ)
130		resubcl 11521	. . . . . . . . . . . . . . . . . 18 ⊢ ((1 ∈ ℝ ∧ (𝑥↑2) ∈ ℝ) → (1 − (𝑥↑2)) ∈ ℝ)
131	89, 129, 130	sylancr 588	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (-1(,)1) → (1 − (𝑥↑2)) ∈ ℝ)
132	86	rexri 11269	. . . . . . . . . . . . . . . . . . 19 ⊢ -1 ∈ ℝ^*
133		1xr 11270	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℝ^*
134		elioo2 13362	. . . . . . . . . . . . . . . . . . 19 ⊢ ((-1 ∈ ℝ^* ∧ 1 ∈ ℝ^*) → (𝑥 ∈ (-1(,)1) ↔ (𝑥 ∈ ℝ ∧ -1 < 𝑥 ∧ 𝑥 < 1)))
135	132, 133, 134	mp2an 691	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (-1(,)1) ↔ (𝑥 ∈ ℝ ∧ -1 < 𝑥 ∧ 𝑥 < 1))
136		recn 11197	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
137	136	abscld 15380	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℝ → (abs‘𝑥) ∈ ℝ)
138	136	absge0d 15388	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℝ → 0 ≤ (abs‘𝑥))
139		0le1 11734	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 ≤ 1
140		lt2sq 14095	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((abs‘𝑥) ∈ ℝ ∧ 0 ≤ (abs‘𝑥)) ∧ (1 ∈ ℝ ∧ 0 ≤ 1)) → ((abs‘𝑥) < 1 ↔ ((abs‘𝑥)↑2) < (1↑2)))
141	89, 139, 140	mpanr12 704	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((abs‘𝑥) ∈ ℝ ∧ 0 ≤ (abs‘𝑥)) → ((abs‘𝑥) < 1 ↔ ((abs‘𝑥)↑2) < (1↑2)))
142	137, 138, 141	syl2anc 585	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℝ → ((abs‘𝑥) < 1 ↔ ((abs‘𝑥)↑2) < (1↑2)))
143		abslt 15258	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑥) < 1 ↔ (-1 < 𝑥 ∧ 𝑥 < 1)))
144	89, 143	mpan2 690	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℝ → ((abs‘𝑥) < 1 ↔ (-1 < 𝑥 ∧ 𝑥 < 1)))
145		absresq 15246	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℝ → ((abs‘𝑥)↑2) = (𝑥↑2))
146		sq1 14156	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1↑2) = 1
147	146	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℝ → (1↑2) = 1)
148	145, 147	breq12d 5161	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℝ → (((abs‘𝑥)↑2) < (1↑2) ↔ (𝑥↑2) < 1))
149		resqcl 14086	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℝ → (𝑥↑2) ∈ ℝ)
150		posdif 11704	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑥↑2) ∈ ℝ ∧ 1 ∈ ℝ) → ((𝑥↑2) < 1 ↔ 0 < (1 − (𝑥↑2))))
151	149, 89, 150	sylancl 587	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℝ → ((𝑥↑2) < 1 ↔ 0 < (1 − (𝑥↑2))))
152	148, 151	bitrd 279	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℝ → (((abs‘𝑥)↑2) < (1↑2) ↔ 0 < (1 − (𝑥↑2))))
153	142, 144, 152	3bitr3d 309	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ → ((-1 < 𝑥 ∧ 𝑥 < 1) ↔ 0 < (1 − (𝑥↑2))))
154	153	biimpd 228	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℝ → ((-1 < 𝑥 ∧ 𝑥 < 1) → 0 < (1 − (𝑥↑2))))
155	154	3impib 1117	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℝ ∧ -1 < 𝑥 ∧ 𝑥 < 1) → 0 < (1 − (𝑥↑2)))
156	135, 155	sylbi 216	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (-1(,)1) → 0 < (1 − (𝑥↑2)))
157	131, 156	elrpd 13010	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (-1(,)1) → (1 − (𝑥↑2)) ∈ ℝ⁺)
158		ioorp 13399	. . . . . . . . . . . . . . . 16 ⊢ (0(,)+∞) = ℝ⁺
159	157, 158	eleqtrrdi 2845	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (-1(,)1) → (1 − (𝑥↑2)) ∈ (0(,)+∞))
160		disjel 4456	. . . . . . . . . . . . . . 15 ⊢ ((((0(,)+∞) ∩ (-∞(,]0)) = ∅ ∧ (1 − (𝑥↑2)) ∈ (0(,)+∞)) → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
161	127, 159, 160	sylancr 588	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (-1(,)1) → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
162	119, 161	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝐷 ∧ 𝑥 ∈ ℝ) → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
163		elioc2 13384	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((-∞ ∈ ℝ^* ∧ 0 ∈ ℝ) → ((1 − (𝑥↑2)) ∈ (-∞(,]0) ↔ ((1 − (𝑥↑2)) ∈ ℝ ∧ -∞ < (1 − (𝑥↑2)) ∧ (1 − (𝑥↑2)) ≤ 0)))
164	51, 36, 163	mp2an 691	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1 − (𝑥↑2)) ∈ (-∞(,]0) ↔ ((1 − (𝑥↑2)) ∈ ℝ ∧ -∞ < (1 − (𝑥↑2)) ∧ (1 − (𝑥↑2)) ≤ 0))
165	164	biimpi 215	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1 − (𝑥↑2)) ∈ (-∞(,]0) → ((1 − (𝑥↑2)) ∈ ℝ ∧ -∞ < (1 − (𝑥↑2)) ∧ (1 − (𝑥↑2)) ≤ 0))
166	165	simp1d 1143	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1 − (𝑥↑2)) ∈ (-∞(,]0) → (1 − (𝑥↑2)) ∈ ℝ)
167		resubcl 11521	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1 ∈ ℝ ∧ (1 − (𝑥↑2)) ∈ ℝ) → (1 − (1 − (𝑥↑2))) ∈ ℝ)
168	89, 166, 167	sylancr 588	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 − (𝑥↑2)) ∈ (-∞(,]0) → (1 − (1 − (𝑥↑2))) ∈ ℝ)
169		nncan 11486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1 ∈ ℂ ∧ (𝑥↑2) ∈ ℂ) → (1 − (1 − (𝑥↑2))) = (𝑥↑2))
170	16, 169	mpan 689	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥↑2) ∈ ℂ → (1 − (1 − (𝑥↑2))) = (𝑥↑2))
171	170	eleq1d 2819	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥↑2) ∈ ℂ → ((1 − (1 − (𝑥↑2))) ∈ ℝ ↔ (𝑥↑2) ∈ ℝ))
172	171	biimpa 478	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥↑2) ∈ ℂ ∧ (1 − (1 − (𝑥↑2))) ∈ ℝ) → (𝑥↑2) ∈ ℝ)
173	168, 172	sylan2 594	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (𝑥↑2) ∈ ℝ)
174	166	adantl 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (1 − (𝑥↑2)) ∈ ℝ)
175	165	simp3d 1145	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1 − (𝑥↑2)) ∈ (-∞(,]0) → (1 − (𝑥↑2)) ≤ 0)
176	175	adantl 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (1 − (𝑥↑2)) ≤ 0)
177		letr 11305	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((1 − (𝑥↑2)) ∈ ℝ ∧ 0 ∈ ℝ ∧ 1 ∈ ℝ) → (((1 − (𝑥↑2)) ≤ 0 ∧ 0 ≤ 1) → (1 − (𝑥↑2)) ≤ 1))
178	36, 89, 177	mp3an23 1454	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1 − (𝑥↑2)) ∈ ℝ → (((1 − (𝑥↑2)) ≤ 0 ∧ 0 ≤ 1) → (1 − (𝑥↑2)) ≤ 1))
179	139, 178	mpan2i 696	. . . . . . . . . . . . . . . . . . . . . 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 11724	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1 ∈ ℝ ∧ (1 − (𝑥↑2)) ∈ ℝ) → (0 ≤ (1 − (1 − (𝑥↑2))) ↔ (1 − (𝑥↑2)) ≤ 1))
182	89, 174, 181	sylancr 588	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (0 ≤ (1 − (1 − (𝑥↑2))) ↔ (1 − (𝑥↑2)) ≤ 1))
183	180, 182	mpbird 257	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → 0 ≤ (1 − (1 − (𝑥↑2))))
184	170	adantr 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (1 − (1 − (𝑥↑2))) = (𝑥↑2))
185	183, 184	breqtrd 5174	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → 0 ≤ (𝑥↑2))
186	173, 185	resqrtcld 15361	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (√‘(𝑥↑2)) ∈ ℝ)
187	17, 186	sylan 581	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (√‘(𝑥↑2)) ∈ ℝ)
188		eleq1 2822	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (√‘(𝑥↑2)) → (𝑥 ∈ ℝ ↔ (√‘(𝑥↑2)) ∈ ℝ))
189	187, 188	syl5ibrcom 246	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (𝑥 = (√‘(𝑥↑2)) → 𝑥 ∈ ℝ))
190	187	renegcld 11638	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → -(√‘(𝑥↑2)) ∈ ℝ)
191		eleq1 2822	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = -(√‘(𝑥↑2)) → (𝑥 ∈ ℝ ↔ -(√‘(𝑥↑2)) ∈ ℝ))
192	190, 191	syl5ibrcom 246	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (𝑥 = -(√‘(𝑥↑2)) → 𝑥 ∈ ℝ))
193		eqid 2733	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥↑2) = (𝑥↑2)
194		eqsqrtor 15310	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℂ ∧ (𝑥↑2) ∈ ℂ) → ((𝑥↑2) = (𝑥↑2) ↔ (𝑥 = (√‘(𝑥↑2)) ∨ 𝑥 = -(√‘(𝑥↑2)))))
195	17, 194	mpdan 686	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℂ → ((𝑥↑2) = (𝑥↑2) ↔ (𝑥 = (√‘(𝑥↑2)) ∨ 𝑥 = -(√‘(𝑥↑2)))))
196	193, 195	mpbii 232	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℂ → (𝑥 = (√‘(𝑥↑2)) ∨ 𝑥 = -(√‘(𝑥↑2))))
197	196	adantr 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (𝑥 = (√‘(𝑥↑2)) ∨ 𝑥 = -(√‘(𝑥↑2))))
198	189, 192, 197	mpjaod 859	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → 𝑥 ∈ ℝ)
199	198	stoic1a 1775	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℂ ∧ ¬ 𝑥 ∈ ℝ) → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
200	12, 199	sylan 581	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝐷 ∧ ¬ 𝑥 ∈ ℝ) → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
201	162, 200	pm2.61dan 812	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐷 → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
202	111, 201	eldifd 3959	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐷 → (1 − (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0)))
203	202	adantl 483	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → (1 − (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0)))
204		2cnd 12287	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℂ → 2 ∈ ℂ)
205		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℂ → 𝑥 ∈ ℂ)
206	204, 205	mulcld 11231	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℂ → (2 · 𝑥) ∈ ℂ)
207	206	negcld 11555	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℂ → -(2 · 𝑥) ∈ ℂ)
208	207	adantl 483	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → -(2 · 𝑥) ∈ ℂ)
209	12, 208	sylan2 594	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → -(2 · 𝑥) ∈ ℂ)
210	59	sqrtcld 15381	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → (√‘𝑦) ∈ ℂ)
211	210	adantl 483	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑦 ∈ (ℂ ∖ (-∞(,]0))) → (√‘𝑦) ∈ ℂ)
212		ovexd 7441	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑦 ∈ (ℂ ∖ (-∞(,]0))) → (1 / (2 · (√‘𝑦))) ∈ V)
213	19	adantl 483	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → (1 − (𝑥↑2)) ∈ ℂ)
214	36	a1i 11	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → 0 ∈ ℝ)
215		1cnd 11206	. . . . . . . . . . . . . 14 ⊢ (⊤ → 1 ∈ ℂ)
216	11, 215	dvmptc 25467	. . . . . . . . . . . . 13 ⊢ (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ 1)) = (𝑥 ∈ ℂ ↦ 0))
217	17	adantl 483	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → (𝑥↑2) ∈ ℂ)
218		2cn 12284	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℂ
219		mulcl 11191	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (2 · 𝑥) ∈ ℂ)
220	218, 219	mpan 689	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℂ → (2 · 𝑥) ∈ ℂ)
221	220	adantl 483	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → (2 · 𝑥) ∈ ℂ)
222		2nn 12282	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℕ
223		dvexp 25462	. . . . . . . . . . . . . . . 16 ⊢ (2 ∈ ℕ → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · (𝑥↑(2 − 1)))))
224	222, 223	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · (𝑥↑(2 − 1))))
225		2m1e1 12335	. . . . . . . . . . . . . . . . . . 19 ⊢ (2 − 1) = 1
226	225	oveq2i 7417	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥↑(2 − 1)) = (𝑥↑1)
227		exp1 14030	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℂ → (𝑥↑1) = 𝑥)
228	226, 227	eqtrid 2785	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℂ → (𝑥↑(2 − 1)) = 𝑥)
229	228	oveq2d 7422	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℂ → (2 · (𝑥↑(2 − 1))) = (2 · 𝑥))
230	229	mpteq2ia 5251	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℂ ↦ (2 · (𝑥↑(2 − 1)))) = (𝑥 ∈ ℂ ↦ (2 · 𝑥))
231	224, 230	eqtri 2761	. . . . . . . . . . . . . 14 ⊢ (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · 𝑥))
232	231	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · 𝑥)))
233	11, 79, 214, 216, 217, 221, 232	dvmptsub 25476	. . . . . . . . . . . 12 ⊢ (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (1 − (𝑥↑2)))) = (𝑥 ∈ ℂ ↦ (0 − (2 · 𝑥))))
234		df-neg 11444	. . . . . . . . . . . . 13 ⊢ -(2 · 𝑥) = (0 − (2 · 𝑥))
235	234	mpteq2i 5253	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℂ ↦ -(2 · 𝑥)) = (𝑥 ∈ ℂ ↦ (0 − (2 · 𝑥)))
236	233, 235	eqtr4di 2791	. . . . . . . . . . 11 ⊢ (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (1 − (𝑥↑2)))) = (𝑥 ∈ ℂ ↦ -(2 · 𝑥)))
237	11, 213, 208, 236, 81, 84, 82, 103	dvmptres 25472	. . . . . . . . . 10 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ (1 − (𝑥↑2)))) = (𝑥 ∈ 𝐷 ↦ -(2 · 𝑥)))
238		eqid 2733	. . . . . . . . . . . 12 ⊢ (ℂ ∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0))
239	238	dvcnsqrt 26242	. . . . . . . . . . 11 ⊢ (ℂ D (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (√‘𝑦))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (1 / (2 · (√‘𝑦))))
240	239	a1i 11	. . . . . . . . . 10 ⊢ (⊤ → (ℂ D (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (√‘𝑦))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (1 / (2 · (√‘𝑦)))))
241		fveq2 6889	. . . . . . . . . 10 ⊢ (𝑦 = (1 − (𝑥↑2)) → (√‘𝑦) = (√‘(1 − (𝑥↑2))))
242	241	oveq2d 7422	. . . . . . . . . . 11 ⊢ (𝑦 = (1 − (𝑥↑2)) → (2 · (√‘𝑦)) = (2 · (√‘(1 − (𝑥↑2)))))
243	242	oveq2d 7422	. . . . . . . . . 10 ⊢ (𝑦 = (1 − (𝑥↑2)) → (1 / (2 · (√‘𝑦))) = (1 / (2 · (√‘(1 − (𝑥↑2))))))
244	11, 11, 203, 209, 211, 212, 237, 240, 241, 243	dvmptco 25481	. . . . . . . . 9 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ (√‘(1 − (𝑥↑2))))) = (𝑥 ∈ 𝐷 ↦ ((1 / (2 · (√‘(1 − (𝑥↑2))))) · -(2 · 𝑥))))
245		mulneg2 11648	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (2 · -𝑥) = -(2 · 𝑥))
246	218, 12, 245	sylancr 588	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐷 → (2 · -𝑥) = -(2 · 𝑥))
247	246	oveq1d 7421	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐷 → ((2 · -𝑥) / (2 · (√‘(1 − (𝑥↑2))))) = (-(2 · 𝑥) / (2 · (√‘(1 − (𝑥↑2))))))
248	12	negcld 11555	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐷 → -𝑥 ∈ ℂ)
249		eldifn 4127	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞))) → ¬ 𝑥 ∈ ((-∞(,]-1) ∪ (1[,)+∞)))
250	249, 3	eleq2s 2852	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐷 → ¬ 𝑥 ∈ ((-∞(,]-1) ∪ (1[,)+∞)))
251		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = -1 → 𝑥 = -1)
252		mnflt 13100	. . . . . . . . . . . . . . . . . . . 20 ⊢ (-1 ∈ ℝ → -∞ < -1)
253	86, 252	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ -∞ < -1
254		ubioc1 13374	. . . . . . . . . . . . . . . . . . 19 ⊢ ((-∞ ∈ ℝ^* ∧ -1 ∈ ℝ^* ∧ -∞ < -1) → -1 ∈ (-∞(,]-1))
255	51, 132, 253, 254	mp3an 1462	. . . . . . . . . . . . . . . . . 18 ⊢ -1 ∈ (-∞(,]-1)
256	251, 255	eqeltrdi 2842	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = -1 → 𝑥 ∈ (-∞(,]-1))
257		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 1 → 𝑥 = 1)
258		ltpnf 13097	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 ∈ ℝ → 1 < +∞)
259	89, 258	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 < +∞
260		lbico1 13375	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ ℝ^* ∧ +∞ ∈ ℝ^* ∧ 1 < +∞) → 1 ∈ (1[,)+∞))
261	133, 121, 259, 260	mp3an 1462	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ (1[,)+∞)
262	257, 261	eqeltrdi 2842	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 1 → 𝑥 ∈ (1[,)+∞))
263	256, 262	orim12i 908	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = -1 ∨ 𝑥 = 1) → (𝑥 ∈ (-∞(,]-1) ∨ 𝑥 ∈ (1[,)+∞)))
264	263	orcoms 871	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = 1 ∨ 𝑥 = -1) → (𝑥 ∈ (-∞(,]-1) ∨ 𝑥 ∈ (1[,)+∞)))
265		elun 4148	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ((-∞(,]-1) ∪ (1[,)+∞)) ↔ (𝑥 ∈ (-∞(,]-1) ∨ 𝑥 ∈ (1[,)+∞)))
266	264, 265	sylibr 233	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 1 ∨ 𝑥 = -1) → 𝑥 ∈ ((-∞(,]-1) ∪ (1[,)+∞)))
267	250, 266	nsyl 140	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐷 → ¬ (𝑥 = 1 ∨ 𝑥 = -1))
268		1cnd 11206	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → 1 ∈ ℂ)
269	17	adantr 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → (𝑥↑2) ∈ ℂ)
270	19	adantr 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → (1 − (𝑥↑2)) ∈ ℂ)
271		simpr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → (√‘(1 − (𝑥↑2))) = 0)
272	270, 271	sqr00d 15385	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → (1 − (𝑥↑2)) = 0)
273	268, 269, 272	subeq0d 11576	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → 1 = (𝑥↑2))
274	146, 273	eqtr2id 2786	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → (𝑥↑2) = (1↑2))
275	274	ex 414	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℂ → ((√‘(1 − (𝑥↑2))) = 0 → (𝑥↑2) = (1↑2)))
276		sqeqor 14177	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑥↑2) = (1↑2) ↔ (𝑥 = 1 ∨ 𝑥 = -1)))
277	16, 276	mpan2 690	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℂ → ((𝑥↑2) = (1↑2) ↔ (𝑥 = 1 ∨ 𝑥 = -1)))
278	275, 277	sylibd 238	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℂ → ((√‘(1 − (𝑥↑2))) = 0 → (𝑥 = 1 ∨ 𝑥 = -1)))
279	278	necon3bd 2955	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℂ → (¬ (𝑥 = 1 ∨ 𝑥 = -1) → (√‘(1 − (𝑥↑2))) ≠ 0))
280	12, 267, 279	sylc 65	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐷 → (√‘(1 − (𝑥↑2))) ≠ 0)
281		2cnne0 12419	. . . . . . . . . . . . 13 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
282		divcan5 11913	. . . . . . . . . . . . 13 ⊢ ((-𝑥 ∈ ℂ ∧ ((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · -𝑥) / (2 · (√‘(1 − (𝑥↑2))))) = (-𝑥 / (√‘(1 − (𝑥↑2)))))
283	281, 282	mp3an3 1451	. . . . . . . . . . . 12 ⊢ ((-𝑥 ∈ ℂ ∧ ((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0)) → ((2 · -𝑥) / (2 · (√‘(1 − (𝑥↑2))))) = (-𝑥 / (√‘(1 − (𝑥↑2)))))
284	248, 112, 280, 283	syl12anc 836	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐷 → ((2 · -𝑥) / (2 · (√‘(1 − (𝑥↑2))))) = (-𝑥 / (√‘(1 − (𝑥↑2)))))
285	218, 12, 219	sylancr 588	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐷 → (2 · 𝑥) ∈ ℂ)
286	285	negcld 11555	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐷 → -(2 · 𝑥) ∈ ℂ)
287		mulcl 11191	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ∈ ℂ) → (2 · (√‘(1 − (𝑥↑2)))) ∈ ℂ)
288	218, 112, 287	sylancr 588	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐷 → (2 · (√‘(1 − (𝑥↑2)))) ∈ ℂ)
289		mulne0 11853	. . . . . . . . . . . . . 14 ⊢ (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ ((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0)) → (2 · (√‘(1 − (𝑥↑2)))) ≠ 0)
290	281, 289	mpan 689	. . . . . . . . . . . . 13 ⊢ (((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0) → (2 · (√‘(1 − (𝑥↑2)))) ≠ 0)
291	112, 280, 290	syl2anc 585	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐷 → (2 · (√‘(1 − (𝑥↑2)))) ≠ 0)
292	286, 288, 291	divrec2d 11991	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐷 → (-(2 · 𝑥) / (2 · (√‘(1 − (𝑥↑2))))) = ((1 / (2 · (√‘(1 − (𝑥↑2))))) · -(2 · 𝑥)))
293	247, 284, 292	3eqtr3rd 2782	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐷 → ((1 / (2 · (√‘(1 − (𝑥↑2))))) · -(2 · 𝑥)) = (-𝑥 / (√‘(1 − (𝑥↑2)))))
294	293	mpteq2ia 5251	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 ↦ ((1 / (2 · (√‘(1 − (𝑥↑2))))) · -(2 · 𝑥))) = (𝑥 ∈ 𝐷 ↦ (-𝑥 / (√‘(1 − (𝑥↑2)))))
295	244, 294	eqtrdi 2789	. . . . . . . 8 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ (√‘(1 − (𝑥↑2))))) = (𝑥 ∈ 𝐷 ↦ (-𝑥 / (√‘(1 − (𝑥↑2))))))
296	11, 74, 75, 109, 113, 114, 295	dvmptadd 25469	. . . . . . 7 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))) = (𝑥 ∈ 𝐷 ↦ (i + (-𝑥 / (√‘(1 − (𝑥↑2)))))))
297		mulcl 11191	. . . . . . . . . . . 12 ⊢ ((i ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ∈ ℂ) → (i · (√‘(1 − (𝑥↑2)))) ∈ ℂ)
298	13, 20, 297	sylancr 588	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℂ → (i · (√‘(1 − (𝑥↑2)))) ∈ ℂ)
299	12, 298	syl 17	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐷 → (i · (√‘(1 − (𝑥↑2)))) ∈ ℂ)
300	299, 248, 112, 280	divdird 12025	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → (((i · (√‘(1 − (𝑥↑2)))) + -𝑥) / (√‘(1 − (𝑥↑2)))) = (((i · (√‘(1 − (𝑥↑2)))) / (√‘(1 − (𝑥↑2)))) + (-𝑥 / (√‘(1 − (𝑥↑2))))))
301		ixi 11840	. . . . . . . . . . . . . . . 16 ⊢ (i · i) = -1
302	301	eqcomi 2742	. . . . . . . . . . . . . . 15 ⊢ -1 = (i · i)
303	302	oveq1i 7416	. . . . . . . . . . . . . 14 ⊢ (-1 · 𝑥) = ((i · i) · 𝑥)
304		mulm1 11652	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℂ → (-1 · 𝑥) = -𝑥)
305		mulass 11195	. . . . . . . . . . . . . . 15 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ ∧ 𝑥 ∈ ℂ) → ((i · i) · 𝑥) = (i · (i · 𝑥)))
306	13, 13, 305	mp3an12 1452	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℂ → ((i · i) · 𝑥) = (i · (i · 𝑥)))
307	303, 304, 306	3eqtr3a 2797	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℂ → -𝑥 = (i · (i · 𝑥)))
308	307	oveq1d 7421	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℂ → (-𝑥 + (i · (√‘(1 − (𝑥↑2))))) = ((i · (i · 𝑥)) + (i · (√‘(1 − (𝑥↑2))))))
309		negcl 11457	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℂ → -𝑥 ∈ ℂ)
310	298, 309	addcomd 11413	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℂ → ((i · (√‘(1 − (𝑥↑2)))) + -𝑥) = (-𝑥 + (i · (√‘(1 − (𝑥↑2))))))
311	13	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℂ → i ∈ ℂ)
312	311, 15, 20	adddid 11235	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℂ → (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) = ((i · (i · 𝑥)) + (i · (√‘(1 − (𝑥↑2))))))
313	308, 310, 312	3eqtr4d 2783	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℂ → ((i · (√‘(1 − (𝑥↑2)))) + -𝑥) = (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
314	12, 313	syl 17	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐷 → ((i · (√‘(1 − (𝑥↑2)))) + -𝑥) = (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
315	314	oveq1d 7421	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → (((i · (√‘(1 − (𝑥↑2)))) + -𝑥) / (√‘(1 − (𝑥↑2)))) = ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))))
316	72, 112, 280	divcan4d 11993	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐷 → ((i · (√‘(1 − (𝑥↑2)))) / (√‘(1 − (𝑥↑2)))) = i)
317	316	oveq1d 7421	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → (((i · (√‘(1 − (𝑥↑2)))) / (√‘(1 − (𝑥↑2)))) + (-𝑥 / (√‘(1 − (𝑥↑2))))) = (i + (-𝑥 / (√‘(1 − (𝑥↑2))))))
318	300, 315, 317	3eqtr3rd 2782	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐷 → (i + (-𝑥 / (√‘(1 − (𝑥↑2))))) = ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))))
319	318	mpteq2ia 5251	. . . . . . 7 ⊢ (𝑥 ∈ 𝐷 ↦ (i + (-𝑥 / (√‘(1 − (𝑥↑2)))))) = (𝑥 ∈ 𝐷 ↦ ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))))
320	296, 319	eqtrdi 2789	. . . . . 6 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))) = (𝑥 ∈ 𝐷 ↦ ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2))))))
321		logf1o 26065	. . . . . . . . . 10 ⊢ log:(ℂ ∖ {0})–1-1-onto→ran log
322		f1of 6831	. . . . . . . . . 10 ⊢ (log:(ℂ ∖ {0})–1-1-onto→ran log → log:(ℂ ∖ {0})⟶ran log)
323	321, 322	mp1i 13	. . . . . . . . 9 ⊢ (⊤ → log:(ℂ ∖ {0})⟶ran log)
324		snssi 4811	. . . . . . . . . . 11 ⊢ (0 ∈ (-∞(,]0) → {0} ⊆ (-∞(,]0))
325	64, 324	ax-mp 5	. . . . . . . . . 10 ⊢ {0} ⊆ (-∞(,]0)
326		sscon 4138	. . . . . . . . . 10 ⊢ ({0} ⊆ (-∞(,]0) → (ℂ ∖ (-∞(,]0)) ⊆ (ℂ ∖ {0}))
327	325, 326	mp1i 13	. . . . . . . . 9 ⊢ (⊤ → (ℂ ∖ (-∞(,]0)) ⊆ (ℂ ∖ {0}))
328	323, 327	feqresmpt 6959	. . . . . . . 8 ⊢ (⊤ → (log ↾ (ℂ ∖ (-∞(,]0))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (log‘𝑦)))
329	328	oveq2d 7422	. . . . . . 7 ⊢ (⊤ → (ℂ D (log ↾ (ℂ ∖ (-∞(,]0)))) = (ℂ D (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (log‘𝑦))))
330	238	dvlog 26151	. . . . . . 7 ⊢ (ℂ D (log ↾ (ℂ ∖ (-∞(,]0)))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (1 / 𝑦))
331	329, 330	eqtr3di 2788	. . . . . 6 ⊢ (⊤ → (ℂ D (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (log‘𝑦))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (1 / 𝑦)))
332		fveq2 6889	. . . . . 6 ⊢ (𝑦 = ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) → (log‘𝑦) = (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
333		oveq2 7414	. . . . . 6 ⊢ (𝑦 = ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) → (1 / 𝑦) = (1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
334	11, 11, 57, 58, 70, 71, 320, 331, 332, 333	dvmptco 25481	. . . . 5 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))) = (𝑥 ∈ 𝐷 ↦ ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))))))
335	22, 24	reccld 11980	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐷 → (1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
336		mulcl 11191	. . . . . . . . . 10 ⊢ ((i ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℂ) → (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
337	13, 21, 336	sylancr 588	. . . . . . . . 9 ⊢ (𝑥 ∈ ℂ → (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
338	12, 337	syl 17	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐷 → (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
339	335, 338, 112, 280	divassd 12022	. . . . . . 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 11991	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) = ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))
341	72, 22, 24	divcan4d 11993	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) = i)
342	340, 341	eqtr3d 2775	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐷 → ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))) = i)
343	342	oveq1d 7421	. . . . . . 7 ⊢ (𝑥 ∈ 𝐷 → (((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))) / (√‘(1 − (𝑥↑2)))) = (i / (√‘(1 − (𝑥↑2)))))
344	339, 343	eqtr3d 2775	. . . . . 6 ⊢ (𝑥 ∈ 𝐷 → ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2))))) = (i / (√‘(1 − (𝑥↑2)))))
345	344	mpteq2ia 5251	. . . . 5 ⊢ (𝑥 ∈ 𝐷 ↦ ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))))) = (𝑥 ∈ 𝐷 ↦ (i / (√‘(1 − (𝑥↑2)))))
346	334, 345	eqtrdi 2789	. . . 4 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))) = (𝑥 ∈ 𝐷 ↦ (i / (√‘(1 − (𝑥↑2))))))
347		negicn 11458	. . . . 5 ⊢ -i ∈ ℂ
348	347	a1i 11	. . . 4 ⊢ (⊤ → -i ∈ ℂ)
349	11, 26, 27, 346, 348	dvmptcmul 25473	. . 3 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))) = (𝑥 ∈ 𝐷 ↦ (-i · (i / (√‘(1 − (𝑥↑2)))))))
350	349	mptru 1549	. 2 ⊢ (ℂ D (𝑥 ∈ 𝐷 ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))) = (𝑥 ∈ 𝐷 ↦ (-i · (i / (√‘(1 − (𝑥↑2))))))
351		divass 11887	. . . . . 6 ⊢ ((-i ∈ ℂ ∧ i ∈ ℂ ∧ ((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0)) → ((-i · i) / (√‘(1 − (𝑥↑2)))) = (-i · (i / (√‘(1 − (𝑥↑2))))))
352	347, 13, 351	mp3an12 1452	. . . . 5 ⊢ (((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0) → ((-i · i) / (√‘(1 − (𝑥↑2)))) = (-i · (i / (√‘(1 − (𝑥↑2))))))
353	112, 280, 352	syl2anc 585	. . . 4 ⊢ (𝑥 ∈ 𝐷 → ((-i · i) / (√‘(1 − (𝑥↑2)))) = (-i · (i / (√‘(1 − (𝑥↑2))))))
354	13, 13	mulneg1i 11657	. . . . . 6 ⊢ (-i · i) = -(i · i)
355	301	negeqi 11450	. . . . . 6 ⊢ -(i · i) = --1
356		negneg1e1 12327	. . . . . 6 ⊢ --1 = 1
357	354, 355, 356	3eqtri 2765	. . . . 5 ⊢ (-i · i) = 1
358	357	oveq1i 7416	. . . 4 ⊢ ((-i · i) / (√‘(1 − (𝑥↑2)))) = (1 / (√‘(1 − (𝑥↑2))))
359	353, 358	eqtr3di 2788	. . 3 ⊢ (𝑥 ∈ 𝐷 → (-i · (i / (√‘(1 − (𝑥↑2))))) = (1 / (√‘(1 − (𝑥↑2)))))
360	359	mpteq2ia 5251	. 2 ⊢ (𝑥 ∈ 𝐷 ↦ (-i · (i / (√‘(1 − (𝑥↑2)))))) = (𝑥 ∈ 𝐷 ↦ (1 / (√‘(1 − (𝑥↑2)))))
361	9, 350, 360	3eqtri 2765	1 ⊢ (ℂ D (arcsin ↾ 𝐷)) = (𝑥 ∈ 𝐷 ↦ (1 / (√‘(1 − (𝑥↑2)))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 397 ∨ wo 846 ∨ w3o 1087 ∧ w3a 1088 = wceq 1542 ⊤wtru 1543 ∈ wcel 2107 ≠ wne 2941 Vcvv 3475 ∖ cdif 3945 ∪ cun 3946 ∩ cin 3947 ⊆ wss 3948 ∅c0 4322 {csn 4628 {cpr 4630 class class class wbr 5148 ↦ cmpt 5231 ran crn 5677 ↾ cres 5678 ⟶wf 6537 –1-1-onto→wf1o 6540 ‘cfv 6541 (class class class)co 7406 ℂcc 11105 ℝcr 11106 0cc0 11107 1c1 11108 ici 11109 + caddc 11110 · cmul 11112 +∞cpnf 11242 -∞cmnf 11243 ℝ^*cxr 11244 < clt 11245 ≤ cle 11246 − cmin 11441 -cneg 11442 / cdiv 11868 ℕcn 12209 2c2 12264 ℝ⁺crp 12971 (,)cioo 13321 (,]cioc 13322 [,)cico 13323 ↑cexp 14024 ℜcre 15041 √csqrt 15177 abscabs 15178 ↾_t crest 17363 TopOpenctopn 17364 topGenctg 17380 ℂ_fldccnfld 20937 Clsdccld 22512 D cdv 25372 logclog 26055 arcsincasin 26357

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7722 ax-inf2 9633 ax-cnex 11163 ax-resscn 11164 ax-1cn 11165 ax-icn 11166 ax-addcl 11167 ax-addrcl 11168 ax-mulcl 11169 ax-mulrcl 11170 ax-mulcom 11171 ax-addass 11172 ax-mulass 11173 ax-distr 11174 ax-i2m1 11175 ax-1ne0 11176 ax-1rid 11177 ax-rnegex 11178 ax-rrecex 11179 ax-cnre 11180 ax-pre-lttri 11181 ax-pre-lttrn 11182 ax-pre-ltadd 11183 ax-pre-mulgt0 11184 ax-pre-sup 11185 ax-addf 11186 ax-mulf 11187

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3377 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-tp 4633 df-op 4635 df-uni 4909 df-int 4951 df-iun 4999 df-iin 5000 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-se 5632 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6298 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6493 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-isom 6550 df-riota 7362 df-ov 7409 df-oprab 7410 df-mpo 7411 df-of 7667 df-om 7853 df-1st 7972 df-2nd 7973 df-supp 8144 df-frecs 8263 df-wrecs 8294 df-recs 8368 df-rdg 8407 df-1o 8463 df-2o 8464 df-er 8700 df-map 8819 df-pm 8820 df-ixp 8889 df-en 8937 df-dom 8938 df-sdom 8939 df-fin 8940 df-fsupp 9359 df-fi 9403 df-sup 9434 df-inf 9435 df-oi 9502 df-card 9931 df-pnf 11247 df-mnf 11248 df-xr 11249 df-ltxr 11250 df-le 11251 df-sub 11443 df-neg 11444 df-div 11869 df-nn 12210 df-2 12272 df-3 12273 df-4 12274 df-5 12275 df-6 12276 df-7 12277 df-8 12278 df-9 12279 df-n0 12470 df-z 12556 df-dec 12675 df-uz 12820 df-q 12930 df-rp 12972 df-xneg 13089 df-xadd 13090 df-xmul 13091 df-ioo 13325 df-ioc 13326 df-ico 13327 df-icc 13328 df-fz 13482 df-fzo 13625 df-fl 13754 df-mod 13832 df-seq 13964 df-exp 14025 df-fac 14231 df-bc 14260 df-hash 14288 df-shft 15011 df-cj 15043 df-re 15044 df-im 15045 df-sqrt 15179 df-abs 15180 df-limsup 15412 df-clim 15429 df-rlim 15430 df-sum 15630 df-ef 16008 df-sin 16010 df-cos 16011 df-tan 16012 df-pi 16013 df-struct 17077 df-sets 17094 df-slot 17112 df-ndx 17124 df-base 17142 df-ress 17171 df-plusg 17207 df-mulr 17208 df-starv 17209 df-sca 17210 df-vsca 17211 df-ip 17212 df-tset 17213 df-ple 17214 df-ds 17216 df-unif 17217 df-hom 17218 df-cco 17219 df-rest 17365 df-topn 17366 df-0g 17384 df-gsum 17385 df-topgen 17386 df-pt 17387 df-prds 17390 df-xrs 17445 df-qtop 17450 df-imas 17451 df-xps 17453 df-mre 17527 df-mrc 17528 df-acs 17530 df-mgm 18558 df-sgrp 18607 df-mnd 18623 df-submnd 18669 df-mulg 18946 df-cntz 19176 df-cmn 19645 df-psmet 20929 df-xmet 20930 df-met 20931 df-bl 20932 df-mopn 20933 df-fbas 20934 df-fg 20935 df-cnfld 20938 df-top 22388 df-topon 22405 df-topsp 22427 df-bases 22441 df-cld 22515 df-ntr 22516 df-cls 22517 df-nei 22594 df-lp 22632 df-perf 22633 df-cn 22723 df-cnp 22724 df-haus 22811 df-cmp 22883 df-tx 23058 df-hmeo 23251 df-fil 23342 df-fm 23434 df-flim 23435 df-flf 23436 df-xms 23818 df-ms 23819 df-tms 23820 df-cncf 24386 df-limc 25375 df-dv 25376 df-log 26057 df-cxp 26058 df-asin 26360

This theorem is referenced by: dvacos 36562 dvreasin 36563

W3C validator