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

Theorem pntrsumo1 27518
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 11252 . . . . . . . . . . 11 1 ∈ ℝ
2 elicopnf 13462 . . . . . . . . . . 11 (1 ∈ ℝ → (𝑥 ∈ (1[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 1 ≤ 𝑥)))
31, 2ax-mp 5 . . . . . . . . . 10 (𝑥 ∈ (1[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 1 ≤ 𝑥))
43simplbi 496 . . . . . . . . 9 (𝑥 ∈ (1[,)+∞) → 𝑥 ∈ ℝ)
5 0red 11255 . . . . . . . . . 10 (𝑥 ∈ (1[,)+∞) → 0 ∈ ℝ)
6 1red 11253 . . . . . . . . . 10 (𝑥 ∈ (1[,)+∞) → 1 ∈ ℝ)
7 0lt1 11774 . . . . . . . . . . 11 0 < 1
87a1i 11 . . . . . . . . . 10 (𝑥 ∈ (1[,)+∞) → 0 < 1)
93simprbi 495 . . . . . . . . . 10 (𝑥 ∈ (1[,)+∞) → 1 ≤ 𝑥)
105, 6, 4, 8, 9ltletrd 11412 . . . . . . . . 9 (𝑥 ∈ (1[,)+∞) → 0 < 𝑥)
114, 10elrpd 13053 . . . . . . . 8 (𝑥 ∈ (1[,)+∞) → 𝑥 ∈ ℝ+)
1211ssriv 3986 . . . . . . 7 (1[,)+∞) ⊆ ℝ+
1312a1i 11 . . . . . 6 (⊤ → (1[,)+∞) ⊆ ℝ+)
14 rpssre 13021 . . . . . 6 + ⊆ ℝ
1513, 14sstrdi 3994 . . . . 5 (⊤ → (1[,)+∞) ⊆ ℝ)
1615resmptd 6049 . . . 4 (⊤ → ((𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) ↾ (1[,)+∞)) = (𝑥 ∈ (1[,)+∞) ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))))
17 chpcl 27076 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → (ψ‘𝑥) ∈ ℝ)
184, 17syl 17 . . . . . . . . . . 11 (𝑥 ∈ (1[,)+∞) → (ψ‘𝑥) ∈ ℝ)
19 peano2re 11425 . . . . . . . . . . 11 ((ψ‘𝑥) ∈ ℝ → ((ψ‘𝑥) + 1) ∈ ℝ)
2018, 19syl 17 . . . . . . . . . 10 (𝑥 ∈ (1[,)+∞) → ((ψ‘𝑥) + 1) ∈ ℝ)
2111rprege0d 13063 . . . . . . . . . . . 12 (𝑥 ∈ (1[,)+∞) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
22 flge0nn0 13825 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → (⌊‘𝑥) ∈ ℕ0)
2321, 22syl 17 . . . . . . . . . . 11 (𝑥 ∈ (1[,)+∞) → (⌊‘𝑥) ∈ ℕ0)
24 nn0p1nn 12549 . . . . . . . . . . 11 ((⌊‘𝑥) ∈ ℕ0 → ((⌊‘𝑥) + 1) ∈ ℕ)
2523, 24syl 17 . . . . . . . . . 10 (𝑥 ∈ (1[,)+∞) → ((⌊‘𝑥) + 1) ∈ ℕ)
2620, 25nndivred 12304 . . . . . . . . 9 (𝑥 ∈ (1[,)+∞) → (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ∈ ℝ)
2726recnd 11280 . . . . . . . 8 (𝑥 ∈ (1[,)+∞) → (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ∈ ℂ)
28 ax-1cn 11204 . . . . . . . 8 1 ∈ ℂ
29 subcl 11497 . . . . . . . 8 (((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ∈ ℂ ∧ 1 ∈ ℂ) → ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) ∈ ℂ)
3027, 28, 29sylancl 584 . . . . . . 7 (𝑥 ∈ (1[,)+∞) → ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) ∈ ℂ)
31 fzfid 13978 . . . . . . . . . 10 (𝑥 ∈ ℝ → (1...(⌊‘𝑥)) ∈ Fin)
32 elfznn 13570 . . . . . . . . . . . 12 (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
3332adantl 480 . . . . . . . . . . 11 ((𝑥 ∈ ℝ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
34 nnrp 13025 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → 𝑛 ∈ ℝ+)
35 pntrval.r . . . . . . . . . . . . . . 15 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))
3635pntrf 27516 . . . . . . . . . . . . . 14 𝑅:ℝ+⟶ℝ
3736ffvelcdmi 7098 . . . . . . . . . . . . 13 (𝑛 ∈ ℝ+ → (𝑅𝑛) ∈ ℝ)
3834, 37syl 17 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → (𝑅𝑛) ∈ ℝ)
39 peano2nn 12262 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℕ)
40 nnmulcl 12274 . . . . . . . . . . . . 13 ((𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ ℕ) → (𝑛 · (𝑛 + 1)) ∈ ℕ)
4139, 40mpdan 685 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → (𝑛 · (𝑛 + 1)) ∈ ℕ)
4238, 41nndivred 12304 . . . . . . . . . . 11 (𝑛 ∈ ℕ → ((𝑅𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ)
4333, 42syl 17 . . . . . . . . . 10 ((𝑥 ∈ ℝ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑅𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ)
4431, 43fsumrecl 15720 . . . . . . . . 9 (𝑥 ∈ ℝ → Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ)
4544recnd 11280 . . . . . . . 8 (𝑥 ∈ ℝ → Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ)
464, 45syl 17 . . . . . . 7 (𝑥 ∈ (1[,)+∞) → Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ)
47 oveq2 7434 . . . . . . . . . . 11 (𝑚 = 𝑛 → (1 / 𝑚) = (1 / 𝑛))
48 fvoveq1 7449 . . . . . . . . . . . 12 (𝑚 = 𝑛 → (ψ‘(𝑚 − 1)) = (ψ‘(𝑛 − 1)))
49 oveq1 7433 . . . . . . . . . . . 12 (𝑚 = 𝑛 → (𝑚 − 1) = (𝑛 − 1))
5048, 49oveq12d 7444 . . . . . . . . . . 11 (𝑚 = 𝑛 → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = ((ψ‘(𝑛 − 1)) − (𝑛 − 1)))
5147, 50jca 510 . . . . . . . . . 10 (𝑚 = 𝑛 → ((1 / 𝑚) = (1 / 𝑛) ∧ ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = ((ψ‘(𝑛 − 1)) − (𝑛 − 1))))
52 oveq2 7434 . . . . . . . . . . 11 (𝑚 = (𝑛 + 1) → (1 / 𝑚) = (1 / (𝑛 + 1)))
53 fvoveq1 7449 . . . . . . . . . . . 12 (𝑚 = (𝑛 + 1) → (ψ‘(𝑚 − 1)) = (ψ‘((𝑛 + 1) − 1)))
54 oveq1 7433 . . . . . . . . . . . 12 (𝑚 = (𝑛 + 1) → (𝑚 − 1) = ((𝑛 + 1) − 1))
5553, 54oveq12d 7444 . . . . . . . . . . 11 (𝑚 = (𝑛 + 1) → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = ((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1)))
5652, 55jca 510 . . . . . . . . . 10 (𝑚 = (𝑛 + 1) → ((1 / 𝑚) = (1 / (𝑛 + 1)) ∧ ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = ((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1))))
57 oveq2 7434 . . . . . . . . . . . 12 (𝑚 = 1 → (1 / 𝑚) = (1 / 1))
58 1div1e1 11942 . . . . . . . . . . . 12 (1 / 1) = 1
5957, 58eqtrdi 2784 . . . . . . . . . . 11 (𝑚 = 1 → (1 / 𝑚) = 1)
60 oveq1 7433 . . . . . . . . . . . . . . . 16 (𝑚 = 1 → (𝑚 − 1) = (1 − 1))
61 1m1e0 12322 . . . . . . . . . . . . . . . 16 (1 − 1) = 0
6260, 61eqtrdi 2784 . . . . . . . . . . . . . . 15 (𝑚 = 1 → (𝑚 − 1) = 0)
6362fveq2d 6906 . . . . . . . . . . . . . 14 (𝑚 = 1 → (ψ‘(𝑚 − 1)) = (ψ‘0))
64 2pos 12353 . . . . . . . . . . . . . . 15 0 < 2
65 0re 11254 . . . . . . . . . . . . . . . 16 0 ∈ ℝ
66 chpeq0 27161 . . . . . . . . . . . . . . . 16 (0 ∈ ℝ → ((ψ‘0) = 0 ↔ 0 < 2))
6765, 66ax-mp 5 . . . . . . . . . . . . . . 15 ((ψ‘0) = 0 ↔ 0 < 2)
6864, 67mpbir 230 . . . . . . . . . . . . . 14 (ψ‘0) = 0
6963, 68eqtrdi 2784 . . . . . . . . . . . . 13 (𝑚 = 1 → (ψ‘(𝑚 − 1)) = 0)
7069, 62oveq12d 7444 . . . . . . . . . . . 12 (𝑚 = 1 → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = (0 − 0))
71 0m0e0 12370 . . . . . . . . . . . 12 (0 − 0) = 0
7270, 71eqtrdi 2784 . . . . . . . . . . 11 (𝑚 = 1 → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = 0)
7359, 72jca 510 . . . . . . . . . 10 (𝑚 = 1 → ((1 / 𝑚) = 1 ∧ ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = 0))
74 oveq2 7434 . . . . . . . . . . 11 (𝑚 = ((⌊‘𝑥) + 1) → (1 / 𝑚) = (1 / ((⌊‘𝑥) + 1)))
75 fvoveq1 7449 . . . . . . . . . . . 12 (𝑚 = ((⌊‘𝑥) + 1) → (ψ‘(𝑚 − 1)) = (ψ‘(((⌊‘𝑥) + 1) − 1)))
76 oveq1 7433 . . . . . . . . . . . 12 (𝑚 = ((⌊‘𝑥) + 1) → (𝑚 − 1) = (((⌊‘𝑥) + 1) − 1))
7775, 76oveq12d 7444 . . . . . . . . . . 11 (𝑚 = ((⌊‘𝑥) + 1) → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = ((ψ‘(((⌊‘𝑥) + 1) − 1)) − (((⌊‘𝑥) + 1) − 1)))
7874, 77jca 510 . . . . . . . . . 10 (𝑚 = ((⌊‘𝑥) + 1) → ((1 / 𝑚) = (1 / ((⌊‘𝑥) + 1)) ∧ ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = ((ψ‘(((⌊‘𝑥) + 1) − 1)) − (((⌊‘𝑥) + 1) − 1))))
79 nnuz 12903 . . . . . . . . . . 11 ℕ = (ℤ‘1)
8025, 79eleqtrdi 2839 . . . . . . . . . 10 (𝑥 ∈ (1[,)+∞) → ((⌊‘𝑥) + 1) ∈ (ℤ‘1))
81 elfznn 13570 . . . . . . . . . . . . 13 (𝑚 ∈ (1...((⌊‘𝑥) + 1)) → 𝑚 ∈ ℕ)
8281adantl 480 . . . . . . . . . . . 12 ((𝑥 ∈ (1[,)+∞) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 𝑚 ∈ ℕ)
8382nnrecred 12301 . . . . . . . . . . 11 ((𝑥 ∈ (1[,)+∞) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (1 / 𝑚) ∈ ℝ)
8483recnd 11280 . . . . . . . . . 10 ((𝑥 ∈ (1[,)+∞) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (1 / 𝑚) ∈ ℂ)
8582nnred 12265 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 𝑚 ∈ ℝ)
86 peano2rem 11565 . . . . . . . . . . . . . 14 (𝑚 ∈ ℝ → (𝑚 − 1) ∈ ℝ)
8785, 86syl 17 . . . . . . . . . . . . 13 ((𝑥 ∈ (1[,)+∞) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑚 − 1) ∈ ℝ)
88 chpcl 27076 . . . . . . . . . . . . 13 ((𝑚 − 1) ∈ ℝ → (ψ‘(𝑚 − 1)) ∈ ℝ)
8987, 88syl 17 . . . . . . . . . . . 12 ((𝑥 ∈ (1[,)+∞) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (ψ‘(𝑚 − 1)) ∈ ℝ)
9089, 87resubcld 11680 . . . . . . . . . . 11 ((𝑥 ∈ (1[,)+∞) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) ∈ ℝ)
9190recnd 11280 . . . . . . . . . 10 ((𝑥 ∈ (1[,)+∞) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) ∈ ℂ)
9251, 56, 73, 78, 80, 84, 91fsumparts 15792 . . . . . . . . 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 13803 . . . . . . . . . . . 12 (𝑥 ∈ (1[,)+∞) → (⌊‘𝑥) ∈ ℤ)
94 fzval3 13741 . . . . . . . . . . . 12 ((⌊‘𝑥) ∈ ℤ → (1...(⌊‘𝑥)) = (1..^((⌊‘𝑥) + 1)))
9593, 94syl 17 . . . . . . . . . . 11 (𝑥 ∈ (1[,)+∞) → (1...(⌊‘𝑥)) = (1..^((⌊‘𝑥) + 1)))
9695eqcomd 2734 . . . . . . . . . 10 (𝑥 ∈ (1[,)+∞) → (1..^((⌊‘𝑥) + 1)) = (1...(⌊‘𝑥)))
9732adantl 480 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
9897nncnd 12266 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℂ)
99 pncan 11504 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛 + 1) − 1) = 𝑛)
10098, 28, 99sylancl 584 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) − 1) = 𝑛)
10197nnred 12265 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ)
102100, 101eqeltrd 2829 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) − 1) ∈ ℝ)
103 chpcl 27076 . . . . . . . . . . . . . . . 16 (((𝑛 + 1) − 1) ∈ ℝ → (ψ‘((𝑛 + 1) − 1)) ∈ ℝ)
104102, 103syl 17 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (ψ‘((𝑛 + 1) − 1)) ∈ ℝ)
105104recnd 11280 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (ψ‘((𝑛 + 1) − 1)) ∈ ℂ)
106102recnd 11280 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) − 1) ∈ ℂ)
107 peano2rem 11565 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℝ → (𝑛 − 1) ∈ ℝ)
108101, 107syl 17 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 − 1) ∈ ℝ)
109 chpcl 27076 . . . . . . . . . . . . . . . 16 ((𝑛 − 1) ∈ ℝ → (ψ‘(𝑛 − 1)) ∈ ℝ)
110108, 109syl 17 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (ψ‘(𝑛 − 1)) ∈ ℝ)
111110recnd 11280 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (ψ‘(𝑛 − 1)) ∈ ℂ)
112 1cnd 11247 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℂ)
11398, 112subcld 11609 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 − 1) ∈ ℂ)
114105, 106, 111, 113sub4d 11658 . . . . . . . . . . . . 13 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1)) − ((ψ‘(𝑛 − 1)) − (𝑛 − 1))) = (((ψ‘((𝑛 + 1) − 1)) − (ψ‘(𝑛 − 1))) − (((𝑛 + 1) − 1) − (𝑛 − 1))))
115 vmacl 27070 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ → (Λ‘𝑛) ∈ ℝ)
11697, 115syl 17 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈ ℝ)
117116recnd 11280 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈ ℂ)
118 nnm1nn0 12551 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → (𝑛 − 1) ∈ ℕ0)
11997, 118syl 17 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 − 1) ∈ ℕ0)
120 chpp1 27107 . . . . . . . . . . . . . . . . 17 ((𝑛 − 1) ∈ ℕ0 → (ψ‘((𝑛 − 1) + 1)) = ((ψ‘(𝑛 − 1)) + (Λ‘((𝑛 − 1) + 1))))
121119, 120syl 17 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (ψ‘((𝑛 − 1) + 1)) = ((ψ‘(𝑛 − 1)) + (Λ‘((𝑛 − 1) + 1))))
122 npcan 11507 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛 − 1) + 1) = 𝑛)
12398, 28, 122sylancl 584 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 − 1) + 1) = 𝑛)
124123, 100eqtr4d 2771 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 − 1) + 1) = ((𝑛 + 1) − 1))
125124fveq2d 6906 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (ψ‘((𝑛 − 1) + 1)) = (ψ‘((𝑛 + 1) − 1)))
126123fveq2d 6906 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘((𝑛 − 1) + 1)) = (Λ‘𝑛))
127126oveq2d 7442 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((ψ‘(𝑛 − 1)) + (Λ‘((𝑛 − 1) + 1))) = ((ψ‘(𝑛 − 1)) + (Λ‘𝑛)))
128121, 125, 1273eqtr3d 2776 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (ψ‘((𝑛 + 1) − 1)) = ((ψ‘(𝑛 − 1)) + (Λ‘𝑛)))
129111, 117, 128mvrladdd 11665 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((ψ‘((𝑛 + 1) − 1)) − (ψ‘(𝑛 − 1))) = (Λ‘𝑛))
130 peano2cn 11424 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℂ → (𝑛 + 1) ∈ ℂ)
13198, 130syl 17 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 + 1) ∈ ℂ)
132131, 98, 112nnncan2d 11644 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑛 + 1) − 1) − (𝑛 − 1)) = ((𝑛 + 1) − 𝑛))
133 pncan2 11505 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛 + 1) − 𝑛) = 1)
13498, 28, 133sylancl 584 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) − 𝑛) = 1)
135132, 134eqtrd 2768 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑛 + 1) − 1) − (𝑛 − 1)) = 1)
136129, 135oveq12d 7444 . . . . . . . . . . . . 13 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((ψ‘((𝑛 + 1) − 1)) − (ψ‘(𝑛 − 1))) − (((𝑛 + 1) − 1) − (𝑛 − 1))) = ((Λ‘𝑛) − 1))
137114, 136eqtrd 2768 . . . . . . . . . . . 12 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1)) − ((ψ‘(𝑛 − 1)) − (𝑛 − 1))) = ((Λ‘𝑛) − 1))
138137oveq2d 7442 . . . . . . . . . . 11 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 / 𝑛) · (((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1)) − ((ψ‘(𝑛 − 1)) − (𝑛 − 1)))) = ((1 / 𝑛) · ((Λ‘𝑛) − 1)))
139 peano2rem 11565 . . . . . . . . . . . . . 14 ((Λ‘𝑛) ∈ ℝ → ((Λ‘𝑛) − 1) ∈ ℝ)
140116, 139syl 17 . . . . . . . . . . . . 13 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) − 1) ∈ ℝ)
141140recnd 11280 . . . . . . . . . . . 12 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) − 1) ∈ ℂ)
14297nnne0d 12300 . . . . . . . . . . . 12 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ≠ 0)
143141, 98, 142divrec2d 12032 . . . . . . . . . . 11 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) − 1) / 𝑛) = ((1 / 𝑛) · ((Λ‘𝑛) − 1)))
144138, 143eqtr4d 2771 . . . . . . . . . 10 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 / 𝑛) · (((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1)) − ((ψ‘(𝑛 − 1)) − (𝑛 − 1)))) = (((Λ‘𝑛) − 1) / 𝑛))
14596, 144sumeq12rdv 15693 . . . . . . . . 9 (𝑥 ∈ (1[,)+∞) → Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))((1 / 𝑛) · (((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1)) − ((ψ‘(𝑛 − 1)) − (𝑛 − 1)))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛))
14623nn0cnd 12572 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (1[,)+∞) → (⌊‘𝑥) ∈ ℂ)
147 pncan 11504 . . . . . . . . . . . . . . . . . . 19 (((⌊‘𝑥) ∈ ℂ ∧ 1 ∈ ℂ) → (((⌊‘𝑥) + 1) − 1) = (⌊‘𝑥))
148146, 28, 147sylancl 584 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (1[,)+∞) → (((⌊‘𝑥) + 1) − 1) = (⌊‘𝑥))
149148fveq2d 6906 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (1[,)+∞) → (ψ‘(((⌊‘𝑥) + 1) − 1)) = (ψ‘(⌊‘𝑥)))
150 chpfl 27102 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℝ → (ψ‘(⌊‘𝑥)) = (ψ‘𝑥))
1514, 150syl 17 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (1[,)+∞) → (ψ‘(⌊‘𝑥)) = (ψ‘𝑥))
152149, 151eqtrd 2768 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1[,)+∞) → (ψ‘(((⌊‘𝑥) + 1) − 1)) = (ψ‘𝑥))
153152oveq1d 7441 . . . . . . . . . . . . . . 15 (𝑥 ∈ (1[,)+∞) → ((ψ‘(((⌊‘𝑥) + 1) − 1)) − (((⌊‘𝑥) + 1) − 1)) = ((ψ‘𝑥) − (((⌊‘𝑥) + 1) − 1)))
15418recnd 11280 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1[,)+∞) → (ψ‘𝑥) ∈ ℂ)
15525nncnd 12266 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1[,)+∞) → ((⌊‘𝑥) + 1) ∈ ℂ)
156 1cnd 11247 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1[,)+∞) → 1 ∈ ℂ)
157154, 155, 156subsub3d 11639 . . . . . . . . . . . . . . 15 (𝑥 ∈ (1[,)+∞) → ((ψ‘𝑥) − (((⌊‘𝑥) + 1) − 1)) = (((ψ‘𝑥) + 1) − ((⌊‘𝑥) + 1)))
158153, 157eqtrd 2768 . . . . . . . . . . . . . 14 (𝑥 ∈ (1[,)+∞) → ((ψ‘(((⌊‘𝑥) + 1) − 1)) − (((⌊‘𝑥) + 1) − 1)) = (((ψ‘𝑥) + 1) − ((⌊‘𝑥) + 1)))
159158oveq2d 7442 . . . . . . . . . . . . 13 (𝑥 ∈ (1[,)+∞) → ((1 / ((⌊‘𝑥) + 1)) · ((ψ‘(((⌊‘𝑥) + 1) − 1)) − (((⌊‘𝑥) + 1) − 1))) = ((1 / ((⌊‘𝑥) + 1)) · (((ψ‘𝑥) + 1) − ((⌊‘𝑥) + 1))))
16025nnrecred 12301 . . . . . . . . . . . . . . 15 (𝑥 ∈ (1[,)+∞) → (1 / ((⌊‘𝑥) + 1)) ∈ ℝ)
161160recnd 11280 . . . . . . . . . . . . . 14 (𝑥 ∈ (1[,)+∞) → (1 / ((⌊‘𝑥) + 1)) ∈ ℂ)
162 peano2cn 11424 . . . . . . . . . . . . . . 15 ((ψ‘𝑥) ∈ ℂ → ((ψ‘𝑥) + 1) ∈ ℂ)
163154, 162syl 17 . . . . . . . . . . . . . 14 (𝑥 ∈ (1[,)+∞) → ((ψ‘𝑥) + 1) ∈ ℂ)
164161, 163, 155subdid 11708 . . . . . . . . . . . . 13 (𝑥 ∈ (1[,)+∞) → ((1 / ((⌊‘𝑥) + 1)) · (((ψ‘𝑥) + 1) − ((⌊‘𝑥) + 1))) = (((1 / ((⌊‘𝑥) + 1)) · ((ψ‘𝑥) + 1)) − ((1 / ((⌊‘𝑥) + 1)) · ((⌊‘𝑥) + 1))))
16525nnne0d 12300 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1[,)+∞) → ((⌊‘𝑥) + 1) ≠ 0)
166163, 155, 165divrec2d 12032 . . . . . . . . . . . . . . 15 (𝑥 ∈ (1[,)+∞) → (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) = ((1 / ((⌊‘𝑥) + 1)) · ((ψ‘𝑥) + 1)))
167166eqcomd 2734 . . . . . . . . . . . . . 14 (𝑥 ∈ (1[,)+∞) → ((1 / ((⌊‘𝑥) + 1)) · ((ψ‘𝑥) + 1)) = (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)))
168155, 165recid2d 12024 . . . . . . . . . . . . . 14 (𝑥 ∈ (1[,)+∞) → ((1 / ((⌊‘𝑥) + 1)) · ((⌊‘𝑥) + 1)) = 1)
169167, 168oveq12d 7444 . . . . . . . . . . . . 13 (𝑥 ∈ (1[,)+∞) → (((1 / ((⌊‘𝑥) + 1)) · ((ψ‘𝑥) + 1)) − ((1 / ((⌊‘𝑥) + 1)) · ((⌊‘𝑥) + 1))) = ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1))
170159, 164, 1693eqtrd 2772 . . . . . . . . . . . 12 (𝑥 ∈ (1[,)+∞) → ((1 / ((⌊‘𝑥) + 1)) · ((ψ‘(((⌊‘𝑥) + 1) − 1)) − (((⌊‘𝑥) + 1) − 1))) = ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1))
17128mul01i 11442 . . . . . . . . . . . . 13 (1 · 0) = 0
172171a1i 11 . . . . . . . . . . . 12 (𝑥 ∈ (1[,)+∞) → (1 · 0) = 0)
173170, 172oveq12d 7444 . . . . . . . . . . 11 (𝑥 ∈ (1[,)+∞) → (((1 / ((⌊‘𝑥) + 1)) · ((ψ‘(((⌊‘𝑥) + 1) − 1)) − (((⌊‘𝑥) + 1) − 1))) − (1 · 0)) = (((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) − 0))
17430subid1d 11598 . . . . . . . . . . 11 (𝑥 ∈ (1[,)+∞) → (((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) − 0) = ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1))
175173, 174eqtrd 2768 . . . . . . . . . 10 (𝑥 ∈ (1[,)+∞) → (((1 / ((⌊‘𝑥) + 1)) · ((ψ‘(((⌊‘𝑥) + 1) − 1)) − (((⌊‘𝑥) + 1) − 1))) − (1 · 0)) = ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1))
17697, 41syl 17 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 · (𝑛 + 1)) ∈ ℕ)
177176nnrecred 12301 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / (𝑛 · (𝑛 + 1))) ∈ ℝ)
178177recnd 11280 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / (𝑛 · (𝑛 + 1))) ∈ ℂ)
17997, 38syl 17 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅𝑛) ∈ ℝ)
180179recnd 11280 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅𝑛) ∈ ℂ)
181178, 180mulneg1d 11705 . . . . . . . . . . . . 13 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (-(1 / (𝑛 · (𝑛 + 1))) · (𝑅𝑛)) = -((1 / (𝑛 · (𝑛 + 1))) · (𝑅𝑛)))
18298, 112mulcld 11272 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 · 1) ∈ ℂ)
18398, 131mulcld 11272 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 · (𝑛 + 1)) ∈ ℂ)
184176nnne0d 12300 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 · (𝑛 + 1)) ≠ 0)
185131, 182, 183, 184divsubdird 12067 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑛 + 1) − (𝑛 · 1)) / (𝑛 · (𝑛 + 1))) = (((𝑛 + 1) / (𝑛 · (𝑛 + 1))) − ((𝑛 · 1) / (𝑛 · (𝑛 + 1)))))
18698mulridd 11269 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 · 1) = 𝑛)
187186oveq2d 7442 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) − (𝑛 · 1)) = ((𝑛 + 1) − 𝑛))
188187, 134eqtrd 2768 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) − (𝑛 · 1)) = 1)
189188oveq1d 7441 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑛 + 1) − (𝑛 · 1)) / (𝑛 · (𝑛 + 1))) = (1 / (𝑛 · (𝑛 + 1))))
190131mulridd 11269 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) · 1) = (𝑛 + 1))
191131, 98mulcomd 11273 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) · 𝑛) = (𝑛 · (𝑛 + 1)))
192190, 191oveq12d 7444 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑛 + 1) · 1) / ((𝑛 + 1) · 𝑛)) = ((𝑛 + 1) / (𝑛 · (𝑛 + 1))))
19397, 39syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 + 1) ∈ ℕ)
194193nnne0d 12300 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 + 1) ≠ 0)
195112, 98, 131, 142, 194divcan5d 12054 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑛 + 1) · 1) / ((𝑛 + 1) · 𝑛)) = (1 / 𝑛))
196192, 195eqtr3d 2770 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) / (𝑛 · (𝑛 + 1))) = (1 / 𝑛))
197112, 131, 98, 194, 142divcan5d 12054 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 · 1) / (𝑛 · (𝑛 + 1))) = (1 / (𝑛 + 1)))
198196, 197oveq12d 7444 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑛 + 1) / (𝑛 · (𝑛 + 1))) − ((𝑛 · 1) / (𝑛 · (𝑛 + 1)))) = ((1 / 𝑛) − (1 / (𝑛 + 1))))
199185, 189, 1983eqtr3d 2776 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / (𝑛 · (𝑛 + 1))) = ((1 / 𝑛) − (1 / (𝑛 + 1))))
200199negeqd 11492 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → -(1 / (𝑛 · (𝑛 + 1))) = -((1 / 𝑛) − (1 / (𝑛 + 1))))
20197nnrecred 12301 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / 𝑛) ∈ ℝ)
202201recnd 11280 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / 𝑛) ∈ ℂ)
203193nnrecred 12301 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / (𝑛 + 1)) ∈ ℝ)
204203recnd 11280 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / (𝑛 + 1)) ∈ ℂ)
205202, 204negsubdi2d 11625 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → -((1 / 𝑛) − (1 / (𝑛 + 1))) = ((1 / (𝑛 + 1)) − (1 / 𝑛)))
206200, 205eqtr2d 2769 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 / (𝑛 + 1)) − (1 / 𝑛)) = -(1 / (𝑛 · (𝑛 + 1))))
20797nnrpd 13054 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ+)
208100, 207eqeltrd 2829 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) − 1) ∈ ℝ+)
20935pntrval 27515 . . . . . . . . . . . . . . . 16 (((𝑛 + 1) − 1) ∈ ℝ+ → (𝑅‘((𝑛 + 1) − 1)) = ((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1)))
210208, 209syl 17 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘((𝑛 + 1) − 1)) = ((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1)))
211100fveq2d 6906 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘((𝑛 + 1) − 1)) = (𝑅𝑛))
212210, 211eqtr3d 2770 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1)) = (𝑅𝑛))
213206, 212oveq12d 7444 . . . . . . . . . . . . 13 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((1 / (𝑛 + 1)) − (1 / 𝑛)) · ((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1))) = (-(1 / (𝑛 · (𝑛 + 1))) · (𝑅𝑛)))
214180, 183, 184divrec2d 12032 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑅𝑛) / (𝑛 · (𝑛 + 1))) = ((1 / (𝑛 · (𝑛 + 1))) · (𝑅𝑛)))
215214negeqd 11492 . . . . . . . . . . . . 13 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → -((𝑅𝑛) / (𝑛 · (𝑛 + 1))) = -((1 / (𝑛 · (𝑛 + 1))) · (𝑅𝑛)))
216181, 213, 2153eqtr4d 2778 . . . . . . . . . . . 12 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((1 / (𝑛 + 1)) − (1 / 𝑛)) · ((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1))) = -((𝑅𝑛) / (𝑛 · (𝑛 + 1))))
21796, 216sumeq12rdv 15693 . . . . . . . . . . 11 (𝑥 ∈ (1[,)+∞) → Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))(((1 / (𝑛 + 1)) − (1 / 𝑛)) · ((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1))) = Σ𝑛 ∈ (1...(⌊‘𝑥))-((𝑅𝑛) / (𝑛 · (𝑛 + 1))))
218 fzfid 13978 . . . . . . . . . . . 12 (𝑥 ∈ (1[,)+∞) → (1...(⌊‘𝑥)) ∈ Fin)
21997, 42syl 17 . . . . . . . . . . . . 13 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑅𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ)
220219recnd 11280 . . . . . . . . . . . 12 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑅𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ)
221218, 220fsumneg 15773 . . . . . . . . . . 11 (𝑥 ∈ (1[,)+∞) → Σ𝑛 ∈ (1...(⌊‘𝑥))-((𝑅𝑛) / (𝑛 · (𝑛 + 1))) = -Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1))))
222217, 221eqtrd 2768 . . . . . . . . . 10 (𝑥 ∈ (1[,)+∞) → Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))(((1 / (𝑛 + 1)) − (1 / 𝑛)) · ((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1))) = -Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1))))
223175, 222oveq12d 7444 . . . . . . . . 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 2776 . . . . . . . 8 (𝑥 ∈ (1[,)+∞) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) = (((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) − -Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))))
22530, 46subnegd 11616 . . . . . . . 8 (𝑥 ∈ (1[,)+∞) → (((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) − -Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) = (((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) + Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))))
226224, 225eqtrd 2768 . . . . . . 7 (𝑥 ∈ (1[,)+∞) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) = (((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) + Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))))
22730, 46, 226mvrladdd 11665 . . . . . 6 (𝑥 ∈ (1[,)+∞) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) − ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1)) = Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1))))
228227mpteq2ia 5255 . . . . 5 (𝑥 ∈ (1[,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) − ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1))) = (𝑥 ∈ (1[,)+∞) ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1))))
229 fzfid 13978 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ ℝ+) → (1...(⌊‘𝑥)) ∈ Fin)
23032adantl 480 . . . . . . . . . . 11 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
231230, 115syl 17 . . . . . . . . . 10 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈ ℝ)
232231, 139syl 17 . . . . . . . . 9 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) − 1) ∈ ℝ)
233232, 230nndivred 12304 . . . . . . . 8 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) − 1) / 𝑛) ∈ ℝ)
234229, 233fsumrecl 15720 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) ∈ ℝ)
235 rpre 13022 . . . . . . . . . . . 12 (𝑥 ∈ ℝ+𝑥 ∈ ℝ)
236235adantl 480 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ)
237236, 17syl 17 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℝ+) → (ψ‘𝑥) ∈ ℝ)
238237, 19syl 17 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((ψ‘𝑥) + 1) ∈ ℝ)
239 rprege0 13029 . . . . . . . . . . . 12 (𝑥 ∈ ℝ+ → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
240239, 22syl 17 . . . . . . . . . . 11 (𝑥 ∈ ℝ+ → (⌊‘𝑥) ∈ ℕ0)
241240adantl 480 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℝ+) → (⌊‘𝑥) ∈ ℕ0)
242241, 24syl 17 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((⌊‘𝑥) + 1) ∈ ℕ)
243238, 242nndivred 12304 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ∈ ℝ)
244 peano2rem 11565 . . . . . . . 8 ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ∈ ℝ → ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) ∈ ℝ)
245243, 244syl 17 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) ∈ ℝ)
246 reex 11237 . . . . . . . . . . . 12 ℝ ∈ V
247246, 14ssexi 5326 . . . . . . . . . . 11 + ∈ V
248247a1i 11 . . . . . . . . . 10 (⊤ → ℝ+ ∈ V)
249231, 230nndivred 12304 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) / 𝑛) ∈ ℝ)
250249recnd 11280 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) / 𝑛) ∈ ℂ)
251229, 250fsumcl 15719 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ∈ ℂ)
252 relogcl 26529 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ+ → (log‘𝑥) ∈ ℝ)
253252adantl 480 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℝ)
254253recnd 11280 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℂ)
255251, 254subcld 11609 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) ∈ ℂ)
256230nnrecred 12301 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / 𝑛) ∈ ℝ)
257229, 256fsumrecl 15720 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) ∈ ℝ)
258257, 253resubcld 11680 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)) ∈ ℝ)
259 eqidd 2729 . . . . . . . . . 10 (⊤ → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) = (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))))
260 eqidd 2729 . . . . . . . . . 10 (⊤ → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) = (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))))
261248, 255, 258, 259, 260offval2 7711 . . . . . . . . 9 (⊤ → ((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘f − (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)))) = (𝑥 ∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)))))
262256recnd 11280 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / 𝑛) ∈ ℂ)
263229, 250, 262fsumsub 15774 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) − (1 / 𝑛)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛)))
264231recnd 11280 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈ ℂ)
265 1cnd 11247 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℂ)
266230nncnd 12266 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℂ)
267230nnne0d 12300 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ≠ 0)
268264, 265, 266, 267divsubdird 12067 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) − 1) / 𝑛) = (((Λ‘𝑛) / 𝑛) − (1 / 𝑛)))
269268sumeq2dv 15689 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) − (1 / 𝑛)))
270257recnd 11280 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) ∈ ℂ)
271251, 270, 254nnncan2d 11644 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛)))
272263, 269, 2713eqtr4rd 2779 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛))
273272mpteq2dva 5252 . . . . . . . . 9 (⊤ → (𝑥 ∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)))) = (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛)))
274261, 273eqtrd 2768 . . . . . . . 8 (⊤ → ((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘f − (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)))) = (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛)))
275 vmadivsum 27435 . . . . . . . . 9 (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1)
27614a1i 11 . . . . . . . . . 10 (⊤ → ℝ+ ⊆ ℝ)
277258recnd 11280 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)) ∈ ℂ)
278 1red 11253 . . . . . . . . . 10 (⊤ → 1 ∈ ℝ)
279 harmoniclbnd 26961 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ+ → (log‘𝑥) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛))
280279adantl 480 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℝ+) → (log‘𝑥) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛))
281253, 257, 280abssubge0d 15418 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)))
282281adantrr 715 . . . . . . . . . . 11 ((⊤ ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)))
283235ad2antrl 726 . . . . . . . . . . . . 13 ((⊤ ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ)
284 simprr 771 . . . . . . . . . . . . 13 ((⊤ ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ≤ 𝑥)
285 harmonicubnd 26962 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) ≤ ((log‘𝑥) + 1))
286283, 284, 285syl2anc 582 . . . . . . . . . . . 12 ((⊤ ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) ≤ ((log‘𝑥) + 1))
287 1red 11253 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ ℝ+) → 1 ∈ ℝ)
288257, 253, 287lesubadd2d 11851 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)) ≤ 1 ↔ Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) ≤ ((log‘𝑥) + 1)))
289288adantrr 715 . . . . . . . . . . . 12 ((⊤ ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)) ≤ 1 ↔ Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) ≤ ((log‘𝑥) + 1)))
290286, 289mpbird 256 . . . . . . . . . . 11 ((⊤ ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)) ≤ 1)
291282, 290eqbrtrd 5174 . . . . . . . . . 10 ((⊤ ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) ≤ 1)
292276, 277, 278, 278, 291elo1d 15520 . . . . . . . . 9 (⊤ → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) ∈ 𝑂(1))
293 o1sub 15600 . . . . . . . . 9 (((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1) ∧ (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) ∈ 𝑂(1)) → ((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘f − (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)))) ∈ 𝑂(1))
294275, 292, 293sylancr 585 . . . . . . . 8 (⊤ → ((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘f − (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)))) ∈ 𝑂(1))
295274, 294eqeltrrd 2830 . . . . . . 7 (⊤ → (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛)) ∈ 𝑂(1))
296243recnd 11280 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ∈ ℂ)
297 1cnd 11247 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ ℝ+) → 1 ∈ ℂ)
298237recnd 11280 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → (ψ‘𝑥) ∈ ℂ)
299 rpcnne0 13032 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ+ → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
300299adantl 480 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
301 divdir 11935 . . . . . . . . . . . 12 (((ψ‘𝑥) ∈ ℂ ∧ 1 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → (((ψ‘𝑥) + 1) / 𝑥) = (((ψ‘𝑥) / 𝑥) + (1 / 𝑥)))
302298, 297, 300, 301syl3anc 1368 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) + 1) / 𝑥) = (((ψ‘𝑥) / 𝑥) + (1 / 𝑥)))
303302mpteq2dva 5252 . . . . . . . . . 10 (⊤ → (𝑥 ∈ ℝ+ ↦ (((ψ‘𝑥) + 1) / 𝑥)) = (𝑥 ∈ ℝ+ ↦ (((ψ‘𝑥) / 𝑥) + (1 / 𝑥))))
304 simpr 483 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ+)
305237, 304rerpdivcld 13087 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((ψ‘𝑥) / 𝑥) ∈ ℝ)
306 rpreccl 13040 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ+ → (1 / 𝑥) ∈ ℝ+)
307306adantl 480 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → (1 / 𝑥) ∈ ℝ+)
308 eqidd 2729 . . . . . . . . . . . 12 (⊤ → (𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) = (𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)))
309 eqidd 2729 . . . . . . . . . . . 12 (⊤ → (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) = (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)))
310248, 305, 307, 308, 309offval2 7711 . . . . . . . . . . 11 (⊤ → ((𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∘f + (𝑥 ∈ ℝ+ ↦ (1 / 𝑥))) = (𝑥 ∈ ℝ+ ↦ (((ψ‘𝑥) / 𝑥) + (1 / 𝑥))))
311 chpo1ub 27433 . . . . . . . . . . . 12 (𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∈ 𝑂(1)
312 divrcnv 15838 . . . . . . . . . . . . . 14 (1 ∈ ℂ → (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) ⇝𝑟 0)
31328, 312ax-mp 5 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) ⇝𝑟 0
314 rlimo1 15601 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) ⇝𝑟 0 → (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) ∈ 𝑂(1))
315313, 314mp1i 13 . . . . . . . . . . . 12 (⊤ → (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) ∈ 𝑂(1))
316 o1add 15598 . . . . . . . . . . . 12 (((𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∈ 𝑂(1) ∧ (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) ∈ 𝑂(1)) → ((𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∘f + (𝑥 ∈ ℝ+ ↦ (1 / 𝑥))) ∈ 𝑂(1))
317311, 315, 316sylancr 585 . . . . . . . . . . 11 (⊤ → ((𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∘f + (𝑥 ∈ ℝ+ ↦ (1 / 𝑥))) ∈ 𝑂(1))
318310, 317eqeltrrd 2830 . . . . . . . . . 10 (⊤ → (𝑥 ∈ ℝ+ ↦ (((ψ‘𝑥) / 𝑥) + (1 / 𝑥))) ∈ 𝑂(1))
319303, 318eqeltrd 2829 . . . . . . . . 9 (⊤ → (𝑥 ∈ ℝ+ ↦ (((ψ‘𝑥) + 1) / 𝑥)) ∈ 𝑂(1))
320238, 304rerpdivcld 13087 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) + 1) / 𝑥) ∈ ℝ)
321 chpge0 27078 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℝ → 0 ≤ (ψ‘𝑥))
322236, 321syl 17 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑥 ∈ ℝ+) → 0 ≤ (ψ‘𝑥))
323237, 322ge0p1rpd 13086 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((ψ‘𝑥) + 1) ∈ ℝ+)
324323rprege0d 13063 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) + 1) ∈ ℝ ∧ 0 ≤ ((ψ‘𝑥) + 1)))
325242nnrpd 13054 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((⌊‘𝑥) + 1) ∈ ℝ+)
326325rpregt0d 13062 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((⌊‘𝑥) + 1) ∈ ℝ ∧ 0 < ((⌊‘𝑥) + 1)))
327 divge0 12121 . . . . . . . . . . . . 13 (((((ψ‘𝑥) + 1) ∈ ℝ ∧ 0 ≤ ((ψ‘𝑥) + 1)) ∧ (((⌊‘𝑥) + 1) ∈ ℝ ∧ 0 < ((⌊‘𝑥) + 1))) → 0 ≤ (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)))
328324, 326, 327syl2anc 582 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → 0 ≤ (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)))
329243, 328absidd 15409 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → (abs‘(((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1))) = (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)))
330320recnd 11280 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) + 1) / 𝑥) ∈ ℂ)
331330abscld 15423 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → (abs‘(((ψ‘𝑥) + 1) / 𝑥)) ∈ ℝ)
332 fllep1 13806 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → 𝑥 ≤ ((⌊‘𝑥) + 1))
333236, 332syl 17 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℝ+) → 𝑥 ≤ ((⌊‘𝑥) + 1))
334 rpregt0 13028 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ+ → (𝑥 ∈ ℝ ∧ 0 < 𝑥))
335334adantl 480 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ ℝ+) → (𝑥 ∈ ℝ ∧ 0 < 𝑥))
336323rpregt0d 13062 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) + 1) ∈ ℝ ∧ 0 < ((ψ‘𝑥) + 1)))
337 lediv2 12142 . . . . . . . . . . . . . 14 (((𝑥 ∈ ℝ ∧ 0 < 𝑥) ∧ (((⌊‘𝑥) + 1) ∈ ℝ ∧ 0 < ((⌊‘𝑥) + 1)) ∧ (((ψ‘𝑥) + 1) ∈ ℝ ∧ 0 < ((ψ‘𝑥) + 1))) → (𝑥 ≤ ((⌊‘𝑥) + 1) ↔ (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ≤ (((ψ‘𝑥) + 1) / 𝑥)))
338335, 326, 336, 337syl3anc 1368 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℝ+) → (𝑥 ≤ ((⌊‘𝑥) + 1) ↔ (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ≤ (((ψ‘𝑥) + 1) / 𝑥)))
339333, 338mpbid 231 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ≤ (((ψ‘𝑥) + 1) / 𝑥))
340320leabsd 15401 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) + 1) / 𝑥) ≤ (abs‘(((ψ‘𝑥) + 1) / 𝑥)))
341243, 320, 331, 339, 340letrd 11409 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ≤ (abs‘(((ψ‘𝑥) + 1) / 𝑥)))
342329, 341eqbrtrd 5174 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℝ+) → (abs‘(((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1))) ≤ (abs‘(((ψ‘𝑥) + 1) / 𝑥)))
343342adantrr 715 . . . . . . . . 9 ((⊤ ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1))) ≤ (abs‘(((ψ‘𝑥) + 1) / 𝑥)))
344278, 319, 320, 296, 343o1le 15639 . . . . . . . 8 (⊤ → (𝑥 ∈ ℝ+ ↦ (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1))) ∈ 𝑂(1))
345 o1const 15604 . . . . . . . . . 10 ((ℝ+ ⊆ ℝ ∧ 1 ∈ ℂ) → (𝑥 ∈ ℝ+ ↦ 1) ∈ 𝑂(1))
34614, 28, 345mp2an 690 . . . . . . . . 9 (𝑥 ∈ ℝ+ ↦ 1) ∈ 𝑂(1)
347346a1i 11 . . . . . . . 8 (⊤ → (𝑥 ∈ ℝ+ ↦ 1) ∈ 𝑂(1))
348296, 297, 344, 347o1sub2 15610 . . . . . . 7 (⊤ → (𝑥 ∈ ℝ+ ↦ ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1)) ∈ 𝑂(1))
349234, 245, 295, 348o1sub2 15610 . . . . . 6 (⊤ → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) − ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1))) ∈ 𝑂(1))
35013, 349o1res2 15547 . . . . 5 (⊤ → (𝑥 ∈ (1[,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) − ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1))) ∈ 𝑂(1))
351228, 350eqeltrrid 2834 . . . 4 (⊤ → (𝑥 ∈ (1[,)+∞) ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) ∈ 𝑂(1))
35216, 351eqeltrd 2829 . . 3 (⊤ → ((𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) ↾ (1[,)+∞)) ∈ 𝑂(1))
353 eqid 2728 . . . . . 6 (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) = (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1))))
354353, 45fmpti 7127 . . . . 5 (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))):ℝ⟶ℂ
355354a1i 11 . . . 4 (⊤ → (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))):ℝ⟶ℂ)
356 ssidd 4005 . . . 4 (⊤ → ℝ ⊆ ℝ)
357355, 356, 278o1resb 15550 . . 3 (⊤ → ((𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) ∈ 𝑂(1) ↔ ((𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) ↾ (1[,)+∞)) ∈ 𝑂(1)))
358352, 357mpbird 256 . 2 (⊤ → (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) ∈ 𝑂(1))
359358mptru 1540 1 (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) ∈ 𝑂(1)
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 394   = wceq 1533  wtru 1534  wcel 2098  wne 2937  Vcvv 3473  wss 3949   class class class wbr 5152  cmpt 5235  cres 5684  wf 6549  cfv 6553  (class class class)co 7426  f cof 7689  cc 11144  cr 11145  0cc0 11146  1c1 11147   + caddc 11149   · cmul 11151  +∞cpnf 11283   < clt 11286  cle 11287  cmin 11482  -cneg 11483   / cdiv 11909  cn 12250  2c2 12305  0cn0 12510  cz 12596  cuz 12860  +crp 13014  [,)cico 13366  ...cfz 13524  ..^cfzo 13667  cfl 13795  abscabs 15221  𝑟 crli 15469  𝑂(1)co1 15470  Σcsu 15672  logclog 26508  Λcvma 27044  ψcchp 27045
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-rep 5289  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-inf2 9672  ax-cnex 11202  ax-resscn 11203  ax-1cn 11204  ax-icn 11205  ax-addcl 11206  ax-addrcl 11207  ax-mulcl 11208  ax-mulrcl 11209  ax-mulcom 11210  ax-addass 11211  ax-mulass 11212  ax-distr 11213  ax-i2m1 11214  ax-1ne0 11215  ax-1rid 11216  ax-rnegex 11217  ax-rrecex 11218  ax-cnre 11219  ax-pre-lttri 11220  ax-pre-lttrn 11221  ax-pre-ltadd 11222  ax-pre-mulgt0 11223  ax-pre-sup 11224  ax-addf 11225
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-tp 4637  df-op 4639  df-uni 4913  df-int 4954  df-iun 5002  df-iin 5003  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-se 5638  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6310  df-ord 6377  df-on 6378  df-lim 6379  df-suc 6380  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-isom 6562  df-riota 7382  df-ov 7429  df-oprab 7430  df-mpo 7431  df-of 7691  df-om 7877  df-1st 7999  df-2nd 8000  df-supp 8172  df-frecs 8293  df-wrecs 8324  df-recs 8398  df-rdg 8437  df-1o 8493  df-2o 8494  df-oadd 8497  df-er 8731  df-map 8853  df-pm 8854  df-ixp 8923  df-en 8971  df-dom 8972  df-sdom 8973  df-fin 8974  df-fsupp 9394  df-fi 9442  df-sup 9473  df-inf 9474  df-oi 9541  df-dju 9932  df-card 9970  df-pnf 11288  df-mnf 11289  df-xr 11290  df-ltxr 11291  df-le 11292  df-sub 11484  df-neg 11485  df-div 11910  df-nn 12251  df-2 12313  df-3 12314  df-4 12315  df-5 12316  df-6 12317  df-7 12318  df-8 12319  df-9 12320  df-n0 12511  df-xnn0 12583  df-z 12597  df-dec 12716  df-uz 12861  df-q 12971  df-rp 13015  df-xneg 13132  df-xadd 13133  df-xmul 13134  df-ioo 13368  df-ioc 13369  df-ico 13370  df-icc 13371  df-fz 13525  df-fzo 13668  df-fl 13797  df-mod 13875  df-seq 14007  df-exp 14067  df-fac 14273  df-bc 14302  df-hash 14330  df-shft 15054  df-cj 15086  df-re 15087  df-im 15088  df-sqrt 15222  df-abs 15223  df-limsup 15455  df-clim 15472  df-rlim 15473  df-o1 15474  df-lo1 15475  df-sum 15673  df-ef 16051  df-e 16052  df-sin 16053  df-cos 16054  df-tan 16055  df-pi 16056  df-dvds 16239  df-gcd 16477  df-prm 16650  df-pc 16813  df-struct 17123  df-sets 17140  df-slot 17158  df-ndx 17170  df-base 17188  df-ress 17217  df-plusg 17253  df-mulr 17254  df-starv 17255  df-sca 17256  df-vsca 17257  df-ip 17258  df-tset 17259  df-ple 17260  df-ds 17262  df-unif 17263  df-hom 17264  df-cco 17265  df-rest 17411  df-topn 17412  df-0g 17430  df-gsum 17431  df-topgen 17432  df-pt 17433  df-prds 17436  df-xrs 17491  df-qtop 17496  df-imas 17497  df-xps 17499  df-mre 17573  df-mrc 17574  df-acs 17576  df-mgm 18607  df-sgrp 18686  df-mnd 18702  df-submnd 18748  df-mulg 19031  df-cntz 19275  df-cmn 19744  df-psmet 21278  df-xmet 21279  df-met 21280  df-bl 21281  df-mopn 21282  df-fbas 21283  df-fg 21284  df-cnfld 21287  df-top 22816  df-topon 22833  df-topsp 22855  df-bases 22869  df-cld 22943  df-ntr 22944  df-cls 22945  df-nei 23022  df-lp 23060  df-perf 23061  df-cn 23151  df-cnp 23152  df-haus 23239  df-cmp 23311  df-tx 23486  df-hmeo 23679  df-fil 23770  df-fm 23862  df-flim 23863  df-flf 23864  df-xms 24246  df-ms 24247  df-tms 24248  df-cncf 24818  df-limc 25815  df-dv 25816  df-ulm 26333  df-log 26510  df-cxp 26511  df-atan 26819  df-em 26945  df-cht 27049  df-vma 27050  df-chp 27051  df-ppi 27052
This theorem is referenced by:  pntrsumbnd  27519
  Copyright terms: Public domain W3C validator