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 27548

Description: Lemma for pntrlog2bnd 27552. 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 13397	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (1(,)+∞) → 𝑥 ∈ ℝ)
2	1	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ∈ ℝ)
3		1rp 13017	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1 ∈ ℝ⁺
4	3	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 ∈ ℝ⁺)
5		1red 11241	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 ∈ ℝ)
6		eliooord 13427	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (1(,)+∞) → (1 < 𝑥 ∧ 𝑥 < +∞))
7	6	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (1 < 𝑥 ∧ 𝑥 < +∞))
8	7	simpld 494	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 < 𝑥)
9	5, 2, 8	ltled 11388	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 ≤ 𝑥)
10	2, 4, 9	rpgecld 13095	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ∈ ℝ⁺)
11	10	rprege0d 13063	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
12		flge0nn0 13842	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → (⌊‘𝑥) ∈ ℕ₀)
13	11, 12	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (⌊‘𝑥) ∈ ℕ₀)
14		nn0p1nn 12545	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⌊‘𝑥) ∈ ℕ₀ → ((⌊‘𝑥) + 1) ∈ ℕ)
15	13, 14	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((⌊‘𝑥) + 1) ∈ ℕ)
16	15	nnrpd 13054	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((⌊‘𝑥) + 1) ∈ ℝ⁺)
17	10, 16	rpdivcld 13073	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 / ((⌊‘𝑥) + 1)) ∈ ℝ⁺)
18		pntrlog2bnd.r	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑅 = (𝑎 ∈ ℝ⁺ ↦ ((ψ‘𝑎) − 𝑎))
19	18	pntrval 27530	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 / ((⌊‘𝑥) + 1)) ∈ ℝ⁺ → (𝑅‘(𝑥 / ((⌊‘𝑥) + 1))) = ((ψ‘(𝑥 / ((⌊‘𝑥) + 1))) − (𝑥 / ((⌊‘𝑥) + 1))))
20	17, 19	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑅‘(𝑥 / ((⌊‘𝑥) + 1))) = ((ψ‘(𝑥 / ((⌊‘𝑥) + 1))) − (𝑥 / ((⌊‘𝑥) + 1))))
21	2, 15	nndivred 12299	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 / ((⌊‘𝑥) + 1)) ∈ ℝ)
22		2re 12319	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 ∈ ℝ
23	22	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 2 ∈ ℝ)
24		flltp1 13822	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℝ → 𝑥 < ((⌊‘𝑥) + 1))
25	2, 24	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 < ((⌊‘𝑥) + 1))
26	15	nncnd 12261	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((⌊‘𝑥) + 1) ∈ ℂ)
27	26	mulridd 11257	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((⌊‘𝑥) + 1) · 1) = ((⌊‘𝑥) + 1))
28	25, 27	breqtrrd 5152	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 < (((⌊‘𝑥) + 1) · 1))
29	2, 5, 16	ltdivmuld 13107	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑥 / ((⌊‘𝑥) + 1)) < 1 ↔ 𝑥 < (((⌊‘𝑥) + 1) · 1)))
30	28, 29	mpbird 257	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 / ((⌊‘𝑥) + 1)) < 1)
31		1lt2 12416	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1 < 2
32	31	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 < 2)
33	21, 5, 23, 30, 32	lttrd 11401	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 / ((⌊‘𝑥) + 1)) < 2)
34		chpeq0 27176	. . . . . . . . . . . . . . . . . . 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 7425	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((ψ‘(𝑥 / ((⌊‘𝑥) + 1))) − (𝑥 / ((⌊‘𝑥) + 1))) = (0 − (𝑥 / ((⌊‘𝑥) + 1))))
38	20, 37	eqtrd 2771	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑅‘(𝑥 / ((⌊‘𝑥) + 1))) = (0 − (𝑥 / ((⌊‘𝑥) + 1))))
39	38	fveq2d 6885	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) = (abs‘(0 − (𝑥 / ((⌊‘𝑥) + 1)))))
40		0red 11243	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 0 ∈ ℝ)
41	17	rpge0d 13060	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ (𝑥 / ((⌊‘𝑥) + 1)))
42	40, 21, 41	abssuble0d 15456	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘(0 − (𝑥 / ((⌊‘𝑥) + 1)))) = ((𝑥 / ((⌊‘𝑥) + 1)) − 0))
43	21	recnd 11268	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 / ((⌊‘𝑥) + 1)) ∈ ℂ)
44	43	subid1d 11588	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑥 / ((⌊‘𝑥) + 1)) − 0) = (𝑥 / ((⌊‘𝑥) + 1)))
45	39, 42, 44	3eqtrd 2775	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) = (𝑥 / ((⌊‘𝑥) + 1)))
46	13	nn0red 12568	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (⌊‘𝑥) ∈ ℝ)
47		pntsval.1	. . . . . . . . . . . . . . . . 17 ⊢ 𝑆 = (𝑎 ∈ ℝ ↦ Σ𝑖 ∈ (1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))))
48	47	pntsval2 27544	. . . . . . . . . . . . . . . 16 ⊢ ((⌊‘𝑥) ∈ ℝ → (𝑆‘(⌊‘𝑥)) = Σ𝑛 ∈ (1...(⌊‘(⌊‘𝑥)))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))))
49	46, 48	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑆‘(⌊‘𝑥)) = Σ𝑛 ∈ (1...(⌊‘(⌊‘𝑥)))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))))
50	13	nn0cnd 12569	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (⌊‘𝑥) ∈ ℂ)
51		1cnd 11235	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 ∈ ℂ)
52	50, 51	pncand 11600	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((⌊‘𝑥) + 1) − 1) = (⌊‘𝑥))
53	52	fveq2d 6885	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑆‘(((⌊‘𝑥) + 1) − 1)) = (𝑆‘(⌊‘𝑥)))
54	47	pntsval2 27544	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℝ → (𝑆‘𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))))
55	2, 54	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑆‘𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))))
56		flidm 13831	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℝ → (⌊‘(⌊‘𝑥)) = (⌊‘𝑥))
57	2, 56	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (⌊‘(⌊‘𝑥)) = (⌊‘𝑥))
58	57	oveq2d 7426	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (1...(⌊‘(⌊‘𝑥))) = (1...(⌊‘𝑥)))
59	58	sumeq1d 15721	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘(⌊‘𝑥)))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))))
60	55, 59	eqtr4d 2774	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑆‘𝑥) = Σ𝑛 ∈ (1...(⌊‘(⌊‘𝑥)))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))))
61	49, 53, 60	3eqtr4d 2781	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑆‘(((⌊‘𝑥) + 1) − 1)) = (𝑆‘𝑥))
62	52	fveq2d 6885	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑇‘(((⌊‘𝑥) + 1) − 1)) = (𝑇‘(⌊‘𝑥)))
63	62	oveq2d 7426	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1))) = (2 · (𝑇‘(⌊‘𝑥))))
64	61, 63	oveq12d 7428	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1)))) = ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))))
65	45, 64	oveq12d 7428	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) · ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1))))) = ((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))))
66	2	recnd 11268	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ∈ ℂ)
67	66	div1d 12014	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 / 1) = 𝑥)
68	67	fveq2d 6885	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑅‘(𝑥 / 1)) = (𝑅‘𝑥))
69	18	pntrf 27531	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑅:ℝ⁺⟶ℝ
70	69	ffvelcdmi 7078	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℝ⁺ → (𝑅‘𝑥) ∈ ℝ)
71	10, 70	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑅‘𝑥) ∈ ℝ)
72	68, 71	eqeltrd 2835	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑅‘(𝑥 / 1)) ∈ ℝ)
73	72	recnd 11268	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑅‘(𝑥 / 1)) ∈ ℂ)
74	73	abscld 15460	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘(𝑅‘(𝑥 / 1))) ∈ ℝ)
75	74	recnd 11268	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘(𝑅‘(𝑥 / 1))) ∈ ℂ)
76	75	mul01d 11439	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((abs‘(𝑅‘(𝑥 / 1))) · 0) = 0)
77	65, 76	oveq12d 7428	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) · ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1))))) − ((abs‘(𝑅‘(𝑥 / 1))) · 0)) = (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) − 0))
78	47	pntsf 27541	. . . . . . . . . . . . . . . . 17 ⊢ 𝑆:ℝ⟶ℝ
79	78	ffvelcdmi 7078	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℝ → (𝑆‘𝑥) ∈ ℝ)
80	2, 79	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑆‘𝑥) ∈ ℝ)
81		pntrlog2bnd.t	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑇 = (𝑎 ∈ ℝ ↦ if(𝑎 ∈ ℝ⁺, (𝑎 · (log‘𝑎)), 0))
82		relogcl 26541	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 ∈ ℝ⁺ → (log‘𝑎) ∈ ℝ)
83		remulcl 11219	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑎 ∈ ℝ ∧ (log‘𝑎) ∈ ℝ) → (𝑎 · (log‘𝑎)) ∈ ℝ)
84	82, 83	sylan2 593	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 ∈ ℝ ∧ 𝑎 ∈ ℝ⁺) → (𝑎 · (log‘𝑎)) ∈ ℝ)
85		0red 11243	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 ∈ ℝ ∧ ¬ 𝑎 ∈ ℝ⁺) → 0 ∈ ℝ)
86	84, 85	ifclda 4541	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 ∈ ℝ → if(𝑎 ∈ ℝ⁺, (𝑎 · (log‘𝑎)), 0) ∈ ℝ)
87	81, 86	fmpti 7107	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑇:ℝ⟶ℝ
88	87	ffvelcdmi 7078	. . . . . . . . . . . . . . . . 17 ⊢ ((⌊‘𝑥) ∈ ℝ → (𝑇‘(⌊‘𝑥)) ∈ ℝ)
89	46, 88	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑇‘(⌊‘𝑥)) ∈ ℝ)
90	23, 89	remulcld 11270	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (2 · (𝑇‘(⌊‘𝑥))) ∈ ℝ)
91	80, 90	resubcld 11670	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) ∈ ℝ)
92	21, 91	remulcld 11270	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) ∈ ℝ)
93	92	recnd 11268	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) ∈ ℂ)
94	93	subid1d 11588	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) − 0) = ((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))))
95	77, 94	eqtrd 2771	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) · ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1))))) − ((abs‘(𝑅‘(𝑥 / 1))) · 0)) = ((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))))
96	2	flcld 13820	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (⌊‘𝑥) ∈ ℤ)
97		fzval3 13755	. . . . . . . . . . . . . 14 ⊢ ((⌊‘𝑥) ∈ ℤ → (1...(⌊‘𝑥)) = (1..^((⌊‘𝑥) + 1)))
98	96, 97	syl 17	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (1...(⌊‘𝑥)) = (1..^((⌊‘𝑥) + 1)))
99	98	eqcomd 2742	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (1..^((⌊‘𝑥) + 1)) = (1...(⌊‘𝑥)))
100	10	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ⁺)
101		elfznn 13575	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
102	101	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
103	102	nnrpd 13054	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ⁺)
104	100, 103	rpdivcld 13073	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ⁺)
105	69	ffvelcdmi 7078	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 / 𝑛) ∈ ℝ⁺ → (𝑅‘(𝑥 / 𝑛)) ∈ ℝ)
106	104, 105	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘(𝑥 / 𝑛)) ∈ ℝ)
107	106	recnd 11268	. . . . . . . . . . . . . . . . . 18 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘(𝑥 / 𝑛)) ∈ ℂ)
108	107	abscld 15460	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑅‘(𝑥 / 𝑛))) ∈ ℝ)
109	108	recnd 11268	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑅‘(𝑥 / 𝑛))) ∈ ℂ)
110	3	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℝ⁺)
111	103, 110	rpaddcld 13071	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 + 1) ∈ ℝ⁺)
112	100, 111	rpdivcld 13073	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / (𝑛 + 1)) ∈ ℝ⁺)
113	69	ffvelcdmi 7078	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 / (𝑛 + 1)) ∈ ℝ⁺ → (𝑅‘(𝑥 / (𝑛 + 1))) ∈ ℝ)
114	112, 113	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘(𝑥 / (𝑛 + 1))) ∈ ℝ)
115	114	recnd 11268	. . . . . . . . . . . . . . . . . 18 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘(𝑥 / (𝑛 + 1))) ∈ ℂ)
116	115	abscld 15460	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) ∈ ℝ)
117	116	recnd 11268	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) ∈ ℂ)
118	109, 117	negsubdi2d 11615	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → -((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) = ((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))))
119	118	eqcomd 2742	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))) = -((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))))
120	102	nncnd 12261	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℂ)
121		1cnd 11235	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℂ)
122	120, 121	pncand 11600	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) − 1) = 𝑛)
123	122	fveq2d 6885	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘((𝑛 + 1) − 1)) = (𝑆‘𝑛))
124	122	fveq2d 6885	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇‘((𝑛 + 1) − 1)) = (𝑇‘𝑛))
125		rpre 13022	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℝ⁺ → 𝑛 ∈ ℝ)
126		eleq1 2823	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = 𝑛 → (𝑎 ∈ ℝ⁺ ↔ 𝑛 ∈ ℝ⁺))
127		id 22	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = 𝑛 → 𝑎 = 𝑛)
128		fveq2 6881	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = 𝑛 → (log‘𝑎) = (log‘𝑛))
129	127, 128	oveq12d 7428	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = 𝑛 → (𝑎 · (log‘𝑎)) = (𝑛 · (log‘𝑛)))
130	126, 129	ifbieq1d 4530	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = 𝑛 → if(𝑎 ∈ ℝ⁺, (𝑎 · (log‘𝑎)), 0) = if(𝑛 ∈ ℝ⁺, (𝑛 · (log‘𝑛)), 0))
131		ovex 7443	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 · (log‘𝑛)) ∈ V
132		c0ex 11234	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 ∈ V
133	131, 132	ifex 4556	. . . . . . . . . . . . . . . . . . . . 21 ⊢ if(𝑛 ∈ ℝ⁺, (𝑛 · (log‘𝑛)), 0) ∈ V
134	130, 81, 133	fvmpt 6991	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℝ → (𝑇‘𝑛) = if(𝑛 ∈ ℝ⁺, (𝑛 · (log‘𝑛)), 0))
135	125, 134	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ℝ⁺ → (𝑇‘𝑛) = if(𝑛 ∈ ℝ⁺, (𝑛 · (log‘𝑛)), 0))
136		iftrue 4511	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ℝ⁺ → if(𝑛 ∈ ℝ⁺, (𝑛 · (log‘𝑛)), 0) = (𝑛 · (log‘𝑛)))
137	135, 136	eqtrd 2771	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℝ⁺ → (𝑇‘𝑛) = (𝑛 · (log‘𝑛)))
138	103, 137	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇‘𝑛) = (𝑛 · (log‘𝑛)))
139	124, 138	eqtrd 2771	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇‘((𝑛 + 1) − 1)) = (𝑛 · (log‘𝑛)))
140	139	oveq2d 7426	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑇‘((𝑛 + 1) − 1))) = (2 · (𝑛 · (log‘𝑛))))
141	123, 140	oveq12d 7428	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))) = ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))
142	119, 141	oveq12d 7428	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))) · ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1))))) = (-((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))))
143	108, 116	resubcld 11670	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) ∈ ℝ)
144	143	recnd 11268	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) ∈ ℂ)
145	102	nnred 12260	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ)
146	78	ffvelcdmi 7078	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℝ → (𝑆‘𝑛) ∈ ℝ)
147	145, 146	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘𝑛) ∈ ℝ)
148	22	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 2 ∈ ℝ)
149	103	relogcld 26589	. . . . . . . . . . . . . . . . . 18 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘𝑛) ∈ ℝ)
150	145, 149	remulcld 11270	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 · (log‘𝑛)) ∈ ℝ)
151	148, 150	remulcld 11270	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑛 · (log‘𝑛))) ∈ ℝ)
152	147, 151	resubcld 11670	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))) ∈ ℝ)
153	152	recnd 11268	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))) ∈ ℂ)
154	144, 153	mulneg1d 11695	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (-((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) = -(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))))
155	142, 154	eqtrd 2771	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))) · ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1))))) = -(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))))
156	99, 155	sumeq12rdv 15728	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))(((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))) · ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1))))) = Σ𝑛 ∈ (1...(⌊‘𝑥))-(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))))
157		fzfid 13996	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (1...(⌊‘𝑥)) ∈ Fin)
158	143, 152	remulcld 11270	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) ∈ ℝ)
159	158	recnd 11268	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) ∈ ℂ)
160	157, 159	fsumneg 15808	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))-(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) = -Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))))
161	156, 160	eqtrd 2771	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))(((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))) · ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1))))) = -Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))))
162	95, 161	oveq12d 7428	. . . . . . . . 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 7418	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑛 → (𝑥 / 𝑚) = (𝑥 / 𝑛))
164	163	fveq2d 6885	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑛 → (𝑅‘(𝑥 / 𝑚)) = (𝑅‘(𝑥 / 𝑛)))
165	164	fveq2d 6885	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → (abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / 𝑛))))
166		fvoveq1 7433	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑛 → (𝑆‘(𝑚 − 1)) = (𝑆‘(𝑛 − 1)))
167		fvoveq1 7433	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑛 → (𝑇‘(𝑚 − 1)) = (𝑇‘(𝑛 − 1)))
168	167	oveq2d 7426	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑛 → (2 · (𝑇‘(𝑚 − 1))) = (2 · (𝑇‘(𝑛 − 1))))
169	166, 168	oveq12d 7428	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1)))))
170	165, 169	jca 511	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → ((abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / 𝑛))) ∧ ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1))))))
171		oveq2 7418	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (𝑛 + 1) → (𝑥 / 𝑚) = (𝑥 / (𝑛 + 1)))
172	171	fveq2d 6885	. . . . . . . . . . . . 13 ⊢ (𝑚 = (𝑛 + 1) → (𝑅‘(𝑥 / 𝑚)) = (𝑅‘(𝑥 / (𝑛 + 1))))
173	172	fveq2d 6885	. . . . . . . . . . . 12 ⊢ (𝑚 = (𝑛 + 1) → (abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / (𝑛 + 1)))))
174		fvoveq1 7433	. . . . . . . . . . . . 13 ⊢ (𝑚 = (𝑛 + 1) → (𝑆‘(𝑚 − 1)) = (𝑆‘((𝑛 + 1) − 1)))
175		fvoveq1 7433	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (𝑛 + 1) → (𝑇‘(𝑚 − 1)) = (𝑇‘((𝑛 + 1) − 1)))
176	175	oveq2d 7426	. . . . . . . . . . . . 13 ⊢ (𝑚 = (𝑛 + 1) → (2 · (𝑇‘(𝑚 − 1))) = (2 · (𝑇‘((𝑛 + 1) − 1))))
177	174, 176	oveq12d 7428	. . . . . . . . . . . 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 7418	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 1 → (𝑥 / 𝑚) = (𝑥 / 1))
180	179	fveq2d 6885	. . . . . . . . . . . . 13 ⊢ (𝑚 = 1 → (𝑅‘(𝑥 / 𝑚)) = (𝑅‘(𝑥 / 1)))
181	180	fveq2d 6885	. . . . . . . . . . . 12 ⊢ (𝑚 = 1 → (abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / 1))))
182		oveq1 7417	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 1 → (𝑚 − 1) = (1 − 1))
183		1m1e0 12317	. . . . . . . . . . . . . . . . 17 ⊢ (1 − 1) = 0
184	182, 183	eqtrdi 2787	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 1 → (𝑚 − 1) = 0)
185	184	fveq2d 6885	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 1 → (𝑆‘(𝑚 − 1)) = (𝑆‘0))
186		0re 11242	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ ℝ
187		fveq2 6881	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = 0 → (⌊‘𝑎) = (⌊‘0))
188		0z 12604	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 ∈ ℤ
189		flid 13830	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (0 ∈ ℤ → (⌊‘0) = 0)
190	188, 189	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⌊‘0) = 0
191	187, 190	eqtrdi 2787	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = 0 → (⌊‘𝑎) = 0)
192	191	oveq2d 7426	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 0 → (1...(⌊‘𝑎)) = (1...0))
193		fz10 13567	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1...0) = ∅
194	192, 193	eqtrdi 2787	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 0 → (1...(⌊‘𝑎)) = ∅)
195	194	sumeq1d 15721	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = 0 → Σ𝑖 ∈ (1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))) = Σ𝑖 ∈ ∅ ((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))))
196		sum0 15742	. . . . . . . . . . . . . . . . . 18 ⊢ Σ𝑖 ∈ ∅ ((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))) = 0
197	195, 196	eqtrdi 2787	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 0 → Σ𝑖 ∈ (1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))) = 0)
198	197, 47, 132	fvmpt 6991	. . . . . . . . . . . . . . . 16 ⊢ (0 ∈ ℝ → (𝑆‘0) = 0)
199	186, 198	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (𝑆‘0) = 0
200	185, 199	eqtrdi 2787	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 1 → (𝑆‘(𝑚 − 1)) = 0)
201	184	fveq2d 6885	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 1 → (𝑇‘(𝑚 − 1)) = (𝑇‘0))
202		rpne0 13030	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 ∈ ℝ⁺ → 𝑎 ≠ 0)
203	202	necon2bi 2963	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = 0 → ¬ 𝑎 ∈ ℝ⁺)
204	203	iffalsed 4516	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = 0 → if(𝑎 ∈ ℝ⁺, (𝑎 · (log‘𝑎)), 0) = 0)
205	204, 81, 132	fvmpt 6991	. . . . . . . . . . . . . . . . . 18 ⊢ (0 ∈ ℝ → (𝑇‘0) = 0)
206	186, 205	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (𝑇‘0) = 0
207	201, 206	eqtrdi 2787	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 1 → (𝑇‘(𝑚 − 1)) = 0)
208	207	oveq2d 7426	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 1 → (2 · (𝑇‘(𝑚 − 1))) = (2 · 0))
209		2t0e0 12414	. . . . . . . . . . . . . . 15 ⊢ (2 · 0) = 0
210	208, 209	eqtrdi 2787	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 1 → (2 · (𝑇‘(𝑚 − 1))) = 0)
211	200, 210	oveq12d 7428	. . . . . . . . . . . . 13 ⊢ (𝑚 = 1 → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = (0 − 0))
212		0m0e0 12365	. . . . . . . . . . . . 13 ⊢ (0 − 0) = 0
213	211, 212	eqtrdi 2787	. . . . . . . . . . . 12 ⊢ (𝑚 = 1 → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = 0)
214	181, 213	jca 511	. . . . . . . . . . 11 ⊢ (𝑚 = 1 → ((abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / 1))) ∧ ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = 0))
215		oveq2 7418	. . . . . . . . . . . . . 14 ⊢ (𝑚 = ((⌊‘𝑥) + 1) → (𝑥 / 𝑚) = (𝑥 / ((⌊‘𝑥) + 1)))
216	215	fveq2d 6885	. . . . . . . . . . . . 13 ⊢ (𝑚 = ((⌊‘𝑥) + 1) → (𝑅‘(𝑥 / 𝑚)) = (𝑅‘(𝑥 / ((⌊‘𝑥) + 1))))
217	216	fveq2d 6885	. . . . . . . . . . . 12 ⊢ (𝑚 = ((⌊‘𝑥) + 1) → (abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))))
218		fvoveq1 7433	. . . . . . . . . . . . 13 ⊢ (𝑚 = ((⌊‘𝑥) + 1) → (𝑆‘(𝑚 − 1)) = (𝑆‘(((⌊‘𝑥) + 1) − 1)))
219		fvoveq1 7433	. . . . . . . . . . . . . 14 ⊢ (𝑚 = ((⌊‘𝑥) + 1) → (𝑇‘(𝑚 − 1)) = (𝑇‘(((⌊‘𝑥) + 1) − 1)))
220	219	oveq2d 7426	. . . . . . . . . . . . 13 ⊢ (𝑚 = ((⌊‘𝑥) + 1) → (2 · (𝑇‘(𝑚 − 1))) = (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1))))
221	218, 220	oveq12d 7428	. . . . . . . . . . . 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 12900	. . . . . . . . . . . 12 ⊢ ℕ = (ℤ_≥‘1)
224	15, 223	eleqtrdi 2845	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((⌊‘𝑥) + 1) ∈ (ℤ_≥‘1))
225	10	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 𝑥 ∈ ℝ⁺)
226		elfznn 13575	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑚 ∈ (1...((⌊‘𝑥) + 1)) → 𝑚 ∈ ℕ)
227	226	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 𝑚 ∈ ℕ)
228	227	nnrpd 13054	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 𝑚 ∈ ℝ⁺)
229	225, 228	rpdivcld 13073	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑥 / 𝑚) ∈ ℝ⁺)
230	69	ffvelcdmi 7078	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 / 𝑚) ∈ ℝ⁺ → (𝑅‘(𝑥 / 𝑚)) ∈ ℝ)
231	229, 230	syl 17	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑅‘(𝑥 / 𝑚)) ∈ ℝ)
232	231	recnd 11268	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑅‘(𝑥 / 𝑚)) ∈ ℂ)
233	232	abscld 15460	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (abs‘(𝑅‘(𝑥 / 𝑚))) ∈ ℝ)
234	233	recnd 11268	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (abs‘(𝑅‘(𝑥 / 𝑚))) ∈ ℂ)
235	227	nnred 12260	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 𝑚 ∈ ℝ)
236		1red 11241	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 1 ∈ ℝ)
237	235, 236	resubcld 11670	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑚 − 1) ∈ ℝ)
238	78	ffvelcdmi 7078	. . . . . . . . . . . . . 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 7078	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 − 1) ∈ ℝ → (𝑇‘(𝑚 − 1)) ∈ ℝ)
242	237, 241	syl 17	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑇‘(𝑚 − 1)) ∈ ℝ)
243	240, 242	remulcld 11270	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (2 · (𝑇‘(𝑚 − 1))) ∈ ℝ)
244	239, 243	resubcld 11670	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) ∈ ℝ)
245	244	recnd 11268	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) ∈ ℂ)
246	170, 178, 214, 222, 224, 234, 245	fsumparts 15827	. . . . . . . . . 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 11268	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘𝑛) ∈ ℂ)
248	87	ffvelcdmi 7078	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℝ → (𝑇‘𝑛) ∈ ℝ)
249	145, 248	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇‘𝑛) ∈ ℝ)
250	148, 249	remulcld 11270	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑇‘𝑛)) ∈ ℝ)
251	250	recnd 11268	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑇‘𝑛)) ∈ ℂ)
252		1red 11241	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℝ)
253	145, 252	resubcld 11670	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 − 1) ∈ ℝ)
254	78	ffvelcdmi 7078	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 − 1) ∈ ℝ → (𝑆‘(𝑛 − 1)) ∈ ℝ)
255	253, 254	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘(𝑛 − 1)) ∈ ℝ)
256	255	recnd 11268	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘(𝑛 − 1)) ∈ ℂ)
257	87	ffvelcdmi 7078	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 − 1) ∈ ℝ → (𝑇‘(𝑛 − 1)) ∈ ℝ)
258	253, 257	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇‘(𝑛 − 1)) ∈ ℝ)
259	148, 258	remulcld 11270	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑇‘(𝑛 − 1))) ∈ ℝ)
260	259	recnd 11268	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑇‘(𝑛 − 1))) ∈ ℂ)
261	247, 251, 256, 260	sub4d 11648	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆‘𝑛) − (2 · (𝑇‘𝑛))) − ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1))))) = (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − ((2 · (𝑇‘𝑛)) − (2 · (𝑇‘(𝑛 − 1))))))
262	124	oveq2d 7426	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑇‘((𝑛 + 1) − 1))) = (2 · (𝑇‘𝑛)))
263	123, 262	oveq12d 7428	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))) = ((𝑆‘𝑛) − (2 · (𝑇‘𝑛))))
264	263	oveq1d 7425	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))) − ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1))))) = (((𝑆‘𝑛) − (2 · (𝑇‘𝑛))) − ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1))))))
265		2cnd 12323	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 2 ∈ ℂ)
266	249	recnd 11268	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇‘𝑛) ∈ ℂ)
267	258	recnd 11268	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇‘(𝑛 − 1)) ∈ ℂ)
268	265, 266, 267	subdid 11698	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))) = ((2 · (𝑇‘𝑛)) − (2 · (𝑇‘(𝑛 − 1)))))
269	268	oveq2d 7426	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))) = (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − ((2 · (𝑇‘𝑛)) − (2 · (𝑇‘(𝑛 − 1))))))
270	261, 264, 269	3eqtr4d 2781	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))) − ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1))))) = (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))
271	270	oveq2d 7426	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))) − ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1)))))) = ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))))
272	99, 271	sumeq12rdv 15728	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))) − ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1)))))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))))
273	246, 272	eqtr3d 2773	. . . . . . . . 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 15754	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) ∈ ℂ)
275	93, 274	subnegd 11606	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) − -Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) = (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))))
276	162, 273, 275	3eqtr3rd 2780	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))))
277	10	relogcld 26589	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ∈ ℝ)
278	277	recnd 11268	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ∈ ℂ)
279	66, 278	mulcomd 11261	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) = ((log‘𝑥) · 𝑥))
280	276, 279	oveq12d 7428	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / ((log‘𝑥) · 𝑥)))
281	147, 255	resubcld 11670	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) ∈ ℝ)
282	249, 258	resubcld 11670	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))) ∈ ℝ)
283	148, 282	remulcld 11270	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))) ∈ ℝ)
284	281, 283	resubcld 11670	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))) ∈ ℝ)
285	108, 284	remulcld 11270	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) ∈ ℝ)
286	157, 285	fsumrecl 15755	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) ∈ ℝ)
287	286	recnd 11268	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) ∈ ℂ)
288	2, 8	rplogcld 26595	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ∈ ℝ⁺)
289	288	rpne0d 13061	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ≠ 0)
290	10	rpne0d 13061	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ≠ 0)
291	287, 278, 66, 289, 290	divdiv1d 12053	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥)) / 𝑥) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / ((log‘𝑥) · 𝑥)))
292	280, 291	eqtr4d 2774	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥)) / 𝑥))
293	292	oveq2d 7426	. . . . 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 11268	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑅‘𝑥) ∈ ℂ)
295	294	abscld 15460	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘(𝑅‘𝑥)) ∈ ℝ)
296	295, 277	remulcld 11270	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((abs‘(𝑅‘𝑥)) · (log‘𝑥)) ∈ ℝ)
297	108, 281	remulcld 11270	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) ∈ ℝ)
298	157, 297	fsumrecl 15755	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) ∈ ℝ)
299	298, 288	rerpdivcld 13087	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥)) ∈ ℝ)
300	296, 299	resubcld 11670	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) ∈ ℝ)
301	300	recnd 11268	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) ∈ ℂ)
302	287, 278, 289	divcld 12022	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥)) ∈ ℂ)
303	301, 302, 66, 290	divdird 12060	. . . . 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 11268	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((abs‘(𝑅‘𝑥)) · (log‘𝑥)) ∈ ℂ)
305	299	recnd 11268	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥)) ∈ ℂ)
306	304, 305, 302	subsubd 11627	. . . . . . 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 12323	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 2 ∈ ℂ)
308	266, 267	subcld 11599	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))) ∈ ℂ)
309	109, 308	mulcld 11260	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))) ∈ ℂ)
310	157, 307, 309	fsummulc2 15805	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(2 · ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))
311	281	recnd 11268	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) ∈ ℂ)
312	265, 308	mulcld 11260	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))) ∈ ℂ)
313	311, 312	nncand 11604	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) = (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))
314	313	oveq2d 7426	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) = ((abs‘(𝑅‘(𝑥 / 𝑛))) · (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))
315	284	recnd 11268	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))) ∈ ℂ)
316	109, 311, 315	subdid 11698	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) = (((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) − ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))))
317	109, 265, 308	mul12d 11449	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))) = (2 · ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))
318	314, 316, 317	3eqtr3d 2779	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) − ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) = (2 · ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))
319	318	sumeq2dv 15723	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) − ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(2 · ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))
320	297	recnd 11268	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) ∈ ℂ)
321	285	recnd 11268	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) ∈ ℂ)
322	157, 320, 321	fsumsub 15809	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) − ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))))
323	310, 319, 322	3eqtr2rd 2778	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) = (2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))
324	323	oveq1d 7425	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) / (log‘𝑥)) = ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))) / (log‘𝑥)))
325	298	recnd 11268	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) ∈ ℂ)
326	325, 287, 278, 289	divsubdird 12061	. . . . . . . . 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 11270	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))) ∈ ℝ)
328	157, 327	fsumrecl 15755	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))) ∈ ℝ)
329	328	recnd 11268	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))) ∈ ℂ)
330	307, 329, 278, 289	div23d 12059	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))) / (log‘𝑥)) = ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))
331	324, 326, 330	3eqtr3d 2779	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥))) = ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))
332	331	oveq2d 7426	. . . . . . 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 2773	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥))) = (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))))
334	333	oveq1d 7425	. . . . 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 2777	. . . 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 5219	. . 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 13087	. . . 4 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥) ∈ ℝ)
338	157, 158	fsumrecl 15755	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) ∈ ℝ)
339	92, 338	readdcld 11269	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) ∈ ℝ)
340	10, 288	rpmulcld 13072	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ∈ ℝ⁺)
341	339, 340	rerpdivcld 13087	. . . 4 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))) ∈ ℝ)
342	47, 18	pntrlog2bndlem1 27545	. . . . 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 13058	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ∈ ℂ)
345	340	rpne0d 13061	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ≠ 0)
346	93, 274, 344, 345	divdird 12060	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))) = ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) / (𝑥 · (log‘𝑥))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥)))))
347	91	recnd 11268	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) ∈ ℂ)
348	43, 347, 344, 345	divassd 12057	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) / (𝑥 · (log‘𝑥))) = ((𝑥 / ((⌊‘𝑥) + 1)) · (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))))
349	348	oveq1d 7425	. . . . . . 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 2771	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))) = (((𝑥 / ((⌊‘𝑥) + 1)) · (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥)))))
351	350	mpteq2dva 5219	. . . . 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 13087	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥))) ∈ ℝ)
353	21, 352	remulcld 11270	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑥 / ((⌊‘𝑥) + 1)) · (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) ∈ ℝ)
354	338, 340	rerpdivcld 13087	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥))) ∈ ℝ)
355		ioossre 13429	. . . . . . . . 9 ⊢ (1(,)+∞) ⊆ ℝ
356	355	a1i 11	. . . . . . . 8 ⊢ (⊤ → (1(,)+∞) ⊆ ℝ)
357		1red 11241	. . . . . . . 8 ⊢ (⊤ → 1 ∈ ℝ)
358	21, 5, 30	ltled 11388	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 / ((⌊‘𝑥) + 1)) ≤ 1)
359	358	adantrr 717	. . . . . . . 8 ⊢ ((⊤ ∧ (𝑥 ∈ (1(,)+∞) ∧ 1 ≤ 𝑥)) → (𝑥 / ((⌊‘𝑥) + 1)) ≤ 1)
360	356, 21, 357, 357, 359	ello1d 15544	. . . . . . 7 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (𝑥 / ((⌊‘𝑥) + 1))) ∈ ≤𝑂(1))
361	80	recnd 11268	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑆‘𝑥) ∈ ℂ)
362	90	recnd 11268	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (2 · (𝑇‘(⌊‘𝑥))) ∈ ℂ)
363	361, 362, 344, 345	divsubdird 12061	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥))) = (((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) − ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥)))))
364	363	mpteq2dva 5219	. . . . . . . . 9 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) = (𝑥 ∈ (1(,)+∞) ↦ (((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) − ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥))))))
365	80, 340	rerpdivcld 13087	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) ∈ ℝ)
366	90, 340	rerpdivcld 13087	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥))) ∈ ℝ)
367		2cnd 12323	. . . . . . . . . . . 12 ⊢ (⊤ → 2 ∈ ℂ)
368		o1const 15641	. . . . . . . . . . . 12 ⊢ (((1(,)+∞) ⊆ ℝ ∧ 2 ∈ ℂ) → (𝑥 ∈ (1(,)+∞) ↦ 2) ∈ 𝑂(1))
369	355, 367, 368	sylancr 587	. . . . . . . . . . 11 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ 2) ∈ 𝑂(1))
370	365	recnd 11268	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) ∈ ℂ)
371	80, 10	rerpdivcld 13087	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑆‘𝑥) / 𝑥) ∈ ℝ)
372	371	recnd 11268	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑆‘𝑥) / 𝑥) ∈ ℂ)
373	307, 278	mulcld 11260	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (2 · (log‘𝑥)) ∈ ℂ)
374	372, 373, 278, 289	divsubdird 12061	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥))) / (log‘𝑥)) = ((((𝑆‘𝑥) / 𝑥) / (log‘𝑥)) − ((2 · (log‘𝑥)) / (log‘𝑥))))
375	23, 277	remulcld 11270	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (2 · (log‘𝑥)) ∈ ℝ)
376	371, 375	resubcld 11670	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥))) ∈ ℝ)
377	376	recnd 11268	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥))) ∈ ℂ)
378	377, 278, 289	divrecd 12025	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥))) / (log‘𝑥)) = ((((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥))) · (1 / (log‘𝑥))))
379	361, 66, 278, 290, 289	divdiv1d 12053	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑆‘𝑥) / 𝑥) / (log‘𝑥)) = ((𝑆‘𝑥) / (𝑥 · (log‘𝑥))))
380	307, 278, 289	divcan4d 12028	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 · (log‘𝑥)) / (log‘𝑥)) = 2)
381	379, 380	oveq12d 7428	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((𝑆‘𝑥) / 𝑥) / (log‘𝑥)) − ((2 · (log‘𝑥)) / (log‘𝑥))) = (((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) − 2))
382	374, 378, 381	3eqtr3rd 2780	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) − 2) = ((((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥))) · (1 / (log‘𝑥))))
383	382	mpteq2dva 5219	. . . . . . . . . . . . 13 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) − 2)) = (𝑥 ∈ (1(,)+∞) ↦ ((((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥))) · (1 / (log‘𝑥)))))
384	5, 288	rerpdivcld 13087	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (1 / (log‘𝑥)) ∈ ℝ)
385	10	ex 412	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) → 𝑥 ∈ ℝ⁺))
386	385	ssrdv 3969	. . . . . . . . . . . . . . 15 ⊢ (⊤ → (1(,)+∞) ⊆ ℝ⁺)
387	47	selbergs 27542	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℝ⁺ ↦ (((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥)))) ∈ 𝑂(1)
388	387	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (⊤ → (𝑥 ∈ ℝ⁺ ↦ (((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥)))) ∈ 𝑂(1))
389	386, 388	o1res2 15584	. . . . . . . . . . . . . 14 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥)))) ∈ 𝑂(1))
390		divlogrlim 26601	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (1(,)+∞) ↦ (1 / (log‘𝑥))) ⇝_𝑟 0
391		rlimo1 15638	. . . . . . . . . . . . . . 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 15646	. . . . . . . . . . . . 13 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥))) · (1 / (log‘𝑥)))) ∈ 𝑂(1))
394	383, 393	eqeltrd 2835	. . . . . . . . . . . 12 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) − 2)) ∈ 𝑂(1))
395	370, 307, 394	o1dif 15651	. . . . . . . . . . 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 11270	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ∈ ℝ)
399		2rp 13018	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ ℝ⁺
400	399	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 2 ∈ ℝ⁺)
401	400	rpge0d 13060	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ 2)
402		flge1nn 13843	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) → (⌊‘𝑥) ∈ ℕ)
403	2, 9, 402	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (⌊‘𝑥) ∈ ℕ)
404	403	nnrpd 13054	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (⌊‘𝑥) ∈ ℝ⁺)
405		rpre 13022	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⌊‘𝑥) ∈ ℝ⁺ → (⌊‘𝑥) ∈ ℝ)
406		eleq1 2823	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = (⌊‘𝑥) → (𝑎 ∈ ℝ⁺ ↔ (⌊‘𝑥) ∈ ℝ⁺))
407		id 22	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = (⌊‘𝑥) → 𝑎 = (⌊‘𝑥))
408		fveq2 6881	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = (⌊‘𝑥) → (log‘𝑎) = (log‘(⌊‘𝑥)))
409	407, 408	oveq12d 7428	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = (⌊‘𝑥) → (𝑎 · (log‘𝑎)) = ((⌊‘𝑥) · (log‘(⌊‘𝑥))))
410	406, 409	ifbieq1d 4530	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = (⌊‘𝑥) → if(𝑎 ∈ ℝ⁺, (𝑎 · (log‘𝑎)), 0) = if((⌊‘𝑥) ∈ ℝ⁺, ((⌊‘𝑥) · (log‘(⌊‘𝑥))), 0))
411		ovex 7443	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((⌊‘𝑥) · (log‘(⌊‘𝑥))) ∈ V
412	411, 132	ifex 4556	. . . . . . . . . . . . . . . . . . . 20 ⊢ if((⌊‘𝑥) ∈ ℝ⁺, ((⌊‘𝑥) · (log‘(⌊‘𝑥))), 0) ∈ V
413	410, 81, 412	fvmpt 6991	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⌊‘𝑥) ∈ ℝ → (𝑇‘(⌊‘𝑥)) = if((⌊‘𝑥) ∈ ℝ⁺, ((⌊‘𝑥) · (log‘(⌊‘𝑥))), 0))
414	405, 413	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((⌊‘𝑥) ∈ ℝ⁺ → (𝑇‘(⌊‘𝑥)) = if((⌊‘𝑥) ∈ ℝ⁺, ((⌊‘𝑥) · (log‘(⌊‘𝑥))), 0))
415		iftrue 4511	. . . . . . . . . . . . . . . . . 18 ⊢ ((⌊‘𝑥) ∈ ℝ⁺ → if((⌊‘𝑥) ∈ ℝ⁺, ((⌊‘𝑥) · (log‘(⌊‘𝑥))), 0) = ((⌊‘𝑥) · (log‘(⌊‘𝑥))))
416	414, 415	eqtrd 2771	. . . . . . . . . . . . . . . . 17 ⊢ ((⌊‘𝑥) ∈ ℝ⁺ → (𝑇‘(⌊‘𝑥)) = ((⌊‘𝑥) · (log‘(⌊‘𝑥))))
417	404, 416	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑇‘(⌊‘𝑥)) = ((⌊‘𝑥) · (log‘(⌊‘𝑥))))
418	404	relogcld 26589	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (log‘(⌊‘𝑥)) ∈ ℝ)
419	13	nn0ge0d 12570	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ (⌊‘𝑥))
420	403	nnge1d 12293	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 ≤ (⌊‘𝑥))
421	46, 420	logge0d 26596	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ (log‘(⌊‘𝑥)))
422		flle 13821	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℝ → (⌊‘𝑥) ≤ 𝑥)
423	2, 422	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (⌊‘𝑥) ≤ 𝑥)
424	404, 10	logled 26593	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((⌊‘𝑥) ≤ 𝑥 ↔ (log‘(⌊‘𝑥)) ≤ (log‘𝑥)))
425	423, 424	mpbid 232	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (log‘(⌊‘𝑥)) ≤ (log‘𝑥))
426	46, 2, 418, 277, 419, 421, 423, 425	lemul12ad 12189	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((⌊‘𝑥) · (log‘(⌊‘𝑥))) ≤ (𝑥 · (log‘𝑥)))
427	417, 426	eqbrtrd 5146	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑇‘(⌊‘𝑥)) ≤ (𝑥 · (log‘𝑥)))
428	89, 398, 23, 401, 427	lemul2ad 12187	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (2 · (𝑇‘(⌊‘𝑥))) ≤ (2 · (𝑥 · (log‘𝑥))))
429	90, 23, 340	ledivmul2d 13110	. . . . . . . . . . . . . 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 15544	. . . . . . . . . . 11 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥)))) ∈ ≤𝑂(1))
433		0red 11243	. . . . . . . . . . . 12 ⊢ (⊤ → 0 ∈ ℝ)
434	46, 418, 419, 421	mulge0d 11819	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ ((⌊‘𝑥) · (log‘(⌊‘𝑥))))
435	434, 417	breqtrrd 5152	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ (𝑇‘(⌊‘𝑥)))
436	23, 89, 401, 435	mulge0d 11819	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ (2 · (𝑇‘(⌊‘𝑥))))
437	90, 340, 436	divge0d 13096	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥))))
438	366, 433, 437	o1lo12 15559	. . . . . . . . . . 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 15647	. . . . . . . . 9 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) − ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥))))) ∈ 𝑂(1))
441	364, 440	eqeltrd 2835	. . . . . . . 8 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1))
442	352, 441	o1lo1d 15560	. . . . . . 7 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) ∈ ≤𝑂(1))
443	21, 352, 360, 442, 41	lo1mul 15649	. . . . . 6 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((𝑥 / ((⌊‘𝑥) + 1)) · (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥))))) ∈ ≤𝑂(1))
444	47	selbergsb 27543	. . . . . . . 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 27547	. . . . . . . . 9 ⊢ ((𝑐 ∈ ℝ⁺ ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘(((𝑆‘𝑦) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝑐) → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1))
448	447	rexlimiva 3134	. . . . . . . 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 15560	. . . . . 6 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥)))) ∈ ≤𝑂(1))
451	353, 354, 443, 450	lo1add 15648	. . . . 5 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((𝑥 / ((⌊‘𝑥) + 1)) · (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥))))) ∈ ≤𝑂(1))
452	351, 451	eqeltrd 2835	. . . 4 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥)))) ∈ ≤𝑂(1))
453	337, 341, 343, 452	lo1add 15648	. . 3 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥) + ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))))) ∈ ≤𝑂(1))
454	336, 453	eqeltrrd 2836	. 2 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / 𝑥)) ∈ ≤𝑂(1))
455	454	mptru 1547	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 1540 ⊤wtru 1541 ∈ wcel 2109 ∀wral 3052 ∃wrex 3061 {crab 3420 ⊆ wss 3931 ∅c0 4313 ifcif 4505 class class class wbr 5124 ↦ cmpt 5206 ‘cfv 6536 (class class class)co 7410 ℂcc 11132 ℝcr 11133 0cc0 11134 1c1 11135 + caddc 11137 · cmul 11139 +∞cpnf 11271 < clt 11274 ≤ cle 11275 − cmin 11471 -cneg 11472 / cdiv 11899 ℕcn 12245 2c2 12300 ℕ₀cn0 12506 ℤcz 12593 ℤ_≥cuz 12857 ℝ⁺crp 13013 (,)cioo 13367 [,)cico 13369 ...cfz 13529 ..^cfzo 13676 ⌊cfl 13812 abscabs 15258 ⇝_𝑟 crli 15506 𝑂(1)co1 15507 ≤𝑂(1)clo1 15508 Σcsu 15707 ∥ cdvds 16277 logclog 26520 Λcvma 27059 ψcchp 27060

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2708 ax-rep 5254 ax-sep 5271 ax-nul 5281 ax-pow 5340 ax-pr 5407 ax-un 7734 ax-inf2 9660 ax-cnex 11190 ax-resscn 11191 ax-1cn 11192 ax-icn 11193 ax-addcl 11194 ax-addrcl 11195 ax-mulcl 11196 ax-mulrcl 11197 ax-mulcom 11198 ax-addass 11199 ax-mulass 11200 ax-distr 11201 ax-i2m1 11202 ax-1ne0 11203 ax-1rid 11204 ax-rnegex 11205 ax-rrecex 11206 ax-cnre 11207 ax-pre-lttri 11208 ax-pre-lttrn 11209 ax-pre-ltadd 11210 ax-pre-mulgt0 11211 ax-pre-sup 11212 ax-addf 11213

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2810 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3062 df-rmo 3364 df-reu 3365 df-rab 3421 df-v 3466 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-pss 3951 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-tp 4611 df-op 4613 df-uni 4889 df-int 4928 df-iun 4974 df-iin 4975 df-disj 5092 df-br 5125 df-opab 5187 df-mpt 5207 df-tr 5235 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-se 5612 df-we 5613 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6295 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-isom 6545 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-of 7676 df-om 7867 df-1st 7993 df-2nd 7994 df-supp 8165 df-frecs 8285 df-wrecs 8316 df-recs 8390 df-rdg 8429 df-1o 8485 df-2o 8486 df-oadd 8489 df-er 8724 df-map 8847 df-pm 8848 df-ixp 8917 df-en 8965 df-dom 8966 df-sdom 8967 df-fin 8968 df-fsupp 9379 df-fi 9428 df-sup 9459 df-inf 9460 df-oi 9529 df-dju 9920 df-card 9958 df-pnf 11276 df-mnf 11277 df-xr 11278 df-ltxr 11279 df-le 11280 df-sub 11473 df-neg 11474 df-div 11900 df-nn 12246 df-2 12308 df-3 12309 df-4 12310 df-5 12311 df-6 12312 df-7 12313 df-8 12314 df-9 12315 df-n0 12507 df-xnn0 12580 df-z 12594 df-dec 12714 df-uz 12858 df-q 12970 df-rp 13014 df-xneg 13133 df-xadd 13134 df-xmul 13135 df-ioo 13371 df-ioc 13372 df-ico 13373 df-icc 13374 df-fz 13530 df-fzo 13677 df-fl 13814 df-mod 13892 df-seq 14025 df-exp 14085 df-fac 14297 df-bc 14326 df-hash 14354 df-shft 15091 df-cj 15123 df-re 15124 df-im 15125 df-sqrt 15259 df-abs 15260 df-limsup 15492 df-clim 15509 df-rlim 15510 df-o1 15511 df-lo1 15512 df-sum 15708 df-ef 16088 df-e 16089 df-sin 16090 df-cos 16091 df-tan 16092 df-pi 16093 df-dvds 16278 df-gcd 16519 df-prm 16696 df-pc 16862 df-struct 17171 df-sets 17188 df-slot 17206 df-ndx 17218 df-base 17234 df-ress 17257 df-plusg 17289 df-mulr 17290 df-starv 17291 df-sca 17292 df-vsca 17293 df-ip 17294 df-tset 17295 df-ple 17296 df-ds 17298 df-unif 17299 df-hom 17300 df-cco 17301 df-rest 17441 df-topn 17442 df-0g 17460 df-gsum 17461 df-topgen 17462 df-pt 17463 df-prds 17466 df-xrs 17521 df-qtop 17526 df-imas 17527 df-xps 17529 df-mre 17603 df-mrc 17604 df-acs 17606 df-mgm 18623 df-sgrp 18702 df-mnd 18718 df-submnd 18767 df-mulg 19056 df-cntz 19305 df-cmn 19768 df-psmet 21312 df-xmet 21313 df-met 21314 df-bl 21315 df-mopn 21316 df-fbas 21317 df-fg 21318 df-cnfld 21321 df-top 22837 df-topon 22854 df-topsp 22876 df-bases 22889 df-cld 22962 df-ntr 22963 df-cls 22964 df-nei 23041 df-lp 23079 df-perf 23080 df-cn 23170 df-cnp 23171 df-haus 23258 df-cmp 23330 df-tx 23505 df-hmeo 23698 df-fil 23789 df-fm 23881 df-flim 23882 df-flf 23883 df-xms 24264 df-ms 24265 df-tms 24266 df-cncf 24827 df-limc 25824 df-dv 25825 df-ulm 26343 df-log 26522 df-cxp 26523 df-atan 26834 df-em 26960 df-cht 27064 df-vma 27065 df-chp 27066 df-ppi 27067 df-mu 27068

This theorem is referenced by: pntrlog2bndlem5 27549

W3C validator