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

Theorem pntrlog2bndlem4 26944
Description: Lemma for pntrlog2bnd 26948. Bound on the difference between the Selberg function and its approximation, inside a sum. (Contributed by Mario Carneiro, 31-May-2016.)
Hypotheses
Ref Expression
pntsval.1 𝑆 = (π‘Ž ∈ ℝ ↦ Σ𝑖 ∈ (1...(βŒŠβ€˜π‘Ž))((Ξ›β€˜π‘–) Β· ((logβ€˜π‘–) + (Οˆβ€˜(π‘Ž / 𝑖)))))
pntrlog2bnd.r 𝑅 = (π‘Ž ∈ ℝ+ ↦ ((Οˆβ€˜π‘Ž) βˆ’ π‘Ž))
pntrlog2bnd.t 𝑇 = (π‘Ž ∈ ℝ ↦ if(π‘Ž ∈ ℝ+, (π‘Ž Β· (logβ€˜π‘Ž)), 0))
Assertion
Ref Expression
pntrlog2bndlem4 (π‘₯ ∈ (1(,)+∞) ↦ ((((absβ€˜(π‘…β€˜π‘₯)) Β· (logβ€˜π‘₯)) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))) / π‘₯)) ∈ ≀𝑂(1)
Distinct variable groups:   𝑖,π‘Ž,𝑛,π‘₯   𝑆,𝑛,π‘₯   𝑅,𝑛,π‘₯   𝑇,𝑛
Allowed substitution hints:   𝑅(𝑖,π‘Ž)   𝑆(𝑖,π‘Ž)   𝑇(π‘₯,𝑖,π‘Ž)

Proof of Theorem pntrlog2bndlem4
Dummy variables 𝑐 π‘š 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elioore 13300 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ ∈ (1(,)+∞) β†’ π‘₯ ∈ ℝ)
21adantl 483 . . . . . . . . . . . . . . . . . . 19 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ π‘₯ ∈ ℝ)
3 1rp 12924 . . . . . . . . . . . . . . . . . . . 20 1 ∈ ℝ+
43a1i 11 . . . . . . . . . . . . . . . . . . 19 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 1 ∈ ℝ+)
5 1red 11161 . . . . . . . . . . . . . . . . . . . 20 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 1 ∈ ℝ)
6 eliooord 13329 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ ∈ (1(,)+∞) β†’ (1 < π‘₯ ∧ π‘₯ < +∞))
76adantl 483 . . . . . . . . . . . . . . . . . . . . 21 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (1 < π‘₯ ∧ π‘₯ < +∞))
87simpld 496 . . . . . . . . . . . . . . . . . . . 20 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 1 < π‘₯)
95, 2, 8ltled 11308 . . . . . . . . . . . . . . . . . . 19 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 1 ≀ π‘₯)
102, 4, 9rpgecld 13001 . . . . . . . . . . . . . . . . . 18 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ π‘₯ ∈ ℝ+)
1110rprege0d 12969 . . . . . . . . . . . . . . . . . . . . 21 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘₯ ∈ ℝ ∧ 0 ≀ π‘₯))
12 flge0nn0 13731 . . . . . . . . . . . . . . . . . . . . 21 ((π‘₯ ∈ ℝ ∧ 0 ≀ π‘₯) β†’ (βŒŠβ€˜π‘₯) ∈ β„•0)
1311, 12syl 17 . . . . . . . . . . . . . . . . . . . 20 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (βŒŠβ€˜π‘₯) ∈ β„•0)
14 nn0p1nn 12457 . . . . . . . . . . . . . . . . . . . 20 ((βŒŠβ€˜π‘₯) ∈ β„•0 β†’ ((βŒŠβ€˜π‘₯) + 1) ∈ β„•)
1513, 14syl 17 . . . . . . . . . . . . . . . . . . 19 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((βŒŠβ€˜π‘₯) + 1) ∈ β„•)
1615nnrpd 12960 . . . . . . . . . . . . . . . . . 18 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((βŒŠβ€˜π‘₯) + 1) ∈ ℝ+)
1710, 16rpdivcld 12979 . . . . . . . . . . . . . . . . 17 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) ∈ ℝ+)
18 pntrlog2bnd.r . . . . . . . . . . . . . . . . . 18 𝑅 = (π‘Ž ∈ ℝ+ ↦ ((Οˆβ€˜π‘Ž) βˆ’ π‘Ž))
1918pntrval 26926 . . . . . . . . . . . . . . . . 17 ((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) ∈ ℝ+ β†’ (π‘…β€˜(π‘₯ / ((βŒŠβ€˜π‘₯) + 1))) = ((Οˆβ€˜(π‘₯ / ((βŒŠβ€˜π‘₯) + 1))) βˆ’ (π‘₯ / ((βŒŠβ€˜π‘₯) + 1))))
2017, 19syl 17 . . . . . . . . . . . . . . . 16 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘…β€˜(π‘₯ / ((βŒŠβ€˜π‘₯) + 1))) = ((Οˆβ€˜(π‘₯ / ((βŒŠβ€˜π‘₯) + 1))) βˆ’ (π‘₯ / ((βŒŠβ€˜π‘₯) + 1))))
212, 15nndivred 12212 . . . . . . . . . . . . . . . . . . 19 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) ∈ ℝ)
22 2re 12232 . . . . . . . . . . . . . . . . . . . 20 2 ∈ ℝ
2322a1i 11 . . . . . . . . . . . . . . . . . . 19 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 2 ∈ ℝ)
24 flltp1 13711 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ ∈ ℝ β†’ π‘₯ < ((βŒŠβ€˜π‘₯) + 1))
252, 24syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ π‘₯ < ((βŒŠβ€˜π‘₯) + 1))
2615nncnd 12174 . . . . . . . . . . . . . . . . . . . . . 22 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((βŒŠβ€˜π‘₯) + 1) ∈ β„‚)
2726mulid1d 11177 . . . . . . . . . . . . . . . . . . . . 21 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((βŒŠβ€˜π‘₯) + 1) Β· 1) = ((βŒŠβ€˜π‘₯) + 1))
2825, 27breqtrrd 5134 . . . . . . . . . . . . . . . . . . . 20 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ π‘₯ < (((βŒŠβ€˜π‘₯) + 1) Β· 1))
292, 5, 16ltdivmuld 13013 . . . . . . . . . . . . . . . . . . . 20 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) < 1 ↔ π‘₯ < (((βŒŠβ€˜π‘₯) + 1) Β· 1)))
3028, 29mpbird 257 . . . . . . . . . . . . . . . . . . 19 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) < 1)
31 1lt2 12329 . . . . . . . . . . . . . . . . . . . 20 1 < 2
3231a1i 11 . . . . . . . . . . . . . . . . . . 19 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 1 < 2)
3321, 5, 23, 30, 32lttrd 11321 . . . . . . . . . . . . . . . . . 18 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) < 2)
34 chpeq0 26572 . . . . . . . . . . . . . . . . . . 19 ((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) ∈ ℝ β†’ ((Οˆβ€˜(π‘₯ / ((βŒŠβ€˜π‘₯) + 1))) = 0 ↔ (π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) < 2))
3521, 34syl 17 . . . . . . . . . . . . . . . . . 18 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((Οˆβ€˜(π‘₯ / ((βŒŠβ€˜π‘₯) + 1))) = 0 ↔ (π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) < 2))
3633, 35mpbird 257 . . . . . . . . . . . . . . . . 17 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (Οˆβ€˜(π‘₯ / ((βŒŠβ€˜π‘₯) + 1))) = 0)
3736oveq1d 7373 . . . . . . . . . . . . . . . 16 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((Οˆβ€˜(π‘₯ / ((βŒŠβ€˜π‘₯) + 1))) βˆ’ (π‘₯ / ((βŒŠβ€˜π‘₯) + 1))) = (0 βˆ’ (π‘₯ / ((βŒŠβ€˜π‘₯) + 1))))
3820, 37eqtrd 2773 . . . . . . . . . . . . . . 15 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘…β€˜(π‘₯ / ((βŒŠβ€˜π‘₯) + 1))) = (0 βˆ’ (π‘₯ / ((βŒŠβ€˜π‘₯) + 1))))
3938fveq2d 6847 . . . . . . . . . . . . . 14 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (absβ€˜(π‘…β€˜(π‘₯ / ((βŒŠβ€˜π‘₯) + 1)))) = (absβ€˜(0 βˆ’ (π‘₯ / ((βŒŠβ€˜π‘₯) + 1)))))
40 0red 11163 . . . . . . . . . . . . . . 15 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 0 ∈ ℝ)
4117rpge0d 12966 . . . . . . . . . . . . . . 15 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 0 ≀ (π‘₯ / ((βŒŠβ€˜π‘₯) + 1)))
4240, 21, 41abssuble0d 15323 . . . . . . . . . . . . . 14 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (absβ€˜(0 βˆ’ (π‘₯ / ((βŒŠβ€˜π‘₯) + 1)))) = ((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) βˆ’ 0))
4321recnd 11188 . . . . . . . . . . . . . . 15 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) ∈ β„‚)
4443subid1d 11506 . . . . . . . . . . . . . 14 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) βˆ’ 0) = (π‘₯ / ((βŒŠβ€˜π‘₯) + 1)))
4539, 42, 443eqtrd 2777 . . . . . . . . . . . . 13 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (absβ€˜(π‘…β€˜(π‘₯ / ((βŒŠβ€˜π‘₯) + 1)))) = (π‘₯ / ((βŒŠβ€˜π‘₯) + 1)))
4613nn0red 12479 . . . . . . . . . . . . . . . 16 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (βŒŠβ€˜π‘₯) ∈ ℝ)
47 pntsval.1 . . . . . . . . . . . . . . . . 17 𝑆 = (π‘Ž ∈ ℝ ↦ Σ𝑖 ∈ (1...(βŒŠβ€˜π‘Ž))((Ξ›β€˜π‘–) Β· ((logβ€˜π‘–) + (Οˆβ€˜(π‘Ž / 𝑖)))))
4847pntsval2 26940 . . . . . . . . . . . . . . . 16 ((βŒŠβ€˜π‘₯) ∈ ℝ β†’ (π‘†β€˜(βŒŠβ€˜π‘₯)) = Σ𝑛 ∈ (1...(βŒŠβ€˜(βŒŠβ€˜π‘₯)))(((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)) + Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š)))))
4946, 48syl 17 . . . . . . . . . . . . . . 15 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘†β€˜(βŒŠβ€˜π‘₯)) = Σ𝑛 ∈ (1...(βŒŠβ€˜(βŒŠβ€˜π‘₯)))(((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)) + Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š)))))
5013nn0cnd 12480 . . . . . . . . . . . . . . . . 17 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (βŒŠβ€˜π‘₯) ∈ β„‚)
51 1cnd 11155 . . . . . . . . . . . . . . . . 17 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 1 ∈ β„‚)
5250, 51pncand 11518 . . . . . . . . . . . . . . . 16 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((βŒŠβ€˜π‘₯) + 1) βˆ’ 1) = (βŒŠβ€˜π‘₯))
5352fveq2d 6847 . . . . . . . . . . . . . . 15 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘†β€˜(((βŒŠβ€˜π‘₯) + 1) βˆ’ 1)) = (π‘†β€˜(βŒŠβ€˜π‘₯)))
5447pntsval2 26940 . . . . . . . . . . . . . . . . 17 (π‘₯ ∈ ℝ β†’ (π‘†β€˜π‘₯) = Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)) + Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š)))))
552, 54syl 17 . . . . . . . . . . . . . . . 16 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘†β€˜π‘₯) = Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)) + Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š)))))
56 flidm 13720 . . . . . . . . . . . . . . . . . . 19 (π‘₯ ∈ ℝ β†’ (βŒŠβ€˜(βŒŠβ€˜π‘₯)) = (βŒŠβ€˜π‘₯))
572, 56syl 17 . . . . . . . . . . . . . . . . . 18 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (βŒŠβ€˜(βŒŠβ€˜π‘₯)) = (βŒŠβ€˜π‘₯))
5857oveq2d 7374 . . . . . . . . . . . . . . . . 17 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (1...(βŒŠβ€˜(βŒŠβ€˜π‘₯))) = (1...(βŒŠβ€˜π‘₯)))
5958sumeq1d 15591 . . . . . . . . . . . . . . . 16 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜(βŒŠβ€˜π‘₯)))(((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)) + Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š)))) = Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)) + Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š)))))
6055, 59eqtr4d 2776 . . . . . . . . . . . . . . 15 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘†β€˜π‘₯) = Σ𝑛 ∈ (1...(βŒŠβ€˜(βŒŠβ€˜π‘₯)))(((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)) + Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š)))))
6149, 53, 603eqtr4d 2783 . . . . . . . . . . . . . 14 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘†β€˜(((βŒŠβ€˜π‘₯) + 1) βˆ’ 1)) = (π‘†β€˜π‘₯))
6252fveq2d 6847 . . . . . . . . . . . . . . 15 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘‡β€˜(((βŒŠβ€˜π‘₯) + 1) βˆ’ 1)) = (π‘‡β€˜(βŒŠβ€˜π‘₯)))
6362oveq2d 7374 . . . . . . . . . . . . . 14 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (2 Β· (π‘‡β€˜(((βŒŠβ€˜π‘₯) + 1) βˆ’ 1))) = (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))
6461, 63oveq12d 7376 . . . . . . . . . . . . 13 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((π‘†β€˜(((βŒŠβ€˜π‘₯) + 1) βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(((βŒŠβ€˜π‘₯) + 1) βˆ’ 1)))) = ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯)))))
6545, 64oveq12d 7376 . . . . . . . . . . . 12 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((absβ€˜(π‘…β€˜(π‘₯ / ((βŒŠβ€˜π‘₯) + 1)))) Β· ((π‘†β€˜(((βŒŠβ€˜π‘₯) + 1) βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(((βŒŠβ€˜π‘₯) + 1) βˆ’ 1))))) = ((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))))
662recnd 11188 . . . . . . . . . . . . . . . . . . 19 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ π‘₯ ∈ β„‚)
6766div1d 11928 . . . . . . . . . . . . . . . . . 18 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘₯ / 1) = π‘₯)
6867fveq2d 6847 . . . . . . . . . . . . . . . . 17 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘…β€˜(π‘₯ / 1)) = (π‘…β€˜π‘₯))
6918pntrf 26927 . . . . . . . . . . . . . . . . . . 19 𝑅:ℝ+βŸΆβ„
7069ffvelcdmi 7035 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ ℝ+ β†’ (π‘…β€˜π‘₯) ∈ ℝ)
7110, 70syl 17 . . . . . . . . . . . . . . . . 17 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘…β€˜π‘₯) ∈ ℝ)
7268, 71eqeltrd 2834 . . . . . . . . . . . . . . . 16 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘…β€˜(π‘₯ / 1)) ∈ ℝ)
7372recnd 11188 . . . . . . . . . . . . . . 15 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘…β€˜(π‘₯ / 1)) ∈ β„‚)
7473abscld 15327 . . . . . . . . . . . . . 14 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (absβ€˜(π‘…β€˜(π‘₯ / 1))) ∈ ℝ)
7574recnd 11188 . . . . . . . . . . . . 13 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (absβ€˜(π‘…β€˜(π‘₯ / 1))) ∈ β„‚)
7675mul01d 11359 . . . . . . . . . . . 12 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((absβ€˜(π‘…β€˜(π‘₯ / 1))) Β· 0) = 0)
7765, 76oveq12d 7376 . . . . . . . . . . 11 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((absβ€˜(π‘…β€˜(π‘₯ / ((βŒŠβ€˜π‘₯) + 1)))) Β· ((π‘†β€˜(((βŒŠβ€˜π‘₯) + 1) βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(((βŒŠβ€˜π‘₯) + 1) βˆ’ 1))))) βˆ’ ((absβ€˜(π‘…β€˜(π‘₯ / 1))) Β· 0)) = (((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))) βˆ’ 0))
7847pntsf 26937 . . . . . . . . . . . . . . . . 17 𝑆:β„βŸΆβ„
7978ffvelcdmi 7035 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ ℝ β†’ (π‘†β€˜π‘₯) ∈ ℝ)
802, 79syl 17 . . . . . . . . . . . . . . 15 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘†β€˜π‘₯) ∈ ℝ)
81 pntrlog2bnd.t . . . . . . . . . . . . . . . . . . 19 𝑇 = (π‘Ž ∈ ℝ ↦ if(π‘Ž ∈ ℝ+, (π‘Ž Β· (logβ€˜π‘Ž)), 0))
82 relogcl 25947 . . . . . . . . . . . . . . . . . . . . 21 (π‘Ž ∈ ℝ+ β†’ (logβ€˜π‘Ž) ∈ ℝ)
83 remulcl 11141 . . . . . . . . . . . . . . . . . . . . 21 ((π‘Ž ∈ ℝ ∧ (logβ€˜π‘Ž) ∈ ℝ) β†’ (π‘Ž Β· (logβ€˜π‘Ž)) ∈ ℝ)
8482, 83sylan2 594 . . . . . . . . . . . . . . . . . . . 20 ((π‘Ž ∈ ℝ ∧ π‘Ž ∈ ℝ+) β†’ (π‘Ž Β· (logβ€˜π‘Ž)) ∈ ℝ)
85 0red 11163 . . . . . . . . . . . . . . . . . . . 20 ((π‘Ž ∈ ℝ ∧ Β¬ π‘Ž ∈ ℝ+) β†’ 0 ∈ ℝ)
8684, 85ifclda 4522 . . . . . . . . . . . . . . . . . . 19 (π‘Ž ∈ ℝ β†’ if(π‘Ž ∈ ℝ+, (π‘Ž Β· (logβ€˜π‘Ž)), 0) ∈ ℝ)
8781, 86fmpti 7061 . . . . . . . . . . . . . . . . . 18 𝑇:β„βŸΆβ„
8887ffvelcdmi 7035 . . . . . . . . . . . . . . . . 17 ((βŒŠβ€˜π‘₯) ∈ ℝ β†’ (π‘‡β€˜(βŒŠβ€˜π‘₯)) ∈ ℝ)
8946, 88syl 17 . . . . . . . . . . . . . . . 16 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘‡β€˜(βŒŠβ€˜π‘₯)) ∈ ℝ)
9023, 89remulcld 11190 . . . . . . . . . . . . . . 15 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))) ∈ ℝ)
9180, 90resubcld 11588 . . . . . . . . . . . . . 14 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯)))) ∈ ℝ)
9221, 91remulcld 11190 . . . . . . . . . . . . 13 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))) ∈ ℝ)
9392recnd 11188 . . . . . . . . . . . 12 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))) ∈ β„‚)
9493subid1d 11506 . . . . . . . . . . 11 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))) βˆ’ 0) = ((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))))
9577, 94eqtrd 2773 . . . . . . . . . 10 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((absβ€˜(π‘…β€˜(π‘₯ / ((βŒŠβ€˜π‘₯) + 1)))) Β· ((π‘†β€˜(((βŒŠβ€˜π‘₯) + 1) βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(((βŒŠβ€˜π‘₯) + 1) βˆ’ 1))))) βˆ’ ((absβ€˜(π‘…β€˜(π‘₯ / 1))) Β· 0)) = ((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))))
962flcld 13709 . . . . . . . . . . . . . 14 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (βŒŠβ€˜π‘₯) ∈ β„€)
97 fzval3 13647 . . . . . . . . . . . . . 14 ((βŒŠβ€˜π‘₯) ∈ β„€ β†’ (1...(βŒŠβ€˜π‘₯)) = (1..^((βŒŠβ€˜π‘₯) + 1)))
9896, 97syl 17 . . . . . . . . . . . . 13 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (1...(βŒŠβ€˜π‘₯)) = (1..^((βŒŠβ€˜π‘₯) + 1)))
9998eqcomd 2739 . . . . . . . . . . . 12 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (1..^((βŒŠβ€˜π‘₯) + 1)) = (1...(βŒŠβ€˜π‘₯)))
10010adantr 482 . . . . . . . . . . . . . . . . . . . . 21 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ π‘₯ ∈ ℝ+)
101 elfznn 13476 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ (1...(βŒŠβ€˜π‘₯)) β†’ 𝑛 ∈ β„•)
102101adantl 483 . . . . . . . . . . . . . . . . . . . . . 22 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ 𝑛 ∈ β„•)
103102nnrpd 12960 . . . . . . . . . . . . . . . . . . . . 21 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ 𝑛 ∈ ℝ+)
104100, 103rpdivcld 12979 . . . . . . . . . . . . . . . . . . . 20 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (π‘₯ / 𝑛) ∈ ℝ+)
10569ffvelcdmi 7035 . . . . . . . . . . . . . . . . . . . 20 ((π‘₯ / 𝑛) ∈ ℝ+ β†’ (π‘…β€˜(π‘₯ / 𝑛)) ∈ ℝ)
106104, 105syl 17 . . . . . . . . . . . . . . . . . . 19 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (π‘…β€˜(π‘₯ / 𝑛)) ∈ ℝ)
107106recnd 11188 . . . . . . . . . . . . . . . . . 18 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (π‘…β€˜(π‘₯ / 𝑛)) ∈ β„‚)
108107abscld 15327 . . . . . . . . . . . . . . . . 17 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) ∈ ℝ)
109108recnd 11188 . . . . . . . . . . . . . . . 16 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) ∈ β„‚)
1103a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ 1 ∈ ℝ+)
111103, 110rpaddcld 12977 . . . . . . . . . . . . . . . . . . . . 21 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (𝑛 + 1) ∈ ℝ+)
112100, 111rpdivcld 12979 . . . . . . . . . . . . . . . . . . . 20 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (π‘₯ / (𝑛 + 1)) ∈ ℝ+)
11369ffvelcdmi 7035 . . . . . . . . . . . . . . . . . . . 20 ((π‘₯ / (𝑛 + 1)) ∈ ℝ+ β†’ (π‘…β€˜(π‘₯ / (𝑛 + 1))) ∈ ℝ)
114112, 113syl 17 . . . . . . . . . . . . . . . . . . 19 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (π‘…β€˜(π‘₯ / (𝑛 + 1))) ∈ ℝ)
115114recnd 11188 . . . . . . . . . . . . . . . . . 18 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (π‘…β€˜(π‘₯ / (𝑛 + 1))) ∈ β„‚)
116115abscld 15327 . . . . . . . . . . . . . . . . 17 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1)))) ∈ ℝ)
117116recnd 11188 . . . . . . . . . . . . . . . 16 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1)))) ∈ β„‚)
118109, 117negsubdi2d 11533 . . . . . . . . . . . . . . 15 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ -((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) = ((absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1)))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / 𝑛)))))
119118eqcomd 2739 . . . . . . . . . . . . . 14 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1)))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / 𝑛)))) = -((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))))
120102nncnd 12174 . . . . . . . . . . . . . . . . 17 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ 𝑛 ∈ β„‚)
121 1cnd 11155 . . . . . . . . . . . . . . . . 17 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ 1 ∈ β„‚)
122120, 121pncand 11518 . . . . . . . . . . . . . . . 16 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((𝑛 + 1) βˆ’ 1) = 𝑛)
123122fveq2d 6847 . . . . . . . . . . . . . . 15 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (π‘†β€˜((𝑛 + 1) βˆ’ 1)) = (π‘†β€˜π‘›))
124122fveq2d 6847 . . . . . . . . . . . . . . . . 17 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (π‘‡β€˜((𝑛 + 1) βˆ’ 1)) = (π‘‡β€˜π‘›))
125 rpre 12928 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℝ+ β†’ 𝑛 ∈ ℝ)
126 eleq1 2822 . . . . . . . . . . . . . . . . . . . . . 22 (π‘Ž = 𝑛 β†’ (π‘Ž ∈ ℝ+ ↔ 𝑛 ∈ ℝ+))
127 id 22 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘Ž = 𝑛 β†’ π‘Ž = 𝑛)
128 fveq2 6843 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘Ž = 𝑛 β†’ (logβ€˜π‘Ž) = (logβ€˜π‘›))
129127, 128oveq12d 7376 . . . . . . . . . . . . . . . . . . . . . 22 (π‘Ž = 𝑛 β†’ (π‘Ž Β· (logβ€˜π‘Ž)) = (𝑛 Β· (logβ€˜π‘›)))
130126, 129ifbieq1d 4511 . . . . . . . . . . . . . . . . . . . . 21 (π‘Ž = 𝑛 β†’ if(π‘Ž ∈ ℝ+, (π‘Ž Β· (logβ€˜π‘Ž)), 0) = if(𝑛 ∈ ℝ+, (𝑛 Β· (logβ€˜π‘›)), 0))
131 ovex 7391 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 Β· (logβ€˜π‘›)) ∈ V
132 c0ex 11154 . . . . . . . . . . . . . . . . . . . . . 22 0 ∈ V
133131, 132ifex 4537 . . . . . . . . . . . . . . . . . . . . 21 if(𝑛 ∈ ℝ+, (𝑛 Β· (logβ€˜π‘›)), 0) ∈ V
134130, 81, 133fvmpt 6949 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℝ β†’ (π‘‡β€˜π‘›) = if(𝑛 ∈ ℝ+, (𝑛 Β· (logβ€˜π‘›)), 0))
135125, 134syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℝ+ β†’ (π‘‡β€˜π‘›) = if(𝑛 ∈ ℝ+, (𝑛 Β· (logβ€˜π‘›)), 0))
136 iftrue 4493 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℝ+ β†’ if(𝑛 ∈ ℝ+, (𝑛 Β· (logβ€˜π‘›)), 0) = (𝑛 Β· (logβ€˜π‘›)))
137135, 136eqtrd 2773 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℝ+ β†’ (π‘‡β€˜π‘›) = (𝑛 Β· (logβ€˜π‘›)))
138103, 137syl 17 . . . . . . . . . . . . . . . . 17 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (π‘‡β€˜π‘›) = (𝑛 Β· (logβ€˜π‘›)))
139124, 138eqtrd 2773 . . . . . . . . . . . . . . . 16 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (π‘‡β€˜((𝑛 + 1) βˆ’ 1)) = (𝑛 Β· (logβ€˜π‘›)))
140139oveq2d 7374 . . . . . . . . . . . . . . 15 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (2 Β· (π‘‡β€˜((𝑛 + 1) βˆ’ 1))) = (2 Β· (𝑛 Β· (logβ€˜π‘›))))
141123, 140oveq12d 7376 . . . . . . . . . . . . . 14 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((π‘†β€˜((𝑛 + 1) βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜((𝑛 + 1) βˆ’ 1)))) = ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›)))))
142119, 141oveq12d 7376 . . . . . . . . . . . . 13 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (((absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1)))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / 𝑛)))) Β· ((π‘†β€˜((𝑛 + 1) βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜((𝑛 + 1) βˆ’ 1))))) = (-((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›))))))
143108, 116resubcld 11588 . . . . . . . . . . . . . . 15 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) ∈ ℝ)
144143recnd 11188 . . . . . . . . . . . . . 14 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) ∈ β„‚)
145102nnred 12173 . . . . . . . . . . . . . . . . 17 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ 𝑛 ∈ ℝ)
14678ffvelcdmi 7035 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℝ β†’ (π‘†β€˜π‘›) ∈ ℝ)
147145, 146syl 17 . . . . . . . . . . . . . . . 16 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (π‘†β€˜π‘›) ∈ ℝ)
14822a1i 11 . . . . . . . . . . . . . . . . 17 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ 2 ∈ ℝ)
149103relogcld 25994 . . . . . . . . . . . . . . . . . 18 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (logβ€˜π‘›) ∈ ℝ)
150145, 149remulcld 11190 . . . . . . . . . . . . . . . . 17 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (𝑛 Β· (logβ€˜π‘›)) ∈ ℝ)
151148, 150remulcld 11190 . . . . . . . . . . . . . . . 16 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (2 Β· (𝑛 Β· (logβ€˜π‘›))) ∈ ℝ)
152147, 151resubcld 11588 . . . . . . . . . . . . . . 15 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›)))) ∈ ℝ)
153152recnd 11188 . . . . . . . . . . . . . 14 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›)))) ∈ β„‚)
154144, 153mulneg1d 11613 . . . . . . . . . . . . 13 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (-((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›))))) = -(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›))))))
155142, 154eqtrd 2773 . . . . . . . . . . . 12 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (((absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1)))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / 𝑛)))) Β· ((π‘†β€˜((𝑛 + 1) βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜((𝑛 + 1) βˆ’ 1))))) = -(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›))))))
15699, 155sumeq12rdv 15597 . . . . . . . . . . 11 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Σ𝑛 ∈ (1..^((βŒŠβ€˜π‘₯) + 1))(((absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1)))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / 𝑛)))) Β· ((π‘†β€˜((𝑛 + 1) βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜((𝑛 + 1) βˆ’ 1))))) = Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))-(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›))))))
157 fzfid 13884 . . . . . . . . . . . 12 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (1...(βŒŠβ€˜π‘₯)) ∈ Fin)
158143, 152remulcld 11190 . . . . . . . . . . . . 13 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›))))) ∈ ℝ)
159158recnd 11188 . . . . . . . . . . . 12 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›))))) ∈ β„‚)
160157, 159fsumneg 15677 . . . . . . . . . . 11 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))-(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›))))) = -Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›))))))
161156, 160eqtrd 2773 . . . . . . . . . 10 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Σ𝑛 ∈ (1..^((βŒŠβ€˜π‘₯) + 1))(((absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1)))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / 𝑛)))) Β· ((π‘†β€˜((𝑛 + 1) βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜((𝑛 + 1) βˆ’ 1))))) = -Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›))))))
16295, 161oveq12d 7376 . . . . . . . . 9 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((((absβ€˜(π‘…β€˜(π‘₯ / ((βŒŠβ€˜π‘₯) + 1)))) Β· ((π‘†β€˜(((βŒŠβ€˜π‘₯) + 1) βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(((βŒŠβ€˜π‘₯) + 1) βˆ’ 1))))) βˆ’ ((absβ€˜(π‘…β€˜(π‘₯ / 1))) Β· 0)) βˆ’ Σ𝑛 ∈ (1..^((βŒŠβ€˜π‘₯) + 1))(((absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1)))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / 𝑛)))) Β· ((π‘†β€˜((𝑛 + 1) βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜((𝑛 + 1) βˆ’ 1)))))) = (((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))) βˆ’ -Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›)))))))
163 oveq2 7366 . . . . . . . . . . . . . 14 (π‘š = 𝑛 β†’ (π‘₯ / π‘š) = (π‘₯ / 𝑛))
164163fveq2d 6847 . . . . . . . . . . . . 13 (π‘š = 𝑛 β†’ (π‘…β€˜(π‘₯ / π‘š)) = (π‘…β€˜(π‘₯ / 𝑛)))
165164fveq2d 6847 . . . . . . . . . . . 12 (π‘š = 𝑛 β†’ (absβ€˜(π‘…β€˜(π‘₯ / π‘š))) = (absβ€˜(π‘…β€˜(π‘₯ / 𝑛))))
166 fvoveq1 7381 . . . . . . . . . . . . 13 (π‘š = 𝑛 β†’ (π‘†β€˜(π‘š βˆ’ 1)) = (π‘†β€˜(𝑛 βˆ’ 1)))
167 fvoveq1 7381 . . . . . . . . . . . . . 14 (π‘š = 𝑛 β†’ (π‘‡β€˜(π‘š βˆ’ 1)) = (π‘‡β€˜(𝑛 βˆ’ 1)))
168167oveq2d 7374 . . . . . . . . . . . . 13 (π‘š = 𝑛 β†’ (2 Β· (π‘‡β€˜(π‘š βˆ’ 1))) = (2 Β· (π‘‡β€˜(𝑛 βˆ’ 1))))
169166, 168oveq12d 7376 . . . . . . . . . . . 12 (π‘š = 𝑛 β†’ ((π‘†β€˜(π‘š βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(π‘š βˆ’ 1)))) = ((π‘†β€˜(𝑛 βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(𝑛 βˆ’ 1)))))
170165, 169jca 513 . . . . . . . . . . 11 (π‘š = 𝑛 β†’ ((absβ€˜(π‘…β€˜(π‘₯ / π‘š))) = (absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) ∧ ((π‘†β€˜(π‘š βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(π‘š βˆ’ 1)))) = ((π‘†β€˜(𝑛 βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(𝑛 βˆ’ 1))))))
171 oveq2 7366 . . . . . . . . . . . . . 14 (π‘š = (𝑛 + 1) β†’ (π‘₯ / π‘š) = (π‘₯ / (𝑛 + 1)))
172171fveq2d 6847 . . . . . . . . . . . . 13 (π‘š = (𝑛 + 1) β†’ (π‘…β€˜(π‘₯ / π‘š)) = (π‘…β€˜(π‘₯ / (𝑛 + 1))))
173172fveq2d 6847 . . . . . . . . . . . 12 (π‘š = (𝑛 + 1) β†’ (absβ€˜(π‘…β€˜(π‘₯ / π‘š))) = (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1)))))
174 fvoveq1 7381 . . . . . . . . . . . . 13 (π‘š = (𝑛 + 1) β†’ (π‘†β€˜(π‘š βˆ’ 1)) = (π‘†β€˜((𝑛 + 1) βˆ’ 1)))
175 fvoveq1 7381 . . . . . . . . . . . . . 14 (π‘š = (𝑛 + 1) β†’ (π‘‡β€˜(π‘š βˆ’ 1)) = (π‘‡β€˜((𝑛 + 1) βˆ’ 1)))
176175oveq2d 7374 . . . . . . . . . . . . 13 (π‘š = (𝑛 + 1) β†’ (2 Β· (π‘‡β€˜(π‘š βˆ’ 1))) = (2 Β· (π‘‡β€˜((𝑛 + 1) βˆ’ 1))))
177174, 176oveq12d 7376 . . . . . . . . . . . 12 (π‘š = (𝑛 + 1) β†’ ((π‘†β€˜(π‘š βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(π‘š βˆ’ 1)))) = ((π‘†β€˜((𝑛 + 1) βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜((𝑛 + 1) βˆ’ 1)))))
178173, 177jca 513 . . . . . . . . . . 11 (π‘š = (𝑛 + 1) β†’ ((absβ€˜(π‘…β€˜(π‘₯ / π‘š))) = (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1)))) ∧ ((π‘†β€˜(π‘š βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(π‘š βˆ’ 1)))) = ((π‘†β€˜((𝑛 + 1) βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜((𝑛 + 1) βˆ’ 1))))))
179 oveq2 7366 . . . . . . . . . . . . . 14 (π‘š = 1 β†’ (π‘₯ / π‘š) = (π‘₯ / 1))
180179fveq2d 6847 . . . . . . . . . . . . 13 (π‘š = 1 β†’ (π‘…β€˜(π‘₯ / π‘š)) = (π‘…β€˜(π‘₯ / 1)))
181180fveq2d 6847 . . . . . . . . . . . 12 (π‘š = 1 β†’ (absβ€˜(π‘…β€˜(π‘₯ / π‘š))) = (absβ€˜(π‘…β€˜(π‘₯ / 1))))
182 oveq1 7365 . . . . . . . . . . . . . . . . 17 (π‘š = 1 β†’ (π‘š βˆ’ 1) = (1 βˆ’ 1))
183 1m1e0 12230 . . . . . . . . . . . . . . . . 17 (1 βˆ’ 1) = 0
184182, 183eqtrdi 2789 . . . . . . . . . . . . . . . 16 (π‘š = 1 β†’ (π‘š βˆ’ 1) = 0)
185184fveq2d 6847 . . . . . . . . . . . . . . 15 (π‘š = 1 β†’ (π‘†β€˜(π‘š βˆ’ 1)) = (π‘†β€˜0))
186 0re 11162 . . . . . . . . . . . . . . . 16 0 ∈ ℝ
187 fveq2 6843 . . . . . . . . . . . . . . . . . . . . . 22 (π‘Ž = 0 β†’ (βŒŠβ€˜π‘Ž) = (βŒŠβ€˜0))
188 0z 12515 . . . . . . . . . . . . . . . . . . . . . . 23 0 ∈ β„€
189 flid 13719 . . . . . . . . . . . . . . . . . . . . . . 23 (0 ∈ β„€ β†’ (βŒŠβ€˜0) = 0)
190188, 189ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 (βŒŠβ€˜0) = 0
191187, 190eqtrdi 2789 . . . . . . . . . . . . . . . . . . . . 21 (π‘Ž = 0 β†’ (βŒŠβ€˜π‘Ž) = 0)
192191oveq2d 7374 . . . . . . . . . . . . . . . . . . . 20 (π‘Ž = 0 β†’ (1...(βŒŠβ€˜π‘Ž)) = (1...0))
193 fz10 13468 . . . . . . . . . . . . . . . . . . . 20 (1...0) = βˆ…
194192, 193eqtrdi 2789 . . . . . . . . . . . . . . . . . . 19 (π‘Ž = 0 β†’ (1...(βŒŠβ€˜π‘Ž)) = βˆ…)
195194sumeq1d 15591 . . . . . . . . . . . . . . . . . 18 (π‘Ž = 0 β†’ Σ𝑖 ∈ (1...(βŒŠβ€˜π‘Ž))((Ξ›β€˜π‘–) Β· ((logβ€˜π‘–) + (Οˆβ€˜(π‘Ž / 𝑖)))) = Σ𝑖 ∈ βˆ… ((Ξ›β€˜π‘–) Β· ((logβ€˜π‘–) + (Οˆβ€˜(π‘Ž / 𝑖)))))
196 sum0 15611 . . . . . . . . . . . . . . . . . 18 Σ𝑖 ∈ βˆ… ((Ξ›β€˜π‘–) Β· ((logβ€˜π‘–) + (Οˆβ€˜(π‘Ž / 𝑖)))) = 0
197195, 196eqtrdi 2789 . . . . . . . . . . . . . . . . 17 (π‘Ž = 0 β†’ Σ𝑖 ∈ (1...(βŒŠβ€˜π‘Ž))((Ξ›β€˜π‘–) Β· ((logβ€˜π‘–) + (Οˆβ€˜(π‘Ž / 𝑖)))) = 0)
198197, 47, 132fvmpt 6949 . . . . . . . . . . . . . . . 16 (0 ∈ ℝ β†’ (π‘†β€˜0) = 0)
199186, 198ax-mp 5 . . . . . . . . . . . . . . 15 (π‘†β€˜0) = 0
200185, 199eqtrdi 2789 . . . . . . . . . . . . . 14 (π‘š = 1 β†’ (π‘†β€˜(π‘š βˆ’ 1)) = 0)
201184fveq2d 6847 . . . . . . . . . . . . . . . . 17 (π‘š = 1 β†’ (π‘‡β€˜(π‘š βˆ’ 1)) = (π‘‡β€˜0))
202 rpne0 12936 . . . . . . . . . . . . . . . . . . . . 21 (π‘Ž ∈ ℝ+ β†’ π‘Ž β‰  0)
203202necon2bi 2971 . . . . . . . . . . . . . . . . . . . 20 (π‘Ž = 0 β†’ Β¬ π‘Ž ∈ ℝ+)
204203iffalsed 4498 . . . . . . . . . . . . . . . . . . 19 (π‘Ž = 0 β†’ if(π‘Ž ∈ ℝ+, (π‘Ž Β· (logβ€˜π‘Ž)), 0) = 0)
205204, 81, 132fvmpt 6949 . . . . . . . . . . . . . . . . . 18 (0 ∈ ℝ β†’ (π‘‡β€˜0) = 0)
206186, 205ax-mp 5 . . . . . . . . . . . . . . . . 17 (π‘‡β€˜0) = 0
207201, 206eqtrdi 2789 . . . . . . . . . . . . . . . 16 (π‘š = 1 β†’ (π‘‡β€˜(π‘š βˆ’ 1)) = 0)
208207oveq2d 7374 . . . . . . . . . . . . . . 15 (π‘š = 1 β†’ (2 Β· (π‘‡β€˜(π‘š βˆ’ 1))) = (2 Β· 0))
209 2t0e0 12327 . . . . . . . . . . . . . . 15 (2 Β· 0) = 0
210208, 209eqtrdi 2789 . . . . . . . . . . . . . 14 (π‘š = 1 β†’ (2 Β· (π‘‡β€˜(π‘š βˆ’ 1))) = 0)
211200, 210oveq12d 7376 . . . . . . . . . . . . 13 (π‘š = 1 β†’ ((π‘†β€˜(π‘š βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(π‘š βˆ’ 1)))) = (0 βˆ’ 0))
212 0m0e0 12278 . . . . . . . . . . . . 13 (0 βˆ’ 0) = 0
213211, 212eqtrdi 2789 . . . . . . . . . . . 12 (π‘š = 1 β†’ ((π‘†β€˜(π‘š βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(π‘š βˆ’ 1)))) = 0)
214181, 213jca 513 . . . . . . . . . . 11 (π‘š = 1 β†’ ((absβ€˜(π‘…β€˜(π‘₯ / π‘š))) = (absβ€˜(π‘…β€˜(π‘₯ / 1))) ∧ ((π‘†β€˜(π‘š βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(π‘š βˆ’ 1)))) = 0))
215 oveq2 7366 . . . . . . . . . . . . . 14 (π‘š = ((βŒŠβ€˜π‘₯) + 1) β†’ (π‘₯ / π‘š) = (π‘₯ / ((βŒŠβ€˜π‘₯) + 1)))
216215fveq2d 6847 . . . . . . . . . . . . 13 (π‘š = ((βŒŠβ€˜π‘₯) + 1) β†’ (π‘…β€˜(π‘₯ / π‘š)) = (π‘…β€˜(π‘₯ / ((βŒŠβ€˜π‘₯) + 1))))
217216fveq2d 6847 . . . . . . . . . . . 12 (π‘š = ((βŒŠβ€˜π‘₯) + 1) β†’ (absβ€˜(π‘…β€˜(π‘₯ / π‘š))) = (absβ€˜(π‘…β€˜(π‘₯ / ((βŒŠβ€˜π‘₯) + 1)))))
218 fvoveq1 7381 . . . . . . . . . . . . 13 (π‘š = ((βŒŠβ€˜π‘₯) + 1) β†’ (π‘†β€˜(π‘š βˆ’ 1)) = (π‘†β€˜(((βŒŠβ€˜π‘₯) + 1) βˆ’ 1)))
219 fvoveq1 7381 . . . . . . . . . . . . . 14 (π‘š = ((βŒŠβ€˜π‘₯) + 1) β†’ (π‘‡β€˜(π‘š βˆ’ 1)) = (π‘‡β€˜(((βŒŠβ€˜π‘₯) + 1) βˆ’ 1)))
220219oveq2d 7374 . . . . . . . . . . . . 13 (π‘š = ((βŒŠβ€˜π‘₯) + 1) β†’ (2 Β· (π‘‡β€˜(π‘š βˆ’ 1))) = (2 Β· (π‘‡β€˜(((βŒŠβ€˜π‘₯) + 1) βˆ’ 1))))
221218, 220oveq12d 7376 . . . . . . . . . . . 12 (π‘š = ((βŒŠβ€˜π‘₯) + 1) β†’ ((π‘†β€˜(π‘š βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(π‘š βˆ’ 1)))) = ((π‘†β€˜(((βŒŠβ€˜π‘₯) + 1) βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(((βŒŠβ€˜π‘₯) + 1) βˆ’ 1)))))
222217, 221jca 513 . . . . . . . . . . 11 (π‘š = ((βŒŠβ€˜π‘₯) + 1) β†’ ((absβ€˜(π‘…β€˜(π‘₯ / π‘š))) = (absβ€˜(π‘…β€˜(π‘₯ / ((βŒŠβ€˜π‘₯) + 1)))) ∧ ((π‘†β€˜(π‘š βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(π‘š βˆ’ 1)))) = ((π‘†β€˜(((βŒŠβ€˜π‘₯) + 1) βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(((βŒŠβ€˜π‘₯) + 1) βˆ’ 1))))))
223 nnuz 12811 . . . . . . . . . . . 12 β„• = (β„€β‰₯β€˜1)
22415, 223eleqtrdi 2844 . . . . . . . . . . 11 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((βŒŠβ€˜π‘₯) + 1) ∈ (β„€β‰₯β€˜1))
22510adantr 482 . . . . . . . . . . . . . . . 16 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...((βŒŠβ€˜π‘₯) + 1))) β†’ π‘₯ ∈ ℝ+)
226 elfznn 13476 . . . . . . . . . . . . . . . . . 18 (π‘š ∈ (1...((βŒŠβ€˜π‘₯) + 1)) β†’ π‘š ∈ β„•)
227226adantl 483 . . . . . . . . . . . . . . . . 17 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...((βŒŠβ€˜π‘₯) + 1))) β†’ π‘š ∈ β„•)
228227nnrpd 12960 . . . . . . . . . . . . . . . 16 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...((βŒŠβ€˜π‘₯) + 1))) β†’ π‘š ∈ ℝ+)
229225, 228rpdivcld 12979 . . . . . . . . . . . . . . 15 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...((βŒŠβ€˜π‘₯) + 1))) β†’ (π‘₯ / π‘š) ∈ ℝ+)
23069ffvelcdmi 7035 . . . . . . . . . . . . . . 15 ((π‘₯ / π‘š) ∈ ℝ+ β†’ (π‘…β€˜(π‘₯ / π‘š)) ∈ ℝ)
231229, 230syl 17 . . . . . . . . . . . . . 14 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...((βŒŠβ€˜π‘₯) + 1))) β†’ (π‘…β€˜(π‘₯ / π‘š)) ∈ ℝ)
232231recnd 11188 . . . . . . . . . . . . 13 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...((βŒŠβ€˜π‘₯) + 1))) β†’ (π‘…β€˜(π‘₯ / π‘š)) ∈ β„‚)
233232abscld 15327 . . . . . . . . . . . 12 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...((βŒŠβ€˜π‘₯) + 1))) β†’ (absβ€˜(π‘…β€˜(π‘₯ / π‘š))) ∈ ℝ)
234233recnd 11188 . . . . . . . . . . 11 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...((βŒŠβ€˜π‘₯) + 1))) β†’ (absβ€˜(π‘…β€˜(π‘₯ / π‘š))) ∈ β„‚)
235227nnred 12173 . . . . . . . . . . . . . . 15 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...((βŒŠβ€˜π‘₯) + 1))) β†’ π‘š ∈ ℝ)
236 1red 11161 . . . . . . . . . . . . . . 15 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...((βŒŠβ€˜π‘₯) + 1))) β†’ 1 ∈ ℝ)
237235, 236resubcld 11588 . . . . . . . . . . . . . 14 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...((βŒŠβ€˜π‘₯) + 1))) β†’ (π‘š βˆ’ 1) ∈ ℝ)
23878ffvelcdmi 7035 . . . . . . . . . . . . . 14 ((π‘š βˆ’ 1) ∈ ℝ β†’ (π‘†β€˜(π‘š βˆ’ 1)) ∈ ℝ)
239237, 238syl 17 . . . . . . . . . . . . 13 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...((βŒŠβ€˜π‘₯) + 1))) β†’ (π‘†β€˜(π‘š βˆ’ 1)) ∈ ℝ)
24022a1i 11 . . . . . . . . . . . . . 14 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...((βŒŠβ€˜π‘₯) + 1))) β†’ 2 ∈ ℝ)
24187ffvelcdmi 7035 . . . . . . . . . . . . . . 15 ((π‘š βˆ’ 1) ∈ ℝ β†’ (π‘‡β€˜(π‘š βˆ’ 1)) ∈ ℝ)
242237, 241syl 17 . . . . . . . . . . . . . 14 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...((βŒŠβ€˜π‘₯) + 1))) β†’ (π‘‡β€˜(π‘š βˆ’ 1)) ∈ ℝ)
243240, 242remulcld 11190 . . . . . . . . . . . . 13 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...((βŒŠβ€˜π‘₯) + 1))) β†’ (2 Β· (π‘‡β€˜(π‘š βˆ’ 1))) ∈ ℝ)
244239, 243resubcld 11588 . . . . . . . . . . . 12 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...((βŒŠβ€˜π‘₯) + 1))) β†’ ((π‘†β€˜(π‘š βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(π‘š βˆ’ 1)))) ∈ ℝ)
245244recnd 11188 . . . . . . . . . . 11 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...((βŒŠβ€˜π‘₯) + 1))) β†’ ((π‘†β€˜(π‘š βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(π‘š βˆ’ 1)))) ∈ β„‚)
246170, 178, 214, 222, 224, 234, 245fsumparts 15696 . . . . . . . . . 10 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Σ𝑛 ∈ (1..^((βŒŠβ€˜π‘₯) + 1))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜((𝑛 + 1) βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜((𝑛 + 1) βˆ’ 1)))) βˆ’ ((π‘†β€˜(𝑛 βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(𝑛 βˆ’ 1)))))) = ((((absβ€˜(π‘…β€˜(π‘₯ / ((βŒŠβ€˜π‘₯) + 1)))) Β· ((π‘†β€˜(((βŒŠβ€˜π‘₯) + 1) βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(((βŒŠβ€˜π‘₯) + 1) βˆ’ 1))))) βˆ’ ((absβ€˜(π‘…β€˜(π‘₯ / 1))) Β· 0)) βˆ’ Σ𝑛 ∈ (1..^((βŒŠβ€˜π‘₯) + 1))(((absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1)))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / 𝑛)))) Β· ((π‘†β€˜((𝑛 + 1) βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜((𝑛 + 1) βˆ’ 1)))))))
247147recnd 11188 . . . . . . . . . . . . . 14 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (π‘†β€˜π‘›) ∈ β„‚)
24887ffvelcdmi 7035 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℝ β†’ (π‘‡β€˜π‘›) ∈ ℝ)
249145, 248syl 17 . . . . . . . . . . . . . . . 16 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (π‘‡β€˜π‘›) ∈ ℝ)
250148, 249remulcld 11190 . . . . . . . . . . . . . . 15 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (2 Β· (π‘‡β€˜π‘›)) ∈ ℝ)
251250recnd 11188 . . . . . . . . . . . . . 14 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (2 Β· (π‘‡β€˜π‘›)) ∈ β„‚)
252 1red 11161 . . . . . . . . . . . . . . . . 17 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ 1 ∈ ℝ)
253145, 252resubcld 11588 . . . . . . . . . . . . . . . 16 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (𝑛 βˆ’ 1) ∈ ℝ)
25478ffvelcdmi 7035 . . . . . . . . . . . . . . . 16 ((𝑛 βˆ’ 1) ∈ ℝ β†’ (π‘†β€˜(𝑛 βˆ’ 1)) ∈ ℝ)
255253, 254syl 17 . . . . . . . . . . . . . . 15 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (π‘†β€˜(𝑛 βˆ’ 1)) ∈ ℝ)
256255recnd 11188 . . . . . . . . . . . . . 14 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (π‘†β€˜(𝑛 βˆ’ 1)) ∈ β„‚)
25787ffvelcdmi 7035 . . . . . . . . . . . . . . . . 17 ((𝑛 βˆ’ 1) ∈ ℝ β†’ (π‘‡β€˜(𝑛 βˆ’ 1)) ∈ ℝ)
258253, 257syl 17 . . . . . . . . . . . . . . . 16 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (π‘‡β€˜(𝑛 βˆ’ 1)) ∈ ℝ)
259148, 258remulcld 11190 . . . . . . . . . . . . . . 15 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (2 Β· (π‘‡β€˜(𝑛 βˆ’ 1))) ∈ ℝ)
260259recnd 11188 . . . . . . . . . . . . . 14 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (2 Β· (π‘‡β€˜(𝑛 βˆ’ 1))) ∈ β„‚)
261247, 251, 256, 260sub4d 11566 . . . . . . . . . . . . 13 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (((π‘†β€˜π‘›) βˆ’ (2 Β· (π‘‡β€˜π‘›))) βˆ’ ((π‘†β€˜(𝑛 βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(𝑛 βˆ’ 1))))) = (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ ((2 Β· (π‘‡β€˜π‘›)) βˆ’ (2 Β· (π‘‡β€˜(𝑛 βˆ’ 1))))))
262124oveq2d 7374 . . . . . . . . . . . . . . 15 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (2 Β· (π‘‡β€˜((𝑛 + 1) βˆ’ 1))) = (2 Β· (π‘‡β€˜π‘›)))
263123, 262oveq12d 7376 . . . . . . . . . . . . . 14 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((π‘†β€˜((𝑛 + 1) βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜((𝑛 + 1) βˆ’ 1)))) = ((π‘†β€˜π‘›) βˆ’ (2 Β· (π‘‡β€˜π‘›))))
264263oveq1d 7373 . . . . . . . . . . . . 13 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (((π‘†β€˜((𝑛 + 1) βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜((𝑛 + 1) βˆ’ 1)))) βˆ’ ((π‘†β€˜(𝑛 βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(𝑛 βˆ’ 1))))) = (((π‘†β€˜π‘›) βˆ’ (2 Β· (π‘‡β€˜π‘›))) βˆ’ ((π‘†β€˜(𝑛 βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(𝑛 βˆ’ 1))))))
265 2cnd 12236 . . . . . . . . . . . . . . 15 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ 2 ∈ β„‚)
266249recnd 11188 . . . . . . . . . . . . . . 15 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (π‘‡β€˜π‘›) ∈ β„‚)
267258recnd 11188 . . . . . . . . . . . . . . 15 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (π‘‡β€˜(𝑛 βˆ’ 1)) ∈ β„‚)
268265, 266, 267subdid 11616 . . . . . . . . . . . . . 14 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))) = ((2 Β· (π‘‡β€˜π‘›)) βˆ’ (2 Β· (π‘‡β€˜(𝑛 βˆ’ 1)))))
269268oveq2d 7374 . . . . . . . . . . . . 13 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))) = (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ ((2 Β· (π‘‡β€˜π‘›)) βˆ’ (2 Β· (π‘‡β€˜(𝑛 βˆ’ 1))))))
270261, 264, 2693eqtr4d 2783 . . . . . . . . . . . 12 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (((π‘†β€˜((𝑛 + 1) βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜((𝑛 + 1) βˆ’ 1)))) βˆ’ ((π‘†β€˜(𝑛 βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(𝑛 βˆ’ 1))))) = (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))))
271270oveq2d 7374 . . . . . . . . . . 11 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜((𝑛 + 1) βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜((𝑛 + 1) βˆ’ 1)))) βˆ’ ((π‘†β€˜(𝑛 βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(𝑛 βˆ’ 1)))))) = ((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))))
27299, 271sumeq12rdv 15597 . . . . . . . . . 10 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Σ𝑛 ∈ (1..^((βŒŠβ€˜π‘₯) + 1))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜((𝑛 + 1) βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜((𝑛 + 1) βˆ’ 1)))) βˆ’ ((π‘†β€˜(𝑛 βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(𝑛 βˆ’ 1)))))) = Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))))
273246, 272eqtr3d 2775 . . . . . . . . 9 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((((absβ€˜(π‘…β€˜(π‘₯ / ((βŒŠβ€˜π‘₯) + 1)))) Β· ((π‘†β€˜(((βŒŠβ€˜π‘₯) + 1) βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(((βŒŠβ€˜π‘₯) + 1) βˆ’ 1))))) βˆ’ ((absβ€˜(π‘…β€˜(π‘₯ / 1))) Β· 0)) βˆ’ Σ𝑛 ∈ (1..^((βŒŠβ€˜π‘₯) + 1))(((absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1)))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / 𝑛)))) Β· ((π‘†β€˜((𝑛 + 1) βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜((𝑛 + 1) βˆ’ 1)))))) = Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))))
274157, 159fsumcl 15623 . . . . . . . . . 10 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›))))) ∈ β„‚)
27593, 274subnegd 11524 . . . . . . . . 9 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))) βˆ’ -Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›)))))) = (((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))) + Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›)))))))
276162, 273, 2753eqtr3rd 2782 . . . . . . . 8 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))) + Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›)))))) = Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))))
27710relogcld 25994 . . . . . . . . . 10 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (logβ€˜π‘₯) ∈ ℝ)
278277recnd 11188 . . . . . . . . 9 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (logβ€˜π‘₯) ∈ β„‚)
27966, 278mulcomd 11181 . . . . . . . 8 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘₯ Β· (logβ€˜π‘₯)) = ((logβ€˜π‘₯) Β· π‘₯))
280276, 279oveq12d 7376 . . . . . . 7 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))) + Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›)))))) / (π‘₯ Β· (logβ€˜π‘₯))) = (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))) / ((logβ€˜π‘₯) Β· π‘₯)))
281147, 255resubcld 11588 . . . . . . . . . . . 12 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) ∈ ℝ)
282249, 258resubcld 11588 . . . . . . . . . . . . 13 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))) ∈ ℝ)
283148, 282remulcld 11190 . . . . . . . . . . . 12 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))) ∈ ℝ)
284281, 283resubcld 11588 . . . . . . . . . . 11 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))) ∈ ℝ)
285108, 284remulcld 11190 . . . . . . . . . 10 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))) ∈ ℝ)
286157, 285fsumrecl 15624 . . . . . . . . 9 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))) ∈ ℝ)
287286recnd 11188 . . . . . . . 8 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))) ∈ β„‚)
2882, 8rplogcld 26000 . . . . . . . . 9 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (logβ€˜π‘₯) ∈ ℝ+)
289288rpne0d 12967 . . . . . . . 8 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (logβ€˜π‘₯) β‰  0)
29010rpne0d 12967 . . . . . . . 8 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ π‘₯ β‰  0)
291287, 278, 66, 289, 290divdiv1d 11967 . . . . . . 7 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))) / (logβ€˜π‘₯)) / π‘₯) = (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))) / ((logβ€˜π‘₯) Β· π‘₯)))
292280, 291eqtr4d 2776 . . . . . 6 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))) + Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›)))))) / (π‘₯ Β· (logβ€˜π‘₯))) = ((Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))) / (logβ€˜π‘₯)) / π‘₯))
293292oveq2d 7374 . . . . 5 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((((absβ€˜(π‘…β€˜π‘₯)) Β· (logβ€˜π‘₯)) βˆ’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) / (logβ€˜π‘₯))) / π‘₯) + ((((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))) + Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›)))))) / (π‘₯ Β· (logβ€˜π‘₯)))) = (((((absβ€˜(π‘…β€˜π‘₯)) Β· (logβ€˜π‘₯)) βˆ’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) / (logβ€˜π‘₯))) / π‘₯) + ((Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))) / (logβ€˜π‘₯)) / π‘₯)))
29471recnd 11188 . . . . . . . . . 10 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘…β€˜π‘₯) ∈ β„‚)
295294abscld 15327 . . . . . . . . 9 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (absβ€˜(π‘…β€˜π‘₯)) ∈ ℝ)
296295, 277remulcld 11190 . . . . . . . 8 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((absβ€˜(π‘…β€˜π‘₯)) Β· (logβ€˜π‘₯)) ∈ ℝ)
297108, 281remulcld 11190 . . . . . . . . . 10 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) ∈ ℝ)
298157, 297fsumrecl 15624 . . . . . . . . 9 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) ∈ ℝ)
299298, 288rerpdivcld 12993 . . . . . . . 8 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) / (logβ€˜π‘₯)) ∈ ℝ)
300296, 299resubcld 11588 . . . . . . 7 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((absβ€˜(π‘…β€˜π‘₯)) Β· (logβ€˜π‘₯)) βˆ’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) / (logβ€˜π‘₯))) ∈ ℝ)
301300recnd 11188 . . . . . 6 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((absβ€˜(π‘…β€˜π‘₯)) Β· (logβ€˜π‘₯)) βˆ’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) / (logβ€˜π‘₯))) ∈ β„‚)
302287, 278, 289divcld 11936 . . . . . 6 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))) / (logβ€˜π‘₯)) ∈ β„‚)
303301, 302, 66, 290divdird 11974 . . . . 5 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((((absβ€˜(π‘…β€˜π‘₯)) Β· (logβ€˜π‘₯)) βˆ’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) / (logβ€˜π‘₯))) + (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))) / (logβ€˜π‘₯))) / π‘₯) = (((((absβ€˜(π‘…β€˜π‘₯)) Β· (logβ€˜π‘₯)) βˆ’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) / (logβ€˜π‘₯))) / π‘₯) + ((Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))) / (logβ€˜π‘₯)) / π‘₯)))
304296recnd 11188 . . . . . . . 8 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((absβ€˜(π‘…β€˜π‘₯)) Β· (logβ€˜π‘₯)) ∈ β„‚)
305299recnd 11188 . . . . . . . 8 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) / (logβ€˜π‘₯)) ∈ β„‚)
306304, 305, 302subsubd 11545 . . . . . . 7 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((absβ€˜(π‘…β€˜π‘₯)) Β· (logβ€˜π‘₯)) βˆ’ ((Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) / (logβ€˜π‘₯)) βˆ’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))) / (logβ€˜π‘₯)))) = ((((absβ€˜(π‘…β€˜π‘₯)) Β· (logβ€˜π‘₯)) βˆ’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) / (logβ€˜π‘₯))) + (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))) / (logβ€˜π‘₯))))
307 2cnd 12236 . . . . . . . . . . . 12 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 2 ∈ β„‚)
308266, 267subcld 11517 . . . . . . . . . . . . 13 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))) ∈ β„‚)
309109, 308mulcld 11180 . . . . . . . . . . . 12 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))) ∈ β„‚)
310157, 307, 309fsummulc2 15674 . . . . . . . . . . 11 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))) = Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(2 Β· ((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))))
311281recnd 11188 . . . . . . . . . . . . . . 15 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) ∈ β„‚)
312265, 308mulcld 11180 . . . . . . . . . . . . . . 15 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))) ∈ β„‚)
313311, 312nncand 11522 . . . . . . . . . . . . . 14 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))) = (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))
314313oveq2d 7374 . . . . . . . . . . . . 13 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))))) = ((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))))
315284recnd 11188 . . . . . . . . . . . . . 14 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))) ∈ β„‚)
316109, 311, 315subdid 11616 . . . . . . . . . . . . 13 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))))) = (((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) βˆ’ ((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))))))
317109, 265, 308mul12d 11369 . . . . . . . . . . . . 13 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))) = (2 Β· ((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))))
318314, 316, 3173eqtr3d 2781 . . . . . . . . . . . 12 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) βˆ’ ((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))))) = (2 Β· ((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))))
319318sumeq2dv 15593 . . . . . . . . . . 11 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) βˆ’ ((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))))) = Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(2 Β· ((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))))
320297recnd 11188 . . . . . . . . . . . 12 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) ∈ β„‚)
321285recnd 11188 . . . . . . . . . . . 12 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))) ∈ β„‚)
322157, 320, 321fsumsub 15678 . . . . . . . . . . 11 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) βˆ’ ((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))))) = (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) βˆ’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))))))
323310, 319, 3223eqtr2rd 2780 . . . . . . . . . 10 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) βˆ’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))))) = (2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))))
324323oveq1d 7373 . . . . . . . . 9 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) βˆ’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))))) / (logβ€˜π‘₯)) = ((2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))) / (logβ€˜π‘₯)))
325298recnd 11188 . . . . . . . . . 10 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) ∈ β„‚)
326325, 287, 278, 289divsubdird 11975 . . . . . . . . 9 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) βˆ’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))))) / (logβ€˜π‘₯)) = ((Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) / (logβ€˜π‘₯)) βˆ’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))) / (logβ€˜π‘₯))))
327108, 282remulcld 11190 . . . . . . . . . . . 12 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))) ∈ ℝ)
328157, 327fsumrecl 15624 . . . . . . . . . . 11 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))) ∈ ℝ)
329328recnd 11188 . . . . . . . . . 10 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))) ∈ β„‚)
330307, 329, 278, 289div23d 11973 . . . . . . . . 9 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))) / (logβ€˜π‘₯)) = ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))))
331324, 326, 3303eqtr3d 2781 . . . . . . . 8 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) / (logβ€˜π‘₯)) βˆ’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))) / (logβ€˜π‘₯))) = ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))))
332331oveq2d 7374 . . . . . . 7 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((absβ€˜(π‘…β€˜π‘₯)) Β· (logβ€˜π‘₯)) βˆ’ ((Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) / (logβ€˜π‘₯)) βˆ’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))) / (logβ€˜π‘₯)))) = (((absβ€˜(π‘…β€˜π‘₯)) Β· (logβ€˜π‘₯)) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))))
333306, 332eqtr3d 2775 . . . . . 6 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((((absβ€˜(π‘…β€˜π‘₯)) Β· (logβ€˜π‘₯)) βˆ’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) / (logβ€˜π‘₯))) + (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))) / (logβ€˜π‘₯))) = (((absβ€˜(π‘…β€˜π‘₯)) Β· (logβ€˜π‘₯)) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))))
334333oveq1d 7373 . . . . 5 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((((absβ€˜(π‘…β€˜π‘₯)) Β· (logβ€˜π‘₯)) βˆ’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) / (logβ€˜π‘₯))) + (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))) / (logβ€˜π‘₯))) / π‘₯) = ((((absβ€˜(π‘…β€˜π‘₯)) Β· (logβ€˜π‘₯)) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))) / π‘₯))
335293, 303, 3343eqtr2d 2779 . . . 4 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((((absβ€˜(π‘…β€˜π‘₯)) Β· (logβ€˜π‘₯)) βˆ’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) / (logβ€˜π‘₯))) / π‘₯) + ((((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))) + Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›)))))) / (π‘₯ Β· (logβ€˜π‘₯)))) = ((((absβ€˜(π‘…β€˜π‘₯)) Β· (logβ€˜π‘₯)) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))) / π‘₯))
336335mpteq2dva 5206 . . 3 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ (((((absβ€˜(π‘…β€˜π‘₯)) Β· (logβ€˜π‘₯)) βˆ’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) / (logβ€˜π‘₯))) / π‘₯) + ((((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))) + Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›)))))) / (π‘₯ Β· (logβ€˜π‘₯))))) = (π‘₯ ∈ (1(,)+∞) ↦ ((((absβ€˜(π‘…β€˜π‘₯)) Β· (logβ€˜π‘₯)) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))) / π‘₯)))
337300, 10rerpdivcld 12993 . . . 4 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((((absβ€˜(π‘…β€˜π‘₯)) Β· (logβ€˜π‘₯)) βˆ’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) / (logβ€˜π‘₯))) / π‘₯) ∈ ℝ)
338157, 158fsumrecl 15624 . . . . . 6 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›))))) ∈ ℝ)
33992, 338readdcld 11189 . . . . 5 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))) + Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›)))))) ∈ ℝ)
34010, 288rpmulcld 12978 . . . . 5 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘₯ Β· (logβ€˜π‘₯)) ∈ ℝ+)
341339, 340rerpdivcld 12993 . . . 4 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))) + Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›)))))) / (π‘₯ Β· (logβ€˜π‘₯))) ∈ ℝ)
34247, 18pntrlog2bndlem1 26941 . . . . 5 (π‘₯ ∈ (1(,)+∞) ↦ ((((absβ€˜(π‘…β€˜π‘₯)) Β· (logβ€˜π‘₯)) βˆ’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) / (logβ€˜π‘₯))) / π‘₯)) ∈ ≀𝑂(1)
343342a1i 11 . . . 4 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ ((((absβ€˜(π‘…β€˜π‘₯)) Β· (logβ€˜π‘₯)) βˆ’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) / (logβ€˜π‘₯))) / π‘₯)) ∈ ≀𝑂(1))
344340rpcnd 12964 . . . . . . . 8 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘₯ Β· (logβ€˜π‘₯)) ∈ β„‚)
345340rpne0d 12967 . . . . . . . 8 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘₯ Β· (logβ€˜π‘₯)) β‰  0)
34693, 274, 344, 345divdird 11974 . . . . . . 7 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))) + Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›)))))) / (π‘₯ Β· (logβ€˜π‘₯))) = ((((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))) / (π‘₯ Β· (logβ€˜π‘₯))) + (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›))))) / (π‘₯ Β· (logβ€˜π‘₯)))))
34791recnd 11188 . . . . . . . . 9 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯)))) ∈ β„‚)
34843, 347, 344, 345divassd 11971 . . . . . . . 8 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))) / (π‘₯ Β· (logβ€˜π‘₯))) = ((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· (((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯)))) / (π‘₯ Β· (logβ€˜π‘₯)))))
349348oveq1d 7373 . . . . . . 7 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))) / (π‘₯ Β· (logβ€˜π‘₯))) + (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›))))) / (π‘₯ Β· (logβ€˜π‘₯)))) = (((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· (((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯)))) / (π‘₯ Β· (logβ€˜π‘₯)))) + (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›))))) / (π‘₯ Β· (logβ€˜π‘₯)))))
350346, 349eqtrd 2773 . . . . . 6 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))) + Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›)))))) / (π‘₯ Β· (logβ€˜π‘₯))) = (((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· (((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯)))) / (π‘₯ Β· (logβ€˜π‘₯)))) + (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›))))) / (π‘₯ Β· (logβ€˜π‘₯)))))
351350mpteq2dva 5206 . . . . 5 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ ((((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))) + Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›)))))) / (π‘₯ Β· (logβ€˜π‘₯)))) = (π‘₯ ∈ (1(,)+∞) ↦ (((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· (((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯)))) / (π‘₯ Β· (logβ€˜π‘₯)))) + (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›))))) / (π‘₯ Β· (logβ€˜π‘₯))))))
35291, 340rerpdivcld 12993 . . . . . . 7 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯)))) / (π‘₯ Β· (logβ€˜π‘₯))) ∈ ℝ)
35321, 352remulcld 11190 . . . . . 6 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· (((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯)))) / (π‘₯ Β· (logβ€˜π‘₯)))) ∈ ℝ)
354338, 340rerpdivcld 12993 . . . . . 6 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›))))) / (π‘₯ Β· (logβ€˜π‘₯))) ∈ ℝ)
355 ioossre 13331 . . . . . . . . 9 (1(,)+∞) βŠ† ℝ
356355a1i 11 . . . . . . . 8 (⊀ β†’ (1(,)+∞) βŠ† ℝ)
357 1red 11161 . . . . . . . 8 (⊀ β†’ 1 ∈ ℝ)
35821, 5, 30ltled 11308 . . . . . . . . 9 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) ≀ 1)
359358adantrr 716 . . . . . . . 8 ((⊀ ∧ (π‘₯ ∈ (1(,)+∞) ∧ 1 ≀ π‘₯)) β†’ (π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) ≀ 1)
360356, 21, 357, 357, 359ello1d 15411 . . . . . . 7 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ (π‘₯ / ((βŒŠβ€˜π‘₯) + 1))) ∈ ≀𝑂(1))
36180recnd 11188 . . . . . . . . . . 11 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘†β€˜π‘₯) ∈ β„‚)
36290recnd 11188 . . . . . . . . . . 11 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))) ∈ β„‚)
363361, 362, 344, 345divsubdird 11975 . . . . . . . . . 10 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯)))) / (π‘₯ Β· (logβ€˜π‘₯))) = (((π‘†β€˜π‘₯) / (π‘₯ Β· (logβ€˜π‘₯))) βˆ’ ((2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))) / (π‘₯ Β· (logβ€˜π‘₯)))))
364363mpteq2dva 5206 . . . . . . . . 9 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ (((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯)))) / (π‘₯ Β· (logβ€˜π‘₯)))) = (π‘₯ ∈ (1(,)+∞) ↦ (((π‘†β€˜π‘₯) / (π‘₯ Β· (logβ€˜π‘₯))) βˆ’ ((2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))) / (π‘₯ Β· (logβ€˜π‘₯))))))
36580, 340rerpdivcld 12993 . . . . . . . . . 10 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((π‘†β€˜π‘₯) / (π‘₯ Β· (logβ€˜π‘₯))) ∈ ℝ)
36690, 340rerpdivcld 12993 . . . . . . . . . 10 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))) / (π‘₯ Β· (logβ€˜π‘₯))) ∈ ℝ)
367 2cnd 12236 . . . . . . . . . . . 12 (⊀ β†’ 2 ∈ β„‚)
368 o1const 15508 . . . . . . . . . . . 12 (((1(,)+∞) βŠ† ℝ ∧ 2 ∈ β„‚) β†’ (π‘₯ ∈ (1(,)+∞) ↦ 2) ∈ 𝑂(1))
369355, 367, 368sylancr 588 . . . . . . . . . . 11 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ 2) ∈ 𝑂(1))
370365recnd 11188 . . . . . . . . . . . 12 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((π‘†β€˜π‘₯) / (π‘₯ Β· (logβ€˜π‘₯))) ∈ β„‚)
37180, 10rerpdivcld 12993 . . . . . . . . . . . . . . . . 17 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((π‘†β€˜π‘₯) / π‘₯) ∈ ℝ)
372371recnd 11188 . . . . . . . . . . . . . . . 16 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((π‘†β€˜π‘₯) / π‘₯) ∈ β„‚)
373307, 278mulcld 11180 . . . . . . . . . . . . . . . 16 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (2 Β· (logβ€˜π‘₯)) ∈ β„‚)
374372, 373, 278, 289divsubdird 11975 . . . . . . . . . . . . . . 15 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((((π‘†β€˜π‘₯) / π‘₯) βˆ’ (2 Β· (logβ€˜π‘₯))) / (logβ€˜π‘₯)) = ((((π‘†β€˜π‘₯) / π‘₯) / (logβ€˜π‘₯)) βˆ’ ((2 Β· (logβ€˜π‘₯)) / (logβ€˜π‘₯))))
37523, 277remulcld 11190 . . . . . . . . . . . . . . . . . 18 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (2 Β· (logβ€˜π‘₯)) ∈ ℝ)
376371, 375resubcld 11588 . . . . . . . . . . . . . . . . 17 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((π‘†β€˜π‘₯) / π‘₯) βˆ’ (2 Β· (logβ€˜π‘₯))) ∈ ℝ)
377376recnd 11188 . . . . . . . . . . . . . . . 16 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((π‘†β€˜π‘₯) / π‘₯) βˆ’ (2 Β· (logβ€˜π‘₯))) ∈ β„‚)
378377, 278, 289divrecd 11939 . . . . . . . . . . . . . . 15 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((((π‘†β€˜π‘₯) / π‘₯) βˆ’ (2 Β· (logβ€˜π‘₯))) / (logβ€˜π‘₯)) = ((((π‘†β€˜π‘₯) / π‘₯) βˆ’ (2 Β· (logβ€˜π‘₯))) Β· (1 / (logβ€˜π‘₯))))
379361, 66, 278, 290, 289divdiv1d 11967 . . . . . . . . . . . . . . . 16 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((π‘†β€˜π‘₯) / π‘₯) / (logβ€˜π‘₯)) = ((π‘†β€˜π‘₯) / (π‘₯ Β· (logβ€˜π‘₯))))
380307, 278, 289divcan4d 11942 . . . . . . . . . . . . . . . 16 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((2 Β· (logβ€˜π‘₯)) / (logβ€˜π‘₯)) = 2)
381379, 380oveq12d 7376 . . . . . . . . . . . . . . 15 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((((π‘†β€˜π‘₯) / π‘₯) / (logβ€˜π‘₯)) βˆ’ ((2 Β· (logβ€˜π‘₯)) / (logβ€˜π‘₯))) = (((π‘†β€˜π‘₯) / (π‘₯ Β· (logβ€˜π‘₯))) βˆ’ 2))
382374, 378, 3813eqtr3rd 2782 . . . . . . . . . . . . . 14 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((π‘†β€˜π‘₯) / (π‘₯ Β· (logβ€˜π‘₯))) βˆ’ 2) = ((((π‘†β€˜π‘₯) / π‘₯) βˆ’ (2 Β· (logβ€˜π‘₯))) Β· (1 / (logβ€˜π‘₯))))
383382mpteq2dva 5206 . . . . . . . . . . . . 13 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ (((π‘†β€˜π‘₯) / (π‘₯ Β· (logβ€˜π‘₯))) βˆ’ 2)) = (π‘₯ ∈ (1(,)+∞) ↦ ((((π‘†β€˜π‘₯) / π‘₯) βˆ’ (2 Β· (logβ€˜π‘₯))) Β· (1 / (logβ€˜π‘₯)))))
3845, 288rerpdivcld 12993 . . . . . . . . . . . . . 14 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (1 / (logβ€˜π‘₯)) ∈ ℝ)
38510ex 414 . . . . . . . . . . . . . . . 16 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) β†’ π‘₯ ∈ ℝ+))
386385ssrdv 3951 . . . . . . . . . . . . . . 15 (⊀ β†’ (1(,)+∞) βŠ† ℝ+)
38747selbergs 26938 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ ℝ+ ↦ (((π‘†β€˜π‘₯) / π‘₯) βˆ’ (2 Β· (logβ€˜π‘₯)))) ∈ 𝑂(1)
388387a1i 11 . . . . . . . . . . . . . . 15 (⊀ β†’ (π‘₯ ∈ ℝ+ ↦ (((π‘†β€˜π‘₯) / π‘₯) βˆ’ (2 Β· (logβ€˜π‘₯)))) ∈ 𝑂(1))
389386, 388o1res2 15451 . . . . . . . . . . . . . 14 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ (((π‘†β€˜π‘₯) / π‘₯) βˆ’ (2 Β· (logβ€˜π‘₯)))) ∈ 𝑂(1))
390 divlogrlim 26006 . . . . . . . . . . . . . . 15 (π‘₯ ∈ (1(,)+∞) ↦ (1 / (logβ€˜π‘₯))) β‡π‘Ÿ 0
391 rlimo1 15505 . . . . . . . . . . . . . . 15 ((π‘₯ ∈ (1(,)+∞) ↦ (1 / (logβ€˜π‘₯))) β‡π‘Ÿ 0 β†’ (π‘₯ ∈ (1(,)+∞) ↦ (1 / (logβ€˜π‘₯))) ∈ 𝑂(1))
392390, 391mp1i 13 . . . . . . . . . . . . . 14 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ (1 / (logβ€˜π‘₯))) ∈ 𝑂(1))
393376, 384, 389, 392o1mul2 15513 . . . . . . . . . . . . 13 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ ((((π‘†β€˜π‘₯) / π‘₯) βˆ’ (2 Β· (logβ€˜π‘₯))) Β· (1 / (logβ€˜π‘₯)))) ∈ 𝑂(1))
394383, 393eqeltrd 2834 . . . . . . . . . . . 12 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ (((π‘†β€˜π‘₯) / (π‘₯ Β· (logβ€˜π‘₯))) βˆ’ 2)) ∈ 𝑂(1))
395370, 307, 394o1dif 15518 . . . . . . . . . . 11 (⊀ β†’ ((π‘₯ ∈ (1(,)+∞) ↦ ((π‘†β€˜π‘₯) / (π‘₯ Β· (logβ€˜π‘₯)))) ∈ 𝑂(1) ↔ (π‘₯ ∈ (1(,)+∞) ↦ 2) ∈ 𝑂(1)))
396369, 395mpbird 257 . . . . . . . . . 10 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ ((π‘†β€˜π‘₯) / (π‘₯ Β· (logβ€˜π‘₯)))) ∈ 𝑂(1))
39722a1i 11 . . . . . . . . . . . 12 (⊀ β†’ 2 ∈ ℝ)
3982, 277remulcld 11190 . . . . . . . . . . . . . . 15 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘₯ Β· (logβ€˜π‘₯)) ∈ ℝ)
399 2rp 12925 . . . . . . . . . . . . . . . . 17 2 ∈ ℝ+
400399a1i 11 . . . . . . . . . . . . . . . 16 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 2 ∈ ℝ+)
401400rpge0d 12966 . . . . . . . . . . . . . . 15 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 0 ≀ 2)
402 flge1nn 13732 . . . . . . . . . . . . . . . . . . 19 ((π‘₯ ∈ ℝ ∧ 1 ≀ π‘₯) β†’ (βŒŠβ€˜π‘₯) ∈ β„•)
4032, 9, 402syl2anc 585 . . . . . . . . . . . . . . . . . 18 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (βŒŠβ€˜π‘₯) ∈ β„•)
404403nnrpd 12960 . . . . . . . . . . . . . . . . 17 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (βŒŠβ€˜π‘₯) ∈ ℝ+)
405 rpre 12928 . . . . . . . . . . . . . . . . . . 19 ((βŒŠβ€˜π‘₯) ∈ ℝ+ β†’ (βŒŠβ€˜π‘₯) ∈ ℝ)
406 eleq1 2822 . . . . . . . . . . . . . . . . . . . . 21 (π‘Ž = (βŒŠβ€˜π‘₯) β†’ (π‘Ž ∈ ℝ+ ↔ (βŒŠβ€˜π‘₯) ∈ ℝ+))
407 id 22 . . . . . . . . . . . . . . . . . . . . . 22 (π‘Ž = (βŒŠβ€˜π‘₯) β†’ π‘Ž = (βŒŠβ€˜π‘₯))
408 fveq2 6843 . . . . . . . . . . . . . . . . . . . . . 22 (π‘Ž = (βŒŠβ€˜π‘₯) β†’ (logβ€˜π‘Ž) = (logβ€˜(βŒŠβ€˜π‘₯)))
409407, 408oveq12d 7376 . . . . . . . . . . . . . . . . . . . . 21 (π‘Ž = (βŒŠβ€˜π‘₯) β†’ (π‘Ž Β· (logβ€˜π‘Ž)) = ((βŒŠβ€˜π‘₯) Β· (logβ€˜(βŒŠβ€˜π‘₯))))
410406, 409ifbieq1d 4511 . . . . . . . . . . . . . . . . . . . 20 (π‘Ž = (βŒŠβ€˜π‘₯) β†’ if(π‘Ž ∈ ℝ+, (π‘Ž Β· (logβ€˜π‘Ž)), 0) = if((βŒŠβ€˜π‘₯) ∈ ℝ+, ((βŒŠβ€˜π‘₯) Β· (logβ€˜(βŒŠβ€˜π‘₯))), 0))
411 ovex 7391 . . . . . . . . . . . . . . . . . . . . 21 ((βŒŠβ€˜π‘₯) Β· (logβ€˜(βŒŠβ€˜π‘₯))) ∈ V
412411, 132ifex 4537 . . . . . . . . . . . . . . . . . . . 20 if((βŒŠβ€˜π‘₯) ∈ ℝ+, ((βŒŠβ€˜π‘₯) Β· (logβ€˜(βŒŠβ€˜π‘₯))), 0) ∈ V
413410, 81, 412fvmpt 6949 . . . . . . . . . . . . . . . . . . 19 ((βŒŠβ€˜π‘₯) ∈ ℝ β†’ (π‘‡β€˜(βŒŠβ€˜π‘₯)) = if((βŒŠβ€˜π‘₯) ∈ ℝ+, ((βŒŠβ€˜π‘₯) Β· (logβ€˜(βŒŠβ€˜π‘₯))), 0))
414405, 413syl 17 . . . . . . . . . . . . . . . . . 18 ((βŒŠβ€˜π‘₯) ∈ ℝ+ β†’ (π‘‡β€˜(βŒŠβ€˜π‘₯)) = if((βŒŠβ€˜π‘₯) ∈ ℝ+, ((βŒŠβ€˜π‘₯) Β· (logβ€˜(βŒŠβ€˜π‘₯))), 0))
415 iftrue 4493 . . . . . . . . . . . . . . . . . 18 ((βŒŠβ€˜π‘₯) ∈ ℝ+ β†’ if((βŒŠβ€˜π‘₯) ∈ ℝ+, ((βŒŠβ€˜π‘₯) Β· (logβ€˜(βŒŠβ€˜π‘₯))), 0) = ((βŒŠβ€˜π‘₯) Β· (logβ€˜(βŒŠβ€˜π‘₯))))
416414, 415eqtrd 2773 . . . . . . . . . . . . . . . . 17 ((βŒŠβ€˜π‘₯) ∈ ℝ+ β†’ (π‘‡β€˜(βŒŠβ€˜π‘₯)) = ((βŒŠβ€˜π‘₯) Β· (logβ€˜(βŒŠβ€˜π‘₯))))
417404, 416syl 17 . . . . . . . . . . . . . . . 16 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘‡β€˜(βŒŠβ€˜π‘₯)) = ((βŒŠβ€˜π‘₯) Β· (logβ€˜(βŒŠβ€˜π‘₯))))
418404relogcld 25994 . . . . . . . . . . . . . . . . 17 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (logβ€˜(βŒŠβ€˜π‘₯)) ∈ ℝ)
41913nn0ge0d 12481 . . . . . . . . . . . . . . . . 17 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 0 ≀ (βŒŠβ€˜π‘₯))
420403nnge1d 12206 . . . . . . . . . . . . . . . . . 18 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 1 ≀ (βŒŠβ€˜π‘₯))
42146, 420logge0d 26001 . . . . . . . . . . . . . . . . 17 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 0 ≀ (logβ€˜(βŒŠβ€˜π‘₯)))
422 flle 13710 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ ℝ β†’ (βŒŠβ€˜π‘₯) ≀ π‘₯)
4232, 422syl 17 . . . . . . . . . . . . . . . . 17 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (βŒŠβ€˜π‘₯) ≀ π‘₯)
424404, 10logled 25998 . . . . . . . . . . . . . . . . . 18 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((βŒŠβ€˜π‘₯) ≀ π‘₯ ↔ (logβ€˜(βŒŠβ€˜π‘₯)) ≀ (logβ€˜π‘₯)))
425423, 424mpbid 231 . . . . . . . . . . . . . . . . 17 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (logβ€˜(βŒŠβ€˜π‘₯)) ≀ (logβ€˜π‘₯))
42646, 2, 418, 277, 419, 421, 423, 425lemul12ad 12102 . . . . . . . . . . . . . . . 16 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((βŒŠβ€˜π‘₯) Β· (logβ€˜(βŒŠβ€˜π‘₯))) ≀ (π‘₯ Β· (logβ€˜π‘₯)))
427417, 426eqbrtrd 5128 . . . . . . . . . . . . . . 15 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘‡β€˜(βŒŠβ€˜π‘₯)) ≀ (π‘₯ Β· (logβ€˜π‘₯)))
42889, 398, 23, 401, 427lemul2ad 12100 . . . . . . . . . . . . . 14 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))) ≀ (2 Β· (π‘₯ Β· (logβ€˜π‘₯))))
42990, 23, 340ledivmul2d 13016 . . . . . . . . . . . . . 14 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))) / (π‘₯ Β· (logβ€˜π‘₯))) ≀ 2 ↔ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))) ≀ (2 Β· (π‘₯ Β· (logβ€˜π‘₯)))))
430428, 429mpbird 257 . . . . . . . . . . . . 13 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))) / (π‘₯ Β· (logβ€˜π‘₯))) ≀ 2)
431430adantrr 716 . . . . . . . . . . . 12 ((⊀ ∧ (π‘₯ ∈ (1(,)+∞) ∧ 1 ≀ π‘₯)) β†’ ((2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))) / (π‘₯ Β· (logβ€˜π‘₯))) ≀ 2)
432356, 366, 357, 397, 431ello1d 15411 . . . . . . . . . . 11 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ ((2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))) / (π‘₯ Β· (logβ€˜π‘₯)))) ∈ ≀𝑂(1))
433 0red 11163 . . . . . . . . . . . 12 (⊀ β†’ 0 ∈ ℝ)
43446, 418, 419, 421mulge0d 11737 . . . . . . . . . . . . . . 15 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 0 ≀ ((βŒŠβ€˜π‘₯) Β· (logβ€˜(βŒŠβ€˜π‘₯))))
435434, 417breqtrrd 5134 . . . . . . . . . . . . . 14 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 0 ≀ (π‘‡β€˜(βŒŠβ€˜π‘₯)))
43623, 89, 401, 435mulge0d 11737 . . . . . . . . . . . . 13 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 0 ≀ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))
43790, 340, 436divge0d 13002 . . . . . . . . . . . 12 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 0 ≀ ((2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))) / (π‘₯ Β· (logβ€˜π‘₯))))
438366, 433, 437o1lo12 15426 . . . . . . . . . . 11 (⊀ β†’ ((π‘₯ ∈ (1(,)+∞) ↦ ((2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))) / (π‘₯ Β· (logβ€˜π‘₯)))) ∈ 𝑂(1) ↔ (π‘₯ ∈ (1(,)+∞) ↦ ((2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))) / (π‘₯ Β· (logβ€˜π‘₯)))) ∈ ≀𝑂(1)))
439432, 438mpbird 257 . . . . . . . . . 10 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ ((2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))) / (π‘₯ Β· (logβ€˜π‘₯)))) ∈ 𝑂(1))
440365, 366, 396, 439o1sub2 15514 . . . . . . . . 9 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ (((π‘†β€˜π‘₯) / (π‘₯ Β· (logβ€˜π‘₯))) βˆ’ ((2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))) / (π‘₯ Β· (logβ€˜π‘₯))))) ∈ 𝑂(1))
441364, 440eqeltrd 2834 . . . . . . . 8 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ (((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯)))) / (π‘₯ Β· (logβ€˜π‘₯)))) ∈ 𝑂(1))
442352, 441o1lo1d 15427 . . . . . . 7 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ (((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯)))) / (π‘₯ Β· (logβ€˜π‘₯)))) ∈ ≀𝑂(1))
44321, 352, 360, 442, 41lo1mul 15516 . . . . . 6 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ ((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· (((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯)))) / (π‘₯ Β· (logβ€˜π‘₯))))) ∈ ≀𝑂(1))
44447selbergsb 26939 . . . . . . . 8 βˆƒπ‘ ∈ ℝ+ βˆ€π‘¦ ∈ (1[,)+∞)(absβ€˜(((π‘†β€˜π‘¦) / 𝑦) βˆ’ (2 Β· (logβ€˜π‘¦)))) ≀ 𝑐
445 simpl 484 . . . . . . . . . 10 ((𝑐 ∈ ℝ+ ∧ βˆ€π‘¦ ∈ (1[,)+∞)(absβ€˜(((π‘†β€˜π‘¦) / 𝑦) βˆ’ (2 Β· (logβ€˜π‘¦)))) ≀ 𝑐) β†’ 𝑐 ∈ ℝ+)
446 simpr 486 . . . . . . . . . 10 ((𝑐 ∈ ℝ+ ∧ βˆ€π‘¦ ∈ (1[,)+∞)(absβ€˜(((π‘†β€˜π‘¦) / 𝑦) βˆ’ (2 Β· (logβ€˜π‘¦)))) ≀ 𝑐) β†’ βˆ€π‘¦ ∈ (1[,)+∞)(absβ€˜(((π‘†β€˜π‘¦) / 𝑦) βˆ’ (2 Β· (logβ€˜π‘¦)))) ≀ 𝑐)
44747, 18, 445, 446pntrlog2bndlem3 26943 . . . . . . . . 9 ((𝑐 ∈ ℝ+ ∧ βˆ€π‘¦ ∈ (1[,)+∞)(absβ€˜(((π‘†β€˜π‘¦) / 𝑦) βˆ’ (2 Β· (logβ€˜π‘¦)))) ≀ 𝑐) β†’ (π‘₯ ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›))))) / (π‘₯ Β· (logβ€˜π‘₯)))) ∈ 𝑂(1))
448447rexlimiva 3141 . . . . . . . 8 (βˆƒπ‘ ∈ ℝ+ βˆ€π‘¦ ∈ (1[,)+∞)(absβ€˜(((π‘†β€˜π‘¦) / 𝑦) βˆ’ (2 Β· (logβ€˜π‘¦)))) ≀ 𝑐 β†’ (π‘₯ ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›))))) / (π‘₯ Β· (logβ€˜π‘₯)))) ∈ 𝑂(1))
449444, 448mp1i 13 . . . . . . 7 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›))))) / (π‘₯ Β· (logβ€˜π‘₯)))) ∈ 𝑂(1))
450354, 449o1lo1d 15427 . . . . . 6 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›))))) / (π‘₯ Β· (logβ€˜π‘₯)))) ∈ ≀𝑂(1))
451353, 354, 443, 450lo1add 15515 . . . . 5 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ (((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· (((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯)))) / (π‘₯ Β· (logβ€˜π‘₯)))) + (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›))))) / (π‘₯ Β· (logβ€˜π‘₯))))) ∈ ≀𝑂(1))
452351, 451eqeltrd 2834 . . . 4 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ ((((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))) + Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›)))))) / (π‘₯ Β· (logβ€˜π‘₯)))) ∈ ≀𝑂(1))
453337, 341, 343, 452lo1add 15515 . . 3 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ (((((absβ€˜(π‘…β€˜π‘₯)) Β· (logβ€˜π‘₯)) βˆ’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) / (logβ€˜π‘₯))) / π‘₯) + ((((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))) + Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›)))))) / (π‘₯ Β· (logβ€˜π‘₯))))) ∈ ≀𝑂(1))
454336, 453eqeltrrd 2835 . 2 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ ((((absβ€˜(π‘…β€˜π‘₯)) Β· (logβ€˜π‘₯)) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))) / π‘₯)) ∈ ≀𝑂(1))
455454mptru 1549 1 (π‘₯ ∈ (1(,)+∞) ↦ ((((absβ€˜(π‘…β€˜π‘₯)) Β· (logβ€˜π‘₯)) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))) / π‘₯)) ∈ ≀𝑂(1)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   ↔ wb 205   ∧ wa 397   = wceq 1542  βŠ€wtru 1543   ∈ wcel 2107  βˆ€wral 3061  βˆƒwrex 3070  {crab 3406   βŠ† wss 3911  βˆ…c0 4283  ifcif 4487   class class class wbr 5106   ↦ cmpt 5189  β€˜cfv 6497  (class class class)co 7358  β„‚cc 11054  β„cr 11055  0cc0 11056  1c1 11057   + caddc 11059   Β· cmul 11061  +∞cpnf 11191   < clt 11194   ≀ cle 11195   βˆ’ cmin 11390  -cneg 11391   / cdiv 11817  β„•cn 12158  2c2 12213  β„•0cn0 12418  β„€cz 12504  β„€β‰₯cuz 12768  β„+crp 12920  (,)cioo 13270  [,)cico 13272  ...cfz 13430  ..^cfzo 13573  βŒŠcfl 13701  abscabs 15125   β‡π‘Ÿ crli 15373  π‘‚(1)co1 15374  β‰€π‘‚(1)clo1 15375  Ξ£csu 15576   βˆ₯ cdvds 16141  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 2704  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-inf2 9582  ax-cnex 11112  ax-resscn 11113  ax-1cn 11114  ax-icn 11115  ax-addcl 11116  ax-addrcl 11117  ax-mulcl 11118  ax-mulrcl 11119  ax-mulcom 11120  ax-addass 11121  ax-mulass 11122  ax-distr 11123  ax-i2m1 11124  ax-1ne0 11125  ax-1rid 11126  ax-rnegex 11127  ax-rrecex 11128  ax-cnre 11129  ax-pre-lttri 11130  ax-pre-lttrn 11131  ax-pre-ltadd 11132  ax-pre-mulgt0 11133  ax-pre-sup 11134  ax-addf 11135  ax-mulf 11136
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 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-tp 4592  df-op 4594  df-uni 4867  df-int 4909  df-iun 4957  df-iin 4958  df-disj 5072  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-se 5590  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-isom 6506  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-of 7618  df-om 7804  df-1st 7922  df-2nd 7923  df-supp 8094  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-rdg 8357  df-1o 8413  df-2o 8414  df-oadd 8417  df-er 8651  df-map 8770  df-pm 8771  df-ixp 8839  df-en 8887  df-dom 8888  df-sdom 8889  df-fin 8890  df-fsupp 9309  df-fi 9352  df-sup 9383  df-inf 9384  df-oi 9451  df-dju 9842  df-card 9880  df-pnf 11196  df-mnf 11197  df-xr 11198  df-ltxr 11199  df-le 11200  df-sub 11392  df-neg 11393  df-div 11818  df-nn 12159  df-2 12221  df-3 12222  df-4 12223  df-5 12224  df-6 12225  df-7 12226  df-8 12227  df-9 12228  df-n0 12419  df-xnn0 12491  df-z 12505  df-dec 12624  df-uz 12769  df-q 12879  df-rp 12921  df-xneg 13038  df-xadd 13039  df-xmul 13040  df-ioo 13274  df-ioc 13275  df-ico 13276  df-icc 13277  df-fz 13431  df-fzo 13574  df-fl 13703  df-mod 13781  df-seq 13913  df-exp 13974  df-fac 14180  df-bc 14209  df-hash 14237  df-shft 14958  df-cj 14990  df-re 14991  df-im 14992  df-sqrt 15126  df-abs 15127  df-limsup 15359  df-clim 15376  df-rlim 15377  df-o1 15378  df-lo1 15379  df-sum 15577  df-ef 15955  df-e 15956  df-sin 15957  df-cos 15958  df-tan 15959  df-pi 15960  df-dvds 16142  df-gcd 16380  df-prm 16553  df-pc 16714  df-struct 17024  df-sets 17041  df-slot 17059  df-ndx 17071  df-base 17089  df-ress 17118  df-plusg 17151  df-mulr 17152  df-starv 17153  df-sca 17154  df-vsca 17155  df-ip 17156  df-tset 17157  df-ple 17158  df-ds 17160  df-unif 17161  df-hom 17162  df-cco 17163  df-rest 17309  df-topn 17310  df-0g 17328  df-gsum 17329  df-topgen 17330  df-pt 17331  df-prds 17334  df-xrs 17389  df-qtop 17394  df-imas 17395  df-xps 17397  df-mre 17471  df-mrc 17472  df-acs 17474  df-mgm 18502  df-sgrp 18551  df-mnd 18562  df-submnd 18607  df-mulg 18878  df-cntz 19102  df-cmn 19569  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:  pntrlog2bndlem5  26945
  Copyright terms: Public domain W3C validator