| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elioore 13418 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ (1(,)+∞) →
𝑥 ∈
ℝ) | 
| 2 | 1 | adantl 481 | . . . . . . . . . . . . . . . . . . 19
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 𝑥 ∈ ℝ) | 
| 3 |  | 1rp 13039 | . . . . . . . . . . . . . . . . . . . 20
⊢ 1 ∈
ℝ+ | 
| 4 | 3 | a1i 11 | . . . . . . . . . . . . . . . . . . 19
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 1 ∈ ℝ+) | 
| 5 |  | 1red 11263 | . . . . . . . . . . . . . . . . . . . 20
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 1 ∈ ℝ) | 
| 6 |  | eliooord 13447 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ (1(,)+∞) → (1
< 𝑥 ∧ 𝑥 <
+∞)) | 
| 7 | 6 | adantl 481 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (1 < 𝑥 ∧ 𝑥 < +∞)) | 
| 8 | 7 | simpld 494 | . . . . . . . . . . . . . . . . . . . 20
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 1 < 𝑥) | 
| 9 | 5, 2, 8 | ltled 11410 | . . . . . . . . . . . . . . . . . . 19
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 1 ≤ 𝑥) | 
| 10 | 2, 4, 9 | rpgecld 13117 | . . . . . . . . . . . . . . . . . 18
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 𝑥 ∈ ℝ+) | 
| 11 | 10 | rprege0d 13085 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥)) | 
| 12 |  | flge0nn0 13861 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) →
(⌊‘𝑥) ∈
ℕ0) | 
| 13 | 11, 12 | syl 17 | . . . . . . . . . . . . . . . . . . . 20
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (⌊‘𝑥) ∈
ℕ0) | 
| 14 |  | nn0p1nn 12567 | . . . . . . . . . . . . . . . . . . . 20
⊢
((⌊‘𝑥)
∈ ℕ0 → ((⌊‘𝑥) + 1) ∈ ℕ) | 
| 15 | 13, 14 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((⌊‘𝑥) + 1) ∈ ℕ) | 
| 16 | 15 | nnrpd 13076 | . . . . . . . . . . . . . . . . . 18
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((⌊‘𝑥) + 1) ∈
ℝ+) | 
| 17 | 10, 16 | rpdivcld 13095 | . . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑥 / ((⌊‘𝑥) + 1)) ∈
ℝ+) | 
| 18 |  | pntrlog2bnd.r | . . . . . . . . . . . . . . . . . 18
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦
((ψ‘𝑎) −
𝑎)) | 
| 19 | 18 | pntrval 27607 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑥 / ((⌊‘𝑥) + 1)) ∈
ℝ+ → (𝑅‘(𝑥 / ((⌊‘𝑥) + 1))) = ((ψ‘(𝑥 / ((⌊‘𝑥) + 1))) − (𝑥 / ((⌊‘𝑥) + 1)))) | 
| 20 | 17, 19 | syl 17 | . . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑅‘(𝑥 / ((⌊‘𝑥) + 1))) = ((ψ‘(𝑥 / ((⌊‘𝑥) + 1))) − (𝑥 / ((⌊‘𝑥) + 1)))) | 
| 21 | 2, 15 | nndivred 12321 | . . . . . . . . . . . . . . . . . . 19
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑥 / ((⌊‘𝑥) + 1)) ∈ ℝ) | 
| 22 |  | 2re 12341 | . . . . . . . . . . . . . . . . . . . 20
⊢ 2 ∈
ℝ | 
| 23 | 22 | a1i 11 | . . . . . . . . . . . . . . . . . . 19
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 2 ∈ ℝ) | 
| 24 |  | flltp1 13841 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ ℝ → 𝑥 < ((⌊‘𝑥) + 1)) | 
| 25 | 2, 24 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 𝑥 < ((⌊‘𝑥) + 1)) | 
| 26 | 15 | nncnd 12283 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((⌊‘𝑥) + 1) ∈ ℂ) | 
| 27 | 26 | mulridd 11279 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((⌊‘𝑥) + 1) · 1) = ((⌊‘𝑥) + 1)) | 
| 28 | 25, 27 | breqtrrd 5170 | . . . . . . . . . . . . . . . . . . . 20
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 𝑥 < (((⌊‘𝑥) + 1) · 1)) | 
| 29 | 2, 5, 16 | ltdivmuld 13129 | . . . . . . . . . . . . . . . . . . . 20
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((𝑥 / ((⌊‘𝑥) + 1)) < 1 ↔ 𝑥 < (((⌊‘𝑥) + 1) · 1))) | 
| 30 | 28, 29 | mpbird 257 | . . . . . . . . . . . . . . . . . . 19
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑥 / ((⌊‘𝑥) + 1)) < 1) | 
| 31 |  | 1lt2 12438 | . . . . . . . . . . . . . . . . . . . 20
⊢ 1 <
2 | 
| 32 | 31 | a1i 11 | . . . . . . . . . . . . . . . . . . 19
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 1 < 2) | 
| 33 | 21, 5, 23, 30, 32 | lttrd 11423 | . . . . . . . . . . . . . . . . . 18
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑥 / ((⌊‘𝑥) + 1)) < 2) | 
| 34 |  | chpeq0 27253 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 / ((⌊‘𝑥) + 1)) ∈ ℝ →
((ψ‘(𝑥 /
((⌊‘𝑥) + 1))) =
0 ↔ (𝑥 /
((⌊‘𝑥) + 1))
< 2)) | 
| 35 | 21, 34 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((ψ‘(𝑥 / ((⌊‘𝑥) + 1))) = 0 ↔ (𝑥 / ((⌊‘𝑥) + 1)) < 2)) | 
| 36 | 33, 35 | mpbird 257 | . . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (ψ‘(𝑥 / ((⌊‘𝑥) + 1))) = 0) | 
| 37 | 36 | oveq1d 7447 | . . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((ψ‘(𝑥 / ((⌊‘𝑥) + 1))) − (𝑥 / ((⌊‘𝑥) + 1))) = (0 − (𝑥 / ((⌊‘𝑥) + 1)))) | 
| 38 | 20, 37 | eqtrd 2776 | . . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑅‘(𝑥 / ((⌊‘𝑥) + 1))) = (0 − (𝑥 / ((⌊‘𝑥) + 1)))) | 
| 39 | 38 | fveq2d 6909 | . . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) = (abs‘(0 − (𝑥 / ((⌊‘𝑥) + 1))))) | 
| 40 |  | 0red 11265 | . . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 0 ∈ ℝ) | 
| 41 | 17 | rpge0d 13082 | . . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 0 ≤ (𝑥 / ((⌊‘𝑥) + 1))) | 
| 42 | 40, 21, 41 | abssuble0d 15472 | . . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘(0 − (𝑥 / ((⌊‘𝑥) + 1)))) = ((𝑥 / ((⌊‘𝑥) + 1)) − 0)) | 
| 43 | 21 | recnd 11290 | . . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑥 / ((⌊‘𝑥) + 1)) ∈ ℂ) | 
| 44 | 43 | subid1d 11610 | . . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((𝑥 / ((⌊‘𝑥) + 1)) − 0) = (𝑥 / ((⌊‘𝑥) + 1))) | 
| 45 | 39, 42, 44 | 3eqtrd 2780 | . . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) = (𝑥 / ((⌊‘𝑥) + 1))) | 
| 46 | 13 | nn0red 12590 | . . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (⌊‘𝑥) ∈ ℝ) | 
| 47 |  | pntsval.1 | . . . . . . . . . . . . . . . . 17
⊢ 𝑆 = (𝑎 ∈ ℝ ↦ Σ𝑖 ∈
(1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖))))) | 
| 48 | 47 | pntsval2 27621 | . . . . . . . . . . . . . . . 16
⊢
((⌊‘𝑥)
∈ ℝ → (𝑆‘(⌊‘𝑥)) = Σ𝑛 ∈
(1...(⌊‘(⌊‘𝑥)))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))))) | 
| 49 | 46, 48 | syl 17 | . . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑆‘(⌊‘𝑥)) = Σ𝑛 ∈
(1...(⌊‘(⌊‘𝑥)))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))))) | 
| 50 | 13 | nn0cnd 12591 | . . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (⌊‘𝑥) ∈ ℂ) | 
| 51 |  | 1cnd 11257 | . . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 1 ∈ ℂ) | 
| 52 | 50, 51 | pncand 11622 | . . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((⌊‘𝑥) + 1) − 1) = (⌊‘𝑥)) | 
| 53 | 52 | fveq2d 6909 | . . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑆‘(((⌊‘𝑥) + 1) − 1)) = (𝑆‘(⌊‘𝑥))) | 
| 54 | 47 | pntsval2 27621 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℝ → (𝑆‘𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))))) | 
| 55 | 2, 54 | syl 17 | . . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑆‘𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))))) | 
| 56 |  | flidm 13850 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℝ →
(⌊‘(⌊‘𝑥)) = (⌊‘𝑥)) | 
| 57 | 2, 56 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (⌊‘(⌊‘𝑥)) = (⌊‘𝑥)) | 
| 58 | 57 | oveq2d 7448 | . . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (1...(⌊‘(⌊‘𝑥))) = (1...(⌊‘𝑥))) | 
| 59 | 58 | sumeq1d 15737 | . . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘(⌊‘𝑥)))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))))) | 
| 60 | 55, 59 | eqtr4d 2779 | . . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑆‘𝑥) = Σ𝑛 ∈
(1...(⌊‘(⌊‘𝑥)))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))))) | 
| 61 | 49, 53, 60 | 3eqtr4d 2786 | . . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑆‘(((⌊‘𝑥) + 1) − 1)) = (𝑆‘𝑥)) | 
| 62 | 52 | fveq2d 6909 | . . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑇‘(((⌊‘𝑥) + 1) − 1)) = (𝑇‘(⌊‘𝑥))) | 
| 63 | 62 | oveq2d 7448 | . . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1))) = (2 · (𝑇‘(⌊‘𝑥)))) | 
| 64 | 61, 63 | oveq12d 7450 | . . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1)))) = ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) | 
| 65 | 45, 64 | oveq12d 7450 | . . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) · ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1))))) = ((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))))) | 
| 66 | 2 | recnd 11290 | . . . . . . . . . . . . . . . . . . 19
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 𝑥 ∈ ℂ) | 
| 67 | 66 | div1d 12036 | . . . . . . . . . . . . . . . . . 18
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑥 / 1) = 𝑥) | 
| 68 | 67 | fveq2d 6909 | . . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑅‘(𝑥 / 1)) = (𝑅‘𝑥)) | 
| 69 | 18 | pntrf 27608 | . . . . . . . . . . . . . . . . . . 19
⊢ 𝑅:ℝ+⟶ℝ | 
| 70 | 69 | ffvelcdmi 7102 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℝ+
→ (𝑅‘𝑥) ∈
ℝ) | 
| 71 | 10, 70 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑅‘𝑥) ∈ ℝ) | 
| 72 | 68, 71 | eqeltrd 2840 | . . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑅‘(𝑥 / 1)) ∈ ℝ) | 
| 73 | 72 | recnd 11290 | . . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑅‘(𝑥 / 1)) ∈ ℂ) | 
| 74 | 73 | abscld 15476 | . . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘(𝑅‘(𝑥 / 1))) ∈ ℝ) | 
| 75 | 74 | recnd 11290 | . . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘(𝑅‘(𝑥 / 1))) ∈ ℂ) | 
| 76 | 75 | mul01d 11461 | . . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((abs‘(𝑅‘(𝑥 / 1))) · 0) = 0) | 
| 77 | 65, 76 | oveq12d 7450 | . . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) · ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1))))) −
((abs‘(𝑅‘(𝑥 / 1))) · 0)) = (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) − 0)) | 
| 78 | 47 | pntsf 27618 | . . . . . . . . . . . . . . . . 17
⊢ 𝑆:ℝ⟶ℝ | 
| 79 | 78 | ffvelcdmi 7102 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℝ → (𝑆‘𝑥) ∈ ℝ) | 
| 80 | 2, 79 | syl 17 | . . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑆‘𝑥) ∈ ℝ) | 
| 81 |  | pntrlog2bnd.t | . . . . . . . . . . . . . . . . . . 19
⊢ 𝑇 = (𝑎 ∈ ℝ ↦ if(𝑎 ∈ ℝ+, (𝑎 · (log‘𝑎)), 0)) | 
| 82 |  | relogcl 26618 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 ∈ ℝ+
→ (log‘𝑎) ∈
ℝ) | 
| 83 |  | remulcl 11241 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎 ∈ ℝ ∧
(log‘𝑎) ∈
ℝ) → (𝑎 ·
(log‘𝑎)) ∈
ℝ) | 
| 84 | 82, 83 | sylan2 593 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 ∈ ℝ ∧ 𝑎 ∈ ℝ+)
→ (𝑎 ·
(log‘𝑎)) ∈
ℝ) | 
| 85 |  | 0red 11265 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 ∈ ℝ ∧ ¬
𝑎 ∈
ℝ+) → 0 ∈ ℝ) | 
| 86 | 84, 85 | ifclda 4560 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 ∈ ℝ → if(𝑎 ∈ ℝ+,
(𝑎 ·
(log‘𝑎)), 0) ∈
ℝ) | 
| 87 | 81, 86 | fmpti 7131 | . . . . . . . . . . . . . . . . . 18
⊢ 𝑇:ℝ⟶ℝ | 
| 88 | 87 | ffvelcdmi 7102 | . . . . . . . . . . . . . . . . 17
⊢
((⌊‘𝑥)
∈ ℝ → (𝑇‘(⌊‘𝑥)) ∈ ℝ) | 
| 89 | 46, 88 | syl 17 | . . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑇‘(⌊‘𝑥)) ∈ ℝ) | 
| 90 | 23, 89 | remulcld 11292 | . . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (2 · (𝑇‘(⌊‘𝑥))) ∈ ℝ) | 
| 91 | 80, 90 | resubcld 11692 | . . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) ∈ ℝ) | 
| 92 | 21, 91 | remulcld 11292 | . . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) ∈ ℝ) | 
| 93 | 92 | recnd 11290 | . . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) ∈ ℂ) | 
| 94 | 93 | subid1d 11610 | . . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) − 0) = ((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))))) | 
| 95 | 77, 94 | eqtrd 2776 | . . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) · ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) − 1))))) −
((abs‘(𝑅‘(𝑥 / 1))) · 0)) = ((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))))) | 
| 96 | 2 | flcld 13839 | . . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (⌊‘𝑥) ∈ ℤ) | 
| 97 |  | fzval3 13774 | . . . . . . . . . . . . . 14
⊢
((⌊‘𝑥)
∈ ℤ → (1...(⌊‘𝑥)) = (1..^((⌊‘𝑥) + 1))) | 
| 98 | 96, 97 | syl 17 | . . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (1...(⌊‘𝑥)) = (1..^((⌊‘𝑥) + 1))) | 
| 99 | 98 | eqcomd 2742 | . . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (1..^((⌊‘𝑥) + 1)) = (1...(⌊‘𝑥))) | 
| 100 | 10 | adantr 480 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ+) | 
| 101 |  | elfznn 13594 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℕ) | 
| 102 | 101 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ) | 
| 103 | 102 | nnrpd 13076 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ+) | 
| 104 | 100, 103 | rpdivcld 13095 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈
ℝ+) | 
| 105 | 69 | ffvelcdmi 7102 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 / 𝑛) ∈ ℝ+ → (𝑅‘(𝑥 / 𝑛)) ∈ ℝ) | 
| 106 | 104, 105 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘(𝑥 / 𝑛)) ∈ ℝ) | 
| 107 | 106 | recnd 11290 | . . . . . . . . . . . . . . . . . 18
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘(𝑥 / 𝑛)) ∈ ℂ) | 
| 108 | 107 | abscld 15476 | . . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑅‘(𝑥 / 𝑛))) ∈ ℝ) | 
| 109 | 108 | recnd 11290 | . . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑅‘(𝑥 / 𝑛))) ∈ ℂ) | 
| 110 | 3 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈
ℝ+) | 
| 111 | 103, 110 | rpaddcld 13093 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 + 1) ∈
ℝ+) | 
| 112 | 100, 111 | rpdivcld 13095 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / (𝑛 + 1)) ∈
ℝ+) | 
| 113 | 69 | ffvelcdmi 7102 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 / (𝑛 + 1)) ∈ ℝ+ →
(𝑅‘(𝑥 / (𝑛 + 1))) ∈ ℝ) | 
| 114 | 112, 113 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘(𝑥 / (𝑛 + 1))) ∈ ℝ) | 
| 115 | 114 | recnd 11290 | . . . . . . . . . . . . . . . . . 18
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘(𝑥 / (𝑛 + 1))) ∈ ℂ) | 
| 116 | 115 | abscld 15476 | . . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) ∈ ℝ) | 
| 117 | 116 | recnd 11290 | . . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) ∈ ℂ) | 
| 118 | 109, 117 | negsubdi2d 11637 | . . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → -((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) = ((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛))))) | 
| 119 | 118 | eqcomd 2742 | . . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))) = -((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1)))))) | 
| 120 | 102 | nncnd 12283 | . . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℂ) | 
| 121 |  | 1cnd 11257 | . . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈
ℂ) | 
| 122 | 120, 121 | pncand 11622 | . . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) − 1) = 𝑛) | 
| 123 | 122 | fveq2d 6909 | . . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘((𝑛 + 1) − 1)) = (𝑆‘𝑛)) | 
| 124 | 122 | fveq2d 6909 | . . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇‘((𝑛 + 1) − 1)) = (𝑇‘𝑛)) | 
| 125 |  | rpre 13044 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ ℝ+
→ 𝑛 ∈
ℝ) | 
| 126 |  | eleq1 2828 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 = 𝑛 → (𝑎 ∈ ℝ+ ↔ 𝑛 ∈
ℝ+)) | 
| 127 |  | id 22 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑎 = 𝑛 → 𝑎 = 𝑛) | 
| 128 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑎 = 𝑛 → (log‘𝑎) = (log‘𝑛)) | 
| 129 | 127, 128 | oveq12d 7450 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 = 𝑛 → (𝑎 · (log‘𝑎)) = (𝑛 · (log‘𝑛))) | 
| 130 | 126, 129 | ifbieq1d 4549 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 = 𝑛 → if(𝑎 ∈ ℝ+, (𝑎 · (log‘𝑎)), 0) = if(𝑛 ∈ ℝ+, (𝑛 · (log‘𝑛)), 0)) | 
| 131 |  | ovex 7465 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 · (log‘𝑛)) ∈ V | 
| 132 |  | c0ex 11256 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ 0 ∈
V | 
| 133 | 131, 132 | ifex 4575 | . . . . . . . . . . . . . . . . . . . . 21
⊢ if(𝑛 ∈ ℝ+,
(𝑛 ·
(log‘𝑛)), 0) ∈
V | 
| 134 | 130, 81, 133 | fvmpt 7015 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ ℝ → (𝑇‘𝑛) = if(𝑛 ∈ ℝ+, (𝑛 · (log‘𝑛)), 0)) | 
| 135 | 125, 134 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℝ+
→ (𝑇‘𝑛) = if(𝑛 ∈ ℝ+, (𝑛 · (log‘𝑛)), 0)) | 
| 136 |  | iftrue 4530 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℝ+
→ if(𝑛 ∈
ℝ+, (𝑛
· (log‘𝑛)), 0)
= (𝑛 ·
(log‘𝑛))) | 
| 137 | 135, 136 | eqtrd 2776 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ℝ+
→ (𝑇‘𝑛) = (𝑛 · (log‘𝑛))) | 
| 138 | 103, 137 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇‘𝑛) = (𝑛 · (log‘𝑛))) | 
| 139 | 124, 138 | eqtrd 2776 | . . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇‘((𝑛 + 1) − 1)) = (𝑛 · (log‘𝑛))) | 
| 140 | 139 | oveq2d 7448 | . . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑇‘((𝑛 + 1) − 1))) = (2 · (𝑛 · (log‘𝑛)))) | 
| 141 | 123, 140 | oveq12d 7450 | . . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))) = ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) | 
| 142 | 119, 141 | oveq12d 7450 | . . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))) · ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1))))) = (-((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) | 
| 143 | 108, 116 | resubcld 11692 | . . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) ∈ ℝ) | 
| 144 | 143 | recnd 11290 | . . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) ∈ ℂ) | 
| 145 | 102 | nnred 12282 | . . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ) | 
| 146 | 78 | ffvelcdmi 7102 | . . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℝ → (𝑆‘𝑛) ∈ ℝ) | 
| 147 | 145, 146 | syl 17 | . . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘𝑛) ∈ ℝ) | 
| 148 | 22 | a1i 11 | . . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 2 ∈
ℝ) | 
| 149 | 103 | relogcld 26666 | . . . . . . . . . . . . . . . . . 18
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘𝑛) ∈
ℝ) | 
| 150 | 145, 149 | remulcld 11292 | . . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 · (log‘𝑛)) ∈ ℝ) | 
| 151 | 148, 150 | remulcld 11292 | . . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑛 · (log‘𝑛))) ∈
ℝ) | 
| 152 | 147, 151 | resubcld 11692 | . . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))) ∈ ℝ) | 
| 153 | 152 | recnd 11290 | . . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))) ∈ ℂ) | 
| 154 | 144, 153 | mulneg1d 11717 | . . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (-((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) = -(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) | 
| 155 | 142, 154 | eqtrd 2776 | . . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))) · ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1))))) = -(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) | 
| 156 | 99, 155 | sumeq12rdv 15744 | . . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))(((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))) · ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1))))) = Σ𝑛 ∈
(1...(⌊‘𝑥))-(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) | 
| 157 |  | fzfid 14015 | . . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (1...(⌊‘𝑥)) ∈ Fin) | 
| 158 | 143, 152 | remulcld 11292 | . . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) ∈ ℝ) | 
| 159 | 158 | recnd 11290 | . . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) ∈ ℂ) | 
| 160 | 157, 159 | fsumneg 15824 | . . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))-(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) = -Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) | 
| 161 | 156, 160 | eqtrd 2776 | . . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))(((abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) − (abs‘(𝑅‘(𝑥 / 𝑛)))) · ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1))))) = -Σ𝑛 ∈
(1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) | 
| 162 | 95, 161 | oveq12d 7450 | . . . . . . . . 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 7440 | . . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑛 → (𝑥 / 𝑚) = (𝑥 / 𝑛)) | 
| 164 | 163 | fveq2d 6909 | . . . . . . . . . . . . 13
⊢ (𝑚 = 𝑛 → (𝑅‘(𝑥 / 𝑚)) = (𝑅‘(𝑥 / 𝑛))) | 
| 165 | 164 | fveq2d 6909 | . . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → (abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / 𝑛)))) | 
| 166 |  | fvoveq1 7455 | . . . . . . . . . . . . 13
⊢ (𝑚 = 𝑛 → (𝑆‘(𝑚 − 1)) = (𝑆‘(𝑛 − 1))) | 
| 167 |  | fvoveq1 7455 | . . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑛 → (𝑇‘(𝑚 − 1)) = (𝑇‘(𝑛 − 1))) | 
| 168 | 167 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢ (𝑚 = 𝑛 → (2 · (𝑇‘(𝑚 − 1))) = (2 · (𝑇‘(𝑛 − 1)))) | 
| 169 | 166, 168 | oveq12d 7450 | . . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1))))) | 
| 170 | 165, 169 | jca 511 | . . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → ((abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / 𝑛))) ∧ ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1)))))) | 
| 171 |  | oveq2 7440 | . . . . . . . . . . . . . 14
⊢ (𝑚 = (𝑛 + 1) → (𝑥 / 𝑚) = (𝑥 / (𝑛 + 1))) | 
| 172 | 171 | fveq2d 6909 | . . . . . . . . . . . . 13
⊢ (𝑚 = (𝑛 + 1) → (𝑅‘(𝑥 / 𝑚)) = (𝑅‘(𝑥 / (𝑛 + 1)))) | 
| 173 | 172 | fveq2d 6909 | . . . . . . . . . . . 12
⊢ (𝑚 = (𝑛 + 1) → (abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) | 
| 174 |  | fvoveq1 7455 | . . . . . . . . . . . . 13
⊢ (𝑚 = (𝑛 + 1) → (𝑆‘(𝑚 − 1)) = (𝑆‘((𝑛 + 1) − 1))) | 
| 175 |  | fvoveq1 7455 | . . . . . . . . . . . . . 14
⊢ (𝑚 = (𝑛 + 1) → (𝑇‘(𝑚 − 1)) = (𝑇‘((𝑛 + 1) − 1))) | 
| 176 | 175 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢ (𝑚 = (𝑛 + 1) → (2 · (𝑇‘(𝑚 − 1))) = (2 · (𝑇‘((𝑛 + 1) − 1)))) | 
| 177 | 174, 176 | oveq12d 7450 | . . . . . . . . . . . 12
⊢ (𝑚 = (𝑛 + 1) → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1))))) | 
| 178 | 173, 177 | jca 511 | . . . . . . . . . . 11
⊢ (𝑚 = (𝑛 + 1) → ((abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / (𝑛 + 1)))) ∧ ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))))) | 
| 179 |  | oveq2 7440 | . . . . . . . . . . . . . 14
⊢ (𝑚 = 1 → (𝑥 / 𝑚) = (𝑥 / 1)) | 
| 180 | 179 | fveq2d 6909 | . . . . . . . . . . . . 13
⊢ (𝑚 = 1 → (𝑅‘(𝑥 / 𝑚)) = (𝑅‘(𝑥 / 1))) | 
| 181 | 180 | fveq2d 6909 | . . . . . . . . . . . 12
⊢ (𝑚 = 1 → (abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / 1)))) | 
| 182 |  | oveq1 7439 | . . . . . . . . . . . . . . . . 17
⊢ (𝑚 = 1 → (𝑚 − 1) = (1 − 1)) | 
| 183 |  | 1m1e0 12339 | . . . . . . . . . . . . . . . . 17
⊢ (1
− 1) = 0 | 
| 184 | 182, 183 | eqtrdi 2792 | . . . . . . . . . . . . . . . 16
⊢ (𝑚 = 1 → (𝑚 − 1) = 0) | 
| 185 | 184 | fveq2d 6909 | . . . . . . . . . . . . . . 15
⊢ (𝑚 = 1 → (𝑆‘(𝑚 − 1)) = (𝑆‘0)) | 
| 186 |  | 0re 11264 | . . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℝ | 
| 187 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 = 0 → (⌊‘𝑎) =
(⌊‘0)) | 
| 188 |  | 0z 12626 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ 0 ∈
ℤ | 
| 189 |  | flid 13849 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (0 ∈
ℤ → (⌊‘0) = 0) | 
| 190 | 188, 189 | ax-mp 5 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(⌊‘0) = 0 | 
| 191 | 187, 190 | eqtrdi 2792 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 = 0 → (⌊‘𝑎) = 0) | 
| 192 | 191 | oveq2d 7448 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 = 0 →
(1...(⌊‘𝑎)) =
(1...0)) | 
| 193 |  | fz10 13586 | . . . . . . . . . . . . . . . . . . . 20
⊢ (1...0) =
∅ | 
| 194 | 192, 193 | eqtrdi 2792 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = 0 →
(1...(⌊‘𝑎)) =
∅) | 
| 195 | 194 | sumeq1d 15737 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = 0 → Σ𝑖 ∈
(1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))) = Σ𝑖 ∈ ∅ ((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖))))) | 
| 196 |  | sum0 15758 | . . . . . . . . . . . . . . . . . 18
⊢
Σ𝑖 ∈
∅ ((Λ‘𝑖)
· ((log‘𝑖) +
(ψ‘(𝑎 / 𝑖)))) = 0 | 
| 197 | 195, 196 | eqtrdi 2792 | . . . . . . . . . . . . . . . . 17
⊢ (𝑎 = 0 → Σ𝑖 ∈
(1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))) = 0) | 
| 198 | 197, 47, 132 | fvmpt 7015 | . . . . . . . . . . . . . . . 16
⊢ (0 ∈
ℝ → (𝑆‘0)
= 0) | 
| 199 | 186, 198 | ax-mp 5 | . . . . . . . . . . . . . . 15
⊢ (𝑆‘0) = 0 | 
| 200 | 185, 199 | eqtrdi 2792 | . . . . . . . . . . . . . 14
⊢ (𝑚 = 1 → (𝑆‘(𝑚 − 1)) = 0) | 
| 201 | 184 | fveq2d 6909 | . . . . . . . . . . . . . . . . 17
⊢ (𝑚 = 1 → (𝑇‘(𝑚 − 1)) = (𝑇‘0)) | 
| 202 |  | rpne0 13052 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 ∈ ℝ+
→ 𝑎 ≠
0) | 
| 203 | 202 | necon2bi 2970 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 = 0 → ¬ 𝑎 ∈
ℝ+) | 
| 204 | 203 | iffalsed 4535 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = 0 → if(𝑎 ∈ ℝ+,
(𝑎 ·
(log‘𝑎)), 0) =
0) | 
| 205 | 204, 81, 132 | fvmpt 7015 | . . . . . . . . . . . . . . . . . 18
⊢ (0 ∈
ℝ → (𝑇‘0)
= 0) | 
| 206 | 186, 205 | ax-mp 5 | . . . . . . . . . . . . . . . . 17
⊢ (𝑇‘0) = 0 | 
| 207 | 201, 206 | eqtrdi 2792 | . . . . . . . . . . . . . . . 16
⊢ (𝑚 = 1 → (𝑇‘(𝑚 − 1)) = 0) | 
| 208 | 207 | oveq2d 7448 | . . . . . . . . . . . . . . 15
⊢ (𝑚 = 1 → (2 · (𝑇‘(𝑚 − 1))) = (2 ·
0)) | 
| 209 |  | 2t0e0 12436 | . . . . . . . . . . . . . . 15
⊢ (2
· 0) = 0 | 
| 210 | 208, 209 | eqtrdi 2792 | . . . . . . . . . . . . . 14
⊢ (𝑚 = 1 → (2 · (𝑇‘(𝑚 − 1))) = 0) | 
| 211 | 200, 210 | oveq12d 7450 | . . . . . . . . . . . . 13
⊢ (𝑚 = 1 → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = (0 −
0)) | 
| 212 |  | 0m0e0 12387 | . . . . . . . . . . . . 13
⊢ (0
− 0) = 0 | 
| 213 | 211, 212 | eqtrdi 2792 | . . . . . . . . . . . 12
⊢ (𝑚 = 1 → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = 0) | 
| 214 | 181, 213 | jca 511 | . . . . . . . . . . 11
⊢ (𝑚 = 1 → ((abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / 1))) ∧ ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = 0)) | 
| 215 |  | oveq2 7440 | . . . . . . . . . . . . . 14
⊢ (𝑚 = ((⌊‘𝑥) + 1) → (𝑥 / 𝑚) = (𝑥 / ((⌊‘𝑥) + 1))) | 
| 216 | 215 | fveq2d 6909 | . . . . . . . . . . . . 13
⊢ (𝑚 = ((⌊‘𝑥) + 1) → (𝑅‘(𝑥 / 𝑚)) = (𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) | 
| 217 | 216 | fveq2d 6909 | . . . . . . . . . . . 12
⊢ (𝑚 = ((⌊‘𝑥) + 1) → (abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1))))) | 
| 218 |  | fvoveq1 7455 | . . . . . . . . . . . . 13
⊢ (𝑚 = ((⌊‘𝑥) + 1) → (𝑆‘(𝑚 − 1)) = (𝑆‘(((⌊‘𝑥) + 1) − 1))) | 
| 219 |  | fvoveq1 7455 | . . . . . . . . . . . . . 14
⊢ (𝑚 = ((⌊‘𝑥) + 1) → (𝑇‘(𝑚 − 1)) = (𝑇‘(((⌊‘𝑥) + 1) − 1))) | 
| 220 | 219 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢ (𝑚 = ((⌊‘𝑥) + 1) → (2 · (𝑇‘(𝑚 − 1))) = (2 · (𝑇‘(((⌊‘𝑥) + 1) −
1)))) | 
| 221 | 218, 220 | oveq12d 7450 | . . . . . . . . . . . 12
⊢ (𝑚 = ((⌊‘𝑥) + 1) → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) −
1))))) | 
| 222 | 217, 221 | jca 511 | . . . . . . . . . . 11
⊢ (𝑚 = ((⌊‘𝑥) + 1) → ((abs‘(𝑅‘(𝑥 / 𝑚))) = (abs‘(𝑅‘(𝑥 / ((⌊‘𝑥) + 1)))) ∧ ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) = ((𝑆‘(((⌊‘𝑥) + 1) − 1)) − (2 · (𝑇‘(((⌊‘𝑥) + 1) −
1)))))) | 
| 223 |  | nnuz 12922 | . . . . . . . . . . . 12
⊢ ℕ =
(ℤ≥‘1) | 
| 224 | 15, 223 | eleqtrdi 2850 | . . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((⌊‘𝑥) + 1) ∈
(ℤ≥‘1)) | 
| 225 | 10 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 𝑥 ∈
ℝ+) | 
| 226 |  | elfznn 13594 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ∈
(1...((⌊‘𝑥) +
1)) → 𝑚 ∈
ℕ) | 
| 227 | 226 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 𝑚 ∈
ℕ) | 
| 228 | 227 | nnrpd 13076 | . . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 𝑚 ∈
ℝ+) | 
| 229 | 225, 228 | rpdivcld 13095 | . . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑥 / 𝑚) ∈
ℝ+) | 
| 230 | 69 | ffvelcdmi 7102 | . . . . . . . . . . . . . . 15
⊢ ((𝑥 / 𝑚) ∈ ℝ+ → (𝑅‘(𝑥 / 𝑚)) ∈ ℝ) | 
| 231 | 229, 230 | syl 17 | . . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑅‘(𝑥 / 𝑚)) ∈ ℝ) | 
| 232 | 231 | recnd 11290 | . . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑅‘(𝑥 / 𝑚)) ∈ ℂ) | 
| 233 | 232 | abscld 15476 | . . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) →
(abs‘(𝑅‘(𝑥 / 𝑚))) ∈ ℝ) | 
| 234 | 233 | recnd 11290 | . . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) →
(abs‘(𝑅‘(𝑥 / 𝑚))) ∈ ℂ) | 
| 235 | 227 | nnred 12282 | . . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 𝑚 ∈
ℝ) | 
| 236 |  | 1red 11263 | . . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 1 ∈
ℝ) | 
| 237 | 235, 236 | resubcld 11692 | . . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑚 − 1) ∈
ℝ) | 
| 238 | 78 | ffvelcdmi 7102 | . . . . . . . . . . . . . 14
⊢ ((𝑚 − 1) ∈ ℝ
→ (𝑆‘(𝑚 − 1)) ∈
ℝ) | 
| 239 | 237, 238 | syl 17 | . . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑆‘(𝑚 − 1)) ∈ ℝ) | 
| 240 | 22 | a1i 11 | . . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 2 ∈
ℝ) | 
| 241 | 87 | ffvelcdmi 7102 | . . . . . . . . . . . . . . 15
⊢ ((𝑚 − 1) ∈ ℝ
→ (𝑇‘(𝑚 − 1)) ∈
ℝ) | 
| 242 | 237, 241 | syl 17 | . . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑇‘(𝑚 − 1)) ∈ ℝ) | 
| 243 | 240, 242 | remulcld 11292 | . . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (2 ·
(𝑇‘(𝑚 − 1))) ∈
ℝ) | 
| 244 | 239, 243 | resubcld 11692 | . . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) ∈
ℝ) | 
| 245 | 244 | recnd 11290 | . . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → ((𝑆‘(𝑚 − 1)) − (2 · (𝑇‘(𝑚 − 1)))) ∈
ℂ) | 
| 246 | 170, 178,
214, 222, 224, 234, 245 | fsumparts 15843 | . . . . . . . . . 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 11290 | . . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘𝑛) ∈ ℂ) | 
| 248 | 87 | ffvelcdmi 7102 | . . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℝ → (𝑇‘𝑛) ∈ ℝ) | 
| 249 | 145, 248 | syl 17 | . . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇‘𝑛) ∈ ℝ) | 
| 250 | 148, 249 | remulcld 11292 | . . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑇‘𝑛)) ∈ ℝ) | 
| 251 | 250 | recnd 11290 | . . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑇‘𝑛)) ∈ ℂ) | 
| 252 |  | 1red 11263 | . . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈
ℝ) | 
| 253 | 145, 252 | resubcld 11692 | . . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 − 1) ∈ ℝ) | 
| 254 | 78 | ffvelcdmi 7102 | . . . . . . . . . . . . . . . 16
⊢ ((𝑛 − 1) ∈ ℝ
→ (𝑆‘(𝑛 − 1)) ∈
ℝ) | 
| 255 | 253, 254 | syl 17 | . . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘(𝑛 − 1)) ∈ ℝ) | 
| 256 | 255 | recnd 11290 | . . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘(𝑛 − 1)) ∈ ℂ) | 
| 257 | 87 | ffvelcdmi 7102 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑛 − 1) ∈ ℝ
→ (𝑇‘(𝑛 − 1)) ∈
ℝ) | 
| 258 | 253, 257 | syl 17 | . . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇‘(𝑛 − 1)) ∈ ℝ) | 
| 259 | 148, 258 | remulcld 11292 | . . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑇‘(𝑛 − 1))) ∈
ℝ) | 
| 260 | 259 | recnd 11290 | . . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑇‘(𝑛 − 1))) ∈
ℂ) | 
| 261 | 247, 251,
256, 260 | sub4d 11670 | . . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆‘𝑛) − (2 · (𝑇‘𝑛))) − ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1))))) = (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − ((2 · (𝑇‘𝑛)) − (2 · (𝑇‘(𝑛 − 1)))))) | 
| 262 | 124 | oveq2d 7448 | . . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (𝑇‘((𝑛 + 1) − 1))) = (2 · (𝑇‘𝑛))) | 
| 263 | 123, 262 | oveq12d 7450 | . . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))) = ((𝑆‘𝑛) − (2 · (𝑇‘𝑛)))) | 
| 264 | 263 | oveq1d 7447 | . . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))) − ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1))))) = (((𝑆‘𝑛) − (2 · (𝑇‘𝑛))) − ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1)))))) | 
| 265 |  | 2cnd 12345 | . . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 2 ∈
ℂ) | 
| 266 | 249 | recnd 11290 | . . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇‘𝑛) ∈ ℂ) | 
| 267 | 258 | recnd 11290 | . . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇‘(𝑛 − 1)) ∈ ℂ) | 
| 268 | 265, 266,
267 | subdid 11720 | . . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))) = ((2 · (𝑇‘𝑛)) − (2 · (𝑇‘(𝑛 − 1))))) | 
| 269 | 268 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))) = (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − ((2 · (𝑇‘𝑛)) − (2 · (𝑇‘(𝑛 − 1)))))) | 
| 270 | 261, 264,
269 | 3eqtr4d 2786 | . . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))) − ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1))))) = (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) | 
| 271 | 270 | oveq2d 7448 | . . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))) − ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1)))))) = ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) | 
| 272 | 99, 271 | sumeq12rdv 15744 | . . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘((𝑛 + 1) − 1)) − (2 · (𝑇‘((𝑛 + 1) − 1)))) − ((𝑆‘(𝑛 − 1)) − (2 · (𝑇‘(𝑛 − 1)))))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) | 
| 273 | 246, 272 | eqtr3d 2778 | . . . . . . . . 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 15770 | . . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) ∈ ℂ) | 
| 275 | 93, 274 | subnegd 11628 | . . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) − -Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) = (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))))) | 
| 276 | 162, 273,
275 | 3eqtr3rd 2785 | . . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) | 
| 277 | 10 | relogcld 26666 | . . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (log‘𝑥) ∈ ℝ) | 
| 278 | 277 | recnd 11290 | . . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (log‘𝑥) ∈ ℂ) | 
| 279 | 66, 278 | mulcomd 11283 | . . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) = ((log‘𝑥) · 𝑥)) | 
| 280 | 276, 279 | oveq12d 7450 | . . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / ((log‘𝑥) · 𝑥))) | 
| 281 | 147, 255 | resubcld 11692 | . . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) ∈
ℝ) | 
| 282 | 249, 258 | resubcld 11692 | . . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))) ∈
ℝ) | 
| 283 | 148, 282 | remulcld 11292 | . . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))) ∈
ℝ) | 
| 284 | 281, 283 | resubcld 11692 | . . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))) ∈
ℝ) | 
| 285 | 108, 284 | remulcld 11292 | . . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) ∈
ℝ) | 
| 286 | 157, 285 | fsumrecl 15771 | . . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) ∈
ℝ) | 
| 287 | 286 | recnd 11290 | . . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) ∈
ℂ) | 
| 288 | 2, 8 | rplogcld 26672 | . . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (log‘𝑥) ∈
ℝ+) | 
| 289 | 288 | rpne0d 13083 | . . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (log‘𝑥) ≠ 0) | 
| 290 | 10 | rpne0d 13083 | . . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 𝑥 ≠ 0) | 
| 291 | 287, 278,
66, 289, 290 | divdiv1d 12075 | . . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥)) / 𝑥) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / ((log‘𝑥) · 𝑥))) | 
| 292 | 280, 291 | eqtr4d 2779 | . . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥)) / 𝑥)) | 
| 293 | 292 | oveq2d 7448 | . . . . 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 11290 | . . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑅‘𝑥) ∈ ℂ) | 
| 295 | 294 | abscld 15476 | . . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘(𝑅‘𝑥)) ∈ ℝ) | 
| 296 | 295, 277 | remulcld 11292 | . . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((abs‘(𝑅‘𝑥)) · (log‘𝑥)) ∈ ℝ) | 
| 297 | 108, 281 | remulcld 11292 | . . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) ∈
ℝ) | 
| 298 | 157, 297 | fsumrecl 15771 | . . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) ∈
ℝ) | 
| 299 | 298, 288 | rerpdivcld 13109 | . . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥)) ∈
ℝ) | 
| 300 | 296, 299 | resubcld 11692 | . . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) ∈
ℝ) | 
| 301 | 300 | recnd 11290 | . . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) ∈
ℂ) | 
| 302 | 287, 278,
289 | divcld 12044 | . . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥)) ∈
ℂ) | 
| 303 | 301, 302,
66, 290 | divdird 12082 | . . . . 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 11290 | . . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((abs‘(𝑅‘𝑥)) · (log‘𝑥)) ∈ ℂ) | 
| 305 | 299 | recnd 11290 | . . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥)) ∈
ℂ) | 
| 306 | 304, 305,
302 | subsubd 11649 | . . . . . . 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 12345 | . . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 2 ∈ ℂ) | 
| 308 | 266, 267 | subcld 11621 | . . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))) ∈
ℂ) | 
| 309 | 109, 308 | mulcld 11282 | . . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))) ∈
ℂ) | 
| 310 | 157, 307,
309 | fsummulc2 15821 | . . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(2 · ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) | 
| 311 | 281 | recnd 11290 | . . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) ∈
ℂ) | 
| 312 | 265, 308 | mulcld 11282 | . . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))) ∈
ℂ) | 
| 313 | 311, 312 | nncand 11626 | . . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) = (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))) | 
| 314 | 313 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) = ((abs‘(𝑅‘(𝑥 / 𝑛))) · (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) | 
| 315 | 284 | recnd 11290 | . . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))) ∈
ℂ) | 
| 316 | 109, 311,
315 | subdid 11720 | . . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) = (((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) − ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))))) | 
| 317 | 109, 265,
308 | mul12d 11471 | . . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))) = (2 ·
((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) | 
| 318 | 314, 316,
317 | 3eqtr3d 2784 | . . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) − ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) = (2 ·
((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) | 
| 319 | 318 | sumeq2dv 15739 | . . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) − ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(2 · ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) | 
| 320 | 297 | recnd 11290 | . . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) ∈
ℂ) | 
| 321 | 285 | recnd 11290 | . . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) ∈
ℂ) | 
| 322 | 157, 320,
321 | fsumsub 15825 | . . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) − ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) = (Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) − Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))))) | 
| 323 | 310, 319,
322 | 3eqtr2rd 2783 | . . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) − Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) = (2 · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) | 
| 324 | 323 | oveq1d 7447 | . . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) − Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) / (log‘𝑥)) = ((2 · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))) / (log‘𝑥))) | 
| 325 | 298 | recnd 11290 | . . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) ∈
ℂ) | 
| 326 | 325, 287,
278, 289 | divsubdird 12083 | . . . . . . . . 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 11292 | . . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))) ∈
ℝ) | 
| 328 | 157, 327 | fsumrecl 15771 | . . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))) ∈
ℝ) | 
| 329 | 328 | recnd 11290 | . . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))) ∈
ℂ) | 
| 330 | 307, 329,
278, 289 | div23d 12081 | . . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))) / (log‘𝑥)) = ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) | 
| 331 | 324, 326,
330 | 3eqtr3d 2784 | . . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥)) − (Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥))) = ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) | 
| 332 | 331 | oveq2d 7448 | . . . . . . 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 2778 | . . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) − (2 · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / (log‘𝑥))) = (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1))))))) | 
| 334 | 333 | oveq1d 7447 | . . . . 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 2782 | . . . 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 5241 | . . 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 13109 | . . . 4
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥) ∈ ℝ) | 
| 338 | 157, 158 | fsumrecl 15771 | . . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) ∈ ℝ) | 
| 339 | 92, 338 | readdcld 11291 | . . . . 5
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) ∈ ℝ) | 
| 340 | 10, 288 | rpmulcld 13094 | . . . . 5
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ∈
ℝ+) | 
| 341 | 339, 340 | rerpdivcld 13109 | . . . 4
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))) ∈ ℝ) | 
| 342 | 47, 18 | pntrlog2bndlem1 27622 | . . . . 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 13080 | . . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ∈ ℂ) | 
| 345 | 340 | rpne0d 13083 | . . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ≠ 0) | 
| 346 | 93, 274, 344, 345 | divdird 12082 | . . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))) = ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) / (𝑥 · (log‘𝑥))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥))))) | 
| 347 | 91 | recnd 11290 | . . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) ∈ ℂ) | 
| 348 | 43, 347, 344, 345 | divassd 12079 | . . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) / (𝑥 · (log‘𝑥))) = ((𝑥 / ((⌊‘𝑥) + 1)) · (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥))))) | 
| 349 | 348 | oveq1d 7447 | . . . . . . 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 2776 | . . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))) = (((𝑥 / ((⌊‘𝑥) + 1)) · (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥))))) | 
| 351 | 350 | mpteq2dva 5241 | . . . . 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 13109 | . . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥))) ∈ ℝ) | 
| 353 | 21, 352 | remulcld 11292 | . . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((𝑥 / ((⌊‘𝑥) + 1)) · (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) ∈ ℝ) | 
| 354 | 338, 340 | rerpdivcld 13109 | . . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥))) ∈ ℝ) | 
| 355 |  | ioossre 13449 | . . . . . . . . 9
⊢
(1(,)+∞) ⊆ ℝ | 
| 356 | 355 | a1i 11 | . . . . . . . 8
⊢ (⊤
→ (1(,)+∞) ⊆ ℝ) | 
| 357 |  | 1red 11263 | . . . . . . . 8
⊢ (⊤
→ 1 ∈ ℝ) | 
| 358 | 21, 5, 30 | ltled 11410 | . . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑥 / ((⌊‘𝑥) + 1)) ≤ 1) | 
| 359 | 358 | adantrr 717 | . . . . . . . 8
⊢
((⊤ ∧ (𝑥
∈ (1(,)+∞) ∧ 1 ≤ 𝑥)) → (𝑥 / ((⌊‘𝑥) + 1)) ≤ 1) | 
| 360 | 356, 21, 357, 357, 359 | ello1d 15560 | . . . . . . 7
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (𝑥 /
((⌊‘𝑥) + 1)))
∈ ≤𝑂(1)) | 
| 361 | 80 | recnd 11290 | . . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑆‘𝑥) ∈ ℂ) | 
| 362 | 90 | recnd 11290 | . . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (2 · (𝑇‘(⌊‘𝑥))) ∈ ℂ) | 
| 363 | 361, 362,
344, 345 | divsubdird 12083 | . . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥))) = (((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) − ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥))))) | 
| 364 | 363 | mpteq2dva 5241 | . . . . . . . . 9
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) = (𝑥 ∈ (1(,)+∞) ↦ (((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) − ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥)))))) | 
| 365 | 80, 340 | rerpdivcld 13109 | . . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) ∈ ℝ) | 
| 366 | 90, 340 | rerpdivcld 13109 | . . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥))) ∈ ℝ) | 
| 367 |  | 2cnd 12345 | . . . . . . . . . . . 12
⊢ (⊤
→ 2 ∈ ℂ) | 
| 368 |  | o1const 15657 | . . . . . . . . . . . 12
⊢
(((1(,)+∞) ⊆ ℝ ∧ 2 ∈ ℂ) → (𝑥 ∈ (1(,)+∞) ↦
2) ∈ 𝑂(1)) | 
| 369 | 355, 367,
368 | sylancr 587 | . . . . . . . . . . 11
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ 2) ∈ 𝑂(1)) | 
| 370 | 365 | recnd 11290 | . . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) ∈ ℂ) | 
| 371 | 80, 10 | rerpdivcld 13109 | . . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((𝑆‘𝑥) / 𝑥) ∈ ℝ) | 
| 372 | 371 | recnd 11290 | . . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((𝑆‘𝑥) / 𝑥) ∈ ℂ) | 
| 373 | 307, 278 | mulcld 11282 | . . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (2 · (log‘𝑥)) ∈ ℂ) | 
| 374 | 372, 373,
278, 289 | divsubdird 12083 | . . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥))) / (log‘𝑥)) = ((((𝑆‘𝑥) / 𝑥) / (log‘𝑥)) − ((2 · (log‘𝑥)) / (log‘𝑥)))) | 
| 375 | 23, 277 | remulcld 11292 | . . . . . . . . . . . . . . . . . 18
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (2 · (log‘𝑥)) ∈ ℝ) | 
| 376 | 371, 375 | resubcld 11692 | . . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥))) ∈
ℝ) | 
| 377 | 376 | recnd 11290 | . . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥))) ∈
ℂ) | 
| 378 | 377, 278,
289 | divrecd 12047 | . . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥))) / (log‘𝑥)) = ((((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥))) · (1 /
(log‘𝑥)))) | 
| 379 | 361, 66, 278, 290, 289 | divdiv1d 12075 | . . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((𝑆‘𝑥) / 𝑥) / (log‘𝑥)) = ((𝑆‘𝑥) / (𝑥 · (log‘𝑥)))) | 
| 380 | 307, 278,
289 | divcan4d 12050 | . . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((2 · (log‘𝑥)) / (log‘𝑥)) = 2) | 
| 381 | 379, 380 | oveq12d 7450 | . . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((𝑆‘𝑥) / 𝑥) / (log‘𝑥)) − ((2 · (log‘𝑥)) / (log‘𝑥))) = (((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) − 2)) | 
| 382 | 374, 378,
381 | 3eqtr3rd 2785 | . . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) − 2) = ((((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥))) · (1 /
(log‘𝑥)))) | 
| 383 | 382 | mpteq2dva 5241 | . . . . . . . . . . . . 13
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) − 2)) = (𝑥 ∈ (1(,)+∞) ↦ ((((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥))) · (1 /
(log‘𝑥))))) | 
| 384 | 5, 288 | rerpdivcld 13109 | . . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (1 / (log‘𝑥)) ∈ ℝ) | 
| 385 | 10 | ex 412 | . . . . . . . . . . . . . . . 16
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) → 𝑥
∈ ℝ+)) | 
| 386 | 385 | ssrdv 3988 | . . . . . . . . . . . . . . 15
⊢ (⊤
→ (1(,)+∞) ⊆ ℝ+) | 
| 387 | 47 | selbergs 27619 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℝ+
↦ (((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥)))) ∈
𝑂(1) | 
| 388 | 387 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥)))) ∈
𝑂(1)) | 
| 389 | 386, 388 | o1res2 15600 | . . . . . . . . . . . . . 14
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥)))) ∈
𝑂(1)) | 
| 390 |  | divlogrlim 26678 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (1(,)+∞) ↦
(1 / (log‘𝑥)))
⇝𝑟 0 | 
| 391 |  | rlimo1 15654 | . . . . . . . . . . . . . . 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 15662 | . . . . . . . . . . . . 13
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ ((((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥))) · (1 /
(log‘𝑥)))) ∈
𝑂(1)) | 
| 394 | 383, 393 | eqeltrd 2840 | . . . . . . . . . . . 12
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) − 2)) ∈
𝑂(1)) | 
| 395 | 370, 307,
394 | o1dif 15667 | . . . . . . . . . . 11
⊢ (⊤
→ ((𝑥 ∈
(1(,)+∞) ↦ ((𝑆‘𝑥) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1) ↔ (𝑥 ∈ (1(,)+∞) ↦
2) ∈ 𝑂(1))) | 
| 396 | 369, 395 | mpbird 257 | . . . . . . . . . 10
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ ((𝑆‘𝑥) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1)) | 
| 397 | 22 | a1i 11 | . . . . . . . . . . . 12
⊢ (⊤
→ 2 ∈ ℝ) | 
| 398 | 2, 277 | remulcld 11292 | . . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ∈ ℝ) | 
| 399 |  | 2rp 13040 | . . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℝ+ | 
| 400 | 399 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 2 ∈ ℝ+) | 
| 401 | 400 | rpge0d 13082 | . . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 0 ≤ 2) | 
| 402 |  | flge1nn 13862 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℝ ∧ 1 ≤
𝑥) →
(⌊‘𝑥) ∈
ℕ) | 
| 403 | 2, 9, 402 | syl2anc 584 | . . . . . . . . . . . . . . . . . 18
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (⌊‘𝑥) ∈ ℕ) | 
| 404 | 403 | nnrpd 13076 | . . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (⌊‘𝑥) ∈
ℝ+) | 
| 405 |  | rpre 13044 | . . . . . . . . . . . . . . . . . . 19
⊢
((⌊‘𝑥)
∈ ℝ+ → (⌊‘𝑥) ∈ ℝ) | 
| 406 |  | eleq1 2828 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 = (⌊‘𝑥) → (𝑎 ∈ ℝ+ ↔
(⌊‘𝑥) ∈
ℝ+)) | 
| 407 |  | id 22 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 = (⌊‘𝑥) → 𝑎 = (⌊‘𝑥)) | 
| 408 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 = (⌊‘𝑥) → (log‘𝑎) =
(log‘(⌊‘𝑥))) | 
| 409 | 407, 408 | oveq12d 7450 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 = (⌊‘𝑥) → (𝑎 · (log‘𝑎)) = ((⌊‘𝑥) · (log‘(⌊‘𝑥)))) | 
| 410 | 406, 409 | ifbieq1d 4549 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 = (⌊‘𝑥) → if(𝑎 ∈ ℝ+, (𝑎 · (log‘𝑎)), 0) = if((⌊‘𝑥) ∈ ℝ+,
((⌊‘𝑥) ·
(log‘(⌊‘𝑥))), 0)) | 
| 411 |  | ovex 7465 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((⌊‘𝑥)
· (log‘(⌊‘𝑥))) ∈ V | 
| 412 | 411, 132 | ifex 4575 | . . . . . . . . . . . . . . . . . . . 20
⊢
if((⌊‘𝑥)
∈ ℝ+, ((⌊‘𝑥) · (log‘(⌊‘𝑥))), 0) ∈
V | 
| 413 | 410, 81, 412 | fvmpt 7015 | . . . . . . . . . . . . . . . . . . 19
⊢
((⌊‘𝑥)
∈ ℝ → (𝑇‘(⌊‘𝑥)) = if((⌊‘𝑥) ∈ ℝ+,
((⌊‘𝑥) ·
(log‘(⌊‘𝑥))), 0)) | 
| 414 | 405, 413 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢
((⌊‘𝑥)
∈ ℝ+ → (𝑇‘(⌊‘𝑥)) = if((⌊‘𝑥) ∈ ℝ+,
((⌊‘𝑥) ·
(log‘(⌊‘𝑥))), 0)) | 
| 415 |  | iftrue 4530 | . . . . . . . . . . . . . . . . . 18
⊢
((⌊‘𝑥)
∈ ℝ+ → if((⌊‘𝑥) ∈ ℝ+,
((⌊‘𝑥) ·
(log‘(⌊‘𝑥))), 0) = ((⌊‘𝑥) · (log‘(⌊‘𝑥)))) | 
| 416 | 414, 415 | eqtrd 2776 | . . . . . . . . . . . . . . . . 17
⊢
((⌊‘𝑥)
∈ ℝ+ → (𝑇‘(⌊‘𝑥)) = ((⌊‘𝑥) · (log‘(⌊‘𝑥)))) | 
| 417 | 404, 416 | syl 17 | . . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑇‘(⌊‘𝑥)) = ((⌊‘𝑥) · (log‘(⌊‘𝑥)))) | 
| 418 | 404 | relogcld 26666 | . . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (log‘(⌊‘𝑥)) ∈ ℝ) | 
| 419 | 13 | nn0ge0d 12592 | . . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 0 ≤ (⌊‘𝑥)) | 
| 420 | 403 | nnge1d 12315 | . . . . . . . . . . . . . . . . . 18
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 1 ≤ (⌊‘𝑥)) | 
| 421 | 46, 420 | logge0d 26673 | . . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 0 ≤ (log‘(⌊‘𝑥))) | 
| 422 |  | flle 13840 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℝ →
(⌊‘𝑥) ≤
𝑥) | 
| 423 | 2, 422 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (⌊‘𝑥) ≤ 𝑥) | 
| 424 | 404, 10 | logled 26670 | . . . . . . . . . . . . . . . . . 18
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((⌊‘𝑥) ≤ 𝑥 ↔ (log‘(⌊‘𝑥)) ≤ (log‘𝑥))) | 
| 425 | 423, 424 | mpbid 232 | . . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (log‘(⌊‘𝑥)) ≤ (log‘𝑥)) | 
| 426 | 46, 2, 418, 277, 419, 421, 423, 425 | lemul12ad 12211 | . . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((⌊‘𝑥) · (log‘(⌊‘𝑥))) ≤ (𝑥 · (log‘𝑥))) | 
| 427 | 417, 426 | eqbrtrd 5164 | . . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑇‘(⌊‘𝑥)) ≤ (𝑥 · (log‘𝑥))) | 
| 428 | 89, 398, 23, 401, 427 | lemul2ad 12209 | . . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (2 · (𝑇‘(⌊‘𝑥))) ≤ (2 · (𝑥 · (log‘𝑥)))) | 
| 429 | 90, 23, 340 | ledivmul2d 13132 | . . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥))) ≤ 2 ↔ (2 · (𝑇‘(⌊‘𝑥))) ≤ (2 · (𝑥 · (log‘𝑥))))) | 
| 430 | 428, 429 | mpbird 257 | . . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥))) ≤ 2) | 
| 431 | 430 | adantrr 717 | . . . . . . . . . . . 12
⊢
((⊤ ∧ (𝑥
∈ (1(,)+∞) ∧ 1 ≤ 𝑥)) → ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥))) ≤ 2) | 
| 432 | 356, 366,
357, 397, 431 | ello1d 15560 | . . . . . . . . . . 11
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥)))) ∈
≤𝑂(1)) | 
| 433 |  | 0red 11265 | . . . . . . . . . . . 12
⊢ (⊤
→ 0 ∈ ℝ) | 
| 434 | 46, 418, 419, 421 | mulge0d 11841 | . . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 0 ≤ ((⌊‘𝑥) · (log‘(⌊‘𝑥)))) | 
| 435 | 434, 417 | breqtrrd 5170 | . . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 0 ≤ (𝑇‘(⌊‘𝑥))) | 
| 436 | 23, 89, 401, 435 | mulge0d 11841 | . . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 0 ≤ (2 · (𝑇‘(⌊‘𝑥)))) | 
| 437 | 90, 340, 436 | divge0d 13118 | . . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 0 ≤ ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥)))) | 
| 438 | 366, 433,
437 | o1lo12 15575 | . . . . . . . . . . 11
⊢ (⊤
→ ((𝑥 ∈
(1(,)+∞) ↦ ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1) ↔ (𝑥 ∈ (1(,)+∞) ↦
((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥)))) ∈
≤𝑂(1))) | 
| 439 | 432, 438 | mpbird 257 | . . . . . . . . . 10
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1)) | 
| 440 | 365, 366,
396, 439 | o1sub2 15663 | . . . . . . . . 9
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (((𝑆‘𝑥) / (𝑥 · (log‘𝑥))) − ((2 · (𝑇‘(⌊‘𝑥))) / (𝑥 · (log‘𝑥))))) ∈ 𝑂(1)) | 
| 441 | 364, 440 | eqeltrd 2840 | . . . . . . . 8
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1)) | 
| 442 | 352, 441 | o1lo1d 15576 | . . . . . . 7
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) ∈
≤𝑂(1)) | 
| 443 | 21, 352, 360, 442, 41 | lo1mul 15665 | . . . . . 6
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ ((𝑥
/ ((⌊‘𝑥) + 1))
· (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥))))) ∈
≤𝑂(1)) | 
| 444 | 47 | selbergsb 27620 | . . . . . . . 8
⊢
∃𝑐 ∈
ℝ+ ∀𝑦 ∈ (1[,)+∞)(abs‘(((𝑆‘𝑦) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝑐 | 
| 445 |  | simpl 482 | . . . . . . . . . 10
⊢ ((𝑐 ∈ ℝ+
∧ ∀𝑦 ∈
(1[,)+∞)(abs‘(((𝑆‘𝑦) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝑐) → 𝑐 ∈ ℝ+) | 
| 446 |  | simpr 484 | . . . . . . . . . 10
⊢ ((𝑐 ∈ ℝ+
∧ ∀𝑦 ∈
(1[,)+∞)(abs‘(((𝑆‘𝑦) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝑐) → ∀𝑦 ∈ (1[,)+∞)(abs‘(((𝑆‘𝑦) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝑐) | 
| 447 | 47, 18, 445, 446 | pntrlog2bndlem3 27624 | . . . . . . . . 9
⊢ ((𝑐 ∈ ℝ+
∧ ∀𝑦 ∈
(1[,)+∞)(abs‘(((𝑆‘𝑦) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝑐) → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1)) | 
| 448 | 447 | rexlimiva 3146 | . . . . . . . 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 15576 | . . . . . 6
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥)))) ∈
≤𝑂(1)) | 
| 451 | 353, 354,
443, 450 | lo1add 15664 | . . . . 5
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (((𝑥
/ ((⌊‘𝑥) + 1))
· (((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥)))) / (𝑥 · (log‘𝑥)))) + (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥))))) ∈
≤𝑂(1)) | 
| 452 | 351, 451 | eqeltrd 2840 | . . . 4
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥)))) ∈
≤𝑂(1)) | 
| 453 | 337, 341,
343, 452 | lo1add 15664 | . . 3
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥) + ((((𝑥 / ((⌊‘𝑥) + 1)) · ((𝑆‘𝑥) − (2 · (𝑇‘(⌊‘𝑥))))) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛)))))) / (𝑥 · (log‘𝑥))))) ∈
≤𝑂(1)) | 
| 454 | 336, 453 | eqeltrrd 2841 | . 2
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / 𝑥)) ∈ ≤𝑂(1)) | 
| 455 | 454 | mptru 1546 | 1
⊢ (𝑥 ∈ (1(,)+∞) ↦
((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / 𝑥)) ∈ ≤𝑂(1) |