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

Theorem pntrsumo1 25188
 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 9999 . . . . . . . . . . 11 1 ∈ ℝ
2 elicopnf 12227 . . . . . . . . . . 11 (1 ∈ ℝ → (𝑥 ∈ (1[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 1 ≤ 𝑥)))
31, 2ax-mp 5 . . . . . . . . . 10 (𝑥 ∈ (1[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 1 ≤ 𝑥))
43simplbi 476 . . . . . . . . 9 (𝑥 ∈ (1[,)+∞) → 𝑥 ∈ ℝ)
5 0red 10001 . . . . . . . . . 10 (𝑥 ∈ (1[,)+∞) → 0 ∈ ℝ)
6 1red 10015 . . . . . . . . . 10 (𝑥 ∈ (1[,)+∞) → 1 ∈ ℝ)
7 0lt1 10510 . . . . . . . . . . 11 0 < 1
87a1i 11 . . . . . . . . . 10 (𝑥 ∈ (1[,)+∞) → 0 < 1)
93simprbi 480 . . . . . . . . . 10 (𝑥 ∈ (1[,)+∞) → 1 ≤ 𝑥)
105, 6, 4, 8, 9ltletrd 10157 . . . . . . . . 9 (𝑥 ∈ (1[,)+∞) → 0 < 𝑥)
114, 10elrpd 11829 . . . . . . . 8 (𝑥 ∈ (1[,)+∞) → 𝑥 ∈ ℝ+)
1211ssriv 3592 . . . . . . 7 (1[,)+∞) ⊆ ℝ+
1312a1i 11 . . . . . 6 (⊤ → (1[,)+∞) ⊆ ℝ+)
14 rpssre 11803 . . . . . 6 + ⊆ ℝ
1513, 14syl6ss 3600 . . . . 5 (⊤ → (1[,)+∞) ⊆ ℝ)
1615resmptd 5421 . . . 4 (⊤ → ((𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) ↾ (1[,)+∞)) = (𝑥 ∈ (1[,)+∞) ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))))
17 oveq2 6623 . . . . . . . . . . . 12 (𝑚 = 𝑛 → (1 / 𝑚) = (1 / 𝑛))
18 oveq1 6622 . . . . . . . . . . . . . 14 (𝑚 = 𝑛 → (𝑚 − 1) = (𝑛 − 1))
1918fveq2d 6162 . . . . . . . . . . . . 13 (𝑚 = 𝑛 → (ψ‘(𝑚 − 1)) = (ψ‘(𝑛 − 1)))
2019, 18oveq12d 6633 . . . . . . . . . . . 12 (𝑚 = 𝑛 → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = ((ψ‘(𝑛 − 1)) − (𝑛 − 1)))
2117, 20jca 554 . . . . . . . . . . 11 (𝑚 = 𝑛 → ((1 / 𝑚) = (1 / 𝑛) ∧ ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = ((ψ‘(𝑛 − 1)) − (𝑛 − 1))))
22 oveq2 6623 . . . . . . . . . . . 12 (𝑚 = (𝑛 + 1) → (1 / 𝑚) = (1 / (𝑛 + 1)))
23 oveq1 6622 . . . . . . . . . . . . . 14 (𝑚 = (𝑛 + 1) → (𝑚 − 1) = ((𝑛 + 1) − 1))
2423fveq2d 6162 . . . . . . . . . . . . 13 (𝑚 = (𝑛 + 1) → (ψ‘(𝑚 − 1)) = (ψ‘((𝑛 + 1) − 1)))
2524, 23oveq12d 6633 . . . . . . . . . . . 12 (𝑚 = (𝑛 + 1) → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = ((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1)))
2622, 25jca 554 . . . . . . . . . . 11 (𝑚 = (𝑛 + 1) → ((1 / 𝑚) = (1 / (𝑛 + 1)) ∧ ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = ((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1))))
27 oveq2 6623 . . . . . . . . . . . . 13 (𝑚 = 1 → (1 / 𝑚) = (1 / 1))
28 1div1e1 10677 . . . . . . . . . . . . 13 (1 / 1) = 1
2927, 28syl6eq 2671 . . . . . . . . . . . 12 (𝑚 = 1 → (1 / 𝑚) = 1)
30 oveq1 6622 . . . . . . . . . . . . . . . . 17 (𝑚 = 1 → (𝑚 − 1) = (1 − 1))
31 1m1e0 11049 . . . . . . . . . . . . . . . . 17 (1 − 1) = 0
3230, 31syl6eq 2671 . . . . . . . . . . . . . . . 16 (𝑚 = 1 → (𝑚 − 1) = 0)
3332fveq2d 6162 . . . . . . . . . . . . . . 15 (𝑚 = 1 → (ψ‘(𝑚 − 1)) = (ψ‘0))
34 2pos 11072 . . . . . . . . . . . . . . . 16 0 < 2
35 0re 10000 . . . . . . . . . . . . . . . . 17 0 ∈ ℝ
36 chpeq0 24867 . . . . . . . . . . . . . . . . 17 (0 ∈ ℝ → ((ψ‘0) = 0 ↔ 0 < 2))
3735, 36ax-mp 5 . . . . . . . . . . . . . . . 16 ((ψ‘0) = 0 ↔ 0 < 2)
3834, 37mpbir 221 . . . . . . . . . . . . . . 15 (ψ‘0) = 0
3933, 38syl6eq 2671 . . . . . . . . . . . . . 14 (𝑚 = 1 → (ψ‘(𝑚 − 1)) = 0)
4039, 32oveq12d 6633 . . . . . . . . . . . . 13 (𝑚 = 1 → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = (0 − 0))
41 0m0e0 11090 . . . . . . . . . . . . 13 (0 − 0) = 0
4240, 41syl6eq 2671 . . . . . . . . . . . 12 (𝑚 = 1 → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = 0)
4329, 42jca 554 . . . . . . . . . . 11 (𝑚 = 1 → ((1 / 𝑚) = 1 ∧ ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = 0))
44 oveq2 6623 . . . . . . . . . . . 12 (𝑚 = ((⌊‘𝑥) + 1) → (1 / 𝑚) = (1 / ((⌊‘𝑥) + 1)))
45 oveq1 6622 . . . . . . . . . . . . . 14 (𝑚 = ((⌊‘𝑥) + 1) → (𝑚 − 1) = (((⌊‘𝑥) + 1) − 1))
4645fveq2d 6162 . . . . . . . . . . . . 13 (𝑚 = ((⌊‘𝑥) + 1) → (ψ‘(𝑚 − 1)) = (ψ‘(((⌊‘𝑥) + 1) − 1)))
4746, 45oveq12d 6633 . . . . . . . . . . . 12 (𝑚 = ((⌊‘𝑥) + 1) → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = ((ψ‘(((⌊‘𝑥) + 1) − 1)) − (((⌊‘𝑥) + 1) − 1)))
4844, 47jca 554 . . . . . . . . . . 11 (𝑚 = ((⌊‘𝑥) + 1) → ((1 / 𝑚) = (1 / ((⌊‘𝑥) + 1)) ∧ ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) = ((ψ‘(((⌊‘𝑥) + 1) − 1)) − (((⌊‘𝑥) + 1) − 1))))
4911rprege0d 11839 . . . . . . . . . . . . . 14 (𝑥 ∈ (1[,)+∞) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
50 flge0nn0 12577 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℝ ∧ 0 ≤ 𝑥) → (⌊‘𝑥) ∈ ℕ0)
5149, 50syl 17 . . . . . . . . . . . . 13 (𝑥 ∈ (1[,)+∞) → (⌊‘𝑥) ∈ ℕ0)
52 nn0p1nn 11292 . . . . . . . . . . . . 13 ((⌊‘𝑥) ∈ ℕ0 → ((⌊‘𝑥) + 1) ∈ ℕ)
5351, 52syl 17 . . . . . . . . . . . 12 (𝑥 ∈ (1[,)+∞) → ((⌊‘𝑥) + 1) ∈ ℕ)
54 nnuz 11683 . . . . . . . . . . . 12 ℕ = (ℤ‘1)
5553, 54syl6eleq 2708 . . . . . . . . . . 11 (𝑥 ∈ (1[,)+∞) → ((⌊‘𝑥) + 1) ∈ (ℤ‘1))
56 elfznn 12328 . . . . . . . . . . . . . 14 (𝑚 ∈ (1...((⌊‘𝑥) + 1)) → 𝑚 ∈ ℕ)
5756adantl 482 . . . . . . . . . . . . 13 ((𝑥 ∈ (1[,)+∞) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 𝑚 ∈ ℕ)
5857nnrecred 11026 . . . . . . . . . . . 12 ((𝑥 ∈ (1[,)+∞) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (1 / 𝑚) ∈ ℝ)
5958recnd 10028 . . . . . . . . . . 11 ((𝑥 ∈ (1[,)+∞) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (1 / 𝑚) ∈ ℂ)
6057nnred 10995 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → 𝑚 ∈ ℝ)
61 peano2rem 10308 . . . . . . . . . . . . . . 15 (𝑚 ∈ ℝ → (𝑚 − 1) ∈ ℝ)
6260, 61syl 17 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (𝑚 − 1) ∈ ℝ)
63 chpcl 24784 . . . . . . . . . . . . . 14 ((𝑚 − 1) ∈ ℝ → (ψ‘(𝑚 − 1)) ∈ ℝ)
6462, 63syl 17 . . . . . . . . . . . . 13 ((𝑥 ∈ (1[,)+∞) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → (ψ‘(𝑚 − 1)) ∈ ℝ)
6564, 62resubcld 10418 . . . . . . . . . . . 12 ((𝑥 ∈ (1[,)+∞) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) ∈ ℝ)
6665recnd 10028 . . . . . . . . . . 11 ((𝑥 ∈ (1[,)+∞) ∧ 𝑚 ∈ (1...((⌊‘𝑥) + 1))) → ((ψ‘(𝑚 − 1)) − (𝑚 − 1)) ∈ ℂ)
6721, 26, 43, 48, 55, 59, 66fsumparts 14484 . . . . . . . . . 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 12555 . . . . . . . . . . . . 13 (𝑥 ∈ (1[,)+∞) → (⌊‘𝑥) ∈ ℤ)
69 fzval3 12493 . . . . . . . . . . . . 13 ((⌊‘𝑥) ∈ ℤ → (1...(⌊‘𝑥)) = (1..^((⌊‘𝑥) + 1)))
7068, 69syl 17 . . . . . . . . . . . 12 (𝑥 ∈ (1[,)+∞) → (1...(⌊‘𝑥)) = (1..^((⌊‘𝑥) + 1)))
7170eqcomd 2627 . . . . . . . . . . 11 (𝑥 ∈ (1[,)+∞) → (1..^((⌊‘𝑥) + 1)) = (1...(⌊‘𝑥)))
72 elfznn 12328 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
7372adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
7473nncnd 10996 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℂ)
75 ax-1cn 9954 . . . . . . . . . . . . . . . . . . 19 1 ∈ ℂ
76 pncan 10247 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛 + 1) − 1) = 𝑛)
7774, 75, 76sylancl 693 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) − 1) = 𝑛)
7873nnred 10995 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ)
7977, 78eqeltrd 2698 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) − 1) ∈ ℝ)
80 chpcl 24784 . . . . . . . . . . . . . . . . 17 (((𝑛 + 1) − 1) ∈ ℝ → (ψ‘((𝑛 + 1) − 1)) ∈ ℝ)
8179, 80syl 17 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (ψ‘((𝑛 + 1) − 1)) ∈ ℝ)
8281recnd 10028 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (ψ‘((𝑛 + 1) − 1)) ∈ ℂ)
8379recnd 10028 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) − 1) ∈ ℂ)
84 peano2rem 10308 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℝ → (𝑛 − 1) ∈ ℝ)
8578, 84syl 17 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 − 1) ∈ ℝ)
86 chpcl 24784 . . . . . . . . . . . . . . . . 17 ((𝑛 − 1) ∈ ℝ → (ψ‘(𝑛 − 1)) ∈ ℝ)
8785, 86syl 17 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (ψ‘(𝑛 − 1)) ∈ ℝ)
8887recnd 10028 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (ψ‘(𝑛 − 1)) ∈ ℂ)
89 1cnd 10016 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℂ)
9074, 89subcld 10352 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 − 1) ∈ ℂ)
9182, 83, 88, 90sub4d 10401 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1)) − ((ψ‘(𝑛 − 1)) − (𝑛 − 1))) = (((ψ‘((𝑛 + 1) − 1)) − (ψ‘(𝑛 − 1))) − (((𝑛 + 1) − 1) − (𝑛 − 1))))
92 nnm1nn0 11294 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ → (𝑛 − 1) ∈ ℕ0)
9373, 92syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 − 1) ∈ ℕ0)
94 chpp1 24815 . . . . . . . . . . . . . . . . . . 19 ((𝑛 − 1) ∈ ℕ0 → (ψ‘((𝑛 − 1) + 1)) = ((ψ‘(𝑛 − 1)) + (Λ‘((𝑛 − 1) + 1))))
9593, 94syl 17 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (ψ‘((𝑛 − 1) + 1)) = ((ψ‘(𝑛 − 1)) + (Λ‘((𝑛 − 1) + 1))))
96 npcan 10250 . . . . . . . . . . . . . . . . . . . . 21 ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛 − 1) + 1) = 𝑛)
9774, 75, 96sylancl 693 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 − 1) + 1) = 𝑛)
9897, 77eqtr4d 2658 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 − 1) + 1) = ((𝑛 + 1) − 1))
9998fveq2d 6162 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (ψ‘((𝑛 − 1) + 1)) = (ψ‘((𝑛 + 1) − 1)))
10097fveq2d 6162 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘((𝑛 − 1) + 1)) = (Λ‘𝑛))
101100oveq2d 6631 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((ψ‘(𝑛 − 1)) + (Λ‘((𝑛 − 1) + 1))) = ((ψ‘(𝑛 − 1)) + (Λ‘𝑛)))
10295, 99, 1013eqtr3d 2663 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (ψ‘((𝑛 + 1) − 1)) = ((ψ‘(𝑛 − 1)) + (Λ‘𝑛)))
103102oveq1d 6630 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((ψ‘((𝑛 + 1) − 1)) − (ψ‘(𝑛 − 1))) = (((ψ‘(𝑛 − 1)) + (Λ‘𝑛)) − (ψ‘(𝑛 − 1))))
104 vmacl 24778 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → (Λ‘𝑛) ∈ ℝ)
10573, 104syl 17 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈ ℝ)
106105recnd 10028 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈ ℂ)
10788, 106pncan2d 10354 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((ψ‘(𝑛 − 1)) + (Λ‘𝑛)) − (ψ‘(𝑛 − 1))) = (Λ‘𝑛))
108103, 107eqtrd 2655 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((ψ‘((𝑛 + 1) − 1)) − (ψ‘(𝑛 − 1))) = (Λ‘𝑛))
109 peano2cn 10168 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℂ → (𝑛 + 1) ∈ ℂ)
11074, 109syl 17 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 + 1) ∈ ℂ)
111110, 74, 89nnncan2d 10387 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑛 + 1) − 1) − (𝑛 − 1)) = ((𝑛 + 1) − 𝑛))
112 pncan2 10248 . . . . . . . . . . . . . . . . 17 ((𝑛 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑛 + 1) − 𝑛) = 1)
11374, 75, 112sylancl 693 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) − 𝑛) = 1)
114111, 113eqtrd 2655 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑛 + 1) − 1) − (𝑛 − 1)) = 1)
115108, 114oveq12d 6633 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((ψ‘((𝑛 + 1) − 1)) − (ψ‘(𝑛 − 1))) − (((𝑛 + 1) − 1) − (𝑛 − 1))) = ((Λ‘𝑛) − 1))
11691, 115eqtrd 2655 . . . . . . . . . . . . 13 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1)) − ((ψ‘(𝑛 − 1)) − (𝑛 − 1))) = ((Λ‘𝑛) − 1))
117116oveq2d 6631 . . . . . . . . . . . 12 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 / 𝑛) · (((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1)) − ((ψ‘(𝑛 − 1)) − (𝑛 − 1)))) = ((1 / 𝑛) · ((Λ‘𝑛) − 1)))
118 peano2rem 10308 . . . . . . . . . . . . . . 15 ((Λ‘𝑛) ∈ ℝ → ((Λ‘𝑛) − 1) ∈ ℝ)
119105, 118syl 17 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) − 1) ∈ ℝ)
120119recnd 10028 . . . . . . . . . . . . 13 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) − 1) ∈ ℂ)
12173nnne0d 11025 . . . . . . . . . . . . 13 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ≠ 0)
122120, 74, 121divrec2d 10765 . . . . . . . . . . . 12 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) − 1) / 𝑛) = ((1 / 𝑛) · ((Λ‘𝑛) − 1)))
123117, 122eqtr4d 2658 . . . . . . . . . . 11 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 / 𝑛) · (((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1)) − ((ψ‘(𝑛 − 1)) − (𝑛 − 1)))) = (((Λ‘𝑛) − 1) / 𝑛))
12471, 123sumeq12rdv 14387 . . . . . . . . . 10 (𝑥 ∈ (1[,)+∞) → Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))((1 / 𝑛) · (((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1)) − ((ψ‘(𝑛 − 1)) − (𝑛 − 1)))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛))
12551nn0cnd 11313 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (1[,)+∞) → (⌊‘𝑥) ∈ ℂ)
126 pncan 10247 . . . . . . . . . . . . . . . . . . . 20 (((⌊‘𝑥) ∈ ℂ ∧ 1 ∈ ℂ) → (((⌊‘𝑥) + 1) − 1) = (⌊‘𝑥))
127125, 75, 126sylancl 693 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (1[,)+∞) → (((⌊‘𝑥) + 1) − 1) = (⌊‘𝑥))
128127fveq2d 6162 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (1[,)+∞) → (ψ‘(((⌊‘𝑥) + 1) − 1)) = (ψ‘(⌊‘𝑥)))
129 chpfl 24810 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℝ → (ψ‘(⌊‘𝑥)) = (ψ‘𝑥))
1304, 129syl 17 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (1[,)+∞) → (ψ‘(⌊‘𝑥)) = (ψ‘𝑥))
131128, 130eqtrd 2655 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (1[,)+∞) → (ψ‘(((⌊‘𝑥) + 1) − 1)) = (ψ‘𝑥))
132131oveq1d 6630 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1[,)+∞) → ((ψ‘(((⌊‘𝑥) + 1) − 1)) − (((⌊‘𝑥) + 1) − 1)) = ((ψ‘𝑥) − (((⌊‘𝑥) + 1) − 1)))
133 chpcl 24784 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℝ → (ψ‘𝑥) ∈ ℝ)
1344, 133syl 17 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (1[,)+∞) → (ψ‘𝑥) ∈ ℝ)
135134recnd 10028 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (1[,)+∞) → (ψ‘𝑥) ∈ ℂ)
13653nncnd 10996 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (1[,)+∞) → ((⌊‘𝑥) + 1) ∈ ℂ)
137 1cnd 10016 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (1[,)+∞) → 1 ∈ ℂ)
138135, 136, 137subsub3d 10382 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1[,)+∞) → ((ψ‘𝑥) − (((⌊‘𝑥) + 1) − 1)) = (((ψ‘𝑥) + 1) − ((⌊‘𝑥) + 1)))
139132, 138eqtrd 2655 . . . . . . . . . . . . . . 15 (𝑥 ∈ (1[,)+∞) → ((ψ‘(((⌊‘𝑥) + 1) − 1)) − (((⌊‘𝑥) + 1) − 1)) = (((ψ‘𝑥) + 1) − ((⌊‘𝑥) + 1)))
140139oveq2d 6631 . . . . . . . . . . . . . 14 (𝑥 ∈ (1[,)+∞) → ((1 / ((⌊‘𝑥) + 1)) · ((ψ‘(((⌊‘𝑥) + 1) − 1)) − (((⌊‘𝑥) + 1) − 1))) = ((1 / ((⌊‘𝑥) + 1)) · (((ψ‘𝑥) + 1) − ((⌊‘𝑥) + 1))))
14153nnrecred 11026 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1[,)+∞) → (1 / ((⌊‘𝑥) + 1)) ∈ ℝ)
142141recnd 10028 . . . . . . . . . . . . . . 15 (𝑥 ∈ (1[,)+∞) → (1 / ((⌊‘𝑥) + 1)) ∈ ℂ)
143 peano2cn 10168 . . . . . . . . . . . . . . . 16 ((ψ‘𝑥) ∈ ℂ → ((ψ‘𝑥) + 1) ∈ ℂ)
144135, 143syl 17 . . . . . . . . . . . . . . 15 (𝑥 ∈ (1[,)+∞) → ((ψ‘𝑥) + 1) ∈ ℂ)
145142, 144, 136subdid 10446 . . . . . . . . . . . . . 14 (𝑥 ∈ (1[,)+∞) → ((1 / ((⌊‘𝑥) + 1)) · (((ψ‘𝑥) + 1) − ((⌊‘𝑥) + 1))) = (((1 / ((⌊‘𝑥) + 1)) · ((ψ‘𝑥) + 1)) − ((1 / ((⌊‘𝑥) + 1)) · ((⌊‘𝑥) + 1))))
14653nnne0d 11025 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (1[,)+∞) → ((⌊‘𝑥) + 1) ≠ 0)
147144, 136, 146divrec2d 10765 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1[,)+∞) → (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) = ((1 / ((⌊‘𝑥) + 1)) · ((ψ‘𝑥) + 1)))
148147eqcomd 2627 . . . . . . . . . . . . . . 15 (𝑥 ∈ (1[,)+∞) → ((1 / ((⌊‘𝑥) + 1)) · ((ψ‘𝑥) + 1)) = (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)))
149136, 146recid2d 10757 . . . . . . . . . . . . . . 15 (𝑥 ∈ (1[,)+∞) → ((1 / ((⌊‘𝑥) + 1)) · ((⌊‘𝑥) + 1)) = 1)
150148, 149oveq12d 6633 . . . . . . . . . . . . . 14 (𝑥 ∈ (1[,)+∞) → (((1 / ((⌊‘𝑥) + 1)) · ((ψ‘𝑥) + 1)) − ((1 / ((⌊‘𝑥) + 1)) · ((⌊‘𝑥) + 1))) = ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1))
151140, 145, 1503eqtrd 2659 . . . . . . . . . . . . 13 (𝑥 ∈ (1[,)+∞) → ((1 / ((⌊‘𝑥) + 1)) · ((ψ‘(((⌊‘𝑥) + 1) − 1)) − (((⌊‘𝑥) + 1) − 1))) = ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1))
15275mul01i 10186 . . . . . . . . . . . . . 14 (1 · 0) = 0
153152a1i 11 . . . . . . . . . . . . 13 (𝑥 ∈ (1[,)+∞) → (1 · 0) = 0)
154151, 153oveq12d 6633 . . . . . . . . . . . 12 (𝑥 ∈ (1[,)+∞) → (((1 / ((⌊‘𝑥) + 1)) · ((ψ‘(((⌊‘𝑥) + 1) − 1)) − (((⌊‘𝑥) + 1) − 1))) − (1 · 0)) = (((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) − 0))
155 peano2re 10169 . . . . . . . . . . . . . . . . 17 ((ψ‘𝑥) ∈ ℝ → ((ψ‘𝑥) + 1) ∈ ℝ)
156134, 155syl 17 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1[,)+∞) → ((ψ‘𝑥) + 1) ∈ ℝ)
157156, 53nndivred 11029 . . . . . . . . . . . . . . 15 (𝑥 ∈ (1[,)+∞) → (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ∈ ℝ)
158157recnd 10028 . . . . . . . . . . . . . 14 (𝑥 ∈ (1[,)+∞) → (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ∈ ℂ)
159 subcl 10240 . . . . . . . . . . . . . 14 (((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ∈ ℂ ∧ 1 ∈ ℂ) → ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) ∈ ℂ)
160158, 75, 159sylancl 693 . . . . . . . . . . . . 13 (𝑥 ∈ (1[,)+∞) → ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) ∈ ℂ)
161160subid1d 10341 . . . . . . . . . . . 12 (𝑥 ∈ (1[,)+∞) → (((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) − 0) = ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1))
162154, 161eqtrd 2655 . . . . . . . . . . 11 (𝑥 ∈ (1[,)+∞) → (((1 / ((⌊‘𝑥) + 1)) · ((ψ‘(((⌊‘𝑥) + 1) − 1)) − (((⌊‘𝑥) + 1) − 1))) − (1 · 0)) = ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1))
163 peano2nn 10992 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ → (𝑛 + 1) ∈ ℕ)
164 nnmulcl 11003 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℕ ∧ (𝑛 + 1) ∈ ℕ) → (𝑛 · (𝑛 + 1)) ∈ ℕ)
165163, 164mpdan 701 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → (𝑛 · (𝑛 + 1)) ∈ ℕ)
16673, 165syl 17 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 · (𝑛 + 1)) ∈ ℕ)
167166nnrecred 11026 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / (𝑛 · (𝑛 + 1))) ∈ ℝ)
168167recnd 10028 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / (𝑛 · (𝑛 + 1))) ∈ ℂ)
169 nnrp 11802 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ → 𝑛 ∈ ℝ+)
170 pntrval.r . . . . . . . . . . . . . . . . . . . 20 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))
171170pntrf 25186 . . . . . . . . . . . . . . . . . . 19 𝑅:ℝ+⟶ℝ
172171ffvelrni 6324 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℝ+ → (𝑅𝑛) ∈ ℝ)
173169, 172syl 17 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ → (𝑅𝑛) ∈ ℝ)
17473, 173syl 17 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅𝑛) ∈ ℝ)
175174recnd 10028 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅𝑛) ∈ ℂ)
176168, 175mulneg1d 10443 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (-(1 / (𝑛 · (𝑛 + 1))) · (𝑅𝑛)) = -((1 / (𝑛 · (𝑛 + 1))) · (𝑅𝑛)))
17774, 89mulcld 10020 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 · 1) ∈ ℂ)
17874, 110mulcld 10020 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 · (𝑛 + 1)) ∈ ℂ)
179166nnne0d 11025 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 · (𝑛 + 1)) ≠ 0)
180110, 177, 178, 179divsubdird 10800 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑛 + 1) − (𝑛 · 1)) / (𝑛 · (𝑛 + 1))) = (((𝑛 + 1) / (𝑛 · (𝑛 + 1))) − ((𝑛 · 1) / (𝑛 · (𝑛 + 1)))))
18174mulid1d 10017 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 · 1) = 𝑛)
182181oveq2d 6631 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) − (𝑛 · 1)) = ((𝑛 + 1) − 𝑛))
183182, 113eqtrd 2655 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) − (𝑛 · 1)) = 1)
184183oveq1d 6630 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑛 + 1) − (𝑛 · 1)) / (𝑛 · (𝑛 + 1))) = (1 / (𝑛 · (𝑛 + 1))))
185110mulid1d 10017 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) · 1) = (𝑛 + 1))
186110, 74mulcomd 10021 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) · 𝑛) = (𝑛 · (𝑛 + 1)))
187185, 186oveq12d 6633 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑛 + 1) · 1) / ((𝑛 + 1) · 𝑛)) = ((𝑛 + 1) / (𝑛 · (𝑛 + 1))))
18873, 163syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 + 1) ∈ ℕ)
189188nnne0d 11025 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 + 1) ≠ 0)
19089, 74, 110, 121, 189divcan5d 10787 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑛 + 1) · 1) / ((𝑛 + 1) · 𝑛)) = (1 / 𝑛))
191187, 190eqtr3d 2657 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) / (𝑛 · (𝑛 + 1))) = (1 / 𝑛))
19289, 110, 74, 189, 121divcan5d 10787 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 · 1) / (𝑛 · (𝑛 + 1))) = (1 / (𝑛 + 1)))
193191, 192oveq12d 6633 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑛 + 1) / (𝑛 · (𝑛 + 1))) − ((𝑛 · 1) / (𝑛 · (𝑛 + 1)))) = ((1 / 𝑛) − (1 / (𝑛 + 1))))
194180, 184, 1933eqtr3d 2663 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / (𝑛 · (𝑛 + 1))) = ((1 / 𝑛) − (1 / (𝑛 + 1))))
195194negeqd 10235 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → -(1 / (𝑛 · (𝑛 + 1))) = -((1 / 𝑛) − (1 / (𝑛 + 1))))
19673nnrecred 11026 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / 𝑛) ∈ ℝ)
197196recnd 10028 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / 𝑛) ∈ ℂ)
198188nnrecred 11026 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / (𝑛 + 1)) ∈ ℝ)
199198recnd 10028 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / (𝑛 + 1)) ∈ ℂ)
200197, 199negsubdi2d 10368 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → -((1 / 𝑛) − (1 / (𝑛 + 1))) = ((1 / (𝑛 + 1)) − (1 / 𝑛)))
201195, 200eqtr2d 2656 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 / (𝑛 + 1)) − (1 / 𝑛)) = -(1 / (𝑛 · (𝑛 + 1))))
20273nnrpd 11830 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ+)
20377, 202eqeltrd 2698 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑛 + 1) − 1) ∈ ℝ+)
204170pntrval 25185 . . . . . . . . . . . . . . . . 17 (((𝑛 + 1) − 1) ∈ ℝ+ → (𝑅‘((𝑛 + 1) − 1)) = ((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1)))
205203, 204syl 17 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘((𝑛 + 1) − 1)) = ((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1)))
20677fveq2d 6162 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘((𝑛 + 1) − 1)) = (𝑅𝑛))
207205, 206eqtr3d 2657 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1)) = (𝑅𝑛))
208201, 207oveq12d 6633 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((1 / (𝑛 + 1)) − (1 / 𝑛)) · ((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1))) = (-(1 / (𝑛 · (𝑛 + 1))) · (𝑅𝑛)))
209175, 178, 179divrec2d 10765 . . . . . . . . . . . . . . 15 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑅𝑛) / (𝑛 · (𝑛 + 1))) = ((1 / (𝑛 · (𝑛 + 1))) · (𝑅𝑛)))
210209negeqd 10235 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → -((𝑅𝑛) / (𝑛 · (𝑛 + 1))) = -((1 / (𝑛 · (𝑛 + 1))) · (𝑅𝑛)))
211176, 208, 2103eqtr4d 2665 . . . . . . . . . . . . 13 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((1 / (𝑛 + 1)) − (1 / 𝑛)) · ((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1))) = -((𝑅𝑛) / (𝑛 · (𝑛 + 1))))
21271, 211sumeq12rdv 14387 . . . . . . . . . . . 12 (𝑥 ∈ (1[,)+∞) → Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))(((1 / (𝑛 + 1)) − (1 / 𝑛)) · ((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1))) = Σ𝑛 ∈ (1...(⌊‘𝑥))-((𝑅𝑛) / (𝑛 · (𝑛 + 1))))
213 fzfid 12728 . . . . . . . . . . . . 13 (𝑥 ∈ (1[,)+∞) → (1...(⌊‘𝑥)) ∈ Fin)
214173, 165nndivred 11029 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → ((𝑅𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ)
21573, 214syl 17 . . . . . . . . . . . . . 14 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑅𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ)
216215recnd 10028 . . . . . . . . . . . . 13 ((𝑥 ∈ (1[,)+∞) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑅𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ)
217213, 216fsumneg 14466 . . . . . . . . . . . 12 (𝑥 ∈ (1[,)+∞) → Σ𝑛 ∈ (1...(⌊‘𝑥))-((𝑅𝑛) / (𝑛 · (𝑛 + 1))) = -Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1))))
218212, 217eqtrd 2655 . . . . . . . . . . 11 (𝑥 ∈ (1[,)+∞) → Σ𝑛 ∈ (1..^((⌊‘𝑥) + 1))(((1 / (𝑛 + 1)) − (1 / 𝑛)) · ((ψ‘((𝑛 + 1) − 1)) − ((𝑛 + 1) − 1))) = -Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1))))
219162, 218oveq12d 6633 . . . . . . . . . 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 2663 . . . . . . . . 9 (𝑥 ∈ (1[,)+∞) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) = (((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) − -Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))))
221 fzfid 12728 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → (1...(⌊‘𝑥)) ∈ Fin)
22272adantl 482 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℝ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
223222, 214syl 17 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑅𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ)
224221, 223fsumrecl 14414 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℝ)
225224recnd 10028 . . . . . . . . . . 11 (𝑥 ∈ ℝ → Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ)
2264, 225syl 17 . . . . . . . . . 10 (𝑥 ∈ (1[,)+∞) → Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1))) ∈ ℂ)
227160, 226subnegd 10359 . . . . . . . . 9 (𝑥 ∈ (1[,)+∞) → (((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) − -Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) = (((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) + Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))))
228220, 227eqtrd 2655 . . . . . . . 8 (𝑥 ∈ (1[,)+∞) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) = (((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) + Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))))
229228oveq1d 6630 . . . . . . 7 (𝑥 ∈ (1[,)+∞) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) − ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1)) = ((((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) + Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) − ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1)))
230160, 226pncan2d 10354 . . . . . . 7 (𝑥 ∈ (1[,)+∞) → ((((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) + Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) − ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1)) = Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1))))
231229, 230eqtrd 2655 . . . . . 6 (𝑥 ∈ (1[,)+∞) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) − ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1)) = Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1))))
232231mpteq2ia 4710 . . . . 5 (𝑥 ∈ (1[,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) − ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1))) = (𝑥 ∈ (1[,)+∞) ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1))))
233 fzfid 12728 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ ℝ+) → (1...(⌊‘𝑥)) ∈ Fin)
23472adantl 482 . . . . . . . . . . 11 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
235234, 104syl 17 . . . . . . . . . 10 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈ ℝ)
236235, 118syl 17 . . . . . . . . 9 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) − 1) ∈ ℝ)
237236, 234nndivred 11029 . . . . . . . 8 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) − 1) / 𝑛) ∈ ℝ)
238233, 237fsumrecl 14414 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) ∈ ℝ)
239 rpre 11799 . . . . . . . . . . . 12 (𝑥 ∈ ℝ+𝑥 ∈ ℝ)
240239adantl 482 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ)
241240, 133syl 17 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℝ+) → (ψ‘𝑥) ∈ ℝ)
242241, 155syl 17 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((ψ‘𝑥) + 1) ∈ ℝ)
243 rprege0 11807 . . . . . . . . . . . 12 (𝑥 ∈ ℝ+ → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥))
244243, 50syl 17 . . . . . . . . . . 11 (𝑥 ∈ ℝ+ → (⌊‘𝑥) ∈ ℕ0)
245244adantl 482 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℝ+) → (⌊‘𝑥) ∈ ℕ0)
246245, 52syl 17 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((⌊‘𝑥) + 1) ∈ ℕ)
247242, 246nndivred 11029 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ∈ ℝ)
248 peano2rem 10308 . . . . . . . 8 ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ∈ ℝ → ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) ∈ ℝ)
249247, 248syl 17 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1) ∈ ℝ)
250 reex 9987 . . . . . . . . . . . 12 ℝ ∈ V
251250, 14ssexi 4773 . . . . . . . . . . 11 + ∈ V
252251a1i 11 . . . . . . . . . 10 (⊤ → ℝ+ ∈ V)
253235, 234nndivred 11029 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) / 𝑛) ∈ ℝ)
254253recnd 10028 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) / 𝑛) ∈ ℂ)
255233, 254fsumcl 14413 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ∈ ℂ)
256 relogcl 24260 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ+ → (log‘𝑥) ∈ ℝ)
257256adantl 482 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℝ)
258257recnd 10028 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℂ)
259255, 258subcld 10352 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) ∈ ℂ)
260234nnrecred 11026 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / 𝑛) ∈ ℝ)
261233, 260fsumrecl 14414 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) ∈ ℝ)
262261, 257resubcld 10418 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)) ∈ ℝ)
263 eqidd 2622 . . . . . . . . . 10 (⊤ → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) = (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))))
264 eqidd 2622 . . . . . . . . . 10 (⊤ → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) = (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))))
265252, 259, 262, 263, 264offval2 6879 . . . . . . . . 9 (⊤ → ((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘𝑓 − (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)))) = (𝑥 ∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)))))
266260recnd 10028 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / 𝑛) ∈ ℂ)
267233, 254, 266fsumsub 14467 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) − (1 / 𝑛)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛)))
268235recnd 10028 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈ ℂ)
269 1cnd 10016 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℂ)
270234nncnd 10996 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℂ)
271234nnne0d 11025 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ≠ 0)
272268, 269, 270, 271divsubdird 10800 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) − 1) / 𝑛) = (((Λ‘𝑛) / 𝑛) − (1 / 𝑛)))
273272sumeq2dv 14383 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) − (1 / 𝑛)))
274261recnd 10028 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) ∈ ℂ)
275255, 274, 258nnncan2d 10387 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛)))
276267, 273, 2753eqtr4rd 2666 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛))
277276mpteq2dva 4714 . . . . . . . . 9 (⊤ → (𝑥 ∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)))) = (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛)))
278265, 277eqtrd 2655 . . . . . . . 8 (⊤ → ((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘𝑓 − (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)))) = (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛)))
279 vmadivsum 25105 . . . . . . . . 9 (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1)
28014a1i 11 . . . . . . . . . 10 (⊤ → ℝ+ ⊆ ℝ)
281262recnd 10028 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)) ∈ ℂ)
282 1red 10015 . . . . . . . . . 10 (⊤ → 1 ∈ ℝ)
283 harmoniclbnd 24669 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ+ → (log‘𝑥) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛))
284283adantl 482 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℝ+) → (log‘𝑥) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛))
285257, 261, 284abssubge0d 14120 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)))
286285adantrr 752 . . . . . . . . . . 11 ((⊤ ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)))
287239ad2antrl 763 . . . . . . . . . . . . 13 ((⊤ ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ)
288 simprr 795 . . . . . . . . . . . . 13 ((⊤ ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ≤ 𝑥)
289 harmonicubnd 24670 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) ≤ ((log‘𝑥) + 1))
290287, 288, 289syl2anc 692 . . . . . . . . . . . 12 ((⊤ ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) ≤ ((log‘𝑥) + 1))
291 1red 10015 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ ℝ+) → 1 ∈ ℝ)
292261, 257, 291lesubadd2d 10586 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)) ≤ 1 ↔ Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) ≤ ((log‘𝑥) + 1)))
293292adantrr 752 . . . . . . . . . . . 12 ((⊤ ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)) ≤ 1 ↔ Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) ≤ ((log‘𝑥) + 1)))
294290, 293mpbird 247 . . . . . . . . . . 11 ((⊤ ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)) ≤ 1)
295286, 294eqbrtrd 4645 . . . . . . . . . 10 ((⊤ ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) ≤ 1)
296280, 281, 282, 282, 295elo1d 14217 . . . . . . . . 9 (⊤ → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) ∈ 𝑂(1))
297 o1sub 14296 . . . . . . . . 9 (((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1) ∧ (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥))) ∈ 𝑂(1)) → ((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘𝑓 − (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)))) ∈ 𝑂(1))
298279, 296, 297sylancr 694 . . . . . . . 8 (⊤ → ((𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘𝑓 − (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) − (log‘𝑥)))) ∈ 𝑂(1))
299278, 298eqeltrrd 2699 . . . . . . 7 (⊤ → (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛)) ∈ 𝑂(1))
300247recnd 10028 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ∈ ℂ)
301 1cnd 10016 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ ℝ+) → 1 ∈ ℂ)
302241recnd 10028 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → (ψ‘𝑥) ∈ ℂ)
303 rpcnne0 11810 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ+ → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
304303adantl 482 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
305 divdir 10670 . . . . . . . . . . . 12 (((ψ‘𝑥) ∈ ℂ ∧ 1 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → (((ψ‘𝑥) + 1) / 𝑥) = (((ψ‘𝑥) / 𝑥) + (1 / 𝑥)))
306302, 301, 304, 305syl3anc 1323 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) + 1) / 𝑥) = (((ψ‘𝑥) / 𝑥) + (1 / 𝑥)))
307306mpteq2dva 4714 . . . . . . . . . 10 (⊤ → (𝑥 ∈ ℝ+ ↦ (((ψ‘𝑥) + 1) / 𝑥)) = (𝑥 ∈ ℝ+ ↦ (((ψ‘𝑥) / 𝑥) + (1 / 𝑥))))
308 simpr 477 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ+)
309241, 308rerpdivcld 11863 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((ψ‘𝑥) / 𝑥) ∈ ℝ)
310 rpreccl 11817 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ+ → (1 / 𝑥) ∈ ℝ+)
311310adantl 482 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → (1 / 𝑥) ∈ ℝ+)
312 eqidd 2622 . . . . . . . . . . . 12 (⊤ → (𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) = (𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)))
313 eqidd 2622 . . . . . . . . . . . 12 (⊤ → (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) = (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)))
314252, 309, 311, 312, 313offval2 6879 . . . . . . . . . . 11 (⊤ → ((𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∘𝑓 + (𝑥 ∈ ℝ+ ↦ (1 / 𝑥))) = (𝑥 ∈ ℝ+ ↦ (((ψ‘𝑥) / 𝑥) + (1 / 𝑥))))
315 chpo1ub 25103 . . . . . . . . . . . 12 (𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∈ 𝑂(1)
316 divrcnv 14528 . . . . . . . . . . . . . 14 (1 ∈ ℂ → (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) ⇝𝑟 0)
31775, 316ax-mp 5 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) ⇝𝑟 0
318 rlimo1 14297 . . . . . . . . . . . . 13 ((𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) ⇝𝑟 0 → (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) ∈ 𝑂(1))
319317, 318mp1i 13 . . . . . . . . . . . 12 (⊤ → (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) ∈ 𝑂(1))
320 o1add 14294 . . . . . . . . . . . 12 (((𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∈ 𝑂(1) ∧ (𝑥 ∈ ℝ+ ↦ (1 / 𝑥)) ∈ 𝑂(1)) → ((𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∘𝑓 + (𝑥 ∈ ℝ+ ↦ (1 / 𝑥))) ∈ 𝑂(1))
321315, 319, 320sylancr 694 . . . . . . . . . . 11 (⊤ → ((𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∘𝑓 + (𝑥 ∈ ℝ+ ↦ (1 / 𝑥))) ∈ 𝑂(1))
322314, 321eqeltrrd 2699 . . . . . . . . . 10 (⊤ → (𝑥 ∈ ℝ+ ↦ (((ψ‘𝑥) / 𝑥) + (1 / 𝑥))) ∈ 𝑂(1))
323307, 322eqeltrd 2698 . . . . . . . . 9 (⊤ → (𝑥 ∈ ℝ+ ↦ (((ψ‘𝑥) + 1) / 𝑥)) ∈ 𝑂(1))
324242, 308rerpdivcld 11863 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) + 1) / 𝑥) ∈ ℝ)
325 chpge0 24786 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℝ → 0 ≤ (ψ‘𝑥))
326240, 325syl 17 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑥 ∈ ℝ+) → 0 ≤ (ψ‘𝑥))
327241, 326ge0p1rpd 11862 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((ψ‘𝑥) + 1) ∈ ℝ+)
328327rprege0d 11839 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) + 1) ∈ ℝ ∧ 0 ≤ ((ψ‘𝑥) + 1)))
329246nnrpd 11830 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ ℝ+) → ((⌊‘𝑥) + 1) ∈ ℝ+)
330329rpregt0d 11838 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((⌊‘𝑥) + 1) ∈ ℝ ∧ 0 < ((⌊‘𝑥) + 1)))
331 divge0 10852 . . . . . . . . . . . . 13 (((((ψ‘𝑥) + 1) ∈ ℝ ∧ 0 ≤ ((ψ‘𝑥) + 1)) ∧ (((⌊‘𝑥) + 1) ∈ ℝ ∧ 0 < ((⌊‘𝑥) + 1))) → 0 ≤ (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)))
332328, 330, 331syl2anc 692 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → 0 ≤ (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)))
333247, 332absidd 14111 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → (abs‘(((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1))) = (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)))
334324recnd 10028 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) + 1) / 𝑥) ∈ ℂ)
335334abscld 14125 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → (abs‘(((ψ‘𝑥) + 1) / 𝑥)) ∈ ℝ)
336 fllep1 12558 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → 𝑥 ≤ ((⌊‘𝑥) + 1))
337240, 336syl 17 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℝ+) → 𝑥 ≤ ((⌊‘𝑥) + 1))
338 rpregt0 11806 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ+ → (𝑥 ∈ ℝ ∧ 0 < 𝑥))
339338adantl 482 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ ℝ+) → (𝑥 ∈ ℝ ∧ 0 < 𝑥))
340327rpregt0d 11838 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) + 1) ∈ ℝ ∧ 0 < ((ψ‘𝑥) + 1)))
341 lediv2 10873 . . . . . . . . . . . . . 14 (((𝑥 ∈ ℝ ∧ 0 < 𝑥) ∧ (((⌊‘𝑥) + 1) ∈ ℝ ∧ 0 < ((⌊‘𝑥) + 1)) ∧ (((ψ‘𝑥) + 1) ∈ ℝ ∧ 0 < ((ψ‘𝑥) + 1))) → (𝑥 ≤ ((⌊‘𝑥) + 1) ↔ (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ≤ (((ψ‘𝑥) + 1) / 𝑥)))
342339, 330, 340, 341syl3anc 1323 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ ℝ+) → (𝑥 ≤ ((⌊‘𝑥) + 1) ↔ (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ≤ (((ψ‘𝑥) + 1) / 𝑥)))
343337, 342mpbid 222 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ≤ (((ψ‘𝑥) + 1) / 𝑥))
344324leabsd 14103 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) + 1) / 𝑥) ≤ (abs‘(((ψ‘𝑥) + 1) / 𝑥)))
345247, 324, 335, 343, 344letrd 10154 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ ℝ+) → (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) ≤ (abs‘(((ψ‘𝑥) + 1) / 𝑥)))
346333, 345eqbrtrd 4645 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ ℝ+) → (abs‘(((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1))) ≤ (abs‘(((ψ‘𝑥) + 1) / 𝑥)))
347346adantrr 752 . . . . . . . . 9 ((⊤ ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1))) ≤ (abs‘(((ψ‘𝑥) + 1) / 𝑥)))
348282, 323, 324, 300, 347o1le 14333 . . . . . . . 8 (⊤ → (𝑥 ∈ ℝ+ ↦ (((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1))) ∈ 𝑂(1))
349 o1const 14300 . . . . . . . . . 10 ((ℝ+ ⊆ ℝ ∧ 1 ∈ ℂ) → (𝑥 ∈ ℝ+ ↦ 1) ∈ 𝑂(1))
35014, 75, 349mp2an 707 . . . . . . . . 9 (𝑥 ∈ ℝ+ ↦ 1) ∈ 𝑂(1)
351350a1i 11 . . . . . . . 8 (⊤ → (𝑥 ∈ ℝ+ ↦ 1) ∈ 𝑂(1))
352300, 301, 348, 351o1sub2 14306 . . . . . . 7 (⊤ → (𝑥 ∈ ℝ+ ↦ ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1)) ∈ 𝑂(1))
353238, 249, 299, 352o1sub2 14306 . . . . . 6 (⊤ → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) − ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1))) ∈ 𝑂(1))
35413, 353o1res2 14244 . . . . 5 (⊤ → (𝑥 ∈ (1[,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) − 1) / 𝑛) − ((((ψ‘𝑥) + 1) / ((⌊‘𝑥) + 1)) − 1))) ∈ 𝑂(1))
355232, 354syl5eqelr 2703 . . . 4 (⊤ → (𝑥 ∈ (1[,)+∞) ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) ∈ 𝑂(1))
35616, 355eqeltrd 2698 . . 3 (⊤ → ((𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) ↾ (1[,)+∞)) ∈ 𝑂(1))
357 eqid 2621 . . . . . 6 (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) = (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1))))
358357, 225fmpti 6349 . . . . 5 (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))):ℝ⟶ℂ
359358a1i 11 . . . 4 (⊤ → (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))):ℝ⟶ℂ)
360 ssid 3609 . . . . 5 ℝ ⊆ ℝ
361360a1i 11 . . . 4 (⊤ → ℝ ⊆ ℝ)
362359, 361, 282o1resb 14247 . . 3 (⊤ → ((𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) ∈ 𝑂(1) ↔ ((𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) ↾ (1[,)+∞)) ∈ 𝑂(1)))
363356, 362mpbird 247 . 2 (⊤ → (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) ∈ 𝑂(1))
364363trud 1490 1 (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) ∈ 𝑂(1)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196   ∧ wa 384   = wceq 1480  ⊤wtru 1481   ∈ wcel 1987   ≠ wne 2790  Vcvv 3190   ⊆ wss 3560   class class class wbr 4623   ↦ cmpt 4683   ↾ cres 5086  ⟶wf 5853  ‘cfv 5857  (class class class)co 6615   ∘𝑓 cof 6860  ℂcc 9894  ℝcr 9895  0cc0 9896  1c1 9897   + caddc 9899   · cmul 9901  +∞cpnf 10031   < clt 10034   ≤ cle 10035   − cmin 10226  -cneg 10227   / cdiv 10644  ℕcn 10980  2c2 11030  ℕ0cn0 11252  ℤcz 11337  ℤ≥cuz 11647  ℝ+crp 11792  [,)cico 12135  ...cfz 12284  ..^cfzo 12422  ⌊cfl 12547  abscabs 13924   ⇝𝑟 crli 14166  𝑂(1)co1 14167  Σcsu 14366  logclog 24239  Λcvma 24752  ψcchp 24753 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4741  ax-sep 4751  ax-nul 4759  ax-pow 4813  ax-pr 4877  ax-un 6914  ax-inf2 8498  ax-cnex 9952  ax-resscn 9953  ax-1cn 9954  ax-icn 9955  ax-addcl 9956  ax-addrcl 9957  ax-mulcl 9958  ax-mulrcl 9959  ax-mulcom 9960  ax-addass 9961  ax-mulass 9962  ax-distr 9963  ax-i2m1 9964  ax-1ne0 9965  ax-1rid 9966  ax-rnegex 9967  ax-rrecex 9968  ax-cnre 9969  ax-pre-lttri 9970  ax-pre-lttrn 9971  ax-pre-ltadd 9972  ax-pre-mulgt0 9973  ax-pre-sup 9974  ax-addf 9975  ax-mulf 9976 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2913  df-rex 2914  df-reu 2915  df-rmo 2916  df-rab 2917  df-v 3192  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3898  df-if 4065  df-pw 4138  df-sn 4156  df-pr 4158  df-tp 4160  df-op 4162  df-uni 4410  df-int 4448  df-iun 4494  df-iin 4495  df-br 4624  df-opab 4684  df-mpt 4685  df-tr 4723  df-eprel 4995  df-id 4999  df-po 5005  df-so 5006  df-fr 5043  df-se 5044  df-we 5045  df-xp 5090  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-res 5096  df-ima 5097  df-pred 5649  df-ord 5695  df-on 5696  df-lim 5697  df-suc 5698  df-iota 5820  df-fun 5859  df-fn 5860  df-f 5861  df-f1 5862  df-fo 5863  df-f1o 5864  df-fv 5865  df-isom 5866  df-riota 6576  df-ov 6618  df-oprab 6619  df-mpt2 6620  df-of 6862  df-om 7028  df-1st 7128  df-2nd 7129  df-supp 7256  df-wrecs 7367  df-recs 7428  df-rdg 7466  df-1o 7520  df-2o 7521  df-oadd 7524  df-er 7702  df-map 7819  df-pm 7820  df-ixp 7869  df-en 7916  df-dom 7917  df-sdom 7918  df-fin 7919  df-fsupp 8236  df-fi 8277  df-sup 8308  df-inf 8309  df-oi 8375  df-card 8725  df-cda 8950  df-pnf 10036  df-mnf 10037  df-xr 10038  df-ltxr 10039  df-le 10040  df-sub 10228  df-neg 10229  df-div 10645  df-nn 10981  df-2 11039  df-3 11040  df-4 11041  df-5 11042  df-6 11043  df-7 11044  df-8 11045  df-9 11046  df-n0 11253  df-xnn0 11324  df-z 11338  df-dec 11454  df-uz 11648  df-q 11749  df-rp 11793  df-xneg 11906  df-xadd 11907  df-xmul 11908  df-ioo 12137  df-ioc 12138  df-ico 12139  df-icc 12140  df-fz 12285  df-fzo 12423  df-fl 12549  df-mod 12625  df-seq 12758  df-exp 12817  df-fac 13017  df-bc 13046  df-hash 13074  df-shft 13757  df-cj 13789  df-re 13790  df-im 13791  df-sqrt 13925  df-abs 13926  df-limsup 14152  df-clim 14169  df-rlim 14170  df-o1 14171  df-lo1 14172  df-sum 14367  df-ef 14742  df-e 14743  df-sin 14744  df-cos 14745  df-pi 14747  df-dvds 14927  df-gcd 15160  df-prm 15329  df-pc 15485  df-struct 15802  df-ndx 15803  df-slot 15804  df-base 15805  df-sets 15806  df-ress 15807  df-plusg 15894  df-mulr 15895  df-starv 15896  df-sca 15897  df-vsca 15898  df-ip 15899  df-tset 15900  df-ple 15901  df-ds 15904  df-unif 15905  df-hom 15906  df-cco 15907  df-rest 16023  df-topn 16024  df-0g 16042  df-gsum 16043  df-topgen 16044  df-pt 16045  df-prds 16048  df-xrs 16102  df-qtop 16107  df-imas 16108  df-xps 16110  df-mre 16186  df-mrc 16187  df-acs 16189  df-mgm 17182  df-sgrp 17224  df-mnd 17235  df-submnd 17276  df-mulg 17481  df-cntz 17690  df-cmn 18135  df-psmet 19678  df-xmet 19679  df-met 19680  df-bl 19681  df-mopn 19682  df-fbas 19683  df-fg 19684  df-cnfld 19687  df-top 20639  df-topon 20656  df-topsp 20677  df-bases 20690  df-cld 20763  df-ntr 20764  df-cls 20765  df-nei 20842  df-lp 20880  df-perf 20881  df-cn 20971  df-cnp 20972  df-haus 21059  df-cmp 21130  df-tx 21305  df-hmeo 21498  df-fil 21590  df-fm 21682  df-flim 21683  df-flf 21684  df-xms 22065  df-ms 22066  df-tms 22067  df-cncf 22621  df-limc 23570  df-dv 23571  df-log 24241  df-cxp 24242  df-em 24653  df-cht 24757  df-vma 24758  df-chp 24759  df-ppi 24760 This theorem is referenced by:  pntrsumbnd  25189
 Copyright terms: Public domain W3C validator