Theorem selbergb 26298

Description: Convert eventual boundedness in selberg 26297 to boundedness on [1, +∞). (We have to bound away from zero because the log terms diverge at zero.) (Contributed by Mario Carneiro, 30-May-2016.)

Assertion

Ref	Expression
selbergb	⊢ ∃𝑐 ∈ ℝ+ ∀𝑥 ∈ (1[,)+∞)(abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) − (2 · (log‘𝑥)))) ≤ 𝑐

Distinct variable group:   𝑛,𝑐,𝑥

Proof of Theorem selbergb

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		1re 10732	. . . . . . 7 ⊢ 1 ∈ ℝ
2		elicopnf 12932	. . . . . . 7 ⊢ (1 ∈ ℝ → (𝑥 ∈ (1[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 1 ≤ 𝑥)))
3	1, 2	mp1i 13	. . . . . 6 ⊢ (⊤ → (𝑥 ∈ (1[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 1 ≤ 𝑥)))
4	3	simprbda 502	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ (1[,)+∞)) → 𝑥 ∈ ℝ)
5	4	ex 416	. . . 4 ⊢ (⊤ → (𝑥 ∈ (1[,)+∞) → 𝑥 ∈ ℝ))
6	5	ssrdv 3893	. . 3 ⊢ (⊤ → (1[,)+∞) ⊆ ℝ)
7	1	a1i 11	. . 3 ⊢ (⊤ → 1 ∈ ℝ)
8		fzfid 13445	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (1[,)+∞)) → (1...(⌊‘𝑥)) ∈ Fin)
9		elfznn 13040	. . . . . . . . . 10 ⊢ (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
10	9	adantl 485	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
11		vmacl 25868	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ → (Λ‘𝑛) ∈ ℝ)
12	10, 11	syl 17	. . . . . . . 8 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈ ℝ)
13	10	nnrpd 12525	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ+)
14	13	relogcld 25379	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘𝑛) ∈ ℝ)
15	4	adantr 484	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ)
16	15, 10	nndivred 11783	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ)
17		chpcl 25874	. . . . . . . . . 10 ⊢ ((𝑥 / 𝑛) ∈ ℝ → (ψ‘(𝑥 / 𝑛)) ∈ ℝ)
18	16, 17	syl 17	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (ψ‘(𝑥 / 𝑛)) ∈ ℝ)
19	14, 18	readdcld 10761	. . . . . . . 8 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘𝑛) + (ψ‘(𝑥 / 𝑛))) ∈ ℝ)
20	12, 19	remulcld 10762	. . . . . . 7 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) ∈ ℝ)
21	8, 20	fsumrecl 15197	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (1[,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) ∈ ℝ)
22		1rp 12489	. . . . . . . 8 ⊢ 1 ∈ ℝ+
23	22	a1i 11	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (1[,)+∞)) → 1 ∈ ℝ+)
24	3	simplbda 503	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (1[,)+∞)) → 1 ≤ 𝑥)
25	4, 23, 24	rpgecld 12566	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (1[,)+∞)) → 𝑥 ∈ ℝ+)
26	21, 25	rerpdivcld 12558	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ (1[,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) ∈ ℝ)
27		2re 11803	. . . . . . 7 ⊢ 2 ∈ ℝ
28	27	a1i 11	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (1[,)+∞)) → 2 ∈ ℝ)
29	25	relogcld 25379	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (1[,)+∞)) → (log‘𝑥) ∈ ℝ)
30	28, 29	remulcld 10762	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ (1[,)+∞)) → (2 · (log‘𝑥)) ∈ ℝ)
31	26, 30	resubcld 11159	. . . 4 ⊢ ((⊤ ∧ 𝑥 ∈ (1[,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) − (2 · (log‘𝑥))) ∈ ℝ)
32	31	recnd 10760	. . 3 ⊢ ((⊤ ∧ 𝑥 ∈ (1[,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) − (2 · (log‘𝑥))) ∈ ℂ)
33	25	ex 416	. . . . 5 ⊢ (⊤ → (𝑥 ∈ (1[,)+∞) → 𝑥 ∈ ℝ+))
34	33	ssrdv 3893	. . . 4 ⊢ (⊤ → (1[,)+∞) ⊆ ℝ+)
35		selberg 26297	. . . . 5 ⊢ (𝑥 ∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) − (2 · (log‘𝑥)))) ∈ 𝑂(1)
36	35	a1i 11	. . . 4 ⊢ (⊤ → (𝑥 ∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) − (2 · (log‘𝑥)))) ∈ 𝑂(1))
37	34, 36	o1res2 15023	. . 3 ⊢ (⊤ → (𝑥 ∈ (1[,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) − (2 · (log‘𝑥)))) ∈ 𝑂(1))
38		fzfid 13445	. . . . 5 ⊢ ((⊤ ∧ (𝑦 ∈ ℝ ∧ 1 ≤ 𝑦)) → (1...(⌊‘𝑦)) ∈ Fin)
39		elfznn 13040	. . . . . . . 8 ⊢ (𝑛 ∈ (1...(⌊‘𝑦)) → 𝑛 ∈ ℕ)
40	39	adantl 485	. . . . . . 7 ⊢ (((⊤ ∧ (𝑦 ∈ ℝ ∧ 1 ≤ 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → 𝑛 ∈ ℕ)
41	40, 11	syl 17	. . . . . 6 ⊢ (((⊤ ∧ (𝑦 ∈ ℝ ∧ 1 ≤ 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → (Λ‘𝑛) ∈ ℝ)
42	40	nnrpd 12525	. . . . . . . 8 ⊢ (((⊤ ∧ (𝑦 ∈ ℝ ∧ 1 ≤ 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → 𝑛 ∈ ℝ+)
43	42	relogcld 25379	. . . . . . 7 ⊢ (((⊤ ∧ (𝑦 ∈ ℝ ∧ 1 ≤ 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → (log‘𝑛) ∈ ℝ)
44		simprl 771	. . . . . . . . . 10 ⊢ ((⊤ ∧ (𝑦 ∈ ℝ ∧ 1 ≤ 𝑦)) → 𝑦 ∈ ℝ)
45	44	adantr 484	. . . . . . . . 9 ⊢ (((⊤ ∧ (𝑦 ∈ ℝ ∧ 1 ≤ 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → 𝑦 ∈ ℝ)
46	45, 40	nndivred 11783	. . . . . . . 8 ⊢ (((⊤ ∧ (𝑦 ∈ ℝ ∧ 1 ≤ 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → (𝑦 / 𝑛) ∈ ℝ)
47		chpcl 25874	. . . . . . . 8 ⊢ ((𝑦 / 𝑛) ∈ ℝ → (ψ‘(𝑦 / 𝑛)) ∈ ℝ)
48	46, 47	syl 17	. . . . . . 7 ⊢ (((⊤ ∧ (𝑦 ∈ ℝ ∧ 1 ≤ 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → (ψ‘(𝑦 / 𝑛)) ∈ ℝ)
49	43, 48	readdcld 10761	. . . . . 6 ⊢ (((⊤ ∧ (𝑦 ∈ ℝ ∧ 1 ≤ 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → ((log‘𝑛) + (ψ‘(𝑦 / 𝑛))) ∈ ℝ)
50	41, 49	remulcld 10762	. . . . 5 ⊢ (((⊤ ∧ (𝑦 ∈ ℝ ∧ 1 ≤ 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → ((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑦 / 𝑛)))) ∈ ℝ)
51	38, 50	fsumrecl 15197	. . . 4 ⊢ ((⊤ ∧ (𝑦 ∈ ℝ ∧ 1 ≤ 𝑦)) → Σ𝑛 ∈ (1...(⌊‘𝑦))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑦 / 𝑛)))) ∈ ℝ)
52	27	a1i 11	. . . . 5 ⊢ ((⊤ ∧ (𝑦 ∈ ℝ ∧ 1 ≤ 𝑦)) → 2 ∈ ℝ)
53	22	a1i 11	. . . . . . 7 ⊢ ((⊤ ∧ (𝑦 ∈ ℝ ∧ 1 ≤ 𝑦)) → 1 ∈ ℝ+)
54		simprr 773	. . . . . . 7 ⊢ ((⊤ ∧ (𝑦 ∈ ℝ ∧ 1 ≤ 𝑦)) → 1 ≤ 𝑦)
55	44, 53, 54	rpgecld 12566	. . . . . 6 ⊢ ((⊤ ∧ (𝑦 ∈ ℝ ∧ 1 ≤ 𝑦)) → 𝑦 ∈ ℝ+)
56	55	relogcld 25379	. . . . 5 ⊢ ((⊤ ∧ (𝑦 ∈ ℝ ∧ 1 ≤ 𝑦)) → (log‘𝑦) ∈ ℝ)
57	52, 56	remulcld 10762	. . . 4 ⊢ ((⊤ ∧ (𝑦 ∈ ℝ ∧ 1 ≤ 𝑦)) → (2 · (log‘𝑦)) ∈ ℝ)
58	51, 57	readdcld 10761	. . 3 ⊢ ((⊤ ∧ (𝑦 ∈ ℝ ∧ 1 ≤ 𝑦)) → (Σ𝑛 ∈ (1...(⌊‘𝑦))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑦 / 𝑛)))) + (2 · (log‘𝑦))) ∈ ℝ)
59	31	adantr 484	. . . . . 6 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) − (2 · (log‘𝑥))) ∈ ℝ)
60	59	recnd 10760	. . . . 5 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) − (2 · (log‘𝑥))) ∈ ℂ)
61	60	abscld 14899	. . . 4 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) − (2 · (log‘𝑥)))) ∈ ℝ)
62	26	adantr 484	. . . . 5 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) ∈ ℝ)
63	30	adantr 484	. . . . 5 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (2 · (log‘𝑥)) ∈ ℝ)
64	62, 63	readdcld 10761	. . . 4 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) + (2 · (log‘𝑥))) ∈ ℝ)
65		fzfid 13445	. . . . . 6 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (1...(⌊‘𝑦)) ∈ Fin)
66	39	adantl 485	. . . . . . . 8 ⊢ ((((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → 𝑛 ∈ ℕ)
67	66, 11	syl 17	. . . . . . 7 ⊢ ((((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → (Λ‘𝑛) ∈ ℝ)
68	66	nnrpd 12525	. . . . . . . . 9 ⊢ ((((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → 𝑛 ∈ ℝ+)
69	68	relogcld 25379	. . . . . . . 8 ⊢ ((((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → (log‘𝑛) ∈ ℝ)
70		simprll 779	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 𝑦 ∈ ℝ)
71	70	adantr 484	. . . . . . . . . 10 ⊢ ((((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → 𝑦 ∈ ℝ)
72	71, 66	nndivred 11783	. . . . . . . . 9 ⊢ ((((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → (𝑦 / 𝑛) ∈ ℝ)
73	72, 47	syl 17	. . . . . . . 8 ⊢ ((((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → (ψ‘(𝑦 / 𝑛)) ∈ ℝ)
74	69, 73	readdcld 10761	. . . . . . 7 ⊢ ((((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → ((log‘𝑛) + (ψ‘(𝑦 / 𝑛))) ∈ ℝ)
75	67, 74	remulcld 10762	. . . . . 6 ⊢ ((((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → ((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑦 / 𝑛)))) ∈ ℝ)
76	65, 75	fsumrecl 15197	. . . . 5 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → Σ𝑛 ∈ (1...(⌊‘𝑦))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑦 / 𝑛)))) ∈ ℝ)
77	27	a1i 11	. . . . . 6 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 2 ∈ ℝ)
78	25	adantr 484	. . . . . . . 8 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 𝑥 ∈ ℝ+)
79	4	adantr 484	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 𝑥 ∈ ℝ)
80		simprr 773	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 𝑥 < 𝑦)
81	79, 70, 80	ltled 10879	. . . . . . . 8 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 𝑥 ≤ 𝑦)
82	70, 78, 81	rpgecld 12566	. . . . . . 7 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 𝑦 ∈ ℝ+)
83	82	relogcld 25379	. . . . . 6 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (log‘𝑦) ∈ ℝ)
84	77, 83	remulcld 10762	. . . . 5 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (2 · (log‘𝑦)) ∈ ℝ)
85	76, 84	readdcld 10761	. . . 4 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (Σ𝑛 ∈ (1...(⌊‘𝑦))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑦 / 𝑛)))) + (2 · (log‘𝑦))) ∈ ℝ)
86	62	recnd 10760	. . . . . 6 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) ∈ ℂ)
87	63	recnd 10760	. . . . . 6 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (2 · (log‘𝑥)) ∈ ℂ)
88	86, 87	abs2dif2d 14921	. . . . 5 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) − (2 · (log‘𝑥)))) ≤ ((abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥)) + (abs‘(2 · (log‘𝑥)))))
89	21	adantr 484	. . . . . . . 8 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) ∈ ℝ)
90		vmage0 25871	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → 0 ≤ (Λ‘𝑛))
91	10, 90	syl 17	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (Λ‘𝑛))
92	10	nnred 11744	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ)
93	10	nnge1d 11777	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ≤ 𝑛)
94	92, 93	logge0d 25386	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (log‘𝑛))
95		chpge0 25876	. . . . . . . . . . . . 13 ⊢ ((𝑥 / 𝑛) ∈ ℝ → 0 ≤ (ψ‘(𝑥 / 𝑛)))
96	16, 95	syl 17	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (ψ‘(𝑥 / 𝑛)))
97	14, 18, 94, 96	addge0d 11307	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ ((log‘𝑛) + (ψ‘(𝑥 / 𝑛))))
98	12, 19, 91, 97	mulge0d 11308	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ ((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))))
99	8, 20, 98	fsumge0 15256	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1[,)+∞)) → 0 ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))))
100	99	adantr 484	. . . . . . . 8 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 0 ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))))
101	89, 78, 100	divge0d 12567	. . . . . . 7 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 0 ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥))
102	62, 101	absidd 14885	. . . . . 6 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥))
103	78	relogcld 25379	. . . . . . . 8 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (log‘𝑥) ∈ ℝ)
104		2rp 12490	. . . . . . . . 9 ⊢ 2 ∈ ℝ+
105		rpge0 12498	. . . . . . . . 9 ⊢ (2 ∈ ℝ+ → 0 ≤ 2)
106	104, 105	mp1i 13	. . . . . . . 8 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 0 ≤ 2)
107	24	adantr 484	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 1 ≤ 𝑥)
108	79, 107	logge0d 25386	. . . . . . . 8 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 0 ≤ (log‘𝑥))
109	77, 103, 106, 108	mulge0d 11308	. . . . . . 7 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 0 ≤ (2 · (log‘𝑥)))
110	63, 109	absidd 14885	. . . . . 6 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (abs‘(2 · (log‘𝑥))) = (2 · (log‘𝑥)))
111	102, 110	oveq12d 7201	. . . . 5 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → ((abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥)) + (abs‘(2 · (log‘𝑥)))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) + (2 · (log‘𝑥))))
112	88, 111	breqtrd 5066	. . . 4 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) − (2 · (log‘𝑥)))) ≤ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) + (2 · (log‘𝑥))))
113	22	a1i 11	. . . . . . 7 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → 1 ∈ ℝ+)
114	79	adantr 484	. . . . . . . . . . . . 13 ⊢ ((((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → 𝑥 ∈ ℝ)
115	114, 66	nndivred 11783	. . . . . . . . . . . 12 ⊢ ((((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → (𝑥 / 𝑛) ∈ ℝ)
116	115, 17	syl 17	. . . . . . . . . . 11 ⊢ ((((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → (ψ‘(𝑥 / 𝑛)) ∈ ℝ)
117	69, 116	readdcld 10761	. . . . . . . . . 10 ⊢ ((((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → ((log‘𝑛) + (ψ‘(𝑥 / 𝑛))) ∈ ℝ)
118	67, 117	remulcld 10762	. . . . . . . . 9 ⊢ ((((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → ((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) ∈ ℝ)
119	65, 118	fsumrecl 15197	. . . . . . . 8 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → Σ𝑛 ∈ (1...(⌊‘𝑦))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) ∈ ℝ)
120	66, 90	syl 17	. . . . . . . . . 10 ⊢ ((((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → 0 ≤ (Λ‘𝑛))
121	66	nnred 11744	. . . . . . . . . . . 12 ⊢ ((((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → 𝑛 ∈ ℝ)
122	66	nnge1d 11777	. . . . . . . . . . . 12 ⊢ ((((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → 1 ≤ 𝑛)
123	121, 122	logge0d 25386	. . . . . . . . . . 11 ⊢ ((((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → 0 ≤ (log‘𝑛))
124	115, 95	syl 17	. . . . . . . . . . 11 ⊢ ((((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → 0 ≤ (ψ‘(𝑥 / 𝑛)))
125	69, 116, 123, 124	addge0d 11307	. . . . . . . . . 10 ⊢ ((((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → 0 ≤ ((log‘𝑛) + (ψ‘(𝑥 / 𝑛))))
126	67, 117, 120, 125	mulge0d 11308	. . . . . . . . 9 ⊢ ((((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → 0 ≤ ((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))))
127		flword2 13287	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 ≤ 𝑦) → (⌊‘𝑦) ∈ (ℤ≥‘(⌊‘𝑥)))
128	79, 70, 81, 127	syl3anc 1372	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (⌊‘𝑦) ∈ (ℤ≥‘(⌊‘𝑥)))
129		fzss2 13051	. . . . . . . . . 10 ⊢ ((⌊‘𝑦) ∈ (ℤ≥‘(⌊‘𝑥)) → (1...(⌊‘𝑥)) ⊆ (1...(⌊‘𝑦)))
130	128, 129	syl 17	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (1...(⌊‘𝑥)) ⊆ (1...(⌊‘𝑦)))
131	65, 118, 126, 130	fsumless 15257	. . . . . . . 8 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑦))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))))
132	81	adantr 484	. . . . . . . . . . . . 13 ⊢ ((((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → 𝑥 ≤ 𝑦)
133	114, 71, 68, 132	lediv1dd 12585	. . . . . . . . . . . 12 ⊢ ((((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → (𝑥 / 𝑛) ≤ (𝑦 / 𝑛))
134		chpwordi 25907	. . . . . . . . . . . 12 ⊢ (((𝑥 / 𝑛) ∈ ℝ ∧ (𝑦 / 𝑛) ∈ ℝ ∧ (𝑥 / 𝑛) ≤ (𝑦 / 𝑛)) → (ψ‘(𝑥 / 𝑛)) ≤ (ψ‘(𝑦 / 𝑛)))
135	115, 72, 133, 134	syl3anc 1372	. . . . . . . . . . 11 ⊢ ((((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → (ψ‘(𝑥 / 𝑛)) ≤ (ψ‘(𝑦 / 𝑛)))
136	116, 73, 69, 135	leadd2dd 11346	. . . . . . . . . 10 ⊢ ((((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → ((log‘𝑛) + (ψ‘(𝑥 / 𝑛))) ≤ ((log‘𝑛) + (ψ‘(𝑦 / 𝑛))))
137	117, 74, 67, 120, 136	lemul2ad 11671	. . . . . . . . 9 ⊢ ((((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) ∧ 𝑛 ∈ (1...(⌊‘𝑦))) → ((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) ≤ ((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑦 / 𝑛)))))
138	65, 118, 75, 137	fsumle 15260	. . . . . . . 8 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → Σ𝑛 ∈ (1...(⌊‘𝑦))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑦))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑦 / 𝑛)))))
139	89, 119, 76, 131, 138	letrd 10888	. . . . . . 7 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑦))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑦 / 𝑛)))))
140	89, 76, 113, 79, 100, 139, 107	lediv12ad 12586	. . . . . 6 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑦))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑦 / 𝑛)))) / 1))
141	76	recnd 10760	. . . . . . 7 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → Σ𝑛 ∈ (1...(⌊‘𝑦))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑦 / 𝑛)))) ∈ ℂ)
142	141	div1d 11499	. . . . . 6 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (Σ𝑛 ∈ (1...(⌊‘𝑦))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑦 / 𝑛)))) / 1) = Σ𝑛 ∈ (1...(⌊‘𝑦))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑦 / 𝑛)))))
143	140, 142	breqtrd 5066	. . . . 5 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) ≤ Σ𝑛 ∈ (1...(⌊‘𝑦))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑦 / 𝑛)))))
144	78, 82	logled 25383	. . . . . . 7 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (𝑥 ≤ 𝑦 ↔ (log‘𝑥) ≤ (log‘𝑦)))
145	81, 144	mpbid 235	. . . . . 6 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (log‘𝑥) ≤ (log‘𝑦))
146	103, 83, 77, 106, 145	lemul2ad 11671	. . . . 5 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (2 · (log‘𝑥)) ≤ (2 · (log‘𝑦)))
147	62, 63, 76, 84, 143, 146	le2addd 11350	. . . 4 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) + (2 · (log‘𝑥))) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑦))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑦 / 𝑛)))) + (2 · (log‘𝑦))))
148	61, 64, 85, 112, 147	letrd 10888	. . 3 ⊢ (((⊤ ∧ 𝑥 ∈ (1[,)+∞)) ∧ ((𝑦 ∈ ℝ ∧ 1 ≤ 𝑦) ∧ 𝑥 < 𝑦)) → (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) − (2 · (log‘𝑥)))) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑦))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑦 / 𝑛)))) + (2 · (log‘𝑦))))
149	6, 7, 32, 37, 58, 148	o1bddrp 15002	. 2 ⊢ (⊤ → ∃𝑐 ∈ ℝ+ ∀𝑥 ∈ (1[,)+∞)(abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) − (2 · (log‘𝑥)))) ≤ 𝑐)
150	149	mptru 1549	1 ⊢ ∃𝑐 ∈ ℝ+ ∀𝑥 ∈ (1[,)+∞)(abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) − (2 · (log‘𝑥)))) ≤ 𝑐

Syntax hints:   ↔ wb 209   ∧ wa 399  ⊤wtru 1543   ∈ wcel 2114  ∀wral 3054  ∃wrex 3055   ⊆ wss 3853   class class class wbr 5040   ↦ cmpt 5120  ‘cfv 6350  (class class class)co 7183  ℝcr 10627  0cc0 10628  1c1 10629   + caddc 10631   · cmul 10633  +∞cpnf 10763   < clt 10766   ≤ cle 10767   − cmin 10961   / cdiv 11388  ℕcn 11729  2c2 11784  ℤ_≥cuz 12337  ℝ⁺crp 12485  [,)cico 12836  ...cfz 12994  ⌊cfl 13264  abscabs 14696  𝑂(1)co1 14946  Σcsu 15148  logclog 25311  Λcvma 25842  ψcchp 25843

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 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2711  ax-rep 5164  ax-sep 5177  ax-nul 5184  ax-pow 5242  ax-pr 5306  ax-un 7492  ax-inf2 9190  ax-cnex 10684  ax-resscn 10685  ax-1cn 10686  ax-icn 10687  ax-addcl 10688  ax-addrcl 10689  ax-mulcl 10690  ax-mulrcl 10691  ax-mulcom 10692  ax-addass 10693  ax-mulass 10694  ax-distr 10695  ax-i2m1 10696  ax-1ne0 10697  ax-1rid 10698  ax-rnegex 10699  ax-rrecex 10700  ax-cnre 10701  ax-pre-lttri 10702  ax-pre-lttrn 10703  ax-pre-ltadd 10704  ax-pre-mulgt0 10705  ax-pre-sup 10706  ax-addf 10707  ax-mulf 10708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2541  df-eu 2571  df-clab 2718  df-cleq 2731  df-clel 2812  df-nfc 2882  df-ne 2936  df-nel 3040  df-ral 3059  df-rex 3060  df-reu 3061  df-rmo 3062  df-rab 3063  df-v 3402  df-sbc 3686  df-csb 3801  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-pss 3872  df-nul 4222  df-if 4425  df-pw 4500  df-sn 4527  df-pr 4529  df-tp 4531  df-op 4533  df-uni 4807  df-int 4847  df-iun 4893  df-iin 4894  df-disj 5006  df-br 5041  df-opab 5103  df-mpt 5121  df-tr 5147  df-id 5439  df-eprel 5444  df-po 5452  df-so 5453  df-fr 5493  df-se 5494  df-we 5495  df-xp 5541  df-rel 5542  df-cnv 5543  df-co 5544  df-dm 5545  df-rn 5546  df-res 5547  df-ima 5548  df-pred 6139  df-ord 6186  df-on 6187  df-lim 6188  df-suc 6189  df-iota 6308  df-fun 6352  df-fn 6353  df-f 6354  df-f1 6355  df-fo 6356  df-f1o 6357  df-fv 6358  df-isom 6359  df-riota 7140  df-ov 7186  df-oprab 7187  df-mpo 7188  df-of 7438  df-om 7613  df-1st 7727  df-2nd 7728  df-supp 7870  df-wrecs 7989  df-recs 8050  df-rdg 8088  df-1o 8144  df-2o 8145  df-oadd 8148  df-er 8333  df-map 8452  df-pm 8453  df-ixp 8521  df-en 8569  df-dom 8570  df-sdom 8571  df-fin 8572  df-fsupp 8920  df-fi 8961  df-sup 8992  df-inf 8993  df-oi 9060  df-dju 9416  df-card 9454  df-pnf 10768  df-mnf 10769  df-xr 10770  df-ltxr 10771  df-le 10772  df-sub 10963  df-neg 10964  df-div 11389  df-nn 11730  df-2 11792  df-3 11793  df-4 11794  df-5 11795  df-6 11796  df-7 11797  df-8 11798  df-9 11799  df-n0 11990  df-xnn0 12062  df-z 12076  df-dec 12193  df-uz 12338  df-q 12444  df-rp 12486  df-xneg 12603  df-xadd 12604  df-xmul 12605  df-ioo 12838  df-ioc 12839  df-ico 12840  df-icc 12841  df-fz 12995  df-fzo 13138  df-fl 13266  df-mod 13342  df-seq 13474  df-exp 13535  df-fac 13739  df-bc 13768  df-hash 13796  df-shft 14529  df-cj 14561  df-re 14562  df-im 14563  df-sqrt 14697  df-abs 14698  df-limsup 14931  df-clim 14948  df-rlim 14949  df-o1 14950  df-lo1 14951  df-sum 15149  df-ef 15526  df-e 15527  df-sin 15528  df-cos 15529  df-tan 15530  df-pi 15531  df-dvds 15713  df-gcd 15951  df-prm 16126  df-pc 16287  df-struct 16601  df-ndx 16602  df-slot 16603  df-base 16605  df-sets 16606  df-ress 16607  df-plusg 16694  df-mulr 16695  df-starv 16696  df-sca 16697  df-vsca 16698  df-ip 16699  df-tset 16700  df-ple 16701  df-ds 16703  df-unif 16704  df-hom 16705  df-cco 16706  df-rest 16812  df-topn 16813  df-0g 16831  df-gsum 16832  df-topgen 16833  df-pt 16834  df-prds 16837  df-xrs 16891  df-qtop 16896  df-imas 16897  df-xps 16899  df-mre 16973  df-mrc 16974  df-acs 16976  df-mgm 17981  df-sgrp 18030  df-mnd 18041  df-submnd 18086  df-mulg 18356  df-cntz 18578  df-cmn 19039  df-psmet 20222  df-xmet 20223  df-met 20224  df-bl 20225  df-mopn 20226  df-fbas 20227  df-fg 20228  df-cnfld 20231  df-top 21658  df-topon 21675  df-topsp 21697  df-bases 21710  df-cld 21783  df-ntr 21784  df-cls 21785  df-nei 21862  df-lp 21900  df-perf 21901  df-cn 21991  df-cnp 21992  df-haus 22079  df-cmp 22151  df-tx 22326  df-hmeo 22519  df-fil 22610  df-fm 22702  df-flim 22703  df-flf 22704  df-xms 23086  df-ms 23087  df-tms 23088  df-cncf 23643  df-limc 24631  df-dv 24632  df-ulm 25137  df-log 25313  df-cxp 25314  df-atan 25618  df-em 25743  df-vma 25848  df-chp 25849  df-mu 25851

This theorem is referenced by:  selberg4  26310  selbergsb  26324