Theorem selberg3lem2 27519

Description: Lemma for selberg3 27520. Equation 10.4.21 of [Shapiro], p. 422. (Contributed by Mario Carneiro, 30-May-2016.)

Assertion

Ref	Expression
selberg3lem2	⊢ (𝑥 ∈ (1(,)+∞) ↦ ((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥)) ∈ 𝑂(1)

Distinct variable group:   𝑥,𝑛

Proof of Theorem selberg3lem2

Dummy variables 𝑚 𝑐 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		1re 11233	. . . . . . . 8 ⊢ 1 ∈ ℝ
2		elicopnf 13460	. . . . . . . 8 ⊢ (1 ∈ ℝ → (𝑦 ∈ (1[,)+∞) ↔ (𝑦 ∈ ℝ ∧ 1 ≤ 𝑦)))
3	1, 2	ax-mp 5	. . . . . . 7 ⊢ (𝑦 ∈ (1[,)+∞) ↔ (𝑦 ∈ ℝ ∧ 1 ≤ 𝑦))
4	3	simplbi 497	. . . . . 6 ⊢ (𝑦 ∈ (1[,)+∞) → 𝑦 ∈ ℝ)
5	4	ssriv 3962	. . . . 5 ⊢ (1[,)+∞) ⊆ ℝ
6	5	a1i 11	. . . 4 ⊢ (⊤ → (1[,)+∞) ⊆ ℝ)
7	1	a1i 11	. . . 4 ⊢ (⊤ → 1 ∈ ℝ)
8		fzfid 13989	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑦 ∈ (1[,)+∞)) → (1...(⌊‘𝑦)) ∈ Fin)
9		elfznn 13568	. . . . . . . . . . 11 ⊢ (𝑚 ∈ (1...(⌊‘𝑦)) → 𝑚 ∈ ℕ)
10	9	adantl 481	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑦))) → 𝑚 ∈ ℕ)
11		vmacl 27078	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ → (Λ‘𝑚) ∈ ℝ)
12	10, 11	syl 17	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑦))) → (Λ‘𝑚) ∈ ℝ)
13	10	nnrpd 13047	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑦))) → 𝑚 ∈ ℝ+)
14	13	relogcld 26582	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑦))) → (log‘𝑚) ∈ ℝ)
15	12, 14	remulcld 11263	. . . . . . . 8 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑦))) → ((Λ‘𝑚) · (log‘𝑚)) ∈ ℝ)
16	8, 15	fsumrecl 15748	. . . . . . 7 ⊢ ((⊤ ∧ 𝑦 ∈ (1[,)+∞)) → Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) ∈ ℝ)
17	4	adantl 481	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑦 ∈ (1[,)+∞)) → 𝑦 ∈ ℝ)
18		chpcl 27084	. . . . . . . . 9 ⊢ (𝑦 ∈ ℝ → (ψ‘𝑦) ∈ ℝ)
19	17, 18	syl 17	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑦 ∈ (1[,)+∞)) → (ψ‘𝑦) ∈ ℝ)
20		1rp 13010	. . . . . . . . . . 11 ⊢ 1 ∈ ℝ+
21	20	a1i 11	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑦 ∈ (1[,)+∞)) → 1 ∈ ℝ+)
22	3	simprbi 496	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (1[,)+∞) → 1 ≤ 𝑦)
23	22	adantl 481	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑦 ∈ (1[,)+∞)) → 1 ≤ 𝑦)
24	17, 21, 23	rpgecld 13088	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑦 ∈ (1[,)+∞)) → 𝑦 ∈ ℝ+)
25	24	relogcld 26582	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑦 ∈ (1[,)+∞)) → (log‘𝑦) ∈ ℝ)
26	19, 25	remulcld 11263	. . . . . . 7 ⊢ ((⊤ ∧ 𝑦 ∈ (1[,)+∞)) → ((ψ‘𝑦) · (log‘𝑦)) ∈ ℝ)
27	16, 26	resubcld 11663	. . . . . 6 ⊢ ((⊤ ∧ 𝑦 ∈ (1[,)+∞)) → (Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦))) ∈ ℝ)
28	27, 24	rerpdivcld 13080	. . . . 5 ⊢ ((⊤ ∧ 𝑦 ∈ (1[,)+∞)) → ((Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦))) / 𝑦) ∈ ℝ)
29	28	recnd 11261	. . . 4 ⊢ ((⊤ ∧ 𝑦 ∈ (1[,)+∞)) → ((Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦))) / 𝑦) ∈ ℂ)
30	24	ex 412	. . . . . 6 ⊢ (⊤ → (𝑦 ∈ (1[,)+∞) → 𝑦 ∈ ℝ+))
31	30	ssrdv 3964	. . . . 5 ⊢ (⊤ → (1[,)+∞) ⊆ ℝ+)
32		selberg2lem 27511	. . . . . 6 ⊢ (𝑦 ∈ ℝ+ ↦ ((Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦))) / 𝑦)) ∈ 𝑂(1)
33	32	a1i 11	. . . . 5 ⊢ (⊤ → (𝑦 ∈ ℝ+ ↦ ((Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦))) / 𝑦)) ∈ 𝑂(1))
34	31, 33	o1res2 15577	. . . 4 ⊢ (⊤ → (𝑦 ∈ (1[,)+∞) ↦ ((Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦))) / 𝑦)) ∈ 𝑂(1))
35		fzfid 13989	. . . . . 6 ⊢ ((⊤ ∧ (𝑥 ∈ ℝ ∧ 1 ≤ 𝑥)) → (1...(⌊‘𝑥)) ∈ Fin)
36		elfznn 13568	. . . . . . . . 9 ⊢ (𝑚 ∈ (1...(⌊‘𝑥)) → 𝑚 ∈ ℕ)
37	36	adantl 481	. . . . . . . 8 ⊢ (((⊤ ∧ (𝑥 ∈ ℝ ∧ 1 ≤ 𝑥)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → 𝑚 ∈ ℕ)
38	37, 11	syl 17	. . . . . . 7 ⊢ (((⊤ ∧ (𝑥 ∈ ℝ ∧ 1 ≤ 𝑥)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑚) ∈ ℝ)
39	37	nnrpd 13047	. . . . . . . 8 ⊢ (((⊤ ∧ (𝑥 ∈ ℝ ∧ 1 ≤ 𝑥)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → 𝑚 ∈ ℝ+)
40	39	relogcld 26582	. . . . . . 7 ⊢ (((⊤ ∧ (𝑥 ∈ ℝ ∧ 1 ≤ 𝑥)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (log‘𝑚) ∈ ℝ)
41	38, 40	remulcld 11263	. . . . . 6 ⊢ (((⊤ ∧ (𝑥 ∈ ℝ ∧ 1 ≤ 𝑥)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑚) · (log‘𝑚)) ∈ ℝ)
42	35, 41	fsumrecl 15748	. . . . 5 ⊢ ((⊤ ∧ (𝑥 ∈ ℝ ∧ 1 ≤ 𝑥)) → Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (log‘𝑚)) ∈ ℝ)
43		chpcl 27084	. . . . . . 7 ⊢ (𝑥 ∈ ℝ → (ψ‘𝑥) ∈ ℝ)
44	43	ad2antrl 728	. . . . . 6 ⊢ ((⊤ ∧ (𝑥 ∈ ℝ ∧ 1 ≤ 𝑥)) → (ψ‘𝑥) ∈ ℝ)
45		simprl 770	. . . . . . . 8 ⊢ ((⊤ ∧ (𝑥 ∈ ℝ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ)
46	20	a1i 11	. . . . . . . 8 ⊢ ((⊤ ∧ (𝑥 ∈ ℝ ∧ 1 ≤ 𝑥)) → 1 ∈ ℝ+)
47		simprr 772	. . . . . . . 8 ⊢ ((⊤ ∧ (𝑥 ∈ ℝ ∧ 1 ≤ 𝑥)) → 1 ≤ 𝑥)
48	45, 46, 47	rpgecld 13088	. . . . . . 7 ⊢ ((⊤ ∧ (𝑥 ∈ ℝ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ+)
49	48	relogcld 26582	. . . . . 6 ⊢ ((⊤ ∧ (𝑥 ∈ ℝ ∧ 1 ≤ 𝑥)) → (log‘𝑥) ∈ ℝ)
50	44, 49	remulcld 11263	. . . . 5 ⊢ ((⊤ ∧ (𝑥 ∈ ℝ ∧ 1 ≤ 𝑥)) → ((ψ‘𝑥) · (log‘𝑥)) ∈ ℝ)
51	42, 50	readdcld 11262	. . . 4 ⊢ ((⊤ ∧ (𝑥 ∈ ℝ ∧ 1 ≤ 𝑥)) → (Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘𝑥) · (log‘𝑥))) ∈ ℝ)
52	27	adantr 480	. . . . . . . 8 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦))) ∈ ℝ)
53	52	recnd 11261	. . . . . . 7 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦))) ∈ ℂ)
54	24	adantr 480	. . . . . . . 8 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → 𝑦 ∈ ℝ+)
55	54	rpcnd 13051	. . . . . . 7 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → 𝑦 ∈ ℂ)
56	54	rpne0d 13054	. . . . . . 7 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → 𝑦 ≠ 0)
57	53, 55, 56	absdivd 15472	. . . . . 6 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (abs‘((Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦))) / 𝑦)) = ((abs‘(Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦)))) / (abs‘𝑦)))
58	17	adantr 480	. . . . . . . 8 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → 𝑦 ∈ ℝ)
59	54	rpge0d 13053	. . . . . . . 8 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → 0 ≤ 𝑦)
60	58, 59	absidd 15439	. . . . . . 7 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (abs‘𝑦) = 𝑦)
61	60	oveq2d 7419	. . . . . 6 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → ((abs‘(Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦)))) / (abs‘𝑦)) = ((abs‘(Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦)))) / 𝑦))
62	57, 61	eqtrd 2770	. . . . 5 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (abs‘((Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦))) / 𝑦)) = ((abs‘(Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦)))) / 𝑦))
63	53	abscld 15453	. . . . . . 7 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (abs‘(Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦)))) ∈ ℝ)
64	63, 54	rerpdivcld 13080	. . . . . 6 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → ((abs‘(Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦)))) / 𝑦) ∈ ℝ)
65	42	ad2ant2r 747	. . . . . . 7 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (log‘𝑚)) ∈ ℝ)
66		simprll 778	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → 𝑥 ∈ ℝ)
67	66, 43	syl 17	. . . . . . . 8 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (ψ‘𝑥) ∈ ℝ)
68		simprr 772	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → 𝑦 < 𝑥)
69	58, 66, 68	ltled 11381	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → 𝑦 ≤ 𝑥)
70	66, 54, 69	rpgecld 13088	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → 𝑥 ∈ ℝ+)
71	70	relogcld 26582	. . . . . . . 8 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (log‘𝑥) ∈ ℝ)
72	67, 71	remulcld 11263	. . . . . . 7 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → ((ψ‘𝑥) · (log‘𝑥)) ∈ ℝ)
73	65, 72	readdcld 11262	. . . . . 6 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘𝑥) · (log‘𝑥))) ∈ ℝ)
74	20	a1i 11	. . . . . . . 8 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → 1 ∈ ℝ+)
75	53	absge0d 15461	. . . . . . . 8 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → 0 ≤ (abs‘(Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦)))))
76	23	adantr 480	. . . . . . . 8 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → 1 ≤ 𝑦)
77	74, 54, 63, 75, 76	lediv2ad 13071	. . . . . . 7 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → ((abs‘(Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦)))) / 𝑦) ≤ ((abs‘(Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦)))) / 1))
78	63	recnd 11261	. . . . . . . 8 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (abs‘(Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦)))) ∈ ℂ)
79	78	div1d 12007	. . . . . . 7 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → ((abs‘(Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦)))) / 1) = (abs‘(Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦)))))
80	77, 79	breqtrd 5145	. . . . . 6 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → ((abs‘(Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦)))) / 𝑦) ≤ (abs‘(Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦)))))
81	16	adantr 480	. . . . . . . 8 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) ∈ ℝ)
82	58, 18	syl 17	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (ψ‘𝑦) ∈ ℝ)
83	54	relogcld 26582	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (log‘𝑦) ∈ ℝ)
84	82, 83	remulcld 11263	. . . . . . . 8 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → ((ψ‘𝑦) · (log‘𝑦)) ∈ ℝ)
85	81, 84	readdcld 11262	. . . . . . 7 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘𝑦) · (log‘𝑦))) ∈ ℝ)
86	81	recnd 11261	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) ∈ ℂ)
87	26	adantr 480	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → ((ψ‘𝑦) · (log‘𝑦)) ∈ ℝ)
88	87	recnd 11261	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → ((ψ‘𝑦) · (log‘𝑦)) ∈ ℂ)
89	86, 88	abs2dif2d 15475	. . . . . . . 8 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (abs‘(Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦)))) ≤ ((abs‘Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚))) + (abs‘((ψ‘𝑦) · (log‘𝑦)))))
90		vmage0 27081	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ → 0 ≤ (Λ‘𝑚))
91	10, 90	syl 17	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑦))) → 0 ≤ (Λ‘𝑚))
92	10	nnred 12253	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑦))) → 𝑚 ∈ ℝ)
93	10	nnge1d 12286	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑦))) → 1 ≤ 𝑚)
94	92, 93	logge0d 26589	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑦))) → 0 ≤ (log‘𝑚))
95	12, 14, 91, 94	mulge0d 11812	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑦))) → 0 ≤ ((Λ‘𝑚) · (log‘𝑚)))
96	8, 15, 95	fsumge0 15809	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑦 ∈ (1[,)+∞)) → 0 ≤ Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)))
97	96	adantr 480	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → 0 ≤ Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)))
98	81, 97	absidd 15439	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (abs‘Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚))) = Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)))
99		chpge0 27086	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℝ → 0 ≤ (ψ‘𝑦))
100	58, 99	syl 17	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → 0 ≤ (ψ‘𝑦))
101	58, 76	logge0d 26589	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → 0 ≤ (log‘𝑦))
102	82, 83, 100, 101	mulge0d 11812	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → 0 ≤ ((ψ‘𝑦) · (log‘𝑦)))
103	87, 102	absidd 15439	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (abs‘((ψ‘𝑦) · (log‘𝑦))) = ((ψ‘𝑦) · (log‘𝑦)))
104	98, 103	oveq12d 7421	. . . . . . . 8 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → ((abs‘Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚))) + (abs‘((ψ‘𝑦) · (log‘𝑦)))) = (Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘𝑦) · (log‘𝑦))))
105	89, 104	breqtrd 5145	. . . . . . 7 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (abs‘(Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦)))) ≤ (Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘𝑦) · (log‘𝑦))))
106		fzfid 13989	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (1...(⌊‘𝑥)) ∈ Fin)
107	36	adantl 481	. . . . . . . . . . 11 ⊢ ((((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → 𝑚 ∈ ℕ)
108	107, 11	syl 17	. . . . . . . . . 10 ⊢ ((((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑚) ∈ ℝ)
109	107	nnrpd 13047	. . . . . . . . . . 11 ⊢ ((((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → 𝑚 ∈ ℝ+)
110	109	relogcld 26582	. . . . . . . . . 10 ⊢ ((((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (log‘𝑚) ∈ ℝ)
111	108, 110	remulcld 11263	. . . . . . . . 9 ⊢ ((((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑚) · (log‘𝑚)) ∈ ℝ)
112	107, 90	syl 17	. . . . . . . . . 10 ⊢ ((((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → 0 ≤ (Λ‘𝑚))
113	107	nnred 12253	. . . . . . . . . . 11 ⊢ ((((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → 𝑚 ∈ ℝ)
114	107	nnge1d 12286	. . . . . . . . . . 11 ⊢ ((((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → 1 ≤ 𝑚)
115	113, 114	logge0d 26589	. . . . . . . . . 10 ⊢ ((((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → 0 ≤ (log‘𝑚))
116	108, 110, 112, 115	mulge0d 11812	. . . . . . . . 9 ⊢ ((((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → 0 ≤ ((Λ‘𝑚) · (log‘𝑚)))
117		flword2 13828	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ 𝑦 ≤ 𝑥) → (⌊‘𝑥) ∈ (ℤ≥‘(⌊‘𝑦)))
118	58, 66, 69, 117	syl3anc 1373	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (⌊‘𝑥) ∈ (ℤ≥‘(⌊‘𝑦)))
119		fzss2 13579	. . . . . . . . . 10 ⊢ ((⌊‘𝑥) ∈ (ℤ≥‘(⌊‘𝑦)) → (1...(⌊‘𝑦)) ⊆ (1...(⌊‘𝑥)))
120	118, 119	syl 17	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (1...(⌊‘𝑦)) ⊆ (1...(⌊‘𝑥)))
121	106, 111, 116, 120	fsumless 15810	. . . . . . . 8 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) ≤ Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (log‘𝑚)))
122		chpwordi 27117	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ 𝑦 ≤ 𝑥) → (ψ‘𝑦) ≤ (ψ‘𝑥))
123	58, 66, 69, 122	syl3anc 1373	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (ψ‘𝑦) ≤ (ψ‘𝑥))
124	54, 70	logled 26586	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (𝑦 ≤ 𝑥 ↔ (log‘𝑦) ≤ (log‘𝑥)))
125	69, 124	mpbid 232	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (log‘𝑦) ≤ (log‘𝑥))
126	82, 67, 83, 71, 100, 101, 123, 125	lemul12ad 12182	. . . . . . . 8 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → ((ψ‘𝑦) · (log‘𝑦)) ≤ ((ψ‘𝑥) · (log‘𝑥)))
127	81, 84, 65, 72, 121, 126	le2addd 11854	. . . . . . 7 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘𝑦) · (log‘𝑦))) ≤ (Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘𝑥) · (log‘𝑥))))
128	63, 85, 73, 105, 127	letrd 11390	. . . . . 6 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (abs‘(Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦)))) ≤ (Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘𝑥) · (log‘𝑥))))
129	64, 63, 73, 80, 128	letrd 11390	. . . . 5 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → ((abs‘(Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦)))) / 𝑦) ≤ (Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘𝑥) · (log‘𝑥))))
130	62, 129	eqbrtrd 5141	. . . 4 ⊢ (((⊤ ∧ 𝑦 ∈ (1[,)+∞)) ∧ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) ∧ 𝑦 < 𝑥)) → (abs‘((Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦))) / 𝑦)) ≤ (Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘𝑥) · (log‘𝑥))))
131	6, 7, 29, 34, 51, 130	o1bddrp 15556	. . 3 ⊢ (⊤ → ∃𝑐 ∈ ℝ+ ∀𝑦 ∈ (1[,)+∞)(abs‘((Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦))) / 𝑦)) ≤ 𝑐)
132	131	mptru 1547	. 2 ⊢ ∃𝑐 ∈ ℝ+ ∀𝑦 ∈ (1[,)+∞)(abs‘((Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦))) / 𝑦)) ≤ 𝑐
133		simpl 482	. . . 4 ⊢ ((𝑐 ∈ ℝ+ ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦))) / 𝑦)) ≤ 𝑐) → 𝑐 ∈ ℝ+)
134		simpr 484	. . . 4 ⊢ ((𝑐 ∈ ℝ+ ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦))) / 𝑦)) ≤ 𝑐) → ∀𝑦 ∈ (1[,)+∞)(abs‘((Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦))) / 𝑦)) ≤ 𝑐)
135	133, 134	selberg3lem1 27518	. . 3 ⊢ ((𝑐 ∈ ℝ+ ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦))) / 𝑦)) ≤ 𝑐) → (𝑥 ∈ (1(,)+∞) ↦ ((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥)) ∈ 𝑂(1))
136	135	rexlimiva 3133	. 2 ⊢ (∃𝑐 ∈ ℝ+ ∀𝑦 ∈ (1[,)+∞)(abs‘((Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘𝑦) · (log‘𝑦))) / 𝑦)) ≤ 𝑐 → (𝑥 ∈ (1(,)+∞) ↦ ((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥)) ∈ 𝑂(1))
137	132, 136	ax-mp 5	1 ⊢ (𝑥 ∈ (1(,)+∞) ↦ ((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥)) ∈ 𝑂(1)

Syntax hints:   ↔ wb 206   ∧ wa 395  ⊤wtru 1541   ∈ wcel 2108  ∀wral 3051  ∃wrex 3060   ⊆ wss 3926   class class class wbr 5119   ↦ cmpt 5201  ‘cfv 6530  (class class class)co 7403  ℝcr 11126  0cc0 11127  1c1 11128   + caddc 11130   · cmul 11132  +∞cpnf 11264   < clt 11267   ≤ cle 11268   − cmin 11464   / cdiv 11892  ℕcn 12238  2c2 12293  ℤ_≥cuz 12850  ℝ⁺crp 13006  (,)cioo 13360  [,)cico 13362  ...cfz 13522  ⌊cfl 13805  abscabs 15251  𝑂(1)co1 15500  Σcsu 15700  logclog 26513  Λcvma 27052  ψcchp 27053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-rep 5249  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727  ax-inf2 9653  ax-cnex 11183  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203  ax-pre-mulgt0 11204  ax-pre-sup 11205  ax-addf 11206

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3359  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-tp 4606  df-op 4608  df-uni 4884  df-int 4923  df-iun 4969  df-iin 4970  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-se 5607  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-fv 6538  df-isom 6539  df-riota 7360  df-ov 7406  df-oprab 7407  df-mpo 7408  df-of 7669  df-om 7860  df-1st 7986  df-2nd 7987  df-supp 8158  df-frecs 8278  df-wrecs 8309  df-recs 8383  df-rdg 8422  df-1o 8478  df-2o 8479  df-oadd 8482  df-er 8717  df-map 8840  df-pm 8841  df-ixp 8910  df-en 8958  df-dom 8959  df-sdom 8960  df-fin 8961  df-fsupp 9372  df-fi 9421  df-sup 9452  df-inf 9453  df-oi 9522  df-dju 9913  df-card 9951  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273  df-sub 11466  df-neg 11467  df-div 11893  df-nn 12239  df-2 12301  df-3 12302  df-4 12303  df-5 12304  df-6 12305  df-7 12306  df-8 12307  df-9 12308  df-n0 12500  df-xnn0 12573  df-z 12587  df-dec 12707  df-uz 12851  df-q 12963  df-rp 13007  df-xneg 13126  df-xadd 13127  df-xmul 13128  df-ioo 13364  df-ioc 13365  df-ico 13366  df-icc 13367  df-fz 13523  df-fzo 13670  df-fl 13807  df-mod 13885  df-seq 14018  df-exp 14078  df-fac 14290  df-bc 14319  df-hash 14347  df-shft 15084  df-cj 15116  df-re 15117  df-im 15118  df-sqrt 15252  df-abs 15253  df-limsup 15485  df-clim 15502  df-rlim 15503  df-o1 15504  df-lo1 15505  df-sum 15701  df-ef 16081  df-e 16082  df-sin 16083  df-cos 16084  df-pi 16086  df-dvds 16271  df-gcd 16512  df-prm 16689  df-pc 16855  df-struct 17164  df-sets 17181  df-slot 17199  df-ndx 17211  df-base 17227  df-ress 17250  df-plusg 17282  df-mulr 17283  df-starv 17284  df-sca 17285  df-vsca 17286  df-ip 17287  df-tset 17288  df-ple 17289  df-ds 17291  df-unif 17292  df-hom 17293  df-cco 17294  df-rest 17434  df-topn 17435  df-0g 17453  df-gsum 17454  df-topgen 17455  df-pt 17456  df-prds 17459  df-xrs 17514  df-qtop 17519  df-imas 17520  df-xps 17522  df-mre 17596  df-mrc 17597  df-acs 17599  df-mgm 18616  df-sgrp 18695  df-mnd 18711  df-submnd 18760  df-mulg 19049  df-cntz 19298  df-cmn 19761  df-psmet 21305  df-xmet 21306  df-met 21307  df-bl 21308  df-mopn 21309  df-fbas 21310  df-fg 21311  df-cnfld 21314  df-top 22830  df-topon 22847  df-topsp 22869  df-bases 22882  df-cld 22955  df-ntr 22956  df-cls 22957  df-nei 23034  df-lp 23072  df-perf 23073  df-cn 23163  df-cnp 23164  df-haus 23251  df-cmp 23323  df-tx 23498  df-hmeo 23691  df-fil 23782  df-fm 23874  df-flim 23875  df-flf 23876  df-xms 24257  df-ms 24258  df-tms 24259  df-cncf 24820  df-limc 25817  df-dv 25818  df-log 26515  df-cxp 26516  df-cht 27057  df-vma 27058  df-chp 27059  df-ppi 27060

This theorem is referenced by:  selberg3  27520  selberg4  27522