Theorem selbergb

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

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

Proof

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