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

Theorem pntrsumo1 27609
Description: A bound on a sum over 𝑅. Equation 10.1.16 of [Shapiro], p. 403. (Contributed by Mario Carneiro, 25-May-2016.)
Hypothesis
Ref Expression
pntrval.r 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))
Assertion
Ref Expression
pntrsumo1 (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) ∈ 𝑂(1)
Distinct variable groups:   𝑛,𝑎,𝑥   𝑅,𝑛,𝑥
Allowed substitution hint:   𝑅(𝑎)

Proof of Theorem pntrsumo1
Dummy variable 𝑚 is distinct from all other variables.
StepHypRef Expression
1 1re 11261 . . . . . . . . . . 11 1 ∈ ℝ
2 elicopnf 13485 . . . . . . . . . . 11 (1 ∈ ℝ → (𝑥 ∈ (1[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 1 ≤ 𝑥)))
31, 2ax-mp 5 . . . . . . . . . 10 (𝑥 ∈ (1[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 1 ≤ 𝑥))
43simplbi 497 . . . . . . . . 9 (𝑥 ∈ (1[,)+∞) → 𝑥 ∈ ℝ)
5 0red 11264 . . . . . . . . . 10 (𝑥 ∈ (1[,)+∞) → 0 ∈ ℝ)
6 1red 11262 . . . . . . . . . 10 (𝑥 ∈ (1[,)+∞) → 1 ∈ ℝ)
7 0lt1 11785 . . . . . . . . . . 11 0 < 1
87a1i 11 . . . . . . . . . 10 (𝑥 ∈ (1[,)+∞) → 0 < 1)
93simprbi 496 . . . . . . . . . 10 (𝑥 ∈ (1[,)+∞) → 1 ≤ 𝑥)
105, 6, 4, 8, 9ltletrd 11421 . . . . . . . . 9 (𝑥 ∈ (1[,)+∞) → 0 < 𝑥)
114, 10elrpd 13074 . . . . . . . 8 (𝑥 ∈ (1[,)+∞) → 𝑥 ∈ ℝ+)
1211ssriv 3987 . . . . . . 7 (1[,)+∞) ⊆ ℝ+
1312a1i 11 . . . . . 6 (⊤ → (1[,)+∞) ⊆ ℝ+)
14 rpssre 13042 . . . . . 6 + ⊆ ℝ
1513, 14sstrdi 3996 . . . . 5 (⊤ → (1[,)+∞) ⊆ ℝ)
1615resmptd 6058 . . . 4 (⊤ → ((𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) ↾ (1[,)+∞)) = (𝑥 ∈ (1[,)+∞) ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))))
17 chpcl 27167 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → (ψ‘𝑥) ∈ ℝ)
184, 17syl 17 . . . . . . . . . . 11 (𝑥 ∈ (1[,)+∞) → (ψ‘𝑥) ∈ ℝ)
19 peano2re 11434 . . . . . . . . . . 11 ((ψ‘𝑥) ∈ ℝ → ((ψ‘𝑥) + 1) ∈ ℝ)
2018, 19syl 17 . . . . . . . . . 10 (𝑥 ∈ (1[,)+∞) → ((ψ‘𝑥) + 1) ∈ ℝ)
2111rprege0d 13084 . . . . . . . . . . . 12 (𝑥 ∈ (1[,)+∞) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
22 flge0nn0 13860 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → (⌊‘𝑥) ∈ ℕ0)
2321, 22syl 17 . . . . . . . . . . 11 (𝑥 ∈ (1[,)+∞) → (⌊‘𝑥) ∈ ℕ0)
24 nn0p1nn 12565 . . . . . . . . . . 11 ((⌊‘𝑥) ∈ ℕ0 → ((⌊‘𝑥) + 1) ∈ ℕ)
2523, 24syl 17 . . . . . . . . . 10 (𝑥 ∈ (1[,)+∞) → ((⌊‘𝑥) + 1) ∈ ℕ)
2620, 25nndivred 12320 . . . . . . . . 9 (𝑥 ∈ (1[,)+∞) → (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ∈ ℝ)
2726recnd 11289 . . . . . . . 8 (𝑥 ∈ (1[,)+∞) → (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ∈ ℂ)
28 ax-1cn 11213 . . . . . . . 8 1 ∈ ℂ
29 subcl 11507 . . . . . . . 8 (((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ∈ ℂ ∧ 1 ∈ ℂ) → ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) ∈ ℂ)
3027, 28, 29sylancl 586 . . . . . . 7 (𝑥 ∈ (1[,)+∞) → ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) ∈ ℂ)
31 fzfid 14014 . . . . . . . . . 10 (𝑥 ∈ ℝ → (1...(⌊‘𝑥)) ∈ Fin)
32 elfznn 13593 . . . . . . . . . . . 12 (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
3332adantl 481 . . . . . . . . . . 11 ((𝑥 ∈ ℝ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
34 nnrp 13046 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → 𝑛 ∈ ℝ+)
35 pntrval.r . . . . . . . . . . . . . . 15 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))
3635pntrf 27607 . . . . . . . . . . . . . 14 𝑅:ℝ+⟶ℝ
3736ffvelcdmi 7103 . . . . . . . . . . . . 13 (𝑛 ∈ ℝ+ → (𝑅𝑛) ∈ ℝ)
3834, 37syl 17 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → (𝑅𝑛) ∈ ℝ)
39 peano2nn 12278 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℕ)
40 nnmulcl 12290 . . . . . . . . . . . . 13 ((𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ ℕ) → (𝑛 · (𝑛 + 1)) ∈ ℕ)
4139, 40mpdan 687 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → (𝑛 · (𝑛 + 1)) ∈ ℕ)
4238, 41nndivred 12320 . . . . . . . . . . 11 (𝑛 ∈ ℕ → ((𝑅𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ)
4333, 42syl 17 . . . . . . . . . 10 ((𝑥 ∈ ℝ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑅𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ)
4431, 43fsumrecl 15770 . . . . . . . . 9 (𝑥 ∈ ℝ → Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ)
4544recnd 11289 . . . . . . . 8 (𝑥 ∈ ℝ → Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ)
464, 45syl 17 . . . . . . 7 (𝑥 ∈ (1[,)+∞) → Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ)
47 oveq2 7439 . . . . . . . . . . 11 (𝑚 = 𝑛 → (1 / 𝑚) = (1 / 𝑛))
48 fvoveq1 7454 . . . . . . . . . . . 12 (𝑚 = 𝑛 → (ψ‘(𝑚 − 1)) = (ψ‘(𝑛 − 1)))
49 oveq1 7438 . . . . . . . . . . . 12 (𝑚 = 𝑛 → (𝑚 − 1) = (𝑛 − 1))
5048, 49oveq12d 7449 . . . . . . . . . . 11 (𝑚 = 𝑛 → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = ((ψ‘(𝑛 − 1)) − (𝑛 − 1)))
5147, 50jca 511 . . . . . . . . . 10 (𝑚 = 𝑛 → ((1 / 𝑚) = (1 / 𝑛) ∧ ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = ((ψ‘(𝑛 − 1)) − (𝑛 − 1))))
52 oveq2 7439 . . . . . . . . . . 11 (𝑚 = (𝑛 + 1) → (1 / 𝑚) = (1 / (𝑛 + 1)))
53 fvoveq1 7454 . . . . . . . . . . . 12 (𝑚 = (𝑛 + 1) → (ψ‘(𝑚 − 1)) = (ψ‘((𝑛 + 1) − 1)))
54 oveq1 7438 . . . . . . . . . . . 12 (𝑚 = (𝑛 + 1) → (𝑚 − 1) = ((𝑛 + 1) − 1))
5553, 54oveq12d 7449 . . . . . . . . . . 11 (𝑚 = (𝑛 + 1) → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = ((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1)))
5652, 55jca 511 . . . . . . . . . 10 (𝑚 = (𝑛 + 1) → ((1 / 𝑚) = (1 / (𝑛 + 1)) ∧ ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = ((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1))))
57 oveq2 7439 . . . . . . . . . . . 12 (𝑚 = 1 → (1 / 𝑚) = (1 / 1))
58 1div1e1 11958 . . . . . . . . . . . 12 (1 / 1) = 1
5957, 58eqtrdi 2793 . . . . . . . . . . 11 (𝑚 = 1 → (1 / 𝑚) = 1)
60 oveq1 7438 . . . . . . . . . . . . . . . 16 (𝑚 = 1 → (𝑚 − 1) = (1 − 1))
61 1m1e0 12338 . . . . . . . . . . . . . . . 16 (1 − 1) = 0
6260, 61eqtrdi 2793 . . . . . . . . . . . . . . 15 (𝑚 = 1 → (𝑚 − 1) = 0)
6362fveq2d 6910 . . . . . . . . . . . . . 14 (𝑚 = 1 → (ψ‘(𝑚 − 1)) = (ψ‘0))
64 2pos 12369 . . . . . . . . . . . . . . 15 0 < 2
65 0re 11263 . . . . . . . . . . . . . . . 16 0 ∈ ℝ
66 chpeq0 27252 . . . . . . . . . . . . . . . 16 (0 ∈ ℝ → ((ψ‘0) = 0 ↔ 0 < 2))
6765, 66ax-mp 5 . . . . . . . . . . . . . . 15 ((ψ‘0) = 0 ↔ 0 < 2)
6864, 67mpbir 231 . . . . . . . . . . . . . 14 (ψ‘0) = 0
6963, 68eqtrdi 2793 . . . . . . . . . . . . 13 (𝑚 = 1 → (ψ‘(𝑚 − 1)) = 0)
7069, 62oveq12d 7449 . . . . . . . . . . . 12 (𝑚 = 1 → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = (0 − 0))
71 0m0e0 12386 . . . . . . . . . . . 12 (0 − 0) = 0
7270, 71eqtrdi 2793 . . . . . . . . . . 11 (𝑚 = 1 → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = 0)
7359, 72jca 511 . . . . . . . . . 10 (𝑚 = 1 → ((1 / 𝑚) = 1 ∧ ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = 0))
74 oveq2 7439 . . . . . . . . . . 11 (𝑚 = ((⌊‘𝑥) + 1) → (1 / 𝑚) = (1 / ((⌊‘𝑥) + 1)))
75 fvoveq1 7454 . . . . . . . . . . . 12 (𝑚 = ((⌊‘𝑥) + 1) → (ψ‘(𝑚 − 1)) = (ψ‘(((⌊‘𝑥) + 1) − 1)))
76 oveq1 7438 . . . . . . . . . . . 12 (𝑚 = ((⌊‘𝑥) + 1) → (𝑚 − 1) = (((⌊‘𝑥) + 1) − 1))
7775, 76oveq12d 7449 . . . . . . . . . . 11 (𝑚 = ((⌊‘𝑥) + 1) → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = ((ψ‘(((⌊‘𝑥) + 1) − 1)) − (((⌊‘𝑥) + 1) − 1)))
7874, 77jca 511 . . . . . . . . . 10 (𝑚 = ((⌊‘𝑥) + 1) → ((1 / 𝑚) = (1 / ((⌊‘𝑥) + 1)) ∧ ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = ((ψ‘(((⌊‘𝑥) + 1) − 1)) − (((⌊‘𝑥) + 1) − 1))))
79 nnuz 12921 . . . . . . . . . . 11 ℕ = (ℤ‘1)
8025, 79eleqtrdi 2851 . . . . . . . . . 10 (𝑥 ∈ (1[,)+∞) → ((⌊‘𝑥) + 1) ∈ (ℤ‘1))
81 elfznn 13593 . . . . . . . . . . . . 13 (𝑚 ∈ (1...((⌊‘𝑥) + 1)) → 𝑚 ∈ ℕ)
8281adantl 481 . . . . . . . . . . . 12 ((𝑥 ∈ (1[,)+∞) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 𝑚 ∈ ℕ)
8382nnrecred 12317 . . . . . . . . . . 11 ((𝑥 ∈ (1[,)+∞) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (1 / 𝑚) ∈ ℝ)
8483recnd 11289 . . . . . . . . . 10 ((𝑥 ∈ (1[,)+∞) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (1 / 𝑚) ∈ ℂ)
8582nnred 12281 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 𝑚 ∈ ℝ)
86 peano2rem 11576 . . . . . . . . . . . . . 14 (𝑚 ∈ ℝ → (𝑚 − 1) ∈ ℝ)
8785, 86syl 17 . . . . . . . . . . . . 13 ((𝑥 ∈ (1[,)+∞) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑚 − 1) ∈ ℝ)
88 chpcl 27167 . . . . . . . . . . . . 13 ((𝑚 − 1) ∈ ℝ → (ψ‘(𝑚 − 1)) ∈ ℝ)
8987, 88syl 17 . . . . . . . . . . . 12 ((𝑥 ∈ (1[,)+∞) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (ψ‘(𝑚 − 1)) ∈ ℝ)
9089, 87resubcld 11691 . . . . . . . . . . 11 ((𝑥 ∈ (1[,)+∞) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) ∈ ℝ)
9190recnd 11289 . . . . . . . . . 10 ((𝑥 ∈ (1[,)+∞) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) ∈ ℂ)
9251, 56, 73, 78, 80, 84, 91fsumparts 15842 . . . . . . . . 9 (𝑥 ∈ (1[,)+∞) → Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))((1 / 𝑛) · (((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1)) − ((ψ‘(𝑛 − 1)) − (𝑛 − 1)))) = ((((1 / ((⌊‘𝑥) + 1)) · ((ψ‘(((⌊‘𝑥) + 1) − 1)) − (((⌊‘𝑥) + 1) − 1))) − (1 · 0)) − Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))(((1 / (𝑛 + 1)) − (1 / 𝑛)) · ((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1)))))
934flcld 13838 . . . . . . . . . . . 12 (𝑥 ∈ (1[,)+∞) → (⌊‘𝑥) ∈ ℤ)
94 fzval3 13773 . . . . . . . . . . . 12 ((⌊‘𝑥) ∈ ℤ → (1...(⌊‘𝑥)) = (1..^((⌊‘𝑥) + 1)))
9593, 94syl 17 . . . . . . . . . . 11 (𝑥 ∈ (1[,)+∞) → (1...(⌊‘𝑥)) = (1..^((⌊‘𝑥) + 1)))
9695eqcomd 2743 . . . . . . . . . 10 (𝑥 ∈ (1[,)+∞) → (1..^((⌊‘𝑥) + 1)) = (1...(⌊‘𝑥)))
9732adantl 481 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
9897nncnd 12282 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℂ)
99 pncan 11514 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛 + 1) − 1) = 𝑛)
10098, 28, 99sylancl 586 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) − 1) = 𝑛)
10197nnred 12281 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ)
102100, 101eqeltrd 2841 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) − 1) ∈ ℝ)
103 chpcl 27167 . . . . . . . . . . . . . . . 16 (((𝑛 + 1) − 1) ∈ ℝ → (ψ‘((𝑛 + 1) − 1)) ∈ ℝ)
104102, 103syl 17 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (ψ‘((𝑛 + 1) − 1)) ∈ ℝ)
105104recnd 11289 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (ψ‘((𝑛 + 1) − 1)) ∈ ℂ)
106102recnd 11289 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) − 1) ∈ ℂ)
107 peano2rem 11576 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℝ → (𝑛 − 1) ∈ ℝ)
108101, 107syl 17 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 − 1) ∈ ℝ)
109 chpcl 27167 . . . . . . . . . . . . . . . 16 ((𝑛 − 1) ∈ ℝ → (ψ‘(𝑛 − 1)) ∈ ℝ)
110108, 109syl 17 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (ψ‘(𝑛 − 1)) ∈ ℝ)
111110recnd 11289 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (ψ‘(𝑛 − 1)) ∈ ℂ)
112 1cnd 11256 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℂ)
11398, 112subcld 11620 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 − 1) ∈ ℂ)
114105, 106, 111, 113sub4d 11669 . . . . . . . . . . . . 13 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1)) − ((ψ‘(𝑛 − 1)) − (𝑛 − 1))) = (((ψ‘((𝑛 + 1) − 1)) − (ψ‘(𝑛 − 1))) − (((𝑛 + 1) − 1) − (𝑛 − 1))))
115 vmacl 27161 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ → (Λ‘𝑛) ∈ ℝ)
11697, 115syl 17 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈ ℝ)
117116recnd 11289 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈ ℂ)
118 nnm1nn0 12567 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → (𝑛 − 1) ∈ ℕ0)
11997, 118syl 17 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 − 1) ∈ ℕ0)
120 chpp1 27198 . . . . . . . . . . . . . . . . 17 ((𝑛 − 1) ∈ ℕ0 → (ψ‘((𝑛 − 1) + 1)) = ((ψ‘(𝑛 − 1)) + (Λ‘((𝑛 − 1) + 1))))
121119, 120syl 17 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (ψ‘((𝑛 − 1) + 1)) = ((ψ‘(𝑛 − 1)) + (Λ‘((𝑛 − 1) + 1))))
122 npcan 11517 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛 − 1) + 1) = 𝑛)
12398, 28, 122sylancl 586 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 − 1) + 1) = 𝑛)
124123, 100eqtr4d 2780 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 − 1) + 1) = ((𝑛 + 1) − 1))
125124fveq2d 6910 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (ψ‘((𝑛 − 1) + 1)) = (ψ‘((𝑛 + 1) − 1)))
126123fveq2d 6910 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘((𝑛 − 1) + 1)) = (Λ‘𝑛))
127126oveq2d 7447 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((ψ‘(𝑛 − 1)) + (Λ‘((𝑛 − 1) + 1))) = ((ψ‘(𝑛 − 1)) + (Λ‘𝑛)))
128121, 125, 1273eqtr3d 2785 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (ψ‘((𝑛 + 1) − 1)) = ((ψ‘(𝑛 − 1)) + (Λ‘𝑛)))
129111, 117, 128mvrladdd 11676 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((ψ‘((𝑛 + 1) − 1)) − (ψ‘(𝑛 − 1))) = (Λ‘𝑛))
130 peano2cn 11433 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℂ → (𝑛 + 1) ∈ ℂ)
13198, 130syl 17 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 + 1) ∈ ℂ)
132131, 98, 112nnncan2d 11655 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑛 + 1) − 1) − (𝑛 − 1)) = ((𝑛 + 1) − 𝑛))
133 pncan2 11515 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛 + 1) − 𝑛) = 1)
13498, 28, 133sylancl 586 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) − 𝑛) = 1)
135132, 134eqtrd 2777 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑛 + 1) − 1) − (𝑛 − 1)) = 1)
136129, 135oveq12d 7449 . . . . . . . . . . . . 13 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((ψ‘((𝑛 + 1) − 1)) − (ψ‘(𝑛 − 1))) − (((𝑛 + 1) − 1) − (𝑛 − 1))) = ((Λ‘𝑛) − 1))
137114, 136eqtrd 2777 . . . . . . . . . . . 12 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1)) − ((ψ‘(𝑛 − 1)) − (𝑛 − 1))) = ((Λ‘𝑛) − 1))
138137oveq2d 7447 . . . . . . . . . . 11 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 / 𝑛) · (((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1)) − ((ψ‘(𝑛 − 1)) − (𝑛 − 1)))) = ((1 / 𝑛) · ((Λ‘𝑛) − 1)))
139 peano2rem 11576 . . . . . . . . . . . . . 14 ((Λ‘𝑛) ∈ ℝ → ((Λ‘𝑛) − 1) ∈ ℝ)
140116, 139syl 17 . . . . . . . . . . . . 13 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) − 1) ∈ ℝ)
141140recnd 11289 . . . . . . . . . . . 12 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) − 1) ∈ ℂ)
14297nnne0d 12316 . . . . . . . . . . . 12 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ≠ 0)
143141, 98, 142divrec2d 12047 . . . . . . . . . . 11 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) − 1) / 𝑛) = ((1 / 𝑛) · ((Λ‘𝑛) − 1)))
144138, 143eqtr4d 2780 . . . . . . . . . 10 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 / 𝑛) · (((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1)) − ((ψ‘(𝑛 − 1)) − (𝑛 − 1)))) = (((Λ‘𝑛) − 1) / 𝑛))
14596, 144sumeq12rdv 15743 . . . . . . . . 9 (𝑥 ∈ (1[,)+∞) → Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))((1 / 𝑛) · (((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1)) − ((ψ‘(𝑛 − 1)) − (𝑛 − 1)))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛))
14623nn0cnd 12589 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (1[,)+∞) → (⌊‘𝑥) ∈ ℂ)
147 pncan 11514 . . . . . . . . . . . . . . . . . . 19 (((⌊‘𝑥) ∈ ℂ ∧ 1 ∈ ℂ) → (((⌊‘𝑥) + 1) − 1) = (⌊‘𝑥))
148146, 28, 147sylancl 586 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (1[,)+∞) → (((⌊‘𝑥) + 1) − 1) = (⌊‘𝑥))
149148fveq2d 6910 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (1[,)+∞) → (ψ‘(((⌊‘𝑥) + 1) − 1)) = (ψ‘(⌊‘𝑥)))
150 chpfl 27193 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℝ → (ψ‘(⌊‘𝑥)) = (ψ‘𝑥))
1514, 150syl 17 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (1[,)+∞) → (ψ‘(⌊‘𝑥)) = (ψ‘𝑥))
152149, 151eqtrd 2777 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1[,)+∞) → (ψ‘(((⌊‘𝑥) + 1) − 1)) = (ψ‘𝑥))
153152oveq1d 7446 . . . . . . . . . . . . . . 15 (𝑥 ∈ (1[,)+∞) → ((ψ‘(((⌊‘𝑥) + 1) − 1)) − (((⌊‘𝑥) + 1) − 1)) = ((ψ‘𝑥) − (((⌊‘𝑥) + 1) − 1)))
15418recnd 11289 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1[,)+∞) → (ψ‘𝑥) ∈ ℂ)
15525nncnd 12282 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1[,)+∞) → ((⌊‘𝑥) + 1) ∈ ℂ)
156 1cnd 11256 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1[,)+∞) → 1 ∈ ℂ)
157154, 155, 156subsub3d 11650 . . . . . . . . . . . . . . 15 (𝑥 ∈ (1[,)+∞) → ((ψ‘𝑥) − (((⌊‘𝑥) + 1) − 1)) = (((ψ‘𝑥) + 1) − ((⌊‘𝑥) + 1)))
158153, 157eqtrd 2777 . . . . . . . . . . . . . 14 (𝑥 ∈ (1[,)+∞) → ((ψ‘(((⌊‘𝑥) + 1) − 1)) − (((⌊‘𝑥) + 1) − 1)) = (((ψ‘𝑥) + 1) − ((⌊‘𝑥) + 1)))
159158oveq2d 7447 . . . . . . . . . . . . 13 (𝑥 ∈ (1[,)+∞) → ((1 / ((⌊‘𝑥) + 1)) · ((ψ‘(((⌊‘𝑥) + 1) − 1)) − (((⌊‘𝑥) + 1) − 1))) = ((1 / ((⌊‘𝑥) + 1)) · (((ψ‘𝑥) + 1) − ((⌊‘𝑥) + 1))))
16025nnrecred 12317 . . . . . . . . . . . . . . 15 (𝑥 ∈ (1[,)+∞) → (1 / ((⌊‘𝑥) + 1)) ∈ ℝ)
161160recnd 11289 . . . . . . . . . . . . . 14 (𝑥 ∈ (1[,)+∞) → (1 / ((⌊‘𝑥) + 1)) ∈ ℂ)
162 peano2cn 11433 . . . . . . . . . . . . . . 15 ((ψ‘𝑥) ∈ ℂ → ((ψ‘𝑥) + 1) ∈ ℂ)
163154, 162syl 17 . . . . . . . . . . . . . 14 (𝑥 ∈ (1[,)+∞) → ((ψ‘𝑥) + 1) ∈ ℂ)
164161, 163, 155subdid 11719 . . . . . . . . . . . . 13 (𝑥 ∈ (1[,)+∞) → ((1 / ((⌊‘𝑥) + 1)) · (((ψ‘𝑥) + 1) − ((⌊‘𝑥) + 1))) = (((1 / ((⌊‘𝑥) + 1)) · ((ψ‘𝑥) + 1)) − ((1 / ((⌊‘𝑥) + 1)) · ((⌊‘𝑥) + 1))))
16525nnne0d 12316 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1[,)+∞) → ((⌊‘𝑥) + 1) ≠ 0)
166163, 155, 165divrec2d 12047 . . . . . . . . . . . . . . 15 (𝑥 ∈ (1[,)+∞) → (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) = ((1 / ((⌊‘𝑥) + 1)) · ((ψ‘𝑥) + 1)))
167166eqcomd 2743 . . . . . . . . . . . . . 14 (𝑥 ∈ (1[,)+∞) → ((1 / ((⌊‘𝑥) + 1)) · ((ψ‘𝑥) + 1)) = (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)))
168155, 165recid2d 12039 . . . . . . . . . . . . . 14 (𝑥 ∈ (1[,)+∞) → ((1 / ((⌊‘𝑥) + 1)) · ((⌊‘𝑥) + 1)) = 1)
169167, 168oveq12d 7449 . . . . . . . . . . . . 13 (𝑥 ∈ (1[,)+∞) → (((1 / ((⌊‘𝑥) + 1)) · ((ψ‘𝑥) + 1)) − ((1 / ((⌊‘𝑥) + 1)) · ((⌊‘𝑥) + 1))) = ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1))
170159, 164, 1693eqtrd 2781 . . . . . . . . . . . 12 (𝑥 ∈ (1[,)+∞) → ((1 / ((⌊‘𝑥) + 1)) · ((ψ‘(((⌊‘𝑥) + 1) − 1)) − (((⌊‘𝑥) + 1) − 1))) = ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1))
17128mul01i 11451 . . . . . . . . . . . . 13 (1 · 0) = 0
172171a1i 11 . . . . . . . . . . . 12 (𝑥 ∈ (1[,)+∞) → (1 · 0) = 0)
173170, 172oveq12d 7449 . . . . . . . . . . 11 (𝑥 ∈ (1[,)+∞) → (((1 / ((⌊‘𝑥) + 1)) · ((ψ‘(((⌊‘𝑥) + 1) − 1)) − (((⌊‘𝑥) + 1) − 1))) − (1 · 0)) = (((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) − 0))
17430subid1d 11609 . . . . . . . . . . 11 (𝑥 ∈ (1[,)+∞) → (((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) − 0) = ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1))
175173, 174eqtrd 2777 . . . . . . . . . 10 (𝑥 ∈ (1[,)+∞) → (((1 / ((⌊‘𝑥) + 1)) · ((ψ‘(((⌊‘𝑥) + 1) − 1)) − (((⌊‘𝑥) + 1) − 1))) − (1 · 0)) = ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1))
17697, 41syl 17 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 · (𝑛 + 1)) ∈ ℕ)
177176nnrecred 12317 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / (𝑛 · (𝑛 + 1))) ∈ ℝ)
178177recnd 11289 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / (𝑛 · (𝑛 + 1))) ∈ ℂ)
17997, 38syl 17 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅𝑛) ∈ ℝ)
180179recnd 11289 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅𝑛) ∈ ℂ)
181178, 180mulneg1d 11716 . . . . . . . . . . . . 13 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (-(1 / (𝑛 · (𝑛 + 1))) · (𝑅𝑛)) = -((1 / (𝑛 · (𝑛 + 1))) · (𝑅𝑛)))
18298, 112mulcld 11281 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 · 1) ∈ ℂ)
18398, 131mulcld 11281 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 · (𝑛 + 1)) ∈ ℂ)
184176nnne0d 12316 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 · (𝑛 + 1)) ≠ 0)
185131, 182, 183, 184divsubdird 12082 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑛 + 1) − (𝑛 · 1)) / (𝑛 · (𝑛 + 1))) = (((𝑛 + 1) / (𝑛 · (𝑛 + 1))) − ((𝑛 · 1) / (𝑛 · (𝑛 + 1)))))
18698mulridd 11278 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 · 1) = 𝑛)
187186oveq2d 7447 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) − (𝑛 · 1)) = ((𝑛 + 1) − 𝑛))
188187, 134eqtrd 2777 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) − (𝑛 · 1)) = 1)
189188oveq1d 7446 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑛 + 1) − (𝑛 · 1)) / (𝑛 · (𝑛 + 1))) = (1 / (𝑛 · (𝑛 + 1))))
190131mulridd 11278 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) · 1) = (𝑛 + 1))
191131, 98mulcomd 11282 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) · 𝑛) = (𝑛 · (𝑛 + 1)))
192190, 191oveq12d 7449 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑛 + 1) · 1) / ((𝑛 + 1) · 𝑛)) = ((𝑛 + 1) / (𝑛 · (𝑛 + 1))))
19397, 39syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 + 1) ∈ ℕ)
194193nnne0d 12316 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 + 1) ≠ 0)
195112, 98, 131, 142, 194divcan5d 12069 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑛 + 1) · 1) / ((𝑛 + 1) · 𝑛)) = (1 / 𝑛))
196192, 195eqtr3d 2779 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) / (𝑛 · (𝑛 + 1))) = (1 / 𝑛))
197112, 131, 98, 194, 142divcan5d 12069 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 · 1) / (𝑛 · (𝑛 + 1))) = (1 / (𝑛 + 1)))
198196, 197oveq12d 7449 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑛 + 1) / (𝑛 · (𝑛 + 1))) − ((𝑛 · 1) / (𝑛 · (𝑛 + 1)))) = ((1 / 𝑛) − (1 / (𝑛 + 1))))
199185, 189, 1983eqtr3d 2785 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / (𝑛 · (𝑛 + 1))) = ((1 / 𝑛) − (1 / (𝑛 + 1))))
200199negeqd 11502 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → -(1 / (𝑛 · (𝑛 + 1))) = -((1 / 𝑛) − (1 / (𝑛 + 1))))
20197nnrecred 12317 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / 𝑛) ∈ ℝ)
202201recnd 11289 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / 𝑛) ∈ ℂ)
203193nnrecred 12317 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / (𝑛 + 1)) ∈ ℝ)
204203recnd 11289 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / (𝑛 + 1)) ∈ ℂ)
205202, 204negsubdi2d 11636 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → -((1 / 𝑛) − (1 / (𝑛 + 1))) = ((1 / (𝑛 + 1)) − (1 / 𝑛)))
206200, 205eqtr2d 2778 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 / (𝑛 + 1)) − (1 / 𝑛)) = -(1 / (𝑛 · (𝑛 + 1))))
20797nnrpd 13075 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ+)
208100, 207eqeltrd 2841 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) − 1) ∈ ℝ+)
20935pntrval 27606 . . . . . . . . . . . . . . . 16 (((𝑛 + 1) − 1) ∈ ℝ+ → (𝑅‘((𝑛 + 1) − 1)) = ((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1)))
210208, 209syl 17 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘((𝑛 + 1) − 1)) = ((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1)))
211100fveq2d 6910 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘((𝑛 + 1) − 1)) = (𝑅𝑛))
212210, 211eqtr3d 2779 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1)) = (𝑅𝑛))
213206, 212oveq12d 7449 . . . . . . . . . . . . 13 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((1 / (𝑛 + 1)) − (1 / 𝑛)) · ((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1))) = (-(1 / (𝑛 · (𝑛 + 1))) · (𝑅𝑛)))
214180, 183, 184divrec2d 12047 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑅𝑛) / (𝑛 · (𝑛 + 1))) = ((1 / (𝑛 · (𝑛 + 1))) · (𝑅𝑛)))
215214negeqd 11502 . . . . . . . . . . . . 13 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → -((𝑅𝑛) / (𝑛 · (𝑛 + 1))) = -((1 / (𝑛 · (𝑛 + 1))) · (𝑅𝑛)))
216181, 213, 2153eqtr4d 2787 . . . . . . . . . . . 12 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((1 / (𝑛 + 1)) − (1 / 𝑛)) · ((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1))) = -((𝑅𝑛) / (𝑛 · (𝑛 + 1))))
21796, 216sumeq12rdv 15743 . . . . . . . . . . 11 (𝑥 ∈ (1[,)+∞) → Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))(((1 / (𝑛 + 1)) − (1 / 𝑛)) · ((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1))) = Σ𝑛 ∈ (1...(⌊‘𝑥))-((𝑅𝑛) / (𝑛 · (𝑛 + 1))))
218 fzfid 14014 . . . . . . . . . . . 12 (𝑥 ∈ (1[,)+∞) → (1...(⌊‘𝑥)) ∈ Fin)
21997, 42syl 17 . . . . . . . . . . . . 13 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑅𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ)
220219recnd 11289 . . . . . . . . . . . 12 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑅𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ)
221218, 220fsumneg 15823 . . . . . . . . . . 11 (𝑥 ∈ (1[,)+∞) → Σ𝑛 ∈ (1...(⌊‘𝑥))-((𝑅𝑛) / (𝑛 · (𝑛 + 1))) = -Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1))))
222217, 221eqtrd 2777 . . . . . . . . . 10 (𝑥 ∈ (1[,)+∞) → Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))(((1 / (𝑛 + 1)) − (1 / 𝑛)) · ((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1))) = -Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1))))
223175, 222oveq12d 7449 . . . . . . . . 9 (𝑥 ∈ (1[,)+∞) → ((((1 / ((⌊‘𝑥) + 1)) · ((ψ‘(((⌊‘𝑥) + 1) − 1)) − (((⌊‘𝑥) + 1) − 1))) − (1 · 0)) − Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))(((1 / (𝑛 + 1)) − (1 / 𝑛)) · ((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1)))) = (((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) − -Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))))
22492, 145, 2233eqtr3d 2785 . . . . . . . 8 (𝑥 ∈ (1[,)+∞) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) = (((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) − -Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))))
22530, 46subnegd 11627 . . . . . . . 8 (𝑥 ∈ (1[,)+∞) → (((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) − -Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) = (((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) + Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))))
226224, 225eqtrd 2777 . . . . . . 7 (𝑥 ∈ (1[,)+∞) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) = (((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) + Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))))
22730, 46, 226mvrladdd 11676 . . . . . 6 (𝑥 ∈ (1[,)+∞) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) − ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1)) = Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1))))
228227mpteq2ia 5245 . . . . 5 (𝑥 ∈ (1[,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) − ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1))) = (𝑥 ∈ (1[,)+∞) ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1))))
229 fzfid 14014 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ ℝ+) → (1...(⌊‘𝑥)) ∈ Fin)
23032adantl 481 . . . . . . . . . . 11 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
231230, 115syl 17 . . . . . . . . . 10 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈ ℝ)
232231, 139syl 17 . . . . . . . . 9 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) − 1) ∈ ℝ)
233232, 230nndivred 12320 . . . . . . . 8 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) − 1) / 𝑛) ∈ ℝ)
234229, 233fsumrecl 15770 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) ∈ ℝ)
235 rpre 13043 . . . . . . . . . . . 12 (𝑥 ∈ ℝ+𝑥 ∈ ℝ)
236235adantl 481 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ)
237236, 17syl 17 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℝ+) → (ψ‘𝑥) ∈ ℝ)
238237, 19syl 17 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((ψ‘𝑥) + 1) ∈ ℝ)
239 rprege0 13050 . . . . . . . . . . . 12 (𝑥 ∈ ℝ+ → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
240239, 22syl 17 . . . . . . . . . . 11 (𝑥 ∈ ℝ+ → (⌊‘𝑥) ∈ ℕ0)
241240adantl 481 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℝ+) → (⌊‘𝑥) ∈ ℕ0)
242241, 24syl 17 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((⌊‘𝑥) + 1) ∈ ℕ)
243238, 242nndivred 12320 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ∈ ℝ)
244 peano2rem 11576 . . . . . . . 8 ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ∈ ℝ → ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) ∈ ℝ)
245243, 244syl 17 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) ∈ ℝ)
246 reex 11246 . . . . . . . . . . . 12 ℝ ∈ V
247246, 14ssexi 5322 . . . . . . . . . . 11 + ∈ V
248247a1i 11 . . . . . . . . . 10 (⊤ → ℝ+ ∈ V)
249231, 230nndivred 12320 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) / 𝑛) ∈ ℝ)
250249recnd 11289 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) / 𝑛) ∈ ℂ)
251229, 250fsumcl 15769 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ∈ ℂ)
252 relogcl 26617 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ+ → (log‘𝑥) ∈ ℝ)
253252adantl 481 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℝ)
254253recnd 11289 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℂ)
255251, 254subcld 11620 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) ∈ ℂ)
256230nnrecred 12317 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / 𝑛) ∈ ℝ)
257229, 256fsumrecl 15770 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) ∈ ℝ)
258257, 253resubcld 11691 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)) ∈ ℝ)
259 eqidd 2738 . . . . . . . . . 10 (⊤ → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) = (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))))
260 eqidd 2738 . . . . . . . . . 10 (⊤ → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) = (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))))
261248, 255, 258, 259, 260offval2 7717 . . . . . . . . 9 (⊤ → ((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘f − (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)))) = (𝑥 ∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)))))
262256recnd 11289 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / 𝑛) ∈ ℂ)
263229, 250, 262fsumsub 15824 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) − (1 / 𝑛)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛)))
264231recnd 11289 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈ ℂ)
265 1cnd 11256 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℂ)
266230nncnd 12282 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℂ)
267230nnne0d 12316 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ≠ 0)
268264, 265, 266, 267divsubdird 12082 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) − 1) / 𝑛) = (((Λ‘𝑛) / 𝑛) − (1 / 𝑛)))
269268sumeq2dv 15738 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) − (1 / 𝑛)))
270257recnd 11289 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) ∈ ℂ)
271251, 270, 254nnncan2d 11655 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛)))
272263, 269, 2713eqtr4rd 2788 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛))
273272mpteq2dva 5242 . . . . . . . . 9 (⊤ → (𝑥 ∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)))) = (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛)))
274261, 273eqtrd 2777 . . . . . . . 8 (⊤ → ((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘f − (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)))) = (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛)))
275 vmadivsum 27526 . . . . . . . . 9 (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1)
27614a1i 11 . . . . . . . . . 10 (⊤ → ℝ+ ⊆ ℝ)
277258recnd 11289 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)) ∈ ℂ)
278 1red 11262 . . . . . . . . . 10 (⊤ → 1 ∈ ℝ)
279 harmoniclbnd 27052 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ+ → (log‘𝑥) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛))
280279adantl 481 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℝ+) → (log‘𝑥) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛))
281253, 257, 280abssubge0d 15470 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)))
282281adantrr 717 . . . . . . . . . . 11 ((⊤ ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)))
283235ad2antrl 728 . . . . . . . . . . . . 13 ((⊤ ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ)
284 simprr 773 . . . . . . . . . . . . 13 ((⊤ ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ≤ 𝑥)
285 harmonicubnd 27053 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) ≤ ((log‘𝑥) + 1))
286283, 284, 285syl2anc 584 . . . . . . . . . . . 12 ((⊤ ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) ≤ ((log‘𝑥) + 1))
287 1red 11262 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ ℝ+) → 1 ∈ ℝ)
288257, 253, 287lesubadd2d 11862 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)) ≤ 1 ↔ Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) ≤ ((log‘𝑥) + 1)))
289288adantrr 717 . . . . . . . . . . . 12 ((⊤ ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)) ≤ 1 ↔ Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) ≤ ((log‘𝑥) + 1)))
290286, 289mpbird 257 . . . . . . . . . . 11 ((⊤ ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)) ≤ 1)
291282, 290eqbrtrd 5165 . . . . . . . . . 10 ((⊤ ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) ≤ 1)
292276, 277, 278, 278, 291elo1d 15572 . . . . . . . . 9 (⊤ → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) ∈ 𝑂(1))
293 o1sub 15652 . . . . . . . . 9 (((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1) ∧ (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) ∈ 𝑂(1)) → ((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘f − (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)))) ∈ 𝑂(1))
294275, 292, 293sylancr 587 . . . . . . . 8 (⊤ → ((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘f − (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)))) ∈ 𝑂(1))
295274, 294eqeltrrd 2842 . . . . . . 7 (⊤ → (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛)) ∈ 𝑂(1))
296243recnd 11289 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ∈ ℂ)
297 1cnd 11256 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ ℝ+) → 1 ∈ ℂ)
298237recnd 11289 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → (ψ‘𝑥) ∈ ℂ)
299 rpcnne0 13053 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ+ → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
300299adantl 481 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
301 divdir 11947 . . . . . . . . . . . 12 (((ψ‘𝑥) ∈ ℂ ∧ 1 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → (((ψ‘𝑥) + 1) / 𝑥) = (((ψ‘𝑥) / 𝑥) + (1 / 𝑥)))
302298, 297, 300, 301syl3anc 1373 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) + 1) / 𝑥) = (((ψ‘𝑥) / 𝑥) + (1 / 𝑥)))
303302mpteq2dva 5242 . . . . . . . . . 10 (⊤ → (𝑥 ∈ ℝ+ ↦ (((ψ‘𝑥) + 1) / 𝑥)) = (𝑥 ∈ ℝ+ ↦ (((ψ‘𝑥) / 𝑥) + (1 / 𝑥))))
304 simpr 484 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ+)
305237, 304rerpdivcld 13108 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((ψ‘𝑥) / 𝑥) ∈ ℝ)
306 rpreccl 13061 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ+ → (1 / 𝑥) ∈ ℝ+)
307306adantl 481 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → (1 / 𝑥) ∈ ℝ+)
308 eqidd 2738 . . . . . . . . . . . 12 (⊤ → (𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) = (𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)))
309 eqidd 2738 . . . . . . . . . . . 12 (⊤ → (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) = (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)))
310248, 305, 307, 308, 309offval2 7717 . . . . . . . . . . 11 (⊤ → ((𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∘f + (𝑥 ∈ ℝ+ ↦ (1 / 𝑥))) = (𝑥 ∈ ℝ+ ↦ (((ψ‘𝑥) / 𝑥) + (1 / 𝑥))))
311 chpo1ub 27524 . . . . . . . . . . . 12 (𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∈ 𝑂(1)
312 divrcnv 15888 . . . . . . . . . . . . . 14 (1 ∈ ℂ → (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) ⇝𝑟 0)
31328, 312ax-mp 5 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) ⇝𝑟 0
314 rlimo1 15653 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) ⇝𝑟 0 → (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) ∈ 𝑂(1))
315313, 314mp1i 13 . . . . . . . . . . . 12 (⊤ → (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) ∈ 𝑂(1))
316 o1add 15650 . . . . . . . . . . . 12 (((𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∈ 𝑂(1) ∧ (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) ∈ 𝑂(1)) → ((𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∘f + (𝑥 ∈ ℝ+ ↦ (1 / 𝑥))) ∈ 𝑂(1))
317311, 315, 316sylancr 587 . . . . . . . . . . 11 (⊤ → ((𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∘f + (𝑥 ∈ ℝ+ ↦ (1 / 𝑥))) ∈ 𝑂(1))
318310, 317eqeltrrd 2842 . . . . . . . . . 10 (⊤ → (𝑥 ∈ ℝ+ ↦ (((ψ‘𝑥) / 𝑥) + (1 / 𝑥))) ∈ 𝑂(1))
319303, 318eqeltrd 2841 . . . . . . . . 9 (⊤ → (𝑥 ∈ ℝ+ ↦ (((ψ‘𝑥) + 1) / 𝑥)) ∈ 𝑂(1))
320238, 304rerpdivcld 13108 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) + 1) / 𝑥) ∈ ℝ)
321 chpge0 27169 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℝ → 0 ≤ (ψ‘𝑥))
322236, 321syl 17 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑥 ∈ ℝ+) → 0 ≤ (ψ‘𝑥))
323237, 322ge0p1rpd 13107 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((ψ‘𝑥) + 1) ∈ ℝ+)
324323rprege0d 13084 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) + 1) ∈ ℝ ∧ 0 ≤ ((ψ‘𝑥) + 1)))
325242nnrpd 13075 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((⌊‘𝑥) + 1) ∈ ℝ+)
326325rpregt0d 13083 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((⌊‘𝑥) + 1) ∈ ℝ ∧ 0 < ((⌊‘𝑥) + 1)))
327 divge0 12137 . . . . . . . . . . . . 13 (((((ψ‘𝑥) + 1) ∈ ℝ ∧ 0 ≤ ((ψ‘𝑥) + 1)) ∧ (((⌊‘𝑥) + 1) ∈ ℝ ∧ 0 < ((⌊‘𝑥) + 1))) → 0 ≤ (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)))
328324, 326, 327syl2anc 584 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → 0 ≤ (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)))
329243, 328absidd 15461 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → (abs‘(((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1))) = (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)))
330320recnd 11289 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) + 1) / 𝑥) ∈ ℂ)
331330abscld 15475 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → (abs‘(((ψ‘𝑥) + 1) / 𝑥)) ∈ ℝ)
332 fllep1 13841 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → 𝑥 ≤ ((⌊‘𝑥) + 1))
333236, 332syl 17 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℝ+) → 𝑥 ≤ ((⌊‘𝑥) + 1))
334 rpregt0 13049 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ+ → (𝑥 ∈ ℝ ∧ 0 < 𝑥))
335334adantl 481 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ ℝ+) → (𝑥 ∈ ℝ ∧ 0 < 𝑥))
336323rpregt0d 13083 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) + 1) ∈ ℝ ∧ 0 < ((ψ‘𝑥) + 1)))
337 lediv2 12158 . . . . . . . . . . . . . 14 (((𝑥 ∈ ℝ ∧ 0 < 𝑥) ∧ (((⌊‘𝑥) + 1) ∈ ℝ ∧ 0 < ((⌊‘𝑥) + 1)) ∧ (((ψ‘𝑥) + 1) ∈ ℝ ∧ 0 < ((ψ‘𝑥) + 1))) → (𝑥 ≤ ((⌊‘𝑥) + 1) ↔ (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ≤ (((ψ‘𝑥) + 1) / 𝑥)))
338335, 326, 336, 337syl3anc 1373 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℝ+) → (𝑥 ≤ ((⌊‘𝑥) + 1) ↔ (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ≤ (((ψ‘𝑥) + 1) / 𝑥)))
339333, 338mpbid 232 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ≤ (((ψ‘𝑥) + 1) / 𝑥))
340320leabsd 15453 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) + 1) / 𝑥) ≤ (abs‘(((ψ‘𝑥) + 1) / 𝑥)))
341243, 320, 331, 339, 340letrd 11418 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ≤ (abs‘(((ψ‘𝑥) + 1) / 𝑥)))
342329, 341eqbrtrd 5165 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℝ+) → (abs‘(((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1))) ≤ (abs‘(((ψ‘𝑥) + 1) / 𝑥)))
343342adantrr 717 . . . . . . . . 9 ((⊤ ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1))) ≤ (abs‘(((ψ‘𝑥) + 1) / 𝑥)))
344278, 319, 320, 296, 343o1le 15689 . . . . . . . 8 (⊤ → (𝑥 ∈ ℝ+ ↦ (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1))) ∈ 𝑂(1))
345 o1const 15656 . . . . . . . . . 10 ((ℝ+ ⊆ ℝ ∧ 1 ∈ ℂ) → (𝑥 ∈ ℝ+ ↦ 1) ∈ 𝑂(1))
34614, 28, 345mp2an 692 . . . . . . . . 9 (𝑥 ∈ ℝ+ ↦ 1) ∈ 𝑂(1)
347346a1i 11 . . . . . . . 8 (⊤ → (𝑥 ∈ ℝ+ ↦ 1) ∈ 𝑂(1))
348296, 297, 344, 347o1sub2 15662 . . . . . . 7 (⊤ → (𝑥 ∈ ℝ+ ↦ ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1)) ∈ 𝑂(1))
349234, 245, 295, 348o1sub2 15662 . . . . . 6 (⊤ → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) − ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1))) ∈ 𝑂(1))
35013, 349o1res2 15599 . . . . 5 (⊤ → (𝑥 ∈ (1[,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) − ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1))) ∈ 𝑂(1))
351228, 350eqeltrrid 2846 . . . 4 (⊤ → (𝑥 ∈ (1[,)+∞) ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) ∈ 𝑂(1))
35216, 351eqeltrd 2841 . . 3 (⊤ → ((𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) ↾ (1[,)+∞)) ∈ 𝑂(1))
353 eqid 2737 . . . . . 6 (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) = (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1))))
354353, 45fmpti 7132 . . . . 5 (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))):ℝ⟶ℂ
355354a1i 11 . . . 4 (⊤ → (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))):ℝ⟶ℂ)
356 ssidd 4007 . . . 4 (⊤ → ℝ ⊆ ℝ)
357355, 356, 278o1resb 15602 . . 3 (⊤ → ((𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) ∈ 𝑂(1) ↔ ((𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) ↾ (1[,)+∞)) ∈ 𝑂(1)))
358352, 357mpbird 257 . 2 (⊤ → (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) ∈ 𝑂(1))
359358mptru 1547 1 (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) ∈ 𝑂(1)
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395   = wceq 1540  wtru 1541  wcel 2108  wne 2940  Vcvv 3480  wss 3951   class class class wbr 5143  cmpt 5225  cres 5687  wf 6557  cfv 6561  (class class class)co 7431  f cof 7695  cc 11153  cr 11154  0cc0 11155  1c1 11156   + caddc 11158   · cmul 11160  +∞cpnf 11292   < clt 11295  cle 11296  cmin 11492  -cneg 11493   / cdiv 11920  cn 12266  2c2 12321  0cn0 12526  cz 12613  cuz 12878  +crp 13034  [,)cico 13389  ...cfz 13547  ..^cfzo 13694  cfl 13830  abscabs 15273  𝑟 crli 15521  𝑂(1)co1 15522  Σcsu 15722  logclog 26596  Λcvma 27135  ψcchp 27136
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-inf2 9681  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233  ax-addf 11234
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-tp 4631  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-iin 4994  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-of 7697  df-om 7888  df-1st 8014  df-2nd 8015  df-supp 8186  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-2o 8507  df-oadd 8510  df-er 8745  df-map 8868  df-pm 8869  df-ixp 8938  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-fsupp 9402  df-fi 9451  df-sup 9482  df-inf 9483  df-oi 9550  df-dju 9941  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-4 12331  df-5 12332  df-6 12333  df-7 12334  df-8 12335  df-9 12336  df-n0 12527  df-xnn0 12600  df-z 12614  df-dec 12734  df-uz 12879  df-q 12991  df-rp 13035  df-xneg 13154  df-xadd 13155  df-xmul 13156  df-ioo 13391  df-ioc 13392  df-ico 13393  df-icc 13394  df-fz 13548  df-fzo 13695  df-fl 13832  df-mod 13910  df-seq 14043  df-exp 14103  df-fac 14313  df-bc 14342  df-hash 14370  df-shft 15106  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275  df-limsup 15507  df-clim 15524  df-rlim 15525  df-o1 15526  df-lo1 15527  df-sum 15723  df-ef 16103  df-e 16104  df-sin 16105  df-cos 16106  df-tan 16107  df-pi 16108  df-dvds 16291  df-gcd 16532  df-prm 16709  df-pc 16875  df-struct 17184  df-sets 17201  df-slot 17219  df-ndx 17231  df-base 17248  df-ress 17275  df-plusg 17310  df-mulr 17311  df-starv 17312  df-sca 17313  df-vsca 17314  df-ip 17315  df-tset 17316  df-ple 17317  df-ds 17319  df-unif 17320  df-hom 17321  df-cco 17322  df-rest 17467  df-topn 17468  df-0g 17486  df-gsum 17487  df-topgen 17488  df-pt 17489  df-prds 17492  df-xrs 17547  df-qtop 17552  df-imas 17553  df-xps 17555  df-mre 17629  df-mrc 17630  df-acs 17632  df-mgm 18653  df-sgrp 18732  df-mnd 18748  df-submnd 18797  df-mulg 19086  df-cntz 19335  df-cmn 19800  df-psmet 21356  df-xmet 21357  df-met 21358  df-bl 21359  df-mopn 21360  df-fbas 21361  df-fg 21362  df-cnfld 21365  df-top 22900  df-topon 22917  df-topsp 22939  df-bases 22953  df-cld 23027  df-ntr 23028  df-cls 23029  df-nei 23106  df-lp 23144  df-perf 23145  df-cn 23235  df-cnp 23236  df-haus 23323  df-cmp 23395  df-tx 23570  df-hmeo 23763  df-fil 23854  df-fm 23946  df-flim 23947  df-flf 23948  df-xms 24330  df-ms 24331  df-tms 24332  df-cncf 24904  df-limc 25901  df-dv 25902  df-ulm 26420  df-log 26598  df-cxp 26599  df-atan 26910  df-em 27036  df-cht 27140  df-vma 27141  df-chp 27142  df-ppi 27143
This theorem is referenced by:  pntrsumbnd  27610
  Copyright terms: Public domain W3C validator