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 32462

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 24309	. . . . 5 ⊢ arcsin = (𝑥 ∈ ℂ ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))
2	1	reseq1i 5300	. . . 4 ⊢ (arcsin ↾ 𝐷) = ((𝑥 ∈ ℂ ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))) ↾ 𝐷)
3		dvasin.d	. . . . . 6 ⊢ 𝐷 = (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞)))
4		difss 3698	. . . . . 6 ⊢ (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞))) ⊆ ℂ
5	3, 4	eqsstri 3597	. . . . 5 ⊢ 𝐷 ⊆ ℂ
6		resmpt 5356	. . . . 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 2631	. . 3 ⊢ (arcsin ↾ 𝐷) = (𝑥 ∈ 𝐷 ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))
9	8	oveq2i 6538	. 2 ⊢ (ℂ D (arcsin ↾ 𝐷)) = (ℂ D (𝑥 ∈ 𝐷 ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))))
10		cnelprrecn 9885	. . . . 5 ⊢ ℂ ∈ {ℝ, ℂ}
11	10	a1i 11	. . . 4 ⊢ (⊤ → ℂ ∈ {ℝ, ℂ})
12	5	sseli 3563	. . . . . . 7 ⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ ℂ)
13		ax-icn 9851	. . . . . . . . 9 ⊢ i ∈ ℂ
14		mulcl 9876	. . . . . . . . 9 ⊢ ((i ∈ ℂ ∧ 𝑥 ∈ ℂ) → (i · 𝑥) ∈ ℂ)
15	13, 14	mpan 701	. . . . . . . 8 ⊢ (𝑥 ∈ ℂ → (i · 𝑥) ∈ ℂ)
16		ax-1cn 9850	. . . . . . . . . 10 ⊢ 1 ∈ ℂ
17		sqcl 12742	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℂ → (𝑥↑2) ∈ ℂ)
18		subcl 10131	. . . . . . . . . 10 ⊢ ((1 ∈ ℂ ∧ (𝑥↑2) ∈ ℂ) → (1 − (𝑥↑2)) ∈ ℂ)
19	16, 17, 18	sylancr 693	. . . . . . . . 9 ⊢ (𝑥 ∈ ℂ → (1 − (𝑥↑2)) ∈ ℂ)
20	19	sqrtcld 13970	. . . . . . . 8 ⊢ (𝑥 ∈ ℂ → (√‘(1 − (𝑥↑2))) ∈ ℂ)
21	15, 20	addcld 9915	. . . . . . 7 ⊢ (𝑥 ∈ ℂ → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℂ)
22	12, 21	syl 17	. . . . . 6 ⊢ (𝑥 ∈ 𝐷 → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℂ)
23		asinlem 24312	. . . . . . 7 ⊢ (𝑥 ∈ ℂ → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≠ 0)
24	12, 23	syl 17	. . . . . 6 ⊢ (𝑥 ∈ 𝐷 → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≠ 0)
25	22, 24	logcld 24038	. . . . 5 ⊢ (𝑥 ∈ 𝐷 → (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
26	25	adantl 480	. . . 4 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
27		ovex 6555	. . . . 5 ⊢ (i / (√‘(1 − (𝑥↑2)))) ∈ V
28	27	a1i 11	. . . 4 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → (i / (√‘(1 − (𝑥↑2)))) ∈ V)
29		simpr 475	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ)
30		asinlem3 24315	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℂ → 0 ≤ (ℜ‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
31		rere 13656	. . . . . . . . . . . . . . . . . . 19 ⊢ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → (ℜ‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) = ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))
32	31	breq2d 4589	. . . . . . . . . . . . . . . . . 18 ⊢ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → (0 ≤ (ℜ‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ↔ 0 ≤ ((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
33	32	biimpac 501	. . . . . . . . . . . . . . . . 17 ⊢ ((0 ≤ (ℜ‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → 0 ≤ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))
34	30, 33	sylan 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → 0 ≤ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))
35	23	adantr 479	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≠ 0)
36	29, 34, 35	ne0gt0d 10025	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → 0 < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))
37		0re 9896	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ ℝ
38		ltnle 9968	. . . . . . . . . . . . . . . . 17 ⊢ ((0 ∈ ℝ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → (0 < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ↔ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
39	37, 38	mpan 701	. . . . . . . . . . . . . . . 16 ⊢ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → (0 < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ↔ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
40	39	adantl 480	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → (0 < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ↔ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
41	36, 40	mpbid 220	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) → ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0)
42	41	ex 448	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℂ → (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
43	12, 42	syl 17	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐷 → (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
44		imor 426	. . . . . . . . . . . 12 ⊢ ((((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ → ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0) ↔ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
45	43, 44	sylib 206	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐷 → (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
46	45	orcomd 401	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐷 → (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ))
47	46	olcd 406	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → (¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ)))
48		3ianor 1047	. . . . . . . . . . 11 ⊢ (¬ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∧ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0) ↔ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∨ ¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
49		3orrot 1036	. . . . . . . . . . 11 ⊢ ((¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∨ ¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0) ↔ (¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ))
50		3orass 1033	. . . . . . . . . . 11 ⊢ ((¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ) ↔ (¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ)))
51	48, 49, 50	3bitrri 285	. . . . . . . . . 10 ⊢ ((¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ)) ↔ ¬ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∧ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
52		mnfxr 11783	. . . . . . . . . . 11 ⊢ -∞ ∈ ℝ^*
53		elioc2 12063	. . . . . . . . . . 11 ⊢ ((-∞ ∈ ℝ^* ∧ 0 ∈ ℝ) → (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (-∞(,]0) ↔ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∧ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0)))
54	52, 37, 53	mp2an 703	. . . . . . . . . 10 ⊢ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (-∞(,]0) ↔ (((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ ∧ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0))
55	51, 54	xchbinxr 323	. . . . . . . . 9 ⊢ ((¬ -∞ < ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∨ (¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ≤ 0 ∨ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℝ)) ↔ ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (-∞(,]0))
56	47, 55	sylib 206	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐷 → ¬ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (-∞(,]0))
57	22, 56	eldifd 3550	. . . . . . 7 ⊢ (𝑥 ∈ 𝐷 → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (ℂ ∖ (-∞(,]0)))
58	57	adantl 480	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ (ℂ ∖ (-∞(,]0)))
59		ovex 6555	. . . . . . 7 ⊢ ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))) ∈ V
60	59	a1i 11	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))) ∈ V)
61		eldifi 3693	. . . . . . . 8 ⊢ (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → 𝑦 ∈ ℂ)
62		eldifn 3694	. . . . . . . . 9 ⊢ (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → ¬ 𝑦 ∈ (-∞(,]0))
63		0xr 9942	. . . . . . . . . . . 12 ⊢ 0 ∈ ℝ^*
64		mnflt0 11796	. . . . . . . . . . . 12 ⊢ -∞ < 0
65		ubioc1 12054	. . . . . . . . . . . 12 ⊢ ((-∞ ∈ ℝ^* ∧ 0 ∈ ℝ^* ∧ -∞ < 0) → 0 ∈ (-∞(,]0))
66	52, 63, 64, 65	mp3an 1415	. . . . . . . . . . 11 ⊢ 0 ∈ (-∞(,]0)
67		eleq1 2675	. . . . . . . . . . 11 ⊢ (𝑦 = 0 → (𝑦 ∈ (-∞(,]0) ↔ 0 ∈ (-∞(,]0)))
68	66, 67	mpbiri 246	. . . . . . . . . 10 ⊢ (𝑦 = 0 → 𝑦 ∈ (-∞(,]0))
69	68	necon3bi 2807	. . . . . . . . 9 ⊢ (¬ 𝑦 ∈ (-∞(,]0) → 𝑦 ≠ 0)
70	62, 69	syl 17	. . . . . . . 8 ⊢ (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → 𝑦 ≠ 0)
71	61, 70	logcld 24038	. . . . . . 7 ⊢ (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → (log‘𝑦) ∈ ℂ)
72	71	adantl 480	. . . . . 6 ⊢ ((⊤ ∧ 𝑦 ∈ (ℂ ∖ (-∞(,]0))) → (log‘𝑦) ∈ ℂ)
73		ovex 6555	. . . . . . 7 ⊢ (1 / 𝑦) ∈ V
74	73	a1i 11	. . . . . 6 ⊢ ((⊤ ∧ 𝑦 ∈ (ℂ ∖ (-∞(,]0))) → (1 / 𝑦) ∈ V)
75	13	a1i 11	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐷 → i ∈ ℂ)
76	75, 12	mulcld 9916	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → (i · 𝑥) ∈ ℂ)
77	76	adantl 480	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → (i · 𝑥) ∈ ℂ)
78	13	a1i 11	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → i ∈ ℂ)
79	12	adantl 480	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ ℂ)
80		1cnd 9912	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → 1 ∈ ℂ)
81		simpr 475	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → 𝑥 ∈ ℂ)
82		1cnd 9912	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → 1 ∈ ℂ)
83	11	dvmptid 23443	. . . . . . . . . . 11 ⊢ (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ 𝑥)) = (𝑥 ∈ ℂ ↦ 1))
84	5	a1i 11	. . . . . . . . . . 11 ⊢ (⊤ → 𝐷 ⊆ ℂ)
85		eqid 2609	. . . . . . . . . . . . . 14 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
86	85	cnfldtopon 22328	. . . . . . . . . . . . 13 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
87	86	toponunii 20489	. . . . . . . . . . . . . 14 ⊢ ℂ = ∪ (TopOpen‘ℂ_fld)
88	87	restid 15863	. . . . . . . . . . . . 13 ⊢ ((TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ) → ((TopOpen‘ℂ_fld) ↾_t ℂ) = (TopOpen‘ℂ_fld))
89	86, 88	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((TopOpen‘ℂ_fld) ↾_t ℂ) = (TopOpen‘ℂ_fld)
90	89	eqcomi 2618	. . . . . . . . . . 11 ⊢ (TopOpen‘ℂ_fld) = ((TopOpen‘ℂ_fld) ↾_t ℂ)
91	85	recld2 22357	. . . . . . . . . . . . . . 15 ⊢ ℝ ∈ (Clsd‘(TopOpen‘ℂ_fld))
92		neg1rr 10972	. . . . . . . . . . . . . . . . . 18 ⊢ -1 ∈ ℝ
93		iocmnfcld 22314	. . . . . . . . . . . . . . . . . 18 ⊢ (-1 ∈ ℝ → (-∞(,]-1) ∈ (Clsd‘(topGen‘ran (,))))
94	92, 93	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (-∞(,]-1) ∈ (Clsd‘(topGen‘ran (,)))
95		1re 9895	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℝ
96		icopnfcld 22313	. . . . . . . . . . . . . . . . . 18 ⊢ (1 ∈ ℝ → (1[,)+∞) ∈ (Clsd‘(topGen‘ran (,))))
97	95, 96	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (1[,)+∞) ∈ (Clsd‘(topGen‘ran (,)))
98		uncld 20597	. . . . . . . . . . . . . . . . 17 ⊢ (((-∞(,]-1) ∈ (Clsd‘(topGen‘ran (,))) ∧ (1[,)+∞) ∈ (Clsd‘(topGen‘ran (,)))) → ((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘(topGen‘ran (,))))
99	94, 97, 98	mp2an 703	. . . . . . . . . . . . . . . 16 ⊢ ((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘(topGen‘ran (,)))
100	85	tgioo2 22346	. . . . . . . . . . . . . . . . 17 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
101	100	fveq2i 6091	. . . . . . . . . . . . . . . 16 ⊢ (Clsd‘(topGen‘ran (,))) = (Clsd‘((TopOpen‘ℂ_fld) ↾_t ℝ))
102	99, 101	eleqtri 2685	. . . . . . . . . . . . . . 15 ⊢ ((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘((TopOpen‘ℂ_fld) ↾_t ℝ))
103		restcldr 20730	. . . . . . . . . . . . . . 15 ⊢ ((ℝ ∈ (Clsd‘(TopOpen‘ℂ_fld)) ∧ ((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘((TopOpen‘ℂ_fld) ↾_t ℝ))) → ((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘(TopOpen‘ℂ_fld)))
104	91, 102, 103	mp2an 703	. . . . . . . . . . . . . 14 ⊢ ((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘(TopOpen‘ℂ_fld))
105	87	cldopn 20587	. . . . . . . . . . . . . 14 ⊢ (((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘(TopOpen‘ℂ_fld)) → (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞))) ∈ (TopOpen‘ℂ_fld))
106	104, 105	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞))) ∈ (TopOpen‘ℂ_fld)
107	3, 106	eqeltri 2683	. . . . . . . . . . . 12 ⊢ 𝐷 ∈ (TopOpen‘ℂ_fld)
108	107	a1i 11	. . . . . . . . . . 11 ⊢ (⊤ → 𝐷 ∈ (TopOpen‘ℂ_fld))
109	11, 81, 82, 83, 84, 90, 85, 108	dvmptres 23449	. . . . . . . . . 10 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ 𝑥)) = (𝑥 ∈ 𝐷 ↦ 1))
110	13	a1i 11	. . . . . . . . . 10 ⊢ (⊤ → i ∈ ℂ)
111	11, 79, 80, 109, 110	dvmptcmul 23450	. . . . . . . . 9 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ (i · 𝑥))) = (𝑥 ∈ 𝐷 ↦ (i · 1)))
112	13	mulid1i 9898	. . . . . . . . . 10 ⊢ (i · 1) = i
113	112	mpteq2i 4663	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 ↦ (i · 1)) = (𝑥 ∈ 𝐷 ↦ i)
114	111, 113	syl6eq 2659	. . . . . . . 8 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ (i · 𝑥))) = (𝑥 ∈ 𝐷 ↦ i))
115	12	sqcld 12823	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐷 → (𝑥↑2) ∈ ℂ)
116	16, 115, 18	sylancr 693	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐷 → (1 − (𝑥↑2)) ∈ ℂ)
117	116	sqrtcld 13970	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → (√‘(1 − (𝑥↑2))) ∈ ℂ)
118	117	adantl 480	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → (√‘(1 − (𝑥↑2))) ∈ ℂ)
119		ovex 6555	. . . . . . . . 9 ⊢ (-𝑥 / (√‘(1 − (𝑥↑2)))) ∈ V
120	119	a1i 11	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → (-𝑥 / (√‘(1 − (𝑥↑2)))) ∈ V)
121		elin 3757	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐷 ∩ ℝ) ↔ (𝑥 ∈ 𝐷 ∧ 𝑥 ∈ ℝ))
122	3	asindmre 32461	. . . . . . . . . . . . . . . . 17 ⊢ (𝐷 ∩ ℝ) = (-1(,)1)
123	122	eqimssi 3621	. . . . . . . . . . . . . . . 16 ⊢ (𝐷 ∩ ℝ) ⊆ (-1(,)1)
124	123	sseli 3563	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐷 ∩ ℝ) → 𝑥 ∈ (-1(,)1))
125	121, 124	sylbir 223	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ 𝐷 ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ (-1(,)1))
126		incom 3766	. . . . . . . . . . . . . . . 16 ⊢ ((0(,)+∞) ∩ (-∞(,]0)) = ((-∞(,]0) ∩ (0(,)+∞))
127		pnfxr 11781	. . . . . . . . . . . . . . . . 17 ⊢ +∞ ∈ ℝ^*
128		df-ioc 12007	. . . . . . . . . . . . . . . . . 18 ⊢ (,] = (𝑥 ∈ ℝ^, 𝑦 ∈ ℝ^ ↦ {𝑧 ∈ ℝ^* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)})
129		df-ioo 12006	. . . . . . . . . . . . . . . . . 18 ⊢ (,) = (𝑥 ∈ ℝ^, 𝑦 ∈ ℝ^ ↦ {𝑧 ∈ ℝ^* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
130		xrltnle 9956	. . . . . . . . . . . . . . . . . 18 ⊢ ((0 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) → (0 < 𝑤 ↔ ¬ 𝑤 ≤ 0))
131	128, 129, 130	ixxdisj 12017	. . . . . . . . . . . . . . . . 17 ⊢ ((-∞ ∈ ℝ^* ∧ 0 ∈ ℝ^* ∧ +∞ ∈ ℝ^*) → ((-∞(,]0) ∩ (0(,)+∞)) = ∅)
132	52, 63, 127, 131	mp3an 1415	. . . . . . . . . . . . . . . 16 ⊢ ((-∞(,]0) ∩ (0(,)+∞)) = ∅
133	126, 132	eqtri 2631	. . . . . . . . . . . . . . 15 ⊢ ((0(,)+∞) ∩ (-∞(,]0)) = ∅
134		elioore 12032	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (-1(,)1) → 𝑥 ∈ ℝ)
135	134	resqcld 12852	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (-1(,)1) → (𝑥↑2) ∈ ℝ)
136		resubcl 10196	. . . . . . . . . . . . . . . . . 18 ⊢ ((1 ∈ ℝ ∧ (𝑥↑2) ∈ ℝ) → (1 − (𝑥↑2)) ∈ ℝ)
137	95, 135, 136	sylancr 693	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (-1(,)1) → (1 − (𝑥↑2)) ∈ ℝ)
138	92	rexri 9948	. . . . . . . . . . . . . . . . . . 19 ⊢ -1 ∈ ℝ^*
139	95	rexri 9948	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℝ^*
140		elioo2 12043	. . . . . . . . . . . . . . . . . . 19 ⊢ ((-1 ∈ ℝ^* ∧ 1 ∈ ℝ^*) → (𝑥 ∈ (-1(,)1) ↔ (𝑥 ∈ ℝ ∧ -1 < 𝑥 ∧ 𝑥 < 1)))
141	138, 139, 140	mp2an 703	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (-1(,)1) ↔ (𝑥 ∈ ℝ ∧ -1 < 𝑥 ∧ 𝑥 < 1))
142		recn 9882	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
143	142	abscld 13969	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℝ → (abs‘𝑥) ∈ ℝ)
144	142	absge0d 13977	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℝ → 0 ≤ (abs‘𝑥))
145		0le1 10400	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 ≤ 1
146		lt2sq 12754	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((abs‘𝑥) ∈ ℝ ∧ 0 ≤ (abs‘𝑥)) ∧ (1 ∈ ℝ ∧ 0 ≤ 1)) → ((abs‘𝑥) < 1 ↔ ((abs‘𝑥)↑2) < (1↑2)))
147	95, 145, 146	mpanr12 716	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((abs‘𝑥) ∈ ℝ ∧ 0 ≤ (abs‘𝑥)) → ((abs‘𝑥) < 1 ↔ ((abs‘𝑥)↑2) < (1↑2)))
148	143, 144, 147	syl2anc 690	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℝ → ((abs‘𝑥) < 1 ↔ ((abs‘𝑥)↑2) < (1↑2)))
149		abslt 13848	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑥) < 1 ↔ (-1 < 𝑥 ∧ 𝑥 < 1)))
150	95, 149	mpan2 702	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℝ → ((abs‘𝑥) < 1 ↔ (-1 < 𝑥 ∧ 𝑥 < 1)))
151		absresq 13836	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℝ → ((abs‘𝑥)↑2) = (𝑥↑2))
152		sq1 12775	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1↑2) = 1
153	152	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℝ → (1↑2) = 1)
154	151, 153	breq12d 4590	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℝ → (((abs‘𝑥)↑2) < (1↑2) ↔ (𝑥↑2) < 1))
155		resqcl 12748	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℝ → (𝑥↑2) ∈ ℝ)
156		posdif 10370	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑥↑2) ∈ ℝ ∧ 1 ∈ ℝ) → ((𝑥↑2) < 1 ↔ 0 < (1 − (𝑥↑2))))
157	155, 95, 156	sylancl 692	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℝ → ((𝑥↑2) < 1 ↔ 0 < (1 − (𝑥↑2))))
158	154, 157	bitrd 266	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℝ → (((abs‘𝑥)↑2) < (1↑2) ↔ 0 < (1 − (𝑥↑2))))
159	148, 150, 158	3bitr3d 296	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℝ → ((-1 < 𝑥 ∧ 𝑥 < 1) ↔ 0 < (1 − (𝑥↑2))))
160	159	biimpd 217	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℝ → ((-1 < 𝑥 ∧ 𝑥 < 1) → 0 < (1 − (𝑥↑2))))
161	160	3impib 1253	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℝ ∧ -1 < 𝑥 ∧ 𝑥 < 1) → 0 < (1 − (𝑥↑2)))
162	141, 161	sylbi 205	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (-1(,)1) → 0 < (1 − (𝑥↑2)))
163	137, 162	elrpd 11701	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (-1(,)1) → (1 − (𝑥↑2)) ∈ ℝ⁺)
164		ioorp 12078	. . . . . . . . . . . . . . . 16 ⊢ (0(,)+∞) = ℝ⁺
165	163, 164	syl6eleqr 2698	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (-1(,)1) → (1 − (𝑥↑2)) ∈ (0(,)+∞))
166		disjel 3974	. . . . . . . . . . . . . . 15 ⊢ ((((0(,)+∞) ∩ (-∞(,]0)) = ∅ ∧ (1 − (𝑥↑2)) ∈ (0(,)+∞)) → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
167	133, 165, 166	sylancr 693	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (-1(,)1) → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
168	125, 167	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝐷 ∧ 𝑥 ∈ ℝ) → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
169		elioc2 12063	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((-∞ ∈ ℝ^* ∧ 0 ∈ ℝ) → ((1 − (𝑥↑2)) ∈ (-∞(,]0) ↔ ((1 − (𝑥↑2)) ∈ ℝ ∧ -∞ < (1 − (𝑥↑2)) ∧ (1 − (𝑥↑2)) ≤ 0)))
170	52, 37, 169	mp2an 703	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1 − (𝑥↑2)) ∈ (-∞(,]0) ↔ ((1 − (𝑥↑2)) ∈ ℝ ∧ -∞ < (1 − (𝑥↑2)) ∧ (1 − (𝑥↑2)) ≤ 0))
171	170	biimpi 204	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1 − (𝑥↑2)) ∈ (-∞(,]0) → ((1 − (𝑥↑2)) ∈ ℝ ∧ -∞ < (1 − (𝑥↑2)) ∧ (1 − (𝑥↑2)) ≤ 0))
172	171	simp1d 1065	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1 − (𝑥↑2)) ∈ (-∞(,]0) → (1 − (𝑥↑2)) ∈ ℝ)
173		resubcl 10196	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1 ∈ ℝ ∧ (1 − (𝑥↑2)) ∈ ℝ) → (1 − (1 − (𝑥↑2))) ∈ ℝ)
174	95, 172, 173	sylancr 693	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 − (𝑥↑2)) ∈ (-∞(,]0) → (1 − (1 − (𝑥↑2))) ∈ ℝ)
175		nncan 10161	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1 ∈ ℂ ∧ (𝑥↑2) ∈ ℂ) → (1 − (1 − (𝑥↑2))) = (𝑥↑2))
176	16, 175	mpan 701	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥↑2) ∈ ℂ → (1 − (1 − (𝑥↑2))) = (𝑥↑2))
177	176	eleq1d 2671	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥↑2) ∈ ℂ → ((1 − (1 − (𝑥↑2))) ∈ ℝ ↔ (𝑥↑2) ∈ ℝ))
178	177	biimpa 499	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥↑2) ∈ ℂ ∧ (1 − (1 − (𝑥↑2))) ∈ ℝ) → (𝑥↑2) ∈ ℝ)
179	174, 178	sylan2 489	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (𝑥↑2) ∈ ℝ)
180	172	adantl 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (1 − (𝑥↑2)) ∈ ℝ)
181	171	simp3d 1067	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1 − (𝑥↑2)) ∈ (-∞(,]0) → (1 − (𝑥↑2)) ≤ 0)
182	181	adantl 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (1 − (𝑥↑2)) ≤ 0)
183		letr 9982	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((1 − (𝑥↑2)) ∈ ℝ ∧ 0 ∈ ℝ ∧ 1 ∈ ℝ) → (((1 − (𝑥↑2)) ≤ 0 ∧ 0 ≤ 1) → (1 − (𝑥↑2)) ≤ 1))
184	37, 95, 183	mp3an23 1407	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1 − (𝑥↑2)) ∈ ℝ → (((1 − (𝑥↑2)) ≤ 0 ∧ 0 ≤ 1) → (1 − (𝑥↑2)) ≤ 1))
185	145, 184	mpan2i 708	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1 − (𝑥↑2)) ∈ ℝ → ((1 − (𝑥↑2)) ≤ 0 → (1 − (𝑥↑2)) ≤ 1))
186	180, 182, 185	sylc 62	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (1 − (𝑥↑2)) ≤ 1)
187		subge0 10390	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1 ∈ ℝ ∧ (1 − (𝑥↑2)) ∈ ℝ) → (0 ≤ (1 − (1 − (𝑥↑2))) ↔ (1 − (𝑥↑2)) ≤ 1))
188	95, 180, 187	sylancr 693	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (0 ≤ (1 − (1 − (𝑥↑2))) ↔ (1 − (𝑥↑2)) ≤ 1))
189	186, 188	mpbird 245	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → 0 ≤ (1 − (1 − (𝑥↑2))))
190	176	adantr 479	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (1 − (1 − (𝑥↑2))) = (𝑥↑2))
191	189, 190	breqtrd 4603	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → 0 ≤ (𝑥↑2))
192	179, 191	resqrtcld 13950	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥↑2) ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (√‘(𝑥↑2)) ∈ ℝ)
193	17, 192	sylan 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (√‘(𝑥↑2)) ∈ ℝ)
194		eleq1 2675	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (√‘(𝑥↑2)) → (𝑥 ∈ ℝ ↔ (√‘(𝑥↑2)) ∈ ℝ))
195	193, 194	syl5ibrcom 235	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (𝑥 = (√‘(𝑥↑2)) → 𝑥 ∈ ℝ))
196	193	renegcld 10308	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → -(√‘(𝑥↑2)) ∈ ℝ)
197		eleq1 2675	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = -(√‘(𝑥↑2)) → (𝑥 ∈ ℝ ↔ -(√‘(𝑥↑2)) ∈ ℝ))
198	196, 197	syl5ibrcom 235	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (𝑥 = -(√‘(𝑥↑2)) → 𝑥 ∈ ℝ))
199		eqid 2609	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥↑2) = (𝑥↑2)
200		eqsqrtor 13900	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℂ ∧ (𝑥↑2) ∈ ℂ) → ((𝑥↑2) = (𝑥↑2) ↔ (𝑥 = (√‘(𝑥↑2)) ∨ 𝑥 = -(√‘(𝑥↑2)))))
201	17, 200	mpdan 698	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℂ → ((𝑥↑2) = (𝑥↑2) ↔ (𝑥 = (√‘(𝑥↑2)) ∨ 𝑥 = -(√‘(𝑥↑2)))))
202	199, 201	mpbii 221	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℂ → (𝑥 = (√‘(𝑥↑2)) ∨ 𝑥 = -(√‘(𝑥↑2))))
203	202	adantr 479	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → (𝑥 = (√‘(𝑥↑2)) ∨ 𝑥 = -(√‘(𝑥↑2))))
204	195, 198, 203	mpjaod 394	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℂ ∧ (1 − (𝑥↑2)) ∈ (-∞(,]0)) → 𝑥 ∈ ℝ)
205	204	stoic1a 1687	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℂ ∧ ¬ 𝑥 ∈ ℝ) → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
206	12, 205	sylan 486	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝐷 ∧ ¬ 𝑥 ∈ ℝ) → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
207	168, 206	pm2.61dan 827	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐷 → ¬ (1 − (𝑥↑2)) ∈ (-∞(,]0))
208	116, 207	eldifd 3550	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐷 → (1 − (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0)))
209	208	adantl 480	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → (1 − (𝑥↑2)) ∈ (ℂ ∖ (-∞(,]0)))
210		2cnd 10940	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℂ → 2 ∈ ℂ)
211		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℂ → 𝑥 ∈ ℂ)
212	210, 211	mulcld 9916	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℂ → (2 · 𝑥) ∈ ℂ)
213	212	negcld 10230	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℂ → -(2 · 𝑥) ∈ ℂ)
214	213	adantl 480	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → -(2 · 𝑥) ∈ ℂ)
215	12, 214	sylan2 489	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → -(2 · 𝑥) ∈ ℂ)
216	61	sqrtcld 13970	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (ℂ ∖ (-∞(,]0)) → (√‘𝑦) ∈ ℂ)
217	216	adantl 480	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑦 ∈ (ℂ ∖ (-∞(,]0))) → (√‘𝑦) ∈ ℂ)
218		ovex 6555	. . . . . . . . . . 11 ⊢ (1 / (2 · (√‘𝑦))) ∈ V
219	218	a1i 11	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑦 ∈ (ℂ ∖ (-∞(,]0))) → (1 / (2 · (√‘𝑦))) ∈ V)
220	19	adantl 480	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → (1 − (𝑥↑2)) ∈ ℂ)
221	37	a1i 11	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → 0 ∈ ℝ)
222		1cnd 9912	. . . . . . . . . . . . . 14 ⊢ (⊤ → 1 ∈ ℂ)
223	11, 222	dvmptc 23444	. . . . . . . . . . . . 13 ⊢ (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ 1)) = (𝑥 ∈ ℂ ↦ 0))
224	17	adantl 480	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → (𝑥↑2) ∈ ℂ)
225		2cn 10938	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℂ
226		mulcl 9876	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (2 · 𝑥) ∈ ℂ)
227	225, 226	mpan 701	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℂ → (2 · 𝑥) ∈ ℂ)
228	227	adantl 480	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → (2 · 𝑥) ∈ ℂ)
229		2nn 11032	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℕ
230		dvexp 23439	. . . . . . . . . . . . . . . 16 ⊢ (2 ∈ ℕ → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · (𝑥↑(2 − 1)))))
231	229, 230	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · (𝑥↑(2 − 1))))
232		2m1e1 10982	. . . . . . . . . . . . . . . . . . 19 ⊢ (2 − 1) = 1
233	232	oveq2i 6538	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥↑(2 − 1)) = (𝑥↑1)
234		exp1 12683	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℂ → (𝑥↑1) = 𝑥)
235	233, 234	syl5eq 2655	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℂ → (𝑥↑(2 − 1)) = 𝑥)
236	235	oveq2d 6543	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℂ → (2 · (𝑥↑(2 − 1))) = (2 · 𝑥))
237	236	mpteq2ia 4662	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℂ ↦ (2 · (𝑥↑(2 − 1)))) = (𝑥 ∈ ℂ ↦ (2 · 𝑥))
238	231, 237	eqtri 2631	. . . . . . . . . . . . . 14 ⊢ (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · 𝑥))
239	238	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · 𝑥)))
240	11, 82, 221, 223, 224, 228, 239	dvmptsub 23453	. . . . . . . . . . . 12 ⊢ (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (1 − (𝑥↑2)))) = (𝑥 ∈ ℂ ↦ (0 − (2 · 𝑥))))
241		df-neg 10120	. . . . . . . . . . . . 13 ⊢ -(2 · 𝑥) = (0 − (2 · 𝑥))
242	241	mpteq2i 4663	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℂ ↦ -(2 · 𝑥)) = (𝑥 ∈ ℂ ↦ (0 − (2 · 𝑥)))
243	240, 242	syl6eqr 2661	. . . . . . . . . . 11 ⊢ (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (1 − (𝑥↑2)))) = (𝑥 ∈ ℂ ↦ -(2 · 𝑥)))
244	11, 220, 214, 243, 84, 90, 85, 108	dvmptres 23449	. . . . . . . . . 10 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ (1 − (𝑥↑2)))) = (𝑥 ∈ 𝐷 ↦ -(2 · 𝑥)))
245		eqid 2609	. . . . . . . . . . . 12 ⊢ (ℂ ∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0))
246	245	dvcnsqrt 24202	. . . . . . . . . . 11 ⊢ (ℂ D (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (√‘𝑦))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (1 / (2 · (√‘𝑦))))
247	246	a1i 11	. . . . . . . . . 10 ⊢ (⊤ → (ℂ D (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (√‘𝑦))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (1 / (2 · (√‘𝑦)))))
248		fveq2 6088	. . . . . . . . . 10 ⊢ (𝑦 = (1 − (𝑥↑2)) → (√‘𝑦) = (√‘(1 − (𝑥↑2))))
249	248	oveq2d 6543	. . . . . . . . . . 11 ⊢ (𝑦 = (1 − (𝑥↑2)) → (2 · (√‘𝑦)) = (2 · (√‘(1 − (𝑥↑2)))))
250	249	oveq2d 6543	. . . . . . . . . 10 ⊢ (𝑦 = (1 − (𝑥↑2)) → (1 / (2 · (√‘𝑦))) = (1 / (2 · (√‘(1 − (𝑥↑2))))))
251	11, 11, 209, 215, 217, 219, 244, 247, 248, 250	dvmptco 23458	. . . . . . . . 9 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ (√‘(1 − (𝑥↑2))))) = (𝑥 ∈ 𝐷 ↦ ((1 / (2 · (√‘(1 − (𝑥↑2))))) · -(2 · 𝑥))))
252		mulneg2 10318	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (2 · -𝑥) = -(2 · 𝑥))
253	225, 12, 252	sylancr 693	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐷 → (2 · -𝑥) = -(2 · 𝑥))
254	253	oveq1d 6542	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐷 → ((2 · -𝑥) / (2 · (√‘(1 − (𝑥↑2))))) = (-(2 · 𝑥) / (2 · (√‘(1 − (𝑥↑2))))))
255	12	negcld 10230	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐷 → -𝑥 ∈ ℂ)
256		eldifn 3694	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞))) → ¬ 𝑥 ∈ ((-∞(,]-1) ∪ (1[,)+∞)))
257	256, 3	eleq2s 2705	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐷 → ¬ 𝑥 ∈ ((-∞(,]-1) ∪ (1[,)+∞)))
258		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = -1 → 𝑥 = -1)
259		mnflt 11794	. . . . . . . . . . . . . . . . . . . 20 ⊢ (-1 ∈ ℝ → -∞ < -1)
260	92, 259	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ -∞ < -1
261		ubioc1 12054	. . . . . . . . . . . . . . . . . . 19 ⊢ ((-∞ ∈ ℝ^* ∧ -1 ∈ ℝ^* ∧ -∞ < -1) → -1 ∈ (-∞(,]-1))
262	52, 138, 260, 261	mp3an 1415	. . . . . . . . . . . . . . . . . 18 ⊢ -1 ∈ (-∞(,]-1)
263	258, 262	syl6eqel 2695	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = -1 → 𝑥 ∈ (-∞(,]-1))
264		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 1 → 𝑥 = 1)
265		ltpnf 11791	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 ∈ ℝ → 1 < +∞)
266	95, 265	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 < +∞
267		lbico1 12055	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ ℝ^* ∧ +∞ ∈ ℝ^* ∧ 1 < +∞) → 1 ∈ (1[,)+∞))
268	139, 127, 266, 267	mp3an 1415	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ (1[,)+∞)
269	264, 268	syl6eqel 2695	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 1 → 𝑥 ∈ (1[,)+∞))
270	263, 269	orim12i 536	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = -1 ∨ 𝑥 = 1) → (𝑥 ∈ (-∞(,]-1) ∨ 𝑥 ∈ (1[,)+∞)))
271	270	orcoms 402	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = 1 ∨ 𝑥 = -1) → (𝑥 ∈ (-∞(,]-1) ∨ 𝑥 ∈ (1[,)+∞)))
272		elun 3714	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ((-∞(,]-1) ∪ (1[,)+∞)) ↔ (𝑥 ∈ (-∞(,]-1) ∨ 𝑥 ∈ (1[,)+∞)))
273	271, 272	sylibr 222	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 1 ∨ 𝑥 = -1) → 𝑥 ∈ ((-∞(,]-1) ∪ (1[,)+∞)))
274	257, 273	nsyl 133	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐷 → ¬ (𝑥 = 1 ∨ 𝑥 = -1))
275		1cnd 9912	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → 1 ∈ ℂ)
276	17	adantr 479	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → (𝑥↑2) ∈ ℂ)
277	19	adantr 479	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → (1 − (𝑥↑2)) ∈ ℂ)
278		simpr 475	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → (√‘(1 − (𝑥↑2))) = 0)
279	277, 278	sqr00d 13974	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → (1 − (𝑥↑2)) = 0)
280	275, 276, 279	subeq0d 10251	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → 1 = (𝑥↑2))
281	152, 280	syl5req 2656	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → (𝑥↑2) = (1↑2))
282	281	ex 448	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℂ → ((√‘(1 − (𝑥↑2))) = 0 → (𝑥↑2) = (1↑2)))
283		sqeqor 12795	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑥↑2) = (1↑2) ↔ (𝑥 = 1 ∨ 𝑥 = -1)))
284	16, 283	mpan2 702	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℂ → ((𝑥↑2) = (1↑2) ↔ (𝑥 = 1 ∨ 𝑥 = -1)))
285	282, 284	sylibd 227	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℂ → ((√‘(1 − (𝑥↑2))) = 0 → (𝑥 = 1 ∨ 𝑥 = -1)))
286	285	necon3bd 2795	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℂ → (¬ (𝑥 = 1 ∨ 𝑥 = -1) → (√‘(1 − (𝑥↑2))) ≠ 0))
287	12, 274, 286	sylc 62	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐷 → (√‘(1 − (𝑥↑2))) ≠ 0)
288		2cnne0 11089	. . . . . . . . . . . . 13 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
289		divcan5 10576	. . . . . . . . . . . . 13 ⊢ ((-𝑥 ∈ ℂ ∧ ((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · -𝑥) / (2 · (√‘(1 − (𝑥↑2))))) = (-𝑥 / (√‘(1 − (𝑥↑2)))))
290	288, 289	mp3an3 1404	. . . . . . . . . . . 12 ⊢ ((-𝑥 ∈ ℂ ∧ ((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0)) → ((2 · -𝑥) / (2 · (√‘(1 − (𝑥↑2))))) = (-𝑥 / (√‘(1 − (𝑥↑2)))))
291	255, 117, 287, 290	syl12anc 1315	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐷 → ((2 · -𝑥) / (2 · (√‘(1 − (𝑥↑2))))) = (-𝑥 / (√‘(1 − (𝑥↑2)))))
292	225, 12, 226	sylancr 693	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐷 → (2 · 𝑥) ∈ ℂ)
293	292	negcld 10230	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐷 → -(2 · 𝑥) ∈ ℂ)
294		mulcl 9876	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ∈ ℂ) → (2 · (√‘(1 − (𝑥↑2)))) ∈ ℂ)
295	225, 117, 294	sylancr 693	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐷 → (2 · (√‘(1 − (𝑥↑2)))) ∈ ℂ)
296		mulne0 10518	. . . . . . . . . . . . . 14 ⊢ (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ ((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0)) → (2 · (√‘(1 − (𝑥↑2)))) ≠ 0)
297	288, 296	mpan 701	. . . . . . . . . . . . 13 ⊢ (((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0) → (2 · (√‘(1 − (𝑥↑2)))) ≠ 0)
298	117, 287, 297	syl2anc 690	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐷 → (2 · (√‘(1 − (𝑥↑2)))) ≠ 0)
299	293, 295, 298	divrec2d 10654	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐷 → (-(2 · 𝑥) / (2 · (√‘(1 − (𝑥↑2))))) = ((1 / (2 · (√‘(1 − (𝑥↑2))))) · -(2 · 𝑥)))
300	254, 291, 299	3eqtr3rd 2652	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐷 → ((1 / (2 · (√‘(1 − (𝑥↑2))))) · -(2 · 𝑥)) = (-𝑥 / (√‘(1 − (𝑥↑2)))))
301	300	mpteq2ia 4662	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 ↦ ((1 / (2 · (√‘(1 − (𝑥↑2))))) · -(2 · 𝑥))) = (𝑥 ∈ 𝐷 ↦ (-𝑥 / (√‘(1 − (𝑥↑2)))))
302	251, 301	syl6eq 2659	. . . . . . . 8 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ (√‘(1 − (𝑥↑2))))) = (𝑥 ∈ 𝐷 ↦ (-𝑥 / (√‘(1 − (𝑥↑2))))))
303	11, 77, 78, 114, 118, 120, 302	dvmptadd 23446	. . . . . . 7 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))) = (𝑥 ∈ 𝐷 ↦ (i + (-𝑥 / (√‘(1 − (𝑥↑2)))))))
304		mulcl 9876	. . . . . . . . . . . 12 ⊢ ((i ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ∈ ℂ) → (i · (√‘(1 − (𝑥↑2)))) ∈ ℂ)
305	13, 20, 304	sylancr 693	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℂ → (i · (√‘(1 − (𝑥↑2)))) ∈ ℂ)
306	12, 305	syl 17	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐷 → (i · (√‘(1 − (𝑥↑2)))) ∈ ℂ)
307	306, 255, 117, 287	divdird 10688	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → (((i · (√‘(1 − (𝑥↑2)))) + -𝑥) / (√‘(1 − (𝑥↑2)))) = (((i · (√‘(1 − (𝑥↑2)))) / (√‘(1 − (𝑥↑2)))) + (-𝑥 / (√‘(1 − (𝑥↑2))))))
308		ixi 10505	. . . . . . . . . . . . . . . 16 ⊢ (i · i) = -1
309	308	eqcomi 2618	. . . . . . . . . . . . . . 15 ⊢ -1 = (i · i)
310	309	oveq1i 6537	. . . . . . . . . . . . . 14 ⊢ (-1 · 𝑥) = ((i · i) · 𝑥)
311		mulm1 10322	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℂ → (-1 · 𝑥) = -𝑥)
312		mulass 9880	. . . . . . . . . . . . . . 15 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ ∧ 𝑥 ∈ ℂ) → ((i · i) · 𝑥) = (i · (i · 𝑥)))
313	13, 13, 312	mp3an12 1405	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℂ → ((i · i) · 𝑥) = (i · (i · 𝑥)))
314	310, 311, 313	3eqtr3a 2667	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℂ → -𝑥 = (i · (i · 𝑥)))
315	314	oveq1d 6542	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℂ → (-𝑥 + (i · (√‘(1 − (𝑥↑2))))) = ((i · (i · 𝑥)) + (i · (√‘(1 − (𝑥↑2))))))
316		negcl 10132	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℂ → -𝑥 ∈ ℂ)
317	305, 316	addcomd 10089	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℂ → ((i · (√‘(1 − (𝑥↑2)))) + -𝑥) = (-𝑥 + (i · (√‘(1 − (𝑥↑2))))))
318	13	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℂ → i ∈ ℂ)
319	318, 15, 20	adddid 9920	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℂ → (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) = ((i · (i · 𝑥)) + (i · (√‘(1 − (𝑥↑2))))))
320	315, 317, 319	3eqtr4d 2653	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℂ → ((i · (√‘(1 − (𝑥↑2)))) + -𝑥) = (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
321	12, 320	syl 17	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐷 → ((i · (√‘(1 − (𝑥↑2)))) + -𝑥) = (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
322	321	oveq1d 6542	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → (((i · (√‘(1 − (𝑥↑2)))) + -𝑥) / (√‘(1 − (𝑥↑2)))) = ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))))
323	75, 117, 287	divcan4d 10656	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐷 → ((i · (√‘(1 − (𝑥↑2)))) / (√‘(1 − (𝑥↑2)))) = i)
324	323	oveq1d 6542	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → (((i · (√‘(1 − (𝑥↑2)))) / (√‘(1 − (𝑥↑2)))) + (-𝑥 / (√‘(1 − (𝑥↑2))))) = (i + (-𝑥 / (√‘(1 − (𝑥↑2))))))
325	307, 322, 324	3eqtr3rd 2652	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐷 → (i + (-𝑥 / (√‘(1 − (𝑥↑2))))) = ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))))
326	325	mpteq2ia 4662	. . . . . . 7 ⊢ (𝑥 ∈ 𝐷 ↦ (i + (-𝑥 / (√‘(1 − (𝑥↑2)))))) = (𝑥 ∈ 𝐷 ↦ ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))))
327	303, 326	syl6eq 2659	. . . . . 6 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))) = (𝑥 ∈ 𝐷 ↦ ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2))))))
328	245	dvlog 24114	. . . . . . 7 ⊢ (ℂ D (log ↾ (ℂ ∖ (-∞(,]0)))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (1 / 𝑦))
329		logf1o 24032	. . . . . . . . . 10 ⊢ log:(ℂ ∖ {0})–1-1-onto→ran log
330		f1of 6035	. . . . . . . . . 10 ⊢ (log:(ℂ ∖ {0})–1-1-onto→ran log → log:(ℂ ∖ {0})⟶ran log)
331	329, 330	mp1i 13	. . . . . . . . 9 ⊢ (⊤ → log:(ℂ ∖ {0})⟶ran log)
332		snssi 4279	. . . . . . . . . . 11 ⊢ (0 ∈ (-∞(,]0) → {0} ⊆ (-∞(,]0))
333	66, 332	ax-mp 5	. . . . . . . . . 10 ⊢ {0} ⊆ (-∞(,]0)
334		sscon 3705	. . . . . . . . . 10 ⊢ ({0} ⊆ (-∞(,]0) → (ℂ ∖ (-∞(,]0)) ⊆ (ℂ ∖ {0}))
335	333, 334	mp1i 13	. . . . . . . . 9 ⊢ (⊤ → (ℂ ∖ (-∞(,]0)) ⊆ (ℂ ∖ {0}))
336	331, 335	feqresmpt 6145	. . . . . . . 8 ⊢ (⊤ → (log ↾ (ℂ ∖ (-∞(,]0))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (log‘𝑦)))
337	336	oveq2d 6543	. . . . . . 7 ⊢ (⊤ → (ℂ D (log ↾ (ℂ ∖ (-∞(,]0)))) = (ℂ D (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (log‘𝑦))))
338	328, 337	syl5reqr 2658	. . . . . 6 ⊢ (⊤ → (ℂ D (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (log‘𝑦))) = (𝑦 ∈ (ℂ ∖ (-∞(,]0)) ↦ (1 / 𝑦)))
339		fveq2 6088	. . . . . 6 ⊢ (𝑦 = ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) → (log‘𝑦) = (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
340		oveq2 6535	. . . . . 6 ⊢ (𝑦 = ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) → (1 / 𝑦) = (1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
341	11, 11, 58, 60, 72, 74, 327, 338, 339, 340	dvmptco 23458	. . . . 5 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))) = (𝑥 ∈ 𝐷 ↦ ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))))))
342	22, 24	reccld 10643	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐷 → (1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
343		mulcl 9876	. . . . . . . . . 10 ⊢ ((i ∈ ℂ ∧ ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) ∈ ℂ) → (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
344	13, 21, 343	sylancr 693	. . . . . . . . 9 ⊢ (𝑥 ∈ ℂ → (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
345	12, 344	syl 17	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐷 → (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) ∈ ℂ)
346	342, 345, 117, 287	divassd 10685	. . . . . . 7 ⊢ (𝑥 ∈ 𝐷 → (((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))) / (√‘(1 − (𝑥↑2)))) = ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2))))))
347	345, 22, 24	divrec2d 10654	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) = ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))
348	75, 22, 24	divcan4d 10656	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) = i)
349	347, 348	eqtr3d 2645	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐷 → ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))) = i)
350	349	oveq1d 6542	. . . . . . 7 ⊢ (𝑥 ∈ 𝐷 → (((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · (i · ((i · 𝑥) + (√‘(1 − (𝑥↑2)))))) / (√‘(1 − (𝑥↑2)))) = (i / (√‘(1 − (𝑥↑2)))))
351	346, 350	eqtr3d 2645	. . . . . 6 ⊢ (𝑥 ∈ 𝐷 → ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2))))) = (i / (√‘(1 − (𝑥↑2)))))
352	351	mpteq2ia 4662	. . . . 5 ⊢ (𝑥 ∈ 𝐷 ↦ ((1 / ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) · ((i · ((i · 𝑥) + (√‘(1 − (𝑥↑2))))) / (√‘(1 − (𝑥↑2)))))) = (𝑥 ∈ 𝐷 ↦ (i / (√‘(1 − (𝑥↑2)))))
353	341, 352	syl6eq 2659	. . . 4 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))) = (𝑥 ∈ 𝐷 ↦ (i / (√‘(1 − (𝑥↑2))))))
354		negicn 10133	. . . . 5 ⊢ -i ∈ ℂ
355	354	a1i 11	. . . 4 ⊢ (⊤ → -i ∈ ℂ)
356	11, 26, 28, 353, 355	dvmptcmul 23450	. . 3 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))) = (𝑥 ∈ 𝐷 ↦ (-i · (i / (√‘(1 − (𝑥↑2)))))))
357	356	trud 1483	. 2 ⊢ (ℂ D (𝑥 ∈ 𝐷 ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))) = (𝑥 ∈ 𝐷 ↦ (-i · (i / (√‘(1 − (𝑥↑2))))))
358	13, 13	mulneg1i 10326	. . . . . 6 ⊢ (-i · i) = -(i · i)
359	308	negeqi 10125	. . . . . 6 ⊢ -(i · i) = --1
360		negneg1e1 10975	. . . . . 6 ⊢ --1 = 1
361	358, 359, 360	3eqtri 2635	. . . . 5 ⊢ (-i · i) = 1
362	361	oveq1i 6537	. . . 4 ⊢ ((-i · i) / (√‘(1 − (𝑥↑2)))) = (1 / (√‘(1 − (𝑥↑2))))
363		divass 10552	. . . . . 6 ⊢ ((-i ∈ ℂ ∧ i ∈ ℂ ∧ ((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0)) → ((-i · i) / (√‘(1 − (𝑥↑2)))) = (-i · (i / (√‘(1 − (𝑥↑2))))))
364	354, 13, 363	mp3an12 1405	. . . . 5 ⊢ (((√‘(1 − (𝑥↑2))) ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) ≠ 0) → ((-i · i) / (√‘(1 − (𝑥↑2)))) = (-i · (i / (√‘(1 − (𝑥↑2))))))
365	117, 287, 364	syl2anc 690	. . . 4 ⊢ (𝑥 ∈ 𝐷 → ((-i · i) / (√‘(1 − (𝑥↑2)))) = (-i · (i / (√‘(1 − (𝑥↑2))))))
366	362, 365	syl5reqr 2658	. . 3 ⊢ (𝑥 ∈ 𝐷 → (-i · (i / (√‘(1 − (𝑥↑2))))) = (1 / (√‘(1 − (𝑥↑2)))))
367	366	mpteq2ia 4662	. 2 ⊢ (𝑥 ∈ 𝐷 ↦ (-i · (i / (√‘(1 − (𝑥↑2)))))) = (𝑥 ∈ 𝐷 ↦ (1 / (√‘(1 − (𝑥↑2)))))
368	9, 357, 367	3eqtri 2635	1 ⊢ (ℂ D (arcsin ↾ 𝐷)) = (𝑥 ∈ 𝐷 ↦ (1 / (√‘(1 − (𝑥↑2)))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 194 ∨ wo 381 ∧ wa 382 ∨ w3o 1029 ∧ w3a 1030 = wceq 1474 ⊤wtru 1475 ∈ wcel 1976 ≠ wne 2779 Vcvv 3172 ∖ cdif 3536 ∪ cun 3537 ∩ cin 3538 ⊆ wss 3539 ∅c0 3873 {csn 4124 {cpr 4126 class class class wbr 4577 ↦ cmpt 4637 ran crn 5029 ↾ cres 5030 ⟶wf 5786 –1-1-onto→wf1o 5789 ‘cfv 5790 (class class class)co 6527 ℂcc 9790 ℝcr 9791 0cc0 9792 1c1 9793 ici 9794 + caddc 9795 · cmul 9797 +∞cpnf 9927 -∞cmnf 9928 ℝ^*cxr 9929 < clt 9930 ≤ cle 9931 − cmin 10117 -cneg 10118 / cdiv 10533 ℕcn 10867 2c2 10917 ℝ⁺crp 11664 (,)cioo 12002 (,]cioc 12003 [,)cico 12004 ↑cexp 12677 ℜcre 13631 √csqrt 13767 abscabs 13768 ↾_t crest 15850 TopOpenctopn 15851 topGenctg 15867 ℂ_fldccnfld 19513 TopOnctopon 20460 Clsdccld 20572 D cdv 23350 logclog 24022 arcsincasin 24306

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1712 ax-4 1727 ax-5 1826 ax-6 1874 ax-7 1921 ax-8 1978 ax-9 1985 ax-10 2005 ax-11 2020 ax-12 2033 ax-13 2233 ax-ext 2589 ax-rep 4693 ax-sep 4703 ax-nul 4712 ax-pow 4764 ax-pr 4828 ax-un 6824 ax-inf2 8398 ax-cnex 9848 ax-resscn 9849 ax-1cn 9850 ax-icn 9851 ax-addcl 9852 ax-addrcl 9853 ax-mulcl 9854 ax-mulrcl 9855 ax-mulcom 9856 ax-addass 9857 ax-mulass 9858 ax-distr 9859 ax-i2m1 9860 ax-1ne0 9861 ax-1rid 9862 ax-rnegex 9863 ax-rrecex 9864 ax-cnre 9865 ax-pre-lttri 9866 ax-pre-lttrn 9867 ax-pre-ltadd 9868 ax-pre-mulgt0 9869 ax-pre-sup 9870 ax-addf 9871 ax-mulf 9872

This theorem depends on definitions: df-bi 195 df-or 383 df-an 384 df-3or 1031 df-3an 1032 df-tru 1477 df-fal 1480 df-ex 1695 df-nf 1700 df-sb 1867 df-eu 2461 df-mo 2462 df-clab 2596 df-cleq 2602 df-clel 2605 df-nfc 2739 df-ne 2781 df-nel 2782 df-ral 2900 df-rex 2901 df-reu 2902 df-rmo 2903 df-rab 2904 df-v 3174 df-sbc 3402 df-csb 3499 df-dif 3542 df-un 3544 df-in 3546 df-ss 3553 df-pss 3555 df-nul 3874 df-if 4036 df-pw 4109 df-sn 4125 df-pr 4127 df-tp 4129 df-op 4131 df-uni 4367 df-int 4405 df-iun 4451 df-iin 4452 df-br 4578 df-opab 4638 df-mpt 4639 df-tr 4675 df-eprel 4939 df-id 4943 df-po 4949 df-so 4950 df-fr 4987 df-se 4988 df-we 4989 df-xp 5034 df-rel 5035 df-cnv 5036 df-co 5037 df-dm 5038 df-rn 5039 df-res 5040 df-ima 5041 df-pred 5583 df-ord 5629 df-on 5630 df-lim 5631 df-suc 5632 df-iota 5754 df-fun 5792 df-fn 5793 df-f 5794 df-f1 5795 df-fo 5796 df-f1o 5797 df-fv 5798 df-isom 5799 df-riota 6489 df-ov 6530 df-oprab 6531 df-mpt2 6532 df-of 6772 df-om 6935 df-1st 7036 df-2nd 7037 df-supp 7160 df-wrecs 7271 df-recs 7332 df-rdg 7370 df-1o 7424 df-2o 7425 df-oadd 7428 df-er 7606 df-map 7723 df-pm 7724 df-ixp 7772 df-en 7819 df-dom 7820 df-sdom 7821 df-fin 7822 df-fsupp 8136 df-fi 8177 df-sup 8208 df-inf 8209 df-oi 8275 df-card 8625 df-cda 8850 df-pnf 9932 df-mnf 9933 df-xr 9934 df-ltxr 9935 df-le 9936 df-sub 10119 df-neg 10120 df-div 10534 df-nn 10868 df-2 10926 df-3 10927 df-4 10928 df-5 10929 df-6 10930 df-7 10931 df-8 10932 df-9 10933 df-n0 11140 df-z 11211 df-dec 11326 df-uz 11520 df-q 11621 df-rp 11665 df-xneg 11778 df-xadd 11779 df-xmul 11780 df-ioo 12006 df-ioc 12007 df-ico 12008 df-icc 12009 df-fz 12153 df-fzo 12290 df-fl 12410 df-mod 12486 df-seq 12619 df-exp 12678 df-fac 12878 df-bc 12907 df-hash 12935 df-shft 13601 df-cj 13633 df-re 13634 df-im 13635 df-sqrt 13769 df-abs 13770 df-limsup 13996 df-clim 14013 df-rlim 14014 df-sum 14211 df-ef 14583 df-sin 14585 df-cos 14586 df-tan 14587 df-pi 14588 df-struct 15643 df-ndx 15644 df-slot 15645 df-base 15646 df-sets 15647 df-ress 15648 df-plusg 15727 df-mulr 15728 df-starv 15729 df-sca 15730 df-vsca 15731 df-ip 15732 df-tset 15733 df-ple 15734 df-ds 15737 df-unif 15738 df-hom 15739 df-cco 15740 df-rest 15852 df-topn 15853 df-0g 15871 df-gsum 15872 df-topgen 15873 df-pt 15874 df-prds 15877 df-xrs 15931 df-qtop 15936 df-imas 15937 df-xps 15939 df-mre 16015 df-mrc 16016 df-acs 16018 df-mgm 17011 df-sgrp 17053 df-mnd 17064 df-submnd 17105 df-mulg 17310 df-cntz 17519 df-cmn 17964 df-psmet 19505 df-xmet 19506 df-met 19507 df-bl 19508 df-mopn 19509 df-fbas 19510 df-fg 19511 df-cnfld 19514 df-top 20463 df-bases 20464 df-topon 20465 df-topsp 20466 df-cld 20575 df-ntr 20576 df-cls 20577 df-nei 20654 df-lp 20692 df-perf 20693 df-cn 20783 df-cnp 20784 df-haus 20871 df-cmp 20942 df-tx 21117 df-hmeo 21310 df-fil 21402 df-fm 21494 df-flim 21495 df-flf 21496 df-xms 21876 df-ms 21877 df-tms 21878 df-cncf 22420 df-limc 23353 df-dv 23354 df-log 24024 df-cxp 24025 df-asin 24309

This theorem is referenced by: dvacos 32463 dvreasin 32464

W3C validator