Theorem dvcjbr 24701

Description: The derivative of the conjugate of a function. For the (simpler but more limited) function version, see dvcj 24702. (This doesn't follow from dvcobr 24698 because ∗ is not a function on the reals, and even if we used complex derivatives, ∗ is not complex-differentiable.) (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Mario Carneiro, 10-Feb-2015.)

Hypotheses

Ref	Expression
dvcj.f	⊢ (𝜑 → 𝐹:𝑋⟶ℂ)
dvcj.x	⊢ (𝜑 → 𝑋 ⊆ ℝ)
dvcj.c	⊢ (𝜑 → 𝐶 ∈ dom (ℝ D 𝐹))

Assertion

Ref	Expression
dvcjbr	⊢ (𝜑 → 𝐶(ℝ D (∗ ∘ 𝐹))(∗‘((ℝ D 𝐹)‘𝐶)))

Proof of Theorem dvcjbr

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ax-resscn 10673	. . . . 5 ⊢ ℝ ⊆ ℂ
2	1	a1i 11	. . . 4 ⊢ (𝜑 → ℝ ⊆ ℂ)
3		dvcj.f	. . . 4 ⊢ (𝜑 → 𝐹:𝑋⟶ℂ)
4		dvcj.x	. . . 4 ⊢ (𝜑 → 𝑋 ⊆ ℝ)
5		eqid 2738	. . . . 5 ⊢ (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
6	5	tgioo2 23556	. . . 4 ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
7	2, 3, 4, 6, 5	dvbssntr 24652	. . 3 ⊢ (𝜑 → dom (ℝ D 𝐹) ⊆ ((int‘(topGen‘ran (,)))‘𝑋))
8		dvcj.c	. . 3 ⊢ (𝜑 → 𝐶 ∈ dom (ℝ D 𝐹))
9	7, 8	sseldd 3879	. 2 ⊢ (𝜑 → 𝐶 ∈ ((int‘(topGen‘ran (,)))‘𝑋))
10	4, 1	sstrdi 3890	. . . . . 6 ⊢ (𝜑 → 𝑋 ⊆ ℂ)
11	1	a1i 11	. . . . . . . . 9 ⊢ ((𝐹:𝑋⟶ℂ ∧ 𝑋 ⊆ ℝ) → ℝ ⊆ ℂ)
12		simpl 486	. . . . . . . . 9 ⊢ ((𝐹:𝑋⟶ℂ ∧ 𝑋 ⊆ ℝ) → 𝐹:𝑋⟶ℂ)
13		simpr 488	. . . . . . . . 9 ⊢ ((𝐹:𝑋⟶ℂ ∧ 𝑋 ⊆ ℝ) → 𝑋 ⊆ ℝ)
14	11, 12, 13	dvbss 24653	. . . . . . . 8 ⊢ ((𝐹:𝑋⟶ℂ ∧ 𝑋 ⊆ ℝ) → dom (ℝ D 𝐹) ⊆ 𝑋)
15	3, 4, 14	syl2anc 587	. . . . . . 7 ⊢ (𝜑 → dom (ℝ D 𝐹) ⊆ 𝑋)
16	15, 8	sseldd 3879	. . . . . 6 ⊢ (𝜑 → 𝐶 ∈ 𝑋)
17	3, 10, 16	dvlem 24648	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶)) ∈ ℂ)
18	17	fmpttd 6890	. . . 4 ⊢ (𝜑 → (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))):(𝑋 ∖ {𝐶})⟶ℂ)
19		ssidd 3901	. . . 4 ⊢ (𝜑 → ℂ ⊆ ℂ)
20	5	cnfldtopon 23536	. . . . 5 ⊢ (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
21	20	toponrestid 21673	. . . 4 ⊢ (TopOpen‘ℂfld) = ((TopOpen‘ℂfld) ↾t ℂ)
22		dvf 24659	. . . . . . . 8 ⊢ (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ
23		ffun 6508	. . . . . . . 8 ⊢ ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ → Fun (ℝ D 𝐹))
24		funfvbrb 6829	. . . . . . . 8 ⊢ (Fun (ℝ D 𝐹) → (𝐶 ∈ dom (ℝ D 𝐹) ↔ 𝐶(ℝ D 𝐹)((ℝ D 𝐹)‘𝐶)))
25	22, 23, 24	mp2b 10	. . . . . . 7 ⊢ (𝐶 ∈ dom (ℝ D 𝐹) ↔ 𝐶(ℝ D 𝐹)((ℝ D 𝐹)‘𝐶))
26	8, 25	sylib 221	. . . . . 6 ⊢ (𝜑 → 𝐶(ℝ D 𝐹)((ℝ D 𝐹)‘𝐶))
27		eqid 2738	. . . . . . 7 ⊢ (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))) = (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶)))
28	6, 5, 27, 2, 3, 4	eldv 24650	. . . . . 6 ⊢ (𝜑 → (𝐶(ℝ D 𝐹)((ℝ D 𝐹)‘𝐶) ↔ (𝐶 ∈ ((int‘(topGen‘ran (,)))‘𝑋) ∧ ((ℝ D 𝐹)‘𝐶) ∈ ((𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))) limℂ 𝐶))))
29	26, 28	mpbid 235	. . . . 5 ⊢ (𝜑 → (𝐶 ∈ ((int‘(topGen‘ran (,)))‘𝑋) ∧ ((ℝ D 𝐹)‘𝐶) ∈ ((𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))) limℂ 𝐶)))
30	29	simprd 499	. . . 4 ⊢ (𝜑 → ((ℝ D 𝐹)‘𝐶) ∈ ((𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))) limℂ 𝐶))
31		cjcncf 23657	. . . . . 6 ⊢ ∗ ∈ (ℂ–cn→ℂ)
32	5	cncfcn1 23664	. . . . . 6 ⊢ (ℂ–cn→ℂ) = ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld))
33	31, 32	eleqtri 2831	. . . . 5 ⊢ ∗ ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld))
34	22	ffvelrni 6861	. . . . . 6 ⊢ (𝐶 ∈ dom (ℝ D 𝐹) → ((ℝ D 𝐹)‘𝐶) ∈ ℂ)
35	8, 34	syl 17	. . . . 5 ⊢ (𝜑 → ((ℝ D 𝐹)‘𝐶) ∈ ℂ)
36		unicntop 23539	. . . . . 6 ⊢ ℂ = ∪ (TopOpen‘ℂfld)
37	36	cncnpi 22030	. . . . 5 ⊢ ((∗ ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)) ∧ ((ℝ D 𝐹)‘𝐶) ∈ ℂ) → ∗ ∈ (((TopOpen‘ℂfld) CnP (TopOpen‘ℂfld))‘((ℝ D 𝐹)‘𝐶)))
38	33, 35, 37	sylancr 590	. . . 4 ⊢ (𝜑 → ∗ ∈ (((TopOpen‘ℂfld) CnP (TopOpen‘ℂfld))‘((ℝ D 𝐹)‘𝐶)))
39	18, 19, 5, 21, 30, 38	limccnp 24643	. . 3 ⊢ (𝜑 → (∗‘((ℝ D 𝐹)‘𝐶)) ∈ ((∗ ∘ (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶)))) limℂ 𝐶))
40		cjf 14554	. . . . . . 7 ⊢ ∗:ℂ⟶ℂ
41	40	a1i 11	. . . . . 6 ⊢ (𝜑 → ∗:ℂ⟶ℂ)
42	41, 17	cofmpt 6905	. . . . 5 ⊢ (𝜑 → (∗ ∘ (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶)))) = (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (∗‘(((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶)))))
43	3	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → 𝐹:𝑋⟶ℂ)
44		eldifi 4018	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝑋 ∖ {𝐶}) → 𝑥 ∈ 𝑋)
45	44	adantl 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → 𝑥 ∈ 𝑋)
46	43, 45	ffvelrnd 6863	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → (𝐹‘𝑥) ∈ ℂ)
47	3, 16	ffvelrnd 6863	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹‘𝐶) ∈ ℂ)
48	47	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → (𝐹‘𝐶) ∈ ℂ)
49	46, 48	subcld 11076	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → ((𝐹‘𝑥) − (𝐹‘𝐶)) ∈ ℂ)
50	4	sselda 3878	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ ℝ)
51	44, 50	sylan2 596	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → 𝑥 ∈ ℝ)
52	4, 16	sseldd 3879	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ ℝ)
53	52	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → 𝐶 ∈ ℝ)
54	51, 53	resubcld 11147	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → (𝑥 − 𝐶) ∈ ℝ)
55	54	recnd 10748	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → (𝑥 − 𝐶) ∈ ℂ)
56	51	recnd 10748	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → 𝑥 ∈ ℂ)
57	53	recnd 10748	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → 𝐶 ∈ ℂ)
58		eldifsni 4679	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝑋 ∖ {𝐶}) → 𝑥 ≠ 𝐶)
59	58	adantl 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → 𝑥 ≠ 𝐶)
60	56, 57, 59	subne0d 11085	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → (𝑥 − 𝐶) ≠ 0)
61	49, 55, 60	cjdivd 14673	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → (∗‘(((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))) = ((∗‘((𝐹‘𝑥) − (𝐹‘𝐶))) / (∗‘(𝑥 − 𝐶))))
62		cjsub 14599	. . . . . . . . . 10 ⊢ (((𝐹‘𝑥) ∈ ℂ ∧ (𝐹‘𝐶) ∈ ℂ) → (∗‘((𝐹‘𝑥) − (𝐹‘𝐶))) = ((∗‘(𝐹‘𝑥)) − (∗‘(𝐹‘𝐶))))
63	46, 48, 62	syl2anc 587	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → (∗‘((𝐹‘𝑥) − (𝐹‘𝐶))) = ((∗‘(𝐹‘𝑥)) − (∗‘(𝐹‘𝐶))))
64		fvco3 6768	. . . . . . . . . . 11 ⊢ ((𝐹:𝑋⟶ℂ ∧ 𝑥 ∈ 𝑋) → ((∗ ∘ 𝐹)‘𝑥) = (∗‘(𝐹‘𝑥)))
65	3, 44, 64	syl2an 599	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → ((∗ ∘ 𝐹)‘𝑥) = (∗‘(𝐹‘𝑥)))
66		fvco3 6768	. . . . . . . . . . . 12 ⊢ ((𝐹:𝑋⟶ℂ ∧ 𝐶 ∈ 𝑋) → ((∗ ∘ 𝐹)‘𝐶) = (∗‘(𝐹‘𝐶)))
67	3, 16, 66	syl2anc 587	. . . . . . . . . . 11 ⊢ (𝜑 → ((∗ ∘ 𝐹)‘𝐶) = (∗‘(𝐹‘𝐶)))
68	67	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → ((∗ ∘ 𝐹)‘𝐶) = (∗‘(𝐹‘𝐶)))
69	65, 68	oveq12d 7189	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → (((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)) = ((∗‘(𝐹‘𝑥)) − (∗‘(𝐹‘𝐶))))
70	63, 69	eqtr4d 2776	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → (∗‘((𝐹‘𝑥) − (𝐹‘𝐶))) = (((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)))
71	54	cjred 14676	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → (∗‘(𝑥 − 𝐶)) = (𝑥 − 𝐶))
72	70, 71	oveq12d 7189	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → ((∗‘((𝐹‘𝑥) − (𝐹‘𝐶))) / (∗‘(𝑥 − 𝐶))) = ((((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)) / (𝑥 − 𝐶)))
73	61, 72	eqtrd 2773	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑋 ∖ {𝐶})) → (∗‘(((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶))) = ((((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)) / (𝑥 − 𝐶)))
74	73	mpteq2dva 5126	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (∗‘(((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶)))) = (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ ((((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)) / (𝑥 − 𝐶))))
75	42, 74	eqtrd 2773	. . . 4 ⊢ (𝜑 → (∗ ∘ (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶)))) = (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ ((((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)) / (𝑥 − 𝐶))))
76	75	oveq1d 7186	. . 3 ⊢ (𝜑 → ((∗ ∘ (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹‘𝑥) − (𝐹‘𝐶)) / (𝑥 − 𝐶)))) limℂ 𝐶) = ((𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ ((((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)) / (𝑥 − 𝐶))) limℂ 𝐶))
77	39, 76	eleqtrd 2835	. 2 ⊢ (𝜑 → (∗‘((ℝ D 𝐹)‘𝐶)) ∈ ((𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ ((((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)) / (𝑥 − 𝐶))) limℂ 𝐶))
78		eqid 2738	. . 3 ⊢ (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ ((((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)) / (𝑥 − 𝐶))) = (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ ((((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)) / (𝑥 − 𝐶)))
79		fco 6529	. . . 4 ⊢ ((∗:ℂ⟶ℂ ∧ 𝐹:𝑋⟶ℂ) → (∗ ∘ 𝐹):𝑋⟶ℂ)
80	40, 3, 79	sylancr 590	. . 3 ⊢ (𝜑 → (∗ ∘ 𝐹):𝑋⟶ℂ)
81	6, 5, 78, 2, 80, 4	eldv 24650	. 2 ⊢ (𝜑 → (𝐶(ℝ D (∗ ∘ 𝐹))(∗‘((ℝ D 𝐹)‘𝐶)) ↔ (𝐶 ∈ ((int‘(topGen‘ran (,)))‘𝑋) ∧ (∗‘((ℝ D 𝐹)‘𝐶)) ∈ ((𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ ((((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)) / (𝑥 − 𝐶))) limℂ 𝐶))))
82	9, 77, 81	mpbir2and 713	1 ⊢ (𝜑 → 𝐶(ℝ D (∗ ∘ 𝐹))(∗‘((ℝ D 𝐹)‘𝐶)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1542   ∈ wcel 2113   ≠ wne 2934   ∖ cdif 3841   ⊆ wss 3844  {csn 4517   class class class wbr 5031   ↦ cmpt 5111  dom cdm 5526  ran crn 5527   ∘ ccom 5530  Fun wfun 6334  ⟶wf 6336  ‘cfv 6340  (class class class)co 7171  ℂcc 10614  ℝcr 10615   − cmin 10949   / cdiv 11376  (,)cioo 12822  ∗ccj 14546  TopOpenctopn 16799  topGenctg 16815  ℂ_fldccnfld 20218  intcnt 21769   Cn ccn 21976   CnP ccnp 21977  –cn→ccncf 23629   lim_ℂ climc 24614   D cdv 24615

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710  ax-rep 5155  ax-sep 5168  ax-nul 5175  ax-pow 5233  ax-pr 5297  ax-un 7480  ax-cnex 10672  ax-resscn 10673  ax-1cn 10674  ax-icn 10675  ax-addcl 10676  ax-addrcl 10677  ax-mulcl 10678  ax-mulrcl 10679  ax-mulcom 10680  ax-addass 10681  ax-mulass 10682  ax-distr 10683  ax-i2m1 10684  ax-1ne0 10685  ax-1rid 10686  ax-rnegex 10687  ax-rrecex 10688  ax-cnre 10689  ax-pre-lttri 10690  ax-pre-lttrn 10691  ax-pre-ltadd 10692  ax-pre-mulgt0 10693  ax-pre-sup 10694

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-nel 3039  df-ral 3058  df-rex 3059  df-reu 3060  df-rmo 3061  df-rab 3062  df-v 3400  df-sbc 3683  df-csb 3792  df-dif 3847  df-un 3849  df-in 3851  df-ss 3861  df-pss 3863  df-nul 4213  df-if 4416  df-pw 4491  df-sn 4518  df-pr 4520  df-tp 4522  df-op 4524  df-uni 4798  df-int 4838  df-iun 4884  df-iin 4885  df-br 5032  df-opab 5094  df-mpt 5112  df-tr 5138  df-id 5430  df-eprel 5435  df-po 5443  df-so 5444  df-fr 5484  df-we 5486  df-xp 5532  df-rel 5533  df-cnv 5534  df-co 5535  df-dm 5536  df-rn 5537  df-res 5538  df-ima 5539  df-pred 6130  df-ord 6176  df-on 6177  df-lim 6178  df-suc 6179  df-iota 6298  df-fun 6342  df-fn 6343  df-f 6344  df-f1 6345  df-fo 6346  df-f1o 6347  df-fv 6348  df-riota 7128  df-ov 7174  df-oprab 7175  df-mpo 7176  df-om 7601  df-1st 7715  df-2nd 7716  df-wrecs 7977  df-recs 8038  df-rdg 8076  df-1o 8132  df-er 8321  df-map 8440  df-pm 8441  df-en 8557  df-dom 8558  df-sdom 8559  df-fin 8560  df-fi 8949  df-sup 8980  df-inf 8981  df-pnf 10756  df-mnf 10757  df-xr 10758  df-ltxr 10759  df-le 10760  df-sub 10951  df-neg 10952  df-div 11377  df-nn 11718  df-2 11780  df-3 11781  df-4 11782  df-5 11783  df-6 11784  df-7 11785  df-8 11786  df-9 11787  df-n0 11978  df-z 12064  df-dec 12181  df-uz 12326  df-q 12432  df-rp 12474  df-xneg 12591  df-xadd 12592  df-xmul 12593  df-ioo 12826  df-icc 12829  df-fz 12983  df-seq 13462  df-exp 13523  df-cj 14549  df-re 14550  df-im 14551  df-sqrt 14685  df-abs 14686  df-struct 16589  df-ndx 16590  df-slot 16591  df-base 16593  df-plusg 16682  df-mulr 16683  df-starv 16684  df-tset 16688  df-ple 16689  df-ds 16691  df-unif 16692  df-rest 16800  df-topn 16801  df-topgen 16821  df-psmet 20210  df-xmet 20211  df-met 20212  df-bl 20213  df-mopn 20214  df-fbas 20215  df-fg 20216  df-cnfld 20219  df-top 21646  df-topon 21663  df-topsp 21685  df-bases 21698  df-cld 21771  df-ntr 21772  df-cls 21773  df-nei 21850  df-lp 21888  df-perf 21889  df-cn 21979  df-cnp 21980  df-haus 22067  df-fil 22598  df-fm 22690  df-flim 22691  df-flf 22692  df-xms 23074  df-ms 23075  df-cncf 23631  df-limc 24618  df-dv 24619

This theorem is referenced by:  dvcj  24702