selberg3lem1 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > selberg3lem1		Structured version Visualization version GIF version

Theorem selberg3lem1 26127

Description: Introduce a log weighting on the summands of Σ𝑚 · 𝑛 ≤ 𝑥, Λ(𝑚)Λ(𝑛), the core of selberg2 26121 (written here as Σ𝑛 ≤ 𝑥, Λ(𝑛)ψ(𝑥 / 𝑛)). Equation 10.4.21 of [Shapiro], p. 422. (Contributed by Mario Carneiro, 30-May-2016.)

**Hypotheses**
Ref	Expression
selberg3lem1.1	⊢ (𝜑 → 𝐴 ∈ ℝ⁺)
selberg3lem1.2	⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((Σ𝑘 ∈ (1...(⌊‘𝑦))((Λ‘𝑘) · (log‘𝑘)) − ((ψ‘𝑦) · (log‘𝑦))) / 𝑦)) ≤ 𝐴)

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

Distinct variable groups: 𝑘,𝑛,𝑥,𝑦,𝐴 𝜑,𝑛,𝑥 Allowed substitution hints: 𝜑(𝑦,𝑘)

Proof of Theorem selberg3lem1 Dummy variable 𝑚 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		1red 10636	. 2 ⊢ (𝜑 → 1 ∈ ℝ)
2		ioossre 12792	. . . 4 ⊢ (1(,)+∞) ⊆ ℝ
3		selberg3lem1.1	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ ℝ⁺)
4	3	rpcnd 12427	. . . 4 ⊢ (𝜑 → 𝐴 ∈ ℂ)
5		o1const 14970	. . . 4 ⊢ (((1(,)+∞) ⊆ ℝ ∧ 𝐴 ∈ ℂ) → (𝑥 ∈ (1(,)+∞) ↦ 𝐴) ∈ 𝑂(1))
6	2, 4, 5	sylancr 589	. . 3 ⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ 𝐴) ∈ 𝑂(1))
7		fzfid 13335	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (1...(⌊‘𝑥)) ∈ Fin)
8		elfznn 12930	. . . . . . . . . 10 ⊢ (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
9	8	adantl 484	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
10		vmacl 25689	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ → (Λ‘𝑛) ∈ ℝ)
11	9, 10	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈ ℝ)
12	11, 9	nndivred 11685	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) / 𝑛) ∈ ℝ)
13	7, 12	fsumrecl 15085	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ∈ ℝ)
14		elioore 12762	. . . . . . . . 9 ⊢ (𝑥 ∈ (1(,)+∞) → 𝑥 ∈ ℝ)
15		eliooord 12790	. . . . . . . . . 10 ⊢ (𝑥 ∈ (1(,)+∞) → (1 < 𝑥 ∧ 𝑥 < +∞))
16	15	simpld 497	. . . . . . . . 9 ⊢ (𝑥 ∈ (1(,)+∞) → 1 < 𝑥)
17	14, 16	rplogcld 25206	. . . . . . . 8 ⊢ (𝑥 ∈ (1(,)+∞) → (log‘𝑥) ∈ ℝ⁺)
18		rpdivcl 12408	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ⁺ ∧ (log‘𝑥) ∈ ℝ⁺) → (𝐴 / (log‘𝑥)) ∈ ℝ⁺)
19	3, 17, 18	syl2an 597	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (𝐴 / (log‘𝑥)) ∈ ℝ⁺)
20	19	rpred 12425	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (𝐴 / (log‘𝑥)) ∈ ℝ)
21	13, 20	remulcld 10665	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 / (log‘𝑥))) ∈ ℝ)
22	21	recnd 10663	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 / (log‘𝑥))) ∈ ℂ)
23	4	adantr 483	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 𝐴 ∈ ℂ)
24	13	recnd 10663	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ∈ ℂ)
25	17	adantl 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ∈ ℝ⁺)
26	25	rpcnd 12427	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ∈ ℂ)
27	19	rpcnd 12427	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (𝐴 / (log‘𝑥)) ∈ ℂ)
28	24, 26, 27	subdird 11091	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) · (𝐴 / (log‘𝑥))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 / (log‘𝑥))) − ((log‘𝑥) · (𝐴 / (log‘𝑥)))))
29	25	rpne0d 12430	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ≠ 0)
30	23, 26, 29	divcan2d 11412	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((log‘𝑥) · (𝐴 / (log‘𝑥))) = 𝐴)
31	30	oveq2d 7166	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 / (log‘𝑥))) − ((log‘𝑥) · (𝐴 / (log‘𝑥)))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 / (log‘𝑥))) − 𝐴))
32	28, 31	eqtrd 2856	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) · (𝐴 / (log‘𝑥))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 / (log‘𝑥))) − 𝐴))
33	32	mpteq2dva 5153	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) · (𝐴 / (log‘𝑥)))) = (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 / (log‘𝑥))) − 𝐴)))
34	25	rpred 12425	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ∈ ℝ)
35	13, 34	resubcld 11062	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) ∈ ℝ)
36	14	adantl 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ∈ ℝ)
37		0red 10638	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 0 ∈ ℝ)
38		1red 10636	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 1 ∈ ℝ)
39		0lt1 11156	. . . . . . . . . . . 12 ⊢ 0 < 1
40	39	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 0 < 1)
41	16	adantl 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 1 < 𝑥)
42	37, 38, 36, 40, 41	lttrd 10795	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 0 < 𝑥)
43	36, 42	elrpd 12422	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ∈ ℝ⁺)
44	43	ex 415	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) → 𝑥 ∈ ℝ⁺))
45	44	ssrdv 3972	. . . . . . 7 ⊢ (𝜑 → (1(,)+∞) ⊆ ℝ⁺)
46		vmadivsum 26052	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1)
47	46	a1i 11	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1))
48	45, 47	o1res2 14914	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1))
49	2	a1i 11	. . . . . . 7 ⊢ (𝜑 → (1(,)+∞) ⊆ ℝ)
50		ere 15436	. . . . . . . 8 ⊢ e ∈ ℝ
51	50	a1i 11	. . . . . . 7 ⊢ (𝜑 → e ∈ ℝ)
52	3	rpred 12425	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℝ)
53	19	adantrr 715	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → (𝐴 / (log‘𝑥)) ∈ ℝ⁺)
54	53	rprege0d 12432	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → ((𝐴 / (log‘𝑥)) ∈ ℝ ∧ 0 ≤ (𝐴 / (log‘𝑥))))
55		absid 14650	. . . . . . . . 9 ⊢ (((𝐴 / (log‘𝑥)) ∈ ℝ ∧ 0 ≤ (𝐴 / (log‘𝑥))) → (abs‘(𝐴 / (log‘𝑥))) = (𝐴 / (log‘𝑥)))
56	54, 55	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → (abs‘(𝐴 / (log‘𝑥))) = (𝐴 / (log‘𝑥)))
57		loge 25164	. . . . . . . . . . 11 ⊢ (log‘e) = 1
58		simprr 771	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → e ≤ 𝑥)
59		epr 15555	. . . . . . . . . . . . 13 ⊢ e ∈ ℝ⁺
60	43	adantrr 715	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → 𝑥 ∈ ℝ⁺)
61		logleb 25180	. . . . . . . . . . . . 13 ⊢ ((e ∈ ℝ⁺ ∧ 𝑥 ∈ ℝ⁺) → (e ≤ 𝑥 ↔ (log‘e) ≤ (log‘𝑥)))
62	59, 60, 61	sylancr 589	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → (e ≤ 𝑥 ↔ (log‘e) ≤ (log‘𝑥)))
63	58, 62	mpbid 234	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → (log‘e) ≤ (log‘𝑥))
64	57, 63	eqbrtrrid 5094	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → 1 ≤ (log‘𝑥))
65		1rp 12387	. . . . . . . . . . . 12 ⊢ 1 ∈ ℝ⁺
66		rpregt0 12397	. . . . . . . . . . . 12 ⊢ (1 ∈ ℝ⁺ → (1 ∈ ℝ ∧ 0 < 1))
67	65, 66	mp1i 13	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → (1 ∈ ℝ ∧ 0 < 1))
68	25	adantrr 715	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → (log‘𝑥) ∈ ℝ⁺)
69	68	rpregt0d 12431	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → ((log‘𝑥) ∈ ℝ ∧ 0 < (log‘𝑥)))
70	3	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → 𝐴 ∈ ℝ⁺)
71	70	rpregt0d 12431	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → (𝐴 ∈ ℝ ∧ 0 < 𝐴))
72		lediv2 11524	. . . . . . . . . . 11 ⊢ (((1 ∈ ℝ ∧ 0 < 1) ∧ ((log‘𝑥) ∈ ℝ ∧ 0 < (log‘𝑥)) ∧ (𝐴 ∈ ℝ ∧ 0 < 𝐴)) → (1 ≤ (log‘𝑥) ↔ (𝐴 / (log‘𝑥)) ≤ (𝐴 / 1)))
73	67, 69, 71, 72	syl3anc 1367	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → (1 ≤ (log‘𝑥) ↔ (𝐴 / (log‘𝑥)) ≤ (𝐴 / 1)))
74	64, 73	mpbid 234	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → (𝐴 / (log‘𝑥)) ≤ (𝐴 / 1))
75	4	adantr 483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → 𝐴 ∈ ℂ)
76	75	div1d 11402	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → (𝐴 / 1) = 𝐴)
77	74, 76	breqtrd 5084	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → (𝐴 / (log‘𝑥)) ≤ 𝐴)
78	56, 77	eqbrtrd 5080	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → (abs‘(𝐴 / (log‘𝑥))) ≤ 𝐴)
79	49, 27, 51, 52, 78	elo1d 14887	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (𝐴 / (log‘𝑥))) ∈ 𝑂(1))
80	35, 20, 48, 79	o1mul2 14975	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) · (𝐴 / (log‘𝑥)))) ∈ 𝑂(1))
81	33, 80	eqeltrrd 2914	. . . 4 ⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 / (log‘𝑥))) − 𝐴)) ∈ 𝑂(1))
82	22, 23, 81	o1dif 14980	. . 3 ⊢ (𝜑 → ((𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 / (log‘𝑥)))) ∈ 𝑂(1) ↔ (𝑥 ∈ (1(,)+∞) ↦ 𝐴) ∈ 𝑂(1)))
83	6, 82	mpbird 259	. 2 ⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 / (log‘𝑥)))) ∈ 𝑂(1))
84		2re 11705	. . . . . . 7 ⊢ 2 ∈ ℝ
85		rerpdivcl 12413	. . . . . . 7 ⊢ ((2 ∈ ℝ ∧ (log‘𝑥) ∈ ℝ⁺) → (2 / (log‘𝑥)) ∈ ℝ)
86	84, 25, 85	sylancr 589	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (2 / (log‘𝑥)) ∈ ℝ)
87		nndivre 11672	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℕ) → (𝑥 / 𝑛) ∈ ℝ)
88	36, 8, 87	syl2an 597	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ)
89		chpcl 25695	. . . . . . . . . 10 ⊢ ((𝑥 / 𝑛) ∈ ℝ → (ψ‘(𝑥 / 𝑛)) ∈ ℝ)
90	88, 89	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (ψ‘(𝑥 / 𝑛)) ∈ ℝ)
91	11, 90	remulcld 10665	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) ∈ ℝ)
92	9	nnrpd 12423	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ⁺)
93	92	relogcld 25200	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘𝑛) ∈ ℝ)
94	91, 93	remulcld 10665	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛)) ∈ ℝ)
95	7, 94	fsumrecl 15085	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛)) ∈ ℝ)
96	86, 95	remulcld 10665	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) ∈ ℝ)
97	7, 91	fsumrecl 15085	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) ∈ ℝ)
98	96, 97	resubcld 11062	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) ∈ ℝ)
99	98, 43	rerpdivcld 12456	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥) ∈ ℝ)
100	99	recnd 10663	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥) ∈ ℂ)
101	100	abscld 14790	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥)) ∈ ℝ)
102	22	abscld 14790	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 / (log‘𝑥)))) ∈ ℝ)
103		2cnd 11709	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 2 ∈ ℂ)
104	95	recnd 10663	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛)) ∈ ℂ)
105	103, 104	mulcld 10655	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) ∈ ℂ)
106	97	recnd 10663	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) ∈ ℂ)
107	106, 26	mulcld 10655	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)) ∈ ℂ)
108	105, 107	subcld 10991	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))) ∈ ℂ)
109	108	abscld 14790	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) ∈ ℝ)
110	42	gt0ne0d 11198	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ≠ 0)
111	109, 36, 110	redivcld 11462	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) / 𝑥) ∈ ℝ)
112	52	adantr 483	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 𝐴 ∈ ℝ)
113	13, 112	remulcld 10665	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝐴) ∈ ℝ)
114	11	recnd 10663	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈ ℂ)
115		fzfid 13335	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1...(⌊‘(𝑥 / 𝑛))) ∈ Fin)
116		elfznn 12930	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛))) → 𝑚 ∈ ℕ)
117	116	adantl 484	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ∈ ℕ)
118		vmacl 25689	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ∈ ℕ → (Λ‘𝑚) ∈ ℝ)
119	117, 118	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (Λ‘𝑚) ∈ ℝ)
120	117	nnrpd 12423	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ∈ ℝ⁺)
121	120	relogcld 25200	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (log‘𝑚) ∈ ℝ)
122	119, 121	remulcld 10665	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((Λ‘𝑚) · (log‘𝑚)) ∈ ℝ)
123	115, 122	fsumrecl 15085	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) ∈ ℝ)
124	8	nnrpd 12423	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℝ⁺)
125		rpdivcl 12408	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ ℝ⁺) → (𝑥 / 𝑛) ∈ ℝ⁺)
126	43, 124, 125	syl2an 597	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ⁺)
127	126	relogcld 25200	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ∈ ℝ)
128	90, 127	remulcld 10665	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))) ∈ ℝ)
129	123, 128	resubcld 11062	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))) ∈ ℝ)
130	129	recnd 10663	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))) ∈ ℂ)
131	114, 130	mulcld 10655	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))) ∈ ℂ)
132	7, 131	fsumcl 15084	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))) ∈ ℂ)
133	132	abscld 14790	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))))) ∈ ℝ)
134	131	abscld 14790	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))))) ∈ ℝ)
135	7, 134	fsumrecl 15085	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))))) ∈ ℝ)
136	112, 36	remulcld 10665	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (𝐴 · 𝑥) ∈ ℝ)
137	13, 136	remulcld 10665	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 · 𝑥)) ∈ ℝ)
138	7, 131	fsumabs 15150	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))))))
139	52	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝐴 ∈ ℝ)
140	36	adantr 483	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ)
141	139, 140	remulcld 10665	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝐴 · 𝑥) ∈ ℝ)
142	12, 141	remulcld 10665	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) / 𝑛) · (𝐴 · 𝑥)) ∈ ℝ)
143	130	abscld 14790	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))) ∈ ℝ)
144	141, 9	nndivred 11685	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝐴 · 𝑥) / 𝑛) ∈ ℝ)
145		vmage0 25692	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → 0 ≤ (Λ‘𝑛))
146	9, 145	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (Λ‘𝑛))
147	88	recnd 10663	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℂ)
148	126	rpne0d 12430	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ≠ 0)
149	130, 147, 148	absdivd 14809	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))) / (𝑥 / 𝑛))) = ((abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))) / (abs‘(𝑥 / 𝑛))))
150	126	rpge0d 12429	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (𝑥 / 𝑛))
151	88, 150	absidd 14776	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑥 / 𝑛)) = (𝑥 / 𝑛))
152	151	oveq2d 7166	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))) / (abs‘(𝑥 / 𝑛))) = ((abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))) / (𝑥 / 𝑛)))
153	149, 152	eqtrd 2856	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))) / (𝑥 / 𝑛))) = ((abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))) / (𝑥 / 𝑛)))
154		fveq2 6664	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = 𝑚 → (Λ‘𝑘) = (Λ‘𝑚))
155		fveq2 6664	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = 𝑚 → (log‘𝑘) = (log‘𝑚))
156	154, 155	oveq12d 7168	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = 𝑚 → ((Λ‘𝑘) · (log‘𝑘)) = ((Λ‘𝑚) · (log‘𝑚)))
157	156	cbvsumv 15047	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Σ𝑘 ∈ (1...(⌊‘𝑦))((Λ‘𝑘) · (log‘𝑘)) = Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚))
158		fveq2 6664	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = (𝑥 / 𝑛) → (⌊‘𝑦) = (⌊‘(𝑥 / 𝑛)))
159	158	oveq2d 7166	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = (𝑥 / 𝑛) → (1...(⌊‘𝑦)) = (1...(⌊‘(𝑥 / 𝑛))))
160	159	sumeq1d 15052	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = (𝑥 / 𝑛) → Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)))
161	157, 160	syl5eq 2868	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = (𝑥 / 𝑛) → Σ𝑘 ∈ (1...(⌊‘𝑦))((Λ‘𝑘) · (log‘𝑘)) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)))
162		fveq2 6664	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = (𝑥 / 𝑛) → (ψ‘𝑦) = (ψ‘(𝑥 / 𝑛)))
163		fveq2 6664	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = (𝑥 / 𝑛) → (log‘𝑦) = (log‘(𝑥 / 𝑛)))
164	162, 163	oveq12d 7168	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = (𝑥 / 𝑛) → ((ψ‘𝑦) · (log‘𝑦)) = ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))
165	161, 164	oveq12d 7168	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (𝑥 / 𝑛) → (Σ𝑘 ∈ (1...(⌊‘𝑦))((Λ‘𝑘) · (log‘𝑘)) − ((ψ‘𝑦) · (log‘𝑦))) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))))
166		id 22	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (𝑥 / 𝑛) → 𝑦 = (𝑥 / 𝑛))
167	165, 166	oveq12d 7168	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (𝑥 / 𝑛) → ((Σ𝑘 ∈ (1...(⌊‘𝑦))((Λ‘𝑘) · (log‘𝑘)) − ((ψ‘𝑦) · (log‘𝑦))) / 𝑦) = ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))) / (𝑥 / 𝑛)))
168	167	fveq2d 6668	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = (𝑥 / 𝑛) → (abs‘((Σ𝑘 ∈ (1...(⌊‘𝑦))((Λ‘𝑘) · (log‘𝑘)) − ((ψ‘𝑦) · (log‘𝑦))) / 𝑦)) = (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))) / (𝑥 / 𝑛))))
169	168	breq1d 5068	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (𝑥 / 𝑛) → ((abs‘((Σ𝑘 ∈ (1...(⌊‘𝑦))((Λ‘𝑘) · (log‘𝑘)) − ((ψ‘𝑦) · (log‘𝑦))) / 𝑦)) ≤ 𝐴 ↔ (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))) / (𝑥 / 𝑛))) ≤ 𝐴))
170		selberg3lem1.2	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((Σ𝑘 ∈ (1...(⌊‘𝑦))((Λ‘𝑘) · (log‘𝑘)) − ((ψ‘𝑦) · (log‘𝑦))) / 𝑦)) ≤ 𝐴)
171	170	ad2antrr 724	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ∀𝑦 ∈ (1[,)+∞)(abs‘((Σ𝑘 ∈ (1...(⌊‘𝑦))((Λ‘𝑘) · (log‘𝑘)) − ((ψ‘𝑦) · (log‘𝑦))) / 𝑦)) ≤ 𝐴)
172	9	nncnd 11648	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℂ)
173	172	mulid2d 10653	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 · 𝑛) = 𝑛)
174		fznnfl 13224	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℝ → (𝑛 ∈ (1...(⌊‘𝑥)) ↔ (𝑛 ∈ ℕ ∧ 𝑛 ≤ 𝑥)))
175	36, 174	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (𝑛 ∈ (1...(⌊‘𝑥)) ↔ (𝑛 ∈ ℕ ∧ 𝑛 ≤ 𝑥)))
176	175	simplbda 502	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ≤ 𝑥)
177	173, 176	eqbrtrd 5080	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 · 𝑛) ≤ 𝑥)
178		1red 10636	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℝ)
179	178, 140, 92	lemuldivd 12474	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 · 𝑛) ≤ 𝑥 ↔ 1 ≤ (𝑥 / 𝑛)))
180	177, 179	mpbid 234	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ≤ (𝑥 / 𝑛))
181		1re 10635	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℝ
182		elicopnf 12827	. . . . . . . . . . . . . . . . . . 19 ⊢ (1 ∈ ℝ → ((𝑥 / 𝑛) ∈ (1[,)+∞) ↔ ((𝑥 / 𝑛) ∈ ℝ ∧ 1 ≤ (𝑥 / 𝑛))))
183	181, 182	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 / 𝑛) ∈ (1[,)+∞) ↔ ((𝑥 / 𝑛) ∈ ℝ ∧ 1 ≤ (𝑥 / 𝑛)))
184	88, 180, 183	sylanbrc 585	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ (1[,)+∞))
185	169, 171, 184	rspcdva 3624	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))) / (𝑥 / 𝑛))) ≤ 𝐴)
186	153, 185	eqbrtrrd 5082	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))) / (𝑥 / 𝑛)) ≤ 𝐴)
187	143, 139, 126	ledivmul2d 12479	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))) / (𝑥 / 𝑛)) ≤ 𝐴 ↔ (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))) ≤ (𝐴 · (𝑥 / 𝑛))))
188	186, 187	mpbid 234	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))) ≤ (𝐴 · (𝑥 / 𝑛)))
189	23	adantr 483	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝐴 ∈ ℂ)
190	140	recnd 10663	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℂ)
191	9	nnne0d 11681	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ≠ 0)
192	189, 190, 172, 191	divassd 11445	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝐴 · 𝑥) / 𝑛) = (𝐴 · (𝑥 / 𝑛)))
193	188, 192	breqtrrd 5086	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))) ≤ ((𝐴 · 𝑥) / 𝑛))
194	143, 144, 11, 146, 193	lemul2ad 11574	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))))) ≤ ((Λ‘𝑛) · ((𝐴 · 𝑥) / 𝑛)))
195	114, 130	absmuld 14808	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))))) = ((abs‘(Λ‘𝑛)) · (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))))))
196	11, 146	absidd 14776	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(Λ‘𝑛)) = (Λ‘𝑛))
197	196	oveq1d 7165	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(Λ‘𝑛)) · (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))))) = ((Λ‘𝑛) · (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))))))
198	195, 197	eqtrd 2856	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))))) = ((Λ‘𝑛) · (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))))))
199	141	recnd 10663	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝐴 · 𝑥) ∈ ℂ)
200	114, 172, 199, 191	div32d 11433	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) / 𝑛) · (𝐴 · 𝑥)) = ((Λ‘𝑛) · ((𝐴 · 𝑥) / 𝑛)))
201	194, 198, 200	3brtr4d 5090	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))))) ≤ (((Λ‘𝑛) / 𝑛) · (𝐴 · 𝑥)))
202	7, 134, 142, 201	fsumle 15148	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (𝐴 · 𝑥)))
203	36	recnd 10663	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ∈ ℂ)
204	23, 203	mulcld 10655	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (𝐴 · 𝑥) ∈ ℂ)
205	114, 172, 191	divcld 11410	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) / 𝑛) ∈ ℂ)
206	7, 204, 205	fsummulc1 15134	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 · 𝑥)) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (𝐴 · 𝑥)))
207	202, 206	breqtrrd 5086	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))))) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 · 𝑥)))
208	133, 135, 137, 138, 207	letrd 10791	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))))) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 · 𝑥)))
209	123	recnd 10663	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) ∈ ℂ)
210	90	recnd 10663	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (ψ‘(𝑥 / 𝑛)) ∈ ℂ)
211	93	recnd 10663	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘𝑛) ∈ ℂ)
212	210, 211	mulcld 10655	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)) ∈ ℂ)
213	209, 212	addcld 10654	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛))) ∈ ℂ)
214	114, 213	mulcld 10655	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))) ∈ ℂ)
215	114, 210	mulcld 10655	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) ∈ ℂ)
216	26	adantr 483	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘𝑥) ∈ ℂ)
217	215, 216	mulcld 10655	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)) ∈ ℂ)
218	7, 214, 217	fsumsub 15137	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))) − (((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))))
219	210, 216	mulcld 10655	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((ψ‘(𝑥 / 𝑛)) · (log‘𝑥)) ∈ ℂ)
220	114, 213, 219	subdid 11090	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛))) − ((ψ‘(𝑥 / 𝑛)) · (log‘𝑥)))) = (((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))) − ((Λ‘𝑛) · ((ψ‘(𝑥 / 𝑛)) · (log‘𝑥)))))
221	43	adantr 483	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ⁺)
222	221, 92	relogdivd 25203	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) = ((log‘𝑥) − (log‘𝑛)))
223	222	oveq2d 7166	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))) = ((ψ‘(𝑥 / 𝑛)) · ((log‘𝑥) − (log‘𝑛))))
224	210, 216, 211	subdid 11090	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((ψ‘(𝑥 / 𝑛)) · ((log‘𝑥) − (log‘𝑛))) = (((ψ‘(𝑥 / 𝑛)) · (log‘𝑥)) − ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛))))
225	223, 224	eqtrd 2856	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))) = (((ψ‘(𝑥 / 𝑛)) · (log‘𝑥)) − ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛))))
226	225	oveq2d 7166	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − (((ψ‘(𝑥 / 𝑛)) · (log‘𝑥)) − ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))))
227	209, 219, 212	subsub3d 11021	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − (((ψ‘(𝑥 / 𝑛)) · (log‘𝑥)) − ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))) = ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛))) − ((ψ‘(𝑥 / 𝑛)) · (log‘𝑥))))
228	226, 227	eqtrd 2856	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))) = ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛))) − ((ψ‘(𝑥 / 𝑛)) · (log‘𝑥))))
229	228	oveq2d 7166	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))) = ((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛))) − ((ψ‘(𝑥 / 𝑛)) · (log‘𝑥)))))
230	114, 210, 216	mulassd 10658	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)) = ((Λ‘𝑛) · ((ψ‘(𝑥 / 𝑛)) · (log‘𝑥))))
231	230	oveq2d 7166	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))) − (((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))) = (((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))) − ((Λ‘𝑛) · ((ψ‘(𝑥 / 𝑛)) · (log‘𝑥)))))
232	220, 229, 231	3eqtr4d 2866	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))) = (((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))) − (((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))))
233	232	sumeq2dv 15054	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))) − (((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))))
234		fveq2 6664	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑚 → (Λ‘𝑛) = (Λ‘𝑚))
235		oveq2 7158	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑚 → (𝑥 / 𝑛) = (𝑥 / 𝑚))
236	235	fveq2d 6668	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑚 → (ψ‘(𝑥 / 𝑛)) = (ψ‘(𝑥 / 𝑚)))
237	234, 236	oveq12d 7168	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑚 → ((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) = ((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚))))
238		fveq2 6664	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑚 → (log‘𝑛) = (log‘𝑚))
239	237, 238	oveq12d 7168	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑚 → (((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛)) = (((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚))) · (log‘𝑚)))
240	239	cbvsumv 15047	. . . . . . . . . . . . . . 15 ⊢ Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛)) = Σ𝑚 ∈ (1...(⌊‘𝑥))(((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚))) · (log‘𝑚))
241		elfznn 12930	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ (1...(⌊‘(𝑥 / 𝑚))) → 𝑛 ∈ ℕ)
242	241	adantl 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑛 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → 𝑛 ∈ ℕ)
243	242, 10	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑛 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → (Λ‘𝑛) ∈ ℝ)
244	243	recnd 10663	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑛 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → (Λ‘𝑛) ∈ ℂ)
245	244	anasss 469	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ (𝑚 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ (1...(⌊‘(𝑥 / 𝑚))))) → (Λ‘𝑛) ∈ ℂ)
246		elfznn 12930	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 ∈ (1...(⌊‘𝑥)) → 𝑚 ∈ ℕ)
247	246	adantl 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → 𝑚 ∈ ℕ)
248	247, 118	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑚) ∈ ℝ)
249	248	recnd 10663	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑚) ∈ ℂ)
250	247	nnrpd 12423	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → 𝑚 ∈ ℝ⁺)
251	250	relogcld 25200	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (log‘𝑚) ∈ ℝ)
252	251	recnd 10663	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (log‘𝑚) ∈ ℂ)
253	249, 252	mulcld 10655	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑚) · (log‘𝑚)) ∈ ℂ)
254	253	adantrr 715	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ (𝑚 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ (1...(⌊‘(𝑥 / 𝑚))))) → ((Λ‘𝑚) · (log‘𝑚)) ∈ ℂ)
255	245, 254	mulcld 10655	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ (𝑚 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ (1...(⌊‘(𝑥 / 𝑚))))) → ((Λ‘𝑛) · ((Λ‘𝑚) · (log‘𝑚))) ∈ ℂ)
256	36, 255	fsumfldivdiag 25761	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑚 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑛) · ((Λ‘𝑚) · (log‘𝑚))) = Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑛) · ((Λ‘𝑚) · (log‘𝑚))))
257	36	adantr 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ)
258	257, 247	nndivred 11685	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑚) ∈ ℝ)
259		chpcl 25695	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 / 𝑚) ∈ ℝ → (ψ‘(𝑥 / 𝑚)) ∈ ℝ)
260	258, 259	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (ψ‘(𝑥 / 𝑚)) ∈ ℝ)
261	260	recnd 10663	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (ψ‘(𝑥 / 𝑚)) ∈ ℂ)
262	249, 261, 252	mul32d 10844	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚))) · (log‘𝑚)) = (((Λ‘𝑚) · (log‘𝑚)) · (ψ‘(𝑥 / 𝑚))))
263	248, 251	remulcld 10665	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑚) · (log‘𝑚)) ∈ ℝ)
264	263	recnd 10663	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑚) · (log‘𝑚)) ∈ ℂ)
265	264, 261	mulcomd 10656	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑚) · (log‘𝑚)) · (ψ‘(𝑥 / 𝑚))) = ((ψ‘(𝑥 / 𝑚)) · ((Λ‘𝑚) · (log‘𝑚))))
266		chpval 25693	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 / 𝑚) ∈ ℝ → (ψ‘(𝑥 / 𝑚)) = Σ𝑛 ∈ (1...(⌊‘(𝑥 / 𝑚)))(Λ‘𝑛))
267	258, 266	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (ψ‘(𝑥 / 𝑚)) = Σ𝑛 ∈ (1...(⌊‘(𝑥 / 𝑚)))(Λ‘𝑛))
268	267	oveq1d 7165	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → ((ψ‘(𝑥 / 𝑚)) · ((Λ‘𝑚) · (log‘𝑚))) = (Σ𝑛 ∈ (1...(⌊‘(𝑥 / 𝑚)))(Λ‘𝑛) · ((Λ‘𝑚) · (log‘𝑚))))
269		fzfid 13335	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (1...(⌊‘(𝑥 / 𝑚))) ∈ Fin)
270	269, 264, 244	fsummulc1 15134	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (Σ𝑛 ∈ (1...(⌊‘(𝑥 / 𝑚)))(Λ‘𝑛) · ((Λ‘𝑚) · (log‘𝑚))) = Σ𝑛 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑛) · ((Λ‘𝑚) · (log‘𝑚))))
271	268, 270	eqtrd 2856	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → ((ψ‘(𝑥 / 𝑚)) · ((Λ‘𝑚) · (log‘𝑚))) = Σ𝑛 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑛) · ((Λ‘𝑚) · (log‘𝑚))))
272	262, 265, 271	3eqtrd 2860	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚))) · (log‘𝑚)) = Σ𝑛 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑛) · ((Λ‘𝑚) · (log‘𝑚))))
273	272	sumeq2dv 15054	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑚 ∈ (1...(⌊‘𝑥))(((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚))) · (log‘𝑚)) = Σ𝑚 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑛) · ((Λ‘𝑚) · (log‘𝑚))))
274	122	recnd 10663	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((Λ‘𝑚) · (log‘𝑚)) ∈ ℂ)
275	115, 114, 274	fsummulc2 15133	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚))) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑛) · ((Λ‘𝑚) · (log‘𝑚))))
276	275	sumeq2dv 15054	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚))) = Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑛) · ((Λ‘𝑚) · (log‘𝑚))))
277	256, 273, 276	3eqtr4d 2866	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑚 ∈ (1...(⌊‘𝑥))(((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚))) · (log‘𝑚)) = Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚))))
278	240, 277	syl5eq 2868	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛)) = Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚))))
279	114, 210, 211	mulassd 10658	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛)) = ((Λ‘𝑛) · ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛))))
280	279	sumeq2dv 15054	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛)) = Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛))))
281	278, 280	oveq12d 7168	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛)) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚))) + Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))))
282	104	2timesd 11874	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛)) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))))
283	114, 209	mulcld 10655	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚))) ∈ ℂ)
284	114, 212	mulcld 10655	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛))) ∈ ℂ)
285	7, 283, 284	fsumadd 15090	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚))) + ((Λ‘𝑛) · ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚))) + Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))))
286	281, 282, 285	3eqtr4d 2866	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚))) + ((Λ‘𝑛) · ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))))
287	114, 209, 212	adddid 10659	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))) = (((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚))) + ((Λ‘𝑛) · ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))))
288	287	sumeq2dv 15054	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚))) + ((Λ‘𝑛) · ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))))
289	286, 288	eqtr4d 2859	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))))
290	91	recnd 10663	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) ∈ ℂ)
291	7, 26, 290	fsummulc1 15134	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))
292	289, 291	oveq12d 7168	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))))
293	218, 233, 292	3eqtr4rd 2867	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))))
294	293	fveq2d 6668	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) = (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))))))
295	24, 23, 203	mulassd 10658	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝐴) · 𝑥) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 · 𝑥)))
296	208, 294, 295	3brtr4d 5090	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) ≤ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝐴) · 𝑥))
297	109, 113, 43	ledivmul2d 12479	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (((abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) / 𝑥) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝐴) ↔ (abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) ≤ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝐴) · 𝑥)))
298	296, 297	mpbird 259	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) / 𝑥) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝐴))
299	111, 113, 25, 298	lediv1dd 12483	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (((abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) / 𝑥) / (log‘𝑥)) ≤ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝐴) / (log‘𝑥)))
300	109	recnd 10663	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) ∈ ℂ)
301	300, 203, 26, 110, 29	divdiv1d 11441	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (((abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) / 𝑥) / (log‘𝑥)) = ((abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) / (𝑥 · (log‘𝑥))))
302	108, 26, 203, 29, 110	divdiv32d 11435	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))) / (log‘𝑥)) / 𝑥) = ((((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))) / 𝑥) / (log‘𝑥)))
303	105, 107, 26, 29	divsubdird 11449	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))) / (log‘𝑥)) = (((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) / (log‘𝑥)) − ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)) / (log‘𝑥))))
304	103, 104, 26, 29	div23d 11447	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) / (log‘𝑥)) = ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))))
305	106, 26, 29	divcan4d 11416	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)) / (log‘𝑥)) = Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))))
306	304, 305	oveq12d 7168	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) / (log‘𝑥)) − ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)) / (log‘𝑥))) = (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))))
307	303, 306	eqtrd 2856	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))) / (log‘𝑥)) = (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))))
308	307	oveq1d 7165	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))) / (log‘𝑥)) / 𝑥) = ((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥))
309	108, 203, 26, 110, 29	divdiv1d 11441	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))) / 𝑥) / (log‘𝑥)) = (((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))) / (𝑥 · (log‘𝑥))))
310	302, 308, 309	3eqtr3d 2864	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥) = (((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))) / (𝑥 · (log‘𝑥))))
311	310	fveq2d 6668	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥)) = (abs‘(((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))) / (𝑥 · (log‘𝑥)))))
312	43, 25	rpmulcld 12441	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ∈ ℝ⁺)
313	312	rpcnd 12427	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ∈ ℂ)
314	312	rpne0d 12430	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ≠ 0)
315	108, 313, 314	absdivd 14809	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘(((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))) / (𝑥 · (log‘𝑥)))) = ((abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) / (abs‘(𝑥 · (log‘𝑥)))))
316	312	rpred 12425	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ∈ ℝ)
317	312	rpge0d 12429	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ (𝑥 · (log‘𝑥)))
318	316, 317	absidd 14776	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘(𝑥 · (log‘𝑥))) = (𝑥 · (log‘𝑥)))
319	318	oveq2d 7166	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) / (abs‘(𝑥 · (log‘𝑥)))) = ((abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) / (𝑥 · (log‘𝑥))))
320	311, 315, 319	3eqtrd 2860	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥)) = ((abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) / (𝑥 · (log‘𝑥))))
321	301, 320	eqtr4d 2859	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (((abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) / 𝑥) / (log‘𝑥)) = (abs‘((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥)))
322	24, 23, 26, 29	divassd 11445	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝐴) / (log‘𝑥)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 / (log‘𝑥))))
323	299, 321, 322	3brtr3d 5089	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥)) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 / (log‘𝑥))))
324	21	leabsd 14768	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 / (log‘𝑥))) ≤ (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 / (log‘𝑥)))))
325	101, 21, 102, 323, 324	letrd 10791	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥)) ≤ (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 / (log‘𝑥)))))
326	325	adantrr 715	. 2 ⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ 1 ≤ 𝑥)) → (abs‘((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥)) ≤ (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 / (log‘𝑥)))))
327	1, 83, 21, 100, 326	o1le 15003	1 ⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥)) ∈ 𝑂(1))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 = wceq 1533 ∈ wcel 2110 ∀wral 3138 ⊆ wss 3935 class class class wbr 5058 ↦ cmpt 5138 ‘cfv 6349 (class class class)co 7150 ℂcc 10529 ℝcr 10530 0cc0 10531 1c1 10532 + caddc 10534 · cmul 10536 +∞cpnf 10666 < clt 10669 ≤ cle 10670 − cmin 10864 / cdiv 11291 ℕcn 11632 2c2 11686 ℝ⁺crp 12383 (,)cioo 12732 [,)cico 12734 ...cfz 12886 ⌊cfl 13154 abscabs 14587 𝑂(1)co1 14837 Σcsu 15036 eceu 15410 logclog 25132 Λcvma 25663 ψcchp 25664

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 ax-rep 5182 ax-sep 5195 ax-nul 5202 ax-pow 5258 ax-pr 5321 ax-un 7455 ax-inf2 9098 ax-cnex 10587 ax-resscn 10588 ax-1cn 10589 ax-icn 10590 ax-addcl 10591 ax-addrcl 10592 ax-mulcl 10593 ax-mulrcl 10594 ax-mulcom 10595 ax-addass 10596 ax-mulass 10597 ax-distr 10598 ax-i2m1 10599 ax-1ne0 10600 ax-1rid 10601 ax-rnegex 10602 ax-rrecex 10603 ax-cnre 10604 ax-pre-lttri 10605 ax-pre-lttrn 10606 ax-pre-ltadd 10607 ax-pre-mulgt0 10608 ax-pre-sup 10609 ax-addf 10610 ax-mulf 10611

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1536 df-fal 1546 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rmo 3146 df-rab 3147 df-v 3496 df-sbc 3772 df-csb 3883 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-pss 3953 df-nul 4291 df-if 4467 df-pw 4540 df-sn 4561 df-pr 4563 df-tp 4565 df-op 4567 df-uni 4832 df-int 4869 df-iun 4913 df-iin 4914 df-br 5059 df-opab 5121 df-mpt 5139 df-tr 5165 df-id 5454 df-eprel 5459 df-po 5468 df-so 5469 df-fr 5508 df-se 5509 df-we 5510 df-xp 5555 df-rel 5556 df-cnv 5557 df-co 5558 df-dm 5559 df-rn 5560 df-res 5561 df-ima 5562 df-pred 6142 df-ord 6188 df-on 6189 df-lim 6190 df-suc 6191 df-iota 6308 df-fun 6351 df-fn 6352 df-f 6353 df-f1 6354 df-fo 6355 df-f1o 6356 df-fv 6357 df-isom 6358 df-riota 7108 df-ov 7153 df-oprab 7154 df-mpo 7155 df-of 7403 df-om 7575 df-1st 7683 df-2nd 7684 df-supp 7825 df-wrecs 7941 df-recs 8002 df-rdg 8040 df-1o 8096 df-2o 8097 df-oadd 8100 df-er 8283 df-map 8402 df-pm 8403 df-ixp 8456 df-en 8504 df-dom 8505 df-sdom 8506 df-fin 8507 df-fsupp 8828 df-fi 8869 df-sup 8900 df-inf 8901 df-oi 8968 df-dju 9324 df-card 9362 df-pnf 10671 df-mnf 10672 df-xr 10673 df-ltxr 10674 df-le 10675 df-sub 10866 df-neg 10867 df-div 11292 df-nn 11633 df-2 11694 df-3 11695 df-4 11696 df-5 11697 df-6 11698 df-7 11699 df-8 11700 df-9 11701 df-n0 11892 df-xnn0 11962 df-z 11976 df-dec 12093 df-uz 12238 df-q 12343 df-rp 12384 df-xneg 12501 df-xadd 12502 df-xmul 12503 df-ioo 12736 df-ioc 12737 df-ico 12738 df-icc 12739 df-fz 12887 df-fzo 13028 df-fl 13156 df-mod 13232 df-seq 13364 df-exp 13424 df-fac 13628 df-bc 13657 df-hash 13685 df-shft 14420 df-cj 14452 df-re 14453 df-im 14454 df-sqrt 14588 df-abs 14589 df-limsup 14822 df-clim 14839 df-rlim 14840 df-o1 14841 df-lo1 14842 df-sum 15037 df-ef 15415 df-e 15416 df-sin 15417 df-cos 15418 df-pi 15420 df-dvds 15602 df-gcd 15838 df-prm 16010 df-pc 16168 df-struct 16479 df-ndx 16480 df-slot 16481 df-base 16483 df-sets 16484 df-ress 16485 df-plusg 16572 df-mulr 16573 df-starv 16574 df-sca 16575 df-vsca 16576 df-ip 16577 df-tset 16578 df-ple 16579 df-ds 16581 df-unif 16582 df-hom 16583 df-cco 16584 df-rest 16690 df-topn 16691 df-0g 16709 df-gsum 16710 df-topgen 16711 df-pt 16712 df-prds 16715 df-xrs 16769 df-qtop 16774 df-imas 16775 df-xps 16777 df-mre 16851 df-mrc 16852 df-acs 16854 df-mgm 17846 df-sgrp 17895 df-mnd 17906 df-submnd 17951 df-mulg 18219 df-cntz 18441 df-cmn 18902 df-psmet 20531 df-xmet 20532 df-met 20533 df-bl 20534 df-mopn 20535 df-fbas 20536 df-fg 20537 df-cnfld 20540 df-top 21496 df-topon 21513 df-topsp 21535 df-bases 21548 df-cld 21621 df-ntr 21622 df-cls 21623 df-nei 21700 df-lp 21738 df-perf 21739 df-cn 21829 df-cnp 21830 df-haus 21917 df-cmp 21989 df-tx 22164 df-hmeo 22357 df-fil 22448 df-fm 22540 df-flim 22541 df-flf 22542 df-xms 22924 df-ms 22925 df-tms 22926 df-cncf 23480 df-limc 24458 df-dv 24459 df-log 25134 df-cxp 25135 df-cht 25668 df-vma 25669 df-chp 25670 df-ppi 25671

This theorem is referenced by: selberg3lem2 26128

W3C validator