Step | Hyp | Ref
| Expression |
1 | | elioore 12205 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ (1(,)+∞) →
𝑥 ∈
ℝ) |
2 | 1 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 𝑥 ∈ ℝ) |
3 | | 1rp 11836 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 ∈
ℝ+ |
4 | 3 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 1 ∈ ℝ+) |
5 | | 1red 10055 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 1 ∈ ℝ) |
6 | | eliooord 12233 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ (1(,)+∞) → (1
< 𝑥 ∧ 𝑥 <
+∞)) |
7 | 6 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (1 < 𝑥 ∧ 𝑥 < +∞)) |
8 | 7 | simpld 475 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 1 < 𝑥) |
9 | 5, 2, 8 | ltled 10185 |
. . . . . . . . . . . . . . . . . . 19
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 1 ≤ 𝑥) |
10 | 2, 4, 9 | rpgecld 11911 |
. . . . . . . . . . . . . . . . . 18
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 𝑥 ∈ ℝ+) |
11 | 10 | rprege0d 11879 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥)) |
12 | | flge0nn0 12621 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) →
(⌊‘𝑥) ∈
ℕ0) |
13 | 11, 12 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (⌊‘𝑥) ∈
ℕ0) |
14 | | nn0p1nn 11332 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((⌊‘𝑥)
∈ ℕ0 → ((⌊‘𝑥) + 1) ∈ ℕ) |
15 | 13, 14 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((⌊‘𝑥) + 1) ∈ ℕ) |
16 | 15 | nnrpd 11870 |
. . . . . . . . . . . . . . . . . 18
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((⌊‘𝑥) + 1) ∈
ℝ+) |
17 | 10, 16 | rpdivcld 11889 |
. . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑥 / ((⌊‘𝑥) + 1)) ∈
ℝ+) |
18 | | pntrlog2bnd.r |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦
((ψ‘𝑎) −
𝑎)) |
19 | 18 | pntrval 25251 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 / ((⌊‘𝑥) + 1)) ∈
ℝ+ → (𝑅‘(𝑥 / ((⌊‘𝑥) + 1))) = ((ψ‘(𝑥 / ((⌊‘𝑥) + 1))) − (𝑥 / ((⌊‘𝑥) + 1)))) |
20 | 17, 19 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑅‘(𝑥 / ((⌊‘𝑥) + 1))) = ((ψ‘(𝑥 / ((⌊‘𝑥) + 1))) − (𝑥 / ((⌊‘𝑥) + 1)))) |
21 | 2, 15 | nndivred 11069 |
. . . . . . . . . . . . . . . . . . 19
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑥 / ((⌊‘𝑥) + 1)) ∈ ℝ) |
22 | | 2re 11090 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ∈
ℝ |
23 | 22 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 2 ∈ ℝ) |
24 | | flltp1 12601 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ ℝ → 𝑥 < ((⌊‘𝑥) + 1)) |
25 | 2, 24 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 𝑥 < ((⌊‘𝑥) + 1)) |
26 | 15 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((⌊‘𝑥) + 1) ∈ ℂ) |
27 | 26 | mulid1d 10057 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((⌊‘𝑥) + 1) · 1) = ((⌊‘𝑥) + 1)) |
28 | 25, 27 | breqtrrd 4681 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 𝑥 < (((⌊‘𝑥) + 1) · 1)) |
29 | 2, 5, 16 | ltdivmuld 11923 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((𝑥 / ((⌊‘𝑥) + 1)) < 1 ↔ 𝑥 < (((⌊‘𝑥) + 1) · 1))) |
30 | 28, 29 | mpbird 247 |
. . . . . . . . . . . . . . . . . . 19
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑥 / ((⌊‘𝑥) + 1)) < 1) |
31 | | 1lt2 11194 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 <
2 |
32 | 31 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 1 < 2) |
33 | 21, 5, 23, 30, 32 | lttrd 10198 |
. . . . . . . . . . . . . . . . . 18
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑥 / ((⌊‘𝑥) + 1)) < 2) |
34 | | chpeq0 24933 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 / ((⌊‘𝑥) + 1)) ∈ ℝ →
((ψ‘(𝑥 /
((⌊‘𝑥) + 1))) =
0 ↔ (𝑥 /
((⌊‘𝑥) + 1))
< 2)) |
35 | 21, 34 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((ψ‘(𝑥 / ((⌊‘𝑥) + 1))) = 0 ↔ (𝑥 / ((⌊‘𝑥) + 1)) < 2)) |
36 | 33, 35 | mpbird 247 |
. . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (ψ‘(𝑥 / ((⌊‘𝑥) + 1))) = 0) |
37 | 36 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((ψ‘(𝑥 / ((⌊‘𝑥) + 1))) − (𝑥 / ((⌊‘𝑥) + 1))) = (0 − (𝑥 / ((⌊‘𝑥) + 1)))) |
38 | 20, 37 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑅‘(𝑥 / ((⌊‘𝑥) + 1))) = (0 − (𝑥 / ((⌊‘𝑥) + 1)))) |
39 | 38 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) = (abs‘(0 − (𝑥 / ((⌊‘𝑥) + 1))))) |
40 | | 0red 10041 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 0 ∈ ℝ) |
41 | 17 | rpge0d 11876 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 0 ≤ (𝑥 / ((⌊‘𝑥) + 1))) |
42 | 40, 21, 41 | abssuble0d 14171 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘(0 − (𝑥 / ((⌊‘𝑥) + 1)))) = ((𝑥 / ((⌊‘𝑥) + 1)) − 0)) |
43 | 21 | recnd 10068 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑥 / ((⌊‘𝑥) + 1)) ∈ ℂ) |
44 | 43 | subid1d 10381 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((𝑥 / ((⌊‘𝑥) + 1)) − 0) = (𝑥 / ((⌊‘𝑥) + 1))) |
45 | 39, 42, 44 | 3eqtrd 2660 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) = (𝑥 / ((⌊‘𝑥) + 1))) |
46 | 13 | nn0red 11352 |
. . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (⌊‘𝑥) ∈ ℝ) |
47 | | pntsval.1 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑆 = (𝑎 ∈ ℝ ↦ Σ𝑖 ∈
(1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖))))) |
48 | 47 | pntsval2 25265 |
. . . . . . . . . . . . . . . 16
⊢
((⌊‘𝑥)
∈ ℝ → (𝑆‘(⌊‘𝑥)) = Σ𝑛 ∈
(1...(⌊‘(⌊‘𝑥)))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))))) |
49 | 46, 48 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑆‘(⌊‘𝑥)) = Σ𝑛 ∈
(1...(⌊‘(⌊‘𝑥)))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))))) |
50 | 13 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (⌊‘𝑥) ∈ ℂ) |
51 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 1 ∈ ℂ) |
52 | 50, 51 | pncand 10393 |
. . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((⌊‘𝑥) + 1) − 1) = (⌊‘𝑥)) |
53 | 52 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑆‘(((⌊‘𝑥) + 1) − 1)) = (𝑆‘(⌊‘𝑥))) |
54 | 47 | pntsval2 25265 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℝ → (𝑆‘𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))))) |
55 | 2, 54 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑆‘𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))))) |
56 | | flidm 12610 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℝ →
(⌊‘(⌊‘𝑥)) = (⌊‘𝑥)) |
57 | 2, 56 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (⌊‘(⌊‘𝑥)) = (⌊‘𝑥)) |
58 | 57 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (1...(⌊‘(⌊‘𝑥))) = (1...(⌊‘𝑥))) |
59 | 58 | sumeq1d 14431 |
. . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘(⌊‘𝑥)))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))))) |
60 | 55, 59 | eqtr4d 2659 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑆‘𝑥) = Σ𝑛 ∈
(1...(⌊‘(⌊‘𝑥)))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))))) |
61 | 49, 53, 60 | 3eqtr4d 2666 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑆‘(((⌊‘𝑥) + 1) − 1)) = (𝑆‘𝑥)) |
62 | 52 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑇‘(((⌊‘𝑥) + 1) − 1)) = (𝑇‘(⌊‘𝑥))) |
63 | 62 | oveq2d 6666 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1))) = (2 · (𝑇‘(⌊‘𝑥)))) |
64 | 61, 63 | oveq12d 6668 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1)))) = ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) |
65 | 45, 64 | oveq12d 6668 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) · ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1))))) = ((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))))) |
66 | 2 | recnd 10068 |
. . . . . . . . . . . . . . . . . . 19
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 𝑥 ∈ ℂ) |
67 | 66 | div1d 10793 |
. . . . . . . . . . . . . . . . . 18
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑥 / 1) = 𝑥) |
68 | 67 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑅‘(𝑥 / 1)) = (𝑅‘𝑥)) |
69 | 18 | pntrf 25252 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑅:ℝ+⟶ℝ |
70 | 69 | ffvelrni 6358 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℝ+
→ (𝑅‘𝑥) ∈
ℝ) |
71 | 10, 70 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑅‘𝑥) ∈ ℝ) |
72 | 68, 71 | eqeltrd 2701 |
. . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑅‘(𝑥 / 1)) ∈ ℝ) |
73 | 72 | recnd 10068 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑅‘(𝑥 / 1)) ∈ ℂ) |
74 | 73 | abscld 14175 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘(𝑅‘(𝑥 / 1))) ∈ ℝ) |
75 | 74 | recnd 10068 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘(𝑅‘(𝑥 / 1))) ∈ ℂ) |
76 | 75 | mul01d 10235 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((abs‘(𝑅‘(𝑥 / 1))) · 0) = 0) |
77 | 65, 76 | oveq12d 6668 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) · ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1))))) −
((abs‘(𝑅‘(𝑥 / 1))) · 0)) = (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) − 0)) |
78 | 47 | pntsf 25262 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑆:ℝ⟶ℝ |
79 | 78 | ffvelrni 6358 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℝ → (𝑆‘𝑥) ∈ ℝ) |
80 | 2, 79 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑆‘𝑥) ∈ ℝ) |
81 | | pntrlog2bnd.t |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑇 = (𝑎 ∈ ℝ ↦ if(𝑎 ∈ ℝ+, (𝑎 · (log‘𝑎)), 0)) |
82 | | relogcl 24322 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 ∈ ℝ+
→ (log‘𝑎) ∈
ℝ) |
83 | | remulcl 10021 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎 ∈ ℝ ∧
(log‘𝑎) ∈
ℝ) → (𝑎 ·
(log‘𝑎)) ∈
ℝ) |
84 | 82, 83 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 ∈ ℝ ∧ 𝑎 ∈ ℝ+)
→ (𝑎 ·
(log‘𝑎)) ∈
ℝ) |
85 | | 0red 10041 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 ∈ ℝ ∧ ¬
𝑎 ∈
ℝ+) → 0 ∈ ℝ) |
86 | 84, 85 | ifclda 4120 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 ∈ ℝ → if(𝑎 ∈ ℝ+,
(𝑎 ·
(log‘𝑎)), 0) ∈
ℝ) |
87 | 81, 86 | fmpti 6383 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑇:ℝ⟶ℝ |
88 | 87 | ffvelrni 6358 |
. . . . . . . . . . . . . . . . 17
⊢
((⌊‘𝑥)
∈ ℝ → (𝑇‘(⌊‘𝑥)) ∈ ℝ) |
89 | 46, 88 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑇‘(⌊‘𝑥)) ∈ ℝ) |
90 | 23, 89 | remulcld 10070 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (2 · (𝑇‘(⌊‘𝑥))) ∈ ℝ) |
91 | 80, 90 | resubcld 10458 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) ∈ ℝ) |
92 | 21, 91 | remulcld 10070 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) ∈ ℝ) |
93 | 92 | recnd 10068 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) ∈ ℂ) |
94 | 93 | subid1d 10381 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) − 0) = ((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))))) |
95 | 77, 94 | eqtrd 2656 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) · ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1))))) −
((abs‘(𝑅‘(𝑥 / 1))) · 0)) = ((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))))) |
96 | 2 | flcld 12599 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (⌊‘𝑥) ∈ ℤ) |
97 | | fzval3 12536 |
. . . . . . . . . . . . . 14
⊢
((⌊‘𝑥)
∈ ℤ → (1...(⌊‘𝑥)) = (1..^((⌊‘𝑥) + 1))) |
98 | 96, 97 | syl 17 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (1...(⌊‘𝑥)) = (1..^((⌊‘𝑥) + 1))) |
99 | 98 | eqcomd 2628 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (1..^((⌊‘𝑥) + 1)) = (1...(⌊‘𝑥))) |
100 | 10 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ+) |
101 | | elfznn 12370 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℕ) |
102 | 101 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ) |
103 | 102 | nnrpd 11870 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ+) |
104 | 100, 103 | rpdivcld 11889 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈
ℝ+) |
105 | 69 | ffvelrni 6358 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 / 𝑛) ∈ ℝ+ → (𝑅‘(𝑥 / 𝑛)) ∈ ℝ) |
106 | 104, 105 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘(𝑥 / 𝑛)) ∈ ℝ) |
107 | 106 | recnd 10068 |
. . . . . . . . . . . . . . . . . 18
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘(𝑥 / 𝑛)) ∈ ℂ) |
108 | 107 | abscld 14175 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑅‘(𝑥 / 𝑛))) ∈ ℝ) |
109 | 108 | recnd 10068 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑅‘(𝑥 / 𝑛))) ∈ ℂ) |
110 | 3 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈
ℝ+) |
111 | 103, 110 | rpaddcld 11887 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 + 1) ∈
ℝ+) |
112 | 100, 111 | rpdivcld 11889 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / (𝑛 + 1)) ∈
ℝ+) |
113 | 69 | ffvelrni 6358 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 / (𝑛 + 1)) ∈ ℝ+ →
(𝑅‘(𝑥 / (𝑛 + 1))) ∈ ℝ) |
114 | 112, 113 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘(𝑥 / (𝑛 + 1))) ∈ ℝ) |
115 | 114 | recnd 10068 |
. . . . . . . . . . . . . . . . . 18
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘(𝑥 / (𝑛 + 1))) ∈ ℂ) |
116 | 115 | abscld 14175 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) ∈ ℝ) |
117 | 116 | recnd 10068 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) ∈ ℂ) |
118 | 109, 117 | negsubdi2d 10408 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → -((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) = ((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛))))) |
119 | 118 | eqcomd 2628 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))) = -((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1)))))) |
120 | 102 | nncnd 11036 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℂ) |
121 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈
ℂ) |
122 | 120, 121 | pncand 10393 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) − 1) = 𝑛) |
123 | 122 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘((𝑛 + 1) − 1)) = (𝑆‘𝑛)) |
124 | 122 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇‘((𝑛 + 1) − 1)) = (𝑇‘𝑛)) |
125 | | rpre 11839 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ ℝ+
→ 𝑛 ∈
ℝ) |
126 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 = 𝑛 → (𝑎 ∈ ℝ+ ↔ 𝑛 ∈
ℝ+)) |
127 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑎 = 𝑛 → 𝑎 = 𝑛) |
128 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑎 = 𝑛 → (log‘𝑎) = (log‘𝑛)) |
129 | 127, 128 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 = 𝑛 → (𝑎 · (log‘𝑎)) = (𝑛 · (log‘𝑛))) |
130 | 126, 129 | ifbieq1d 4109 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 = 𝑛 → if(𝑎 ∈ ℝ+, (𝑎 · (log‘𝑎)), 0) = if(𝑛 ∈ ℝ+, (𝑛 · (log‘𝑛)), 0)) |
131 | | ovex 6678 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 · (log‘𝑛)) ∈ V |
132 | | c0ex 10034 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 0 ∈
V |
133 | 131, 132 | ifex 4156 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ if(𝑛 ∈ ℝ+,
(𝑛 ·
(log‘𝑛)), 0) ∈
V |
134 | 130, 81, 133 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ ℝ → (𝑇‘𝑛) = if(𝑛 ∈ ℝ+, (𝑛 · (log‘𝑛)), 0)) |
135 | 125, 134 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℝ+
→ (𝑇‘𝑛) = if(𝑛 ∈ ℝ+, (𝑛 · (log‘𝑛)), 0)) |
136 | | iftrue 4092 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℝ+
→ if(𝑛 ∈
ℝ+, (𝑛
· (log‘𝑛)), 0)
= (𝑛 ·
(log‘𝑛))) |
137 | 135, 136 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℝ+
→ (𝑇‘𝑛) = (𝑛 · (log‘𝑛))) |
138 | 103, 137 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇‘𝑛) = (𝑛 · (log‘𝑛))) |
139 | 124, 138 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇‘((𝑛 + 1) − 1)) = (𝑛 · (log‘𝑛))) |
140 | 139 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑇‘((𝑛 + 1) − 1))) = (2 · (𝑛 · (log‘𝑛)))) |
141 | 123, 140 | oveq12d 6668 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))) = ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) |
142 | 119, 141 | oveq12d 6668 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))) · ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1))))) = (-((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) |
143 | 108, 116 | resubcld 10458 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) ∈ ℝ) |
144 | 143 | recnd 10068 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) ∈ ℂ) |
145 | 102 | nnred 11035 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ) |
146 | 78 | ffvelrni 6358 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℝ → (𝑆‘𝑛) ∈ ℝ) |
147 | 145, 146 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘𝑛) ∈ ℝ) |
148 | 22 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 2 ∈
ℝ) |
149 | 103 | relogcld 24369 |
. . . . . . . . . . . . . . . . . 18
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘𝑛) ∈
ℝ) |
150 | 145, 149 | remulcld 10070 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 · (log‘𝑛)) ∈ ℝ) |
151 | 148, 150 | remulcld 10070 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑛 · (log‘𝑛))) ∈
ℝ) |
152 | 147, 151 | resubcld 10458 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))) ∈ ℝ) |
153 | 152 | recnd 10068 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))) ∈ ℂ) |
154 | 144, 153 | mulneg1d 10483 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (-((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) = -(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) |
155 | 142, 154 | eqtrd 2656 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))) · ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1))))) = -(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) |
156 | 99, 155 | sumeq12rdv 14438 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))(((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))) · ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1))))) = Σ𝑛 ∈
(1...(⌊‘𝑥))-(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) |
157 | | fzfid 12772 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (1...(⌊‘𝑥)) ∈ Fin) |
158 | 143, 152 | remulcld 10070 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) ∈ ℝ) |
159 | 158 | recnd 10068 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) ∈ ℂ) |
160 | 157, 159 | fsumneg 14519 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))-(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) = -Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) |
161 | 156, 160 | eqtrd 2656 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))(((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))) · ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1))))) = -Σ𝑛 ∈
(1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) |
162 | 95, 161 | oveq12d 6668 |
. . . . . . . . 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 6658 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑛 → (𝑥 / 𝑚) = (𝑥 / 𝑛)) |
164 | 163 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑛 → (𝑅‘(𝑥 / 𝑚)) = (𝑅‘(𝑥 / 𝑛))) |
165 | 164 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → (abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / 𝑛)))) |
166 | | oveq1 6657 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑛 → (𝑚 − 1) = (𝑛 − 1)) |
167 | 166 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑛 → (𝑆‘(𝑚 − 1)) = (𝑆‘(𝑛 − 1))) |
168 | 166 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑛 → (𝑇‘(𝑚 − 1)) = (𝑇‘(𝑛 − 1))) |
169 | 168 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑛 → (2 · (𝑇‘(𝑚 − 1))) = (2 · (𝑇‘(𝑛 − 1)))) |
170 | 167, 169 | oveq12d 6668 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1))))) |
171 | 165, 170 | jca 554 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → ((abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / 𝑛))) ∧ ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1)))))) |
172 | | oveq2 6658 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = (𝑛 + 1) → (𝑥 / 𝑚) = (𝑥 / (𝑛 + 1))) |
173 | 172 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝑚 = (𝑛 + 1) → (𝑅‘(𝑥 / 𝑚)) = (𝑅‘(𝑥 / (𝑛 + 1)))) |
174 | 173 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝑚 = (𝑛 + 1) → (abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) |
175 | | oveq1 6657 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = (𝑛 + 1) → (𝑚 − 1) = ((𝑛 + 1) − 1)) |
176 | 175 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝑚 = (𝑛 + 1) → (𝑆‘(𝑚 − 1)) = (𝑆‘((𝑛 + 1) − 1))) |
177 | 175 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = (𝑛 + 1) → (𝑇‘(𝑚 − 1)) = (𝑇‘((𝑛 + 1) − 1))) |
178 | 177 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢ (𝑚 = (𝑛 + 1) → (2 · (𝑇‘(𝑚 − 1))) = (2 · (𝑇‘((𝑛 + 1) − 1)))) |
179 | 176, 178 | oveq12d 6668 |
. . . . . . . . . . . 12
⊢ (𝑚 = (𝑛 + 1) → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1))))) |
180 | 174, 179 | jca 554 |
. . . . . . . . . . 11
⊢ (𝑚 = (𝑛 + 1) → ((abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) ∧ ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))))) |
181 | | oveq2 6658 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 1 → (𝑥 / 𝑚) = (𝑥 / 1)) |
182 | 181 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 1 → (𝑅‘(𝑥 / 𝑚)) = (𝑅‘(𝑥 / 1))) |
183 | 182 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝑚 = 1 → (abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / 1)))) |
184 | | oveq1 6657 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 = 1 → (𝑚 − 1) = (1 − 1)) |
185 | | 1m1e0 11089 |
. . . . . . . . . . . . . . . . 17
⊢ (1
− 1) = 0 |
186 | 184, 185 | syl6eq 2672 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 = 1 → (𝑚 − 1) = 0) |
187 | 186 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = 1 → (𝑆‘(𝑚 − 1)) = (𝑆‘0)) |
188 | | 0re 10040 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℝ |
189 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 = 0 → (⌊‘𝑎) =
(⌊‘0)) |
190 | | 0z 11388 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 0 ∈
ℤ |
191 | | flid 12609 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (0 ∈
ℤ → (⌊‘0) = 0) |
192 | 190, 191 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(⌊‘0) = 0 |
193 | 189, 192 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 = 0 → (⌊‘𝑎) = 0) |
194 | 193 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 = 0 →
(1...(⌊‘𝑎)) =
(1...0)) |
195 | | fz10 12362 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (1...0) =
∅ |
196 | 194, 195 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = 0 →
(1...(⌊‘𝑎)) =
∅) |
197 | 196 | sumeq1d 14431 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = 0 → Σ𝑖 ∈
(1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))) = Σ𝑖 ∈ ∅ ((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖))))) |
198 | | sum0 14452 |
. . . . . . . . . . . . . . . . . 18
⊢
Σ𝑖 ∈
∅ ((Λ‘𝑖)
· ((log‘𝑖) +
(ψ‘(𝑎 / 𝑖)))) = 0 |
199 | 197, 198 | syl6eq 2672 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = 0 → Σ𝑖 ∈
(1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))) = 0) |
200 | 199, 47, 132 | fvmpt 6282 |
. . . . . . . . . . . . . . . 16
⊢ (0 ∈
ℝ → (𝑆‘0)
= 0) |
201 | 188, 200 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ (𝑆‘0) = 0 |
202 | 187, 201 | syl6eq 2672 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 1 → (𝑆‘(𝑚 − 1)) = 0) |
203 | 186 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 = 1 → (𝑇‘(𝑚 − 1)) = (𝑇‘0)) |
204 | | rpne0 11848 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 ∈ ℝ+
→ 𝑎 ≠
0) |
205 | 204 | necon2bi 2824 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 = 0 → ¬ 𝑎 ∈
ℝ+) |
206 | 205 | iffalsed 4097 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = 0 → if(𝑎 ∈ ℝ+,
(𝑎 ·
(log‘𝑎)), 0) =
0) |
207 | 206, 81, 132 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . 18
⊢ (0 ∈
ℝ → (𝑇‘0)
= 0) |
208 | 188, 207 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑇‘0) = 0 |
209 | 203, 208 | syl6eq 2672 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 = 1 → (𝑇‘(𝑚 − 1)) = 0) |
210 | 209 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = 1 → (2 · (𝑇‘(𝑚 − 1))) = (2 ·
0)) |
211 | | 2t0e0 11183 |
. . . . . . . . . . . . . . 15
⊢ (2
· 0) = 0 |
212 | 210, 211 | syl6eq 2672 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 1 → (2 · (𝑇‘(𝑚 − 1))) = 0) |
213 | 202, 212 | oveq12d 6668 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 1 → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = (0 −
0)) |
214 | | 0m0e0 11130 |
. . . . . . . . . . . . 13
⊢ (0
− 0) = 0 |
215 | 213, 214 | syl6eq 2672 |
. . . . . . . . . . . 12
⊢ (𝑚 = 1 → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = 0) |
216 | 183, 215 | jca 554 |
. . . . . . . . . . 11
⊢ (𝑚 = 1 → ((abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / 1))) ∧ ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = 0)) |
217 | | oveq2 6658 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = ((⌊‘𝑥) + 1) → (𝑥 / 𝑚) = (𝑥 / ((⌊‘𝑥) + 1))) |
218 | 217 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝑚 = ((⌊‘𝑥) + 1) → (𝑅‘(𝑥 / 𝑚)) = (𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) |
219 | 218 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝑚 = ((⌊‘𝑥) + 1) → (abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1))))) |
220 | | oveq1 6657 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = ((⌊‘𝑥) + 1) → (𝑚 − 1) =
(((⌊‘𝑥) + 1)
− 1)) |
221 | 220 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝑚 = ((⌊‘𝑥) + 1) → (𝑆‘(𝑚 − 1)) = (𝑆‘(((⌊‘𝑥) + 1) − 1))) |
222 | 220 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = ((⌊‘𝑥) + 1) → (𝑇‘(𝑚 − 1)) = (𝑇‘(((⌊‘𝑥) + 1) − 1))) |
223 | 222 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢ (𝑚 = ((⌊‘𝑥) + 1) → (2 · (𝑇‘(𝑚 − 1))) = (2 · (𝑇‘(((⌊‘𝑥) + 1) −
1)))) |
224 | 221, 223 | oveq12d 6668 |
. . . . . . . . . . . 12
⊢ (𝑚 = ((⌊‘𝑥) + 1) → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) −
1))))) |
225 | 219, 224 | jca 554 |
. . . . . . . . . . 11
⊢ (𝑚 = ((⌊‘𝑥) + 1) → ((abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) ∧ ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) −
1)))))) |
226 | | nnuz 11723 |
. . . . . . . . . . . 12
⊢ ℕ =
(ℤ≥‘1) |
227 | 15, 226 | syl6eleq 2711 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((⌊‘𝑥) + 1) ∈
(ℤ≥‘1)) |
228 | 10 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 𝑥 ∈
ℝ+) |
229 | | elfznn 12370 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ∈
(1...((⌊‘𝑥) +
1)) → 𝑚 ∈
ℕ) |
230 | 229 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 𝑚 ∈
ℕ) |
231 | 230 | nnrpd 11870 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 𝑚 ∈
ℝ+) |
232 | 228, 231 | rpdivcld 11889 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑥 / 𝑚) ∈
ℝ+) |
233 | 69 | ffvelrni 6358 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 / 𝑚) ∈ ℝ+ → (𝑅‘(𝑥 / 𝑚)) ∈ ℝ) |
234 | 232, 233 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑅‘(𝑥 / 𝑚)) ∈ ℝ) |
235 | 234 | recnd 10068 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑅‘(𝑥 / 𝑚)) ∈ ℂ) |
236 | 235 | abscld 14175 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) →
(abs‘(𝑅‘(𝑥 / 𝑚))) ∈ ℝ) |
237 | 236 | recnd 10068 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) →
(abs‘(𝑅‘(𝑥 / 𝑚))) ∈ ℂ) |
238 | 230 | nnred 11035 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 𝑚 ∈
ℝ) |
239 | | 1red 10055 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 1 ∈
ℝ) |
240 | 238, 239 | resubcld 10458 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑚 − 1) ∈
ℝ) |
241 | 78 | ffvelrni 6358 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 − 1) ∈ ℝ
→ (𝑆‘(𝑚 − 1)) ∈
ℝ) |
242 | 240, 241 | syl 17 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑆‘(𝑚 − 1)) ∈ ℝ) |
243 | 22 | a1i 11 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 2 ∈
ℝ) |
244 | 87 | ffvelrni 6358 |
. . . . . . . . . . . . . . 15
⊢ ((𝑚 − 1) ∈ ℝ
→ (𝑇‘(𝑚 − 1)) ∈
ℝ) |
245 | 240, 244 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑇‘(𝑚 − 1)) ∈ ℝ) |
246 | 243, 245 | remulcld 10070 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (2 ·
(𝑇‘(𝑚 − 1))) ∈
ℝ) |
247 | 242, 246 | resubcld 10458 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) ∈
ℝ) |
248 | 247 | recnd 10068 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) ∈
ℂ) |
249 | 171, 180,
216, 225, 227, 237, 248 | fsumparts 14538 |
. . . . . . . . . 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))))))) |
250 | 147 | recnd 10068 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘𝑛) ∈ ℂ) |
251 | 87 | ffvelrni 6358 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℝ → (𝑇‘𝑛) ∈ ℝ) |
252 | 145, 251 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇‘𝑛) ∈ ℝ) |
253 | 148, 252 | remulcld 10070 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑇‘𝑛)) ∈ ℝ) |
254 | 253 | recnd 10068 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑇‘𝑛)) ∈ ℂ) |
255 | | 1red 10055 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈
ℝ) |
256 | 145, 255 | resubcld 10458 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 − 1) ∈ ℝ) |
257 | 78 | ffvelrni 6358 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 − 1) ∈ ℝ
→ (𝑆‘(𝑛 − 1)) ∈
ℝ) |
258 | 256, 257 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘(𝑛 − 1)) ∈ ℝ) |
259 | 258 | recnd 10068 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘(𝑛 − 1)) ∈ ℂ) |
260 | 87 | ffvelrni 6358 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 − 1) ∈ ℝ
→ (𝑇‘(𝑛 − 1)) ∈
ℝ) |
261 | 256, 260 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇‘(𝑛 − 1)) ∈ ℝ) |
262 | 148, 261 | remulcld 10070 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑇‘(𝑛 − 1))) ∈
ℝ) |
263 | 262 | recnd 10068 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑇‘(𝑛 − 1))) ∈
ℂ) |
264 | 250, 254,
259, 263 | sub4d 10441 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆‘𝑛) − (2 · (𝑇‘𝑛))) − ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1))))) = (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − ((2 · (𝑇‘𝑛)) − (2 · (𝑇‘(𝑛 − 1)))))) |
265 | 124 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑇‘((𝑛 + 1) − 1))) = (2 · (𝑇‘𝑛))) |
266 | 123, 265 | oveq12d 6668 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))) = ((𝑆‘𝑛) − (2 · (𝑇‘𝑛)))) |
267 | 266 | oveq1d 6665 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))) − ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1))))) = (((𝑆‘𝑛) − (2 · (𝑇‘𝑛))) − ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1)))))) |
268 | | 2cnd 11093 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 2 ∈
ℂ) |
269 | 252 | recnd 10068 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇‘𝑛) ∈ ℂ) |
270 | 261 | recnd 10068 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇‘(𝑛 − 1)) ∈ ℂ) |
271 | 268, 269,
270 | subdid 10486 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))) = ((2 · (𝑇‘𝑛)) − (2 · (𝑇‘(𝑛 − 1))))) |
272 | 271 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))) = (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − ((2 · (𝑇‘𝑛)) − (2 · (𝑇‘(𝑛 − 1)))))) |
273 | 264, 267,
272 | 3eqtr4d 2666 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))) − ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1))))) = (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) |
274 | 273 | oveq2d 6666 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))) − ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1)))))) = ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) |
275 | 99, 274 | sumeq12rdv 14438 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))) − ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1)))))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) |
276 | 249, 275 | eqtr3d 2658 |
. . . . . . . . 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))))))) |
277 | 157, 159 | fsumcl 14464 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) ∈ ℂ) |
278 | 93, 277 | subnegd 10399 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) − -Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) = (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))))) |
279 | 162, 276,
278 | 3eqtr3rd 2665 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) |
280 | 10 | relogcld 24369 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (log‘𝑥) ∈ ℝ) |
281 | 280 | recnd 10068 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (log‘𝑥) ∈ ℂ) |
282 | 66, 281 | mulcomd 10061 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) = ((log‘𝑥) · 𝑥)) |
283 | 279, 282 | oveq12d 6668 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / ((log‘𝑥) · 𝑥))) |
284 | 147, 258 | resubcld 10458 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) ∈
ℝ) |
285 | 252, 261 | resubcld 10458 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))) ∈
ℝ) |
286 | 148, 285 | remulcld 10070 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))) ∈
ℝ) |
287 | 284, 286 | resubcld 10458 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))) ∈
ℝ) |
288 | 108, 287 | remulcld 10070 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) ∈
ℝ) |
289 | 157, 288 | fsumrecl 14465 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) ∈
ℝ) |
290 | 289 | recnd 10068 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) ∈
ℂ) |
291 | 2, 8 | rplogcld 24375 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (log‘𝑥) ∈
ℝ+) |
292 | 291 | rpne0d 11877 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (log‘𝑥) ≠ 0) |
293 | 10 | rpne0d 11877 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 𝑥 ≠ 0) |
294 | 290, 281,
66, 292, 293 | divdiv1d 10832 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥)) / 𝑥) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / ((log‘𝑥) · 𝑥))) |
295 | 283, 294 | eqtr4d 2659 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥)) / 𝑥)) |
296 | 295 | oveq2d 6666 |
. . . . 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‘𝑥)) / 𝑥))) |
297 | 71 | recnd 10068 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑅‘𝑥) ∈ ℂ) |
298 | 297 | abscld 14175 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘(𝑅‘𝑥)) ∈ ℝ) |
299 | 298, 280 | remulcld 10070 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((abs‘(𝑅‘𝑥)) · (log‘𝑥)) ∈ ℝ) |
300 | 108, 284 | remulcld 10070 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) ∈
ℝ) |
301 | 157, 300 | fsumrecl 14465 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) ∈
ℝ) |
302 | 301, 291 | rerpdivcld 11903 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥)) ∈
ℝ) |
303 | 299, 302 | resubcld 10458 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) ∈
ℝ) |
304 | 303 | recnd 10068 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) ∈
ℂ) |
305 | 290, 281,
292 | divcld 10801 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥)) ∈
ℂ) |
306 | 304, 305,
66, 293 | divdird 10839 |
. . . . 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‘𝑥)) / 𝑥))) |
307 | 299 | recnd 10068 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((abs‘(𝑅‘𝑥)) · (log‘𝑥)) ∈ ℂ) |
308 | 302 | recnd 10068 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥)) ∈
ℂ) |
309 | 307, 308,
305 | subsubd 10420 |
. . . . . . 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‘𝑥)))) |
310 | | 2cnd 11093 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 2 ∈ ℂ) |
311 | 269, 270 | subcld 10392 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))) ∈
ℂ) |
312 | 109, 311 | mulcld 10060 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))) ∈
ℂ) |
313 | 157, 310,
312 | fsummulc2 14516 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(2 · ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) |
314 | 284 | recnd 10068 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) ∈
ℂ) |
315 | 268, 311 | mulcld 10060 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))) ∈
ℂ) |
316 | 314, 315 | nncand 10397 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) = (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))) |
317 | 316 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) = ((abs‘(𝑅‘(𝑥 / 𝑛))) · (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) |
318 | 287 | recnd 10068 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))) ∈
ℂ) |
319 | 109, 314,
318 | subdid 10486 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) = (((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) − ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))))) |
320 | 109, 268,
311 | mul12d 10245 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))) = (2 ·
((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) |
321 | 317, 319,
320 | 3eqtr3d 2664 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) − ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) = (2 ·
((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) |
322 | 321 | sumeq2dv 14433 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) − ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(2 · ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) |
323 | 300 | recnd 10068 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) ∈
ℂ) |
324 | 288 | recnd 10068 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) ∈
ℂ) |
325 | 157, 323,
324 | fsumsub 14520 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) − ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) = (Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) − Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))))) |
326 | 313, 322,
325 | 3eqtr2rd 2663 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) − Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) = (2 · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) |
327 | 326 | oveq1d 6665 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) − Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) / (log‘𝑥)) = ((2 · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))) / (log‘𝑥))) |
328 | 301 | recnd 10068 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) ∈
ℂ) |
329 | 328, 290,
281, 292 | divsubdird 10840 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) − Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) / (log‘𝑥)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥)) − (Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥)))) |
330 | 108, 285 | remulcld 10070 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))) ∈
ℝ) |
331 | 157, 330 | fsumrecl 14465 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))) ∈
ℝ) |
332 | 331 | recnd 10068 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))) ∈
ℂ) |
333 | 310, 332,
281, 292 | div23d 10838 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))) / (log‘𝑥)) = ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) |
334 | 327, 329,
333 | 3eqtr3d 2664 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥)) − (Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥))) = ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) |
335 | 334 | oveq2d 6666 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥)) − (Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥)))) = (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) |
336 | 309, 335 | eqtr3d 2658 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥))) = (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) |
337 | 336 | oveq1d 6665 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥))) / 𝑥) = ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / 𝑥)) |
338 | 296, 306,
337 | 3eqtr2d 2662 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥) + ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥)))) = ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / 𝑥)) |
339 | 338 | mpteq2dva 4744 |
. . 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)))))) / 𝑥))) |
340 | 303, 10 | rerpdivcld 11903 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥) ∈ ℝ) |
341 | 157, 158 | fsumrecl 14465 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) ∈ ℝ) |
342 | 92, 341 | readdcld 10069 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) ∈ ℝ) |
343 | 10, 291 | rpmulcld 11888 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ∈
ℝ+) |
344 | 342, 343 | rerpdivcld 11903 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))) ∈ ℝ) |
345 | 47, 18 | pntrlog2bndlem1 25266 |
. . . . 5
⊢ (𝑥 ∈ (1(,)+∞) ↦
((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥)) ∈ ≤𝑂(1) |
346 | 345 | a1i 11 |
. . . 4
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥)) ∈ ≤𝑂(1)) |
347 | 343 | rpcnd 11874 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ∈ ℂ) |
348 | 343 | rpne0d 11877 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ≠ 0) |
349 | 93, 277, 347, 348 | divdird 10839 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))) = ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) / (𝑥 · (log‘𝑥))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥))))) |
350 | 91 | recnd 10068 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) ∈ ℂ) |
351 | 43, 350, 347, 348 | divassd 10836 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) / (𝑥 · (log‘𝑥))) = ((𝑥 / ((⌊‘𝑥) + 1)) · (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥))))) |
352 | 351 | oveq1d 6665 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) / (𝑥 · (log‘𝑥))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥)))) = (((𝑥 / ((⌊‘𝑥) + 1)) · (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥))))) |
353 | 349, 352 | eqtrd 2656 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))) = (((𝑥 / ((⌊‘𝑥) + 1)) · (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥))))) |
354 | 353 | mpteq2dva 4744 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥)))) = (𝑥 ∈ (1(,)+∞) ↦ (((𝑥 / ((⌊‘𝑥) + 1)) · (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥)))))) |
355 | 91, 343 | rerpdivcld 11903 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥))) ∈ ℝ) |
356 | 21, 355 | remulcld 10070 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((𝑥 / ((⌊‘𝑥) + 1)) · (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) ∈ ℝ) |
357 | 341, 343 | rerpdivcld 11903 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥))) ∈ ℝ) |
358 | | ioossre 12235 |
. . . . . . . . 9
⊢
(1(,)+∞) ⊆ ℝ |
359 | 358 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ (1(,)+∞) ⊆ ℝ) |
360 | | 1red 10055 |
. . . . . . . 8
⊢ (⊤
→ 1 ∈ ℝ) |
361 | 21, 5, 30 | ltled 10185 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑥 / ((⌊‘𝑥) + 1)) ≤ 1) |
362 | 361 | adantrr 753 |
. . . . . . . 8
⊢
((⊤ ∧ (𝑥
∈ (1(,)+∞) ∧ 1 ≤ 𝑥)) → (𝑥 / ((⌊‘𝑥) + 1)) ≤ 1) |
363 | 359, 21, 360, 360, 362 | ello1d 14254 |
. . . . . . 7
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (𝑥 /
((⌊‘𝑥) + 1)))
∈ ≤𝑂(1)) |
364 | 80 | recnd 10068 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑆‘𝑥) ∈ ℂ) |
365 | 90 | recnd 10068 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (2 · (𝑇‘(⌊‘𝑥))) ∈ ℂ) |
366 | 364, 365,
347, 348 | divsubdird 10840 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥))) = (((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) − ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥))))) |
367 | 366 | mpteq2dva 4744 |
. . . . . . . . 9
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) = (𝑥 ∈ (1(,)+∞) ↦ (((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) − ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥)))))) |
368 | 80, 343 | rerpdivcld 11903 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) ∈ ℝ) |
369 | 90, 343 | rerpdivcld 11903 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥))) ∈ ℝ) |
370 | | 2cnd 11093 |
. . . . . . . . . . . 12
⊢ (⊤
→ 2 ∈ ℂ) |
371 | | o1const 14350 |
. . . . . . . . . . . 12
⊢
(((1(,)+∞) ⊆ ℝ ∧ 2 ∈ ℂ) → (𝑥 ∈ (1(,)+∞) ↦
2) ∈ 𝑂(1)) |
372 | 358, 370,
371 | sylancr 695 |
. . . . . . . . . . 11
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ 2) ∈ 𝑂(1)) |
373 | 368 | recnd 10068 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) ∈ ℂ) |
374 | 80, 10 | rerpdivcld 11903 |
. . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((𝑆‘𝑥) / 𝑥) ∈ ℝ) |
375 | 374 | recnd 10068 |
. . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((𝑆‘𝑥) / 𝑥) ∈ ℂ) |
376 | 310, 281 | mulcld 10060 |
. . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (2 · (log‘𝑥)) ∈ ℂ) |
377 | 375, 376,
281, 292 | divsubdird 10840 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥))) / (log‘𝑥)) = ((((𝑆‘𝑥) / 𝑥) / (log‘𝑥)) − ((2 · (log‘𝑥)) / (log‘𝑥)))) |
378 | 23, 280 | remulcld 10070 |
. . . . . . . . . . . . . . . . . 18
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (2 · (log‘𝑥)) ∈ ℝ) |
379 | 374, 378 | resubcld 10458 |
. . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥))) ∈
ℝ) |
380 | 379 | recnd 10068 |
. . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥))) ∈
ℂ) |
381 | 380, 281,
292 | divrecd 10804 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥))) / (log‘𝑥)) = ((((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥))) · (1 /
(log‘𝑥)))) |
382 | 364, 66, 281, 293, 292 | divdiv1d 10832 |
. . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((𝑆‘𝑥) / 𝑥) / (log‘𝑥)) = ((𝑆‘𝑥) / (𝑥 · (log‘𝑥)))) |
383 | 310, 281,
292 | divcan4d 10807 |
. . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((2 · (log‘𝑥)) / (log‘𝑥)) = 2) |
384 | 382, 383 | oveq12d 6668 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((𝑆‘𝑥) / 𝑥) / (log‘𝑥)) − ((2 · (log‘𝑥)) / (log‘𝑥))) = (((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) − 2)) |
385 | 377, 381,
384 | 3eqtr3rd 2665 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) − 2) = ((((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥))) · (1 /
(log‘𝑥)))) |
386 | 385 | mpteq2dva 4744 |
. . . . . . . . . . . . 13
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) − 2)) = (𝑥 ∈ (1(,)+∞) ↦ ((((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥))) · (1 /
(log‘𝑥))))) |
387 | 5, 291 | rerpdivcld 11903 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (1 / (log‘𝑥)) ∈ ℝ) |
388 | 10 | ex 450 |
. . . . . . . . . . . . . . . 16
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) → 𝑥
∈ ℝ+)) |
389 | 388 | ssrdv 3609 |
. . . . . . . . . . . . . . 15
⊢ (⊤
→ (1(,)+∞) ⊆ ℝ+) |
390 | 47 | selbergs 25263 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℝ+
↦ (((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥)))) ∈
𝑂(1) |
391 | 390 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥)))) ∈
𝑂(1)) |
392 | 389, 391 | o1res2 14294 |
. . . . . . . . . . . . . 14
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥)))) ∈
𝑂(1)) |
393 | | divlogrlim 24381 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (1(,)+∞) ↦
(1 / (log‘𝑥)))
⇝𝑟 0 |
394 | | rlimo1 14347 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (1(,)+∞) ↦
(1 / (log‘𝑥)))
⇝𝑟 0 → (𝑥 ∈ (1(,)+∞) ↦ (1 /
(log‘𝑥))) ∈
𝑂(1)) |
395 | 393, 394 | mp1i 13 |
. . . . . . . . . . . . . 14
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (1 / (log‘𝑥))) ∈ 𝑂(1)) |
396 | 379, 387,
392, 395 | o1mul2 14355 |
. . . . . . . . . . . . 13
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ ((((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥))) · (1 /
(log‘𝑥)))) ∈
𝑂(1)) |
397 | 386, 396 | eqeltrd 2701 |
. . . . . . . . . . . 12
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) − 2)) ∈
𝑂(1)) |
398 | 373, 310,
397 | o1dif 14360 |
. . . . . . . . . . 11
⊢ (⊤
→ ((𝑥 ∈
(1(,)+∞) ↦ ((𝑆‘𝑥) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1) ↔ (𝑥 ∈ (1(,)+∞) ↦
2) ∈ 𝑂(1))) |
399 | 372, 398 | mpbird 247 |
. . . . . . . . . 10
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ ((𝑆‘𝑥) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1)) |
400 | 22 | a1i 11 |
. . . . . . . . . . . 12
⊢ (⊤
→ 2 ∈ ℝ) |
401 | 2, 280 | remulcld 10070 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ∈ ℝ) |
402 | | 2rp 11837 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℝ+ |
403 | 402 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 2 ∈ ℝ+) |
404 | 403 | rpge0d 11876 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 0 ≤ 2) |
405 | | flge1nn 12622 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℝ ∧ 1 ≤
𝑥) →
(⌊‘𝑥) ∈
ℕ) |
406 | 2, 9, 405 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (⌊‘𝑥) ∈ ℕ) |
407 | 406 | nnrpd 11870 |
. . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (⌊‘𝑥) ∈
ℝ+) |
408 | | rpre 11839 |
. . . . . . . . . . . . . . . . . . 19
⊢
((⌊‘𝑥)
∈ ℝ+ → (⌊‘𝑥) ∈ ℝ) |
409 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 = (⌊‘𝑥) → (𝑎 ∈ ℝ+ ↔
(⌊‘𝑥) ∈
ℝ+)) |
410 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 = (⌊‘𝑥) → 𝑎 = (⌊‘𝑥)) |
411 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 = (⌊‘𝑥) → (log‘𝑎) =
(log‘(⌊‘𝑥))) |
412 | 410, 411 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 = (⌊‘𝑥) → (𝑎 · (log‘𝑎)) = ((⌊‘𝑥) · (log‘(⌊‘𝑥)))) |
413 | 409, 412 | ifbieq1d 4109 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 = (⌊‘𝑥) → if(𝑎 ∈ ℝ+, (𝑎 · (log‘𝑎)), 0) = if((⌊‘𝑥) ∈ ℝ+,
((⌊‘𝑥) ·
(log‘(⌊‘𝑥))), 0)) |
414 | | ovex 6678 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((⌊‘𝑥)
· (log‘(⌊‘𝑥))) ∈ V |
415 | 414, 132 | ifex 4156 |
. . . . . . . . . . . . . . . . . . . 20
⊢
if((⌊‘𝑥)
∈ ℝ+, ((⌊‘𝑥) · (log‘(⌊‘𝑥))), 0) ∈
V |
416 | 413, 81, 415 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . . 19
⊢
((⌊‘𝑥)
∈ ℝ → (𝑇‘(⌊‘𝑥)) = if((⌊‘𝑥) ∈ ℝ+,
((⌊‘𝑥) ·
(log‘(⌊‘𝑥))), 0)) |
417 | 408, 416 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
((⌊‘𝑥)
∈ ℝ+ → (𝑇‘(⌊‘𝑥)) = if((⌊‘𝑥) ∈ ℝ+,
((⌊‘𝑥) ·
(log‘(⌊‘𝑥))), 0)) |
418 | | iftrue 4092 |
. . . . . . . . . . . . . . . . . 18
⊢
((⌊‘𝑥)
∈ ℝ+ → if((⌊‘𝑥) ∈ ℝ+,
((⌊‘𝑥) ·
(log‘(⌊‘𝑥))), 0) = ((⌊‘𝑥) · (log‘(⌊‘𝑥)))) |
419 | 417, 418 | eqtrd 2656 |
. . . . . . . . . . . . . . . . 17
⊢
((⌊‘𝑥)
∈ ℝ+ → (𝑇‘(⌊‘𝑥)) = ((⌊‘𝑥) · (log‘(⌊‘𝑥)))) |
420 | 407, 419 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑇‘(⌊‘𝑥)) = ((⌊‘𝑥) · (log‘(⌊‘𝑥)))) |
421 | 407 | relogcld 24369 |
. . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (log‘(⌊‘𝑥)) ∈ ℝ) |
422 | 13 | nn0ge0d 11354 |
. . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 0 ≤ (⌊‘𝑥)) |
423 | 406 | nnge1d 11063 |
. . . . . . . . . . . . . . . . . 18
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 1 ≤ (⌊‘𝑥)) |
424 | 46, 423 | logge0d 24376 |
. . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 0 ≤ (log‘(⌊‘𝑥))) |
425 | | flle 12600 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℝ →
(⌊‘𝑥) ≤
𝑥) |
426 | 2, 425 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (⌊‘𝑥) ≤ 𝑥) |
427 | 407, 10 | logled 24373 |
. . . . . . . . . . . . . . . . . 18
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((⌊‘𝑥) ≤ 𝑥 ↔ (log‘(⌊‘𝑥)) ≤ (log‘𝑥))) |
428 | 426, 427 | mpbid 222 |
. . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (log‘(⌊‘𝑥)) ≤ (log‘𝑥)) |
429 | 46, 2, 421, 280, 422, 424, 426, 428 | lemul12ad 10966 |
. . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((⌊‘𝑥) · (log‘(⌊‘𝑥))) ≤ (𝑥 · (log‘𝑥))) |
430 | 420, 429 | eqbrtrd 4675 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑇‘(⌊‘𝑥)) ≤ (𝑥 · (log‘𝑥))) |
431 | 89, 401, 23, 404, 430 | lemul2ad 10964 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (2 · (𝑇‘(⌊‘𝑥))) ≤ (2 · (𝑥 · (log‘𝑥)))) |
432 | 90, 23, 343 | ledivmul2d 11926 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥))) ≤ 2 ↔ (2 · (𝑇‘(⌊‘𝑥))) ≤ (2 · (𝑥 · (log‘𝑥))))) |
433 | 431, 432 | mpbird 247 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥))) ≤ 2) |
434 | 433 | adantrr 753 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ (𝑥
∈ (1(,)+∞) ∧ 1 ≤ 𝑥)) → ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥))) ≤ 2) |
435 | 359, 369,
360, 400, 434 | ello1d 14254 |
. . . . . . . . . . 11
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥)))) ∈
≤𝑂(1)) |
436 | | 0red 10041 |
. . . . . . . . . . . 12
⊢ (⊤
→ 0 ∈ ℝ) |
437 | 46, 421, 422, 424 | mulge0d 10604 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 0 ≤ ((⌊‘𝑥) · (log‘(⌊‘𝑥)))) |
438 | 437, 420 | breqtrrd 4681 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 0 ≤ (𝑇‘(⌊‘𝑥))) |
439 | 23, 89, 404, 438 | mulge0d 10604 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 0 ≤ (2 · (𝑇‘(⌊‘𝑥)))) |
440 | 90, 343, 439 | divge0d 11912 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 0 ≤ ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥)))) |
441 | 369, 436,
440 | o1lo12 14269 |
. . . . . . . . . . 11
⊢ (⊤
→ ((𝑥 ∈
(1(,)+∞) ↦ ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1) ↔ (𝑥 ∈ (1(,)+∞) ↦
((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥)))) ∈
≤𝑂(1))) |
442 | 435, 441 | mpbird 247 |
. . . . . . . . . 10
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1)) |
443 | 368, 369,
399, 442 | o1sub2 14356 |
. . . . . . . . 9
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) − ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥))))) ∈ 𝑂(1)) |
444 | 367, 443 | eqeltrd 2701 |
. . . . . . . 8
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1)) |
445 | 355, 444 | o1lo1d 14270 |
. . . . . . 7
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) ∈
≤𝑂(1)) |
446 | 21, 355, 363, 445, 41 | lo1mul 14358 |
. . . . . 6
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ ((𝑥
/ ((⌊‘𝑥) + 1))
· (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥))))) ∈
≤𝑂(1)) |
447 | 47 | selbergsb 25264 |
. . . . . . . 8
⊢
∃𝑐 ∈
ℝ+ ∀𝑦 ∈ (1[,)+∞)(abs‘(((𝑆‘𝑦) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝑐 |
448 | | simpl 473 |
. . . . . . . . . 10
⊢ ((𝑐 ∈ ℝ+
∧ ∀𝑦 ∈
(1[,)+∞)(abs‘(((𝑆‘𝑦) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝑐) → 𝑐 ∈ ℝ+) |
449 | | simpr 477 |
. . . . . . . . . 10
⊢ ((𝑐 ∈ ℝ+
∧ ∀𝑦 ∈
(1[,)+∞)(abs‘(((𝑆‘𝑦) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝑐) → ∀𝑦 ∈ (1[,)+∞)(abs‘(((𝑆‘𝑦) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝑐) |
450 | 47, 18, 448, 449 | pntrlog2bndlem3 25268 |
. . . . . . . . 9
⊢ ((𝑐 ∈ ℝ+
∧ ∀𝑦 ∈
(1[,)+∞)(abs‘(((𝑆‘𝑦) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝑐) → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1)) |
451 | 450 | rexlimiva 3028 |
. . . . . . . 8
⊢
(∃𝑐 ∈
ℝ+ ∀𝑦 ∈ (1[,)+∞)(abs‘(((𝑆‘𝑦) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝑐 → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1)) |
452 | 447, 451 | mp1i 13 |
. . . . . . 7
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1)) |
453 | 357, 452 | o1lo1d 14270 |
. . . . . 6
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥)))) ∈
≤𝑂(1)) |
454 | 356, 357,
446, 453 | lo1add 14357 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (((𝑥
/ ((⌊‘𝑥) + 1))
· (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥))))) ∈
≤𝑂(1)) |
455 | 354, 454 | eqeltrd 2701 |
. . . 4
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥)))) ∈
≤𝑂(1)) |
456 | 340, 344,
346, 455 | lo1add 14357 |
. . 3
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥) + ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))))) ∈
≤𝑂(1)) |
457 | 339, 456 | eqeltrrd 2702 |
. 2
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / 𝑥)) ∈ ≤𝑂(1)) |
458 | 457 | trud 1493 |
1
⊢ (𝑥 ∈ (1(,)+∞) ↦
((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / 𝑥)) ∈ ≤𝑂(1) |