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 24702

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 2765	. . . 4 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
2	1	cnfldtopon 22879	. . . . 5 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
3	2	toponrestid 21019	. . . 4 ⊢ (TopOpen‘ℂ_fld) = ((TopOpen‘ℂ_fld) ↾_t ℂ)
4		cnelprrecn 10286	. . . . 5 ⊢ ℂ ∈ {ℝ, ℂ}
5	4	a1i 11	. . . 4 ⊢ (⊤ → ℂ ∈ {ℝ, ℂ})
6		logcn.d	. . . . . 6 ⊢ 𝐷 = (ℂ ∖ (-∞(,]0))
7	6	logdmopn 24700	. . . . 5 ⊢ 𝐷 ∈ (TopOpen‘ℂ_fld)
8	7	a1i 11	. . . 4 ⊢ (⊤ → 𝐷 ∈ (TopOpen‘ℂ_fld))
9		logf1o 24616	. . . . . . . . 9 ⊢ log:(ℂ ∖ {0})–1-1-onto→ran log
10		f1of1 6323	. . . . . . . . 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 24693	. . . . . . . 8 ⊢ 𝐷 ⊆ (ℂ ∖ {0})
13		f1ores 6338	. . . . . . . 8 ⊢ ((log:(ℂ ∖ {0})–1-1→ran log ∧ 𝐷 ⊆ (ℂ ∖ {0})) → (log ↾ 𝐷):𝐷–1-1-onto→(log “ 𝐷))
14	11, 12, 13	mp2an 683	. . . . . . 7 ⊢ (log ↾ 𝐷):𝐷–1-1-onto→(log “ 𝐷)
15		f1ocnv 6336	. . . . . . 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 24608	. . . . . . . . . . 11 ⊢ log = ^◡(exp ↾ (^◡ℑ “ (-π(,]π)))
18	17	reseq1i 5563	. . . . . . . . . 10 ⊢ (log ↾ 𝐷) = (^◡(exp ↾ (^◡ℑ “ (-π(,]π))) ↾ 𝐷)
19	18	cnveqi 5467	. . . . . . . . 9 ⊢ ^◡(log ↾ 𝐷) = ^◡(^◡(exp ↾ (^◡ℑ “ (-π(,]π))) ↾ 𝐷)
20		eff 15108	. . . . . . . . . . 11 ⊢ exp:ℂ⟶ℂ
21		cnvimass 5669	. . . . . . . . . . . 12 ⊢ (^◡ℑ “ (-π(,]π)) ⊆ dom ℑ
22		imf 14152	. . . . . . . . . . . . 13 ⊢ ℑ:ℂ⟶ℝ
23	22	fdmi 6235	. . . . . . . . . . . 12 ⊢ dom ℑ = ℂ
24	21, 23	sseqtri 3799	. . . . . . . . . . 11 ⊢ (^◡ℑ “ (-π(,]π)) ⊆ ℂ
25		fssres 6254	. . . . . . . . . . 11 ⊢ ((exp:ℂ⟶ℂ ∧ (^◡ℑ “ (-π(,]π)) ⊆ ℂ) → (exp ↾ (^◡ℑ “ (-π(,]π))):(^◡ℑ “ (-π(,]π))⟶ℂ)
26	20, 24, 25	mp2an 683	. . . . . . . . . 10 ⊢ (exp ↾ (^◡ℑ “ (-π(,]π))):(^◡ℑ “ (-π(,]π))⟶ℂ
27		ffun 6228	. . . . . . . . . 10 ⊢ ((exp ↾ (^◡ℑ “ (-π(,]π))):(^◡ℑ “ (-π(,]π))⟶ℂ → Fun (exp ↾ (^◡ℑ “ (-π(,]π))))
28		funcnvres2 6149	. . . . . . . . . 10 ⊢ (Fun (exp ↾ (^◡ℑ “ (-π(,]π))) → ^◡(^◡(exp ↾ (^◡ℑ “ (-π(,]π))) ↾ 𝐷) = ((exp ↾ (^◡ℑ “ (-π(,]π))) ↾ (^◡(exp ↾ (^◡ℑ “ (-π(,]π))) “ 𝐷)))
29	26, 27, 28	mp2b 10	. . . . . . . . 9 ⊢ ^◡(^◡(exp ↾ (^◡ℑ “ (-π(,]π))) ↾ 𝐷) = ((exp ↾ (^◡ℑ “ (-π(,]π))) ↾ (^◡(exp ↾ (^◡ℑ “ (-π(,]π))) “ 𝐷))
30		cnvimass 5669	. . . . . . . . . . 11 ⊢ (^◡(exp ↾ (^◡ℑ “ (-π(,]π))) “ 𝐷) ⊆ dom (exp ↾ (^◡ℑ “ (-π(,]π)))
31	26	fdmi 6235	. . . . . . . . . . 11 ⊢ dom (exp ↾ (^◡ℑ “ (-π(,]π))) = (^◡ℑ “ (-π(,]π))
32	30, 31	sseqtri 3799	. . . . . . . . . 10 ⊢ (^◡(exp ↾ (^◡ℑ “ (-π(,]π))) “ 𝐷) ⊆ (^◡ℑ “ (-π(,]π))
33		resabs1 5604	. . . . . . . . . 10 ⊢ ((^◡(exp ↾ (^◡ℑ “ (-π(,]π))) “ 𝐷) ⊆ (^◡ℑ “ (-π(,]π)) → ((exp ↾ (^◡ℑ “ (-π(,]π))) ↾ (^◡(exp ↾ (^◡ℑ “ (-π(,]π))) “ 𝐷)) = (exp ↾ (^◡(exp ↾ (^◡ℑ “ (-π(,]π))) “ 𝐷)))
34	32, 33	ax-mp 5	. . . . . . . . 9 ⊢ ((exp ↾ (^◡ℑ “ (-π(,]π))) ↾ (^◡(exp ↾ (^◡ℑ “ (-π(,]π))) “ 𝐷)) = (exp ↾ (^◡(exp ↾ (^◡ℑ “ (-π(,]π))) “ 𝐷))
35	19, 29, 34	3eqtri 2791	. . . . . . . 8 ⊢ ^◡(log ↾ 𝐷) = (exp ↾ (^◡(exp ↾ (^◡ℑ “ (-π(,]π))) “ 𝐷))
36	17	imaeq1i 5647	. . . . . . . . 9 ⊢ (log “ 𝐷) = (^◡(exp ↾ (^◡ℑ “ (-π(,]π))) “ 𝐷)
37	36	reseq2i 5564	. . . . . . . 8 ⊢ (exp ↾ (log “ 𝐷)) = (exp ↾ (^◡(exp ↾ (^◡ℑ “ (-π(,]π))) “ 𝐷))
38	35, 37	eqtr4i 2790	. . . . . . 7 ⊢ ^◡(log ↾ 𝐷) = (exp ↾ (log “ 𝐷))
39		f1oeq1 6314	. . . . . . 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 221	. . . . 5 ⊢ (exp ↾ (log “ 𝐷)):(log “ 𝐷)–1-1-onto→𝐷
42	41	a1i 11	. . . 4 ⊢ (⊤ → (exp ↾ (log “ 𝐷)):(log “ 𝐷)–1-1-onto→𝐷)
43	38	cnveqi 5467	. . . . . 6 ⊢ ^◡^◡(log ↾ 𝐷) = ^◡(exp ↾ (log “ 𝐷))
44		relres 5603	. . . . . . 7 ⊢ Rel (log ↾ 𝐷)
45		dfrel2 5768	. . . . . . 7 ⊢ (Rel (log ↾ 𝐷) ↔ ^◡^◡(log ↾ 𝐷) = (log ↾ 𝐷))
46	44, 45	mpbi 221	. . . . . 6 ⊢ ^◡^◡(log ↾ 𝐷) = (log ↾ 𝐷)
47	43, 46	eqtr3i 2789	. . . . 5 ⊢ ^◡(exp ↾ (log “ 𝐷)) = (log ↾ 𝐷)
48		f1of 6324	. . . . . . 7 ⊢ ((log ↾ 𝐷):𝐷–1-1-onto→(log “ 𝐷) → (log ↾ 𝐷):𝐷⟶(log “ 𝐷))
49	14, 48	mp1i 13	. . . . . 6 ⊢ (⊤ → (log ↾ 𝐷):𝐷⟶(log “ 𝐷))
50		imassrn 5661	. . . . . . . 8 ⊢ (log “ 𝐷) ⊆ ran log
51		logrncn 24614	. . . . . . . . 9 ⊢ (𝑥 ∈ ran log → 𝑥 ∈ ℂ)
52	51	ssriv 3767	. . . . . . . 8 ⊢ ran log ⊆ ℂ
53	50, 52	sstri 3772	. . . . . . 7 ⊢ (log “ 𝐷) ⊆ ℂ
54	6	logcn 24698	. . . . . . 7 ⊢ (log ↾ 𝐷) ∈ (𝐷–cn→ℂ)
55		cncffvrn 22994	. . . . . . 7 ⊢ (((log “ 𝐷) ⊆ ℂ ∧ (log ↾ 𝐷) ∈ (𝐷–cn→ℂ)) → ((log ↾ 𝐷) ∈ (𝐷–cn→(log “ 𝐷)) ↔ (log ↾ 𝐷):𝐷⟶(log “ 𝐷)))
56	53, 54, 55	mp2an 683	. . . . . 6 ⊢ ((log ↾ 𝐷) ∈ (𝐷–cn→(log “ 𝐷)) ↔ (log ↾ 𝐷):𝐷⟶(log “ 𝐷))
57	49, 56	sylibr 225	. . . . 5 ⊢ (⊤ → (log ↾ 𝐷) ∈ (𝐷–cn→(log “ 𝐷)))
58	47, 57	syl5eqel 2848	. . . 4 ⊢ (⊤ → ^◡(exp ↾ (log “ 𝐷)) ∈ (𝐷–cn→(log “ 𝐷)))
59		ssid 3785	. . . . . . . . 9 ⊢ ℂ ⊆ ℂ
60	1, 3	dvres 23980	. . . . . . . . 9 ⊢ (((ℂ ⊆ ℂ ∧ exp:ℂ⟶ℂ) ∧ (ℂ ⊆ ℂ ∧ (log “ 𝐷) ⊆ ℂ)) → (ℂ D (exp ↾ (log “ 𝐷))) = ((ℂ D exp) ↾ ((int‘(TopOpen‘ℂ_fld))‘(log “ 𝐷))))
61	59, 20, 59, 53, 60	mp4an 684	. . . . . . . 8 ⊢ (ℂ D (exp ↾ (log “ 𝐷))) = ((ℂ D exp) ↾ ((int‘(TopOpen‘ℂ_fld))‘(log “ 𝐷)))
62		dvef 24048	. . . . . . . . 9 ⊢ (ℂ D exp) = exp
63	1	cnfldtop 22880	. . . . . . . . . 10 ⊢ (TopOpen‘ℂ_fld) ∈ Top
64	6	dvloglem 24699	. . . . . . . . . 10 ⊢ (log “ 𝐷) ∈ (TopOpen‘ℂ_fld)
65		isopn3i 21180	. . . . . . . . . 10 ⊢ (((TopOpen‘ℂ_fld) ∈ Top ∧ (log “ 𝐷) ∈ (TopOpen‘ℂ_fld)) → ((int‘(TopOpen‘ℂ_fld))‘(log “ 𝐷)) = (log “ 𝐷))
66	63, 64, 65	mp2an 683	. . . . . . . . 9 ⊢ ((int‘(TopOpen‘ℂ_fld))‘(log “ 𝐷)) = (log “ 𝐷)
67	62, 66	reseq12i 5565	. . . . . . . 8 ⊢ ((ℂ D exp) ↾ ((int‘(TopOpen‘ℂ_fld))‘(log “ 𝐷))) = (exp ↾ (log “ 𝐷))
68	61, 67	eqtri 2787	. . . . . . 7 ⊢ (ℂ D (exp ↾ (log “ 𝐷))) = (exp ↾ (log “ 𝐷))
69	68	dmeqi 5495	. . . . . 6 ⊢ dom (ℂ D (exp ↾ (log “ 𝐷))) = dom (exp ↾ (log “ 𝐷))
70		dmres 5596	. . . . . 6 ⊢ dom (exp ↾ (log “ 𝐷)) = ((log “ 𝐷) ∩ dom exp)
71	20	fdmi 6235	. . . . . . . 8 ⊢ dom exp = ℂ
72	53, 71	sseqtr4i 3800	. . . . . . 7 ⊢ (log “ 𝐷) ⊆ dom exp
73		df-ss 3748	. . . . . . 7 ⊢ ((log “ 𝐷) ⊆ dom exp ↔ ((log “ 𝐷) ∩ dom exp) = (log “ 𝐷))
74	72, 73	mpbi 221	. . . . . 6 ⊢ ((log “ 𝐷) ∩ dom exp) = (log “ 𝐷)
75	69, 70, 74	3eqtri 2791	. . . . 5 ⊢ dom (ℂ D (exp ↾ (log “ 𝐷))) = (log “ 𝐷)
76	75	a1i 11	. . . 4 ⊢ (⊤ → dom (ℂ D (exp ↾ (log “ 𝐷))) = (log “ 𝐷))
77		neirr 2946	. . . . . 6 ⊢ ¬ 0 ≠ 0
78		resss 5599	. . . . . . . . . . . . 13 ⊢ ((ℂ D exp) ↾ ((int‘(TopOpen‘ℂ_fld))‘(log “ 𝐷))) ⊆ (ℂ D exp)
79	61, 78	eqsstri 3797	. . . . . . . . . . . 12 ⊢ (ℂ D (exp ↾ (log “ 𝐷))) ⊆ (ℂ D exp)
80	79, 62	sseqtri 3799	. . . . . . . . . . 11 ⊢ (ℂ D (exp ↾ (log “ 𝐷))) ⊆ exp
81		rnss 5524	. . . . . . . . . . 11 ⊢ ((ℂ D (exp ↾ (log “ 𝐷))) ⊆ exp → ran (ℂ D (exp ↾ (log “ 𝐷))) ⊆ ran exp)
82	80, 81	ax-mp 5	. . . . . . . . . 10 ⊢ ran (ℂ D (exp ↾ (log “ 𝐷))) ⊆ ran exp
83		eff2 15125	. . . . . . . . . . 11 ⊢ exp:ℂ⟶(ℂ ∖ {0})
84		frn 6231	. . . . . . . . . . 11 ⊢ (exp:ℂ⟶(ℂ ∖ {0}) → ran exp ⊆ (ℂ ∖ {0}))
85	83, 84	ax-mp 5	. . . . . . . . . 10 ⊢ ran exp ⊆ (ℂ ∖ {0})
86	82, 85	sstri 3772	. . . . . . . . 9 ⊢ ran (ℂ D (exp ↾ (log “ 𝐷))) ⊆ (ℂ ∖ {0})
87	86	sseli 3759	. . . . . . . 8 ⊢ (0 ∈ ran (ℂ D (exp ↾ (log “ 𝐷))) → 0 ∈ (ℂ ∖ {0}))
88		eldifsn 4474	. . . . . . . 8 ⊢ (0 ∈ (ℂ ∖ {0}) ↔ (0 ∈ ℂ ∧ 0 ≠ 0))
89	87, 88	sylib 209	. . . . . . 7 ⊢ (0 ∈ ran (ℂ D (exp ↾ (log “ 𝐷))) → (0 ∈ ℂ ∧ 0 ≠ 0))
90	89	simprd 489	. . . . . 6 ⊢ (0 ∈ ran (ℂ D (exp ↾ (log “ 𝐷))) → 0 ≠ 0)
91	77, 90	mto 188	. . . . 5 ⊢ ¬ 0 ∈ ran (ℂ D (exp ↾ (log “ 𝐷)))
92	91	a1i 11	. . . 4 ⊢ (⊤ → ¬ 0 ∈ ran (ℂ D (exp ↾ (log “ 𝐷))))
93	1, 3, 5, 8, 42, 58, 76, 92	dvcnv 24045	. . 3 ⊢ (⊤ → (ℂ D ^◡(exp ↾ (log “ 𝐷))) = (𝑥 ∈ 𝐷 ↦ (1 / ((ℂ D (exp ↾ (log “ 𝐷)))‘(^◡(exp ↾ (log “ 𝐷))‘𝑥)))))
94	93	mptru 1660	. 2 ⊢ (ℂ D ^◡(exp ↾ (log “ 𝐷))) = (𝑥 ∈ 𝐷 ↦ (1 / ((ℂ D (exp ↾ (log “ 𝐷)))‘(^◡(exp ↾ (log “ 𝐷))‘𝑥))))
95	47	oveq2i 6857	. 2 ⊢ (ℂ D ^◡(exp ↾ (log “ 𝐷))) = (ℂ D (log ↾ 𝐷))
96	68	fveq1i 6380	. . . . 5 ⊢ ((ℂ D (exp ↾ (log “ 𝐷)))‘(^◡(exp ↾ (log “ 𝐷))‘𝑥)) = ((exp ↾ (log “ 𝐷))‘(^◡(exp ↾ (log “ 𝐷))‘𝑥))
97		f1ocnvfv2 6729	. . . . . 6 ⊢ (((exp ↾ (log “ 𝐷)):(log “ 𝐷)–1-1-onto→𝐷 ∧ 𝑥 ∈ 𝐷) → ((exp ↾ (log “ 𝐷))‘(^◡(exp ↾ (log “ 𝐷))‘𝑥)) = 𝑥)
98	41, 97	mpan 681	. . . . 5 ⊢ (𝑥 ∈ 𝐷 → ((exp ↾ (log “ 𝐷))‘(^◡(exp ↾ (log “ 𝐷))‘𝑥)) = 𝑥)
99	96, 98	syl5eq 2811	. . . 4 ⊢ (𝑥 ∈ 𝐷 → ((ℂ D (exp ↾ (log “ 𝐷)))‘(^◡(exp ↾ (log “ 𝐷))‘𝑥)) = 𝑥)
100	99	oveq2d 6862	. . 3 ⊢ (𝑥 ∈ 𝐷 → (1 / ((ℂ D (exp ↾ (log “ 𝐷)))‘(^◡(exp ↾ (log “ 𝐷))‘𝑥))) = (1 / 𝑥))
101	100	mpteq2ia 4901	. 2 ⊢ (𝑥 ∈ 𝐷 ↦ (1 / ((ℂ D (exp ↾ (log “ 𝐷)))‘(^◡(exp ↾ (log “ 𝐷))‘𝑥)))) = (𝑥 ∈ 𝐷 ↦ (1 / 𝑥))
102	94, 95, 101	3eqtr3i 2795	1 ⊢ (ℂ D (log ↾ 𝐷)) = (𝑥 ∈ 𝐷 ↦ (1 / 𝑥))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 ↔ wb 197 ∧ wa 384 = wceq 1652 ⊤wtru 1653 ∈ wcel 2155 ≠ wne 2937 ∖ cdif 3731 ∩ cin 3733 ⊆ wss 3734 {csn 4336 {cpr 4338 ↦ cmpt 4890 ^◡ccnv 5278 dom cdm 5279 ran crn 5280 ↾ cres 5281 “ cima 5282 Rel wrel 5284 Fun wfun 6064 ⟶wf 6066 –1-1→wf1 6067 –1-1-onto→wf1o 6069 ‘cfv 6070 (class class class)co 6846 ℂcc 10191 ℝcr 10192 0cc0 10193 1c1 10194 -∞cmnf 10330 -cneg 10525 / cdiv 10942 (,]cioc 12383 ℑcim 14137 expce 15088 πcpi 15093 TopOpenctopn 16362 ℂ_fldccnfld 20033 Topctop 20991 intcnt 21115 –cn→ccncf 22972 D cdv 23932 logclog 24606

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1890 ax-4 1904 ax-5 2005 ax-6 2070 ax-7 2105 ax-8 2157 ax-9 2164 ax-10 2183 ax-11 2198 ax-12 2211 ax-13 2352 ax-ext 2743 ax-rep 4932 ax-sep 4943 ax-nul 4951 ax-pow 5003 ax-pr 5064 ax-un 7151 ax-inf2 8757 ax-cnex 10249 ax-resscn 10250 ax-1cn 10251 ax-icn 10252 ax-addcl 10253 ax-addrcl 10254 ax-mulcl 10255 ax-mulrcl 10256 ax-mulcom 10257 ax-addass 10258 ax-mulass 10259 ax-distr 10260 ax-i2m1 10261 ax-1ne0 10262 ax-1rid 10263 ax-rnegex 10264 ax-rrecex 10265 ax-cnre 10266 ax-pre-lttri 10267 ax-pre-lttrn 10268 ax-pre-ltadd 10269 ax-pre-mulgt0 10270 ax-pre-sup 10271 ax-addf 10272 ax-mulf 10273

This theorem depends on definitions: df-bi 198 df-an 385 df-or 874 df-3or 1108 df-3an 1109 df-tru 1656 df-fal 1666 df-ex 1875 df-nf 1879 df-sb 2063 df-mo 2565 df-eu 2582 df-clab 2752 df-cleq 2758 df-clel 2761 df-nfc 2896 df-ne 2938 df-nel 3041 df-ral 3060 df-rex 3061 df-reu 3062 df-rmo 3063 df-rab 3064 df-v 3352 df-sbc 3599 df-csb 3694 df-dif 3737 df-un 3739 df-in 3741 df-ss 3748 df-pss 3750 df-nul 4082 df-if 4246 df-pw 4319 df-sn 4337 df-pr 4339 df-tp 4341 df-op 4343 df-uni 4597 df-int 4636 df-iun 4680 df-iin 4681 df-br 4812 df-opab 4874 df-mpt 4891 df-tr 4914 df-id 5187 df-eprel 5192 df-po 5200 df-so 5201 df-fr 5238 df-se 5239 df-we 5240 df-xp 5285 df-rel 5286 df-cnv 5287 df-co 5288 df-dm 5289 df-rn 5290 df-res 5291 df-ima 5292 df-pred 5867 df-ord 5913 df-on 5914 df-lim 5915 df-suc 5916 df-iota 6033 df-fun 6072 df-fn 6073 df-f 6074 df-f1 6075 df-fo 6076 df-f1o 6077 df-fv 6078 df-isom 6079 df-riota 6807 df-ov 6849 df-oprab 6850 df-mpt2 6851 df-of 7099 df-om 7268 df-1st 7370 df-2nd 7371 df-supp 7502 df-wrecs 7614 df-recs 7676 df-rdg 7714 df-1o 7768 df-2o 7769 df-oadd 7772 df-er 7951 df-map 8066 df-pm 8067 df-ixp 8118 df-en 8165 df-dom 8166 df-sdom 8167 df-fin 8168 df-fsupp 8487 df-fi 8528 df-sup 8559 df-inf 8560 df-oi 8626 df-card 9020 df-cda 9247 df-pnf 10334 df-mnf 10335 df-xr 10336 df-ltxr 10337 df-le 10338 df-sub 10526 df-neg 10527 df-div 10943 df-nn 11279 df-2 11339 df-3 11340 df-4 11341 df-5 11342 df-6 11343 df-7 11344 df-8 11345 df-9 11346 df-n0 11543 df-z 11629 df-dec 11746 df-uz 11892 df-q 11995 df-rp 12034 df-xneg 12151 df-xadd 12152 df-xmul 12153 df-ioo 12386 df-ioc 12387 df-ico 12388 df-icc 12389 df-fz 12539 df-fzo 12679 df-fl 12806 df-mod 12882 df-seq 13014 df-exp 13073 df-fac 13270 df-bc 13299 df-hash 13327 df-shft 14106 df-cj 14138 df-re 14139 df-im 14140 df-sqrt 14274 df-abs 14275 df-limsup 14501 df-clim 14518 df-rlim 14519 df-sum 14716 df-ef 15094 df-sin 15096 df-cos 15097 df-tan 15098 df-pi 15099 df-struct 16146 df-ndx 16147 df-slot 16148 df-base 16150 df-sets 16151 df-ress 16152 df-plusg 16241 df-mulr 16242 df-starv 16243 df-sca 16244 df-vsca 16245 df-ip 16246 df-tset 16247 df-ple 16248 df-ds 16250 df-unif 16251 df-hom 16252 df-cco 16253 df-rest 16363 df-topn 16364 df-0g 16382 df-gsum 16383 df-topgen 16384 df-pt 16385 df-prds 16388 df-xrs 16442 df-qtop 16447 df-imas 16448 df-xps 16450 df-mre 16526 df-mrc 16527 df-acs 16529 df-mgm 17522 df-sgrp 17564 df-mnd 17575 df-submnd 17616 df-mulg 17822 df-cntz 18027 df-cmn 18475 df-psmet 20025 df-xmet 20026 df-met 20027 df-bl 20028 df-mopn 20029 df-fbas 20030 df-fg 20031 df-cnfld 20034 df-top 20992 df-topon 21009 df-topsp 21031 df-bases 21044 df-cld 21117 df-ntr 21118 df-cls 21119 df-nei 21196 df-lp 21234 df-perf 21235 df-cn 21325 df-cnp 21326 df-haus 21413 df-cmp 21484 df-tx 21659 df-hmeo 21852 df-fil 21943 df-fm 22035 df-flim 22036 df-flf 22037 df-xms 22418 df-ms 22419 df-tms 22420 df-cncf 22974 df-limc 23935 df-dv 23936 df-log 24608

This theorem is referenced by: dvlog2 24704 dvcncxp1 24789 dvatan 24967 lgamgulmlem2 25061 dvasin 33940

W3C validator