pntrlog2bndlem4 - Metamath Proof Explorer

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

Theorem pntrlog2bndlem4 27524

Description: Lemma for pntrlog2bnd 27528. Bound on the difference between the Selberg function and its approximation, inside a sum. (Contributed by Mario Carneiro, 31-May-2016.)

**Hypotheses**
Ref	Expression
pntsval.1	⊢ 𝑆 = (𝑎 ∈ ℝ ↦ Σ𝑖 ∈ (1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))))
pntrlog2bnd.r	⊢ 𝑅 = (𝑎 ∈ ℝ⁺ ↦ ((ψ‘𝑎) − 𝑎))
pntrlog2bnd.t	⊢ 𝑇 = (𝑎 ∈ ℝ ↦ if(𝑎 ∈ ℝ⁺, (𝑎 · (log‘𝑎)), 0))

**Assertion**
Ref	Expression
pntrlog2bndlem4	⊢ (𝑥 ∈ (1(,)+∞) ↦ ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / 𝑥)) ∈ ≤𝑂(1)

Distinct variable groups: 𝑖,𝑎,𝑛,𝑥 𝑆,𝑛,𝑥 𝑅,𝑛,𝑥 𝑇,𝑛 Allowed substitution hints: 𝑅(𝑖,𝑎) 𝑆(𝑖,𝑎) 𝑇(𝑥,𝑖,𝑎)

Proof of Theorem pntrlog2bndlem4 Dummy variables 𝑐 𝑚 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elioore 13281	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (1(,)+∞) → 𝑥 ∈ ℝ)
2	1	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ∈ ℝ)
3		1rp 12900	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1 ∈ ℝ⁺
4	3	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 ∈ ℝ⁺)
5		1red 11119	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 ∈ ℝ)
6		eliooord 13311	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (1(,)+∞) → (1 < 𝑥 ∧ 𝑥 < +∞))
7	6	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (1 < 𝑥 ∧ 𝑥 < +∞))
8	7	simpld 494	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 < 𝑥)
9	5, 2, 8	ltled 11267	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 ≤ 𝑥)
10	2, 4, 9	rpgecld 12979	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ∈ ℝ⁺)
11	10	rprege0d 12947	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
12		flge0nn0 13730	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → (⌊‘𝑥) ∈ ℕ₀)
13	11, 12	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (⌊‘𝑥) ∈ ℕ₀)
14		nn0p1nn 12426	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⌊‘𝑥) ∈ ℕ₀ → ((⌊‘𝑥) + 1) ∈ ℕ)
15	13, 14	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((⌊‘𝑥) + 1) ∈ ℕ)
16	15	nnrpd 12938	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((⌊‘𝑥) + 1) ∈ ℝ⁺)
17	10, 16	rpdivcld 12957	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 / ((⌊‘𝑥) + 1)) ∈ ℝ⁺)
18		pntrlog2bnd.r	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑅 = (𝑎 ∈ ℝ⁺ ↦ ((ψ‘𝑎) − 𝑎))
19	18	pntrval 27506	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 / ((⌊‘𝑥) + 1)) ∈ ℝ⁺ → (𝑅‘(𝑥 / ((⌊‘𝑥) + 1))) = ((ψ‘(𝑥 / ((⌊‘𝑥) + 1))) − (𝑥 / ((⌊‘𝑥) + 1))))
20	17, 19	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑅‘(𝑥 / ((⌊‘𝑥) + 1))) = ((ψ‘(𝑥 / ((⌊‘𝑥) + 1))) − (𝑥 / ((⌊‘𝑥) + 1))))
21	2, 15	nndivred 12185	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 / ((⌊‘𝑥) + 1)) ∈ ℝ)
22		2re 12205	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 ∈ ℝ
23	22	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 2 ∈ ℝ)
24		flltp1 13710	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℝ → 𝑥 < ((⌊‘𝑥) + 1))
25	2, 24	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 < ((⌊‘𝑥) + 1))
26	15	nncnd 12147	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((⌊‘𝑥) + 1) ∈ ℂ)
27	26	mulridd 11135	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((⌊‘𝑥) + 1) · 1) = ((⌊‘𝑥) + 1))
28	25, 27	breqtrrd 5121	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 < (((⌊‘𝑥) + 1) · 1))
29	2, 5, 16	ltdivmuld 12991	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑥 / ((⌊‘𝑥) + 1)) < 1 ↔ 𝑥 < (((⌊‘𝑥) + 1) · 1)))
30	28, 29	mpbird 257	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 / ((⌊‘𝑥) + 1)) < 1)
31		1lt2 12297	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1 < 2
32	31	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 < 2)
33	21, 5, 23, 30, 32	lttrd 11280	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 / ((⌊‘𝑥) + 1)) < 2)
34		chpeq0 27152	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 / ((⌊‘𝑥) + 1)) ∈ ℝ → ((ψ‘(𝑥 / ((⌊‘𝑥) + 1))) = 0 ↔ (𝑥 / ((⌊‘𝑥) + 1)) < 2))
35	21, 34	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((ψ‘(𝑥 / ((⌊‘𝑥) + 1))) = 0 ↔ (𝑥 / ((⌊‘𝑥) + 1)) < 2))
36	33, 35	mpbird 257	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (ψ‘(𝑥 / ((⌊‘𝑥) + 1))) = 0)
37	36	oveq1d 7367	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((ψ‘(𝑥 / ((⌊‘𝑥) + 1))) − (𝑥 / ((⌊‘𝑥) + 1))) = (0 − (𝑥 / ((⌊‘𝑥) + 1))))
38	20, 37	eqtrd 2766	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑅‘(𝑥 / ((⌊‘𝑥) + 1))) = (0 − (𝑥 / ((⌊‘𝑥) + 1))))
39	38	fveq2d 6832	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) = (abs‘(0 − (𝑥 / ((⌊‘𝑥) + 1)))))
40		0red 11121	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 0 ∈ ℝ)
41	17	rpge0d 12944	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ (𝑥 / ((⌊‘𝑥) + 1)))
42	40, 21, 41	abssuble0d 15348	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘(0 − (𝑥 / ((⌊‘𝑥) + 1)))) = ((𝑥 / ((⌊‘𝑥) + 1)) − 0))
43	21	recnd 11146	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 / ((⌊‘𝑥) + 1)) ∈ ℂ)
44	43	subid1d 11467	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑥 / ((⌊‘𝑥) + 1)) − 0) = (𝑥 / ((⌊‘𝑥) + 1)))
45	39, 42, 44	3eqtrd 2770	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) = (𝑥 / ((⌊‘𝑥) + 1)))
46	13	nn0red 12449	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (⌊‘𝑥) ∈ ℝ)
47		pntsval.1	. . . . . . . . . . . . . . . . 17 ⊢ 𝑆 = (𝑎 ∈ ℝ ↦ Σ𝑖 ∈ (1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))))
48	47	pntsval2 27520	. . . . . . . . . . . . . . . 16 ⊢ ((⌊‘𝑥) ∈ ℝ → (𝑆‘(⌊‘𝑥)) = Σ𝑛 ∈ (1...(⌊‘(⌊‘𝑥)))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))))
49	46, 48	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑆‘(⌊‘𝑥)) = Σ𝑛 ∈ (1...(⌊‘(⌊‘𝑥)))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))))
50	13	nn0cnd 12450	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (⌊‘𝑥) ∈ ℂ)
51		1cnd 11113	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 ∈ ℂ)
52	50, 51	pncand 11479	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((⌊‘𝑥) + 1) − 1) = (⌊‘𝑥))
53	52	fveq2d 6832	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑆‘(((⌊‘𝑥) + 1) − 1)) = (𝑆‘(⌊‘𝑥)))
54	47	pntsval2 27520	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℝ → (𝑆‘𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))))
55	2, 54	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑆‘𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))))
56		flidm 13719	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℝ → (⌊‘(⌊‘𝑥)) = (⌊‘𝑥))
57	2, 56	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (⌊‘(⌊‘𝑥)) = (⌊‘𝑥))
58	57	oveq2d 7368	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (1...(⌊‘(⌊‘𝑥))) = (1...(⌊‘𝑥)))
59	58	sumeq1d 15613	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘(⌊‘𝑥)))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))))
60	55, 59	eqtr4d 2769	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑆‘𝑥) = Σ𝑛 ∈ (1...(⌊‘(⌊‘𝑥)))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))))
61	49, 53, 60	3eqtr4d 2776	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑆‘(((⌊‘𝑥) + 1) − 1)) = (𝑆‘𝑥))
62	52	fveq2d 6832	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑇‘(((⌊‘𝑥) + 1) − 1)) = (𝑇‘(⌊‘𝑥)))
63	62	oveq2d 7368	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1))) = (2 · (𝑇‘(⌊‘𝑥))))
64	61, 63	oveq12d 7370	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1)))) = ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))))
65	45, 64	oveq12d 7370	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) · ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1))))) = ((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))))
66	2	recnd 11146	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ∈ ℂ)
67	66	div1d 11895	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 / 1) = 𝑥)
68	67	fveq2d 6832	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑅‘(𝑥 / 1)) = (𝑅‘𝑥))
69	18	pntrf 27507	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑅:ℝ⁺⟶ℝ
70	69	ffvelcdmi 7022	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℝ⁺ → (𝑅‘𝑥) ∈ ℝ)
71	10, 70	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑅‘𝑥) ∈ ℝ)
72	68, 71	eqeltrd 2831	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑅‘(𝑥 / 1)) ∈ ℝ)
73	72	recnd 11146	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑅‘(𝑥 / 1)) ∈ ℂ)
74	73	abscld 15352	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘(𝑅‘(𝑥 / 1))) ∈ ℝ)
75	74	recnd 11146	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘(𝑅‘(𝑥 / 1))) ∈ ℂ)
76	75	mul01d 11318	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((abs‘(𝑅‘(𝑥 / 1))) · 0) = 0)
77	65, 76	oveq12d 7370	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) · ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1))))) − ((abs‘(𝑅‘(𝑥 / 1))) · 0)) = (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) − 0))
78	47	pntsf 27517	. . . . . . . . . . . . . . . . 17 ⊢ 𝑆:ℝ⟶ℝ
79	78	ffvelcdmi 7022	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℝ → (𝑆‘𝑥) ∈ ℝ)
80	2, 79	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑆‘𝑥) ∈ ℝ)
81		pntrlog2bnd.t	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑇 = (𝑎 ∈ ℝ ↦ if(𝑎 ∈ ℝ⁺, (𝑎 · (log‘𝑎)), 0))
82		relogcl 26517	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 ∈ ℝ⁺ → (log‘𝑎) ∈ ℝ)
83		remulcl 11097	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑎 ∈ ℝ ∧ (log‘𝑎) ∈ ℝ) → (𝑎 · (log‘𝑎)) ∈ ℝ)
84	82, 83	sylan2 593	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 ∈ ℝ ∧ 𝑎 ∈ ℝ⁺) → (𝑎 · (log‘𝑎)) ∈ ℝ)
85		0red 11121	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 ∈ ℝ ∧ ¬ 𝑎 ∈ ℝ⁺) → 0 ∈ ℝ)
86	84, 85	ifclda 4510	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 ∈ ℝ → if(𝑎 ∈ ℝ⁺, (𝑎 · (log‘𝑎)), 0) ∈ ℝ)
87	81, 86	fmpti 7051	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑇:ℝ⟶ℝ
88	87	ffvelcdmi 7022	. . . . . . . . . . . . . . . . 17 ⊢ ((⌊‘𝑥) ∈ ℝ → (𝑇‘(⌊‘𝑥)) ∈ ℝ)
89	46, 88	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑇‘(⌊‘𝑥)) ∈ ℝ)
90	23, 89	remulcld 11148	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (2 · (𝑇‘(⌊‘𝑥))) ∈ ℝ)
91	80, 90	resubcld 11551	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) ∈ ℝ)
92	21, 91	remulcld 11148	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) ∈ ℝ)
93	92	recnd 11146	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) ∈ ℂ)
94	93	subid1d 11467	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) − 0) = ((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))))
95	77, 94	eqtrd 2766	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) · ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1))))) − ((abs‘(𝑅‘(𝑥 / 1))) · 0)) = ((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))))
96	2	flcld 13708	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (⌊‘𝑥) ∈ ℤ)
97		fzval3 13640	. . . . . . . . . . . . . 14 ⊢ ((⌊‘𝑥) ∈ ℤ → (1...(⌊‘𝑥)) = (1..^((⌊‘𝑥) + 1)))
98	96, 97	syl 17	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (1...(⌊‘𝑥)) = (1..^((⌊‘𝑥) + 1)))
99	98	eqcomd 2737	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (1..^((⌊‘𝑥) + 1)) = (1...(⌊‘𝑥)))
100	10	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ⁺)
101		elfznn 13459	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
102	101	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
103	102	nnrpd 12938	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ⁺)
104	100, 103	rpdivcld 12957	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ⁺)
105	69	ffvelcdmi 7022	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 / 𝑛) ∈ ℝ⁺ → (𝑅‘(𝑥 / 𝑛)) ∈ ℝ)
106	104, 105	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘(𝑥 / 𝑛)) ∈ ℝ)
107	106	recnd 11146	. . . . . . . . . . . . . . . . . 18 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘(𝑥 / 𝑛)) ∈ ℂ)
108	107	abscld 15352	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑅‘(𝑥 / 𝑛))) ∈ ℝ)
109	108	recnd 11146	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑅‘(𝑥 / 𝑛))) ∈ ℂ)
110	3	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℝ⁺)
111	103, 110	rpaddcld 12955	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 + 1) ∈ ℝ⁺)
112	100, 111	rpdivcld 12957	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / (𝑛 + 1)) ∈ ℝ⁺)
113	69	ffvelcdmi 7022	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 / (𝑛 + 1)) ∈ ℝ⁺ → (𝑅‘(𝑥 / (𝑛 + 1))) ∈ ℝ)
114	112, 113	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘(𝑥 / (𝑛 + 1))) ∈ ℝ)
115	114	recnd 11146	. . . . . . . . . . . . . . . . . 18 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘(𝑥 / (𝑛 + 1))) ∈ ℂ)
116	115	abscld 15352	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) ∈ ℝ)
117	116	recnd 11146	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) ∈ ℂ)
118	109, 117	negsubdi2d 11494	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → -((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) = ((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))))
119	118	eqcomd 2737	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))) = -((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))))
120	102	nncnd 12147	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℂ)
121		1cnd 11113	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℂ)
122	120, 121	pncand 11479	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) − 1) = 𝑛)
123	122	fveq2d 6832	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘((𝑛 + 1) − 1)) = (𝑆‘𝑛))
124	122	fveq2d 6832	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇‘((𝑛 + 1) − 1)) = (𝑇‘𝑛))
125		rpre 12905	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℝ⁺ → 𝑛 ∈ ℝ)
126		eleq1 2819	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = 𝑛 → (𝑎 ∈ ℝ⁺ ↔ 𝑛 ∈ ℝ⁺))
127		id 22	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = 𝑛 → 𝑎 = 𝑛)
128		fveq2 6828	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = 𝑛 → (log‘𝑎) = (log‘𝑛))
129	127, 128	oveq12d 7370	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = 𝑛 → (𝑎 · (log‘𝑎)) = (𝑛 · (log‘𝑛)))
130	126, 129	ifbieq1d 4499	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = 𝑛 → if(𝑎 ∈ ℝ⁺, (𝑎 · (log‘𝑎)), 0) = if(𝑛 ∈ ℝ⁺, (𝑛 · (log‘𝑛)), 0))
131		ovex 7385	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 · (log‘𝑛)) ∈ V
132		c0ex 11112	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 ∈ V
133	131, 132	ifex 4525	. . . . . . . . . . . . . . . . . . . . 21 ⊢ if(𝑛 ∈ ℝ⁺, (𝑛 · (log‘𝑛)), 0) ∈ V
134	130, 81, 133	fvmpt 6935	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℝ → (𝑇‘𝑛) = if(𝑛 ∈ ℝ⁺, (𝑛 · (log‘𝑛)), 0))
135	125, 134	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ℝ⁺ → (𝑇‘𝑛) = if(𝑛 ∈ ℝ⁺, (𝑛 · (log‘𝑛)), 0))
136		iftrue 4480	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ℝ⁺ → if(𝑛 ∈ ℝ⁺, (𝑛 · (log‘𝑛)), 0) = (𝑛 · (log‘𝑛)))
137	135, 136	eqtrd 2766	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℝ⁺ → (𝑇‘𝑛) = (𝑛 · (log‘𝑛)))
138	103, 137	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇‘𝑛) = (𝑛 · (log‘𝑛)))
139	124, 138	eqtrd 2766	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇‘((𝑛 + 1) − 1)) = (𝑛 · (log‘𝑛)))
140	139	oveq2d 7368	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑇‘((𝑛 + 1) − 1))) = (2 · (𝑛 · (log‘𝑛))))
141	123, 140	oveq12d 7370	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))) = ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))
142	119, 141	oveq12d 7370	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))) · ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1))))) = (-((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))))
143	108, 116	resubcld 11551	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) ∈ ℝ)
144	143	recnd 11146	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) ∈ ℂ)
145	102	nnred 12146	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ)
146	78	ffvelcdmi 7022	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℝ → (𝑆‘𝑛) ∈ ℝ)
147	145, 146	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘𝑛) ∈ ℝ)
148	22	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 2 ∈ ℝ)
149	103	relogcld 26565	. . . . . . . . . . . . . . . . . 18 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘𝑛) ∈ ℝ)
150	145, 149	remulcld 11148	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 · (log‘𝑛)) ∈ ℝ)
151	148, 150	remulcld 11148	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑛 · (log‘𝑛))) ∈ ℝ)
152	147, 151	resubcld 11551	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))) ∈ ℝ)
153	152	recnd 11146	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))) ∈ ℂ)
154	144, 153	mulneg1d 11576	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (-((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) = -(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))))
155	142, 154	eqtrd 2766	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))) · ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1))))) = -(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))))
156	99, 155	sumeq12rdv 15620	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))(((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))) · ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1))))) = Σ𝑛 ∈ (1...(⌊‘𝑥))-(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))))
157		fzfid 13886	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (1...(⌊‘𝑥)) ∈ Fin)
158	143, 152	remulcld 11148	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) ∈ ℝ)
159	158	recnd 11146	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) ∈ ℂ)
160	157, 159	fsumneg 15700	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))-(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) = -Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))))
161	156, 160	eqtrd 2766	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))(((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))) · ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1))))) = -Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))))
162	95, 161	oveq12d 7370	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) · ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1))))) − ((abs‘(𝑅‘(𝑥 / 1))) · 0)) − Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))(((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))) · ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))))) = (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) − -Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))))
163		oveq2 7360	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑛 → (𝑥 / 𝑚) = (𝑥 / 𝑛))
164	163	fveq2d 6832	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑛 → (𝑅‘(𝑥 / 𝑚)) = (𝑅‘(𝑥 / 𝑛)))
165	164	fveq2d 6832	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → (abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / 𝑛))))
166		fvoveq1 7375	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑛 → (𝑆‘(𝑚 − 1)) = (𝑆‘(𝑛 − 1)))
167		fvoveq1 7375	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑛 → (𝑇‘(𝑚 − 1)) = (𝑇‘(𝑛 − 1)))
168	167	oveq2d 7368	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑛 → (2 · (𝑇‘(𝑚 − 1))) = (2 · (𝑇‘(𝑛 − 1))))
169	166, 168	oveq12d 7370	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1)))))
170	165, 169	jca 511	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → ((abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / 𝑛))) ∧ ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1))))))
171		oveq2 7360	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (𝑛 + 1) → (𝑥 / 𝑚) = (𝑥 / (𝑛 + 1)))
172	171	fveq2d 6832	. . . . . . . . . . . . 13 ⊢ (𝑚 = (𝑛 + 1) → (𝑅‘(𝑥 / 𝑚)) = (𝑅‘(𝑥 / (𝑛 + 1))))
173	172	fveq2d 6832	. . . . . . . . . . . 12 ⊢ (𝑚 = (𝑛 + 1) → (abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / (𝑛 + 1)))))
174		fvoveq1 7375	. . . . . . . . . . . . 13 ⊢ (𝑚 = (𝑛 + 1) → (𝑆‘(𝑚 − 1)) = (𝑆‘((𝑛 + 1) − 1)))
175		fvoveq1 7375	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (𝑛 + 1) → (𝑇‘(𝑚 − 1)) = (𝑇‘((𝑛 + 1) − 1)))
176	175	oveq2d 7368	. . . . . . . . . . . . 13 ⊢ (𝑚 = (𝑛 + 1) → (2 · (𝑇‘(𝑚 − 1))) = (2 · (𝑇‘((𝑛 + 1) − 1))))
177	174, 176	oveq12d 7370	. . . . . . . . . . . 12 ⊢ (𝑚 = (𝑛 + 1) → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))))
178	173, 177	jca 511	. . . . . . . . . . 11 ⊢ (𝑚 = (𝑛 + 1) → ((abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) ∧ ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1))))))
179		oveq2 7360	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 1 → (𝑥 / 𝑚) = (𝑥 / 1))
180	179	fveq2d 6832	. . . . . . . . . . . . 13 ⊢ (𝑚 = 1 → (𝑅‘(𝑥 / 𝑚)) = (𝑅‘(𝑥 / 1)))
181	180	fveq2d 6832	. . . . . . . . . . . 12 ⊢ (𝑚 = 1 → (abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / 1))))
182		oveq1 7359	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 1 → (𝑚 − 1) = (1 − 1))
183		1m1e0 12203	. . . . . . . . . . . . . . . . 17 ⊢ (1 − 1) = 0
184	182, 183	eqtrdi 2782	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 1 → (𝑚 − 1) = 0)
185	184	fveq2d 6832	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 1 → (𝑆‘(𝑚 − 1)) = (𝑆‘0))
186		0re 11120	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ ℝ
187		fveq2 6828	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = 0 → (⌊‘𝑎) = (⌊‘0))
188		0z 12485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 ∈ ℤ
189		flid 13718	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (0 ∈ ℤ → (⌊‘0) = 0)
190	188, 189	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⌊‘0) = 0
191	187, 190	eqtrdi 2782	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = 0 → (⌊‘𝑎) = 0)
192	191	oveq2d 7368	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 0 → (1...(⌊‘𝑎)) = (1...0))
193		fz10 13451	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1...0) = ∅
194	192, 193	eqtrdi 2782	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 0 → (1...(⌊‘𝑎)) = ∅)
195	194	sumeq1d 15613	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 0 → Σ𝑖 ∈ (1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))) = Σ𝑖 ∈ ∅ ((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))))
196		sum0 15634	. . . . . . . . . . . . . . . . . 18 ⊢ Σ𝑖 ∈ ∅ ((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))) = 0
197	195, 196	eqtrdi 2782	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 0 → Σ𝑖 ∈ (1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))) = 0)
198	197, 47, 132	fvmpt 6935	. . . . . . . . . . . . . . . 16 ⊢ (0 ∈ ℝ → (𝑆‘0) = 0)
199	186, 198	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (𝑆‘0) = 0
200	185, 199	eqtrdi 2782	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 1 → (𝑆‘(𝑚 − 1)) = 0)
201	184	fveq2d 6832	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 1 → (𝑇‘(𝑚 − 1)) = (𝑇‘0))
202		rpne0 12913	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 ∈ ℝ⁺ → 𝑎 ≠ 0)
203	202	necon2bi 2958	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 0 → ¬ 𝑎 ∈ ℝ⁺)
204	203	iffalsed 4485	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 0 → if(𝑎 ∈ ℝ⁺, (𝑎 · (log‘𝑎)), 0) = 0)
205	204, 81, 132	fvmpt 6935	. . . . . . . . . . . . . . . . . 18 ⊢ (0 ∈ ℝ → (𝑇‘0) = 0)
206	186, 205	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (𝑇‘0) = 0
207	201, 206	eqtrdi 2782	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 1 → (𝑇‘(𝑚 − 1)) = 0)
208	207	oveq2d 7368	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 1 → (2 · (𝑇‘(𝑚 − 1))) = (2 · 0))
209		2t0e0 12295	. . . . . . . . . . . . . . 15 ⊢ (2 · 0) = 0
210	208, 209	eqtrdi 2782	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 1 → (2 · (𝑇‘(𝑚 − 1))) = 0)
211	200, 210	oveq12d 7370	. . . . . . . . . . . . 13 ⊢ (𝑚 = 1 → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = (0 − 0))
212		0m0e0 12246	. . . . . . . . . . . . 13 ⊢ (0 − 0) = 0
213	211, 212	eqtrdi 2782	. . . . . . . . . . . 12 ⊢ (𝑚 = 1 → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = 0)
214	181, 213	jca 511	. . . . . . . . . . 11 ⊢ (𝑚 = 1 → ((abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / 1))) ∧ ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = 0))
215		oveq2 7360	. . . . . . . . . . . . . 14 ⊢ (𝑚 = ((⌊‘𝑥) + 1) → (𝑥 / 𝑚) = (𝑥 / ((⌊‘𝑥) + 1)))
216	215	fveq2d 6832	. . . . . . . . . . . . 13 ⊢ (𝑚 = ((⌊‘𝑥) + 1) → (𝑅‘(𝑥 / 𝑚)) = (𝑅‘(𝑥 / ((⌊‘𝑥) + 1))))
217	216	fveq2d 6832	. . . . . . . . . . . 12 ⊢ (𝑚 = ((⌊‘𝑥) + 1) → (abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))))
218		fvoveq1 7375	. . . . . . . . . . . . 13 ⊢ (𝑚 = ((⌊‘𝑥) + 1) → (𝑆‘(𝑚 − 1)) = (𝑆‘(((⌊‘𝑥) + 1) − 1)))
219		fvoveq1 7375	. . . . . . . . . . . . . 14 ⊢ (𝑚 = ((⌊‘𝑥) + 1) → (𝑇‘(𝑚 − 1)) = (𝑇‘(((⌊‘𝑥) + 1) − 1)))
220	219	oveq2d 7368	. . . . . . . . . . . . 13 ⊢ (𝑚 = ((⌊‘𝑥) + 1) → (2 · (𝑇‘(𝑚 − 1))) = (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1))))
221	218, 220	oveq12d 7370	. . . . . . . . . . . 12 ⊢ (𝑚 = ((⌊‘𝑥) + 1) → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1)))))
222	217, 221	jca 511	. . . . . . . . . . 11 ⊢ (𝑚 = ((⌊‘𝑥) + 1) → ((abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) ∧ ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1))))))
223		nnuz 12781	. . . . . . . . . . . 12 ⊢ ℕ = (ℤ_≥‘1)
224	15, 223	eleqtrdi 2841	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((⌊‘𝑥) + 1) ∈ (ℤ_≥‘1))
225	10	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 𝑥 ∈ ℝ⁺)
226		elfznn 13459	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ (1...((⌊‘𝑥) + 1)) → 𝑚 ∈ ℕ)
227	226	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 𝑚 ∈ ℕ)
228	227	nnrpd 12938	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 𝑚 ∈ ℝ⁺)
229	225, 228	rpdivcld 12957	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑥 / 𝑚) ∈ ℝ⁺)
230	69	ffvelcdmi 7022	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 / 𝑚) ∈ ℝ⁺ → (𝑅‘(𝑥 / 𝑚)) ∈ ℝ)
231	229, 230	syl 17	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑅‘(𝑥 / 𝑚)) ∈ ℝ)
232	231	recnd 11146	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑅‘(𝑥 / 𝑚)) ∈ ℂ)
233	232	abscld 15352	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (abs‘(𝑅‘(𝑥 / 𝑚))) ∈ ℝ)
234	233	recnd 11146	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (abs‘(𝑅‘(𝑥 / 𝑚))) ∈ ℂ)
235	227	nnred 12146	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 𝑚 ∈ ℝ)
236		1red 11119	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 1 ∈ ℝ)
237	235, 236	resubcld 11551	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑚 − 1) ∈ ℝ)
238	78	ffvelcdmi 7022	. . . . . . . . . . . . . 14 ⊢ ((𝑚 − 1) ∈ ℝ → (𝑆‘(𝑚 − 1)) ∈ ℝ)
239	237, 238	syl 17	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑆‘(𝑚 − 1)) ∈ ℝ)
240	22	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 2 ∈ ℝ)
241	87	ffvelcdmi 7022	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 − 1) ∈ ℝ → (𝑇‘(𝑚 − 1)) ∈ ℝ)
242	237, 241	syl 17	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑇‘(𝑚 − 1)) ∈ ℝ)
243	240, 242	remulcld 11148	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (2 · (𝑇‘(𝑚 − 1))) ∈ ℝ)
244	239, 243	resubcld 11551	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) ∈ ℝ)
245	244	recnd 11146	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) ∈ ℂ)
246	170, 178, 214, 222, 224, 234, 245	fsumparts 15719	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))) − ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1)))))) = ((((abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) · ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1))))) − ((abs‘(𝑅‘(𝑥 / 1))) · 0)) − Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))(((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))) · ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))))))
247	147	recnd 11146	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘𝑛) ∈ ℂ)
248	87	ffvelcdmi 7022	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℝ → (𝑇‘𝑛) ∈ ℝ)
249	145, 248	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇‘𝑛) ∈ ℝ)
250	148, 249	remulcld 11148	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑇‘𝑛)) ∈ ℝ)
251	250	recnd 11146	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑇‘𝑛)) ∈ ℂ)
252		1red 11119	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℝ)
253	145, 252	resubcld 11551	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 − 1) ∈ ℝ)
254	78	ffvelcdmi 7022	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 − 1) ∈ ℝ → (𝑆‘(𝑛 − 1)) ∈ ℝ)
255	253, 254	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘(𝑛 − 1)) ∈ ℝ)
256	255	recnd 11146	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘(𝑛 − 1)) ∈ ℂ)
257	87	ffvelcdmi 7022	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 − 1) ∈ ℝ → (𝑇‘(𝑛 − 1)) ∈ ℝ)
258	253, 257	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇‘(𝑛 − 1)) ∈ ℝ)
259	148, 258	remulcld 11148	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑇‘(𝑛 − 1))) ∈ ℝ)
260	259	recnd 11146	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑇‘(𝑛 − 1))) ∈ ℂ)
261	247, 251, 256, 260	sub4d 11527	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆‘𝑛) − (2 · (𝑇‘𝑛))) − ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1))))) = (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − ((2 · (𝑇‘𝑛)) − (2 · (𝑇‘(𝑛 − 1))))))
262	124	oveq2d 7368	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑇‘((𝑛 + 1) − 1))) = (2 · (𝑇‘𝑛)))
263	123, 262	oveq12d 7370	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))) = ((𝑆‘𝑛) − (2 · (𝑇‘𝑛))))
264	263	oveq1d 7367	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))) − ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1))))) = (((𝑆‘𝑛) − (2 · (𝑇‘𝑛))) − ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1))))))
265		2cnd 12209	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 2 ∈ ℂ)
266	249	recnd 11146	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇‘𝑛) ∈ ℂ)
267	258	recnd 11146	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇‘(𝑛 − 1)) ∈ ℂ)
268	265, 266, 267	subdid 11579	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))) = ((2 · (𝑇‘𝑛)) − (2 · (𝑇‘(𝑛 − 1)))))
269	268	oveq2d 7368	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))) = (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − ((2 · (𝑇‘𝑛)) − (2 · (𝑇‘(𝑛 − 1))))))
270	261, 264, 269	3eqtr4d 2776	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))) − ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1))))) = (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))
271	270	oveq2d 7368	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))) − ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1)))))) = ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))))
272	99, 271	sumeq12rdv 15620	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))) − ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1)))))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))))
273	246, 272	eqtr3d 2768	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) · ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1))))) − ((abs‘(𝑅‘(𝑥 / 1))) · 0)) − Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))(((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))) · ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))))
274	157, 159	fsumcl 15646	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) ∈ ℂ)
275	93, 274	subnegd 11485	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) − -Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) = (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))))
276	162, 273, 275	3eqtr3rd 2775	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))))
277	10	relogcld 26565	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ∈ ℝ)
278	277	recnd 11146	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ∈ ℂ)
279	66, 278	mulcomd 11139	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) = ((log‘𝑥) · 𝑥))
280	276, 279	oveq12d 7370	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / ((log‘𝑥) · 𝑥)))
281	147, 255	resubcld 11551	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) ∈ ℝ)
282	249, 258	resubcld 11551	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))) ∈ ℝ)
283	148, 282	remulcld 11148	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))) ∈ ℝ)
284	281, 283	resubcld 11551	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))) ∈ ℝ)
285	108, 284	remulcld 11148	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) ∈ ℝ)
286	157, 285	fsumrecl 15647	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) ∈ ℝ)
287	286	recnd 11146	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) ∈ ℂ)
288	2, 8	rplogcld 26571	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ∈ ℝ⁺)
289	288	rpne0d 12945	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ≠ 0)
290	10	rpne0d 12945	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ≠ 0)
291	287, 278, 66, 289, 290	divdiv1d 11934	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥)) / 𝑥) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / ((log‘𝑥) · 𝑥)))
292	280, 291	eqtr4d 2769	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥)) / 𝑥))
293	292	oveq2d 7368	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥) + ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥)))) = (((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥) + ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥)) / 𝑥)))
294	71	recnd 11146	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑅‘𝑥) ∈ ℂ)
295	294	abscld 15352	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘(𝑅‘𝑥)) ∈ ℝ)
296	295, 277	remulcld 11148	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((abs‘(𝑅‘𝑥)) · (log‘𝑥)) ∈ ℝ)
297	108, 281	remulcld 11148	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) ∈ ℝ)
298	157, 297	fsumrecl 15647	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) ∈ ℝ)
299	298, 288	rerpdivcld 12971	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥)) ∈ ℝ)
300	296, 299	resubcld 11551	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) ∈ ℝ)
301	300	recnd 11146	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) ∈ ℂ)
302	287, 278, 289	divcld 11903	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥)) ∈ ℂ)
303	301, 302, 66, 290	divdird 11941	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥))) / 𝑥) = (((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥) + ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥)) / 𝑥)))
304	296	recnd 11146	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((abs‘(𝑅‘𝑥)) · (log‘𝑥)) ∈ ℂ)
305	299	recnd 11146	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥)) ∈ ℂ)
306	304, 305, 302	subsubd 11506	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥)))) = ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥))))
307		2cnd 12209	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 2 ∈ ℂ)
308	266, 267	subcld 11478	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))) ∈ ℂ)
309	109, 308	mulcld 11138	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))) ∈ ℂ)
310	157, 307, 309	fsummulc2 15697	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(2 · ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))
311	281	recnd 11146	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) ∈ ℂ)
312	265, 308	mulcld 11138	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))) ∈ ℂ)
313	311, 312	nncand 11483	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) = (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))
314	313	oveq2d 7368	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) = ((abs‘(𝑅‘(𝑥 / 𝑛))) · (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))
315	284	recnd 11146	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))) ∈ ℂ)
316	109, 311, 315	subdid 11579	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) = (((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) − ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))))
317	109, 265, 308	mul12d 11328	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))) = (2 · ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))
318	314, 316, 317	3eqtr3d 2774	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) − ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) = (2 · ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))
319	318	sumeq2dv 15615	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) − ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(2 · ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))
320	297	recnd 11146	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) ∈ ℂ)
321	285	recnd 11146	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) ∈ ℂ)
322	157, 320, 321	fsumsub 15701	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) − ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))))
323	310, 319, 322	3eqtr2rd 2773	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) = (2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))
324	323	oveq1d 7367	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) / (log‘𝑥)) = ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))) / (log‘𝑥)))
325	298	recnd 11146	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) ∈ ℂ)
326	325, 287, 278, 289	divsubdird 11942	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) / (log‘𝑥)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥))))
327	108, 282	remulcld 11148	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))) ∈ ℝ)
328	157, 327	fsumrecl 15647	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))) ∈ ℝ)
329	328	recnd 11146	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))) ∈ ℂ)
330	307, 329, 278, 289	div23d 11940	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))) / (log‘𝑥)) = ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))
331	324, 326, 330	3eqtr3d 2774	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥))) = ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))
332	331	oveq2d 7368	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥)))) = (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))))
333	306, 332	eqtr3d 2768	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥))) = (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))))
334	333	oveq1d 7367	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥))) / 𝑥) = ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / 𝑥))
335	293, 303, 334	3eqtr2d 2772	. . . 4 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥) + ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥)))) = ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / 𝑥))
336	335	mpteq2dva 5186	. . 3 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥) + ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))))) = (𝑥 ∈ (1(,)+∞) ↦ ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / 𝑥)))
337	300, 10	rerpdivcld 12971	. . . 4 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥) ∈ ℝ)
338	157, 158	fsumrecl 15647	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) ∈ ℝ)
339	92, 338	readdcld 11147	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) ∈ ℝ)
340	10, 288	rpmulcld 12956	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ∈ ℝ⁺)
341	339, 340	rerpdivcld 12971	. . . 4 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))) ∈ ℝ)
342	47, 18	pntrlog2bndlem1 27521	. . . . 5 ⊢ (𝑥 ∈ (1(,)+∞) ↦ ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥)) ∈ ≤𝑂(1)
343	342	a1i 11	. . . 4 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥)) ∈ ≤𝑂(1))
344	340	rpcnd 12942	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ∈ ℂ)
345	340	rpne0d 12945	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ≠ 0)
346	93, 274, 344, 345	divdird 11941	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))) = ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) / (𝑥 · (log‘𝑥))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥)))))
347	91	recnd 11146	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) ∈ ℂ)
348	43, 347, 344, 345	divassd 11938	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) / (𝑥 · (log‘𝑥))) = ((𝑥 / ((⌊‘𝑥) + 1)) · (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))))
349	348	oveq1d 7367	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) / (𝑥 · (log‘𝑥))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥)))) = (((𝑥 / ((⌊‘𝑥) + 1)) · (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥)))))
350	346, 349	eqtrd 2766	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))) = (((𝑥 / ((⌊‘𝑥) + 1)) · (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥)))))
351	350	mpteq2dva 5186	. . . . 5 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥)))) = (𝑥 ∈ (1(,)+∞) ↦ (((𝑥 / ((⌊‘𝑥) + 1)) · (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥))))))
352	91, 340	rerpdivcld 12971	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥))) ∈ ℝ)
353	21, 352	remulcld 11148	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑥 / ((⌊‘𝑥) + 1)) · (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) ∈ ℝ)
354	338, 340	rerpdivcld 12971	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥))) ∈ ℝ)
355		ioossre 13313	. . . . . . . . 9 ⊢ (1(,)+∞) ⊆ ℝ
356	355	a1i 11	. . . . . . . 8 ⊢ (⊤ → (1(,)+∞) ⊆ ℝ)
357		1red 11119	. . . . . . . 8 ⊢ (⊤ → 1 ∈ ℝ)
358	21, 5, 30	ltled 11267	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 / ((⌊‘𝑥) + 1)) ≤ 1)
359	358	adantrr 717	. . . . . . . 8 ⊢ ((⊤ ∧ (𝑥 ∈ (1(,)+∞) ∧ 1 ≤ 𝑥)) → (𝑥 / ((⌊‘𝑥) + 1)) ≤ 1)
360	356, 21, 357, 357, 359	ello1d 15436	. . . . . . 7 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (𝑥 / ((⌊‘𝑥) + 1))) ∈ ≤𝑂(1))
361	80	recnd 11146	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑆‘𝑥) ∈ ℂ)
362	90	recnd 11146	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (2 · (𝑇‘(⌊‘𝑥))) ∈ ℂ)
363	361, 362, 344, 345	divsubdird 11942	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥))) = (((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) − ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥)))))
364	363	mpteq2dva 5186	. . . . . . . . 9 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) = (𝑥 ∈ (1(,)+∞) ↦ (((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) − ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥))))))
365	80, 340	rerpdivcld 12971	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) ∈ ℝ)
366	90, 340	rerpdivcld 12971	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥))) ∈ ℝ)
367		2cnd 12209	. . . . . . . . . . . 12 ⊢ (⊤ → 2 ∈ ℂ)
368		o1const 15533	. . . . . . . . . . . 12 ⊢ (((1(,)+∞) ⊆ ℝ ∧ 2 ∈ ℂ) → (𝑥 ∈ (1(,)+∞) ↦ 2) ∈ 𝑂(1))
369	355, 367, 368	sylancr 587	. . . . . . . . . . 11 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ 2) ∈ 𝑂(1))
370	365	recnd 11146	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) ∈ ℂ)
371	80, 10	rerpdivcld 12971	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑆‘𝑥) / 𝑥) ∈ ℝ)
372	371	recnd 11146	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑆‘𝑥) / 𝑥) ∈ ℂ)
373	307, 278	mulcld 11138	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (2 · (log‘𝑥)) ∈ ℂ)
374	372, 373, 278, 289	divsubdird 11942	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥))) / (log‘𝑥)) = ((((𝑆‘𝑥) / 𝑥) / (log‘𝑥)) − ((2 · (log‘𝑥)) / (log‘𝑥))))
375	23, 277	remulcld 11148	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (2 · (log‘𝑥)) ∈ ℝ)
376	371, 375	resubcld 11551	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥))) ∈ ℝ)
377	376	recnd 11146	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥))) ∈ ℂ)
378	377, 278, 289	divrecd 11906	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥))) / (log‘𝑥)) = ((((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥))) · (1 / (log‘𝑥))))
379	361, 66, 278, 290, 289	divdiv1d 11934	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑆‘𝑥) / 𝑥) / (log‘𝑥)) = ((𝑆‘𝑥) / (𝑥 · (log‘𝑥))))
380	307, 278, 289	divcan4d 11909	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 · (log‘𝑥)) / (log‘𝑥)) = 2)
381	379, 380	oveq12d 7370	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((𝑆‘𝑥) / 𝑥) / (log‘𝑥)) − ((2 · (log‘𝑥)) / (log‘𝑥))) = (((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) − 2))
382	374, 378, 381	3eqtr3rd 2775	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) − 2) = ((((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥))) · (1 / (log‘𝑥))))
383	382	mpteq2dva 5186	. . . . . . . . . . . . 13 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) − 2)) = (𝑥 ∈ (1(,)+∞) ↦ ((((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥))) · (1 / (log‘𝑥)))))
384	5, 288	rerpdivcld 12971	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (1 / (log‘𝑥)) ∈ ℝ)
385	10	ex 412	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) → 𝑥 ∈ ℝ⁺))
386	385	ssrdv 3935	. . . . . . . . . . . . . . 15 ⊢ (⊤ → (1(,)+∞) ⊆ ℝ⁺)
387	47	selbergs 27518	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℝ⁺ ↦ (((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥)))) ∈ 𝑂(1)
388	387	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ (((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥)))) ∈ 𝑂(1))
389	386, 388	o1res2 15476	. . . . . . . . . . . . . 14 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥)))) ∈ 𝑂(1))
390		divlogrlim 26577	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (1(,)+∞) ↦ (1 / (log‘𝑥))) ⇝_𝑟 0
391		rlimo1 15530	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ (1(,)+∞) ↦ (1 / (log‘𝑥))) ⇝_𝑟 0 → (𝑥 ∈ (1(,)+∞) ↦ (1 / (log‘𝑥))) ∈ 𝑂(1))
392	390, 391	mp1i 13	. . . . . . . . . . . . . 14 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (1 / (log‘𝑥))) ∈ 𝑂(1))
393	376, 384, 389, 392	o1mul2 15538	. . . . . . . . . . . . 13 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥))) · (1 / (log‘𝑥)))) ∈ 𝑂(1))
394	383, 393	eqeltrd 2831	. . . . . . . . . . . 12 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) − 2)) ∈ 𝑂(1))
395	370, 307, 394	o1dif 15543	. . . . . . . . . . 11 ⊢ (⊤ → ((𝑥 ∈ (1(,)+∞) ↦ ((𝑆‘𝑥) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1) ↔ (𝑥 ∈ (1(,)+∞) ↦ 2) ∈ 𝑂(1)))
396	369, 395	mpbird 257	. . . . . . . . . 10 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((𝑆‘𝑥) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1))
397	22	a1i 11	. . . . . . . . . . . 12 ⊢ (⊤ → 2 ∈ ℝ)
398	2, 277	remulcld 11148	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ∈ ℝ)
399		2rp 12901	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℝ⁺
400	399	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 2 ∈ ℝ⁺)
401	400	rpge0d 12944	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ 2)
402		flge1nn 13731	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) → (⌊‘𝑥) ∈ ℕ)
403	2, 9, 402	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (⌊‘𝑥) ∈ ℕ)
404	403	nnrpd 12938	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (⌊‘𝑥) ∈ ℝ⁺)
405		rpre 12905	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⌊‘𝑥) ∈ ℝ⁺ → (⌊‘𝑥) ∈ ℝ)
406		eleq1 2819	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = (⌊‘𝑥) → (𝑎 ∈ ℝ⁺ ↔ (⌊‘𝑥) ∈ ℝ⁺))
407		id 22	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = (⌊‘𝑥) → 𝑎 = (⌊‘𝑥))
408		fveq2 6828	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = (⌊‘𝑥) → (log‘𝑎) = (log‘(⌊‘𝑥)))
409	407, 408	oveq12d 7370	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = (⌊‘𝑥) → (𝑎 · (log‘𝑎)) = ((⌊‘𝑥) · (log‘(⌊‘𝑥))))
410	406, 409	ifbieq1d 4499	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = (⌊‘𝑥) → if(𝑎 ∈ ℝ⁺, (𝑎 · (log‘𝑎)), 0) = if((⌊‘𝑥) ∈ ℝ⁺, ((⌊‘𝑥) · (log‘(⌊‘𝑥))), 0))
411		ovex 7385	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((⌊‘𝑥) · (log‘(⌊‘𝑥))) ∈ V
412	411, 132	ifex 4525	. . . . . . . . . . . . . . . . . . . 20 ⊢ if((⌊‘𝑥) ∈ ℝ⁺, ((⌊‘𝑥) · (log‘(⌊‘𝑥))), 0) ∈ V
413	410, 81, 412	fvmpt 6935	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⌊‘𝑥) ∈ ℝ → (𝑇‘(⌊‘𝑥)) = if((⌊‘𝑥) ∈ ℝ⁺, ((⌊‘𝑥) · (log‘(⌊‘𝑥))), 0))
414	405, 413	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((⌊‘𝑥) ∈ ℝ⁺ → (𝑇‘(⌊‘𝑥)) = if((⌊‘𝑥) ∈ ℝ⁺, ((⌊‘𝑥) · (log‘(⌊‘𝑥))), 0))
415		iftrue 4480	. . . . . . . . . . . . . . . . . 18 ⊢ ((⌊‘𝑥) ∈ ℝ⁺ → if((⌊‘𝑥) ∈ ℝ⁺, ((⌊‘𝑥) · (log‘(⌊‘𝑥))), 0) = ((⌊‘𝑥) · (log‘(⌊‘𝑥))))
416	414, 415	eqtrd 2766	. . . . . . . . . . . . . . . . 17 ⊢ ((⌊‘𝑥) ∈ ℝ⁺ → (𝑇‘(⌊‘𝑥)) = ((⌊‘𝑥) · (log‘(⌊‘𝑥))))
417	404, 416	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑇‘(⌊‘𝑥)) = ((⌊‘𝑥) · (log‘(⌊‘𝑥))))
418	404	relogcld 26565	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (log‘(⌊‘𝑥)) ∈ ℝ)
419	13	nn0ge0d 12451	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ (⌊‘𝑥))
420	403	nnge1d 12179	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 ≤ (⌊‘𝑥))
421	46, 420	logge0d 26572	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ (log‘(⌊‘𝑥)))
422		flle 13709	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℝ → (⌊‘𝑥) ≤ 𝑥)
423	2, 422	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (⌊‘𝑥) ≤ 𝑥)
424	404, 10	logled 26569	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((⌊‘𝑥) ≤ 𝑥 ↔ (log‘(⌊‘𝑥)) ≤ (log‘𝑥)))
425	423, 424	mpbid 232	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (log‘(⌊‘𝑥)) ≤ (log‘𝑥))
426	46, 2, 418, 277, 419, 421, 423, 425	lemul12ad 12070	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((⌊‘𝑥) · (log‘(⌊‘𝑥))) ≤ (𝑥 · (log‘𝑥)))
427	417, 426	eqbrtrd 5115	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑇‘(⌊‘𝑥)) ≤ (𝑥 · (log‘𝑥)))
428	89, 398, 23, 401, 427	lemul2ad 12068	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (2 · (𝑇‘(⌊‘𝑥))) ≤ (2 · (𝑥 · (log‘𝑥))))
429	90, 23, 340	ledivmul2d 12994	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥))) ≤ 2 ↔ (2 · (𝑇‘(⌊‘𝑥))) ≤ (2 · (𝑥 · (log‘𝑥)))))
430	428, 429	mpbird 257	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥))) ≤ 2)
431	430	adantrr 717	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ (𝑥 ∈ (1(,)+∞) ∧ 1 ≤ 𝑥)) → ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥))) ≤ 2)
432	356, 366, 357, 397, 431	ello1d 15436	. . . . . . . . . . 11 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥)))) ∈ ≤𝑂(1))
433		0red 11121	. . . . . . . . . . . 12 ⊢ (⊤ → 0 ∈ ℝ)
434	46, 418, 419, 421	mulge0d 11700	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ ((⌊‘𝑥) · (log‘(⌊‘𝑥))))
435	434, 417	breqtrrd 5121	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ (𝑇‘(⌊‘𝑥)))
436	23, 89, 401, 435	mulge0d 11700	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ (2 · (𝑇‘(⌊‘𝑥))))
437	90, 340, 436	divge0d 12980	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥))))
438	366, 433, 437	o1lo12 15451	. . . . . . . . . . 11 ⊢ (⊤ → ((𝑥 ∈ (1(,)+∞) ↦ ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1) ↔ (𝑥 ∈ (1(,)+∞) ↦ ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥)))) ∈ ≤𝑂(1)))
439	432, 438	mpbird 257	. . . . . . . . . 10 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1))
440	365, 366, 396, 439	o1sub2 15539	. . . . . . . . 9 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) − ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥))))) ∈ 𝑂(1))
441	364, 440	eqeltrd 2831	. . . . . . . 8 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1))
442	352, 441	o1lo1d 15452	. . . . . . 7 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) ∈ ≤𝑂(1))
443	21, 352, 360, 442, 41	lo1mul 15541	. . . . . 6 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((𝑥 / ((⌊‘𝑥) + 1)) · (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥))))) ∈ ≤𝑂(1))
444	47	selbergsb 27519	. . . . . . . 8 ⊢ ∃𝑐 ∈ ℝ⁺ ∀𝑦 ∈ (1[,)+∞)(abs‘(((𝑆‘𝑦) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝑐
445		simpl 482	. . . . . . . . . 10 ⊢ ((𝑐 ∈ ℝ⁺ ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘(((𝑆‘𝑦) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝑐) → 𝑐 ∈ ℝ⁺)
446		simpr 484	. . . . . . . . . 10 ⊢ ((𝑐 ∈ ℝ⁺ ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘(((𝑆‘𝑦) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝑐) → ∀𝑦 ∈ (1[,)+∞)(abs‘(((𝑆‘𝑦) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝑐)
447	47, 18, 445, 446	pntrlog2bndlem3 27523	. . . . . . . . 9 ⊢ ((𝑐 ∈ ℝ⁺ ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘(((𝑆‘𝑦) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝑐) → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1))
448	447	rexlimiva 3125	. . . . . . . 8 ⊢ (∃𝑐 ∈ ℝ⁺ ∀𝑦 ∈ (1[,)+∞)(abs‘(((𝑆‘𝑦) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝑐 → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1))
449	444, 448	mp1i 13	. . . . . . 7 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1))
450	354, 449	o1lo1d 15452	. . . . . 6 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥)))) ∈ ≤𝑂(1))
451	353, 354, 443, 450	lo1add 15540	. . . . 5 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((𝑥 / ((⌊‘𝑥) + 1)) · (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥))))) ∈ ≤𝑂(1))
452	351, 451	eqeltrd 2831	. . . 4 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥)))) ∈ ≤𝑂(1))
453	337, 341, 343, 452	lo1add 15540	. . 3 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥) + ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))))) ∈ ≤𝑂(1))
454	336, 453	eqeltrrd 2832	. 2 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / 𝑥)) ∈ ≤𝑂(1))
455	454	mptru 1548	1 ⊢ (𝑥 ∈ (1(,)+∞) ↦ ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / 𝑥)) ∈ ≤𝑂(1)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 ↔ wb 206 ∧ wa 395 = wceq 1541 ⊤wtru 1542 ∈ wcel 2111 ∀wral 3047 ∃wrex 3056 {crab 3395 ⊆ wss 3897 ∅c0 4282 ifcif 4474 class class class wbr 5093 ↦ cmpt 5174 ‘cfv 6487 (class class class)co 7352 ℂcc 11010 ℝcr 11011 0cc0 11012 1c1 11013 + caddc 11015 · cmul 11017 +∞cpnf 11149 < clt 11152 ≤ cle 11153 − cmin 11350 -cneg 11351 / cdiv 11780 ℕcn 12131 2c2 12186 ℕ₀cn0 12387 ℤcz 12474 ℤ_≥cuz 12738 ℝ⁺crp 12896 (,)cioo 13251 [,)cico 13253 ...cfz 13413 ..^cfzo 13560 ⌊cfl 13700 abscabs 15147 ⇝_𝑟 crli 15398 𝑂(1)co1 15399 ≤𝑂(1)clo1 15400 Σcsu 15599 ∥ cdvds 16169 logclog 26496 Λcvma 27035 ψcchp 27036

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5219 ax-sep 5236 ax-nul 5246 ax-pow 5305 ax-pr 5372 ax-un 7674 ax-inf2 9537 ax-cnex 11068 ax-resscn 11069 ax-1cn 11070 ax-icn 11071 ax-addcl 11072 ax-addrcl 11073 ax-mulcl 11074 ax-mulrcl 11075 ax-mulcom 11076 ax-addass 11077 ax-mulass 11078 ax-distr 11079 ax-i2m1 11080 ax-1ne0 11081 ax-1rid 11082 ax-rnegex 11083 ax-rrecex 11084 ax-cnre 11085 ax-pre-lttri 11086 ax-pre-lttrn 11087 ax-pre-ltadd 11088 ax-pre-mulgt0 11089 ax-pre-sup 11090 ax-addf 11091

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rmo 3346 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3917 df-nul 4283 df-if 4475 df-pw 4551 df-sn 4576 df-pr 4578 df-tp 4580 df-op 4582 df-uni 4859 df-int 4898 df-iun 4943 df-iin 4944 df-disj 5061 df-br 5094 df-opab 5156 df-mpt 5175 df-tr 5201 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-se 5573 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6254 df-ord 6315 df-on 6316 df-lim 6317 df-suc 6318 df-iota 6443 df-fun 6489 df-fn 6490 df-f 6491 df-f1 6492 df-fo 6493 df-f1o 6494 df-fv 6495 df-isom 6496 df-riota 7309 df-ov 7355 df-oprab 7356 df-mpo 7357 df-of 7616 df-om 7803 df-1st 7927 df-2nd 7928 df-supp 8097 df-frecs 8217 df-wrecs 8248 df-recs 8297 df-rdg 8335 df-1o 8391 df-2o 8392 df-oadd 8395 df-er 8628 df-map 8758 df-pm 8759 df-ixp 8828 df-en 8876 df-dom 8877 df-sdom 8878 df-fin 8879 df-fsupp 9252 df-fi 9301 df-sup 9332 df-inf 9333 df-oi 9402 df-dju 9800 df-card 9838 df-pnf 11154 df-mnf 11155 df-xr 11156 df-ltxr 11157 df-le 11158 df-sub 11352 df-neg 11353 df-div 11781 df-nn 12132 df-2 12194 df-3 12195 df-4 12196 df-5 12197 df-6 12198 df-7 12199 df-8 12200 df-9 12201 df-n0 12388 df-xnn0 12461 df-z 12475 df-dec 12595 df-uz 12739 df-q 12853 df-rp 12897 df-xneg 13017 df-xadd 13018 df-xmul 13019 df-ioo 13255 df-ioc 13256 df-ico 13257 df-icc 13258 df-fz 13414 df-fzo 13561 df-fl 13702 df-mod 13780 df-seq 13915 df-exp 13975 df-fac 14187 df-bc 14216 df-hash 14244 df-shft 14980 df-cj 15012 df-re 15013 df-im 15014 df-sqrt 15148 df-abs 15149 df-limsup 15384 df-clim 15401 df-rlim 15402 df-o1 15403 df-lo1 15404 df-sum 15600 df-ef 15980 df-e 15981 df-sin 15982 df-cos 15983 df-tan 15984 df-pi 15985 df-dvds 16170 df-gcd 16412 df-prm 16589 df-pc 16755 df-struct 17064 df-sets 17081 df-slot 17099 df-ndx 17111 df-base 17127 df-ress 17148 df-plusg 17180 df-mulr 17181 df-starv 17182 df-sca 17183 df-vsca 17184 df-ip 17185 df-tset 17186 df-ple 17187 df-ds 17189 df-unif 17190 df-hom 17191 df-cco 17192 df-rest 17332 df-topn 17333 df-0g 17351 df-gsum 17352 df-topgen 17353 df-pt 17354 df-prds 17357 df-xrs 17412 df-qtop 17417 df-imas 17418 df-xps 17420 df-mre 17494 df-mrc 17495 df-acs 17497 df-mgm 18554 df-sgrp 18633 df-mnd 18649 df-submnd 18698 df-mulg 18987 df-cntz 19235 df-cmn 19700 df-psmet 21289 df-xmet 21290 df-met 21291 df-bl 21292 df-mopn 21293 df-fbas 21294 df-fg 21295 df-cnfld 21298 df-top 22815 df-topon 22832 df-topsp 22854 df-bases 22867 df-cld 22940 df-ntr 22941 df-cls 22942 df-nei 23019 df-lp 23057 df-perf 23058 df-cn 23148 df-cnp 23149 df-haus 23236 df-cmp 23308 df-tx 23483 df-hmeo 23676 df-fil 23767 df-fm 23859 df-flim 23860 df-flf 23861 df-xms 24241 df-ms 24242 df-tms 24243 df-cncf 24804 df-limc 25800 df-dv 25801 df-ulm 26319 df-log 26498 df-cxp 26499 df-atan 26810 df-em 26936 df-cht 27040 df-vma 27041 df-chp 27042 df-ppi 27043 df-mu 27044

This theorem is referenced by: pntrlog2bndlem5 27525

W3C validator