Theorem selberg2lem

Description: Lemma for selberg2 . Equation 10.4.12 of Shapiro, p. 420. (Contributed by Mario Carneiro, 23-May-2016)

	Ref	Expression
Assertion	selberg2lem	⊢ ( 𝑥 ∈ ℝ+ ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) − ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / 𝑥 ) ) ∈ 𝑂(1)

Proof

Step	Hyp	Ref	Expression
1		rpre	⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ )
2		chpcl	⊢ ( 𝑥 ∈ ℝ → ( ψ ‘ 𝑥 ) ∈ ℝ )
3	1 2	syl	⊢ ( 𝑥 ∈ ℝ+ → ( ψ ‘ 𝑥 ) ∈ ℝ )
4	3	recnd	⊢ ( 𝑥 ∈ ℝ+ → ( ψ ‘ 𝑥 ) ∈ ℂ )
5		rprege0	⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) )
6		flge0nn0	⊢ ( ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) → ( ⌊ ‘ 𝑥 ) ∈ ℕ0 )
7	5 6	syl	⊢ ( 𝑥 ∈ ℝ+ → ( ⌊ ‘ 𝑥 ) ∈ ℕ0 )
8		nn0p1nn	⊢ ( ( ⌊ ‘ 𝑥 ) ∈ ℕ0 → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℕ )
9	7 8	syl	⊢ ( 𝑥 ∈ ℝ+ → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℕ )
10	9	nnrpd	⊢ ( 𝑥 ∈ ℝ+ → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℝ+ )
11	10	relogcld	⊢ ( 𝑥 ∈ ℝ+ → ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ∈ ℝ )
12	11	recnd	⊢ ( 𝑥 ∈ ℝ+ → ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ∈ ℂ )
13		relogcl	⊢ ( 𝑥 ∈ ℝ+ → ( log ‘ 𝑥 ) ∈ ℝ )
14	13	recnd	⊢ ( 𝑥 ∈ ℝ+ → ( log ‘ 𝑥 ) ∈ ℂ )
15	12 14	subcld	⊢ ( 𝑥 ∈ ℝ+ → ( ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − ( log ‘ 𝑥 ) ) ∈ ℂ )
16	4 15	mulcld	⊢ ( 𝑥 ∈ ℝ+ → ( ( ψ ‘ 𝑥 ) · ( ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − ( log ‘ 𝑥 ) ) ) ∈ ℂ )
17		fzfid	⊢ ( 𝑥 ∈ ℝ+ → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
18		elfznn	⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℕ )
19	18	adantl	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℕ )
20	19	nnrpd	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℝ+ )
21		1rp	⊢ 1 ∈ ℝ+
22		rpaddcl	⊢ ( ( 𝑛 ∈ ℝ+ ∧ 1 ∈ ℝ+ ) → ( 𝑛 + 1 ) ∈ ℝ+ )
23	21 22	mpan2	⊢ ( 𝑛 ∈ ℝ+ → ( 𝑛 + 1 ) ∈ ℝ+ )
24	23	relogcld	⊢ ( 𝑛 ∈ ℝ+ → ( log ‘ ( 𝑛 + 1 ) ) ∈ ℝ )
25		relogcl	⊢ ( 𝑛 ∈ ℝ+ → ( log ‘ 𝑛 ) ∈ ℝ )
26	24 25	resubcld	⊢ ( 𝑛 ∈ ℝ+ → ( ( log ‘ ( 𝑛 + 1 ) ) − ( log ‘ 𝑛 ) ) ∈ ℝ )
27		rpre	⊢ ( 𝑛 ∈ ℝ+ → 𝑛 ∈ ℝ )
28		chpcl	⊢ ( 𝑛 ∈ ℝ → ( ψ ‘ 𝑛 ) ∈ ℝ )
29	27 28	syl	⊢ ( 𝑛 ∈ ℝ+ → ( ψ ‘ 𝑛 ) ∈ ℝ )
30	26 29	remulcld	⊢ ( 𝑛 ∈ ℝ+ → ( ( ( log ‘ ( 𝑛 + 1 ) ) − ( log ‘ 𝑛 ) ) · ( ψ ‘ 𝑛 ) ) ∈ ℝ )
31	30	recnd	⊢ ( 𝑛 ∈ ℝ+ → ( ( ( log ‘ ( 𝑛 + 1 ) ) − ( log ‘ 𝑛 ) ) · ( ψ ‘ 𝑛 ) ) ∈ ℂ )
32	20 31	syl	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( log ‘ ( 𝑛 + 1 ) ) − ( log ‘ 𝑛 ) ) · ( ψ ‘ 𝑛 ) ) ∈ ℂ )
33	17 32	fsumcl	⊢ ( 𝑥 ∈ ℝ+ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( log ‘ ( 𝑛 + 1 ) ) − ( log ‘ 𝑛 ) ) · ( ψ ‘ 𝑛 ) ) ∈ ℂ )
34		rpcnne0	⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) )
35		divsubdir	⊢ ( ( ( ( ψ ‘ 𝑥 ) · ( ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − ( log ‘ 𝑥 ) ) ) ∈ ℂ ∧ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( log ‘ ( 𝑛 + 1 ) ) − ( log ‘ 𝑛 ) ) · ( ψ ‘ 𝑛 ) ) ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ) → ( ( ( ( ψ ‘ 𝑥 ) · ( ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − ( log ‘ 𝑥 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( log ‘ ( 𝑛 + 1 ) ) − ( log ‘ 𝑛 ) ) · ( ψ ‘ 𝑛 ) ) ) / 𝑥 ) = ( ( ( ( ψ ‘ 𝑥 ) · ( ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − ( log ‘ 𝑥 ) ) ) / 𝑥 ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( log ‘ ( 𝑛 + 1 ) ) − ( log ‘ 𝑛 ) ) · ( ψ ‘ 𝑛 ) ) / 𝑥 ) ) )
36	16 33 34 35	syl3anc	⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ( ψ ‘ 𝑥 ) · ( ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − ( log ‘ 𝑥 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( log ‘ ( 𝑛 + 1 ) ) − ( log ‘ 𝑛 ) ) · ( ψ ‘ 𝑛 ) ) ) / 𝑥 ) = ( ( ( ( ψ ‘ 𝑥 ) · ( ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − ( log ‘ 𝑥 ) ) ) / 𝑥 ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( log ‘ ( 𝑛 + 1 ) ) − ( log ‘ 𝑛 ) ) · ( ψ ‘ 𝑛 ) ) / 𝑥 ) ) )
37	4 12	mulcld	⊢ ( 𝑥 ∈ ℝ+ → ( ( ψ ‘ 𝑥 ) · ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ∈ ℂ )
38	4 14	mulcld	⊢ ( 𝑥 ∈ ℝ+ → ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ∈ ℂ )
39	37 38 33	sub32d	⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) − ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( log ‘ ( 𝑛 + 1 ) ) − ( log ‘ 𝑛 ) ) · ( ψ ‘ 𝑛 ) ) ) = ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( log ‘ ( 𝑛 + 1 ) ) − ( log ‘ 𝑛 ) ) · ( ψ ‘ 𝑛 ) ) ) − ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) )
40	4 12 14	subdid	⊢ ( 𝑥 ∈ ℝ+ → ( ( ψ ‘ 𝑥 ) · ( ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − ( log ‘ 𝑥 ) ) ) = ( ( ( ψ ‘ 𝑥 ) · ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) − ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) )
41	40	oveq1d	⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ψ ‘ 𝑥 ) · ( ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − ( log ‘ 𝑥 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( log ‘ ( 𝑛 + 1 ) ) − ( log ‘ 𝑛 ) ) · ( ψ ‘ 𝑛 ) ) ) = ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) − ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( log ‘ ( 𝑛 + 1 ) ) − ( log ‘ 𝑛 ) ) · ( ψ ‘ 𝑛 ) ) ) )
42		fveq2	⊢ ( 𝑚 = 𝑛 → ( log ‘ 𝑚 ) = ( log ‘ 𝑛 ) )
43		fvoveq1	⊢ ( 𝑚 = 𝑛 → ( ψ ‘ ( 𝑚 − 1 ) ) = ( ψ ‘ ( 𝑛 − 1 ) ) )
44	42 43	jca	⊢ ( 𝑚 = 𝑛 → ( ( log ‘ 𝑚 ) = ( log ‘ 𝑛 ) ∧ ( ψ ‘ ( 𝑚 − 1 ) ) = ( ψ ‘ ( 𝑛 − 1 ) ) ) )
45		fveq2	⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( log ‘ 𝑚 ) = ( log ‘ ( 𝑛 + 1 ) ) )
46		fvoveq1	⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( ψ ‘ ( 𝑚 − 1 ) ) = ( ψ ‘ ( ( 𝑛 + 1 ) − 1 ) ) )
47	45 46	jca	⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( ( log ‘ 𝑚 ) = ( log ‘ ( 𝑛 + 1 ) ) ∧ ( ψ ‘ ( 𝑚 − 1 ) ) = ( ψ ‘ ( ( 𝑛 + 1 ) − 1 ) ) ) )
48		fveq2	⊢ ( 𝑚 = 1 → ( log ‘ 𝑚 ) = ( log ‘ 1 ) )
49		log1	⊢ ( log ‘ 1 ) = 0
50	48 49	eqtrdi	⊢ ( 𝑚 = 1 → ( log ‘ 𝑚 ) = 0 )
51		oveq1	⊢ ( 𝑚 = 1 → ( 𝑚 − 1 ) = ( 1 − 1 ) )
52		1m1e0	⊢ ( 1 − 1 ) = 0
53	51 52	eqtrdi	⊢ ( 𝑚 = 1 → ( 𝑚 − 1 ) = 0 )
54	53	fveq2d	⊢ ( 𝑚 = 1 → ( ψ ‘ ( 𝑚 − 1 ) ) = ( ψ ‘ 0 ) )
55		2pos	⊢ 0 < 2
56		0re	⊢ 0 ∈ ℝ
57		chpeq0	⊢ ( 0 ∈ ℝ → ( ( ψ ‘ 0 ) = 0 ↔ 0 < 2 ) )
58	56 57	ax-mp	⊢ ( ( ψ ‘ 0 ) = 0 ↔ 0 < 2 )
59	55 58	mpbir	⊢ ( ψ ‘ 0 ) = 0
60	54 59	eqtrdi	⊢ ( 𝑚 = 1 → ( ψ ‘ ( 𝑚 − 1 ) ) = 0 )
61	50 60	jca	⊢ ( 𝑚 = 1 → ( ( log ‘ 𝑚 ) = 0 ∧ ( ψ ‘ ( 𝑚 − 1 ) ) = 0 ) )
62		fveq2	⊢ ( 𝑚 = ( ( ⌊ ‘ 𝑥 ) + 1 ) → ( log ‘ 𝑚 ) = ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) )
63		fvoveq1	⊢ ( 𝑚 = ( ( ⌊ ‘ 𝑥 ) + 1 ) → ( ψ ‘ ( 𝑚 − 1 ) ) = ( ψ ‘ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) )
64	62 63	jca	⊢ ( 𝑚 = ( ( ⌊ ‘ 𝑥 ) + 1 ) → ( ( log ‘ 𝑚 ) = ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ∧ ( ψ ‘ ( 𝑚 − 1 ) ) = ( ψ ‘ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) ) )
65		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
66	9 65	eleqtrdi	⊢ ( 𝑥 ∈ ℝ+ → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
67		elfznn	⊢ ( 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝑥 ) + 1 ) ) → 𝑚 ∈ ℕ )
68	67	adantl	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → 𝑚 ∈ ℕ )
69	68	nnrpd	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → 𝑚 ∈ ℝ+ )
70	69	relogcld	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → ( log ‘ 𝑚 ) ∈ ℝ )
71	70	recnd	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → ( log ‘ 𝑚 ) ∈ ℂ )
72	68	nnred	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → 𝑚 ∈ ℝ )
73		peano2rem	⊢ ( 𝑚 ∈ ℝ → ( 𝑚 − 1 ) ∈ ℝ )
74	72 73	syl	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → ( 𝑚 − 1 ) ∈ ℝ )
75		chpcl	⊢ ( ( 𝑚 − 1 ) ∈ ℝ → ( ψ ‘ ( 𝑚 − 1 ) ) ∈ ℝ )
76	74 75	syl	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → ( ψ ‘ ( 𝑚 − 1 ) ) ∈ ℝ )
77	76	recnd	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → ( ψ ‘ ( 𝑚 − 1 ) ) ∈ ℂ )
78	44 47 61 64 66 71 77	fsumparts	⊢ ( 𝑥 ∈ ℝ+ → Σ 𝑛 ∈ ( 1 ..^ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ( ( log ‘ 𝑛 ) · ( ( ψ ‘ ( ( 𝑛 + 1 ) − 1 ) ) − ( ψ ‘ ( 𝑛 − 1 ) ) ) ) = ( ( ( ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ψ ‘ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) ) − ( 0 · 0 ) ) − Σ 𝑛 ∈ ( 1 ..^ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ( ( ( log ‘ ( 𝑛 + 1 ) ) − ( log ‘ 𝑛 ) ) · ( ψ ‘ ( ( 𝑛 + 1 ) − 1 ) ) ) ) )
79	7	nn0zd	⊢ ( 𝑥 ∈ ℝ+ → ( ⌊ ‘ 𝑥 ) ∈ ℤ )
80		fzval3	⊢ ( ( ⌊ ‘ 𝑥 ) ∈ ℤ → ( 1 ... ( ⌊ ‘ 𝑥 ) ) = ( 1 ..^ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) )
81	79 80	syl	⊢ ( 𝑥 ∈ ℝ+ → ( 1 ... ( ⌊ ‘ 𝑥 ) ) = ( 1 ..^ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) )
82	81	eqcomd	⊢ ( 𝑥 ∈ ℝ+ → ( 1 ..^ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) = ( 1 ... ( ⌊ ‘ 𝑥 ) ) )
83		nnm1nn0	⊢ ( 𝑛 ∈ ℕ → ( 𝑛 − 1 ) ∈ ℕ0 )
84	19 83	syl	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑛 − 1 ) ∈ ℕ0 )
85	84	nn0red	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑛 − 1 ) ∈ ℝ )
86		chpcl	⊢ ( ( 𝑛 − 1 ) ∈ ℝ → ( ψ ‘ ( 𝑛 − 1 ) ) ∈ ℝ )
87	85 86	syl	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ψ ‘ ( 𝑛 − 1 ) ) ∈ ℝ )
88	87	recnd	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ψ ‘ ( 𝑛 − 1 ) ) ∈ ℂ )
89		vmacl	⊢ ( 𝑛 ∈ ℕ → ( Λ ‘ 𝑛 ) ∈ ℝ )
90	19 89	syl	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℝ )
91	90	recnd	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℂ )
92	19	nncnd	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℂ )
93		ax-1cn	⊢ 1 ∈ ℂ
94		pncan	⊢ ( ( 𝑛 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑛 + 1 ) − 1 ) = 𝑛 )
95	92 93 94	sylancl	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑛 + 1 ) − 1 ) = 𝑛 )
96		npcan	⊢ ( ( 𝑛 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑛 − 1 ) + 1 ) = 𝑛 )
97	92 93 96	sylancl	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑛 − 1 ) + 1 ) = 𝑛 )
98	95 97	eqtr4d	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑛 + 1 ) − 1 ) = ( ( 𝑛 − 1 ) + 1 ) )
99	98	fveq2d	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ψ ‘ ( ( 𝑛 + 1 ) − 1 ) ) = ( ψ ‘ ( ( 𝑛 − 1 ) + 1 ) ) )
100		chpp1	⊢ ( ( 𝑛 − 1 ) ∈ ℕ0 → ( ψ ‘ ( ( 𝑛 − 1 ) + 1 ) ) = ( ( ψ ‘ ( 𝑛 − 1 ) ) + ( Λ ‘ ( ( 𝑛 − 1 ) + 1 ) ) ) )
101	84 100	syl	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ψ ‘ ( ( 𝑛 − 1 ) + 1 ) ) = ( ( ψ ‘ ( 𝑛 − 1 ) ) + ( Λ ‘ ( ( 𝑛 − 1 ) + 1 ) ) ) )
102	97	fveq2d	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ ( ( 𝑛 − 1 ) + 1 ) ) = ( Λ ‘ 𝑛 ) )
103	102	oveq2d	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ψ ‘ ( 𝑛 − 1 ) ) + ( Λ ‘ ( ( 𝑛 − 1 ) + 1 ) ) ) = ( ( ψ ‘ ( 𝑛 − 1 ) ) + ( Λ ‘ 𝑛 ) ) )
104	99 101 103	3eqtrd	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ψ ‘ ( ( 𝑛 + 1 ) − 1 ) ) = ( ( ψ ‘ ( 𝑛 − 1 ) ) + ( Λ ‘ 𝑛 ) ) )
105	88 91 104	mvrladdd	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ψ ‘ ( ( 𝑛 + 1 ) − 1 ) ) − ( ψ ‘ ( 𝑛 − 1 ) ) ) = ( Λ ‘ 𝑛 ) )
106	105	oveq2d	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( log ‘ 𝑛 ) · ( ( ψ ‘ ( ( 𝑛 + 1 ) − 1 ) ) − ( ψ ‘ ( 𝑛 − 1 ) ) ) ) = ( ( log ‘ 𝑛 ) · ( Λ ‘ 𝑛 ) ) )
107	20	relogcld	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ 𝑛 ) ∈ ℝ )
108	107	recnd	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ 𝑛 ) ∈ ℂ )
109	91 108	mulcomd	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) = ( ( log ‘ 𝑛 ) · ( Λ ‘ 𝑛 ) ) )
110	106 109	eqtr4d	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( log ‘ 𝑛 ) · ( ( ψ ‘ ( ( 𝑛 + 1 ) − 1 ) ) − ( ψ ‘ ( 𝑛 − 1 ) ) ) ) = ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) )
111	82 110	sumeq12rdv	⊢ ( 𝑥 ∈ ℝ+ → Σ 𝑛 ∈ ( 1 ..^ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ( ( log ‘ 𝑛 ) · ( ( ψ ‘ ( ( 𝑛 + 1 ) − 1 ) ) − ( ψ ‘ ( 𝑛 − 1 ) ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) )
112	7	nn0cnd	⊢ ( 𝑥 ∈ ℝ+ → ( ⌊ ‘ 𝑥 ) ∈ ℂ )
113		pncan	⊢ ( ( ( ⌊ ‘ 𝑥 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) = ( ⌊ ‘ 𝑥 ) )
114	112 93 113	sylancl	⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) = ( ⌊ ‘ 𝑥 ) )
115	114	fveq2d	⊢ ( 𝑥 ∈ ℝ+ → ( ψ ‘ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) = ( ψ ‘ ( ⌊ ‘ 𝑥 ) ) )
116		chpfl	⊢ ( 𝑥 ∈ ℝ → ( ψ ‘ ( ⌊ ‘ 𝑥 ) ) = ( ψ ‘ 𝑥 ) )
117	1 116	syl	⊢ ( 𝑥 ∈ ℝ+ → ( ψ ‘ ( ⌊ ‘ 𝑥 ) ) = ( ψ ‘ 𝑥 ) )
118	115 117	eqtrd	⊢ ( 𝑥 ∈ ℝ+ → ( ψ ‘ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) = ( ψ ‘ 𝑥 ) )
119	118	oveq2d	⊢ ( 𝑥 ∈ ℝ+ → ( ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ψ ‘ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) ) = ( ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ψ ‘ 𝑥 ) ) )
120	12 4	mulcomd	⊢ ( 𝑥 ∈ ℝ+ → ( ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ψ ‘ 𝑥 ) ) = ( ( ψ ‘ 𝑥 ) · ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) )
121	119 120	eqtrd	⊢ ( 𝑥 ∈ ℝ+ → ( ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ψ ‘ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) ) = ( ( ψ ‘ 𝑥 ) · ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) )
122		0cn	⊢ 0 ∈ ℂ
123	122	mul01i	⊢ ( 0 · 0 ) = 0
124	123	a1i	⊢ ( 𝑥 ∈ ℝ+ → ( 0 · 0 ) = 0 )
125	121 124	oveq12d	⊢ ( 𝑥 ∈ ℝ+ → ( ( ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ψ ‘ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) ) − ( 0 · 0 ) ) = ( ( ( ψ ‘ 𝑥 ) · ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) − 0 ) )
126	37	subid1d	⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ψ ‘ 𝑥 ) · ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) − 0 ) = ( ( ψ ‘ 𝑥 ) · ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) )
127	125 126	eqtrd	⊢ ( 𝑥 ∈ ℝ+ → ( ( ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ψ ‘ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) ) − ( 0 · 0 ) ) = ( ( ψ ‘ 𝑥 ) · ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) )
128	95	fveq2d	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ψ ‘ ( ( 𝑛 + 1 ) − 1 ) ) = ( ψ ‘ 𝑛 ) )
129	128	oveq2d	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( log ‘ ( 𝑛 + 1 ) ) − ( log ‘ 𝑛 ) ) · ( ψ ‘ ( ( 𝑛 + 1 ) − 1 ) ) ) = ( ( ( log ‘ ( 𝑛 + 1 ) ) − ( log ‘ 𝑛 ) ) · ( ψ ‘ 𝑛 ) ) )
130	82 129	sumeq12rdv	⊢ ( 𝑥 ∈ ℝ+ → Σ 𝑛 ∈ ( 1 ..^ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ( ( ( log ‘ ( 𝑛 + 1 ) ) − ( log ‘ 𝑛 ) ) · ( ψ ‘ ( ( 𝑛 + 1 ) − 1 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( log ‘ ( 𝑛 + 1 ) ) − ( log ‘ 𝑛 ) ) · ( ψ ‘ 𝑛 ) ) )
131	127 130	oveq12d	⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ψ ‘ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) ) − ( 0 · 0 ) ) − Σ 𝑛 ∈ ( 1 ..^ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ( ( ( log ‘ ( 𝑛 + 1 ) ) − ( log ‘ 𝑛 ) ) · ( ψ ‘ ( ( 𝑛 + 1 ) − 1 ) ) ) ) = ( ( ( ψ ‘ 𝑥 ) · ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( log ‘ ( 𝑛 + 1 ) ) − ( log ‘ 𝑛 ) ) · ( ψ ‘ 𝑛 ) ) ) )
132	78 111 131	3eqtr3d	⊢ ( 𝑥 ∈ ℝ+ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) = ( ( ( ψ ‘ 𝑥 ) · ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( log ‘ ( 𝑛 + 1 ) ) − ( log ‘ 𝑛 ) ) · ( ψ ‘ 𝑛 ) ) ) )
133	132	oveq1d	⊢ ( 𝑥 ∈ ℝ+ → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) − ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) = ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( log ‘ ( 𝑛 + 1 ) ) − ( log ‘ 𝑛 ) ) · ( ψ ‘ 𝑛 ) ) ) − ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) )
134	39 41 133	3eqtr4d	⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ψ ‘ 𝑥 ) · ( ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − ( log ‘ 𝑥 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( log ‘ ( 𝑛 + 1 ) ) − ( log ‘ 𝑛 ) ) · ( ψ ‘ 𝑛 ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) − ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) )
135	134	oveq1d	⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ( ψ ‘ 𝑥 ) · ( ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − ( log ‘ 𝑥 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( log ‘ ( 𝑛 + 1 ) ) − ( log ‘ 𝑛 ) ) · ( ψ ‘ 𝑛 ) ) ) / 𝑥 ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) − ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / 𝑥 ) )
136		div23	⊢ ( ( ( ψ ‘ 𝑥 ) ∈ ℂ ∧ ( ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − ( log ‘ 𝑥 ) ) ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ) → ( ( ( ψ ‘ 𝑥 ) · ( ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − ( log ‘ 𝑥 ) ) ) / 𝑥 ) = ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) · ( ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − ( log ‘ 𝑥 ) ) ) )
137	4 15 34 136	syl3anc	⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ψ ‘ 𝑥 ) · ( ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − ( log ‘ 𝑥 ) ) ) / 𝑥 ) = ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) · ( ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − ( log ‘ 𝑥 ) ) ) )
138	137	oveq1d	⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ( ψ ‘ 𝑥 ) · ( ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − ( log ‘ 𝑥 ) ) ) / 𝑥 ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( log ‘ ( 𝑛 + 1 ) ) − ( log ‘ 𝑛 ) ) · ( ψ ‘ 𝑛 ) ) / 𝑥 ) ) = ( ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) · ( ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − ( log ‘ 𝑥 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( log ‘ ( 𝑛 + 1 ) ) − ( log ‘ 𝑛 ) ) · ( ψ ‘ 𝑛 ) ) / 𝑥 ) ) )
139	36 135 138	3eqtr3rd	⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) · ( ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − ( log ‘ 𝑥 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( log ‘ ( 𝑛 + 1 ) ) − ( log ‘ 𝑛 ) ) · ( ψ ‘ 𝑛 ) ) / 𝑥 ) ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) − ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / 𝑥 ) )
140	139	mpteq2ia	⊢ ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) · ( ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − ( log ‘ 𝑥 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( log ‘ ( 𝑛 + 1 ) ) − ( log ‘ 𝑛 ) ) · ( ψ ‘ 𝑛 ) ) / 𝑥 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) − ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / 𝑥 ) )
141		ovexd	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) · ( ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − ( log ‘ 𝑥 ) ) ) ∈ V )
142		ovexd	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( log ‘ ( 𝑛 + 1 ) ) − ( log ‘ 𝑛 ) ) · ( ψ ‘ 𝑛 ) ) / 𝑥 ) ∈ V )
143		reex	⊢ ℝ ∈ V
144		rpssre	⊢ ℝ+ ⊆ ℝ
145	143 144	ssexi	⊢ ℝ+ ∈ V
146	145	a1i	⊢ ( ⊤ → ℝ+ ∈ V )
147		ovexd	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( ψ ‘ 𝑥 ) / 𝑥 ) ∈ V )
148	15	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − ( log ‘ 𝑥 ) ) ∈ ℂ )
149		eqidd	⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) )
150		eqidd	⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − ( log ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − ( log ‘ 𝑥 ) ) ) )
151	146 147 148 149 150	offval2	⊢ ( ⊤ → ( ( 𝑥 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) ∘f · ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − ( log ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) · ( ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − ( log ‘ 𝑥 ) ) ) ) )
152		chpo1ub	⊢ ( 𝑥 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) ∈ 𝑂(1)
153		0red	⊢ ( ⊤ → 0 ∈ ℝ )
154		1red	⊢ ( ⊤ → 1 ∈ ℝ )
155		divrcnv	⊢ ( 1 ∈ ℂ → ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) ) ⇝𝑟 0 )
156	93 155	mp1i	⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) ) ⇝𝑟 0 )
157		rpreccl	⊢ ( 𝑥 ∈ ℝ+ → ( 1 / 𝑥 ) ∈ ℝ+ )
158	157	rpred	⊢ ( 𝑥 ∈ ℝ+ → ( 1 / 𝑥 ) ∈ ℝ )
159	158	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( 1 / 𝑥 ) ∈ ℝ )
160	11 13	resubcld	⊢ ( 𝑥 ∈ ℝ+ → ( ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − ( log ‘ 𝑥 ) ) ∈ ℝ )
161	160	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − ( log ‘ 𝑥 ) ) ∈ ℝ )
162		rpaddcl	⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ∈ ℝ+ ) → ( 𝑥 + 1 ) ∈ ℝ+ )
163	21 162	mpan2	⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 + 1 ) ∈ ℝ+ )
164	163	relogcld	⊢ ( 𝑥 ∈ ℝ+ → ( log ‘ ( 𝑥 + 1 ) ) ∈ ℝ )
165	164 13	resubcld	⊢ ( 𝑥 ∈ ℝ+ → ( ( log ‘ ( 𝑥 + 1 ) ) − ( log ‘ 𝑥 ) ) ∈ ℝ )
166	7	nn0red	⊢ ( 𝑥 ∈ ℝ+ → ( ⌊ ‘ 𝑥 ) ∈ ℝ )
167		1red	⊢ ( 𝑥 ∈ ℝ+ → 1 ∈ ℝ )
168		flle	⊢ ( 𝑥 ∈ ℝ → ( ⌊ ‘ 𝑥 ) ≤ 𝑥 )
169	1 168	syl	⊢ ( 𝑥 ∈ ℝ+ → ( ⌊ ‘ 𝑥 ) ≤ 𝑥 )
170	166 1 167 169	leadd1dd	⊢ ( 𝑥 ∈ ℝ+ → ( ( ⌊ ‘ 𝑥 ) + 1 ) ≤ ( 𝑥 + 1 ) )
171	10 163	logled	⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ≤ ( 𝑥 + 1 ) ↔ ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ≤ ( log ‘ ( 𝑥 + 1 ) ) ) )
172	170 171	mpbid	⊢ ( 𝑥 ∈ ℝ+ → ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ≤ ( log ‘ ( 𝑥 + 1 ) ) )
173	11 164 13 172	lesub1dd	⊢ ( 𝑥 ∈ ℝ+ → ( ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − ( log ‘ 𝑥 ) ) ≤ ( ( log ‘ ( 𝑥 + 1 ) ) − ( log ‘ 𝑥 ) ) )
174		logdifbnd	⊢ ( 𝑥 ∈ ℝ+ → ( ( log ‘ ( 𝑥 + 1 ) ) − ( log ‘ 𝑥 ) ) ≤ ( 1 / 𝑥 ) )
175	160 165 158 173 174	letrd	⊢ ( 𝑥 ∈ ℝ+ → ( ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − ( log ‘ 𝑥 ) ) ≤ ( 1 / 𝑥 ) )
176	175	ad2antrl	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − ( log ‘ 𝑥 ) ) ≤ ( 1 / 𝑥 ) )
177		fllep1	⊢ ( 𝑥 ∈ ℝ → 𝑥 ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) )
178	1 177	syl	⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) )
179		logleb	⊢ ( ( 𝑥 ∈ ℝ+ ∧ ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℝ+ ) → ( 𝑥 ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) ↔ ( log ‘ 𝑥 ) ≤ ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) )
180	10 179	mpdan	⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) ↔ ( log ‘ 𝑥 ) ≤ ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) )
181	178 180	mpbid	⊢ ( 𝑥 ∈ ℝ+ → ( log ‘ 𝑥 ) ≤ ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) )
182	11 13	subge0d	⊢ ( 𝑥 ∈ ℝ+ → ( 0 ≤ ( ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − ( log ‘ 𝑥 ) ) ↔ ( log ‘ 𝑥 ) ≤ ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) )
183	181 182	mpbird	⊢ ( 𝑥 ∈ ℝ+ → 0 ≤ ( ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − ( log ‘ 𝑥 ) ) )
184	183	ad2antrl	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 0 ≤ ( ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − ( log ‘ 𝑥 ) ) )
185	153 154 156 159 161 176 184	rlimsqz2	⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − ( log ‘ 𝑥 ) ) ) ⇝𝑟 0 )
186		rlimo1	⊢ ( ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − ( log ‘ 𝑥 ) ) ) ⇝𝑟 0 → ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) )
187	185 186	syl	⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) )
188		o1mul	⊢ ( ( ( 𝑥 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) ∈ 𝑂(1) ∧ ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) ) → ( ( 𝑥 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) ∘f · ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )
189	152 187 188	sylancr	⊢ ( ⊤ → ( ( 𝑥 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) ∘f · ( 𝑥 ∈ ℝ+ ↦ ( ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )
190	151 189	eqeltrrd	⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) · ( ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )
191		nnrp	⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℝ+ )
192	191	ssriv	⊢ ℕ ⊆ ℝ+
193	192	a1i	⊢ ( ⊤ → ℕ ⊆ ℝ+ )
194	193	sselda	⊢ ( ( ⊤ ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℝ+ )
195	194 31	syl	⊢ ( ( ⊤ ∧ 𝑛 ∈ ℕ ) → ( ( ( log ‘ ( 𝑛 + 1 ) ) − ( log ‘ 𝑛 ) ) · ( ψ ‘ 𝑛 ) ) ∈ ℂ )
196		chpo1ub	⊢ ( 𝑛 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑛 ) / 𝑛 ) ) ∈ 𝑂(1)
197	196	a1i	⊢ ( ⊤ → ( 𝑛 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑛 ) / 𝑛 ) ) ∈ 𝑂(1) )
198		rerpdivcl	⊢ ( ( ( ψ ‘ 𝑛 ) ∈ ℝ ∧ 𝑛 ∈ ℝ+ ) → ( ( ψ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
199	29 198	mpancom	⊢ ( 𝑛 ∈ ℝ+ → ( ( ψ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
200	199	adantl	⊢ ( ( ⊤ ∧ 𝑛 ∈ ℝ+ ) → ( ( ψ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
201	31	adantl	⊢ ( ( ⊤ ∧ 𝑛 ∈ ℝ+ ) → ( ( ( log ‘ ( 𝑛 + 1 ) ) − ( log ‘ 𝑛 ) ) · ( ψ ‘ 𝑛 ) ) ∈ ℂ )
202		rpreccl	⊢ ( 𝑛 ∈ ℝ+ → ( 1 / 𝑛 ) ∈ ℝ+ )
203	202	rpred	⊢ ( 𝑛 ∈ ℝ+ → ( 1 / 𝑛 ) ∈ ℝ )
204		chpge0	⊢ ( 𝑛 ∈ ℝ → 0 ≤ ( ψ ‘ 𝑛 ) )
205	27 204	syl	⊢ ( 𝑛 ∈ ℝ+ → 0 ≤ ( ψ ‘ 𝑛 ) )
206		logdifbnd	⊢ ( 𝑛 ∈ ℝ+ → ( ( log ‘ ( 𝑛 + 1 ) ) − ( log ‘ 𝑛 ) ) ≤ ( 1 / 𝑛 ) )
207	26 203 29 205 206	lemul1ad	⊢ ( 𝑛 ∈ ℝ+ → ( ( ( log ‘ ( 𝑛 + 1 ) ) − ( log ‘ 𝑛 ) ) · ( ψ ‘ 𝑛 ) ) ≤ ( ( 1 / 𝑛 ) · ( ψ ‘ 𝑛 ) ) )
208	27	lep1d	⊢ ( 𝑛 ∈ ℝ+ → 𝑛 ≤ ( 𝑛 + 1 ) )
209		logleb	⊢ ( ( 𝑛 ∈ ℝ+ ∧ ( 𝑛 + 1 ) ∈ ℝ+ ) → ( 𝑛 ≤ ( 𝑛 + 1 ) ↔ ( log ‘ 𝑛 ) ≤ ( log ‘ ( 𝑛 + 1 ) ) ) )
210	23 209	mpdan	⊢ ( 𝑛 ∈ ℝ+ → ( 𝑛 ≤ ( 𝑛 + 1 ) ↔ ( log ‘ 𝑛 ) ≤ ( log ‘ ( 𝑛 + 1 ) ) ) )
211	208 210	mpbid	⊢ ( 𝑛 ∈ ℝ+ → ( log ‘ 𝑛 ) ≤ ( log ‘ ( 𝑛 + 1 ) ) )
212	24 25	subge0d	⊢ ( 𝑛 ∈ ℝ+ → ( 0 ≤ ( ( log ‘ ( 𝑛 + 1 ) ) − ( log ‘ 𝑛 ) ) ↔ ( log ‘ 𝑛 ) ≤ ( log ‘ ( 𝑛 + 1 ) ) ) )
213	211 212	mpbird	⊢ ( 𝑛 ∈ ℝ+ → 0 ≤ ( ( log ‘ ( 𝑛 + 1 ) ) − ( log ‘ 𝑛 ) ) )
214	26 29 213 205	mulge0d	⊢ ( 𝑛 ∈ ℝ+ → 0 ≤ ( ( ( log ‘ ( 𝑛 + 1 ) ) − ( log ‘ 𝑛 ) ) · ( ψ ‘ 𝑛 ) ) )
215	30 214	absidd	⊢ ( 𝑛 ∈ ℝ+ → ( abs ‘ ( ( ( log ‘ ( 𝑛 + 1 ) ) − ( log ‘ 𝑛 ) ) · ( ψ ‘ 𝑛 ) ) ) = ( ( ( log ‘ ( 𝑛 + 1 ) ) − ( log ‘ 𝑛 ) ) · ( ψ ‘ 𝑛 ) ) )
216		rpregt0	⊢ ( 𝑛 ∈ ℝ+ → ( 𝑛 ∈ ℝ ∧ 0 < 𝑛 ) )
217		divge0	⊢ ( ( ( ( ψ ‘ 𝑛 ) ∈ ℝ ∧ 0 ≤ ( ψ ‘ 𝑛 ) ) ∧ ( 𝑛 ∈ ℝ ∧ 0 < 𝑛 ) ) → 0 ≤ ( ( ψ ‘ 𝑛 ) / 𝑛 ) )
218	29 205 216 217	syl21anc	⊢ ( 𝑛 ∈ ℝ+ → 0 ≤ ( ( ψ ‘ 𝑛 ) / 𝑛 ) )
219	199 218	absidd	⊢ ( 𝑛 ∈ ℝ+ → ( abs ‘ ( ( ψ ‘ 𝑛 ) / 𝑛 ) ) = ( ( ψ ‘ 𝑛 ) / 𝑛 ) )
220	29	recnd	⊢ ( 𝑛 ∈ ℝ+ → ( ψ ‘ 𝑛 ) ∈ ℂ )
221		rpcn	⊢ ( 𝑛 ∈ ℝ+ → 𝑛 ∈ ℂ )
222		rpne0	⊢ ( 𝑛 ∈ ℝ+ → 𝑛 ≠ 0 )
223	220 221 222	divrec2d	⊢ ( 𝑛 ∈ ℝ+ → ( ( ψ ‘ 𝑛 ) / 𝑛 ) = ( ( 1 / 𝑛 ) · ( ψ ‘ 𝑛 ) ) )
224	219 223	eqtrd	⊢ ( 𝑛 ∈ ℝ+ → ( abs ‘ ( ( ψ ‘ 𝑛 ) / 𝑛 ) ) = ( ( 1 / 𝑛 ) · ( ψ ‘ 𝑛 ) ) )
225	207 215 224	3brtr4d	⊢ ( 𝑛 ∈ ℝ+ → ( abs ‘ ( ( ( log ‘ ( 𝑛 + 1 ) ) − ( log ‘ 𝑛 ) ) · ( ψ ‘ 𝑛 ) ) ) ≤ ( abs ‘ ( ( ψ ‘ 𝑛 ) / 𝑛 ) ) )
226	225	ad2antrl	⊢ ( ( ⊤ ∧ ( 𝑛 ∈ ℝ+ ∧ 1 ≤ 𝑛 ) ) → ( abs ‘ ( ( ( log ‘ ( 𝑛 + 1 ) ) − ( log ‘ 𝑛 ) ) · ( ψ ‘ 𝑛 ) ) ) ≤ ( abs ‘ ( ( ψ ‘ 𝑛 ) / 𝑛 ) ) )
227	154 197 200 201 226	o1le	⊢ ( ⊤ → ( 𝑛 ∈ ℝ+ ↦ ( ( ( log ‘ ( 𝑛 + 1 ) ) − ( log ‘ 𝑛 ) ) · ( ψ ‘ 𝑛 ) ) ) ∈ 𝑂(1) )
228	193 227	o1res2	⊢ ( ⊤ → ( 𝑛 ∈ ℕ ↦ ( ( ( log ‘ ( 𝑛 + 1 ) ) − ( log ‘ 𝑛 ) ) · ( ψ ‘ 𝑛 ) ) ) ∈ 𝑂(1) )
229	195 228	o1fsum	⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( log ‘ ( 𝑛 + 1 ) ) − ( log ‘ 𝑛 ) ) · ( ψ ‘ 𝑛 ) ) / 𝑥 ) ) ∈ 𝑂(1) )
230	141 142 190 229	o1sub2	⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) · ( ( log ‘ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − ( log ‘ 𝑥 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( log ‘ ( 𝑛 + 1 ) ) − ( log ‘ 𝑛 ) ) · ( ψ ‘ 𝑛 ) ) / 𝑥 ) ) ) ∈ 𝑂(1) )
231	140 230	eqeltrrid	⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) − ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / 𝑥 ) ) ∈ 𝑂(1) )
232	231	mptru	⊢ ( 𝑥 ∈ ℝ+ ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( log ‘ 𝑛 ) ) − ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / 𝑥 ) ) ∈ 𝑂(1)