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

Theorem vmalogdivsum2 26902
Description: The sum Σ𝑛 ≀ π‘₯, Ξ›(𝑛)log(π‘₯ / 𝑛) / 𝑛 is asymptotic to log↑2(π‘₯) / 2 + 𝑂(logπ‘₯). Exercise 9.1.7 of [Shapiro], p. 336. (Contributed by Mario Carneiro, 30-May-2016.)
Assertion
Ref Expression
vmalogdivsum2 (π‘₯ ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) / 𝑛) Β· (logβ€˜(π‘₯ / 𝑛))) / (logβ€˜π‘₯)) βˆ’ ((logβ€˜π‘₯) / 2))) ∈ 𝑂(1)
Distinct variable group:   π‘₯,𝑛

Proof of Theorem vmalogdivsum2
Dummy variables π‘˜ π‘š 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fzfid 13885 . . . . . . . . 9 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (1...(βŒŠβ€˜π‘₯)) ∈ Fin)
2 elfznn 13477 . . . . . . . . . . . . 13 (π‘˜ ∈ (1...(βŒŠβ€˜π‘₯)) β†’ π‘˜ ∈ β„•)
32adantl 483 . . . . . . . . . . . 12 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))) β†’ π‘˜ ∈ β„•)
43nnrpd 12962 . . . . . . . . . . 11 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))) β†’ π‘˜ ∈ ℝ+)
54relogcld 25994 . . . . . . . . . 10 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (logβ€˜π‘˜) ∈ ℝ)
65, 3nndivred 12214 . . . . . . . . 9 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((logβ€˜π‘˜) / π‘˜) ∈ ℝ)
71, 6fsumrecl 15626 . . . . . . . 8 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))((logβ€˜π‘˜) / π‘˜) ∈ ℝ)
87recnd 11190 . . . . . . 7 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))((logβ€˜π‘˜) / π‘˜) ∈ β„‚)
9 elioore 13301 . . . . . . . . . . . . 13 (π‘₯ ∈ (1(,)+∞) β†’ π‘₯ ∈ ℝ)
109adantl 483 . . . . . . . . . . . 12 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ π‘₯ ∈ ℝ)
11 1rp 12926 . . . . . . . . . . . . 13 1 ∈ ℝ+
1211a1i 11 . . . . . . . . . . . 12 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 1 ∈ ℝ+)
13 1red 11163 . . . . . . . . . . . . 13 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 1 ∈ ℝ)
14 eliooord 13330 . . . . . . . . . . . . . . 15 (π‘₯ ∈ (1(,)+∞) β†’ (1 < π‘₯ ∧ π‘₯ < +∞))
1514adantl 483 . . . . . . . . . . . . . 14 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (1 < π‘₯ ∧ π‘₯ < +∞))
1615simpld 496 . . . . . . . . . . . . 13 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 1 < π‘₯)
1713, 10, 16ltled 11310 . . . . . . . . . . . 12 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 1 ≀ π‘₯)
1810, 12, 17rpgecld 13003 . . . . . . . . . . 11 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ π‘₯ ∈ ℝ+)
1918relogcld 25994 . . . . . . . . . 10 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (logβ€˜π‘₯) ∈ ℝ)
2019resqcld 14037 . . . . . . . . 9 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((logβ€˜π‘₯)↑2) ∈ ℝ)
2120rehalfcld 12407 . . . . . . . 8 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((logβ€˜π‘₯)↑2) / 2) ∈ ℝ)
2221recnd 11190 . . . . . . 7 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((logβ€˜π‘₯)↑2) / 2) ∈ β„‚)
2319recnd 11190 . . . . . . 7 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (logβ€˜π‘₯) ∈ β„‚)
2410, 16rplogcld 26000 . . . . . . . 8 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (logβ€˜π‘₯) ∈ ℝ+)
2524rpne0d 12969 . . . . . . 7 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (logβ€˜π‘₯) β‰  0)
268, 22, 23, 25divsubdird 11977 . . . . . 6 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))((logβ€˜π‘˜) / π‘˜) βˆ’ (((logβ€˜π‘₯)↑2) / 2)) / (logβ€˜π‘₯)) = ((Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))((logβ€˜π‘˜) / π‘˜) / (logβ€˜π‘₯)) βˆ’ ((((logβ€˜π‘₯)↑2) / 2) / (logβ€˜π‘₯))))
277, 21resubcld 11590 . . . . . . . 8 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))((logβ€˜π‘˜) / π‘˜) βˆ’ (((logβ€˜π‘₯)↑2) / 2)) ∈ ℝ)
2827recnd 11190 . . . . . . 7 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))((logβ€˜π‘˜) / π‘˜) βˆ’ (((logβ€˜π‘₯)↑2) / 2)) ∈ β„‚)
2928, 23, 25divrecd 11941 . . . . . 6 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))((logβ€˜π‘˜) / π‘˜) βˆ’ (((logβ€˜π‘₯)↑2) / 2)) / (logβ€˜π‘₯)) = ((Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))((logβ€˜π‘˜) / π‘˜) βˆ’ (((logβ€˜π‘₯)↑2) / 2)) Β· (1 / (logβ€˜π‘₯))))
3020recnd 11190 . . . . . . . . 9 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((logβ€˜π‘₯)↑2) ∈ β„‚)
31 2cnd 12238 . . . . . . . . 9 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 2 ∈ β„‚)
32 2ne0 12264 . . . . . . . . . 10 2 β‰  0
3332a1i 11 . . . . . . . . 9 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 2 β‰  0)
3430, 31, 23, 33, 25divdiv32d 11963 . . . . . . . 8 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((((logβ€˜π‘₯)↑2) / 2) / (logβ€˜π‘₯)) = ((((logβ€˜π‘₯)↑2) / (logβ€˜π‘₯)) / 2))
3523sqvald 14055 . . . . . . . . . . 11 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((logβ€˜π‘₯)↑2) = ((logβ€˜π‘₯) Β· (logβ€˜π‘₯)))
3635oveq1d 7377 . . . . . . . . . 10 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((logβ€˜π‘₯)↑2) / (logβ€˜π‘₯)) = (((logβ€˜π‘₯) Β· (logβ€˜π‘₯)) / (logβ€˜π‘₯)))
3723, 23, 25divcan3d 11943 . . . . . . . . . 10 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((logβ€˜π‘₯) Β· (logβ€˜π‘₯)) / (logβ€˜π‘₯)) = (logβ€˜π‘₯))
3836, 37eqtrd 2777 . . . . . . . . 9 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((logβ€˜π‘₯)↑2) / (logβ€˜π‘₯)) = (logβ€˜π‘₯))
3938oveq1d 7377 . . . . . . . 8 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((((logβ€˜π‘₯)↑2) / (logβ€˜π‘₯)) / 2) = ((logβ€˜π‘₯) / 2))
4034, 39eqtrd 2777 . . . . . . 7 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((((logβ€˜π‘₯)↑2) / 2) / (logβ€˜π‘₯)) = ((logβ€˜π‘₯) / 2))
4140oveq2d 7378 . . . . . 6 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))((logβ€˜π‘˜) / π‘˜) / (logβ€˜π‘₯)) βˆ’ ((((logβ€˜π‘₯)↑2) / 2) / (logβ€˜π‘₯))) = ((Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))((logβ€˜π‘˜) / π‘˜) / (logβ€˜π‘₯)) βˆ’ ((logβ€˜π‘₯) / 2)))
4226, 29, 413eqtr3rd 2786 . . . . 5 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))((logβ€˜π‘˜) / π‘˜) / (logβ€˜π‘₯)) βˆ’ ((logβ€˜π‘₯) / 2)) = ((Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))((logβ€˜π‘˜) / π‘˜) βˆ’ (((logβ€˜π‘₯)↑2) / 2)) Β· (1 / (logβ€˜π‘₯))))
4342mpteq2dva 5210 . . . 4 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ ((Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))((logβ€˜π‘˜) / π‘˜) / (logβ€˜π‘₯)) βˆ’ ((logβ€˜π‘₯) / 2))) = (π‘₯ ∈ (1(,)+∞) ↦ ((Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))((logβ€˜π‘˜) / π‘˜) βˆ’ (((logβ€˜π‘₯)↑2) / 2)) Β· (1 / (logβ€˜π‘₯)))))
4424rprecred 12975 . . . . 5 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (1 / (logβ€˜π‘₯)) ∈ ℝ)
4518ex 414 . . . . . . 7 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) β†’ π‘₯ ∈ ℝ+))
4645ssrdv 3955 . . . . . 6 (⊀ β†’ (1(,)+∞) βŠ† ℝ+)
47 eqid 2737 . . . . . . . . 9 (π‘₯ ∈ ℝ+ ↦ (Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))((logβ€˜π‘˜) / π‘˜) βˆ’ (((logβ€˜π‘₯)↑2) / 2))) = (π‘₯ ∈ ℝ+ ↦ (Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))((logβ€˜π‘˜) / π‘˜) βˆ’ (((logβ€˜π‘₯)↑2) / 2)))
4847logdivsum 26897 . . . . . . . 8 ((π‘₯ ∈ ℝ+ ↦ (Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))((logβ€˜π‘˜) / π‘˜) βˆ’ (((logβ€˜π‘₯)↑2) / 2))):ℝ+βŸΆβ„ ∧ (π‘₯ ∈ ℝ+ ↦ (Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))((logβ€˜π‘˜) / π‘˜) βˆ’ (((logβ€˜π‘₯)↑2) / 2))) ∈ dom β‡π‘Ÿ ∧ (((π‘₯ ∈ ℝ+ ↦ (Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))((logβ€˜π‘˜) / π‘˜) βˆ’ (((logβ€˜π‘₯)↑2) / 2))) β‡π‘Ÿ 1 ∧ 1 ∈ ℝ+ ∧ e ≀ 1) β†’ (absβ€˜(((π‘₯ ∈ ℝ+ ↦ (Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))((logβ€˜π‘˜) / π‘˜) βˆ’ (((logβ€˜π‘₯)↑2) / 2)))β€˜1) βˆ’ 1)) ≀ ((logβ€˜1) / 1)))
4948simp2i 1141 . . . . . . 7 (π‘₯ ∈ ℝ+ ↦ (Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))((logβ€˜π‘˜) / π‘˜) βˆ’ (((logβ€˜π‘₯)↑2) / 2))) ∈ dom β‡π‘Ÿ
50 rlimdmo1 15507 . . . . . . 7 ((π‘₯ ∈ ℝ+ ↦ (Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))((logβ€˜π‘˜) / π‘˜) βˆ’ (((logβ€˜π‘₯)↑2) / 2))) ∈ dom β‡π‘Ÿ β†’ (π‘₯ ∈ ℝ+ ↦ (Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))((logβ€˜π‘˜) / π‘˜) βˆ’ (((logβ€˜π‘₯)↑2) / 2))) ∈ 𝑂(1))
5149, 50mp1i 13 . . . . . 6 (⊀ β†’ (π‘₯ ∈ ℝ+ ↦ (Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))((logβ€˜π‘˜) / π‘˜) βˆ’ (((logβ€˜π‘₯)↑2) / 2))) ∈ 𝑂(1))
5246, 51o1res2 15452 . . . . 5 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ (Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))((logβ€˜π‘˜) / π‘˜) βˆ’ (((logβ€˜π‘₯)↑2) / 2))) ∈ 𝑂(1))
53 divlogrlim 26006 . . . . . 6 (π‘₯ ∈ (1(,)+∞) ↦ (1 / (logβ€˜π‘₯))) β‡π‘Ÿ 0
54 rlimo1 15506 . . . . . 6 ((π‘₯ ∈ (1(,)+∞) ↦ (1 / (logβ€˜π‘₯))) β‡π‘Ÿ 0 β†’ (π‘₯ ∈ (1(,)+∞) ↦ (1 / (logβ€˜π‘₯))) ∈ 𝑂(1))
5553, 54mp1i 13 . . . . 5 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ (1 / (logβ€˜π‘₯))) ∈ 𝑂(1))
5627, 44, 52, 55o1mul2 15514 . . . 4 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ ((Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))((logβ€˜π‘˜) / π‘˜) βˆ’ (((logβ€˜π‘₯)↑2) / 2)) Β· (1 / (logβ€˜π‘₯)))) ∈ 𝑂(1))
5743, 56eqeltrd 2838 . . 3 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ ((Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))((logβ€˜π‘˜) / π‘˜) / (logβ€˜π‘₯)) βˆ’ ((logβ€˜π‘₯) / 2))) ∈ 𝑂(1))
588, 23, 25divcld 11938 . . . . 5 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))((logβ€˜π‘˜) / π‘˜) / (logβ€˜π‘₯)) ∈ β„‚)
5923halfcld 12405 . . . . 5 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((logβ€˜π‘₯) / 2) ∈ β„‚)
6058, 59subcld 11519 . . . 4 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))((logβ€˜π‘˜) / π‘˜) / (logβ€˜π‘₯)) βˆ’ ((logβ€˜π‘₯) / 2)) ∈ β„‚)
61 elfznn 13477 . . . . . . . . . . . 12 (𝑛 ∈ (1...(βŒŠβ€˜π‘₯)) β†’ 𝑛 ∈ β„•)
6261adantl 483 . . . . . . . . . . 11 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ 𝑛 ∈ β„•)
63 vmacl 26483 . . . . . . . . . . 11 (𝑛 ∈ β„• β†’ (Ξ›β€˜π‘›) ∈ ℝ)
6462, 63syl 17 . . . . . . . . . 10 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (Ξ›β€˜π‘›) ∈ ℝ)
6564, 62nndivred 12214 . . . . . . . . 9 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((Ξ›β€˜π‘›) / 𝑛) ∈ ℝ)
6618adantr 482 . . . . . . . . . . 11 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ π‘₯ ∈ ℝ+)
6762nnrpd 12962 . . . . . . . . . . 11 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ 𝑛 ∈ ℝ+)
6866, 67rpdivcld 12981 . . . . . . . . . 10 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (π‘₯ / 𝑛) ∈ ℝ+)
6968relogcld 25994 . . . . . . . . 9 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (logβ€˜(π‘₯ / 𝑛)) ∈ ℝ)
7065, 69remulcld 11192 . . . . . . . 8 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (((Ξ›β€˜π‘›) / 𝑛) Β· (logβ€˜(π‘₯ / 𝑛))) ∈ ℝ)
711, 70fsumrecl 15626 . . . . . . 7 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) / 𝑛) Β· (logβ€˜(π‘₯ / 𝑛))) ∈ ℝ)
7271recnd 11190 . . . . . 6 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) / 𝑛) Β· (logβ€˜(π‘₯ / 𝑛))) ∈ β„‚)
7324rpcnd 12966 . . . . . 6 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (logβ€˜π‘₯) ∈ β„‚)
7472, 73, 25divcld 11938 . . . . 5 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) / 𝑛) Β· (logβ€˜(π‘₯ / 𝑛))) / (logβ€˜π‘₯)) ∈ β„‚)
7573halfcld 12405 . . . . 5 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((logβ€˜π‘₯) / 2) ∈ β„‚)
7674, 75subcld 11519 . . . 4 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) / 𝑛) Β· (logβ€˜(π‘₯ / 𝑛))) / (logβ€˜π‘₯)) βˆ’ ((logβ€˜π‘₯) / 2)) ∈ β„‚)
7758, 74, 59nnncan2d 11554 . . . . . . 7 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))((logβ€˜π‘˜) / π‘˜) / (logβ€˜π‘₯)) βˆ’ ((logβ€˜π‘₯) / 2)) βˆ’ ((Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) / 𝑛) Β· (logβ€˜(π‘₯ / 𝑛))) / (logβ€˜π‘₯)) βˆ’ ((logβ€˜π‘₯) / 2))) = ((Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))((logβ€˜π‘˜) / π‘˜) / (logβ€˜π‘₯)) βˆ’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) / 𝑛) Β· (logβ€˜(π‘₯ / 𝑛))) / (logβ€˜π‘₯))))
788, 72, 23, 25divsubdird 11977 . . . . . . 7 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))((logβ€˜π‘˜) / π‘˜) βˆ’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) / 𝑛) Β· (logβ€˜(π‘₯ / 𝑛)))) / (logβ€˜π‘₯)) = ((Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))((logβ€˜π‘˜) / π‘˜) / (logβ€˜π‘₯)) βˆ’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) / 𝑛) Β· (logβ€˜(π‘₯ / 𝑛))) / (logβ€˜π‘₯))))
79 fzfid 13885 . . . . . . . . . . . 12 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (1...(βŒŠβ€˜(π‘₯ / 𝑛))) ∈ Fin)
8064adantr 482 . . . . . . . . . . . . 13 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))) β†’ (Ξ›β€˜π‘›) ∈ ℝ)
8162adantr 482 . . . . . . . . . . . . . 14 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))) β†’ 𝑛 ∈ β„•)
82 elfznn 13477 . . . . . . . . . . . . . . 15 (π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛))) β†’ π‘š ∈ β„•)
8382adantl 483 . . . . . . . . . . . . . 14 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))) β†’ π‘š ∈ β„•)
8481, 83nnmulcld 12213 . . . . . . . . . . . . 13 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))) β†’ (𝑛 Β· π‘š) ∈ β„•)
8580, 84nndivred 12214 . . . . . . . . . . . 12 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))) β†’ ((Ξ›β€˜π‘›) / (𝑛 Β· π‘š)) ∈ ℝ)
8679, 85fsumrecl 15626 . . . . . . . . . . 11 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))((Ξ›β€˜π‘›) / (𝑛 Β· π‘š)) ∈ ℝ)
8786recnd 11190 . . . . . . . . . 10 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))((Ξ›β€˜π‘›) / (𝑛 Β· π‘š)) ∈ β„‚)
8870recnd 11190 . . . . . . . . . 10 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (((Ξ›β€˜π‘›) / 𝑛) Β· (logβ€˜(π‘₯ / 𝑛))) ∈ β„‚)
891, 87, 88fsumsub 15680 . . . . . . . . 9 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))((Ξ›β€˜π‘›) / (𝑛 Β· π‘š)) βˆ’ (((Ξ›β€˜π‘›) / 𝑛) Β· (logβ€˜(π‘₯ / 𝑛)))) = (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))((Ξ›β€˜π‘›) / (𝑛 Β· π‘š)) βˆ’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) / 𝑛) Β· (logβ€˜(π‘₯ / 𝑛)))))
9064recnd 11190 . . . . . . . . . . . . 13 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (Ξ›β€˜π‘›) ∈ β„‚)
9162nncnd 12176 . . . . . . . . . . . . 13 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ 𝑛 ∈ β„‚)
9262nnne0d 12210 . . . . . . . . . . . . 13 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ 𝑛 β‰  0)
9390, 91, 92divcld 11938 . . . . . . . . . . . 12 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((Ξ›β€˜π‘›) / 𝑛) ∈ β„‚)
9483nnrecred 12211 . . . . . . . . . . . . . 14 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))) β†’ (1 / π‘š) ∈ ℝ)
9579, 94fsumrecl 15626 . . . . . . . . . . . . 13 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))(1 / π‘š) ∈ ℝ)
9695recnd 11190 . . . . . . . . . . . 12 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))(1 / π‘š) ∈ β„‚)
9769recnd 11190 . . . . . . . . . . . 12 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (logβ€˜(π‘₯ / 𝑛)) ∈ β„‚)
9893, 96, 97subdid 11618 . . . . . . . . . . 11 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (((Ξ›β€˜π‘›) / 𝑛) Β· (Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))(1 / π‘š) βˆ’ (logβ€˜(π‘₯ / 𝑛)))) = ((((Ξ›β€˜π‘›) / 𝑛) Β· Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))(1 / π‘š)) βˆ’ (((Ξ›β€˜π‘›) / 𝑛) Β· (logβ€˜(π‘₯ / 𝑛)))))
9990adantr 482 . . . . . . . . . . . . . . . 16 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))) β†’ (Ξ›β€˜π‘›) ∈ β„‚)
10091adantr 482 . . . . . . . . . . . . . . . 16 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))) β†’ 𝑛 ∈ β„‚)
10183nncnd 12176 . . . . . . . . . . . . . . . 16 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))) β†’ π‘š ∈ β„‚)
10292adantr 482 . . . . . . . . . . . . . . . 16 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))) β†’ 𝑛 β‰  0)
10383nnne0d 12210 . . . . . . . . . . . . . . . 16 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))) β†’ π‘š β‰  0)
10499, 100, 101, 102, 103divdiv1d 11969 . . . . . . . . . . . . . . 15 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))) β†’ (((Ξ›β€˜π‘›) / 𝑛) / π‘š) = ((Ξ›β€˜π‘›) / (𝑛 Β· π‘š)))
10599, 100, 102divcld 11938 . . . . . . . . . . . . . . . 16 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))) β†’ ((Ξ›β€˜π‘›) / 𝑛) ∈ β„‚)
106105, 101, 103divrecd 11941 . . . . . . . . . . . . . . 15 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))) β†’ (((Ξ›β€˜π‘›) / 𝑛) / π‘š) = (((Ξ›β€˜π‘›) / 𝑛) Β· (1 / π‘š)))
107104, 106eqtr3d 2779 . . . . . . . . . . . . . 14 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))) β†’ ((Ξ›β€˜π‘›) / (𝑛 Β· π‘š)) = (((Ξ›β€˜π‘›) / 𝑛) Β· (1 / π‘š)))
108107sumeq2dv 15595 . . . . . . . . . . . . 13 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))((Ξ›β€˜π‘›) / (𝑛 Β· π‘š)) = Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))(((Ξ›β€˜π‘›) / 𝑛) Β· (1 / π‘š)))
109101, 103reccld 11931 . . . . . . . . . . . . . 14 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) ∧ π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))) β†’ (1 / π‘š) ∈ β„‚)
11079, 93, 109fsummulc2 15676 . . . . . . . . . . . . 13 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (((Ξ›β€˜π‘›) / 𝑛) Β· Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))(1 / π‘š)) = Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))(((Ξ›β€˜π‘›) / 𝑛) Β· (1 / π‘š)))
111108, 110eqtr4d 2780 . . . . . . . . . . . 12 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))((Ξ›β€˜π‘›) / (𝑛 Β· π‘š)) = (((Ξ›β€˜π‘›) / 𝑛) Β· Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))(1 / π‘š)))
112111oveq1d 7377 . . . . . . . . . . 11 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))((Ξ›β€˜π‘›) / (𝑛 Β· π‘š)) βˆ’ (((Ξ›β€˜π‘›) / 𝑛) Β· (logβ€˜(π‘₯ / 𝑛)))) = ((((Ξ›β€˜π‘›) / 𝑛) Β· Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))(1 / π‘š)) βˆ’ (((Ξ›β€˜π‘›) / 𝑛) Β· (logβ€˜(π‘₯ / 𝑛)))))
11398, 112eqtr4d 2780 . . . . . . . . . 10 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (((Ξ›β€˜π‘›) / 𝑛) Β· (Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))(1 / π‘š) βˆ’ (logβ€˜(π‘₯ / 𝑛)))) = (Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))((Ξ›β€˜π‘›) / (𝑛 Β· π‘š)) βˆ’ (((Ξ›β€˜π‘›) / 𝑛) Β· (logβ€˜(π‘₯ / 𝑛)))))
114113sumeq2dv 15595 . . . . . . . . 9 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) / 𝑛) Β· (Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))(1 / π‘š) βˆ’ (logβ€˜(π‘₯ / 𝑛)))) = Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))((Ξ›β€˜π‘›) / (𝑛 Β· π‘š)) βˆ’ (((Ξ›β€˜π‘›) / 𝑛) Β· (logβ€˜(π‘₯ / 𝑛)))))
115 vmasum 26580 . . . . . . . . . . . . . . 15 (π‘˜ ∈ β„• β†’ Σ𝑛 ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ π‘˜} (Ξ›β€˜π‘›) = (logβ€˜π‘˜))
1163, 115syl 17 . . . . . . . . . . . . . 14 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))) β†’ Σ𝑛 ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ π‘˜} (Ξ›β€˜π‘›) = (logβ€˜π‘˜))
117116oveq1d 7377 . . . . . . . . . . . . 13 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (Σ𝑛 ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ π‘˜} (Ξ›β€˜π‘›) / π‘˜) = ((logβ€˜π‘˜) / π‘˜))
118 fzfid 13885 . . . . . . . . . . . . . . 15 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (1...π‘˜) ∈ Fin)
119 dvdsssfz1 16207 . . . . . . . . . . . . . . . 16 (π‘˜ ∈ β„• β†’ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ π‘˜} βŠ† (1...π‘˜))
1203, 119syl 17 . . . . . . . . . . . . . . 15 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))) β†’ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ π‘˜} βŠ† (1...π‘˜))
121118, 120ssfid 9218 . . . . . . . . . . . . . 14 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))) β†’ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ π‘˜} ∈ Fin)
1223nncnd 12176 . . . . . . . . . . . . . 14 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))) β†’ π‘˜ ∈ β„‚)
123 ssrab2 4042 . . . . . . . . . . . . . . . . . 18 {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ π‘˜} βŠ† β„•
124 simprr 772 . . . . . . . . . . . . . . . . . 18 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ (π‘˜ ∈ (1...(βŒŠβ€˜π‘₯)) ∧ 𝑛 ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ π‘˜})) β†’ 𝑛 ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ π‘˜})
125123, 124sselid 3947 . . . . . . . . . . . . . . . . 17 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ (π‘˜ ∈ (1...(βŒŠβ€˜π‘₯)) ∧ 𝑛 ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ π‘˜})) β†’ 𝑛 ∈ β„•)
126125, 63syl 17 . . . . . . . . . . . . . . . 16 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ (π‘˜ ∈ (1...(βŒŠβ€˜π‘₯)) ∧ 𝑛 ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ π‘˜})) β†’ (Ξ›β€˜π‘›) ∈ ℝ)
127126recnd 11190 . . . . . . . . . . . . . . 15 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ (π‘˜ ∈ (1...(βŒŠβ€˜π‘₯)) ∧ 𝑛 ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ π‘˜})) β†’ (Ξ›β€˜π‘›) ∈ β„‚)
128127anassrs 469 . . . . . . . . . . . . . 14 ((((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))) ∧ 𝑛 ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ π‘˜}) β†’ (Ξ›β€˜π‘›) ∈ β„‚)
1293nnne0d 12210 . . . . . . . . . . . . . 14 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))) β†’ π‘˜ β‰  0)
130121, 122, 128, 129fsumdivc 15678 . . . . . . . . . . . . 13 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (Σ𝑛 ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ π‘˜} (Ξ›β€˜π‘›) / π‘˜) = Σ𝑛 ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ π‘˜} ((Ξ›β€˜π‘›) / π‘˜))
131117, 130eqtr3d 2779 . . . . . . . . . . . 12 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((logβ€˜π‘˜) / π‘˜) = Σ𝑛 ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ π‘˜} ((Ξ›β€˜π‘›) / π‘˜))
132131sumeq2dv 15595 . . . . . . . . . . 11 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))((logβ€˜π‘˜) / π‘˜) = Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))Σ𝑛 ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ π‘˜} ((Ξ›β€˜π‘›) / π‘˜))
133 oveq2 7370 . . . . . . . . . . . 12 (π‘˜ = (𝑛 Β· π‘š) β†’ ((Ξ›β€˜π‘›) / π‘˜) = ((Ξ›β€˜π‘›) / (𝑛 Β· π‘š)))
1342ad2antrl 727 . . . . . . . . . . . . . 14 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ (π‘˜ ∈ (1...(βŒŠβ€˜π‘₯)) ∧ 𝑛 ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ π‘˜})) β†’ π‘˜ ∈ β„•)
135134nncnd 12176 . . . . . . . . . . . . 13 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ (π‘˜ ∈ (1...(βŒŠβ€˜π‘₯)) ∧ 𝑛 ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ π‘˜})) β†’ π‘˜ ∈ β„‚)
136134nnne0d 12210 . . . . . . . . . . . . 13 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ (π‘˜ ∈ (1...(βŒŠβ€˜π‘₯)) ∧ 𝑛 ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ π‘˜})) β†’ π‘˜ β‰  0)
137127, 135, 136divcld 11938 . . . . . . . . . . . 12 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ (π‘˜ ∈ (1...(βŒŠβ€˜π‘₯)) ∧ 𝑛 ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ π‘˜})) β†’ ((Ξ›β€˜π‘›) / π‘˜) ∈ β„‚)
138133, 10, 137dvdsflsumcom 26553 . . . . . . . . . . 11 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))Σ𝑛 ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ π‘˜} ((Ξ›β€˜π‘›) / π‘˜) = Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))((Ξ›β€˜π‘›) / (𝑛 Β· π‘š)))
139132, 138eqtrd 2777 . . . . . . . . . 10 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))((logβ€˜π‘˜) / π‘˜) = Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))((Ξ›β€˜π‘›) / (𝑛 Β· π‘š)))
140139oveq1d 7377 . . . . . . . . 9 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))((logβ€˜π‘˜) / π‘˜) βˆ’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) / 𝑛) Β· (logβ€˜(π‘₯ / 𝑛)))) = (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))((Ξ›β€˜π‘›) / (𝑛 Β· π‘š)) βˆ’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) / 𝑛) Β· (logβ€˜(π‘₯ / 𝑛)))))
14189, 114, 1403eqtr4rd 2788 . . . . . . . 8 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))((logβ€˜π‘˜) / π‘˜) βˆ’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) / 𝑛) Β· (logβ€˜(π‘₯ / 𝑛)))) = Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) / 𝑛) Β· (Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))(1 / π‘š) βˆ’ (logβ€˜(π‘₯ / 𝑛)))))
142141oveq1d 7377 . . . . . . 7 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))((logβ€˜π‘˜) / π‘˜) βˆ’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) / 𝑛) Β· (logβ€˜(π‘₯ / 𝑛)))) / (logβ€˜π‘₯)) = (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) / 𝑛) Β· (Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))(1 / π‘š) βˆ’ (logβ€˜(π‘₯ / 𝑛)))) / (logβ€˜π‘₯)))
14377, 78, 1423eqtr2d 2783 . . . . . 6 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))((logβ€˜π‘˜) / π‘˜) / (logβ€˜π‘₯)) βˆ’ ((logβ€˜π‘₯) / 2)) βˆ’ ((Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) / 𝑛) Β· (logβ€˜(π‘₯ / 𝑛))) / (logβ€˜π‘₯)) βˆ’ ((logβ€˜π‘₯) / 2))) = (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) / 𝑛) Β· (Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))(1 / π‘š) βˆ’ (logβ€˜(π‘₯ / 𝑛)))) / (logβ€˜π‘₯)))
144143mpteq2dva 5210 . . . . 5 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ (((Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))((logβ€˜π‘˜) / π‘˜) / (logβ€˜π‘₯)) βˆ’ ((logβ€˜π‘₯) / 2)) βˆ’ ((Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) / 𝑛) Β· (logβ€˜(π‘₯ / 𝑛))) / (logβ€˜π‘₯)) βˆ’ ((logβ€˜π‘₯) / 2)))) = (π‘₯ ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) / 𝑛) Β· (Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))(1 / π‘š) βˆ’ (logβ€˜(π‘₯ / 𝑛)))) / (logβ€˜π‘₯))))
145 1red 11163 . . . . . . 7 (⊀ β†’ 1 ∈ ℝ)
1461, 65fsumrecl 15626 . . . . . . . . 9 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘›) / 𝑛) ∈ ℝ)
147146, 24rerpdivcld 12995 . . . . . . . 8 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘›) / 𝑛) / (logβ€˜π‘₯)) ∈ ℝ)
148 ioossre 13332 . . . . . . . . . . 11 (1(,)+∞) βŠ† ℝ
149 ax-1cn 11116 . . . . . . . . . . 11 1 ∈ β„‚
150 o1const 15509 . . . . . . . . . . 11 (((1(,)+∞) βŠ† ℝ ∧ 1 ∈ β„‚) β†’ (π‘₯ ∈ (1(,)+∞) ↦ 1) ∈ 𝑂(1))
151148, 149, 150mp2an 691 . . . . . . . . . 10 (π‘₯ ∈ (1(,)+∞) ↦ 1) ∈ 𝑂(1)
152151a1i 11 . . . . . . . . 9 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ 1) ∈ 𝑂(1))
153147recnd 11190 . . . . . . . . . 10 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘›) / 𝑛) / (logβ€˜π‘₯)) ∈ β„‚)
15412rpcnd 12966 . . . . . . . . . 10 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 1 ∈ β„‚)
155146recnd 11190 . . . . . . . . . . . . . 14 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘›) / 𝑛) ∈ β„‚)
156155, 23, 23, 25divsubdird 11977 . . . . . . . . . . . . 13 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘›) / 𝑛) βˆ’ (logβ€˜π‘₯)) / (logβ€˜π‘₯)) = ((Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘›) / 𝑛) / (logβ€˜π‘₯)) βˆ’ ((logβ€˜π‘₯) / (logβ€˜π‘₯))))
157155, 23subcld 11519 . . . . . . . . . . . . . 14 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘›) / 𝑛) βˆ’ (logβ€˜π‘₯)) ∈ β„‚)
158157, 23, 25divrecd 11941 . . . . . . . . . . . . 13 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘›) / 𝑛) βˆ’ (logβ€˜π‘₯)) / (logβ€˜π‘₯)) = ((Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘›) / 𝑛) βˆ’ (logβ€˜π‘₯)) Β· (1 / (logβ€˜π‘₯))))
15923, 25dividd 11936 . . . . . . . . . . . . . 14 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((logβ€˜π‘₯) / (logβ€˜π‘₯)) = 1)
160159oveq2d 7378 . . . . . . . . . . . . 13 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘›) / 𝑛) / (logβ€˜π‘₯)) βˆ’ ((logβ€˜π‘₯) / (logβ€˜π‘₯))) = ((Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘›) / 𝑛) / (logβ€˜π‘₯)) βˆ’ 1))
161156, 158, 1603eqtr3rd 2786 . . . . . . . . . . . 12 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘›) / 𝑛) / (logβ€˜π‘₯)) βˆ’ 1) = ((Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘›) / 𝑛) βˆ’ (logβ€˜π‘₯)) Β· (1 / (logβ€˜π‘₯))))
162161mpteq2dva 5210 . . . . . . . . . . 11 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘›) / 𝑛) / (logβ€˜π‘₯)) βˆ’ 1)) = (π‘₯ ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘›) / 𝑛) βˆ’ (logβ€˜π‘₯)) Β· (1 / (logβ€˜π‘₯)))))
163146, 19resubcld 11590 . . . . . . . . . . . 12 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘›) / 𝑛) βˆ’ (logβ€˜π‘₯)) ∈ ℝ)
164 vmadivsum 26846 . . . . . . . . . . . . . 14 (π‘₯ ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘›) / 𝑛) βˆ’ (logβ€˜π‘₯))) ∈ 𝑂(1)
165164a1i 11 . . . . . . . . . . . . 13 (⊀ β†’ (π‘₯ ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘›) / 𝑛) βˆ’ (logβ€˜π‘₯))) ∈ 𝑂(1))
16646, 165o1res2 15452 . . . . . . . . . . . 12 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘›) / 𝑛) βˆ’ (logβ€˜π‘₯))) ∈ 𝑂(1))
167163, 44, 166, 55o1mul2 15514 . . . . . . . . . . 11 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘›) / 𝑛) βˆ’ (logβ€˜π‘₯)) Β· (1 / (logβ€˜π‘₯)))) ∈ 𝑂(1))
168162, 167eqeltrd 2838 . . . . . . . . . 10 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘›) / 𝑛) / (logβ€˜π‘₯)) βˆ’ 1)) ∈ 𝑂(1))
169153, 154, 168o1dif 15519 . . . . . . . . 9 (⊀ β†’ ((π‘₯ ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘›) / 𝑛) / (logβ€˜π‘₯))) ∈ 𝑂(1) ↔ (π‘₯ ∈ (1(,)+∞) ↦ 1) ∈ 𝑂(1)))
170152, 169mpbird 257 . . . . . . . 8 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘›) / 𝑛) / (logβ€˜π‘₯))) ∈ 𝑂(1))
171147, 170o1lo1d 15428 . . . . . . 7 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘›) / 𝑛) / (logβ€˜π‘₯))) ∈ ≀𝑂(1))
17295, 69resubcld 11590 . . . . . . . . . 10 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))(1 / π‘š) βˆ’ (logβ€˜(π‘₯ / 𝑛))) ∈ ℝ)
17365, 172remulcld 11192 . . . . . . . . 9 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (((Ξ›β€˜π‘›) / 𝑛) Β· (Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))(1 / π‘š) βˆ’ (logβ€˜(π‘₯ / 𝑛)))) ∈ ℝ)
1741, 173fsumrecl 15626 . . . . . . . 8 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) / 𝑛) Β· (Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))(1 / π‘š) βˆ’ (logβ€˜(π‘₯ / 𝑛)))) ∈ ℝ)
175174, 24rerpdivcld 12995 . . . . . . 7 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) / 𝑛) Β· (Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))(1 / π‘š) βˆ’ (logβ€˜(π‘₯ / 𝑛)))) / (logβ€˜π‘₯)) ∈ ℝ)
176 1red 11163 . . . . . . . . . . . 12 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ 1 ∈ ℝ)
177 vmage0 26486 . . . . . . . . . . . . . 14 (𝑛 ∈ β„• β†’ 0 ≀ (Ξ›β€˜π‘›))
17862, 177syl 17 . . . . . . . . . . . . 13 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ 0 ≀ (Ξ›β€˜π‘›))
17964, 67, 178divge0d 13004 . . . . . . . . . . . 12 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ 0 ≀ ((Ξ›β€˜π‘›) / 𝑛))
18068rpred 12964 . . . . . . . . . . . . . 14 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (π‘₯ / 𝑛) ∈ ℝ)
18191mulid2d 11180 . . . . . . . . . . . . . . . 16 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (1 Β· 𝑛) = 𝑛)
182 fznnfl 13774 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ ℝ β†’ (𝑛 ∈ (1...(βŒŠβ€˜π‘₯)) ↔ (𝑛 ∈ β„• ∧ 𝑛 ≀ π‘₯)))
18310, 182syl 17 . . . . . . . . . . . . . . . . 17 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (𝑛 ∈ (1...(βŒŠβ€˜π‘₯)) ↔ (𝑛 ∈ β„• ∧ 𝑛 ≀ π‘₯)))
184183simplbda 501 . . . . . . . . . . . . . . . 16 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ 𝑛 ≀ π‘₯)
185181, 184eqbrtrd 5132 . . . . . . . . . . . . . . 15 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (1 Β· 𝑛) ≀ π‘₯)
18610adantr 482 . . . . . . . . . . . . . . . 16 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ π‘₯ ∈ ℝ)
187176, 186, 67lemuldivd 13013 . . . . . . . . . . . . . . 15 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((1 Β· 𝑛) ≀ π‘₯ ↔ 1 ≀ (π‘₯ / 𝑛)))
188185, 187mpbid 231 . . . . . . . . . . . . . 14 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ 1 ≀ (π‘₯ / 𝑛))
189 harmonicubnd 26375 . . . . . . . . . . . . . 14 (((π‘₯ / 𝑛) ∈ ℝ ∧ 1 ≀ (π‘₯ / 𝑛)) β†’ Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))(1 / π‘š) ≀ ((logβ€˜(π‘₯ / 𝑛)) + 1))
190180, 188, 189syl2anc 585 . . . . . . . . . . . . 13 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))(1 / π‘š) ≀ ((logβ€˜(π‘₯ / 𝑛)) + 1))
19195, 69, 176lesubadd2d 11761 . . . . . . . . . . . . 13 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))(1 / π‘š) βˆ’ (logβ€˜(π‘₯ / 𝑛))) ≀ 1 ↔ Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))(1 / π‘š) ≀ ((logβ€˜(π‘₯ / 𝑛)) + 1)))
192190, 191mpbird 257 . . . . . . . . . . . 12 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))(1 / π‘š) βˆ’ (logβ€˜(π‘₯ / 𝑛))) ≀ 1)
193172, 176, 65, 179, 192lemul2ad 12102 . . . . . . . . . . 11 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (((Ξ›β€˜π‘›) / 𝑛) Β· (Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))(1 / π‘š) βˆ’ (logβ€˜(π‘₯ / 𝑛)))) ≀ (((Ξ›β€˜π‘›) / 𝑛) Β· 1))
19493mulid1d 11179 . . . . . . . . . . 11 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (((Ξ›β€˜π‘›) / 𝑛) Β· 1) = ((Ξ›β€˜π‘›) / 𝑛))
195193, 194breqtrd 5136 . . . . . . . . . 10 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (((Ξ›β€˜π‘›) / 𝑛) Β· (Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))(1 / π‘š) βˆ’ (logβ€˜(π‘₯ / 𝑛)))) ≀ ((Ξ›β€˜π‘›) / 𝑛))
1961, 173, 65, 195fsumle 15691 . . . . . . . . 9 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) / 𝑛) Β· (Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))(1 / π‘š) βˆ’ (logβ€˜(π‘₯ / 𝑛)))) ≀ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘›) / 𝑛))
197174, 146, 24, 196lediv1dd 13022 . . . . . . . 8 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) / 𝑛) Β· (Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))(1 / π‘š) βˆ’ (logβ€˜(π‘₯ / 𝑛)))) / (logβ€˜π‘₯)) ≀ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘›) / 𝑛) / (logβ€˜π‘₯)))
198197adantrr 716 . . . . . . 7 ((⊀ ∧ (π‘₯ ∈ (1(,)+∞) ∧ 1 ≀ π‘₯)) β†’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) / 𝑛) Β· (Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))(1 / π‘š) βˆ’ (logβ€˜(π‘₯ / 𝑛)))) / (logβ€˜π‘₯)) ≀ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((Ξ›β€˜π‘›) / 𝑛) / (logβ€˜π‘₯)))
199145, 171, 147, 175, 198lo1le 15543 . . . . . 6 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) / 𝑛) Β· (Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))(1 / π‘š) βˆ’ (logβ€˜(π‘₯ / 𝑛)))) / (logβ€˜π‘₯))) ∈ ≀𝑂(1))
200 0red 11165 . . . . . . 7 (⊀ β†’ 0 ∈ ℝ)
201 harmoniclbnd 26374 . . . . . . . . . . . 12 ((π‘₯ / 𝑛) ∈ ℝ+ β†’ (logβ€˜(π‘₯ / 𝑛)) ≀ Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))(1 / π‘š))
20268, 201syl 17 . . . . . . . . . . 11 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (logβ€˜(π‘₯ / 𝑛)) ≀ Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))(1 / π‘š))
20395, 69subge0d 11752 . . . . . . . . . . 11 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (0 ≀ (Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))(1 / π‘š) βˆ’ (logβ€˜(π‘₯ / 𝑛))) ↔ (logβ€˜(π‘₯ / 𝑛)) ≀ Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))(1 / π‘š)))
204202, 203mpbird 257 . . . . . . . . . 10 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ 0 ≀ (Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))(1 / π‘š) βˆ’ (logβ€˜(π‘₯ / 𝑛))))
20565, 172, 179, 204mulge0d 11739 . . . . . . . . 9 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ 0 ≀ (((Ξ›β€˜π‘›) / 𝑛) Β· (Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))(1 / π‘š) βˆ’ (logβ€˜(π‘₯ / 𝑛)))))
2061, 173, 205fsumge0 15687 . . . . . . . 8 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 0 ≀ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) / 𝑛) Β· (Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))(1 / π‘š) βˆ’ (logβ€˜(π‘₯ / 𝑛)))))
207174, 24, 206divge0d 13004 . . . . . . 7 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 0 ≀ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) / 𝑛) Β· (Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))(1 / π‘š) βˆ’ (logβ€˜(π‘₯ / 𝑛)))) / (logβ€˜π‘₯)))
208175, 200, 207o1lo12 15427 . . . . . 6 (⊀ β†’ ((π‘₯ ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) / 𝑛) Β· (Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))(1 / π‘š) βˆ’ (logβ€˜(π‘₯ / 𝑛)))) / (logβ€˜π‘₯))) ∈ 𝑂(1) ↔ (π‘₯ ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) / 𝑛) Β· (Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))(1 / π‘š) βˆ’ (logβ€˜(π‘₯ / 𝑛)))) / (logβ€˜π‘₯))) ∈ ≀𝑂(1)))
209199, 208mpbird 257 . . . . 5 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) / 𝑛) Β· (Ξ£π‘š ∈ (1...(βŒŠβ€˜(π‘₯ / 𝑛)))(1 / π‘š) βˆ’ (logβ€˜(π‘₯ / 𝑛)))) / (logβ€˜π‘₯))) ∈ 𝑂(1))
210144, 209eqeltrd 2838 . . . 4 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ (((Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))((logβ€˜π‘˜) / π‘˜) / (logβ€˜π‘₯)) βˆ’ ((logβ€˜π‘₯) / 2)) βˆ’ ((Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) / 𝑛) Β· (logβ€˜(π‘₯ / 𝑛))) / (logβ€˜π‘₯)) βˆ’ ((logβ€˜π‘₯) / 2)))) ∈ 𝑂(1))
21160, 76, 210o1dif 15519 . . 3 (⊀ β†’ ((π‘₯ ∈ (1(,)+∞) ↦ ((Ξ£π‘˜ ∈ (1...(βŒŠβ€˜π‘₯))((logβ€˜π‘˜) / π‘˜) / (logβ€˜π‘₯)) βˆ’ ((logβ€˜π‘₯) / 2))) ∈ 𝑂(1) ↔ (π‘₯ ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) / 𝑛) Β· (logβ€˜(π‘₯ / 𝑛))) / (logβ€˜π‘₯)) βˆ’ ((logβ€˜π‘₯) / 2))) ∈ 𝑂(1)))
21257, 211mpbid 231 . 2 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) / 𝑛) Β· (logβ€˜(π‘₯ / 𝑛))) / (logβ€˜π‘₯)) βˆ’ ((logβ€˜π‘₯) / 2))) ∈ 𝑂(1))
213212mptru 1549 1 (π‘₯ ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) / 𝑛) Β· (logβ€˜(π‘₯ / 𝑛))) / (logβ€˜π‘₯)) βˆ’ ((logβ€˜π‘₯) / 2))) ∈ 𝑂(1)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542  βŠ€wtru 1543   ∈ wcel 2107   β‰  wne 2944  {crab 3410   βŠ† wss 3915   class class class wbr 5110   ↦ cmpt 5193  dom cdm 5638  βŸΆwf 6497  β€˜cfv 6501  (class class class)co 7362  β„‚cc 11056  β„cr 11057  0cc0 11058  1c1 11059   + caddc 11061   Β· cmul 11063  +∞cpnf 11193   < clt 11196   ≀ cle 11197   βˆ’ cmin 11392   / cdiv 11819  β„•cn 12160  2c2 12215  β„+crp 12922  (,)cioo 13271  ...cfz 13431  βŒŠcfl 13702  β†‘cexp 13974  abscabs 15126   β‡π‘Ÿ crli 15374  π‘‚(1)co1 15375  β‰€π‘‚(1)clo1 15376  Ξ£csu 15577  eceu 15952   βˆ₯ cdvds 16143  logclog 25926  Ξ›cvma 26457
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-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
This theorem is referenced by:  vmalogdivsum  26903  2vmadivsumlem  26904  selberg4lem1  26924
  Copyright terms: Public domain W3C validator