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

Theorem 2vmadivsumlem 26794
Description: Lemma for 2vmadivsum 26795. (Contributed by Mario Carneiro, 30-May-2016.)
Hypotheses
Ref Expression
2vmadivsum.1 (𝜑𝐴 ∈ ℝ+)
2vmadivsum.2 (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘(Σ𝑖 ∈ (1...(⌊‘𝑦))((Λ‘𝑖) / 𝑖) − (log‘𝑦))) ≤ 𝐴)
Assertion
Ref Expression
2vmadivsumlem (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥)) − ((log‘𝑥) / 2))) ∈ 𝑂(1))
Distinct variable groups:   𝑖,𝑚,𝑛,𝑥,𝑦,𝐴   𝜑,𝑚,𝑛,𝑥
Allowed substitution hints:   𝜑(𝑦,𝑖)

Proof of Theorem 2vmadivsumlem
StepHypRef Expression
1 vmalogdivsum2 26792 . . 3 (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2))) ∈ 𝑂(1)
21a1i 11 . 2 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2))) ∈ 𝑂(1))
3 fzfid 13794 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → (1...(⌊‘𝑥)) ∈ Fin)
4 elfznn 13386 . . . . . . . . . . 11 (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
54adantl 482 . . . . . . . . . 10 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
6 vmacl 26373 . . . . . . . . . 10 (𝑛 ∈ ℕ → (Λ‘𝑛) ∈ ℝ)
75, 6syl 17 . . . . . . . . 9 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈ ℝ)
87, 5nndivred 12128 . . . . . . . 8 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) / 𝑛) ∈ ℝ)
9 fzfid 13794 . . . . . . . . 9 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1...(⌊‘(𝑥 / 𝑛))) ∈ Fin)
10 elfznn 13386 . . . . . . . . . . . 12 (𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛))) → 𝑚 ∈ ℕ)
1110adantl 482 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ∈ ℕ)
12 vmacl 26373 . . . . . . . . . . 11 (𝑚 ∈ ℕ → (Λ‘𝑚) ∈ ℝ)
1311, 12syl 17 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (Λ‘𝑚) ∈ ℝ)
1413, 11nndivred 12128 . . . . . . . . 9 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((Λ‘𝑚) / 𝑚) ∈ ℝ)
159, 14fsumrecl 15545 . . . . . . . 8 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) ∈ ℝ)
168, 15remulcld 11106 . . . . . . 7 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) ∈ ℝ)
173, 16fsumrecl 15545 . . . . . 6 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) ∈ ℝ)
18 elioore 13210 . . . . . . . 8 (𝑥 ∈ (1(,)+∞) → 𝑥 ∈ ℝ)
1918adantl 482 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → 𝑥 ∈ ℝ)
20 eliooord 13239 . . . . . . . . 9 (𝑥 ∈ (1(,)+∞) → (1 < 𝑥𝑥 < +∞))
2120adantl 482 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → (1 < 𝑥𝑥 < +∞))
2221simpld 495 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → 1 < 𝑥)
2319, 22rplogcld 25890 . . . . . 6 ((𝜑𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ∈ ℝ+)
2417, 23rerpdivcld 12904 . . . . 5 ((𝜑𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥)) ∈ ℝ)
25 1rp 12835 . . . . . . . . 9 1 ∈ ℝ+
2625a1i 11 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → 1 ∈ ℝ+)
27 1red 11077 . . . . . . . . 9 ((𝜑𝑥 ∈ (1(,)+∞)) → 1 ∈ ℝ)
2827, 19, 22ltled 11224 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → 1 ≤ 𝑥)
2919, 26, 28rpgecld 12912 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → 𝑥 ∈ ℝ+)
3029relogcld 25884 . . . . . 6 ((𝜑𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ∈ ℝ)
3130rehalfcld 12321 . . . . 5 ((𝜑𝑥 ∈ (1(,)+∞)) → ((log‘𝑥) / 2) ∈ ℝ)
3224, 31resubcld 11504 . . . 4 ((𝜑𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥)) − ((log‘𝑥) / 2)) ∈ ℝ)
3332recnd 11104 . . 3 ((𝜑𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥)) − ((log‘𝑥) / 2)) ∈ ℂ)
3429adantr 481 . . . . . . . . . 10 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ+)
355nnrpd 12871 . . . . . . . . . 10 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ+)
3634, 35rpdivcld 12890 . . . . . . . . 9 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ+)
3736relogcld 25884 . . . . . . . 8 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ∈ ℝ)
388, 37remulcld 11106 . . . . . . 7 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) ∈ ℝ)
393, 38fsumrecl 15545 . . . . . 6 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) ∈ ℝ)
4039, 23rerpdivcld 12904 . . . . 5 ((𝜑𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) ∈ ℝ)
4140, 31resubcld 11504 . . . 4 ((𝜑𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2)) ∈ ℝ)
4241recnd 11104 . . 3 ((𝜑𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2)) ∈ ℂ)
4317recnd 11104 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) ∈ ℂ)
4439recnd 11104 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) ∈ ℂ)
4530recnd 11104 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ∈ ℂ)
4623rpne0d 12878 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ≠ 0)
4743, 44, 45, 46divsubdird 11891 . . . . . 6 ((𝜑𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) / (log‘𝑥)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥))))
488recnd 11104 . . . . . . . . . 10 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) / 𝑛) ∈ ℂ)
4915recnd 11104 . . . . . . . . . 10 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) ∈ ℂ)
5037recnd 11104 . . . . . . . . . 10 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ∈ ℂ)
5148, 49, 50subdid 11532 . . . . . . . . 9 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) = ((((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) − (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))))
5251sumeq2dv 15514 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) − (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))))
5316recnd 11104 . . . . . . . . 9 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) ∈ ℂ)
5438recnd 11104 . . . . . . . . 9 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) ∈ ℂ)
553, 53, 54fsumsub 15599 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) − (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))))
5652, 55eqtrd 2776 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))))
5756oveq1d 7352 . . . . . 6 ((𝜑𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) / (log‘𝑥)))
5824recnd 11104 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥)) ∈ ℂ)
5940recnd 11104 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) ∈ ℂ)
6031recnd 11104 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → ((log‘𝑥) / 2) ∈ ℂ)
6158, 59, 60nnncan2d 11468 . . . . . 6 ((𝜑𝑥 ∈ (1(,)+∞)) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥)) − ((log‘𝑥) / 2)) − ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥))))
6247, 57, 613eqtr4d 2786 . . . . 5 ((𝜑𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥)) = (((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥)) − ((log‘𝑥) / 2)) − ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2))))
6362mpteq2dva 5192 . . . 4 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥))) = (𝑥 ∈ (1(,)+∞) ↦ (((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥)) − ((log‘𝑥) / 2)) − ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2)))))
64 1red 11077 . . . . 5 (𝜑 → 1 ∈ ℝ)
653, 8fsumrecl 15545 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ∈ ℝ)
6665, 23rerpdivcld 12904 . . . . . 6 ((𝜑𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) ∈ ℝ)
67 2vmadivsum.1 . . . . . . . 8 (𝜑𝐴 ∈ ℝ+)
6867rpred 12873 . . . . . . 7 (𝜑𝐴 ∈ ℝ)
6968adantr 481 . . . . . 6 ((𝜑𝑥 ∈ (1(,)+∞)) → 𝐴 ∈ ℝ)
70 ioossre 13241 . . . . . . . 8 (1(,)+∞) ⊆ ℝ
71 1cnd 11071 . . . . . . . 8 (𝜑 → 1 ∈ ℂ)
72 o1const 15428 . . . . . . . 8 (((1(,)+∞) ⊆ ℝ ∧ 1 ∈ ℂ) → (𝑥 ∈ (1(,)+∞) ↦ 1) ∈ 𝑂(1))
7370, 71, 72sylancr 587 . . . . . . 7 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ 1) ∈ 𝑂(1))
7466recnd 11104 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) ∈ ℂ)
75 1cnd 11071 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → 1 ∈ ℂ)
7665recnd 11104 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ∈ ℂ)
7776, 45, 45, 46divsubdird 11891 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) / (log‘𝑥)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) − ((log‘𝑥) / (log‘𝑥))))
7876, 45subcld 11433 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) ∈ ℂ)
7978, 45, 46divrecd 11855 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) / (log‘𝑥)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) · (1 / (log‘𝑥))))
8045, 46dividd 11850 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1(,)+∞)) → ((log‘𝑥) / (log‘𝑥)) = 1)
8180oveq2d 7353 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) − ((log‘𝑥) / (log‘𝑥))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) − 1))
8277, 79, 813eqtr3d 2784 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) · (1 / (log‘𝑥))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) − 1))
8382mpteq2dva 5192 . . . . . . . . 9 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) · (1 / (log‘𝑥)))) = (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) − 1)))
8465, 30resubcld 11504 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) ∈ ℝ)
8527, 23rerpdivcld 12904 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1(,)+∞)) → (1 / (log‘𝑥)) ∈ ℝ)
8629ex 413 . . . . . . . . . . . 12 (𝜑 → (𝑥 ∈ (1(,)+∞) → 𝑥 ∈ ℝ+))
8786ssrdv 3938 . . . . . . . . . . 11 (𝜑 → (1(,)+∞) ⊆ ℝ+)
88 vmadivsum 26736 . . . . . . . . . . . 12 (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1)
8988a1i 11 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1))
9087, 89o1res2 15371 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1))
91 divlogrlim 25896 . . . . . . . . . . 11 (𝑥 ∈ (1(,)+∞) ↦ (1 / (log‘𝑥))) ⇝𝑟 0
92 rlimo1 15425 . . . . . . . . . . 11 ((𝑥 ∈ (1(,)+∞) ↦ (1 / (log‘𝑥))) ⇝𝑟 0 → (𝑥 ∈ (1(,)+∞) ↦ (1 / (log‘𝑥))) ∈ 𝑂(1))
9391, 92mp1i 13 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (1 / (log‘𝑥))) ∈ 𝑂(1))
9484, 85, 90, 93o1mul2 15433 . . . . . . . . 9 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) · (1 / (log‘𝑥)))) ∈ 𝑂(1))
9583, 94eqeltrrd 2838 . . . . . . . 8 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) − 1)) ∈ 𝑂(1))
9674, 75, 95o1dif 15438 . . . . . . 7 (𝜑 → ((𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥))) ∈ 𝑂(1) ↔ (𝑥 ∈ (1(,)+∞) ↦ 1) ∈ 𝑂(1)))
9773, 96mpbird 256 . . . . . 6 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥))) ∈ 𝑂(1))
9868recnd 11104 . . . . . . 7 (𝜑𝐴 ∈ ℂ)
99 o1const 15428 . . . . . . 7 (((1(,)+∞) ⊆ ℝ ∧ 𝐴 ∈ ℂ) → (𝑥 ∈ (1(,)+∞) ↦ 𝐴) ∈ 𝑂(1))
10070, 98, 99sylancr 587 . . . . . 6 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ 𝐴) ∈ 𝑂(1))
10166, 69, 97, 100o1mul2 15433 . . . . 5 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) · 𝐴)) ∈ 𝑂(1))
10266, 69remulcld 11106 . . . . 5 ((𝜑𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) · 𝐴) ∈ ℝ)
10315, 37resubcld 11504 . . . . . . . . 9 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))) ∈ ℝ)
1048, 103remulcld 11106 . . . . . . . 8 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) ∈ ℝ)
1053, 104fsumrecl 15545 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) ∈ ℝ)
106105recnd 11104 . . . . . 6 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) ∈ ℂ)
107106, 45, 46divcld 11852 . . . . 5 ((𝜑𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥)) ∈ ℂ)
108106abscld 15247 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) ∈ ℝ)
10965, 69remulcld 11106 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝐴) ∈ ℝ)
110104recnd 11104 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) ∈ ℂ)
111110abscld 15247 . . . . . . . . . 10 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) ∈ ℝ)
1123, 111fsumrecl 15545 . . . . . . . . 9 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) ∈ ℝ)
1133, 110fsumabs 15612 . . . . . . . . 9 ((𝜑𝑥 ∈ (1(,)+∞)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))))
11469adantr 481 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝐴 ∈ ℝ)
1158, 114remulcld 11106 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) / 𝑛) · 𝐴) ∈ ℝ)
116103recnd 11104 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))) ∈ ℂ)
11748, 116absmuld 15265 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) = ((abs‘((Λ‘𝑛) / 𝑛)) · (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))))
118 vmage0 26376 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ → 0 ≤ (Λ‘𝑛))
1195, 118syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (Λ‘𝑛))
1207, 35, 119divge0d 12913 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ ((Λ‘𝑛) / 𝑛))
1218, 120absidd 15233 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((Λ‘𝑛) / 𝑛)) = ((Λ‘𝑛) / 𝑛))
122121oveq1d 7352 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘((Λ‘𝑛) / 𝑛)) · (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) = (((Λ‘𝑛) / 𝑛) · (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))))
123117, 122eqtrd 2776 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) = (((Λ‘𝑛) / 𝑛) · (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))))
124116abscld 15247 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) ∈ ℝ)
125 fveq2 6825 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑚 → (Λ‘𝑖) = (Λ‘𝑚))
126 id 22 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑚𝑖 = 𝑚)
127125, 126oveq12d 7355 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑚 → ((Λ‘𝑖) / 𝑖) = ((Λ‘𝑚) / 𝑚))
128127cbvsumv 15507 . . . . . . . . . . . . . . . . . 18 Σ𝑖 ∈ (1...(⌊‘𝑦))((Λ‘𝑖) / 𝑖) = Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) / 𝑚)
129 fveq2 6825 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝑥 / 𝑛) → (⌊‘𝑦) = (⌊‘(𝑥 / 𝑛)))
130129oveq2d 7353 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝑥 / 𝑛) → (1...(⌊‘𝑦)) = (1...(⌊‘(𝑥 / 𝑛))))
131130sumeq1d 15512 . . . . . . . . . . . . . . . . . 18 (𝑦 = (𝑥 / 𝑛) → Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) / 𝑚) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚))
132128, 131eqtrid 2788 . . . . . . . . . . . . . . . . 17 (𝑦 = (𝑥 / 𝑛) → Σ𝑖 ∈ (1...(⌊‘𝑦))((Λ‘𝑖) / 𝑖) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚))
133 fveq2 6825 . . . . . . . . . . . . . . . . 17 (𝑦 = (𝑥 / 𝑛) → (log‘𝑦) = (log‘(𝑥 / 𝑛)))
134132, 133oveq12d 7355 . . . . . . . . . . . . . . . 16 (𝑦 = (𝑥 / 𝑛) → (Σ𝑖 ∈ (1...(⌊‘𝑦))((Λ‘𝑖) / 𝑖) − (log‘𝑦)) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))
135134fveq2d 6829 . . . . . . . . . . . . . . 15 (𝑦 = (𝑥 / 𝑛) → (abs‘(Σ𝑖 ∈ (1...(⌊‘𝑦))((Λ‘𝑖) / 𝑖) − (log‘𝑦))) = (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))))
136135breq1d 5102 . . . . . . . . . . . . . 14 (𝑦 = (𝑥 / 𝑛) → ((abs‘(Σ𝑖 ∈ (1...(⌊‘𝑦))((Λ‘𝑖) / 𝑖) − (log‘𝑦))) ≤ 𝐴 ↔ (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) ≤ 𝐴))
137 2vmadivsum.2 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘(Σ𝑖 ∈ (1...(⌊‘𝑦))((Λ‘𝑖) / 𝑖) − (log‘𝑦))) ≤ 𝐴)
138137ad2antrr 723 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ∀𝑦 ∈ (1[,)+∞)(abs‘(Σ𝑖 ∈ (1...(⌊‘𝑦))((Λ‘𝑖) / 𝑖) − (log‘𝑦))) ≤ 𝐴)
13936rpred 12873 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ)
1405nncnd 12090 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℂ)
141140mulid2d 11094 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 · 𝑛) = 𝑛)
142 fznnfl 13683 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℝ → (𝑛 ∈ (1...(⌊‘𝑥)) ↔ (𝑛 ∈ ℕ ∧ 𝑛𝑥)))
14319, 142syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (1(,)+∞)) → (𝑛 ∈ (1...(⌊‘𝑥)) ↔ (𝑛 ∈ ℕ ∧ 𝑛𝑥)))
144143simplbda 500 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛𝑥)
145141, 144eqbrtrd 5114 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 · 𝑛) ≤ 𝑥)
146 1red 11077 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℝ)
14719adantr 481 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ)
148146, 147, 35lemuldivd 12922 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 · 𝑛) ≤ 𝑥 ↔ 1 ≤ (𝑥 / 𝑛)))
149145, 148mpbid 231 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ≤ (𝑥 / 𝑛))
150 1re 11076 . . . . . . . . . . . . . . . 16 1 ∈ ℝ
151 elicopnf 13278 . . . . . . . . . . . . . . . 16 (1 ∈ ℝ → ((𝑥 / 𝑛) ∈ (1[,)+∞) ↔ ((𝑥 / 𝑛) ∈ ℝ ∧ 1 ≤ (𝑥 / 𝑛))))
152150, 151ax-mp 5 . . . . . . . . . . . . . . 15 ((𝑥 / 𝑛) ∈ (1[,)+∞) ↔ ((𝑥 / 𝑛) ∈ ℝ ∧ 1 ≤ (𝑥 / 𝑛)))
153139, 149, 152sylanbrc 583 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ (1[,)+∞))
154136, 138, 153rspcdva 3571 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) ≤ 𝐴)
155124, 114, 8, 120, 154lemul2ad 12016 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) / 𝑛) · (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) ≤ (((Λ‘𝑛) / 𝑛) · 𝐴))
156123, 155eqbrtrd 5114 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) ≤ (((Λ‘𝑛) / 𝑛) · 𝐴))
1573, 111, 115, 156fsumle 15610 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · 𝐴))
15898adantr 481 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1(,)+∞)) → 𝐴 ∈ ℂ)
1593, 158, 48fsummulc1 15596 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝐴) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · 𝐴))
160157, 159breqtrrd 5120 . . . . . . . . 9 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝐴))
161108, 112, 109, 113, 160letrd 11233 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝐴))
162108, 109, 23, 161lediv1dd 12931 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) / (log‘𝑥)) ≤ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝐴) / (log‘𝑥)))
163106, 45, 46absdivd 15266 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥))) = ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) / (abs‘(log‘𝑥))))
16423rpge0d 12877 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1(,)+∞)) → 0 ≤ (log‘𝑥))
16530, 164absidd 15233 . . . . . . . . 9 ((𝜑𝑥 ∈ (1(,)+∞)) → (abs‘(log‘𝑥)) = (log‘𝑥))
166165oveq2d 7353 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) / (abs‘(log‘𝑥))) = ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) / (log‘𝑥)))
167163, 166eqtrd 2776 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥))) = ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) / (log‘𝑥)))
1683, 8, 120fsumge0 15606 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1(,)+∞)) → 0 ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛))
16965, 23, 168divge0d 12913 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1(,)+∞)) → 0 ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)))
17067adantr 481 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1(,)+∞)) → 𝐴 ∈ ℝ+)
171170rpge0d 12877 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1(,)+∞)) → 0 ≤ 𝐴)
17266, 69, 169, 171mulge0d 11653 . . . . . . . . 9 ((𝜑𝑥 ∈ (1(,)+∞)) → 0 ≤ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) · 𝐴))
173102, 172absidd 15233 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) · 𝐴)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) · 𝐴))
17476, 158, 45, 46div23d 11889 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝐴) / (log‘𝑥)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) · 𝐴))
175173, 174eqtr4d 2779 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) · 𝐴)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝐴) / (log‘𝑥)))
176162, 167, 1753brtr4d 5124 . . . . . 6 ((𝜑𝑥 ∈ (1(,)+∞)) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥))) ≤ (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) · 𝐴)))
177176adantrr 714 . . . . 5 ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ 1 ≤ 𝑥)) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥))) ≤ (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) · 𝐴)))
17864, 101, 102, 107, 177o1le 15463 . . . 4 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥))) ∈ 𝑂(1))
17963, 178eqeltrrd 2838 . . 3 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥)) − ((log‘𝑥) / 2)) − ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2)))) ∈ 𝑂(1))
18033, 42, 179o1dif 15438 . 2 (𝜑 → ((𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥)) − ((log‘𝑥) / 2))) ∈ 𝑂(1) ↔ (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2))) ∈ 𝑂(1)))
1812, 180mpbird 256 1 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥)) − ((log‘𝑥) / 2))) ∈ 𝑂(1))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1540  wcel 2105  wral 3061  wss 3898   class class class wbr 5092  cmpt 5175  cfv 6479  (class class class)co 7337  cc 10970  cr 10971  0cc0 10972  1c1 10973   · cmul 10977  +∞cpnf 11107   < clt 11110  cle 11111  cmin 11306   / cdiv 11733  cn 12074  2c2 12129  +crp 12831  (,)cioo 13180  [,)cico 13182  ...cfz 13340  cfl 13611  abscabs 15044  𝑟 crli 15293  𝑂(1)co1 15294  Σcsu 15496  logclog 25816  Λcvma 26347
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5229  ax-sep 5243  ax-nul 5250  ax-pow 5308  ax-pr 5372  ax-un 7650  ax-inf2 9498  ax-cnex 11028  ax-resscn 11029  ax-1cn 11030  ax-icn 11031  ax-addcl 11032  ax-addrcl 11033  ax-mulcl 11034  ax-mulrcl 11035  ax-mulcom 11036  ax-addass 11037  ax-mulass 11038  ax-distr 11039  ax-i2m1 11040  ax-1ne0 11041  ax-1rid 11042  ax-rnegex 11043  ax-rrecex 11044  ax-cnre 11045  ax-pre-lttri 11046  ax-pre-lttrn 11047  ax-pre-ltadd 11048  ax-pre-mulgt0 11049  ax-pre-sup 11050  ax-addf 11051  ax-mulf 11052
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3728  df-csb 3844  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3917  df-nul 4270  df-if 4474  df-pw 4549  df-sn 4574  df-pr 4576  df-tp 4578  df-op 4580  df-uni 4853  df-int 4895  df-iun 4943  df-iin 4944  df-br 5093  df-opab 5155  df-mpt 5176  df-tr 5210  df-id 5518  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5575  df-se 5576  df-we 5577  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-pred 6238  df-ord 6305  df-on 6306  df-lim 6307  df-suc 6308  df-iota 6431  df-fun 6481  df-fn 6482  df-f 6483  df-f1 6484  df-fo 6485  df-f1o 6486  df-fv 6487  df-isom 6488  df-riota 7293  df-ov 7340  df-oprab 7341  df-mpo 7342  df-of 7595  df-om 7781  df-1st 7899  df-2nd 7900  df-supp 8048  df-frecs 8167  df-wrecs 8198  df-recs 8272  df-rdg 8311  df-1o 8367  df-2o 8368  df-oadd 8371  df-er 8569  df-map 8688  df-pm 8689  df-ixp 8757  df-en 8805  df-dom 8806  df-sdom 8807  df-fin 8808  df-fsupp 9227  df-fi 9268  df-sup 9299  df-inf 9300  df-oi 9367  df-dju 9758  df-card 9796  df-pnf 11112  df-mnf 11113  df-xr 11114  df-ltxr 11115  df-le 11116  df-sub 11308  df-neg 11309  df-div 11734  df-nn 12075  df-2 12137  df-3 12138  df-4 12139  df-5 12140  df-6 12141  df-7 12142  df-8 12143  df-9 12144  df-n0 12335  df-xnn0 12407  df-z 12421  df-dec 12539  df-uz 12684  df-q 12790  df-rp 12832  df-xneg 12949  df-xadd 12950  df-xmul 12951  df-ioo 13184  df-ioc 13185  df-ico 13186  df-icc 13187  df-fz 13341  df-fzo 13484  df-fl 13613  df-mod 13691  df-seq 13823  df-exp 13884  df-fac 14089  df-bc 14118  df-hash 14146  df-shft 14877  df-cj 14909  df-re 14910  df-im 14911  df-sqrt 15045  df-abs 15046  df-limsup 15279  df-clim 15296  df-rlim 15297  df-o1 15298  df-lo1 15299  df-sum 15497  df-ef 15876  df-e 15877  df-sin 15878  df-cos 15879  df-tan 15880  df-pi 15881  df-dvds 16063  df-gcd 16301  df-prm 16474  df-pc 16635  df-struct 16945  df-sets 16962  df-slot 16980  df-ndx 16992  df-base 17010  df-ress 17039  df-plusg 17072  df-mulr 17073  df-starv 17074  df-sca 17075  df-vsca 17076  df-ip 17077  df-tset 17078  df-ple 17079  df-ds 17081  df-unif 17082  df-hom 17083  df-cco 17084  df-rest 17230  df-topn 17231  df-0g 17249  df-gsum 17250  df-topgen 17251  df-pt 17252  df-prds 17255  df-xrs 17310  df-qtop 17315  df-imas 17316  df-xps 17318  df-mre 17392  df-mrc 17393  df-acs 17395  df-mgm 18423  df-sgrp 18472  df-mnd 18483  df-submnd 18528  df-mulg 18797  df-cntz 19019  df-cmn 19483  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
This theorem is referenced by:  2vmadivsum  26795
  Copyright terms: Public domain W3C validator