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

Theorem pntrlog2bndlem4 27500
Description: Lemma for pntrlog2bnd 27504. 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 13378 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ ∈ (1(,)+∞) β†’ π‘₯ ∈ ℝ)
21adantl 481 . . . . . . . . . . . . . . . . . . 19 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ π‘₯ ∈ ℝ)
3 1rp 13002 . . . . . . . . . . . . . . . . . . . 20 1 ∈ ℝ+
43a1i 11 . . . . . . . . . . . . . . . . . . 19 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 1 ∈ ℝ+)
5 1red 11237 . . . . . . . . . . . . . . . . . . . 20 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 1 ∈ ℝ)
6 eliooord 13407 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ ∈ (1(,)+∞) β†’ (1 < π‘₯ ∧ π‘₯ < +∞))
76adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (1 < π‘₯ ∧ π‘₯ < +∞))
87simpld 494 . . . . . . . . . . . . . . . . . . . 20 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 1 < π‘₯)
95, 2, 8ltled 11384 . . . . . . . . . . . . . . . . . . 19 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 1 ≀ π‘₯)
102, 4, 9rpgecld 13079 . . . . . . . . . . . . . . . . . 18 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ π‘₯ ∈ ℝ+)
1110rprege0d 13047 . . . . . . . . . . . . . . . . . . . . 21 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘₯ ∈ ℝ ∧ 0 ≀ π‘₯))
12 flge0nn0 13809 . . . . . . . . . . . . . . . . . . . . 21 ((π‘₯ ∈ ℝ ∧ 0 ≀ π‘₯) β†’ (βŒŠβ€˜π‘₯) ∈ β„•0)
1311, 12syl 17 . . . . . . . . . . . . . . . . . . . 20 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (βŒŠβ€˜π‘₯) ∈ β„•0)
14 nn0p1nn 12533 . . . . . . . . . . . . . . . . . . . 20 ((βŒŠβ€˜π‘₯) ∈ β„•0 β†’ ((βŒŠβ€˜π‘₯) + 1) ∈ β„•)
1513, 14syl 17 . . . . . . . . . . . . . . . . . . 19 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((βŒŠβ€˜π‘₯) + 1) ∈ β„•)
1615nnrpd 13038 . . . . . . . . . . . . . . . . . 18 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((βŒŠβ€˜π‘₯) + 1) ∈ ℝ+)
1710, 16rpdivcld 13057 . . . . . . . . . . . . . . . . 17 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) ∈ ℝ+)
18 pntrlog2bnd.r . . . . . . . . . . . . . . . . . 18 𝑅 = (π‘Ž ∈ ℝ+ ↦ ((Οˆβ€˜π‘Ž) βˆ’ π‘Ž))
1918pntrval 27482 . . . . . . . . . . . . . . . . 17 ((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) ∈ ℝ+ β†’ (π‘…β€˜(π‘₯ / ((βŒŠβ€˜π‘₯) + 1))) = ((Οˆβ€˜(π‘₯ / ((βŒŠβ€˜π‘₯) + 1))) βˆ’ (π‘₯ / ((βŒŠβ€˜π‘₯) + 1))))
2017, 19syl 17 . . . . . . . . . . . . . . . 16 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘…β€˜(π‘₯ / ((βŒŠβ€˜π‘₯) + 1))) = ((Οˆβ€˜(π‘₯ / ((βŒŠβ€˜π‘₯) + 1))) βˆ’ (π‘₯ / ((βŒŠβ€˜π‘₯) + 1))))
212, 15nndivred 12288 . . . . . . . . . . . . . . . . . . 19 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) ∈ ℝ)
22 2re 12308 . . . . . . . . . . . . . . . . . . . 20 2 ∈ ℝ
2322a1i 11 . . . . . . . . . . . . . . . . . . 19 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 2 ∈ ℝ)
24 flltp1 13789 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ ∈ ℝ β†’ π‘₯ < ((βŒŠβ€˜π‘₯) + 1))
252, 24syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ π‘₯ < ((βŒŠβ€˜π‘₯) + 1))
2615nncnd 12250 . . . . . . . . . . . . . . . . . . . . . 22 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((βŒŠβ€˜π‘₯) + 1) ∈ β„‚)
2726mulridd 11253 . . . . . . . . . . . . . . . . . . . . 21 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((βŒŠβ€˜π‘₯) + 1) Β· 1) = ((βŒŠβ€˜π‘₯) + 1))
2825, 27breqtrrd 5170 . . . . . . . . . . . . . . . . . . . 20 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ π‘₯ < (((βŒŠβ€˜π‘₯) + 1) Β· 1))
292, 5, 16ltdivmuld 13091 . . . . . . . . . . . . . . . . . . . 20 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) < 1 ↔ π‘₯ < (((βŒŠβ€˜π‘₯) + 1) Β· 1)))
3028, 29mpbird 257 . . . . . . . . . . . . . . . . . . 19 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) < 1)
31 1lt2 12405 . . . . . . . . . . . . . . . . . . . 20 1 < 2
3231a1i 11 . . . . . . . . . . . . . . . . . . 19 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 1 < 2)
3321, 5, 23, 30, 32lttrd 11397 . . . . . . . . . . . . . . . . . 18 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) < 2)
34 chpeq0 27128 . . . . . . . . . . . . . . . . . . 19 ((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) ∈ ℝ β†’ ((Οˆβ€˜(π‘₯ / ((βŒŠβ€˜π‘₯) + 1))) = 0 ↔ (π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) < 2))
3521, 34syl 17 . . . . . . . . . . . . . . . . . 18 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((Οˆβ€˜(π‘₯ / ((βŒŠβ€˜π‘₯) + 1))) = 0 ↔ (π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) < 2))
3633, 35mpbird 257 . . . . . . . . . . . . . . . . 17 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (Οˆβ€˜(π‘₯ / ((βŒŠβ€˜π‘₯) + 1))) = 0)
3736oveq1d 7429 . . . . . . . . . . . . . . . 16 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((Οˆβ€˜(π‘₯ / ((βŒŠβ€˜π‘₯) + 1))) βˆ’ (π‘₯ / ((βŒŠβ€˜π‘₯) + 1))) = (0 βˆ’ (π‘₯ / ((βŒŠβ€˜π‘₯) + 1))))
3820, 37eqtrd 2767 . . . . . . . . . . . . . . 15 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘…β€˜(π‘₯ / ((βŒŠβ€˜π‘₯) + 1))) = (0 βˆ’ (π‘₯ / ((βŒŠβ€˜π‘₯) + 1))))
3938fveq2d 6895 . . . . . . . . . . . . . 14 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (absβ€˜(π‘…β€˜(π‘₯ / ((βŒŠβ€˜π‘₯) + 1)))) = (absβ€˜(0 βˆ’ (π‘₯ / ((βŒŠβ€˜π‘₯) + 1)))))
40 0red 11239 . . . . . . . . . . . . . . 15 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 0 ∈ ℝ)
4117rpge0d 13044 . . . . . . . . . . . . . . 15 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 0 ≀ (π‘₯ / ((βŒŠβ€˜π‘₯) + 1)))
4240, 21, 41abssuble0d 15403 . . . . . . . . . . . . . 14 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (absβ€˜(0 βˆ’ (π‘₯ / ((βŒŠβ€˜π‘₯) + 1)))) = ((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) βˆ’ 0))
4321recnd 11264 . . . . . . . . . . . . . . 15 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) ∈ β„‚)
4443subid1d 11582 . . . . . . . . . . . . . 14 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) βˆ’ 0) = (π‘₯ / ((βŒŠβ€˜π‘₯) + 1)))
4539, 42, 443eqtrd 2771 . . . . . . . . . . . . 13 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (absβ€˜(π‘…β€˜(π‘₯ / ((βŒŠβ€˜π‘₯) + 1)))) = (π‘₯ / ((βŒŠβ€˜π‘₯) + 1)))
4613nn0red 12555 . . . . . . . . . . . . . . . 16 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (βŒŠβ€˜π‘₯) ∈ ℝ)
47 pntsval.1 . . . . . . . . . . . . . . . . 17 𝑆 = (π‘Ž ∈ ℝ ↦ Σ𝑖 ∈ (1...(βŒŠβ€˜π‘Ž))((Ξ›β€˜π‘–) Β· ((logβ€˜π‘–) + (Οˆβ€˜(π‘Ž / 𝑖)))))
4847pntsval2 27496 . . . . . . . . . . . . . . . 16 ((βŒŠβ€˜π‘₯) ∈ ℝ β†’ (π‘†β€˜(βŒŠβ€˜π‘₯)) = Σ𝑛 ∈ (1...(βŒŠβ€˜(βŒŠβ€˜π‘₯)))(((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)) + Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š)))))
4946, 48syl 17 . . . . . . . . . . . . . . 15 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘†β€˜(βŒŠβ€˜π‘₯)) = Σ𝑛 ∈ (1...(βŒŠβ€˜(βŒŠβ€˜π‘₯)))(((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)) + Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š)))))
5013nn0cnd 12556 . . . . . . . . . . . . . . . . 17 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (βŒŠβ€˜π‘₯) ∈ β„‚)
51 1cnd 11231 . . . . . . . . . . . . . . . . 17 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 1 ∈ β„‚)
5250, 51pncand 11594 . . . . . . . . . . . . . . . 16 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((βŒŠβ€˜π‘₯) + 1) βˆ’ 1) = (βŒŠβ€˜π‘₯))
5352fveq2d 6895 . . . . . . . . . . . . . . 15 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘†β€˜(((βŒŠβ€˜π‘₯) + 1) βˆ’ 1)) = (π‘†β€˜(βŒŠβ€˜π‘₯)))
5447pntsval2 27496 . . . . . . . . . . . . . . . . 17 (π‘₯ ∈ ℝ β†’ (π‘†β€˜π‘₯) = Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)) + Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š)))))
552, 54syl 17 . . . . . . . . . . . . . . . 16 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘†β€˜π‘₯) = Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)) + Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š)))))
56 flidm 13798 . . . . . . . . . . . . . . . . . . 19 (π‘₯ ∈ ℝ β†’ (βŒŠβ€˜(βŒŠβ€˜π‘₯)) = (βŒŠβ€˜π‘₯))
572, 56syl 17 . . . . . . . . . . . . . . . . . 18 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (βŒŠβ€˜(βŒŠβ€˜π‘₯)) = (βŒŠβ€˜π‘₯))
5857oveq2d 7430 . . . . . . . . . . . . . . . . 17 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (1...(βŒŠβ€˜(βŒŠβ€˜π‘₯))) = (1...(βŒŠβ€˜π‘₯)))
5958sumeq1d 15671 . . . . . . . . . . . . . . . 16 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜(βŒŠβ€˜π‘₯)))(((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)) + Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š)))) = Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)) + Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š)))))
6055, 59eqtr4d 2770 . . . . . . . . . . . . . . 15 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘†β€˜π‘₯) = Σ𝑛 ∈ (1...(βŒŠβ€˜(βŒŠβ€˜π‘₯)))(((Ξ›β€˜π‘›) Β· (logβ€˜π‘›)) + Ξ£π‘š ∈ {𝑦 ∈ β„• ∣ 𝑦 βˆ₯ 𝑛} ((Ξ›β€˜π‘š) Β· (Ξ›β€˜(𝑛 / π‘š)))))
6149, 53, 603eqtr4d 2777 . . . . . . . . . . . . . 14 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘†β€˜(((βŒŠβ€˜π‘₯) + 1) βˆ’ 1)) = (π‘†β€˜π‘₯))
6252fveq2d 6895 . . . . . . . . . . . . . . 15 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘‡β€˜(((βŒŠβ€˜π‘₯) + 1) βˆ’ 1)) = (π‘‡β€˜(βŒŠβ€˜π‘₯)))
6362oveq2d 7430 . . . . . . . . . . . . . 14 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (2 Β· (π‘‡β€˜(((βŒŠβ€˜π‘₯) + 1) βˆ’ 1))) = (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))
6461, 63oveq12d 7432 . . . . . . . . . . . . 13 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((π‘†β€˜(((βŒŠβ€˜π‘₯) + 1) βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(((βŒŠβ€˜π‘₯) + 1) βˆ’ 1)))) = ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯)))))
6545, 64oveq12d 7432 . . . . . . . . . . . 12 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((absβ€˜(π‘…β€˜(π‘₯ / ((βŒŠβ€˜π‘₯) + 1)))) Β· ((π‘†β€˜(((βŒŠβ€˜π‘₯) + 1) βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(((βŒŠβ€˜π‘₯) + 1) βˆ’ 1))))) = ((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))))
662recnd 11264 . . . . . . . . . . . . . . . . . . 19 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ π‘₯ ∈ β„‚)
6766div1d 12004 . . . . . . . . . . . . . . . . . 18 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘₯ / 1) = π‘₯)
6867fveq2d 6895 . . . . . . . . . . . . . . . . 17 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘…β€˜(π‘₯ / 1)) = (π‘…β€˜π‘₯))
6918pntrf 27483 . . . . . . . . . . . . . . . . . . 19 𝑅:ℝ+βŸΆβ„
7069ffvelcdmi 7087 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ ℝ+ β†’ (π‘…β€˜π‘₯) ∈ ℝ)
7110, 70syl 17 . . . . . . . . . . . . . . . . 17 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘…β€˜π‘₯) ∈ ℝ)
7268, 71eqeltrd 2828 . . . . . . . . . . . . . . . 16 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘…β€˜(π‘₯ / 1)) ∈ ℝ)
7372recnd 11264 . . . . . . . . . . . . . . 15 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘…β€˜(π‘₯ / 1)) ∈ β„‚)
7473abscld 15407 . . . . . . . . . . . . . 14 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (absβ€˜(π‘…β€˜(π‘₯ / 1))) ∈ ℝ)
7574recnd 11264 . . . . . . . . . . . . 13 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (absβ€˜(π‘…β€˜(π‘₯ / 1))) ∈ β„‚)
7675mul01d 11435 . . . . . . . . . . . 12 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((absβ€˜(π‘…β€˜(π‘₯ / 1))) Β· 0) = 0)
7765, 76oveq12d 7432 . . . . . . . . . . 11 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((absβ€˜(π‘…β€˜(π‘₯ / ((βŒŠβ€˜π‘₯) + 1)))) Β· ((π‘†β€˜(((βŒŠβ€˜π‘₯) + 1) βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(((βŒŠβ€˜π‘₯) + 1) βˆ’ 1))))) βˆ’ ((absβ€˜(π‘…β€˜(π‘₯ / 1))) Β· 0)) = (((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))) βˆ’ 0))
7847pntsf 27493 . . . . . . . . . . . . . . . . 17 𝑆:β„βŸΆβ„
7978ffvelcdmi 7087 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ ℝ β†’ (π‘†β€˜π‘₯) ∈ ℝ)
802, 79syl 17 . . . . . . . . . . . . . . 15 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘†β€˜π‘₯) ∈ ℝ)
81 pntrlog2bnd.t . . . . . . . . . . . . . . . . . . 19 𝑇 = (π‘Ž ∈ ℝ ↦ if(π‘Ž ∈ ℝ+, (π‘Ž Β· (logβ€˜π‘Ž)), 0))
82 relogcl 26496 . . . . . . . . . . . . . . . . . . . . 21 (π‘Ž ∈ ℝ+ β†’ (logβ€˜π‘Ž) ∈ ℝ)
83 remulcl 11215 . . . . . . . . . . . . . . . . . . . . 21 ((π‘Ž ∈ ℝ ∧ (logβ€˜π‘Ž) ∈ ℝ) β†’ (π‘Ž Β· (logβ€˜π‘Ž)) ∈ ℝ)
8482, 83sylan2 592 . . . . . . . . . . . . . . . . . . . 20 ((π‘Ž ∈ ℝ ∧ π‘Ž ∈ ℝ+) β†’ (π‘Ž Β· (logβ€˜π‘Ž)) ∈ ℝ)
85 0red 11239 . . . . . . . . . . . . . . . . . . . 20 ((π‘Ž ∈ ℝ ∧ Β¬ π‘Ž ∈ ℝ+) β†’ 0 ∈ ℝ)
8684, 85ifclda 4559 . . . . . . . . . . . . . . . . . . 19 (π‘Ž ∈ ℝ β†’ if(π‘Ž ∈ ℝ+, (π‘Ž Β· (logβ€˜π‘Ž)), 0) ∈ ℝ)
8781, 86fmpti 7116 . . . . . . . . . . . . . . . . . 18 𝑇:β„βŸΆβ„
8887ffvelcdmi 7087 . . . . . . . . . . . . . . . . 17 ((βŒŠβ€˜π‘₯) ∈ ℝ β†’ (π‘‡β€˜(βŒŠβ€˜π‘₯)) ∈ ℝ)
8946, 88syl 17 . . . . . . . . . . . . . . . 16 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘‡β€˜(βŒŠβ€˜π‘₯)) ∈ ℝ)
9023, 89remulcld 11266 . . . . . . . . . . . . . . 15 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))) ∈ ℝ)
9180, 90resubcld 11664 . . . . . . . . . . . . . 14 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯)))) ∈ ℝ)
9221, 91remulcld 11266 . . . . . . . . . . . . 13 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))) ∈ ℝ)
9392recnd 11264 . . . . . . . . . . . 12 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))) ∈ β„‚)
9493subid1d 11582 . . . . . . . . . . 11 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))) βˆ’ 0) = ((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))))
9577, 94eqtrd 2767 . . . . . . . . . 10 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((absβ€˜(π‘…β€˜(π‘₯ / ((βŒŠβ€˜π‘₯) + 1)))) Β· ((π‘†β€˜(((βŒŠβ€˜π‘₯) + 1) βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(((βŒŠβ€˜π‘₯) + 1) βˆ’ 1))))) βˆ’ ((absβ€˜(π‘…β€˜(π‘₯ / 1))) Β· 0)) = ((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))))
962flcld 13787 . . . . . . . . . . . . . 14 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (βŒŠβ€˜π‘₯) ∈ β„€)
97 fzval3 13725 . . . . . . . . . . . . . 14 ((βŒŠβ€˜π‘₯) ∈ β„€ β†’ (1...(βŒŠβ€˜π‘₯)) = (1..^((βŒŠβ€˜π‘₯) + 1)))
9896, 97syl 17 . . . . . . . . . . . . 13 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (1...(βŒŠβ€˜π‘₯)) = (1..^((βŒŠβ€˜π‘₯) + 1)))
9998eqcomd 2733 . . . . . . . . . . . 12 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (1..^((βŒŠβ€˜π‘₯) + 1)) = (1...(βŒŠβ€˜π‘₯)))
10010adantr 480 . . . . . . . . . . . . . . . . . . . . 21 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ π‘₯ ∈ ℝ+)
101 elfznn 13554 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ (1...(βŒŠβ€˜π‘₯)) β†’ 𝑛 ∈ β„•)
102101adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ 𝑛 ∈ β„•)
103102nnrpd 13038 . . . . . . . . . . . . . . . . . . . . 21 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ 𝑛 ∈ ℝ+)
104100, 103rpdivcld 13057 . . . . . . . . . . . . . . . . . . . 20 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (π‘₯ / 𝑛) ∈ ℝ+)
10569ffvelcdmi 7087 . . . . . . . . . . . . . . . . . . . 20 ((π‘₯ / 𝑛) ∈ ℝ+ β†’ (π‘…β€˜(π‘₯ / 𝑛)) ∈ ℝ)
106104, 105syl 17 . . . . . . . . . . . . . . . . . . 19 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (π‘…β€˜(π‘₯ / 𝑛)) ∈ ℝ)
107106recnd 11264 . . . . . . . . . . . . . . . . . 18 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (π‘…β€˜(π‘₯ / 𝑛)) ∈ β„‚)
108107abscld 15407 . . . . . . . . . . . . . . . . 17 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) ∈ ℝ)
109108recnd 11264 . . . . . . . . . . . . . . . 16 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) ∈ β„‚)
1103a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ 1 ∈ ℝ+)
111103, 110rpaddcld 13055 . . . . . . . . . . . . . . . . . . . . 21 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (𝑛 + 1) ∈ ℝ+)
112100, 111rpdivcld 13057 . . . . . . . . . . . . . . . . . . . 20 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (π‘₯ / (𝑛 + 1)) ∈ ℝ+)
11369ffvelcdmi 7087 . . . . . . . . . . . . . . . . . . . 20 ((π‘₯ / (𝑛 + 1)) ∈ ℝ+ β†’ (π‘…β€˜(π‘₯ / (𝑛 + 1))) ∈ ℝ)
114112, 113syl 17 . . . . . . . . . . . . . . . . . . 19 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (π‘…β€˜(π‘₯ / (𝑛 + 1))) ∈ ℝ)
115114recnd 11264 . . . . . . . . . . . . . . . . . 18 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (π‘…β€˜(π‘₯ / (𝑛 + 1))) ∈ β„‚)
116115abscld 15407 . . . . . . . . . . . . . . . . 17 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1)))) ∈ ℝ)
117116recnd 11264 . . . . . . . . . . . . . . . 16 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1)))) ∈ β„‚)
118109, 117negsubdi2d 11609 . . . . . . . . . . . . . . 15 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ -((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) = ((absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1)))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / 𝑛)))))
119118eqcomd 2733 . . . . . . . . . . . . . 14 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1)))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / 𝑛)))) = -((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))))
120102nncnd 12250 . . . . . . . . . . . . . . . . 17 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ 𝑛 ∈ β„‚)
121 1cnd 11231 . . . . . . . . . . . . . . . . 17 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ 1 ∈ β„‚)
122120, 121pncand 11594 . . . . . . . . . . . . . . . 16 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((𝑛 + 1) βˆ’ 1) = 𝑛)
123122fveq2d 6895 . . . . . . . . . . . . . . 15 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (π‘†β€˜((𝑛 + 1) βˆ’ 1)) = (π‘†β€˜π‘›))
124122fveq2d 6895 . . . . . . . . . . . . . . . . 17 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (π‘‡β€˜((𝑛 + 1) βˆ’ 1)) = (π‘‡β€˜π‘›))
125 rpre 13006 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℝ+ β†’ 𝑛 ∈ ℝ)
126 eleq1 2816 . . . . . . . . . . . . . . . . . . . . . 22 (π‘Ž = 𝑛 β†’ (π‘Ž ∈ ℝ+ ↔ 𝑛 ∈ ℝ+))
127 id 22 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘Ž = 𝑛 β†’ π‘Ž = 𝑛)
128 fveq2 6891 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘Ž = 𝑛 β†’ (logβ€˜π‘Ž) = (logβ€˜π‘›))
129127, 128oveq12d 7432 . . . . . . . . . . . . . . . . . . . . . 22 (π‘Ž = 𝑛 β†’ (π‘Ž Β· (logβ€˜π‘Ž)) = (𝑛 Β· (logβ€˜π‘›)))
130126, 129ifbieq1d 4548 . . . . . . . . . . . . . . . . . . . . 21 (π‘Ž = 𝑛 β†’ if(π‘Ž ∈ ℝ+, (π‘Ž Β· (logβ€˜π‘Ž)), 0) = if(𝑛 ∈ ℝ+, (𝑛 Β· (logβ€˜π‘›)), 0))
131 ovex 7447 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 Β· (logβ€˜π‘›)) ∈ V
132 c0ex 11230 . . . . . . . . . . . . . . . . . . . . . 22 0 ∈ V
133131, 132ifex 4574 . . . . . . . . . . . . . . . . . . . . 21 if(𝑛 ∈ ℝ+, (𝑛 Β· (logβ€˜π‘›)), 0) ∈ V
134130, 81, 133fvmpt 6999 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℝ β†’ (π‘‡β€˜π‘›) = if(𝑛 ∈ ℝ+, (𝑛 Β· (logβ€˜π‘›)), 0))
135125, 134syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℝ+ β†’ (π‘‡β€˜π‘›) = if(𝑛 ∈ ℝ+, (𝑛 Β· (logβ€˜π‘›)), 0))
136 iftrue 4530 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℝ+ β†’ if(𝑛 ∈ ℝ+, (𝑛 Β· (logβ€˜π‘›)), 0) = (𝑛 Β· (logβ€˜π‘›)))
137135, 136eqtrd 2767 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℝ+ β†’ (π‘‡β€˜π‘›) = (𝑛 Β· (logβ€˜π‘›)))
138103, 137syl 17 . . . . . . . . . . . . . . . . 17 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (π‘‡β€˜π‘›) = (𝑛 Β· (logβ€˜π‘›)))
139124, 138eqtrd 2767 . . . . . . . . . . . . . . . 16 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (π‘‡β€˜((𝑛 + 1) βˆ’ 1)) = (𝑛 Β· (logβ€˜π‘›)))
140139oveq2d 7430 . . . . . . . . . . . . . . 15 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (2 Β· (π‘‡β€˜((𝑛 + 1) βˆ’ 1))) = (2 Β· (𝑛 Β· (logβ€˜π‘›))))
141123, 140oveq12d 7432 . . . . . . . . . . . . . 14 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((π‘†β€˜((𝑛 + 1) βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜((𝑛 + 1) βˆ’ 1)))) = ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›)))))
142119, 141oveq12d 7432 . . . . . . . . . . . . 13 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (((absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1)))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / 𝑛)))) Β· ((π‘†β€˜((𝑛 + 1) βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜((𝑛 + 1) βˆ’ 1))))) = (-((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›))))))
143108, 116resubcld 11664 . . . . . . . . . . . . . . 15 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) ∈ ℝ)
144143recnd 11264 . . . . . . . . . . . . . 14 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) ∈ β„‚)
145102nnred 12249 . . . . . . . . . . . . . . . . 17 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ 𝑛 ∈ ℝ)
14678ffvelcdmi 7087 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℝ β†’ (π‘†β€˜π‘›) ∈ ℝ)
147145, 146syl 17 . . . . . . . . . . . . . . . 16 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (π‘†β€˜π‘›) ∈ ℝ)
14822a1i 11 . . . . . . . . . . . . . . . . 17 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ 2 ∈ ℝ)
149103relogcld 26544 . . . . . . . . . . . . . . . . . 18 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (logβ€˜π‘›) ∈ ℝ)
150145, 149remulcld 11266 . . . . . . . . . . . . . . . . 17 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (𝑛 Β· (logβ€˜π‘›)) ∈ ℝ)
151148, 150remulcld 11266 . . . . . . . . . . . . . . . 16 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (2 Β· (𝑛 Β· (logβ€˜π‘›))) ∈ ℝ)
152147, 151resubcld 11664 . . . . . . . . . . . . . . 15 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›)))) ∈ ℝ)
153152recnd 11264 . . . . . . . . . . . . . 14 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›)))) ∈ β„‚)
154144, 153mulneg1d 11689 . . . . . . . . . . . . 13 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (-((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›))))) = -(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›))))))
155142, 154eqtrd 2767 . . . . . . . . . . . 12 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (((absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1)))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / 𝑛)))) Β· ((π‘†β€˜((𝑛 + 1) βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜((𝑛 + 1) βˆ’ 1))))) = -(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›))))))
15699, 155sumeq12rdv 15677 . . . . . . . . . . 11 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Σ𝑛 ∈ (1..^((βŒŠβ€˜π‘₯) + 1))(((absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1)))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / 𝑛)))) Β· ((π‘†β€˜((𝑛 + 1) βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜((𝑛 + 1) βˆ’ 1))))) = Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))-(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›))))))
157 fzfid 13962 . . . . . . . . . . . 12 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (1...(βŒŠβ€˜π‘₯)) ∈ Fin)
158143, 152remulcld 11266 . . . . . . . . . . . . 13 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›))))) ∈ ℝ)
159158recnd 11264 . . . . . . . . . . . 12 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›))))) ∈ β„‚)
160157, 159fsumneg 15757 . . . . . . . . . . 11 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))-(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›))))) = -Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›))))))
161156, 160eqtrd 2767 . . . . . . . . . 10 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Σ𝑛 ∈ (1..^((βŒŠβ€˜π‘₯) + 1))(((absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1)))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / 𝑛)))) Β· ((π‘†β€˜((𝑛 + 1) βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜((𝑛 + 1) βˆ’ 1))))) = -Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›))))))
16295, 161oveq12d 7432 . . . . . . . . 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 7422 . . . . . . . . . . . . . 14 (π‘š = 𝑛 β†’ (π‘₯ / π‘š) = (π‘₯ / 𝑛))
164163fveq2d 6895 . . . . . . . . . . . . 13 (π‘š = 𝑛 β†’ (π‘…β€˜(π‘₯ / π‘š)) = (π‘…β€˜(π‘₯ / 𝑛)))
165164fveq2d 6895 . . . . . . . . . . . 12 (π‘š = 𝑛 β†’ (absβ€˜(π‘…β€˜(π‘₯ / π‘š))) = (absβ€˜(π‘…β€˜(π‘₯ / 𝑛))))
166 fvoveq1 7437 . . . . . . . . . . . . 13 (π‘š = 𝑛 β†’ (π‘†β€˜(π‘š βˆ’ 1)) = (π‘†β€˜(𝑛 βˆ’ 1)))
167 fvoveq1 7437 . . . . . . . . . . . . . 14 (π‘š = 𝑛 β†’ (π‘‡β€˜(π‘š βˆ’ 1)) = (π‘‡β€˜(𝑛 βˆ’ 1)))
168167oveq2d 7430 . . . . . . . . . . . . 13 (π‘š = 𝑛 β†’ (2 Β· (π‘‡β€˜(π‘š βˆ’ 1))) = (2 Β· (π‘‡β€˜(𝑛 βˆ’ 1))))
169166, 168oveq12d 7432 . . . . . . . . . . . 12 (π‘š = 𝑛 β†’ ((π‘†β€˜(π‘š βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(π‘š βˆ’ 1)))) = ((π‘†β€˜(𝑛 βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(𝑛 βˆ’ 1)))))
170165, 169jca 511 . . . . . . . . . . 11 (π‘š = 𝑛 β†’ ((absβ€˜(π‘…β€˜(π‘₯ / π‘š))) = (absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) ∧ ((π‘†β€˜(π‘š βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(π‘š βˆ’ 1)))) = ((π‘†β€˜(𝑛 βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(𝑛 βˆ’ 1))))))
171 oveq2 7422 . . . . . . . . . . . . . 14 (π‘š = (𝑛 + 1) β†’ (π‘₯ / π‘š) = (π‘₯ / (𝑛 + 1)))
172171fveq2d 6895 . . . . . . . . . . . . 13 (π‘š = (𝑛 + 1) β†’ (π‘…β€˜(π‘₯ / π‘š)) = (π‘…β€˜(π‘₯ / (𝑛 + 1))))
173172fveq2d 6895 . . . . . . . . . . . 12 (π‘š = (𝑛 + 1) β†’ (absβ€˜(π‘…β€˜(π‘₯ / π‘š))) = (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1)))))
174 fvoveq1 7437 . . . . . . . . . . . . 13 (π‘š = (𝑛 + 1) β†’ (π‘†β€˜(π‘š βˆ’ 1)) = (π‘†β€˜((𝑛 + 1) βˆ’ 1)))
175 fvoveq1 7437 . . . . . . . . . . . . . 14 (π‘š = (𝑛 + 1) β†’ (π‘‡β€˜(π‘š βˆ’ 1)) = (π‘‡β€˜((𝑛 + 1) βˆ’ 1)))
176175oveq2d 7430 . . . . . . . . . . . . 13 (π‘š = (𝑛 + 1) β†’ (2 Β· (π‘‡β€˜(π‘š βˆ’ 1))) = (2 Β· (π‘‡β€˜((𝑛 + 1) βˆ’ 1))))
177174, 176oveq12d 7432 . . . . . . . . . . . 12 (π‘š = (𝑛 + 1) β†’ ((π‘†β€˜(π‘š βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(π‘š βˆ’ 1)))) = ((π‘†β€˜((𝑛 + 1) βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜((𝑛 + 1) βˆ’ 1)))))
178173, 177jca 511 . . . . . . . . . . 11 (π‘š = (𝑛 + 1) β†’ ((absβ€˜(π‘…β€˜(π‘₯ / π‘š))) = (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1)))) ∧ ((π‘†β€˜(π‘š βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(π‘š βˆ’ 1)))) = ((π‘†β€˜((𝑛 + 1) βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜((𝑛 + 1) βˆ’ 1))))))
179 oveq2 7422 . . . . . . . . . . . . . 14 (π‘š = 1 β†’ (π‘₯ / π‘š) = (π‘₯ / 1))
180179fveq2d 6895 . . . . . . . . . . . . 13 (π‘š = 1 β†’ (π‘…β€˜(π‘₯ / π‘š)) = (π‘…β€˜(π‘₯ / 1)))
181180fveq2d 6895 . . . . . . . . . . . 12 (π‘š = 1 β†’ (absβ€˜(π‘…β€˜(π‘₯ / π‘š))) = (absβ€˜(π‘…β€˜(π‘₯ / 1))))
182 oveq1 7421 . . . . . . . . . . . . . . . . 17 (π‘š = 1 β†’ (π‘š βˆ’ 1) = (1 βˆ’ 1))
183 1m1e0 12306 . . . . . . . . . . . . . . . . 17 (1 βˆ’ 1) = 0
184182, 183eqtrdi 2783 . . . . . . . . . . . . . . . 16 (π‘š = 1 β†’ (π‘š βˆ’ 1) = 0)
185184fveq2d 6895 . . . . . . . . . . . . . . 15 (π‘š = 1 β†’ (π‘†β€˜(π‘š βˆ’ 1)) = (π‘†β€˜0))
186 0re 11238 . . . . . . . . . . . . . . . 16 0 ∈ ℝ
187 fveq2 6891 . . . . . . . . . . . . . . . . . . . . . 22 (π‘Ž = 0 β†’ (βŒŠβ€˜π‘Ž) = (βŒŠβ€˜0))
188 0z 12591 . . . . . . . . . . . . . . . . . . . . . . 23 0 ∈ β„€
189 flid 13797 . . . . . . . . . . . . . . . . . . . . . . 23 (0 ∈ β„€ β†’ (βŒŠβ€˜0) = 0)
190188, 189ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 (βŒŠβ€˜0) = 0
191187, 190eqtrdi 2783 . . . . . . . . . . . . . . . . . . . . 21 (π‘Ž = 0 β†’ (βŒŠβ€˜π‘Ž) = 0)
192191oveq2d 7430 . . . . . . . . . . . . . . . . . . . 20 (π‘Ž = 0 β†’ (1...(βŒŠβ€˜π‘Ž)) = (1...0))
193 fz10 13546 . . . . . . . . . . . . . . . . . . . 20 (1...0) = βˆ…
194192, 193eqtrdi 2783 . . . . . . . . . . . . . . . . . . 19 (π‘Ž = 0 β†’ (1...(βŒŠβ€˜π‘Ž)) = βˆ…)
195194sumeq1d 15671 . . . . . . . . . . . . . . . . . 18 (π‘Ž = 0 β†’ Σ𝑖 ∈ (1...(βŒŠβ€˜π‘Ž))((Ξ›β€˜π‘–) Β· ((logβ€˜π‘–) + (Οˆβ€˜(π‘Ž / 𝑖)))) = Σ𝑖 ∈ βˆ… ((Ξ›β€˜π‘–) Β· ((logβ€˜π‘–) + (Οˆβ€˜(π‘Ž / 𝑖)))))
196 sum0 15691 . . . . . . . . . . . . . . . . . 18 Σ𝑖 ∈ βˆ… ((Ξ›β€˜π‘–) Β· ((logβ€˜π‘–) + (Οˆβ€˜(π‘Ž / 𝑖)))) = 0
197195, 196eqtrdi 2783 . . . . . . . . . . . . . . . . 17 (π‘Ž = 0 β†’ Σ𝑖 ∈ (1...(βŒŠβ€˜π‘Ž))((Ξ›β€˜π‘–) Β· ((logβ€˜π‘–) + (Οˆβ€˜(π‘Ž / 𝑖)))) = 0)
198197, 47, 132fvmpt 6999 . . . . . . . . . . . . . . . 16 (0 ∈ ℝ β†’ (π‘†β€˜0) = 0)
199186, 198ax-mp 5 . . . . . . . . . . . . . . 15 (π‘†β€˜0) = 0
200185, 199eqtrdi 2783 . . . . . . . . . . . . . 14 (π‘š = 1 β†’ (π‘†β€˜(π‘š βˆ’ 1)) = 0)
201184fveq2d 6895 . . . . . . . . . . . . . . . . 17 (π‘š = 1 β†’ (π‘‡β€˜(π‘š βˆ’ 1)) = (π‘‡β€˜0))
202 rpne0 13014 . . . . . . . . . . . . . . . . . . . . 21 (π‘Ž ∈ ℝ+ β†’ π‘Ž β‰  0)
203202necon2bi 2966 . . . . . . . . . . . . . . . . . . . 20 (π‘Ž = 0 β†’ Β¬ π‘Ž ∈ ℝ+)
204203iffalsed 4535 . . . . . . . . . . . . . . . . . . 19 (π‘Ž = 0 β†’ if(π‘Ž ∈ ℝ+, (π‘Ž Β· (logβ€˜π‘Ž)), 0) = 0)
205204, 81, 132fvmpt 6999 . . . . . . . . . . . . . . . . . 18 (0 ∈ ℝ β†’ (π‘‡β€˜0) = 0)
206186, 205ax-mp 5 . . . . . . . . . . . . . . . . 17 (π‘‡β€˜0) = 0
207201, 206eqtrdi 2783 . . . . . . . . . . . . . . . 16 (π‘š = 1 β†’ (π‘‡β€˜(π‘š βˆ’ 1)) = 0)
208207oveq2d 7430 . . . . . . . . . . . . . . 15 (π‘š = 1 β†’ (2 Β· (π‘‡β€˜(π‘š βˆ’ 1))) = (2 Β· 0))
209 2t0e0 12403 . . . . . . . . . . . . . . 15 (2 Β· 0) = 0
210208, 209eqtrdi 2783 . . . . . . . . . . . . . 14 (π‘š = 1 β†’ (2 Β· (π‘‡β€˜(π‘š βˆ’ 1))) = 0)
211200, 210oveq12d 7432 . . . . . . . . . . . . 13 (π‘š = 1 β†’ ((π‘†β€˜(π‘š βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(π‘š βˆ’ 1)))) = (0 βˆ’ 0))
212 0m0e0 12354 . . . . . . . . . . . . 13 (0 βˆ’ 0) = 0
213211, 212eqtrdi 2783 . . . . . . . . . . . 12 (π‘š = 1 β†’ ((π‘†β€˜(π‘š βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(π‘š βˆ’ 1)))) = 0)
214181, 213jca 511 . . . . . . . . . . 11 (π‘š = 1 β†’ ((absβ€˜(π‘…β€˜(π‘₯ / π‘š))) = (absβ€˜(π‘…β€˜(π‘₯ / 1))) ∧ ((π‘†β€˜(π‘š βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(π‘š βˆ’ 1)))) = 0))
215 oveq2 7422 . . . . . . . . . . . . . 14 (π‘š = ((βŒŠβ€˜π‘₯) + 1) β†’ (π‘₯ / π‘š) = (π‘₯ / ((βŒŠβ€˜π‘₯) + 1)))
216215fveq2d 6895 . . . . . . . . . . . . 13 (π‘š = ((βŒŠβ€˜π‘₯) + 1) β†’ (π‘…β€˜(π‘₯ / π‘š)) = (π‘…β€˜(π‘₯ / ((βŒŠβ€˜π‘₯) + 1))))
217216fveq2d 6895 . . . . . . . . . . . 12 (π‘š = ((βŒŠβ€˜π‘₯) + 1) β†’ (absβ€˜(π‘…β€˜(π‘₯ / π‘š))) = (absβ€˜(π‘…β€˜(π‘₯ / ((βŒŠβ€˜π‘₯) + 1)))))
218 fvoveq1 7437 . . . . . . . . . . . . 13 (π‘š = ((βŒŠβ€˜π‘₯) + 1) β†’ (π‘†β€˜(π‘š βˆ’ 1)) = (π‘†β€˜(((βŒŠβ€˜π‘₯) + 1) βˆ’ 1)))
219 fvoveq1 7437 . . . . . . . . . . . . . 14 (π‘š = ((βŒŠβ€˜π‘₯) + 1) β†’ (π‘‡β€˜(π‘š βˆ’ 1)) = (π‘‡β€˜(((βŒŠβ€˜π‘₯) + 1) βˆ’ 1)))
220219oveq2d 7430 . . . . . . . . . . . . 13 (π‘š = ((βŒŠβ€˜π‘₯) + 1) β†’ (2 Β· (π‘‡β€˜(π‘š βˆ’ 1))) = (2 Β· (π‘‡β€˜(((βŒŠβ€˜π‘₯) + 1) βˆ’ 1))))
221218, 220oveq12d 7432 . . . . . . . . . . . 12 (π‘š = ((βŒŠβ€˜π‘₯) + 1) β†’ ((π‘†β€˜(π‘š βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(π‘š βˆ’ 1)))) = ((π‘†β€˜(((βŒŠβ€˜π‘₯) + 1) βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(((βŒŠβ€˜π‘₯) + 1) βˆ’ 1)))))
222217, 221jca 511 . . . . . . . . . . 11 (π‘š = ((βŒŠβ€˜π‘₯) + 1) β†’ ((absβ€˜(π‘…β€˜(π‘₯ / π‘š))) = (absβ€˜(π‘…β€˜(π‘₯ / ((βŒŠβ€˜π‘₯) + 1)))) ∧ ((π‘†β€˜(π‘š βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(π‘š βˆ’ 1)))) = ((π‘†β€˜(((βŒŠβ€˜π‘₯) + 1) βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(((βŒŠβ€˜π‘₯) + 1) βˆ’ 1))))))
223 nnuz 12887 . . . . . . . . . . . 12 β„• = (β„€β‰₯β€˜1)
22415, 223eleqtrdi 2838 . . . . . . . . . . 11 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((βŒŠβ€˜π‘₯) + 1) ∈ (β„€β‰₯β€˜1))
22510adantr 480 . . . . . . . . . . . . . . . 16 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...((βŒŠβ€˜π‘₯) + 1))) β†’ π‘₯ ∈ ℝ+)
226 elfznn 13554 . . . . . . . . . . . . . . . . . 18 (π‘š ∈ (1...((βŒŠβ€˜π‘₯) + 1)) β†’ π‘š ∈ β„•)
227226adantl 481 . . . . . . . . . . . . . . . . 17 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...((βŒŠβ€˜π‘₯) + 1))) β†’ π‘š ∈ β„•)
228227nnrpd 13038 . . . . . . . . . . . . . . . 16 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...((βŒŠβ€˜π‘₯) + 1))) β†’ π‘š ∈ ℝ+)
229225, 228rpdivcld 13057 . . . . . . . . . . . . . . 15 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...((βŒŠβ€˜π‘₯) + 1))) β†’ (π‘₯ / π‘š) ∈ ℝ+)
23069ffvelcdmi 7087 . . . . . . . . . . . . . . 15 ((π‘₯ / π‘š) ∈ ℝ+ β†’ (π‘…β€˜(π‘₯ / π‘š)) ∈ ℝ)
231229, 230syl 17 . . . . . . . . . . . . . 14 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...((βŒŠβ€˜π‘₯) + 1))) β†’ (π‘…β€˜(π‘₯ / π‘š)) ∈ ℝ)
232231recnd 11264 . . . . . . . . . . . . 13 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...((βŒŠβ€˜π‘₯) + 1))) β†’ (π‘…β€˜(π‘₯ / π‘š)) ∈ β„‚)
233232abscld 15407 . . . . . . . . . . . 12 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...((βŒŠβ€˜π‘₯) + 1))) β†’ (absβ€˜(π‘…β€˜(π‘₯ / π‘š))) ∈ ℝ)
234233recnd 11264 . . . . . . . . . . 11 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...((βŒŠβ€˜π‘₯) + 1))) β†’ (absβ€˜(π‘…β€˜(π‘₯ / π‘š))) ∈ β„‚)
235227nnred 12249 . . . . . . . . . . . . . . 15 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...((βŒŠβ€˜π‘₯) + 1))) β†’ π‘š ∈ ℝ)
236 1red 11237 . . . . . . . . . . . . . . 15 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...((βŒŠβ€˜π‘₯) + 1))) β†’ 1 ∈ ℝ)
237235, 236resubcld 11664 . . . . . . . . . . . . . 14 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...((βŒŠβ€˜π‘₯) + 1))) β†’ (π‘š βˆ’ 1) ∈ ℝ)
23878ffvelcdmi 7087 . . . . . . . . . . . . . 14 ((π‘š βˆ’ 1) ∈ ℝ β†’ (π‘†β€˜(π‘š βˆ’ 1)) ∈ ℝ)
239237, 238syl 17 . . . . . . . . . . . . 13 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...((βŒŠβ€˜π‘₯) + 1))) β†’ (π‘†β€˜(π‘š βˆ’ 1)) ∈ ℝ)
24022a1i 11 . . . . . . . . . . . . . 14 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...((βŒŠβ€˜π‘₯) + 1))) β†’ 2 ∈ ℝ)
24187ffvelcdmi 7087 . . . . . . . . . . . . . . 15 ((π‘š βˆ’ 1) ∈ ℝ β†’ (π‘‡β€˜(π‘š βˆ’ 1)) ∈ ℝ)
242237, 241syl 17 . . . . . . . . . . . . . 14 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...((βŒŠβ€˜π‘₯) + 1))) β†’ (π‘‡β€˜(π‘š βˆ’ 1)) ∈ ℝ)
243240, 242remulcld 11266 . . . . . . . . . . . . 13 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...((βŒŠβ€˜π‘₯) + 1))) β†’ (2 Β· (π‘‡β€˜(π‘š βˆ’ 1))) ∈ ℝ)
244239, 243resubcld 11664 . . . . . . . . . . . 12 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...((βŒŠβ€˜π‘₯) + 1))) β†’ ((π‘†β€˜(π‘š βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(π‘š βˆ’ 1)))) ∈ ℝ)
245244recnd 11264 . . . . . . . . . . 11 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ π‘š ∈ (1...((βŒŠβ€˜π‘₯) + 1))) β†’ ((π‘†β€˜(π‘š βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(π‘š βˆ’ 1)))) ∈ β„‚)
246170, 178, 214, 222, 224, 234, 245fsumparts 15776 . . . . . . . . . 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 11264 . . . . . . . . . . . . . 14 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (π‘†β€˜π‘›) ∈ β„‚)
24887ffvelcdmi 7087 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℝ β†’ (π‘‡β€˜π‘›) ∈ ℝ)
249145, 248syl 17 . . . . . . . . . . . . . . . 16 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (π‘‡β€˜π‘›) ∈ ℝ)
250148, 249remulcld 11266 . . . . . . . . . . . . . . 15 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (2 Β· (π‘‡β€˜π‘›)) ∈ ℝ)
251250recnd 11264 . . . . . . . . . . . . . 14 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (2 Β· (π‘‡β€˜π‘›)) ∈ β„‚)
252 1red 11237 . . . . . . . . . . . . . . . . 17 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ 1 ∈ ℝ)
253145, 252resubcld 11664 . . . . . . . . . . . . . . . 16 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (𝑛 βˆ’ 1) ∈ ℝ)
25478ffvelcdmi 7087 . . . . . . . . . . . . . . . 16 ((𝑛 βˆ’ 1) ∈ ℝ β†’ (π‘†β€˜(𝑛 βˆ’ 1)) ∈ ℝ)
255253, 254syl 17 . . . . . . . . . . . . . . 15 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (π‘†β€˜(𝑛 βˆ’ 1)) ∈ ℝ)
256255recnd 11264 . . . . . . . . . . . . . 14 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (π‘†β€˜(𝑛 βˆ’ 1)) ∈ β„‚)
25787ffvelcdmi 7087 . . . . . . . . . . . . . . . . 17 ((𝑛 βˆ’ 1) ∈ ℝ β†’ (π‘‡β€˜(𝑛 βˆ’ 1)) ∈ ℝ)
258253, 257syl 17 . . . . . . . . . . . . . . . 16 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (π‘‡β€˜(𝑛 βˆ’ 1)) ∈ ℝ)
259148, 258remulcld 11266 . . . . . . . . . . . . . . 15 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (2 Β· (π‘‡β€˜(𝑛 βˆ’ 1))) ∈ ℝ)
260259recnd 11264 . . . . . . . . . . . . . 14 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (2 Β· (π‘‡β€˜(𝑛 βˆ’ 1))) ∈ β„‚)
261247, 251, 256, 260sub4d 11642 . . . . . . . . . . . . 13 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (((π‘†β€˜π‘›) βˆ’ (2 Β· (π‘‡β€˜π‘›))) βˆ’ ((π‘†β€˜(𝑛 βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(𝑛 βˆ’ 1))))) = (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ ((2 Β· (π‘‡β€˜π‘›)) βˆ’ (2 Β· (π‘‡β€˜(𝑛 βˆ’ 1))))))
262124oveq2d 7430 . . . . . . . . . . . . . . 15 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (2 Β· (π‘‡β€˜((𝑛 + 1) βˆ’ 1))) = (2 Β· (π‘‡β€˜π‘›)))
263123, 262oveq12d 7432 . . . . . . . . . . . . . 14 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((π‘†β€˜((𝑛 + 1) βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜((𝑛 + 1) βˆ’ 1)))) = ((π‘†β€˜π‘›) βˆ’ (2 Β· (π‘‡β€˜π‘›))))
264263oveq1d 7429 . . . . . . . . . . . . 13 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (((π‘†β€˜((𝑛 + 1) βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜((𝑛 + 1) βˆ’ 1)))) βˆ’ ((π‘†β€˜(𝑛 βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(𝑛 βˆ’ 1))))) = (((π‘†β€˜π‘›) βˆ’ (2 Β· (π‘‡β€˜π‘›))) βˆ’ ((π‘†β€˜(𝑛 βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(𝑛 βˆ’ 1))))))
265 2cnd 12312 . . . . . . . . . . . . . . 15 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ 2 ∈ β„‚)
266249recnd 11264 . . . . . . . . . . . . . . 15 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (π‘‡β€˜π‘›) ∈ β„‚)
267258recnd 11264 . . . . . . . . . . . . . . 15 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (π‘‡β€˜(𝑛 βˆ’ 1)) ∈ β„‚)
268265, 266, 267subdid 11692 . . . . . . . . . . . . . 14 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))) = ((2 Β· (π‘‡β€˜π‘›)) βˆ’ (2 Β· (π‘‡β€˜(𝑛 βˆ’ 1)))))
269268oveq2d 7430 . . . . . . . . . . . . 13 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))) = (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ ((2 Β· (π‘‡β€˜π‘›)) βˆ’ (2 Β· (π‘‡β€˜(𝑛 βˆ’ 1))))))
270261, 264, 2693eqtr4d 2777 . . . . . . . . . . . 12 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (((π‘†β€˜((𝑛 + 1) βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜((𝑛 + 1) βˆ’ 1)))) βˆ’ ((π‘†β€˜(𝑛 βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(𝑛 βˆ’ 1))))) = (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))))
271270oveq2d 7430 . . . . . . . . . . 11 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜((𝑛 + 1) βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜((𝑛 + 1) βˆ’ 1)))) βˆ’ ((π‘†β€˜(𝑛 βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(𝑛 βˆ’ 1)))))) = ((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))))
27299, 271sumeq12rdv 15677 . . . . . . . . . 10 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Σ𝑛 ∈ (1..^((βŒŠβ€˜π‘₯) + 1))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜((𝑛 + 1) βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜((𝑛 + 1) βˆ’ 1)))) βˆ’ ((π‘†β€˜(𝑛 βˆ’ 1)) βˆ’ (2 Β· (π‘‡β€˜(𝑛 βˆ’ 1)))))) = Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))))
273246, 272eqtr3d 2769 . . . . . . . . 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 15703 . . . . . . . . . 10 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›))))) ∈ β„‚)
27593, 274subnegd 11600 . . . . . . . . 9 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))) βˆ’ -Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›)))))) = (((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))) + Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›)))))))
276162, 273, 2753eqtr3rd 2776 . . . . . . . 8 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))) + Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›)))))) = Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))))
27710relogcld 26544 . . . . . . . . . 10 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (logβ€˜π‘₯) ∈ ℝ)
278277recnd 11264 . . . . . . . . 9 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (logβ€˜π‘₯) ∈ β„‚)
27966, 278mulcomd 11257 . . . . . . . 8 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘₯ Β· (logβ€˜π‘₯)) = ((logβ€˜π‘₯) Β· π‘₯))
280276, 279oveq12d 7432 . . . . . . 7 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))) + Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›)))))) / (π‘₯ Β· (logβ€˜π‘₯))) = (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))) / ((logβ€˜π‘₯) Β· π‘₯)))
281147, 255resubcld 11664 . . . . . . . . . . . 12 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) ∈ ℝ)
282249, 258resubcld 11664 . . . . . . . . . . . . 13 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))) ∈ ℝ)
283148, 282remulcld 11266 . . . . . . . . . . . 12 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))) ∈ ℝ)
284281, 283resubcld 11664 . . . . . . . . . . 11 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))) ∈ ℝ)
285108, 284remulcld 11266 . . . . . . . . . 10 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))) ∈ ℝ)
286157, 285fsumrecl 15704 . . . . . . . . 9 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))) ∈ ℝ)
287286recnd 11264 . . . . . . . 8 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))) ∈ β„‚)
2882, 8rplogcld 26550 . . . . . . . . 9 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (logβ€˜π‘₯) ∈ ℝ+)
289288rpne0d 13045 . . . . . . . 8 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (logβ€˜π‘₯) β‰  0)
29010rpne0d 13045 . . . . . . . 8 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ π‘₯ β‰  0)
291287, 278, 66, 289, 290divdiv1d 12043 . . . . . . 7 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))) / (logβ€˜π‘₯)) / π‘₯) = (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))) / ((logβ€˜π‘₯) Β· π‘₯)))
292280, 291eqtr4d 2770 . . . . . 6 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))) + Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›)))))) / (π‘₯ Β· (logβ€˜π‘₯))) = ((Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))) / (logβ€˜π‘₯)) / π‘₯))
293292oveq2d 7430 . . . . 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 11264 . . . . . . . . . 10 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘…β€˜π‘₯) ∈ β„‚)
295294abscld 15407 . . . . . . . . 9 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (absβ€˜(π‘…β€˜π‘₯)) ∈ ℝ)
296295, 277remulcld 11266 . . . . . . . 8 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((absβ€˜(π‘…β€˜π‘₯)) Β· (logβ€˜π‘₯)) ∈ ℝ)
297108, 281remulcld 11266 . . . . . . . . . 10 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) ∈ ℝ)
298157, 297fsumrecl 15704 . . . . . . . . 9 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) ∈ ℝ)
299298, 288rerpdivcld 13071 . . . . . . . 8 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) / (logβ€˜π‘₯)) ∈ ℝ)
300296, 299resubcld 11664 . . . . . . 7 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((absβ€˜(π‘…β€˜π‘₯)) Β· (logβ€˜π‘₯)) βˆ’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) / (logβ€˜π‘₯))) ∈ ℝ)
301300recnd 11264 . . . . . 6 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((absβ€˜(π‘…β€˜π‘₯)) Β· (logβ€˜π‘₯)) βˆ’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) / (logβ€˜π‘₯))) ∈ β„‚)
302287, 278, 289divcld 12012 . . . . . 6 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))) / (logβ€˜π‘₯)) ∈ β„‚)
303301, 302, 66, 290divdird 12050 . . . . 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 11264 . . . . . . . 8 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((absβ€˜(π‘…β€˜π‘₯)) Β· (logβ€˜π‘₯)) ∈ β„‚)
305299recnd 11264 . . . . . . . 8 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) / (logβ€˜π‘₯)) ∈ β„‚)
306304, 305, 302subsubd 11621 . . . . . . 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 12312 . . . . . . . . . . . 12 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 2 ∈ β„‚)
308266, 267subcld 11593 . . . . . . . . . . . . 13 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))) ∈ β„‚)
309109, 308mulcld 11256 . . . . . . . . . . . 12 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))) ∈ β„‚)
310157, 307, 309fsummulc2 15754 . . . . . . . . . . 11 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))) = Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(2 Β· ((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))))
311281recnd 11264 . . . . . . . . . . . . . . 15 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) ∈ β„‚)
312265, 308mulcld 11256 . . . . . . . . . . . . . . 15 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))) ∈ β„‚)
313311, 312nncand 11598 . . . . . . . . . . . . . 14 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))) = (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))
314313oveq2d 7430 . . . . . . . . . . . . 13 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))))) = ((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))))
315284recnd 11264 . . . . . . . . . . . . . 14 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))) ∈ β„‚)
316109, 311, 315subdid 11692 . . . . . . . . . . . . 13 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))))) = (((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) βˆ’ ((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))))))
317109, 265, 308mul12d 11445 . . . . . . . . . . . . 13 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))) = (2 Β· ((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))))
318314, 316, 3173eqtr3d 2775 . . . . . . . . . . . 12 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ (((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) βˆ’ ((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))))) = (2 Β· ((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))))
319318sumeq2dv 15673 . . . . . . . . . . 11 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) βˆ’ ((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))))) = Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(2 Β· ((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))))
320297recnd 11264 . . . . . . . . . . . 12 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) ∈ β„‚)
321285recnd 11264 . . . . . . . . . . . 12 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))) ∈ β„‚)
322157, 320, 321fsumsub 15758 . . . . . . . . . . 11 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) βˆ’ ((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))))) = (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) βˆ’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))))))
323310, 319, 3223eqtr2rd 2774 . . . . . . . . . 10 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) βˆ’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))))) = (2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))))
324323oveq1d 7429 . . . . . . . . 9 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) βˆ’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))))) / (logβ€˜π‘₯)) = ((2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))) / (logβ€˜π‘₯)))
325298recnd 11264 . . . . . . . . . 10 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) ∈ β„‚)
326325, 287, 278, 289divsubdird 12051 . . . . . . . . 9 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) βˆ’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))))) / (logβ€˜π‘₯)) = ((Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) / (logβ€˜π‘₯)) βˆ’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))) / (logβ€˜π‘₯))))
327108, 282remulcld 11266 . . . . . . . . . . . 12 (((⊀ ∧ π‘₯ ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(βŒŠβ€˜π‘₯))) β†’ ((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))) ∈ ℝ)
328157, 327fsumrecl 15704 . . . . . . . . . . 11 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))) ∈ ℝ)
329328recnd 11264 . . . . . . . . . 10 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))) ∈ β„‚)
330307, 329, 278, 289div23d 12049 . . . . . . . . 9 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((2 Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))) / (logβ€˜π‘₯)) = ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))))
331324, 326, 3303eqtr3d 2775 . . . . . . . 8 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) / (logβ€˜π‘₯)) βˆ’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))) / (logβ€˜π‘₯))) = ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1))))))
332331oveq2d 7430 . . . . . . 7 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((absβ€˜(π‘…β€˜π‘₯)) Β· (logβ€˜π‘₯)) βˆ’ ((Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) / (logβ€˜π‘₯)) βˆ’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))) / (logβ€˜π‘₯)))) = (((absβ€˜(π‘…β€˜π‘₯)) Β· (logβ€˜π‘₯)) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))))
333306, 332eqtr3d 2769 . . . . . 6 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((((absβ€˜(π‘…β€˜π‘₯)) Β· (logβ€˜π‘₯)) βˆ’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) / (logβ€˜π‘₯))) + (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))) / (logβ€˜π‘₯))) = (((absβ€˜(π‘…β€˜π‘₯)) Β· (logβ€˜π‘₯)) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))))
334333oveq1d 7429 . . . . 5 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((((absβ€˜(π‘…β€˜π‘₯)) Β· (logβ€˜π‘₯)) βˆ’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) / (logβ€˜π‘₯))) + (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· (((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1))) βˆ’ (2 Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))) / (logβ€˜π‘₯))) / π‘₯) = ((((absβ€˜(π‘…β€˜π‘₯)) Β· (logβ€˜π‘₯)) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))) / π‘₯))
335293, 303, 3343eqtr2d 2773 . . . 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 5242 . . 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 13071 . . . 4 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((((absβ€˜(π‘…β€˜π‘₯)) Β· (logβ€˜π‘₯)) βˆ’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) / (logβ€˜π‘₯))) / π‘₯) ∈ ℝ)
338157, 158fsumrecl 15704 . . . . . 6 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›))))) ∈ ℝ)
33992, 338readdcld 11265 . . . . 5 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))) + Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›)))))) ∈ ℝ)
34010, 288rpmulcld 13056 . . . . 5 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘₯ Β· (logβ€˜π‘₯)) ∈ ℝ+)
341339, 340rerpdivcld 13071 . . . 4 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))) + Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›)))))) / (π‘₯ Β· (logβ€˜π‘₯))) ∈ ℝ)
34247, 18pntrlog2bndlem1 27497 . . . . 5 (π‘₯ ∈ (1(,)+∞) ↦ ((((absβ€˜(π‘…β€˜π‘₯)) Β· (logβ€˜π‘₯)) βˆ’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) / (logβ€˜π‘₯))) / π‘₯)) ∈ ≀𝑂(1)
343342a1i 11 . . . 4 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ ((((absβ€˜(π‘…β€˜π‘₯)) Β· (logβ€˜π‘₯)) βˆ’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) / (logβ€˜π‘₯))) / π‘₯)) ∈ ≀𝑂(1))
344340rpcnd 13042 . . . . . . . 8 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘₯ Β· (logβ€˜π‘₯)) ∈ β„‚)
345340rpne0d 13045 . . . . . . . 8 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘₯ Β· (logβ€˜π‘₯)) β‰  0)
34693, 274, 344, 345divdird 12050 . . . . . . 7 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))) + Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›)))))) / (π‘₯ Β· (logβ€˜π‘₯))) = ((((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))) / (π‘₯ Β· (logβ€˜π‘₯))) + (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›))))) / (π‘₯ Β· (logβ€˜π‘₯)))))
34791recnd 11264 . . . . . . . . 9 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯)))) ∈ β„‚)
34843, 347, 344, 345divassd 12047 . . . . . . . 8 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))) / (π‘₯ Β· (logβ€˜π‘₯))) = ((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· (((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯)))) / (π‘₯ Β· (logβ€˜π‘₯)))))
349348oveq1d 7429 . . . . . . 7 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))) / (π‘₯ Β· (logβ€˜π‘₯))) + (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›))))) / (π‘₯ Β· (logβ€˜π‘₯)))) = (((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· (((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯)))) / (π‘₯ Β· (logβ€˜π‘₯)))) + (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›))))) / (π‘₯ Β· (logβ€˜π‘₯)))))
350346, 349eqtrd 2767 . . . . . 6 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))) + Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›)))))) / (π‘₯ Β· (logβ€˜π‘₯))) = (((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· (((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯)))) / (π‘₯ Β· (logβ€˜π‘₯)))) + (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›))))) / (π‘₯ Β· (logβ€˜π‘₯)))))
351350mpteq2dva 5242 . . . . 5 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ ((((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))) + Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›)))))) / (π‘₯ Β· (logβ€˜π‘₯)))) = (π‘₯ ∈ (1(,)+∞) ↦ (((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· (((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯)))) / (π‘₯ Β· (logβ€˜π‘₯)))) + (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›))))) / (π‘₯ Β· (logβ€˜π‘₯))))))
35291, 340rerpdivcld 13071 . . . . . . 7 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯)))) / (π‘₯ Β· (logβ€˜π‘₯))) ∈ ℝ)
35321, 352remulcld 11266 . . . . . 6 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· (((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯)))) / (π‘₯ Β· (logβ€˜π‘₯)))) ∈ ℝ)
354338, 340rerpdivcld 13071 . . . . . 6 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›))))) / (π‘₯ Β· (logβ€˜π‘₯))) ∈ ℝ)
355 ioossre 13409 . . . . . . . . 9 (1(,)+∞) βŠ† ℝ
356355a1i 11 . . . . . . . 8 (⊀ β†’ (1(,)+∞) βŠ† ℝ)
357 1red 11237 . . . . . . . 8 (⊀ β†’ 1 ∈ ℝ)
35821, 5, 30ltled 11384 . . . . . . . . 9 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) ≀ 1)
359358adantrr 716 . . . . . . . 8 ((⊀ ∧ (π‘₯ ∈ (1(,)+∞) ∧ 1 ≀ π‘₯)) β†’ (π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) ≀ 1)
360356, 21, 357, 357, 359ello1d 15491 . . . . . . 7 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ (π‘₯ / ((βŒŠβ€˜π‘₯) + 1))) ∈ ≀𝑂(1))
36180recnd 11264 . . . . . . . . . . 11 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘†β€˜π‘₯) ∈ β„‚)
36290recnd 11264 . . . . . . . . . . 11 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))) ∈ β„‚)
363361, 362, 344, 345divsubdird 12051 . . . . . . . . . 10 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯)))) / (π‘₯ Β· (logβ€˜π‘₯))) = (((π‘†β€˜π‘₯) / (π‘₯ Β· (logβ€˜π‘₯))) βˆ’ ((2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))) / (π‘₯ Β· (logβ€˜π‘₯)))))
364363mpteq2dva 5242 . . . . . . . . 9 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ (((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯)))) / (π‘₯ Β· (logβ€˜π‘₯)))) = (π‘₯ ∈ (1(,)+∞) ↦ (((π‘†β€˜π‘₯) / (π‘₯ Β· (logβ€˜π‘₯))) βˆ’ ((2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))) / (π‘₯ Β· (logβ€˜π‘₯))))))
36580, 340rerpdivcld 13071 . . . . . . . . . 10 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((π‘†β€˜π‘₯) / (π‘₯ Β· (logβ€˜π‘₯))) ∈ ℝ)
36690, 340rerpdivcld 13071 . . . . . . . . . 10 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))) / (π‘₯ Β· (logβ€˜π‘₯))) ∈ ℝ)
367 2cnd 12312 . . . . . . . . . . . 12 (⊀ β†’ 2 ∈ β„‚)
368 o1const 15588 . . . . . . . . . . . 12 (((1(,)+∞) βŠ† ℝ ∧ 2 ∈ β„‚) β†’ (π‘₯ ∈ (1(,)+∞) ↦ 2) ∈ 𝑂(1))
369355, 367, 368sylancr 586 . . . . . . . . . . 11 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ 2) ∈ 𝑂(1))
370365recnd 11264 . . . . . . . . . . . 12 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((π‘†β€˜π‘₯) / (π‘₯ Β· (logβ€˜π‘₯))) ∈ β„‚)
37180, 10rerpdivcld 13071 . . . . . . . . . . . . . . . . 17 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((π‘†β€˜π‘₯) / π‘₯) ∈ ℝ)
372371recnd 11264 . . . . . . . . . . . . . . . 16 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((π‘†β€˜π‘₯) / π‘₯) ∈ β„‚)
373307, 278mulcld 11256 . . . . . . . . . . . . . . . 16 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (2 Β· (logβ€˜π‘₯)) ∈ β„‚)
374372, 373, 278, 289divsubdird 12051 . . . . . . . . . . . . . . 15 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((((π‘†β€˜π‘₯) / π‘₯) βˆ’ (2 Β· (logβ€˜π‘₯))) / (logβ€˜π‘₯)) = ((((π‘†β€˜π‘₯) / π‘₯) / (logβ€˜π‘₯)) βˆ’ ((2 Β· (logβ€˜π‘₯)) / (logβ€˜π‘₯))))
37523, 277remulcld 11266 . . . . . . . . . . . . . . . . . 18 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (2 Β· (logβ€˜π‘₯)) ∈ ℝ)
376371, 375resubcld 11664 . . . . . . . . . . . . . . . . 17 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((π‘†β€˜π‘₯) / π‘₯) βˆ’ (2 Β· (logβ€˜π‘₯))) ∈ ℝ)
377376recnd 11264 . . . . . . . . . . . . . . . 16 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((π‘†β€˜π‘₯) / π‘₯) βˆ’ (2 Β· (logβ€˜π‘₯))) ∈ β„‚)
378377, 278, 289divrecd 12015 . . . . . . . . . . . . . . 15 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((((π‘†β€˜π‘₯) / π‘₯) βˆ’ (2 Β· (logβ€˜π‘₯))) / (logβ€˜π‘₯)) = ((((π‘†β€˜π‘₯) / π‘₯) βˆ’ (2 Β· (logβ€˜π‘₯))) Β· (1 / (logβ€˜π‘₯))))
379361, 66, 278, 290, 289divdiv1d 12043 . . . . . . . . . . . . . . . 16 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((π‘†β€˜π‘₯) / π‘₯) / (logβ€˜π‘₯)) = ((π‘†β€˜π‘₯) / (π‘₯ Β· (logβ€˜π‘₯))))
380307, 278, 289divcan4d 12018 . . . . . . . . . . . . . . . 16 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((2 Β· (logβ€˜π‘₯)) / (logβ€˜π‘₯)) = 2)
381379, 380oveq12d 7432 . . . . . . . . . . . . . . 15 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((((π‘†β€˜π‘₯) / π‘₯) / (logβ€˜π‘₯)) βˆ’ ((2 Β· (logβ€˜π‘₯)) / (logβ€˜π‘₯))) = (((π‘†β€˜π‘₯) / (π‘₯ Β· (logβ€˜π‘₯))) βˆ’ 2))
382374, 378, 3813eqtr3rd 2776 . . . . . . . . . . . . . 14 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (((π‘†β€˜π‘₯) / (π‘₯ Β· (logβ€˜π‘₯))) βˆ’ 2) = ((((π‘†β€˜π‘₯) / π‘₯) βˆ’ (2 Β· (logβ€˜π‘₯))) Β· (1 / (logβ€˜π‘₯))))
383382mpteq2dva 5242 . . . . . . . . . . . . 13 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ (((π‘†β€˜π‘₯) / (π‘₯ Β· (logβ€˜π‘₯))) βˆ’ 2)) = (π‘₯ ∈ (1(,)+∞) ↦ ((((π‘†β€˜π‘₯) / π‘₯) βˆ’ (2 Β· (logβ€˜π‘₯))) Β· (1 / (logβ€˜π‘₯)))))
3845, 288rerpdivcld 13071 . . . . . . . . . . . . . 14 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (1 / (logβ€˜π‘₯)) ∈ ℝ)
38510ex 412 . . . . . . . . . . . . . . . 16 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) β†’ π‘₯ ∈ ℝ+))
386385ssrdv 3984 . . . . . . . . . . . . . . 15 (⊀ β†’ (1(,)+∞) βŠ† ℝ+)
38747selbergs 27494 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ ℝ+ ↦ (((π‘†β€˜π‘₯) / π‘₯) βˆ’ (2 Β· (logβ€˜π‘₯)))) ∈ 𝑂(1)
388387a1i 11 . . . . . . . . . . . . . . 15 (⊀ β†’ (π‘₯ ∈ ℝ+ ↦ (((π‘†β€˜π‘₯) / π‘₯) βˆ’ (2 Β· (logβ€˜π‘₯)))) ∈ 𝑂(1))
389386, 388o1res2 15531 . . . . . . . . . . . . . 14 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ (((π‘†β€˜π‘₯) / π‘₯) βˆ’ (2 Β· (logβ€˜π‘₯)))) ∈ 𝑂(1))
390 divlogrlim 26556 . . . . . . . . . . . . . . 15 (π‘₯ ∈ (1(,)+∞) ↦ (1 / (logβ€˜π‘₯))) β‡π‘Ÿ 0
391 rlimo1 15585 . . . . . . . . . . . . . . 15 ((π‘₯ ∈ (1(,)+∞) ↦ (1 / (logβ€˜π‘₯))) β‡π‘Ÿ 0 β†’ (π‘₯ ∈ (1(,)+∞) ↦ (1 / (logβ€˜π‘₯))) ∈ 𝑂(1))
392390, 391mp1i 13 . . . . . . . . . . . . . 14 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ (1 / (logβ€˜π‘₯))) ∈ 𝑂(1))
393376, 384, 389, 392o1mul2 15593 . . . . . . . . . . . . 13 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ ((((π‘†β€˜π‘₯) / π‘₯) βˆ’ (2 Β· (logβ€˜π‘₯))) Β· (1 / (logβ€˜π‘₯)))) ∈ 𝑂(1))
394383, 393eqeltrd 2828 . . . . . . . . . . . 12 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ (((π‘†β€˜π‘₯) / (π‘₯ Β· (logβ€˜π‘₯))) βˆ’ 2)) ∈ 𝑂(1))
395370, 307, 394o1dif 15598 . . . . . . . . . . 11 (⊀ β†’ ((π‘₯ ∈ (1(,)+∞) ↦ ((π‘†β€˜π‘₯) / (π‘₯ Β· (logβ€˜π‘₯)))) ∈ 𝑂(1) ↔ (π‘₯ ∈ (1(,)+∞) ↦ 2) ∈ 𝑂(1)))
396369, 395mpbird 257 . . . . . . . . . 10 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ ((π‘†β€˜π‘₯) / (π‘₯ Β· (logβ€˜π‘₯)))) ∈ 𝑂(1))
39722a1i 11 . . . . . . . . . . . 12 (⊀ β†’ 2 ∈ ℝ)
3982, 277remulcld 11266 . . . . . . . . . . . . . . 15 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘₯ Β· (logβ€˜π‘₯)) ∈ ℝ)
399 2rp 13003 . . . . . . . . . . . . . . . . 17 2 ∈ ℝ+
400399a1i 11 . . . . . . . . . . . . . . . 16 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 2 ∈ ℝ+)
401400rpge0d 13044 . . . . . . . . . . . . . . 15 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 0 ≀ 2)
402 flge1nn 13810 . . . . . . . . . . . . . . . . . . 19 ((π‘₯ ∈ ℝ ∧ 1 ≀ π‘₯) β†’ (βŒŠβ€˜π‘₯) ∈ β„•)
4032, 9, 402syl2anc 583 . . . . . . . . . . . . . . . . . 18 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (βŒŠβ€˜π‘₯) ∈ β„•)
404403nnrpd 13038 . . . . . . . . . . . . . . . . 17 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (βŒŠβ€˜π‘₯) ∈ ℝ+)
405 rpre 13006 . . . . . . . . . . . . . . . . . . 19 ((βŒŠβ€˜π‘₯) ∈ ℝ+ β†’ (βŒŠβ€˜π‘₯) ∈ ℝ)
406 eleq1 2816 . . . . . . . . . . . . . . . . . . . . 21 (π‘Ž = (βŒŠβ€˜π‘₯) β†’ (π‘Ž ∈ ℝ+ ↔ (βŒŠβ€˜π‘₯) ∈ ℝ+))
407 id 22 . . . . . . . . . . . . . . . . . . . . . 22 (π‘Ž = (βŒŠβ€˜π‘₯) β†’ π‘Ž = (βŒŠβ€˜π‘₯))
408 fveq2 6891 . . . . . . . . . . . . . . . . . . . . . 22 (π‘Ž = (βŒŠβ€˜π‘₯) β†’ (logβ€˜π‘Ž) = (logβ€˜(βŒŠβ€˜π‘₯)))
409407, 408oveq12d 7432 . . . . . . . . . . . . . . . . . . . . 21 (π‘Ž = (βŒŠβ€˜π‘₯) β†’ (π‘Ž Β· (logβ€˜π‘Ž)) = ((βŒŠβ€˜π‘₯) Β· (logβ€˜(βŒŠβ€˜π‘₯))))
410406, 409ifbieq1d 4548 . . . . . . . . . . . . . . . . . . . 20 (π‘Ž = (βŒŠβ€˜π‘₯) β†’ if(π‘Ž ∈ ℝ+, (π‘Ž Β· (logβ€˜π‘Ž)), 0) = if((βŒŠβ€˜π‘₯) ∈ ℝ+, ((βŒŠβ€˜π‘₯) Β· (logβ€˜(βŒŠβ€˜π‘₯))), 0))
411 ovex 7447 . . . . . . . . . . . . . . . . . . . . 21 ((βŒŠβ€˜π‘₯) Β· (logβ€˜(βŒŠβ€˜π‘₯))) ∈ V
412411, 132ifex 4574 . . . . . . . . . . . . . . . . . . . 20 if((βŒŠβ€˜π‘₯) ∈ ℝ+, ((βŒŠβ€˜π‘₯) Β· (logβ€˜(βŒŠβ€˜π‘₯))), 0) ∈ V
413410, 81, 412fvmpt 6999 . . . . . . . . . . . . . . . . . . 19 ((βŒŠβ€˜π‘₯) ∈ ℝ β†’ (π‘‡β€˜(βŒŠβ€˜π‘₯)) = if((βŒŠβ€˜π‘₯) ∈ ℝ+, ((βŒŠβ€˜π‘₯) Β· (logβ€˜(βŒŠβ€˜π‘₯))), 0))
414405, 413syl 17 . . . . . . . . . . . . . . . . . 18 ((βŒŠβ€˜π‘₯) ∈ ℝ+ β†’ (π‘‡β€˜(βŒŠβ€˜π‘₯)) = if((βŒŠβ€˜π‘₯) ∈ ℝ+, ((βŒŠβ€˜π‘₯) Β· (logβ€˜(βŒŠβ€˜π‘₯))), 0))
415 iftrue 4530 . . . . . . . . . . . . . . . . . 18 ((βŒŠβ€˜π‘₯) ∈ ℝ+ β†’ if((βŒŠβ€˜π‘₯) ∈ ℝ+, ((βŒŠβ€˜π‘₯) Β· (logβ€˜(βŒŠβ€˜π‘₯))), 0) = ((βŒŠβ€˜π‘₯) Β· (logβ€˜(βŒŠβ€˜π‘₯))))
416414, 415eqtrd 2767 . . . . . . . . . . . . . . . . 17 ((βŒŠβ€˜π‘₯) ∈ ℝ+ β†’ (π‘‡β€˜(βŒŠβ€˜π‘₯)) = ((βŒŠβ€˜π‘₯) Β· (logβ€˜(βŒŠβ€˜π‘₯))))
417404, 416syl 17 . . . . . . . . . . . . . . . 16 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘‡β€˜(βŒŠβ€˜π‘₯)) = ((βŒŠβ€˜π‘₯) Β· (logβ€˜(βŒŠβ€˜π‘₯))))
418404relogcld 26544 . . . . . . . . . . . . . . . . 17 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (logβ€˜(βŒŠβ€˜π‘₯)) ∈ ℝ)
41913nn0ge0d 12557 . . . . . . . . . . . . . . . . 17 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 0 ≀ (βŒŠβ€˜π‘₯))
420403nnge1d 12282 . . . . . . . . . . . . . . . . . 18 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 1 ≀ (βŒŠβ€˜π‘₯))
42146, 420logge0d 26551 . . . . . . . . . . . . . . . . 17 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 0 ≀ (logβ€˜(βŒŠβ€˜π‘₯)))
422 flle 13788 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ ℝ β†’ (βŒŠβ€˜π‘₯) ≀ π‘₯)
4232, 422syl 17 . . . . . . . . . . . . . . . . 17 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (βŒŠβ€˜π‘₯) ≀ π‘₯)
424404, 10logled 26548 . . . . . . . . . . . . . . . . . 18 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((βŒŠβ€˜π‘₯) ≀ π‘₯ ↔ (logβ€˜(βŒŠβ€˜π‘₯)) ≀ (logβ€˜π‘₯)))
425423, 424mpbid 231 . . . . . . . . . . . . . . . . 17 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (logβ€˜(βŒŠβ€˜π‘₯)) ≀ (logβ€˜π‘₯))
42646, 2, 418, 277, 419, 421, 423, 425lemul12ad 12178 . . . . . . . . . . . . . . . 16 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ ((βŒŠβ€˜π‘₯) Β· (logβ€˜(βŒŠβ€˜π‘₯))) ≀ (π‘₯ Β· (logβ€˜π‘₯)))
427417, 426eqbrtrd 5164 . . . . . . . . . . . . . . 15 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (π‘‡β€˜(βŒŠβ€˜π‘₯)) ≀ (π‘₯ Β· (logβ€˜π‘₯)))
42889, 398, 23, 401, 427lemul2ad 12176 . . . . . . . . . . . . . 14 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))) ≀ (2 Β· (π‘₯ Β· (logβ€˜π‘₯))))
42990, 23, 340ledivmul2d 13094 . . . . . . . . . . . . . 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 15491 . . . . . . . . . . 11 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ ((2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))) / (π‘₯ Β· (logβ€˜π‘₯)))) ∈ ≀𝑂(1))
433 0red 11239 . . . . . . . . . . . 12 (⊀ β†’ 0 ∈ ℝ)
43446, 418, 419, 421mulge0d 11813 . . . . . . . . . . . . . . 15 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 0 ≀ ((βŒŠβ€˜π‘₯) Β· (logβ€˜(βŒŠβ€˜π‘₯))))
435434, 417breqtrrd 5170 . . . . . . . . . . . . . 14 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 0 ≀ (π‘‡β€˜(βŒŠβ€˜π‘₯)))
43623, 89, 401, 435mulge0d 11813 . . . . . . . . . . . . 13 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 0 ≀ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))
43790, 340, 436divge0d 13080 . . . . . . . . . . . 12 ((⊀ ∧ π‘₯ ∈ (1(,)+∞)) β†’ 0 ≀ ((2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))) / (π‘₯ Β· (logβ€˜π‘₯))))
438366, 433, 437o1lo12 15506 . . . . . . . . . . 11 (⊀ β†’ ((π‘₯ ∈ (1(,)+∞) ↦ ((2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))) / (π‘₯ Β· (logβ€˜π‘₯)))) ∈ 𝑂(1) ↔ (π‘₯ ∈ (1(,)+∞) ↦ ((2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))) / (π‘₯ Β· (logβ€˜π‘₯)))) ∈ ≀𝑂(1)))
439432, 438mpbird 257 . . . . . . . . . 10 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ ((2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))) / (π‘₯ Β· (logβ€˜π‘₯)))) ∈ 𝑂(1))
440365, 366, 396, 439o1sub2 15594 . . . . . . . . 9 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ (((π‘†β€˜π‘₯) / (π‘₯ Β· (logβ€˜π‘₯))) βˆ’ ((2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))) / (π‘₯ Β· (logβ€˜π‘₯))))) ∈ 𝑂(1))
441364, 440eqeltrd 2828 . . . . . . . 8 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ (((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯)))) / (π‘₯ Β· (logβ€˜π‘₯)))) ∈ 𝑂(1))
442352, 441o1lo1d 15507 . . . . . . 7 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ (((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯)))) / (π‘₯ Β· (logβ€˜π‘₯)))) ∈ ≀𝑂(1))
44321, 352, 360, 442, 41lo1mul 15596 . . . . . 6 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ ((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· (((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯)))) / (π‘₯ Β· (logβ€˜π‘₯))))) ∈ ≀𝑂(1))
44447selbergsb 27495 . . . . . . . 8 βˆƒπ‘ ∈ ℝ+ βˆ€π‘¦ ∈ (1[,)+∞)(absβ€˜(((π‘†β€˜π‘¦) / 𝑦) βˆ’ (2 Β· (logβ€˜π‘¦)))) ≀ 𝑐
445 simpl 482 . . . . . . . . . 10 ((𝑐 ∈ ℝ+ ∧ βˆ€π‘¦ ∈ (1[,)+∞)(absβ€˜(((π‘†β€˜π‘¦) / 𝑦) βˆ’ (2 Β· (logβ€˜π‘¦)))) ≀ 𝑐) β†’ 𝑐 ∈ ℝ+)
446 simpr 484 . . . . . . . . . 10 ((𝑐 ∈ ℝ+ ∧ βˆ€π‘¦ ∈ (1[,)+∞)(absβ€˜(((π‘†β€˜π‘¦) / 𝑦) βˆ’ (2 Β· (logβ€˜π‘¦)))) ≀ 𝑐) β†’ βˆ€π‘¦ ∈ (1[,)+∞)(absβ€˜(((π‘†β€˜π‘¦) / 𝑦) βˆ’ (2 Β· (logβ€˜π‘¦)))) ≀ 𝑐)
44747, 18, 445, 446pntrlog2bndlem3 27499 . . . . . . . . 9 ((𝑐 ∈ ℝ+ ∧ βˆ€π‘¦ ∈ (1[,)+∞)(absβ€˜(((π‘†β€˜π‘¦) / 𝑦) βˆ’ (2 Β· (logβ€˜π‘¦)))) ≀ 𝑐) β†’ (π‘₯ ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›))))) / (π‘₯ Β· (logβ€˜π‘₯)))) ∈ 𝑂(1))
448447rexlimiva 3142 . . . . . . . 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 15507 . . . . . 6 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›))))) / (π‘₯ Β· (logβ€˜π‘₯)))) ∈ ≀𝑂(1))
451353, 354, 443, 450lo1add 15595 . . . . 5 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ (((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· (((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯)))) / (π‘₯ Β· (logβ€˜π‘₯)))) + (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›))))) / (π‘₯ Β· (logβ€˜π‘₯))))) ∈ ≀𝑂(1))
452351, 451eqeltrd 2828 . . . 4 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ ((((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))) + Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›)))))) / (π‘₯ Β· (logβ€˜π‘₯)))) ∈ ≀𝑂(1))
453337, 341, 343, 452lo1add 15595 . . 3 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ (((((absβ€˜(π‘…β€˜π‘₯)) Β· (logβ€˜π‘₯)) βˆ’ (Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘†β€˜π‘›) βˆ’ (π‘†β€˜(𝑛 βˆ’ 1)))) / (logβ€˜π‘₯))) / π‘₯) + ((((π‘₯ / ((βŒŠβ€˜π‘₯) + 1)) Β· ((π‘†β€˜π‘₯) βˆ’ (2 Β· (π‘‡β€˜(βŒŠβ€˜π‘₯))))) + Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))(((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) βˆ’ (absβ€˜(π‘…β€˜(π‘₯ / (𝑛 + 1))))) Β· ((π‘†β€˜π‘›) βˆ’ (2 Β· (𝑛 Β· (logβ€˜π‘›)))))) / (π‘₯ Β· (logβ€˜π‘₯))))) ∈ ≀𝑂(1))
454336, 453eqeltrrd 2829 . 2 (⊀ β†’ (π‘₯ ∈ (1(,)+∞) ↦ ((((absβ€˜(π‘…β€˜π‘₯)) Β· (logβ€˜π‘₯)) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))) / π‘₯)) ∈ ≀𝑂(1))
455454mptru 1541 1 (π‘₯ ∈ (1(,)+∞) ↦ ((((absβ€˜(π‘…β€˜π‘₯)) Β· (logβ€˜π‘₯)) βˆ’ ((2 / (logβ€˜π‘₯)) Β· Σ𝑛 ∈ (1...(βŒŠβ€˜π‘₯))((absβ€˜(π‘…β€˜(π‘₯ / 𝑛))) Β· ((π‘‡β€˜π‘›) βˆ’ (π‘‡β€˜(𝑛 βˆ’ 1)))))) / π‘₯)) ∈ ≀𝑂(1)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   ↔ wb 205   ∧ wa 395   = wceq 1534  βŠ€wtru 1535   ∈ wcel 2099  βˆ€wral 3056  βˆƒwrex 3065  {crab 3427   βŠ† wss 3944  βˆ…c0 4318  ifcif 4524   class class class wbr 5142   ↦ cmpt 5225  β€˜cfv 6542  (class class class)co 7414  β„‚cc 11128  β„cr 11129  0cc0 11130  1c1 11131   + caddc 11133   Β· cmul 11135  +∞cpnf 11267   < clt 11270   ≀ cle 11271   βˆ’ cmin 11466  -cneg 11467   / cdiv 11893  β„•cn 12234  2c2 12289  β„•0cn0 12494  β„€cz 12580  β„€β‰₯cuz 12844  β„+crp 12998  (,)cioo 13348  [,)cico 13350  ...cfz 13508  ..^cfzo 13651  βŒŠcfl 13779  abscabs 15205   β‡π‘Ÿ crli 15453  π‘‚(1)co1 15454  β‰€π‘‚(1)clo1 15455  Ξ£csu 15656   βˆ₯ cdvds 16222  logclog 26475  Ξ›cvma 27011  Οˆcchp 27012
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-inf2 9656  ax-cnex 11186  ax-resscn 11187  ax-1cn 11188  ax-icn 11189  ax-addcl 11190  ax-addrcl 11191  ax-mulcl 11192  ax-mulrcl 11193  ax-mulcom 11194  ax-addass 11195  ax-mulass 11196  ax-distr 11197  ax-i2m1 11198  ax-1ne0 11199  ax-1rid 11200  ax-rnegex 11201  ax-rrecex 11202  ax-cnre 11203  ax-pre-lttri 11204  ax-pre-lttrn 11205  ax-pre-ltadd 11206  ax-pre-mulgt0 11207  ax-pre-sup 11208  ax-addf 11209
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-tp 4629  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-iin 4994  df-disj 5108  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-of 7679  df-om 7865  df-1st 7987  df-2nd 7988  df-supp 8160  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-2o 8481  df-oadd 8484  df-er 8718  df-map 8838  df-pm 8839  df-ixp 8908  df-en 8956  df-dom 8957  df-sdom 8958  df-fin 8959  df-fsupp 9378  df-fi 9426  df-sup 9457  df-inf 9458  df-oi 9525  df-dju 9916  df-card 9954  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11468  df-neg 11469  df-div 11894  df-nn 12235  df-2 12297  df-3 12298  df-4 12299  df-5 12300  df-6 12301  df-7 12302  df-8 12303  df-9 12304  df-n0 12495  df-xnn0 12567  df-z 12581  df-dec 12700  df-uz 12845  df-q 12955  df-rp 12999  df-xneg 13116  df-xadd 13117  df-xmul 13118  df-ioo 13352  df-ioc 13353  df-ico 13354  df-icc 13355  df-fz 13509  df-fzo 13652  df-fl 13781  df-mod 13859  df-seq 13991  df-exp 14051  df-fac 14257  df-bc 14286  df-hash 14314  df-shft 15038  df-cj 15070  df-re 15071  df-im 15072  df-sqrt 15206  df-abs 15207  df-limsup 15439  df-clim 15456  df-rlim 15457  df-o1 15458  df-lo1 15459  df-sum 15657  df-ef 16035  df-e 16036  df-sin 16037  df-cos 16038  df-tan 16039  df-pi 16040  df-dvds 16223  df-gcd 16461  df-prm 16634  df-pc 16797  df-struct 17107  df-sets 17124  df-slot 17142  df-ndx 17154  df-base 17172  df-ress 17201  df-plusg 17237  df-mulr 17238  df-starv 17239  df-sca 17240  df-vsca 17241  df-ip 17242  df-tset 17243  df-ple 17244  df-ds 17246  df-unif 17247  df-hom 17248  df-cco 17249  df-rest 17395  df-topn 17396  df-0g 17414  df-gsum 17415  df-topgen 17416  df-pt 17417  df-prds 17420  df-xrs 17475  df-qtop 17480  df-imas 17481  df-xps 17483  df-mre 17557  df-mrc 17558  df-acs 17560  df-mgm 18591  df-sgrp 18670  df-mnd 18686  df-submnd 18732  df-mulg 19015  df-cntz 19259  df-cmn 19728  df-psmet 21258  df-xmet 21259  df-met 21260  df-bl 21261  df-mopn 21262  df-fbas 21263  df-fg 21264  df-cnfld 21267  df-top 22783  df-topon 22800  df-topsp 22822  df-bases 22836  df-cld 22910  df-ntr 22911  df-cls 22912  df-nei 22989  df-lp 23027  df-perf 23028  df-cn 23118  df-cnp 23119  df-haus 23206  df-cmp 23278  df-tx 23453  df-hmeo 23646  df-fil 23737  df-fm 23829  df-flim 23830  df-flf 23831  df-xms 24213  df-ms 24214  df-tms 24215  df-cncf 24785  df-limc 25782  df-dv 25783  df-ulm 26300  df-log 26477  df-cxp 26478  df-atan 26786  df-em 26912  df-cht 27016  df-vma 27017  df-chp 27018  df-ppi 27019  df-mu 27020
This theorem is referenced by:  pntrlog2bndlem5  27501
  Copyright terms: Public domain W3C validator