dvlog - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > dvlog		Structured version Visualization version GIF version

Theorem dvlog 25234

Description: The derivative of the complex logarithm function. (Contributed by Mario Carneiro, 25-Feb-2015.)

**Hypothesis**
Ref	Expression
logcn.d	⊢ 𝐷 = (ℂ ∖ (-∞(,]0))

**Assertion**
Ref	Expression
dvlog	⊢ (ℂ D (log ↾ 𝐷)) = (𝑥 ∈ 𝐷 ↦ (1 / 𝑥))

Distinct variable group: 𝑥,𝐷

**Proof of Theorem dvlog**
Step	Hyp	Ref	Expression
1		eqid 2821	. . . 4 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
2	1	cnfldtopon 23391	. . . . 5 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
3	2	toponrestid 21529	. . . 4 ⊢ (TopOpen‘ℂ_fld) = ((TopOpen‘ℂ_fld) ↾_t ℂ)
4		cnelprrecn 10630	. . . . 5 ⊢ ℂ ∈ {ℝ, ℂ}
5	4	a1i 11	. . . 4 ⊢ (⊤ → ℂ ∈ {ℝ, ℂ})
6		logcn.d	. . . . . 6 ⊢ 𝐷 = (ℂ ∖ (-∞(,]0))
7	6	logdmopn 25232	. . . . 5 ⊢ 𝐷 ∈ (TopOpen‘ℂ_fld)
8	7	a1i 11	. . . 4 ⊢ (⊤ → 𝐷 ∈ (TopOpen‘ℂ_fld))
9		logf1o 25148	. . . . . . . . 9 ⊢ log:(ℂ ∖ {0})–1-1-onto→ran log
10		f1of1 6614	. . . . . . . . 9 ⊢ (log:(ℂ ∖ {0})–1-1-onto→ran log → log:(ℂ ∖ {0})–1-1→ran log)
11	9, 10	ax-mp 5	. . . . . . . 8 ⊢ log:(ℂ ∖ {0})–1-1→ran log
12	6	logdmss 25225	. . . . . . . 8 ⊢ 𝐷 ⊆ (ℂ ∖ {0})
13		f1ores 6629	. . . . . . . 8 ⊢ ((log:(ℂ ∖ {0})–1-1→ran log ∧ 𝐷 ⊆ (ℂ ∖ {0})) → (log ↾ 𝐷):𝐷–1-1-onto→(log “ 𝐷))
14	11, 12, 13	mp2an 690	. . . . . . 7 ⊢ (log ↾ 𝐷):𝐷–1-1-onto→(log “ 𝐷)
15		f1ocnv 6627	. . . . . . 7 ⊢ ((log ↾ 𝐷):𝐷–1-1-onto→(log “ 𝐷) → ^◡(log ↾ 𝐷):(log “ 𝐷)–1-1-onto→𝐷)
16	14, 15	ax-mp 5	. . . . . 6 ⊢ ^◡(log ↾ 𝐷):(log “ 𝐷)–1-1-onto→𝐷
17		df-log 25140	. . . . . . . . . . 11 ⊢ log = ^◡(exp ↾ (^◡ℑ “ (-π(,]π)))
18	17	reseq1i 5849	. . . . . . . . . 10 ⊢ (log ↾ 𝐷) = (^◡(exp ↾ (^◡ℑ “ (-π(,]π))) ↾ 𝐷)
19	18	cnveqi 5745	. . . . . . . . 9 ⊢ ^◡(log ↾ 𝐷) = ^◡(^◡(exp ↾ (^◡ℑ “ (-π(,]π))) ↾ 𝐷)
20		eff 15435	. . . . . . . . . . 11 ⊢ exp:ℂ⟶ℂ
21		cnvimass 5949	. . . . . . . . . . . 12 ⊢ (^◡ℑ “ (-π(,]π)) ⊆ dom ℑ
22		imf 14472	. . . . . . . . . . . . 13 ⊢ ℑ:ℂ⟶ℝ
23	22	fdmi 6524	. . . . . . . . . . . 12 ⊢ dom ℑ = ℂ
24	21, 23	sseqtri 4003	. . . . . . . . . . 11 ⊢ (^◡ℑ “ (-π(,]π)) ⊆ ℂ
25		fssres 6544	. . . . . . . . . . 11 ⊢ ((exp:ℂ⟶ℂ ∧ (^◡ℑ “ (-π(,]π)) ⊆ ℂ) → (exp ↾ (^◡ℑ “ (-π(,]π))):(^◡ℑ “ (-π(,]π))⟶ℂ)
26	20, 24, 25	mp2an 690	. . . . . . . . . 10 ⊢ (exp ↾ (^◡ℑ “ (-π(,]π))):(^◡ℑ “ (-π(,]π))⟶ℂ
27		ffun 6517	. . . . . . . . . 10 ⊢ ((exp ↾ (^◡ℑ “ (-π(,]π))):(^◡ℑ “ (-π(,]π))⟶ℂ → Fun (exp ↾ (^◡ℑ “ (-π(,]π))))
28		funcnvres2 6434	. . . . . . . . . 10 ⊢ (Fun (exp ↾ (^◡ℑ “ (-π(,]π))) → ^◡(^◡(exp ↾ (^◡ℑ “ (-π(,]π))) ↾ 𝐷) = ((exp ↾ (^◡ℑ “ (-π(,]π))) ↾ (^◡(exp ↾ (^◡ℑ “ (-π(,]π))) “ 𝐷)))
29	26, 27, 28	mp2b 10	. . . . . . . . 9 ⊢ ^◡(^◡(exp ↾ (^◡ℑ “ (-π(,]π))) ↾ 𝐷) = ((exp ↾ (^◡ℑ “ (-π(,]π))) ↾ (^◡(exp ↾ (^◡ℑ “ (-π(,]π))) “ 𝐷))
30		cnvimass 5949	. . . . . . . . . . 11 ⊢ (^◡(exp ↾ (^◡ℑ “ (-π(,]π))) “ 𝐷) ⊆ dom (exp ↾ (^◡ℑ “ (-π(,]π)))
31	26	fdmi 6524	. . . . . . . . . . 11 ⊢ dom (exp ↾ (^◡ℑ “ (-π(,]π))) = (^◡ℑ “ (-π(,]π))
32	30, 31	sseqtri 4003	. . . . . . . . . 10 ⊢ (^◡(exp ↾ (^◡ℑ “ (-π(,]π))) “ 𝐷) ⊆ (^◡ℑ “ (-π(,]π))
33		resabs1 5883	. . . . . . . . . 10 ⊢ ((^◡(exp ↾ (^◡ℑ “ (-π(,]π))) “ 𝐷) ⊆ (^◡ℑ “ (-π(,]π)) → ((exp ↾ (^◡ℑ “ (-π(,]π))) ↾ (^◡(exp ↾ (^◡ℑ “ (-π(,]π))) “ 𝐷)) = (exp ↾ (^◡(exp ↾ (^◡ℑ “ (-π(,]π))) “ 𝐷)))
34	32, 33	ax-mp 5	. . . . . . . . 9 ⊢ ((exp ↾ (^◡ℑ “ (-π(,]π))) ↾ (^◡(exp ↾ (^◡ℑ “ (-π(,]π))) “ 𝐷)) = (exp ↾ (^◡(exp ↾ (^◡ℑ “ (-π(,]π))) “ 𝐷))
35	19, 29, 34	3eqtri 2848	. . . . . . . 8 ⊢ ^◡(log ↾ 𝐷) = (exp ↾ (^◡(exp ↾ (^◡ℑ “ (-π(,]π))) “ 𝐷))
36	17	imaeq1i 5926	. . . . . . . . 9 ⊢ (log “ 𝐷) = (^◡(exp ↾ (^◡ℑ “ (-π(,]π))) “ 𝐷)
37	36	reseq2i 5850	. . . . . . . 8 ⊢ (exp ↾ (log “ 𝐷)) = (exp ↾ (^◡(exp ↾ (^◡ℑ “ (-π(,]π))) “ 𝐷))
38	35, 37	eqtr4i 2847	. . . . . . 7 ⊢ ^◡(log ↾ 𝐷) = (exp ↾ (log “ 𝐷))
39		f1oeq1 6604	. . . . . . 7 ⊢ (^◡(log ↾ 𝐷) = (exp ↾ (log “ 𝐷)) → (^◡(log ↾ 𝐷):(log “ 𝐷)–1-1-onto→𝐷 ↔ (exp ↾ (log “ 𝐷)):(log “ 𝐷)–1-1-onto→𝐷))
40	38, 39	ax-mp 5	. . . . . 6 ⊢ (^◡(log ↾ 𝐷):(log “ 𝐷)–1-1-onto→𝐷 ↔ (exp ↾ (log “ 𝐷)):(log “ 𝐷)–1-1-onto→𝐷)
41	16, 40	mpbi 232	. . . . 5 ⊢ (exp ↾ (log “ 𝐷)):(log “ 𝐷)–1-1-onto→𝐷
42	41	a1i 11	. . . 4 ⊢ (⊤ → (exp ↾ (log “ 𝐷)):(log “ 𝐷)–1-1-onto→𝐷)
43	38	cnveqi 5745	. . . . . 6 ⊢ ^◡^◡(log ↾ 𝐷) = ^◡(exp ↾ (log “ 𝐷))
44		relres 5882	. . . . . . 7 ⊢ Rel (log ↾ 𝐷)
45		dfrel2 6046	. . . . . . 7 ⊢ (Rel (log ↾ 𝐷) ↔ ^◡^◡(log ↾ 𝐷) = (log ↾ 𝐷))
46	44, 45	mpbi 232	. . . . . 6 ⊢ ^◡^◡(log ↾ 𝐷) = (log ↾ 𝐷)
47	43, 46	eqtr3i 2846	. . . . 5 ⊢ ^◡(exp ↾ (log “ 𝐷)) = (log ↾ 𝐷)
48		f1of 6615	. . . . . . 7 ⊢ ((log ↾ 𝐷):𝐷–1-1-onto→(log “ 𝐷) → (log ↾ 𝐷):𝐷⟶(log “ 𝐷))
49	14, 48	mp1i 13	. . . . . 6 ⊢ (⊤ → (log ↾ 𝐷):𝐷⟶(log “ 𝐷))
50		imassrn 5940	. . . . . . . 8 ⊢ (log “ 𝐷) ⊆ ran log
51		logrncn 25146	. . . . . . . . 9 ⊢ (𝑥 ∈ ran log → 𝑥 ∈ ℂ)
52	51	ssriv 3971	. . . . . . . 8 ⊢ ran log ⊆ ℂ
53	50, 52	sstri 3976	. . . . . . 7 ⊢ (log “ 𝐷) ⊆ ℂ
54	6	logcn 25230	. . . . . . 7 ⊢ (log ↾ 𝐷) ∈ (𝐷–cn→ℂ)
55		cncffvrn 23506	. . . . . . 7 ⊢ (((log “ 𝐷) ⊆ ℂ ∧ (log ↾ 𝐷) ∈ (𝐷–cn→ℂ)) → ((log ↾ 𝐷) ∈ (𝐷–cn→(log “ 𝐷)) ↔ (log ↾ 𝐷):𝐷⟶(log “ 𝐷)))
56	53, 54, 55	mp2an 690	. . . . . 6 ⊢ ((log ↾ 𝐷) ∈ (𝐷–cn→(log “ 𝐷)) ↔ (log ↾ 𝐷):𝐷⟶(log “ 𝐷))
57	49, 56	sylibr 236	. . . . 5 ⊢ (⊤ → (log ↾ 𝐷) ∈ (𝐷–cn→(log “ 𝐷)))
58	47, 57	eqeltrid 2917	. . . 4 ⊢ (⊤ → ^◡(exp ↾ (log “ 𝐷)) ∈ (𝐷–cn→(log “ 𝐷)))
59		ssid 3989	. . . . . . . . 9 ⊢ ℂ ⊆ ℂ
60	1, 3	dvres 24509	. . . . . . . . 9 ⊢ (((ℂ ⊆ ℂ ∧ exp:ℂ⟶ℂ) ∧ (ℂ ⊆ ℂ ∧ (log “ 𝐷) ⊆ ℂ)) → (ℂ D (exp ↾ (log “ 𝐷))) = ((ℂ D exp) ↾ ((int‘(TopOpen‘ℂ_fld))‘(log “ 𝐷))))
61	59, 20, 59, 53, 60	mp4an 691	. . . . . . . 8 ⊢ (ℂ D (exp ↾ (log “ 𝐷))) = ((ℂ D exp) ↾ ((int‘(TopOpen‘ℂ_fld))‘(log “ 𝐷)))
62		dvef 24577	. . . . . . . . 9 ⊢ (ℂ D exp) = exp
63	1	cnfldtop 23392	. . . . . . . . . 10 ⊢ (TopOpen‘ℂ_fld) ∈ Top
64	6	dvloglem 25231	. . . . . . . . . 10 ⊢ (log “ 𝐷) ∈ (TopOpen‘ℂ_fld)
65		isopn3i 21690	. . . . . . . . . 10 ⊢ (((TopOpen‘ℂ_fld) ∈ Top ∧ (log “ 𝐷) ∈ (TopOpen‘ℂ_fld)) → ((int‘(TopOpen‘ℂ_fld))‘(log “ 𝐷)) = (log “ 𝐷))
66	63, 64, 65	mp2an 690	. . . . . . . . 9 ⊢ ((int‘(TopOpen‘ℂ_fld))‘(log “ 𝐷)) = (log “ 𝐷)
67	62, 66	reseq12i 5851	. . . . . . . 8 ⊢ ((ℂ D exp) ↾ ((int‘(TopOpen‘ℂ_fld))‘(log “ 𝐷))) = (exp ↾ (log “ 𝐷))
68	61, 67	eqtri 2844	. . . . . . 7 ⊢ (ℂ D (exp ↾ (log “ 𝐷))) = (exp ↾ (log “ 𝐷))
69	68	dmeqi 5773	. . . . . 6 ⊢ dom (ℂ D (exp ↾ (log “ 𝐷))) = dom (exp ↾ (log “ 𝐷))
70		dmres 5875	. . . . . 6 ⊢ dom (exp ↾ (log “ 𝐷)) = ((log “ 𝐷) ∩ dom exp)
71	20	fdmi 6524	. . . . . . . 8 ⊢ dom exp = ℂ
72	53, 71	sseqtrri 4004	. . . . . . 7 ⊢ (log “ 𝐷) ⊆ dom exp
73		df-ss 3952	. . . . . . 7 ⊢ ((log “ 𝐷) ⊆ dom exp ↔ ((log “ 𝐷) ∩ dom exp) = (log “ 𝐷))
74	72, 73	mpbi 232	. . . . . 6 ⊢ ((log “ 𝐷) ∩ dom exp) = (log “ 𝐷)
75	69, 70, 74	3eqtri 2848	. . . . 5 ⊢ dom (ℂ D (exp ↾ (log “ 𝐷))) = (log “ 𝐷)
76	75	a1i 11	. . . 4 ⊢ (⊤ → dom (ℂ D (exp ↾ (log “ 𝐷))) = (log “ 𝐷))
77		neirr 3025	. . . . . 6 ⊢ ¬ 0 ≠ 0
78		resss 5878	. . . . . . . . . . . . 13 ⊢ ((ℂ D exp) ↾ ((int‘(TopOpen‘ℂ_fld))‘(log “ 𝐷))) ⊆ (ℂ D exp)
79	61, 78	eqsstri 4001	. . . . . . . . . . . 12 ⊢ (ℂ D (exp ↾ (log “ 𝐷))) ⊆ (ℂ D exp)
80	79, 62	sseqtri 4003	. . . . . . . . . . 11 ⊢ (ℂ D (exp ↾ (log “ 𝐷))) ⊆ exp
81	80	rnssi 5810	. . . . . . . . . 10 ⊢ ran (ℂ D (exp ↾ (log “ 𝐷))) ⊆ ran exp
82		eff2 15452	. . . . . . . . . . 11 ⊢ exp:ℂ⟶(ℂ ∖ {0})
83		frn 6520	. . . . . . . . . . 11 ⊢ (exp:ℂ⟶(ℂ ∖ {0}) → ran exp ⊆ (ℂ ∖ {0}))
84	82, 83	ax-mp 5	. . . . . . . . . 10 ⊢ ran exp ⊆ (ℂ ∖ {0})
85	81, 84	sstri 3976	. . . . . . . . 9 ⊢ ran (ℂ D (exp ↾ (log “ 𝐷))) ⊆ (ℂ ∖ {0})
86	85	sseli 3963	. . . . . . . 8 ⊢ (0 ∈ ran (ℂ D (exp ↾ (log “ 𝐷))) → 0 ∈ (ℂ ∖ {0}))
87		eldifsn 4719	. . . . . . . 8 ⊢ (0 ∈ (ℂ ∖ {0}) ↔ (0 ∈ ℂ ∧ 0 ≠ 0))
88	86, 87	sylib 220	. . . . . . 7 ⊢ (0 ∈ ran (ℂ D (exp ↾ (log “ 𝐷))) → (0 ∈ ℂ ∧ 0 ≠ 0))
89	88	simprd 498	. . . . . 6 ⊢ (0 ∈ ran (ℂ D (exp ↾ (log “ 𝐷))) → 0 ≠ 0)
90	77, 89	mto 199	. . . . 5 ⊢ ¬ 0 ∈ ran (ℂ D (exp ↾ (log “ 𝐷)))
91	90	a1i 11	. . . 4 ⊢ (⊤ → ¬ 0 ∈ ran (ℂ D (exp ↾ (log “ 𝐷))))
92	1, 3, 5, 8, 42, 58, 76, 91	dvcnv 24574	. . 3 ⊢ (⊤ → (ℂ D ^◡(exp ↾ (log “ 𝐷))) = (𝑥 ∈ 𝐷 ↦ (1 / ((ℂ D (exp ↾ (log “ 𝐷)))‘(^◡(exp ↾ (log “ 𝐷))‘𝑥)))))
93	92	mptru 1544	. 2 ⊢ (ℂ D ^◡(exp ↾ (log “ 𝐷))) = (𝑥 ∈ 𝐷 ↦ (1 / ((ℂ D (exp ↾ (log “ 𝐷)))‘(^◡(exp ↾ (log “ 𝐷))‘𝑥))))
94	47	oveq2i 7167	. 2 ⊢ (ℂ D ^◡(exp ↾ (log “ 𝐷))) = (ℂ D (log ↾ 𝐷))
95	68	fveq1i 6671	. . . . 5 ⊢ ((ℂ D (exp ↾ (log “ 𝐷)))‘(^◡(exp ↾ (log “ 𝐷))‘𝑥)) = ((exp ↾ (log “ 𝐷))‘(^◡(exp ↾ (log “ 𝐷))‘𝑥))
96		f1ocnvfv2 7034	. . . . . 6 ⊢ (((exp ↾ (log “ 𝐷)):(log “ 𝐷)–1-1-onto→𝐷 ∧ 𝑥 ∈ 𝐷) → ((exp ↾ (log “ 𝐷))‘(^◡(exp ↾ (log “ 𝐷))‘𝑥)) = 𝑥)
97	41, 96	mpan 688	. . . . 5 ⊢ (𝑥 ∈ 𝐷 → ((exp ↾ (log “ 𝐷))‘(^◡(exp ↾ (log “ 𝐷))‘𝑥)) = 𝑥)
98	95, 97	syl5eq 2868	. . . 4 ⊢ (𝑥 ∈ 𝐷 → ((ℂ D (exp ↾ (log “ 𝐷)))‘(^◡(exp ↾ (log “ 𝐷))‘𝑥)) = 𝑥)
99	98	oveq2d 7172	. . 3 ⊢ (𝑥 ∈ 𝐷 → (1 / ((ℂ D (exp ↾ (log “ 𝐷)))‘(^◡(exp ↾ (log “ 𝐷))‘𝑥))) = (1 / 𝑥))
100	99	mpteq2ia 5157	. 2 ⊢ (𝑥 ∈ 𝐷 ↦ (1 / ((ℂ D (exp ↾ (log “ 𝐷)))‘(^◡(exp ↾ (log “ 𝐷))‘𝑥)))) = (𝑥 ∈ 𝐷 ↦ (1 / 𝑥))
101	93, 94, 100	3eqtr3i 2852	1 ⊢ (ℂ D (log ↾ 𝐷)) = (𝑥 ∈ 𝐷 ↦ (1 / 𝑥))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 ↔ wb 208 ∧ wa 398 = wceq 1537 ⊤wtru 1538 ∈ wcel 2114 ≠ wne 3016 ∖ cdif 3933 ∩ cin 3935 ⊆ wss 3936 {csn 4567 {cpr 4569 ↦ cmpt 5146 ^◡ccnv 5554 dom cdm 5555 ran crn 5556 ↾ cres 5557 “ cima 5558 Rel wrel 5560 Fun wfun 6349 ⟶wf 6351 –1-1→wf1 6352 –1-1-onto→wf1o 6354 ‘cfv 6355 (class class class)co 7156 ℂcc 10535 ℝcr 10536 0cc0 10537 1c1 10538 -∞cmnf 10673 -cneg 10871 / cdiv 11297 (,]cioc 12740 ℑcim 14457 expce 15415 πcpi 15420 TopOpenctopn 16695 ℂ_fldccnfld 20545 Topctop 21501 intcnt 21625 –cn→ccncf 23484 D cdv 24461 logclog 25138

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-rep 5190 ax-sep 5203 ax-nul 5210 ax-pow 5266 ax-pr 5330 ax-un 7461 ax-inf2 9104 ax-cnex 10593 ax-resscn 10594 ax-1cn 10595 ax-icn 10596 ax-addcl 10597 ax-addrcl 10598 ax-mulcl 10599 ax-mulrcl 10600 ax-mulcom 10601 ax-addass 10602 ax-mulass 10603 ax-distr 10604 ax-i2m1 10605 ax-1ne0 10606 ax-1rid 10607 ax-rnegex 10608 ax-rrecex 10609 ax-cnre 10610 ax-pre-lttri 10611 ax-pre-lttrn 10612 ax-pre-ltadd 10613 ax-pre-mulgt0 10614 ax-pre-sup 10615 ax-addf 10616 ax-mulf 10617

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-fal 1550 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rmo 3146 df-rab 3147 df-v 3496 df-sbc 3773 df-csb 3884 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-pss 3954 df-nul 4292 df-if 4468 df-pw 4541 df-sn 4568 df-pr 4570 df-tp 4572 df-op 4574 df-uni 4839 df-int 4877 df-iun 4921 df-iin 4922 df-br 5067 df-opab 5129 df-mpt 5147 df-tr 5173 df-id 5460 df-eprel 5465 df-po 5474 df-so 5475 df-fr 5514 df-se 5515 df-we 5516 df-xp 5561 df-rel 5562 df-cnv 5563 df-co 5564 df-dm 5565 df-rn 5566 df-res 5567 df-ima 5568 df-pred 6148 df-ord 6194 df-on 6195 df-lim 6196 df-suc 6197 df-iota 6314 df-fun 6357 df-fn 6358 df-f 6359 df-f1 6360 df-fo 6361 df-f1o 6362 df-fv 6363 df-isom 6364 df-riota 7114 df-ov 7159 df-oprab 7160 df-mpo 7161 df-of 7409 df-om 7581 df-1st 7689 df-2nd 7690 df-supp 7831 df-wrecs 7947 df-recs 8008 df-rdg 8046 df-1o 8102 df-2o 8103 df-oadd 8106 df-er 8289 df-map 8408 df-pm 8409 df-ixp 8462 df-en 8510 df-dom 8511 df-sdom 8512 df-fin 8513 df-fsupp 8834 df-fi 8875 df-sup 8906 df-inf 8907 df-oi 8974 df-card 9368 df-pnf 10677 df-mnf 10678 df-xr 10679 df-ltxr 10680 df-le 10681 df-sub 10872 df-neg 10873 df-div 11298 df-nn 11639 df-2 11701 df-3 11702 df-4 11703 df-5 11704 df-6 11705 df-7 11706 df-8 11707 df-9 11708 df-n0 11899 df-z 11983 df-dec 12100 df-uz 12245 df-q 12350 df-rp 12391 df-xneg 12508 df-xadd 12509 df-xmul 12510 df-ioo 12743 df-ioc 12744 df-ico 12745 df-icc 12746 df-fz 12894 df-fzo 13035 df-fl 13163 df-mod 13239 df-seq 13371 df-exp 13431 df-fac 13635 df-bc 13664 df-hash 13692 df-shft 14426 df-cj 14458 df-re 14459 df-im 14460 df-sqrt 14594 df-abs 14595 df-limsup 14828 df-clim 14845 df-rlim 14846 df-sum 15043 df-ef 15421 df-sin 15423 df-cos 15424 df-tan 15425 df-pi 15426 df-struct 16485 df-ndx 16486 df-slot 16487 df-base 16489 df-sets 16490 df-ress 16491 df-plusg 16578 df-mulr 16579 df-starv 16580 df-sca 16581 df-vsca 16582 df-ip 16583 df-tset 16584 df-ple 16585 df-ds 16587 df-unif 16588 df-hom 16589 df-cco 16590 df-rest 16696 df-topn 16697 df-0g 16715 df-gsum 16716 df-topgen 16717 df-pt 16718 df-prds 16721 df-xrs 16775 df-qtop 16780 df-imas 16781 df-xps 16783 df-mre 16857 df-mrc 16858 df-acs 16860 df-mgm 17852 df-sgrp 17901 df-mnd 17912 df-submnd 17957 df-mulg 18225 df-cntz 18447 df-cmn 18908 df-psmet 20537 df-xmet 20538 df-met 20539 df-bl 20540 df-mopn 20541 df-fbas 20542 df-fg 20543 df-cnfld 20546 df-top 21502 df-topon 21519 df-topsp 21541 df-bases 21554 df-cld 21627 df-ntr 21628 df-cls 21629 df-nei 21706 df-lp 21744 df-perf 21745 df-cn 21835 df-cnp 21836 df-haus 21923 df-cmp 21995 df-tx 22170 df-hmeo 22363 df-fil 22454 df-fm 22546 df-flim 22547 df-flf 22548 df-xms 22930 df-ms 22931 df-tms 22932 df-cncf 23486 df-limc 24464 df-dv 24465 df-log 25140

This theorem is referenced by: dvlog2 25236 dvcncxp1 25324 dvatan 25513 lgamgulmlem2 25607 dvasin 34993

W3C validator