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

Theorem 2vmadivsumlem 27566
Description: Lemma for 2vmadivsum 27567. (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 27564 . . 3 (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2))) ∈ 𝑂(1)
21a1i 11 . 2 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2))) ∈ 𝑂(1))
3 fzfid 13987 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → (1...(⌊‘𝑥)) ∈ Fin)
4 elfznn 13578 . . . . . . . . . . 11 (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
54adantl 480 . . . . . . . . . 10 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
6 vmacl 27143 . . . . . . . . . 10 (𝑛 ∈ ℕ → (Λ‘𝑛) ∈ ℝ)
75, 6syl 17 . . . . . . . . 9 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈ ℝ)
87, 5nndivred 12312 . . . . . . . 8 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) / 𝑛) ∈ ℝ)
9 fzfid 13987 . . . . . . . . 9 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1...(⌊‘(𝑥 / 𝑛))) ∈ Fin)
10 elfznn 13578 . . . . . . . . . . . 12 (𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛))) → 𝑚 ∈ ℕ)
1110adantl 480 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ∈ ℕ)
12 vmacl 27143 . . . . . . . . . . 11 (𝑚 ∈ ℕ → (Λ‘𝑚) ∈ ℝ)
1311, 12syl 17 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (Λ‘𝑚) ∈ ℝ)
1413, 11nndivred 12312 . . . . . . . . 9 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((Λ‘𝑚) / 𝑚) ∈ ℝ)
159, 14fsumrecl 15733 . . . . . . . 8 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) ∈ ℝ)
168, 15remulcld 11285 . . . . . . 7 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) ∈ ℝ)
173, 16fsumrecl 15733 . . . . . 6 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) ∈ ℝ)
18 elioore 13402 . . . . . . . 8 (𝑥 ∈ (1(,)+∞) → 𝑥 ∈ ℝ)
1918adantl 480 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → 𝑥 ∈ ℝ)
20 eliooord 13431 . . . . . . . . 9 (𝑥 ∈ (1(,)+∞) → (1 < 𝑥𝑥 < +∞))
2120adantl 480 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → (1 < 𝑥𝑥 < +∞))
2221simpld 493 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → 1 < 𝑥)
2319, 22rplogcld 26653 . . . . . 6 ((𝜑𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ∈ ℝ+)
2417, 23rerpdivcld 13095 . . . . 5 ((𝜑𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥)) ∈ ℝ)
25 1rp 13026 . . . . . . . . 9 1 ∈ ℝ+
2625a1i 11 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → 1 ∈ ℝ+)
27 1red 11256 . . . . . . . . 9 ((𝜑𝑥 ∈ (1(,)+∞)) → 1 ∈ ℝ)
2827, 19, 22ltled 11403 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → 1 ≤ 𝑥)
2919, 26, 28rpgecld 13103 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → 𝑥 ∈ ℝ+)
3029relogcld 26647 . . . . . 6 ((𝜑𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ∈ ℝ)
3130rehalfcld 12505 . . . . 5 ((𝜑𝑥 ∈ (1(,)+∞)) → ((log‘𝑥) / 2) ∈ ℝ)
3224, 31resubcld 11683 . . . 4 ((𝜑𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥)) − ((log‘𝑥) / 2)) ∈ ℝ)
3332recnd 11283 . . 3 ((𝜑𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥)) − ((log‘𝑥) / 2)) ∈ ℂ)
3429adantr 479 . . . . . . . . . 10 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ+)
355nnrpd 13062 . . . . . . . . . 10 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ+)
3634, 35rpdivcld 13081 . . . . . . . . 9 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ+)
3736relogcld 26647 . . . . . . . 8 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ∈ ℝ)
388, 37remulcld 11285 . . . . . . 7 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) ∈ ℝ)
393, 38fsumrecl 15733 . . . . . 6 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) ∈ ℝ)
4039, 23rerpdivcld 13095 . . . . 5 ((𝜑𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) ∈ ℝ)
4140, 31resubcld 11683 . . . 4 ((𝜑𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2)) ∈ ℝ)
4241recnd 11283 . . 3 ((𝜑𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2)) ∈ ℂ)
4317recnd 11283 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) ∈ ℂ)
4439recnd 11283 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) ∈ ℂ)
4530recnd 11283 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ∈ ℂ)
4623rpne0d 13069 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ≠ 0)
4743, 44, 45, 46divsubdird 12074 . . . . . 6 ((𝜑𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) / (log‘𝑥)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥))))
488recnd 11283 . . . . . . . . . 10 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) / 𝑛) ∈ ℂ)
4915recnd 11283 . . . . . . . . . 10 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) ∈ ℂ)
5037recnd 11283 . . . . . . . . . 10 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ∈ ℂ)
5148, 49, 50subdid 11711 . . . . . . . . 9 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) = ((((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) − (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))))
5251sumeq2dv 15702 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) − (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))))
5316recnd 11283 . . . . . . . . 9 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) ∈ ℂ)
5438recnd 11283 . . . . . . . . 9 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) ∈ ℂ)
553, 53, 54fsumsub 15787 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) − (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))))
5652, 55eqtrd 2766 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))))
5756oveq1d 7431 . . . . . 6 ((𝜑𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) / (log‘𝑥)))
5824recnd 11283 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥)) ∈ ℂ)
5940recnd 11283 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) ∈ ℂ)
6031recnd 11283 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → ((log‘𝑥) / 2) ∈ ℂ)
6158, 59, 60nnncan2d 11647 . . . . . 6 ((𝜑𝑥 ∈ (1(,)+∞)) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥)) − ((log‘𝑥) / 2)) − ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥))))
6247, 57, 613eqtr4d 2776 . . . . 5 ((𝜑𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥)) = (((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥)) − ((log‘𝑥) / 2)) − ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2))))
6362mpteq2dva 5245 . . . 4 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥))) = (𝑥 ∈ (1(,)+∞) ↦ (((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥)) − ((log‘𝑥) / 2)) − ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2)))))
64 1red 11256 . . . . 5 (𝜑 → 1 ∈ ℝ)
653, 8fsumrecl 15733 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ∈ ℝ)
6665, 23rerpdivcld 13095 . . . . . 6 ((𝜑𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) ∈ ℝ)
67 2vmadivsum.1 . . . . . . . 8 (𝜑𝐴 ∈ ℝ+)
6867rpred 13064 . . . . . . 7 (𝜑𝐴 ∈ ℝ)
6968adantr 479 . . . . . 6 ((𝜑𝑥 ∈ (1(,)+∞)) → 𝐴 ∈ ℝ)
70 ioossre 13433 . . . . . . . 8 (1(,)+∞) ⊆ ℝ
71 1cnd 11250 . . . . . . . 8 (𝜑 → 1 ∈ ℂ)
72 o1const 15617 . . . . . . . 8 (((1(,)+∞) ⊆ ℝ ∧ 1 ∈ ℂ) → (𝑥 ∈ (1(,)+∞) ↦ 1) ∈ 𝑂(1))
7370, 71, 72sylancr 585 . . . . . . 7 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ 1) ∈ 𝑂(1))
7466recnd 11283 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) ∈ ℂ)
75 1cnd 11250 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → 1 ∈ ℂ)
7665recnd 11283 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ∈ ℂ)
7776, 45, 45, 46divsubdird 12074 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) / (log‘𝑥)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) − ((log‘𝑥) / (log‘𝑥))))
7876, 45subcld 11612 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) ∈ ℂ)
7978, 45, 46divrecd 12038 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) / (log‘𝑥)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) · (1 / (log‘𝑥))))
8045, 46dividd 12033 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1(,)+∞)) → ((log‘𝑥) / (log‘𝑥)) = 1)
8180oveq2d 7432 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) − ((log‘𝑥) / (log‘𝑥))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) − 1))
8277, 79, 813eqtr3d 2774 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) · (1 / (log‘𝑥))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) − 1))
8382mpteq2dva 5245 . . . . . . . . 9 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) · (1 / (log‘𝑥)))) = (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) − 1)))
8465, 30resubcld 11683 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) ∈ ℝ)
8527, 23rerpdivcld 13095 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1(,)+∞)) → (1 / (log‘𝑥)) ∈ ℝ)
8629ex 411 . . . . . . . . . . . 12 (𝜑 → (𝑥 ∈ (1(,)+∞) → 𝑥 ∈ ℝ+))
8786ssrdv 3984 . . . . . . . . . . 11 (𝜑 → (1(,)+∞) ⊆ ℝ+)
88 vmadivsum 27508 . . . . . . . . . . . 12 (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1)
8988a1i 11 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1))
9087, 89o1res2 15560 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1))
91 divlogrlim 26659 . . . . . . . . . . 11 (𝑥 ∈ (1(,)+∞) ↦ (1 / (log‘𝑥))) ⇝𝑟 0
92 rlimo1 15614 . . . . . . . . . . 11 ((𝑥 ∈ (1(,)+∞) ↦ (1 / (log‘𝑥))) ⇝𝑟 0 → (𝑥 ∈ (1(,)+∞) ↦ (1 / (log‘𝑥))) ∈ 𝑂(1))
9391, 92mp1i 13 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (1 / (log‘𝑥))) ∈ 𝑂(1))
9484, 85, 90, 93o1mul2 15622 . . . . . . . . 9 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) · (1 / (log‘𝑥)))) ∈ 𝑂(1))
9583, 94eqeltrrd 2827 . . . . . . . 8 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) − 1)) ∈ 𝑂(1))
9674, 75, 95o1dif 15627 . . . . . . 7 (𝜑 → ((𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥))) ∈ 𝑂(1) ↔ (𝑥 ∈ (1(,)+∞) ↦ 1) ∈ 𝑂(1)))
9773, 96mpbird 256 . . . . . 6 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥))) ∈ 𝑂(1))
9868recnd 11283 . . . . . . 7 (𝜑𝐴 ∈ ℂ)
99 o1const 15617 . . . . . . 7 (((1(,)+∞) ⊆ ℝ ∧ 𝐴 ∈ ℂ) → (𝑥 ∈ (1(,)+∞) ↦ 𝐴) ∈ 𝑂(1))
10070, 98, 99sylancr 585 . . . . . 6 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ 𝐴) ∈ 𝑂(1))
10166, 69, 97, 100o1mul2 15622 . . . . 5 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) · 𝐴)) ∈ 𝑂(1))
10266, 69remulcld 11285 . . . . 5 ((𝜑𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) · 𝐴) ∈ ℝ)
10315, 37resubcld 11683 . . . . . . . . 9 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))) ∈ ℝ)
1048, 103remulcld 11285 . . . . . . . 8 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) ∈ ℝ)
1053, 104fsumrecl 15733 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) ∈ ℝ)
106105recnd 11283 . . . . . 6 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) ∈ ℂ)
107106, 45, 46divcld 12035 . . . . 5 ((𝜑𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥)) ∈ ℂ)
108106abscld 15436 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) ∈ ℝ)
10965, 69remulcld 11285 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝐴) ∈ ℝ)
110104recnd 11283 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) ∈ ℂ)
111110abscld 15436 . . . . . . . . . 10 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) ∈ ℝ)
1123, 111fsumrecl 15733 . . . . . . . . 9 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) ∈ ℝ)
1133, 110fsumabs 15800 . . . . . . . . 9 ((𝜑𝑥 ∈ (1(,)+∞)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))))
11469adantr 479 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝐴 ∈ ℝ)
1158, 114remulcld 11285 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) / 𝑛) · 𝐴) ∈ ℝ)
116103recnd 11283 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))) ∈ ℂ)
11748, 116absmuld 15454 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) = ((abs‘((Λ‘𝑛) / 𝑛)) · (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))))
118 vmage0 27146 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ → 0 ≤ (Λ‘𝑛))
1195, 118syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (Λ‘𝑛))
1207, 35, 119divge0d 13104 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ ((Λ‘𝑛) / 𝑛))
1218, 120absidd 15422 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((Λ‘𝑛) / 𝑛)) = ((Λ‘𝑛) / 𝑛))
122121oveq1d 7431 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘((Λ‘𝑛) / 𝑛)) · (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) = (((Λ‘𝑛) / 𝑛) · (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))))
123117, 122eqtrd 2766 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) = (((Λ‘𝑛) / 𝑛) · (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))))
124116abscld 15436 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) ∈ ℝ)
125 fveq2 6893 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑚 → (Λ‘𝑖) = (Λ‘𝑚))
126 id 22 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑚𝑖 = 𝑚)
127125, 126oveq12d 7434 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑚 → ((Λ‘𝑖) / 𝑖) = ((Λ‘𝑚) / 𝑚))
128127cbvsumv 15695 . . . . . . . . . . . . . . . . . 18 Σ𝑖 ∈ (1...(⌊‘𝑦))((Λ‘𝑖) / 𝑖) = Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) / 𝑚)
129 fveq2 6893 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝑥 / 𝑛) → (⌊‘𝑦) = (⌊‘(𝑥 / 𝑛)))
130129oveq2d 7432 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝑥 / 𝑛) → (1...(⌊‘𝑦)) = (1...(⌊‘(𝑥 / 𝑛))))
131130sumeq1d 15700 . . . . . . . . . . . . . . . . . 18 (𝑦 = (𝑥 / 𝑛) → Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) / 𝑚) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚))
132128, 131eqtrid 2778 . . . . . . . . . . . . . . . . 17 (𝑦 = (𝑥 / 𝑛) → Σ𝑖 ∈ (1...(⌊‘𝑦))((Λ‘𝑖) / 𝑖) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚))
133 fveq2 6893 . . . . . . . . . . . . . . . . 17 (𝑦 = (𝑥 / 𝑛) → (log‘𝑦) = (log‘(𝑥 / 𝑛)))
134132, 133oveq12d 7434 . . . . . . . . . . . . . . . 16 (𝑦 = (𝑥 / 𝑛) → (Σ𝑖 ∈ (1...(⌊‘𝑦))((Λ‘𝑖) / 𝑖) − (log‘𝑦)) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))
135134fveq2d 6897 . . . . . . . . . . . . . . 15 (𝑦 = (𝑥 / 𝑛) → (abs‘(Σ𝑖 ∈ (1...(⌊‘𝑦))((Λ‘𝑖) / 𝑖) − (log‘𝑦))) = (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))))
136135breq1d 5155 . . . . . . . . . . . . . 14 (𝑦 = (𝑥 / 𝑛) → ((abs‘(Σ𝑖 ∈ (1...(⌊‘𝑦))((Λ‘𝑖) / 𝑖) − (log‘𝑦))) ≤ 𝐴 ↔ (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) ≤ 𝐴))
137 2vmadivsum.2 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘(Σ𝑖 ∈ (1...(⌊‘𝑦))((Λ‘𝑖) / 𝑖) − (log‘𝑦))) ≤ 𝐴)
138137ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ∀𝑦 ∈ (1[,)+∞)(abs‘(Σ𝑖 ∈ (1...(⌊‘𝑦))((Λ‘𝑖) / 𝑖) − (log‘𝑦))) ≤ 𝐴)
13936rpred 13064 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ)
1405nncnd 12274 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℂ)
141140mullidd 11273 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 · 𝑛) = 𝑛)
142 fznnfl 13876 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℝ → (𝑛 ∈ (1...(⌊‘𝑥)) ↔ (𝑛 ∈ ℕ ∧ 𝑛𝑥)))
14319, 142syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (1(,)+∞)) → (𝑛 ∈ (1...(⌊‘𝑥)) ↔ (𝑛 ∈ ℕ ∧ 𝑛𝑥)))
144143simplbda 498 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛𝑥)
145141, 144eqbrtrd 5167 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 · 𝑛) ≤ 𝑥)
146 1red 11256 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℝ)
14719adantr 479 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ)
148146, 147, 35lemuldivd 13113 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 · 𝑛) ≤ 𝑥 ↔ 1 ≤ (𝑥 / 𝑛)))
149145, 148mpbid 231 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ≤ (𝑥 / 𝑛))
150 1re 11255 . . . . . . . . . . . . . . . 16 1 ∈ ℝ
151 elicopnf 13470 . . . . . . . . . . . . . . . 16 (1 ∈ ℝ → ((𝑥 / 𝑛) ∈ (1[,)+∞) ↔ ((𝑥 / 𝑛) ∈ ℝ ∧ 1 ≤ (𝑥 / 𝑛))))
152150, 151ax-mp 5 . . . . . . . . . . . . . . 15 ((𝑥 / 𝑛) ∈ (1[,)+∞) ↔ ((𝑥 / 𝑛) ∈ ℝ ∧ 1 ≤ (𝑥 / 𝑛)))
153139, 149, 152sylanbrc 581 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ (1[,)+∞))
154136, 138, 153rspcdva 3608 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) ≤ 𝐴)
155124, 114, 8, 120, 154lemul2ad 12200 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) / 𝑛) · (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) ≤ (((Λ‘𝑛) / 𝑛) · 𝐴))
156123, 155eqbrtrd 5167 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) ≤ (((Λ‘𝑛) / 𝑛) · 𝐴))
1573, 111, 115, 156fsumle 15798 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · 𝐴))
15898adantr 479 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1(,)+∞)) → 𝐴 ∈ ℂ)
1593, 158, 48fsummulc1 15784 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝐴) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · 𝐴))
160157, 159breqtrrd 5173 . . . . . . . . 9 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝐴))
161108, 112, 109, 113, 160letrd 11412 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝐴))
162108, 109, 23, 161lediv1dd 13122 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) / (log‘𝑥)) ≤ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝐴) / (log‘𝑥)))
163106, 45, 46absdivd 15455 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥))) = ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) / (abs‘(log‘𝑥))))
16423rpge0d 13068 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1(,)+∞)) → 0 ≤ (log‘𝑥))
16530, 164absidd 15422 . . . . . . . . 9 ((𝜑𝑥 ∈ (1(,)+∞)) → (abs‘(log‘𝑥)) = (log‘𝑥))
166165oveq2d 7432 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) / (abs‘(log‘𝑥))) = ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) / (log‘𝑥)))
167163, 166eqtrd 2766 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥))) = ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) / (log‘𝑥)))
1683, 8, 120fsumge0 15794 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1(,)+∞)) → 0 ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛))
16965, 23, 168divge0d 13104 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1(,)+∞)) → 0 ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)))
17067adantr 479 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1(,)+∞)) → 𝐴 ∈ ℝ+)
171170rpge0d 13068 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1(,)+∞)) → 0 ≤ 𝐴)
17266, 69, 169, 171mulge0d 11832 . . . . . . . . 9 ((𝜑𝑥 ∈ (1(,)+∞)) → 0 ≤ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) · 𝐴))
173102, 172absidd 15422 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) · 𝐴)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) · 𝐴))
17476, 158, 45, 46div23d 12072 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝐴) / (log‘𝑥)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) · 𝐴))
175173, 174eqtr4d 2769 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) · 𝐴)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝐴) / (log‘𝑥)))
176162, 167, 1753brtr4d 5177 . . . . . 6 ((𝜑𝑥 ∈ (1(,)+∞)) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥))) ≤ (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) · 𝐴)))
177176adantrr 715 . . . . 5 ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ 1 ≤ 𝑥)) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥))) ≤ (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) · 𝐴)))
17864, 101, 102, 107, 177o1le 15652 . . . 4 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥))) ∈ 𝑂(1))
17963, 178eqeltrrd 2827 . . 3 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥)) − ((log‘𝑥) / 2)) − ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2)))) ∈ 𝑂(1))
18033, 42, 179o1dif 15627 . 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 394   = wceq 1534  wcel 2099  wral 3051  wss 3946   class class class wbr 5145  cmpt 5228  cfv 6546  (class class class)co 7416  cc 11147  cr 11148  0cc0 11149  1c1 11150   · cmul 11154  +∞cpnf 11286   < clt 11289  cle 11290  cmin 11485   / cdiv 11912  cn 12258  2c2 12313  +crp 13022  (,)cioo 13372  [,)cico 13374  ...cfz 13532  cfl 13804  abscabs 15234  𝑟 crli 15482  𝑂(1)co1 15483  Σcsu 15685  logclog 26578  Λcvma 27117
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-rep 5282  ax-sep 5296  ax-nul 5303  ax-pow 5361  ax-pr 5425  ax-un 7738  ax-inf2 9677  ax-cnex 11205  ax-resscn 11206  ax-1cn 11207  ax-icn 11208  ax-addcl 11209  ax-addrcl 11210  ax-mulcl 11211  ax-mulrcl 11212  ax-mulcom 11213  ax-addass 11214  ax-mulass 11215  ax-distr 11216  ax-i2m1 11217  ax-1ne0 11218  ax-1rid 11219  ax-rnegex 11220  ax-rrecex 11221  ax-cnre 11222  ax-pre-lttri 11223  ax-pre-lttrn 11224  ax-pre-ltadd 11225  ax-pre-mulgt0 11226  ax-pre-sup 11227  ax-addf 11228
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3966  df-nul 4323  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-tp 4628  df-op 4630  df-uni 4906  df-int 4947  df-iun 4995  df-iin 4996  df-br 5146  df-opab 5208  df-mpt 5229  df-tr 5263  df-id 5572  df-eprel 5578  df-po 5586  df-so 5587  df-fr 5629  df-se 5630  df-we 5631  df-xp 5680  df-rel 5681  df-cnv 5682  df-co 5683  df-dm 5684  df-rn 5685  df-res 5686  df-ima 5687  df-pred 6304  df-ord 6371  df-on 6372  df-lim 6373  df-suc 6374  df-iota 6498  df-fun 6548  df-fn 6549  df-f 6550  df-f1 6551  df-fo 6552  df-f1o 6553  df-fv 6554  df-isom 6555  df-riota 7372  df-ov 7419  df-oprab 7420  df-mpo 7421  df-of 7682  df-om 7869  df-1st 7995  df-2nd 7996  df-supp 8167  df-frecs 8288  df-wrecs 8319  df-recs 8393  df-rdg 8432  df-1o 8488  df-2o 8489  df-oadd 8492  df-er 8726  df-map 8849  df-pm 8850  df-ixp 8919  df-en 8967  df-dom 8968  df-sdom 8969  df-fin 8970  df-fsupp 9399  df-fi 9447  df-sup 9478  df-inf 9479  df-oi 9546  df-dju 9937  df-card 9975  df-pnf 11291  df-mnf 11292  df-xr 11293  df-ltxr 11294  df-le 11295  df-sub 11487  df-neg 11488  df-div 11913  df-nn 12259  df-2 12321  df-3 12322  df-4 12323  df-5 12324  df-6 12325  df-7 12326  df-8 12327  df-9 12328  df-n0 12519  df-xnn0 12591  df-z 12605  df-dec 12724  df-uz 12869  df-q 12979  df-rp 13023  df-xneg 13140  df-xadd 13141  df-xmul 13142  df-ioo 13376  df-ioc 13377  df-ico 13378  df-icc 13379  df-fz 13533  df-fzo 13676  df-fl 13806  df-mod 13884  df-seq 14016  df-exp 14076  df-fac 14286  df-bc 14315  df-hash 14343  df-shft 15067  df-cj 15099  df-re 15100  df-im 15101  df-sqrt 15235  df-abs 15236  df-limsup 15468  df-clim 15485  df-rlim 15486  df-o1 15487  df-lo1 15488  df-sum 15686  df-ef 16064  df-e 16065  df-sin 16066  df-cos 16067  df-tan 16068  df-pi 16069  df-dvds 16252  df-gcd 16490  df-prm 16668  df-pc 16834  df-struct 17144  df-sets 17161  df-slot 17179  df-ndx 17191  df-base 17209  df-ress 17238  df-plusg 17274  df-mulr 17275  df-starv 17276  df-sca 17277  df-vsca 17278  df-ip 17279  df-tset 17280  df-ple 17281  df-ds 17283  df-unif 17284  df-hom 17285  df-cco 17286  df-rest 17432  df-topn 17433  df-0g 17451  df-gsum 17452  df-topgen 17453  df-pt 17454  df-prds 17457  df-xrs 17512  df-qtop 17517  df-imas 17518  df-xps 17520  df-mre 17594  df-mrc 17595  df-acs 17597  df-mgm 18628  df-sgrp 18707  df-mnd 18723  df-submnd 18769  df-mulg 19058  df-cntz 19307  df-cmn 19776  df-psmet 21331  df-xmet 21332  df-met 21333  df-bl 21334  df-mopn 21335  df-fbas 21336  df-fg 21337  df-cnfld 21340  df-top 22884  df-topon 22901  df-topsp 22923  df-bases 22937  df-cld 23011  df-ntr 23012  df-cls 23013  df-nei 23090  df-lp 23128  df-perf 23129  df-cn 23219  df-cnp 23220  df-haus 23307  df-cmp 23379  df-tx 23554  df-hmeo 23747  df-fil 23838  df-fm 23930  df-flim 23931  df-flf 23932  df-xms 24314  df-ms 24315  df-tms 24316  df-cncf 24886  df-limc 25883  df-dv 25884  df-ulm 26403  df-log 26580  df-cxp 26581  df-atan 26892  df-em 27018  df-cht 27122  df-vma 27123  df-chp 27124  df-ppi 27125
This theorem is referenced by:  2vmadivsum  27567
  Copyright terms: Public domain W3C validator