vmalogdivsum2 - Metamath Proof Explorer

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

Theorem vmalogdivsum2 27477

Description: The sum Σ𝑛 ≤ 𝑥, Λ(𝑛)log(𝑥 / 𝑛) / 𝑛 is asymptotic to log↑2(𝑥) / 2 + 𝑂(log𝑥). Exercise 9.1.7 of [Shapiro], p. 336. (Contributed by Mario Carneiro, 30-May-2016.)

**Assertion**
Ref	Expression
vmalogdivsum2	⊢ (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2))) ∈ 𝑂(1)

Distinct variable group: 𝑥,𝑛

Proof of Theorem vmalogdivsum2 Dummy variables 𝑘 𝑚 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fzfid 13882	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (1...(⌊‘𝑥)) ∈ Fin)
2		elfznn 13455	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (1...(⌊‘𝑥)) → 𝑘 ∈ ℕ)
3	2	adantl 481	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → 𝑘 ∈ ℕ)
4	3	nnrpd 12934	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → 𝑘 ∈ ℝ⁺)
5	4	relogcld 26560	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → (log‘𝑘) ∈ ℝ)
6	5, 3	nndivred 12186	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → ((log‘𝑘) / 𝑘) ∈ ℝ)
7	1, 6	fsumrecl 15643	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) ∈ ℝ)
8	7	recnd 11147	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) ∈ ℂ)
9		elioore 13277	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (1(,)+∞) → 𝑥 ∈ ℝ)
10	9	adantl 481	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ∈ ℝ)
11		1rp 12896	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℝ⁺
12	11	a1i 11	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 ∈ ℝ⁺)
13		1red 11120	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 ∈ ℝ)
14		eliooord 13307	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (1(,)+∞) → (1 < 𝑥 ∧ 𝑥 < +∞))
15	14	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (1 < 𝑥 ∧ 𝑥 < +∞))
16	15	simpld 494	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 < 𝑥)
17	13, 10, 16	ltled 11268	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 ≤ 𝑥)
18	10, 12, 17	rpgecld 12975	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ∈ ℝ⁺)
19	18	relogcld 26560	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ∈ ℝ)
20	19	resqcld 14034	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((log‘𝑥)↑2) ∈ ℝ)
21	20	rehalfcld 12375	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((log‘𝑥)↑2) / 2) ∈ ℝ)
22	21	recnd 11147	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((log‘𝑥)↑2) / 2) ∈ ℂ)
23	19	recnd 11147	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ∈ ℂ)
24	10, 16	rplogcld 26566	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ∈ ℝ⁺)
25	24	rpne0d 12941	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ≠ 0)
26	8, 22, 23, 25	divsubdird 11943	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2)) / (log‘𝑥)) = ((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) / (log‘𝑥)) − ((((log‘𝑥)↑2) / 2) / (log‘𝑥))))
27	7, 21	resubcld 11552	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2)) ∈ ℝ)
28	27	recnd 11147	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2)) ∈ ℂ)
29	28, 23, 25	divrecd 11907	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2)) / (log‘𝑥)) = ((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2)) · (1 / (log‘𝑥))))
30	20	recnd 11147	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((log‘𝑥)↑2) ∈ ℂ)
31		2cnd 12210	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 2 ∈ ℂ)
32		2ne0 12236	. . . . . . . . . 10 ⊢ 2 ≠ 0
33	32	a1i 11	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 2 ≠ 0)
34	30, 31, 23, 33, 25	divdiv32d 11929	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((log‘𝑥)↑2) / 2) / (log‘𝑥)) = ((((log‘𝑥)↑2) / (log‘𝑥)) / 2))
35	23	sqvald 14052	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((log‘𝑥)↑2) = ((log‘𝑥) · (log‘𝑥)))
36	35	oveq1d 7367	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((log‘𝑥)↑2) / (log‘𝑥)) = (((log‘𝑥) · (log‘𝑥)) / (log‘𝑥)))
37	23, 23, 25	divcan3d 11909	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((log‘𝑥) · (log‘𝑥)) / (log‘𝑥)) = (log‘𝑥))
38	36, 37	eqtrd 2768	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((log‘𝑥)↑2) / (log‘𝑥)) = (log‘𝑥))
39	38	oveq1d 7367	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((log‘𝑥)↑2) / (log‘𝑥)) / 2) = ((log‘𝑥) / 2))
40	34, 39	eqtrd 2768	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((log‘𝑥)↑2) / 2) / (log‘𝑥)) = ((log‘𝑥) / 2))
41	40	oveq2d 7368	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) / (log‘𝑥)) − ((((log‘𝑥)↑2) / 2) / (log‘𝑥))) = ((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) / (log‘𝑥)) − ((log‘𝑥) / 2)))
42	26, 29, 41	3eqtr3rd 2777	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) / (log‘𝑥)) − ((log‘𝑥) / 2)) = ((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2)) · (1 / (log‘𝑥))))
43	42	mpteq2dva 5186	. . . 4 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) / (log‘𝑥)) − ((log‘𝑥) / 2))) = (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2)) · (1 / (log‘𝑥)))))
44	24	rprecred 12947	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (1 / (log‘𝑥)) ∈ ℝ)
45	18	ex 412	. . . . . . 7 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) → 𝑥 ∈ ℝ⁺))
46	45	ssrdv 3936	. . . . . 6 ⊢ (⊤ → (1(,)+∞) ⊆ ℝ⁺)
47		eqid 2733	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ⁺ ↦ (Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2))) = (𝑥 ∈ ℝ⁺ ↦ (Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2)))
48	47	logdivsum 27472	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ⁺ ↦ (Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2))):ℝ⁺⟶ℝ ∧ (𝑥 ∈ ℝ⁺ ↦ (Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2))) ∈ dom ⇝_𝑟 ∧ (((𝑥 ∈ ℝ⁺ ↦ (Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2))) ⇝_𝑟 1 ∧ 1 ∈ ℝ⁺ ∧ e ≤ 1) → (abs‘(((𝑥 ∈ ℝ⁺ ↦ (Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2)))‘1) − 1)) ≤ ((log‘1) / 1)))
49	48	simp2i 1140	. . . . . . 7 ⊢ (𝑥 ∈ ℝ⁺ ↦ (Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2))) ∈ dom ⇝_𝑟
50		rlimdmo1 15527	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ⁺ ↦ (Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2))) ∈ dom ⇝_𝑟 → (𝑥 ∈ ℝ⁺ ↦ (Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2))) ∈ 𝑂(1))
51	49, 50	mp1i 13	. . . . . 6 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ (Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2))) ∈ 𝑂(1))
52	46, 51	o1res2 15472	. . . . 5 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2))) ∈ 𝑂(1))
53		divlogrlim 26572	. . . . . 6 ⊢ (𝑥 ∈ (1(,)+∞) ↦ (1 / (log‘𝑥))) ⇝_𝑟 0
54		rlimo1 15526	. . . . . 6 ⊢ ((𝑥 ∈ (1(,)+∞) ↦ (1 / (log‘𝑥))) ⇝_𝑟 0 → (𝑥 ∈ (1(,)+∞) ↦ (1 / (log‘𝑥))) ∈ 𝑂(1))
55	53, 54	mp1i 13	. . . . 5 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (1 / (log‘𝑥))) ∈ 𝑂(1))
56	27, 44, 52, 55	o1mul2 15534	. . . 4 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − (((log‘𝑥)↑2) / 2)) · (1 / (log‘𝑥)))) ∈ 𝑂(1))
57	43, 56	eqeltrd 2833	. . 3 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) / (log‘𝑥)) − ((log‘𝑥) / 2))) ∈ 𝑂(1))
58	8, 23, 25	divcld 11904	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) / (log‘𝑥)) ∈ ℂ)
59	23	halfcld 12373	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((log‘𝑥) / 2) ∈ ℂ)
60	58, 59	subcld 11479	. . . 4 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) / (log‘𝑥)) − ((log‘𝑥) / 2)) ∈ ℂ)
61		elfznn 13455	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
62	61	adantl 481	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
63		vmacl 27056	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ → (Λ‘𝑛) ∈ ℝ)
64	62, 63	syl 17	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈ ℝ)
65	64, 62	nndivred 12186	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) / 𝑛) ∈ ℝ)
66	18	adantr 480	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ⁺)
67	62	nnrpd 12934	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ⁺)
68	66, 67	rpdivcld 12953	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ⁺)
69	68	relogcld 26560	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ∈ ℝ)
70	65, 69	remulcld 11149	. . . . . . . 8 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) ∈ ℝ)
71	1, 70	fsumrecl 15643	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) ∈ ℝ)
72	71	recnd 11147	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) ∈ ℂ)
73	24	rpcnd 12938	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ∈ ℂ)
74	72, 73, 25	divcld 11904	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) ∈ ℂ)
75	73	halfcld 12373	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((log‘𝑥) / 2) ∈ ℂ)
76	74, 75	subcld 11479	. . . 4 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2)) ∈ ℂ)
77	58, 74, 59	nnncan2d 11514	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) / (log‘𝑥)) − ((log‘𝑥) / 2)) − ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2))) = ((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) / (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥))))
78	8, 72, 23, 25	divsubdird 11943	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) / (log‘𝑥)) = ((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) / (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥))))
79		fzfid 13882	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1...(⌊‘(𝑥 / 𝑛))) ∈ Fin)
80	64	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (Λ‘𝑛) ∈ ℝ)
81	62	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑛 ∈ ℕ)
82		elfznn 13455	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛))) → 𝑚 ∈ ℕ)
83	82	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ∈ ℕ)
84	81, 83	nnmulcld 12185	. . . . . . . . . . . . 13 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (𝑛 · 𝑚) ∈ ℕ)
85	80, 84	nndivred 12186	. . . . . . . . . . . 12 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((Λ‘𝑛) / (𝑛 · 𝑚)) ∈ ℝ)
86	79, 85	fsumrecl 15643	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑛) / (𝑛 · 𝑚)) ∈ ℝ)
87	86	recnd 11147	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑛) / (𝑛 · 𝑚)) ∈ ℂ)
88	70	recnd 11147	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) ∈ ℂ)
89	1, 87, 88	fsumsub 15697	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑛) / (𝑛 · 𝑚)) − (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑛) / (𝑛 · 𝑚)) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))))
90	64	recnd 11147	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈ ℂ)
91	62	nncnd 12148	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℂ)
92	62	nnne0d 12182	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ≠ 0)
93	90, 91, 92	divcld 11904	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) / 𝑛) ∈ ℂ)
94	83	nnrecred 12183	. . . . . . . . . . . . . 14 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (1 / 𝑚) ∈ ℝ)
95	79, 94	fsumrecl 15643	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) ∈ ℝ)
96	95	recnd 11147	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) ∈ ℂ)
97	69	recnd 11147	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ∈ ℂ)
98	93, 96, 97	subdid 11580	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) = ((((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚)) − (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))))
99	90	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (Λ‘𝑛) ∈ ℂ)
100	91	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑛 ∈ ℂ)
101	83	nncnd 12148	. . . . . . . . . . . . . . . 16 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ∈ ℂ)
102	92	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑛 ≠ 0)
103	83	nnne0d 12182	. . . . . . . . . . . . . . . 16 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ≠ 0)
104	99, 100, 101, 102, 103	divdiv1d 11935	. . . . . . . . . . . . . . 15 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (((Λ‘𝑛) / 𝑛) / 𝑚) = ((Λ‘𝑛) / (𝑛 · 𝑚)))
105	99, 100, 102	divcld 11904	. . . . . . . . . . . . . . . 16 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((Λ‘𝑛) / 𝑛) ∈ ℂ)
106	105, 101, 103	divrecd 11907	. . . . . . . . . . . . . . 15 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (((Λ‘𝑛) / 𝑛) / 𝑚) = (((Λ‘𝑛) / 𝑛) · (1 / 𝑚)))
107	104, 106	eqtr3d 2770	. . . . . . . . . . . . . 14 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((Λ‘𝑛) / (𝑛 · 𝑚)) = (((Λ‘𝑛) / 𝑛) · (1 / 𝑚)))
108	107	sumeq2dv 15611	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑛) / (𝑛 · 𝑚)) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(((Λ‘𝑛) / 𝑛) · (1 / 𝑚)))
109	101, 103	reccld 11897	. . . . . . . . . . . . . 14 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (1 / 𝑚) ∈ ℂ)
110	79, 93, 109	fsummulc2 15693	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚)) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(((Λ‘𝑛) / 𝑛) · (1 / 𝑚)))
111	108, 110	eqtr4d 2771	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑛) / (𝑛 · 𝑚)) = (((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚)))
112	111	oveq1d 7367	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑛) / (𝑛 · 𝑚)) − (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) = ((((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚)) − (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))))
113	98, 112	eqtr4d 2771	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑛) / (𝑛 · 𝑚)) − (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))))
114	113	sumeq2dv 15611	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑛) / (𝑛 · 𝑚)) − (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))))
115		vmasum 27155	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℕ → Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} (Λ‘𝑛) = (log‘𝑘))
116	3, 115	syl 17	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} (Λ‘𝑛) = (log‘𝑘))
117	116	oveq1d 7367	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → (Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} (Λ‘𝑛) / 𝑘) = ((log‘𝑘) / 𝑘))
118		fzfid 13882	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → (1...𝑘) ∈ Fin)
119		dvdsssfz1 16231	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ℕ → {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ⊆ (1...𝑘))
120	3, 119	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ⊆ (1...𝑘))
121	118, 120	ssfid 9160	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ∈ Fin)
122	3	nncnd 12148	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → 𝑘 ∈ ℂ)
123		ssrab2 4029	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ⊆ ℕ
124		simprr 772	. . . . . . . . . . . . . . . . . 18 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})
125	123, 124	sselid 3928	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → 𝑛 ∈ ℕ)
126	125, 63	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → (Λ‘𝑛) ∈ ℝ)
127	126	recnd 11147	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → (Λ‘𝑛) ∈ ℂ)
128	127	anassrs 467	. . . . . . . . . . . . . 14 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) → (Λ‘𝑛) ∈ ℂ)
129	3	nnne0d 12182	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → 𝑘 ≠ 0)
130	121, 122, 128, 129	fsumdivc 15695	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → (Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} (Λ‘𝑛) / 𝑘) = Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑛) / 𝑘))
131	117, 130	eqtr3d 2770	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → ((log‘𝑘) / 𝑘) = Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑛) / 𝑘))
132	131	sumeq2dv 15611	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) = Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑛) / 𝑘))
133		oveq2 7360	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑛 · 𝑚) → ((Λ‘𝑛) / 𝑘) = ((Λ‘𝑛) / (𝑛 · 𝑚)))
134	2	ad2antrl 728	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → 𝑘 ∈ ℕ)
135	134	nncnd 12148	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → 𝑘 ∈ ℂ)
136	134	nnne0d 12182	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → 𝑘 ≠ 0)
137	127, 135, 136	divcld 11904	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → ((Λ‘𝑛) / 𝑘) ∈ ℂ)
138	133, 10, 137	dvdsflsumcom 27126	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑛) / 𝑘) = Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑛) / (𝑛 · 𝑚)))
139	132, 138	eqtrd 2768	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) = Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑛) / (𝑛 · 𝑚)))
140	139	oveq1d 7367	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑛) / (𝑛 · 𝑚)) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))))
141	89, 114, 140	3eqtr4rd 2779	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))))
142	141	oveq1d 7367	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) / (log‘𝑥)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥)))
143	77, 78, 142	3eqtr2d 2774	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) / (log‘𝑥)) − ((log‘𝑥) / 2)) − ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥)))
144	143	mpteq2dva 5186	. . . . 5 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) / (log‘𝑥)) − ((log‘𝑥) / 2)) − ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2)))) = (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥))))
145		1red 11120	. . . . . . 7 ⊢ (⊤ → 1 ∈ ℝ)
146	1, 65	fsumrecl 15643	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ∈ ℝ)
147	146, 24	rerpdivcld 12967	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) ∈ ℝ)
148		ioossre 13309	. . . . . . . . . . 11 ⊢ (1(,)+∞) ⊆ ℝ
149		ax-1cn 11071	. . . . . . . . . . 11 ⊢ 1 ∈ ℂ
150		o1const 15529	. . . . . . . . . . 11 ⊢ (((1(,)+∞) ⊆ ℝ ∧ 1 ∈ ℂ) → (𝑥 ∈ (1(,)+∞) ↦ 1) ∈ 𝑂(1))
151	148, 149, 150	mp2an 692	. . . . . . . . . 10 ⊢ (𝑥 ∈ (1(,)+∞) ↦ 1) ∈ 𝑂(1)
152	151	a1i 11	. . . . . . . . 9 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ 1) ∈ 𝑂(1))
153	147	recnd 11147	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) ∈ ℂ)
154	12	rpcnd 12938	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 ∈ ℂ)
155	146	recnd 11147	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ∈ ℂ)
156	155, 23, 23, 25	divsubdird 11943	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) / (log‘𝑥)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) − ((log‘𝑥) / (log‘𝑥))))
157	155, 23	subcld 11479	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) ∈ ℂ)
158	157, 23, 25	divrecd 11907	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) / (log‘𝑥)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) · (1 / (log‘𝑥))))
159	23, 25	dividd 11902	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((log‘𝑥) / (log‘𝑥)) = 1)
160	159	oveq2d 7368	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) − ((log‘𝑥) / (log‘𝑥))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) − 1))
161	156, 158, 160	3eqtr3rd 2777	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) − 1) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) · (1 / (log‘𝑥))))
162	161	mpteq2dva 5186	. . . . . . . . . . 11 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) − 1)) = (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) · (1 / (log‘𝑥)))))
163	146, 19	resubcld 11552	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) ∈ ℝ)
164		vmadivsum 27421	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1)
165	164	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1))
166	46, 165	o1res2 15472	. . . . . . . . . . . 12 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1))
167	163, 44, 166, 55	o1mul2 15534	. . . . . . . . . . 11 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) · (1 / (log‘𝑥)))) ∈ 𝑂(1))
168	162, 167	eqeltrd 2833	. . . . . . . . . 10 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) − 1)) ∈ 𝑂(1))
169	153, 154, 168	o1dif 15539	. . . . . . . . 9 ⊢ (⊤ → ((𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥))) ∈ 𝑂(1) ↔ (𝑥 ∈ (1(,)+∞) ↦ 1) ∈ 𝑂(1)))
170	152, 169	mpbird 257	. . . . . . . 8 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥))) ∈ 𝑂(1))
171	147, 170	o1lo1d 15448	. . . . . . 7 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥))) ∈ ≤𝑂(1))
172	95, 69	resubcld 11552	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛))) ∈ ℝ)
173	65, 172	remulcld 11149	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) ∈ ℝ)
174	1, 173	fsumrecl 15643	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) ∈ ℝ)
175	174, 24	rerpdivcld 12967	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥)) ∈ ℝ)
176		1red 11120	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℝ)
177		vmage0 27059	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → 0 ≤ (Λ‘𝑛))
178	62, 177	syl 17	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (Λ‘𝑛))
179	64, 67, 178	divge0d 12976	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ ((Λ‘𝑛) / 𝑛))
180	68	rpred 12936	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ)
181	91	mullidd 11137	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 · 𝑛) = 𝑛)
182		fznnfl 13768	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℝ → (𝑛 ∈ (1...(⌊‘𝑥)) ↔ (𝑛 ∈ ℕ ∧ 𝑛 ≤ 𝑥)))
183	10, 182	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑛 ∈ (1...(⌊‘𝑥)) ↔ (𝑛 ∈ ℕ ∧ 𝑛 ≤ 𝑥)))
184	183	simplbda 499	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ≤ 𝑥)
185	181, 184	eqbrtrd 5115	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 · 𝑛) ≤ 𝑥)
186	10	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ)
187	176, 186, 67	lemuldivd 12985	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 · 𝑛) ≤ 𝑥 ↔ 1 ≤ (𝑥 / 𝑛)))
188	185, 187	mpbid 232	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ≤ (𝑥 / 𝑛))
189		harmonicubnd 26948	. . . . . . . . . . . . . 14 ⊢ (((𝑥 / 𝑛) ∈ ℝ ∧ 1 ≤ (𝑥 / 𝑛)) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) ≤ ((log‘(𝑥 / 𝑛)) + 1))
190	180, 188, 189	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) ≤ ((log‘(𝑥 / 𝑛)) + 1))
191	95, 69, 176	lesubadd2d 11723	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛))) ≤ 1 ↔ Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) ≤ ((log‘(𝑥 / 𝑛)) + 1)))
192	190, 191	mpbird 257	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛))) ≤ 1)
193	172, 176, 65, 179, 192	lemul2ad 12069	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) ≤ (((Λ‘𝑛) / 𝑛) · 1))
194	93	mulridd 11136	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) / 𝑛) · 1) = ((Λ‘𝑛) / 𝑛))
195	193, 194	breqtrd 5119	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) ≤ ((Λ‘𝑛) / 𝑛))
196	1, 173, 65, 195	fsumle 15708	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛))
197	174, 146, 24, 196	lediv1dd 12994	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥)) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)))
198	197	adantrr 717	. . . . . . 7 ⊢ ((⊤ ∧ (𝑥 ∈ (1(,)+∞) ∧ 1 ≤ 𝑥)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥)) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)))
199	145, 171, 147, 175, 198	lo1le 15561	. . . . . 6 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥))) ∈ ≤𝑂(1))
200		0red 11122	. . . . . . 7 ⊢ (⊤ → 0 ∈ ℝ)
201		harmoniclbnd 26947	. . . . . . . . . . . 12 ⊢ ((𝑥 / 𝑛) ∈ ℝ⁺ → (log‘(𝑥 / 𝑛)) ≤ Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚))
202	68, 201	syl 17	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ≤ Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚))
203	95, 69	subge0d 11714	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (0 ≤ (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛))) ↔ (log‘(𝑥 / 𝑛)) ≤ Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚)))
204	202, 203	mpbird 257	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛))))
205	65, 172, 179, 204	mulge0d 11701	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))))
206	1, 173, 205	fsumge0 15704	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))))
207	174, 24, 206	divge0d 12976	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥)))
208	175, 200, 207	o1lo12 15447	. . . . . 6 ⊢ (⊤ → ((𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥))) ∈ 𝑂(1) ↔ (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥))) ∈ ≤𝑂(1)))
209	199, 208	mpbird 257	. . . . 5 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥))) ∈ 𝑂(1))
210	144, 209	eqeltrd 2833	. . . 4 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) / (log‘𝑥)) − ((log‘𝑥) / 2)) − ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2)))) ∈ 𝑂(1))
211	60, 76, 210	o1dif 15539	. . 3 ⊢ (⊤ → ((𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑘 ∈ (1...(⌊‘𝑥))((log‘𝑘) / 𝑘) / (log‘𝑥)) − ((log‘𝑥) / 2))) ∈ 𝑂(1) ↔ (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2))) ∈ 𝑂(1)))
212	57, 211	mpbid 232	. 2 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2))) ∈ 𝑂(1))
213	212	mptru 1548	1 ⊢ (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2))) ∈ 𝑂(1)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ⊤wtru 1542 ∈ wcel 2113 ≠ wne 2929 {crab 3396 ⊆ wss 3898 class class class wbr 5093 ↦ cmpt 5174 dom cdm 5619 ⟶wf 6482 ‘cfv 6486 (class class class)co 7352 ℂcc 11011 ℝcr 11012 0cc0 11013 1c1 11014 + caddc 11016 · cmul 11018 +∞cpnf 11150 < clt 11153 ≤ cle 11154 − cmin 11351 / cdiv 11781 ℕcn 12132 2c2 12187 ℝ⁺crp 12892 (,)cioo 13247 ...cfz 13409 ⌊cfl 13696 ↑cexp 13970 abscabs 15143 ⇝_𝑟 crli 15394 𝑂(1)co1 15395 ≤𝑂(1)clo1 15396 Σcsu 15595 eceu 15971 ∥ cdvds 16165 logclog 26491 Λcvma 27030

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 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2705 ax-rep 5219 ax-sep 5236 ax-nul 5246 ax-pow 5305 ax-pr 5372 ax-un 7674 ax-inf2 9538 ax-cnex 11069 ax-resscn 11070 ax-1cn 11071 ax-icn 11072 ax-addcl 11073 ax-addrcl 11074 ax-mulcl 11075 ax-mulrcl 11076 ax-mulcom 11077 ax-addass 11078 ax-mulass 11079 ax-distr 11080 ax-i2m1 11081 ax-1ne0 11082 ax-1rid 11083 ax-rnegex 11084 ax-rrecex 11085 ax-cnre 11086 ax-pre-lttri 11087 ax-pre-lttrn 11088 ax-pre-ltadd 11089 ax-pre-mulgt0 11090 ax-pre-sup 11091 ax-addf 11092

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2725 df-clel 2808 df-nfc 2882 df-ne 2930 df-nel 3034 df-ral 3049 df-rex 3058 df-rmo 3347 df-reu 3348 df-rab 3397 df-v 3439 df-sbc 3738 df-csb 3847 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-pss 3918 df-nul 4283 df-if 4475 df-pw 4551 df-sn 4576 df-pr 4578 df-tp 4580 df-op 4582 df-uni 4859 df-int 4898 df-iun 4943 df-iin 4944 df-br 5094 df-opab 5156 df-mpt 5175 df-tr 5201 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-se 5573 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6253 df-ord 6314 df-on 6315 df-lim 6316 df-suc 6317 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-isom 6495 df-riota 7309 df-ov 7355 df-oprab 7356 df-mpo 7357 df-of 7616 df-om 7803 df-1st 7927 df-2nd 7928 df-supp 8097 df-frecs 8217 df-wrecs 8248 df-recs 8297 df-rdg 8335 df-1o 8391 df-2o 8392 df-oadd 8395 df-er 8628 df-map 8758 df-pm 8759 df-ixp 8828 df-en 8876 df-dom 8877 df-sdom 8878 df-fin 8879 df-fsupp 9253 df-fi 9302 df-sup 9333 df-inf 9334 df-oi 9403 df-dju 9801 df-card 9839 df-pnf 11155 df-mnf 11156 df-xr 11157 df-ltxr 11158 df-le 11159 df-sub 11353 df-neg 11354 df-div 11782 df-nn 12133 df-2 12195 df-3 12196 df-4 12197 df-5 12198 df-6 12199 df-7 12200 df-8 12201 df-9 12202 df-n0 12389 df-xnn0 12462 df-z 12476 df-dec 12595 df-uz 12739 df-q 12849 df-rp 12893 df-xneg 13013 df-xadd 13014 df-xmul 13015 df-ioo 13251 df-ioc 13252 df-ico 13253 df-icc 13254 df-fz 13410 df-fzo 13557 df-fl 13698 df-mod 13776 df-seq 13911 df-exp 13971 df-fac 14183 df-bc 14212 df-hash 14240 df-shft 14976 df-cj 15008 df-re 15009 df-im 15010 df-sqrt 15144 df-abs 15145 df-limsup 15380 df-clim 15397 df-rlim 15398 df-o1 15399 df-lo1 15400 df-sum 15596 df-ef 15976 df-e 15977 df-sin 15978 df-cos 15979 df-tan 15980 df-pi 15981 df-dvds 16166 df-gcd 16408 df-prm 16585 df-pc 16751 df-struct 17060 df-sets 17077 df-slot 17095 df-ndx 17107 df-base 17123 df-ress 17144 df-plusg 17176 df-mulr 17177 df-starv 17178 df-sca 17179 df-vsca 17180 df-ip 17181 df-tset 17182 df-ple 17183 df-ds 17185 df-unif 17186 df-hom 17187 df-cco 17188 df-rest 17328 df-topn 17329 df-0g 17347 df-gsum 17348 df-topgen 17349 df-pt 17350 df-prds 17353 df-xrs 17408 df-qtop 17413 df-imas 17414 df-xps 17416 df-mre 17490 df-mrc 17491 df-acs 17493 df-mgm 18550 df-sgrp 18629 df-mnd 18645 df-submnd 18694 df-mulg 18983 df-cntz 19231 df-cmn 19696 df-psmet 21285 df-xmet 21286 df-met 21287 df-bl 21288 df-mopn 21289 df-fbas 21290 df-fg 21291 df-cnfld 21294 df-top 22810 df-topon 22827 df-topsp 22849 df-bases 22862 df-cld 22935 df-ntr 22936 df-cls 22937 df-nei 23014 df-lp 23052 df-perf 23053 df-cn 23143 df-cnp 23144 df-haus 23231 df-cmp 23303 df-tx 23478 df-hmeo 23671 df-fil 23762 df-fm 23854 df-flim 23855 df-flf 23856 df-xms 24236 df-ms 24237 df-tms 24238 df-cncf 24799 df-limc 25795 df-dv 25796 df-ulm 26314 df-log 26493 df-cxp 26494 df-atan 26805 df-em 26931 df-cht 27035 df-vma 27036 df-chp 27037 df-ppi 27038

This theorem is referenced by: vmalogdivsum 27478 2vmadivsumlem 27479 selberg4lem1 27499

W3C validator