selberg34r - Metamath Proof Explorer

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

Theorem selberg34r 26299

Description: The sum of selberg3r 26297 and selberg4r 26298. (Contributed by Mario Carneiro, 31-May-2016.)

**Hypothesis**
Ref	Expression
pntrval.r	⊢ 𝑅 = (𝑎 ∈ ℝ⁺ ↦ ((ψ‘𝑎) − 𝑎))

**Assertion**
Ref	Expression
selberg34r	⊢ (𝑥 ∈ (1(,)+∞) ↦ ((((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 𝑥)) ∈ 𝑂(1)

Distinct variable groups: 𝑚,𝑎,𝑛,𝑥 𝑦,𝑚,𝑅,𝑛,𝑥 Allowed substitution hint: 𝑅(𝑎)

Proof of Theorem selberg34r Dummy variable 𝑘 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		2re 11783	. . . . . . . . . 10 ⊢ 2 ∈ ℝ
2	1	a1i 11	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 2 ∈ ℝ)
3		elioore 12844	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (1(,)+∞) → 𝑥 ∈ ℝ)
4	3	adantl 485	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ∈ ℝ)
5		1rp 12469	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℝ⁺
6	5	a1i 11	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 ∈ ℝ⁺)
7		1red 10713	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 ∈ ℝ)
8		eliooord 12873	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (1(,)+∞) → (1 < 𝑥 ∧ 𝑥 < +∞))
9	8	adantl 485	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (1 < 𝑥 ∧ 𝑥 < +∞))
10	9	simpld 498	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 < 𝑥)
11	7, 4, 10	ltled 10859	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 ≤ 𝑥)
12	4, 6, 11	rpgecld 12546	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ∈ ℝ⁺)
13		pntrval.r	. . . . . . . . . . . . 13 ⊢ 𝑅 = (𝑎 ∈ ℝ⁺ ↦ ((ψ‘𝑎) − 𝑎))
14	13	pntrf 26291	. . . . . . . . . . . 12 ⊢ 𝑅:ℝ⁺⟶ℝ
15	14	ffvelrni 6854	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ⁺ → (𝑅‘𝑥) ∈ ℝ)
16	12, 15	syl 17	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑅‘𝑥) ∈ ℝ)
17	12	relogcld 25358	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ∈ ℝ)
18	16, 17	remulcld 10742	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑅‘𝑥) · (log‘𝑥)) ∈ ℝ)
19	2, 18	remulcld 10742	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (2 · ((𝑅‘𝑥) · (log‘𝑥))) ∈ ℝ)
20	19	recnd 10740	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (2 · ((𝑅‘𝑥) · (log‘𝑥))) ∈ ℂ)
21	4, 10	rplogcld 25364	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ∈ ℝ⁺)
22	2, 21	rerpdivcld 12538	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (2 / (log‘𝑥)) ∈ ℝ)
23	22	recnd 10740	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (2 / (log‘𝑥)) ∈ ℂ)
24		fzfid 13425	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (1...(⌊‘𝑥)) ∈ Fin)
25	12	adantr 484	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ⁺)
26		elfznn 13020	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
27	26	adantl 485	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
28	27	nnrpd 12505	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ⁺)
29	25, 28	rpdivcld 12524	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ⁺)
30	14	ffvelrni 6854	. . . . . . . . . . . 12 ⊢ ((𝑥 / 𝑛) ∈ ℝ⁺ → (𝑅‘(𝑥 / 𝑛)) ∈ ℝ)
31	29, 30	syl 17	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘(𝑥 / 𝑛)) ∈ ℝ)
32		fzfid 13425	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1...𝑛) ∈ Fin)
33		dvdsssfz1 15756	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ⊆ (1...𝑛))
34	27, 33	syl 17	. . . . . . . . . . . . . 14 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ⊆ (1...𝑛))
35	32, 34	ssfid 8812	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ∈ Fin)
36		ssrab2 3967	. . . . . . . . . . . . . . . 16 ⊢ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ⊆ ℕ
37		simpr 488	. . . . . . . . . . . . . . . 16 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛})
38	36, 37	sseldi 3873	. . . . . . . . . . . . . . 15 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → 𝑚 ∈ ℕ)
39		vmacl 25847	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℕ → (Λ‘𝑚) ∈ ℝ)
40	38, 39	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → (Λ‘𝑚) ∈ ℝ)
41		dvdsdivcl 15754	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ ℕ ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → (𝑛 / 𝑚) ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛})
42	27, 41	sylan 583	. . . . . . . . . . . . . . . 16 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → (𝑛 / 𝑚) ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛})
43	36, 42	sseldi 3873	. . . . . . . . . . . . . . 15 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → (𝑛 / 𝑚) ∈ ℕ)
44		vmacl 25847	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 / 𝑚) ∈ ℕ → (Λ‘(𝑛 / 𝑚)) ∈ ℝ)
45	43, 44	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → (Λ‘(𝑛 / 𝑚)) ∈ ℝ)
46	40, 45	remulcld 10742	. . . . . . . . . . . . 13 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) ∈ ℝ)
47	35, 46	fsumrecl 15177	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) ∈ ℝ)
48		vmacl 25847	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → (Λ‘𝑛) ∈ ℝ)
49	27, 48	syl 17	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈ ℝ)
50	28	relogcld 25358	. . . . . . . . . . . . 13 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘𝑛) ∈ ℝ)
51	49, 50	remulcld 10742	. . . . . . . . . . . 12 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · (log‘𝑛)) ∈ ℝ)
52	47, 51	resubcld 11139	. . . . . . . . . . 11 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))) ∈ ℝ)
53	31, 52	remulcld 10742	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) ∈ ℝ)
54	24, 53	fsumrecl 15177	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) ∈ ℝ)
55	54	recnd 10740	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) ∈ ℂ)
56	23, 55	mulcld 10732	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) ∈ ℂ)
57	20, 56	subcld 11068	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 · ((𝑅‘𝑥) · (log‘𝑥))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))))) ∈ ℂ)
58	4	recnd 10740	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ∈ ℂ)
59		2cnd 11787	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 2 ∈ ℂ)
60	12	rpne0d 12512	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ≠ 0)
61		2ne0 11813	. . . . . . 7 ⊢ 2 ≠ 0
62	61	a1i 11	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 2 ≠ 0)
63	57, 58, 59, 60, 62	divdiv32d 11512	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((2 · ((𝑅‘𝑥) · (log‘𝑥))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))))) / 𝑥) / 2) = ((((2 · ((𝑅‘𝑥) · (log‘𝑥))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))))) / 2) / 𝑥))
64	57, 58, 60	divcld 11487	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((2 · ((𝑅‘𝑥) · (log‘𝑥))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))))) / 𝑥) ∈ ℂ)
65	64, 59, 62	divrecd 11490	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((2 · ((𝑅‘𝑥) · (log‘𝑥))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))))) / 𝑥) / 2) = ((((2 · ((𝑅‘𝑥) · (log‘𝑥))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))))) / 𝑥) · (1 / 2)))
66	20, 56, 59, 62	divsubdird 11526	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((2 · ((𝑅‘𝑥) · (log‘𝑥))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))))) / 2) = (((2 · ((𝑅‘𝑥) · (log‘𝑥))) / 2) − (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) / 2)))
67	18	recnd 10740	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑅‘𝑥) · (log‘𝑥)) ∈ ℂ)
68	67, 59, 62	divcan3d 11492	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 · ((𝑅‘𝑥) · (log‘𝑥))) / 2) = ((𝑅‘𝑥) · (log‘𝑥)))
69	21	rpcnd 12509	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ∈ ℂ)
70	21	rpne0d 12512	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ≠ 0)
71	59, 69, 55, 70	div32d 11510	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) = (2 · (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))))
72	71	oveq1d 7179	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) / 2) = ((2 · (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 2))
73	54, 21	rerpdivcld 12538	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥)) ∈ ℝ)
74	73	recnd 10740	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥)) ∈ ℂ)
75	74, 59, 62	divcan3d 11492	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 · (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 2) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥)))
76	72, 75	eqtrd 2773	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) / 2) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥)))
77	68, 76	oveq12d 7182	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((2 · ((𝑅‘𝑥) · (log‘𝑥))) / 2) − (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) / 2)) = (((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))))
78	66, 77	eqtrd 2773	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((2 · ((𝑅‘𝑥) · (log‘𝑥))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))))) / 2) = (((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))))
79	78	oveq1d 7179	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((2 · ((𝑅‘𝑥) · (log‘𝑥))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))))) / 2) / 𝑥) = ((((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 𝑥))
80	63, 65, 79	3eqtr3d 2781	. . . 4 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((2 · ((𝑅‘𝑥) · (log‘𝑥))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))))) / 𝑥) · (1 / 2)) = ((((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 𝑥))
81	80	mpteq2dva 5122	. . 3 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((((2 · ((𝑅‘𝑥) · (log‘𝑥))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))))) / 𝑥) · (1 / 2))) = (𝑥 ∈ (1(,)+∞) ↦ ((((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 𝑥)))
82	22, 54	remulcld 10742	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) ∈ ℝ)
83	19, 82	resubcld 11139	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 · ((𝑅‘𝑥) · (log‘𝑥))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))))) ∈ ℝ)
84	83, 12	rerpdivcld 12538	. . . 4 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((2 · ((𝑅‘𝑥) · (log‘𝑥))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))))) / 𝑥) ∈ ℝ)
85	7	rehalfcld 11956	. . . 4 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (1 / 2) ∈ ℝ)
86	31	recnd 10740	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘(𝑥 / 𝑛)) ∈ ℂ)
87	47	recnd 10740	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) ∈ ℂ)
88	49	recnd 10740	. . . . . . . . . . . . . . . . . 18 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈ ℂ)
89	50	recnd 10740	. . . . . . . . . . . . . . . . . 18 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘𝑛) ∈ ℂ)
90	88, 89	mulcld 10732	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · (log‘𝑛)) ∈ ℂ)
91	86, 87, 90	subdid 11167	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) = (((𝑅‘(𝑥 / 𝑛)) · Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) − ((𝑅‘(𝑥 / 𝑛)) · ((Λ‘𝑛) · (log‘𝑛)))))
92	86, 88, 89	mul12d 10920	. . . . . . . . . . . . . . . . . 18 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑅‘(𝑥 / 𝑛)) · ((Λ‘𝑛) · (log‘𝑛))) = ((Λ‘𝑛) · ((𝑅‘(𝑥 / 𝑛)) · (log‘𝑛))))
93	88, 86, 89	mulassd 10735	. . . . . . . . . . . . . . . . . 18 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)) = ((Λ‘𝑛) · ((𝑅‘(𝑥 / 𝑛)) · (log‘𝑛))))
94	92, 93	eqtr4d 2776	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑅‘(𝑥 / 𝑛)) · ((Λ‘𝑛) · (log‘𝑛))) = (((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))
95	94	oveq2d 7180	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑅‘(𝑥 / 𝑛)) · Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) − ((𝑅‘(𝑥 / 𝑛)) · ((Λ‘𝑛) · (log‘𝑛)))) = (((𝑅‘(𝑥 / 𝑛)) · Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) − (((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛))))
96	91, 95	eqtrd 2773	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) = (((𝑅‘(𝑥 / 𝑛)) · Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) − (((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛))))
97	96	sumeq2dv 15146	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑅‘(𝑥 / 𝑛)) · Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) − (((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛))))
98	86, 87	mulcld 10732	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑅‘(𝑥 / 𝑛)) · Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) ∈ ℂ)
99	88, 86	mulcld 10732	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) ∈ ℂ)
100	99, 89	mulcld 10732	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)) ∈ ℂ)
101	24, 98, 100	fsumsub 15229	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((𝑅‘(𝑥 / 𝑛)) · Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) − (((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛))))
102	46	recnd 10740	. . . . . . . . . . . . . . . . . 18 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) ∈ ℂ)
103	35, 86, 102	fsummulc2 15225	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑅‘(𝑥 / 𝑛)) · Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) = Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((𝑅‘(𝑥 / 𝑛)) · ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))))
104	103	sumeq2dv 15146	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) = Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((𝑅‘(𝑥 / 𝑛)) · ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))))
105		oveq2 7172	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = (𝑚 · 𝑘) → (𝑥 / 𝑛) = (𝑥 / (𝑚 · 𝑘)))
106	105	fveq2d 6672	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = (𝑚 · 𝑘) → (𝑅‘(𝑥 / 𝑛)) = (𝑅‘(𝑥 / (𝑚 · 𝑘))))
107		fvoveq1 7187	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = (𝑚 · 𝑘) → (Λ‘(𝑛 / 𝑚)) = (Λ‘((𝑚 · 𝑘) / 𝑚)))
108	107	oveq2d 7180	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = (𝑚 · 𝑘) → ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) = ((Λ‘𝑚) · (Λ‘((𝑚 · 𝑘) / 𝑚))))
109	106, 108	oveq12d 7182	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = (𝑚 · 𝑘) → ((𝑅‘(𝑥 / 𝑛)) · ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) = ((𝑅‘(𝑥 / (𝑚 · 𝑘))) · ((Λ‘𝑚) · (Λ‘((𝑚 · 𝑘) / 𝑚)))))
110	31	adantrr 717	. . . . . . . . . . . . . . . . . . 19 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛})) → (𝑅‘(𝑥 / 𝑛)) ∈ ℝ)
111	40	anasss 470	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛})) → (Λ‘𝑚) ∈ ℝ)
112	45	anasss 470	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛})) → (Λ‘(𝑛 / 𝑚)) ∈ ℝ)
113	111, 112	remulcld 10742	. . . . . . . . . . . . . . . . . . 19 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛})) → ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) ∈ ℝ)
114	110, 113	remulcld 10742	. . . . . . . . . . . . . . . . . 18 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛})) → ((𝑅‘(𝑥 / 𝑛)) · ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) ∈ ℝ)
115	114	recnd 10740	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛})) → ((𝑅‘(𝑥 / 𝑛)) · ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) ∈ ℂ)
116	109, 4, 115	dvdsflsumcom 25917	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((𝑅‘(𝑥 / 𝑛)) · ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) = Σ𝑚 ∈ (1...(⌊‘𝑥))Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((𝑅‘(𝑥 / (𝑚 · 𝑘))) · ((Λ‘𝑚) · (Λ‘((𝑚 · 𝑘) / 𝑚)))))
117	58	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → 𝑥 ∈ ℂ)
118		elfznn 13020	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑚 ∈ (1...(⌊‘𝑥)) → 𝑚 ∈ ℕ)
119	118	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → 𝑚 ∈ ℕ)
120	119	nnrpd 12505	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → 𝑚 ∈ ℝ⁺)
121	120	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → 𝑚 ∈ ℝ⁺)
122	121	rpcnd 12509	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → 𝑚 ∈ ℂ)
123		elfznn 13020	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚))) → 𝑘 ∈ ℕ)
124	123	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → 𝑘 ∈ ℕ)
125	124	nncnd 11725	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → 𝑘 ∈ ℂ)
126	121	rpne0d 12512	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → 𝑚 ≠ 0)
127	124	nnne0d 11759	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → 𝑘 ≠ 0)
128	117, 122, 125, 126, 127	divdiv1d 11518	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → ((𝑥 / 𝑚) / 𝑘) = (𝑥 / (𝑚 · 𝑘)))
129	128	eqcomd 2744	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → (𝑥 / (𝑚 · 𝑘)) = ((𝑥 / 𝑚) / 𝑘))
130	129	fveq2d 6672	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → (𝑅‘(𝑥 / (𝑚 · 𝑘))) = (𝑅‘((𝑥 / 𝑚) / 𝑘)))
131	125, 122, 126	divcan3d 11492	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → ((𝑚 · 𝑘) / 𝑚) = 𝑘)
132	131	fveq2d 6672	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → (Λ‘((𝑚 · 𝑘) / 𝑚)) = (Λ‘𝑘))
133	132	oveq2d 7180	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → ((Λ‘𝑚) · (Λ‘((𝑚 · 𝑘) / 𝑚))) = ((Λ‘𝑚) · (Λ‘𝑘)))
134	130, 133	oveq12d 7182	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → ((𝑅‘(𝑥 / (𝑚 · 𝑘))) · ((Λ‘𝑚) · (Λ‘((𝑚 · 𝑘) / 𝑚)))) = ((𝑅‘((𝑥 / 𝑚) / 𝑘)) · ((Λ‘𝑚) · (Λ‘𝑘))))
135	12	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → 𝑥 ∈ ℝ⁺)
136	135, 121	rpdivcld 12524	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → (𝑥 / 𝑚) ∈ ℝ⁺)
137	124	nnrpd 12505	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → 𝑘 ∈ ℝ⁺)
138	136, 137	rpdivcld 12524	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → ((𝑥 / 𝑚) / 𝑘) ∈ ℝ⁺)
139	14	ffvelrni 6854	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑥 / 𝑚) / 𝑘) ∈ ℝ⁺ → (𝑅‘((𝑥 / 𝑚) / 𝑘)) ∈ ℝ)
140	138, 139	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → (𝑅‘((𝑥 / 𝑚) / 𝑘)) ∈ ℝ)
141	140	recnd 10740	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → (𝑅‘((𝑥 / 𝑚) / 𝑘)) ∈ ℂ)
142	119, 39	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑚) ∈ ℝ)
143	142	recnd 10740	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑚) ∈ ℂ)
144	143	adantr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → (Λ‘𝑚) ∈ ℂ)
145		vmacl 25847	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 ∈ ℕ → (Λ‘𝑘) ∈ ℝ)
146	124, 145	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → (Λ‘𝑘) ∈ ℝ)
147	146	recnd 10740	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → (Λ‘𝑘) ∈ ℂ)
148	144, 147	mulcld 10732	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → ((Λ‘𝑚) · (Λ‘𝑘)) ∈ ℂ)
149	141, 148	mulcomd 10733	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → ((𝑅‘((𝑥 / 𝑚) / 𝑘)) · ((Λ‘𝑚) · (Λ‘𝑘))) = (((Λ‘𝑚) · (Λ‘𝑘)) · (𝑅‘((𝑥 / 𝑚) / 𝑘))))
150	144, 147, 141	mulassd 10735	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → (((Λ‘𝑚) · (Λ‘𝑘)) · (𝑅‘((𝑥 / 𝑚) / 𝑘))) = ((Λ‘𝑚) · ((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))))
151	134, 149, 150	3eqtrd 2777	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → ((𝑅‘(𝑥 / (𝑚 · 𝑘))) · ((Λ‘𝑚) · (Λ‘((𝑚 · 𝑘) / 𝑚)))) = ((Λ‘𝑚) · ((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))))
152	151	sumeq2dv 15146	. . . . . . . . . . . . . . . . . 18 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((𝑅‘(𝑥 / (𝑚 · 𝑘))) · ((Λ‘𝑚) · (Λ‘((𝑚 · 𝑘) / 𝑚)))) = Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑚) · ((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))))
153		fzfid 13425	. . . . . . . . . . . . . . . . . . 19 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (1...(⌊‘(𝑥 / 𝑚))) ∈ Fin)
154	146, 140	remulcld 10742	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → ((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘))) ∈ ℝ)
155	154	recnd 10740	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → ((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘))) ∈ ℂ)
156	153, 143, 155	fsummulc2 15225	. . . . . . . . . . . . . . . . . 18 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))) = Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑚) · ((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))))
157	152, 156	eqtr4d 2776	. . . . . . . . . . . . . . . . 17 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((𝑅‘(𝑥 / (𝑚 · 𝑘))) · ((Λ‘𝑚) · (Λ‘((𝑚 · 𝑘) / 𝑚)))) = ((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))))
158	157	sumeq2dv 15146	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑚 ∈ (1...(⌊‘𝑥))Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((𝑅‘(𝑥 / (𝑚 · 𝑘))) · ((Λ‘𝑚) · (Λ‘((𝑚 · 𝑘) / 𝑚)))) = Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))))
159	104, 116, 158	3eqtrd 2777	. . . . . . . . . . . . . . 15 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) = Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))))
160	159	oveq1d 7179	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛))) = (Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛))))
161	97, 101, 160	3eqtrd 2777	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) = (Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛))))
162	161	oveq2d 7180	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) = ((2 / (log‘𝑥)) · (Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))))
163	153, 154	fsumrecl 15177	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘))) ∈ ℝ)
164	142, 163	remulcld 10742	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))) ∈ ℝ)
165	24, 164	fsumrecl 15177	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))) ∈ ℝ)
166	165	recnd 10740	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))) ∈ ℂ)
167	49, 31	remulcld 10742	. . . . . . . . . . . . . . . 16 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) ∈ ℝ)
168	167, 50	remulcld 10742	. . . . . . . . . . . . . . 15 ⊢ (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)) ∈ ℝ)
169	24, 168	fsumrecl 15177	. . . . . . . . . . . . . 14 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)) ∈ ℝ)
170	169	recnd 10740	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)) ∈ ℂ)
171	23, 166, 170	subdid 11167	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · (Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) = (((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘))))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))))
172	162, 171	eqtrd 2773	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) = (((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘))))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))))
173	172	oveq2d 7180	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 · ((𝑅‘𝑥) · (log‘𝑥))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))))) = ((2 · ((𝑅‘𝑥) · (log‘𝑥))) − (((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘))))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛))))))
174	23, 166	mulcld 10732	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘))))) ∈ ℂ)
175	22, 169	remulcld 10742	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛))) ∈ ℝ)
176	175	recnd 10740	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛))) ∈ ℂ)
177	20, 174, 176	subsub3d 11098	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 · ((𝑅‘𝑥) · (log‘𝑥))) − (((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘))))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛))))) = (((2 · ((𝑅‘𝑥) · (log‘𝑥))) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) − ((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))))))
178	173, 177	eqtrd 2773	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 · ((𝑅‘𝑥) · (log‘𝑥))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))))) = (((2 · ((𝑅‘𝑥) · (log‘𝑥))) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) − ((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))))))
179	67	2timesd 11952	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (2 · ((𝑅‘𝑥) · (log‘𝑥))) = (((𝑅‘𝑥) · (log‘𝑥)) + ((𝑅‘𝑥) · (log‘𝑥))))
180	179	oveq1d 7179	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 · ((𝑅‘𝑥) · (log‘𝑥))) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) = ((((𝑅‘𝑥) · (log‘𝑥)) + ((𝑅‘𝑥) · (log‘𝑥))) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))))
181	67, 176, 67	add32d 10938	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((𝑅‘𝑥) · (log‘𝑥)) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) + ((𝑅‘𝑥) · (log‘𝑥))) = ((((𝑅‘𝑥) · (log‘𝑥)) + ((𝑅‘𝑥) · (log‘𝑥))) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))))
182	180, 181	eqtr4d 2776	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 · ((𝑅‘𝑥) · (log‘𝑥))) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) = ((((𝑅‘𝑥) · (log‘𝑥)) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) + ((𝑅‘𝑥) · (log‘𝑥))))
183	182	oveq1d 7179	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((2 · ((𝑅‘𝑥) · (log‘𝑥))) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) − ((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))))) = (((((𝑅‘𝑥) · (log‘𝑥)) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) + ((𝑅‘𝑥) · (log‘𝑥))) − ((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))))))
184	18, 175	readdcld 10741	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑅‘𝑥) · (log‘𝑥)) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) ∈ ℝ)
185	184	recnd 10740	. . . . . . . . . 10 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑅‘𝑥) · (log‘𝑥)) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) ∈ ℂ)
186	185, 67, 174	addsubassd 11088	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((((𝑅‘𝑥) · (log‘𝑥)) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) + ((𝑅‘𝑥) · (log‘𝑥))) − ((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))))) = ((((𝑅‘𝑥) · (log‘𝑥)) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) + (((𝑅‘𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘))))))))
187	178, 183, 186	3eqtrd 2777	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 · ((𝑅‘𝑥) · (log‘𝑥))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))))) = ((((𝑅‘𝑥) · (log‘𝑥)) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) + (((𝑅‘𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘))))))))
188	187	oveq1d 7179	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((2 · ((𝑅‘𝑥) · (log‘𝑥))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))))) / 𝑥) = (((((𝑅‘𝑥) · (log‘𝑥)) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) + (((𝑅‘𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘))))))) / 𝑥))
189	67, 174	subcld 11068	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑅‘𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))))) ∈ ℂ)
190	185, 189, 58, 60	divdird 11525	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((((𝑅‘𝑥) · (log‘𝑥)) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) + (((𝑅‘𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘))))))) / 𝑥) = (((((𝑅‘𝑥) · (log‘𝑥)) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) / 𝑥) + ((((𝑅‘𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))))) / 𝑥)))
191	188, 190	eqtrd 2773	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((2 · ((𝑅‘𝑥) · (log‘𝑥))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))))) / 𝑥) = (((((𝑅‘𝑥) · (log‘𝑥)) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) / 𝑥) + ((((𝑅‘𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))))) / 𝑥)))
192	191	mpteq2dva 5122	. . . . 5 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((2 · ((𝑅‘𝑥) · (log‘𝑥))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))))) / 𝑥)) = (𝑥 ∈ (1(,)+∞) ↦ (((((𝑅‘𝑥) · (log‘𝑥)) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) / 𝑥) + ((((𝑅‘𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))))) / 𝑥))))
193	184, 12	rerpdivcld 12538	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((𝑅‘𝑥) · (log‘𝑥)) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) / 𝑥) ∈ ℝ)
194	22, 165	remulcld 10742	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘))))) ∈ ℝ)
195	18, 194	resubcld 11139	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑅‘𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))))) ∈ ℝ)
196	195, 12	rerpdivcld 12538	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((𝑅‘𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))))) / 𝑥) ∈ ℝ)
197	13	selberg3r 26297	. . . . . . 7 ⊢ (𝑥 ∈ (1(,)+∞) ↦ ((((𝑅‘𝑥) · (log‘𝑥)) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) / 𝑥)) ∈ 𝑂(1)
198	197	a1i 11	. . . . . 6 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((((𝑅‘𝑥) · (log‘𝑥)) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) / 𝑥)) ∈ 𝑂(1))
199	13	selberg4r 26298	. . . . . . 7 ⊢ (𝑥 ∈ (1(,)+∞) ↦ ((((𝑅‘𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))))) / 𝑥)) ∈ 𝑂(1)
200	199	a1i 11	. . . . . 6 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((((𝑅‘𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))))) / 𝑥)) ∈ 𝑂(1))
201	193, 196, 198, 200	o1add2 15064	. . . . 5 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((((𝑅‘𝑥) · (log‘𝑥)) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) / 𝑥) + ((((𝑅‘𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑘) · (𝑅‘((𝑥 / 𝑚) / 𝑘)))))) / 𝑥))) ∈ 𝑂(1))
202	192, 201	eqeltrd 2833	. . . 4 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((2 · ((𝑅‘𝑥) · (log‘𝑥))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))))) / 𝑥)) ∈ 𝑂(1))
203		ioossre 12875	. . . . 5 ⊢ (1(,)+∞) ⊆ ℝ
204		1cnd 10707	. . . . . 6 ⊢ (⊤ → 1 ∈ ℂ)
205	204	halfcld 11954	. . . . 5 ⊢ (⊤ → (1 / 2) ∈ ℂ)
206		o1const 15060	. . . . 5 ⊢ (((1(,)+∞) ⊆ ℝ ∧ (1 / 2) ∈ ℂ) → (𝑥 ∈ (1(,)+∞) ↦ (1 / 2)) ∈ 𝑂(1))
207	203, 205, 206	sylancr 590	. . . 4 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (1 / 2)) ∈ 𝑂(1))
208	84, 85, 202, 207	o1mul2 15065	. . 3 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((((2 · ((𝑅‘𝑥) · (log‘𝑥))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))))) / 𝑥) · (1 / 2))) ∈ 𝑂(1))
209	81, 208	eqeltrrd 2834	. 2 ⊢ (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 𝑥)) ∈ 𝑂(1))
210	209	mptru 1549	1 ⊢ (𝑥 ∈ (1(,)+∞) ↦ ((((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 𝑥)) ∈ 𝑂(1)

Colors of variables: wff setvar class

Syntax hints: ∧ wa 399 = wceq 1542 ⊤wtru 1543 ∈ wcel 2113 ≠ wne 2934 {crab 3057 ⊆ wss 3841 class class class wbr 5027 ↦ cmpt 5107 ‘cfv 6333 (class class class)co 7164 ℂcc 10606 ℝcr 10607 0cc0 10608 1c1 10609 + caddc 10611 · cmul 10613 +∞cpnf 10743 < clt 10746 − cmin 10941 / cdiv 11368 ℕcn 11709 2c2 11764 ℝ⁺crp 12465 (,)cioo 12814 ...cfz 12974 ⌊cfl 13244 𝑂(1)co1 14926 Σcsu 15128 ∥ cdvds 15692 logclog 25290 Λcvma 25821 ψcchp 25822

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2161 ax-12 2178 ax-ext 2710 ax-rep 5151 ax-sep 5164 ax-nul 5171 ax-pow 5229 ax-pr 5293 ax-un 7473 ax-inf2 9170 ax-cnex 10664 ax-resscn 10665 ax-1cn 10666 ax-icn 10667 ax-addcl 10668 ax-addrcl 10669 ax-mulcl 10670 ax-mulrcl 10671 ax-mulcom 10672 ax-addass 10673 ax-mulass 10674 ax-distr 10675 ax-i2m1 10676 ax-1ne0 10677 ax-1rid 10678 ax-rnegex 10679 ax-rrecex 10680 ax-cnre 10681 ax-pre-lttri 10682 ax-pre-lttrn 10683 ax-pre-ltadd 10684 ax-pre-mulgt0 10685 ax-pre-sup 10686 ax-addf 10687 ax-mulf 10688

This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2540 df-eu 2570 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-ne 2935 df-nel 3039 df-ral 3058 df-rex 3059 df-reu 3060 df-rmo 3061 df-rab 3062 df-v 3399 df-sbc 3680 df-csb 3789 df-dif 3844 df-un 3846 df-in 3848 df-ss 3858 df-pss 3860 df-nul 4210 df-if 4412 df-pw 4487 df-sn 4514 df-pr 4516 df-tp 4518 df-op 4520 df-uni 4794 df-int 4834 df-iun 4880 df-iin 4881 df-disj 4993 df-br 5028 df-opab 5090 df-mpt 5108 df-tr 5134 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 6123 df-ord 6169 df-on 6170 df-lim 6171 df-suc 6172 df-iota 6291 df-fun 6335 df-fn 6336 df-f 6337 df-f1 6338 df-fo 6339 df-f1o 6340 df-fv 6341 df-isom 6342 df-riota 7121 df-ov 7167 df-oprab 7168 df-mpo 7169 df-of 7419 df-om 7594 df-1st 7707 df-2nd 7708 df-supp 7850 df-wrecs 7969 df-recs 8030 df-rdg 8068 df-1o 8124 df-2o 8125 df-oadd 8128 df-er 8313 df-map 8432 df-pm 8433 df-ixp 8501 df-en 8549 df-dom 8550 df-sdom 8551 df-fin 8552 df-fsupp 8900 df-fi 8941 df-sup 8972 df-inf 8973 df-oi 9040 df-dju 9396 df-card 9434 df-pnf 10748 df-mnf 10749 df-xr 10750 df-ltxr 10751 df-le 10752 df-sub 10943 df-neg 10944 df-div 11369 df-nn 11710 df-2 11772 df-3 11773 df-4 11774 df-5 11775 df-6 11776 df-7 11777 df-8 11778 df-9 11779 df-n0 11970 df-xnn0 12042 df-z 12056 df-dec 12173 df-uz 12318 df-q 12424 df-rp 12466 df-xneg 12583 df-xadd 12584 df-xmul 12585 df-ioo 12818 df-ioc 12819 df-ico 12820 df-icc 12821 df-fz 12975 df-fzo 13118 df-fl 13246 df-mod 13322 df-seq 13454 df-exp 13515 df-fac 13719 df-bc 13748 df-hash 13776 df-shft 14509 df-cj 14541 df-re 14542 df-im 14543 df-sqrt 14677 df-abs 14678 df-limsup 14911 df-clim 14928 df-rlim 14929 df-o1 14930 df-lo1 14931 df-sum 15129 df-ef 15506 df-e 15507 df-sin 15508 df-cos 15509 df-tan 15510 df-pi 15511 df-dvds 15693 df-gcd 15931 df-prm 16106 df-pc 16267 df-struct 16581 df-ndx 16582 df-slot 16583 df-base 16585 df-sets 16586 df-ress 16587 df-plusg 16674 df-mulr 16675 df-starv 16676 df-sca 16677 df-vsca 16678 df-ip 16679 df-tset 16680 df-ple 16681 df-ds 16683 df-unif 16684 df-hom 16685 df-cco 16686 df-rest 16792 df-topn 16793 df-0g 16811 df-gsum 16812 df-topgen 16813 df-pt 16814 df-prds 16817 df-xrs 16871 df-qtop 16876 df-imas 16877 df-xps 16879 df-mre 16953 df-mrc 16954 df-acs 16956 df-mgm 17961 df-sgrp 18010 df-mnd 18021 df-submnd 18066 df-mulg 18336 df-cntz 18558 df-cmn 19019 df-psmet 20202 df-xmet 20203 df-met 20204 df-bl 20205 df-mopn 20206 df-fbas 20207 df-fg 20208 df-cnfld 20211 df-top 21638 df-topon 21655 df-topsp 21677 df-bases 21690 df-cld 21763 df-ntr 21764 df-cls 21765 df-nei 21842 df-lp 21880 df-perf 21881 df-cn 21971 df-cnp 21972 df-haus 22059 df-cmp 22131 df-tx 22306 df-hmeo 22499 df-fil 22590 df-fm 22682 df-flim 22683 df-flf 22684 df-xms 23066 df-ms 23067 df-tms 23068 df-cncf 23623 df-limc 24610 df-dv 24611 df-ulm 25116 df-log 25292 df-cxp 25293 df-atan 25597 df-em 25722 df-cht 25826 df-vma 25827 df-chp 25828 df-ppi 25829 df-mu 25830

This theorem is referenced by: pntrlog2bndlem1 26305

W3C validator