Step | Hyp | Ref
| Expression |
1 | | elioore 12844 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ (1(,)+∞) →
𝑥 ∈
ℝ) |
2 | 1 | adantl 485 |
. . . . . . . . . . . . . . . . . . 19
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 𝑥 ∈ ℝ) |
3 | | 1rp 12469 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 ∈
ℝ+ |
4 | 3 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 1 ∈ ℝ+) |
5 | | 1red 10713 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 1 ∈ ℝ) |
6 | | eliooord 12873 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ (1(,)+∞) → (1
< 𝑥 ∧ 𝑥 <
+∞)) |
7 | 6 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (1 < 𝑥 ∧ 𝑥 < +∞)) |
8 | 7 | simpld 498 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 1 < 𝑥) |
9 | 5, 2, 8 | ltled 10859 |
. . . . . . . . . . . . . . . . . . 19
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 1 ≤ 𝑥) |
10 | 2, 4, 9 | rpgecld 12546 |
. . . . . . . . . . . . . . . . . 18
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 𝑥 ∈ ℝ+) |
11 | 10 | rprege0d 12514 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥)) |
12 | | flge0nn0 13274 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) →
(⌊‘𝑥) ∈
ℕ0) |
13 | 11, 12 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (⌊‘𝑥) ∈
ℕ0) |
14 | | nn0p1nn 12008 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((⌊‘𝑥)
∈ ℕ0 → ((⌊‘𝑥) + 1) ∈ ℕ) |
15 | 13, 14 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((⌊‘𝑥) + 1) ∈ ℕ) |
16 | 15 | nnrpd 12505 |
. . . . . . . . . . . . . . . . . 18
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((⌊‘𝑥) + 1) ∈
ℝ+) |
17 | 10, 16 | rpdivcld 12524 |
. . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑥 / ((⌊‘𝑥) + 1)) ∈
ℝ+) |
18 | | pntrlog2bnd.r |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦
((ψ‘𝑎) −
𝑎)) |
19 | 18 | pntrval 26290 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 / ((⌊‘𝑥) + 1)) ∈
ℝ+ → (𝑅‘(𝑥 / ((⌊‘𝑥) + 1))) = ((ψ‘(𝑥 / ((⌊‘𝑥) + 1))) − (𝑥 / ((⌊‘𝑥) + 1)))) |
20 | 17, 19 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑅‘(𝑥 / ((⌊‘𝑥) + 1))) = ((ψ‘(𝑥 / ((⌊‘𝑥) + 1))) − (𝑥 / ((⌊‘𝑥) + 1)))) |
21 | 2, 15 | nndivred 11763 |
. . . . . . . . . . . . . . . . . . 19
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑥 / ((⌊‘𝑥) + 1)) ∈ ℝ) |
22 | | 2re 11783 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ∈
ℝ |
23 | 22 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 2 ∈ ℝ) |
24 | | flltp1 13254 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ ℝ → 𝑥 < ((⌊‘𝑥) + 1)) |
25 | 2, 24 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 𝑥 < ((⌊‘𝑥) + 1)) |
26 | 15 | nncnd 11725 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((⌊‘𝑥) + 1) ∈ ℂ) |
27 | 26 | mulid1d 10729 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((⌊‘𝑥) + 1) · 1) = ((⌊‘𝑥) + 1)) |
28 | 25, 27 | breqtrrd 5055 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 𝑥 < (((⌊‘𝑥) + 1) · 1)) |
29 | 2, 5, 16 | ltdivmuld 12558 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((𝑥 / ((⌊‘𝑥) + 1)) < 1 ↔ 𝑥 < (((⌊‘𝑥) + 1) · 1))) |
30 | 28, 29 | mpbird 260 |
. . . . . . . . . . . . . . . . . . 19
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑥 / ((⌊‘𝑥) + 1)) < 1) |
31 | | 1lt2 11880 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 <
2 |
32 | 31 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 1 < 2) |
33 | 21, 5, 23, 30, 32 | lttrd 10872 |
. . . . . . . . . . . . . . . . . 18
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑥 / ((⌊‘𝑥) + 1)) < 2) |
34 | | chpeq0 25936 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 / ((⌊‘𝑥) + 1)) ∈ ℝ →
((ψ‘(𝑥 /
((⌊‘𝑥) + 1))) =
0 ↔ (𝑥 /
((⌊‘𝑥) + 1))
< 2)) |
35 | 21, 34 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((ψ‘(𝑥 / ((⌊‘𝑥) + 1))) = 0 ↔ (𝑥 / ((⌊‘𝑥) + 1)) < 2)) |
36 | 33, 35 | mpbird 260 |
. . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (ψ‘(𝑥 / ((⌊‘𝑥) + 1))) = 0) |
37 | 36 | oveq1d 7179 |
. . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((ψ‘(𝑥 / ((⌊‘𝑥) + 1))) − (𝑥 / ((⌊‘𝑥) + 1))) = (0 − (𝑥 / ((⌊‘𝑥) + 1)))) |
38 | 20, 37 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑅‘(𝑥 / ((⌊‘𝑥) + 1))) = (0 − (𝑥 / ((⌊‘𝑥) + 1)))) |
39 | 38 | fveq2d 6672 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) = (abs‘(0 − (𝑥 / ((⌊‘𝑥) + 1))))) |
40 | | 0red 10715 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 0 ∈ ℝ) |
41 | 17 | rpge0d 12511 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 0 ≤ (𝑥 / ((⌊‘𝑥) + 1))) |
42 | 40, 21, 41 | abssuble0d 14875 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘(0 − (𝑥 / ((⌊‘𝑥) + 1)))) = ((𝑥 / ((⌊‘𝑥) + 1)) − 0)) |
43 | 21 | recnd 10740 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑥 / ((⌊‘𝑥) + 1)) ∈ ℂ) |
44 | 43 | subid1d 11057 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((𝑥 / ((⌊‘𝑥) + 1)) − 0) = (𝑥 / ((⌊‘𝑥) + 1))) |
45 | 39, 42, 44 | 3eqtrd 2777 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) = (𝑥 / ((⌊‘𝑥) + 1))) |
46 | 13 | nn0red 12030 |
. . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (⌊‘𝑥) ∈ ℝ) |
47 | | pntsval.1 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑆 = (𝑎 ∈ ℝ ↦ Σ𝑖 ∈
(1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖))))) |
48 | 47 | pntsval2 26304 |
. . . . . . . . . . . . . . . 16
⊢
((⌊‘𝑥)
∈ ℝ → (𝑆‘(⌊‘𝑥)) = Σ𝑛 ∈
(1...(⌊‘(⌊‘𝑥)))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))))) |
49 | 46, 48 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑆‘(⌊‘𝑥)) = Σ𝑛 ∈
(1...(⌊‘(⌊‘𝑥)))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))))) |
50 | 13 | nn0cnd 12031 |
. . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (⌊‘𝑥) ∈ ℂ) |
51 | | 1cnd 10707 |
. . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 1 ∈ ℂ) |
52 | 50, 51 | pncand 11069 |
. . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((⌊‘𝑥) + 1) − 1) = (⌊‘𝑥)) |
53 | 52 | fveq2d 6672 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑆‘(((⌊‘𝑥) + 1) − 1)) = (𝑆‘(⌊‘𝑥))) |
54 | 47 | pntsval2 26304 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℝ → (𝑆‘𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))))) |
55 | 2, 54 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑆‘𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))))) |
56 | | flidm 13263 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℝ →
(⌊‘(⌊‘𝑥)) = (⌊‘𝑥)) |
57 | 2, 56 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (⌊‘(⌊‘𝑥)) = (⌊‘𝑥)) |
58 | 57 | oveq2d 7180 |
. . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (1...(⌊‘(⌊‘𝑥))) = (1...(⌊‘𝑥))) |
59 | 58 | sumeq1d 15144 |
. . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘(⌊‘𝑥)))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))))) |
60 | 55, 59 | eqtr4d 2776 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑆‘𝑥) = Σ𝑛 ∈
(1...(⌊‘(⌊‘𝑥)))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))))) |
61 | 49, 53, 60 | 3eqtr4d 2783 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑆‘(((⌊‘𝑥) + 1) − 1)) = (𝑆‘𝑥)) |
62 | 52 | fveq2d 6672 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑇‘(((⌊‘𝑥) + 1) − 1)) = (𝑇‘(⌊‘𝑥))) |
63 | 62 | oveq2d 7180 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1))) = (2 · (𝑇‘(⌊‘𝑥)))) |
64 | 61, 63 | oveq12d 7182 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1)))) = ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) |
65 | 45, 64 | oveq12d 7182 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) · ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1))))) = ((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))))) |
66 | 2 | recnd 10740 |
. . . . . . . . . . . . . . . . . . 19
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 𝑥 ∈ ℂ) |
67 | 66 | div1d 11479 |
. . . . . . . . . . . . . . . . . 18
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑥 / 1) = 𝑥) |
68 | 67 | fveq2d 6672 |
. . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑅‘(𝑥 / 1)) = (𝑅‘𝑥)) |
69 | 18 | pntrf 26291 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑅:ℝ+⟶ℝ |
70 | 69 | ffvelrni 6854 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℝ+
→ (𝑅‘𝑥) ∈
ℝ) |
71 | 10, 70 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑅‘𝑥) ∈ ℝ) |
72 | 68, 71 | eqeltrd 2833 |
. . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑅‘(𝑥 / 1)) ∈ ℝ) |
73 | 72 | recnd 10740 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑅‘(𝑥 / 1)) ∈ ℂ) |
74 | 73 | abscld 14879 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘(𝑅‘(𝑥 / 1))) ∈ ℝ) |
75 | 74 | recnd 10740 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘(𝑅‘(𝑥 / 1))) ∈ ℂ) |
76 | 75 | mul01d 10910 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((abs‘(𝑅‘(𝑥 / 1))) · 0) = 0) |
77 | 65, 76 | oveq12d 7182 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) · ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1))))) −
((abs‘(𝑅‘(𝑥 / 1))) · 0)) = (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) − 0)) |
78 | 47 | pntsf 26301 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑆:ℝ⟶ℝ |
79 | 78 | ffvelrni 6854 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℝ → (𝑆‘𝑥) ∈ ℝ) |
80 | 2, 79 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑆‘𝑥) ∈ ℝ) |
81 | | pntrlog2bnd.t |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑇 = (𝑎 ∈ ℝ ↦ if(𝑎 ∈ ℝ+, (𝑎 · (log‘𝑎)), 0)) |
82 | | relogcl 25311 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 ∈ ℝ+
→ (log‘𝑎) ∈
ℝ) |
83 | | remulcl 10693 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎 ∈ ℝ ∧
(log‘𝑎) ∈
ℝ) → (𝑎 ·
(log‘𝑎)) ∈
ℝ) |
84 | 82, 83 | sylan2 596 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 ∈ ℝ ∧ 𝑎 ∈ ℝ+)
→ (𝑎 ·
(log‘𝑎)) ∈
ℝ) |
85 | | 0red 10715 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 ∈ ℝ ∧ ¬
𝑎 ∈
ℝ+) → 0 ∈ ℝ) |
86 | 84, 85 | ifclda 4446 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 ∈ ℝ → if(𝑎 ∈ ℝ+,
(𝑎 ·
(log‘𝑎)), 0) ∈
ℝ) |
87 | 81, 86 | fmpti 6880 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑇:ℝ⟶ℝ |
88 | 87 | ffvelrni 6854 |
. . . . . . . . . . . . . . . . 17
⊢
((⌊‘𝑥)
∈ ℝ → (𝑇‘(⌊‘𝑥)) ∈ ℝ) |
89 | 46, 88 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑇‘(⌊‘𝑥)) ∈ ℝ) |
90 | 23, 89 | remulcld 10742 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (2 · (𝑇‘(⌊‘𝑥))) ∈ ℝ) |
91 | 80, 90 | resubcld 11139 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) ∈ ℝ) |
92 | 21, 91 | remulcld 10742 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) ∈ ℝ) |
93 | 92 | recnd 10740 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) ∈ ℂ) |
94 | 93 | subid1d 11057 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) − 0) = ((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))))) |
95 | 77, 94 | eqtrd 2773 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) · ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1))))) −
((abs‘(𝑅‘(𝑥 / 1))) · 0)) = ((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))))) |
96 | 2 | flcld 13252 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (⌊‘𝑥) ∈ ℤ) |
97 | | fzval3 13190 |
. . . . . . . . . . . . . 14
⊢
((⌊‘𝑥)
∈ ℤ → (1...(⌊‘𝑥)) = (1..^((⌊‘𝑥) + 1))) |
98 | 96, 97 | syl 17 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (1...(⌊‘𝑥)) = (1..^((⌊‘𝑥) + 1))) |
99 | 98 | eqcomd 2744 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (1..^((⌊‘𝑥) + 1)) = (1...(⌊‘𝑥))) |
100 | 10 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ+) |
101 | | elfznn 13020 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℕ) |
102 | 101 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ) |
103 | 102 | nnrpd 12505 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ+) |
104 | 100, 103 | rpdivcld 12524 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈
ℝ+) |
105 | 69 | ffvelrni 6854 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 / 𝑛) ∈ ℝ+ → (𝑅‘(𝑥 / 𝑛)) ∈ ℝ) |
106 | 104, 105 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘(𝑥 / 𝑛)) ∈ ℝ) |
107 | 106 | recnd 10740 |
. . . . . . . . . . . . . . . . . 18
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘(𝑥 / 𝑛)) ∈ ℂ) |
108 | 107 | abscld 14879 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑅‘(𝑥 / 𝑛))) ∈ ℝ) |
109 | 108 | recnd 10740 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑅‘(𝑥 / 𝑛))) ∈ ℂ) |
110 | 3 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈
ℝ+) |
111 | 103, 110 | rpaddcld 12522 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 + 1) ∈
ℝ+) |
112 | 100, 111 | rpdivcld 12524 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / (𝑛 + 1)) ∈
ℝ+) |
113 | 69 | ffvelrni 6854 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 / (𝑛 + 1)) ∈ ℝ+ →
(𝑅‘(𝑥 / (𝑛 + 1))) ∈ ℝ) |
114 | 112, 113 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘(𝑥 / (𝑛 + 1))) ∈ ℝ) |
115 | 114 | recnd 10740 |
. . . . . . . . . . . . . . . . . 18
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘(𝑥 / (𝑛 + 1))) ∈ ℂ) |
116 | 115 | abscld 14879 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) ∈ ℝ) |
117 | 116 | recnd 10740 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) ∈ ℂ) |
118 | 109, 117 | negsubdi2d 11084 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → -((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) = ((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛))))) |
119 | 118 | eqcomd 2744 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))) = -((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1)))))) |
120 | 102 | nncnd 11725 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℂ) |
121 | | 1cnd 10707 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈
ℂ) |
122 | 120, 121 | pncand 11069 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) − 1) = 𝑛) |
123 | 122 | fveq2d 6672 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘((𝑛 + 1) − 1)) = (𝑆‘𝑛)) |
124 | 122 | fveq2d 6672 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇‘((𝑛 + 1) − 1)) = (𝑇‘𝑛)) |
125 | | rpre 12473 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ ℝ+
→ 𝑛 ∈
ℝ) |
126 | | eleq1 2820 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 = 𝑛 → (𝑎 ∈ ℝ+ ↔ 𝑛 ∈
ℝ+)) |
127 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑎 = 𝑛 → 𝑎 = 𝑛) |
128 | | fveq2 6668 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑎 = 𝑛 → (log‘𝑎) = (log‘𝑛)) |
129 | 127, 128 | oveq12d 7182 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 = 𝑛 → (𝑎 · (log‘𝑎)) = (𝑛 · (log‘𝑛))) |
130 | 126, 129 | ifbieq1d 4435 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 = 𝑛 → if(𝑎 ∈ ℝ+, (𝑎 · (log‘𝑎)), 0) = if(𝑛 ∈ ℝ+, (𝑛 · (log‘𝑛)), 0)) |
131 | | ovex 7197 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 · (log‘𝑛)) ∈ V |
132 | | c0ex 10706 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 0 ∈
V |
133 | 131, 132 | ifex 4461 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ if(𝑛 ∈ ℝ+,
(𝑛 ·
(log‘𝑛)), 0) ∈
V |
134 | 130, 81, 133 | fvmpt 6769 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ ℝ → (𝑇‘𝑛) = if(𝑛 ∈ ℝ+, (𝑛 · (log‘𝑛)), 0)) |
135 | 125, 134 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℝ+
→ (𝑇‘𝑛) = if(𝑛 ∈ ℝ+, (𝑛 · (log‘𝑛)), 0)) |
136 | | iftrue 4417 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℝ+
→ if(𝑛 ∈
ℝ+, (𝑛
· (log‘𝑛)), 0)
= (𝑛 ·
(log‘𝑛))) |
137 | 135, 136 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℝ+
→ (𝑇‘𝑛) = (𝑛 · (log‘𝑛))) |
138 | 103, 137 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇‘𝑛) = (𝑛 · (log‘𝑛))) |
139 | 124, 138 | eqtrd 2773 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇‘((𝑛 + 1) − 1)) = (𝑛 · (log‘𝑛))) |
140 | 139 | oveq2d 7180 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑇‘((𝑛 + 1) − 1))) = (2 · (𝑛 · (log‘𝑛)))) |
141 | 123, 140 | oveq12d 7182 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))) = ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) |
142 | 119, 141 | oveq12d 7182 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))) · ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1))))) = (-((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) |
143 | 108, 116 | resubcld 11139 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) ∈ ℝ) |
144 | 143 | recnd 10740 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) ∈ ℂ) |
145 | 102 | nnred 11724 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ) |
146 | 78 | ffvelrni 6854 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℝ → (𝑆‘𝑛) ∈ ℝ) |
147 | 145, 146 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘𝑛) ∈ ℝ) |
148 | 22 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 2 ∈
ℝ) |
149 | 103 | relogcld 25358 |
. . . . . . . . . . . . . . . . . 18
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘𝑛) ∈
ℝ) |
150 | 145, 149 | remulcld 10742 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 · (log‘𝑛)) ∈ ℝ) |
151 | 148, 150 | remulcld 10742 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑛 · (log‘𝑛))) ∈
ℝ) |
152 | 147, 151 | resubcld 11139 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))) ∈ ℝ) |
153 | 152 | recnd 10740 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))) ∈ ℂ) |
154 | 144, 153 | mulneg1d 11164 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (-((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) = -(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) |
155 | 142, 154 | eqtrd 2773 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))) · ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1))))) = -(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) |
156 | 99, 155 | sumeq12rdv 15150 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))(((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))) · ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1))))) = Σ𝑛 ∈
(1...(⌊‘𝑥))-(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) |
157 | | fzfid 13425 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (1...(⌊‘𝑥)) ∈ Fin) |
158 | 143, 152 | remulcld 10742 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) ∈ ℝ) |
159 | 158 | recnd 10740 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) ∈ ℂ) |
160 | 157, 159 | fsumneg 15228 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))-(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) = -Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) |
161 | 156, 160 | eqtrd 2773 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))(((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))) · ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1))))) = -Σ𝑛 ∈
(1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) |
162 | 95, 161 | oveq12d 7182 |
. . . . . . . . 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 7172 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑛 → (𝑥 / 𝑚) = (𝑥 / 𝑛)) |
164 | 163 | fveq2d 6672 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑛 → (𝑅‘(𝑥 / 𝑚)) = (𝑅‘(𝑥 / 𝑛))) |
165 | 164 | fveq2d 6672 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → (abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / 𝑛)))) |
166 | | fvoveq1 7187 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑛 → (𝑆‘(𝑚 − 1)) = (𝑆‘(𝑛 − 1))) |
167 | | fvoveq1 7187 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑛 → (𝑇‘(𝑚 − 1)) = (𝑇‘(𝑛 − 1))) |
168 | 167 | oveq2d 7180 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑛 → (2 · (𝑇‘(𝑚 − 1))) = (2 · (𝑇‘(𝑛 − 1)))) |
169 | 166, 168 | oveq12d 7182 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1))))) |
170 | 165, 169 | jca 515 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → ((abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / 𝑛))) ∧ ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1)))))) |
171 | | oveq2 7172 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = (𝑛 + 1) → (𝑥 / 𝑚) = (𝑥 / (𝑛 + 1))) |
172 | 171 | fveq2d 6672 |
. . . . . . . . . . . . 13
⊢ (𝑚 = (𝑛 + 1) → (𝑅‘(𝑥 / 𝑚)) = (𝑅‘(𝑥 / (𝑛 + 1)))) |
173 | 172 | fveq2d 6672 |
. . . . . . . . . . . 12
⊢ (𝑚 = (𝑛 + 1) → (abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) |
174 | | fvoveq1 7187 |
. . . . . . . . . . . . 13
⊢ (𝑚 = (𝑛 + 1) → (𝑆‘(𝑚 − 1)) = (𝑆‘((𝑛 + 1) − 1))) |
175 | | fvoveq1 7187 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = (𝑛 + 1) → (𝑇‘(𝑚 − 1)) = (𝑇‘((𝑛 + 1) − 1))) |
176 | 175 | oveq2d 7180 |
. . . . . . . . . . . . 13
⊢ (𝑚 = (𝑛 + 1) → (2 · (𝑇‘(𝑚 − 1))) = (2 · (𝑇‘((𝑛 + 1) − 1)))) |
177 | 174, 176 | oveq12d 7182 |
. . . . . . . . . . . 12
⊢ (𝑚 = (𝑛 + 1) → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1))))) |
178 | 173, 177 | jca 515 |
. . . . . . . . . . 11
⊢ (𝑚 = (𝑛 + 1) → ((abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) ∧ ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))))) |
179 | | oveq2 7172 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 1 → (𝑥 / 𝑚) = (𝑥 / 1)) |
180 | 179 | fveq2d 6672 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 1 → (𝑅‘(𝑥 / 𝑚)) = (𝑅‘(𝑥 / 1))) |
181 | 180 | fveq2d 6672 |
. . . . . . . . . . . 12
⊢ (𝑚 = 1 → (abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / 1)))) |
182 | | oveq1 7171 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 = 1 → (𝑚 − 1) = (1 − 1)) |
183 | | 1m1e0 11781 |
. . . . . . . . . . . . . . . . 17
⊢ (1
− 1) = 0 |
184 | 182, 183 | eqtrdi 2789 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 = 1 → (𝑚 − 1) = 0) |
185 | 184 | fveq2d 6672 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = 1 → (𝑆‘(𝑚 − 1)) = (𝑆‘0)) |
186 | | 0re 10714 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℝ |
187 | | fveq2 6668 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 = 0 → (⌊‘𝑎) =
(⌊‘0)) |
188 | | 0z 12066 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 0 ∈
ℤ |
189 | | flid 13262 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (0 ∈
ℤ → (⌊‘0) = 0) |
190 | 188, 189 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(⌊‘0) = 0 |
191 | 187, 190 | eqtrdi 2789 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 = 0 → (⌊‘𝑎) = 0) |
192 | 191 | oveq2d 7180 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 = 0 →
(1...(⌊‘𝑎)) =
(1...0)) |
193 | | fz10 13012 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (1...0) =
∅ |
194 | 192, 193 | eqtrdi 2789 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = 0 →
(1...(⌊‘𝑎)) =
∅) |
195 | 194 | sumeq1d 15144 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = 0 → Σ𝑖 ∈
(1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))) = Σ𝑖 ∈ ∅ ((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖))))) |
196 | | sum0 15164 |
. . . . . . . . . . . . . . . . . 18
⊢
Σ𝑖 ∈
∅ ((Λ‘𝑖)
· ((log‘𝑖) +
(ψ‘(𝑎 / 𝑖)))) = 0 |
197 | 195, 196 | eqtrdi 2789 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = 0 → Σ𝑖 ∈
(1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))) = 0) |
198 | 197, 47, 132 | fvmpt 6769 |
. . . . . . . . . . . . . . . 16
⊢ (0 ∈
ℝ → (𝑆‘0)
= 0) |
199 | 186, 198 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ (𝑆‘0) = 0 |
200 | 185, 199 | eqtrdi 2789 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 1 → (𝑆‘(𝑚 − 1)) = 0) |
201 | 184 | fveq2d 6672 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 = 1 → (𝑇‘(𝑚 − 1)) = (𝑇‘0)) |
202 | | rpne0 12481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 ∈ ℝ+
→ 𝑎 ≠
0) |
203 | 202 | necon2bi 2964 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 = 0 → ¬ 𝑎 ∈
ℝ+) |
204 | 203 | iffalsed 4422 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = 0 → if(𝑎 ∈ ℝ+,
(𝑎 ·
(log‘𝑎)), 0) =
0) |
205 | 204, 81, 132 | fvmpt 6769 |
. . . . . . . . . . . . . . . . . 18
⊢ (0 ∈
ℝ → (𝑇‘0)
= 0) |
206 | 186, 205 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑇‘0) = 0 |
207 | 201, 206 | eqtrdi 2789 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 = 1 → (𝑇‘(𝑚 − 1)) = 0) |
208 | 207 | oveq2d 7180 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = 1 → (2 · (𝑇‘(𝑚 − 1))) = (2 ·
0)) |
209 | | 2t0e0 11878 |
. . . . . . . . . . . . . . 15
⊢ (2
· 0) = 0 |
210 | 208, 209 | eqtrdi 2789 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 1 → (2 · (𝑇‘(𝑚 − 1))) = 0) |
211 | 200, 210 | oveq12d 7182 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 1 → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = (0 −
0)) |
212 | | 0m0e0 11829 |
. . . . . . . . . . . . 13
⊢ (0
− 0) = 0 |
213 | 211, 212 | eqtrdi 2789 |
. . . . . . . . . . . 12
⊢ (𝑚 = 1 → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = 0) |
214 | 181, 213 | jca 515 |
. . . . . . . . . . 11
⊢ (𝑚 = 1 → ((abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / 1))) ∧ ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = 0)) |
215 | | oveq2 7172 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = ((⌊‘𝑥) + 1) → (𝑥 / 𝑚) = (𝑥 / ((⌊‘𝑥) + 1))) |
216 | 215 | fveq2d 6672 |
. . . . . . . . . . . . 13
⊢ (𝑚 = ((⌊‘𝑥) + 1) → (𝑅‘(𝑥 / 𝑚)) = (𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) |
217 | 216 | fveq2d 6672 |
. . . . . . . . . . . 12
⊢ (𝑚 = ((⌊‘𝑥) + 1) → (abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1))))) |
218 | | fvoveq1 7187 |
. . . . . . . . . . . . 13
⊢ (𝑚 = ((⌊‘𝑥) + 1) → (𝑆‘(𝑚 − 1)) = (𝑆‘(((⌊‘𝑥) + 1) − 1))) |
219 | | fvoveq1 7187 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = ((⌊‘𝑥) + 1) → (𝑇‘(𝑚 − 1)) = (𝑇‘(((⌊‘𝑥) + 1) − 1))) |
220 | 219 | oveq2d 7180 |
. . . . . . . . . . . . 13
⊢ (𝑚 = ((⌊‘𝑥) + 1) → (2 · (𝑇‘(𝑚 − 1))) = (2 · (𝑇‘(((⌊‘𝑥) + 1) −
1)))) |
221 | 218, 220 | oveq12d 7182 |
. . . . . . . . . . . 12
⊢ (𝑚 = ((⌊‘𝑥) + 1) → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) −
1))))) |
222 | 217, 221 | jca 515 |
. . . . . . . . . . 11
⊢ (𝑚 = ((⌊‘𝑥) + 1) → ((abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) ∧ ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) −
1)))))) |
223 | | nnuz 12356 |
. . . . . . . . . . . 12
⊢ ℕ =
(ℤ≥‘1) |
224 | 15, 223 | eleqtrdi 2843 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((⌊‘𝑥) + 1) ∈
(ℤ≥‘1)) |
225 | 10 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 𝑥 ∈
ℝ+) |
226 | | elfznn 13020 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ∈
(1...((⌊‘𝑥) +
1)) → 𝑚 ∈
ℕ) |
227 | 226 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 𝑚 ∈
ℕ) |
228 | 227 | nnrpd 12505 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 𝑚 ∈
ℝ+) |
229 | 225, 228 | rpdivcld 12524 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑥 / 𝑚) ∈
ℝ+) |
230 | 69 | ffvelrni 6854 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 / 𝑚) ∈ ℝ+ → (𝑅‘(𝑥 / 𝑚)) ∈ ℝ) |
231 | 229, 230 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑅‘(𝑥 / 𝑚)) ∈ ℝ) |
232 | 231 | recnd 10740 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑅‘(𝑥 / 𝑚)) ∈ ℂ) |
233 | 232 | abscld 14879 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) →
(abs‘(𝑅‘(𝑥 / 𝑚))) ∈ ℝ) |
234 | 233 | recnd 10740 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) →
(abs‘(𝑅‘(𝑥 / 𝑚))) ∈ ℂ) |
235 | 227 | nnred 11724 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 𝑚 ∈
ℝ) |
236 | | 1red 10713 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 1 ∈
ℝ) |
237 | 235, 236 | resubcld 11139 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑚 − 1) ∈
ℝ) |
238 | 78 | ffvelrni 6854 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 − 1) ∈ ℝ
→ (𝑆‘(𝑚 − 1)) ∈
ℝ) |
239 | 237, 238 | syl 17 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑆‘(𝑚 − 1)) ∈ ℝ) |
240 | 22 | a1i 11 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 2 ∈
ℝ) |
241 | 87 | ffvelrni 6854 |
. . . . . . . . . . . . . . 15
⊢ ((𝑚 − 1) ∈ ℝ
→ (𝑇‘(𝑚 − 1)) ∈
ℝ) |
242 | 237, 241 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑇‘(𝑚 − 1)) ∈ ℝ) |
243 | 240, 242 | remulcld 10742 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (2 ·
(𝑇‘(𝑚 − 1))) ∈
ℝ) |
244 | 239, 243 | resubcld 11139 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) ∈
ℝ) |
245 | 244 | recnd 10740 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) ∈
ℂ) |
246 | 170, 178,
214, 222, 224, 234, 245 | fsumparts 15247 |
. . . . . . . . . 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))))))) |
247 | 147 | recnd 10740 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘𝑛) ∈ ℂ) |
248 | 87 | ffvelrni 6854 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℝ → (𝑇‘𝑛) ∈ ℝ) |
249 | 145, 248 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇‘𝑛) ∈ ℝ) |
250 | 148, 249 | remulcld 10742 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑇‘𝑛)) ∈ ℝ) |
251 | 250 | recnd 10740 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑇‘𝑛)) ∈ ℂ) |
252 | | 1red 10713 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈
ℝ) |
253 | 145, 252 | resubcld 11139 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 − 1) ∈ ℝ) |
254 | 78 | ffvelrni 6854 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 − 1) ∈ ℝ
→ (𝑆‘(𝑛 − 1)) ∈
ℝ) |
255 | 253, 254 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘(𝑛 − 1)) ∈ ℝ) |
256 | 255 | recnd 10740 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘(𝑛 − 1)) ∈ ℂ) |
257 | 87 | ffvelrni 6854 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 − 1) ∈ ℝ
→ (𝑇‘(𝑛 − 1)) ∈
ℝ) |
258 | 253, 257 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇‘(𝑛 − 1)) ∈ ℝ) |
259 | 148, 258 | remulcld 10742 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑇‘(𝑛 − 1))) ∈
ℝ) |
260 | 259 | recnd 10740 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑇‘(𝑛 − 1))) ∈
ℂ) |
261 | 247, 251,
256, 260 | sub4d 11117 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆‘𝑛) − (2 · (𝑇‘𝑛))) − ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1))))) = (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − ((2 · (𝑇‘𝑛)) − (2 · (𝑇‘(𝑛 − 1)))))) |
262 | 124 | oveq2d 7180 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑇‘((𝑛 + 1) − 1))) = (2 · (𝑇‘𝑛))) |
263 | 123, 262 | oveq12d 7182 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))) = ((𝑆‘𝑛) − (2 · (𝑇‘𝑛)))) |
264 | 263 | oveq1d 7179 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))) − ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1))))) = (((𝑆‘𝑛) − (2 · (𝑇‘𝑛))) − ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1)))))) |
265 | | 2cnd 11787 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 2 ∈
ℂ) |
266 | 249 | recnd 10740 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇‘𝑛) ∈ ℂ) |
267 | 258 | recnd 10740 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇‘(𝑛 − 1)) ∈ ℂ) |
268 | 265, 266,
267 | subdid 11167 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))) = ((2 · (𝑇‘𝑛)) − (2 · (𝑇‘(𝑛 − 1))))) |
269 | 268 | oveq2d 7180 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))) = (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − ((2 · (𝑇‘𝑛)) − (2 · (𝑇‘(𝑛 − 1)))))) |
270 | 261, 264,
269 | 3eqtr4d 2783 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))) − ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1))))) = (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) |
271 | 270 | oveq2d 7180 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))) − ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1)))))) = ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) |
272 | 99, 271 | sumeq12rdv 15150 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))) − ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1)))))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) |
273 | 246, 272 | eqtr3d 2775 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) · ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1))))) −
((abs‘(𝑅‘(𝑥 / 1))) · 0)) −
Σ𝑛 ∈
(1..^((⌊‘𝑥) +
1))(((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))) · ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))))) = Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) |
274 | 157, 159 | fsumcl 15176 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) ∈ ℂ) |
275 | 93, 274 | subnegd 11075 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) − -Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) = (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))))) |
276 | 162, 273,
275 | 3eqtr3rd 2782 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) |
277 | 10 | relogcld 25358 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (log‘𝑥) ∈ ℝ) |
278 | 277 | recnd 10740 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (log‘𝑥) ∈ ℂ) |
279 | 66, 278 | mulcomd 10733 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) = ((log‘𝑥) · 𝑥)) |
280 | 276, 279 | oveq12d 7182 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / ((log‘𝑥) · 𝑥))) |
281 | 147, 255 | resubcld 11139 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) ∈
ℝ) |
282 | 249, 258 | resubcld 11139 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))) ∈
ℝ) |
283 | 148, 282 | remulcld 10742 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))) ∈
ℝ) |
284 | 281, 283 | resubcld 11139 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))) ∈
ℝ) |
285 | 108, 284 | remulcld 10742 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) ∈
ℝ) |
286 | 157, 285 | fsumrecl 15177 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) ∈
ℝ) |
287 | 286 | recnd 10740 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) ∈
ℂ) |
288 | 2, 8 | rplogcld 25364 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (log‘𝑥) ∈
ℝ+) |
289 | 288 | rpne0d 12512 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (log‘𝑥) ≠ 0) |
290 | 10 | rpne0d 12512 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 𝑥 ≠ 0) |
291 | 287, 278,
66, 289, 290 | divdiv1d 11518 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥)) / 𝑥) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / ((log‘𝑥) · 𝑥))) |
292 | 280, 291 | eqtr4d 2776 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥)) / 𝑥)) |
293 | 292 | oveq2d 7180 |
. . . . 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‘𝑥)) / 𝑥))) |
294 | 71 | recnd 10740 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑅‘𝑥) ∈ ℂ) |
295 | 294 | abscld 14879 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘(𝑅‘𝑥)) ∈ ℝ) |
296 | 295, 277 | remulcld 10742 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((abs‘(𝑅‘𝑥)) · (log‘𝑥)) ∈ ℝ) |
297 | 108, 281 | remulcld 10742 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) ∈
ℝ) |
298 | 157, 297 | fsumrecl 15177 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) ∈
ℝ) |
299 | 298, 288 | rerpdivcld 12538 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥)) ∈
ℝ) |
300 | 296, 299 | resubcld 11139 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) ∈
ℝ) |
301 | 300 | recnd 10740 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) ∈
ℂ) |
302 | 287, 278,
289 | divcld 11487 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥)) ∈
ℂ) |
303 | 301, 302,
66, 290 | divdird 11525 |
. . . . 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‘𝑥)) / 𝑥))) |
304 | 296 | recnd 10740 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((abs‘(𝑅‘𝑥)) · (log‘𝑥)) ∈ ℂ) |
305 | 299 | recnd 10740 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥)) ∈
ℂ) |
306 | 304, 305,
302 | subsubd 11096 |
. . . . . . 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 11787 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 2 ∈ ℂ) |
308 | 266, 267 | subcld 11068 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))) ∈
ℂ) |
309 | 109, 308 | mulcld 10732 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))) ∈
ℂ) |
310 | 157, 307,
309 | fsummulc2 15225 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(2 · ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) |
311 | 281 | recnd 10740 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) ∈
ℂ) |
312 | 265, 308 | mulcld 10732 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))) ∈
ℂ) |
313 | 311, 312 | nncand 11073 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) = (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))) |
314 | 313 | oveq2d 7180 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) = ((abs‘(𝑅‘(𝑥 / 𝑛))) · (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) |
315 | 284 | recnd 10740 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))) ∈
ℂ) |
316 | 109, 311,
315 | subdid 11167 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) = (((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) − ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))))) |
317 | 109, 265,
308 | mul12d 10920 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))) = (2 ·
((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) |
318 | 314, 316,
317 | 3eqtr3d 2781 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) − ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) = (2 ·
((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) |
319 | 318 | sumeq2dv 15146 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) − ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(2 · ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) |
320 | 297 | recnd 10740 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) ∈
ℂ) |
321 | 285 | recnd 10740 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) ∈
ℂ) |
322 | 157, 320,
321 | fsumsub 15229 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) − ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) = (Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) − Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))))) |
323 | 310, 319,
322 | 3eqtr2rd 2780 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) − Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) = (2 · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) |
324 | 323 | oveq1d 7179 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) − Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) / (log‘𝑥)) = ((2 · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))) / (log‘𝑥))) |
325 | 298 | recnd 10740 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) ∈
ℂ) |
326 | 325, 287,
278, 289 | divsubdird 11526 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) − Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) / (log‘𝑥)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥)) − (Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥)))) |
327 | 108, 282 | remulcld 10742 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))) ∈
ℝ) |
328 | 157, 327 | fsumrecl 15177 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))) ∈
ℝ) |
329 | 328 | recnd 10740 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))) ∈
ℂ) |
330 | 307, 329,
278, 289 | div23d 11524 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))) / (log‘𝑥)) = ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) |
331 | 324, 326,
330 | 3eqtr3d 2781 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥)) − (Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥))) = ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) |
332 | 331 | oveq2d 7180 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥)) − (Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥)))) = (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) |
333 | 306, 332 | eqtr3d 2775 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥))) = (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) |
334 | 333 | oveq1d 7179 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥))) / 𝑥) = ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / 𝑥)) |
335 | 293, 303,
334 | 3eqtr2d 2779 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥) + ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥)))) = ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / 𝑥)) |
336 | 335 | mpteq2dva 5122 |
. . 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)))))) / 𝑥))) |
337 | 300, 10 | rerpdivcld 12538 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥) ∈ ℝ) |
338 | 157, 158 | fsumrecl 15177 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) ∈ ℝ) |
339 | 92, 338 | readdcld 10741 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) ∈ ℝ) |
340 | 10, 288 | rpmulcld 12523 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ∈
ℝ+) |
341 | 339, 340 | rerpdivcld 12538 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))) ∈ ℝ) |
342 | 47, 18 | pntrlog2bndlem1 26305 |
. . . . 5
⊢ (𝑥 ∈ (1(,)+∞) ↦
((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥)) ∈ ≤𝑂(1) |
343 | 342 | a1i 11 |
. . . 4
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥)) ∈ ≤𝑂(1)) |
344 | 340 | rpcnd 12509 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ∈ ℂ) |
345 | 340 | rpne0d 12512 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ≠ 0) |
346 | 93, 274, 344, 345 | divdird 11525 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))) = ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) / (𝑥 · (log‘𝑥))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥))))) |
347 | 91 | recnd 10740 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) ∈ ℂ) |
348 | 43, 347, 344, 345 | divassd 11522 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) / (𝑥 · (log‘𝑥))) = ((𝑥 / ((⌊‘𝑥) + 1)) · (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥))))) |
349 | 348 | oveq1d 7179 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) / (𝑥 · (log‘𝑥))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥)))) = (((𝑥 / ((⌊‘𝑥) + 1)) · (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥))))) |
350 | 346, 349 | eqtrd 2773 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))) = (((𝑥 / ((⌊‘𝑥) + 1)) · (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥))))) |
351 | 350 | mpteq2dva 5122 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥)))) = (𝑥 ∈ (1(,)+∞) ↦ (((𝑥 / ((⌊‘𝑥) + 1)) · (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥)))))) |
352 | 91, 340 | rerpdivcld 12538 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥))) ∈ ℝ) |
353 | 21, 352 | remulcld 10742 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((𝑥 / ((⌊‘𝑥) + 1)) · (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) ∈ ℝ) |
354 | 338, 340 | rerpdivcld 12538 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥))) ∈ ℝ) |
355 | | ioossre 12875 |
. . . . . . . . 9
⊢
(1(,)+∞) ⊆ ℝ |
356 | 355 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ (1(,)+∞) ⊆ ℝ) |
357 | | 1red 10713 |
. . . . . . . 8
⊢ (⊤
→ 1 ∈ ℝ) |
358 | 21, 5, 30 | ltled 10859 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑥 / ((⌊‘𝑥) + 1)) ≤ 1) |
359 | 358 | adantrr 717 |
. . . . . . . 8
⊢
((⊤ ∧ (𝑥
∈ (1(,)+∞) ∧ 1 ≤ 𝑥)) → (𝑥 / ((⌊‘𝑥) + 1)) ≤ 1) |
360 | 356, 21, 357, 357, 359 | ello1d 14963 |
. . . . . . 7
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (𝑥 /
((⌊‘𝑥) + 1)))
∈ ≤𝑂(1)) |
361 | 80 | recnd 10740 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑆‘𝑥) ∈ ℂ) |
362 | 90 | recnd 10740 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (2 · (𝑇‘(⌊‘𝑥))) ∈ ℂ) |
363 | 361, 362,
344, 345 | divsubdird 11526 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥))) = (((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) − ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥))))) |
364 | 363 | mpteq2dva 5122 |
. . . . . . . . 9
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) = (𝑥 ∈ (1(,)+∞) ↦ (((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) − ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥)))))) |
365 | 80, 340 | rerpdivcld 12538 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) ∈ ℝ) |
366 | 90, 340 | rerpdivcld 12538 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥))) ∈ ℝ) |
367 | | 2cnd 11787 |
. . . . . . . . . . . 12
⊢ (⊤
→ 2 ∈ ℂ) |
368 | | o1const 15060 |
. . . . . . . . . . . 12
⊢
(((1(,)+∞) ⊆ ℝ ∧ 2 ∈ ℂ) → (𝑥 ∈ (1(,)+∞) ↦
2) ∈ 𝑂(1)) |
369 | 355, 367,
368 | sylancr 590 |
. . . . . . . . . . 11
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ 2) ∈ 𝑂(1)) |
370 | 365 | recnd 10740 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) ∈ ℂ) |
371 | 80, 10 | rerpdivcld 12538 |
. . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((𝑆‘𝑥) / 𝑥) ∈ ℝ) |
372 | 371 | recnd 10740 |
. . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((𝑆‘𝑥) / 𝑥) ∈ ℂ) |
373 | 307, 278 | mulcld 10732 |
. . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (2 · (log‘𝑥)) ∈ ℂ) |
374 | 372, 373,
278, 289 | divsubdird 11526 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥))) / (log‘𝑥)) = ((((𝑆‘𝑥) / 𝑥) / (log‘𝑥)) − ((2 · (log‘𝑥)) / (log‘𝑥)))) |
375 | 23, 277 | remulcld 10742 |
. . . . . . . . . . . . . . . . . 18
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (2 · (log‘𝑥)) ∈ ℝ) |
376 | 371, 375 | resubcld 11139 |
. . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥))) ∈
ℝ) |
377 | 376 | recnd 10740 |
. . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥))) ∈
ℂ) |
378 | 377, 278,
289 | divrecd 11490 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥))) / (log‘𝑥)) = ((((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥))) · (1 /
(log‘𝑥)))) |
379 | 361, 66, 278, 290, 289 | divdiv1d 11518 |
. . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((𝑆‘𝑥) / 𝑥) / (log‘𝑥)) = ((𝑆‘𝑥) / (𝑥 · (log‘𝑥)))) |
380 | 307, 278,
289 | divcan4d 11493 |
. . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((2 · (log‘𝑥)) / (log‘𝑥)) = 2) |
381 | 379, 380 | oveq12d 7182 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((𝑆‘𝑥) / 𝑥) / (log‘𝑥)) − ((2 · (log‘𝑥)) / (log‘𝑥))) = (((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) − 2)) |
382 | 374, 378,
381 | 3eqtr3rd 2782 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) − 2) = ((((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥))) · (1 /
(log‘𝑥)))) |
383 | 382 | mpteq2dva 5122 |
. . . . . . . . . . . . 13
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) − 2)) = (𝑥 ∈ (1(,)+∞) ↦ ((((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥))) · (1 /
(log‘𝑥))))) |
384 | 5, 288 | rerpdivcld 12538 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (1 / (log‘𝑥)) ∈ ℝ) |
385 | 10 | ex 416 |
. . . . . . . . . . . . . . . 16
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) → 𝑥
∈ ℝ+)) |
386 | 385 | ssrdv 3881 |
. . . . . . . . . . . . . . 15
⊢ (⊤
→ (1(,)+∞) ⊆ ℝ+) |
387 | 47 | selbergs 26302 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℝ+
↦ (((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥)))) ∈
𝑂(1) |
388 | 387 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥)))) ∈
𝑂(1)) |
389 | 386, 388 | o1res2 15003 |
. . . . . . . . . . . . . 14
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥)))) ∈
𝑂(1)) |
390 | | divlogrlim 25370 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (1(,)+∞) ↦
(1 / (log‘𝑥)))
⇝𝑟 0 |
391 | | rlimo1 15057 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (1(,)+∞) ↦
(1 / (log‘𝑥)))
⇝𝑟 0 → (𝑥 ∈ (1(,)+∞) ↦ (1 /
(log‘𝑥))) ∈
𝑂(1)) |
392 | 390, 391 | mp1i 13 |
. . . . . . . . . . . . . 14
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (1 / (log‘𝑥))) ∈ 𝑂(1)) |
393 | 376, 384,
389, 392 | o1mul2 15065 |
. . . . . . . . . . . . 13
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ ((((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥))) · (1 /
(log‘𝑥)))) ∈
𝑂(1)) |
394 | 383, 393 | eqeltrd 2833 |
. . . . . . . . . . . 12
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) − 2)) ∈
𝑂(1)) |
395 | 370, 307,
394 | o1dif 15070 |
. . . . . . . . . . 11
⊢ (⊤
→ ((𝑥 ∈
(1(,)+∞) ↦ ((𝑆‘𝑥) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1) ↔ (𝑥 ∈ (1(,)+∞) ↦
2) ∈ 𝑂(1))) |
396 | 369, 395 | mpbird 260 |
. . . . . . . . . 10
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ ((𝑆‘𝑥) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1)) |
397 | 22 | a1i 11 |
. . . . . . . . . . . 12
⊢ (⊤
→ 2 ∈ ℝ) |
398 | 2, 277 | remulcld 10742 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ∈ ℝ) |
399 | | 2rp 12470 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℝ+ |
400 | 399 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 2 ∈ ℝ+) |
401 | 400 | rpge0d 12511 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 0 ≤ 2) |
402 | | flge1nn 13275 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℝ ∧ 1 ≤
𝑥) →
(⌊‘𝑥) ∈
ℕ) |
403 | 2, 9, 402 | syl2anc 587 |
. . . . . . . . . . . . . . . . . 18
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (⌊‘𝑥) ∈ ℕ) |
404 | 403 | nnrpd 12505 |
. . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (⌊‘𝑥) ∈
ℝ+) |
405 | | rpre 12473 |
. . . . . . . . . . . . . . . . . . 19
⊢
((⌊‘𝑥)
∈ ℝ+ → (⌊‘𝑥) ∈ ℝ) |
406 | | eleq1 2820 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 = (⌊‘𝑥) → (𝑎 ∈ ℝ+ ↔
(⌊‘𝑥) ∈
ℝ+)) |
407 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 = (⌊‘𝑥) → 𝑎 = (⌊‘𝑥)) |
408 | | fveq2 6668 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 = (⌊‘𝑥) → (log‘𝑎) =
(log‘(⌊‘𝑥))) |
409 | 407, 408 | oveq12d 7182 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 = (⌊‘𝑥) → (𝑎 · (log‘𝑎)) = ((⌊‘𝑥) · (log‘(⌊‘𝑥)))) |
410 | 406, 409 | ifbieq1d 4435 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 = (⌊‘𝑥) → if(𝑎 ∈ ℝ+, (𝑎 · (log‘𝑎)), 0) = if((⌊‘𝑥) ∈ ℝ+,
((⌊‘𝑥) ·
(log‘(⌊‘𝑥))), 0)) |
411 | | ovex 7197 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((⌊‘𝑥)
· (log‘(⌊‘𝑥))) ∈ V |
412 | 411, 132 | ifex 4461 |
. . . . . . . . . . . . . . . . . . . 20
⊢
if((⌊‘𝑥)
∈ ℝ+, ((⌊‘𝑥) · (log‘(⌊‘𝑥))), 0) ∈
V |
413 | 410, 81, 412 | fvmpt 6769 |
. . . . . . . . . . . . . . . . . . 19
⊢
((⌊‘𝑥)
∈ ℝ → (𝑇‘(⌊‘𝑥)) = if((⌊‘𝑥) ∈ ℝ+,
((⌊‘𝑥) ·
(log‘(⌊‘𝑥))), 0)) |
414 | 405, 413 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
((⌊‘𝑥)
∈ ℝ+ → (𝑇‘(⌊‘𝑥)) = if((⌊‘𝑥) ∈ ℝ+,
((⌊‘𝑥) ·
(log‘(⌊‘𝑥))), 0)) |
415 | | iftrue 4417 |
. . . . . . . . . . . . . . . . . 18
⊢
((⌊‘𝑥)
∈ ℝ+ → if((⌊‘𝑥) ∈ ℝ+,
((⌊‘𝑥) ·
(log‘(⌊‘𝑥))), 0) = ((⌊‘𝑥) · (log‘(⌊‘𝑥)))) |
416 | 414, 415 | eqtrd 2773 |
. . . . . . . . . . . . . . . . 17
⊢
((⌊‘𝑥)
∈ ℝ+ → (𝑇‘(⌊‘𝑥)) = ((⌊‘𝑥) · (log‘(⌊‘𝑥)))) |
417 | 404, 416 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑇‘(⌊‘𝑥)) = ((⌊‘𝑥) · (log‘(⌊‘𝑥)))) |
418 | 404 | relogcld 25358 |
. . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (log‘(⌊‘𝑥)) ∈ ℝ) |
419 | 13 | nn0ge0d 12032 |
. . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 0 ≤ (⌊‘𝑥)) |
420 | 403 | nnge1d 11757 |
. . . . . . . . . . . . . . . . . 18
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 1 ≤ (⌊‘𝑥)) |
421 | 46, 420 | logge0d 25365 |
. . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 0 ≤ (log‘(⌊‘𝑥))) |
422 | | flle 13253 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℝ →
(⌊‘𝑥) ≤
𝑥) |
423 | 2, 422 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (⌊‘𝑥) ≤ 𝑥) |
424 | 404, 10 | logled 25362 |
. . . . . . . . . . . . . . . . . 18
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((⌊‘𝑥) ≤ 𝑥 ↔ (log‘(⌊‘𝑥)) ≤ (log‘𝑥))) |
425 | 423, 424 | mpbid 235 |
. . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (log‘(⌊‘𝑥)) ≤ (log‘𝑥)) |
426 | 46, 2, 418, 277, 419, 421, 423, 425 | lemul12ad 11653 |
. . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((⌊‘𝑥) · (log‘(⌊‘𝑥))) ≤ (𝑥 · (log‘𝑥))) |
427 | 417, 426 | eqbrtrd 5049 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑇‘(⌊‘𝑥)) ≤ (𝑥 · (log‘𝑥))) |
428 | 89, 398, 23, 401, 427 | lemul2ad 11651 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (2 · (𝑇‘(⌊‘𝑥))) ≤ (2 · (𝑥 · (log‘𝑥)))) |
429 | 90, 23, 340 | ledivmul2d 12561 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥))) ≤ 2 ↔ (2 · (𝑇‘(⌊‘𝑥))) ≤ (2 · (𝑥 · (log‘𝑥))))) |
430 | 428, 429 | mpbird 260 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥))) ≤ 2) |
431 | 430 | adantrr 717 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ (𝑥
∈ (1(,)+∞) ∧ 1 ≤ 𝑥)) → ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥))) ≤ 2) |
432 | 356, 366,
357, 397, 431 | ello1d 14963 |
. . . . . . . . . . 11
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥)))) ∈
≤𝑂(1)) |
433 | | 0red 10715 |
. . . . . . . . . . . 12
⊢ (⊤
→ 0 ∈ ℝ) |
434 | 46, 418, 419, 421 | mulge0d 11288 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 0 ≤ ((⌊‘𝑥) · (log‘(⌊‘𝑥)))) |
435 | 434, 417 | breqtrrd 5055 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 0 ≤ (𝑇‘(⌊‘𝑥))) |
436 | 23, 89, 401, 435 | mulge0d 11288 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 0 ≤ (2 · (𝑇‘(⌊‘𝑥)))) |
437 | 90, 340, 436 | divge0d 12547 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 0 ≤ ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥)))) |
438 | 366, 433,
437 | o1lo12 14978 |
. . . . . . . . . . 11
⊢ (⊤
→ ((𝑥 ∈
(1(,)+∞) ↦ ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1) ↔ (𝑥 ∈ (1(,)+∞) ↦
((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥)))) ∈
≤𝑂(1))) |
439 | 432, 438 | mpbird 260 |
. . . . . . . . . 10
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1)) |
440 | 365, 366,
396, 439 | o1sub2 15066 |
. . . . . . . . 9
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) − ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥))))) ∈ 𝑂(1)) |
441 | 364, 440 | eqeltrd 2833 |
. . . . . . . 8
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1)) |
442 | 352, 441 | o1lo1d 14979 |
. . . . . . 7
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) ∈
≤𝑂(1)) |
443 | 21, 352, 360, 442, 41 | lo1mul 15068 |
. . . . . 6
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ ((𝑥
/ ((⌊‘𝑥) + 1))
· (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥))))) ∈
≤𝑂(1)) |
444 | 47 | selbergsb 26303 |
. . . . . . . 8
⊢
∃𝑐 ∈
ℝ+ ∀𝑦 ∈ (1[,)+∞)(abs‘(((𝑆‘𝑦) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝑐 |
445 | | simpl 486 |
. . . . . . . . . 10
⊢ ((𝑐 ∈ ℝ+
∧ ∀𝑦 ∈
(1[,)+∞)(abs‘(((𝑆‘𝑦) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝑐) → 𝑐 ∈ ℝ+) |
446 | | simpr 488 |
. . . . . . . . . 10
⊢ ((𝑐 ∈ ℝ+
∧ ∀𝑦 ∈
(1[,)+∞)(abs‘(((𝑆‘𝑦) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝑐) → ∀𝑦 ∈ (1[,)+∞)(abs‘(((𝑆‘𝑦) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝑐) |
447 | 47, 18, 445, 446 | pntrlog2bndlem3 26307 |
. . . . . . . . 9
⊢ ((𝑐 ∈ ℝ+
∧ ∀𝑦 ∈
(1[,)+∞)(abs‘(((𝑆‘𝑦) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝑐) → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1)) |
448 | 447 | rexlimiva 3190 |
. . . . . . . 8
⊢
(∃𝑐 ∈
ℝ+ ∀𝑦 ∈ (1[,)+∞)(abs‘(((𝑆‘𝑦) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝑐 → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1)) |
449 | 444, 448 | mp1i 13 |
. . . . . . 7
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1)) |
450 | 354, 449 | o1lo1d 14979 |
. . . . . 6
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥)))) ∈
≤𝑂(1)) |
451 | 353, 354,
443, 450 | lo1add 15067 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (((𝑥
/ ((⌊‘𝑥) + 1))
· (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥))))) ∈
≤𝑂(1)) |
452 | 351, 451 | eqeltrd 2833 |
. . . 4
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥)))) ∈
≤𝑂(1)) |
453 | 337, 341,
343, 452 | lo1add 15067 |
. . 3
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥) + ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))))) ∈
≤𝑂(1)) |
454 | 336, 453 | eqeltrrd 2834 |
. 2
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / 𝑥)) ∈ ≤𝑂(1)) |
455 | 454 | mptru 1549 |
1
⊢ (𝑥 ∈ (1(,)+∞) ↦
((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / 𝑥)) ∈ ≤𝑂(1) |