vmadivsum - Metamath Proof Explorer

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

Theorem vmadivsum 26628

Description: The sum of the von Mangoldt function over 𝑛 is asymptotic to log𝑥 + 𝑂(1). Equation 9.2.13 of [Shapiro], p. 331. (Contributed by Mario Carneiro, 16-Apr-2016.)

**Assertion**
Ref	Expression
vmadivsum	⊢ (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1)

Distinct variable group: 𝑥,𝑛

**Proof of Theorem vmadivsum**
Step	Hyp	Ref	Expression
1		reex 10963	. . . . . . 7 ⊢ ℝ ∈ V
2		rpssre 12736	. . . . . . 7 ⊢ ℝ⁺ ⊆ ℝ
3	1, 2	ssexi 5250	. . . . . 6 ⊢ ℝ⁺ ∈ V
4	3	a1i 11	. . . . 5 ⊢ (⊤ → ℝ⁺ ∈ V)
5		ovexd 7306	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − ((log‘(!‘(⌊‘𝑥))) / 𝑥)) ∈ V)
6		ovexd 7306	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((log‘𝑥) − ((log‘(!‘(⌊‘𝑥))) / 𝑥)) ∈ V)
7		eqidd 2741	. . . . 5 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − ((log‘(!‘(⌊‘𝑥))) / 𝑥))) = (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − ((log‘(!‘(⌊‘𝑥))) / 𝑥))))
8		eqidd 2741	. . . . 5 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ ((log‘𝑥) − ((log‘(!‘(⌊‘𝑥))) / 𝑥))) = (𝑥 ∈ ℝ⁺ ↦ ((log‘𝑥) − ((log‘(!‘(⌊‘𝑥))) / 𝑥))))
9	4, 5, 6, 7, 8	offval2 7547	. . . 4 ⊢ (⊤ → ((𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − ((log‘(!‘(⌊‘𝑥))) / 𝑥))) ∘_f − (𝑥 ∈ ℝ⁺ ↦ ((log‘𝑥) − ((log‘(!‘(⌊‘𝑥))) / 𝑥)))) = (𝑥 ∈ ℝ⁺ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − ((log‘(!‘(⌊‘𝑥))) / 𝑥)) − ((log‘𝑥) − ((log‘(!‘(⌊‘𝑥))) / 𝑥)))))
10	9	mptru 1549	. . 3 ⊢ ((𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − ((log‘(!‘(⌊‘𝑥))) / 𝑥))) ∘_f − (𝑥 ∈ ℝ⁺ ↦ ((log‘𝑥) − ((log‘(!‘(⌊‘𝑥))) / 𝑥)))) = (𝑥 ∈ ℝ⁺ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − ((log‘(!‘(⌊‘𝑥))) / 𝑥)) − ((log‘𝑥) − ((log‘(!‘(⌊‘𝑥))) / 𝑥))))
11		fzfid 13691	. . . . . . 7 ⊢ (𝑥 ∈ ℝ⁺ → (1...(⌊‘𝑥)) ∈ Fin)
12		elfznn 13284	. . . . . . . . . 10 ⊢ (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
13	12	adantl 482	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
14		vmacl 26265	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ → (Λ‘𝑛) ∈ ℝ)
15	13, 14	syl 17	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈ ℝ)
16	15, 13	nndivred 12027	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) / 𝑛) ∈ ℝ)
17	11, 16	fsumrecl 15444	. . . . . 6 ⊢ (𝑥 ∈ ℝ⁺ → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ∈ ℝ)
18	17	recnd 11004	. . . . 5 ⊢ (𝑥 ∈ ℝ⁺ → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ∈ ℂ)
19		relogcl 25729	. . . . . 6 ⊢ (𝑥 ∈ ℝ⁺ → (log‘𝑥) ∈ ℝ)
20	19	recnd 11004	. . . . 5 ⊢ (𝑥 ∈ ℝ⁺ → (log‘𝑥) ∈ ℂ)
21		rprege0 12744	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
22		flge0nn0 13538	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → (⌊‘𝑥) ∈ ℕ₀)
23		faccl 13995	. . . . . . . . . 10 ⊢ ((⌊‘𝑥) ∈ ℕ₀ → (!‘(⌊‘𝑥)) ∈ ℕ)
24	21, 22, 23	3syl 18	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ⁺ → (!‘(⌊‘𝑥)) ∈ ℕ)
25	24	nnrpd 12769	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ⁺ → (!‘(⌊‘𝑥)) ∈ ℝ⁺)
26	25	relogcld 25776	. . . . . . 7 ⊢ (𝑥 ∈ ℝ⁺ → (log‘(!‘(⌊‘𝑥))) ∈ ℝ)
27		rerpdivcl 12759	. . . . . . 7 ⊢ (((log‘(!‘(⌊‘𝑥))) ∈ ℝ ∧ 𝑥 ∈ ℝ⁺) → ((log‘(!‘(⌊‘𝑥))) / 𝑥) ∈ ℝ)
28	26, 27	mpancom 685	. . . . . 6 ⊢ (𝑥 ∈ ℝ⁺ → ((log‘(!‘(⌊‘𝑥))) / 𝑥) ∈ ℝ)
29	28	recnd 11004	. . . . 5 ⊢ (𝑥 ∈ ℝ⁺ → ((log‘(!‘(⌊‘𝑥))) / 𝑥) ∈ ℂ)
30	18, 20, 29	nnncan2d 11367	. . . 4 ⊢ (𝑥 ∈ ℝ⁺ → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − ((log‘(!‘(⌊‘𝑥))) / 𝑥)) − ((log‘𝑥) − ((log‘(!‘(⌊‘𝑥))) / 𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)))
31	30	mpteq2ia 5182	. . 3 ⊢ (𝑥 ∈ ℝ⁺ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − ((log‘(!‘(⌊‘𝑥))) / 𝑥)) − ((log‘𝑥) − ((log‘(!‘(⌊‘𝑥))) / 𝑥)))) = (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)))
32	10, 31	eqtri 2768	. 2 ⊢ ((𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − ((log‘(!‘(⌊‘𝑥))) / 𝑥))) ∘_f − (𝑥 ∈ ℝ⁺ ↦ ((log‘𝑥) − ((log‘(!‘(⌊‘𝑥))) / 𝑥)))) = (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)))
33		1red 10977	. . . . 5 ⊢ (⊤ → 1 ∈ ℝ)
34		chpo1ub 26626	. . . . . 6 ⊢ (𝑥 ∈ ℝ⁺ ↦ ((ψ‘𝑥) / 𝑥)) ∈ 𝑂(1)
35	34	a1i 11	. . . . 5 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ ((ψ‘𝑥) / 𝑥)) ∈ 𝑂(1))
36		rpre 12737	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℝ)
37		chpcl 26271	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ → (ψ‘𝑥) ∈ ℝ)
38	36, 37	syl 17	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ⁺ → (ψ‘𝑥) ∈ ℝ)
39		rerpdivcl 12759	. . . . . . . 8 ⊢ (((ψ‘𝑥) ∈ ℝ ∧ 𝑥 ∈ ℝ⁺) → ((ψ‘𝑥) / 𝑥) ∈ ℝ)
40	38, 39	mpancom 685	. . . . . . 7 ⊢ (𝑥 ∈ ℝ⁺ → ((ψ‘𝑥) / 𝑥) ∈ ℝ)
41	40	recnd 11004	. . . . . 6 ⊢ (𝑥 ∈ ℝ⁺ → ((ψ‘𝑥) / 𝑥) ∈ ℂ)
42	41	adantl 482	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → ((ψ‘𝑥) / 𝑥) ∈ ℂ)
43	18, 29	subcld 11332	. . . . . 6 ⊢ (𝑥 ∈ ℝ⁺ → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − ((log‘(!‘(⌊‘𝑥))) / 𝑥)) ∈ ℂ)
44	43	adantl 482	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ⁺) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − ((log‘(!‘(⌊‘𝑥))) / 𝑥)) ∈ ℂ)
45	36	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ)
46	16, 45	remulcld 11006	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) / 𝑛) · 𝑥) ∈ ℝ)
47		nndivre 12014	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℕ) → (𝑥 / 𝑛) ∈ ℝ)
48	36, 12, 47	syl2an 596	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ)
49		reflcl 13514	. . . . . . . . . . . . 13 ⊢ ((𝑥 / 𝑛) ∈ ℝ → (⌊‘(𝑥 / 𝑛)) ∈ ℝ)
50	48, 49	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (⌊‘(𝑥 / 𝑛)) ∈ ℝ)
51	15, 50	remulcld 11006	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · (⌊‘(𝑥 / 𝑛))) ∈ ℝ)
52	46, 51	resubcld 11403	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((((Λ‘𝑛) / 𝑛) · 𝑥) − ((Λ‘𝑛) · (⌊‘(𝑥 / 𝑛)))) ∈ ℝ)
53	48, 50	resubcld 11403	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) ∈ ℝ)
54		1red 10977	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℝ)
55		vmage0 26268	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → 0 ≤ (Λ‘𝑛))
56	13, 55	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (Λ‘𝑛))
57		fracle1 13521	. . . . . . . . . . . . 13 ⊢ ((𝑥 / 𝑛) ∈ ℝ → ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) ≤ 1)
58	48, 57	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) ≤ 1)
59	53, 54, 15, 56, 58	lemul2ad 11915	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛)))) ≤ ((Λ‘𝑛) · 1))
60	15	recnd 11004	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈ ℂ)
61	48	recnd 11004	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℂ)
62	50	recnd 11004	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (⌊‘(𝑥 / 𝑛)) ∈ ℂ)
63	60, 61, 62	subdid 11431	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛)))) = (((Λ‘𝑛) · (𝑥 / 𝑛)) − ((Λ‘𝑛) · (⌊‘(𝑥 / 𝑛)))))
64		rpcn 12739	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℂ)
65	64	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℂ)
66	13	nnrpd 12769	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ⁺)
67		rpcnne0 12747	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℝ⁺ → (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0))
68	66, 67	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0))
69		div23 11652	. . . . . . . . . . . . . . 15 ⊢ (((Λ‘𝑛) ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → (((Λ‘𝑛) · 𝑥) / 𝑛) = (((Λ‘𝑛) / 𝑛) · 𝑥))
70		divass 11651	. . . . . . . . . . . . . . 15 ⊢ (((Λ‘𝑛) ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → (((Λ‘𝑛) · 𝑥) / 𝑛) = ((Λ‘𝑛) · (𝑥 / 𝑛)))
71	69, 70	eqtr3d 2782	. . . . . . . . . . . . . 14 ⊢ (((Λ‘𝑛) ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → (((Λ‘𝑛) / 𝑛) · 𝑥) = ((Λ‘𝑛) · (𝑥 / 𝑛)))
72	60, 65, 68, 71	syl3anc 1370	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) / 𝑛) · 𝑥) = ((Λ‘𝑛) · (𝑥 / 𝑛)))
73	72	oveq1d 7286	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((((Λ‘𝑛) / 𝑛) · 𝑥) − ((Λ‘𝑛) · (⌊‘(𝑥 / 𝑛)))) = (((Λ‘𝑛) · (𝑥 / 𝑛)) − ((Λ‘𝑛) · (⌊‘(𝑥 / 𝑛)))))
74	63, 73	eqtr4d 2783	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛)))) = ((((Λ‘𝑛) / 𝑛) · 𝑥) − ((Λ‘𝑛) · (⌊‘(𝑥 / 𝑛)))))
75	60	mulid1d 10993	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · 1) = (Λ‘𝑛))
76	59, 74, 75	3brtr3d 5110	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((((Λ‘𝑛) / 𝑛) · 𝑥) − ((Λ‘𝑛) · (⌊‘(𝑥 / 𝑛)))) ≤ (Λ‘𝑛))
77	11, 52, 15, 76	fsumle 15509	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ⁺ → Σ𝑛 ∈ (1...(⌊‘𝑥))((((Λ‘𝑛) / 𝑛) · 𝑥) − ((Λ‘𝑛) · (⌊‘(𝑥 / 𝑛)))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(Λ‘𝑛))
78	16	recnd 11004	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) / 𝑛) ∈ ℂ)
79	11, 64, 78	fsummulc1 15495	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ⁺ → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · 𝑥))
80		logfac2 26363	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → (log‘(!‘(⌊‘𝑥))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (⌊‘(𝑥 / 𝑛))))
81	21, 80	syl 17	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ⁺ → (log‘(!‘(⌊‘𝑥))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (⌊‘(𝑥 / 𝑛))))
82	79, 81	oveq12d 7289	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ⁺ → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) − (log‘(!‘(⌊‘𝑥)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · 𝑥) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (⌊‘(𝑥 / 𝑛)))))
83	46	recnd 11004	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) / 𝑛) · 𝑥) ∈ ℂ)
84	51	recnd 11004	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · (⌊‘(𝑥 / 𝑛))) ∈ ℂ)
85	11, 83, 84	fsumsub 15498	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ⁺ → Σ𝑛 ∈ (1...(⌊‘𝑥))((((Λ‘𝑛) / 𝑛) · 𝑥) − ((Λ‘𝑛) · (⌊‘(𝑥 / 𝑛)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · 𝑥) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (⌊‘(𝑥 / 𝑛)))))
86	82, 85	eqtr4d 2783	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ⁺ → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) − (log‘(!‘(⌊‘𝑥)))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((((Λ‘𝑛) / 𝑛) · 𝑥) − ((Λ‘𝑛) · (⌊‘(𝑥 / 𝑛)))))
87		chpval 26269	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ → (ψ‘𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))(Λ‘𝑛))
88	36, 87	syl 17	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ⁺ → (ψ‘𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))(Λ‘𝑛))
89	77, 86, 88	3brtr4d 5111	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ⁺ → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) − (log‘(!‘(⌊‘𝑥)))) ≤ (ψ‘𝑥))
90	17, 36	remulcld 11006	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ⁺ → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) ∈ ℝ)
91	90, 26	resubcld 11403	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ⁺ → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) − (log‘(!‘(⌊‘𝑥)))) ∈ ℝ)
92		rpregt0 12743	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 ∈ ℝ ∧ 0 < 𝑥))
93		lediv1 11840	. . . . . . . . 9 ⊢ ((((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) − (log‘(!‘(⌊‘𝑥)))) ∈ ℝ ∧ (ψ‘𝑥) ∈ ℝ ∧ (𝑥 ∈ ℝ ∧ 0 < 𝑥)) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) − (log‘(!‘(⌊‘𝑥)))) ≤ (ψ‘𝑥) ↔ (((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) − (log‘(!‘(⌊‘𝑥)))) / 𝑥) ≤ ((ψ‘𝑥) / 𝑥)))
94	91, 38, 92, 93	syl3anc 1370	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ⁺ → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) − (log‘(!‘(⌊‘𝑥)))) ≤ (ψ‘𝑥) ↔ (((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) − (log‘(!‘(⌊‘𝑥)))) / 𝑥) ≤ ((ψ‘𝑥) / 𝑥)))
95	89, 94	mpbid 231	. . . . . . 7 ⊢ (𝑥 ∈ ℝ⁺ → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) − (log‘(!‘(⌊‘𝑥)))) / 𝑥) ≤ ((ψ‘𝑥) / 𝑥))
96	90	recnd 11004	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ⁺ → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) ∈ ℂ)
97	26	recnd 11004	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ⁺ → (log‘(!‘(⌊‘𝑥))) ∈ ℂ)
98		rpcnne0 12747	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ⁺ → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
99		divsubdir 11669	. . . . . . . . . . 11 ⊢ (((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) ∈ ℂ ∧ (log‘(!‘(⌊‘𝑥))) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) − (log‘(!‘(⌊‘𝑥)))) / 𝑥) = (((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) / 𝑥) − ((log‘(!‘(⌊‘𝑥))) / 𝑥)))
100	96, 97, 98, 99	syl3anc 1370	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ⁺ → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) − (log‘(!‘(⌊‘𝑥)))) / 𝑥) = (((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) / 𝑥) − ((log‘(!‘(⌊‘𝑥))) / 𝑥)))
101		rpne0 12745	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ≠ 0)
102	18, 64, 101	divcan4d 11757	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ⁺ → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) / 𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛))
103	102	oveq1d 7286	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ⁺ → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) / 𝑥) − ((log‘(!‘(⌊‘𝑥))) / 𝑥)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − ((log‘(!‘(⌊‘𝑥))) / 𝑥)))
104	100, 103	eqtr2d 2781	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ⁺ → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − ((log‘(!‘(⌊‘𝑥))) / 𝑥)) = (((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) − (log‘(!‘(⌊‘𝑥)))) / 𝑥))
105	104	fveq2d 6775	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ⁺ → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − ((log‘(!‘(⌊‘𝑥))) / 𝑥))) = (abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) − (log‘(!‘(⌊‘𝑥)))) / 𝑥)))
106		rerpdivcl 12759	. . . . . . . . . 10 ⊢ ((((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) − (log‘(!‘(⌊‘𝑥)))) ∈ ℝ ∧ 𝑥 ∈ ℝ⁺) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) − (log‘(!‘(⌊‘𝑥)))) / 𝑥) ∈ ℝ)
107	91, 106	mpancom 685	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ⁺ → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) − (log‘(!‘(⌊‘𝑥)))) / 𝑥) ∈ ℝ)
108		flle 13517	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 / 𝑛) ∈ ℝ → (⌊‘(𝑥 / 𝑛)) ≤ (𝑥 / 𝑛))
109	48, 108	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (⌊‘(𝑥 / 𝑛)) ≤ (𝑥 / 𝑛))
110	48, 50	subge0d 11565	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (0 ≤ ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))) ↔ (⌊‘(𝑥 / 𝑛)) ≤ (𝑥 / 𝑛)))
111	109, 110	mpbird 256	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛))))
112	15, 53, 56, 111	mulge0d 11552	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ ((Λ‘𝑛) · ((𝑥 / 𝑛) − (⌊‘(𝑥 / 𝑛)))))
113	112, 74	breqtrd 5105	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ ((((Λ‘𝑛) / 𝑛) · 𝑥) − ((Λ‘𝑛) · (⌊‘(𝑥 / 𝑛)))))
114	11, 52, 113	fsumge0 15505	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ⁺ → 0 ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))((((Λ‘𝑛) / 𝑛) · 𝑥) − ((Λ‘𝑛) · (⌊‘(𝑥 / 𝑛)))))
115	114, 86	breqtrrd 5107	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ⁺ → 0 ≤ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) − (log‘(!‘(⌊‘𝑥)))))
116		divge0 11844	. . . . . . . . . 10 ⊢ (((((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) − (log‘(!‘(⌊‘𝑥)))) ∈ ℝ ∧ 0 ≤ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) − (log‘(!‘(⌊‘𝑥))))) ∧ (𝑥 ∈ ℝ ∧ 0 < 𝑥)) → 0 ≤ (((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) − (log‘(!‘(⌊‘𝑥)))) / 𝑥))
117	91, 115, 92, 116	syl21anc 835	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ⁺ → 0 ≤ (((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) − (log‘(!‘(⌊‘𝑥)))) / 𝑥))
118	107, 117	absidd 15132	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ⁺ → (abs‘(((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) − (log‘(!‘(⌊‘𝑥)))) / 𝑥)) = (((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) − (log‘(!‘(⌊‘𝑥)))) / 𝑥))
119	105, 118	eqtrd 2780	. . . . . . 7 ⊢ (𝑥 ∈ ℝ⁺ → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − ((log‘(!‘(⌊‘𝑥))) / 𝑥))) = (((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝑥) − (log‘(!‘(⌊‘𝑥)))) / 𝑥))
120		chpge0 26273	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ → 0 ≤ (ψ‘𝑥))
121	36, 120	syl 17	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ⁺ → 0 ≤ (ψ‘𝑥))
122		divge0 11844	. . . . . . . . 9 ⊢ ((((ψ‘𝑥) ∈ ℝ ∧ 0 ≤ (ψ‘𝑥)) ∧ (𝑥 ∈ ℝ ∧ 0 < 𝑥)) → 0 ≤ ((ψ‘𝑥) / 𝑥))
123	38, 121, 92, 122	syl21anc 835	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ⁺ → 0 ≤ ((ψ‘𝑥) / 𝑥))
124	40, 123	absidd 15132	. . . . . . 7 ⊢ (𝑥 ∈ ℝ⁺ → (abs‘((ψ‘𝑥) / 𝑥)) = ((ψ‘𝑥) / 𝑥))
125	95, 119, 124	3brtr4d 5111	. . . . . 6 ⊢ (𝑥 ∈ ℝ⁺ → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − ((log‘(!‘(⌊‘𝑥))) / 𝑥))) ≤ (abs‘((ψ‘𝑥) / 𝑥)))
126	125	ad2antrl 725	. . . . 5 ⊢ ((⊤ ∧ (𝑥 ∈ ℝ⁺ ∧ 1 ≤ 𝑥)) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − ((log‘(!‘(⌊‘𝑥))) / 𝑥))) ≤ (abs‘((ψ‘𝑥) / 𝑥)))
127	33, 35, 42, 44, 126	o1le 15362	. . . 4 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − ((log‘(!‘(⌊‘𝑥))) / 𝑥))) ∈ 𝑂(1))
128	127	mptru 1549	. . 3 ⊢ (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − ((log‘(!‘(⌊‘𝑥))) / 𝑥))) ∈ 𝑂(1)
129		logfacrlim 26370	. . . 4 ⊢ (𝑥 ∈ ℝ⁺ ↦ ((log‘𝑥) − ((log‘(!‘(⌊‘𝑥))) / 𝑥))) ⇝_𝑟 1
130		rlimo1 15324	. . . 4 ⊢ ((𝑥 ∈ ℝ⁺ ↦ ((log‘𝑥) − ((log‘(!‘(⌊‘𝑥))) / 𝑥))) ⇝_𝑟 1 → (𝑥 ∈ ℝ⁺ ↦ ((log‘𝑥) − ((log‘(!‘(⌊‘𝑥))) / 𝑥))) ∈ 𝑂(1))
131	129, 130	ax-mp 5	. . 3 ⊢ (𝑥 ∈ ℝ⁺ ↦ ((log‘𝑥) − ((log‘(!‘(⌊‘𝑥))) / 𝑥))) ∈ 𝑂(1)
132		o1sub 15323	. . 3 ⊢ (((𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − ((log‘(!‘(⌊‘𝑥))) / 𝑥))) ∈ 𝑂(1) ∧ (𝑥 ∈ ℝ⁺ ↦ ((log‘𝑥) − ((log‘(!‘(⌊‘𝑥))) / 𝑥))) ∈ 𝑂(1)) → ((𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − ((log‘(!‘(⌊‘𝑥))) / 𝑥))) ∘_f − (𝑥 ∈ ℝ⁺ ↦ ((log‘𝑥) − ((log‘(!‘(⌊‘𝑥))) / 𝑥)))) ∈ 𝑂(1))
133	128, 131, 132	mp2an 689	. 2 ⊢ ((𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − ((log‘(!‘(⌊‘𝑥))) / 𝑥))) ∘_f − (𝑥 ∈ ℝ⁺ ↦ ((log‘𝑥) − ((log‘(!‘(⌊‘𝑥))) / 𝑥)))) ∈ 𝑂(1)
134	32, 133	eqeltrri 2838	1 ⊢ (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1)

Colors of variables: wff setvar class

Syntax hints: ↔ wb 205 ∧ wa 396 ∧ w3a 1086 = wceq 1542 ⊤wtru 1543 ∈ wcel 2110 ≠ wne 2945 Vcvv 3431 class class class wbr 5079 ↦ cmpt 5162 ‘cfv 6432 (class class class)co 7271 ∘_f cof 7525 ℂcc 10870 ℝcr 10871 0cc0 10872 1c1 10873 · cmul 10877 < clt 11010 ≤ cle 11011 − cmin 11205 / cdiv 11632 ℕcn 11973 ℕ₀cn0 12233 ℝ⁺crp 12729 ...cfz 13238 ⌊cfl 13508 !cfa 13985 abscabs 14943 ⇝_𝑟 crli 15192 𝑂(1)co1 15193 Σcsu 15395 logclog 25708 Λcvma 26239 ψcchp 26240

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 1917 ax-6 1975 ax-7 2015 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2711 ax-rep 5214 ax-sep 5227 ax-nul 5234 ax-pow 5292 ax-pr 5356 ax-un 7582 ax-inf2 9377 ax-cnex 10928 ax-resscn 10929 ax-1cn 10930 ax-icn 10931 ax-addcl 10932 ax-addrcl 10933 ax-mulcl 10934 ax-mulrcl 10935 ax-mulcom 10936 ax-addass 10937 ax-mulass 10938 ax-distr 10939 ax-i2m1 10940 ax-1ne0 10941 ax-1rid 10942 ax-rnegex 10943 ax-rrecex 10944 ax-cnre 10945 ax-pre-lttri 10946 ax-pre-lttrn 10947 ax-pre-ltadd 10948 ax-pre-mulgt0 10949 ax-pre-sup 10950 ax-addf 10951 ax-mulf 10952

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2072 df-mo 2542 df-eu 2571 df-clab 2718 df-cleq 2732 df-clel 2818 df-nfc 2891 df-ne 2946 df-nel 3052 df-ral 3071 df-rex 3072 df-reu 3073 df-rmo 3074 df-rab 3075 df-v 3433 df-sbc 3721 df-csb 3838 df-dif 3895 df-un 3897 df-in 3899 df-ss 3909 df-pss 3911 df-nul 4263 df-if 4466 df-pw 4541 df-sn 4568 df-pr 4570 df-tp 4572 df-op 4574 df-uni 4846 df-int 4886 df-iun 4932 df-iin 4933 df-br 5080 df-opab 5142 df-mpt 5163 df-tr 5197 df-id 5490 df-eprel 5496 df-po 5504 df-so 5505 df-fr 5545 df-se 5546 df-we 5547 df-xp 5596 df-rel 5597 df-cnv 5598 df-co 5599 df-dm 5600 df-rn 5601 df-res 5602 df-ima 5603 df-pred 6201 df-ord 6268 df-on 6269 df-lim 6270 df-suc 6271 df-iota 6390 df-fun 6434 df-fn 6435 df-f 6436 df-f1 6437 df-fo 6438 df-f1o 6439 df-fv 6440 df-isom 6441 df-riota 7228 df-ov 7274 df-oprab 7275 df-mpo 7276 df-of 7527 df-om 7707 df-1st 7824 df-2nd 7825 df-supp 7969 df-frecs 8088 df-wrecs 8119 df-recs 8193 df-rdg 8232 df-1o 8288 df-2o 8289 df-oadd 8292 df-er 8481 df-map 8600 df-pm 8601 df-ixp 8669 df-en 8717 df-dom 8718 df-sdom 8719 df-fin 8720 df-fsupp 9107 df-fi 9148 df-sup 9179 df-inf 9180 df-oi 9247 df-dju 9660 df-card 9698 df-pnf 11012 df-mnf 11013 df-xr 11014 df-ltxr 11015 df-le 11016 df-sub 11207 df-neg 11208 df-div 11633 df-nn 11974 df-2 12036 df-3 12037 df-4 12038 df-5 12039 df-6 12040 df-7 12041 df-8 12042 df-9 12043 df-n0 12234 df-xnn0 12306 df-z 12320 df-dec 12437 df-uz 12582 df-q 12688 df-rp 12730 df-xneg 12847 df-xadd 12848 df-xmul 12849 df-ioo 13082 df-ioc 13083 df-ico 13084 df-icc 13085 df-fz 13239 df-fzo 13382 df-fl 13510 df-mod 13588 df-seq 13720 df-exp 13781 df-fac 13986 df-bc 14015 df-hash 14043 df-shft 14776 df-cj 14808 df-re 14809 df-im 14810 df-sqrt 14944 df-abs 14945 df-limsup 15178 df-clim 15195 df-rlim 15196 df-o1 15197 df-lo1 15198 df-sum 15396 df-ef 15775 df-e 15776 df-sin 15777 df-cos 15778 df-pi 15780 df-dvds 15962 df-gcd 16200 df-prm 16375 df-pc 16536 df-struct 16846 df-sets 16863 df-slot 16881 df-ndx 16893 df-base 16911 df-ress 16940 df-plusg 16973 df-mulr 16974 df-starv 16975 df-sca 16976 df-vsca 16977 df-ip 16978 df-tset 16979 df-ple 16980 df-ds 16982 df-unif 16983 df-hom 16984 df-cco 16985 df-rest 17131 df-topn 17132 df-0g 17150 df-gsum 17151 df-topgen 17152 df-pt 17153 df-prds 17156 df-xrs 17211 df-qtop 17216 df-imas 17217 df-xps 17219 df-mre 17293 df-mrc 17294 df-acs 17296 df-mgm 18324 df-sgrp 18373 df-mnd 18384 df-submnd 18429 df-mulg 18699 df-cntz 18921 df-cmn 19386 df-psmet 20587 df-xmet 20588 df-met 20589 df-bl 20590 df-mopn 20591 df-fbas 20592 df-fg 20593 df-cnfld 20596 df-top 22041 df-topon 22058 df-topsp 22080 df-bases 22094 df-cld 22168 df-ntr 22169 df-cls 22170 df-nei 22247 df-lp 22285 df-perf 22286 df-cn 22376 df-cnp 22377 df-haus 22464 df-cmp 22536 df-tx 22711 df-hmeo 22904 df-fil 22995 df-fm 23087 df-flim 23088 df-flf 23089 df-xms 23471 df-ms 23472 df-tms 23473 df-cncf 24039 df-limc 25028 df-dv 25029 df-log 25710 df-cxp 25711 df-cht 26244 df-vma 26245 df-chp 26246 df-ppi 26247

This theorem is referenced by: vmadivsumb 26629 rpvmasumlem 26633 vmalogdivsum2 26684 vmalogdivsum 26685 2vmadivsumlem 26686 selberg3lem1 26703 selberg4lem1 26706 pntrsumo1 26711 selbergr 26714

W3C validator