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 26164

Description: Lemma for pntrlog2bnd 26168. 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 12756	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (1(,)+∞) → 𝑥 ∈ ℝ)
2	1	adantl 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ∈ ℝ)
3		1rp 12381	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1 ∈ ℝ⁺
4	3	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 ∈ ℝ⁺)
5		1red 10631	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 ∈ ℝ)
6		eliooord 12784	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (1(,)+∞) → (1 < 𝑥 ∧ 𝑥 < +∞))
7	6	adantl 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (1 < 𝑥 ∧ 𝑥 < +∞))
8	7	simpld 498	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 < 𝑥)
9	5, 2, 8	ltled 10777	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 ≤ 𝑥)
10	2, 4, 9	rpgecld 12458	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ∈ ℝ⁺)
11	10	rprege0d 12426	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
12		flge0nn0 13185	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → (⌊‘𝑥) ∈ ℕ₀)
13	11, 12	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (⌊‘𝑥) ∈ ℕ₀)
14		nn0p1nn 11924	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⌊‘𝑥) ∈ ℕ₀ → ((⌊‘𝑥) + 1) ∈ ℕ)
15	13, 14	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((⌊‘𝑥) + 1) ∈ ℕ)
16	15	nnrpd 12417	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((⌊‘𝑥) + 1) ∈ ℝ⁺)
17	10, 16	rpdivcld 12436	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 / ((⌊‘𝑥) + 1)) ∈ ℝ⁺)
18		pntrlog2bnd.r	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑅 = (𝑎 ∈ ℝ⁺ ↦ ((ψ‘𝑎) − 𝑎))
19	18	pntrval 26146	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 / ((⌊‘𝑥) + 1)) ∈ ℝ⁺ → (𝑅‘(𝑥 / ((⌊‘𝑥) + 1))) = ((ψ‘(𝑥 / ((⌊‘𝑥) + 1))) − (𝑥 / ((⌊‘𝑥) + 1))))
20	17, 19	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑅‘(𝑥 / ((⌊‘𝑥) + 1))) = ((ψ‘(𝑥 / ((⌊‘𝑥) + 1))) − (𝑥 / ((⌊‘𝑥) + 1))))
21	2, 15	nndivred 11679	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 / ((⌊‘𝑥) + 1)) ∈ ℝ)
22		2re 11699	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 ∈ ℝ
23	22	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 2 ∈ ℝ)
24		flltp1 13165	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℝ → 𝑥 < ((⌊‘𝑥) + 1))
25	2, 24	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 < ((⌊‘𝑥) + 1))
26	15	nncnd 11641	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((⌊‘𝑥) + 1) ∈ ℂ)
27	26	mulid1d 10647	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((⌊‘𝑥) + 1) · 1) = ((⌊‘𝑥) + 1))
28	25, 27	breqtrrd 5058	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 < (((⌊‘𝑥) + 1) · 1))
29	2, 5, 16	ltdivmuld 12470	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑥 / ((⌊‘𝑥) + 1)) < 1 ↔ 𝑥 < (((⌊‘𝑥) + 1) · 1)))
30	28, 29	mpbird 260	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 / ((⌊‘𝑥) + 1)) < 1)
31		1lt2 11796	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1 < 2
32	31	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 < 2)
33	21, 5, 23, 30, 32	lttrd 10790	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 / ((⌊‘𝑥) + 1)) < 2)
34		chpeq0 25792	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 / ((⌊‘𝑥) + 1)) ∈ ℝ → ((ψ‘(𝑥 / ((⌊‘𝑥) + 1))) = 0 ↔ (𝑥 / ((⌊‘𝑥) + 1)) < 2))
35	21, 34	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((ψ‘(𝑥 / ((⌊‘𝑥) + 1))) = 0 ↔ (𝑥 / ((⌊‘𝑥) + 1)) < 2))
36	33, 35	mpbird 260	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (ψ‘(𝑥 / ((⌊‘𝑥) + 1))) = 0)
37	36	oveq1d 7150	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((ψ‘(𝑥 / ((⌊‘𝑥) + 1))) − (𝑥 / ((⌊‘𝑥) + 1))) = (0 − (𝑥 / ((⌊‘𝑥) + 1))))
38	20, 37	eqtrd 2833	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑅‘(𝑥 / ((⌊‘𝑥) + 1))) = (0 − (𝑥 / ((⌊‘𝑥) + 1))))
39	38	fveq2d 6649	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) = (abs‘(0 − (𝑥 / ((⌊‘𝑥) + 1)))))
40		0red 10633	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 0 ∈ ℝ)
41	17	rpge0d 12423	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ (𝑥 / ((⌊‘𝑥) + 1)))
42	40, 21, 41	abssuble0d 14784	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘(0 − (𝑥 / ((⌊‘𝑥) + 1)))) = ((𝑥 / ((⌊‘𝑥) + 1)) − 0))
43	21	recnd 10658	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 / ((⌊‘𝑥) + 1)) ∈ ℂ)
44	43	subid1d 10975	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑥 / ((⌊‘𝑥) + 1)) − 0) = (𝑥 / ((⌊‘𝑥) + 1)))
45	39, 42, 44	3eqtrd 2837	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) = (𝑥 / ((⌊‘𝑥) + 1)))
46	13	nn0red 11944	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (⌊‘𝑥) ∈ ℝ)
47		pntsval.1	. . . . . . . . . . . . . . . . 17 ⊢ 𝑆 = (𝑎 ∈ ℝ ↦ Σ𝑖 ∈ (1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))))
48	47	pntsval2 26160	. . . . . . . . . . . . . . . 16 ⊢ ((⌊‘𝑥) ∈ ℝ → (𝑆‘(⌊‘𝑥)) = Σ𝑛 ∈ (1...(⌊‘(⌊‘𝑥)))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))))
49	46, 48	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑆‘(⌊‘𝑥)) = Σ𝑛 ∈ (1...(⌊‘(⌊‘𝑥)))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))))
50	13	nn0cnd 11945	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (⌊‘𝑥) ∈ ℂ)
51		1cnd 10625	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 ∈ ℂ)
52	50, 51	pncand 10987	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((⌊‘𝑥) + 1) − 1) = (⌊‘𝑥))
53	52	fveq2d 6649	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑆‘(((⌊‘𝑥) + 1) − 1)) = (𝑆‘(⌊‘𝑥)))
54	47	pntsval2 26160	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℝ → (𝑆‘𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))))
55	2, 54	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑆‘𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))))
56		flidm 13174	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℝ → (⌊‘(⌊‘𝑥)) = (⌊‘𝑥))
57	2, 56	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (⌊‘(⌊‘𝑥)) = (⌊‘𝑥))
58	57	oveq2d 7151	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (1...(⌊‘(⌊‘𝑥))) = (1...(⌊‘𝑥)))
59	58	sumeq1d 15050	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘(⌊‘𝑥)))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))))
60	55, 59	eqtr4d 2836	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑆‘𝑥) = Σ𝑛 ∈ (1...(⌊‘(⌊‘𝑥)))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))))
61	49, 53, 60	3eqtr4d 2843	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑆‘(((⌊‘𝑥) + 1) − 1)) = (𝑆‘𝑥))
62	52	fveq2d 6649	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑇‘(((⌊‘𝑥) + 1) − 1)) = (𝑇‘(⌊‘𝑥)))
63	62	oveq2d 7151	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1))) = (2 · (𝑇‘(⌊‘𝑥))))
64	61, 63	oveq12d 7153	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1)))) = ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))))
65	45, 64	oveq12d 7153	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) · ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1))))) = ((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))))
66	2	recnd 10658	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ∈ ℂ)
67	66	div1d 11397	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 / 1) = 𝑥)
68	67	fveq2d 6649	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑅‘(𝑥 / 1)) = (𝑅‘𝑥))
69	18	pntrf 26147	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑅:ℝ⁺⟶ℝ
70	69	ffvelrni 6827	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℝ⁺ → (𝑅‘𝑥) ∈ ℝ)
71	10, 70	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑅‘𝑥) ∈ ℝ)
72	68, 71	eqeltrd 2890	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑅‘(𝑥 / 1)) ∈ ℝ)
73	72	recnd 10658	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑅‘(𝑥 / 1)) ∈ ℂ)
74	73	abscld 14788	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘(𝑅‘(𝑥 / 1))) ∈ ℝ)
75	74	recnd 10658	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘(𝑅‘(𝑥 / 1))) ∈ ℂ)
76	75	mul01d 10828	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((abs‘(𝑅‘(𝑥 / 1))) · 0) = 0)
77	65, 76	oveq12d 7153	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) · ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1))))) − ((abs‘(𝑅‘(𝑥 / 1))) · 0)) = (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) − 0))
78	47	pntsf 26157	. . . . . . . . . . . . . . . . 17 ⊢ 𝑆:ℝ⟶ℝ
79	78	ffvelrni 6827	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℝ → (𝑆‘𝑥) ∈ ℝ)
80	2, 79	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑆‘𝑥) ∈ ℝ)
81		pntrlog2bnd.t	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑇 = (𝑎 ∈ ℝ ↦ if(𝑎 ∈ ℝ⁺, (𝑎 · (log‘𝑎)), 0))
82		relogcl 25167	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 ∈ ℝ⁺ → (log‘𝑎) ∈ ℝ)
83		remulcl 10611	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑎 ∈ ℝ ∧ (log‘𝑎) ∈ ℝ) → (𝑎 · (log‘𝑎)) ∈ ℝ)
84	82, 83	sylan2 595	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 ∈ ℝ ∧ 𝑎 ∈ ℝ⁺) → (𝑎 · (log‘𝑎)) ∈ ℝ)
85		0red 10633	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 ∈ ℝ ∧ ¬ 𝑎 ∈ ℝ⁺) → 0 ∈ ℝ)
86	84, 85	ifclda 4459	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 ∈ ℝ → if(𝑎 ∈ ℝ⁺, (𝑎 · (log‘𝑎)), 0) ∈ ℝ)
87	81, 86	fmpti 6853	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑇:ℝ⟶ℝ
88	87	ffvelrni 6827	. . . . . . . . . . . . . . . . 17 ⊢ ((⌊‘𝑥) ∈ ℝ → (𝑇‘(⌊‘𝑥)) ∈ ℝ)
89	46, 88	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑇‘(⌊‘𝑥)) ∈ ℝ)
90	23, 89	remulcld 10660	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (2 · (𝑇‘(⌊‘𝑥))) ∈ ℝ)
91	80, 90	resubcld 11057	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) ∈ ℝ)
92	21, 91	remulcld 10660	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) ∈ ℝ)
93	92	recnd 10658	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) ∈ ℂ)
94	93	subid1d 10975	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) − 0) = ((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))))
95	77, 94	eqtrd 2833	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) · ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1))))) − ((abs‘(𝑅‘(𝑥 / 1))) · 0)) = ((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))))
96	2	flcld 13163	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (⌊‘𝑥) ∈ ℤ)
97		fzval3 13101	. . . . . . . . . . . . . 14 ⊢ ((⌊‘𝑥) ∈ ℤ → (1...(⌊‘𝑥)) = (1..^((⌊‘𝑥) + 1)))
98	96, 97	syl 17	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (1...(⌊‘𝑥)) = (1..^((⌊‘𝑥) + 1)))
99	98	eqcomd 2804	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (1..^((⌊‘𝑥) + 1)) = (1...(⌊‘𝑥)))
100	10	adantr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ⁺)
101		elfznn 12931	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
102	101	adantl 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
103	102	nnrpd 12417	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ⁺)
104	100, 103	rpdivcld 12436	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ⁺)
105	69	ffvelrni 6827	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 / 𝑛) ∈ ℝ⁺ → (𝑅‘(𝑥 / 𝑛)) ∈ ℝ)
106	104, 105	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘(𝑥 / 𝑛)) ∈ ℝ)
107	106	recnd 10658	. . . . . . . . . . . . . . . . . 18 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘(𝑥 / 𝑛)) ∈ ℂ)
108	107	abscld 14788	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑅‘(𝑥 / 𝑛))) ∈ ℝ)
109	108	recnd 10658	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑅‘(𝑥 / 𝑛))) ∈ ℂ)
110	3	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℝ⁺)
111	103, 110	rpaddcld 12434	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 + 1) ∈ ℝ⁺)
112	100, 111	rpdivcld 12436	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / (𝑛 + 1)) ∈ ℝ⁺)
113	69	ffvelrni 6827	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 / (𝑛 + 1)) ∈ ℝ⁺ → (𝑅‘(𝑥 / (𝑛 + 1))) ∈ ℝ)
114	112, 113	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘(𝑥 / (𝑛 + 1))) ∈ ℝ)
115	114	recnd 10658	. . . . . . . . . . . . . . . . . 18 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘(𝑥 / (𝑛 + 1))) ∈ ℂ)
116	115	abscld 14788	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) ∈ ℝ)
117	116	recnd 10658	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) ∈ ℂ)
118	109, 117	negsubdi2d 11002	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → -((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) = ((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))))
119	118	eqcomd 2804	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))) = -((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))))
120	102	nncnd 11641	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℂ)
121		1cnd 10625	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℂ)
122	120, 121	pncand 10987	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) − 1) = 𝑛)
123	122	fveq2d 6649	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘((𝑛 + 1) − 1)) = (𝑆‘𝑛))
124	122	fveq2d 6649	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇‘((𝑛 + 1) − 1)) = (𝑇‘𝑛))
125		rpre 12385	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℝ⁺ → 𝑛 ∈ ℝ)
126		eleq1 2877	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = 𝑛 → (𝑎 ∈ ℝ⁺ ↔ 𝑛 ∈ ℝ⁺))
127		id 22	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = 𝑛 → 𝑎 = 𝑛)
128		fveq2 6645	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = 𝑛 → (log‘𝑎) = (log‘𝑛))
129	127, 128	oveq12d 7153	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = 𝑛 → (𝑎 · (log‘𝑎)) = (𝑛 · (log‘𝑛)))
130	126, 129	ifbieq1d 4448	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = 𝑛 → if(𝑎 ∈ ℝ⁺, (𝑎 · (log‘𝑎)), 0) = if(𝑛 ∈ ℝ⁺, (𝑛 · (log‘𝑛)), 0))
131		ovex 7168	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 · (log‘𝑛)) ∈ V
132		c0ex 10624	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 ∈ V
133	131, 132	ifex 4473	. . . . . . . . . . . . . . . . . . . . 21 ⊢ if(𝑛 ∈ ℝ⁺, (𝑛 · (log‘𝑛)), 0) ∈ V
134	130, 81, 133	fvmpt 6745	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℝ → (𝑇‘𝑛) = if(𝑛 ∈ ℝ⁺, (𝑛 · (log‘𝑛)), 0))
135	125, 134	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ℝ⁺ → (𝑇‘𝑛) = if(𝑛 ∈ ℝ⁺, (𝑛 · (log‘𝑛)), 0))
136		iftrue 4431	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ℝ⁺ → if(𝑛 ∈ ℝ⁺, (𝑛 · (log‘𝑛)), 0) = (𝑛 · (log‘𝑛)))
137	135, 136	eqtrd 2833	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℝ⁺ → (𝑇‘𝑛) = (𝑛 · (log‘𝑛)))
138	103, 137	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇‘𝑛) = (𝑛 · (log‘𝑛)))
139	124, 138	eqtrd 2833	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇‘((𝑛 + 1) − 1)) = (𝑛 · (log‘𝑛)))
140	139	oveq2d 7151	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑇‘((𝑛 + 1) − 1))) = (2 · (𝑛 · (log‘𝑛))))
141	123, 140	oveq12d 7153	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))) = ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))
142	119, 141	oveq12d 7153	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))) · ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1))))) = (-((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))))
143	108, 116	resubcld 11057	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) ∈ ℝ)
144	143	recnd 10658	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) ∈ ℂ)
145	102	nnred 11640	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ)
146	78	ffvelrni 6827	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℝ → (𝑆‘𝑛) ∈ ℝ)
147	145, 146	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘𝑛) ∈ ℝ)
148	22	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 2 ∈ ℝ)
149	103	relogcld 25214	. . . . . . . . . . . . . . . . . 18 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘𝑛) ∈ ℝ)
150	145, 149	remulcld 10660	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 · (log‘𝑛)) ∈ ℝ)
151	148, 150	remulcld 10660	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑛 · (log‘𝑛))) ∈ ℝ)
152	147, 151	resubcld 11057	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))) ∈ ℝ)
153	152	recnd 10658	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))) ∈ ℂ)
154	144, 153	mulneg1d 11082	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (-((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) = -(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))))
155	142, 154	eqtrd 2833	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))) · ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1))))) = -(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))))
156	99, 155	sumeq12rdv 15056	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))(((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))) · ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1))))) = Σ𝑛 ∈ (1...(⌊‘𝑥))-(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))))
157		fzfid 13336	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (1...(⌊‘𝑥)) ∈ Fin)
158	143, 152	remulcld 10660	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) ∈ ℝ)
159	158	recnd 10658	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) ∈ ℂ)
160	157, 159	fsumneg 15134	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))-(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) = -Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))))
161	156, 160	eqtrd 2833	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))(((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))) · ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1))))) = -Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))))
162	95, 161	oveq12d 7153	. . . . . . . . 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 7143	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑛 → (𝑥 / 𝑚) = (𝑥 / 𝑛))
164	163	fveq2d 6649	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑛 → (𝑅‘(𝑥 / 𝑚)) = (𝑅‘(𝑥 / 𝑛)))
165	164	fveq2d 6649	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → (abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / 𝑛))))
166		fvoveq1 7158	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑛 → (𝑆‘(𝑚 − 1)) = (𝑆‘(𝑛 − 1)))
167		fvoveq1 7158	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑛 → (𝑇‘(𝑚 − 1)) = (𝑇‘(𝑛 − 1)))
168	167	oveq2d 7151	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑛 → (2 · (𝑇‘(𝑚 − 1))) = (2 · (𝑇‘(𝑛 − 1))))
169	166, 168	oveq12d 7153	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1)))))
170	165, 169	jca 515	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → ((abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / 𝑛))) ∧ ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1))))))
171		oveq2 7143	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (𝑛 + 1) → (𝑥 / 𝑚) = (𝑥 / (𝑛 + 1)))
172	171	fveq2d 6649	. . . . . . . . . . . . 13 ⊢ (𝑚 = (𝑛 + 1) → (𝑅‘(𝑥 / 𝑚)) = (𝑅‘(𝑥 / (𝑛 + 1))))
173	172	fveq2d 6649	. . . . . . . . . . . 12 ⊢ (𝑚 = (𝑛 + 1) → (abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / (𝑛 + 1)))))
174		fvoveq1 7158	. . . . . . . . . . . . 13 ⊢ (𝑚 = (𝑛 + 1) → (𝑆‘(𝑚 − 1)) = (𝑆‘((𝑛 + 1) − 1)))
175		fvoveq1 7158	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (𝑛 + 1) → (𝑇‘(𝑚 − 1)) = (𝑇‘((𝑛 + 1) − 1)))
176	175	oveq2d 7151	. . . . . . . . . . . . 13 ⊢ (𝑚 = (𝑛 + 1) → (2 · (𝑇‘(𝑚 − 1))) = (2 · (𝑇‘((𝑛 + 1) − 1))))
177	174, 176	oveq12d 7153	. . . . . . . . . . . 12 ⊢ (𝑚 = (𝑛 + 1) → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))))
178	173, 177	jca 515	. . . . . . . . . . 11 ⊢ (𝑚 = (𝑛 + 1) → ((abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) ∧ ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1))))))
179		oveq2 7143	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 1 → (𝑥 / 𝑚) = (𝑥 / 1))
180	179	fveq2d 6649	. . . . . . . . . . . . 13 ⊢ (𝑚 = 1 → (𝑅‘(𝑥 / 𝑚)) = (𝑅‘(𝑥 / 1)))
181	180	fveq2d 6649	. . . . . . . . . . . 12 ⊢ (𝑚 = 1 → (abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / 1))))
182		oveq1 7142	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 1 → (𝑚 − 1) = (1 − 1))
183		1m1e0 11697	. . . . . . . . . . . . . . . . 17 ⊢ (1 − 1) = 0
184	182, 183	eqtrdi 2849	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 1 → (𝑚 − 1) = 0)
185	184	fveq2d 6649	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 1 → (𝑆‘(𝑚 − 1)) = (𝑆‘0))
186		0re 10632	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ ℝ
187		fveq2 6645	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = 0 → (⌊‘𝑎) = (⌊‘0))
188		0z 11980	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 ∈ ℤ
189		flid 13173	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (0 ∈ ℤ → (⌊‘0) = 0)
190	188, 189	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⌊‘0) = 0
191	187, 190	eqtrdi 2849	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = 0 → (⌊‘𝑎) = 0)
192	191	oveq2d 7151	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 0 → (1...(⌊‘𝑎)) = (1...0))
193		fz10 12923	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1...0) = ∅
194	192, 193	eqtrdi 2849	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 0 → (1...(⌊‘𝑎)) = ∅)
195	194	sumeq1d 15050	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 0 → Σ𝑖 ∈ (1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))) = Σ𝑖 ∈ ∅ ((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))))
196		sum0 15070	. . . . . . . . . . . . . . . . . 18 ⊢ Σ𝑖 ∈ ∅ ((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))) = 0
197	195, 196	eqtrdi 2849	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 0 → Σ𝑖 ∈ (1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))) = 0)
198	197, 47, 132	fvmpt 6745	. . . . . . . . . . . . . . . 16 ⊢ (0 ∈ ℝ → (𝑆‘0) = 0)
199	186, 198	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (𝑆‘0) = 0
200	185, 199	eqtrdi 2849	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 1 → (𝑆‘(𝑚 − 1)) = 0)
201	184	fveq2d 6649	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 1 → (𝑇‘(𝑚 − 1)) = (𝑇‘0))
202		rpne0 12393	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 ∈ ℝ⁺ → 𝑎 ≠ 0)
203	202	necon2bi 3017	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 0 → ¬ 𝑎 ∈ ℝ⁺)
204	203	iffalsed 4436	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 0 → if(𝑎 ∈ ℝ⁺, (𝑎 · (log‘𝑎)), 0) = 0)
205	204, 81, 132	fvmpt 6745	. . . . . . . . . . . . . . . . . 18 ⊢ (0 ∈ ℝ → (𝑇‘0) = 0)
206	186, 205	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (𝑇‘0) = 0
207	201, 206	eqtrdi 2849	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 1 → (𝑇‘(𝑚 − 1)) = 0)
208	207	oveq2d 7151	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 1 → (2 · (𝑇‘(𝑚 − 1))) = (2 · 0))
209		2t0e0 11794	. . . . . . . . . . . . . . 15 ⊢ (2 · 0) = 0
210	208, 209	eqtrdi 2849	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 1 → (2 · (𝑇‘(𝑚 − 1))) = 0)
211	200, 210	oveq12d 7153	. . . . . . . . . . . . 13 ⊢ (𝑚 = 1 → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = (0 − 0))
212		0m0e0 11745	. . . . . . . . . . . . 13 ⊢ (0 − 0) = 0
213	211, 212	eqtrdi 2849	. . . . . . . . . . . 12 ⊢ (𝑚 = 1 → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = 0)
214	181, 213	jca 515	. . . . . . . . . . 11 ⊢ (𝑚 = 1 → ((abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / 1))) ∧ ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = 0))
215		oveq2 7143	. . . . . . . . . . . . . 14 ⊢ (𝑚 = ((⌊‘𝑥) + 1) → (𝑥 / 𝑚) = (𝑥 / ((⌊‘𝑥) + 1)))
216	215	fveq2d 6649	. . . . . . . . . . . . 13 ⊢ (𝑚 = ((⌊‘𝑥) + 1) → (𝑅‘(𝑥 / 𝑚)) = (𝑅‘(𝑥 / ((⌊‘𝑥) + 1))))
217	216	fveq2d 6649	. . . . . . . . . . . 12 ⊢ (𝑚 = ((⌊‘𝑥) + 1) → (abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))))
218		fvoveq1 7158	. . . . . . . . . . . . 13 ⊢ (𝑚 = ((⌊‘𝑥) + 1) → (𝑆‘(𝑚 − 1)) = (𝑆‘(((⌊‘𝑥) + 1) − 1)))
219		fvoveq1 7158	. . . . . . . . . . . . . 14 ⊢ (𝑚 = ((⌊‘𝑥) + 1) → (𝑇‘(𝑚 − 1)) = (𝑇‘(((⌊‘𝑥) + 1) − 1)))
220	219	oveq2d 7151	. . . . . . . . . . . . 13 ⊢ (𝑚 = ((⌊‘𝑥) + 1) → (2 · (𝑇‘(𝑚 − 1))) = (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1))))
221	218, 220	oveq12d 7153	. . . . . . . . . . . 12 ⊢ (𝑚 = ((⌊‘𝑥) + 1) → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1)))))
222	217, 221	jca 515	. . . . . . . . . . 11 ⊢ (𝑚 = ((⌊‘𝑥) + 1) → ((abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) ∧ ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1))))))
223		nnuz 12269	. . . . . . . . . . . 12 ⊢ ℕ = (ℤ_≥‘1)
224	15, 223	eleqtrdi 2900	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((⌊‘𝑥) + 1) ∈ (ℤ_≥‘1))
225	10	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 𝑥 ∈ ℝ⁺)
226		elfznn 12931	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ (1...((⌊‘𝑥) + 1)) → 𝑚 ∈ ℕ)
227	226	adantl 485	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 𝑚 ∈ ℕ)
228	227	nnrpd 12417	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 𝑚 ∈ ℝ⁺)
229	225, 228	rpdivcld 12436	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑥 / 𝑚) ∈ ℝ⁺)
230	69	ffvelrni 6827	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 / 𝑚) ∈ ℝ⁺ → (𝑅‘(𝑥 / 𝑚)) ∈ ℝ)
231	229, 230	syl 17	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑅‘(𝑥 / 𝑚)) ∈ ℝ)
232	231	recnd 10658	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑅‘(𝑥 / 𝑚)) ∈ ℂ)
233	232	abscld 14788	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (abs‘(𝑅‘(𝑥 / 𝑚))) ∈ ℝ)
234	233	recnd 10658	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (abs‘(𝑅‘(𝑥 / 𝑚))) ∈ ℂ)
235	227	nnred 11640	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 𝑚 ∈ ℝ)
236		1red 10631	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 1 ∈ ℝ)
237	235, 236	resubcld 11057	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑚 − 1) ∈ ℝ)
238	78	ffvelrni 6827	. . . . . . . . . . . . . 14 ⊢ ((𝑚 − 1) ∈ ℝ → (𝑆‘(𝑚 − 1)) ∈ ℝ)
239	237, 238	syl 17	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑆‘(𝑚 − 1)) ∈ ℝ)
240	22	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 2 ∈ ℝ)
241	87	ffvelrni 6827	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 − 1) ∈ ℝ → (𝑇‘(𝑚 − 1)) ∈ ℝ)
242	237, 241	syl 17	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑇‘(𝑚 − 1)) ∈ ℝ)
243	240, 242	remulcld 10660	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (2 · (𝑇‘(𝑚 − 1))) ∈ ℝ)
244	239, 243	resubcld 11057	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) ∈ ℝ)
245	244	recnd 10658	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) ∈ ℂ)
246	170, 178, 214, 222, 224, 234, 245	fsumparts 15153	. . . . . . . . . 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 10658	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘𝑛) ∈ ℂ)
248	87	ffvelrni 6827	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℝ → (𝑇‘𝑛) ∈ ℝ)
249	145, 248	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇‘𝑛) ∈ ℝ)
250	148, 249	remulcld 10660	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑇‘𝑛)) ∈ ℝ)
251	250	recnd 10658	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑇‘𝑛)) ∈ ℂ)
252		1red 10631	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℝ)
253	145, 252	resubcld 11057	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 − 1) ∈ ℝ)
254	78	ffvelrni 6827	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 − 1) ∈ ℝ → (𝑆‘(𝑛 − 1)) ∈ ℝ)
255	253, 254	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘(𝑛 − 1)) ∈ ℝ)
256	255	recnd 10658	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘(𝑛 − 1)) ∈ ℂ)
257	87	ffvelrni 6827	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 − 1) ∈ ℝ → (𝑇‘(𝑛 − 1)) ∈ ℝ)
258	253, 257	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇‘(𝑛 − 1)) ∈ ℝ)
259	148, 258	remulcld 10660	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑇‘(𝑛 − 1))) ∈ ℝ)
260	259	recnd 10658	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑇‘(𝑛 − 1))) ∈ ℂ)
261	247, 251, 256, 260	sub4d 11035	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆‘𝑛) − (2 · (𝑇‘𝑛))) − ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1))))) = (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − ((2 · (𝑇‘𝑛)) − (2 · (𝑇‘(𝑛 − 1))))))
262	124	oveq2d 7151	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑇‘((𝑛 + 1) − 1))) = (2 · (𝑇‘𝑛)))
263	123, 262	oveq12d 7153	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))) = ((𝑆‘𝑛) − (2 · (𝑇‘𝑛))))
264	263	oveq1d 7150	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))) − ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1))))) = (((𝑆‘𝑛) − (2 · (𝑇‘𝑛))) − ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1))))))
265		2cnd 11703	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 2 ∈ ℂ)
266	249	recnd 10658	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇‘𝑛) ∈ ℂ)
267	258	recnd 10658	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇‘(𝑛 − 1)) ∈ ℂ)
268	265, 266, 267	subdid 11085	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))) = ((2 · (𝑇‘𝑛)) − (2 · (𝑇‘(𝑛 − 1)))))
269	268	oveq2d 7151	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))) = (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − ((2 · (𝑇‘𝑛)) − (2 · (𝑇‘(𝑛 − 1))))))
270	261, 264, 269	3eqtr4d 2843	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))) − ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1))))) = (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))
271	270	oveq2d 7151	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))) − ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1)))))) = ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))))
272	99, 271	sumeq12rdv 15056	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))) − ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1)))))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))))
273	246, 272	eqtr3d 2835	. . . . . . . . 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 15082	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) ∈ ℂ)
275	93, 274	subnegd 10993	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) − -Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) = (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))))
276	162, 273, 275	3eqtr3rd 2842	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))))
277	10	relogcld 25214	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ∈ ℝ)
278	277	recnd 10658	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ∈ ℂ)
279	66, 278	mulcomd 10651	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) = ((log‘𝑥) · 𝑥))
280	276, 279	oveq12d 7153	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / ((log‘𝑥) · 𝑥)))
281	147, 255	resubcld 11057	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) ∈ ℝ)
282	249, 258	resubcld 11057	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))) ∈ ℝ)
283	148, 282	remulcld 10660	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))) ∈ ℝ)
284	281, 283	resubcld 11057	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))) ∈ ℝ)
285	108, 284	remulcld 10660	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) ∈ ℝ)
286	157, 285	fsumrecl 15083	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) ∈ ℝ)
287	286	recnd 10658	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) ∈ ℂ)
288	2, 8	rplogcld 25220	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ∈ ℝ⁺)
289	288	rpne0d 12424	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ≠ 0)
290	10	rpne0d 12424	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ≠ 0)
291	287, 278, 66, 289, 290	divdiv1d 11436	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥)) / 𝑥) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / ((log‘𝑥) · 𝑥)))
292	280, 291	eqtr4d 2836	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥)) / 𝑥))
293	292	oveq2d 7151	. . . . 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 10658	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑅‘𝑥) ∈ ℂ)
295	294	abscld 14788	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘(𝑅‘𝑥)) ∈ ℝ)
296	295, 277	remulcld 10660	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((abs‘(𝑅‘𝑥)) · (log‘𝑥)) ∈ ℝ)
297	108, 281	remulcld 10660	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) ∈ ℝ)
298	157, 297	fsumrecl 15083	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) ∈ ℝ)
299	298, 288	rerpdivcld 12450	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥)) ∈ ℝ)
300	296, 299	resubcld 11057	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) ∈ ℝ)
301	300	recnd 10658	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) ∈ ℂ)
302	287, 278, 289	divcld 11405	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥)) ∈ ℂ)
303	301, 302, 66, 290	divdird 11443	. . . . 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 10658	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((abs‘(𝑅‘𝑥)) · (log‘𝑥)) ∈ ℂ)
305	299	recnd 10658	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥)) ∈ ℂ)
306	304, 305, 302	subsubd 11014	. . . . . . 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 11703	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 2 ∈ ℂ)
308	266, 267	subcld 10986	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))) ∈ ℂ)
309	109, 308	mulcld 10650	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))) ∈ ℂ)
310	157, 307, 309	fsummulc2 15131	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(2 · ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))
311	281	recnd 10658	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) ∈ ℂ)
312	265, 308	mulcld 10650	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))) ∈ ℂ)
313	311, 312	nncand 10991	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) = (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))
314	313	oveq2d 7151	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) = ((abs‘(𝑅‘(𝑥 / 𝑛))) · (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))
315	284	recnd 10658	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))) ∈ ℂ)
316	109, 311, 315	subdid 11085	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) = (((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) − ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))))
317	109, 265, 308	mul12d 10838	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))) = (2 · ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))
318	314, 316, 317	3eqtr3d 2841	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) − ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) = (2 · ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))
319	318	sumeq2dv 15052	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) − ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(2 · ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))
320	297	recnd 10658	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) ∈ ℂ)
321	285	recnd 10658	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) ∈ ℂ)
322	157, 320, 321	fsumsub 15135	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) − ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))))
323	310, 319, 322	3eqtr2rd 2840	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) = (2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))
324	323	oveq1d 7150	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) / (log‘𝑥)) = ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))) / (log‘𝑥)))
325	298	recnd 10658	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) ∈ ℂ)
326	325, 287, 278, 289	divsubdird 11444	. . . . . . . . 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 10660	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))) ∈ ℝ)
328	157, 327	fsumrecl 15083	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))) ∈ ℝ)
329	328	recnd 10658	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))) ∈ ℂ)
330	307, 329, 278, 289	div23d 11442	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))) / (log‘𝑥)) = ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))
331	324, 326, 330	3eqtr3d 2841	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥))) = ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))
332	331	oveq2d 7151	. . . . . . 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 2835	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥))) = (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))))
334	333	oveq1d 7150	. . . . 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 2839	. . . 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 5125	. . 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 12450	. . . 4 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥) ∈ ℝ)
338	157, 158	fsumrecl 15083	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) ∈ ℝ)
339	92, 338	readdcld 10659	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) ∈ ℝ)
340	10, 288	rpmulcld 12435	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ∈ ℝ⁺)
341	339, 340	rerpdivcld 12450	. . . 4 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))) ∈ ℝ)
342	47, 18	pntrlog2bndlem1 26161	. . . . 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 12421	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ∈ ℂ)
345	340	rpne0d 12424	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ≠ 0)
346	93, 274, 344, 345	divdird 11443	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))) = ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) / (𝑥 · (log‘𝑥))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥)))))
347	91	recnd 10658	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) ∈ ℂ)
348	43, 347, 344, 345	divassd 11440	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) / (𝑥 · (log‘𝑥))) = ((𝑥 / ((⌊‘𝑥) + 1)) · (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))))
349	348	oveq1d 7150	. . . . . . 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 2833	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))) = (((𝑥 / ((⌊‘𝑥) + 1)) · (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥)))))
351	350	mpteq2dva 5125	. . . . 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 12450	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥))) ∈ ℝ)
353	21, 352	remulcld 10660	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑥 / ((⌊‘𝑥) + 1)) · (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) ∈ ℝ)
354	338, 340	rerpdivcld 12450	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥))) ∈ ℝ)
355		ioossre 12786	. . . . . . . . 9 ⊢ (1(,)+∞) ⊆ ℝ
356	355	a1i 11	. . . . . . . 8 ⊢ (⊤ → (1(,)+∞) ⊆ ℝ)
357		1red 10631	. . . . . . . 8 ⊢ (⊤ → 1 ∈ ℝ)
358	21, 5, 30	ltled 10777	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 / ((⌊‘𝑥) + 1)) ≤ 1)
359	358	adantrr 716	. . . . . . . 8 ⊢ ((⊤ ∧ (𝑥 ∈ (1(,)+∞) ∧ 1 ≤ 𝑥)) → (𝑥 / ((⌊‘𝑥) + 1)) ≤ 1)
360	356, 21, 357, 357, 359	ello1d 14872	. . . . . . 7 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (𝑥 / ((⌊‘𝑥) + 1))) ∈ ≤𝑂(1))
361	80	recnd 10658	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑆‘𝑥) ∈ ℂ)
362	90	recnd 10658	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (2 · (𝑇‘(⌊‘𝑥))) ∈ ℂ)
363	361, 362, 344, 345	divsubdird 11444	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥))) = (((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) − ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥)))))
364	363	mpteq2dva 5125	. . . . . . . . 9 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) = (𝑥 ∈ (1(,)+∞) ↦ (((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) − ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥))))))
365	80, 340	rerpdivcld 12450	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) ∈ ℝ)
366	90, 340	rerpdivcld 12450	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥))) ∈ ℝ)
367		2cnd 11703	. . . . . . . . . . . 12 ⊢ (⊤ → 2 ∈ ℂ)
368		o1const 14968	. . . . . . . . . . . 12 ⊢ (((1(,)+∞) ⊆ ℝ ∧ 2 ∈ ℂ) → (𝑥 ∈ (1(,)+∞) ↦ 2) ∈ 𝑂(1))
369	355, 367, 368	sylancr 590	. . . . . . . . . . 11 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ 2) ∈ 𝑂(1))
370	365	recnd 10658	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) ∈ ℂ)
371	80, 10	rerpdivcld 12450	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑆‘𝑥) / 𝑥) ∈ ℝ)
372	371	recnd 10658	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑆‘𝑥) / 𝑥) ∈ ℂ)
373	307, 278	mulcld 10650	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (2 · (log‘𝑥)) ∈ ℂ)
374	372, 373, 278, 289	divsubdird 11444	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥))) / (log‘𝑥)) = ((((𝑆‘𝑥) / 𝑥) / (log‘𝑥)) − ((2 · (log‘𝑥)) / (log‘𝑥))))
375	23, 277	remulcld 10660	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (2 · (log‘𝑥)) ∈ ℝ)
376	371, 375	resubcld 11057	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥))) ∈ ℝ)
377	376	recnd 10658	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥))) ∈ ℂ)
378	377, 278, 289	divrecd 11408	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥))) / (log‘𝑥)) = ((((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥))) · (1 / (log‘𝑥))))
379	361, 66, 278, 290, 289	divdiv1d 11436	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑆‘𝑥) / 𝑥) / (log‘𝑥)) = ((𝑆‘𝑥) / (𝑥 · (log‘𝑥))))
380	307, 278, 289	divcan4d 11411	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 · (log‘𝑥)) / (log‘𝑥)) = 2)
381	379, 380	oveq12d 7153	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((𝑆‘𝑥) / 𝑥) / (log‘𝑥)) − ((2 · (log‘𝑥)) / (log‘𝑥))) = (((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) − 2))
382	374, 378, 381	3eqtr3rd 2842	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) − 2) = ((((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥))) · (1 / (log‘𝑥))))
383	382	mpteq2dva 5125	. . . . . . . . . . . . 13 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) − 2)) = (𝑥 ∈ (1(,)+∞) ↦ ((((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥))) · (1 / (log‘𝑥)))))
384	5, 288	rerpdivcld 12450	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (1 / (log‘𝑥)) ∈ ℝ)
385	10	ex 416	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) → 𝑥 ∈ ℝ⁺))
386	385	ssrdv 3921	. . . . . . . . . . . . . . 15 ⊢ (⊤ → (1(,)+∞) ⊆ ℝ⁺)
387	47	selbergs 26158	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℝ⁺ ↦ (((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥)))) ∈ 𝑂(1)
388	387	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ (((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥)))) ∈ 𝑂(1))
389	386, 388	o1res2 14912	. . . . . . . . . . . . . 14 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥)))) ∈ 𝑂(1))
390		divlogrlim 25226	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (1(,)+∞) ↦ (1 / (log‘𝑥))) ⇝_𝑟 0
391		rlimo1 14965	. . . . . . . . . . . . . . 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 14973	. . . . . . . . . . . . 13 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥))) · (1 / (log‘𝑥)))) ∈ 𝑂(1))
394	383, 393	eqeltrd 2890	. . . . . . . . . . . 12 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) − 2)) ∈ 𝑂(1))
395	370, 307, 394	o1dif 14978	. . . . . . . . . . 11 ⊢ (⊤ → ((𝑥 ∈ (1(,)+∞) ↦ ((𝑆‘𝑥) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1) ↔ (𝑥 ∈ (1(,)+∞) ↦ 2) ∈ 𝑂(1)))
396	369, 395	mpbird 260	. . . . . . . . . 10 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((𝑆‘𝑥) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1))
397	22	a1i 11	. . . . . . . . . . . 12 ⊢ (⊤ → 2 ∈ ℝ)
398	2, 277	remulcld 10660	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ∈ ℝ)
399		2rp 12382	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℝ⁺
400	399	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 2 ∈ ℝ⁺)
401	400	rpge0d 12423	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ 2)
402		flge1nn 13186	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) → (⌊‘𝑥) ∈ ℕ)
403	2, 9, 402	syl2anc 587	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (⌊‘𝑥) ∈ ℕ)
404	403	nnrpd 12417	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (⌊‘𝑥) ∈ ℝ⁺)
405		rpre 12385	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⌊‘𝑥) ∈ ℝ⁺ → (⌊‘𝑥) ∈ ℝ)
406		eleq1 2877	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = (⌊‘𝑥) → (𝑎 ∈ ℝ⁺ ↔ (⌊‘𝑥) ∈ ℝ⁺))
407		id 22	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = (⌊‘𝑥) → 𝑎 = (⌊‘𝑥))
408		fveq2 6645	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = (⌊‘𝑥) → (log‘𝑎) = (log‘(⌊‘𝑥)))
409	407, 408	oveq12d 7153	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = (⌊‘𝑥) → (𝑎 · (log‘𝑎)) = ((⌊‘𝑥) · (log‘(⌊‘𝑥))))
410	406, 409	ifbieq1d 4448	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = (⌊‘𝑥) → if(𝑎 ∈ ℝ⁺, (𝑎 · (log‘𝑎)), 0) = if((⌊‘𝑥) ∈ ℝ⁺, ((⌊‘𝑥) · (log‘(⌊‘𝑥))), 0))
411		ovex 7168	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((⌊‘𝑥) · (log‘(⌊‘𝑥))) ∈ V
412	411, 132	ifex 4473	. . . . . . . . . . . . . . . . . . . 20 ⊢ if((⌊‘𝑥) ∈ ℝ⁺, ((⌊‘𝑥) · (log‘(⌊‘𝑥))), 0) ∈ V
413	410, 81, 412	fvmpt 6745	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⌊‘𝑥) ∈ ℝ → (𝑇‘(⌊‘𝑥)) = if((⌊‘𝑥) ∈ ℝ⁺, ((⌊‘𝑥) · (log‘(⌊‘𝑥))), 0))
414	405, 413	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((⌊‘𝑥) ∈ ℝ⁺ → (𝑇‘(⌊‘𝑥)) = if((⌊‘𝑥) ∈ ℝ⁺, ((⌊‘𝑥) · (log‘(⌊‘𝑥))), 0))
415		iftrue 4431	. . . . . . . . . . . . . . . . . 18 ⊢ ((⌊‘𝑥) ∈ ℝ⁺ → if((⌊‘𝑥) ∈ ℝ⁺, ((⌊‘𝑥) · (log‘(⌊‘𝑥))), 0) = ((⌊‘𝑥) · (log‘(⌊‘𝑥))))
416	414, 415	eqtrd 2833	. . . . . . . . . . . . . . . . 17 ⊢ ((⌊‘𝑥) ∈ ℝ⁺ → (𝑇‘(⌊‘𝑥)) = ((⌊‘𝑥) · (log‘(⌊‘𝑥))))
417	404, 416	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑇‘(⌊‘𝑥)) = ((⌊‘𝑥) · (log‘(⌊‘𝑥))))
418	404	relogcld 25214	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (log‘(⌊‘𝑥)) ∈ ℝ)
419	13	nn0ge0d 11946	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ (⌊‘𝑥))
420	403	nnge1d 11673	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 ≤ (⌊‘𝑥))
421	46, 420	logge0d 25221	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ (log‘(⌊‘𝑥)))
422		flle 13164	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℝ → (⌊‘𝑥) ≤ 𝑥)
423	2, 422	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (⌊‘𝑥) ≤ 𝑥)
424	404, 10	logled 25218	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((⌊‘𝑥) ≤ 𝑥 ↔ (log‘(⌊‘𝑥)) ≤ (log‘𝑥)))
425	423, 424	mpbid 235	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (log‘(⌊‘𝑥)) ≤ (log‘𝑥))
426	46, 2, 418, 277, 419, 421, 423, 425	lemul12ad 11571	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((⌊‘𝑥) · (log‘(⌊‘𝑥))) ≤ (𝑥 · (log‘𝑥)))
427	417, 426	eqbrtrd 5052	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑇‘(⌊‘𝑥)) ≤ (𝑥 · (log‘𝑥)))
428	89, 398, 23, 401, 427	lemul2ad 11569	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (2 · (𝑇‘(⌊‘𝑥))) ≤ (2 · (𝑥 · (log‘𝑥))))
429	90, 23, 340	ledivmul2d 12473	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥))) ≤ 2 ↔ (2 · (𝑇‘(⌊‘𝑥))) ≤ (2 · (𝑥 · (log‘𝑥)))))
430	428, 429	mpbird 260	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥))) ≤ 2)
431	430	adantrr 716	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ (𝑥 ∈ (1(,)+∞) ∧ 1 ≤ 𝑥)) → ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥))) ≤ 2)
432	356, 366, 357, 397, 431	ello1d 14872	. . . . . . . . . . 11 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥)))) ∈ ≤𝑂(1))
433		0red 10633	. . . . . . . . . . . 12 ⊢ (⊤ → 0 ∈ ℝ)
434	46, 418, 419, 421	mulge0d 11206	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ ((⌊‘𝑥) · (log‘(⌊‘𝑥))))
435	434, 417	breqtrrd 5058	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ (𝑇‘(⌊‘𝑥)))
436	23, 89, 401, 435	mulge0d 11206	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ (2 · (𝑇‘(⌊‘𝑥))))
437	90, 340, 436	divge0d 12459	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥))))
438	366, 433, 437	o1lo12 14887	. . . . . . . . . . 11 ⊢ (⊤ → ((𝑥 ∈ (1(,)+∞) ↦ ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1) ↔ (𝑥 ∈ (1(,)+∞) ↦ ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥)))) ∈ ≤𝑂(1)))
439	432, 438	mpbird 260	. . . . . . . . . 10 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1))
440	365, 366, 396, 439	o1sub2 14974	. . . . . . . . 9 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) − ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥))))) ∈ 𝑂(1))
441	364, 440	eqeltrd 2890	. . . . . . . 8 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1))
442	352, 441	o1lo1d 14888	. . . . . . 7 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) ∈ ≤𝑂(1))
443	21, 352, 360, 442, 41	lo1mul 14976	. . . . . 6 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((𝑥 / ((⌊‘𝑥) + 1)) · (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥))))) ∈ ≤𝑂(1))
444	47	selbergsb 26159	. . . . . . . 8 ⊢ ∃𝑐 ∈ ℝ⁺ ∀𝑦 ∈ (1[,)+∞)(abs‘(((𝑆‘𝑦) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝑐
445		simpl 486	. . . . . . . . . 10 ⊢ ((𝑐 ∈ ℝ⁺ ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘(((𝑆‘𝑦) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝑐) → 𝑐 ∈ ℝ⁺)
446		simpr 488	. . . . . . . . . 10 ⊢ ((𝑐 ∈ ℝ⁺ ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘(((𝑆‘𝑦) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝑐) → ∀𝑦 ∈ (1[,)+∞)(abs‘(((𝑆‘𝑦) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝑐)
447	47, 18, 445, 446	pntrlog2bndlem3 26163	. . . . . . . . 9 ⊢ ((𝑐 ∈ ℝ⁺ ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘(((𝑆‘𝑦) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝑐) → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1))
448	447	rexlimiva 3240	. . . . . . . 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 14888	. . . . . 6 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥)))) ∈ ≤𝑂(1))
451	353, 354, 443, 450	lo1add 14975	. . . . 5 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((𝑥 / ((⌊‘𝑥) + 1)) · (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥))))) ∈ ≤𝑂(1))
452	351, 451	eqeltrd 2890	. . . 4 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥)))) ∈ ≤𝑂(1))
453	337, 341, 343, 452	lo1add 14975	. . 3 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥) + ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))))) ∈ ≤𝑂(1))
454	336, 453	eqeltrrd 2891	. 2 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / 𝑥)) ∈ ≤𝑂(1))
455	454	mptru 1545	1 ⊢ (𝑥 ∈ (1(,)+∞) ↦ ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / 𝑥)) ∈ ≤𝑂(1)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 ↔ wb 209 ∧ wa 399 = wceq 1538 ⊤wtru 1539 ∈ wcel 2111 ∀wral 3106 ∃wrex 3107 {crab 3110 ⊆ wss 3881 ∅c0 4243 ifcif 4425 class class class wbr 5030 ↦ cmpt 5110 ‘cfv 6324 (class class class)co 7135 ℂcc 10524 ℝcr 10525 0cc0 10526 1c1 10527 + caddc 10529 · cmul 10531 +∞cpnf 10661 < clt 10664 ≤ cle 10665 − cmin 10859 -cneg 10860 / cdiv 11286 ℕcn 11625 2c2 11680 ℕ₀cn0 11885 ℤcz 11969 ℤ_≥cuz 12231 ℝ⁺crp 12377 (,)cioo 12726 [,)cico 12728 ...cfz 12885 ..^cfzo 13028 ⌊cfl 13155 abscabs 14585 ⇝_𝑟 crli 14834 𝑂(1)co1 14835 ≤𝑂(1)clo1 14836 Σcsu 15034 ∥ cdvds 15599 logclog 25146 Λcvma 25677 ψcchp 25678

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-rep 5154 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 ax-un 7441 ax-inf2 9088 ax-cnex 10582 ax-resscn 10583 ax-1cn 10584 ax-icn 10585 ax-addcl 10586 ax-addrcl 10587 ax-mulcl 10588 ax-mulrcl 10589 ax-mulcom 10590 ax-addass 10591 ax-mulass 10592 ax-distr 10593 ax-i2m1 10594 ax-1ne0 10595 ax-1rid 10596 ax-rnegex 10597 ax-rrecex 10598 ax-cnre 10599 ax-pre-lttri 10600 ax-pre-lttrn 10601 ax-pre-ltadd 10602 ax-pre-mulgt0 10603 ax-pre-sup 10604 ax-addf 10605 ax-mulf 10606

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-fal 1551 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ne 2988 df-nel 3092 df-ral 3111 df-rex 3112 df-reu 3113 df-rmo 3114 df-rab 3115 df-v 3443 df-sbc 3721 df-csb 3829 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-pss 3900 df-nul 4244 df-if 4426 df-pw 4499 df-sn 4526 df-pr 4528 df-tp 4530 df-op 4532 df-uni 4801 df-int 4839 df-iun 4883 df-iin 4884 df-disj 4996 df-br 5031 df-opab 5093 df-mpt 5111 df-tr 5137 df-id 5425 df-eprel 5430 df-po 5438 df-so 5439 df-fr 5478 df-se 5479 df-we 5480 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-pred 6116 df-ord 6162 df-on 6163 df-lim 6164 df-suc 6165 df-iota 6283 df-fun 6326 df-fn 6327 df-f 6328 df-f1 6329 df-fo 6330 df-f1o 6331 df-fv 6332 df-isom 6333 df-riota 7093 df-ov 7138 df-oprab 7139 df-mpo 7140 df-of 7389 df-om 7561 df-1st 7671 df-2nd 7672 df-supp 7814 df-wrecs 7930 df-recs 7991 df-rdg 8029 df-1o 8085 df-2o 8086 df-oadd 8089 df-er 8272 df-map 8391 df-pm 8392 df-ixp 8445 df-en 8493 df-dom 8494 df-sdom 8495 df-fin 8496 df-fsupp 8818 df-fi 8859 df-sup 8890 df-inf 8891 df-oi 8958 df-dju 9314 df-card 9352 df-pnf 10666 df-mnf 10667 df-xr 10668 df-ltxr 10669 df-le 10670 df-sub 10861 df-neg 10862 df-div 11287 df-nn 11626 df-2 11688 df-3 11689 df-4 11690 df-5 11691 df-6 11692 df-7 11693 df-8 11694 df-9 11695 df-n0 11886 df-xnn0 11956 df-z 11970 df-dec 12087 df-uz 12232 df-q 12337 df-rp 12378 df-xneg 12495 df-xadd 12496 df-xmul 12497 df-ioo 12730 df-ioc 12731 df-ico 12732 df-icc 12733 df-fz 12886 df-fzo 13029 df-fl 13157 df-mod 13233 df-seq 13365 df-exp 13426 df-fac 13630 df-bc 13659 df-hash 13687 df-shft 14418 df-cj 14450 df-re 14451 df-im 14452 df-sqrt 14586 df-abs 14587 df-limsup 14820 df-clim 14837 df-rlim 14838 df-o1 14839 df-lo1 14840 df-sum 15035 df-ef 15413 df-e 15414 df-sin 15415 df-cos 15416 df-tan 15417 df-pi 15418 df-dvds 15600 df-gcd 15834 df-prm 16006 df-pc 16164 df-struct 16477 df-ndx 16478 df-slot 16479 df-base 16481 df-sets 16482 df-ress 16483 df-plusg 16570 df-mulr 16571 df-starv 16572 df-sca 16573 df-vsca 16574 df-ip 16575 df-tset 16576 df-ple 16577 df-ds 16579 df-unif 16580 df-hom 16581 df-cco 16582 df-rest 16688 df-topn 16689 df-0g 16707 df-gsum 16708 df-topgen 16709 df-pt 16710 df-prds 16713 df-xrs 16767 df-qtop 16772 df-imas 16773 df-xps 16775 df-mre 16849 df-mrc 16850 df-acs 16852 df-mgm 17844 df-sgrp 17893 df-mnd 17904 df-submnd 17949 df-mulg 18217 df-cntz 18439 df-cmn 18900 df-psmet 20083 df-xmet 20084 df-met 20085 df-bl 20086 df-mopn 20087 df-fbas 20088 df-fg 20089 df-cnfld 20092 df-top 21499 df-topon 21516 df-topsp 21538 df-bases 21551 df-cld 21624 df-ntr 21625 df-cls 21626 df-nei 21703 df-lp 21741 df-perf 21742 df-cn 21832 df-cnp 21833 df-haus 21920 df-cmp 21992 df-tx 22167 df-hmeo 22360 df-fil 22451 df-fm 22543 df-flim 22544 df-flf 22545 df-xms 22927 df-ms 22928 df-tms 22929 df-cncf 23483 df-limc 24469 df-dv 24470 df-ulm 24972 df-log 25148 df-cxp 25149 df-atan 25453 df-em 25578 df-cht 25682 df-vma 25683 df-chp 25684 df-ppi 25685 df-mu 25686

This theorem is referenced by: pntrlog2bndlem5 26165

W3C validator