Theorem selberg2b

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

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