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

Theorem pntrlog2bndlem5 26835
Description: Lemma for pntrlog2bnd 26838. Bound on the difference between the Selberg function and its approximation, inside a sum. (Contributed by Mario Carneiro, 31-May-2016.)
Hypotheses
Ref Expression
pntsval.1 𝑆 = (𝑎 ∈ ℝ ↦ Σ𝑖 ∈ (1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))))
pntrlog2bnd.r 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))
pntrlog2bnd.t 𝑇 = (𝑎 ∈ ℝ ↦ if(𝑎 ∈ ℝ+, (𝑎 · (log‘𝑎)), 0))
pntrlog2bndlem5.1 (𝜑𝐵 ∈ ℝ+)
pntrlog2bndlem5.2 (𝜑 → ∀𝑦 ∈ ℝ+ (abs‘((𝑅𝑦) / 𝑦)) ≤ 𝐵)
Assertion
Ref Expression
pntrlog2bndlem5 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((((abs‘(𝑅𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) / 𝑥)) ∈ ≤𝑂(1))
Distinct variable groups:   𝑖,𝑎,𝑛,𝑥,𝑦   𝐵,𝑛,𝑥,𝑦   𝜑,𝑛,𝑥   𝑆,𝑛,𝑥,𝑦   𝑅,𝑛,𝑥,𝑦   𝑇,𝑛
Allowed substitution hints:   𝜑(𝑦,𝑖,𝑎)   𝐵(𝑖,𝑎)   𝑅(𝑖,𝑎)   𝑆(𝑖,𝑎)   𝑇(𝑥,𝑦,𝑖,𝑎)

Proof of Theorem pntrlog2bndlem5
StepHypRef Expression
1 elioore 13215 . . . . . . . . . . . . 13 (𝑥 ∈ (1(,)+∞) → 𝑥 ∈ ℝ)
21adantl 483 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1(,)+∞)) → 𝑥 ∈ ℝ)
3 1rp 12840 . . . . . . . . . . . . 13 1 ∈ ℝ+
43a1i 11 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1(,)+∞)) → 1 ∈ ℝ+)
5 1red 11082 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1(,)+∞)) → 1 ∈ ℝ)
6 eliooord 13244 . . . . . . . . . . . . . . 15 (𝑥 ∈ (1(,)+∞) → (1 < 𝑥𝑥 < +∞))
76adantl 483 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (1(,)+∞)) → (1 < 𝑥𝑥 < +∞))
87simpld 496 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1(,)+∞)) → 1 < 𝑥)
95, 2, 8ltled 11229 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1(,)+∞)) → 1 ≤ 𝑥)
102, 4, 9rpgecld 12917 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1(,)+∞)) → 𝑥 ∈ ℝ+)
11 pntrlog2bnd.r . . . . . . . . . . . . 13 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))
1211pntrf 26817 . . . . . . . . . . . 12 𝑅:ℝ+⟶ℝ
1312ffvelcdmi 7021 . . . . . . . . . . 11 (𝑥 ∈ ℝ+ → (𝑅𝑥) ∈ ℝ)
1410, 13syl 17 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1(,)+∞)) → (𝑅𝑥) ∈ ℝ)
1514recnd 11109 . . . . . . . . 9 ((𝜑𝑥 ∈ (1(,)+∞)) → (𝑅𝑥) ∈ ℂ)
1615abscld 15248 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → (abs‘(𝑅𝑥)) ∈ ℝ)
1716recnd 11109 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → (abs‘(𝑅𝑥)) ∈ ℂ)
1810relogcld 25884 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ∈ ℝ)
1918recnd 11109 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ∈ ℂ)
2017, 19mulcld 11101 . . . . . 6 ((𝜑𝑥 ∈ (1(,)+∞)) → ((abs‘(𝑅𝑥)) · (log‘𝑥)) ∈ ℂ)
21 2cnd 12157 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → 2 ∈ ℂ)
222, 8rplogcld 25890 . . . . . . . . 9 ((𝜑𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ∈ ℝ+)
2322rpne0d 12883 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ≠ 0)
2421, 19, 23divcld 11857 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → (2 / (log‘𝑥)) ∈ ℂ)
25 fzfid 13799 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → (1...(⌊‘𝑥)) ∈ Fin)
2610adantr 482 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ+)
27 elfznn 13391 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
2827adantl 483 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
2928nnrpd 12876 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ+)
3026, 29rpdivcld 12895 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ+)
3112ffvelcdmi 7021 . . . . . . . . . . . . 13 ((𝑥 / 𝑛) ∈ ℝ+ → (𝑅‘(𝑥 / 𝑛)) ∈ ℝ)
3230, 31syl 17 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘(𝑥 / 𝑛)) ∈ ℝ)
3332recnd 11109 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘(𝑥 / 𝑛)) ∈ ℂ)
3433abscld 15248 . . . . . . . . . 10 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑅‘(𝑥 / 𝑛))) ∈ ℝ)
3529relogcld 25884 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘𝑛) ∈ ℝ)
36 1red 11082 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℝ)
3735, 36readdcld 11110 . . . . . . . . . 10 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘𝑛) + 1) ∈ ℝ)
3834, 37remulcld 11111 . . . . . . . . 9 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)) ∈ ℝ)
3938recnd 11109 . . . . . . . 8 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)) ∈ ℂ)
4025, 39fsumcl 15545 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)) ∈ ℂ)
4124, 40mulcld 11101 . . . . . 6 ((𝜑𝑥 ∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1))) ∈ ℂ)
4220, 41subcld 11438 . . . . 5 ((𝜑𝑥 ∈ (1(,)+∞)) → (((abs‘(𝑅𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)))) ∈ ℂ)
4334recnd 11109 . . . . . . 7 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑅‘(𝑥 / 𝑛))) ∈ ℂ)
4425, 43fsumcl 15545 . . . . . 6 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛))) ∈ ℂ)
4524, 44mulcld 11101 . . . . 5 ((𝜑𝑥 ∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛)))) ∈ ℂ)
462recnd 11109 . . . . 5 ((𝜑𝑥 ∈ (1(,)+∞)) → 𝑥 ∈ ℂ)
4710rpne0d 12883 . . . . 5 ((𝜑𝑥 ∈ (1(,)+∞)) → 𝑥 ≠ 0)
4842, 45, 46, 47divdird 11895 . . . 4 ((𝜑𝑥 ∈ (1(,)+∞)) → (((((abs‘(𝑅𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)))) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛))))) / 𝑥) = (((((abs‘(𝑅𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)))) / 𝑥) + (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛)))) / 𝑥)))
4916, 18remulcld 11111 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → ((abs‘(𝑅𝑥)) · (log‘𝑥)) ∈ ℝ)
5049recnd 11109 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → ((abs‘(𝑅𝑥)) · (log‘𝑥)) ∈ ℂ)
5150, 41, 45subsubd 11466 . . . . . 6 ((𝜑𝑥 ∈ (1(,)+∞)) → (((abs‘(𝑅𝑥)) · (log‘𝑥)) − (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛)))))) = ((((abs‘(𝑅𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)))) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛))))))
5224, 40, 44subdid 11537 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)) − Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛))))) = (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛))))))
5325, 39, 43fsumsub 15600 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)) − (abs‘(𝑅‘(𝑥 / 𝑛)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)) − Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛)))))
5437recnd 11109 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘𝑛) + 1) ∈ ℂ)
55 1cnd 11076 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℂ)
5643, 54, 55subdid 11537 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((log‘𝑛) + 1) − 1)) = (((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)) − ((abs‘(𝑅‘(𝑥 / 𝑛))) · 1)))
5735recnd 11109 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘𝑛) ∈ ℂ)
5857, 55pncand 11439 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((log‘𝑛) + 1) − 1) = (log‘𝑛))
5958oveq2d 7358 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (((log‘𝑛) + 1) − 1)) = ((abs‘(𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))
6043mulid1d 11098 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · 1) = (abs‘(𝑅‘(𝑥 / 𝑛))))
6160oveq2d 7358 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)) − ((abs‘(𝑅‘(𝑥 / 𝑛))) · 1)) = (((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)) − (abs‘(𝑅‘(𝑥 / 𝑛)))))
6256, 59, 613eqtr3rd 2786 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)) − (abs‘(𝑅‘(𝑥 / 𝑛)))) = ((abs‘(𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))
6362sumeq2dv 15515 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)) − (abs‘(𝑅‘(𝑥 / 𝑛)))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))
6453, 63eqtr3d 2779 . . . . . . . . 9 ((𝜑𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)) − Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛)))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))
6564oveq2d 7358 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)) − Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛))))) = ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (log‘𝑛))))
6652, 65eqtr3d 2779 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛))))) = ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (log‘𝑛))))
6766oveq2d 7358 . . . . . 6 ((𝜑𝑥 ∈ (1(,)+∞)) → (((abs‘(𝑅𝑥)) · (log‘𝑥)) − (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛)))))) = (((abs‘(𝑅𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))))
6851, 67eqtr3d 2779 . . . . 5 ((𝜑𝑥 ∈ (1(,)+∞)) → ((((abs‘(𝑅𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)))) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛))))) = (((abs‘(𝑅𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))))
6968oveq1d 7357 . . . 4 ((𝜑𝑥 ∈ (1(,)+∞)) → (((((abs‘(𝑅𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)))) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛))))) / 𝑥) = ((((abs‘(𝑅𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) / 𝑥))
7048, 69eqtr3d 2779 . . 3 ((𝜑𝑥 ∈ (1(,)+∞)) → (((((abs‘(𝑅𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)))) / 𝑥) + (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛)))) / 𝑥)) = ((((abs‘(𝑅𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) / 𝑥))
7170mpteq2dva 5197 . 2 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (((((abs‘(𝑅𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)))) / 𝑥) + (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛)))) / 𝑥))) = (𝑥 ∈ (1(,)+∞) ↦ ((((abs‘(𝑅𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) / 𝑥)))
72 2re 12153 . . . . . . . 8 2 ∈ ℝ
7372a1i 11 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → 2 ∈ ℝ)
7473, 22rerpdivcld 12909 . . . . . 6 ((𝜑𝑥 ∈ (1(,)+∞)) → (2 / (log‘𝑥)) ∈ ℝ)
7525, 38fsumrecl 15546 . . . . . 6 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)) ∈ ℝ)
7674, 75remulcld 11111 . . . . 5 ((𝜑𝑥 ∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1))) ∈ ℝ)
7749, 76resubcld 11509 . . . 4 ((𝜑𝑥 ∈ (1(,)+∞)) → (((abs‘(𝑅𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)))) ∈ ℝ)
7877, 10rerpdivcld 12909 . . 3 ((𝜑𝑥 ∈ (1(,)+∞)) → ((((abs‘(𝑅𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)))) / 𝑥) ∈ ℝ)
7925, 34fsumrecl 15546 . . . . 5 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛))) ∈ ℝ)
8074, 79remulcld 11111 . . . 4 ((𝜑𝑥 ∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛)))) ∈ ℝ)
8180, 10rerpdivcld 12909 . . 3 ((𝜑𝑥 ∈ (1(,)+∞)) → (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛)))) / 𝑥) ∈ ℝ)
82 1red 11082 . . . 4 (𝜑 → 1 ∈ ℝ)
83 pntsval.1 . . . . . 6 𝑆 = (𝑎 ∈ ℝ ↦ Σ𝑖 ∈ (1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))))
84 pntrlog2bnd.t . . . . . 6 𝑇 = (𝑎 ∈ ℝ ↦ if(𝑎 ∈ ℝ+, (𝑎 · (log‘𝑎)), 0))
8583, 11, 84pntrlog2bndlem4 26834 . . . . 5 (𝑥 ∈ (1(,)+∞) ↦ ((((abs‘(𝑅𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))) / 𝑥)) ∈ ≤𝑂(1)
8685a1i 11 . . . 4 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((((abs‘(𝑅𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))) / 𝑥)) ∈ ≤𝑂(1))
8728nnred 12094 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ)
88 simpl 484 . . . . . . . . . . . . . . 15 ((𝑎 ∈ ℝ ∧ 𝑎 ∈ ℝ+) → 𝑎 ∈ ℝ)
89 simpr 486 . . . . . . . . . . . . . . . 16 ((𝑎 ∈ ℝ ∧ 𝑎 ∈ ℝ+) → 𝑎 ∈ ℝ+)
9089relogcld 25884 . . . . . . . . . . . . . . 15 ((𝑎 ∈ ℝ ∧ 𝑎 ∈ ℝ+) → (log‘𝑎) ∈ ℝ)
9188, 90remulcld 11111 . . . . . . . . . . . . . 14 ((𝑎 ∈ ℝ ∧ 𝑎 ∈ ℝ+) → (𝑎 · (log‘𝑎)) ∈ ℝ)
92 0red 11084 . . . . . . . . . . . . . 14 ((𝑎 ∈ ℝ ∧ ¬ 𝑎 ∈ ℝ+) → 0 ∈ ℝ)
9391, 92ifclda 4513 . . . . . . . . . . . . 13 (𝑎 ∈ ℝ → if(𝑎 ∈ ℝ+, (𝑎 · (log‘𝑎)), 0) ∈ ℝ)
9484, 93fmpti 7047 . . . . . . . . . . . 12 𝑇:ℝ⟶ℝ
9594ffvelcdmi 7021 . . . . . . . . . . 11 (𝑛 ∈ ℝ → (𝑇𝑛) ∈ ℝ)
9687, 95syl 17 . . . . . . . . . 10 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇𝑛) ∈ ℝ)
9787, 36resubcld 11509 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 − 1) ∈ ℝ)
9894ffvelcdmi 7021 . . . . . . . . . . 11 ((𝑛 − 1) ∈ ℝ → (𝑇‘(𝑛 − 1)) ∈ ℝ)
9997, 98syl 17 . . . . . . . . . 10 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇‘(𝑛 − 1)) ∈ ℝ)
10096, 99resubcld 11509 . . . . . . . . 9 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑇𝑛) − (𝑇‘(𝑛 − 1))) ∈ ℝ)
10134, 100remulcld 11111 . . . . . . . 8 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))) ∈ ℝ)
10225, 101fsumrecl 15546 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))) ∈ ℝ)
10374, 102remulcld 11111 . . . . . 6 ((𝜑𝑥 ∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))) ∈ ℝ)
10449, 103resubcld 11509 . . . . 5 ((𝜑𝑥 ∈ (1(,)+∞)) → (((abs‘(𝑅𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))) ∈ ℝ)
105104, 10rerpdivcld 12909 . . . 4 ((𝜑𝑥 ∈ (1(,)+∞)) → ((((abs‘(𝑅𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))) / 𝑥) ∈ ℝ)
106 2rp 12841 . . . . . . . . . . 11 2 ∈ ℝ+
107106a1i 11 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1(,)+∞)) → 2 ∈ ℝ+)
108107rpge0d 12882 . . . . . . . . 9 ((𝜑𝑥 ∈ (1(,)+∞)) → 0 ≤ 2)
10973, 22, 108divge0d 12918 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → 0 ≤ (2 / (log‘𝑥)))
11033absge0d 15256 . . . . . . . . . 10 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (abs‘(𝑅‘(𝑥 / 𝑛))))
11129adantr 482 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 1 < 𝑛) → 𝑛 ∈ ℝ+)
112111rpcnd 12880 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 1 < 𝑛) → 𝑛 ∈ ℂ)
11357adantr 482 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 1 < 𝑛) → (log‘𝑛) ∈ ℂ)
114112, 113mulcld 11101 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 1 < 𝑛) → (𝑛 · (log‘𝑛)) ∈ ℂ)
115 simpr 486 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 1 < 𝑛) → 1 < 𝑛)
116 1re 11081 . . . . . . . . . . . . . . . . . . 19 1 ∈ ℝ
117111rpred 12878 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 1 < 𝑛) → 𝑛 ∈ ℝ)
118 difrp 12874 . . . . . . . . . . . . . . . . . . 19 ((1 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (1 < 𝑛 ↔ (𝑛 − 1) ∈ ℝ+))
119116, 117, 118sylancr 588 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 1 < 𝑛) → (1 < 𝑛 ↔ (𝑛 − 1) ∈ ℝ+))
120115, 119mpbid 231 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 1 < 𝑛) → (𝑛 − 1) ∈ ℝ+)
121120relogcld 25884 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 1 < 𝑛) → (log‘(𝑛 − 1)) ∈ ℝ)
122121recnd 11109 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 1 < 𝑛) → (log‘(𝑛 − 1)) ∈ ℂ)
123112, 122mulcld 11101 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 1 < 𝑛) → (𝑛 · (log‘(𝑛 − 1))) ∈ ℂ)
124114, 123, 122subsubd 11466 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 1 < 𝑛) → ((𝑛 · (log‘𝑛)) − ((𝑛 · (log‘(𝑛 − 1))) − (log‘(𝑛 − 1)))) = (((𝑛 · (log‘𝑛)) − (𝑛 · (log‘(𝑛 − 1)))) + (log‘(𝑛 − 1))))
125 rpre 12844 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℝ+𝑛 ∈ ℝ)
126 eleq1 2825 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑛 → (𝑎 ∈ ℝ+𝑛 ∈ ℝ+))
127 id 22 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑛𝑎 = 𝑛)
128 fveq2 6830 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑛 → (log‘𝑎) = (log‘𝑛))
129127, 128oveq12d 7360 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑛 → (𝑎 · (log‘𝑎)) = (𝑛 · (log‘𝑛)))
130126, 129ifbieq1d 4502 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑛 → if(𝑎 ∈ ℝ+, (𝑎 · (log‘𝑎)), 0) = if(𝑛 ∈ ℝ+, (𝑛 · (log‘𝑛)), 0))
131 ovex 7375 . . . . . . . . . . . . . . . . . . 19 (𝑛 · (log‘𝑛)) ∈ V
132 c0ex 11075 . . . . . . . . . . . . . . . . . . 19 0 ∈ V
133131, 132ifex 4528 . . . . . . . . . . . . . . . . . 18 if(𝑛 ∈ ℝ+, (𝑛 · (log‘𝑛)), 0) ∈ V
134130, 84, 133fvmpt 6936 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℝ → (𝑇𝑛) = if(𝑛 ∈ ℝ+, (𝑛 · (log‘𝑛)), 0))
135125, 134syl 17 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℝ+ → (𝑇𝑛) = if(𝑛 ∈ ℝ+, (𝑛 · (log‘𝑛)), 0))
136 iftrue 4484 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℝ+ → if(𝑛 ∈ ℝ+, (𝑛 · (log‘𝑛)), 0) = (𝑛 · (log‘𝑛)))
137135, 136eqtrd 2777 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℝ+ → (𝑇𝑛) = (𝑛 · (log‘𝑛)))
138111, 137syl 17 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 1 < 𝑛) → (𝑇𝑛) = (𝑛 · (log‘𝑛)))
139 rpre 12844 . . . . . . . . . . . . . . . . . 18 ((𝑛 − 1) ∈ ℝ+ → (𝑛 − 1) ∈ ℝ)
140 eleq1 2825 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = (𝑛 − 1) → (𝑎 ∈ ℝ+ ↔ (𝑛 − 1) ∈ ℝ+))
141 id 22 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = (𝑛 − 1) → 𝑎 = (𝑛 − 1))
142 fveq2 6830 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = (𝑛 − 1) → (log‘𝑎) = (log‘(𝑛 − 1)))
143141, 142oveq12d 7360 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = (𝑛 − 1) → (𝑎 · (log‘𝑎)) = ((𝑛 − 1) · (log‘(𝑛 − 1))))
144140, 143ifbieq1d 4502 . . . . . . . . . . . . . . . . . . 19 (𝑎 = (𝑛 − 1) → if(𝑎 ∈ ℝ+, (𝑎 · (log‘𝑎)), 0) = if((𝑛 − 1) ∈ ℝ+, ((𝑛 − 1) · (log‘(𝑛 − 1))), 0))
145 ovex 7375 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 − 1) · (log‘(𝑛 − 1))) ∈ V
146145, 132ifex 4528 . . . . . . . . . . . . . . . . . . 19 if((𝑛 − 1) ∈ ℝ+, ((𝑛 − 1) · (log‘(𝑛 − 1))), 0) ∈ V
147144, 84, 146fvmpt 6936 . . . . . . . . . . . . . . . . . 18 ((𝑛 − 1) ∈ ℝ → (𝑇‘(𝑛 − 1)) = if((𝑛 − 1) ∈ ℝ+, ((𝑛 − 1) · (log‘(𝑛 − 1))), 0))
148139, 147syl 17 . . . . . . . . . . . . . . . . 17 ((𝑛 − 1) ∈ ℝ+ → (𝑇‘(𝑛 − 1)) = if((𝑛 − 1) ∈ ℝ+, ((𝑛 − 1) · (log‘(𝑛 − 1))), 0))
149 iftrue 4484 . . . . . . . . . . . . . . . . 17 ((𝑛 − 1) ∈ ℝ+ → if((𝑛 − 1) ∈ ℝ+, ((𝑛 − 1) · (log‘(𝑛 − 1))), 0) = ((𝑛 − 1) · (log‘(𝑛 − 1))))
150148, 149eqtrd 2777 . . . . . . . . . . . . . . . 16 ((𝑛 − 1) ∈ ℝ+ → (𝑇‘(𝑛 − 1)) = ((𝑛 − 1) · (log‘(𝑛 − 1))))
151120, 150syl 17 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 1 < 𝑛) → (𝑇‘(𝑛 − 1)) = ((𝑛 − 1) · (log‘(𝑛 − 1))))
152 1cnd 11076 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 1 < 𝑛) → 1 ∈ ℂ)
153112, 152, 122subdird 11538 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 1 < 𝑛) → ((𝑛 − 1) · (log‘(𝑛 − 1))) = ((𝑛 · (log‘(𝑛 − 1))) − (1 · (log‘(𝑛 − 1)))))
154122mulid2d 11099 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 1 < 𝑛) → (1 · (log‘(𝑛 − 1))) = (log‘(𝑛 − 1)))
155154oveq2d 7358 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 1 < 𝑛) → ((𝑛 · (log‘(𝑛 − 1))) − (1 · (log‘(𝑛 − 1)))) = ((𝑛 · (log‘(𝑛 − 1))) − (log‘(𝑛 − 1))))
156151, 153, 1553eqtrd 2781 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 1 < 𝑛) → (𝑇‘(𝑛 − 1)) = ((𝑛 · (log‘(𝑛 − 1))) − (log‘(𝑛 − 1))))
157138, 156oveq12d 7360 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 1 < 𝑛) → ((𝑇𝑛) − (𝑇‘(𝑛 − 1))) = ((𝑛 · (log‘𝑛)) − ((𝑛 · (log‘(𝑛 − 1))) − (log‘(𝑛 − 1)))))
158112, 113, 122subdid 11537 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 1 < 𝑛) → (𝑛 · ((log‘𝑛) − (log‘(𝑛 − 1)))) = ((𝑛 · (log‘𝑛)) − (𝑛 · (log‘(𝑛 − 1)))))
159158oveq1d 7357 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 1 < 𝑛) → ((𝑛 · ((log‘𝑛) − (log‘(𝑛 − 1)))) + (log‘(𝑛 − 1))) = (((𝑛 · (log‘𝑛)) − (𝑛 · (log‘(𝑛 − 1)))) + (log‘(𝑛 − 1))))
160124, 157, 1593eqtr4d 2787 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 1 < 𝑛) → ((𝑇𝑛) − (𝑇‘(𝑛 − 1))) = ((𝑛 · ((log‘𝑛) − (log‘(𝑛 − 1)))) + (log‘(𝑛 − 1))))
161111relogcld 25884 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 1 < 𝑛) → (log‘𝑛) ∈ ℝ)
162161, 121resubcld 11509 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 1 < 𝑛) → ((log‘𝑛) − (log‘(𝑛 − 1))) ∈ ℝ)
163162recnd 11109 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 1 < 𝑛) → ((log‘𝑛) − (log‘(𝑛 − 1))) ∈ ℂ)
164112, 152, 163subdird 11538 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 1 < 𝑛) → ((𝑛 − 1) · ((log‘𝑛) − (log‘(𝑛 − 1)))) = ((𝑛 · ((log‘𝑛) − (log‘(𝑛 − 1)))) − (1 · ((log‘𝑛) − (log‘(𝑛 − 1))))))
165163mulid2d 11099 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 1 < 𝑛) → (1 · ((log‘𝑛) − (log‘(𝑛 − 1)))) = ((log‘𝑛) − (log‘(𝑛 − 1))))
166165oveq2d 7358 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 1 < 𝑛) → ((𝑛 · ((log‘𝑛) − (log‘(𝑛 − 1)))) − (1 · ((log‘𝑛) − (log‘(𝑛 − 1))))) = ((𝑛 · ((log‘𝑛) − (log‘(𝑛 − 1)))) − ((log‘𝑛) − (log‘(𝑛 − 1)))))
167117, 162remulcld 11111 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 1 < 𝑛) → (𝑛 · ((log‘𝑛) − (log‘(𝑛 − 1)))) ∈ ℝ)
168167recnd 11109 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 1 < 𝑛) → (𝑛 · ((log‘𝑛) − (log‘(𝑛 − 1)))) ∈ ℂ)
169168, 113, 122subsub3d 11468 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 1 < 𝑛) → ((𝑛 · ((log‘𝑛) − (log‘(𝑛 − 1)))) − ((log‘𝑛) − (log‘(𝑛 − 1)))) = (((𝑛 · ((log‘𝑛) − (log‘(𝑛 − 1)))) + (log‘(𝑛 − 1))) − (log‘𝑛)))
170164, 166, 1693eqtrd 2781 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 1 < 𝑛) → ((𝑛 − 1) · ((log‘𝑛) − (log‘(𝑛 − 1)))) = (((𝑛 · ((log‘𝑛) − (log‘(𝑛 − 1)))) + (log‘(𝑛 − 1))) − (log‘𝑛)))
171112, 152npcand 11442 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 1 < 𝑛) → ((𝑛 − 1) + 1) = 𝑛)
172171fveq2d 6834 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 1 < 𝑛) → (log‘((𝑛 − 1) + 1)) = (log‘𝑛))
173172oveq1d 7357 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 1 < 𝑛) → ((log‘((𝑛 − 1) + 1)) − (log‘(𝑛 − 1))) = ((log‘𝑛) − (log‘(𝑛 − 1))))
174 logdifbnd 26249 . . . . . . . . . . . . . . . . 17 ((𝑛 − 1) ∈ ℝ+ → ((log‘((𝑛 − 1) + 1)) − (log‘(𝑛 − 1))) ≤ (1 / (𝑛 − 1)))
175120, 174syl 17 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 1 < 𝑛) → ((log‘((𝑛 − 1) + 1)) − (log‘(𝑛 − 1))) ≤ (1 / (𝑛 − 1)))
176173, 175eqbrtrrd 5121 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 1 < 𝑛) → ((log‘𝑛) − (log‘(𝑛 − 1))) ≤ (1 / (𝑛 − 1)))
177 1red 11082 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 1 < 𝑛) → 1 ∈ ℝ)
178162, 177, 120lemuldiv2d 12928 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 1 < 𝑛) → (((𝑛 − 1) · ((log‘𝑛) − (log‘(𝑛 − 1)))) ≤ 1 ↔ ((log‘𝑛) − (log‘(𝑛 − 1))) ≤ (1 / (𝑛 − 1))))
179176, 178mpbird 257 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 1 < 𝑛) → ((𝑛 − 1) · ((log‘𝑛) − (log‘(𝑛 − 1)))) ≤ 1)
180170, 179eqbrtrrd 5121 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 1 < 𝑛) → (((𝑛 · ((log‘𝑛) − (log‘(𝑛 − 1)))) + (log‘(𝑛 − 1))) − (log‘𝑛)) ≤ 1)
181167, 121readdcld 11110 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 1 < 𝑛) → ((𝑛 · ((log‘𝑛) − (log‘(𝑛 − 1)))) + (log‘(𝑛 − 1))) ∈ ℝ)
182181, 161, 177lesubadd2d 11680 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 1 < 𝑛) → ((((𝑛 · ((log‘𝑛) − (log‘(𝑛 − 1)))) + (log‘(𝑛 − 1))) − (log‘𝑛)) ≤ 1 ↔ ((𝑛 · ((log‘𝑛) − (log‘(𝑛 − 1)))) + (log‘(𝑛 − 1))) ≤ ((log‘𝑛) + 1)))
183180, 182mpbid 231 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 1 < 𝑛) → ((𝑛 · ((log‘𝑛) − (log‘(𝑛 − 1)))) + (log‘(𝑛 − 1))) ≤ ((log‘𝑛) + 1))
184160, 183eqbrtrd 5119 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 1 < 𝑛) → ((𝑇𝑛) − (𝑇‘(𝑛 − 1))) ≤ ((log‘𝑛) + 1))
185 fveq2 6830 . . . . . . . . . . . . . . . . 17 (𝑛 = 1 → (𝑇𝑛) = (𝑇‘1))
186 id 22 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = 1 → 𝑎 = 1)
187186, 3eqeltrdi 2846 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = 1 → 𝑎 ∈ ℝ+)
188187iftrued 4486 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 1 → if(𝑎 ∈ ℝ+, (𝑎 · (log‘𝑎)), 0) = (𝑎 · (log‘𝑎)))
189 fveq2 6830 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 = 1 → (log‘𝑎) = (log‘1))
190 log1 25847 . . . . . . . . . . . . . . . . . . . . . . 23 (log‘1) = 0
191189, 190eqtrdi 2793 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = 1 → (log‘𝑎) = 0)
192186, 191oveq12d 7360 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = 1 → (𝑎 · (log‘𝑎)) = (1 · 0))
193 ax-1cn 11035 . . . . . . . . . . . . . . . . . . . . . 22 1 ∈ ℂ
194193mul01i 11271 . . . . . . . . . . . . . . . . . . . . 21 (1 · 0) = 0
195192, 194eqtrdi 2793 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 1 → (𝑎 · (log‘𝑎)) = 0)
196188, 195eqtrd 2777 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 1 → if(𝑎 ∈ ℝ+, (𝑎 · (log‘𝑎)), 0) = 0)
197196, 84, 132fvmpt 6936 . . . . . . . . . . . . . . . . . 18 (1 ∈ ℝ → (𝑇‘1) = 0)
198116, 197ax-mp 5 . . . . . . . . . . . . . . . . 17 (𝑇‘1) = 0
199185, 198eqtrdi 2793 . . . . . . . . . . . . . . . 16 (𝑛 = 1 → (𝑇𝑛) = 0)
200 oveq1 7349 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 1 → (𝑛 − 1) = (1 − 1))
201 1m1e0 12151 . . . . . . . . . . . . . . . . . . 19 (1 − 1) = 0
202200, 201eqtrdi 2793 . . . . . . . . . . . . . . . . . 18 (𝑛 = 1 → (𝑛 − 1) = 0)
203202fveq2d 6834 . . . . . . . . . . . . . . . . 17 (𝑛 = 1 → (𝑇‘(𝑛 − 1)) = (𝑇‘0))
204 0re 11083 . . . . . . . . . . . . . . . . . 18 0 ∈ ℝ
205 rpne0 12852 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 ∈ ℝ+𝑎 ≠ 0)
206205necon2bi 2972 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 0 → ¬ 𝑎 ∈ ℝ+)
207206iffalsed 4489 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 0 → if(𝑎 ∈ ℝ+, (𝑎 · (log‘𝑎)), 0) = 0)
208207, 84, 132fvmpt 6936 . . . . . . . . . . . . . . . . . 18 (0 ∈ ℝ → (𝑇‘0) = 0)
209204, 208ax-mp 5 . . . . . . . . . . . . . . . . 17 (𝑇‘0) = 0
210203, 209eqtrdi 2793 . . . . . . . . . . . . . . . 16 (𝑛 = 1 → (𝑇‘(𝑛 − 1)) = 0)
211199, 210oveq12d 7360 . . . . . . . . . . . . . . 15 (𝑛 = 1 → ((𝑇𝑛) − (𝑇‘(𝑛 − 1))) = (0 − 0))
212 0m0e0 12199 . . . . . . . . . . . . . . 15 (0 − 0) = 0
213211, 212eqtrdi 2793 . . . . . . . . . . . . . 14 (𝑛 = 1 → ((𝑇𝑛) − (𝑇‘(𝑛 − 1))) = 0)
214213eqcoms 2745 . . . . . . . . . . . . 13 (1 = 𝑛 → ((𝑇𝑛) − (𝑇‘(𝑛 − 1))) = 0)
215214adantl 483 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 1 = 𝑛) → ((𝑇𝑛) − (𝑇‘(𝑛 − 1))) = 0)
216 0red 11084 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ∈ ℝ)
21728nnge1d 12127 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ≤ 𝑛)
21887, 217logge0d 25891 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (log‘𝑛))
21935lep1d 12012 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘𝑛) ≤ ((log‘𝑛) + 1))
220216, 35, 37, 218, 219letrd 11238 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ ((log‘𝑛) + 1))
221220adantr 482 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 1 = 𝑛) → 0 ≤ ((log‘𝑛) + 1))
222215, 221eqbrtrd 5119 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 1 = 𝑛) → ((𝑇𝑛) − (𝑇‘(𝑛 − 1))) ≤ ((log‘𝑛) + 1))
223 elfzle1 13365 . . . . . . . . . . . . 13 (𝑛 ∈ (1...(⌊‘𝑥)) → 1 ≤ 𝑛)
224223adantl 483 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ≤ 𝑛)
22536, 87leloed 11224 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 ≤ 𝑛 ↔ (1 < 𝑛 ∨ 1 = 𝑛)))
226224, 225mpbid 231 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 < 𝑛 ∨ 1 = 𝑛))
227184, 222, 226mpjaodan 957 . . . . . . . . . 10 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑇𝑛) − (𝑇‘(𝑛 − 1))) ≤ ((log‘𝑛) + 1))
228100, 37, 34, 110, 227lemul2ad 12021 . . . . . . . . 9 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))) ≤ ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)))
22925, 101, 38, 228fsumle 15611 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)))
230102, 75, 74, 109, 229lemul2ad 12021 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1))))) ≤ ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1))))
231103, 76, 49, 230lesub2dd 11698 . . . . . 6 ((𝜑𝑥 ∈ (1(,)+∞)) → (((abs‘(𝑅𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)))) ≤ (((abs‘(𝑅𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))))
23277, 104, 10, 231lediv1dd 12936 . . . . 5 ((𝜑𝑥 ∈ (1(,)+∞)) → ((((abs‘(𝑅𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)))) / 𝑥) ≤ ((((abs‘(𝑅𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))) / 𝑥))
233232adantrr 715 . . . 4 ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ 1 ≤ 𝑥)) → ((((abs‘(𝑅𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)))) / 𝑥) ≤ ((((abs‘(𝑅𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇𝑛) − (𝑇‘(𝑛 − 1)))))) / 𝑥))
23482, 86, 105, 78, 233lo1le 15463 . . 3 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((((abs‘(𝑅𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)))) / 𝑥)) ∈ ≤𝑂(1))
235106a1i 11 . . . . . . . 8 (𝜑 → 2 ∈ ℝ+)
236 pntrlog2bndlem5.1 . . . . . . . 8 (𝜑𝐵 ∈ ℝ+)
237235, 236rpmulcld 12894 . . . . . . 7 (𝜑 → (2 · 𝐵) ∈ ℝ+)
238237rpred 12878 . . . . . 6 (𝜑 → (2 · 𝐵) ∈ ℝ)
239238adantr 482 . . . . 5 ((𝜑𝑥 ∈ (1(,)+∞)) → (2 · 𝐵) ∈ ℝ)
2405, 22rerpdivcld 12909 . . . . . 6 ((𝜑𝑥 ∈ (1(,)+∞)) → (1 / (log‘𝑥)) ∈ ℝ)
2415, 240readdcld 11110 . . . . 5 ((𝜑𝑥 ∈ (1(,)+∞)) → (1 + (1 / (log‘𝑥))) ∈ ℝ)
242 ioossre 13246 . . . . . 6 (1(,)+∞) ⊆ ℝ
243 lo1const 15430 . . . . . 6 (((1(,)+∞) ⊆ ℝ ∧ (2 · 𝐵) ∈ ℝ) → (𝑥 ∈ (1(,)+∞) ↦ (2 · 𝐵)) ∈ ≤𝑂(1))
244242, 238, 243sylancr 588 . . . . 5 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (2 · 𝐵)) ∈ ≤𝑂(1))
245 lo1const 15430 . . . . . . 7 (((1(,)+∞) ⊆ ℝ ∧ 1 ∈ ℝ) → (𝑥 ∈ (1(,)+∞) ↦ 1) ∈ ≤𝑂(1))
246242, 82, 245sylancr 588 . . . . . 6 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ 1) ∈ ≤𝑂(1))
247 divlogrlim 25896 . . . . . . . 8 (𝑥 ∈ (1(,)+∞) ↦ (1 / (log‘𝑥))) ⇝𝑟 0
248 rlimo1 15426 . . . . . . . 8 ((𝑥 ∈ (1(,)+∞) ↦ (1 / (log‘𝑥))) ⇝𝑟 0 → (𝑥 ∈ (1(,)+∞) ↦ (1 / (log‘𝑥))) ∈ 𝑂(1))
249247, 248mp1i 13 . . . . . . 7 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (1 / (log‘𝑥))) ∈ 𝑂(1))
250240, 249o1lo1d 15348 . . . . . 6 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (1 / (log‘𝑥))) ∈ ≤𝑂(1))
2515, 240, 246, 250lo1add 15436 . . . . 5 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (1 + (1 / (log‘𝑥)))) ∈ ≤𝑂(1))
252237adantr 482 . . . . . 6 ((𝜑𝑥 ∈ (1(,)+∞)) → (2 · 𝐵) ∈ ℝ+)
253252rpge0d 12882 . . . . 5 ((𝜑𝑥 ∈ (1(,)+∞)) → 0 ≤ (2 · 𝐵))
254239, 241, 244, 251, 253lo1mul 15437 . . . 4 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((2 · 𝐵) · (1 + (1 / (log‘𝑥))))) ∈ ≤𝑂(1))
255239, 241remulcld 11111 . . . 4 ((𝜑𝑥 ∈ (1(,)+∞)) → ((2 · 𝐵) · (1 + (1 / (log‘𝑥)))) ∈ ℝ)
25679, 10rerpdivcld 12909 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛))) / 𝑥) ∈ ℝ)
25718, 5readdcld 11110 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → ((log‘𝑥) + 1) ∈ ℝ)
258236adantr 482 . . . . . . . . 9 ((𝜑𝑥 ∈ (1(,)+∞)) → 𝐵 ∈ ℝ+)
259258rpred 12878 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → 𝐵 ∈ ℝ)
260257, 259remulcld 11111 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → (((log‘𝑥) + 1) · 𝐵) ∈ ℝ)
26128nnrecred 12130 . . . . . . . . . 10 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / 𝑛) ∈ ℝ)
26225, 261fsumrecl 15546 . . . . . . . . 9 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) ∈ ℝ)
263262, 259remulcld 11111 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) · 𝐵) ∈ ℝ)
26434, 26rerpdivcld 12909 . . . . . . . . . 10 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) / 𝑥) ∈ ℝ)
265259adantr 482 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝐵 ∈ ℝ)
266261, 265remulcld 11111 . . . . . . . . . 10 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 / 𝑛) · 𝐵) ∈ ℝ)
26730rpcnd 12880 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℂ)
26830rpne0d 12883 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ≠ 0)
26933, 267, 268absdivd 15267 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((𝑅‘(𝑥 / 𝑛)) / (𝑥 / 𝑛))) = ((abs‘(𝑅‘(𝑥 / 𝑛))) / (abs‘(𝑥 / 𝑛))))
2702adantr 482 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ)
271270, 28nndivred 12133 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ)
27230rpge0d 12882 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (𝑥 / 𝑛))
273271, 272absidd 15234 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑥 / 𝑛)) = (𝑥 / 𝑛))
274273oveq2d 7358 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) / (abs‘(𝑥 / 𝑛))) = ((abs‘(𝑅‘(𝑥 / 𝑛))) / (𝑥 / 𝑛)))
275269, 274eqtrd 2777 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((𝑅‘(𝑥 / 𝑛)) / (𝑥 / 𝑛))) = ((abs‘(𝑅‘(𝑥 / 𝑛))) / (𝑥 / 𝑛)))
27646adantr 482 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℂ)
27787recnd 11109 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℂ)
27847adantr 482 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ≠ 0)
27928nnne0d 12129 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ≠ 0)
28043, 276, 277, 278, 279divdiv2d 11889 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) / (𝑥 / 𝑛)) = (((abs‘(𝑅‘(𝑥 / 𝑛))) · 𝑛) / 𝑥))
28143, 277, 276, 278div23d 11894 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((abs‘(𝑅‘(𝑥 / 𝑛))) · 𝑛) / 𝑥) = (((abs‘(𝑅‘(𝑥 / 𝑛))) / 𝑥) · 𝑛))
282275, 280, 2813eqtrd 2781 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((𝑅‘(𝑥 / 𝑛)) / (𝑥 / 𝑛))) = (((abs‘(𝑅‘(𝑥 / 𝑛))) / 𝑥) · 𝑛))
283 fveq2 6830 . . . . . . . . . . . . . . . . 17 (𝑦 = (𝑥 / 𝑛) → (𝑅𝑦) = (𝑅‘(𝑥 / 𝑛)))
284 id 22 . . . . . . . . . . . . . . . . 17 (𝑦 = (𝑥 / 𝑛) → 𝑦 = (𝑥 / 𝑛))
285283, 284oveq12d 7360 . . . . . . . . . . . . . . . 16 (𝑦 = (𝑥 / 𝑛) → ((𝑅𝑦) / 𝑦) = ((𝑅‘(𝑥 / 𝑛)) / (𝑥 / 𝑛)))
286285fveq2d 6834 . . . . . . . . . . . . . . 15 (𝑦 = (𝑥 / 𝑛) → (abs‘((𝑅𝑦) / 𝑦)) = (abs‘((𝑅‘(𝑥 / 𝑛)) / (𝑥 / 𝑛))))
287286breq1d 5107 . . . . . . . . . . . . . 14 (𝑦 = (𝑥 / 𝑛) → ((abs‘((𝑅𝑦) / 𝑦)) ≤ 𝐵 ↔ (abs‘((𝑅‘(𝑥 / 𝑛)) / (𝑥 / 𝑛))) ≤ 𝐵))
288 pntrlog2bndlem5.2 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑦 ∈ ℝ+ (abs‘((𝑅𝑦) / 𝑦)) ≤ 𝐵)
289288ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ∀𝑦 ∈ ℝ+ (abs‘((𝑅𝑦) / 𝑦)) ≤ 𝐵)
290287, 289, 30rspcdva 3575 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((𝑅‘(𝑥 / 𝑛)) / (𝑥 / 𝑛))) ≤ 𝐵)
291282, 290eqbrtrrd 5121 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((abs‘(𝑅‘(𝑥 / 𝑛))) / 𝑥) · 𝑛) ≤ 𝐵)
292264, 265, 29lemuldivd 12927 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((((abs‘(𝑅‘(𝑥 / 𝑛))) / 𝑥) · 𝑛) ≤ 𝐵 ↔ ((abs‘(𝑅‘(𝑥 / 𝑛))) / 𝑥) ≤ (𝐵 / 𝑛)))
293291, 292mpbid 231 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) / 𝑥) ≤ (𝐵 / 𝑛))
294265recnd 11109 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝐵 ∈ ℂ)
295294, 277, 279divrec2d 11861 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝐵 / 𝑛) = ((1 / 𝑛) · 𝐵))
296293, 295breqtrd 5123 . . . . . . . . . 10 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) / 𝑥) ≤ ((1 / 𝑛) · 𝐵))
29725, 264, 266, 296fsumle 15611 . . . . . . . . 9 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) / 𝑥) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))((1 / 𝑛) · 𝐵))
29825, 46, 43, 47fsumdivc 15598 . . . . . . . . 9 ((𝜑𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛))) / 𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) / 𝑥))
299258rpcnd 12880 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1(,)+∞)) → 𝐵 ∈ ℂ)
300261recnd 11109 . . . . . . . . . 10 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 / 𝑛) ∈ ℂ)
30125, 299, 300fsummulc1 15597 . . . . . . . . 9 ((𝜑𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) · 𝐵) = Σ𝑛 ∈ (1...(⌊‘𝑥))((1 / 𝑛) · 𝐵))
302297, 298, 3013brtr4d 5129 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛))) / 𝑥) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) · 𝐵))
303258rpge0d 12882 . . . . . . . . 9 ((𝜑𝑥 ∈ (1(,)+∞)) → 0 ≤ 𝐵)
304 harmonicubnd 26265 . . . . . . . . . 10 ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) → Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) ≤ ((log‘𝑥) + 1))
3052, 9, 304syl2anc 585 . . . . . . . . 9 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) ≤ ((log‘𝑥) + 1))
306262, 257, 259, 303, 305lemul1ad 12020 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / 𝑛) · 𝐵) ≤ (((log‘𝑥) + 1) · 𝐵))
307256, 263, 260, 302, 306letrd 11238 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛))) / 𝑥) ≤ (((log‘𝑥) + 1) · 𝐵))
308256, 260, 74, 109, 307lemul2ad 12021 . . . . . 6 ((𝜑𝑥 ∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛))) / 𝑥)) ≤ ((2 / (log‘𝑥)) · (((log‘𝑥) + 1) · 𝐵)))
30924, 44, 46, 47divassd 11892 . . . . . 6 ((𝜑𝑥 ∈ (1(,)+∞)) → (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛)))) / 𝑥) = ((2 / (log‘𝑥)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛))) / 𝑥)))
310241recnd 11109 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → (1 + (1 / (log‘𝑥))) ∈ ℂ)
31121, 299, 310mul32d 11291 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → ((2 · 𝐵) · (1 + (1 / (log‘𝑥)))) = ((2 · (1 + (1 / (log‘𝑥)))) · 𝐵))
312 1cnd 11076 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1(,)+∞)) → 1 ∈ ℂ)
31319, 312, 19, 23divdird 11895 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1(,)+∞)) → (((log‘𝑥) + 1) / (log‘𝑥)) = (((log‘𝑥) / (log‘𝑥)) + (1 / (log‘𝑥))))
31419, 23dividd 11855 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1(,)+∞)) → ((log‘𝑥) / (log‘𝑥)) = 1)
315314oveq1d 7357 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1(,)+∞)) → (((log‘𝑥) / (log‘𝑥)) + (1 / (log‘𝑥))) = (1 + (1 / (log‘𝑥))))
316313, 315eqtr2d 2778 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1(,)+∞)) → (1 + (1 / (log‘𝑥))) = (((log‘𝑥) + 1) / (log‘𝑥)))
317316oveq2d 7358 . . . . . . . . 9 ((𝜑𝑥 ∈ (1(,)+∞)) → (2 · (1 + (1 / (log‘𝑥)))) = (2 · (((log‘𝑥) + 1) / (log‘𝑥))))
31819, 312addcld 11100 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1(,)+∞)) → ((log‘𝑥) + 1) ∈ ℂ)
31921, 19, 318, 23div32d 11880 . . . . . . . . 9 ((𝜑𝑥 ∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · ((log‘𝑥) + 1)) = (2 · (((log‘𝑥) + 1) / (log‘𝑥))))
320317, 319eqtr4d 2780 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → (2 · (1 + (1 / (log‘𝑥)))) = ((2 / (log‘𝑥)) · ((log‘𝑥) + 1)))
321320oveq1d 7357 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → ((2 · (1 + (1 / (log‘𝑥)))) · 𝐵) = (((2 / (log‘𝑥)) · ((log‘𝑥) + 1)) · 𝐵))
32224, 318, 299mulassd 11104 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → (((2 / (log‘𝑥)) · ((log‘𝑥) + 1)) · 𝐵) = ((2 / (log‘𝑥)) · (((log‘𝑥) + 1) · 𝐵)))
323311, 321, 3223eqtrd 2781 . . . . . 6 ((𝜑𝑥 ∈ (1(,)+∞)) → ((2 · 𝐵) · (1 + (1 / (log‘𝑥)))) = ((2 / (log‘𝑥)) · (((log‘𝑥) + 1) · 𝐵)))
324308, 309, 3233brtr4d 5129 . . . . 5 ((𝜑𝑥 ∈ (1(,)+∞)) → (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛)))) / 𝑥) ≤ ((2 · 𝐵) · (1 + (1 / (log‘𝑥)))))
325324adantrr 715 . . . 4 ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ 1 ≤ 𝑥)) → (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛)))) / 𝑥) ≤ ((2 · 𝐵) · (1 + (1 / (log‘𝑥)))))
32682, 254, 255, 81, 325lo1le 15463 . . 3 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛)))) / 𝑥)) ∈ ≤𝑂(1))
32778, 81, 234, 326lo1add 15436 . 2 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (((((abs‘(𝑅𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((log‘𝑛) + 1)))) / 𝑥) + (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(𝑅‘(𝑥 / 𝑛)))) / 𝑥))) ∈ ≤𝑂(1))
32871, 327eqeltrrd 2839 1 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((((abs‘(𝑅𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) / 𝑥)) ∈ ≤𝑂(1))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  wo 845   = wceq 1541  wcel 2106  wne 2941  wral 3062  wss 3902  ifcif 4478   class class class wbr 5097  cmpt 5180  cfv 6484  (class class class)co 7342  cc 10975  cr 10976  0cc0 10977  1c1 10978   + caddc 10980   · cmul 10982  +∞cpnf 11112   < clt 11115  cle 11116  cmin 11311   / cdiv 11738  cn 12079  2c2 12134  +crp 12836  (,)cioo 13185  ...cfz 13345  cfl 13616  abscabs 15045  𝑟 crli 15294  𝑂(1)co1 15295  ≤𝑂(1)clo1 15296  Σcsu 15497  logclog 25816  Λcvma 26347  ψcchp 26348
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-rep 5234  ax-sep 5248  ax-nul 5255  ax-pow 5313  ax-pr 5377  ax-un 7655  ax-inf2 9503  ax-cnex 11033  ax-resscn 11034  ax-1cn 11035  ax-icn 11036  ax-addcl 11037  ax-addrcl 11038  ax-mulcl 11039  ax-mulrcl 11040  ax-mulcom 11041  ax-addass 11042  ax-mulass 11043  ax-distr 11044  ax-i2m1 11045  ax-1ne0 11046  ax-1rid 11047  ax-rnegex 11048  ax-rrecex 11049  ax-cnre 11050  ax-pre-lttri 11051  ax-pre-lttrn 11052  ax-pre-ltadd 11053  ax-pre-mulgt0 11054  ax-pre-sup 11055  ax-addf 11056  ax-mulf 11057
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3350  df-reu 3351  df-rab 3405  df-v 3444  df-sbc 3732  df-csb 3848  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3921  df-nul 4275  df-if 4479  df-pw 4554  df-sn 4579  df-pr 4581  df-tp 4583  df-op 4585  df-uni 4858  df-int 4900  df-iun 4948  df-iin 4949  df-disj 5063  df-br 5098  df-opab 5160  df-mpt 5181  df-tr 5215  df-id 5523  df-eprel 5529  df-po 5537  df-so 5538  df-fr 5580  df-se 5581  df-we 5582  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6243  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6436  df-fun 6486  df-fn 6487  df-f 6488  df-f1 6489  df-fo 6490  df-f1o 6491  df-fv 6492  df-isom 6493  df-riota 7298  df-ov 7345  df-oprab 7346  df-mpo 7347  df-of 7600  df-om 7786  df-1st 7904  df-2nd 7905  df-supp 8053  df-frecs 8172  df-wrecs 8203  df-recs 8277  df-rdg 8316  df-1o 8372  df-2o 8373  df-oadd 8376  df-er 8574  df-map 8693  df-pm 8694  df-ixp 8762  df-en 8810  df-dom 8811  df-sdom 8812  df-fin 8813  df-fsupp 9232  df-fi 9273  df-sup 9304  df-inf 9305  df-oi 9372  df-dju 9763  df-card 9801  df-pnf 11117  df-mnf 11118  df-xr 11119  df-ltxr 11120  df-le 11121  df-sub 11313  df-neg 11314  df-div 11739  df-nn 12080  df-2 12142  df-3 12143  df-4 12144  df-5 12145  df-6 12146  df-7 12147  df-8 12148  df-9 12149  df-n0 12340  df-xnn0 12412  df-z 12426  df-dec 12544  df-uz 12689  df-q 12795  df-rp 12837  df-xneg 12954  df-xadd 12955  df-xmul 12956  df-ioo 13189  df-ioc 13190  df-ico 13191  df-icc 13192  df-fz 13346  df-fzo 13489  df-fl 13618  df-mod 13696  df-seq 13828  df-exp 13889  df-fac 14094  df-bc 14123  df-hash 14151  df-shft 14878  df-cj 14910  df-re 14911  df-im 14912  df-sqrt 15046  df-abs 15047  df-limsup 15280  df-clim 15297  df-rlim 15298  df-o1 15299  df-lo1 15300  df-sum 15498  df-ef 15877  df-e 15878  df-sin 15879  df-cos 15880  df-tan 15881  df-pi 15882  df-dvds 16064  df-gcd 16302  df-prm 16475  df-pc 16636  df-struct 16946  df-sets 16963  df-slot 16981  df-ndx 16993  df-base 17011  df-ress 17040  df-plusg 17073  df-mulr 17074  df-starv 17075  df-sca 17076  df-vsca 17077  df-ip 17078  df-tset 17079  df-ple 17080  df-ds 17082  df-unif 17083  df-hom 17084  df-cco 17085  df-rest 17231  df-topn 17232  df-0g 17250  df-gsum 17251  df-topgen 17252  df-pt 17253  df-prds 17256  df-xrs 17311  df-qtop 17316  df-imas 17317  df-xps 17319  df-mre 17393  df-mrc 17394  df-acs 17396  df-mgm 18424  df-sgrp 18473  df-mnd 18484  df-submnd 18529  df-mulg 18798  df-cntz 19020  df-cmn 19484  df-psmet 20695  df-xmet 20696  df-met 20697  df-bl 20698  df-mopn 20699  df-fbas 20700  df-fg 20701  df-cnfld 20704  df-top 22149  df-topon 22166  df-topsp 22188  df-bases 22202  df-cld 22276  df-ntr 22277  df-cls 22278  df-nei 22355  df-lp 22393  df-perf 22394  df-cn 22484  df-cnp 22485  df-haus 22572  df-cmp 22644  df-tx 22819  df-hmeo 23012  df-fil 23103  df-fm 23195  df-flim 23196  df-flf 23197  df-xms 23579  df-ms 23580  df-tms 23581  df-cncf 24147  df-limc 25136  df-dv 25137  df-ulm 25642  df-log 25818  df-cxp 25819  df-atan 26123  df-em 26248  df-cht 26352  df-vma 26353  df-chp 26354  df-ppi 26355  df-mu 26356
This theorem is referenced by:  pntrlog2bndlem6  26837
  Copyright terms: Public domain W3C validator