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

Theorem pntrsumo1 26145
 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 10633 . . . . . . . . . . 11 1 ∈ ℝ
2 elicopnf 12828 . . . . . . . . . . 11 (1 ∈ ℝ → (𝑥 ∈ (1[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 1 ≤ 𝑥)))
31, 2ax-mp 5 . . . . . . . . . 10 (𝑥 ∈ (1[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 1 ≤ 𝑥))
43simplbi 501 . . . . . . . . 9 (𝑥 ∈ (1[,)+∞) → 𝑥 ∈ ℝ)
5 0red 10636 . . . . . . . . . 10 (𝑥 ∈ (1[,)+∞) → 0 ∈ ℝ)
6 1red 10634 . . . . . . . . . 10 (𝑥 ∈ (1[,)+∞) → 1 ∈ ℝ)
7 0lt1 11154 . . . . . . . . . . 11 0 < 1
87a1i 11 . . . . . . . . . 10 (𝑥 ∈ (1[,)+∞) → 0 < 1)
93simprbi 500 . . . . . . . . . 10 (𝑥 ∈ (1[,)+∞) → 1 ≤ 𝑥)
105, 6, 4, 8, 9ltletrd 10792 . . . . . . . . 9 (𝑥 ∈ (1[,)+∞) → 0 < 𝑥)
114, 10elrpd 12421 . . . . . . . 8 (𝑥 ∈ (1[,)+∞) → 𝑥 ∈ ℝ+)
1211ssriv 3956 . . . . . . 7 (1[,)+∞) ⊆ ℝ+
1312a1i 11 . . . . . 6 (⊤ → (1[,)+∞) ⊆ ℝ+)
14 rpssre 12389 . . . . . 6 + ⊆ ℝ
1513, 14sstrdi 3964 . . . . 5 (⊤ → (1[,)+∞) ⊆ ℝ)
1615resmptd 5895 . . . 4 (⊤ → ((𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) ↾ (1[,)+∞)) = (𝑥 ∈ (1[,)+∞) ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))))
17 chpcl 25705 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → (ψ‘𝑥) ∈ ℝ)
184, 17syl 17 . . . . . . . . . . 11 (𝑥 ∈ (1[,)+∞) → (ψ‘𝑥) ∈ ℝ)
19 peano2re 10805 . . . . . . . . . . 11 ((ψ‘𝑥) ∈ ℝ → ((ψ‘𝑥) + 1) ∈ ℝ)
2018, 19syl 17 . . . . . . . . . 10 (𝑥 ∈ (1[,)+∞) → ((ψ‘𝑥) + 1) ∈ ℝ)
2111rprege0d 12431 . . . . . . . . . . . 12 (𝑥 ∈ (1[,)+∞) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
22 flge0nn0 13190 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → (⌊‘𝑥) ∈ ℕ0)
2321, 22syl 17 . . . . . . . . . . 11 (𝑥 ∈ (1[,)+∞) → (⌊‘𝑥) ∈ ℕ0)
24 nn0p1nn 11929 . . . . . . . . . . 11 ((⌊‘𝑥) ∈ ℕ0 → ((⌊‘𝑥) + 1) ∈ ℕ)
2523, 24syl 17 . . . . . . . . . 10 (𝑥 ∈ (1[,)+∞) → ((⌊‘𝑥) + 1) ∈ ℕ)
2620, 25nndivred 11684 . . . . . . . . 9 (𝑥 ∈ (1[,)+∞) → (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ∈ ℝ)
2726recnd 10661 . . . . . . . 8 (𝑥 ∈ (1[,)+∞) → (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ∈ ℂ)
28 ax-1cn 10587 . . . . . . . 8 1 ∈ ℂ
29 subcl 10877 . . . . . . . 8 (((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ∈ ℂ ∧ 1 ∈ ℂ) → ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) ∈ ℂ)
3027, 28, 29sylancl 589 . . . . . . 7 (𝑥 ∈ (1[,)+∞) → ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) ∈ ℂ)
31 fzfid 13341 . . . . . . . . . 10 (𝑥 ∈ ℝ → (1...(⌊‘𝑥)) ∈ Fin)
32 elfznn 12936 . . . . . . . . . . . 12 (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
3332adantl 485 . . . . . . . . . . 11 ((𝑥 ∈ ℝ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
34 nnrp 12393 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → 𝑛 ∈ ℝ+)
35 pntrval.r . . . . . . . . . . . . . . 15 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))
3635pntrf 26143 . . . . . . . . . . . . . 14 𝑅:ℝ+⟶ℝ
3736ffvelrni 6838 . . . . . . . . . . . . 13 (𝑛 ∈ ℝ+ → (𝑅𝑛) ∈ ℝ)
3834, 37syl 17 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → (𝑅𝑛) ∈ ℝ)
39 peano2nn 11642 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℕ)
40 nnmulcl 11654 . . . . . . . . . . . . 13 ((𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ ℕ) → (𝑛 · (𝑛 + 1)) ∈ ℕ)
4139, 40mpdan 686 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → (𝑛 · (𝑛 + 1)) ∈ ℕ)
4238, 41nndivred 11684 . . . . . . . . . . 11 (𝑛 ∈ ℕ → ((𝑅𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ)
4333, 42syl 17 . . . . . . . . . 10 ((𝑥 ∈ ℝ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑅𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ)
4431, 43fsumrecl 15087 . . . . . . . . 9 (𝑥 ∈ ℝ → Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ)
4544recnd 10661 . . . . . . . 8 (𝑥 ∈ ℝ → Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ)
464, 45syl 17 . . . . . . 7 (𝑥 ∈ (1[,)+∞) → Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ)
47 oveq2 7153 . . . . . . . . . . 11 (𝑚 = 𝑛 → (1 / 𝑚) = (1 / 𝑛))
48 fvoveq1 7168 . . . . . . . . . . . 12 (𝑚 = 𝑛 → (ψ‘(𝑚 − 1)) = (ψ‘(𝑛 − 1)))
49 oveq1 7152 . . . . . . . . . . . 12 (𝑚 = 𝑛 → (𝑚 − 1) = (𝑛 − 1))
5048, 49oveq12d 7163 . . . . . . . . . . 11 (𝑚 = 𝑛 → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = ((ψ‘(𝑛 − 1)) − (𝑛 − 1)))
5147, 50jca 515 . . . . . . . . . 10 (𝑚 = 𝑛 → ((1 / 𝑚) = (1 / 𝑛) ∧ ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = ((ψ‘(𝑛 − 1)) − (𝑛 − 1))))
52 oveq2 7153 . . . . . . . . . . 11 (𝑚 = (𝑛 + 1) → (1 / 𝑚) = (1 / (𝑛 + 1)))
53 fvoveq1 7168 . . . . . . . . . . . 12 (𝑚 = (𝑛 + 1) → (ψ‘(𝑚 − 1)) = (ψ‘((𝑛 + 1) − 1)))
54 oveq1 7152 . . . . . . . . . . . 12 (𝑚 = (𝑛 + 1) → (𝑚 − 1) = ((𝑛 + 1) − 1))
5553, 54oveq12d 7163 . . . . . . . . . . 11 (𝑚 = (𝑛 + 1) → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = ((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1)))
5652, 55jca 515 . . . . . . . . . 10 (𝑚 = (𝑛 + 1) → ((1 / 𝑚) = (1 / (𝑛 + 1)) ∧ ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = ((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1))))
57 oveq2 7153 . . . . . . . . . . . 12 (𝑚 = 1 → (1 / 𝑚) = (1 / 1))
58 1div1e1 11322 . . . . . . . . . . . 12 (1 / 1) = 1
5957, 58syl6eq 2875 . . . . . . . . . . 11 (𝑚 = 1 → (1 / 𝑚) = 1)
60 oveq1 7152 . . . . . . . . . . . . . . . 16 (𝑚 = 1 → (𝑚 − 1) = (1 − 1))
61 1m1e0 11702 . . . . . . . . . . . . . . . 16 (1 − 1) = 0
6260, 61syl6eq 2875 . . . . . . . . . . . . . . 15 (𝑚 = 1 → (𝑚 − 1) = 0)
6362fveq2d 6662 . . . . . . . . . . . . . 14 (𝑚 = 1 → (ψ‘(𝑚 − 1)) = (ψ‘0))
64 2pos 11733 . . . . . . . . . . . . . . 15 0 < 2
65 0re 10635 . . . . . . . . . . . . . . . 16 0 ∈ ℝ
66 chpeq0 25788 . . . . . . . . . . . . . . . 16 (0 ∈ ℝ → ((ψ‘0) = 0 ↔ 0 < 2))
6765, 66ax-mp 5 . . . . . . . . . . . . . . 15 ((ψ‘0) = 0 ↔ 0 < 2)
6864, 67mpbir 234 . . . . . . . . . . . . . 14 (ψ‘0) = 0
6963, 68syl6eq 2875 . . . . . . . . . . . . 13 (𝑚 = 1 → (ψ‘(𝑚 − 1)) = 0)
7069, 62oveq12d 7163 . . . . . . . . . . . 12 (𝑚 = 1 → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = (0 − 0))
71 0m0e0 11750 . . . . . . . . . . . 12 (0 − 0) = 0
7270, 71syl6eq 2875 . . . . . . . . . . 11 (𝑚 = 1 → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = 0)
7359, 72jca 515 . . . . . . . . . 10 (𝑚 = 1 → ((1 / 𝑚) = 1 ∧ ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = 0))
74 oveq2 7153 . . . . . . . . . . 11 (𝑚 = ((⌊‘𝑥) + 1) → (1 / 𝑚) = (1 / ((⌊‘𝑥) + 1)))
75 fvoveq1 7168 . . . . . . . . . . . 12 (𝑚 = ((⌊‘𝑥) + 1) → (ψ‘(𝑚 − 1)) = (ψ‘(((⌊‘𝑥) + 1) − 1)))
76 oveq1 7152 . . . . . . . . . . . 12 (𝑚 = ((⌊‘𝑥) + 1) → (𝑚 − 1) = (((⌊‘𝑥) + 1) − 1))
7775, 76oveq12d 7163 . . . . . . . . . . 11 (𝑚 = ((⌊‘𝑥) + 1) → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = ((ψ‘(((⌊‘𝑥) + 1) − 1)) − (((⌊‘𝑥) + 1) − 1)))
7874, 77jca 515 . . . . . . . . . 10 (𝑚 = ((⌊‘𝑥) + 1) → ((1 / 𝑚) = (1 / ((⌊‘𝑥) + 1)) ∧ ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = ((ψ‘(((⌊‘𝑥) + 1) − 1)) − (((⌊‘𝑥) + 1) − 1))))
79 nnuz 12274 . . . . . . . . . . 11 ℕ = (ℤ‘1)
8025, 79eleqtrdi 2926 . . . . . . . . . 10 (𝑥 ∈ (1[,)+∞) → ((⌊‘𝑥) + 1) ∈ (ℤ‘1))
81 elfznn 12936 . . . . . . . . . . . . 13 (𝑚 ∈ (1...((⌊‘𝑥) + 1)) → 𝑚 ∈ ℕ)
8281adantl 485 . . . . . . . . . . . 12 ((𝑥 ∈ (1[,)+∞) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 𝑚 ∈ ℕ)
8382nnrecred 11681 . . . . . . . . . . 11 ((𝑥 ∈ (1[,)+∞) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (1 / 𝑚) ∈ ℝ)
8483recnd 10661 . . . . . . . . . 10 ((𝑥 ∈ (1[,)+∞) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (1 / 𝑚) ∈ ℂ)
8582nnred 11645 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 𝑚 ∈ ℝ)
86 peano2rem 10945 . . . . . . . . . . . . . 14 (𝑚 ∈ ℝ → (𝑚 − 1) ∈ ℝ)
8785, 86syl 17 . . . . . . . . . . . . 13 ((𝑥 ∈ (1[,)+∞) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑚 − 1) ∈ ℝ)
88 chpcl 25705 . . . . . . . . . . . . 13 ((𝑚 − 1) ∈ ℝ → (ψ‘(𝑚 − 1)) ∈ ℝ)
8987, 88syl 17 . . . . . . . . . . . 12 ((𝑥 ∈ (1[,)+∞) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (ψ‘(𝑚 − 1)) ∈ ℝ)
9089, 87resubcld 11060 . . . . . . . . . . 11 ((𝑥 ∈ (1[,)+∞) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) ∈ ℝ)
9190recnd 10661 . . . . . . . . . 10 ((𝑥 ∈ (1[,)+∞) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) ∈ ℂ)
9251, 56, 73, 78, 80, 84, 91fsumparts 15157 . . . . . . . . 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 13168 . . . . . . . . . . . 12 (𝑥 ∈ (1[,)+∞) → (⌊‘𝑥) ∈ ℤ)
94 fzval3 13106 . . . . . . . . . . . 12 ((⌊‘𝑥) ∈ ℤ → (1...(⌊‘𝑥)) = (1..^((⌊‘𝑥) + 1)))
9593, 94syl 17 . . . . . . . . . . 11 (𝑥 ∈ (1[,)+∞) → (1...(⌊‘𝑥)) = (1..^((⌊‘𝑥) + 1)))
9695eqcomd 2830 . . . . . . . . . 10 (𝑥 ∈ (1[,)+∞) → (1..^((⌊‘𝑥) + 1)) = (1...(⌊‘𝑥)))
9732adantl 485 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
9897nncnd 11646 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℂ)
99 pncan 10884 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛 + 1) − 1) = 𝑛)
10098, 28, 99sylancl 589 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) − 1) = 𝑛)
10197nnred 11645 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ)
102100, 101eqeltrd 2916 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) − 1) ∈ ℝ)
103 chpcl 25705 . . . . . . . . . . . . . . . 16 (((𝑛 + 1) − 1) ∈ ℝ → (ψ‘((𝑛 + 1) − 1)) ∈ ℝ)
104102, 103syl 17 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (ψ‘((𝑛 + 1) − 1)) ∈ ℝ)
105104recnd 10661 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (ψ‘((𝑛 + 1) − 1)) ∈ ℂ)
106102recnd 10661 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) − 1) ∈ ℂ)
107 peano2rem 10945 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℝ → (𝑛 − 1) ∈ ℝ)
108101, 107syl 17 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 − 1) ∈ ℝ)
109 chpcl 25705 . . . . . . . . . . . . . . . 16 ((𝑛 − 1) ∈ ℝ → (ψ‘(𝑛 − 1)) ∈ ℝ)
110108, 109syl 17 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (ψ‘(𝑛 − 1)) ∈ ℝ)
111110recnd 10661 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (ψ‘(𝑛 − 1)) ∈ ℂ)
112 1cnd 10628 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℂ)
11398, 112subcld 10989 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 − 1) ∈ ℂ)
114105, 106, 111, 113sub4d 11038 . . . . . . . . . . . . 13 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1)) − ((ψ‘(𝑛 − 1)) − (𝑛 − 1))) = (((ψ‘((𝑛 + 1) − 1)) − (ψ‘(𝑛 − 1))) − (((𝑛 + 1) − 1) − (𝑛 − 1))))
115 vmacl 25699 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ → (Λ‘𝑛) ∈ ℝ)
11697, 115syl 17 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈ ℝ)
117116recnd 10661 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈ ℂ)
118 nnm1nn0 11931 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → (𝑛 − 1) ∈ ℕ0)
11997, 118syl 17 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 − 1) ∈ ℕ0)
120 chpp1 25736 . . . . . . . . . . . . . . . . 17 ((𝑛 − 1) ∈ ℕ0 → (ψ‘((𝑛 − 1) + 1)) = ((ψ‘(𝑛 − 1)) + (Λ‘((𝑛 − 1) + 1))))
121119, 120syl 17 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (ψ‘((𝑛 − 1) + 1)) = ((ψ‘(𝑛 − 1)) + (Λ‘((𝑛 − 1) + 1))))
122 npcan 10887 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛 − 1) + 1) = 𝑛)
12398, 28, 122sylancl 589 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 − 1) + 1) = 𝑛)
124123, 100eqtr4d 2862 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 − 1) + 1) = ((𝑛 + 1) − 1))
125124fveq2d 6662 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (ψ‘((𝑛 − 1) + 1)) = (ψ‘((𝑛 + 1) − 1)))
126123fveq2d 6662 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘((𝑛 − 1) + 1)) = (Λ‘𝑛))
127126oveq2d 7161 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((ψ‘(𝑛 − 1)) + (Λ‘((𝑛 − 1) + 1))) = ((ψ‘(𝑛 − 1)) + (Λ‘𝑛)))
128121, 125, 1273eqtr3d 2867 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (ψ‘((𝑛 + 1) − 1)) = ((ψ‘(𝑛 − 1)) + (Λ‘𝑛)))
129111, 117, 128mvrladdd 11045 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((ψ‘((𝑛 + 1) − 1)) − (ψ‘(𝑛 − 1))) = (Λ‘𝑛))
130 peano2cn 10804 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℂ → (𝑛 + 1) ∈ ℂ)
13198, 130syl 17 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 + 1) ∈ ℂ)
132131, 98, 112nnncan2d 11024 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑛 + 1) − 1) − (𝑛 − 1)) = ((𝑛 + 1) − 𝑛))
133 pncan2 10885 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛 + 1) − 𝑛) = 1)
13498, 28, 133sylancl 589 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) − 𝑛) = 1)
135132, 134eqtrd 2859 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑛 + 1) − 1) − (𝑛 − 1)) = 1)
136129, 135oveq12d 7163 . . . . . . . . . . . . 13 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((ψ‘((𝑛 + 1) − 1)) − (ψ‘(𝑛 − 1))) − (((𝑛 + 1) − 1) − (𝑛 − 1))) = ((Λ‘𝑛) − 1))
137114, 136eqtrd 2859 . . . . . . . . . . . 12 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1)) − ((ψ‘(𝑛 − 1)) − (𝑛 − 1))) = ((Λ‘𝑛) − 1))
138137oveq2d 7161 . . . . . . . . . . 11 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 / 𝑛) · (((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1)) − ((ψ‘(𝑛 − 1)) − (𝑛 − 1)))) = ((1 / 𝑛) · ((Λ‘𝑛) − 1)))
139 peano2rem 10945 . . . . . . . . . . . . . 14 ((Λ‘𝑛) ∈ ℝ → ((Λ‘𝑛) − 1) ∈ ℝ)
140116, 139syl 17 . . . . . . . . . . . . 13 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) − 1) ∈ ℝ)
141140recnd 10661 . . . . . . . . . . . 12 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) − 1) ∈ ℂ)
14297nnne0d 11680 . . . . . . . . . . . 12 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ≠ 0)
143141, 98, 142divrec2d 11412 . . . . . . . . . . 11 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) − 1) / 𝑛) = ((1 / 𝑛) · ((Λ‘𝑛) − 1)))
144138, 143eqtr4d 2862 . . . . . . . . . 10 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 / 𝑛) · (((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1)) − ((ψ‘(𝑛 − 1)) − (𝑛 − 1)))) = (((Λ‘𝑛) − 1) / 𝑛))
14596, 144sumeq12rdv 15060 . . . . . . . . 9 (𝑥 ∈ (1[,)+∞) → Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))((1 / 𝑛) · (((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1)) − ((ψ‘(𝑛 − 1)) − (𝑛 − 1)))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛))
14623nn0cnd 11950 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (1[,)+∞) → (⌊‘𝑥) ∈ ℂ)
147 pncan 10884 . . . . . . . . . . . . . . . . . . 19 (((⌊‘𝑥) ∈ ℂ ∧ 1 ∈ ℂ) → (((⌊‘𝑥) + 1) − 1) = (⌊‘𝑥))
148146, 28, 147sylancl 589 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (1[,)+∞) → (((⌊‘𝑥) + 1) − 1) = (⌊‘𝑥))
149148fveq2d 6662 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (1[,)+∞) → (ψ‘(((⌊‘𝑥) + 1) − 1)) = (ψ‘(⌊‘𝑥)))
150 chpfl 25731 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℝ → (ψ‘(⌊‘𝑥)) = (ψ‘𝑥))
1514, 150syl 17 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (1[,)+∞) → (ψ‘(⌊‘𝑥)) = (ψ‘𝑥))
152149, 151eqtrd 2859 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1[,)+∞) → (ψ‘(((⌊‘𝑥) + 1) − 1)) = (ψ‘𝑥))
153152oveq1d 7160 . . . . . . . . . . . . . . 15 (𝑥 ∈ (1[,)+∞) → ((ψ‘(((⌊‘𝑥) + 1) − 1)) − (((⌊‘𝑥) + 1) − 1)) = ((ψ‘𝑥) − (((⌊‘𝑥) + 1) − 1)))
15418recnd 10661 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1[,)+∞) → (ψ‘𝑥) ∈ ℂ)
15525nncnd 11646 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1[,)+∞) → ((⌊‘𝑥) + 1) ∈ ℂ)
156 1cnd 10628 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1[,)+∞) → 1 ∈ ℂ)
157154, 155, 156subsub3d 11019 . . . . . . . . . . . . . . 15 (𝑥 ∈ (1[,)+∞) → ((ψ‘𝑥) − (((⌊‘𝑥) + 1) − 1)) = (((ψ‘𝑥) + 1) − ((⌊‘𝑥) + 1)))
158153, 157eqtrd 2859 . . . . . . . . . . . . . 14 (𝑥 ∈ (1[,)+∞) → ((ψ‘(((⌊‘𝑥) + 1) − 1)) − (((⌊‘𝑥) + 1) − 1)) = (((ψ‘𝑥) + 1) − ((⌊‘𝑥) + 1)))
159158oveq2d 7161 . . . . . . . . . . . . 13 (𝑥 ∈ (1[,)+∞) → ((1 / ((⌊‘𝑥) + 1)) · ((ψ‘(((⌊‘𝑥) + 1) − 1)) − (((⌊‘𝑥) + 1) − 1))) = ((1 / ((⌊‘𝑥) + 1)) · (((ψ‘𝑥) + 1) − ((⌊‘𝑥) + 1))))
16025nnrecred 11681 . . . . . . . . . . . . . . 15 (𝑥 ∈ (1[,)+∞) → (1 / ((⌊‘𝑥) + 1)) ∈ ℝ)
161160recnd 10661 . . . . . . . . . . . . . 14 (𝑥 ∈ (1[,)+∞) → (1 / ((⌊‘𝑥) + 1)) ∈ ℂ)
162 peano2cn 10804 . . . . . . . . . . . . . . 15 ((ψ‘𝑥) ∈ ℂ → ((ψ‘𝑥) + 1) ∈ ℂ)
163154, 162syl 17 . . . . . . . . . . . . . 14 (𝑥 ∈ (1[,)+∞) → ((ψ‘𝑥) + 1) ∈ ℂ)
164161, 163, 155subdid 11088 . . . . . . . . . . . . 13 (𝑥 ∈ (1[,)+∞) → ((1 / ((⌊‘𝑥) + 1)) · (((ψ‘𝑥) + 1) − ((⌊‘𝑥) + 1))) = (((1 / ((⌊‘𝑥) + 1)) · ((ψ‘𝑥) + 1)) − ((1 / ((⌊‘𝑥) + 1)) · ((⌊‘𝑥) + 1))))
16525nnne0d 11680 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1[,)+∞) → ((⌊‘𝑥) + 1) ≠ 0)
166163, 155, 165divrec2d 11412 . . . . . . . . . . . . . . 15 (𝑥 ∈ (1[,)+∞) → (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) = ((1 / ((⌊‘𝑥) + 1)) · ((ψ‘𝑥) + 1)))
167166eqcomd 2830 . . . . . . . . . . . . . 14 (𝑥 ∈ (1[,)+∞) → ((1 / ((⌊‘𝑥) + 1)) · ((ψ‘𝑥) + 1)) = (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)))
168155, 165recid2d 11404 . . . . . . . . . . . . . 14 (𝑥 ∈ (1[,)+∞) → ((1 / ((⌊‘𝑥) + 1)) · ((⌊‘𝑥) + 1)) = 1)
169167, 168oveq12d 7163 . . . . . . . . . . . . 13 (𝑥 ∈ (1[,)+∞) → (((1 / ((⌊‘𝑥) + 1)) · ((ψ‘𝑥) + 1)) − ((1 / ((⌊‘𝑥) + 1)) · ((⌊‘𝑥) + 1))) = ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1))
170159, 164, 1693eqtrd 2863 . . . . . . . . . . . 12 (𝑥 ∈ (1[,)+∞) → ((1 / ((⌊‘𝑥) + 1)) · ((ψ‘(((⌊‘𝑥) + 1) − 1)) − (((⌊‘𝑥) + 1) − 1))) = ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1))
17128mul01i 10822 . . . . . . . . . . . . 13 (1 · 0) = 0
172171a1i 11 . . . . . . . . . . . 12 (𝑥 ∈ (1[,)+∞) → (1 · 0) = 0)
173170, 172oveq12d 7163 . . . . . . . . . . 11 (𝑥 ∈ (1[,)+∞) → (((1 / ((⌊‘𝑥) + 1)) · ((ψ‘(((⌊‘𝑥) + 1) − 1)) − (((⌊‘𝑥) + 1) − 1))) − (1 · 0)) = (((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) − 0))
17430subid1d 10978 . . . . . . . . . . 11 (𝑥 ∈ (1[,)+∞) → (((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) − 0) = ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1))
175173, 174eqtrd 2859 . . . . . . . . . 10 (𝑥 ∈ (1[,)+∞) → (((1 / ((⌊‘𝑥) + 1)) · ((ψ‘(((⌊‘𝑥) + 1) − 1)) − (((⌊‘𝑥) + 1) − 1))) − (1 · 0)) = ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1))
17697, 41syl 17 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 · (𝑛 + 1)) ∈ ℕ)
177176nnrecred 11681 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / (𝑛 · (𝑛 + 1))) ∈ ℝ)
178177recnd 10661 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / (𝑛 · (𝑛 + 1))) ∈ ℂ)
17997, 38syl 17 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅𝑛) ∈ ℝ)
180179recnd 10661 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅𝑛) ∈ ℂ)
181178, 180mulneg1d 11085 . . . . . . . . . . . . 13 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (-(1 / (𝑛 · (𝑛 + 1))) · (𝑅𝑛)) = -((1 / (𝑛 · (𝑛 + 1))) · (𝑅𝑛)))
18298, 112mulcld 10653 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 · 1) ∈ ℂ)
18398, 131mulcld 10653 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 · (𝑛 + 1)) ∈ ℂ)
184176nnne0d 11680 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 · (𝑛 + 1)) ≠ 0)
185131, 182, 183, 184divsubdird 11447 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑛 + 1) − (𝑛 · 1)) / (𝑛 · (𝑛 + 1))) = (((𝑛 + 1) / (𝑛 · (𝑛 + 1))) − ((𝑛 · 1) / (𝑛 · (𝑛 + 1)))))
18698mulid1d 10650 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 · 1) = 𝑛)
187186oveq2d 7161 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) − (𝑛 · 1)) = ((𝑛 + 1) − 𝑛))
188187, 134eqtrd 2859 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) − (𝑛 · 1)) = 1)
189188oveq1d 7160 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑛 + 1) − (𝑛 · 1)) / (𝑛 · (𝑛 + 1))) = (1 / (𝑛 · (𝑛 + 1))))
190131mulid1d 10650 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) · 1) = (𝑛 + 1))
191131, 98mulcomd 10654 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) · 𝑛) = (𝑛 · (𝑛 + 1)))
192190, 191oveq12d 7163 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑛 + 1) · 1) / ((𝑛 + 1) · 𝑛)) = ((𝑛 + 1) / (𝑛 · (𝑛 + 1))))
19397, 39syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 + 1) ∈ ℕ)
194193nnne0d 11680 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 + 1) ≠ 0)
195112, 98, 131, 142, 194divcan5d 11434 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑛 + 1) · 1) / ((𝑛 + 1) · 𝑛)) = (1 / 𝑛))
196192, 195eqtr3d 2861 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) / (𝑛 · (𝑛 + 1))) = (1 / 𝑛))
197112, 131, 98, 194, 142divcan5d 11434 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 · 1) / (𝑛 · (𝑛 + 1))) = (1 / (𝑛 + 1)))
198196, 197oveq12d 7163 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑛 + 1) / (𝑛 · (𝑛 + 1))) − ((𝑛 · 1) / (𝑛 · (𝑛 + 1)))) = ((1 / 𝑛) − (1 / (𝑛 + 1))))
199185, 189, 1983eqtr3d 2867 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / (𝑛 · (𝑛 + 1))) = ((1 / 𝑛) − (1 / (𝑛 + 1))))
200199negeqd 10872 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → -(1 / (𝑛 · (𝑛 + 1))) = -((1 / 𝑛) − (1 / (𝑛 + 1))))
20197nnrecred 11681 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / 𝑛) ∈ ℝ)
202201recnd 10661 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / 𝑛) ∈ ℂ)
203193nnrecred 11681 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / (𝑛 + 1)) ∈ ℝ)
204203recnd 10661 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / (𝑛 + 1)) ∈ ℂ)
205202, 204negsubdi2d 11005 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → -((1 / 𝑛) − (1 / (𝑛 + 1))) = ((1 / (𝑛 + 1)) − (1 / 𝑛)))
206200, 205eqtr2d 2860 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 / (𝑛 + 1)) − (1 / 𝑛)) = -(1 / (𝑛 · (𝑛 + 1))))
20797nnrpd 12422 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ+)
208100, 207eqeltrd 2916 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) − 1) ∈ ℝ+)
20935pntrval 26142 . . . . . . . . . . . . . . . 16 (((𝑛 + 1) − 1) ∈ ℝ+ → (𝑅‘((𝑛 + 1) − 1)) = ((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1)))
210208, 209syl 17 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘((𝑛 + 1) − 1)) = ((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1)))
211100fveq2d 6662 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘((𝑛 + 1) − 1)) = (𝑅𝑛))
212210, 211eqtr3d 2861 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1)) = (𝑅𝑛))
213206, 212oveq12d 7163 . . . . . . . . . . . . 13 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((1 / (𝑛 + 1)) − (1 / 𝑛)) · ((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1))) = (-(1 / (𝑛 · (𝑛 + 1))) · (𝑅𝑛)))
214180, 183, 184divrec2d 11412 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑅𝑛) / (𝑛 · (𝑛 + 1))) = ((1 / (𝑛 · (𝑛 + 1))) · (𝑅𝑛)))
215214negeqd 10872 . . . . . . . . . . . . 13 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → -((𝑅𝑛) / (𝑛 · (𝑛 + 1))) = -((1 / (𝑛 · (𝑛 + 1))) · (𝑅𝑛)))
216181, 213, 2153eqtr4d 2869 . . . . . . . . . . . 12 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((1 / (𝑛 + 1)) − (1 / 𝑛)) · ((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1))) = -((𝑅𝑛) / (𝑛 · (𝑛 + 1))))
21796, 216sumeq12rdv 15060 . . . . . . . . . . 11 (𝑥 ∈ (1[,)+∞) → Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))(((1 / (𝑛 + 1)) − (1 / 𝑛)) · ((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1))) = Σ𝑛 ∈ (1...(⌊‘𝑥))-((𝑅𝑛) / (𝑛 · (𝑛 + 1))))
218 fzfid 13341 . . . . . . . . . . . 12 (𝑥 ∈ (1[,)+∞) → (1...(⌊‘𝑥)) ∈ Fin)
21997, 42syl 17 . . . . . . . . . . . . 13 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑅𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ)
220219recnd 10661 . . . . . . . . . . . 12 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑅𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ)
221218, 220fsumneg 15138 . . . . . . . . . . 11 (𝑥 ∈ (1[,)+∞) → Σ𝑛 ∈ (1...(⌊‘𝑥))-((𝑅𝑛) / (𝑛 · (𝑛 + 1))) = -Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1))))
222217, 221eqtrd 2859 . . . . . . . . . 10 (𝑥 ∈ (1[,)+∞) → Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))(((1 / (𝑛 + 1)) − (1 / 𝑛)) · ((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1))) = -Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1))))
223175, 222oveq12d 7163 . . . . . . . . 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 2867 . . . . . . . 8 (𝑥 ∈ (1[,)+∞) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) = (((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) − -Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))))
22530, 46subnegd 10996 . . . . . . . 8 (𝑥 ∈ (1[,)+∞) → (((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) − -Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) = (((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) + Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))))
226224, 225eqtrd 2859 . . . . . . 7 (𝑥 ∈ (1[,)+∞) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) = (((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) + Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))))
22730, 46, 226mvrladdd 11045 . . . . . 6 (𝑥 ∈ (1[,)+∞) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) − ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1)) = Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1))))
228227mpteq2ia 5143 . . . . 5 (𝑥 ∈ (1[,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) − ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1))) = (𝑥 ∈ (1[,)+∞) ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1))))
229 fzfid 13341 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ ℝ+) → (1...(⌊‘𝑥)) ∈ Fin)
23032adantl 485 . . . . . . . . . . 11 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
231230, 115syl 17 . . . . . . . . . 10 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈ ℝ)
232231, 139syl 17 . . . . . . . . 9 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) − 1) ∈ ℝ)
233232, 230nndivred 11684 . . . . . . . 8 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) − 1) / 𝑛) ∈ ℝ)
234229, 233fsumrecl 15087 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) ∈ ℝ)
235 rpre 12390 . . . . . . . . . . . 12 (𝑥 ∈ ℝ+𝑥 ∈ ℝ)
236235adantl 485 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ)
237236, 17syl 17 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℝ+) → (ψ‘𝑥) ∈ ℝ)
238237, 19syl 17 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((ψ‘𝑥) + 1) ∈ ℝ)
239 rprege0 12397 . . . . . . . . . . . 12 (𝑥 ∈ ℝ+ → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
240239, 22syl 17 . . . . . . . . . . 11 (𝑥 ∈ ℝ+ → (⌊‘𝑥) ∈ ℕ0)
241240adantl 485 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℝ+) → (⌊‘𝑥) ∈ ℕ0)
242241, 24syl 17 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((⌊‘𝑥) + 1) ∈ ℕ)
243238, 242nndivred 11684 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ∈ ℝ)
244 peano2rem 10945 . . . . . . . 8 ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ∈ ℝ → ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) ∈ ℝ)
245243, 244syl 17 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) ∈ ℝ)
246 reex 10620 . . . . . . . . . . . 12 ℝ ∈ V
247246, 14ssexi 5212 . . . . . . . . . . 11 + ∈ V
248247a1i 11 . . . . . . . . . 10 (⊤ → ℝ+ ∈ V)
249231, 230nndivred 11684 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) / 𝑛) ∈ ℝ)
250249recnd 10661 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) / 𝑛) ∈ ℂ)
251229, 250fsumcl 15086 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ∈ ℂ)
252 relogcl 25163 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ+ → (log‘𝑥) ∈ ℝ)
253252adantl 485 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℝ)
254253recnd 10661 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℂ)
255251, 254subcld 10989 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) ∈ ℂ)
256230nnrecred 11681 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / 𝑛) ∈ ℝ)
257229, 256fsumrecl 15087 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) ∈ ℝ)
258257, 253resubcld 11060 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)) ∈ ℝ)
259 eqidd 2825 . . . . . . . . . 10 (⊤ → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) = (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))))
260 eqidd 2825 . . . . . . . . . 10 (⊤ → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) = (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))))
261248, 255, 258, 259, 260offval2 7416 . . . . . . . . 9 (⊤ → ((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘f − (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)))) = (𝑥 ∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)))))
262256recnd 10661 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / 𝑛) ∈ ℂ)
263229, 250, 262fsumsub 15139 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) − (1 / 𝑛)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛)))
264231recnd 10661 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈ ℂ)
265 1cnd 10628 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℂ)
266230nncnd 11646 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℂ)
267230nnne0d 11680 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ≠ 0)
268264, 265, 266, 267divsubdird 11447 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) − 1) / 𝑛) = (((Λ‘𝑛) / 𝑛) − (1 / 𝑛)))
269268sumeq2dv 15056 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) − (1 / 𝑛)))
270257recnd 10661 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) ∈ ℂ)
271251, 270, 254nnncan2d 11024 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛)))
272263, 269, 2713eqtr4rd 2870 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛))
273272mpteq2dva 5147 . . . . . . . . 9 (⊤ → (𝑥 ∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)))) = (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛)))
274261, 273eqtrd 2859 . . . . . . . 8 (⊤ → ((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘f − (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)))) = (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛)))
275 vmadivsum 26062 . . . . . . . . 9 (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1)
27614a1i 11 . . . . . . . . . 10 (⊤ → ℝ+ ⊆ ℝ)
277258recnd 10661 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)) ∈ ℂ)
278 1red 10634 . . . . . . . . . 10 (⊤ → 1 ∈ ℝ)
279 harmoniclbnd 25590 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ+ → (log‘𝑥) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛))
280279adantl 485 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℝ+) → (log‘𝑥) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛))
281253, 257, 280abssubge0d 14787 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)))
282281adantrr 716 . . . . . . . . . . 11 ((⊤ ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)))
283235ad2antrl 727 . . . . . . . . . . . . 13 ((⊤ ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ)
284 simprr 772 . . . . . . . . . . . . 13 ((⊤ ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ≤ 𝑥)
285 harmonicubnd 25591 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) ≤ ((log‘𝑥) + 1))
286283, 284, 285syl2anc 587 . . . . . . . . . . . 12 ((⊤ ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) ≤ ((log‘𝑥) + 1))
287 1red 10634 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ ℝ+) → 1 ∈ ℝ)
288257, 253, 287lesubadd2d 11231 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)) ≤ 1 ↔ Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) ≤ ((log‘𝑥) + 1)))
289288adantrr 716 . . . . . . . . . . . 12 ((⊤ ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)) ≤ 1 ↔ Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) ≤ ((log‘𝑥) + 1)))
290286, 289mpbird 260 . . . . . . . . . . 11 ((⊤ ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)) ≤ 1)
291282, 290eqbrtrd 5074 . . . . . . . . . 10 ((⊤ ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) ≤ 1)
292276, 277, 278, 278, 291elo1d 14889 . . . . . . . . 9 (⊤ → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) ∈ 𝑂(1))
293 o1sub 14968 . . . . . . . . 9 (((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1) ∧ (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) ∈ 𝑂(1)) → ((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘f − (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)))) ∈ 𝑂(1))
294275, 292, 293sylancr 590 . . . . . . . 8 (⊤ → ((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘f − (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)))) ∈ 𝑂(1))
295274, 294eqeltrrd 2917 . . . . . . 7 (⊤ → (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛)) ∈ 𝑂(1))
296243recnd 10661 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ∈ ℂ)
297 1cnd 10628 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ ℝ+) → 1 ∈ ℂ)
298237recnd 10661 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → (ψ‘𝑥) ∈ ℂ)
299 rpcnne0 12400 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ+ → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
300299adantl 485 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
301 divdir 11315 . . . . . . . . . . . 12 (((ψ‘𝑥) ∈ ℂ ∧ 1 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → (((ψ‘𝑥) + 1) / 𝑥) = (((ψ‘𝑥) / 𝑥) + (1 / 𝑥)))
302298, 297, 300, 301syl3anc 1368 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) + 1) / 𝑥) = (((ψ‘𝑥) / 𝑥) + (1 / 𝑥)))
303302mpteq2dva 5147 . . . . . . . . . 10 (⊤ → (𝑥 ∈ ℝ+ ↦ (((ψ‘𝑥) + 1) / 𝑥)) = (𝑥 ∈ ℝ+ ↦ (((ψ‘𝑥) / 𝑥) + (1 / 𝑥))))
304 simpr 488 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ+)
305237, 304rerpdivcld 12455 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((ψ‘𝑥) / 𝑥) ∈ ℝ)
306 rpreccl 12408 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ+ → (1 / 𝑥) ∈ ℝ+)
307306adantl 485 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → (1 / 𝑥) ∈ ℝ+)
308 eqidd 2825 . . . . . . . . . . . 12 (⊤ → (𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) = (𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)))
309 eqidd 2825 . . . . . . . . . . . 12 (⊤ → (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) = (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)))
310248, 305, 307, 308, 309offval2 7416 . . . . . . . . . . 11 (⊤ → ((𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∘f + (𝑥 ∈ ℝ+ ↦ (1 / 𝑥))) = (𝑥 ∈ ℝ+ ↦ (((ψ‘𝑥) / 𝑥) + (1 / 𝑥))))
311 chpo1ub 26060 . . . . . . . . . . . 12 (𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∈ 𝑂(1)
312 divrcnv 15203 . . . . . . . . . . . . . 14 (1 ∈ ℂ → (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) ⇝𝑟 0)
31328, 312ax-mp 5 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) ⇝𝑟 0
314 rlimo1 14969 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) ⇝𝑟 0 → (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) ∈ 𝑂(1))
315313, 314mp1i 13 . . . . . . . . . . . 12 (⊤ → (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) ∈ 𝑂(1))
316 o1add 14966 . . . . . . . . . . . 12 (((𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∈ 𝑂(1) ∧ (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) ∈ 𝑂(1)) → ((𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∘f + (𝑥 ∈ ℝ+ ↦ (1 / 𝑥))) ∈ 𝑂(1))
317311, 315, 316sylancr 590 . . . . . . . . . . 11 (⊤ → ((𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∘f + (𝑥 ∈ ℝ+ ↦ (1 / 𝑥))) ∈ 𝑂(1))
318310, 317eqeltrrd 2917 . . . . . . . . . 10 (⊤ → (𝑥 ∈ ℝ+ ↦ (((ψ‘𝑥) / 𝑥) + (1 / 𝑥))) ∈ 𝑂(1))
319303, 318eqeltrd 2916 . . . . . . . . 9 (⊤ → (𝑥 ∈ ℝ+ ↦ (((ψ‘𝑥) + 1) / 𝑥)) ∈ 𝑂(1))
320238, 304rerpdivcld 12455 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) + 1) / 𝑥) ∈ ℝ)
321 chpge0 25707 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℝ → 0 ≤ (ψ‘𝑥))
322236, 321syl 17 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑥 ∈ ℝ+) → 0 ≤ (ψ‘𝑥))
323237, 322ge0p1rpd 12454 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((ψ‘𝑥) + 1) ∈ ℝ+)
324323rprege0d 12431 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) + 1) ∈ ℝ ∧ 0 ≤ ((ψ‘𝑥) + 1)))
325242nnrpd 12422 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((⌊‘𝑥) + 1) ∈ ℝ+)
326325rpregt0d 12430 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((⌊‘𝑥) + 1) ∈ ℝ ∧ 0 < ((⌊‘𝑥) + 1)))
327 divge0 11501 . . . . . . . . . . . . 13 (((((ψ‘𝑥) + 1) ∈ ℝ ∧ 0 ≤ ((ψ‘𝑥) + 1)) ∧ (((⌊‘𝑥) + 1) ∈ ℝ ∧ 0 < ((⌊‘𝑥) + 1))) → 0 ≤ (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)))
328324, 326, 327syl2anc 587 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → 0 ≤ (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)))
329243, 328absidd 14778 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → (abs‘(((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1))) = (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)))
330320recnd 10661 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) + 1) / 𝑥) ∈ ℂ)
331330abscld 14792 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → (abs‘(((ψ‘𝑥) + 1) / 𝑥)) ∈ ℝ)
332 fllep1 13171 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → 𝑥 ≤ ((⌊‘𝑥) + 1))
333236, 332syl 17 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℝ+) → 𝑥 ≤ ((⌊‘𝑥) + 1))
334 rpregt0 12396 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ+ → (𝑥 ∈ ℝ ∧ 0 < 𝑥))
335334adantl 485 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ ℝ+) → (𝑥 ∈ ℝ ∧ 0 < 𝑥))
336323rpregt0d 12430 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) + 1) ∈ ℝ ∧ 0 < ((ψ‘𝑥) + 1)))
337 lediv2 11522 . . . . . . . . . . . . . 14 (((𝑥 ∈ ℝ ∧ 0 < 𝑥) ∧ (((⌊‘𝑥) + 1) ∈ ℝ ∧ 0 < ((⌊‘𝑥) + 1)) ∧ (((ψ‘𝑥) + 1) ∈ ℝ ∧ 0 < ((ψ‘𝑥) + 1))) → (𝑥 ≤ ((⌊‘𝑥) + 1) ↔ (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ≤ (((ψ‘𝑥) + 1) / 𝑥)))
338335, 326, 336, 337syl3anc 1368 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℝ+) → (𝑥 ≤ ((⌊‘𝑥) + 1) ↔ (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ≤ (((ψ‘𝑥) + 1) / 𝑥)))
339333, 338mpbid 235 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ≤ (((ψ‘𝑥) + 1) / 𝑥))
340320leabsd 14770 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) + 1) / 𝑥) ≤ (abs‘(((ψ‘𝑥) + 1) / 𝑥)))
341243, 320, 331, 339, 340letrd 10789 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ≤ (abs‘(((ψ‘𝑥) + 1) / 𝑥)))
342329, 341eqbrtrd 5074 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℝ+) → (abs‘(((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1))) ≤ (abs‘(((ψ‘𝑥) + 1) / 𝑥)))
343342adantrr 716 . . . . . . . . 9 ((⊤ ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1))) ≤ (abs‘(((ψ‘𝑥) + 1) / 𝑥)))
344278, 319, 320, 296, 343o1le 15005 . . . . . . . 8 (⊤ → (𝑥 ∈ ℝ+ ↦ (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1))) ∈ 𝑂(1))
345 o1const 14972 . . . . . . . . . 10 ((ℝ+ ⊆ ℝ ∧ 1 ∈ ℂ) → (𝑥 ∈ ℝ+ ↦ 1) ∈ 𝑂(1))
34614, 28, 345mp2an 691 . . . . . . . . 9 (𝑥 ∈ ℝ+ ↦ 1) ∈ 𝑂(1)
347346a1i 11 . . . . . . . 8 (⊤ → (𝑥 ∈ ℝ+ ↦ 1) ∈ 𝑂(1))
348296, 297, 344, 347o1sub2 14978 . . . . . . 7 (⊤ → (𝑥 ∈ ℝ+ ↦ ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1)) ∈ 𝑂(1))
349234, 245, 295, 348o1sub2 14978 . . . . . 6 (⊤ → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) − ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1))) ∈ 𝑂(1))
35013, 349o1res2 14916 . . . . 5 (⊤ → (𝑥 ∈ (1[,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) − ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1))) ∈ 𝑂(1))
351228, 350eqeltrrid 2921 . . . 4 (⊤ → (𝑥 ∈ (1[,)+∞) ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) ∈ 𝑂(1))
35216, 351eqeltrd 2916 . . 3 (⊤ → ((𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) ↾ (1[,)+∞)) ∈ 𝑂(1))
353 eqid 2824 . . . . . 6 (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) = (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1))))
354353, 45fmpti 6864 . . . . 5 (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))):ℝ⟶ℂ
355354a1i 11 . . . 4 (⊤ → (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))):ℝ⟶ℂ)
356 ssidd 3975 . . . 4 (⊤ → ℝ ⊆ ℝ)
357355, 356, 278o1resb 14919 . . 3 (⊤ → ((𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) ∈ 𝑂(1) ↔ ((𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) ↾ (1[,)+∞)) ∈ 𝑂(1)))
358352, 357mpbird 260 . 2 (⊤ → (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) ∈ 𝑂(1))
359358mptru 1545 1 (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) ∈ 𝑂(1)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∧ wa 399   = wceq 1538  ⊤wtru 1539   ∈ wcel 2115   ≠ wne 3014  Vcvv 3480   ⊆ wss 3919   class class class wbr 5052   ↦ cmpt 5132   ↾ cres 5544  ⟶wf 6339  ‘cfv 6343  (class class class)co 7145   ∘f cof 7397  ℂcc 10527  ℝcr 10528  0cc0 10529  1c1 10530   + caddc 10532   · cmul 10534  +∞cpnf 10664   < clt 10667   ≤ cle 10668   − cmin 10862  -cneg 10863   / cdiv 11289  ℕcn 11630  2c2 11685  ℕ0cn0 11890  ℤcz 11974  ℤ≥cuz 12236  ℝ+crp 12382  [,)cico 12733  ...cfz 12890  ..^cfzo 13033  ⌊cfl 13160  abscabs 14589   ⇝𝑟 crli 14838  𝑂(1)co1 14839  Σcsu 15038  logclog 25142  Λcvma 25673  ψcchp 25674 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5176  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7451  ax-inf2 9095  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606  ax-pre-sup 10607  ax-addf 10608  ax-mulf 10609 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-nel 3119  df-ral 3138  df-rex 3139  df-reu 3140  df-rmo 3141  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4276  df-if 4450  df-pw 4523  df-sn 4550  df-pr 4552  df-tp 4554  df-op 4556  df-uni 4825  df-int 4863  df-iun 4907  df-iin 4908  df-br 5053  df-opab 5115  df-mpt 5133  df-tr 5159  df-id 5447  df-eprel 5452  df-po 5461  df-so 5462  df-fr 5501  df-se 5502  df-we 5503  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-pred 6135  df-ord 6181  df-on 6182  df-lim 6183  df-suc 6184  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-fv 6351  df-isom 6352  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-of 7399  df-om 7571  df-1st 7679  df-2nd 7680  df-supp 7821  df-wrecs 7937  df-recs 7998  df-rdg 8036  df-1o 8092  df-2o 8093  df-oadd 8096  df-er 8279  df-map 8398  df-pm 8399  df-ixp 8452  df-en 8500  df-dom 8501  df-sdom 8502  df-fin 8503  df-fsupp 8825  df-fi 8866  df-sup 8897  df-inf 8898  df-oi 8965  df-dju 9321  df-card 9359  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-div 11290  df-nn 11631  df-2 11693  df-3 11694  df-4 11695  df-5 11696  df-6 11697  df-7 11698  df-8 11699  df-9 11700  df-n0 11891  df-xnn0 11961  df-z 11975  df-dec 12092  df-uz 12237  df-q 12342  df-rp 12383  df-xneg 12500  df-xadd 12501  df-xmul 12502  df-ioo 12735  df-ioc 12736  df-ico 12737  df-icc 12738  df-fz 12891  df-fzo 13034  df-fl 13162  df-mod 13238  df-seq 13370  df-exp 13431  df-fac 13635  df-bc 13664  df-hash 13692  df-shft 14422  df-cj 14454  df-re 14455  df-im 14456  df-sqrt 14590  df-abs 14591  df-limsup 14824  df-clim 14841  df-rlim 14842  df-o1 14843  df-lo1 14844  df-sum 15039  df-ef 15417  df-e 15418  df-sin 15419  df-cos 15420  df-tan 15421  df-pi 15422  df-dvds 15604  df-gcd 15838  df-prm 16010  df-pc 16168  df-struct 16481  df-ndx 16482  df-slot 16483  df-base 16485  df-sets 16486  df-ress 16487  df-plusg 16574  df-mulr 16575  df-starv 16576  df-sca 16577  df-vsca 16578  df-ip 16579  df-tset 16580  df-ple 16581  df-ds 16583  df-unif 16584  df-hom 16585  df-cco 16586  df-rest 16692  df-topn 16693  df-0g 16711  df-gsum 16712  df-topgen 16713  df-pt 16714  df-prds 16717  df-xrs 16771  df-qtop 16776  df-imas 16777  df-xps 16779  df-mre 16853  df-mrc 16854  df-acs 16856  df-mgm 17848  df-sgrp 17897  df-mnd 17908  df-submnd 17953  df-mulg 18221  df-cntz 18443  df-cmn 18904  df-psmet 20530  df-xmet 20531  df-met 20532  df-bl 20533  df-mopn 20534  df-fbas 20535  df-fg 20536  df-cnfld 20539  df-top 21495  df-topon 21512  df-topsp 21534  df-bases 21547  df-cld 21620  df-ntr 21621  df-cls 21622  df-nei 21699  df-lp 21737  df-perf 21738  df-cn 21828  df-cnp 21829  df-haus 21916  df-cmp 21988  df-tx 22163  df-hmeo 22356  df-fil 22447  df-fm 22539  df-flim 22540  df-flf 22541  df-xms 22923  df-ms 22924  df-tms 22925  df-cncf 23479  df-limc 24465  df-dv 24466  df-ulm 24968  df-log 25144  df-cxp 25145  df-atan 25449  df-em 25574  df-cht 25678  df-vma 25679  df-chp 25680  df-ppi 25681 This theorem is referenced by:  pntrsumbnd  26146
 Copyright terms: Public domain W3C validator