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 38715

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 27198	. . . . 5 ⊢ arcsin = (𝑥 ∈ ℂ ↦ ( -i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))
2	1	reseq1i 5965	. . . 4 ⊢ (arcsin ↾ 𝐷) = ((𝑥 ∈ ℂ ↦ ( -i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))) ↾ 𝐷)
3		dvasin.d	. . . . . 6 ⊢ 𝐷 = (ℂ ∖ ((-∞(,] -1) ∪ (1[,)+∞)))
4		difss 4072	. . . . . 6 ⊢ (ℂ ∖ ((-∞(,] -1) ∪ (1[,)+∞))) ⊆ ℂ
5	3, 4	eqsstri 3954	. . . . 5 ⊢ 𝐷 ⊆ ℂ
6		resmpt 6028	. . . . 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 2783	. . 3 ⊢ (arcsin ↾ 𝐷) = (𝑥 ∈ 𝐷 ↦ ( -i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))
9	8	oveq2i 7431	. 2 ⊢ (ℂ D (arcsin ↾ 𝐷)) = (ℂ D (𝑥 ∈ 𝐷 ↦ ( -i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))))
10		cnelprrecn 11296	. . . . 5 ⊢ ℂ ∈ {ℝ, ℂ}
11	10	a1i 11	. . . 4 ⊢ (⊤ → ℂ ∈ {ℝ, ℂ})
12	5	sseli 3904	. . . . . . 7 ⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ ℂ)
13		ax-icn 11262	. . . . . . . . 9 ⊢ i ∈ ℂ
14		mulcl 11287	. . . . . . . . 9 ⊢ ((i ∈ ℂ ∧ 𝑥 ∈ ℂ) → (i · 𝑥) ∈ ℂ)
15	13, 14	mpan 703	. . . . . . . 8 ⊢ (𝑥 ∈ ℂ → (i · 𝑥) ∈ ℂ)
16		ax-1cn 11261	. . . . . . . . . 10 ⊢ 1 ∈ ℂ
17		sqcl 14264	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℂ → (𝑥↑2) ∈ ℂ)
18		subcl 11559	. . . . . . . . . 10 ⊢ ((1 ∈ ℂ ∧ (𝑥↑2) ∈ ℂ) → (1 − (𝑥↑2)) ∈ ℂ)
19	16, 17, 18	sylancr 599	. . . . . . . . 9 ⊢ (𝑥 ∈ ℂ → (1 − (𝑥↑2)) ∈ ℂ)
20	19	sqrtcld 15612	. . . . . . . 8 ⊢ (𝑥 ∈ ℂ → (√‘(1 − (𝑥↑2))) ∈ ℂ)
21	15, 20	addcld 11331	. . . . . . 7 ⊢ (𝑥 ∈ ℂ → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℂ)
22	12, 21	syl 18	. . . . . 6 ⊢ (𝑥 ∈ 𝐷 → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℂ)
23		asinlem 27201	. . . . . . 7 ⊢ (𝑥 ∈ ℂ → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≠ 0)
24	12, 23	syl 18	. . . . . 6 ⊢ (𝑥 ∈ 𝐷 → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≠ 0)
25	22, 24	logcld 26903	. . . . 5 ⊢ (𝑥 ∈ 𝐷 → (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
26	25	adantl 487	. . . 4 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
27		ovexd 7455	. . . 4 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → (i / (√‘(1 − (𝑥↑2)))) ∈ V)
28		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ)
29		asinlem3 27204	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℂ → 0 ≤ (ℜ‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
30		rere 15294	. . . . . . . . . . . . . . . . . . 19 ⊢ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → (ℜ‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) = ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))
31	30	breq2d 5114	. . . . . . . . . . . . . . . . . 18 ⊢ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → (0 ≤ (ℜ‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ↔ 0 ≤ ((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
32	31	biimpac 484	. . . . . . . . . . . . . . . . 17 ⊢ ((0 ≤ (ℜ‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → 0 ≤ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))
33	29, 32	sylan 592	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → 0 ≤ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))
34	23	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≠ 0)
35	28, 33, 34	ne0gt0d 11450	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → 0 < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))
36		0re 11313	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ ℝ
37		ltnle 11392	. . . . . . . . . . . . . . . . 17 ⊢ ((0 ∈ ℝ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → (0 < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ↔ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
38	36, 37	mpan 703	. . . . . . . . . . . . . . . 16 ⊢ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → (0 < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ↔ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
39	38	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → (0 < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ↔ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
40	35, 39	mpbid 235	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0)
41	40	ex 418	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℂ → (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
42	12, 41	syl 18	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐷 → (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
43		imor 867	. . . . . . . . . . . 12 ⊢ ((((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0) ↔ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
44	42, 43	sylib 221	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐷 → (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
45	44	orcomd 885	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐷 → (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ))
46	45	olcd 888	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → (¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ)))
47		3ianor 1124	. . . . . . . . . . 11 ⊢ (¬ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∧ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0) ↔ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∨ ¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
48		3orrot 1108	. . . . . . . . . . 11 ⊢ ((¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∨ ¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0) ↔ (¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ))
49		3orass 1106	. . . . . . . . . . 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 301	. . . . . . . . . 10 ⊢ ((¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ)) ↔ ¬ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∧ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
51		mnfxr 11369	. . . . . . . . . . 11 ⊢ -∞ ∈ ℝ^*
52		elioc2 13543	. . . . . . . . . . 11 ⊢ ((-∞ ∈ ℝ^* ∧ 0 ∈ ℝ) → (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (-∞(,]0) ↔ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∧ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0)))
53	51, 36, 52	mp2an 705	. . . . . . . . . 10 ⊢ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (-∞(,]0) ↔ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∧ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
54	50, 53	xchbinxr 338	. . . . . . . . 9 ⊢ ((¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ)) ↔ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (-∞(,]0))
55	46, 54	sylib 221	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐷 → ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (-∞(,]0))
56	22, 55	eldifd 4050	. . . . . . 7 ⊢ (𝑥 ∈ 𝐷 → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (ℂ ∖ (-∞(,]0)))
57	56	adantl 487	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (ℂ ∖ (-∞(,]0)))
58		ovexd 7455	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))) ∈ V)
59		eldifi 4067	. . . . . . . 8 ⊢ (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → 𝑦 ∈ ℂ)
60		eldifn 4068	. . . . . . . . 9 ⊢ (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → ¬ 𝑦 ∈ (-∞(,]0))
61		0xr 11359	. . . . . . . . . . . 12 ⊢ 0 ∈ ℝ^*
62		mnflt0 13257	. . . . . . . . . . . 12 ⊢ -∞ < 0
63		ubioc1 13533	. . . . . . . . . . . 12 ⊢ ((-∞ ∈ ℝ^* ∧ 0 ∈ ℝ^* ∧ -∞ < 0) → 0 ∈ (-∞(,]0))
64	51, 61, 62, 63	mp3an 1490	. . . . . . . . . . 11 ⊢ 0 ∈ (-∞(,]0)
65		eleq1 2848	. . . . . . . . . . 11 ⊢ (𝑦 = 0 → (𝑦 ∈ (-∞(,]0) ↔ 0 ∈ (-∞(,]0)))
66	64, 65	mpbiri 261	. . . . . . . . . 10 ⊢ (𝑦 = 0 → 𝑦 ∈ (-∞(,]0))
67	66	necon3bi 2981	. . . . . . . . 9 ⊢ (¬ 𝑦 ∈ (-∞(,]0) → 𝑦 ≠ 0)
68	60, 67	syl 18	. . . . . . . 8 ⊢ (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → 𝑦 ≠ 0)
69	59, 68	logcld 26903	. . . . . . 7 ⊢ (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → (log‘𝑦) ∈ ℂ)
70	69	adantl 487	. . . . . 6 ⊢ ((⊤ ∧ 𝑦 ∈ (ℂ ∖ (-∞(,]0))) → (log‘𝑦) ∈ ℂ)
71		ovexd 7455	. . . . . 6 ⊢ ((⊤ ∧ 𝑦 ∈ (ℂ ∖ (-∞(,]0))) → (1 / 𝑦) ∈ V)
72	13	a1i 11	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐷 → i ∈ ℂ)
73	72, 12	mulcld 11332	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → (i · 𝑥) ∈ ℂ)
74	73	adantl 487	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → (i · 𝑥) ∈ ℂ)
75	13	a1i 11	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → i ∈ ℂ)
76	12	adantl 487	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ ℂ)
77		1cnd 11305	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → 1 ∈ ℂ)
78		simpr 490	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → 𝑥 ∈ ℂ)
79		1cnd 11305	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → 1 ∈ ℂ)
80	11	dvmptid 26282	. . . . . . . . . . 11 ⊢ (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ 𝑥)) = (𝑥 ∈ ℂ ↦ 1))
81	5	a1i 11	. . . . . . . . . . 11 ⊢ (⊤ → 𝐷 ⊆ ℂ)
82		eqid 2760	. . . . . . . . . . . . 13 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
83	82	cnfldtopon 25106	. . . . . . . . . . . 12 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
84	83	toponrestid 23244	. . . . . . . . . . 11 ⊢ (TopOpen‘ℂ_fld) = ((TopOpen‘ℂ_fld) ↾_t ℂ)
85	82	recld2 25139	. . . . . . . . . . . . . . 15 ⊢ ℝ ∈ (Clsd‘(TopOpen‘ℂ_fld))
86		neg1rr 12309	. . . . . . . . . . . . . . . . . 18 ⊢ -1 ∈ ℝ
87		iocmnfcld 25092	. . . . . . . . . . . . . . . . . 18 ⊢ ( -1 ∈ ℝ → (-∞(,] -1) ∈ (Clsd‘(topGen‘ran (,))))
88	86, 87	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (-∞(,] -1) ∈ (Clsd‘(topGen‘ran (,)))
89		1re 11311	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℝ
90		icopnfcld 25091	. . . . . . . . . . . . . . . . . 18 ⊢ (1 ∈ ℝ → (1[,)+∞) ∈ (Clsd‘(topGen‘ran (,))))
91	89, 90	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (1[,)+∞) ∈ (Clsd‘(topGen‘ran (,)))
92		uncld 23364	. . . . . . . . . . . . . . . . 17 ⊢ (((-∞(,] -1) ∈ (Clsd‘(topGen‘ran (,))) ∧ (1[,)+∞) ∈ (Clsd‘(topGen‘ran (,)))) → ((-∞(,] -1) ∪ (1[,)+∞)) ∈ (Clsd‘(topGen‘ran (,))))
93	88, 91, 92	mp2an 705	. . . . . . . . . . . . . . . 16 ⊢ ((-∞(,] -1) ∪ (1[,)+∞)) ∈ (Clsd‘(topGen‘ran (,)))
94		tgioo4 25129	. . . . . . . . . . . . . . . . 17 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
95	94	fveq2i 6888	. . . . . . . . . . . . . . . 16 ⊢ (Clsd‘(topGen‘ran (,))) = (Clsd‘((TopOpen‘ℂ_fld) ↾_t ℝ))
96	93, 95	eleqtri 2858	. . . . . . . . . . . . . . 15 ⊢ ((-∞(,] -1) ∪ (1[,)+∞)) ∈ (Clsd‘((TopOpen‘ℂ_fld) ↾_t ℝ))
97		restcldr 23497	. . . . . . . . . . . . . . 15 ⊢ ((ℝ ∈ (Clsd‘(TopOpen‘ℂ_fld)) ∧ ((-∞(,] -1) ∪ (1[,)+∞)) ∈ (Clsd‘((TopOpen‘ℂ_fld) ↾_t ℝ))) → ((-∞(,] -1) ∪ (1[,)+∞)) ∈ (Clsd‘(TopOpen‘ℂ_fld)))
98	85, 96, 97	mp2an 705	. . . . . . . . . . . . . 14 ⊢ ((-∞(,] -1) ∪ (1[,)+∞)) ∈ (Clsd‘(TopOpen‘ℂ_fld))
99	83	toponunii 23239	. . . . . . . . . . . . . . 15 ⊢ ℂ = ∪ (TopOpen‘ℂ_fld)
100	99	cldopn 23354	. . . . . . . . . . . . . 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 2856	. . . . . . . . . . . 12 ⊢ 𝐷 ∈ (TopOpen‘ℂ_fld)
103	102	a1i 11	. . . . . . . . . . 11 ⊢ (⊤ → 𝐷 ∈ (TopOpen‘ℂ_fld))
104	11, 78, 79, 80, 81, 84, 82, 103	dvmptres 26288	. . . . . . . . . 10 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ 𝑥)) = (𝑥 ∈ 𝐷 ↦ 1))
105	13	a1i 11	. . . . . . . . . 10 ⊢ (⊤ → i ∈ ℂ)
106	11, 76, 77, 104, 105	dvmptcmul 26289	. . . . . . . . 9 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ (i · 𝑥))) = (𝑥 ∈ 𝐷 ↦ (i · 1)))
107	13	mulridi 11316	. . . . . . . . . 10 ⊢ (i · 1) = i
108	107	mpteq2i 5200	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 ↦ (i · 1)) = (𝑥 ∈ 𝐷 ↦ i)
109	106, 108	eqtrdi 2811	. . . . . . . 8 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ (i · 𝑥))) = (𝑥 ∈ 𝐷 ↦ i))
110	12	sqcld 14290	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐷 → (𝑥↑2) ∈ ℂ)
111	16, 110, 18	sylancr 599	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐷 → (1 − (𝑥↑2)) ∈ ℂ)
112	111	sqrtcld 15612	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → (√‘(1 − (𝑥↑2))) ∈ ℂ)
113	112	adantl 487	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → (√‘(1 − (𝑥↑2))) ∈ ℂ)
114		ovexd 7455	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → ( -𝑥 / (√‘(1 − (𝑥↑2)))) ∈ V)
115		elin 4093	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐷 ∩ ℝ) ↔ (𝑥 ∈ 𝐷 ∧ 𝑥 ∈ ℝ))
116	3	asindmre 38714	. . . . . . . . . . . . . . . . 17 ⊢ (𝐷 ∩ ℝ) = ( -1(,)1)
117	116	eqimssi 3968	. . . . . . . . . . . . . . . 16 ⊢ (𝐷 ∩ ℝ) ⊆ ( -1(,)1)
118	117	sseli 3904	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐷 ∩ ℝ) → 𝑥 ∈ ( -1(,)1))
119	115, 118	sylbir 238	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ 𝐷 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ( -1(,)1))
120		incom 4106	. . . . . . . . . . . . . . . 16 ⊢ ((0(,)+∞) ∩ (-∞(,]0)) = ((-∞(,]0) ∩ (0(,)+∞))
121		pnfxr 11366	. . . . . . . . . . . . . . . . 17 ⊢ +∞ ∈ ℝ^*
122		df-ioc 13484	. . . . . . . . . . . . . . . . . 18 ⊢ (,] = (𝑥 ∈ ℝ^, 𝑦 ∈ ℝ^ ↦ {𝑧 ∈ ℝ^* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})
123		df-ioo 13483	. . . . . . . . . . . . . . . . . 18 ⊢ (,) = (𝑥 ∈ ℝ^, 𝑦 ∈ ℝ^ ↦ {𝑧 ∈ ℝ^* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
124		xrltnle 11379	. . . . . . . . . . . . . . . . . 18 ⊢ ((0 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) → (0 < 𝑤 ↔ ¬ 𝑤 ≤ 0))
125	122, 123, 124	ixxdisj 13494	. . . . . . . . . . . . . . . . 17 ⊢ ((-∞ ∈ ℝ^* ∧ 0 ∈ ℝ^* ∧ +∞ ∈ ℝ^*) → ((-∞(,]0) ∩ (0(,)+∞)) = ∅)
126	51, 61, 121, 125	mp3an 1490	. . . . . . . . . . . . . . . 16 ⊢ ((-∞(,]0) ∩ (0(,)+∞)) = ∅
127	120, 126	eqtri 2783	. . . . . . . . . . . . . . 15 ⊢ ((0(,)+∞) ∩ (-∞(,]0)) = ∅
128		elioore 13509	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ( -1(,)1) → 𝑥 ∈ ℝ)
129	128	resqcld 14271	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ( -1(,)1) → (𝑥↑2) ∈ ℝ)
130		resubcl 11625	. . . . . . . . . . . . . . . . . 18 ⊢ ((1 ∈ ℝ ∧ (𝑥↑2) ∈ ℝ) → (1 − (𝑥↑2)) ∈ ℝ)
131	89, 129, 130	sylancr 599	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ( -1(,)1) → (1 − (𝑥↑2)) ∈ ℝ)
132	86	rexri 11370	. . . . . . . . . . . . . . . . . . 19 ⊢ -1 ∈ ℝ^*
133		1xr 11371	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℝ^*
134		elioo2 13520	. . . . . . . . . . . . . . . . . . 19 ⊢ (( -1 ∈ ℝ^* ∧ 1 ∈ ℝ^*) → (𝑥 ∈ ( -1(,)1) ↔ (𝑥 ∈ ℝ ∧ -1 < 𝑥 ∧ 𝑥 < 1)))
135	132, 133, 134	mp2an 705	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ( -1(,)1) ↔ (𝑥 ∈ ℝ ∧ -1 < 𝑥 ∧ 𝑥 < 1))
136		recn 11293	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
137	136	abscld 15611	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℝ → (abs‘𝑥) ∈ ℝ)
138	136	absge0d 15619	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℝ → 0 ≤ (abs‘𝑥))
139		0le1 11842	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 ≤ 1
140		lt2sq 14279	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((abs‘𝑥) ∈ ℝ ∧ 0 ≤ (abs‘𝑥)) ∧ (1 ∈ ℝ ∧ 0 ≤ 1)) → ((abs‘𝑥) < 1 ↔ ((abs‘𝑥)↑2) < (1↑2)))
141	89, 139, 140	mpanr12 718	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((abs‘𝑥) ∈ ℝ ∧ 0 ≤ (abs‘𝑥)) → ((abs‘𝑥) < 1 ↔ ((abs‘𝑥)↑2) < (1↑2)))
142	137, 138, 141	syl2anc 596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℝ → ((abs‘𝑥) < 1 ↔ ((abs‘𝑥)↑2) < (1↑2)))
143		abslt 15487	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑥) < 1 ↔ ( -1 < 𝑥 ∧ 𝑥 < 1)))
144	89, 143	mpan2 704	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℝ → ((abs‘𝑥) < 1 ↔ ( -1 < 𝑥 ∧ 𝑥 < 1)))
145		absresq 15474	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℝ → ((abs‘𝑥)↑2) = (𝑥↑2))
146		sq1 14341	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1↑2) = 1
147	146	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℝ → (1↑2) = 1)
148	145, 147	breq12d 5115	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℝ → (((abs‘𝑥)↑2) < (1↑2) ↔ (𝑥↑2) < 1))
149		resqcl 14270	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℝ → (𝑥↑2) ∈ ℝ)
150		posdif 11812	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑥↑2) ∈ ℝ ∧ 1 ∈ ℝ) → ((𝑥↑2) < 1 ↔ 0 < (1 − (𝑥↑2))))
151	149, 89, 150	sylancl 598	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℝ → ((𝑥↑2) < 1 ↔ 0 < (1 − (𝑥↑2))))
152	148, 151	bitrd 282	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℝ → (((abs‘𝑥)↑2) < (1↑2) ↔ 0 < (1 − (𝑥↑2))))
153	142, 144, 152	3bitr3d 312	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ → (( -1 < 𝑥 ∧ 𝑥 < 1) ↔ 0 < (1 − (𝑥↑2))))
154	153	biimpd 232	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℝ → (( -1 < 𝑥 ∧ 𝑥 < 1) → 0 < (1 − (𝑥↑2))))
155	154	3impib 1134	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℝ ∧ -1 < 𝑥 ∧ 𝑥 < 1) → 0 < (1 − (𝑥↑2)))
156	135, 155	sylbi 220	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ( -1(,)1) → 0 < (1 − (𝑥↑2)))
157	131, 156	elrpd 13164	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ( -1(,)1) → (1 − (𝑥↑2)) ∈ ℝ⁺)
158		ioorp 13559	. . . . . . . . . . . . . . . 16 ⊢ (0(,)+∞) = ℝ⁺
159	157, 158	eleqtrrdi 2871	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ( -1(,)1) → (1 − (𝑥↑2)) ∈ (0(,)+∞))
160		disjel 4409	. . . . . . . . . . . . . . 15 ⊢ ((((0(,)+∞) ∩ (-∞(,]0)) = ∅ ∧ (1 − (𝑥↑2)) ∈ (0(,)+∞)) → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
161	127, 159, 160	sylancr 599	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ( -1(,)1) → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
162	119, 161	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝐷 ∧ 𝑥 ∈ ℝ) → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
163		elioc2 13543	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((-∞ ∈ ℝ^* ∧ 0 ∈ ℝ) → ((1 − (𝑥↑2)) ∈ (-∞(,]0) ↔ ((1 − (𝑥↑2)) ∈ ℝ ∧ -∞ < (1 − (𝑥↑2)) ∧ (1 − (𝑥↑2)) ≤ 0)))
164	51, 36, 163	mp2an 705	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1 − (𝑥↑2)) ∈ (-∞(,]0) ↔ ((1 − (𝑥↑2)) ∈ ℝ ∧ -∞ < (1 − (𝑥↑2)) ∧ (1 − (𝑥↑2)) ≤ 0))
165	164	biimpi 219	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1 − (𝑥↑2)) ∈ (-∞(,]0) → ((1 − (𝑥↑2)) ∈ ℝ ∧ -∞ < (1 − (𝑥↑2)) ∧ (1 − (𝑥↑2)) ≤ 0))
166	165	simp1d 1160	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1 − (𝑥↑2)) ∈ (-∞(,]0) → (1 − (𝑥↑2)) ∈ ℝ)
167		resubcl 11625	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1 ∈ ℝ ∧ (1 − (𝑥↑2)) ∈ ℝ) → (1 − (1 − (𝑥↑2))) ∈ ℝ)
168	89, 166, 167	sylancr 599	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 − (𝑥↑2)) ∈ (-∞(,]0) → (1 − (1 − (𝑥↑2))) ∈ ℝ)
169		nncan 11590	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1 ∈ ℂ ∧ (𝑥↑2) ∈ ℂ) → (1 − (1 − (𝑥↑2))) = (𝑥↑2))
170	16, 169	mpan 703	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥↑2) ∈ ℂ → (1 − (1 − (𝑥↑2))) = (𝑥↑2))
171	170	eleq1d 2845	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥↑2) ∈ ℂ → ((1 − (1 − (𝑥↑2))) ∈ ℝ ↔ (𝑥↑2) ∈ ℝ))
172	171	biimpa 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥↑2) ∈ ℂ ∧ (1 − (1 − (𝑥↑2))) ∈ ℝ) → (𝑥↑2) ∈ ℝ)
173	168, 172	sylan2 605	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (𝑥↑2) ∈ ℝ)
174	166	adantl 487	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (1 − (𝑥↑2)) ∈ ℝ)
175	165	simp3d 1162	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1 − (𝑥↑2)) ∈ (-∞(,]0) → (1 − (𝑥↑2)) ≤ 0)
176	175	adantl 487	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (1 − (𝑥↑2)) ≤ 0)
177		letr 11407	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((1 − (𝑥↑2)) ∈ ℝ ∧ 0 ∈ ℝ ∧ 1 ∈ ℝ) → (((1 − (𝑥↑2)) ≤ 0 ∧ 0 ≤ 1) → (1 − (𝑥↑2)) ≤ 1))
178	36, 89, 177	mp3an23 1482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1 − (𝑥↑2)) ∈ ℝ → (((1 − (𝑥↑2)) ≤ 0 ∧ 0 ≤ 1) → (1 − (𝑥↑2)) ≤ 1))
179	139, 178	mpan2i 710	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1 − (𝑥↑2)) ∈ ℝ → ((1 − (𝑥↑2)) ≤ 0 → (1 − (𝑥↑2)) ≤ 1))
180	174, 176, 179	sylc 66	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (1 − (𝑥↑2)) ≤ 1)
181		subge0 11832	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1 ∈ ℝ ∧ (1 − (𝑥↑2)) ∈ ℝ) → (0 ≤ (1 − (1 − (𝑥↑2))) ↔ (1 − (𝑥↑2)) ≤ 1))
182	89, 174, 181	sylancr 599	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (0 ≤ (1 − (1 − (𝑥↑2))) ↔ (1 − (𝑥↑2)) ≤ 1))
183	180, 182	mpbird 260	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → 0 ≤ (1 − (1 − (𝑥↑2))))
184	170	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (1 − (1 − (𝑥↑2))) = (𝑥↑2))
185	183, 184	breqtrd 5130	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → 0 ≤ (𝑥↑2))
186	173, 185	resqrtcld 15590	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (√‘(𝑥↑2)) ∈ ℝ)
187	17, 186	sylan 592	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (√‘(𝑥↑2)) ∈ ℝ)
188		eleq1 2848	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (√‘(𝑥↑2)) → (𝑥 ∈ ℝ ↔ (√‘(𝑥↑2)) ∈ ℝ))
189	187, 188	syl5ibrcom 250	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (𝑥 = (√‘(𝑥↑2)) → 𝑥 ∈ ℝ))
190	187	renegcld 11746	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → -(√‘(𝑥↑2)) ∈ ℝ)
191		eleq1 2848	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = -(√‘(𝑥↑2)) → (𝑥 ∈ ℝ ↔ -(√‘(𝑥↑2)) ∈ ℝ))
192	190, 191	syl5ibrcom 250	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (𝑥 = -(√‘(𝑥↑2)) → 𝑥 ∈ ℝ))
193		eqid 2760	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥↑2) = (𝑥↑2)
194		eqsqrtor 15539	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℂ ∧ (𝑥↑2) ∈ ℂ) → ((𝑥↑2) = (𝑥↑2) ↔ (𝑥 = (√‘(𝑥↑2)) ∨ 𝑥 = -(√‘(𝑥↑2)))))
195	17, 194	mpdan 700	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℂ → ((𝑥↑2) = (𝑥↑2) ↔ (𝑥 = (√‘(𝑥↑2)) ∨ 𝑥 = -(√‘(𝑥↑2)))))
196	193, 195	mpbii 236	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℂ → (𝑥 = (√‘(𝑥↑2)) ∨ 𝑥 = -(√‘(𝑥↑2))))
197	196	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (𝑥 = (√‘(𝑥↑2)) ∨ 𝑥 = -(√‘(𝑥↑2))))
198	189, 192, 197	mpjaod 874	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → 𝑥 ∈ ℝ)
199	198	stoic1a 1804	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℂ ∧ ¬ 𝑥 ∈ ℝ) → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
200	12, 199	sylan 592	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝐷 ∧ ¬ 𝑥 ∈ ℝ) → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
201	162, 200	pm2.61dan 825	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐷 → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
202	111, 201	eldifd 4050	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐷 → (1 − (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0)))
203	202	adantl 487	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → (1 − (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0)))
204		2cnd 12424	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℂ → 2 ∈ ℂ)
205		id 23	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℂ → 𝑥 ∈ ℂ)
206	204, 205	mulcld 11332	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℂ → (2 · 𝑥) ∈ ℂ)
207	206	negcld 11659	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℂ → -(2 · 𝑥) ∈ ℂ)
208	207	adantl 487	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → -(2 · 𝑥) ∈ ℂ)
209	12, 208	sylan2 605	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → -(2 · 𝑥) ∈ ℂ)
210	59	sqrtcld 15612	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → (√‘𝑦) ∈ ℂ)
211	210	adantl 487	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑦 ∈ (ℂ ∖ (-∞(,]0))) → (√‘𝑦) ∈ ℂ)
212		ovexd 7455	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑦 ∈ (ℂ ∖ (-∞(,]0))) → (1 / (2 · (√‘𝑦))) ∈ V)
213	19	adantl 487	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → (1 − (𝑥↑2)) ∈ ℂ)
214	36	a1i 11	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → 0 ∈ ℝ)
215		1cnd 11305	. . . . . . . . . . . . . 14 ⊢ (⊤ → 1 ∈ ℂ)
216	11, 215	dvmptc 26283	. . . . . . . . . . . . 13 ⊢ (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ 1)) = (𝑥 ∈ ℂ ↦ 0))
217	17	adantl 487	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → (𝑥↑2) ∈ ℂ)
218		2cn 12421	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℂ
219		mulcl 11287	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (2 · 𝑥) ∈ ℂ)
220	218, 219	mpan 703	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℂ → (2 · 𝑥) ∈ ℂ)
221	220	adantl 487	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → (2 · 𝑥) ∈ ℂ)
222		2nn 12419	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℕ
223		dvexp 26278	. . . . . . . . . . . . . . . 16 ⊢ (2 ∈ ℕ → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · (𝑥↑(2 − 1)))))
224	222, 223	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · (𝑥↑(2 − 1))))
225		2m1e1 12470	. . . . . . . . . . . . . . . . . . 19 ⊢ (2 − 1) = 1
226	225	oveq2i 7431	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥↑(2 − 1)) = (𝑥↑1)
227		exp1 14213	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℂ → (𝑥↑1) = 𝑥)
228	226, 227	eqtrid 2807	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℂ → (𝑥↑(2 − 1)) = 𝑥)
229	228	oveq2d 7436	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℂ → (2 · (𝑥↑(2 − 1))) = (2 · 𝑥))
230	229	mpteq2ia 5199	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℂ ↦ (2 · (𝑥↑(2 − 1)))) = (𝑥 ∈ ℂ ↦ (2 · 𝑥))
231	224, 230	eqtri 2783	. . . . . . . . . . . . . 14 ⊢ (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · 𝑥))
232	231	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · 𝑥)))
233	11, 79, 214, 216, 217, 221, 232	dvmptsub 26292	. . . . . . . . . . . 12 ⊢ (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (1 − (𝑥↑2)))) = (𝑥 ∈ ℂ ↦ (0 − (2 · 𝑥))))
234		df-neg 11547	. . . . . . . . . . . . 13 ⊢ -(2 · 𝑥) = (0 − (2 · 𝑥))
235	234	mpteq2i 5200	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℂ ↦ -(2 · 𝑥)) = (𝑥 ∈ ℂ ↦ (0 − (2 · 𝑥)))
236	233, 235	eqtr4di 2813	. . . . . . . . . . 11 ⊢ (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (1 − (𝑥↑2)))) = (𝑥 ∈ ℂ ↦ -(2 · 𝑥)))
237	11, 213, 208, 236, 81, 84, 82, 103	dvmptres 26288	. . . . . . . . . 10 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ (1 − (𝑥↑2)))) = (𝑥 ∈ 𝐷 ↦ -(2 · 𝑥)))
238		eqid 2760	. . . . . . . . . . . 12 ⊢ (ℂ ∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0))
239	238	dvcnsqrt 27077	. . . . . . . . . . 11 ⊢ (ℂ D (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (√‘𝑦))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (1 / (2 · (√‘𝑦))))
240	239	a1i 11	. . . . . . . . . 10 ⊢ (⊤ → (ℂ D (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (√‘𝑦))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (1 / (2 · (√‘𝑦)))))
241		fveq2 6885	. . . . . . . . . 10 ⊢ (𝑦 = (1 − (𝑥↑2)) → (√‘𝑦) = (√‘(1 − (𝑥↑2))))
242	241	oveq2d 7436	. . . . . . . . . . 11 ⊢ (𝑦 = (1 − (𝑥↑2)) → (2 · (√‘𝑦)) = (2 · (√‘(1 − (𝑥↑2)))))
243	242	oveq2d 7436	. . . . . . . . . 10 ⊢ (𝑦 = (1 − (𝑥↑2)) → (1 / (2 · (√‘𝑦))) = (1 / (2 · (√‘(1 − (𝑥↑2))))))
244	11, 11, 203, 209, 211, 212, 237, 240, 241, 243	dvmptco 26297	. . . . . . . . 9 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ (√‘(1 − (𝑥↑2))))) = (𝑥 ∈ 𝐷 ↦ ((1 / (2 · (√‘(1 − (𝑥↑2))))) · -(2 · 𝑥))))
245		mulneg2 11756	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (2 · -𝑥) = -(2 · 𝑥))
246	218, 12, 245	sylancr 599	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐷 → (2 · -𝑥) = -(2 · 𝑥))
247	246	oveq1d 7435	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐷 → ((2 · -𝑥) / (2 · (√‘(1 − (𝑥↑2))))) = ( -(2 · 𝑥) / (2 · (√‘(1 − (𝑥↑2))))))
248	12	negcld 11659	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐷 → -𝑥 ∈ ℂ)
249		eldifn 4068	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (ℂ ∖ ((-∞(,] -1) ∪ (1[,)+∞))) → ¬ 𝑥 ∈ ((-∞(,] -1) ∪ (1[,)+∞)))
250	249, 3	eleq2s 2878	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐷 → ¬ 𝑥 ∈ ((-∞(,] -1) ∪ (1[,)+∞)))
251		id 23	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = -1 → 𝑥 = -1)
252		mnflt 13255	. . . . . . . . . . . . . . . . . . . 20 ⊢ ( -1 ∈ ℝ → -∞ < -1)
253	86, 252	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ -∞ < -1
254		ubioc1 13533	. . . . . . . . . . . . . . . . . . 19 ⊢ ((-∞ ∈ ℝ^* ∧ -1 ∈ ℝ^* ∧ -∞ < -1) → -1 ∈ (-∞(,] -1))
255	51, 132, 253, 254	mp3an 1490	. . . . . . . . . . . . . . . . . 18 ⊢ -1 ∈ (-∞(,] -1)
256	251, 255	eqeltrdi 2868	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = -1 → 𝑥 ∈ (-∞(,] -1))
257		id 23	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 1 → 𝑥 = 1)
258		ltpnf 13252	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 ∈ ℝ → 1 < +∞)
259	89, 258	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 < +∞
260		lbico1 13534	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ ℝ^* ∧ +∞ ∈ ℝ^* ∧ 1 < +∞) → 1 ∈ (1[,)+∞))
261	133, 121, 259, 260	mp3an 1490	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ (1[,)+∞)
262	257, 261	eqeltrdi 2868	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 1 → 𝑥 ∈ (1[,)+∞))
263	256, 262	orim12i 922	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = -1 ∨ 𝑥 = 1) → (𝑥 ∈ (-∞(,] -1) ∨ 𝑥 ∈ (1[,)+∞)))
264	263	orcoms 886	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = 1 ∨ 𝑥 = -1) → (𝑥 ∈ (-∞(,] -1) ∨ 𝑥 ∈ (1[,)+∞)))
265		elun 4152	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ((-∞(,] -1) ∪ (1[,)+∞)) ↔ (𝑥 ∈ (-∞(,] -1) ∨ 𝑥 ∈ (1[,)+∞)))
266	264, 265	sylibr 237	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 1 ∨ 𝑥 = -1) → 𝑥 ∈ ((-∞(,] -1) ∪ (1[,)+∞)))
267	250, 266	nsyl 141	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐷 → ¬ (𝑥 = 1 ∨ 𝑥 = -1))
268		1cnd 11305	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → 1 ∈ ℂ)
269	17	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → (𝑥↑2) ∈ ℂ)
270	19	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → (1 − (𝑥↑2)) ∈ ℂ)
271		simpr 490	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → (√‘(1 − (𝑥↑2))) = 0)
272	270, 271	sqr00d 15616	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → (1 − (𝑥↑2)) = 0)
273	268, 269, 272	subeq0d 11681	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → 1 = (𝑥↑2))
274	146, 273	eqtr2id 2808	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → (𝑥↑2) = (1↑2))
275	274	ex 418	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℂ → ((√‘(1 − (𝑥↑2))) = 0 → (𝑥↑2) = (1↑2)))
276		sqeqor 14363	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑥↑2) = (1↑2) ↔ (𝑥 = 1 ∨ 𝑥 = -1)))
277	16, 276	mpan2 704	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℂ → ((𝑥↑2) = (1↑2) ↔ (𝑥 = 1 ∨ 𝑥 = -1)))
278	275, 277	sylibd 242	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℂ → ((√‘(1 − (𝑥↑2))) = 0 → (𝑥 = 1 ∨ 𝑥 = -1)))
279	278	necon3bd 2969	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℂ → (¬ (𝑥 = 1 ∨ 𝑥 = -1) → (√‘(1 − (𝑥↑2))) ≠ 0))
280	12, 267, 279	sylc 66	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐷 → (√‘(1 − (𝑥↑2))) ≠ 0)
281		2cnne0 12558	. . . . . . . . . . . . 13 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
282		divcan5 12022	. . . . . . . . . . . . 13 ⊢ (( -𝑥 ∈ ℂ ∧ ((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · -𝑥) / (2 · (√‘(1 − (𝑥↑2))))) = ( -𝑥 / (√‘(1 − (𝑥↑2)))))
283	281, 282	mp3an3 1479	. . . . . . . . . . . 12 ⊢ (( -𝑥 ∈ ℂ ∧ ((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0)) → ((2 · -𝑥) / (2 · (√‘(1 − (𝑥↑2))))) = ( -𝑥 / (√‘(1 − (𝑥↑2)))))
284	248, 112, 280, 283	syl12anc 850	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐷 → ((2 · -𝑥) / (2 · (√‘(1 − (𝑥↑2))))) = ( -𝑥 / (√‘(1 − (𝑥↑2)))))
285	218, 12, 219	sylancr 599	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐷 → (2 · 𝑥) ∈ ℂ)
286	285	negcld 11659	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐷 → -(2 · 𝑥) ∈ ℂ)
287		mulcl 11287	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ∈ ℂ) → (2 · (√‘(1 − (𝑥↑2)))) ∈ ℂ)
288	218, 112, 287	sylancr 599	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐷 → (2 · (√‘(1 − (𝑥↑2)))) ∈ ℂ)
289		mulne0 11961	. . . . . . . . . . . . . 14 ⊢ (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ ((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0)) → (2 · (√‘(1 − (𝑥↑2)))) ≠ 0)
290	281, 289	mpan 703	. . . . . . . . . . . . 13 ⊢ (((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0) → (2 · (√‘(1 − (𝑥↑2)))) ≠ 0)
291	112, 280, 290	syl2anc 596	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐷 → (2 · (√‘(1 − (𝑥↑2)))) ≠ 0)
292	286, 288, 291	divrec2d 12100	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐷 → ( -(2 · 𝑥) / (2 · (√‘(1 − (𝑥↑2))))) = ((1 / (2 · (√‘(1 − (𝑥↑2))))) · -(2 · 𝑥)))
293	247, 284, 292	3eqtr3rd 2804	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐷 → ((1 / (2 · (√‘(1 − (𝑥↑2))))) · -(2 · 𝑥)) = ( -𝑥 / (√‘(1 − (𝑥↑2)))))
294	293	mpteq2ia 5199	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 ↦ ((1 / (2 · (√‘(1 − (𝑥↑2))))) · -(2 · 𝑥))) = (𝑥 ∈ 𝐷 ↦ ( -𝑥 / (√‘(1 − (𝑥↑2)))))
295	244, 294	eqtrdi 2811	. . . . . . . 8 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ (√‘(1 − (𝑥↑2))))) = (𝑥 ∈ 𝐷 ↦ ( -𝑥 / (√‘(1 − (𝑥↑2))))))
296	11, 74, 75, 109, 113, 114, 295	dvmptadd 26285	. . . . . . 7 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))) = (𝑥 ∈ 𝐷 ↦ (i + ( -𝑥 / (√‘(1 − (𝑥↑2)))))))
297		mulcl 11287	. . . . . . . . . . . 12 ⊢ ((i ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ∈ ℂ) → (i · (√‘(1 − (𝑥↑2)))) ∈ ℂ)
298	13, 20, 297	sylancr 599	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℂ → (i · (√‘(1 − (𝑥↑2)))) ∈ ℂ)
299	12, 298	syl 18	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐷 → (i · (√‘(1 − (𝑥↑2)))) ∈ ℂ)
300	299, 248, 112, 280	divdird 12134	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → (((i · (√‘(1 − (𝑥↑2)))) + -𝑥) / (√‘(1 − (𝑥↑2)))) = (((i · (√‘(1 − (𝑥↑2)))) / (√‘(1 − (𝑥↑2)))) + ( -𝑥 / (√‘(1 − (𝑥↑2))))))
301		ixi 11948	. . . . . . . . . . . . . . . 16 ⊢ (i · i) = -1
302	301	eqcomi 2769	. . . . . . . . . . . . . . 15 ⊢ -1 = (i · i)
303	302	oveq1i 7430	. . . . . . . . . . . . . 14 ⊢ ( -1 · 𝑥) = ((i · i) · 𝑥)
304		mulm1 11760	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℂ → ( -1 · 𝑥) = -𝑥)
305		mulass 11291	. . . . . . . . . . . . . . 15 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ ∧ 𝑥 ∈ ℂ) → ((i · i) · 𝑥) = (i · (i · 𝑥)))
306	13, 13, 305	mp3an12 1480	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℂ → ((i · i) · 𝑥) = (i · (i · 𝑥)))
307	303, 304, 306	3eqtr3a 2819	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℂ → -𝑥 = (i · (i · 𝑥)))
308	307	oveq1d 7435	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℂ → ( -𝑥 + (i · (√‘(1 − (𝑥↑2))))) = ((i · (i · 𝑥)) + (i · (√‘(1 − (𝑥↑2))))))
309		negcl 11560	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℂ → -𝑥 ∈ ℂ)
310	298, 309	addcomd 11515	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℂ → ((i · (√‘(1 − (𝑥↑2)))) + -𝑥) = ( -𝑥 + (i · (√‘(1 − (𝑥↑2))))))
311	13	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℂ → i ∈ ℂ)
312	311, 15, 20	adddid 11336	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℂ → (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) = ((i · (i · 𝑥)) + (i · (√‘(1 − (𝑥↑2))))))
313	308, 310, 312	3eqtr4d 2805	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℂ → ((i · (√‘(1 − (𝑥↑2)))) + -𝑥) = (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
314	12, 313	syl 18	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐷 → ((i · (√‘(1 − (𝑥↑2)))) + -𝑥) = (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
315	314	oveq1d 7435	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → (((i · (√‘(1 − (𝑥↑2)))) + -𝑥) / (√‘(1 − (𝑥↑2)))) = ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))))
316	72, 112, 280	divcan4d 12102	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐷 → ((i · (√‘(1 − (𝑥↑2)))) / (√‘(1 − (𝑥↑2)))) = i)
317	316	oveq1d 7435	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → (((i · (√‘(1 − (𝑥↑2)))) / (√‘(1 − (𝑥↑2)))) + ( -𝑥 / (√‘(1 − (𝑥↑2))))) = (i + ( -𝑥 / (√‘(1 − (𝑥↑2))))))
318	300, 315, 317	3eqtr3rd 2804	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐷 → (i + ( -𝑥 / (√‘(1 − (𝑥↑2))))) = ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))))
319	318	mpteq2ia 5199	. . . . . . 7 ⊢ (𝑥 ∈ 𝐷 ↦ (i + ( -𝑥 / (√‘(1 − (𝑥↑2)))))) = (𝑥 ∈ 𝐷 ↦ ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))))
320	296, 319	eqtrdi 2811	. . . . . 6 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))) = (𝑥 ∈ 𝐷 ↦ ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2))))))
321		logf1o 26897	. . . . . . . . . 10 ⊢ log:(ℂ ∖ {0})–1-1-onto→ran log
322		f1of 6824	. . . . . . . . . 10 ⊢ (log:(ℂ ∖ {0})–1-1-onto→ran log → log:(ℂ ∖ {0})⟶ran log)
323	321, 322	mp1i 14	. . . . . . . . 9 ⊢ (⊤ → log:(ℂ ∖ {0})⟶ran log)
324		snssi 4742	. . . . . . . . . . 11 ⊢ (0 ∈ (-∞(,]0) → {0} ⊆ (-∞(,]0))
325	64, 324	ax-mp 5	. . . . . . . . . 10 ⊢ {0} ⊆ (-∞(,]0)
326		sscon 4079	. . . . . . . . . 10 ⊢ ({0} ⊆ (-∞(,]0) → (ℂ ∖ (-∞(,]0)) ⊆ (ℂ ∖ {0}))
327	325, 326	mp1i 14	. . . . . . . . 9 ⊢ (⊤ → (ℂ ∖ (-∞(,]0)) ⊆ (ℂ ∖ {0}))
328	323, 327	feqresmpt 6954	. . . . . . . 8 ⊢ (⊤ → (log ↾ (ℂ ∖ (-∞(,]0))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (log‘𝑦)))
329	328	oveq2d 7436	. . . . . . 7 ⊢ (⊤ → (ℂ D (log ↾ (ℂ ∖ (-∞(,]0)))) = (ℂ D (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (log‘𝑦))))
330	238	dvlog 26984	. . . . . . 7 ⊢ (ℂ D (log ↾ (ℂ ∖ (-∞(,]0)))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (1 / 𝑦))
331	329, 330	eqtr3di 2810	. . . . . 6 ⊢ (⊤ → (ℂ D (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (log‘𝑦))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (1 / 𝑦)))
332		fveq2 6885	. . . . . 6 ⊢ (𝑦 = ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) → (log‘𝑦) = (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
333		oveq2 7428	. . . . . 6 ⊢ (𝑦 = ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) → (1 / 𝑦) = (1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
334	11, 11, 57, 58, 70, 71, 320, 331, 332, 333	dvmptco 26297	. . . . 5 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))) = (𝑥 ∈ 𝐷 ↦ ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))))))
335	22, 24	reccld 12089	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐷 → (1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
336		mulcl 11287	. . . . . . . . . 10 ⊢ ((i ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℂ) → (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
337	13, 21, 336	sylancr 599	. . . . . . . . 9 ⊢ (𝑥 ∈ ℂ → (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
338	12, 337	syl 18	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐷 → (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
339	335, 338, 112, 280	divassd 12131	. . . . . . 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 12100	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) = ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))
341	72, 22, 24	divcan4d 12102	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) = i)
342	340, 341	eqtr3d 2797	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐷 → ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))) = i)
343	342	oveq1d 7435	. . . . . . 7 ⊢ (𝑥 ∈ 𝐷 → (((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))) / (√‘(1 − (𝑥↑2)))) = (i / (√‘(1 − (𝑥↑2)))))
344	339, 343	eqtr3d 2797	. . . . . 6 ⊢ (𝑥 ∈ 𝐷 → ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2))))) = (i / (√‘(1 − (𝑥↑2)))))
345	344	mpteq2ia 5199	. . . . 5 ⊢ (𝑥 ∈ 𝐷 ↦ ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))))) = (𝑥 ∈ 𝐷 ↦ (i / (√‘(1 − (𝑥↑2)))))
346	334, 345	eqtrdi 2811	. . . 4 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))) = (𝑥 ∈ 𝐷 ↦ (i / (√‘(1 − (𝑥↑2))))))
347		negicn 11561	. . . . 5 ⊢ -i ∈ ℂ
348	347	a1i 11	. . . 4 ⊢ (⊤ → -i ∈ ℂ)
349	11, 26, 27, 346, 348	dvmptcmul 26289	. . 3 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ ( -i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))) = (𝑥 ∈ 𝐷 ↦ ( -i · (i / (√‘(1 − (𝑥↑2)))))))
350	349	mptru 1576	. 2 ⊢ (ℂ D (𝑥 ∈ 𝐷 ↦ ( -i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))) = (𝑥 ∈ 𝐷 ↦ ( -i · (i / (√‘(1 − (𝑥↑2))))))
351		divass 11995	. . . . . 6 ⊢ (( -i ∈ ℂ ∧ i ∈ ℂ ∧ ((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0)) → (( -i · i) / (√‘(1 − (𝑥↑2)))) = ( -i · (i / (√‘(1 − (𝑥↑2))))))
352	347, 13, 351	mp3an12 1480	. . . . 5 ⊢ (((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0) → (( -i · i) / (√‘(1 − (𝑥↑2)))) = ( -i · (i / (√‘(1 − (𝑥↑2))))))
353	112, 280, 352	syl2anc 596	. . . 4 ⊢ (𝑥 ∈ 𝐷 → (( -i · i) / (√‘(1 − (𝑥↑2)))) = ( -i · (i / (√‘(1 − (𝑥↑2))))))
354	13, 13	mulneg1i 11765	. . . . . 6 ⊢ ( -i · i) = -(i · i)
355	301	negeqi 11553	. . . . . 6 ⊢ -(i · i) = - -1
356		negneg1e1 12312	. . . . . 6 ⊢ - -1 = 1
357	354, 355, 356	3eqtri 2787	. . . . 5 ⊢ ( -i · i) = 1
358	357	oveq1i 7430	. . . 4 ⊢ (( -i · i) / (√‘(1 − (𝑥↑2)))) = (1 / (√‘(1 − (𝑥↑2))))
359	353, 358	eqtr3di 2810	. . 3 ⊢ (𝑥 ∈ 𝐷 → ( -i · (i / (√‘(1 − (𝑥↑2))))) = (1 / (√‘(1 − (𝑥↑2)))))
360	359	mpteq2ia 5199	. 2 ⊢ (𝑥 ∈ 𝐷 ↦ ( -i · (i / (√‘(1 − (𝑥↑2)))))) = (𝑥 ∈ 𝐷 ↦ (1 / (√‘(1 − (𝑥↑2)))))
361	9, 350, 360	3eqtri 2787	1 ⊢ (ℂ D (arcsin ↾ 𝐷)) = (𝑥 ∈ 𝐷 ↦ (1 / (√‘(1 − (𝑥↑2)))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∨ w3o 1102 ∧ w3a 1103 = wceq 1569 ⊤wtru 1570 ∈ wcel 2144 ≠ wne 2955 Vcvv 3450 ⊆ wss 3895 ∖ cdif 4045 ∩ cin 4089 ∪ cun 4149 ∅c0 4278 {csn 4584 {cpr 4586 class class class wbr 5102 ↦ cmpt 5185 ran crn 5651 ↾ cres 5652 ⟶wf 6534 –1-1-onto→wf1o 6537 ‘cfv 6538 (class class class)co 7420 ℂcc 11201 ℝcr 11202 0cc0 11203 1c1 11204 ici 11205 + caddc 11206 · cmul 11208 +∞cpnf 11343 -∞cmnf 11344 ℝ^*cxr 11345 < clt 11346 ≤ cle 11347 − cmin 11544 -cneg 11545 / cdiv 11976 ℕcn 12338 2c2 12400 ℝ⁺crp 13123 (,)cioo 13479 (,]cioc 13480 [,)cico 13481 ↑cexp 14207 ℜcre 15269 √csqrt 15405 abscabs 15406 ↾_t crest 17596 TopOpenctopn 17597 topGenctg 17613 ℂ_fldccnfld 21683 Clsdccld 23339 D cdv 26188 logclog 26887 arcsincasin 27195

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751 ax-inf2 9645 ax-cnex 11259 ax-resscn 11260 ax-1cn 11261 ax-icn 11262 ax-addcl 11263 ax-addrcl 11264 ax-mulcl 11265 ax-mulrcl 11266 ax-mulcom 11267 ax-addass 11268 ax-mulass 11269 ax-distr 11270 ax-i2m1 11271 ax-1ne0 11272 ax-1rid 11273 ax-rnegex 11274 ax-rrecex 11275 ax-cnre 11276 ax-pre-lttri 11277 ax-pre-lttrn 11278 ax-pre-ltadd 11279 ax-pre-mulgt0 11280 ax-pre-sup 11281 ax-addf 11282

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4835 df-uni 4867 df-int 4907 df-iun 4952 df-iin 4953 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-se 5604 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-isom 6547 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-of 7693 df-om 7878 df-1st 8001 df-2nd 8002 df-supp 8180 df-frecs 8302 df-wrecs 8333 df-recs 8382 df-rdg 8421 df-1o 8479 df-2o 8480 df-er 8720 df-map 8852 df-pm 8853 df-ixp 8929 df-en 8977 df-dom 8978 df-sdom 8979 df-fin 8980 df-fsupp 9357 df-fi 9406 df-sup 9437 df-inf 9438 df-oi 9507 df-card 10023 df-pnf 11348 df-mnf 11349 df-xr 11350 df-ltxr 11351 df-le 11352 df-sub 11546 df-neg 11547 df-div 11977 df-nn 12339 df-2 12408 df-3 12409 df-4 12410 df-5 12411 df-6 12412 df-7 12413 df-8 12414 df-9 12415 df-n0 12610 df-z 12697 df-dec 12818 df-uz 12969 df-q 13079 df-rp 13124 df-xneg 13244 df-xadd 13245 df-xmul 13246 df-ioo 13483 df-ioc 13484 df-ico 13485 df-icc 13486 df-fz 13643 df-fzo 13792 df-fl 13935 df-mod 14013 df-seq 14148 df-exp 14208 df-fac 14421 df-bc 14450 df-hash 14478 df-shft 15225 df-cj 15271 df-re 15272 df-im 15273 df-sqrt 15407 df-abs 15408 df-limsup 15643 df-clim 15660 df-rlim 15661 df-sum 15859 df-ef 16238 df-sin 16240 df-cos 16241 df-tan 16242 df-pi 16243 df-struct 17330 df-sets 17347 df-slot 17365 df-ndx 17377 df-base 17393 df-ress 17414 df-plusg 17446 df-mulr 17447 df-starv 17448 df-sca 17449 df-vsca 17450 df-ip 17451 df-tset 17452 df-ple 17453 df-ds 17455 df-unif 17456 df-hom 17457 df-cco 17458 df-rest 17598 df-topn 17599 df-0g 17617 df-gsum 17618 df-topgen 17619 df-pt 17620 df-prds 17623 df-xrs 17679 df-qtop 17684 df-imas 17685 df-xps 17687 df-mre 17761 df-mrc 17762 df-acs 17764 df-mgm 18821 df-sgrp 18913 df-mnd 18929 df-submnd 18984 df-mulg 19283 df-cntz 19536 df-cmn 20001 df-psmet 21675 df-xmet 21676 df-met 21677 df-bl 21678 df-mopn 21679 df-fbas 21680 df-fg 21681 df-cnfld 21684 df-top 23217 df-topon 23234 df-topsp 23256 df-bases 23269 df-cld 23342 df-ntr 23343 df-cls 23344 df-nei 23421 df-lp 23459 df-perf 23460 df-cn 23550 df-cnp 23551 df-haus 23638 df-cmp 23710 df-tx 23886 df-hmeo 24079 df-fil 24170 df-fm 24262 df-flim 24263 df-flf 24264 df-xms 24644 df-ms 24645 df-tms 24646 df-cncf 25204 df-limc 26191 df-dv 26192 df-log 26889 df-cxp 26890 df-asin 27198

This theorem is used by: dvacos 38716 dvreasin 38717

W3C validator