Theorem selberg2lem 27033

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

Assertion

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

Distinct variable group:   𝑥,𝑛

Proof of Theorem selberg2lem

Dummy variable 𝑚 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		rpre 12978	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ)
2		chpcl 26608	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ → (ψ‘𝑥) ∈ ℝ)
3	1, 2	syl 17	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ+ → (ψ‘𝑥) ∈ ℝ)
4	3	recnd 11238	. . . . . . 7 ⊢ (𝑥 ∈ ℝ+ → (ψ‘𝑥) ∈ ℂ)
5		rprege0 12985	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ+ → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
6		flge0nn0 13781	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → (⌊‘𝑥) ∈ ℕ0)
7	5, 6	syl 17	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ+ → (⌊‘𝑥) ∈ ℕ0)
8		nn0p1nn 12507	. . . . . . . . . . . 12 ⊢ ((⌊‘𝑥) ∈ ℕ0 → ((⌊‘𝑥) + 1) ∈ ℕ)
9	7, 8	syl 17	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ+ → ((⌊‘𝑥) + 1) ∈ ℕ)
10	9	nnrpd 13010	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ+ → ((⌊‘𝑥) + 1) ∈ ℝ+)
11	10	relogcld 26113	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ+ → (log‘((⌊‘𝑥) + 1)) ∈ ℝ)
12	11	recnd 11238	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ+ → (log‘((⌊‘𝑥) + 1)) ∈ ℂ)
13		relogcl 26066	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ+ → (log‘𝑥) ∈ ℝ)
14	13	recnd 11238	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ+ → (log‘𝑥) ∈ ℂ)
15	12, 14	subcld 11567	. . . . . . 7 ⊢ (𝑥 ∈ ℝ+ → ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)) ∈ ℂ)
16	4, 15	mulcld 11230	. . . . . 6 ⊢ (𝑥 ∈ ℝ+ → ((ψ‘𝑥) · ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) ∈ ℂ)
17		fzfid 13934	. . . . . . 7 ⊢ (𝑥 ∈ ℝ+ → (1...(⌊‘𝑥)) ∈ Fin)
18		elfznn 13526	. . . . . . . . . 10 ⊢ (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
19	18	adantl 483	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
20	19	nnrpd 13010	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ+)
21		1rp 12974	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℝ+
22		rpaddcl 12992	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ ℝ+ ∧ 1 ∈ ℝ+) → (𝑛 + 1) ∈ ℝ+)
23	21, 22	mpan2 690	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℝ+ → (𝑛 + 1) ∈ ℝ+)
24	23	relogcld 26113	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℝ+ → (log‘(𝑛 + 1)) ∈ ℝ)
25		relogcl 26066	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℝ+ → (log‘𝑛) ∈ ℝ)
26	24, 25	resubcld 11638	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℝ+ → ((log‘(𝑛 + 1)) − (log‘𝑛)) ∈ ℝ)
27		rpre 12978	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℝ+ → 𝑛 ∈ ℝ)
28		chpcl 26608	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℝ → (ψ‘𝑛) ∈ ℝ)
29	27, 28	syl 17	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℝ+ → (ψ‘𝑛) ∈ ℝ)
30	26, 29	remulcld 11240	. . . . . . . . 9 ⊢ (𝑛 ∈ ℝ+ → (((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) ∈ ℝ)
31	30	recnd 11238	. . . . . . . 8 ⊢ (𝑛 ∈ ℝ+ → (((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) ∈ ℂ)
32	20, 31	syl 17	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) ∈ ℂ)
33	17, 32	fsumcl 15675	. . . . . 6 ⊢ (𝑥 ∈ ℝ+ → Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) ∈ ℂ)
34		rpcnne0 12988	. . . . . 6 ⊢ (𝑥 ∈ ℝ+ → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
35		divsubdir 11904	. . . . . 6 ⊢ ((((ψ‘𝑥) · ((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 1372	. . . . 5 ⊢ (𝑥 ∈ ℝ+ → ((((ψ‘𝑥) · ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) / 𝑥) = ((((ψ‘𝑥) · ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) / 𝑥) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) / 𝑥)))
37	4, 12	mulcld 11230	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ+ → ((ψ‘𝑥) · (log‘((⌊‘𝑥) + 1))) ∈ ℂ)
38	4, 14	mulcld 11230	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ+ → ((ψ‘𝑥) · (log‘𝑥)) ∈ ℂ)
39	37, 38, 33	sub32d 11599	. . . . . . 7 ⊢ (𝑥 ∈ ℝ+ → ((((ψ‘𝑥) · (log‘((⌊‘𝑥) + 1))) − ((ψ‘𝑥) · (log‘𝑥))) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) = ((((ψ‘𝑥) · (log‘((⌊‘𝑥) + 1))) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) − ((ψ‘𝑥) · (log‘𝑥))))
40	4, 12, 14	subdid 11666	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ+ → ((ψ‘𝑥) · ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) = (((ψ‘𝑥) · (log‘((⌊‘𝑥) + 1))) − ((ψ‘𝑥) · (log‘𝑥))))
41	40	oveq1d 7419	. . . . . . 7 ⊢ (𝑥 ∈ ℝ+ → (((ψ‘𝑥) · ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) = ((((ψ‘𝑥) · (log‘((⌊‘𝑥) + 1))) − ((ψ‘𝑥) · (log‘𝑥))) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))))
42		fveq2 6888	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → (log‘𝑚) = (log‘𝑛))
43		fvoveq1 7427	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → (ψ‘(𝑚 − 1)) = (ψ‘(𝑛 − 1)))
44	42, 43	jca 513	. . . . . . . . . 10 ⊢ (𝑚 = 𝑛 → ((log‘𝑚) = (log‘𝑛) ∧ (ψ‘(𝑚 − 1)) = (ψ‘(𝑛 − 1))))
45		fveq2 6888	. . . . . . . . . . 11 ⊢ (𝑚 = (𝑛 + 1) → (log‘𝑚) = (log‘(𝑛 + 1)))
46		fvoveq1 7427	. . . . . . . . . . 11 ⊢ (𝑚 = (𝑛 + 1) → (ψ‘(𝑚 − 1)) = (ψ‘((𝑛 + 1) − 1)))
47	45, 46	jca 513	. . . . . . . . . 10 ⊢ (𝑚 = (𝑛 + 1) → ((log‘𝑚) = (log‘(𝑛 + 1)) ∧ (ψ‘(𝑚 − 1)) = (ψ‘((𝑛 + 1) − 1))))
48		fveq2 6888	. . . . . . . . . . . 12 ⊢ (𝑚 = 1 → (log‘𝑚) = (log‘1))
49		log1 26076	. . . . . . . . . . . 12 ⊢ (log‘1) = 0
50	48, 49	eqtrdi 2789	. . . . . . . . . . 11 ⊢ (𝑚 = 1 → (log‘𝑚) = 0)
51		oveq1 7411	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 1 → (𝑚 − 1) = (1 − 1))
52		1m1e0 12280	. . . . . . . . . . . . . 14 ⊢ (1 − 1) = 0
53	51, 52	eqtrdi 2789	. . . . . . . . . . . . 13 ⊢ (𝑚 = 1 → (𝑚 − 1) = 0)
54	53	fveq2d 6892	. . . . . . . . . . . 12 ⊢ (𝑚 = 1 → (ψ‘(𝑚 − 1)) = (ψ‘0))
55		2pos 12311	. . . . . . . . . . . . 13 ⊢ 0 < 2
56		0re 11212	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℝ
57		chpeq0 26691	. . . . . . . . . . . . . 14 ⊢ (0 ∈ ℝ → ((ψ‘0) = 0 ↔ 0 < 2))
58	56, 57	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ((ψ‘0) = 0 ↔ 0 < 2)
59	55, 58	mpbir 230	. . . . . . . . . . . 12 ⊢ (ψ‘0) = 0
60	54, 59	eqtrdi 2789	. . . . . . . . . . 11 ⊢ (𝑚 = 1 → (ψ‘(𝑚 − 1)) = 0)
61	50, 60	jca 513	. . . . . . . . . 10 ⊢ (𝑚 = 1 → ((log‘𝑚) = 0 ∧ (ψ‘(𝑚 − 1)) = 0))
62		fveq2 6888	. . . . . . . . . . 11 ⊢ (𝑚 = ((⌊‘𝑥) + 1) → (log‘𝑚) = (log‘((⌊‘𝑥) + 1)))
63		fvoveq1 7427	. . . . . . . . . . 11 ⊢ (𝑚 = ((⌊‘𝑥) + 1) → (ψ‘(𝑚 − 1)) = (ψ‘(((⌊‘𝑥) + 1) − 1)))
64	62, 63	jca 513	. . . . . . . . . 10 ⊢ (𝑚 = ((⌊‘𝑥) + 1) → ((log‘𝑚) = (log‘((⌊‘𝑥) + 1)) ∧ (ψ‘(𝑚 − 1)) = (ψ‘(((⌊‘𝑥) + 1) − 1))))
65		nnuz 12861	. . . . . . . . . . 11 ⊢ ℕ = (ℤ≥‘1)
66	9, 65	eleqtrdi 2844	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ+ → ((⌊‘𝑥) + 1) ∈ (ℤ≥‘1))
67		elfznn 13526	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ (1...((⌊‘𝑥) + 1)) → 𝑚 ∈ ℕ)
68	67	adantl 483	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 𝑚 ∈ ℕ)
69	68	nnrpd 13010	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 𝑚 ∈ ℝ+)
70	69	relogcld 26113	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (log‘𝑚) ∈ ℝ)
71	70	recnd 11238	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (log‘𝑚) ∈ ℂ)
72	68	nnred 12223	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 𝑚 ∈ ℝ)
73		peano2rem 11523	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ℝ → (𝑚 − 1) ∈ ℝ)
74	72, 73	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑚 − 1) ∈ ℝ)
75		chpcl 26608	. . . . . . . . . . . 12 ⊢ ((𝑚 − 1) ∈ ℝ → (ψ‘(𝑚 − 1)) ∈ ℝ)
76	74, 75	syl 17	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (ψ‘(𝑚 − 1)) ∈ ℝ)
77	76	recnd 11238	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (ψ‘(𝑚 − 1)) ∈ ℂ)
78	44, 47, 61, 64, 66, 71, 77	fsumparts 15748	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ+ → Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))((log‘𝑛) · ((ψ‘((𝑛 + 1) − 1)) − (ψ‘(𝑛 − 1)))) = ((((log‘((⌊‘𝑥) + 1)) · (ψ‘(((⌊‘𝑥) + 1) − 1))) − (0 · 0)) − Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘((𝑛 + 1) − 1)))))
79	7	nn0zd 12580	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ+ → (⌊‘𝑥) ∈ ℤ)
80		fzval3 13697	. . . . . . . . . . . 12 ⊢ ((⌊‘𝑥) ∈ ℤ → (1...(⌊‘𝑥)) = (1..^((⌊‘𝑥) + 1)))
81	79, 80	syl 17	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ+ → (1...(⌊‘𝑥)) = (1..^((⌊‘𝑥) + 1)))
82	81	eqcomd 2739	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ+ → (1..^((⌊‘𝑥) + 1)) = (1...(⌊‘𝑥)))
83		nnm1nn0 12509	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ → (𝑛 − 1) ∈ ℕ0)
84	19, 83	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 − 1) ∈ ℕ0)
85	84	nn0red 12529	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 − 1) ∈ ℝ)
86		chpcl 26608	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 − 1) ∈ ℝ → (ψ‘(𝑛 − 1)) ∈ ℝ)
87	85, 86	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (ψ‘(𝑛 − 1)) ∈ ℝ)
88	87	recnd 11238	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (ψ‘(𝑛 − 1)) ∈ ℂ)
89		vmacl 26602	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → (Λ‘𝑛) ∈ ℝ)
90	19, 89	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈ ℝ)
91	90	recnd 11238	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈ ℂ)
92	19	nncnd 12224	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℂ)
93		ax-1cn 11164	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℂ
94		pncan 11462	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛 + 1) − 1) = 𝑛)
95	92, 93, 94	sylancl 587	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) − 1) = 𝑛)
96		npcan 11465	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛 − 1) + 1) = 𝑛)
97	92, 93, 96	sylancl 587	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 − 1) + 1) = 𝑛)
98	95, 97	eqtr4d 2776	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) − 1) = ((𝑛 − 1) + 1))
99	98	fveq2d 6892	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (ψ‘((𝑛 + 1) − 1)) = (ψ‘((𝑛 − 1) + 1)))
100		chpp1 26639	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 − 1) ∈ ℕ0 → (ψ‘((𝑛 − 1) + 1)) = ((ψ‘(𝑛 − 1)) + (Λ‘((𝑛 − 1) + 1))))
101	84, 100	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (ψ‘((𝑛 − 1) + 1)) = ((ψ‘(𝑛 − 1)) + (Λ‘((𝑛 − 1) + 1))))
102	97	fveq2d 6892	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘((𝑛 − 1) + 1)) = (Λ‘𝑛))
103	102	oveq2d 7420	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((ψ‘(𝑛 − 1)) + (Λ‘((𝑛 − 1) + 1))) = ((ψ‘(𝑛 − 1)) + (Λ‘𝑛)))
104	99, 101, 103	3eqtrd 2777	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (ψ‘((𝑛 + 1) − 1)) = ((ψ‘(𝑛 − 1)) + (Λ‘𝑛)))
105	88, 91, 104	mvrladdd 11623	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((ψ‘((𝑛 + 1) − 1)) − (ψ‘(𝑛 − 1))) = (Λ‘𝑛))
106	105	oveq2d 7420	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘𝑛) · ((ψ‘((𝑛 + 1) − 1)) − (ψ‘(𝑛 − 1)))) = ((log‘𝑛) · (Λ‘𝑛)))
107	20	relogcld 26113	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘𝑛) ∈ ℝ)
108	107	recnd 11238	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘𝑛) ∈ ℂ)
109	91, 108	mulcomd 11231	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · (log‘𝑛)) = ((log‘𝑛) · (Λ‘𝑛)))
110	106, 109	eqtr4d 2776	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘𝑛) · ((ψ‘((𝑛 + 1) − 1)) − (ψ‘(𝑛 − 1)))) = ((Λ‘𝑛) · (log‘𝑛)))
111	82, 110	sumeq12rdv 15649	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ+ → Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))((log‘𝑛) · ((ψ‘((𝑛 + 1) − 1)) − (ψ‘(𝑛 − 1)))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (log‘𝑛)))
112	7	nn0cnd 12530	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℝ+ → (⌊‘𝑥) ∈ ℂ)
113		pncan 11462	. . . . . . . . . . . . . . . . 17 ⊢ (((⌊‘𝑥) ∈ ℂ ∧ 1 ∈ ℂ) → (((⌊‘𝑥) + 1) − 1) = (⌊‘𝑥))
114	112, 93, 113	sylancl 587	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℝ+ → (((⌊‘𝑥) + 1) − 1) = (⌊‘𝑥))
115	114	fveq2d 6892	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ+ → (ψ‘(((⌊‘𝑥) + 1) − 1)) = (ψ‘(⌊‘𝑥)))
116		chpfl 26634	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℝ → (ψ‘(⌊‘𝑥)) = (ψ‘𝑥))
117	1, 116	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ+ → (ψ‘(⌊‘𝑥)) = (ψ‘𝑥))
118	115, 117	eqtrd 2773	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ+ → (ψ‘(((⌊‘𝑥) + 1) − 1)) = (ψ‘𝑥))
119	118	oveq2d 7420	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ+ → ((log‘((⌊‘𝑥) + 1)) · (ψ‘(((⌊‘𝑥) + 1) − 1))) = ((log‘((⌊‘𝑥) + 1)) · (ψ‘𝑥)))
120	12, 4	mulcomd 11231	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ+ → ((log‘((⌊‘𝑥) + 1)) · (ψ‘𝑥)) = ((ψ‘𝑥) · (log‘((⌊‘𝑥) + 1))))
121	119, 120	eqtrd 2773	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ+ → ((log‘((⌊‘𝑥) + 1)) · (ψ‘(((⌊‘𝑥) + 1) − 1))) = ((ψ‘𝑥) · (log‘((⌊‘𝑥) + 1))))
122		0cn 11202	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℂ
123	122	mul01i 11400	. . . . . . . . . . . . 13 ⊢ (0 · 0) = 0
124	123	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ+ → (0 · 0) = 0)
125	121, 124	oveq12d 7422	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ+ → (((log‘((⌊‘𝑥) + 1)) · (ψ‘(((⌊‘𝑥) + 1) − 1))) − (0 · 0)) = (((ψ‘𝑥) · (log‘((⌊‘𝑥) + 1))) − 0))
126	37	subid1d 11556	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ+ → (((ψ‘𝑥) · (log‘((⌊‘𝑥) + 1))) − 0) = ((ψ‘𝑥) · (log‘((⌊‘𝑥) + 1))))
127	125, 126	eqtrd 2773	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ+ → (((log‘((⌊‘𝑥) + 1)) · (ψ‘(((⌊‘𝑥) + 1) − 1))) − (0 · 0)) = ((ψ‘𝑥) · (log‘((⌊‘𝑥) + 1))))
128	95	fveq2d 6892	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (ψ‘((𝑛 + 1) − 1)) = (ψ‘𝑛))
129	128	oveq2d 7420	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ+ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘((𝑛 + 1) − 1))) = (((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)))
130	82, 129	sumeq12rdv 15649	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ+ → Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘((𝑛 + 1) − 1))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)))
131	127, 130	oveq12d 7422	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ+ → ((((log‘((⌊‘𝑥) + 1)) · (ψ‘(((⌊‘𝑥) + 1) − 1))) − (0 · 0)) − Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘((𝑛 + 1) − 1)))) = (((ψ‘𝑥) · (log‘((⌊‘𝑥) + 1))) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))))
132	78, 111, 131	3eqtr3d 2781	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ+ → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (log‘𝑛)) = (((ψ‘𝑥) · (log‘((⌊‘𝑥) + 1))) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))))
133	132	oveq1d 7419	. . . . . . 7 ⊢ (𝑥 ∈ ℝ+ → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (log‘𝑛)) − ((ψ‘𝑥) · (log‘𝑥))) = ((((ψ‘𝑥) · (log‘((⌊‘𝑥) + 1))) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) − ((ψ‘𝑥) · (log‘𝑥))))
134	39, 41, 133	3eqtr4d 2783	. . . . . 6 ⊢ (𝑥 ∈ ℝ+ → (((ψ‘𝑥) · ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (log‘𝑛)) − ((ψ‘𝑥) · (log‘𝑥))))
135	134	oveq1d 7419	. . . . 5 ⊢ (𝑥 ∈ ℝ+ → ((((ψ‘𝑥) · ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (log‘𝑛)) − ((ψ‘𝑥) · (log‘𝑥))) / 𝑥))
136		div23 11887	. . . . . . 7 ⊢ (((ψ‘𝑥) ∈ ℂ ∧ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → (((ψ‘𝑥) · ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) / 𝑥) = (((ψ‘𝑥) / 𝑥) · ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))))
137	4, 15, 34, 136	syl3anc 1372	. . . . . 6 ⊢ (𝑥 ∈ ℝ+ → (((ψ‘𝑥) · ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) / 𝑥) = (((ψ‘𝑥) / 𝑥) · ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))))
138	137	oveq1d 7419	. . . . 5 ⊢ (𝑥 ∈ ℝ+ → ((((ψ‘𝑥) · ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) / 𝑥) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) / 𝑥)) = ((((ψ‘𝑥) / 𝑥) · ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) / 𝑥)))
139	36, 135, 138	3eqtr3rd 2782	. . . 4 ⊢ (𝑥 ∈ ℝ+ → ((((ψ‘𝑥) / 𝑥) · ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) / 𝑥)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (log‘𝑛)) − ((ψ‘𝑥) · (log‘𝑥))) / 𝑥))
140	139	mpteq2ia 5250	. . 3 ⊢ (𝑥 ∈ ℝ+ ↦ ((((ψ‘𝑥) / 𝑥) · ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) / 𝑥))) = (𝑥 ∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (log‘𝑛)) − ((ψ‘𝑥) · (log‘𝑥))) / 𝑥))
141		ovexd 7439	. . . 4 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) / 𝑥) · ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) ∈ V)
142		ovexd 7439	. . . 4 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) / 𝑥) ∈ V)
143		reex 11197	. . . . . . . 8 ⊢ ℝ ∈ V
144		rpssre 12977	. . . . . . . 8 ⊢ ℝ+ ⊆ ℝ
145	143, 144	ssexi 5321	. . . . . . 7 ⊢ ℝ+ ∈ V
146	145	a1i 11	. . . . . 6 ⊢ (⊤ → ℝ+ ∈ V)
147		ovexd 7439	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ+) → ((ψ‘𝑥) / 𝑥) ∈ V)
148	15	adantl 483	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ+) → ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)) ∈ ℂ)
149		eqidd 2734	. . . . . 6 ⊢ (⊤ → (𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) = (𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)))
150		eqidd 2734	. . . . . 6 ⊢ (⊤ → (𝑥 ∈ ℝ+ ↦ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) = (𝑥 ∈ ℝ+ ↦ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))))
151	146, 147, 148, 149, 150	offval2 7685	. . . . 5 ⊢ (⊤ → ((𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∘f · (𝑥 ∈ ℝ+ ↦ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)))) = (𝑥 ∈ ℝ+ ↦ (((ψ‘𝑥) / 𝑥) · ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)))))
152		chpo1ub 26963	. . . . . 6 ⊢ (𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∈ 𝑂(1)
153		0red 11213	. . . . . . . 8 ⊢ (⊤ → 0 ∈ ℝ)
154		1red 11211	. . . . . . . 8 ⊢ (⊤ → 1 ∈ ℝ)
155		divrcnv 15794	. . . . . . . . 9 ⊢ (1 ∈ ℂ → (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) ⇝𝑟 0)
156	93, 155	mp1i 13	. . . . . . . 8 ⊢ (⊤ → (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) ⇝𝑟 0)
157		rpreccl 12996	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ+ → (1 / 𝑥) ∈ ℝ+)
158	157	rpred 13012	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ+ → (1 / 𝑥) ∈ ℝ)
159	158	adantl 483	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ+) → (1 / 𝑥) ∈ ℝ)
160	11, 13	resubcld 11638	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ+ → ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)) ∈ ℝ)
161	160	adantl 483	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ+) → ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)) ∈ ℝ)
162		rpaddcl 12992	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℝ+ ∧ 1 ∈ ℝ+) → (𝑥 + 1) ∈ ℝ+)
163	21, 162	mpan2 690	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ+ → (𝑥 + 1) ∈ ℝ+)
164	163	relogcld 26113	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ+ → (log‘(𝑥 + 1)) ∈ ℝ)
165	164, 13	resubcld 11638	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ+ → ((log‘(𝑥 + 1)) − (log‘𝑥)) ∈ ℝ)
166	7	nn0red 12529	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ+ → (⌊‘𝑥) ∈ ℝ)
167		1red 11211	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ+ → 1 ∈ ℝ)
168		flle 13760	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → (⌊‘𝑥) ≤ 𝑥)
169	1, 168	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ+ → (⌊‘𝑥) ≤ 𝑥)
170	166, 1, 167, 169	leadd1dd 11824	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ+ → ((⌊‘𝑥) + 1) ≤ (𝑥 + 1))
171	10, 163	logled 26117	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ+ → (((⌊‘𝑥) + 1) ≤ (𝑥 + 1) ↔ (log‘((⌊‘𝑥) + 1)) ≤ (log‘(𝑥 + 1))))
172	170, 171	mpbid 231	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ+ → (log‘((⌊‘𝑥) + 1)) ≤ (log‘(𝑥 + 1)))
173	11, 164, 13, 172	lesub1dd 11826	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ+ → ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)) ≤ ((log‘(𝑥 + 1)) − (log‘𝑥)))
174		logdifbnd 26478	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ+ → ((log‘(𝑥 + 1)) − (log‘𝑥)) ≤ (1 / 𝑥))
175	160, 165, 158, 173, 174	letrd 11367	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ+ → ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)) ≤ (1 / 𝑥))
176	175	ad2antrl 727	. . . . . . . 8 ⊢ ((⊤ ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)) ≤ (1 / 𝑥))
177		fllep1 13762	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → 𝑥 ≤ ((⌊‘𝑥) + 1))
178	1, 177	syl 17	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ+ → 𝑥 ≤ ((⌊‘𝑥) + 1))
179		logleb 26093	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ+ ∧ ((⌊‘𝑥) + 1) ∈ ℝ+) → (𝑥 ≤ ((⌊‘𝑥) + 1) ↔ (log‘𝑥) ≤ (log‘((⌊‘𝑥) + 1))))
180	10, 179	mpdan 686	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ+ → (𝑥 ≤ ((⌊‘𝑥) + 1) ↔ (log‘𝑥) ≤ (log‘((⌊‘𝑥) + 1))))
181	178, 180	mpbid 231	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ+ → (log‘𝑥) ≤ (log‘((⌊‘𝑥) + 1)))
182	11, 13	subge0d 11800	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ+ → (0 ≤ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)) ↔ (log‘𝑥) ≤ (log‘((⌊‘𝑥) + 1))))
183	181, 182	mpbird 257	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ+ → 0 ≤ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)))
184	183	ad2antrl 727	. . . . . . . 8 ⊢ ((⊤ ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 0 ≤ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)))
185	153, 154, 156, 159, 161, 176, 184	rlimsqz2 15593	. . . . . . 7 ⊢ (⊤ → (𝑥 ∈ ℝ+ ↦ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) ⇝𝑟 0)
186		rlimo1 15557	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ+ ↦ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) ⇝𝑟 0 → (𝑥 ∈ ℝ+ ↦ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) ∈ 𝑂(1))
187	185, 186	syl 17	. . . . . 6 ⊢ (⊤ → (𝑥 ∈ ℝ+ ↦ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) ∈ 𝑂(1))
188		o1mul 15555	. . . . . 6 ⊢ (((𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∈ 𝑂(1) ∧ (𝑥 ∈ ℝ+ ↦ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) ∈ 𝑂(1)) → ((𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∘f · (𝑥 ∈ ℝ+ ↦ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)))) ∈ 𝑂(1))
189	152, 187, 188	sylancr 588	. . . . 5 ⊢ (⊤ → ((𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∘f · (𝑥 ∈ ℝ+ ↦ ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)))) ∈ 𝑂(1))
190	151, 189	eqeltrrd 2835	. . . 4 ⊢ (⊤ → (𝑥 ∈ ℝ+ ↦ (((ψ‘𝑥) / 𝑥) · ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥)))) ∈ 𝑂(1))
191		nnrp 12981	. . . . . . . . 9 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℝ+)
192	191	ssriv 3985	. . . . . . . 8 ⊢ ℕ ⊆ ℝ+
193	192	a1i 11	. . . . . . 7 ⊢ (⊤ → ℕ ⊆ ℝ+)
194	193	sselda 3981	. . . . . 6 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℝ+)
195	194, 31	syl 17	. . . . 5 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → (((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) ∈ ℂ)
196		chpo1ub 26963	. . . . . . . 8 ⊢ (𝑛 ∈ ℝ+ ↦ ((ψ‘𝑛) / 𝑛)) ∈ 𝑂(1)
197	196	a1i 11	. . . . . . 7 ⊢ (⊤ → (𝑛 ∈ ℝ+ ↦ ((ψ‘𝑛) / 𝑛)) ∈ 𝑂(1))
198		rerpdivcl 13000	. . . . . . . . 9 ⊢ (((ψ‘𝑛) ∈ ℝ ∧ 𝑛 ∈ ℝ+) → ((ψ‘𝑛) / 𝑛) ∈ ℝ)
199	29, 198	mpancom 687	. . . . . . . 8 ⊢ (𝑛 ∈ ℝ+ → ((ψ‘𝑛) / 𝑛) ∈ ℝ)
200	199	adantl 483	. . . . . . 7 ⊢ ((⊤ ∧ 𝑛 ∈ ℝ+) → ((ψ‘𝑛) / 𝑛) ∈ ℝ)
201	31	adantl 483	. . . . . . 7 ⊢ ((⊤ ∧ 𝑛 ∈ ℝ+) → (((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) ∈ ℂ)
202		rpreccl 12996	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℝ+ → (1 / 𝑛) ∈ ℝ+)
203	202	rpred 13012	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℝ+ → (1 / 𝑛) ∈ ℝ)
204		chpge0 26610	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℝ → 0 ≤ (ψ‘𝑛))
205	27, 204	syl 17	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℝ+ → 0 ≤ (ψ‘𝑛))
206		logdifbnd 26478	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℝ+ → ((log‘(𝑛 + 1)) − (log‘𝑛)) ≤ (1 / 𝑛))
207	26, 203, 29, 205, 206	lemul1ad 12149	. . . . . . . . 9 ⊢ (𝑛 ∈ ℝ+ → (((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) ≤ ((1 / 𝑛) · (ψ‘𝑛)))
208	27	lep1d 12141	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℝ+ → 𝑛 ≤ (𝑛 + 1))
209		logleb 26093	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ ℝ+ ∧ (𝑛 + 1) ∈ ℝ+) → (𝑛 ≤ (𝑛 + 1) ↔ (log‘𝑛) ≤ (log‘(𝑛 + 1))))
210	23, 209	mpdan 686	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℝ+ → (𝑛 ≤ (𝑛 + 1) ↔ (log‘𝑛) ≤ (log‘(𝑛 + 1))))
211	208, 210	mpbid 231	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℝ+ → (log‘𝑛) ≤ (log‘(𝑛 + 1)))
212	24, 25	subge0d 11800	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℝ+ → (0 ≤ ((log‘(𝑛 + 1)) − (log‘𝑛)) ↔ (log‘𝑛) ≤ (log‘(𝑛 + 1))))
213	211, 212	mpbird 257	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℝ+ → 0 ≤ ((log‘(𝑛 + 1)) − (log‘𝑛)))
214	26, 29, 213, 205	mulge0d 11787	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℝ+ → 0 ≤ (((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)))
215	30, 214	absidd 15365	. . . . . . . . 9 ⊢ (𝑛 ∈ ℝ+ → (abs‘(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) = (((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)))
216		rpregt0 12984	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℝ+ → (𝑛 ∈ ℝ ∧ 0 < 𝑛))
217		divge0 12079	. . . . . . . . . . . 12 ⊢ ((((ψ‘𝑛) ∈ ℝ ∧ 0 ≤ (ψ‘𝑛)) ∧ (𝑛 ∈ ℝ ∧ 0 < 𝑛)) → 0 ≤ ((ψ‘𝑛) / 𝑛))
218	29, 205, 216, 217	syl21anc 837	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℝ+ → 0 ≤ ((ψ‘𝑛) / 𝑛))
219	199, 218	absidd 15365	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℝ+ → (abs‘((ψ‘𝑛) / 𝑛)) = ((ψ‘𝑛) / 𝑛))
220	29	recnd 11238	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℝ+ → (ψ‘𝑛) ∈ ℂ)
221		rpcn 12980	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℝ+ → 𝑛 ∈ ℂ)
222		rpne0 12986	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℝ+ → 𝑛 ≠ 0)
223	220, 221, 222	divrec2d 11990	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℝ+ → ((ψ‘𝑛) / 𝑛) = ((1 / 𝑛) · (ψ‘𝑛)))
224	219, 223	eqtrd 2773	. . . . . . . . 9 ⊢ (𝑛 ∈ ℝ+ → (abs‘((ψ‘𝑛) / 𝑛)) = ((1 / 𝑛) · (ψ‘𝑛)))
225	207, 215, 224	3brtr4d 5179	. . . . . . . 8 ⊢ (𝑛 ∈ ℝ+ → (abs‘(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) ≤ (abs‘((ψ‘𝑛) / 𝑛)))
226	225	ad2antrl 727	. . . . . . 7 ⊢ ((⊤ ∧ (𝑛 ∈ ℝ+ ∧ 1 ≤ 𝑛)) → (abs‘(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) ≤ (abs‘((ψ‘𝑛) / 𝑛)))
227	154, 197, 200, 201, 226	o1le 15595	. . . . . 6 ⊢ (⊤ → (𝑛 ∈ ℝ+ ↦ (((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) ∈ 𝑂(1))
228	193, 227	o1res2 15503	. . . . 5 ⊢ (⊤ → (𝑛 ∈ ℕ ↦ (((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛))) ∈ 𝑂(1))
229	195, 228	o1fsum 15755	. . . 4 ⊢ (⊤ → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) / 𝑥)) ∈ 𝑂(1))
230	141, 142, 190, 229	o1sub2 15566	. . 3 ⊢ (⊤ → (𝑥 ∈ ℝ+ ↦ ((((ψ‘𝑥) / 𝑥) · ((log‘((⌊‘𝑥) + 1)) − (log‘𝑥))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑛 + 1)) − (log‘𝑛)) · (ψ‘𝑛)) / 𝑥))) ∈ 𝑂(1))
231	140, 230	eqeltrrid 2839	. 2 ⊢ (⊤ → (𝑥 ∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (log‘𝑛)) − ((ψ‘𝑥) · (log‘𝑥))) / 𝑥)) ∈ 𝑂(1))
232	231	mptru 1549	1 ⊢ (𝑥 ∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (log‘𝑛)) − ((ψ‘𝑥) · (log‘𝑥))) / 𝑥)) ∈ 𝑂(1)

Syntax hints:   ↔ wb 205   ∧ wa 397   = wceq 1542  ⊤wtru 1543   ∈ wcel 2107   ≠ wne 2941  Vcvv 3475   ⊆ wss 3947   class class class wbr 5147   ↦ cmpt 5230  ‘cfv 6540  (class class class)co 7404   ∘_f cof 7663  ℂcc 11104  ℝcr 11105  0cc0 11106  1c1 11107   + caddc 11109   · cmul 11111   < clt 11244   ≤ cle 11245   − cmin 11440   / cdiv 11867  ℕcn 12208  2c2 12263  ℕ₀cn0 12468  ℤcz 12554  ℤ_≥cuz 12818  ℝ⁺crp 12970  ...cfz 13480  ..^cfzo 13623  ⌊cfl 13751  abscabs 15177   ⇝_𝑟 crli 15425  𝑂(1)co1 15426  Σcsu 15628  logclog 26045  Λcvma 26576  ψcchp 26577

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7720  ax-inf2 9632  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184  ax-addf 11185  ax-mulf 11186

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-tp 4632  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-iin 4999  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549  df-riota 7360  df-ov 7407  df-oprab 7408  df-mpo 7409  df-of 7665  df-om 7851  df-1st 7970  df-2nd 7971  df-supp 8142  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-2o 8462  df-oadd 8465  df-er 8699  df-map 8818  df-pm 8819  df-ixp 8888  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-fsupp 9358  df-fi 9402  df-sup 9433  df-inf 9434  df-oi 9501  df-dju 9892  df-card 9930  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-div 11868  df-nn 12209  df-2 12271  df-3 12272  df-4 12273  df-5 12274  df-6 12275  df-7 12276  df-8 12277  df-9 12278  df-n0 12469  df-xnn0 12541  df-z 12555  df-dec 12674  df-uz 12819  df-q 12929  df-rp 12971  df-xneg 13088  df-xadd 13089  df-xmul 13090  df-ioo 13324  df-ioc 13325  df-ico 13326  df-icc 13327  df-fz 13481  df-fzo 13624  df-fl 13753  df-mod 13831  df-seq 13963  df-exp 14024  df-fac 14230  df-bc 14259  df-hash 14287  df-shft 15010  df-cj 15042  df-re 15043  df-im 15044  df-sqrt 15178  df-abs 15179  df-limsup 15411  df-clim 15428  df-rlim 15429  df-o1 15430  df-lo1 15431  df-sum 15629  df-ef 16007  df-e 16008  df-sin 16009  df-cos 16010  df-pi 16012  df-dvds 16194  df-gcd 16432  df-prm 16605  df-pc 16766  df-struct 17076  df-sets 17093  df-slot 17111  df-ndx 17123  df-base 17141  df-ress 17170  df-plusg 17206  df-mulr 17207  df-starv 17208  df-sca 17209  df-vsca 17210  df-ip 17211  df-tset 17212  df-ple 17213  df-ds 17215  df-unif 17216  df-hom 17217  df-cco 17218  df-rest 17364  df-topn 17365  df-0g 17383  df-gsum 17384  df-topgen 17385  df-pt 17386  df-prds 17389  df-xrs 17444  df-qtop 17449  df-imas 17450  df-xps 17452  df-mre 17526  df-mrc 17527  df-acs 17529  df-mgm 18557  df-sgrp 18606  df-mnd 18622  df-submnd 18668  df-mulg 18945  df-cntz 19175  df-cmn 19643  df-psmet 20921  df-xmet 20922  df-met 20923  df-bl 20924  df-mopn 20925  df-fbas 20926  df-fg 20927  df-cnfld 20930  df-top 22378  df-topon 22395  df-topsp 22417  df-bases 22431  df-cld 22505  df-ntr 22506  df-cls 22507  df-nei 22584  df-lp 22622  df-perf 22623  df-cn 22713  df-cnp 22714  df-haus 22801  df-tx 23048  df-hmeo 23241  df-fil 23332  df-fm 23424  df-flim 23425  df-flf 23426  df-xms 23808  df-ms 23809  df-tms 23810  df-cncf 24376  df-limc 25365  df-dv 25366  df-log 26047  df-cxp 26048  df-cht 26581  df-vma 26582  df-chp 26583  df-ppi 26584

This theorem is referenced by:  selberg2  27034  selberg3lem2  27041