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

Theorem mulog2sumlem2 24941
Description: Lemma for mulog2sum 24943. (Contributed by Mario Carneiro, 19-May-2016.)
Hypotheses
Ref Expression
logdivsum.1 𝐹 = (𝑦 ∈ ℝ+ ↦ (Σ𝑖 ∈ (1...(⌊‘𝑦))((log‘𝑖) / 𝑖) − (((log‘𝑦)↑2) / 2)))
mulog2sumlem.1 (𝜑𝐹𝑟 𝐿)
mulog2sumlem2.t 𝑇 = ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ · (log‘(𝑥 / 𝑛))) − 𝐿))
mulog2sumlem2.r 𝑅 = (((1 / 2) + (γ + (abs‘𝐿))) + Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚))
Assertion
Ref Expression
mulog2sumlem2 (𝜑 → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥))) ∈ 𝑂(1))
Distinct variable groups:   𝑖,𝑚,𝑛,𝑥,𝑦   𝑥,𝐹   𝑛,𝐿,𝑥   𝜑,𝑚,𝑛,𝑥   𝑅,𝑛,𝑥
Allowed substitution hints:   𝜑(𝑦,𝑖)   𝑅(𝑦,𝑖,𝑚)   𝑇(𝑥,𝑦,𝑖,𝑚,𝑛)   𝐹(𝑦,𝑖,𝑚,𝑛)   𝐿(𝑦,𝑖,𝑚)

Proof of Theorem mulog2sumlem2
Dummy variable 𝑘 is distinct from all other variables.
StepHypRef Expression
1 1red 9911 . 2 (𝜑 → 1 ∈ ℝ)
2 2re 10937 . . . 4 2 ∈ ℝ
3 fzfid 12589 . . . . 5 ((𝜑𝑥 ∈ ℝ+) → (1...(⌊‘𝑥)) ∈ Fin)
4 simpr 475 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ+)
5 elfznn 12196 . . . . . . . . 9 (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
65nnrpd 11702 . . . . . . . 8 (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℝ+)
7 rpdivcl 11688 . . . . . . . 8 ((𝑥 ∈ ℝ+𝑛 ∈ ℝ+) → (𝑥 / 𝑛) ∈ ℝ+)
84, 6, 7syl2an 492 . . . . . . 7 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ+)
98relogcld 24090 . . . . . 6 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ∈ ℝ)
10 simplr 787 . . . . . 6 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ+)
119, 10rerpdivcld 11735 . . . . 5 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛)) / 𝑥) ∈ ℝ)
123, 11fsumrecl 14258 . . . 4 ((𝜑𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥) ∈ ℝ)
13 remulcl 9877 . . . 4 ((2 ∈ ℝ ∧ Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥) ∈ ℝ) → (2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) ∈ ℝ)
142, 12, 13sylancr 693 . . 3 ((𝜑𝑥 ∈ ℝ+) → (2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) ∈ ℝ)
15 mulog2sumlem2.r . . . . . 6 𝑅 = (((1 / 2) + (γ + (abs‘𝐿))) + Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚))
16 halfre 11093 . . . . . . . 8 (1 / 2) ∈ ℝ
17 emre 24449 . . . . . . . . 9 γ ∈ ℝ
18 mulog2sumlem.1 . . . . . . . . . . 11 (𝜑𝐹𝑟 𝐿)
19 rlimcl 14028 . . . . . . . . . . 11 (𝐹𝑟 𝐿𝐿 ∈ ℂ)
2018, 19syl 17 . . . . . . . . . 10 (𝜑𝐿 ∈ ℂ)
2120abscld 13969 . . . . . . . . 9 (𝜑 → (abs‘𝐿) ∈ ℝ)
22 readdcl 9875 . . . . . . . . 9 ((γ ∈ ℝ ∧ (abs‘𝐿) ∈ ℝ) → (γ + (abs‘𝐿)) ∈ ℝ)
2317, 21, 22sylancr 693 . . . . . . . 8 (𝜑 → (γ + (abs‘𝐿)) ∈ ℝ)
24 readdcl 9875 . . . . . . . 8 (((1 / 2) ∈ ℝ ∧ (γ + (abs‘𝐿)) ∈ ℝ) → ((1 / 2) + (γ + (abs‘𝐿))) ∈ ℝ)
2516, 23, 24sylancr 693 . . . . . . 7 (𝜑 → ((1 / 2) + (γ + (abs‘𝐿))) ∈ ℝ)
26 fzfid 12589 . . . . . . . 8 (𝜑 → (1...2) ∈ Fin)
27 epr 14721 . . . . . . . . . . 11 e ∈ ℝ+
28 elfznn 12196 . . . . . . . . . . . . 13 (𝑚 ∈ (1...2) → 𝑚 ∈ ℕ)
2928adantl 480 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (1...2)) → 𝑚 ∈ ℕ)
3029nnrpd 11702 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (1...2)) → 𝑚 ∈ ℝ+)
31 rpdivcl 11688 . . . . . . . . . . 11 ((e ∈ ℝ+𝑚 ∈ ℝ+) → (e / 𝑚) ∈ ℝ+)
3227, 30, 31sylancr 693 . . . . . . . . . 10 ((𝜑𝑚 ∈ (1...2)) → (e / 𝑚) ∈ ℝ+)
3332relogcld 24090 . . . . . . . . 9 ((𝜑𝑚 ∈ (1...2)) → (log‘(e / 𝑚)) ∈ ℝ)
3433, 29nndivred 10916 . . . . . . . 8 ((𝜑𝑚 ∈ (1...2)) → ((log‘(e / 𝑚)) / 𝑚) ∈ ℝ)
3526, 34fsumrecl 14258 . . . . . . 7 (𝜑 → Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚) ∈ ℝ)
3625, 35readdcld 9925 . . . . . 6 (𝜑 → (((1 / 2) + (γ + (abs‘𝐿))) + Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚)) ∈ ℝ)
3715, 36syl5eqel 2691 . . . . 5 (𝜑𝑅 ∈ ℝ)
38 remulcl 9877 . . . . 5 ((𝑅 ∈ ℝ ∧ 2 ∈ ℝ) → (𝑅 · 2) ∈ ℝ)
3937, 2, 38sylancl 692 . . . 4 (𝜑 → (𝑅 · 2) ∈ ℝ)
4039adantr 479 . . 3 ((𝜑𝑥 ∈ ℝ+) → (𝑅 · 2) ∈ ℝ)
412a1i 11 . . . 4 ((𝜑𝑥 ∈ ℝ+) → 2 ∈ ℝ)
42 rpssre 11675 . . . . 5 + ⊆ ℝ
43 2cnd 10940 . . . . 5 (𝜑 → 2 ∈ ℂ)
44 o1const 14144 . . . . 5 ((ℝ+ ⊆ ℝ ∧ 2 ∈ ℂ) → (𝑥 ∈ ℝ+ ↦ 2) ∈ 𝑂(1))
4542, 43, 44sylancr 693 . . . 4 (𝜑 → (𝑥 ∈ ℝ+ ↦ 2) ∈ 𝑂(1))
46 logfacrlim2 24668 . . . . 5 (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) ⇝𝑟 1
47 rlimo1 14141 . . . . 5 ((𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) ⇝𝑟 1 → (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) ∈ 𝑂(1))
4846, 47mp1i 13 . . . 4 (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) ∈ 𝑂(1))
4941, 12, 45, 48o1mul2 14149 . . 3 (𝜑 → (𝑥 ∈ ℝ+ ↦ (2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥))) ∈ 𝑂(1))
5039recnd 9924 . . . 4 (𝜑 → (𝑅 · 2) ∈ ℂ)
51 o1const 14144 . . . 4 ((ℝ+ ⊆ ℝ ∧ (𝑅 · 2) ∈ ℂ) → (𝑥 ∈ ℝ+ ↦ (𝑅 · 2)) ∈ 𝑂(1))
5242, 50, 51sylancr 693 . . 3 (𝜑 → (𝑥 ∈ ℝ+ ↦ (𝑅 · 2)) ∈ 𝑂(1))
5314, 40, 49, 52o1add2 14148 . 2 (𝜑 → (𝑥 ∈ ℝ+ ↦ ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2))) ∈ 𝑂(1))
5414, 40readdcld 9925 . 2 ((𝜑𝑥 ∈ ℝ+) → ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2)) ∈ ℝ)
555adantl 480 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
56 mucl 24584 . . . . . . . . 9 (𝑛 ∈ ℕ → (μ‘𝑛) ∈ ℤ)
5755, 56syl 17 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℤ)
5857zred 11314 . . . . . . 7 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℝ)
5958, 55nndivred 10916 . . . . . 6 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) / 𝑛) ∈ ℝ)
6059recnd 9924 . . . . 5 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) / 𝑛) ∈ ℂ)
61 mulog2sumlem2.t . . . . . 6 𝑇 = ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ · (log‘(𝑥 / 𝑛))) − 𝐿))
629recnd 9924 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ∈ ℂ)
6362sqcld 12823 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛))↑2) ∈ ℂ)
6463halfcld 11124 . . . . . . 7 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((log‘(𝑥 / 𝑛))↑2) / 2) ∈ ℂ)
65 remulcl 9877 . . . . . . . . . 10 ((γ ∈ ℝ ∧ (log‘(𝑥 / 𝑛)) ∈ ℝ) → (γ · (log‘(𝑥 / 𝑛))) ∈ ℝ)
6617, 9, 65sylancr 693 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (γ · (log‘(𝑥 / 𝑛))) ∈ ℝ)
6766recnd 9924 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (γ · (log‘(𝑥 / 𝑛))) ∈ ℂ)
6820ad2antrr 757 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝐿 ∈ ℂ)
6967, 68subcld 10243 . . . . . . 7 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((γ · (log‘(𝑥 / 𝑛))) − 𝐿) ∈ ℂ)
7064, 69addcld 9915 . . . . . 6 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ · (log‘(𝑥 / 𝑛))) − 𝐿)) ∈ ℂ)
7161, 70syl5eqel 2691 . . . . 5 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑇 ∈ ℂ)
7260, 71mulcld 9916 . . . 4 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) / 𝑛) · 𝑇) ∈ ℂ)
733, 72fsumcl 14257 . . 3 ((𝜑𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) ∈ ℂ)
74 relogcl 24043 . . . . 5 (𝑥 ∈ ℝ+ → (log‘𝑥) ∈ ℝ)
7574adantl 480 . . . 4 ((𝜑𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℝ)
7675recnd 9924 . . 3 ((𝜑𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℂ)
7773, 76subcld 10243 . 2 ((𝜑𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥)) ∈ ℂ)
7877abscld 13969 . . . 4 ((𝜑𝑥 ∈ ℝ+) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥))) ∈ ℝ)
7978adantrr 748 . . 3 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥))) ∈ ℝ)
8054adantrr 748 . . 3 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2)) ∈ ℝ)
8154recnd 9924 . . . . 5 ((𝜑𝑥 ∈ ℝ+) → ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2)) ∈ ℂ)
8281abscld 13969 . . . 4 ((𝜑𝑥 ∈ ℝ+) → (abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2))) ∈ ℝ)
8382adantrr 748 . . 3 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2))) ∈ ℝ)
8457zcnd 11315 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈ ℂ)
85 fzfid 12589 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1...(⌊‘(𝑥 / 𝑛))) ∈ Fin)
86 elfznn 12196 . . . . . . . . . . . . . 14 (𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛))) → 𝑚 ∈ ℕ)
87 nnrp 11674 . . . . . . . . . . . . . . . . . 18 (𝑚 ∈ ℕ → 𝑚 ∈ ℝ+)
88 rpdivcl 11688 . . . . . . . . . . . . . . . . . 18 (((𝑥 / 𝑛) ∈ ℝ+𝑚 ∈ ℝ+) → ((𝑥 / 𝑛) / 𝑚) ∈ ℝ+)
898, 87, 88syl2an 492 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → ((𝑥 / 𝑛) / 𝑚) ∈ ℝ+)
9089relogcld 24090 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (log‘((𝑥 / 𝑛) / 𝑚)) ∈ ℝ)
91 simpr 475 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℕ)
9290, 91nndivred 10916 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℝ)
9392recnd 9924 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℂ)
9486, 93sylan2 489 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℂ)
9585, 94fsumcl 14257 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℂ)
9671, 95subcld 10243 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) ∈ ℂ)
9755nncnd 10883 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℂ)
9855nnne0d 10912 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ≠ 0)
9984, 96, 97, 98div23d 10687 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛) = (((μ‘𝑛) / 𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
10060, 71, 95subdid 10336 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) / 𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) = ((((μ‘𝑛) / 𝑛) · 𝑇) − (((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
10199, 100eqtrd 2643 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛) = ((((μ‘𝑛) / 𝑛) · 𝑇) − (((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
102101sumeq2dv 14227 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛) = Σ𝑛 ∈ (1...(⌊‘𝑥))((((μ‘𝑛) / 𝑛) · 𝑇) − (((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
10360, 95mulcld 9916 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) ∈ ℂ)
1043, 72, 103fsumsub 14308 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((((μ‘𝑛) / 𝑛) · 𝑇) − (((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
105102, 104eqtrd 2643 . . . . . . 7 ((𝜑𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
106105adantrr 748 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
10785, 60, 94fsummulc2 14304 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(((μ‘𝑛) / 𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))
10884adantr 479 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (μ‘𝑛) ∈ ℂ)
10997, 98jca 552 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0))
110109adantr 479 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0))
111 div23 10553 . . . . . . . . . . . . . . . . 17 (((μ‘𝑛) ∈ ℂ ∧ ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → (((μ‘𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) / 𝑛) = (((μ‘𝑛) / 𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))
112 divass 10552 . . . . . . . . . . . . . . . . 17 (((μ‘𝑛) ∈ ℂ ∧ ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → (((μ‘𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) / 𝑛) = ((μ‘𝑛) · (((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) / 𝑛)))
113111, 112eqtr3d 2645 . . . . . . . . . . . . . . . 16 (((μ‘𝑛) ∈ ℂ ∧ ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → (((μ‘𝑛) / 𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = ((μ‘𝑛) · (((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) / 𝑛)))
114108, 93, 110, 113syl3anc 1317 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (((μ‘𝑛) / 𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = ((μ‘𝑛) · (((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) / 𝑛)))
11590recnd 9924 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (log‘((𝑥 / 𝑛) / 𝑚)) ∈ ℂ)
11691nnrpd 11702 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℝ+)
117 rpcnne0 11682 . . . . . . . . . . . . . . . . . . 19 (𝑚 ∈ ℝ+ → (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0))
118116, 117syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0))
119 divdiv1 10585 . . . . . . . . . . . . . . . . . 18 (((log‘((𝑥 / 𝑛) / 𝑚)) ∈ ℂ ∧ (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0) ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → (((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) / 𝑛) = ((log‘((𝑥 / 𝑛) / 𝑚)) / (𝑚 · 𝑛)))
120115, 118, 110, 119syl3anc 1317 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) / 𝑛) = ((log‘((𝑥 / 𝑛) / 𝑚)) / (𝑚 · 𝑛)))
121 rpre 11671 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∈ ℝ+𝑥 ∈ ℝ)
122121adantl 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ)
123122adantr 479 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ)
124123recnd 9924 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℂ)
125124adantr 479 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → 𝑥 ∈ ℂ)
126 divdiv1 10585 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0) ∧ (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0)) → ((𝑥 / 𝑛) / 𝑚) = (𝑥 / (𝑛 · 𝑚)))
127125, 110, 118, 126syl3anc 1317 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → ((𝑥 / 𝑛) / 𝑚) = (𝑥 / (𝑛 · 𝑚)))
128127fveq2d 6092 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (log‘((𝑥 / 𝑛) / 𝑚)) = (log‘(𝑥 / (𝑛 · 𝑚))))
12991nncnd 10883 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℂ)
13097adantr 479 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → 𝑛 ∈ ℂ)
131129, 130mulcomd 9917 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (𝑚 · 𝑛) = (𝑛 · 𝑚))
132128, 131oveq12d 6545 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → ((log‘((𝑥 / 𝑛) / 𝑚)) / (𝑚 · 𝑛)) = ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚)))
133120, 132eqtrd 2643 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) / 𝑛) = ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚)))
134133oveq2d 6543 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → ((μ‘𝑛) · (((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) / 𝑛)) = ((μ‘𝑛) · ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚))))
135114, 134eqtrd 2643 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (((μ‘𝑛) / 𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = ((μ‘𝑛) · ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚))))
13686, 135sylan2 489 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (((μ‘𝑛) / 𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = ((μ‘𝑛) · ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚))))
137136sumeq2dv 14227 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(((μ‘𝑛) / 𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚))))
138107, 137eqtrd 2643 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚))))
139138sumeq2dv 14227 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚))))
140 oveq2 6535 . . . . . . . . . . . . . 14 (𝑘 = (𝑛 · 𝑚) → (𝑥 / 𝑘) = (𝑥 / (𝑛 · 𝑚)))
141140fveq2d 6092 . . . . . . . . . . . . 13 (𝑘 = (𝑛 · 𝑚) → (log‘(𝑥 / 𝑘)) = (log‘(𝑥 / (𝑛 · 𝑚))))
142 id 22 . . . . . . . . . . . . 13 (𝑘 = (𝑛 · 𝑚) → 𝑘 = (𝑛 · 𝑚))
143141, 142oveq12d 6545 . . . . . . . . . . . 12 (𝑘 = (𝑛 · 𝑚) → ((log‘(𝑥 / 𝑘)) / 𝑘) = ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚)))
144143oveq2d 6543 . . . . . . . . . . 11 (𝑘 = (𝑛 · 𝑚) → ((μ‘𝑛) · ((log‘(𝑥 / 𝑘)) / 𝑘)) = ((μ‘𝑛) · ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚))))
1454rpred 11704 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ)
146 ssrab2 3649 . . . . . . . . . . . . . . . 16 {𝑦 ∈ ℕ ∣ 𝑦𝑘} ⊆ ℕ
147 simprr 791 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑘})) → 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑘})
148146, 147sseldi 3565 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑘})) → 𝑛 ∈ ℕ)
149148, 56syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑘})) → (μ‘𝑛) ∈ ℤ)
150149zred 11314 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑘})) → (μ‘𝑛) ∈ ℝ)
151 elfznn 12196 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ (1...(⌊‘𝑥)) → 𝑘 ∈ ℕ)
152151adantr 479 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑘}) → 𝑘 ∈ ℕ)
153152nnrpd 11702 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑘}) → 𝑘 ∈ ℝ+)
154 rpdivcl 11688 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℝ+𝑘 ∈ ℝ+) → (𝑥 / 𝑘) ∈ ℝ+)
1554, 153, 154syl2an 492 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑘})) → (𝑥 / 𝑘) ∈ ℝ+)
156155relogcld 24090 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑘})) → (log‘(𝑥 / 𝑘)) ∈ ℝ)
157151ad2antrl 759 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑘})) → 𝑘 ∈ ℕ)
158156, 157nndivred 10916 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑘})) → ((log‘(𝑥 / 𝑘)) / 𝑘) ∈ ℝ)
159150, 158remulcld 9926 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑘})) → ((μ‘𝑛) · ((log‘(𝑥 / 𝑘)) / 𝑘)) ∈ ℝ)
160159recnd 9924 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑘 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑘})) → ((μ‘𝑛) · ((log‘(𝑥 / 𝑘)) / 𝑘)) ∈ ℂ)
161144, 145, 160dvdsflsumcom 24631 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ+) → Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑘} ((μ‘𝑛) · ((log‘(𝑥 / 𝑘)) / 𝑘)) = Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚))))
162139, 161eqtr4d 2646 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑘} ((μ‘𝑛) · ((log‘(𝑥 / 𝑘)) / 𝑘)))
163162adantrr 748 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑘} ((μ‘𝑛) · ((log‘(𝑥 / 𝑘)) / 𝑘)))
164 oveq2 6535 . . . . . . . . . . 11 (𝑘 = 1 → (𝑥 / 𝑘) = (𝑥 / 1))
165164fveq2d 6092 . . . . . . . . . 10 (𝑘 = 1 → (log‘(𝑥 / 𝑘)) = (log‘(𝑥 / 1)))
166 id 22 . . . . . . . . . 10 (𝑘 = 1 → 𝑘 = 1)
167165, 166oveq12d 6545 . . . . . . . . 9 (𝑘 = 1 → ((log‘(𝑥 / 𝑘)) / 𝑘) = ((log‘(𝑥 / 1)) / 1))
168 fzfid 12589 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (1...(⌊‘𝑥)) ∈ Fin)
1695ssriv 3571 . . . . . . . . . 10 (1...(⌊‘𝑥)) ⊆ ℕ
170169a1i 11 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (1...(⌊‘𝑥)) ⊆ ℕ)
171122adantrr 748 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 𝑥 ∈ ℝ)
172 simprr 791 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ≤ 𝑥)
173 flge1nn 12439 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ ∧ 1 ≤ 𝑥) → (⌊‘𝑥) ∈ ℕ)
174171, 172, 173syl2anc 690 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (⌊‘𝑥) ∈ ℕ)
175 nnuz 11555 . . . . . . . . . . 11 ℕ = (ℤ‘1)
176174, 175syl6eleq 2697 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (⌊‘𝑥) ∈ (ℤ‘1))
177 eluzfz1 12174 . . . . . . . . . 10 ((⌊‘𝑥) ∈ (ℤ‘1) → 1 ∈ (1...(⌊‘𝑥)))
178176, 177syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → 1 ∈ (1...(⌊‘𝑥)))
179151nnrpd 11702 . . . . . . . . . . . . . 14 (𝑘 ∈ (1...(⌊‘𝑥)) → 𝑘 ∈ ℝ+)
1804, 179, 154syl2an 492 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑘) ∈ ℝ+)
181180relogcld 24090 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑘)) ∈ ℝ)
182169a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ℝ+) → (1...(⌊‘𝑥)) ⊆ ℕ)
183182sselda 3567 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → 𝑘 ∈ ℕ)
184181, 183nndivred 10916 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑘)) / 𝑘) ∈ ℝ)
185184recnd 9924 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑘)) / 𝑘) ∈ ℂ)
186185adantlrr 752 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) ∧ 𝑘 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑘)) / 𝑘) ∈ ℂ)
187167, 168, 170, 178, 186musumsum 24635 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑘} ((μ‘𝑛) · ((log‘(𝑥 / 𝑘)) / 𝑘)) = ((log‘(𝑥 / 1)) / 1))
1884rpcnd 11706 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ℝ+) → 𝑥 ∈ ℂ)
189188div1d 10642 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ℝ+) → (𝑥 / 1) = 𝑥)
190189fveq2d 6092 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ℝ+) → (log‘(𝑥 / 1)) = (log‘𝑥))
191190oveq1d 6542 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ+) → ((log‘(𝑥 / 1)) / 1) = ((log‘𝑥) / 1))
19276div1d 10642 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ+) → ((log‘𝑥) / 1) = (log‘𝑥))
193191, 192eqtrd 2643 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ+) → ((log‘(𝑥 / 1)) / 1) = (log‘𝑥))
194193adantrr 748 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((log‘(𝑥 / 1)) / 1) = (log‘𝑥))
195163, 187, 1943eqtrd 2647 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = (log‘𝑥))
196195oveq2d 6543 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥)))
197106, 196eqtrd 2643 . . . . 5 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥)))
198197fveq2d 6092 . . . 4 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛)) = (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥))))
199 ere 14604 . . . . . . . . 9 e ∈ ℝ
200199a1i 11 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ+) → e ∈ ℝ)
201 1re 9895 . . . . . . . . 9 1 ∈ ℝ
202 1lt2 11041 . . . . . . . . . 10 1 < 2
203 egt2lt3 14719 . . . . . . . . . . 11 (2 < e ∧ e < 3)
204203simpli 472 . . . . . . . . . 10 2 < e
205201, 2, 199lttri 10014 . . . . . . . . . 10 ((1 < 2 ∧ 2 < e) → 1 < e)
206202, 204, 205mp2an 703 . . . . . . . . 9 1 < e
207201, 199, 206ltleii 10011 . . . . . . . 8 1 ≤ e
208200, 207jctir 558 . . . . . . 7 ((𝜑𝑥 ∈ ℝ+) → (e ∈ ℝ ∧ 1 ≤ e))
20937adantr 479 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ+) → 𝑅 ∈ ℝ)
21016a1i 11 . . . . . . . . . . . 12 (𝜑 → (1 / 2) ∈ ℝ)
211 1rp 11668 . . . . . . . . . . . . . 14 1 ∈ ℝ+
212 rphalfcl 11690 . . . . . . . . . . . . . 14 (1 ∈ ℝ+ → (1 / 2) ∈ ℝ+)
213211, 212ax-mp 5 . . . . . . . . . . . . 13 (1 / 2) ∈ ℝ+
214 rpge0 11677 . . . . . . . . . . . . 13 ((1 / 2) ∈ ℝ+ → 0 ≤ (1 / 2))
215213, 214mp1i 13 . . . . . . . . . . . 12 (𝜑 → 0 ≤ (1 / 2))
21617a1i 11 . . . . . . . . . . . . 13 (𝜑 → γ ∈ ℝ)
217 0re 9896 . . . . . . . . . . . . . . 15 0 ∈ ℝ
218 emgt0 24450 . . . . . . . . . . . . . . 15 0 < γ
219217, 17, 218ltleii 10011 . . . . . . . . . . . . . 14 0 ≤ γ
220219a1i 11 . . . . . . . . . . . . 13 (𝜑 → 0 ≤ γ)
22120absge0d 13977 . . . . . . . . . . . . 13 (𝜑 → 0 ≤ (abs‘𝐿))
222216, 21, 220, 221addge0d 10452 . . . . . . . . . . . 12 (𝜑 → 0 ≤ (γ + (abs‘𝐿)))
223210, 23, 215, 222addge0d 10452 . . . . . . . . . . 11 (𝜑 → 0 ≤ ((1 / 2) + (γ + (abs‘𝐿))))
224 log1 24053 . . . . . . . . . . . . . 14 (log‘1) = 0
22529nncnd 10883 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ (1...2)) → 𝑚 ∈ ℂ)
226225mulid2d 9914 . . . . . . . . . . . . . . . . 17 ((𝜑𝑚 ∈ (1...2)) → (1 · 𝑚) = 𝑚)
22730rpred 11704 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ (1...2)) → 𝑚 ∈ ℝ)
2282a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ (1...2)) → 2 ∈ ℝ)
229199a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ (1...2)) → e ∈ ℝ)
230 elfzle2 12171 . . . . . . . . . . . . . . . . . . 19 (𝑚 ∈ (1...2) → 𝑚 ≤ 2)
231230adantl 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ (1...2)) → 𝑚 ≤ 2)
2322, 199, 204ltleii 10011 . . . . . . . . . . . . . . . . . . 19 2 ≤ e
233232a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑚 ∈ (1...2)) → 2 ≤ e)
234227, 228, 229, 231, 233letrd 10045 . . . . . . . . . . . . . . . . 17 ((𝜑𝑚 ∈ (1...2)) → 𝑚 ≤ e)
235226, 234eqbrtrd 4599 . . . . . . . . . . . . . . . 16 ((𝜑𝑚 ∈ (1...2)) → (1 · 𝑚) ≤ e)
236 1red 9911 . . . . . . . . . . . . . . . . 17 ((𝜑𝑚 ∈ (1...2)) → 1 ∈ ℝ)
237236, 229, 30lemuldivd 11753 . . . . . . . . . . . . . . . 16 ((𝜑𝑚 ∈ (1...2)) → ((1 · 𝑚) ≤ e ↔ 1 ≤ (e / 𝑚)))
238235, 237mpbid 220 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ (1...2)) → 1 ≤ (e / 𝑚))
239 logleb 24070 . . . . . . . . . . . . . . . 16 ((1 ∈ ℝ+ ∧ (e / 𝑚) ∈ ℝ+) → (1 ≤ (e / 𝑚) ↔ (log‘1) ≤ (log‘(e / 𝑚))))
240211, 32, 239sylancr 693 . . . . . . . . . . . . . . 15 ((𝜑𝑚 ∈ (1...2)) → (1 ≤ (e / 𝑚) ↔ (log‘1) ≤ (log‘(e / 𝑚))))
241238, 240mpbid 220 . . . . . . . . . . . . . 14 ((𝜑𝑚 ∈ (1...2)) → (log‘1) ≤ (log‘(e / 𝑚)))
242224, 241syl5eqbrr 4613 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ (1...2)) → 0 ≤ (log‘(e / 𝑚)))
24333, 30, 242divge0d 11744 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (1...2)) → 0 ≤ ((log‘(e / 𝑚)) / 𝑚))
24426, 34, 243fsumge0 14314 . . . . . . . . . . 11 (𝜑 → 0 ≤ Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚))
24525, 35, 223, 244addge0d 10452 . . . . . . . . . 10 (𝜑 → 0 ≤ (((1 / 2) + (γ + (abs‘𝐿))) + Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚)))
246245, 15syl6breqr 4619 . . . . . . . . 9 (𝜑 → 0 ≤ 𝑅)
247246adantr 479 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ+) → 0 ≤ 𝑅)
248209, 247jca 552 . . . . . . 7 ((𝜑𝑥 ∈ ℝ+) → (𝑅 ∈ ℝ ∧ 0 ≤ 𝑅))
24984, 96mulcld 9916 . . . . . . 7 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ∈ ℂ)
250 remulcl 9877 . . . . . . . 8 ((2 ∈ ℝ ∧ ((log‘(𝑥 / 𝑛)) / 𝑥) ∈ ℝ) → (2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) ∈ ℝ)
2512, 11, 250sylancr 693 . . . . . . 7 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) ∈ ℝ)
2522a1i 11 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 2 ∈ ℝ)
253 0le2 10958 . . . . . . . . 9 0 ≤ 2
254253a1i 11 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ 2)
25597mulid2d 9914 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 · 𝑛) = 𝑛)
256 fznnfl 12478 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ → (𝑛 ∈ (1...(⌊‘𝑥)) ↔ (𝑛 ∈ ℕ ∧ 𝑛𝑥)))
257122, 256syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ+) → (𝑛 ∈ (1...(⌊‘𝑥)) ↔ (𝑛 ∈ ℕ ∧ 𝑛𝑥)))
258257simplbda 651 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛𝑥)
259255, 258eqbrtrd 4599 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 · 𝑛) ≤ 𝑥)
260 1red 9911 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℝ)
26155nnrpd 11702 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ+)
262260, 123, 261lemuldivd 11753 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 · 𝑛) ≤ 𝑥 ↔ 1 ≤ (𝑥 / 𝑛)))
263259, 262mpbid 220 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ≤ (𝑥 / 𝑛))
264 logleb 24070 . . . . . . . . . . . 12 ((1 ∈ ℝ+ ∧ (𝑥 / 𝑛) ∈ ℝ+) → (1 ≤ (𝑥 / 𝑛) ↔ (log‘1) ≤ (log‘(𝑥 / 𝑛))))
265211, 8, 264sylancr 693 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 ≤ (𝑥 / 𝑛) ↔ (log‘1) ≤ (log‘(𝑥 / 𝑛))))
266263, 265mpbid 220 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘1) ≤ (log‘(𝑥 / 𝑛)))
267224, 266syl5eqbrr 4613 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (log‘(𝑥 / 𝑛)))
268 rpregt0 11678 . . . . . . . . . 10 (𝑥 ∈ ℝ+ → (𝑥 ∈ ℝ ∧ 0 < 𝑥))
269268ad2antlr 758 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 ∈ ℝ ∧ 0 < 𝑥))
270 divge0 10741 . . . . . . . . 9 ((((log‘(𝑥 / 𝑛)) ∈ ℝ ∧ 0 ≤ (log‘(𝑥 / 𝑛))) ∧ (𝑥 ∈ ℝ ∧ 0 < 𝑥)) → 0 ≤ ((log‘(𝑥 / 𝑛)) / 𝑥))
2719, 267, 269, 270syl21anc 1316 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ ((log‘(𝑥 / 𝑛)) / 𝑥))
272252, 11, 254, 271mulge0d 10453 . . . . . . 7 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (2 · ((log‘(𝑥 / 𝑛)) / 𝑥)))
273249abscld 13969 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ∈ ℝ)
274273adantr 479 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → (abs‘((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ∈ ℝ)
27596adantr 479 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) ∈ ℂ)
276275abscld 13969 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ∈ ℝ)
277261rpred 11704 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ)
278251, 277remulcld 9926 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) · 𝑛) ∈ ℝ)
279278adantr 479 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → ((2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) · 𝑛) ∈ ℝ)
28084, 96absmuld 13987 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) = ((abs‘(μ‘𝑛)) · (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))))
28184abscld 13969 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(μ‘𝑛)) ∈ ℝ)
28296abscld 13969 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ∈ ℝ)
28396absge0d 13977 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
284 mule1 24591 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → (abs‘(μ‘𝑛)) ≤ 1)
28555, 284syl 17 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(μ‘𝑛)) ≤ 1)
286281, 260, 282, 283, 285lemul1ad 10812 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(μ‘𝑛)) · (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ≤ (1 · (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))))
287282recnd 9924 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ∈ ℂ)
288287mulid2d 9914 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 · (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) = (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
289286, 288breqtrd 4603 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(μ‘𝑛)) · (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ≤ (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
290280, 289eqbrtrd 4599 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ≤ (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
291290adantr 479 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → (abs‘((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ≤ (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
292 logdivsum.1 . . . . . . . . . 10 𝐹 = (𝑦 ∈ ℝ+ ↦ (Σ𝑖 ∈ (1...(⌊‘𝑦))((log‘𝑖) / 𝑖) − (((log‘𝑦)↑2) / 2)))
29318ad3antrrr 761 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → 𝐹𝑟 𝐿)
2948adantr 479 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → (𝑥 / 𝑛) ∈ ℝ+)
295 simpr 475 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → e ≤ (𝑥 / 𝑛))
296292, 293, 294, 295mulog2sumlem1 24940 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) − ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ · (log‘(𝑥 / 𝑛))) − 𝐿)))) ≤ (2 · ((log‘(𝑥 / 𝑛)) / (𝑥 / 𝑛))))
29771, 95abssubd 13986 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) = (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) − 𝑇)))
298297adantr 479 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) = (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) − 𝑇)))
29961oveq2i 6538 . . . . . . . . . . 11 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) − 𝑇) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) − ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ · (log‘(𝑥 / 𝑛))) − 𝐿)))
300299fveq2i 6091 . . . . . . . . . 10 (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) − 𝑇)) = (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) − ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ · (log‘(𝑥 / 𝑛))) − 𝐿))))
301298, 300syl6eq 2659 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) = (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) − ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ · (log‘(𝑥 / 𝑛))) − 𝐿)))))
302 2cnd 10940 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 2 ∈ ℂ)
30311recnd 9924 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛)) / 𝑥) ∈ ℂ)
304302, 303, 97mulassd 9919 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) · 𝑛) = (2 · (((log‘(𝑥 / 𝑛)) / 𝑥) · 𝑛)))
305 rpcnne0 11682 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ+ → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
306305ad2antlr 758 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
307 divdiv2 10586 . . . . . . . . . . . . . 14 (((log‘(𝑥 / 𝑛)) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → ((log‘(𝑥 / 𝑛)) / (𝑥 / 𝑛)) = (((log‘(𝑥 / 𝑛)) · 𝑛) / 𝑥))
30862, 306, 109, 307syl3anc 1317 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛)) / (𝑥 / 𝑛)) = (((log‘(𝑥 / 𝑛)) · 𝑛) / 𝑥))
309 div23 10553 . . . . . . . . . . . . . 14 (((log‘(𝑥 / 𝑛)) ∈ ℂ ∧ 𝑛 ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) → (((log‘(𝑥 / 𝑛)) · 𝑛) / 𝑥) = (((log‘(𝑥 / 𝑛)) / 𝑥) · 𝑛))
31062, 97, 306, 309syl3anc 1317 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((log‘(𝑥 / 𝑛)) · 𝑛) / 𝑥) = (((log‘(𝑥 / 𝑛)) / 𝑥) · 𝑛))
311308, 310eqtrd 2643 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛)) / (𝑥 / 𝑛)) = (((log‘(𝑥 / 𝑛)) / 𝑥) · 𝑛))
312311oveq2d 6543 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · ((log‘(𝑥 / 𝑛)) / (𝑥 / 𝑛))) = (2 · (((log‘(𝑥 / 𝑛)) / 𝑥) · 𝑛)))
313304, 312eqtr4d 2646 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) · 𝑛) = (2 · ((log‘(𝑥 / 𝑛)) / (𝑥 / 𝑛))))
314313adantr 479 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → ((2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) · 𝑛) = (2 · ((log‘(𝑥 / 𝑛)) / (𝑥 / 𝑛))))
315296, 301, 3143brtr4d 4609 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ≤ ((2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) · 𝑛))
316274, 276, 279, 291, 315letrd 10045 . . . . . . 7 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ e ≤ (𝑥 / 𝑛)) → (abs‘((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ≤ ((2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) · 𝑛))
317273adantr 479 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ∈ ℝ)
318282adantr 479 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ∈ ℝ)
31937ad3antrrr 761 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → 𝑅 ∈ ℝ)
320290adantr 479 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ≤ (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
32171adantr 479 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → 𝑇 ∈ ℂ)
322321abscld 13969 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘𝑇) ∈ ℝ)
32395adantr 479 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℂ)
324323abscld 13969 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) ∈ ℝ)
325322, 324readdcld 9925 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((abs‘𝑇) + (abs‘Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ∈ ℝ)
326321, 323abs2dif2d 13991 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ≤ ((abs‘𝑇) + (abs‘Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))
32725ad3antrrr 761 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((1 / 2) + (γ + (abs‘𝐿))) ∈ ℝ)
32835ad3antrrr 761 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚) ∈ ℝ)
32961fveq2i 6091 . . . . . . . . . . . 12 (abs‘𝑇) = (abs‘((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ · (log‘(𝑥 / 𝑛))) − 𝐿)))
330329, 322syl5eqelr 2692 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ · (log‘(𝑥 / 𝑛))) − 𝐿))) ∈ ℝ)
33164adantr 479 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (((log‘(𝑥 / 𝑛))↑2) / 2) ∈ ℂ)
332331abscld 13969 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘(((log‘(𝑥 / 𝑛))↑2) / 2)) ∈ ℝ)
33369adantr 479 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((γ · (log‘(𝑥 / 𝑛))) − 𝐿) ∈ ℂ)
334333abscld 13969 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘((γ · (log‘(𝑥 / 𝑛))) − 𝐿)) ∈ ℝ)
335332, 334readdcld 9925 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((abs‘(((log‘(𝑥 / 𝑛))↑2) / 2)) + (abs‘((γ · (log‘(𝑥 / 𝑛))) − 𝐿))) ∈ ℝ)
336331, 333abstrid 13989 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ · (log‘(𝑥 / 𝑛))) − 𝐿))) ≤ ((abs‘(((log‘(𝑥 / 𝑛))↑2) / 2)) + (abs‘((γ · (log‘(𝑥 / 𝑛))) − 𝐿))))
33716a1i 11 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (1 / 2) ∈ ℝ)
33823ad3antrrr 761 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (γ + (abs‘𝐿)) ∈ ℝ)
3399resqcld 12852 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛))↑2) ∈ ℝ)
340339rehalfcld 11126 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((log‘(𝑥 / 𝑛))↑2) / 2) ∈ ℝ)
3419sqge0d 12853 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ ((log‘(𝑥 / 𝑛))↑2))
342 2pos 10959 . . . . . . . . . . . . . . . . . . . 20 0 < 2
3432, 342pm3.2i 469 . . . . . . . . . . . . . . . . . . 19 (2 ∈ ℝ ∧ 0 < 2)
344343a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 ∈ ℝ ∧ 0 < 2))
345 divge0 10741 . . . . . . . . . . . . . . . . . 18 (((((log‘(𝑥 / 𝑛))↑2) ∈ ℝ ∧ 0 ≤ ((log‘(𝑥 / 𝑛))↑2)) ∧ (2 ∈ ℝ ∧ 0 < 2)) → 0 ≤ (((log‘(𝑥 / 𝑛))↑2) / 2))
346339, 341, 344, 345syl21anc 1316 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (((log‘(𝑥 / 𝑛))↑2) / 2))
347340, 346absidd 13955 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(((log‘(𝑥 / 𝑛))↑2) / 2)) = (((log‘(𝑥 / 𝑛))↑2) / 2))
348347adantr 479 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘(((log‘(𝑥 / 𝑛))↑2) / 2)) = (((log‘(𝑥 / 𝑛))↑2) / 2))
3498rpred 11704 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ)
350 ltle 9977 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑥 / 𝑛) ∈ ℝ ∧ e ∈ ℝ) → ((𝑥 / 𝑛) < e → (𝑥 / 𝑛) ≤ e))
351349, 199, 350sylancl 692 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑥 / 𝑛) < e → (𝑥 / 𝑛) ≤ e))
352351imp 443 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (𝑥 / 𝑛) ≤ e)
3538adantr 479 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (𝑥 / 𝑛) ∈ ℝ+)
354 logleb 24070 . . . . . . . . . . . . . . . . . . . . 21 (((𝑥 / 𝑛) ∈ ℝ+ ∧ e ∈ ℝ+) → ((𝑥 / 𝑛) ≤ e ↔ (log‘(𝑥 / 𝑛)) ≤ (log‘e)))
355353, 27, 354sylancl 692 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((𝑥 / 𝑛) ≤ e ↔ (log‘(𝑥 / 𝑛)) ≤ (log‘e)))
356352, 355mpbid 220 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (log‘(𝑥 / 𝑛)) ≤ (log‘e))
357 loge 24054 . . . . . . . . . . . . . . . . . . 19 (log‘e) = 1
358356, 357syl6breq 4618 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (log‘(𝑥 / 𝑛)) ≤ 1)
359 0le1 10400 . . . . . . . . . . . . . . . . . . . . 21 0 ≤ 1
360359a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ 1)
3619, 260, 267, 360le2sqd 12861 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛)) ≤ 1 ↔ ((log‘(𝑥 / 𝑛))↑2) ≤ (1↑2)))
362361adantr 479 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((log‘(𝑥 / 𝑛)) ≤ 1 ↔ ((log‘(𝑥 / 𝑛))↑2) ≤ (1↑2)))
363358, 362mpbid 220 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((log‘(𝑥 / 𝑛))↑2) ≤ (1↑2))
364 sq1 12775 . . . . . . . . . . . . . . . . 17 (1↑2) = 1
365363, 364syl6breq 4618 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((log‘(𝑥 / 𝑛))↑2) ≤ 1)
366339adantr 479 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((log‘(𝑥 / 𝑛))↑2) ∈ ℝ)
367 1red 9911 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → 1 ∈ ℝ)
368343a1i 11 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (2 ∈ ℝ ∧ 0 < 2))
369 lediv1 10737 . . . . . . . . . . . . . . . . 17 ((((log‘(𝑥 / 𝑛))↑2) ∈ ℝ ∧ 1 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (((log‘(𝑥 / 𝑛))↑2) ≤ 1 ↔ (((log‘(𝑥 / 𝑛))↑2) / 2) ≤ (1 / 2)))
370366, 367, 368, 369syl3anc 1317 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (((log‘(𝑥 / 𝑛))↑2) ≤ 1 ↔ (((log‘(𝑥 / 𝑛))↑2) / 2) ≤ (1 / 2)))
371365, 370mpbid 220 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (((log‘(𝑥 / 𝑛))↑2) / 2) ≤ (1 / 2))
372348, 371eqbrtrd 4599 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘(((log‘(𝑥 / 𝑛))↑2) / 2)) ≤ (1 / 2))
37368abscld 13969 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘𝐿) ∈ ℝ)
37466, 373readdcld 9925 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((γ · (log‘(𝑥 / 𝑛))) + (abs‘𝐿)) ∈ ℝ)
375374adantr 479 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((γ · (log‘(𝑥 / 𝑛))) + (abs‘𝐿)) ∈ ℝ)
37667adantr 479 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (γ · (log‘(𝑥 / 𝑛))) ∈ ℂ)
37720ad3antrrr 761 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → 𝐿 ∈ ℂ)
378376, 377abs2dif2d 13991 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘((γ · (log‘(𝑥 / 𝑛))) − 𝐿)) ≤ ((abs‘(γ · (log‘(𝑥 / 𝑛)))) + (abs‘𝐿)))
37917a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → γ ∈ ℝ)
380219a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ γ)
381379, 9, 380, 267mulge0d 10453 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (γ · (log‘(𝑥 / 𝑛))))
38266, 381absidd 13955 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(γ · (log‘(𝑥 / 𝑛)))) = (γ · (log‘(𝑥 / 𝑛))))
383382adantr 479 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘(γ · (log‘(𝑥 / 𝑛)))) = (γ · (log‘(𝑥 / 𝑛))))
384383oveq1d 6542 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((abs‘(γ · (log‘(𝑥 / 𝑛)))) + (abs‘𝐿)) = ((γ · (log‘(𝑥 / 𝑛))) + (abs‘𝐿)))
385378, 384breqtrd 4603 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘((γ · (log‘(𝑥 / 𝑛))) − 𝐿)) ≤ ((γ · (log‘(𝑥 / 𝑛))) + (abs‘𝐿)))
38666adantr 479 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (γ · (log‘(𝑥 / 𝑛))) ∈ ℝ)
38717a1i 11 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → γ ∈ ℝ)
388377abscld 13969 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘𝐿) ∈ ℝ)
3899adantr 479 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (log‘(𝑥 / 𝑛)) ∈ ℝ)
390387, 218jctir 558 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (γ ∈ ℝ ∧ 0 < γ))
391 lemul2 10725 . . . . . . . . . . . . . . . . . . 19 (((log‘(𝑥 / 𝑛)) ∈ ℝ ∧ 1 ∈ ℝ ∧ (γ ∈ ℝ ∧ 0 < γ)) → ((log‘(𝑥 / 𝑛)) ≤ 1 ↔ (γ · (log‘(𝑥 / 𝑛))) ≤ (γ · 1)))
392389, 367, 390, 391syl3anc 1317 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((log‘(𝑥 / 𝑛)) ≤ 1 ↔ (γ · (log‘(𝑥 / 𝑛))) ≤ (γ · 1)))
393358, 392mpbid 220 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (γ · (log‘(𝑥 / 𝑛))) ≤ (γ · 1))
39417recni 9908 . . . . . . . . . . . . . . . . . 18 γ ∈ ℂ
395394mulid1i 9898 . . . . . . . . . . . . . . . . 17 (γ · 1) = γ
396393, 395syl6breq 4618 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (γ · (log‘(𝑥 / 𝑛))) ≤ γ)
397386, 387, 388, 396leadd1dd 10490 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((γ · (log‘(𝑥 / 𝑛))) + (abs‘𝐿)) ≤ (γ + (abs‘𝐿)))
398334, 375, 338, 385, 397letrd 10045 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘((γ · (log‘(𝑥 / 𝑛))) − 𝐿)) ≤ (γ + (abs‘𝐿)))
399332, 334, 337, 338, 372, 398le2addd 10495 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((abs‘(((log‘(𝑥 / 𝑛))↑2) / 2)) + (abs‘((γ · (log‘(𝑥 / 𝑛))) − 𝐿))) ≤ ((1 / 2) + (γ + (abs‘𝐿))))
400330, 335, 327, 336, 399letrd 10045 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ · (log‘(𝑥 / 𝑛))) − 𝐿))) ≤ ((1 / 2) + (γ + (abs‘𝐿))))
401329, 400syl5eqbr 4612 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘𝑇) ≤ ((1 / 2) + (γ + (abs‘𝐿))))
40286, 92sylan2 489 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℝ)
40385, 402fsumrecl 14258 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℝ)
404403adantr 479 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℝ)
40586, 90sylan2 489 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (log‘((𝑥 / 𝑛) / 𝑚)) ∈ ℝ)
40686, 129sylan2 489 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ∈ ℂ)
407406mulid2d 9914 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (1 · 𝑚) = 𝑚)
408 fznnfl 12478 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 / 𝑛) ∈ ℝ → (𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛))) ↔ (𝑚 ∈ ℕ ∧ 𝑚 ≤ (𝑥 / 𝑛))))
409349, 408syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛))) ↔ (𝑚 ∈ ℕ ∧ 𝑚 ≤ (𝑥 / 𝑛))))
410409simplbda 651 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ≤ (𝑥 / 𝑛))
411407, 410eqbrtrd 4599 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (1 · 𝑚) ≤ (𝑥 / 𝑛))
412 1red 9911 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 1 ∈ ℝ)
413349adantr 479 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (𝑥 / 𝑛) ∈ ℝ)
414116rpregt0d 11710 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ ℕ) → (𝑚 ∈ ℝ ∧ 0 < 𝑚))
41586, 414sylan2 489 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (𝑚 ∈ ℝ ∧ 0 < 𝑚))
416 lemuldiv 10752 . . . . . . . . . . . . . . . . . . . 20 ((1 ∈ ℝ ∧ (𝑥 / 𝑛) ∈ ℝ ∧ (𝑚 ∈ ℝ ∧ 0 < 𝑚)) → ((1 · 𝑚) ≤ (𝑥 / 𝑛) ↔ 1 ≤ ((𝑥 / 𝑛) / 𝑚)))
417412, 413, 415, 416syl3anc 1317 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((1 · 𝑚) ≤ (𝑥 / 𝑛) ↔ 1 ≤ ((𝑥 / 𝑛) / 𝑚)))
418411, 417mpbid 220 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 1 ≤ ((𝑥 / 𝑛) / 𝑚))
41986, 89sylan2 489 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((𝑥 / 𝑛) / 𝑚) ∈ ℝ+)
420 logleb 24070 . . . . . . . . . . . . . . . . . . 19 ((1 ∈ ℝ+ ∧ ((𝑥 / 𝑛) / 𝑚) ∈ ℝ+) → (1 ≤ ((𝑥 / 𝑛) / 𝑚) ↔ (log‘1) ≤ (log‘((𝑥 / 𝑛) / 𝑚))))
421211, 419, 420sylancr 693 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (1 ≤ ((𝑥 / 𝑛) / 𝑚) ↔ (log‘1) ≤ (log‘((𝑥 / 𝑛) / 𝑚))))
422418, 421mpbid 220 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (log‘1) ≤ (log‘((𝑥 / 𝑛) / 𝑚)))
423224, 422syl5eqbrr 4613 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 0 ≤ (log‘((𝑥 / 𝑛) / 𝑚)))
424 divge0 10741 . . . . . . . . . . . . . . . 16 ((((log‘((𝑥 / 𝑛) / 𝑚)) ∈ ℝ ∧ 0 ≤ (log‘((𝑥 / 𝑛) / 𝑚))) ∧ (𝑚 ∈ ℝ ∧ 0 < 𝑚)) → 0 ≤ ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))
425405, 423, 415, 424syl21anc 1316 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 0 ≤ ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))
42685, 402, 425fsumge0 14314 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))
427426adantr 479 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → 0 ≤ Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))
428404, 427absidd 13955 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))
429 fzfid 12589 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (1...(⌊‘(𝑥 / 𝑛))) ∈ Fin)
430349flcld 12416 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (⌊‘(𝑥 / 𝑛)) ∈ ℤ)
431430adantr 479 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (⌊‘(𝑥 / 𝑛)) ∈ ℤ)
432 2z 11242 . . . . . . . . . . . . . . . . . . 19 2 ∈ ℤ
433432a1i 11 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → 2 ∈ ℤ)
434349adantr 479 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (𝑥 / 𝑛) ∈ ℝ)
435199a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → e ∈ ℝ)
436 3re 10941 . . . . . . . . . . . . . . . . . . . . . . 23 3 ∈ ℝ
437436a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → 3 ∈ ℝ)
438 simpr 475 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (𝑥 / 𝑛) < e)
439203simpri 476 . . . . . . . . . . . . . . . . . . . . . . 23 e < 3
440439a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → e < 3)
441434, 435, 437, 438, 440lttrd 10049 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (𝑥 / 𝑛) < 3)
442 3z 11243 . . . . . . . . . . . . . . . . . . . . . 22 3 ∈ ℤ
443 fllt 12424 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑥 / 𝑛) ∈ ℝ ∧ 3 ∈ ℤ) → ((𝑥 / 𝑛) < 3 ↔ (⌊‘(𝑥 / 𝑛)) < 3))
444434, 442, 443sylancl 692 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((𝑥 / 𝑛) < 3 ↔ (⌊‘(𝑥 / 𝑛)) < 3))
445441, 444mpbid 220 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (⌊‘(𝑥 / 𝑛)) < 3)
446 df-3 10927 . . . . . . . . . . . . . . . . . . . 20 3 = (2 + 1)
447445, 446syl6breq 4618 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (⌊‘(𝑥 / 𝑛)) < (2 + 1))
448 zleltp1 11261 . . . . . . . . . . . . . . . . . . . 20 (((⌊‘(𝑥 / 𝑛)) ∈ ℤ ∧ 2 ∈ ℤ) → ((⌊‘(𝑥 / 𝑛)) ≤ 2 ↔ (⌊‘(𝑥 / 𝑛)) < (2 + 1)))
449431, 432, 448sylancl 692 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((⌊‘(𝑥 / 𝑛)) ≤ 2 ↔ (⌊‘(𝑥 / 𝑛)) < (2 + 1)))
450447, 449mpbird 245 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (⌊‘(𝑥 / 𝑛)) ≤ 2)
451 eluz2 11525 . . . . . . . . . . . . . . . . . 18 (2 ∈ (ℤ‘(⌊‘(𝑥 / 𝑛))) ↔ ((⌊‘(𝑥 / 𝑛)) ∈ ℤ ∧ 2 ∈ ℤ ∧ (⌊‘(𝑥 / 𝑛)) ≤ 2))
452431, 433, 450, 451syl3anbrc 1238 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → 2 ∈ (ℤ‘(⌊‘(𝑥 / 𝑛))))
453 fzss2 12207 . . . . . . . . . . . . . . . . 17 (2 ∈ (ℤ‘(⌊‘(𝑥 / 𝑛))) → (1...(⌊‘(𝑥 / 𝑛))) ⊆ (1...2))
454452, 453syl 17 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (1...(⌊‘(𝑥 / 𝑛))) ⊆ (1...2))
455454sselda 3567 . . . . . . . . . . . . . . 15 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ∈ (1...2))
456 simplll 793 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → 𝜑)
457456, 34sylan 486 . . . . . . . . . . . . . . 15 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → ((log‘(e / 𝑚)) / 𝑚) ∈ ℝ)
458455, 457syldan 485 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((log‘(e / 𝑚)) / 𝑚) ∈ ℝ)
459429, 458fsumrecl 14258 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘(e / 𝑚)) / 𝑚) ∈ ℝ)
46092adantlr 746 . . . . . . . . . . . . . . 15 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ ℕ) → ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℝ)
46186, 460sylan2 489 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℝ)
462352adantr 479 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → (𝑥 / 𝑛) ≤ e)
463434adantr 479 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → (𝑥 / 𝑛) ∈ ℝ)
464199a1i 11 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → e ∈ ℝ)
46530rpregt0d 11710 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑚 ∈ (1...2)) → (𝑚 ∈ ℝ ∧ 0 < 𝑚))
466456, 465sylan 486 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → (𝑚 ∈ ℝ ∧ 0 < 𝑚))
467 lediv1 10737 . . . . . . . . . . . . . . . . . . 19 (((𝑥 / 𝑛) ∈ ℝ ∧ e ∈ ℝ ∧ (𝑚 ∈ ℝ ∧ 0 < 𝑚)) → ((𝑥 / 𝑛) ≤ e ↔ ((𝑥 / 𝑛) / 𝑚) ≤ (e / 𝑚)))
468463, 464, 466, 467syl3anc 1317 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → ((𝑥 / 𝑛) ≤ e ↔ ((𝑥 / 𝑛) / 𝑚) ≤ (e / 𝑚)))
469462, 468mpbid 220 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → ((𝑥 / 𝑛) / 𝑚) ≤ (e / 𝑚))
47089adantlr 746 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ ℕ) → ((𝑥 / 𝑛) / 𝑚) ∈ ℝ+)
47128, 470sylan2 489 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → ((𝑥 / 𝑛) / 𝑚) ∈ ℝ+)
472456, 32sylan 486 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → (e / 𝑚) ∈ ℝ+)
473471, 472logled 24094 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → (((𝑥 / 𝑛) / 𝑚) ≤ (e / 𝑚) ↔ (log‘((𝑥 / 𝑛) / 𝑚)) ≤ (log‘(e / 𝑚))))
474469, 473mpbid 220 . . . . . . . . . . . . . . . 16 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → (log‘((𝑥 / 𝑛) / 𝑚)) ≤ (log‘(e / 𝑚)))
47590adantlr 746 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ ℕ) → (log‘((𝑥 / 𝑛) / 𝑚)) ∈ ℝ)
47628, 475sylan2 489 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → (log‘((𝑥 / 𝑛) / 𝑚)) ∈ ℝ)
477456, 33sylan 486 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → (log‘(e / 𝑚)) ∈ ℝ)
478 lediv1 10737 . . . . . . . . . . . . . . . . 17 (((log‘((𝑥 / 𝑛) / 𝑚)) ∈ ℝ ∧ (log‘(e / 𝑚)) ∈ ℝ ∧ (𝑚 ∈ ℝ ∧ 0 < 𝑚)) → ((log‘((𝑥 / 𝑛) / 𝑚)) ≤ (log‘(e / 𝑚)) ↔ ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ≤ ((log‘(e / 𝑚)) / 𝑚)))
479476, 477, 466, 478syl3anc 1317 . . . . . . . . . . . . . . . 16 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → ((log‘((𝑥 / 𝑛) / 𝑚)) ≤ (log‘(e / 𝑚)) ↔ ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ≤ ((log‘(e / 𝑚)) / 𝑚)))
480474, 479mpbid 220 . . . . . . . . . . . . . . 15 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ≤ ((log‘(e / 𝑚)) / 𝑚))
481455, 480syldan 485 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ≤ ((log‘(e / 𝑚)) / 𝑚))
482429, 461, 458, 481fsumle 14318 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ≤ Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘(e / 𝑚)) / 𝑚))
483 fzfid 12589 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (1...2) ∈ Fin)
484456, 243sylan 486 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → 0 ≤ ((log‘(e / 𝑚)) / 𝑚))
485483, 457, 484, 454fsumless 14315 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘(e / 𝑚)) / 𝑚) ≤ Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚))
486404, 459, 328, 482, 485letrd 10045 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ≤ Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚))
487428, 486eqbrtrd 4599 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) ≤ Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚))
488322, 324, 327, 328, 401, 487le2addd 10495 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((abs‘𝑇) + (abs‘Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ≤ (((1 / 2) + (γ + (abs‘𝐿))) + Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚)))
489488, 15syl6breqr 4619 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → ((abs‘𝑇) + (abs‘Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ≤ 𝑅)
490318, 325, 319, 326, 489letrd 10045 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ≤ 𝑅)
491317, 318, 319, 320, 490letrd 10045 . . . . . . 7 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ (𝑥 / 𝑛) < e) → (abs‘((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ≤ 𝑅)
4924, 208, 248, 249, 251, 272, 316, 491fsumharmonic 24455 . . . . . 6 ((𝜑𝑥 ∈ ℝ+) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛)) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))(2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · ((log‘e) + 1))))
493 2cnd 10940 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ+) → 2 ∈ ℂ)
4943, 493, 303fsummulc2 14304 . . . . . . 7 ((𝜑𝑥 ∈ ℝ+) → (2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) = Σ𝑛 ∈ (1...(⌊‘𝑥))(2 · ((log‘(𝑥 / 𝑛)) / 𝑥)))
495 df-2 10926 . . . . . . . . . 10 2 = (1 + 1)
496357oveq1i 6537 . . . . . . . . . 10 ((log‘e) + 1) = (1 + 1)
497495, 496eqtr4i 2634 . . . . . . . . 9 2 = ((log‘e) + 1)
498497a1i 11 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ+) → 2 = ((log‘e) + 1))
499498oveq2d 6543 . . . . . . 7 ((𝜑𝑥 ∈ ℝ+) → (𝑅 · 2) = (𝑅 · ((log‘e) + 1)))
500494, 499oveq12d 6545 . . . . . 6 ((𝜑𝑥 ∈ ℝ+) → ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · ((log‘e) + 1))))
501492, 500breqtrrd 4605 . . . . 5 ((𝜑𝑥 ∈ ℝ+) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛)) ≤ ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2)))
502501adantrr 748 . . . 4 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛)) ≤ ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2)))
503198, 502eqbrtrrd 4601 . . 3 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥))) ≤ ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2)))
50454leabsd 13947 . . . 4 ((𝜑𝑥 ∈ ℝ+) → ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2)) ≤ (abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2))))
505504adantrr 748 . . 3 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2)) ≤ (abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2))))
50679, 80, 83, 503, 505letrd 10045 . 2 ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥))) ≤ (abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2))))
5071, 53, 54, 77, 506o1le 14177 1 (𝜑 → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥))) ∈ 𝑂(1))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382  w3a 1030   = wceq 1474  wcel 1976  wne 2779  {crab 2899  wss 3539   class class class wbr 4577  cmpt 4637  cfv 5790  (class class class)co 6527  cc 9790  cr 9791  0cc0 9792  1c1 9793   + caddc 9795   · cmul 9797   < clt 9930  cle 9931  cmin 10117   / cdiv 10533  cn 10867  2c2 10917  3c3 10918  cz 11210  cuz 11519  +crp 11664  ...cfz 12152  cfl 12408  cexp 12677  abscabs 13768  𝑟 crli 14010  𝑂(1)co1 14011  Σcsu 14210  eceu 14578  cdvds 14767  logclog 24022  γcem 24435  μcmu 24538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824  ax-inf2 8398  ax-cnex 9848  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868  ax-pre-mulgt0 9869  ax-pre-sup 9870  ax-addf 9871  ax-mulf 9872
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 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-iin 4452  df-disj 4548  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-se 4988  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-isom 5799  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-of 6772  df-om 6935  df-1st 7036  df-2nd 7037  df-supp 7160  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-1o 7424  df-2o 7425  df-oadd 7428  df-er 7606  df-map 7723  df-pm 7724  df-ixp 7772  df-en 7819  df-dom 7820  df-sdom 7821  df-fin 7822  df-fsupp 8136  df-fi 8177  df-sup 8208  df-inf 8209  df-oi 8275  df-card 8625  df-cda 8850  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-sub 10119  df-neg 10120  df-div 10534  df-nn 10868  df-2 10926  df-3 10927  df-4 10928  df-5 10929  df-6 10930  df-7 10931  df-8 10932  df-9 10933  df-n0 11140  df-z 11211  df-dec 11326  df-uz 11520  df-q 11621  df-rp 11665  df-xneg 11778  df-xadd 11779  df-xmul 11780  df-ioo 12006  df-ioc 12007  df-ico 12008  df-icc 12009  df-fz 12153  df-fzo 12290  df-fl 12410  df-mod 12486  df-seq 12619  df-exp 12678  df-fac 12878  df-bc 12907  df-hash 12935  df-shft 13601  df-cj 13633  df-re 13634  df-im 13635  df-sqrt 13769  df-abs 13770  df-limsup 13996  df-clim 14013  df-rlim 14014  df-o1 14015  df-lo1 14016  df-sum 14211  df-ef 14583  df-e 14584  df-sin 14585  df-cos 14586  df-pi 14588  df-dvds 14768  df-gcd 15001  df-prm 15170  df-pc 15326  df-struct 15643  df-ndx 15644  df-slot 15645  df-base 15646  df-sets 15647  df-ress 15648  df-plusg 15727  df-mulr 15728  df-starv 15729  df-sca 15730  df-vsca 15731  df-ip 15732  df-tset 15733  df-ple 15734  df-ds 15737  df-unif 15738  df-hom 15739  df-cco 15740  df-rest 15852  df-topn 15853  df-0g 15871  df-gsum 15872  df-topgen 15873  df-pt 15874  df-prds 15877  df-xrs 15931  df-qtop 15936  df-imas 15937  df-xps 15939  df-mre 16015  df-mrc 16016  df-acs 16018  df-mgm 17011  df-sgrp 17053  df-mnd 17064  df-submnd 17105  df-mulg 17310  df-cntz 17519  df-cmn 17964  df-psmet 19505  df-xmet 19506  df-met 19507  df-bl 19508  df-mopn 19509  df-fbas 19510  df-fg 19511  df-cnfld 19514  df-top 20463  df-bases 20464  df-topon 20465  df-topsp 20466  df-cld 20575  df-ntr 20576  df-cls 20577  df-nei 20654  df-lp 20692  df-perf 20693  df-cn 20783  df-cnp 20784  df-haus 20871  df-cmp 20942  df-tx 21117  df-hmeo 21310  df-fil 21402  df-fm 21494  df-flim 21495  df-flf 21496  df-xms 21876  df-ms 21877  df-tms 21878  df-cncf 22420  df-limc 23353  df-dv 23354  df-log 24024  df-cxp 24025  df-em 24436  df-mu 24544
This theorem is referenced by:  mulog2sumlem3  24942
  Copyright terms: Public domain W3C validator