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

Theorem selberg34r 26935
Description: The sum of selberg3r 26933 and selberg4r 26934. (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.
StepHypRef Expression
1 2re 12234 . . . . . . . . . 10 2 ∈ ℝ
21a1i 11 . . . . . . . . 9 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 2 ∈ ℝ)
3 elioore 13301 . . . . . . . . . . . . 13 (π‘₯ ∈ (1(,)+∞) β†’ π‘₯ ∈ ℝ)
43adantl 483 . . . . . . . . . . . 12 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ π‘₯ ∈ ℝ)
5 1rp 12926 . . . . . . . . . . . . 13 1 ∈ ℝ+
65a1i 11 . . . . . . . . . . . 12 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 1 ∈ ℝ+)
7 1red 11163 . . . . . . . . . . . . 13 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 1 ∈ ℝ)
8 eliooord 13330 . . . . . . . . . . . . . . 15 (π‘₯ ∈ (1(,)+∞) β†’ (1 < π‘₯ ∧ π‘₯ < +∞))
98adantl 483 . . . . . . . . . . . . . 14 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (1 < π‘₯ ∧ π‘₯ < +∞))
109simpld 496 . . . . . . . . . . . . 13 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 1 < π‘₯)
117, 4, 10ltled 11310 . . . . . . . . . . . 12 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 1 ≀ π‘₯)
124, 6, 11rpgecld 13003 . . . . . . . . . . 11 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ π‘₯ ∈ ℝ+)
13 pntrval.r . . . . . . . . . . . . 13 𝑅 = (π‘Ž ∈ ℝ+ ↦ ((Οˆβ€˜π‘Ž) βˆ’ π‘Ž))
1413pntrf 26927 . . . . . . . . . . . 12 𝑅:ℝ+βŸΆβ„
1514ffvelcdmi 7039 . . . . . . . . . . 11 (π‘₯ ∈ ℝ+ β†’ (π‘…β€˜π‘₯) ∈ ℝ)
1612, 15syl 17 . . . . . . . . . 10 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘…β€˜π‘₯) ∈ ℝ)
1712relogcld 25994 . . . . . . . . . 10 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (logβ€˜π‘₯) ∈ ℝ)
1816, 17remulcld 11192 . . . . . . . . 9 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯)) ∈ ℝ)
192, 18remulcld 11192 . . . . . . . 8 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (2 Β· ((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯))) ∈ ℝ)
2019recnd 11190 . . . . . . 7 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (2 Β· ((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯))) ∈ β„‚)
214, 10rplogcld 26000 . . . . . . . . . 10 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (logβ€˜π‘₯) ∈ ℝ+)
222, 21rerpdivcld 12995 . . . . . . . . 9 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (2 / (logβ€˜π‘₯)) ∈ ℝ)
2322recnd 11190 . . . . . . . 8 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (2 / (logβ€˜π‘₯)) ∈ β„‚)
24 fzfid 13885 . . . . . . . . . 10 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (1...(βŒŠβ€˜π‘₯)) ∈ Fin)
2512adantr 482 . . . . . . . . . . . . 13 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ π‘₯ ∈ ℝ+)
26 elfznn 13477 . . . . . . . . . . . . . . 15 (𝑛 ∈ (1...(βŒŠβ€˜π‘₯)) β†’ 𝑛 ∈ β„•)
2726adantl 483 . . . . . . . . . . . . . 14 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ 𝑛 ∈ β„•)
2827nnrpd 12962 . . . . . . . . . . . . 13 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ 𝑛 ∈ ℝ+)
2925, 28rpdivcld 12981 . . . . . . . . . . . 12 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (π‘₯ / 𝑛) ∈ ℝ+)
3014ffvelcdmi 7039 . . . . . . . . . . . 12 ((π‘₯ / 𝑛) ∈ ℝ+ β†’ (π‘…β€˜(π‘₯ / 𝑛)) ∈ ℝ)
3129, 30syl 17 . . . . . . . . . . 11 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (π‘…β€˜(π‘₯ / 𝑛)) ∈ ℝ)
32 fzfid 13885 . . . . . . . . . . . . . 14 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (1...𝑛) ∈ Fin)
33 dvdsssfz1 16207 . . . . . . . . . . . . . . 15 (𝑛 ∈ β„• β†’ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} βŠ† (1...𝑛))
3427, 33syl 17 . . . . . . . . . . . . . 14 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} βŠ† (1...𝑛))
3532, 34ssfid 9218 . . . . . . . . . . . . 13 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ∈ Fin)
36 ssrab2 4042 . . . . . . . . . . . . . . . 16 {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} βŠ† β„•
37 simpr 486 . . . . . . . . . . . . . . . 16 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛}) β†’ π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛})
3836, 37sselid 3947 . . . . . . . . . . . . . . 15 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛}) β†’ π‘š ∈ β„•)
39 vmacl 26483 . . . . . . . . . . . . . . 15 (π‘š ∈ β„• β†’ (Ξ›β€˜π‘š) ∈ ℝ)
4038, 39syl 17 . . . . . . . . . . . . . 14 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛}) β†’ (Ξ›β€˜π‘š) ∈ ℝ)
41 dvdsdivcl 16205 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ β„• ∧ π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛}) β†’ (𝑛 / π‘š) ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛})
4227, 41sylan 581 . . . . . . . . . . . . . . . 16 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛}) β†’ (𝑛 / π‘š) ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛})
4336, 42sselid 3947 . . . . . . . . . . . . . . 15 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛}) β†’ (𝑛 / π‘š) ∈ β„•)
44 vmacl 26483 . . . . . . . . . . . . . . 15 ((𝑛 / π‘š) ∈ β„• β†’ (Ξ›β€˜(𝑛 / π‘š)) ∈ ℝ)
4543, 44syl 17 . . . . . . . . . . . . . 14 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛}) β†’ (Ξ›β€˜(𝑛 / π‘š)) ∈ ℝ)
4640, 45remulcld 11192 . . . . . . . . . . . . 13 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛}) β†’ ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) ∈ ℝ)
4735, 46fsumrecl 15626 . . . . . . . . . . . 12 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) ∈ ℝ)
48 vmacl 26483 . . . . . . . . . . . . . 14 (𝑛 ∈ β„• β†’ (Ξ›β€˜π‘›) ∈ ℝ)
4927, 48syl 17 . . . . . . . . . . . . 13 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (Ξ›β€˜π‘›) ∈ ℝ)
5028relogcld 25994 . . . . . . . . . . . . 13 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (logβ€˜π‘›) ∈ ℝ)
5149, 50remulcld 11192 . . . . . . . . . . . 12 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)) ∈ ℝ)
5247, 51resubcld 11590 . . . . . . . . . . 11 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›))) ∈ ℝ)
5331, 52remulcld 11192 . . . . . . . . . 10 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((π‘…β€˜(π‘₯ / 𝑛)) Β· (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)))) ∈ ℝ)
5424, 53fsumrecl 15626 . . . . . . . . 9 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)))) ∈ ℝ)
5554recnd 11190 . . . . . . . 8 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)))) ∈ β„‚)
5623, 55mulcld 11182 . . . . . . 7 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›))))) ∈ β„‚)
5720, 56subcld 11519 . . . . . 6 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((2 Β· ((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯))) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)))))) ∈ β„‚)
584recnd 11190 . . . . . 6 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ π‘₯ ∈ β„‚)
59 2cnd 12238 . . . . . 6 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 2 ∈ β„‚)
6012rpne0d 12969 . . . . . 6 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ π‘₯ β‰  0)
61 2ne0 12264 . . . . . . 7 2 β‰  0
6261a1i 11 . . . . . 6 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 2 β‰  0)
6357, 58, 59, 60, 62divdiv32d 11963 . . . . 5 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((((2 Β· ((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯))) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)))))) / π‘₯) / 2) = ((((2 Β· ((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯))) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)))))) / 2) / π‘₯))
6457, 58, 60divcld 11938 . . . . . 6 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((2 Β· ((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯))) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)))))) / π‘₯) ∈ β„‚)
6564, 59, 62divrecd 11941 . . . . 5 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((((2 Β· ((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯))) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)))))) / π‘₯) / 2) = ((((2 Β· ((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯))) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)))))) / π‘₯) Β· (1 / 2)))
6620, 56, 59, 62divsubdird 11977 . . . . . . 7 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((2 Β· ((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯))) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)))))) / 2) = (((2 Β· ((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯))) / 2) βˆ’ (((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›))))) / 2)))
6718recnd 11190 . . . . . . . . 9 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯)) ∈ β„‚)
6867, 59, 62divcan3d 11943 . . . . . . . 8 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((2 Β· ((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯))) / 2) = ((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯)))
6921rpcnd 12966 . . . . . . . . . . 11 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (logβ€˜π‘₯) ∈ β„‚)
7021rpne0d 12969 . . . . . . . . . . 11 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (logβ€˜π‘₯) β‰  0)
7159, 69, 55, 70div32d 11961 . . . . . . . . . 10 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›))))) = (2 Β· (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)))) / (logβ€˜π‘₯))))
7271oveq1d 7377 . . . . . . . . 9 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›))))) / 2) = ((2 Β· (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)))) / (logβ€˜π‘₯))) / 2))
7354, 21rerpdivcld 12995 . . . . . . . . . . 11 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)))) / (logβ€˜π‘₯)) ∈ ℝ)
7473recnd 11190 . . . . . . . . . 10 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)))) / (logβ€˜π‘₯)) ∈ β„‚)
7574, 59, 62divcan3d 11943 . . . . . . . . 9 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((2 Β· (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)))) / (logβ€˜π‘₯))) / 2) = (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)))) / (logβ€˜π‘₯)))
7672, 75eqtrd 2777 . . . . . . . 8 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›))))) / 2) = (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)))) / (logβ€˜π‘₯)))
7768, 76oveq12d 7380 . . . . . . 7 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((2 Β· ((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯))) / 2) βˆ’ (((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›))))) / 2)) = (((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯)) βˆ’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)))) / (logβ€˜π‘₯))))
7866, 77eqtrd 2777 . . . . . 6 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((2 Β· ((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯))) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)))))) / 2) = (((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯)) βˆ’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)))) / (logβ€˜π‘₯))))
7978oveq1d 7377 . . . . 5 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((((2 Β· ((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯))) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)))))) / 2) / π‘₯) = ((((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯)) βˆ’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)))) / (logβ€˜π‘₯))) / π‘₯))
8063, 65, 793eqtr3d 2785 . . . 4 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((((2 Β· ((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯))) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)))))) / π‘₯) Β· (1 / 2)) = ((((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯)) βˆ’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)))) / (logβ€˜π‘₯))) / π‘₯))
8180mpteq2dva 5210 . . 3 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ ((((2 Β· ((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯))) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)))))) / π‘₯) Β· (1 / 2))) = (π‘₯ ∈ (1(,)+∞) ↦ ((((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯)) βˆ’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)))) / (logβ€˜π‘₯))) / π‘₯)))
8222, 54remulcld 11192 . . . . . 6 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›))))) ∈ ℝ)
8319, 82resubcld 11590 . . . . 5 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((2 Β· ((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯))) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)))))) ∈ ℝ)
8483, 12rerpdivcld 12995 . . . 4 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((2 Β· ((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯))) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)))))) / π‘₯) ∈ ℝ)
857rehalfcld 12407 . . . 4 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (1 / 2) ∈ ℝ)
8631recnd 11190 . . . . . . . . . . . . . . . . 17 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (π‘…β€˜(π‘₯ / 𝑛)) ∈ β„‚)
8747recnd 11190 . . . . . . . . . . . . . . . . 17 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) ∈ β„‚)
8849recnd 11190 . . . . . . . . . . . . . . . . . 18 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (Ξ›β€˜π‘›) ∈ β„‚)
8950recnd 11190 . . . . . . . . . . . . . . . . . 18 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (logβ€˜π‘›) ∈ β„‚)
9088, 89mulcld 11182 . . . . . . . . . . . . . . . . 17 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)) ∈ β„‚)
9186, 87, 90subdid 11618 . . . . . . . . . . . . . . . 16 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((π‘…β€˜(π‘₯ / 𝑛)) Β· (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)))) = (((π‘…β€˜(π‘₯ / 𝑛)) Β· Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š)))) βˆ’ ((π‘…β€˜(π‘₯ / 𝑛)) Β· ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)))))
9286, 88, 89mul12d 11371 . . . . . . . . . . . . . . . . . 18 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((π‘…β€˜(π‘₯ / 𝑛)) Β· ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›))) = ((Ξ›β€˜π‘›) Β· ((π‘…β€˜(π‘₯ / 𝑛)) Β· (logβ€˜π‘›))))
9388, 86, 89mulassd 11185 . . . . . . . . . . . . . . . . . 18 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (((Ξ›β€˜π‘›) Β· (π‘…β€˜(π‘₯ / 𝑛))) Β· (logβ€˜π‘›)) = ((Ξ›β€˜π‘›) Β· ((π‘…β€˜(π‘₯ / 𝑛)) Β· (logβ€˜π‘›))))
9492, 93eqtr4d 2780 . . . . . . . . . . . . . . . . 17 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((π‘…β€˜(π‘₯ / 𝑛)) Β· ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›))) = (((Ξ›β€˜π‘›) Β· (π‘…β€˜(π‘₯ / 𝑛))) Β· (logβ€˜π‘›)))
9594oveq2d 7378 . . . . . . . . . . . . . . . 16 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (((π‘…β€˜(π‘₯ / 𝑛)) Β· Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š)))) βˆ’ ((π‘…β€˜(π‘₯ / 𝑛)) Β· ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)))) = (((π‘…β€˜(π‘₯ / 𝑛)) Β· Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š)))) βˆ’ (((Ξ›β€˜π‘›) Β· (π‘…β€˜(π‘₯ / 𝑛))) Β· (logβ€˜π‘›))))
9691, 95eqtrd 2777 . . . . . . . . . . . . . . 15 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((π‘…β€˜(π‘₯ / 𝑛)) Β· (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)))) = (((π‘…β€˜(π‘₯ / 𝑛)) Β· Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š)))) βˆ’ (((Ξ›β€˜π‘›) Β· (π‘…β€˜(π‘₯ / 𝑛))) Β· (logβ€˜π‘›))))
9796sumeq2dv 15595 . . . . . . . . . . . . . 14 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)))) = Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((π‘…β€˜(π‘₯ / 𝑛)) Β· Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š)))) βˆ’ (((Ξ›β€˜π‘›) Β· (π‘…β€˜(π‘₯ / 𝑛))) Β· (logβ€˜π‘›))))
9886, 87mulcld 11182 . . . . . . . . . . . . . . 15 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((π‘…β€˜(π‘₯ / 𝑛)) Β· Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š)))) ∈ β„‚)
9988, 86mulcld 11182 . . . . . . . . . . . . . . . 16 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((Ξ›β€˜π‘›) Β· (π‘…β€˜(π‘₯ / 𝑛))) ∈ β„‚)
10099, 89mulcld 11182 . . . . . . . . . . . . . . 15 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (((Ξ›β€˜π‘›) Β· (π‘…β€˜(π‘₯ / 𝑛))) Β· (logβ€˜π‘›)) ∈ β„‚)
10124, 98, 100fsumsub 15680 . . . . . . . . . . . . . 14 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((π‘…β€˜(π‘₯ / 𝑛)) Β· Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š)))) βˆ’ (((Ξ›β€˜π‘›) Β· (π‘…β€˜(π‘₯ / 𝑛))) Β· (logβ€˜π‘›))) = (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š)))) βˆ’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) Β· (π‘…β€˜(π‘₯ / 𝑛))) Β· (logβ€˜π‘›))))
10246recnd 11190 . . . . . . . . . . . . . . . . . 18 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛}) β†’ ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) ∈ β„‚)
10335, 86, 102fsummulc2 15676 . . . . . . . . . . . . . . . . 17 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((π‘…β€˜(π‘₯ / 𝑛)) Β· Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š)))) = Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((π‘…β€˜(π‘₯ / 𝑛)) Β· ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š)))))
104103sumeq2dv 15595 . . . . . . . . . . . . . . . 16 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š)))) = Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((π‘…β€˜(π‘₯ / 𝑛)) Β· ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š)))))
105 oveq2 7370 . . . . . . . . . . . . . . . . . . 19 (𝑛 = (π‘š Β· π‘˜) β†’ (π‘₯ / 𝑛) = (π‘₯ / (π‘š Β· π‘˜)))
106105fveq2d 6851 . . . . . . . . . . . . . . . . . 18 (𝑛 = (π‘š Β· π‘˜) β†’ (π‘…β€˜(π‘₯ / 𝑛)) = (π‘…β€˜(π‘₯ / (π‘š Β· π‘˜))))
107 fvoveq1 7385 . . . . . . . . . . . . . . . . . . 19 (𝑛 = (π‘š Β· π‘˜) β†’ (Ξ›β€˜(𝑛 / π‘š)) = (Ξ›β€˜((π‘š Β· π‘˜) / π‘š)))
108107oveq2d 7378 . . . . . . . . . . . . . . . . . 18 (𝑛 = (π‘š Β· π‘˜) β†’ ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) = ((Ξ›β€˜π‘š) Β· (Ξ›β€˜((π‘š Β· π‘˜) / π‘š))))
109106, 108oveq12d 7380 . . . . . . . . . . . . . . . . 17 (𝑛 = (π‘š Β· π‘˜) β†’ ((π‘…β€˜(π‘₯ / 𝑛)) Β· ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š)))) = ((π‘…β€˜(π‘₯ / (π‘š Β· π‘˜))) Β· ((Ξ›β€˜π‘š) Β· (Ξ›β€˜((π‘š Β· π‘˜) / π‘š)))))
11031adantrr 716 . . . . . . . . . . . . . . . . . . 19 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ (𝑛 ∈ (1...(βŒŠβ€˜π‘₯)) ∧ π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛})) β†’ (π‘…β€˜(π‘₯ / 𝑛)) ∈ ℝ)
11140anasss 468 . . . . . . . . . . . . . . . . . . . 20 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ (𝑛 ∈ (1...(βŒŠβ€˜π‘₯)) ∧ π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛})) β†’ (Ξ›β€˜π‘š) ∈ ℝ)
11245anasss 468 . . . . . . . . . . . . . . . . . . . 20 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ (𝑛 ∈ (1...(βŒŠβ€˜π‘₯)) ∧ π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛})) β†’ (Ξ›β€˜(𝑛 / π‘š)) ∈ ℝ)
113111, 112remulcld 11192 . . . . . . . . . . . . . . . . . . 19 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ (𝑛 ∈ (1...(βŒŠβ€˜π‘₯)) ∧ π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛})) β†’ ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) ∈ ℝ)
114110, 113remulcld 11192 . . . . . . . . . . . . . . . . . 18 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ (𝑛 ∈ (1...(βŒŠβ€˜π‘₯)) ∧ π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛})) β†’ ((π‘…β€˜(π‘₯ / 𝑛)) Β· ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š)))) ∈ ℝ)
115114recnd 11190 . . . . . . . . . . . . . . . . 17 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ (𝑛 ∈ (1...(βŒŠβ€˜π‘₯)) ∧ π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛})) β†’ ((π‘…β€˜(π‘₯ / 𝑛)) Β· ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š)))) ∈ β„‚)
116109, 4, 115dvdsflsumcom 26553 . . . . . . . . . . . . . . . 16 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((π‘…β€˜(π‘₯ / 𝑛)) Β· ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š)))) = Ξ£π‘š ∈ (1...(βŒŠβ€˜π‘₯))Ξ£π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))((π‘…β€˜(π‘₯ / (π‘š Β· π‘˜))) Β· ((Ξ›β€˜π‘š) Β· (Ξ›β€˜((π‘š Β· π‘˜) / π‘š)))))
11758ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))) β†’ π‘₯ ∈ β„‚)
118 elfznn 13477 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (π‘š ∈ (1...(βŒŠβ€˜π‘₯)) β†’ π‘š ∈ β„•)
119118adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...(βŒŠβ€˜π‘₯))) β†’ π‘š ∈ β„•)
120119nnrpd 12962 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...(βŒŠβ€˜π‘₯))) β†’ π‘š ∈ ℝ+)
121120adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))) β†’ π‘š ∈ ℝ+)
122121rpcnd 12966 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))) β†’ π‘š ∈ β„‚)
123 elfznn 13477 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š))) β†’ π‘˜ ∈ β„•)
124123adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))) β†’ π‘˜ ∈ β„•)
125124nncnd 12176 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))) β†’ π‘˜ ∈ β„‚)
126121rpne0d 12969 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))) β†’ π‘š β‰  0)
127124nnne0d 12210 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))) β†’ π‘˜ β‰  0)
128117, 122, 125, 126, 127divdiv1d 11969 . . . . . . . . . . . . . . . . . . . . . . 23 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))) β†’ ((π‘₯ / π‘š) / π‘˜) = (π‘₯ / (π‘š Β· π‘˜)))
129128eqcomd 2743 . . . . . . . . . . . . . . . . . . . . . 22 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))) β†’ (π‘₯ / (π‘š Β· π‘˜)) = ((π‘₯ / π‘š) / π‘˜))
130129fveq2d 6851 . . . . . . . . . . . . . . . . . . . . 21 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))) β†’ (π‘…β€˜(π‘₯ / (π‘š Β· π‘˜))) = (π‘…β€˜((π‘₯ / π‘š) / π‘˜)))
131125, 122, 126divcan3d 11943 . . . . . . . . . . . . . . . . . . . . . . 23 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))) β†’ ((π‘š Β· π‘˜) / π‘š) = π‘˜)
132131fveq2d 6851 . . . . . . . . . . . . . . . . . . . . . 22 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))) β†’ (Ξ›β€˜((π‘š Β· π‘˜) / π‘š)) = (Ξ›β€˜π‘˜))
133132oveq2d 7378 . . . . . . . . . . . . . . . . . . . . 21 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))) β†’ ((Ξ›β€˜π‘š) Β· (Ξ›β€˜((π‘š Β· π‘˜) / π‘š))) = ((Ξ›β€˜π‘š) Β· (Ξ›β€˜π‘˜)))
134130, 133oveq12d 7380 . . . . . . . . . . . . . . . . . . . 20 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))) β†’ ((π‘…β€˜(π‘₯ / (π‘š Β· π‘˜))) Β· ((Ξ›β€˜π‘š) Β· (Ξ›β€˜((π‘š Β· π‘˜) / π‘š)))) = ((π‘…β€˜((π‘₯ / π‘š) / π‘˜)) Β· ((Ξ›β€˜π‘š) Β· (Ξ›β€˜π‘˜))))
13512ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))) β†’ π‘₯ ∈ ℝ+)
136135, 121rpdivcld 12981 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))) β†’ (π‘₯ / π‘š) ∈ ℝ+)
137124nnrpd 12962 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))) β†’ π‘˜ ∈ ℝ+)
138136, 137rpdivcld 12981 . . . . . . . . . . . . . . . . . . . . . . 23 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))) β†’ ((π‘₯ / π‘š) / π‘˜) ∈ ℝ+)
13914ffvelcdmi 7039 . . . . . . . . . . . . . . . . . . . . . . 23 (((π‘₯ / π‘š) / π‘˜) ∈ ℝ+ β†’ (π‘…β€˜((π‘₯ / π‘š) / π‘˜)) ∈ ℝ)
140138, 139syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))) β†’ (π‘…β€˜((π‘₯ / π‘š) / π‘˜)) ∈ ℝ)
141140recnd 11190 . . . . . . . . . . . . . . . . . . . . 21 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))) β†’ (π‘…β€˜((π‘₯ / π‘š) / π‘˜)) ∈ β„‚)
142119, 39syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (Ξ›β€˜π‘š) ∈ ℝ)
143142recnd 11190 . . . . . . . . . . . . . . . . . . . . . . 23 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (Ξ›β€˜π‘š) ∈ β„‚)
144143adantr 482 . . . . . . . . . . . . . . . . . . . . . 22 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))) β†’ (Ξ›β€˜π‘š) ∈ β„‚)
145 vmacl 26483 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘˜ ∈ β„• β†’ (Ξ›β€˜π‘˜) ∈ ℝ)
146124, 145syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))) β†’ (Ξ›β€˜π‘˜) ∈ ℝ)
147146recnd 11190 . . . . . . . . . . . . . . . . . . . . . 22 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))) β†’ (Ξ›β€˜π‘˜) ∈ β„‚)
148144, 147mulcld 11182 . . . . . . . . . . . . . . . . . . . . 21 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))) β†’ ((Ξ›β€˜π‘š) Β· (Ξ›β€˜π‘˜)) ∈ β„‚)
149141, 148mulcomd 11183 . . . . . . . . . . . . . . . . . . . 20 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))) β†’ ((π‘…β€˜((π‘₯ / π‘š) / π‘˜)) Β· ((Ξ›β€˜π‘š) Β· (Ξ›β€˜π‘˜))) = (((Ξ›β€˜π‘š) Β· (Ξ›β€˜π‘˜)) Β· (π‘…β€˜((π‘₯ / π‘š) / π‘˜))))
150144, 147, 141mulassd 11185 . . . . . . . . . . . . . . . . . . . 20 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))) β†’ (((Ξ›β€˜π‘š) Β· (Ξ›β€˜π‘˜)) Β· (π‘…β€˜((π‘₯ / π‘š) / π‘˜))) = ((Ξ›β€˜π‘š) Β· ((Ξ›β€˜π‘˜) Β· (π‘…β€˜((π‘₯ / π‘š) / π‘˜)))))
151134, 149, 1503eqtrd 2781 . . . . . . . . . . . . . . . . . . 19 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))) β†’ ((π‘…β€˜(π‘₯ / (π‘š Β· π‘˜))) Β· ((Ξ›β€˜π‘š) Β· (Ξ›β€˜((π‘š Β· π‘˜) / π‘š)))) = ((Ξ›β€˜π‘š) Β· ((Ξ›β€˜π‘˜) Β· (π‘…β€˜((π‘₯ / π‘š) / π‘˜)))))
152151sumeq2dv 15595 . . . . . . . . . . . . . . . . . 18 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...(βŒŠβ€˜π‘₯))) β†’ Ξ£π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))((π‘…β€˜(π‘₯ / (π‘š Β· π‘˜))) Β· ((Ξ›β€˜π‘š) Β· (Ξ›β€˜((π‘š Β· π‘˜) / π‘š)))) = Ξ£π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))((Ξ›β€˜π‘š) Β· ((Ξ›β€˜π‘˜) Β· (π‘…β€˜((π‘₯ / π‘š) / π‘˜)))))
153 fzfid 13885 . . . . . . . . . . . . . . . . . . 19 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (1...(βŒŠβ€˜(π‘₯ / π‘š))) ∈ Fin)
154146, 140remulcld 11192 . . . . . . . . . . . . . . . . . . . 20 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))) β†’ ((Ξ›β€˜π‘˜) Β· (π‘…β€˜((π‘₯ / π‘š) / π‘˜))) ∈ ℝ)
155154recnd 11190 . . . . . . . . . . . . . . . . . . 19 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))) β†’ ((Ξ›β€˜π‘˜) Β· (π‘…β€˜((π‘₯ / π‘š) / π‘˜))) ∈ β„‚)
156153, 143, 155fsummulc2 15676 . . . . . . . . . . . . . . . . . 18 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((Ξ›β€˜π‘š) Β· Ξ£π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))((Ξ›β€˜π‘˜) Β· (π‘…β€˜((π‘₯ / π‘š) / π‘˜)))) = Ξ£π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))((Ξ›β€˜π‘š) Β· ((Ξ›β€˜π‘˜) Β· (π‘…β€˜((π‘₯ / π‘š) / π‘˜)))))
157152, 156eqtr4d 2780 . . . . . . . . . . . . . . . . 17 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...(βŒŠβ€˜π‘₯))) β†’ Ξ£π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))((π‘…β€˜(π‘₯ / (π‘š Β· π‘˜))) Β· ((Ξ›β€˜π‘š) Β· (Ξ›β€˜((π‘š Β· π‘˜) / π‘š)))) = ((Ξ›β€˜π‘š) Β· Ξ£π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))((Ξ›β€˜π‘˜) Β· (π‘…β€˜((π‘₯ / π‘š) / π‘˜)))))
158157sumeq2dv 15595 . . . . . . . . . . . . . . . 16 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Ξ£π‘š ∈ (1...(βŒŠβ€˜π‘₯))Ξ£π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))((π‘…β€˜(π‘₯ / (π‘š Β· π‘˜))) Β· ((Ξ›β€˜π‘š) Β· (Ξ›β€˜((π‘š Β· π‘˜) / π‘š)))) = Ξ£π‘š ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘š) Β· Ξ£π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))((Ξ›β€˜π‘˜) Β· (π‘…β€˜((π‘₯ / π‘š) / π‘˜)))))
159104, 116, 1583eqtrd 2781 . . . . . . . . . . . . . . 15 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š)))) = Ξ£π‘š ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘š) Β· Ξ£π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))((Ξ›β€˜π‘˜) Β· (π‘…β€˜((π‘₯ / π‘š) / π‘˜)))))
160159oveq1d 7377 . . . . . . . . . . . . . 14 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š)))) βˆ’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) Β· (π‘…β€˜(π‘₯ / 𝑛))) Β· (logβ€˜π‘›))) = (Ξ£π‘š ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘š) Β· Ξ£π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))((Ξ›β€˜π‘˜) Β· (π‘…β€˜((π‘₯ / π‘š) / π‘˜)))) βˆ’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) Β· (π‘…β€˜(π‘₯ / 𝑛))) Β· (logβ€˜π‘›))))
16197, 101, 1603eqtrd 2781 . . . . . . . . . . . . 13 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)))) = (Ξ£π‘š ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘š) Β· Ξ£π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))((Ξ›β€˜π‘˜) Β· (π‘…β€˜((π‘₯ / π‘š) / π‘˜)))) βˆ’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) Β· (π‘…β€˜(π‘₯ / 𝑛))) Β· (logβ€˜π‘›))))
162161oveq2d 7378 . . . . . . . . . . . 12 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›))))) = ((2 / (logβ€˜π‘₯)) Β· (Ξ£π‘š ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘š) Β· Ξ£π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))((Ξ›β€˜π‘˜) Β· (π‘…β€˜((π‘₯ / π‘š) / π‘˜)))) βˆ’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) Β· (π‘…β€˜(π‘₯ / 𝑛))) Β· (logβ€˜π‘›)))))
163153, 154fsumrecl 15626 . . . . . . . . . . . . . . . 16 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...(βŒŠβ€˜π‘₯))) β†’ Ξ£π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))((Ξ›β€˜π‘˜) Β· (π‘…β€˜((π‘₯ / π‘š) / π‘˜))) ∈ ℝ)
164142, 163remulcld 11192 . . . . . . . . . . . . . . 15 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((Ξ›β€˜π‘š) Β· Ξ£π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))((Ξ›β€˜π‘˜) Β· (π‘…β€˜((π‘₯ / π‘š) / π‘˜)))) ∈ ℝ)
16524, 164fsumrecl 15626 . . . . . . . . . . . . . 14 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Ξ£π‘š ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘š) Β· Ξ£π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))((Ξ›β€˜π‘˜) Β· (π‘…β€˜((π‘₯ / π‘š) / π‘˜)))) ∈ ℝ)
166165recnd 11190 . . . . . . . . . . . . 13 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Ξ£π‘š ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘š) Β· Ξ£π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))((Ξ›β€˜π‘˜) Β· (π‘…β€˜((π‘₯ / π‘š) / π‘˜)))) ∈ β„‚)
16749, 31remulcld 11192 . . . . . . . . . . . . . . . 16 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((Ξ›β€˜π‘›) Β· (π‘…β€˜(π‘₯ / 𝑛))) ∈ ℝ)
168167, 50remulcld 11192 . . . . . . . . . . . . . . 15 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (((Ξ›β€˜π‘›) Β· (π‘…β€˜(π‘₯ / 𝑛))) Β· (logβ€˜π‘›)) ∈ ℝ)
16924, 168fsumrecl 15626 . . . . . . . . . . . . . 14 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) Β· (π‘…β€˜(π‘₯ / 𝑛))) Β· (logβ€˜π‘›)) ∈ ℝ)
170169recnd 11190 . . . . . . . . . . . . 13 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) Β· (π‘…β€˜(π‘₯ / 𝑛))) Β· (logβ€˜π‘›)) ∈ β„‚)
17123, 166, 170subdid 11618 . . . . . . . . . . . 12 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((2 / (logβ€˜π‘₯)) Β· (Ξ£π‘š ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘š) Β· Ξ£π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))((Ξ›β€˜π‘˜) Β· (π‘…β€˜((π‘₯ / π‘š) / π‘˜)))) βˆ’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) Β· (π‘…β€˜(π‘₯ / 𝑛))) Β· (logβ€˜π‘›)))) = (((2 / (logβ€˜π‘₯)) Β· Ξ£π‘š ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘š) Β· Ξ£π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))((Ξ›β€˜π‘˜) Β· (π‘…β€˜((π‘₯ / π‘š) / π‘˜))))) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) Β· (π‘…β€˜(π‘₯ / 𝑛))) Β· (logβ€˜π‘›)))))
172162, 171eqtrd 2777 . . . . . . . . . . 11 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›))))) = (((2 / (logβ€˜π‘₯)) Β· Ξ£π‘š ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘š) Β· Ξ£π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))((Ξ›β€˜π‘˜) Β· (π‘…β€˜((π‘₯ / π‘š) / π‘˜))))) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) Β· (π‘…β€˜(π‘₯ / 𝑛))) Β· (logβ€˜π‘›)))))
173172oveq2d 7378 . . . . . . . . . 10 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((2 Β· ((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯))) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)))))) = ((2 Β· ((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯))) βˆ’ (((2 / (logβ€˜π‘₯)) Β· Ξ£π‘š ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘š) Β· Ξ£π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))((Ξ›β€˜π‘˜) Β· (π‘…β€˜((π‘₯ / π‘š) / π‘˜))))) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) Β· (π‘…β€˜(π‘₯ / 𝑛))) Β· (logβ€˜π‘›))))))
17423, 166mulcld 11182 . . . . . . . . . . 11 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((2 / (logβ€˜π‘₯)) Β· Ξ£π‘š ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘š) Β· Ξ£π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))((Ξ›β€˜π‘˜) Β· (π‘…β€˜((π‘₯ / π‘š) / π‘˜))))) ∈ β„‚)
17522, 169remulcld 11192 . . . . . . . . . . . 12 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) Β· (π‘…β€˜(π‘₯ / 𝑛))) Β· (logβ€˜π‘›))) ∈ ℝ)
176175recnd 11190 . . . . . . . . . . 11 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) Β· (π‘…β€˜(π‘₯ / 𝑛))) Β· (logβ€˜π‘›))) ∈ β„‚)
17720, 174, 176subsub3d 11549 . . . . . . . . . 10 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((2 Β· ((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯))) βˆ’ (((2 / (logβ€˜π‘₯)) Β· Ξ£π‘š ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘š) Β· Ξ£π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))((Ξ›β€˜π‘˜) Β· (π‘…β€˜((π‘₯ / π‘š) / π‘˜))))) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) Β· (π‘…β€˜(π‘₯ / 𝑛))) Β· (logβ€˜π‘›))))) = (((2 Β· ((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯))) + ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) Β· (π‘…β€˜(π‘₯ / 𝑛))) Β· (logβ€˜π‘›)))) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Ξ£π‘š ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘š) Β· Ξ£π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))((Ξ›β€˜π‘˜) Β· (π‘…β€˜((π‘₯ / π‘š) / π‘˜)))))))
178173, 177eqtrd 2777 . . . . . . . . 9 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((2 Β· ((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯))) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)))))) = (((2 Β· ((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯))) + ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) Β· (π‘…β€˜(π‘₯ / 𝑛))) Β· (logβ€˜π‘›)))) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Ξ£π‘š ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘š) Β· Ξ£π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))((Ξ›β€˜π‘˜) Β· (π‘…β€˜((π‘₯ / π‘š) / π‘˜)))))))
179672timesd 12403 . . . . . . . . . . . 12 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (2 Β· ((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯))) = (((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯)) + ((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯))))
180179oveq1d 7377 . . . . . . . . . . 11 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((2 Β· ((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯))) + ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) Β· (π‘…β€˜(π‘₯ / 𝑛))) Β· (logβ€˜π‘›)))) = ((((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯)) + ((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯))) + ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) Β· (π‘…β€˜(π‘₯ / 𝑛))) Β· (logβ€˜π‘›)))))
18167, 176, 67add32d 11389 . . . . . . . . . . 11 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯)) + ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) Β· (π‘…β€˜(π‘₯ / 𝑛))) Β· (logβ€˜π‘›)))) + ((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯))) = ((((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯)) + ((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯))) + ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) Β· (π‘…β€˜(π‘₯ / 𝑛))) Β· (logβ€˜π‘›)))))
182180, 181eqtr4d 2780 . . . . . . . . . 10 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((2 Β· ((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯))) + ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) Β· (π‘…β€˜(π‘₯ / 𝑛))) Β· (logβ€˜π‘›)))) = ((((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯)) + ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) Β· (π‘…β€˜(π‘₯ / 𝑛))) Β· (logβ€˜π‘›)))) + ((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯))))
183182oveq1d 7377 . . . . . . . . 9 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((2 Β· ((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯))) + ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) Β· (π‘…β€˜(π‘₯ / 𝑛))) Β· (logβ€˜π‘›)))) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Ξ£π‘š ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘š) Β· Ξ£π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))((Ξ›β€˜π‘˜) Β· (π‘…β€˜((π‘₯ / π‘š) / π‘˜)))))) = (((((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯)) + ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) Β· (π‘…β€˜(π‘₯ / 𝑛))) Β· (logβ€˜π‘›)))) + ((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯))) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Ξ£π‘š ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘š) Β· Ξ£π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))((Ξ›β€˜π‘˜) Β· (π‘…β€˜((π‘₯ / π‘š) / π‘˜)))))))
18418, 175readdcld 11191 . . . . . . . . . . 11 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯)) + ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) Β· (π‘…β€˜(π‘₯ / 𝑛))) Β· (logβ€˜π‘›)))) ∈ ℝ)
185184recnd 11190 . . . . . . . . . 10 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯)) + ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) Β· (π‘…β€˜(π‘₯ / 𝑛))) Β· (logβ€˜π‘›)))) ∈ β„‚)
186185, 67, 174addsubassd 11539 . . . . . . . . 9 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯)) + ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) Β· (π‘…β€˜(π‘₯ / 𝑛))) Β· (logβ€˜π‘›)))) + ((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯))) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Ξ£π‘š ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘š) Β· Ξ£π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))((Ξ›β€˜π‘˜) Β· (π‘…β€˜((π‘₯ / π‘š) / π‘˜)))))) = ((((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯)) + ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) Β· (π‘…β€˜(π‘₯ / 𝑛))) Β· (logβ€˜π‘›)))) + (((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯)) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Ξ£π‘š ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘š) Β· Ξ£π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))((Ξ›β€˜π‘˜) Β· (π‘…β€˜((π‘₯ / π‘š) / π‘˜))))))))
187178, 183, 1863eqtrd 2781 . . . . . . . 8 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((2 Β· ((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯))) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)))))) = ((((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯)) + ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) Β· (π‘…β€˜(π‘₯ / 𝑛))) Β· (logβ€˜π‘›)))) + (((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯)) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Ξ£π‘š ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘š) Β· Ξ£π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))((Ξ›β€˜π‘˜) Β· (π‘…β€˜((π‘₯ / π‘š) / π‘˜))))))))
188187oveq1d 7377 . . . . . . 7 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((2 Β· ((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯))) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)))))) / π‘₯) = (((((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯)) + ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) Β· (π‘…β€˜(π‘₯ / 𝑛))) Β· (logβ€˜π‘›)))) + (((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯)) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Ξ£π‘š ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘š) Β· Ξ£π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))((Ξ›β€˜π‘˜) Β· (π‘…β€˜((π‘₯ / π‘š) / π‘˜))))))) / π‘₯))
18967, 174subcld 11519 . . . . . . . 8 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯)) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Ξ£π‘š ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘š) Β· Ξ£π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))((Ξ›β€˜π‘˜) Β· (π‘…β€˜((π‘₯ / π‘š) / π‘˜)))))) ∈ β„‚)
190185, 189, 58, 60divdird 11976 . . . . . . 7 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯)) + ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) Β· (π‘…β€˜(π‘₯ / 𝑛))) Β· (logβ€˜π‘›)))) + (((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯)) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Ξ£π‘š ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘š) Β· Ξ£π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))((Ξ›β€˜π‘˜) Β· (π‘…β€˜((π‘₯ / π‘š) / π‘˜))))))) / π‘₯) = (((((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯)) + ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) Β· (π‘…β€˜(π‘₯ / 𝑛))) Β· (logβ€˜π‘›)))) / π‘₯) + ((((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯)) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Ξ£π‘š ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘š) Β· Ξ£π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))((Ξ›β€˜π‘˜) Β· (π‘…β€˜((π‘₯ / π‘š) / π‘˜)))))) / π‘₯)))
191188, 190eqtrd 2777 . . . . . 6 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((2 Β· ((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯))) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)))))) / π‘₯) = (((((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯)) + ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) Β· (π‘…β€˜(π‘₯ / 𝑛))) Β· (logβ€˜π‘›)))) / π‘₯) + ((((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯)) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Ξ£π‘š ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘š) Β· Ξ£π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))((Ξ›β€˜π‘˜) Β· (π‘…β€˜((π‘₯ / π‘š) / π‘˜)))))) / π‘₯)))
192191mpteq2dva 5210 . . . . 5 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ (((2 Β· ((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯))) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)))))) / π‘₯)) = (π‘₯ ∈ (1(,)+∞) ↦ (((((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯)) + ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) Β· (π‘…β€˜(π‘₯ / 𝑛))) Β· (logβ€˜π‘›)))) / π‘₯) + ((((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯)) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Ξ£π‘š ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘š) Β· Ξ£π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))((Ξ›β€˜π‘˜) Β· (π‘…β€˜((π‘₯ / π‘š) / π‘˜)))))) / π‘₯))))
193184, 12rerpdivcld 12995 . . . . . 6 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯)) + ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) Β· (π‘…β€˜(π‘₯ / 𝑛))) Β· (logβ€˜π‘›)))) / π‘₯) ∈ ℝ)
19422, 165remulcld 11192 . . . . . . . 8 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((2 / (logβ€˜π‘₯)) Β· Ξ£π‘š ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘š) Β· Ξ£π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))((Ξ›β€˜π‘˜) Β· (π‘…β€˜((π‘₯ / π‘š) / π‘˜))))) ∈ ℝ)
19518, 194resubcld 11590 . . . . . . 7 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯)) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Ξ£π‘š ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘š) Β· Ξ£π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))((Ξ›β€˜π‘˜) Β· (π‘…β€˜((π‘₯ / π‘š) / π‘˜)))))) ∈ ℝ)
196195, 12rerpdivcld 12995 . . . . . 6 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯)) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Ξ£π‘š ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘š) Β· Ξ£π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))((Ξ›β€˜π‘˜) Β· (π‘…β€˜((π‘₯ / π‘š) / π‘˜)))))) / π‘₯) ∈ ℝ)
19713selberg3r 26933 . . . . . . 7 (π‘₯ ∈ (1(,)+∞) ↦ ((((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯)) + ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) Β· (π‘…β€˜(π‘₯ / 𝑛))) Β· (logβ€˜π‘›)))) / π‘₯)) ∈ 𝑂(1)
198197a1i 11 . . . . . 6 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ ((((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯)) + ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) Β· (π‘…β€˜(π‘₯ / 𝑛))) Β· (logβ€˜π‘›)))) / π‘₯)) ∈ 𝑂(1))
19913selberg4r 26934 . . . . . . 7 (π‘₯ ∈ (1(,)+∞) ↦ ((((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯)) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Ξ£π‘š ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘š) Β· Ξ£π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))((Ξ›β€˜π‘˜) Β· (π‘…β€˜((π‘₯ / π‘š) / π‘˜)))))) / π‘₯)) ∈ 𝑂(1)
200199a1i 11 . . . . . 6 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ ((((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯)) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Ξ£π‘š ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘š) Β· Ξ£π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))((Ξ›β€˜π‘˜) Β· (π‘…β€˜((π‘₯ / π‘š) / π‘˜)))))) / π‘₯)) ∈ 𝑂(1))
201193, 196, 198, 200o1add2 15513 . . . . 5 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ (((((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯)) + ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) Β· (π‘…β€˜(π‘₯ / 𝑛))) Β· (logβ€˜π‘›)))) / π‘₯) + ((((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯)) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Ξ£π‘š ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘š) Β· Ξ£π‘˜ ∈ (1...(βŒŠβ€˜(π‘₯ / π‘š)))((Ξ›β€˜π‘˜) Β· (π‘…β€˜((π‘₯ / π‘š) / π‘˜)))))) / π‘₯))) ∈ 𝑂(1))
202192, 201eqeltrd 2838 . . . 4 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ (((2 Β· ((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯))) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)))))) / π‘₯)) ∈ 𝑂(1))
203 ioossre 13332 . . . . 5 (1(,)+∞) βŠ† ℝ
204 1cnd 11157 . . . . . 6 (⊀ β†’ 1 ∈ β„‚)
205204halfcld 12405 . . . . 5 (⊀ β†’ (1 / 2) ∈ β„‚)
206 o1const 15509 . . . . 5 (((1(,)+∞) βŠ† ℝ ∧ (1 / 2) ∈ β„‚) β†’ (π‘₯ ∈ (1(,)+∞) ↦ (1 / 2)) ∈ 𝑂(1))
207203, 205, 206sylancr 588 . . . 4 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ (1 / 2)) ∈ 𝑂(1))
20884, 85, 202, 207o1mul2 15514 . . 3 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ ((((2 Β· ((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯))) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)))))) / π‘₯) Β· (1 / 2))) ∈ 𝑂(1))
20981, 208eqeltrrd 2839 . 2 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ ((((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯)) βˆ’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)))) / (logβ€˜π‘₯))) / π‘₯)) ∈ 𝑂(1))
210209mptru 1549 1 (π‘₯ ∈ (1(,)+∞) ↦ ((((π‘…β€˜π‘₯) Β· (logβ€˜π‘₯)) βˆ’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((π‘…β€˜(π‘₯ / 𝑛)) Β· (Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š))) βˆ’ ((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)))) / (logβ€˜π‘₯))) / π‘₯)) ∈ 𝑂(1)
Colors of variables: wff setvar class
Syntax hints:   ∧ wa 397   = wceq 1542  βŠ€wtru 1543   ∈ wcel 2107   β‰  wne 2944  {crab 3410   βŠ† wss 3915   class class class wbr 5110   ↦ cmpt 5193  β€˜cfv 6501  (class class class)co 7362  β„‚cc 11056  β„cr 11057  0cc0 11058  1c1 11059   + caddc 11061   Β· cmul 11063  +∞cpnf 11193   < clt 11196   βˆ’ cmin 11392   / cdiv 11819  β„•cn 12160  2c2 12215  β„+crp 12922  (,)cioo 13271  ...cfz 13431  βŒŠcfl 13702  π‘‚(1)co1 15375  Ξ£csu 15577   βˆ₯ cdvds 16143  logclog 25926  Ξ›cvma 26457  Οˆcchp 26458
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-inf2 9584  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135  ax-pre-sup 11136  ax-addf 11137  ax-mulf 11138
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-tp 4596  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-iin 4962  df-disj 5076  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-se 5594  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-isom 6510  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-of 7622  df-om 7808  df-1st 7926  df-2nd 7927  df-supp 8098  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-2o 8418  df-oadd 8421  df-er 8655  df-map 8774  df-pm 8775  df-ixp 8843  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-fsupp 9313  df-fi 9354  df-sup 9385  df-inf 9386  df-oi 9453  df-dju 9844  df-card 9882  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-div 11820  df-nn 12161  df-2 12223  df-3 12224  df-4 12225  df-5 12226  df-6 12227  df-7 12228  df-8 12229  df-9 12230  df-n0 12421  df-xnn0 12493  df-z 12507  df-dec 12626  df-uz 12771  df-q 12881  df-rp 12923  df-xneg 13040  df-xadd 13041  df-xmul 13042  df-ioo 13275  df-ioc 13276  df-ico 13277  df-icc 13278  df-fz 13432  df-fzo 13575  df-fl 13704  df-mod 13782  df-seq 13914  df-exp 13975  df-fac 14181  df-bc 14210  df-hash 14238  df-shft 14959  df-cj 14991  df-re 14992  df-im 14993  df-sqrt 15127  df-abs 15128  df-limsup 15360  df-clim 15377  df-rlim 15378  df-o1 15379  df-lo1 15380  df-sum 15578  df-ef 15957  df-e 15958  df-sin 15959  df-cos 15960  df-tan 15961  df-pi 15962  df-dvds 16144  df-gcd 16382  df-prm 16555  df-pc 16716  df-struct 17026  df-sets 17043  df-slot 17061  df-ndx 17073  df-base 17091  df-ress 17120  df-plusg 17153  df-mulr 17154  df-starv 17155  df-sca 17156  df-vsca 17157  df-ip 17158  df-tset 17159  df-ple 17160  df-ds 17162  df-unif 17163  df-hom 17164  df-cco 17165  df-rest 17311  df-topn 17312  df-0g 17330  df-gsum 17331  df-topgen 17332  df-pt 17333  df-prds 17336  df-xrs 17391  df-qtop 17396  df-imas 17397  df-xps 17399  df-mre 17473  df-mrc 17474  df-acs 17476  df-mgm 18504  df-sgrp 18553  df-mnd 18564  df-submnd 18609  df-mulg 18880  df-cntz 19104  df-cmn 19571  df-psmet 20804  df-xmet 20805  df-met 20806  df-bl 20807  df-mopn 20808  df-fbas 20809  df-fg 20810  df-cnfld 20813  df-top 22259  df-topon 22276  df-topsp 22298  df-bases 22312  df-cld 22386  df-ntr 22387  df-cls 22388  df-nei 22465  df-lp 22503  df-perf 22504  df-cn 22594  df-cnp 22595  df-haus 22682  df-cmp 22754  df-tx 22929  df-hmeo 23122  df-fil 23213  df-fm 23305  df-flim 23306  df-flf 23307  df-xms 23689  df-ms 23690  df-tms 23691  df-cncf 24257  df-limc 25246  df-dv 25247  df-ulm 25752  df-log 25928  df-cxp 25929  df-atan 26233  df-em 26358  df-cht 26462  df-vma 26463  df-chp 26464  df-ppi 26465  df-mu 26466
This theorem is referenced by:  pntrlog2bndlem1  26941
  Copyright terms: Public domain W3C validator