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 25815

Description: Introduce a log weighting on the summands of Σ𝑚 · 𝑛 ≤ 𝑥, Λ(𝑚)Λ(𝑛), the core of selberg2 25809 (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 10488	. 2 ⊢ (𝜑 → 1 ∈ ℝ)
2		ioossre 12648	. . . 4 ⊢ (1(,)+∞) ⊆ ℝ
3		selberg3lem1.1	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ ℝ⁺)
4	3	rpcnd 12283	. . . 4 ⊢ (𝜑 → 𝐴 ∈ ℂ)
5		o1const 14810	. . . 4 ⊢ (((1(,)+∞) ⊆ ℝ ∧ 𝐴 ∈ ℂ) → (𝑥 ∈ (1(,)+∞) ↦ 𝐴) ∈ 𝑂(1))
6	2, 4, 5	sylancr 587	. . 3 ⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ 𝐴) ∈ 𝑂(1))
7		fzfid 13191	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (1...(⌊‘𝑥)) ∈ Fin)
8		elfznn 12786	. . . . . . . . . 10 ⊢ (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
9	8	adantl 482	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
10		vmacl 25377	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ → (Λ‘𝑛) ∈ ℝ)
11	9, 10	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈ ℝ)
12	11, 9	nndivred 11539	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) / 𝑛) ∈ ℝ)
13	7, 12	fsumrecl 14924	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ∈ ℝ)
14		elioore 12618	. . . . . . . . 9 ⊢ (𝑥 ∈ (1(,)+∞) → 𝑥 ∈ ℝ)
15		eliooord 12646	. . . . . . . . . 10 ⊢ (𝑥 ∈ (1(,)+∞) → (1 < 𝑥 ∧ 𝑥 < +∞))
16	15	simpld 495	. . . . . . . . 9 ⊢ (𝑥 ∈ (1(,)+∞) → 1 < 𝑥)
17	14, 16	rplogcld 24893	. . . . . . . 8 ⊢ (𝑥 ∈ (1(,)+∞) → (log‘𝑥) ∈ ℝ⁺)
18		rpdivcl 12264	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ⁺ ∧ (log‘𝑥) ∈ ℝ⁺) → (𝐴 / (log‘𝑥)) ∈ ℝ⁺)
19	3, 17, 18	syl2an 595	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (𝐴 / (log‘𝑥)) ∈ ℝ⁺)
20	19	rpred 12281	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (𝐴 / (log‘𝑥)) ∈ ℝ)
21	13, 20	remulcld 10517	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 / (log‘𝑥))) ∈ ℝ)
22	21	recnd 10515	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 / (log‘𝑥))) ∈ ℂ)
23	4	adantr 481	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 𝐴 ∈ ℂ)
24	13	recnd 10515	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ∈ ℂ)
25	17	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ∈ ℝ⁺)
26	25	rpcnd 12283	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ∈ ℂ)
27	19	rpcnd 12283	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (𝐴 / (log‘𝑥)) ∈ ℂ)
28	24, 26, 27	subdird 10945	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) · (𝐴 / (log‘𝑥))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 / (log‘𝑥))) − ((log‘𝑥) · (𝐴 / (log‘𝑥)))))
29	25	rpne0d 12286	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ≠ 0)
30	23, 26, 29	divcan2d 11266	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((log‘𝑥) · (𝐴 / (log‘𝑥))) = 𝐴)
31	30	oveq2d 7032	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 / (log‘𝑥))) − ((log‘𝑥) · (𝐴 / (log‘𝑥)))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 / (log‘𝑥))) − 𝐴))
32	28, 31	eqtrd 2831	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) · (𝐴 / (log‘𝑥))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 / (log‘𝑥))) − 𝐴))
33	32	mpteq2dva 5055	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) · (𝐴 / (log‘𝑥)))) = (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 / (log‘𝑥))) − 𝐴)))
34	25	rpred 12281	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ∈ ℝ)
35	13, 34	resubcld 10916	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) ∈ ℝ)
36	14	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ∈ ℝ)
37		0red 10490	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 0 ∈ ℝ)
38		1red 10488	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 1 ∈ ℝ)
39		0lt1 11010	. . . . . . . . . . . 12 ⊢ 0 < 1
40	39	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 0 < 1)
41	16	adantl 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 1 < 𝑥)
42	37, 38, 36, 40, 41	lttrd 10648	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 0 < 𝑥)
43	36, 42	elrpd 12278	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ∈ ℝ⁺)
44	43	ex 413	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) → 𝑥 ∈ ℝ⁺))
45	44	ssrdv 3895	. . . . . . 7 ⊢ (𝜑 → (1(,)+∞) ⊆ ℝ⁺)
46		vmadivsum 25740	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1)
47	46	a1i 11	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ ℝ⁺ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1))
48	45, 47	o1res2 14754	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1))
49	2	a1i 11	. . . . . . 7 ⊢ (𝜑 → (1(,)+∞) ⊆ ℝ)
50		ere 15275	. . . . . . . 8 ⊢ e ∈ ℝ
51	50	a1i 11	. . . . . . 7 ⊢ (𝜑 → e ∈ ℝ)
52	3	rpred 12281	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℝ)
53	19	adantrr 713	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → (𝐴 / (log‘𝑥)) ∈ ℝ⁺)
54	53	rprege0d 12288	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → ((𝐴 / (log‘𝑥)) ∈ ℝ ∧ 0 ≤ (𝐴 / (log‘𝑥))))
55		absid 14490	. . . . . . . . 9 ⊢ (((𝐴 / (log‘𝑥)) ∈ ℝ ∧ 0 ≤ (𝐴 / (log‘𝑥))) → (abs‘(𝐴 / (log‘𝑥))) = (𝐴 / (log‘𝑥)))
56	54, 55	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → (abs‘(𝐴 / (log‘𝑥))) = (𝐴 / (log‘𝑥)))
57		loge 24851	. . . . . . . . . . 11 ⊢ (log‘e) = 1
58		simprr 769	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → e ≤ 𝑥)
59		epr 15394	. . . . . . . . . . . . 13 ⊢ e ∈ ℝ⁺
60	43	adantrr 713	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → 𝑥 ∈ ℝ⁺)
61		logleb 24867	. . . . . . . . . . . . 13 ⊢ ((e ∈ ℝ⁺ ∧ 𝑥 ∈ ℝ⁺) → (e ≤ 𝑥 ↔ (log‘e) ≤ (log‘𝑥)))
62	59, 60, 61	sylancr 587	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → (e ≤ 𝑥 ↔ (log‘e) ≤ (log‘𝑥)))
63	58, 62	mpbid 233	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → (log‘e) ≤ (log‘𝑥))
64	57, 63	eqbrtrrid 4998	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → 1 ≤ (log‘𝑥))
65		1rp 12243	. . . . . . . . . . . 12 ⊢ 1 ∈ ℝ⁺
66		rpregt0 12253	. . . . . . . . . . . 12 ⊢ (1 ∈ ℝ⁺ → (1 ∈ ℝ ∧ 0 < 1))
67	65, 66	mp1i 13	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → (1 ∈ ℝ ∧ 0 < 1))
68	25	adantrr 713	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → (log‘𝑥) ∈ ℝ⁺)
69	68	rpregt0d 12287	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → ((log‘𝑥) ∈ ℝ ∧ 0 < (log‘𝑥)))
70	3	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → 𝐴 ∈ ℝ⁺)
71	70	rpregt0d 12287	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → (𝐴 ∈ ℝ ∧ 0 < 𝐴))
72		lediv2 11378	. . . . . . . . . . 11 ⊢ (((1 ∈ ℝ ∧ 0 < 1) ∧ ((log‘𝑥) ∈ ℝ ∧ 0 < (log‘𝑥)) ∧ (𝐴 ∈ ℝ ∧ 0 < 𝐴)) → (1 ≤ (log‘𝑥) ↔ (𝐴 / (log‘𝑥)) ≤ (𝐴 / 1)))
73	67, 69, 71, 72	syl3anc 1364	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → (1 ≤ (log‘𝑥) ↔ (𝐴 / (log‘𝑥)) ≤ (𝐴 / 1)))
74	64, 73	mpbid 233	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → (𝐴 / (log‘𝑥)) ≤ (𝐴 / 1))
75	4	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → 𝐴 ∈ ℂ)
76	75	div1d 11256	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → (𝐴 / 1) = 𝐴)
77	74, 76	breqtrd 4988	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → (𝐴 / (log‘𝑥)) ≤ 𝐴)
78	56, 77	eqbrtrd 4984	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → (abs‘(𝐴 / (log‘𝑥))) ≤ 𝐴)
79	49, 27, 51, 52, 78	elo1d 14727	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (𝐴 / (log‘𝑥))) ∈ 𝑂(1))
80	35, 20, 48, 79	o1mul2 14815	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) · (𝐴 / (log‘𝑥)))) ∈ 𝑂(1))
81	33, 80	eqeltrrd 2884	. . . 4 ⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 / (log‘𝑥))) − 𝐴)) ∈ 𝑂(1))
82	22, 23, 81	o1dif 14820	. . 3 ⊢ (𝜑 → ((𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 / (log‘𝑥)))) ∈ 𝑂(1) ↔ (𝑥 ∈ (1(,)+∞) ↦ 𝐴) ∈ 𝑂(1)))
83	6, 82	mpbird 258	. 2 ⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 / (log‘𝑥)))) ∈ 𝑂(1))
84		2re 11559	. . . . . . 7 ⊢ 2 ∈ ℝ
85		rerpdivcl 12269	. . . . . . 7 ⊢ ((2 ∈ ℝ ∧ (log‘𝑥) ∈ ℝ⁺) → (2 / (log‘𝑥)) ∈ ℝ)
86	84, 25, 85	sylancr 587	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (2 / (log‘𝑥)) ∈ ℝ)
87		nndivre 11526	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℕ) → (𝑥 / 𝑛) ∈ ℝ)
88	36, 8, 87	syl2an 595	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ)
89		chpcl 25383	. . . . . . . . . 10 ⊢ ((𝑥 / 𝑛) ∈ ℝ → (ψ‘(𝑥 / 𝑛)) ∈ ℝ)
90	88, 89	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (ψ‘(𝑥 / 𝑛)) ∈ ℝ)
91	11, 90	remulcld 10517	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) ∈ ℝ)
92	9	nnrpd 12279	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ⁺)
93	92	relogcld 24887	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘𝑛) ∈ ℝ)
94	91, 93	remulcld 10517	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛)) ∈ ℝ)
95	7, 94	fsumrecl 14924	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛)) ∈ ℝ)
96	86, 95	remulcld 10517	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) ∈ ℝ)
97	7, 91	fsumrecl 14924	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) ∈ ℝ)
98	96, 97	resubcld 10916	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) ∈ ℝ)
99	98, 43	rerpdivcld 12312	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥) ∈ ℝ)
100	99	recnd 10515	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥) ∈ ℂ)
101	100	abscld 14630	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥)) ∈ ℝ)
102	22	abscld 14630	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 / (log‘𝑥)))) ∈ ℝ)
103		2cnd 11563	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 2 ∈ ℂ)
104	95	recnd 10515	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛)) ∈ ℂ)
105	103, 104	mulcld 10507	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) ∈ ℂ)
106	97	recnd 10515	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) ∈ ℂ)
107	106, 26	mulcld 10507	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)) ∈ ℂ)
108	105, 107	subcld 10845	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))) ∈ ℂ)
109	108	abscld 14630	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) ∈ ℝ)
110	42	gt0ne0d 11052	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ≠ 0)
111	109, 36, 110	redivcld 11316	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) / 𝑥) ∈ ℝ)
112	52	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 𝐴 ∈ ℝ)
113	13, 112	remulcld 10517	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝐴) ∈ ℝ)
114	11	recnd 10515	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈ ℂ)
115		fzfid 13191	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1...(⌊‘(𝑥 / 𝑛))) ∈ Fin)
116		elfznn 12786	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛))) → 𝑚 ∈ ℕ)
117	116	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ∈ ℕ)
118		vmacl 25377	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 ∈ ℕ → (Λ‘𝑚) ∈ ℝ)
119	117, 118	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (Λ‘𝑚) ∈ ℝ)
120	117	nnrpd 12279	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ∈ ℝ⁺)
121	120	relogcld 24887	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (log‘𝑚) ∈ ℝ)
122	119, 121	remulcld 10517	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((Λ‘𝑚) · (log‘𝑚)) ∈ ℝ)
123	115, 122	fsumrecl 14924	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) ∈ ℝ)
124	8	nnrpd 12279	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℝ⁺)
125		rpdivcl 12264	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑛 ∈ ℝ⁺) → (𝑥 / 𝑛) ∈ ℝ⁺)
126	43, 124, 125	syl2an 595	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ⁺)
127	126	relogcld 24887	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ∈ ℝ)
128	90, 127	remulcld 10517	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))) ∈ ℝ)
129	123, 128	resubcld 10916	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))) ∈ ℝ)
130	129	recnd 10515	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))) ∈ ℂ)
131	114, 130	mulcld 10507	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))) ∈ ℂ)
132	7, 131	fsumcl 14923	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))) ∈ ℂ)
133	132	abscld 14630	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))))) ∈ ℝ)
134	131	abscld 14630	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))))) ∈ ℝ)
135	7, 134	fsumrecl 14924	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))))) ∈ ℝ)
136	112, 36	remulcld 10517	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (𝐴 · 𝑥) ∈ ℝ)
137	13, 136	remulcld 10517	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 · 𝑥)) ∈ ℝ)
138	7, 131	fsumabs 14989	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))))))
139	52	ad2antrr 722	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝐴 ∈ ℝ)
140	36	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ)
141	139, 140	remulcld 10517	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝐴 · 𝑥) ∈ ℝ)
142	12, 141	remulcld 10517	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) / 𝑛) · (𝐴 · 𝑥)) ∈ ℝ)
143	130	abscld 14630	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))) ∈ ℝ)
144	141, 9	nndivred 11539	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝐴 · 𝑥) / 𝑛) ∈ ℝ)
145		vmage0 25380	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → 0 ≤ (Λ‘𝑛))
146	9, 145	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (Λ‘𝑛))
147	88	recnd 10515	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℂ)
148	126	rpne0d 12286	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ≠ 0)
149	130, 147, 148	absdivd 14649	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))) / (𝑥 / 𝑛))) = ((abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))) / (abs‘(𝑥 / 𝑛))))
150	126	rpge0d 12285	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (𝑥 / 𝑛))
151	88, 150	absidd 14616	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑥 / 𝑛)) = (𝑥 / 𝑛))
152	151	oveq2d 7032	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))) / (abs‘(𝑥 / 𝑛))) = ((abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))) / (𝑥 / 𝑛)))
153	149, 152	eqtrd 2831	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))) / (𝑥 / 𝑛))) = ((abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))) / (𝑥 / 𝑛)))
154		fveq2 6538	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = 𝑚 → (Λ‘𝑘) = (Λ‘𝑚))
155		fveq2 6538	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = 𝑚 → (log‘𝑘) = (log‘𝑚))
156	154, 155	oveq12d 7034	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = 𝑚 → ((Λ‘𝑘) · (log‘𝑘)) = ((Λ‘𝑚) · (log‘𝑚)))
157	156	cbvsumv 14886	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Σ𝑘 ∈ (1...(⌊‘𝑦))((Λ‘𝑘) · (log‘𝑘)) = Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚))
158		fveq2 6538	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = (𝑥 / 𝑛) → (⌊‘𝑦) = (⌊‘(𝑥 / 𝑛)))
159	158	oveq2d 7032	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = (𝑥 / 𝑛) → (1...(⌊‘𝑦)) = (1...(⌊‘(𝑥 / 𝑛))))
160	159	sumeq1d 14891	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = (𝑥 / 𝑛) → Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)))
161	157, 160	syl5eq 2843	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = (𝑥 / 𝑛) → Σ𝑘 ∈ (1...(⌊‘𝑦))((Λ‘𝑘) · (log‘𝑘)) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)))
162		fveq2 6538	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = (𝑥 / 𝑛) → (ψ‘𝑦) = (ψ‘(𝑥 / 𝑛)))
163		fveq2 6538	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = (𝑥 / 𝑛) → (log‘𝑦) = (log‘(𝑥 / 𝑛)))
164	162, 163	oveq12d 7034	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = (𝑥 / 𝑛) → ((ψ‘𝑦) · (log‘𝑦)) = ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))
165	161, 164	oveq12d 7034	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (𝑥 / 𝑛) → (Σ𝑘 ∈ (1...(⌊‘𝑦))((Λ‘𝑘) · (log‘𝑘)) − ((ψ‘𝑦) · (log‘𝑦))) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))))
166		id 22	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (𝑥 / 𝑛) → 𝑦 = (𝑥 / 𝑛))
167	165, 166	oveq12d 7034	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (𝑥 / 𝑛) → ((Σ𝑘 ∈ (1...(⌊‘𝑦))((Λ‘𝑘) · (log‘𝑘)) − ((ψ‘𝑦) · (log‘𝑦))) / 𝑦) = ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))) / (𝑥 / 𝑛)))
168	167	fveq2d 6542	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = (𝑥 / 𝑛) → (abs‘((Σ𝑘 ∈ (1...(⌊‘𝑦))((Λ‘𝑘) · (log‘𝑘)) − ((ψ‘𝑦) · (log‘𝑦))) / 𝑦)) = (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))) / (𝑥 / 𝑛))))
169	168	breq1d 4972	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (𝑥 / 𝑛) → ((abs‘((Σ𝑘 ∈ (1...(⌊‘𝑦))((Λ‘𝑘) · (log‘𝑘)) − ((ψ‘𝑦) · (log‘𝑦))) / 𝑦)) ≤ 𝐴 ↔ (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))) / (𝑥 / 𝑛))) ≤ 𝐴))
170		selberg3lem1.2	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((Σ𝑘 ∈ (1...(⌊‘𝑦))((Λ‘𝑘) · (log‘𝑘)) − ((ψ‘𝑦) · (log‘𝑦))) / 𝑦)) ≤ 𝐴)
171	170	ad2antrr 722	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ∀𝑦 ∈ (1[,)+∞)(abs‘((Σ𝑘 ∈ (1...(⌊‘𝑦))((Λ‘𝑘) · (log‘𝑘)) − ((ψ‘𝑦) · (log‘𝑦))) / 𝑦)) ≤ 𝐴)
172	9	nncnd 11502	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℂ)
173	172	mulid2d 10505	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 · 𝑛) = 𝑛)
174		fznnfl 13080	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℝ → (𝑛 ∈ (1...(⌊‘𝑥)) ↔ (𝑛 ∈ ℕ ∧ 𝑛 ≤ 𝑥)))
175	36, 174	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (𝑛 ∈ (1...(⌊‘𝑥)) ↔ (𝑛 ∈ ℕ ∧ 𝑛 ≤ 𝑥)))
176	175	simplbda 500	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ≤ 𝑥)
177	173, 176	eqbrtrd 4984	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 · 𝑛) ≤ 𝑥)
178		1red 10488	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℝ)
179	178, 140, 92	lemuldivd 12330	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 · 𝑛) ≤ 𝑥 ↔ 1 ≤ (𝑥 / 𝑛)))
180	177, 179	mpbid 233	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ≤ (𝑥 / 𝑛))
181		1re 10487	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℝ
182		elicopnf 12683	. . . . . . . . . . . . . . . . . . 19 ⊢ (1 ∈ ℝ → ((𝑥 / 𝑛) ∈ (1[,)+∞) ↔ ((𝑥 / 𝑛) ∈ ℝ ∧ 1 ≤ (𝑥 / 𝑛))))
183	181, 182	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 / 𝑛) ∈ (1[,)+∞) ↔ ((𝑥 / 𝑛) ∈ ℝ ∧ 1 ≤ (𝑥 / 𝑛)))
184	88, 180, 183	sylanbrc 583	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ (1[,)+∞))
185	169, 171, 184	rspcdva 3565	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))) / (𝑥 / 𝑛))) ≤ 𝐴)
186	153, 185	eqbrtrrd 4986	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))) / (𝑥 / 𝑛)) ≤ 𝐴)
187	143, 139, 126	ledivmul2d 12335	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))) / (𝑥 / 𝑛)) ≤ 𝐴 ↔ (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))) ≤ (𝐴 · (𝑥 / 𝑛))))
188	186, 187	mpbid 233	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))) ≤ (𝐴 · (𝑥 / 𝑛)))
189	23	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝐴 ∈ ℂ)
190	140	recnd 10515	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℂ)
191	9	nnne0d 11535	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ≠ 0)
192	189, 190, 172, 191	divassd 11299	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝐴 · 𝑥) / 𝑛) = (𝐴 · (𝑥 / 𝑛)))
193	188, 192	breqtrrd 4990	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))) ≤ ((𝐴 · 𝑥) / 𝑛))
194	143, 144, 11, 146, 193	lemul2ad 11428	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))))) ≤ ((Λ‘𝑛) · ((𝐴 · 𝑥) / 𝑛)))
195	114, 130	absmuld 14648	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))))) = ((abs‘(Λ‘𝑛)) · (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))))))
196	11, 146	absidd 14616	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(Λ‘𝑛)) = (Λ‘𝑛))
197	196	oveq1d 7031	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(Λ‘𝑛)) · (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))))) = ((Λ‘𝑛) · (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))))))
198	195, 197	eqtrd 2831	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))))) = ((Λ‘𝑛) · (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))))))
199	141	recnd 10515	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝐴 · 𝑥) ∈ ℂ)
200	114, 172, 199, 191	div32d 11287	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) / 𝑛) · (𝐴 · 𝑥)) = ((Λ‘𝑛) · ((𝐴 · 𝑥) / 𝑛)))
201	194, 198, 200	3brtr4d 4994	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))))) ≤ (((Λ‘𝑛) / 𝑛) · (𝐴 · 𝑥)))
202	7, 134, 142, 201	fsumle 14987	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (𝐴 · 𝑥)))
203	36	recnd 10515	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ∈ ℂ)
204	23, 203	mulcld 10507	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (𝐴 · 𝑥) ∈ ℂ)
205	114, 172, 191	divcld 11264	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) / 𝑛) ∈ ℂ)
206	7, 204, 205	fsummulc1 14973	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 · 𝑥)) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (𝐴 · 𝑥)))
207	202, 206	breqtrrd 4990	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))))) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 · 𝑥)))
208	133, 135, 137, 138, 207	letrd 10644	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))))) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 · 𝑥)))
209	123	recnd 10515	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) ∈ ℂ)
210	90	recnd 10515	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (ψ‘(𝑥 / 𝑛)) ∈ ℂ)
211	93	recnd 10515	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘𝑛) ∈ ℂ)
212	210, 211	mulcld 10507	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)) ∈ ℂ)
213	209, 212	addcld 10506	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛))) ∈ ℂ)
214	114, 213	mulcld 10507	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))) ∈ ℂ)
215	114, 210	mulcld 10507	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) ∈ ℂ)
216	26	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘𝑥) ∈ ℂ)
217	215, 216	mulcld 10507	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)) ∈ ℂ)
218	7, 214, 217	fsumsub 14976	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))) − (((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))))
219	210, 216	mulcld 10507	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((ψ‘(𝑥 / 𝑛)) · (log‘𝑥)) ∈ ℂ)
220	114, 213, 219	subdid 10944	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛))) − ((ψ‘(𝑥 / 𝑛)) · (log‘𝑥)))) = (((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))) − ((Λ‘𝑛) · ((ψ‘(𝑥 / 𝑛)) · (log‘𝑥)))))
221	43	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ⁺)
222	221, 92	relogdivd 24890	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) = ((log‘𝑥) − (log‘𝑛)))
223	222	oveq2d 7032	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))) = ((ψ‘(𝑥 / 𝑛)) · ((log‘𝑥) − (log‘𝑛))))
224	210, 216, 211	subdid 10944	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((ψ‘(𝑥 / 𝑛)) · ((log‘𝑥) − (log‘𝑛))) = (((ψ‘(𝑥 / 𝑛)) · (log‘𝑥)) − ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛))))
225	223, 224	eqtrd 2831	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))) = (((ψ‘(𝑥 / 𝑛)) · (log‘𝑥)) − ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛))))
226	225	oveq2d 7032	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − (((ψ‘(𝑥 / 𝑛)) · (log‘𝑥)) − ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))))
227	209, 219, 212	subsub3d 10875	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − (((ψ‘(𝑥 / 𝑛)) · (log‘𝑥)) − ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))) = ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛))) − ((ψ‘(𝑥 / 𝑛)) · (log‘𝑥))))
228	226, 227	eqtrd 2831	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))) = ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛))) − ((ψ‘(𝑥 / 𝑛)) · (log‘𝑥))))
229	228	oveq2d 7032	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))) = ((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛))) − ((ψ‘(𝑥 / 𝑛)) · (log‘𝑥)))))
230	114, 210, 216	mulassd 10510	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)) = ((Λ‘𝑛) · ((ψ‘(𝑥 / 𝑛)) · (log‘𝑥))))
231	230	oveq2d 7032	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))) − (((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))) = (((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))) − ((Λ‘𝑛) · ((ψ‘(𝑥 / 𝑛)) · (log‘𝑥)))))
232	220, 229, 231	3eqtr4d 2841	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))) = (((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))) − (((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))))
233	232	sumeq2dv 14893	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))) − (((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))))
234		fveq2 6538	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑚 → (Λ‘𝑛) = (Λ‘𝑚))
235		oveq2 7024	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑚 → (𝑥 / 𝑛) = (𝑥 / 𝑚))
236	235	fveq2d 6542	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑚 → (ψ‘(𝑥 / 𝑛)) = (ψ‘(𝑥 / 𝑚)))
237	234, 236	oveq12d 7034	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑚 → ((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) = ((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚))))
238		fveq2 6538	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑚 → (log‘𝑛) = (log‘𝑚))
239	237, 238	oveq12d 7034	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑚 → (((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛)) = (((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚))) · (log‘𝑚)))
240	239	cbvsumv 14886	. . . . . . . . . . . . . . 15 ⊢ Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛)) = Σ𝑚 ∈ (1...(⌊‘𝑥))(((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚))) · (log‘𝑚))
241		elfznn 12786	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ (1...(⌊‘(𝑥 / 𝑚))) → 𝑛 ∈ ℕ)
242	241	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑛 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → 𝑛 ∈ ℕ)
243	242, 10	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑛 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → (Λ‘𝑛) ∈ ℝ)
244	243	recnd 10515	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑛 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → (Λ‘𝑛) ∈ ℂ)
245	244	anasss 467	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ (𝑚 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ (1...(⌊‘(𝑥 / 𝑚))))) → (Λ‘𝑛) ∈ ℂ)
246		elfznn 12786	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑚 ∈ (1...(⌊‘𝑥)) → 𝑚 ∈ ℕ)
247	246	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → 𝑚 ∈ ℕ)
248	247, 118	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑚) ∈ ℝ)
249	248	recnd 10515	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑚) ∈ ℂ)
250	247	nnrpd 12279	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → 𝑚 ∈ ℝ⁺)
251	250	relogcld 24887	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (log‘𝑚) ∈ ℝ)
252	251	recnd 10515	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (log‘𝑚) ∈ ℂ)
253	249, 252	mulcld 10507	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑚) · (log‘𝑚)) ∈ ℂ)
254	253	adantrr 713	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ (𝑚 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ (1...(⌊‘(𝑥 / 𝑚))))) → ((Λ‘𝑚) · (log‘𝑚)) ∈ ℂ)
255	245, 254	mulcld 10507	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ (𝑚 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ (1...(⌊‘(𝑥 / 𝑚))))) → ((Λ‘𝑛) · ((Λ‘𝑚) · (log‘𝑚))) ∈ ℂ)
256	36, 255	fsumfldivdiag 25449	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑚 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑛) · ((Λ‘𝑚) · (log‘𝑚))) = Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑛) · ((Λ‘𝑚) · (log‘𝑚))))
257	36	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ)
258	257, 247	nndivred 11539	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑚) ∈ ℝ)
259		chpcl 25383	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 / 𝑚) ∈ ℝ → (ψ‘(𝑥 / 𝑚)) ∈ ℝ)
260	258, 259	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (ψ‘(𝑥 / 𝑚)) ∈ ℝ)
261	260	recnd 10515	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (ψ‘(𝑥 / 𝑚)) ∈ ℂ)
262	249, 261, 252	mul32d 10697	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚))) · (log‘𝑚)) = (((Λ‘𝑚) · (log‘𝑚)) · (ψ‘(𝑥 / 𝑚))))
263	248, 251	remulcld 10517	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑚) · (log‘𝑚)) ∈ ℝ)
264	263	recnd 10515	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑚) · (log‘𝑚)) ∈ ℂ)
265	264, 261	mulcomd 10508	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑚) · (log‘𝑚)) · (ψ‘(𝑥 / 𝑚))) = ((ψ‘(𝑥 / 𝑚)) · ((Λ‘𝑚) · (log‘𝑚))))
266		chpval 25381	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 / 𝑚) ∈ ℝ → (ψ‘(𝑥 / 𝑚)) = Σ𝑛 ∈ (1...(⌊‘(𝑥 / 𝑚)))(Λ‘𝑛))
267	258, 266	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (ψ‘(𝑥 / 𝑚)) = Σ𝑛 ∈ (1...(⌊‘(𝑥 / 𝑚)))(Λ‘𝑛))
268	267	oveq1d 7031	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → ((ψ‘(𝑥 / 𝑚)) · ((Λ‘𝑚) · (log‘𝑚))) = (Σ𝑛 ∈ (1...(⌊‘(𝑥 / 𝑚)))(Λ‘𝑛) · ((Λ‘𝑚) · (log‘𝑚))))
269		fzfid 13191	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (1...(⌊‘(𝑥 / 𝑚))) ∈ Fin)
270	269, 264, 244	fsummulc1 14973	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (Σ𝑛 ∈ (1...(⌊‘(𝑥 / 𝑚)))(Λ‘𝑛) · ((Λ‘𝑚) · (log‘𝑚))) = Σ𝑛 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑛) · ((Λ‘𝑚) · (log‘𝑚))))
271	268, 270	eqtrd 2831	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → ((ψ‘(𝑥 / 𝑚)) · ((Λ‘𝑚) · (log‘𝑚))) = Σ𝑛 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑛) · ((Λ‘𝑚) · (log‘𝑚))))
272	262, 265, 271	3eqtrd 2835	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚))) · (log‘𝑚)) = Σ𝑛 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑛) · ((Λ‘𝑚) · (log‘𝑚))))
273	272	sumeq2dv 14893	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑚 ∈ (1...(⌊‘𝑥))(((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚))) · (log‘𝑚)) = Σ𝑚 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑛) · ((Λ‘𝑚) · (log‘𝑚))))
274	122	recnd 10515	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((Λ‘𝑚) · (log‘𝑚)) ∈ ℂ)
275	115, 114, 274	fsummulc2 14972	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚))) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑛) · ((Λ‘𝑚) · (log‘𝑚))))
276	275	sumeq2dv 14893	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚))) = Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑛) · ((Λ‘𝑚) · (log‘𝑚))))
277	256, 273, 276	3eqtr4d 2841	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑚 ∈ (1...(⌊‘𝑥))(((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚))) · (log‘𝑚)) = Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚))))
278	240, 277	syl5eq 2843	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛)) = Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚))))
279	114, 210, 211	mulassd 10510	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛)) = ((Λ‘𝑛) · ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛))))
280	279	sumeq2dv 14893	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛)) = Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛))))
281	278, 280	oveq12d 7034	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛)) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚))) + Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))))
282	104	2timesd 11728	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛)) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))))
283	114, 209	mulcld 10507	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚))) ∈ ℂ)
284	114, 212	mulcld 10507	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛))) ∈ ℂ)
285	7, 283, 284	fsumadd 14929	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚))) + ((Λ‘𝑛) · ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚))) + Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))))
286	281, 282, 285	3eqtr4d 2841	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚))) + ((Λ‘𝑛) · ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))))
287	114, 209, 212	adddid 10511	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))) = (((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚))) + ((Λ‘𝑛) · ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))))
288	287	sumeq2dv 14893	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚))) + ((Λ‘𝑛) · ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))))
289	286, 288	eqtr4d 2834	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))))
290	91	recnd 10515	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) ∈ ℂ)
291	7, 26, 290	fsummulc1 14973	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))
292	289, 291	oveq12d 7034	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))))
293	218, 233, 292	3eqtr4rd 2842	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))))
294	293	fveq2d 6542	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) = (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))))))
295	24, 23, 203	mulassd 10510	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝐴) · 𝑥) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 · 𝑥)))
296	208, 294, 295	3brtr4d 4994	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) ≤ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝐴) · 𝑥))
297	109, 113, 43	ledivmul2d 12335	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (((abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) / 𝑥) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝐴) ↔ (abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) ≤ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝐴) · 𝑥)))
298	296, 297	mpbird 258	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) / 𝑥) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝐴))
299	111, 113, 25, 298	lediv1dd 12339	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (((abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) / 𝑥) / (log‘𝑥)) ≤ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝐴) / (log‘𝑥)))
300	109	recnd 10515	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) ∈ ℂ)
301	300, 203, 26, 110, 29	divdiv1d 11295	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (((abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) / 𝑥) / (log‘𝑥)) = ((abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) / (𝑥 · (log‘𝑥))))
302	108, 26, 203, 29, 110	divdiv32d 11289	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))) / (log‘𝑥)) / 𝑥) = ((((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))) / 𝑥) / (log‘𝑥)))
303	105, 107, 26, 29	divsubdird 11303	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))) / (log‘𝑥)) = (((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) / (log‘𝑥)) − ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)) / (log‘𝑥))))
304	103, 104, 26, 29	div23d 11301	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) / (log‘𝑥)) = ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))))
305	106, 26, 29	divcan4d 11270	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)) / (log‘𝑥)) = Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))))
306	304, 305	oveq12d 7034	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) / (log‘𝑥)) − ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)) / (log‘𝑥))) = (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))))
307	303, 306	eqtrd 2831	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))) / (log‘𝑥)) = (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))))
308	307	oveq1d 7031	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))) / (log‘𝑥)) / 𝑥) = ((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥))
309	108, 203, 26, 110, 29	divdiv1d 11295	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))) / 𝑥) / (log‘𝑥)) = (((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))) / (𝑥 · (log‘𝑥))))
310	302, 308, 309	3eqtr3d 2839	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥) = (((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))) / (𝑥 · (log‘𝑥))))
311	310	fveq2d 6542	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥)) = (abs‘(((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))) / (𝑥 · (log‘𝑥)))))
312	43, 25	rpmulcld 12297	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ∈ ℝ⁺)
313	312	rpcnd 12283	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ∈ ℂ)
314	312	rpne0d 12286	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ≠ 0)
315	108, 313, 314	absdivd 14649	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘(((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))) / (𝑥 · (log‘𝑥)))) = ((abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) / (abs‘(𝑥 · (log‘𝑥)))))
316	312	rpred 12281	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ∈ ℝ)
317	312	rpge0d 12285	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ (𝑥 · (log‘𝑥)))
318	316, 317	absidd 14616	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘(𝑥 · (log‘𝑥))) = (𝑥 · (log‘𝑥)))
319	318	oveq2d 7032	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) / (abs‘(𝑥 · (log‘𝑥)))) = ((abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) / (𝑥 · (log‘𝑥))))
320	311, 315, 319	3eqtrd 2835	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥)) = ((abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) / (𝑥 · (log‘𝑥))))
321	301, 320	eqtr4d 2834	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (((abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) / 𝑥) / (log‘𝑥)) = (abs‘((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥)))
322	24, 23, 26, 29	divassd 11299	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝐴) / (log‘𝑥)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 / (log‘𝑥))))
323	299, 321, 322	3brtr3d 4993	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥)) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 / (log‘𝑥))))
324	21	leabsd 14608	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 / (log‘𝑥))) ≤ (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 / (log‘𝑥)))))
325	101, 21, 102, 323, 324	letrd 10644	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥)) ≤ (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 / (log‘𝑥)))))
326	325	adantrr 713	. 2 ⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ 1 ≤ 𝑥)) → (abs‘((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥)) ≤ (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 / (log‘𝑥)))))
327	1, 83, 21, 100, 326	o1le 14843	1 ⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥)) ∈ 𝑂(1))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 = wceq 1522 ∈ wcel 2081 ∀wral 3105 ⊆ wss 3859 class class class wbr 4962 ↦ cmpt 5041 ‘cfv 6225 (class class class)co 7016 ℂcc 10381 ℝcr 10382 0cc0 10383 1c1 10384 + caddc 10386 · cmul 10388 +∞cpnf 10518 < clt 10521 ≤ cle 10522 − cmin 10717 / cdiv 11145 ℕcn 11486 2c2 11540 ℝ⁺crp 12239 (,)cioo 12588 [,)cico 12590 ...cfz 12742 ⌊cfl 13010 abscabs 14427 𝑂(1)co1 14677 Σcsu 14876 eceu 15249 logclog 24819 Λcvma 25351 ψcchp 25352

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-rep 5081 ax-sep 5094 ax-nul 5101 ax-pow 5157 ax-pr 5221 ax-un 7319 ax-inf2 8950 ax-cnex 10439 ax-resscn 10440 ax-1cn 10441 ax-icn 10442 ax-addcl 10443 ax-addrcl 10444 ax-mulcl 10445 ax-mulrcl 10446 ax-mulcom 10447 ax-addass 10448 ax-mulass 10449 ax-distr 10450 ax-i2m1 10451 ax-1ne0 10452 ax-1rid 10453 ax-rnegex 10454 ax-rrecex 10455 ax-cnre 10456 ax-pre-lttri 10457 ax-pre-lttrn 10458 ax-pre-ltadd 10459 ax-pre-mulgt0 10460 ax-pre-sup 10461 ax-addf 10462 ax-mulf 10463

This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1081 df-3an 1082 df-tru 1525 df-fal 1535 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ne 2985 df-nel 3091 df-ral 3110 df-rex 3111 df-reu 3112 df-rmo 3113 df-rab 3114 df-v 3439 df-sbc 3707 df-csb 3812 df-dif 3862 df-un 3864 df-in 3866 df-ss 3874 df-pss 3876 df-nul 4212 df-if 4382 df-pw 4455 df-sn 4473 df-pr 4475 df-tp 4477 df-op 4479 df-uni 4746 df-int 4783 df-iun 4827 df-iin 4828 df-br 4963 df-opab 5025 df-mpt 5042 df-tr 5064 df-id 5348 df-eprel 5353 df-po 5362 df-so 5363 df-fr 5402 df-se 5403 df-we 5404 df-xp 5449 df-rel 5450 df-cnv 5451 df-co 5452 df-dm 5453 df-rn 5454 df-res 5455 df-ima 5456 df-pred 6023 df-ord 6069 df-on 6070 df-lim 6071 df-suc 6072 df-iota 6189 df-fun 6227 df-fn 6228 df-f 6229 df-f1 6230 df-fo 6231 df-f1o 6232 df-fv 6233 df-isom 6234 df-riota 6977 df-ov 7019 df-oprab 7020 df-mpo 7021 df-of 7267 df-om 7437 df-1st 7545 df-2nd 7546 df-supp 7682 df-wrecs 7798 df-recs 7860 df-rdg 7898 df-1o 7953 df-2o 7954 df-oadd 7957 df-er 8139 df-map 8258 df-pm 8259 df-ixp 8311 df-en 8358 df-dom 8359 df-sdom 8360 df-fin 8361 df-fsupp 8680 df-fi 8721 df-sup 8752 df-inf 8753 df-oi 8820 df-dju 9176 df-card 9214 df-pnf 10523 df-mnf 10524 df-xr 10525 df-ltxr 10526 df-le 10527 df-sub 10719 df-neg 10720 df-div 11146 df-nn 11487 df-2 11548 df-3 11549 df-4 11550 df-5 11551 df-6 11552 df-7 11553 df-8 11554 df-9 11555 df-n0 11746 df-xnn0 11816 df-z 11830 df-dec 11948 df-uz 12094 df-q 12198 df-rp 12240 df-xneg 12357 df-xadd 12358 df-xmul 12359 df-ioo 12592 df-ioc 12593 df-ico 12594 df-icc 12595 df-fz 12743 df-fzo 12884 df-fl 13012 df-mod 13088 df-seq 13220 df-exp 13280 df-fac 13484 df-bc 13513 df-hash 13541 df-shft 14260 df-cj 14292 df-re 14293 df-im 14294 df-sqrt 14428 df-abs 14429 df-limsup 14662 df-clim 14679 df-rlim 14680 df-o1 14681 df-lo1 14682 df-sum 14877 df-ef 15254 df-e 15255 df-sin 15256 df-cos 15257 df-pi 15259 df-dvds 15441 df-gcd 15677 df-prm 15845 df-pc 16003 df-struct 16314 df-ndx 16315 df-slot 16316 df-base 16318 df-sets 16319 df-ress 16320 df-plusg 16407 df-mulr 16408 df-starv 16409 df-sca 16410 df-vsca 16411 df-ip 16412 df-tset 16413 df-ple 16414 df-ds 16416 df-unif 16417 df-hom 16418 df-cco 16419 df-rest 16525 df-topn 16526 df-0g 16544 df-gsum 16545 df-topgen 16546 df-pt 16547 df-prds 16550 df-xrs 16604 df-qtop 16609 df-imas 16610 df-xps 16612 df-mre 16686 df-mrc 16687 df-acs 16689 df-mgm 17681 df-sgrp 17723 df-mnd 17734 df-submnd 17775 df-mulg 17982 df-cntz 18188 df-cmn 18635 df-psmet 20219 df-xmet 20220 df-met 20221 df-bl 20222 df-mopn 20223 df-fbas 20224 df-fg 20225 df-cnfld 20228 df-top 21186 df-topon 21203 df-topsp 21225 df-bases 21238 df-cld 21311 df-ntr 21312 df-cls 21313 df-nei 21390 df-lp 21428 df-perf 21429 df-cn 21519 df-cnp 21520 df-haus 21607 df-cmp 21679 df-tx 21854 df-hmeo 22047 df-fil 22138 df-fm 22230 df-flim 22231 df-flf 22232 df-xms 22613 df-ms 22614 df-tms 22615 df-cncf 23169 df-limc 24147 df-dv 24148 df-log 24821 df-cxp 24822 df-cht 25356 df-vma 25357 df-chp 25358 df-ppi 25359

This theorem is referenced by: selberg3lem2 25816

W3C validator