logdivsum - Metamath Proof Explorer

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

Theorem logdivsum 27453

Description: Asymptotic analysis of Σ𝑛 ≤ 𝑥, log𝑛 / 𝑛 = (log𝑥)↑2 / 2 + 𝐿 + 𝑂(log𝑥 / 𝑥). (Contributed by Mario Carneiro, 18-May-2016.)

**Hypothesis**
Ref	Expression
logdivsum.1	⊢ 𝐹 = (𝑦 ∈ ℝ⁺ ↦ (Σ𝑖 ∈ (1...(⌊‘𝑦))((log‘𝑖) / 𝑖) − (((log‘𝑦)↑2) / 2)))

**Assertion**
Ref	Expression
logdivsum	⊢ (𝐹:ℝ⁺⟶ℝ ∧ 𝐹 ∈ dom ⇝_𝑟 ∧ ((𝐹 ⇝_𝑟 𝐿 ∧ 𝐴 ∈ ℝ⁺ ∧ e ≤ 𝐴) → (abs‘((𝐹‘𝐴) − 𝐿)) ≤ ((log‘𝐴) / 𝐴)))

Distinct variable group: 𝑦,𝑖,𝐴 Allowed substitution hints: 𝐹(𝑦,𝑖) 𝐿(𝑦,𝑖)

Proof of Theorem logdivsum Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ioorp 13426	. . . 4 ⊢ (0(,)+∞) = ℝ⁺
2	1	eqcomi 2736	. . 3 ⊢ ℝ⁺ = (0(,)+∞)
3		nnuz 12887	. . 3 ⊢ ℕ = (ℤ_≥‘1)
4		1zzd 12615	. . 3 ⊢ (⊤ → 1 ∈ ℤ)
5		ere 16057	. . . 4 ⊢ e ∈ ℝ
6	5	a1i 11	. . 3 ⊢ (⊤ → e ∈ ℝ)
7		0re 11238	. . . . . 6 ⊢ 0 ∈ ℝ
8		epos 16175	. . . . . 6 ⊢ 0 < e
9	7, 5, 8	ltleii 11359	. . . . 5 ⊢ 0 ≤ e
10	9	a1i 11	. . . 4 ⊢ (⊤ → 0 ≤ e)
11		1re 11236	. . . . 5 ⊢ 1 ∈ ℝ
12		addge02 11747	. . . . 5 ⊢ ((1 ∈ ℝ ∧ e ∈ ℝ) → (0 ≤ e ↔ 1 ≤ (e + 1)))
13	11, 5, 12	mp2an 691	. . . 4 ⊢ (0 ≤ e ↔ 1 ≤ (e + 1))
14	10, 13	sylib 217	. . 3 ⊢ (⊤ → 1 ≤ (e + 1))
15	7	a1i 11	. . 3 ⊢ (⊤ → 0 ∈ ℝ)
16		relogcl 26496	. . . . . 6 ⊢ (𝑦 ∈ ℝ⁺ → (log‘𝑦) ∈ ℝ)
17	16	adantl 481	. . . . 5 ⊢ ((⊤ ∧ 𝑦 ∈ ℝ⁺) → (log‘𝑦) ∈ ℝ)
18	17	resqcld 14113	. . . 4 ⊢ ((⊤ ∧ 𝑦 ∈ ℝ⁺) → ((log‘𝑦)↑2) ∈ ℝ)
19	18	rehalfcld 12481	. . 3 ⊢ ((⊤ ∧ 𝑦 ∈ ℝ⁺) → (((log‘𝑦)↑2) / 2) ∈ ℝ)
20		rerpdivcl 13028	. . . . 5 ⊢ (((log‘𝑦) ∈ ℝ ∧ 𝑦 ∈ ℝ⁺) → ((log‘𝑦) / 𝑦) ∈ ℝ)
21	16, 20	mpancom 687	. . . 4 ⊢ (𝑦 ∈ ℝ⁺ → ((log‘𝑦) / 𝑦) ∈ ℝ)
22	21	adantl 481	. . 3 ⊢ ((⊤ ∧ 𝑦 ∈ ℝ⁺) → ((log‘𝑦) / 𝑦) ∈ ℝ)
23		nnrp 13009	. . . 4 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℝ⁺)
24	23, 22	sylan2 592	. . 3 ⊢ ((⊤ ∧ 𝑦 ∈ ℕ) → ((log‘𝑦) / 𝑦) ∈ ℝ)
25		reelprrecn 11222	. . . . . 6 ⊢ ℝ ∈ {ℝ, ℂ}
26	25	a1i 11	. . . . 5 ⊢ (⊤ → ℝ ∈ {ℝ, ℂ})
27		cnelprrecn 11223	. . . . . 6 ⊢ ℂ ∈ {ℝ, ℂ}
28	27	a1i 11	. . . . 5 ⊢ (⊤ → ℂ ∈ {ℝ, ℂ})
29	17	recnd 11264	. . . . 5 ⊢ ((⊤ ∧ 𝑦 ∈ ℝ⁺) → (log‘𝑦) ∈ ℂ)
30		ovexd 7449	. . . . 5 ⊢ ((⊤ ∧ 𝑦 ∈ ℝ⁺) → (1 / 𝑦) ∈ V)
31		sqcl 14106	. . . . . . 7 ⊢ (𝑥 ∈ ℂ → (𝑥↑2) ∈ ℂ)
32	31	adantl 481	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → (𝑥↑2) ∈ ℂ)
33	32	halfcld 12479	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → ((𝑥↑2) / 2) ∈ ℂ)
34		simpr 484	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → 𝑥 ∈ ℂ)
35		relogf1o 26487	. . . . . . . . . 10 ⊢ (log ↾ ℝ⁺):ℝ⁺–1-1-onto→ℝ
36		f1of 6833	. . . . . . . . . 10 ⊢ ((log ↾ ℝ⁺):ℝ⁺–1-1-onto→ℝ → (log ↾ ℝ⁺):ℝ⁺⟶ℝ)
37	35, 36	mp1i 13	. . . . . . . . 9 ⊢ (⊤ → (log ↾ ℝ⁺):ℝ⁺⟶ℝ)
38	37	feqmptd 6961	. . . . . . . 8 ⊢ (⊤ → (log ↾ ℝ⁺) = (𝑦 ∈ ℝ⁺ ↦ ((log ↾ ℝ⁺)‘𝑦)))
39		fvres 6910	. . . . . . . . 9 ⊢ (𝑦 ∈ ℝ⁺ → ((log ↾ ℝ⁺)‘𝑦) = (log‘𝑦))
40	39	mpteq2ia 5245	. . . . . . . 8 ⊢ (𝑦 ∈ ℝ⁺ ↦ ((log ↾ ℝ⁺)‘𝑦)) = (𝑦 ∈ ℝ⁺ ↦ (log‘𝑦))
41	38, 40	eqtrdi 2783	. . . . . . 7 ⊢ (⊤ → (log ↾ ℝ⁺) = (𝑦 ∈ ℝ⁺ ↦ (log‘𝑦)))
42	41	oveq2d 7430	. . . . . 6 ⊢ (⊤ → (ℝ D (log ↾ ℝ⁺)) = (ℝ D (𝑦 ∈ ℝ⁺ ↦ (log‘𝑦))))
43		dvrelog 26558	. . . . . 6 ⊢ (ℝ D (log ↾ ℝ⁺)) = (𝑦 ∈ ℝ⁺ ↦ (1 / 𝑦))
44	42, 43	eqtr3di 2782	. . . . 5 ⊢ (⊤ → (ℝ D (𝑦 ∈ ℝ⁺ ↦ (log‘𝑦))) = (𝑦 ∈ ℝ⁺ ↦ (1 / 𝑦)))
45		ovexd 7449	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → (2 · 𝑥) ∈ V)
46		2nn 12307	. . . . . . . . 9 ⊢ 2 ∈ ℕ
47		dvexp 25872	. . . . . . . . 9 ⊢ (2 ∈ ℕ → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · (𝑥↑(2 − 1)))))
48	46, 47	mp1i 13	. . . . . . . 8 ⊢ (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · (𝑥↑(2 − 1)))))
49		2m1e1 12360	. . . . . . . . . . . 12 ⊢ (2 − 1) = 1
50	49	oveq2i 7425	. . . . . . . . . . 11 ⊢ (𝑥↑(2 − 1)) = (𝑥↑1)
51		exp1 14056	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℂ → (𝑥↑1) = 𝑥)
52	51	adantl 481	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → (𝑥↑1) = 𝑥)
53	50, 52	eqtrid 2779	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → (𝑥↑(2 − 1)) = 𝑥)
54	53	oveq2d 7430	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → (2 · (𝑥↑(2 − 1))) = (2 · 𝑥))
55	54	mpteq2dva 5242	. . . . . . . 8 ⊢ (⊤ → (𝑥 ∈ ℂ ↦ (2 · (𝑥↑(2 − 1)))) = (𝑥 ∈ ℂ ↦ (2 · 𝑥)))
56	48, 55	eqtrd 2767	. . . . . . 7 ⊢ (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑2))) = (𝑥 ∈ ℂ ↦ (2 · 𝑥)))
57		2cnd 12312	. . . . . . 7 ⊢ (⊤ → 2 ∈ ℂ)
58		2ne0 12338	. . . . . . . 8 ⊢ 2 ≠ 0
59	58	a1i 11	. . . . . . 7 ⊢ (⊤ → 2 ≠ 0)
60	28, 32, 45, 56, 57, 59	dvmptdivc 25884	. . . . . 6 ⊢ (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ ((𝑥↑2) / 2))) = (𝑥 ∈ ℂ ↦ ((2 · 𝑥) / 2)))
61		2cn 12309	. . . . . . . . 9 ⊢ 2 ∈ ℂ
62		divcan3 11920	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → ((2 · 𝑥) / 2) = 𝑥)
63	61, 58, 62	mp3an23 1450	. . . . . . . 8 ⊢ (𝑥 ∈ ℂ → ((2 · 𝑥) / 2) = 𝑥)
64	63	adantl 481	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → ((2 · 𝑥) / 2) = 𝑥)
65	64	mpteq2dva 5242	. . . . . 6 ⊢ (⊤ → (𝑥 ∈ ℂ ↦ ((2 · 𝑥) / 2)) = (𝑥 ∈ ℂ ↦ 𝑥))
66	60, 65	eqtrd 2767	. . . . 5 ⊢ (⊤ → (ℂ D (𝑥 ∈ ℂ ↦ ((𝑥↑2) / 2))) = (𝑥 ∈ ℂ ↦ 𝑥))
67		oveq1 7421	. . . . . 6 ⊢ (𝑥 = (log‘𝑦) → (𝑥↑2) = ((log‘𝑦)↑2))
68	67	oveq1d 7429	. . . . 5 ⊢ (𝑥 = (log‘𝑦) → ((𝑥↑2) / 2) = (((log‘𝑦)↑2) / 2))
69		id 22	. . . . 5 ⊢ (𝑥 = (log‘𝑦) → 𝑥 = (log‘𝑦))
70	26, 28, 29, 30, 33, 34, 44, 66, 68, 69	dvmptco 25891	. . . 4 ⊢ (⊤ → (ℝ D (𝑦 ∈ ℝ⁺ ↦ (((log‘𝑦)↑2) / 2))) = (𝑦 ∈ ℝ⁺ ↦ ((log‘𝑦) · (1 / 𝑦))))
71		rpcn 13008	. . . . . . 7 ⊢ (𝑦 ∈ ℝ⁺ → 𝑦 ∈ ℂ)
72	71	adantl 481	. . . . . 6 ⊢ ((⊤ ∧ 𝑦 ∈ ℝ⁺) → 𝑦 ∈ ℂ)
73		rpne0 13014	. . . . . . 7 ⊢ (𝑦 ∈ ℝ⁺ → 𝑦 ≠ 0)
74	73	adantl 481	. . . . . 6 ⊢ ((⊤ ∧ 𝑦 ∈ ℝ⁺) → 𝑦 ≠ 0)
75	29, 72, 74	divrecd 12015	. . . . 5 ⊢ ((⊤ ∧ 𝑦 ∈ ℝ⁺) → ((log‘𝑦) / 𝑦) = ((log‘𝑦) · (1 / 𝑦)))
76	75	mpteq2dva 5242	. . . 4 ⊢ (⊤ → (𝑦 ∈ ℝ⁺ ↦ ((log‘𝑦) / 𝑦)) = (𝑦 ∈ ℝ⁺ ↦ ((log‘𝑦) · (1 / 𝑦))))
77	70, 76	eqtr4d 2770	. . 3 ⊢ (⊤ → (ℝ D (𝑦 ∈ ℝ⁺ ↦ (((log‘𝑦)↑2) / 2))) = (𝑦 ∈ ℝ⁺ ↦ ((log‘𝑦) / 𝑦)))
78		fveq2 6891	. . . 4 ⊢ (𝑦 = 𝑖 → (log‘𝑦) = (log‘𝑖))
79		id 22	. . . 4 ⊢ (𝑦 = 𝑖 → 𝑦 = 𝑖)
80	78, 79	oveq12d 7432	. . 3 ⊢ (𝑦 = 𝑖 → ((log‘𝑦) / 𝑦) = ((log‘𝑖) / 𝑖))
81		simp3r 1200	. . . 4 ⊢ ((⊤ ∧ (𝑦 ∈ ℝ⁺ ∧ 𝑖 ∈ ℝ⁺) ∧ (e ≤ 𝑦 ∧ 𝑦 ≤ 𝑖)) → 𝑦 ≤ 𝑖)
82		simp2l 1197	. . . . . 6 ⊢ ((⊤ ∧ (𝑦 ∈ ℝ⁺ ∧ 𝑖 ∈ ℝ⁺) ∧ (e ≤ 𝑦 ∧ 𝑦 ≤ 𝑖)) → 𝑦 ∈ ℝ⁺)
83	82	rpred 13040	. . . . 5 ⊢ ((⊤ ∧ (𝑦 ∈ ℝ⁺ ∧ 𝑖 ∈ ℝ⁺) ∧ (e ≤ 𝑦 ∧ 𝑦 ≤ 𝑖)) → 𝑦 ∈ ℝ)
84		simp3l 1199	. . . . 5 ⊢ ((⊤ ∧ (𝑦 ∈ ℝ⁺ ∧ 𝑖 ∈ ℝ⁺) ∧ (e ≤ 𝑦 ∧ 𝑦 ≤ 𝑖)) → e ≤ 𝑦)
85		simp2r 1198	. . . . . 6 ⊢ ((⊤ ∧ (𝑦 ∈ ℝ⁺ ∧ 𝑖 ∈ ℝ⁺) ∧ (e ≤ 𝑦 ∧ 𝑦 ≤ 𝑖)) → 𝑖 ∈ ℝ⁺)
86	85	rpred 13040	. . . . 5 ⊢ ((⊤ ∧ (𝑦 ∈ ℝ⁺ ∧ 𝑖 ∈ ℝ⁺) ∧ (e ≤ 𝑦 ∧ 𝑦 ≤ 𝑖)) → 𝑖 ∈ ℝ)
87	5	a1i 11	. . . . . 6 ⊢ ((⊤ ∧ (𝑦 ∈ ℝ⁺ ∧ 𝑖 ∈ ℝ⁺) ∧ (e ≤ 𝑦 ∧ 𝑦 ≤ 𝑖)) → e ∈ ℝ)
88	87, 83, 86, 84, 81	letrd 11393	. . . . 5 ⊢ ((⊤ ∧ (𝑦 ∈ ℝ⁺ ∧ 𝑖 ∈ ℝ⁺) ∧ (e ≤ 𝑦 ∧ 𝑦 ≤ 𝑖)) → e ≤ 𝑖)
89		logdivle 26543	. . . . 5 ⊢ (((𝑦 ∈ ℝ ∧ e ≤ 𝑦) ∧ (𝑖 ∈ ℝ ∧ e ≤ 𝑖)) → (𝑦 ≤ 𝑖 ↔ ((log‘𝑖) / 𝑖) ≤ ((log‘𝑦) / 𝑦)))
90	83, 84, 86, 88, 89	syl22anc 838	. . . 4 ⊢ ((⊤ ∧ (𝑦 ∈ ℝ⁺ ∧ 𝑖 ∈ ℝ⁺) ∧ (e ≤ 𝑦 ∧ 𝑦 ≤ 𝑖)) → (𝑦 ≤ 𝑖 ↔ ((log‘𝑖) / 𝑖) ≤ ((log‘𝑦) / 𝑦)))
91	81, 90	mpbid 231	. . 3 ⊢ ((⊤ ∧ (𝑦 ∈ ℝ⁺ ∧ 𝑖 ∈ ℝ⁺) ∧ (e ≤ 𝑦 ∧ 𝑦 ≤ 𝑖)) → ((log‘𝑖) / 𝑖) ≤ ((log‘𝑦) / 𝑦))
92		logdivsum.1	. . 3 ⊢ 𝐹 = (𝑦 ∈ ℝ⁺ ↦ (Σ𝑖 ∈ (1...(⌊‘𝑦))((log‘𝑖) / 𝑖) − (((log‘𝑦)↑2) / 2)))
93	71	cxp1d 26627	. . . . . 6 ⊢ (𝑦 ∈ ℝ⁺ → (𝑦↑_𝑐1) = 𝑦)
94	93	oveq2d 7430	. . . . 5 ⊢ (𝑦 ∈ ℝ⁺ → ((log‘𝑦) / (𝑦↑_𝑐1)) = ((log‘𝑦) / 𝑦))
95	94	mpteq2ia 5245	. . . 4 ⊢ (𝑦 ∈ ℝ⁺ ↦ ((log‘𝑦) / (𝑦↑_𝑐1))) = (𝑦 ∈ ℝ⁺ ↦ ((log‘𝑦) / 𝑦))
96		1rp 13002	. . . . 5 ⊢ 1 ∈ ℝ⁺
97		cxploglim 26897	. . . . 5 ⊢ (1 ∈ ℝ⁺ → (𝑦 ∈ ℝ⁺ ↦ ((log‘𝑦) / (𝑦↑_𝑐1))) ⇝_𝑟 0)
98	96, 97	mp1i 13	. . . 4 ⊢ (⊤ → (𝑦 ∈ ℝ⁺ ↦ ((log‘𝑦) / (𝑦↑_𝑐1))) ⇝_𝑟 0)
99	95, 98	eqbrtrrid 5178	. . 3 ⊢ (⊤ → (𝑦 ∈ ℝ⁺ ↦ ((log‘𝑦) / 𝑦)) ⇝_𝑟 0)
100		fveq2 6891	. . . 4 ⊢ (𝑦 = 𝐴 → (log‘𝑦) = (log‘𝐴))
101		id 22	. . . 4 ⊢ (𝑦 = 𝐴 → 𝑦 = 𝐴)
102	100, 101	oveq12d 7432	. . 3 ⊢ (𝑦 = 𝐴 → ((log‘𝑦) / 𝑦) = ((log‘𝐴) / 𝐴))
103	2, 3, 4, 6, 14, 15, 19, 22, 24, 77, 80, 91, 92, 99, 102	dvfsumrlim3 25955	. 2 ⊢ (⊤ → (𝐹:ℝ⁺⟶ℝ ∧ 𝐹 ∈ dom ⇝_𝑟 ∧ ((𝐹 ⇝_𝑟 𝐿 ∧ 𝐴 ∈ ℝ⁺ ∧ e ≤ 𝐴) → (abs‘((𝐹‘𝐴) − 𝐿)) ≤ ((log‘𝐴) / 𝐴))))
104	103	mptru 1541	1 ⊢ (𝐹:ℝ⁺⟶ℝ ∧ 𝐹 ∈ dom ⇝_𝑟 ∧ ((𝐹 ⇝_𝑟 𝐿 ∧ 𝐴 ∈ ℝ⁺ ∧ e ≤ 𝐴) → (abs‘((𝐹‘𝐴) − 𝐿)) ≤ ((log‘𝐴) / 𝐴)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 ∧ w3a 1085 = wceq 1534 ⊤wtru 1535 ∈ wcel 2099 ≠ wne 2935 Vcvv 3469 {cpr 4626 class class class wbr 5142 ↦ cmpt 5225 dom cdm 5672 ↾ cres 5674 ⟶wf 6538 –1-1-onto→wf1o 6541 ‘cfv 6542 (class class class)co 7414 ℂcc 11128 ℝcr 11129 0cc0 11130 1c1 11131 + caddc 11133 · cmul 11135 +∞cpnf 11267 ≤ cle 11271 − cmin 11466 / cdiv 11893 ℕcn 12234 2c2 12289 ℝ⁺crp 12998 (,)cioo 13348 ...cfz 13508 ⌊cfl 13779 ↑cexp 14050 abscabs 15205 ⇝_𝑟 crli 15453 Σcsu 15656 eceu 16030 D cdv 25779 logclog 26475 ↑_𝑐ccxp 26476

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2164 ax-ext 2698 ax-rep 5279 ax-sep 5293 ax-nul 5300 ax-pow 5359 ax-pr 5423 ax-un 7734 ax-inf2 9656 ax-cnex 11186 ax-resscn 11187 ax-1cn 11188 ax-icn 11189 ax-addcl 11190 ax-addrcl 11191 ax-mulcl 11192 ax-mulrcl 11193 ax-mulcom 11194 ax-addass 11195 ax-mulass 11196 ax-distr 11197 ax-i2m1 11198 ax-1ne0 11199 ax-1rid 11200 ax-rnegex 11201 ax-rrecex 11202 ax-cnre 11203 ax-pre-lttri 11204 ax-pre-lttrn 11205 ax-pre-ltadd 11206 ax-pre-mulgt0 11207 ax-pre-sup 11208 ax-addf 11209

This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3or 1086 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2705 df-cleq 2719 df-clel 2805 df-nfc 2880 df-ne 2936 df-nel 3042 df-ral 3057 df-rex 3066 df-rmo 3371 df-reu 3372 df-rab 3428 df-v 3471 df-sbc 3775 df-csb 3890 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-pss 3963 df-nul 4319 df-if 4525 df-pw 4600 df-sn 4625 df-pr 4627 df-tp 4629 df-op 4631 df-uni 4904 df-int 4945 df-iun 4993 df-iin 4994 df-br 5143 df-opab 5205 df-mpt 5226 df-tr 5260 df-id 5570 df-eprel 5576 df-po 5584 df-so 5585 df-fr 5627 df-se 5628 df-we 5629 df-xp 5678 df-rel 5679 df-cnv 5680 df-co 5681 df-dm 5682 df-rn 5683 df-res 5684 df-ima 5685 df-pred 6299 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-isom 6551 df-riota 7370 df-ov 7417 df-oprab 7418 df-mpo 7419 df-of 7679 df-om 7865 df-1st 7987 df-2nd 7988 df-supp 8160 df-frecs 8280 df-wrecs 8311 df-recs 8385 df-rdg 8424 df-1o 8480 df-2o 8481 df-er 8718 df-map 8838 df-pm 8839 df-ixp 8908 df-en 8956 df-dom 8957 df-sdom 8958 df-fin 8959 df-fsupp 9378 df-fi 9426 df-sup 9457 df-inf 9458 df-oi 9525 df-card 9954 df-pnf 11272 df-mnf 11273 df-xr 11274 df-ltxr 11275 df-le 11276 df-sub 11468 df-neg 11469 df-div 11894 df-nn 12235 df-2 12297 df-3 12298 df-4 12299 df-5 12300 df-6 12301 df-7 12302 df-8 12303 df-9 12304 df-n0 12495 df-z 12581 df-dec 12700 df-uz 12845 df-q 12955 df-rp 12999 df-xneg 13116 df-xadd 13117 df-xmul 13118 df-ioo 13352 df-ioc 13353 df-ico 13354 df-icc 13355 df-fz 13509 df-fzo 13652 df-fl 13781 df-mod 13859 df-seq 13991 df-exp 14051 df-fac 14257 df-bc 14286 df-hash 14314 df-shft 15038 df-cj 15070 df-re 15071 df-im 15072 df-sqrt 15206 df-abs 15207 df-limsup 15439 df-clim 15456 df-rlim 15457 df-sum 15657 df-ef 16035 df-e 16036 df-sin 16037 df-cos 16038 df-pi 16040 df-struct 17107 df-sets 17124 df-slot 17142 df-ndx 17154 df-base 17172 df-ress 17201 df-plusg 17237 df-mulr 17238 df-starv 17239 df-sca 17240 df-vsca 17241 df-ip 17242 df-tset 17243 df-ple 17244 df-ds 17246 df-unif 17247 df-hom 17248 df-cco 17249 df-rest 17395 df-topn 17396 df-0g 17414 df-gsum 17415 df-topgen 17416 df-pt 17417 df-prds 17420 df-xrs 17475 df-qtop 17480 df-imas 17481 df-xps 17483 df-mre 17557 df-mrc 17558 df-acs 17560 df-mgm 18591 df-sgrp 18670 df-mnd 18686 df-submnd 18732 df-mulg 19015 df-cntz 19259 df-cmn 19728 df-psmet 21258 df-xmet 21259 df-met 21260 df-bl 21261 df-mopn 21262 df-fbas 21263 df-fg 21264 df-cnfld 21267 df-top 22783 df-topon 22800 df-topsp 22822 df-bases 22836 df-cld 22910 df-ntr 22911 df-cls 22912 df-nei 22989 df-lp 23027 df-perf 23028 df-cn 23118 df-cnp 23119 df-haus 23206 df-cmp 23278 df-tx 23453 df-hmeo 23646 df-fil 23737 df-fm 23829 df-flim 23830 df-flf 23831 df-xms 24213 df-ms 24214 df-tms 24215 df-cncf 24785 df-limc 25782 df-dv 25783 df-log 26477 df-cxp 26478

This theorem is referenced by: mulog2sumlem1 27454 mulog2sum 27457 vmalogdivsum2 27458

W3C validator