dvacos - Mathbox for Brendan Leahy

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

Theorem dvacos 33802

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

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

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

Distinct variable group: 𝑥,𝐷

**Proof of Theorem dvacos**
Step	Hyp	Ref	Expression
1		df-acos 24784	. . . . 5 ⊢ arccos = (𝑥 ∈ ℂ ↦ ((π / 2) − (arcsin‘𝑥)))
2	1	reseq1i 5539	. . . 4 ⊢ (arccos ↾ 𝐷) = ((𝑥 ∈ ℂ ↦ ((π / 2) − (arcsin‘𝑥))) ↾ 𝐷)
3		dvasin.d	. . . . . 6 ⊢ 𝐷 = (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞)))
4		difss 3872	. . . . . 6 ⊢ (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞))) ⊆ ℂ
5	3, 4	eqsstri 3768	. . . . 5 ⊢ 𝐷 ⊆ ℂ
6		resmpt 5599	. . . . 5 ⊢ (𝐷 ⊆ ℂ → ((𝑥 ∈ ℂ ↦ ((π / 2) − (arcsin‘𝑥))) ↾ 𝐷) = (𝑥 ∈ 𝐷 ↦ ((π / 2) − (arcsin‘𝑥))))
7	5, 6	ax-mp 5	. . . 4 ⊢ ((𝑥 ∈ ℂ ↦ ((π / 2) − (arcsin‘𝑥))) ↾ 𝐷) = (𝑥 ∈ 𝐷 ↦ ((π / 2) − (arcsin‘𝑥)))
8	2, 7	eqtri 2774	. . 3 ⊢ (arccos ↾ 𝐷) = (𝑥 ∈ 𝐷 ↦ ((π / 2) − (arcsin‘𝑥)))
9	8	oveq2i 6816	. 2 ⊢ (ℂ D (arccos ↾ 𝐷)) = (ℂ D (𝑥 ∈ 𝐷 ↦ ((π / 2) − (arcsin‘𝑥))))
10		cnelprrecn 10213	. . . . 5 ⊢ ℂ ∈ {ℝ, ℂ}
11	10	a1i 11	. . . 4 ⊢ (⊤ → ℂ ∈ {ℝ, ℂ})
12		halfpire 24407	. . . . . 6 ⊢ (π / 2) ∈ ℝ
13	12	recni 10236	. . . . 5 ⊢ (π / 2) ∈ ℂ
14	13	a1i 11	. . . 4 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → (π / 2) ∈ ℂ)
15		c0ex 10218	. . . . 5 ⊢ 0 ∈ V
16	15	a1i 11	. . . 4 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → 0 ∈ V)
17	13	a1i 11	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → (π / 2) ∈ ℂ)
18	15	a1i 11	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → 0 ∈ V)
19	13	a1i 11	. . . . . 6 ⊢ (⊤ → (π / 2) ∈ ℂ)
20	11, 19	dvmptc 23912	. . . . 5 ⊢ (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (π / 2))) = (𝑥 ∈ ℂ ↦ 0))
21	5	a1i 11	. . . . 5 ⊢ (⊤ → 𝐷 ⊆ ℂ)
22		eqid 2752	. . . . . . . 8 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
23	22	cnfldtopon 22779	. . . . . . 7 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
24	23	toponunii 20915	. . . . . . . 8 ⊢ ℂ = ∪ (TopOpen‘ℂ_fld)
25	24	restid 16288	. . . . . . 7 ⊢ ((TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ) → ((TopOpen‘ℂ_fld) ↾_t ℂ) = (TopOpen‘ℂ_fld))
26	23, 25	ax-mp 5	. . . . . 6 ⊢ ((TopOpen‘ℂ_fld) ↾_t ℂ) = (TopOpen‘ℂ_fld)
27	26	eqcomi 2761	. . . . 5 ⊢ (TopOpen‘ℂ_fld) = ((TopOpen‘ℂ_fld) ↾_t ℂ)
28	22	recld2 22810	. . . . . . . . . 10 ⊢ ℝ ∈ (Clsd‘(TopOpen‘ℂ_fld))
29		neg1rr 11309	. . . . . . . . . . . 12 ⊢ -1 ∈ ℝ
30		iocmnfcld 22765	. . . . . . . . . . . 12 ⊢ (-1 ∈ ℝ → (-∞(,]-1) ∈ (Clsd‘(topGen‘ran (,))))
31	29, 30	ax-mp 5	. . . . . . . . . . 11 ⊢ (-∞(,]-1) ∈ (Clsd‘(topGen‘ran (,)))
32	22	tgioo2 22799	. . . . . . . . . . . 12 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂ_fld) ↾_t ℝ)
33	32	fveq2i 6347	. . . . . . . . . . 11 ⊢ (Clsd‘(topGen‘ran (,))) = (Clsd‘((TopOpen‘ℂ_fld) ↾_t ℝ))
34	31, 33	eleqtri 2829	. . . . . . . . . 10 ⊢ (-∞(,]-1) ∈ (Clsd‘((TopOpen‘ℂ_fld) ↾_t ℝ))
35		restcldr 21172	. . . . . . . . . 10 ⊢ ((ℝ ∈ (Clsd‘(TopOpen‘ℂ_fld)) ∧ (-∞(,]-1) ∈ (Clsd‘((TopOpen‘ℂ_fld) ↾_t ℝ))) → (-∞(,]-1) ∈ (Clsd‘(TopOpen‘ℂ_fld)))
36	28, 34, 35	mp2an 710	. . . . . . . . 9 ⊢ (-∞(,]-1) ∈ (Clsd‘(TopOpen‘ℂ_fld))
37		1re 10223	. . . . . . . . . . . 12 ⊢ 1 ∈ ℝ
38		icopnfcld 22764	. . . . . . . . . . . 12 ⊢ (1 ∈ ℝ → (1[,)+∞) ∈ (Clsd‘(topGen‘ran (,))))
39	37, 38	ax-mp 5	. . . . . . . . . . 11 ⊢ (1[,)+∞) ∈ (Clsd‘(topGen‘ran (,)))
40	39, 33	eleqtri 2829	. . . . . . . . . 10 ⊢ (1[,)+∞) ∈ (Clsd‘((TopOpen‘ℂ_fld) ↾_t ℝ))
41		restcldr 21172	. . . . . . . . . 10 ⊢ ((ℝ ∈ (Clsd‘(TopOpen‘ℂ_fld)) ∧ (1[,)+∞) ∈ (Clsd‘((TopOpen‘ℂ_fld) ↾_t ℝ))) → (1[,)+∞) ∈ (Clsd‘(TopOpen‘ℂ_fld)))
42	28, 40, 41	mp2an 710	. . . . . . . . 9 ⊢ (1[,)+∞) ∈ (Clsd‘(TopOpen‘ℂ_fld))
43		uncld 21039	. . . . . . . . 9 ⊢ (((-∞(,]-1) ∈ (Clsd‘(TopOpen‘ℂ_fld)) ∧ (1[,)+∞) ∈ (Clsd‘(TopOpen‘ℂ_fld))) → ((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘(TopOpen‘ℂ_fld)))
44	36, 42, 43	mp2an 710	. . . . . . . 8 ⊢ ((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘(TopOpen‘ℂ_fld))
45	24	cldopn 21029	. . . . . . . 8 ⊢ (((-∞(,]-1) ∪ (1[,)+∞)) ∈ (Clsd‘(TopOpen‘ℂ_fld)) → (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞))) ∈ (TopOpen‘ℂ_fld))
46	44, 45	ax-mp 5	. . . . . . 7 ⊢ (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞))) ∈ (TopOpen‘ℂ_fld)
47	3, 46	eqeltri 2827	. . . . . 6 ⊢ 𝐷 ∈ (TopOpen‘ℂ_fld)
48	47	a1i 11	. . . . 5 ⊢ (⊤ → 𝐷 ∈ (TopOpen‘ℂ_fld))
49	11, 17, 18, 20, 21, 27, 22, 48	dvmptres 23917	. . . 4 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ (π / 2))) = (𝑥 ∈ 𝐷 ↦ 0))
50	5	sseli 3732	. . . . . 6 ⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ ℂ)
51		asincl 24791	. . . . . 6 ⊢ (𝑥 ∈ ℂ → (arcsin‘𝑥) ∈ ℂ)
52	50, 51	syl 17	. . . . 5 ⊢ (𝑥 ∈ 𝐷 → (arcsin‘𝑥) ∈ ℂ)
53	52	adantl 473	. . . 4 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → (arcsin‘𝑥) ∈ ℂ)
54		ovexd 6835	. . . 4 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐷) → (1 / (√‘(1 − (𝑥↑2)))) ∈ V)
55	3	dvasin 33801	. . . . 5 ⊢ (ℂ D (arcsin ↾ 𝐷)) = (𝑥 ∈ 𝐷 ↦ (1 / (√‘(1 − (𝑥↑2)))))
56		asinf 24790	. . . . . . . 8 ⊢ arcsin:ℂ⟶ℂ
57	56	a1i 11	. . . . . . 7 ⊢ (⊤ → arcsin:ℂ⟶ℂ)
58	57, 21	feqresmpt 6404	. . . . . 6 ⊢ (⊤ → (arcsin ↾ 𝐷) = (𝑥 ∈ 𝐷 ↦ (arcsin‘𝑥)))
59	58	oveq2d 6821	. . . . 5 ⊢ (⊤ → (ℂ D (arcsin ↾ 𝐷)) = (ℂ D (𝑥 ∈ 𝐷 ↦ (arcsin‘𝑥))))
60	55, 59	syl5reqr 2801	. . . 4 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ (arcsin‘𝑥))) = (𝑥 ∈ 𝐷 ↦ (1 / (√‘(1 − (𝑥↑2))))))
61	11, 14, 16, 49, 53, 54, 60	dvmptsub 23921	. . 3 ⊢ (⊤ → (ℂ D (𝑥 ∈ 𝐷 ↦ ((π / 2) − (arcsin‘𝑥)))) = (𝑥 ∈ 𝐷 ↦ (0 − (1 / (√‘(1 − (𝑥↑2)))))))
62	61	trud 1634	. 2 ⊢ (ℂ D (𝑥 ∈ 𝐷 ↦ ((π / 2) − (arcsin‘𝑥)))) = (𝑥 ∈ 𝐷 ↦ (0 − (1 / (√‘(1 − (𝑥↑2))))))
63		df-neg 10453	. . . 4 ⊢ -(1 / (√‘(1 − (𝑥↑2)))) = (0 − (1 / (√‘(1 − (𝑥↑2)))))
64		1cnd 10240	. . . . 5 ⊢ (𝑥 ∈ 𝐷 → 1 ∈ ℂ)
65		ax-1cn 10178	. . . . . . 7 ⊢ 1 ∈ ℂ
66	50	sqcld 13192	. . . . . . 7 ⊢ (𝑥 ∈ 𝐷 → (𝑥↑2) ∈ ℂ)
67		subcl 10464	. . . . . . 7 ⊢ ((1 ∈ ℂ ∧ (𝑥↑2) ∈ ℂ) → (1 − (𝑥↑2)) ∈ ℂ)
68	65, 66, 67	sylancr 698	. . . . . 6 ⊢ (𝑥 ∈ 𝐷 → (1 − (𝑥↑2)) ∈ ℂ)
69	68	sqrtcld 14367	. . . . 5 ⊢ (𝑥 ∈ 𝐷 → (√‘(1 − (𝑥↑2))) ∈ ℂ)
70		eldifn 3868	. . . . . . . 8 ⊢ (𝑥 ∈ (ℂ ∖ ((-∞(,]-1) ∪ (1[,)+∞))) → ¬ 𝑥 ∈ ((-∞(,]-1) ∪ (1[,)+∞)))
71	70, 3	eleq2s 2849	. . . . . . 7 ⊢ (𝑥 ∈ 𝐷 → ¬ 𝑥 ∈ ((-∞(,]-1) ∪ (1[,)+∞)))
72		mnfxr 10280	. . . . . . . . . . . 12 ⊢ -∞ ∈ ℝ^*
73	29	rexri 10281	. . . . . . . . . . . 12 ⊢ -1 ∈ ℝ^*
74		mnflt 12142	. . . . . . . . . . . . 13 ⊢ (-1 ∈ ℝ → -∞ < -1)
75	29, 74	ax-mp 5	. . . . . . . . . . . 12 ⊢ -∞ < -1
76		ubioc1 12412	. . . . . . . . . . . 12 ⊢ ((-∞ ∈ ℝ^* ∧ -1 ∈ ℝ^* ∧ -∞ < -1) → -1 ∈ (-∞(,]-1))
77	72, 73, 75, 76	mp3an 1565	. . . . . . . . . . 11 ⊢ -1 ∈ (-∞(,]-1)
78		eleq1 2819	. . . . . . . . . . 11 ⊢ (𝑥 = -1 → (𝑥 ∈ (-∞(,]-1) ↔ -1 ∈ (-∞(,]-1)))
79	77, 78	mpbiri 248	. . . . . . . . . 10 ⊢ (𝑥 = -1 → 𝑥 ∈ (-∞(,]-1))
80	37	rexri 10281	. . . . . . . . . . . 12 ⊢ 1 ∈ ℝ^*
81		pnfxr 10276	. . . . . . . . . . . 12 ⊢ +∞ ∈ ℝ^*
82		ltpnf 12139	. . . . . . . . . . . . 13 ⊢ (1 ∈ ℝ → 1 < +∞)
83	37, 82	ax-mp 5	. . . . . . . . . . . 12 ⊢ 1 < +∞
84		lbico1 12413	. . . . . . . . . . . 12 ⊢ ((1 ∈ ℝ^* ∧ +∞ ∈ ℝ^* ∧ 1 < +∞) → 1 ∈ (1[,)+∞))
85	80, 81, 83, 84	mp3an 1565	. . . . . . . . . . 11 ⊢ 1 ∈ (1[,)+∞)
86		eleq1 2819	. . . . . . . . . . 11 ⊢ (𝑥 = 1 → (𝑥 ∈ (1[,)+∞) ↔ 1 ∈ (1[,)+∞)))
87	85, 86	mpbiri 248	. . . . . . . . . 10 ⊢ (𝑥 = 1 → 𝑥 ∈ (1[,)+∞))
88	79, 87	orim12i 539	. . . . . . . . 9 ⊢ ((𝑥 = -1 ∨ 𝑥 = 1) → (𝑥 ∈ (-∞(,]-1) ∨ 𝑥 ∈ (1[,)+∞)))
89	88	orcoms 403	. . . . . . . 8 ⊢ ((𝑥 = 1 ∨ 𝑥 = -1) → (𝑥 ∈ (-∞(,]-1) ∨ 𝑥 ∈ (1[,)+∞)))
90		elun 3888	. . . . . . . 8 ⊢ (𝑥 ∈ ((-∞(,]-1) ∪ (1[,)+∞)) ↔ (𝑥 ∈ (-∞(,]-1) ∨ 𝑥 ∈ (1[,)+∞)))
91	89, 90	sylibr 224	. . . . . . 7 ⊢ ((𝑥 = 1 ∨ 𝑥 = -1) → 𝑥 ∈ ((-∞(,]-1) ∪ (1[,)+∞)))
92	71, 91	nsyl 135	. . . . . 6 ⊢ (𝑥 ∈ 𝐷 → ¬ (𝑥 = 1 ∨ 𝑥 = -1))
93		sq1 13144	. . . . . . . . . 10 ⊢ (1↑2) = 1
94		1cnd 10240	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → 1 ∈ ℂ)
95		sqcl 13111	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℂ → (𝑥↑2) ∈ ℂ)
96	95	adantr 472	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → (𝑥↑2) ∈ ℂ)
97	65, 95, 67	sylancr 698	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℂ → (1 − (𝑥↑2)) ∈ ℂ)
98	97	adantr 472	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → (1 − (𝑥↑2)) ∈ ℂ)
99		simpr 479	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → (√‘(1 − (𝑥↑2))) = 0)
100	98, 99	sqr00d 14371	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → (1 − (𝑥↑2)) = 0)
101	94, 96, 100	subeq0d 10584	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → 1 = (𝑥↑2))
102	93, 101	syl5req 2799	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℂ ∧ (√‘(1 − (𝑥↑2))) = 0) → (𝑥↑2) = (1↑2))
103	102	ex 449	. . . . . . . 8 ⊢ (𝑥 ∈ ℂ → ((√‘(1 − (𝑥↑2))) = 0 → (𝑥↑2) = (1↑2)))
104		sqeqor 13164	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑥↑2) = (1↑2) ↔ (𝑥 = 1 ∨ 𝑥 = -1)))
105	65, 104	mpan2 709	. . . . . . . 8 ⊢ (𝑥 ∈ ℂ → ((𝑥↑2) = (1↑2) ↔ (𝑥 = 1 ∨ 𝑥 = -1)))
106	103, 105	sylibd 229	. . . . . . 7 ⊢ (𝑥 ∈ ℂ → ((√‘(1 − (𝑥↑2))) = 0 → (𝑥 = 1 ∨ 𝑥 = -1)))
107	106	necon3bd 2938	. . . . . 6 ⊢ (𝑥 ∈ ℂ → (¬ (𝑥 = 1 ∨ 𝑥 = -1) → (√‘(1 − (𝑥↑2))) ≠ 0))
108	50, 92, 107	sylc 65	. . . . 5 ⊢ (𝑥 ∈ 𝐷 → (√‘(1 − (𝑥↑2))) ≠ 0)
109	64, 69, 108	divnegd 10998	. . . 4 ⊢ (𝑥 ∈ 𝐷 → -(1 / (√‘(1 − (𝑥↑2)))) = (-1 / (√‘(1 − (𝑥↑2)))))
110	63, 109	syl5eqr 2800	. . 3 ⊢ (𝑥 ∈ 𝐷 → (0 − (1 / (√‘(1 − (𝑥↑2))))) = (-1 / (√‘(1 − (𝑥↑2)))))
111	110	mpteq2ia 4884	. 2 ⊢ (𝑥 ∈ 𝐷 ↦ (0 − (1 / (√‘(1 − (𝑥↑2)))))) = (𝑥 ∈ 𝐷 ↦ (-1 / (√‘(1 − (𝑥↑2)))))
112	9, 62, 111	3eqtri 2778	1 ⊢ (ℂ D (arccos ↾ 𝐷)) = (𝑥 ∈ 𝐷 ↦ (-1 / (√‘(1 − (𝑥↑2)))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 ↔ wb 196 ∨ wo 382 ∧ wa 383 = wceq 1624 ⊤wtru 1625 ∈ wcel 2131 ≠ wne 2924 Vcvv 3332 ∖ cdif 3704 ∪ cun 3705 ⊆ wss 3707 {cpr 4315 class class class wbr 4796 ↦ cmpt 4873 ran crn 5259 ↾ cres 5260 ⟶wf 6037 ‘cfv 6041 (class class class)co 6805 ℂcc 10118 ℝcr 10119 0cc0 10120 1c1 10121 +∞cpnf 10255 -∞cmnf 10256 ℝ^*cxr 10257 < clt 10258 − cmin 10450 -cneg 10451 / cdiv 10868 2c2 11254 (,)cioo 12360 (,]cioc 12361 [,)cico 12362 ↑cexp 13046 √csqrt 14164 πcpi 14988 ↾_t crest 16275 TopOpenctopn 16276 topGenctg 16292 ℂ_fldccnfld 19940 TopOnctopon 20909 Clsdccld 21014 D cdv 23818 arcsincasin 24780 arccoscacos 24781

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1863 ax-4 1878 ax-5 1980 ax-6 2046 ax-7 2082 ax-8 2133 ax-9 2140 ax-10 2160 ax-11 2175 ax-12 2188 ax-13 2383 ax-ext 2732 ax-rep 4915 ax-sep 4925 ax-nul 4933 ax-pow 4984 ax-pr 5047 ax-un 7106 ax-inf2 8703 ax-cnex 10176 ax-resscn 10177 ax-1cn 10178 ax-icn 10179 ax-addcl 10180 ax-addrcl 10181 ax-mulcl 10182 ax-mulrcl 10183 ax-mulcom 10184 ax-addass 10185 ax-mulass 10186 ax-distr 10187 ax-i2m1 10188 ax-1ne0 10189 ax-1rid 10190 ax-rnegex 10191 ax-rrecex 10192 ax-cnre 10193 ax-pre-lttri 10194 ax-pre-lttrn 10195 ax-pre-ltadd 10196 ax-pre-mulgt0 10197 ax-pre-sup 10198 ax-addf 10199 ax-mulf 10200

This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1627 df-fal 1630 df-ex 1846 df-nf 1851 df-sb 2039 df-eu 2603 df-mo 2604 df-clab 2739 df-cleq 2745 df-clel 2748 df-nfc 2883 df-ne 2925 df-nel 3028 df-ral 3047 df-rex 3048 df-reu 3049 df-rmo 3050 df-rab 3051 df-v 3334 df-sbc 3569 df-csb 3667 df-dif 3710 df-un 3712 df-in 3714 df-ss 3721 df-pss 3723 df-nul 4051 df-if 4223 df-pw 4296 df-sn 4314 df-pr 4316 df-tp 4318 df-op 4320 df-uni 4581 df-int 4620 df-iun 4666 df-iin 4667 df-br 4797 df-opab 4857 df-mpt 4874 df-tr 4897 df-id 5166 df-eprel 5171 df-po 5179 df-so 5180 df-fr 5217 df-se 5218 df-we 5219 df-xp 5264 df-rel 5265 df-cnv 5266 df-co 5267 df-dm 5268 df-rn 5269 df-res 5270 df-ima 5271 df-pred 5833 df-ord 5879 df-on 5880 df-lim 5881 df-suc 5882 df-iota 6004 df-fun 6043 df-fn 6044 df-f 6045 df-f1 6046 df-fo 6047 df-f1o 6048 df-fv 6049 df-isom 6050 df-riota 6766 df-ov 6808 df-oprab 6809 df-mpt2 6810 df-of 7054 df-om 7223 df-1st 7325 df-2nd 7326 df-supp 7456 df-wrecs 7568 df-recs 7629 df-rdg 7667 df-1o 7721 df-2o 7722 df-oadd 7725 df-er 7903 df-map 8017 df-pm 8018 df-ixp 8067 df-en 8114 df-dom 8115 df-sdom 8116 df-fin 8117 df-fsupp 8433 df-fi 8474 df-sup 8505 df-inf 8506 df-oi 8572 df-card 8947 df-cda 9174 df-pnf 10260 df-mnf 10261 df-xr 10262 df-ltxr 10263 df-le 10264 df-sub 10452 df-neg 10453 df-div 10869 df-nn 11205 df-2 11263 df-3 11264 df-4 11265 df-5 11266 df-6 11267 df-7 11268 df-8 11269 df-9 11270 df-n0 11477 df-z 11562 df-dec 11678 df-uz 11872 df-q 11974 df-rp 12018 df-xneg 12131 df-xadd 12132 df-xmul 12133 df-ioo 12364 df-ioc 12365 df-ico 12366 df-icc 12367 df-fz 12512 df-fzo 12652 df-fl 12779 df-mod 12855 df-seq 12988 df-exp 13047 df-fac 13247 df-bc 13276 df-hash 13304 df-shft 13998 df-cj 14030 df-re 14031 df-im 14032 df-sqrt 14166 df-abs 14167 df-limsup 14393 df-clim 14410 df-rlim 14411 df-sum 14608 df-ef 14989 df-sin 14991 df-cos 14992 df-tan 14993 df-pi 14994 df-struct 16053 df-ndx 16054 df-slot 16055 df-base 16057 df-sets 16058 df-ress 16059 df-plusg 16148 df-mulr 16149 df-starv 16150 df-sca 16151 df-vsca 16152 df-ip 16153 df-tset 16154 df-ple 16155 df-ds 16158 df-unif 16159 df-hom 16160 df-cco 16161 df-rest 16277 df-topn 16278 df-0g 16296 df-gsum 16297 df-topgen 16298 df-pt 16299 df-prds 16302 df-xrs 16356 df-qtop 16361 df-imas 16362 df-xps 16364 df-mre 16440 df-mrc 16441 df-acs 16443 df-mgm 17435 df-sgrp 17477 df-mnd 17488 df-submnd 17529 df-mulg 17734 df-cntz 17942 df-cmn 18387 df-psmet 19932 df-xmet 19933 df-met 19934 df-bl 19935 df-mopn 19936 df-fbas 19937 df-fg 19938 df-cnfld 19941 df-top 20893 df-topon 20910 df-topsp 20931 df-bases 20944 df-cld 21017 df-ntr 21018 df-cls 21019 df-nei 21096 df-lp 21134 df-perf 21135 df-cn 21225 df-cnp 21226 df-haus 21313 df-cmp 21384 df-tx 21559 df-hmeo 21752 df-fil 21843 df-fm 21935 df-flim 21936 df-flf 21937 df-xms 22318 df-ms 22319 df-tms 22320 df-cncf 22874 df-limc 23821 df-dv 23822 df-log 24494 df-cxp 24495 df-asin 24783 df-acos 24784

This theorem is referenced by: dvreacos 33804

W3C validator