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

Theorem pntrsumo1 24967
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 9891 . . . . . . . . . . 11 1 ∈ ℝ
2 elicopnf 12092 . . . . . . . . . . 11 (1 ∈ ℝ → (𝑥 ∈ (1[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 1 ≤ 𝑥)))
31, 2ax-mp 5 . . . . . . . . . 10 (𝑥 ∈ (1[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 1 ≤ 𝑥))
43simplbi 474 . . . . . . . . 9 (𝑥 ∈ (1[,)+∞) → 𝑥 ∈ ℝ)
5 0red 9893 . . . . . . . . . 10 (𝑥 ∈ (1[,)+∞) → 0 ∈ ℝ)
6 1red 9907 . . . . . . . . . 10 (𝑥 ∈ (1[,)+∞) → 1 ∈ ℝ)
7 0lt1 10395 . . . . . . . . . . 11 0 < 1
87a1i 11 . . . . . . . . . 10 (𝑥 ∈ (1[,)+∞) → 0 < 1)
93simprbi 478 . . . . . . . . . 10 (𝑥 ∈ (1[,)+∞) → 1 ≤ 𝑥)
105, 6, 4, 8, 9ltletrd 10044 . . . . . . . . 9 (𝑥 ∈ (1[,)+∞) → 0 < 𝑥)
114, 10elrpd 11697 . . . . . . . 8 (𝑥 ∈ (1[,)+∞) → 𝑥 ∈ ℝ+)
1211ssriv 3567 . . . . . . 7 (1[,)+∞) ⊆ ℝ+
1312a1i 11 . . . . . 6 (⊤ → (1[,)+∞) ⊆ ℝ+)
14 rpssre 11671 . . . . . 6 + ⊆ ℝ
1513, 14syl6ss 3575 . . . . 5 (⊤ → (1[,)+∞) ⊆ ℝ)
1615resmptd 5354 . . . 4 (⊤ → ((𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) ↾ (1[,)+∞)) = (𝑥 ∈ (1[,)+∞) ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))))
17 oveq2 6531 . . . . . . . . . . . 12 (𝑚 = 𝑛 → (1 / 𝑚) = (1 / 𝑛))
18 oveq1 6530 . . . . . . . . . . . . . 14 (𝑚 = 𝑛 → (𝑚 − 1) = (𝑛 − 1))
1918fveq2d 6088 . . . . . . . . . . . . 13 (𝑚 = 𝑛 → (ψ‘(𝑚 − 1)) = (ψ‘(𝑛 − 1)))
2019, 18oveq12d 6541 . . . . . . . . . . . 12 (𝑚 = 𝑛 → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = ((ψ‘(𝑛 − 1)) − (𝑛 − 1)))
2117, 20jca 552 . . . . . . . . . . 11 (𝑚 = 𝑛 → ((1 / 𝑚) = (1 / 𝑛) ∧ ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = ((ψ‘(𝑛 − 1)) − (𝑛 − 1))))
22 oveq2 6531 . . . . . . . . . . . 12 (𝑚 = (𝑛 + 1) → (1 / 𝑚) = (1 / (𝑛 + 1)))
23 oveq1 6530 . . . . . . . . . . . . . 14 (𝑚 = (𝑛 + 1) → (𝑚 − 1) = ((𝑛 + 1) − 1))
2423fveq2d 6088 . . . . . . . . . . . . 13 (𝑚 = (𝑛 + 1) → (ψ‘(𝑚 − 1)) = (ψ‘((𝑛 + 1) − 1)))
2524, 23oveq12d 6541 . . . . . . . . . . . 12 (𝑚 = (𝑛 + 1) → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = ((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1)))
2622, 25jca 552 . . . . . . . . . . 11 (𝑚 = (𝑛 + 1) → ((1 / 𝑚) = (1 / (𝑛 + 1)) ∧ ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = ((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1))))
27 oveq2 6531 . . . . . . . . . . . . 13 (𝑚 = 1 → (1 / 𝑚) = (1 / 1))
28 1div1e1 10562 . . . . . . . . . . . . 13 (1 / 1) = 1
2927, 28syl6eq 2655 . . . . . . . . . . . 12 (𝑚 = 1 → (1 / 𝑚) = 1)
30 oveq1 6530 . . . . . . . . . . . . . . . . 17 (𝑚 = 1 → (𝑚 − 1) = (1 − 1))
31 1m1e0 10932 . . . . . . . . . . . . . . . . 17 (1 − 1) = 0
3230, 31syl6eq 2655 . . . . . . . . . . . . . . . 16 (𝑚 = 1 → (𝑚 − 1) = 0)
3332fveq2d 6088 . . . . . . . . . . . . . . 15 (𝑚 = 1 → (ψ‘(𝑚 − 1)) = (ψ‘0))
34 2pos 10955 . . . . . . . . . . . . . . . 16 0 < 2
35 0re 9892 . . . . . . . . . . . . . . . . 17 0 ∈ ℝ
36 chpeq0 24646 . . . . . . . . . . . . . . . . 17 (0 ∈ ℝ → ((ψ‘0) = 0 ↔ 0 < 2))
3735, 36ax-mp 5 . . . . . . . . . . . . . . . 16 ((ψ‘0) = 0 ↔ 0 < 2)
3834, 37mpbir 219 . . . . . . . . . . . . . . 15 (ψ‘0) = 0
3933, 38syl6eq 2655 . . . . . . . . . . . . . 14 (𝑚 = 1 → (ψ‘(𝑚 − 1)) = 0)
4039, 32oveq12d 6541 . . . . . . . . . . . . 13 (𝑚 = 1 → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = (0 − 0))
41 0m0e0 10973 . . . . . . . . . . . . 13 (0 − 0) = 0
4240, 41syl6eq 2655 . . . . . . . . . . . 12 (𝑚 = 1 → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = 0)
4329, 42jca 552 . . . . . . . . . . 11 (𝑚 = 1 → ((1 / 𝑚) = 1 ∧ ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = 0))
44 oveq2 6531 . . . . . . . . . . . 12 (𝑚 = ((⌊‘𝑥) + 1) → (1 / 𝑚) = (1 / ((⌊‘𝑥) + 1)))
45 oveq1 6530 . . . . . . . . . . . . . 14 (𝑚 = ((⌊‘𝑥) + 1) → (𝑚 − 1) = (((⌊‘𝑥) + 1) − 1))
4645fveq2d 6088 . . . . . . . . . . . . 13 (𝑚 = ((⌊‘𝑥) + 1) → (ψ‘(𝑚 − 1)) = (ψ‘(((⌊‘𝑥) + 1) − 1)))
4746, 45oveq12d 6541 . . . . . . . . . . . 12 (𝑚 = ((⌊‘𝑥) + 1) → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = ((ψ‘(((⌊‘𝑥) + 1) − 1)) − (((⌊‘𝑥) + 1) − 1)))
4844, 47jca 552 . . . . . . . . . . 11 (𝑚 = ((⌊‘𝑥) + 1) → ((1 / 𝑚) = (1 / ((⌊‘𝑥) + 1)) ∧ ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = ((ψ‘(((⌊‘𝑥) + 1) − 1)) − (((⌊‘𝑥) + 1) − 1))))
4911rprege0d 11707 . . . . . . . . . . . . . 14 (𝑥 ∈ (1[,)+∞) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
50 flge0nn0 12434 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → (⌊‘𝑥) ∈ ℕ0)
5149, 50syl 17 . . . . . . . . . . . . 13 (𝑥 ∈ (1[,)+∞) → (⌊‘𝑥) ∈ ℕ0)
52 nn0p1nn 11175 . . . . . . . . . . . . 13 ((⌊‘𝑥) ∈ ℕ0 → ((⌊‘𝑥) + 1) ∈ ℕ)
5351, 52syl 17 . . . . . . . . . . . 12 (𝑥 ∈ (1[,)+∞) → ((⌊‘𝑥) + 1) ∈ ℕ)
54 nnuz 11551 . . . . . . . . . . . 12 ℕ = (ℤ‘1)
5553, 54syl6eleq 2693 . . . . . . . . . . 11 (𝑥 ∈ (1[,)+∞) → ((⌊‘𝑥) + 1) ∈ (ℤ‘1))
56 elfznn 12192 . . . . . . . . . . . . . 14 (𝑚 ∈ (1...((⌊‘𝑥) + 1)) → 𝑚 ∈ ℕ)
5756adantl 480 . . . . . . . . . . . . 13 ((𝑥 ∈ (1[,)+∞) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 𝑚 ∈ ℕ)
5857nnrecred 10909 . . . . . . . . . . . 12 ((𝑥 ∈ (1[,)+∞) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (1 / 𝑚) ∈ ℝ)
5958recnd 9920 . . . . . . . . . . 11 ((𝑥 ∈ (1[,)+∞) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (1 / 𝑚) ∈ ℂ)
6057nnred 10878 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 𝑚 ∈ ℝ)
61 peano2rem 10195 . . . . . . . . . . . . . . 15 (𝑚 ∈ ℝ → (𝑚 − 1) ∈ ℝ)
6260, 61syl 17 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑚 − 1) ∈ ℝ)
63 chpcl 24563 . . . . . . . . . . . . . 14 ((𝑚 − 1) ∈ ℝ → (ψ‘(𝑚 − 1)) ∈ ℝ)
6462, 63syl 17 . . . . . . . . . . . . 13 ((𝑥 ∈ (1[,)+∞) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (ψ‘(𝑚 − 1)) ∈ ℝ)
6564, 62resubcld 10305 . . . . . . . . . . . 12 ((𝑥 ∈ (1[,)+∞) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) ∈ ℝ)
6665recnd 9920 . . . . . . . . . . 11 ((𝑥 ∈ (1[,)+∞) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) ∈ ℂ)
6721, 26, 43, 48, 55, 59, 66fsumparts 14321 . . . . . . . . . 10 (𝑥 ∈ (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)))))
684flcld 12412 . . . . . . . . . . . . 13 (𝑥 ∈ (1[,)+∞) → (⌊‘𝑥) ∈ ℤ)
69 fzval3 12355 . . . . . . . . . . . . 13 ((⌊‘𝑥) ∈ ℤ → (1...(⌊‘𝑥)) = (1..^((⌊‘𝑥) + 1)))
7068, 69syl 17 . . . . . . . . . . . 12 (𝑥 ∈ (1[,)+∞) → (1...(⌊‘𝑥)) = (1..^((⌊‘𝑥) + 1)))
7170eqcomd 2611 . . . . . . . . . . 11 (𝑥 ∈ (1[,)+∞) → (1..^((⌊‘𝑥) + 1)) = (1...(⌊‘𝑥)))
72 elfznn 12192 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
7372adantl 480 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
7473nncnd 10879 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℂ)
75 ax-1cn 9846 . . . . . . . . . . . . . . . . . . 19 1 ∈ ℂ
76 pncan 10134 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛 + 1) − 1) = 𝑛)
7774, 75, 76sylancl 692 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) − 1) = 𝑛)
7873nnred 10878 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ)
7977, 78eqeltrd 2683 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) − 1) ∈ ℝ)
80 chpcl 24563 . . . . . . . . . . . . . . . . 17 (((𝑛 + 1) − 1) ∈ ℝ → (ψ‘((𝑛 + 1) − 1)) ∈ ℝ)
8179, 80syl 17 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (ψ‘((𝑛 + 1) − 1)) ∈ ℝ)
8281recnd 9920 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (ψ‘((𝑛 + 1) − 1)) ∈ ℂ)
8379recnd 9920 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) − 1) ∈ ℂ)
84 peano2rem 10195 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℝ → (𝑛 − 1) ∈ ℝ)
8578, 84syl 17 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 − 1) ∈ ℝ)
86 chpcl 24563 . . . . . . . . . . . . . . . . 17 ((𝑛 − 1) ∈ ℝ → (ψ‘(𝑛 − 1)) ∈ ℝ)
8785, 86syl 17 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (ψ‘(𝑛 − 1)) ∈ ℝ)
8887recnd 9920 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (ψ‘(𝑛 − 1)) ∈ ℂ)
89 1cnd 9908 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℂ)
9074, 89subcld 10239 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 − 1) ∈ ℂ)
9182, 83, 88, 90sub4d 10288 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1)) − ((ψ‘(𝑛 − 1)) − (𝑛 − 1))) = (((ψ‘((𝑛 + 1) − 1)) − (ψ‘(𝑛 − 1))) − (((𝑛 + 1) − 1) − (𝑛 − 1))))
92 nnm1nn0 11177 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ → (𝑛 − 1) ∈ ℕ0)
9373, 92syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 − 1) ∈ ℕ0)
94 chpp1 24594 . . . . . . . . . . . . . . . . . . 19 ((𝑛 − 1) ∈ ℕ0 → (ψ‘((𝑛 − 1) + 1)) = ((ψ‘(𝑛 − 1)) + (Λ‘((𝑛 − 1) + 1))))
9593, 94syl 17 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (ψ‘((𝑛 − 1) + 1)) = ((ψ‘(𝑛 − 1)) + (Λ‘((𝑛 − 1) + 1))))
96 npcan 10137 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛 − 1) + 1) = 𝑛)
9774, 75, 96sylancl 692 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 − 1) + 1) = 𝑛)
9897, 77eqtr4d 2642 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 − 1) + 1) = ((𝑛 + 1) − 1))
9998fveq2d 6088 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (ψ‘((𝑛 − 1) + 1)) = (ψ‘((𝑛 + 1) − 1)))
10097fveq2d 6088 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘((𝑛 − 1) + 1)) = (Λ‘𝑛))
101100oveq2d 6539 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((ψ‘(𝑛 − 1)) + (Λ‘((𝑛 − 1) + 1))) = ((ψ‘(𝑛 − 1)) + (Λ‘𝑛)))
10295, 99, 1013eqtr3d 2647 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (ψ‘((𝑛 + 1) − 1)) = ((ψ‘(𝑛 − 1)) + (Λ‘𝑛)))
103102oveq1d 6538 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((ψ‘((𝑛 + 1) − 1)) − (ψ‘(𝑛 − 1))) = (((ψ‘(𝑛 − 1)) + (Λ‘𝑛)) − (ψ‘(𝑛 − 1))))
104 vmacl 24557 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → (Λ‘𝑛) ∈ ℝ)
10573, 104syl 17 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈ ℝ)
106105recnd 9920 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈ ℂ)
10788, 106pncan2d 10241 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((ψ‘(𝑛 − 1)) + (Λ‘𝑛)) − (ψ‘(𝑛 − 1))) = (Λ‘𝑛))
108103, 107eqtrd 2639 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((ψ‘((𝑛 + 1) − 1)) − (ψ‘(𝑛 − 1))) = (Λ‘𝑛))
109 peano2cn 10055 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℂ → (𝑛 + 1) ∈ ℂ)
11074, 109syl 17 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 + 1) ∈ ℂ)
111110, 74, 89nnncan2d 10274 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑛 + 1) − 1) − (𝑛 − 1)) = ((𝑛 + 1) − 𝑛))
112 pncan2 10135 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛 + 1) − 𝑛) = 1)
11374, 75, 112sylancl 692 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) − 𝑛) = 1)
114111, 113eqtrd 2639 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑛 + 1) − 1) − (𝑛 − 1)) = 1)
115108, 114oveq12d 6541 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((ψ‘((𝑛 + 1) − 1)) − (ψ‘(𝑛 − 1))) − (((𝑛 + 1) − 1) − (𝑛 − 1))) = ((Λ‘𝑛) − 1))
11691, 115eqtrd 2639 . . . . . . . . . . . . 13 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1)) − ((ψ‘(𝑛 − 1)) − (𝑛 − 1))) = ((Λ‘𝑛) − 1))
117116oveq2d 6539 . . . . . . . . . . . 12 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 / 𝑛) · (((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1)) − ((ψ‘(𝑛 − 1)) − (𝑛 − 1)))) = ((1 / 𝑛) · ((Λ‘𝑛) − 1)))
118 peano2rem 10195 . . . . . . . . . . . . . . 15 ((Λ‘𝑛) ∈ ℝ → ((Λ‘𝑛) − 1) ∈ ℝ)
119105, 118syl 17 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) − 1) ∈ ℝ)
120119recnd 9920 . . . . . . . . . . . . 13 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) − 1) ∈ ℂ)
12173nnne0d 10908 . . . . . . . . . . . . 13 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ≠ 0)
122120, 74, 121divrec2d 10650 . . . . . . . . . . . 12 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) − 1) / 𝑛) = ((1 / 𝑛) · ((Λ‘𝑛) − 1)))
123117, 122eqtr4d 2642 . . . . . . . . . . 11 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 / 𝑛) · (((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1)) − ((ψ‘(𝑛 − 1)) − (𝑛 − 1)))) = (((Λ‘𝑛) − 1) / 𝑛))
12471, 123sumeq12rdv 14227 . . . . . . . . . 10 (𝑥 ∈ (1[,)+∞) → Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))((1 / 𝑛) · (((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1)) − ((ψ‘(𝑛 − 1)) − (𝑛 − 1)))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛))
12551nn0cnd 11196 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (1[,)+∞) → (⌊‘𝑥) ∈ ℂ)
126 pncan 10134 . . . . . . . . . . . . . . . . . . . 20 (((⌊‘𝑥) ∈ ℂ ∧ 1 ∈ ℂ) → (((⌊‘𝑥) + 1) − 1) = (⌊‘𝑥))
127125, 75, 126sylancl 692 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (1[,)+∞) → (((⌊‘𝑥) + 1) − 1) = (⌊‘𝑥))
128127fveq2d 6088 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (1[,)+∞) → (ψ‘(((⌊‘𝑥) + 1) − 1)) = (ψ‘(⌊‘𝑥)))
129 chpfl 24589 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℝ → (ψ‘(⌊‘𝑥)) = (ψ‘𝑥))
1304, 129syl 17 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (1[,)+∞) → (ψ‘(⌊‘𝑥)) = (ψ‘𝑥))
131128, 130eqtrd 2639 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (1[,)+∞) → (ψ‘(((⌊‘𝑥) + 1) − 1)) = (ψ‘𝑥))
132131oveq1d 6538 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1[,)+∞) → ((ψ‘(((⌊‘𝑥) + 1) − 1)) − (((⌊‘𝑥) + 1) − 1)) = ((ψ‘𝑥) − (((⌊‘𝑥) + 1) − 1)))
133 chpcl 24563 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℝ → (ψ‘𝑥) ∈ ℝ)
1344, 133syl 17 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (1[,)+∞) → (ψ‘𝑥) ∈ ℝ)
135134recnd 9920 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (1[,)+∞) → (ψ‘𝑥) ∈ ℂ)
13653nncnd 10879 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (1[,)+∞) → ((⌊‘𝑥) + 1) ∈ ℂ)
137 1cnd 9908 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (1[,)+∞) → 1 ∈ ℂ)
138135, 136, 137subsub3d 10269 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1[,)+∞) → ((ψ‘𝑥) − (((⌊‘𝑥) + 1) − 1)) = (((ψ‘𝑥) + 1) − ((⌊‘𝑥) + 1)))
139132, 138eqtrd 2639 . . . . . . . . . . . . . . 15 (𝑥 ∈ (1[,)+∞) → ((ψ‘(((⌊‘𝑥) + 1) − 1)) − (((⌊‘𝑥) + 1) − 1)) = (((ψ‘𝑥) + 1) − ((⌊‘𝑥) + 1)))
140139oveq2d 6539 . . . . . . . . . . . . . 14 (𝑥 ∈ (1[,)+∞) → ((1 / ((⌊‘𝑥) + 1)) · ((ψ‘(((⌊‘𝑥) + 1) − 1)) − (((⌊‘𝑥) + 1) − 1))) = ((1 / ((⌊‘𝑥) + 1)) · (((ψ‘𝑥) + 1) − ((⌊‘𝑥) + 1))))
14153nnrecred 10909 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1[,)+∞) → (1 / ((⌊‘𝑥) + 1)) ∈ ℝ)
142141recnd 9920 . . . . . . . . . . . . . . 15 (𝑥 ∈ (1[,)+∞) → (1 / ((⌊‘𝑥) + 1)) ∈ ℂ)
143 peano2cn 10055 . . . . . . . . . . . . . . . 16 ((ψ‘𝑥) ∈ ℂ → ((ψ‘𝑥) + 1) ∈ ℂ)
144135, 143syl 17 . . . . . . . . . . . . . . 15 (𝑥 ∈ (1[,)+∞) → ((ψ‘𝑥) + 1) ∈ ℂ)
145142, 144, 136subdid 10332 . . . . . . . . . . . . . 14 (𝑥 ∈ (1[,)+∞) → ((1 / ((⌊‘𝑥) + 1)) · (((ψ‘𝑥) + 1) − ((⌊‘𝑥) + 1))) = (((1 / ((⌊‘𝑥) + 1)) · ((ψ‘𝑥) + 1)) − ((1 / ((⌊‘𝑥) + 1)) · ((⌊‘𝑥) + 1))))
14653nnne0d 10908 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (1[,)+∞) → ((⌊‘𝑥) + 1) ≠ 0)
147144, 136, 146divrec2d 10650 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1[,)+∞) → (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) = ((1 / ((⌊‘𝑥) + 1)) · ((ψ‘𝑥) + 1)))
148147eqcomd 2611 . . . . . . . . . . . . . . 15 (𝑥 ∈ (1[,)+∞) → ((1 / ((⌊‘𝑥) + 1)) · ((ψ‘𝑥) + 1)) = (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)))
149136, 146recid2d 10642 . . . . . . . . . . . . . . 15 (𝑥 ∈ (1[,)+∞) → ((1 / ((⌊‘𝑥) + 1)) · ((⌊‘𝑥) + 1)) = 1)
150148, 149oveq12d 6541 . . . . . . . . . . . . . 14 (𝑥 ∈ (1[,)+∞) → (((1 / ((⌊‘𝑥) + 1)) · ((ψ‘𝑥) + 1)) − ((1 / ((⌊‘𝑥) + 1)) · ((⌊‘𝑥) + 1))) = ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1))
151140, 145, 1503eqtrd 2643 . . . . . . . . . . . . 13 (𝑥 ∈ (1[,)+∞) → ((1 / ((⌊‘𝑥) + 1)) · ((ψ‘(((⌊‘𝑥) + 1) − 1)) − (((⌊‘𝑥) + 1) − 1))) = ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1))
15275mul01i 10073 . . . . . . . . . . . . . 14 (1 · 0) = 0
153152a1i 11 . . . . . . . . . . . . 13 (𝑥 ∈ (1[,)+∞) → (1 · 0) = 0)
154151, 153oveq12d 6541 . . . . . . . . . . . 12 (𝑥 ∈ (1[,)+∞) → (((1 / ((⌊‘𝑥) + 1)) · ((ψ‘(((⌊‘𝑥) + 1) − 1)) − (((⌊‘𝑥) + 1) − 1))) − (1 · 0)) = (((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) − 0))
155 peano2re 10056 . . . . . . . . . . . . . . . . 17 ((ψ‘𝑥) ∈ ℝ → ((ψ‘𝑥) + 1) ∈ ℝ)
156134, 155syl 17 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1[,)+∞) → ((ψ‘𝑥) + 1) ∈ ℝ)
157156, 53nndivred 10912 . . . . . . . . . . . . . . 15 (𝑥 ∈ (1[,)+∞) → (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ∈ ℝ)
158157recnd 9920 . . . . . . . . . . . . . 14 (𝑥 ∈ (1[,)+∞) → (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ∈ ℂ)
159 subcl 10127 . . . . . . . . . . . . . 14 (((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ∈ ℂ ∧ 1 ∈ ℂ) → ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) ∈ ℂ)
160158, 75, 159sylancl 692 . . . . . . . . . . . . 13 (𝑥 ∈ (1[,)+∞) → ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) ∈ ℂ)
161160subid1d 10228 . . . . . . . . . . . 12 (𝑥 ∈ (1[,)+∞) → (((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) − 0) = ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1))
162154, 161eqtrd 2639 . . . . . . . . . . 11 (𝑥 ∈ (1[,)+∞) → (((1 / ((⌊‘𝑥) + 1)) · ((ψ‘(((⌊‘𝑥) + 1) − 1)) − (((⌊‘𝑥) + 1) − 1))) − (1 · 0)) = ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1))
163 peano2nn 10875 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℕ)
164 nnmulcl 10886 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ ℕ) → (𝑛 · (𝑛 + 1)) ∈ ℕ)
165163, 164mpdan 698 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → (𝑛 · (𝑛 + 1)) ∈ ℕ)
16673, 165syl 17 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 · (𝑛 + 1)) ∈ ℕ)
167166nnrecred 10909 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / (𝑛 · (𝑛 + 1))) ∈ ℝ)
168167recnd 9920 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / (𝑛 · (𝑛 + 1))) ∈ ℂ)
169 nnrp 11670 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → 𝑛 ∈ ℝ+)
170 pntrval.r . . . . . . . . . . . . . . . . . . . 20 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))
171170pntrf 24965 . . . . . . . . . . . . . . . . . . 19 𝑅:ℝ+⟶ℝ
172171ffvelrni 6247 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℝ+ → (𝑅𝑛) ∈ ℝ)
173169, 172syl 17 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ → (𝑅𝑛) ∈ ℝ)
17473, 173syl 17 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅𝑛) ∈ ℝ)
175174recnd 9920 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅𝑛) ∈ ℂ)
176168, 175mulneg1d 10329 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (-(1 / (𝑛 · (𝑛 + 1))) · (𝑅𝑛)) = -((1 / (𝑛 · (𝑛 + 1))) · (𝑅𝑛)))
17774, 89mulcld 9912 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 · 1) ∈ ℂ)
17874, 110mulcld 9912 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 · (𝑛 + 1)) ∈ ℂ)
179166nnne0d 10908 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 · (𝑛 + 1)) ≠ 0)
180110, 177, 178, 179divsubdird 10685 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑛 + 1) − (𝑛 · 1)) / (𝑛 · (𝑛 + 1))) = (((𝑛 + 1) / (𝑛 · (𝑛 + 1))) − ((𝑛 · 1) / (𝑛 · (𝑛 + 1)))))
18174mulid1d 9909 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 · 1) = 𝑛)
182181oveq2d 6539 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) − (𝑛 · 1)) = ((𝑛 + 1) − 𝑛))
183182, 113eqtrd 2639 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) − (𝑛 · 1)) = 1)
184183oveq1d 6538 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑛 + 1) − (𝑛 · 1)) / (𝑛 · (𝑛 + 1))) = (1 / (𝑛 · (𝑛 + 1))))
185110mulid1d 9909 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) · 1) = (𝑛 + 1))
186110, 74mulcomd 9913 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) · 𝑛) = (𝑛 · (𝑛 + 1)))
187185, 186oveq12d 6541 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑛 + 1) · 1) / ((𝑛 + 1) · 𝑛)) = ((𝑛 + 1) / (𝑛 · (𝑛 + 1))))
18873, 163syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 + 1) ∈ ℕ)
189188nnne0d 10908 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 + 1) ≠ 0)
19089, 74, 110, 121, 189divcan5d 10672 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑛 + 1) · 1) / ((𝑛 + 1) · 𝑛)) = (1 / 𝑛))
191187, 190eqtr3d 2641 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) / (𝑛 · (𝑛 + 1))) = (1 / 𝑛))
19289, 110, 74, 189, 121divcan5d 10672 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 · 1) / (𝑛 · (𝑛 + 1))) = (1 / (𝑛 + 1)))
193191, 192oveq12d 6541 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑛 + 1) / (𝑛 · (𝑛 + 1))) − ((𝑛 · 1) / (𝑛 · (𝑛 + 1)))) = ((1 / 𝑛) − (1 / (𝑛 + 1))))
194180, 184, 1933eqtr3d 2647 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / (𝑛 · (𝑛 + 1))) = ((1 / 𝑛) − (1 / (𝑛 + 1))))
195194negeqd 10122 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → -(1 / (𝑛 · (𝑛 + 1))) = -((1 / 𝑛) − (1 / (𝑛 + 1))))
19673nnrecred 10909 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / 𝑛) ∈ ℝ)
197196recnd 9920 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / 𝑛) ∈ ℂ)
198188nnrecred 10909 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / (𝑛 + 1)) ∈ ℝ)
199198recnd 9920 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / (𝑛 + 1)) ∈ ℂ)
200197, 199negsubdi2d 10255 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → -((1 / 𝑛) − (1 / (𝑛 + 1))) = ((1 / (𝑛 + 1)) − (1 / 𝑛)))
201195, 200eqtr2d 2640 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 / (𝑛 + 1)) − (1 / 𝑛)) = -(1 / (𝑛 · (𝑛 + 1))))
20273nnrpd 11698 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ+)
20377, 202eqeltrd 2683 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) − 1) ∈ ℝ+)
204170pntrval 24964 . . . . . . . . . . . . . . . . 17 (((𝑛 + 1) − 1) ∈ ℝ+ → (𝑅‘((𝑛 + 1) − 1)) = ((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1)))
205203, 204syl 17 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘((𝑛 + 1) − 1)) = ((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1)))
20677fveq2d 6088 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘((𝑛 + 1) − 1)) = (𝑅𝑛))
207205, 206eqtr3d 2641 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1)) = (𝑅𝑛))
208201, 207oveq12d 6541 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((1 / (𝑛 + 1)) − (1 / 𝑛)) · ((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1))) = (-(1 / (𝑛 · (𝑛 + 1))) · (𝑅𝑛)))
209175, 178, 179divrec2d 10650 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑅𝑛) / (𝑛 · (𝑛 + 1))) = ((1 / (𝑛 · (𝑛 + 1))) · (𝑅𝑛)))
210209negeqd 10122 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → -((𝑅𝑛) / (𝑛 · (𝑛 + 1))) = -((1 / (𝑛 · (𝑛 + 1))) · (𝑅𝑛)))
211176, 208, 2103eqtr4d 2649 . . . . . . . . . . . . 13 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((1 / (𝑛 + 1)) − (1 / 𝑛)) · ((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1))) = -((𝑅𝑛) / (𝑛 · (𝑛 + 1))))
21271, 211sumeq12rdv 14227 . . . . . . . . . . . 12 (𝑥 ∈ (1[,)+∞) → Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))(((1 / (𝑛 + 1)) − (1 / 𝑛)) · ((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1))) = Σ𝑛 ∈ (1...(⌊‘𝑥))-((𝑅𝑛) / (𝑛 · (𝑛 + 1))))
213 fzfid 12585 . . . . . . . . . . . . 13 (𝑥 ∈ (1[,)+∞) → (1...(⌊‘𝑥)) ∈ Fin)
214173, 165nndivred 10912 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → ((𝑅𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ)
21573, 214syl 17 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑅𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ)
216215recnd 9920 . . . . . . . . . . . . 13 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑅𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ)
217213, 216fsumneg 14303 . . . . . . . . . . . 12 (𝑥 ∈ (1[,)+∞) → Σ𝑛 ∈ (1...(⌊‘𝑥))-((𝑅𝑛) / (𝑛 · (𝑛 + 1))) = -Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1))))
218212, 217eqtrd 2639 . . . . . . . . . . 11 (𝑥 ∈ (1[,)+∞) → Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))(((1 / (𝑛 + 1)) − (1 / 𝑛)) · ((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1))) = -Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1))))
219162, 218oveq12d 6541 . . . . . . . . . 10 (𝑥 ∈ (1[,)+∞) → ((((1 / ((⌊‘𝑥) + 1)) · ((ψ‘(((⌊‘𝑥) + 1) − 1)) − (((⌊‘𝑥) + 1) − 1))) − (1 · 0)) − Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))(((1 / (𝑛 + 1)) − (1 / 𝑛)) · ((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1)))) = (((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) − -Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))))
22067, 124, 2193eqtr3d 2647 . . . . . . . . 9 (𝑥 ∈ (1[,)+∞) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) = (((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) − -Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))))
221 fzfid 12585 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → (1...(⌊‘𝑥)) ∈ Fin)
22272adantl 480 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℝ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
223222, 214syl 17 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑅𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ)
224221, 223fsumrecl 14254 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ)
225224recnd 9920 . . . . . . . . . . 11 (𝑥 ∈ ℝ → Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ)
2264, 225syl 17 . . . . . . . . . 10 (𝑥 ∈ (1[,)+∞) → Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ)
227160, 226subnegd 10246 . . . . . . . . 9 (𝑥 ∈ (1[,)+∞) → (((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) − -Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) = (((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) + Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))))
228220, 227eqtrd 2639 . . . . . . . 8 (𝑥 ∈ (1[,)+∞) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) = (((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) + Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))))
229228oveq1d 6538 . . . . . . 7 (𝑥 ∈ (1[,)+∞) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) − ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1)) = ((((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) + Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) − ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1)))
230160, 226pncan2d 10241 . . . . . . 7 (𝑥 ∈ (1[,)+∞) → ((((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) + Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) − ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1)) = Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1))))
231229, 230eqtrd 2639 . . . . . 6 (𝑥 ∈ (1[,)+∞) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) − ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1)) = Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1))))
232231mpteq2ia 4658 . . . . 5 (𝑥 ∈ (1[,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) − ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1))) = (𝑥 ∈ (1[,)+∞) ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1))))
233 fzfid 12585 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ ℝ+) → (1...(⌊‘𝑥)) ∈ Fin)
23472adantl 480 . . . . . . . . . . 11 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
235234, 104syl 17 . . . . . . . . . 10 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈ ℝ)
236235, 118syl 17 . . . . . . . . 9 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) − 1) ∈ ℝ)
237236, 234nndivred 10912 . . . . . . . 8 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) − 1) / 𝑛) ∈ ℝ)
238233, 237fsumrecl 14254 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) ∈ ℝ)
239 rpre 11667 . . . . . . . . . . . 12 (𝑥 ∈ ℝ+𝑥 ∈ ℝ)
240239adantl 480 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ)
241240, 133syl 17 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℝ+) → (ψ‘𝑥) ∈ ℝ)
242241, 155syl 17 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((ψ‘𝑥) + 1) ∈ ℝ)
243 rprege0 11675 . . . . . . . . . . . 12 (𝑥 ∈ ℝ+ → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
244243, 50syl 17 . . . . . . . . . . 11 (𝑥 ∈ ℝ+ → (⌊‘𝑥) ∈ ℕ0)
245244adantl 480 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℝ+) → (⌊‘𝑥) ∈ ℕ0)
246245, 52syl 17 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((⌊‘𝑥) + 1) ∈ ℕ)
247242, 246nndivred 10912 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ∈ ℝ)
248 peano2rem 10195 . . . . . . . 8 ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ∈ ℝ → ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) ∈ ℝ)
249247, 248syl 17 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) ∈ ℝ)
250 reex 9879 . . . . . . . . . . . 12 ℝ ∈ V
251250, 14ssexi 4722 . . . . . . . . . . 11 + ∈ V
252251a1i 11 . . . . . . . . . 10 (⊤ → ℝ+ ∈ V)
253235, 234nndivred 10912 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) / 𝑛) ∈ ℝ)
254253recnd 9920 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) / 𝑛) ∈ ℂ)
255233, 254fsumcl 14253 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ∈ ℂ)
256 relogcl 24039 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ+ → (log‘𝑥) ∈ ℝ)
257256adantl 480 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℝ)
258257recnd 9920 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℂ)
259255, 258subcld 10239 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) ∈ ℂ)
260234nnrecred 10909 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / 𝑛) ∈ ℝ)
261233, 260fsumrecl 14254 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) ∈ ℝ)
262261, 257resubcld 10305 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)) ∈ ℝ)
263 eqidd 2606 . . . . . . . . . 10 (⊤ → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) = (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))))
264 eqidd 2606 . . . . . . . . . 10 (⊤ → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) = (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))))
265252, 259, 262, 263, 264offval2 6785 . . . . . . . . 9 (⊤ → ((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘𝑓 − (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)))) = (𝑥 ∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)))))
266260recnd 9920 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / 𝑛) ∈ ℂ)
267233, 254, 266fsumsub 14304 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) − (1 / 𝑛)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛)))
268235recnd 9920 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈ ℂ)
269 1cnd 9908 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℂ)
270234nncnd 10879 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℂ)
271234nnne0d 10908 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ≠ 0)
272268, 269, 270, 271divsubdird 10685 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) − 1) / 𝑛) = (((Λ‘𝑛) / 𝑛) − (1 / 𝑛)))
273272sumeq2dv 14223 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) − (1 / 𝑛)))
274261recnd 9920 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) ∈ ℂ)
275255, 274, 258nnncan2d 10274 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛)))
276267, 273, 2753eqtr4rd 2650 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛))
277276mpteq2dva 4662 . . . . . . . . 9 (⊤ → (𝑥 ∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)))) = (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛)))
278265, 277eqtrd 2639 . . . . . . . 8 (⊤ → ((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘𝑓 − (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)))) = (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛)))
279 vmadivsum 24884 . . . . . . . . 9 (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1)
28014a1i 11 . . . . . . . . . 10 (⊤ → ℝ+ ⊆ ℝ)
281262recnd 9920 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)) ∈ ℂ)
282 1red 9907 . . . . . . . . . 10 (⊤ → 1 ∈ ℝ)
283 harmoniclbnd 24448 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ+ → (log‘𝑥) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛))
284283adantl 480 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℝ+) → (log‘𝑥) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛))
285257, 261, 284abssubge0d 13960 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)))
286285adantrr 748 . . . . . . . . . . 11 ((⊤ ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)))
287239ad2antrl 759 . . . . . . . . . . . . 13 ((⊤ ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ)
288 simprr 791 . . . . . . . . . . . . 13 ((⊤ ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ≤ 𝑥)
289 harmonicubnd 24449 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) ≤ ((log‘𝑥) + 1))
290287, 288, 289syl2anc 690 . . . . . . . . . . . 12 ((⊤ ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) ≤ ((log‘𝑥) + 1))
291 1red 9907 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ ℝ+) → 1 ∈ ℝ)
292261, 257, 291lesubadd2d 10471 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)) ≤ 1 ↔ Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) ≤ ((log‘𝑥) + 1)))
293292adantrr 748 . . . . . . . . . . . 12 ((⊤ ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)) ≤ 1 ↔ Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) ≤ ((log‘𝑥) + 1)))
294290, 293mpbird 245 . . . . . . . . . . 11 ((⊤ ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)) ≤ 1)
295286, 294eqbrtrd 4595 . . . . . . . . . 10 ((⊤ ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) ≤ 1)
296280, 281, 282, 282, 295elo1d 14057 . . . . . . . . 9 (⊤ → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) ∈ 𝑂(1))
297 o1sub 14136 . . . . . . . . 9 (((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1) ∧ (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) ∈ 𝑂(1)) → ((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘𝑓 − (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)))) ∈ 𝑂(1))
298279, 296, 297sylancr 693 . . . . . . . 8 (⊤ → ((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘𝑓 − (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)))) ∈ 𝑂(1))
299278, 298eqeltrrd 2684 . . . . . . 7 (⊤ → (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛)) ∈ 𝑂(1))
300247recnd 9920 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ∈ ℂ)
301 1cnd 9908 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ ℝ+) → 1 ∈ ℂ)
302241recnd 9920 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → (ψ‘𝑥) ∈ ℂ)
303 rpcnne0 11678 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ+ → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
304303adantl 480 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
305 divdir 10555 . . . . . . . . . . . 12 (((ψ‘𝑥) ∈ ℂ ∧ 1 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → (((ψ‘𝑥) + 1) / 𝑥) = (((ψ‘𝑥) / 𝑥) + (1 / 𝑥)))
306302, 301, 304, 305syl3anc 1317 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) + 1) / 𝑥) = (((ψ‘𝑥) / 𝑥) + (1 / 𝑥)))
307306mpteq2dva 4662 . . . . . . . . . 10 (⊤ → (𝑥 ∈ ℝ+ ↦ (((ψ‘𝑥) + 1) / 𝑥)) = (𝑥 ∈ ℝ+ ↦ (((ψ‘𝑥) / 𝑥) + (1 / 𝑥))))
308 simpr 475 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ+)
309241, 308rerpdivcld 11731 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((ψ‘𝑥) / 𝑥) ∈ ℝ)
310 rpreccl 11685 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ+ → (1 / 𝑥) ∈ ℝ+)
311310adantl 480 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → (1 / 𝑥) ∈ ℝ+)
312 eqidd 2606 . . . . . . . . . . . 12 (⊤ → (𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) = (𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)))
313 eqidd 2606 . . . . . . . . . . . 12 (⊤ → (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) = (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)))
314252, 309, 311, 312, 313offval2 6785 . . . . . . . . . . 11 (⊤ → ((𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∘𝑓 + (𝑥 ∈ ℝ+ ↦ (1 / 𝑥))) = (𝑥 ∈ ℝ+ ↦ (((ψ‘𝑥) / 𝑥) + (1 / 𝑥))))
315 chpo1ub 24882 . . . . . . . . . . . 12 (𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∈ 𝑂(1)
316 divrcnv 14365 . . . . . . . . . . . . . 14 (1 ∈ ℂ → (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) ⇝𝑟 0)
31775, 316ax-mp 5 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) ⇝𝑟 0
318 rlimo1 14137 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) ⇝𝑟 0 → (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) ∈ 𝑂(1))
319317, 318mp1i 13 . . . . . . . . . . . 12 (⊤ → (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) ∈ 𝑂(1))
320 o1add 14134 . . . . . . . . . . . 12 (((𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∈ 𝑂(1) ∧ (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) ∈ 𝑂(1)) → ((𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∘𝑓 + (𝑥 ∈ ℝ+ ↦ (1 / 𝑥))) ∈ 𝑂(1))
321315, 319, 320sylancr 693 . . . . . . . . . . 11 (⊤ → ((𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∘𝑓 + (𝑥 ∈ ℝ+ ↦ (1 / 𝑥))) ∈ 𝑂(1))
322314, 321eqeltrrd 2684 . . . . . . . . . 10 (⊤ → (𝑥 ∈ ℝ+ ↦ (((ψ‘𝑥) / 𝑥) + (1 / 𝑥))) ∈ 𝑂(1))
323307, 322eqeltrd 2683 . . . . . . . . 9 (⊤ → (𝑥 ∈ ℝ+ ↦ (((ψ‘𝑥) + 1) / 𝑥)) ∈ 𝑂(1))
324242, 308rerpdivcld 11731 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) + 1) / 𝑥) ∈ ℝ)
325 chpge0 24565 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℝ → 0 ≤ (ψ‘𝑥))
326240, 325syl 17 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑥 ∈ ℝ+) → 0 ≤ (ψ‘𝑥))
327241, 326ge0p1rpd 11730 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((ψ‘𝑥) + 1) ∈ ℝ+)
328327rprege0d 11707 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) + 1) ∈ ℝ ∧ 0 ≤ ((ψ‘𝑥) + 1)))
329246nnrpd 11698 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((⌊‘𝑥) + 1) ∈ ℝ+)
330329rpregt0d 11706 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((⌊‘𝑥) + 1) ∈ ℝ ∧ 0 < ((⌊‘𝑥) + 1)))
331 divge0 10737 . . . . . . . . . . . . 13 (((((ψ‘𝑥) + 1) ∈ ℝ ∧ 0 ≤ ((ψ‘𝑥) + 1)) ∧ (((⌊‘𝑥) + 1) ∈ ℝ ∧ 0 < ((⌊‘𝑥) + 1))) → 0 ≤ (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)))
332328, 330, 331syl2anc 690 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → 0 ≤ (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)))
333247, 332absidd 13951 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → (abs‘(((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1))) = (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)))
334324recnd 9920 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) + 1) / 𝑥) ∈ ℂ)
335334abscld 13965 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → (abs‘(((ψ‘𝑥) + 1) / 𝑥)) ∈ ℝ)
336 fllep1 12415 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → 𝑥 ≤ ((⌊‘𝑥) + 1))
337240, 336syl 17 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℝ+) → 𝑥 ≤ ((⌊‘𝑥) + 1))
338 rpregt0 11674 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ+ → (𝑥 ∈ ℝ ∧ 0 < 𝑥))
339338adantl 480 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ ℝ+) → (𝑥 ∈ ℝ ∧ 0 < 𝑥))
340327rpregt0d 11706 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) + 1) ∈ ℝ ∧ 0 < ((ψ‘𝑥) + 1)))
341 lediv2 10758 . . . . . . . . . . . . . 14 (((𝑥 ∈ ℝ ∧ 0 < 𝑥) ∧ (((⌊‘𝑥) + 1) ∈ ℝ ∧ 0 < ((⌊‘𝑥) + 1)) ∧ (((ψ‘𝑥) + 1) ∈ ℝ ∧ 0 < ((ψ‘𝑥) + 1))) → (𝑥 ≤ ((⌊‘𝑥) + 1) ↔ (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ≤ (((ψ‘𝑥) + 1) / 𝑥)))
342339, 330, 340, 341syl3anc 1317 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℝ+) → (𝑥 ≤ ((⌊‘𝑥) + 1) ↔ (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ≤ (((ψ‘𝑥) + 1) / 𝑥)))
343337, 342mpbid 220 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ≤ (((ψ‘𝑥) + 1) / 𝑥))
344324leabsd 13943 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) + 1) / 𝑥) ≤ (abs‘(((ψ‘𝑥) + 1) / 𝑥)))
345247, 324, 335, 343, 344letrd 10041 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ≤ (abs‘(((ψ‘𝑥) + 1) / 𝑥)))
346333, 345eqbrtrd 4595 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℝ+) → (abs‘(((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1))) ≤ (abs‘(((ψ‘𝑥) + 1) / 𝑥)))
347346adantrr 748 . . . . . . . . 9 ((⊤ ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1))) ≤ (abs‘(((ψ‘𝑥) + 1) / 𝑥)))
348282, 323, 324, 300, 347o1le 14173 . . . . . . . 8 (⊤ → (𝑥 ∈ ℝ+ ↦ (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1))) ∈ 𝑂(1))
349 o1const 14140 . . . . . . . . . 10 ((ℝ+ ⊆ ℝ ∧ 1 ∈ ℂ) → (𝑥 ∈ ℝ+ ↦ 1) ∈ 𝑂(1))
35014, 75, 349mp2an 703 . . . . . . . . 9 (𝑥 ∈ ℝ+ ↦ 1) ∈ 𝑂(1)
351350a1i 11 . . . . . . . 8 (⊤ → (𝑥 ∈ ℝ+ ↦ 1) ∈ 𝑂(1))
352300, 301, 348, 351o1sub2 14146 . . . . . . 7 (⊤ → (𝑥 ∈ ℝ+ ↦ ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1)) ∈ 𝑂(1))
353238, 249, 299, 352o1sub2 14146 . . . . . 6 (⊤ → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) − ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1))) ∈ 𝑂(1))
35413, 353o1res2 14084 . . . . 5 (⊤ → (𝑥 ∈ (1[,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) − ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1))) ∈ 𝑂(1))
355232, 354syl5eqelr 2688 . . . 4 (⊤ → (𝑥 ∈ (1[,)+∞) ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) ∈ 𝑂(1))
35616, 355eqeltrd 2683 . . 3 (⊤ → ((𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) ↾ (1[,)+∞)) ∈ 𝑂(1))
357 eqid 2605 . . . . . 6 (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) = (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1))))
358357, 225fmpti 6272 . . . . 5 (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))):ℝ⟶ℂ
359358a1i 11 . . . 4 (⊤ → (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))):ℝ⟶ℂ)
360 ssid 3582 . . . . 5 ℝ ⊆ ℝ
361360a1i 11 . . . 4 (⊤ → ℝ ⊆ ℝ)
362359, 361, 282o1resb 14087 . . 3 (⊤ → ((𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) ∈ 𝑂(1) ↔ ((𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) ↾ (1[,)+∞)) ∈ 𝑂(1)))
363356, 362mpbird 245 . 2 (⊤ → (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) ∈ 𝑂(1))
364363trud 1483 1 (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) ∈ 𝑂(1)
Colors of variables: wff setvar class
Syntax hints:  wb 194  wa 382   = wceq 1474  wtru 1475  wcel 1975  wne 2775  Vcvv 3168  wss 3535   class class class wbr 4573  cmpt 4633  cres 5026  wf 5782  cfv 5786  (class class class)co 6523  𝑓 cof 6766  cc 9786  cr 9787  0cc0 9788  1c1 9789   + caddc 9791   · cmul 9793  +∞cpnf 9923   < clt 9926  cle 9927  cmin 10113  -cneg 10114   / cdiv 10529  cn 10863  2c2 10913  0cn0 11135  cz 11206  cuz 11515  +crp 11660  [,)cico 12000  ...cfz 12148  ..^cfzo 12285  cfl 12404  abscabs 13764  𝑟 crli 14006  𝑂(1)co1 14007  Σcsu 14206  logclog 24018  Λcvma 24531  ψcchp 24532
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-8 1977  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-rep 4689  ax-sep 4699  ax-nul 4708  ax-pow 4760  ax-pr 4824  ax-un 6820  ax-inf2 8394  ax-cnex 9844  ax-resscn 9845  ax-1cn 9846  ax-icn 9847  ax-addcl 9848  ax-addrcl 9849  ax-mulcl 9850  ax-mulrcl 9851  ax-mulcom 9852  ax-addass 9853  ax-mulass 9854  ax-distr 9855  ax-i2m1 9856  ax-1ne0 9857  ax-1rid 9858  ax-rnegex 9859  ax-rrecex 9860  ax-cnre 9861  ax-pre-lttri 9862  ax-pre-lttrn 9863  ax-pre-ltadd 9864  ax-pre-mulgt0 9865  ax-pre-sup 9866  ax-addf 9867  ax-mulf 9868
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2457  df-mo 2458  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-ne 2777  df-nel 2778  df-ral 2896  df-rex 2897  df-reu 2898  df-rmo 2899  df-rab 2900  df-v 3170  df-sbc 3398  df-csb 3495  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-pss 3551  df-nul 3870  df-if 4032  df-pw 4105  df-sn 4121  df-pr 4123  df-tp 4125  df-op 4127  df-uni 4363  df-int 4401  df-iun 4447  df-iin 4448  df-br 4574  df-opab 4634  df-mpt 4635  df-tr 4671  df-eprel 4935  df-id 4939  df-po 4945  df-so 4946  df-fr 4983  df-se 4984  df-we 4985  df-xp 5030  df-rel 5031  df-cnv 5032  df-co 5033  df-dm 5034  df-rn 5035  df-res 5036  df-ima 5037  df-pred 5579  df-ord 5625  df-on 5626  df-lim 5627  df-suc 5628  df-iota 5750  df-fun 5788  df-fn 5789  df-f 5790  df-f1 5791  df-fo 5792  df-f1o 5793  df-fv 5794  df-isom 5795  df-riota 6485  df-ov 6526  df-oprab 6527  df-mpt2 6528  df-of 6768  df-om 6931  df-1st 7032  df-2nd 7033  df-supp 7156  df-wrecs 7267  df-recs 7328  df-rdg 7366  df-1o 7420  df-2o 7421  df-oadd 7424  df-er 7602  df-map 7719  df-pm 7720  df-ixp 7768  df-en 7815  df-dom 7816  df-sdom 7817  df-fin 7818  df-fsupp 8132  df-fi 8173  df-sup 8204  df-inf 8205  df-oi 8271  df-card 8621  df-cda 8846  df-pnf 9928  df-mnf 9929  df-xr 9930  df-ltxr 9931  df-le 9932  df-sub 10115  df-neg 10116  df-div 10530  df-nn 10864  df-2 10922  df-3 10923  df-4 10924  df-5 10925  df-6 10926  df-7 10927  df-8 10928  df-9 10929  df-n0 11136  df-z 11207  df-dec 11322  df-uz 11516  df-q 11617  df-rp 11661  df-xneg 11774  df-xadd 11775  df-xmul 11776  df-ioo 12002  df-ioc 12003  df-ico 12004  df-icc 12005  df-fz 12149  df-fzo 12286  df-fl 12406  df-mod 12482  df-seq 12615  df-exp 12674  df-fac 12874  df-bc 12903  df-hash 12931  df-shft 13597  df-cj 13629  df-re 13630  df-im 13631  df-sqrt 13765  df-abs 13766  df-limsup 13992  df-clim 14009  df-rlim 14010  df-o1 14011  df-lo1 14012  df-sum 14207  df-ef 14579  df-e 14580  df-sin 14581  df-cos 14582  df-pi 14584  df-dvds 14764  df-gcd 14997  df-prm 15166  df-pc 15322  df-struct 15639  df-ndx 15640  df-slot 15641  df-base 15642  df-sets 15643  df-ress 15644  df-plusg 15723  df-mulr 15724  df-starv 15725  df-sca 15726  df-vsca 15727  df-ip 15728  df-tset 15729  df-ple 15730  df-ds 15733  df-unif 15734  df-hom 15735  df-cco 15736  df-rest 15848  df-topn 15849  df-0g 15867  df-gsum 15868  df-topgen 15869  df-pt 15870  df-prds 15873  df-xrs 15927  df-qtop 15932  df-imas 15933  df-xps 15935  df-mre 16011  df-mrc 16012  df-acs 16014  df-mgm 17007  df-sgrp 17049  df-mnd 17060  df-submnd 17101  df-mulg 17306  df-cntz 17515  df-cmn 17960  df-psmet 19501  df-xmet 19502  df-met 19503  df-bl 19504  df-mopn 19505  df-fbas 19506  df-fg 19507  df-cnfld 19510  df-top 20459  df-bases 20460  df-topon 20461  df-topsp 20462  df-cld 20571  df-ntr 20572  df-cls 20573  df-nei 20650  df-lp 20688  df-perf 20689  df-cn 20779  df-cnp 20780  df-haus 20867  df-cmp 20938  df-tx 21113  df-hmeo 21306  df-fil 21398  df-fm 21490  df-flim 21491  df-flf 21492  df-xms 21872  df-ms 21873  df-tms 21874  df-cncf 22416  df-limc 23349  df-dv 23350  df-log 24020  df-cxp 24021  df-em 24432  df-cht 24536  df-vma 24537  df-chp 24538  df-ppi 24539
This theorem is referenced by:  pntrsumbnd  24968
  Copyright terms: Public domain W3C validator