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

Theorem selberg4lem1 25446
Description: Lemma for selberg4 25447. Equation 10.4.20 of [Shapiro], p. 422. (Contributed by Mario Carneiro, 30-May-2016.)
Hypotheses
Ref Expression
selberg4lem1.1 (𝜑𝐴 ∈ ℝ+)
selberg4lem1.2 (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((Σ𝑖 ∈ (1...(⌊‘𝑦))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑦 / 𝑖)))) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝐴)
Assertion
Ref Expression
selberg4lem1 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / (𝑥 · (log‘𝑥))) − (log‘𝑥))) ∈ 𝑂(1))
Distinct variable groups:   𝑖,𝑚,𝑛,𝑥,𝑦,𝐴   𝜑,𝑚,𝑛,𝑥
Allowed substitution hints:   𝜑(𝑦,𝑖)

Proof of Theorem selberg4lem1
StepHypRef Expression
1 2cnd 11283 . . . . . 6 ((𝜑𝑥 ∈ (1(,)+∞)) → 2 ∈ ℂ)
2 fzfid 12964 . . . . . . . . 9 ((𝜑𝑥 ∈ (1(,)+∞)) → (1...(⌊‘𝑥)) ∈ Fin)
3 elfznn 12561 . . . . . . . . . . . . 13 (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
43adantl 473 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
5 vmacl 25041 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → (Λ‘𝑛) ∈ ℝ)
64, 5syl 17 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈ ℝ)
76, 4nndivred 11259 . . . . . . . . . 10 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) / 𝑛) ∈ ℝ)
8 elioore 12396 . . . . . . . . . . . . . . 15 (𝑥 ∈ (1(,)+∞) → 𝑥 ∈ ℝ)
98adantl 473 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (1(,)+∞)) → 𝑥 ∈ ℝ)
10 1rp 12027 . . . . . . . . . . . . . . 15 1 ∈ ℝ+
1110a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (1(,)+∞)) → 1 ∈ ℝ+)
12 1red 10245 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (1(,)+∞)) → 1 ∈ ℝ)
13 eliooord 12424 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (1(,)+∞) → (1 < 𝑥𝑥 < +∞))
1413adantl 473 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (1(,)+∞)) → (1 < 𝑥𝑥 < +∞))
1514simpld 477 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (1(,)+∞)) → 1 < 𝑥)
1612, 9, 15ltled 10375 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (1(,)+∞)) → 1 ≤ 𝑥)
179, 11, 16rpgecld 12102 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1(,)+∞)) → 𝑥 ∈ ℝ+)
1817adantr 472 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ+)
194nnrpd 12061 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ+)
2018, 19rpdivcld 12080 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ+)
2120relogcld 24566 . . . . . . . . . 10 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ∈ ℝ)
227, 21remulcld 10260 . . . . . . . . 9 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) ∈ ℝ)
232, 22fsumrecl 14662 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) ∈ ℝ)
249, 15rplogcld 24572 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ∈ ℝ+)
2523, 24rerpdivcld 12094 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) ∈ ℝ)
2625recnd 10258 . . . . . 6 ((𝜑𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) ∈ ℂ)
2717relogcld 24566 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ∈ ℝ)
2827rehalfcld 11469 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → ((log‘𝑥) / 2) ∈ ℝ)
2928recnd 10258 . . . . . 6 ((𝜑𝑥 ∈ (1(,)+∞)) → ((log‘𝑥) / 2) ∈ ℂ)
301, 26, 29subdid 10676 . . . . 5 ((𝜑𝑥 ∈ (1(,)+∞)) → (2 · ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2))) = ((2 · (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥))) − (2 · ((log‘𝑥) / 2))))
3127recnd 10258 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ∈ ℂ)
32 2ne0 11303 . . . . . . . 8 2 ≠ 0
3332a1i 11 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → 2 ≠ 0)
3431, 1, 33divcan2d 10993 . . . . . 6 ((𝜑𝑥 ∈ (1(,)+∞)) → (2 · ((log‘𝑥) / 2)) = (log‘𝑥))
3534oveq2d 6827 . . . . 5 ((𝜑𝑥 ∈ (1(,)+∞)) → ((2 · (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥))) − (2 · ((log‘𝑥) / 2))) = ((2 · (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥))) − (log‘𝑥)))
3630, 35eqtrd 2792 . . . 4 ((𝜑𝑥 ∈ (1(,)+∞)) → (2 · ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2))) = ((2 · (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥))) − (log‘𝑥)))
3736mpteq2dva 4894 . . 3 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (2 · ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2)))) = (𝑥 ∈ (1(,)+∞) ↦ ((2 · (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥))) − (log‘𝑥))))
38 2re 11280 . . . . 5 2 ∈ ℝ
3938a1i 11 . . . 4 ((𝜑𝑥 ∈ (1(,)+∞)) → 2 ∈ ℝ)
4025, 28resubcld 10648 . . . 4 ((𝜑𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2)) ∈ ℝ)
41 ioossre 12426 . . . . . 6 (1(,)+∞) ⊆ ℝ
42 2cn 11281 . . . . . 6 2 ∈ ℂ
43 o1const 14547 . . . . . 6 (((1(,)+∞) ⊆ ℝ ∧ 2 ∈ ℂ) → (𝑥 ∈ (1(,)+∞) ↦ 2) ∈ 𝑂(1))
4441, 42, 43mp2an 710 . . . . 5 (𝑥 ∈ (1(,)+∞) ↦ 2) ∈ 𝑂(1)
4544a1i 11 . . . 4 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ 2) ∈ 𝑂(1))
46 vmalogdivsum2 25424 . . . . 5 (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2))) ∈ 𝑂(1)
4746a1i 11 . . . 4 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2))) ∈ 𝑂(1))
4839, 40, 45, 47o1mul2 14552 . . 3 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (2 · ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2)))) ∈ 𝑂(1))
4937, 48eqeltrrd 2838 . 2 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((2 · (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥))) − (log‘𝑥))) ∈ 𝑂(1))
50 fzfid 12964 . . . . . . . . 9 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1...(⌊‘(𝑥 / 𝑛))) ∈ Fin)
51 elfznn 12561 . . . . . . . . . . . 12 (𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛))) → 𝑚 ∈ ℕ)
5251adantl 473 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ∈ ℕ)
53 vmacl 25041 . . . . . . . . . . 11 (𝑚 ∈ ℕ → (Λ‘𝑚) ∈ ℝ)
5452, 53syl 17 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (Λ‘𝑚) ∈ ℝ)
5552nnrpd 12061 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ∈ ℝ+)
5655relogcld 24566 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (log‘𝑚) ∈ ℝ)
579adantr 472 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ)
5857, 4nndivred 11259 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ)
5958adantr 472 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (𝑥 / 𝑛) ∈ ℝ)
6059, 52nndivred 11259 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((𝑥 / 𝑛) / 𝑚) ∈ ℝ)
61 chpcl 25047 . . . . . . . . . . . 12 (((𝑥 / 𝑛) / 𝑚) ∈ ℝ → (ψ‘((𝑥 / 𝑛) / 𝑚)) ∈ ℝ)
6260, 61syl 17 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (ψ‘((𝑥 / 𝑛) / 𝑚)) ∈ ℝ)
6356, 62readdcld 10259 . . . . . . . . . 10 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))) ∈ ℝ)
6454, 63remulcld 10260 . . . . . . . . 9 ((((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) ∈ ℝ)
6550, 64fsumrecl 14662 . . . . . . . 8 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) ∈ ℝ)
666, 65remulcld 10260 . . . . . . 7 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) ∈ ℝ)
672, 66fsumrecl 14662 . . . . . 6 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) ∈ ℝ)
6817, 24rpmulcld 12079 . . . . . 6 ((𝜑𝑥 ∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ∈ ℝ+)
6967, 68rerpdivcld 12094 . . . . 5 ((𝜑𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / (𝑥 · (log‘𝑥))) ∈ ℝ)
7069, 27resubcld 10648 . . . 4 ((𝜑𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / (𝑥 · (log‘𝑥))) − (log‘𝑥)) ∈ ℝ)
7170recnd 10258 . . 3 ((𝜑𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / (𝑥 · (log‘𝑥))) − (log‘𝑥)) ∈ ℂ)
7223recnd 10258 . . . . . 6 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) ∈ ℂ)
7324rpne0d 12068 . . . . . 6 ((𝜑𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ≠ 0)
7472, 31, 73divcld 10991 . . . . 5 ((𝜑𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) ∈ ℂ)
751, 74mulcld 10250 . . . 4 ((𝜑𝑥 ∈ (1(,)+∞)) → (2 · (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥))) ∈ ℂ)
7675, 31subcld 10582 . . 3 ((𝜑𝑥 ∈ (1(,)+∞)) → ((2 · (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥))) − (log‘𝑥)) ∈ ℂ)
7769recnd 10258 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / (𝑥 · (log‘𝑥))) ∈ ℂ)
7877, 75, 31nnncan2d 10617 . . . . . 6 ((𝜑𝑥 ∈ (1(,)+∞)) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / (𝑥 · (log‘𝑥))) − (log‘𝑥)) − ((2 · (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥))) − (log‘𝑥))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / (𝑥 · (log‘𝑥))) − (2 · (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)))))
7967recnd 10258 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) ∈ ℂ)
809recnd 10258 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → 𝑥 ∈ ℂ)
8117rpne0d 12068 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → 𝑥 ≠ 0)
8279, 80, 31, 81, 73divdiv1d 11022 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / 𝑥) / (log‘𝑥)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / (𝑥 · (log‘𝑥))))
831, 72, 31, 73divassd 11026 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) / (log‘𝑥)) = (2 · (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥))))
8482, 83oveq12d 6829 . . . . . 6 ((𝜑𝑥 ∈ (1(,)+∞)) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / 𝑥) / (log‘𝑥)) − ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) / (log‘𝑥))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / (𝑥 · (log‘𝑥))) − (2 · (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)))))
8567, 17rerpdivcld 12094 . . . . . . . . 9 ((𝜑𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / 𝑥) ∈ ℝ)
8685recnd 10258 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / 𝑥) ∈ ℂ)
871, 72mulcld 10250 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → (2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) ∈ ℂ)
8886, 87, 31, 73divsubdird 11030 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / 𝑥) − (2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))) / (log‘𝑥)) = (((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / 𝑥) / (log‘𝑥)) − ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) / (log‘𝑥))))
8981adantr 472 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ≠ 0)
9066, 57, 89redivcld 11043 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / 𝑥) ∈ ℝ)
9190recnd 10258 . . . . . . . . . 10 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / 𝑥) ∈ ℂ)
9238a1i 11 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 2 ∈ ℝ)
9392, 22remulcld 10260 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) ∈ ℝ)
9493recnd 10258 . . . . . . . . . 10 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) ∈ ℂ)
952, 91, 94fsumsub 14717 . . . . . . . . 9 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / 𝑥) − (2 · (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / 𝑥) − Σ𝑛 ∈ (1...(⌊‘𝑥))(2 · (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))))
966recnd 10258 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈ ℂ)
9765, 57, 89redivcld 11043 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) ∈ ℝ)
9897recnd 10258 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) ∈ ℂ)
99 2cnd 11283 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 2 ∈ ℂ)
10021recnd 10258 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ∈ ℂ)
1014nncnd 11226 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℂ)
1024nnne0d 11255 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ≠ 0)
103100, 101, 102divcld 10991 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛)) / 𝑛) ∈ ℂ)
10499, 103mulcld 10250 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)) ∈ ℂ)
10596, 98, 104subdid 10676 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) = (((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥)) − ((Λ‘𝑛) · (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))))
10665recnd 10258 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) ∈ ℂ)
10780adantr 472 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℂ)
10896, 106, 107, 89divassd 11026 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / 𝑥) = ((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥)))
10996, 101, 100, 102div32d 11014 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) = ((Λ‘𝑛) · ((log‘(𝑥 / 𝑛)) / 𝑛)))
110109oveq2d 6827 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) = (2 · ((Λ‘𝑛) · ((log‘(𝑥 / 𝑛)) / 𝑛))))
11199, 96, 103mul12d 10435 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · ((Λ‘𝑛) · ((log‘(𝑥 / 𝑛)) / 𝑛))) = ((Λ‘𝑛) · (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))))
112110, 111eqtrd 2792 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) = ((Λ‘𝑛) · (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))))
113108, 112oveq12d 6829 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / 𝑥) − (2 · (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))) = (((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥)) − ((Λ‘𝑛) · (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))))
114105, 113eqtr4d 2795 . . . . . . . . . 10 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) = ((((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / 𝑥) − (2 · (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))))
115114sumeq2dv 14630 . . . . . . . . 9 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / 𝑥) − (2 · (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))))
11666recnd 10258 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) ∈ ℂ)
1172, 80, 116, 81fsumdivc 14715 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / 𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / 𝑥))
11822recnd 10258 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) ∈ ℂ)
1192, 1, 118fsummulc2 14713 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1(,)+∞)) → (2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(2 · (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))))
120117, 119oveq12d 6829 . . . . . . . . 9 ((𝜑𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / 𝑥) − (2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / 𝑥) − Σ𝑛 ∈ (1...(⌊‘𝑥))(2 · (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))))
12195, 115, 1203eqtr4rd 2803 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / 𝑥) − (2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))))
122121oveq1d 6826 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / 𝑥) − (2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))) / (log‘𝑥)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) / (log‘𝑥)))
12388, 122eqtr3d 2794 . . . . . 6 ((𝜑𝑥 ∈ (1(,)+∞)) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / 𝑥) / (log‘𝑥)) − ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) / (log‘𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) / (log‘𝑥)))
12478, 84, 1233eqtr2d 2798 . . . . 5 ((𝜑𝑥 ∈ (1(,)+∞)) → (((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / (𝑥 · (log‘𝑥))) − (log‘𝑥)) − ((2 · (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥))) − (log‘𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) / (log‘𝑥)))
125124mpteq2dva 4894 . . . 4 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / (𝑥 · (log‘𝑥))) − (log‘𝑥)) − ((2 · (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥))) − (log‘𝑥)))) = (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) / (log‘𝑥))))
126 1red 10245 . . . . 5 (𝜑 → 1 ∈ ℝ)
127 selberg4lem1.1 . . . . . . . 8 (𝜑𝐴 ∈ ℝ+)
128127adantr 472 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → 𝐴 ∈ ℝ+)
129128rpred 12063 . . . . . 6 ((𝜑𝑥 ∈ (1(,)+∞)) → 𝐴 ∈ ℝ)
1302, 7fsumrecl 14662 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ∈ ℝ)
131130, 24rerpdivcld 12094 . . . . . 6 ((𝜑𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) ∈ ℝ)
132127rpcnd 12065 . . . . . . 7 (𝜑𝐴 ∈ ℂ)
133 o1const 14547 . . . . . . 7 (((1(,)+∞) ⊆ ℝ ∧ 𝐴 ∈ ℂ) → (𝑥 ∈ (1(,)+∞) ↦ 𝐴) ∈ 𝑂(1))
13441, 132, 133sylancr 698 . . . . . 6 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ 𝐴) ∈ 𝑂(1))
135 1cnd 10246 . . . . . . . 8 (𝜑 → 1 ∈ ℂ)
136 o1const 14547 . . . . . . . 8 (((1(,)+∞) ⊆ ℝ ∧ 1 ∈ ℂ) → (𝑥 ∈ (1(,)+∞) ↦ 1) ∈ 𝑂(1))
13741, 135, 136sylancr 698 . . . . . . 7 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ 1) ∈ 𝑂(1))
138131recnd 10258 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) ∈ ℂ)
139 1cnd 10246 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → 1 ∈ ℂ)
140130recnd 10258 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ∈ ℂ)
141140, 31, 31, 73divsubdird 11030 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) / (log‘𝑥)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) − ((log‘𝑥) / (log‘𝑥))))
142140, 31subcld 10582 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) ∈ ℂ)
143142, 31, 73divrecd 10994 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) / (log‘𝑥)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) · (1 / (log‘𝑥))))
14431, 73dividd 10989 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1(,)+∞)) → ((log‘𝑥) / (log‘𝑥)) = 1)
145144oveq2d 6827 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) − ((log‘𝑥) / (log‘𝑥))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) − 1))
146141, 143, 1453eqtr3d 2800 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) · (1 / (log‘𝑥))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) − 1))
147146mpteq2dva 4894 . . . . . . . . 9 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) · (1 / (log‘𝑥)))) = (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) − 1)))
148130, 27resubcld 10648 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) ∈ ℝ)
14912, 24rerpdivcld 12094 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1(,)+∞)) → (1 / (log‘𝑥)) ∈ ℝ)
15017ex 449 . . . . . . . . . . . 12 (𝜑 → (𝑥 ∈ (1(,)+∞) → 𝑥 ∈ ℝ+))
151150ssrdv 3748 . . . . . . . . . . 11 (𝜑 → (1(,)+∞) ⊆ ℝ+)
152 vmadivsum 25368 . . . . . . . . . . . 12 (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1)
153152a1i 11 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1))
154151, 153o1res2 14491 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1))
155 divlogrlim 24578 . . . . . . . . . . 11 (𝑥 ∈ (1(,)+∞) ↦ (1 / (log‘𝑥))) ⇝𝑟 0
156 rlimo1 14544 . . . . . . . . . . 11 ((𝑥 ∈ (1(,)+∞) ↦ (1 / (log‘𝑥))) ⇝𝑟 0 → (𝑥 ∈ (1(,)+∞) ↦ (1 / (log‘𝑥))) ∈ 𝑂(1))
157155, 156mp1i 13 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (1 / (log‘𝑥))) ∈ 𝑂(1))
158148, 149, 154, 157o1mul2 14552 . . . . . . . . 9 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) · (1 / (log‘𝑥)))) ∈ 𝑂(1))
159147, 158eqeltrrd 2838 . . . . . . . 8 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) − 1)) ∈ 𝑂(1))
160138, 139, 159o1dif 14557 . . . . . . 7 (𝜑 → ((𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥))) ∈ 𝑂(1) ↔ (𝑥 ∈ (1(,)+∞) ↦ 1) ∈ 𝑂(1)))
161137, 160mpbird 247 . . . . . 6 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥))) ∈ 𝑂(1))
162129, 131, 134, 161o1mul2 14552 . . . . 5 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (𝐴 · (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)))) ∈ 𝑂(1))
163129, 131remulcld 10260 . . . . 5 ((𝜑𝑥 ∈ (1(,)+∞)) → (𝐴 · (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥))) ∈ ℝ)
16421, 4nndivred 11259 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛)) / 𝑛) ∈ ℝ)
16592, 164remulcld 10260 . . . . . . . . . 10 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)) ∈ ℝ)
16697, 165resubcld 10648 . . . . . . . . 9 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))) ∈ ℝ)
1676, 166remulcld 10260 . . . . . . . 8 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) ∈ ℝ)
1682, 167fsumrecl 14662 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) ∈ ℝ)
169168, 24rerpdivcld 12094 . . . . . 6 ((𝜑𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) / (log‘𝑥)) ∈ ℝ)
170169recnd 10258 . . . . 5 ((𝜑𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) / (log‘𝑥)) ∈ ℂ)
171168recnd 10258 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) ∈ ℂ)
172171abscld 14372 . . . . . . . . 9 ((𝜑𝑥 ∈ (1(,)+∞)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))))) ∈ ℝ)
173129, 130remulcld 10260 . . . . . . . . 9 ((𝜑𝑥 ∈ (1(,)+∞)) → (𝐴 · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛)) ∈ ℝ)
17498, 104subcld 10582 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))) ∈ ℂ)
17596, 174mulcld 10250 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) ∈ ℂ)
176175abscld 14372 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))))) ∈ ℝ)
1772, 176fsumrecl 14662 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))))) ∈ ℝ)
178167recnd 10258 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) ∈ ℂ)
1792, 178fsumabs 14730 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1(,)+∞)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))))))
180129adantr 472 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝐴 ∈ ℝ)
181180, 7remulcld 10260 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝐴 · ((Λ‘𝑛) / 𝑛)) ∈ ℝ)
182174abscld 14372 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) ∈ ℝ)
183180, 4nndivred 11259 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝐴 / 𝑛) ∈ ℝ)
184 vmage0 25044 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ → 0 ≤ (Λ‘𝑛))
1854, 184syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ (Λ‘𝑛))
186106, 107, 101, 89, 102divdiv2d 11023 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / (𝑥 / 𝑛)) = ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) · 𝑛) / 𝑥))
187106, 101, 107, 89div23d 11028 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) · 𝑛) / 𝑥) = ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) · 𝑛))
188186, 187eqtrd 2792 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / (𝑥 / 𝑛)) = ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) · 𝑛))
18999, 103, 101mulassd 10253 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((2 · ((log‘(𝑥 / 𝑛)) / 𝑛)) · 𝑛) = (2 · (((log‘(𝑥 / 𝑛)) / 𝑛) · 𝑛)))
190100, 101, 102divcan1d 10992 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((log‘(𝑥 / 𝑛)) / 𝑛) · 𝑛) = (log‘(𝑥 / 𝑛)))
191190oveq2d 6827 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (((log‘(𝑥 / 𝑛)) / 𝑛) · 𝑛)) = (2 · (log‘(𝑥 / 𝑛))))
192189, 191eqtr2d 2793 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 · (log‘(𝑥 / 𝑛))) = ((2 · ((log‘(𝑥 / 𝑛)) / 𝑛)) · 𝑛))
193188, 192oveq12d 6829 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / (𝑥 / 𝑛)) − (2 · (log‘(𝑥 / 𝑛)))) = (((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) · 𝑛) − ((2 · ((log‘(𝑥 / 𝑛)) / 𝑛)) · 𝑛)))
19498, 104, 101subdird 10677 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))) · 𝑛) = (((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) · 𝑛) − ((2 · ((log‘(𝑥 / 𝑛)) / 𝑛)) · 𝑛)))
195193, 194eqtr4d 2795 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / (𝑥 / 𝑛)) − (2 · (log‘(𝑥 / 𝑛)))) = (((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))) · 𝑛))
196195fveq2d 6354 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / (𝑥 / 𝑛)) − (2 · (log‘(𝑥 / 𝑛))))) = (abs‘(((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))) · 𝑛)))
197174, 101absmuld 14390 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))) · 𝑛)) = ((abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) · (abs‘𝑛)))
1984nnred 11225 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ)
19919rpge0d 12067 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ 𝑛)
200198, 199absidd 14358 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘𝑛) = 𝑛)
201200oveq2d 6827 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) · (abs‘𝑛)) = ((abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) · 𝑛))
202196, 197, 2013eqtrd 2796 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / (𝑥 / 𝑛)) − (2 · (log‘(𝑥 / 𝑛))))) = ((abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) · 𝑛))
203101mulid2d 10248 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 · 𝑛) = 𝑛)
204 fznnfl 12853 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℝ → (𝑛 ∈ (1...(⌊‘𝑥)) ↔ (𝑛 ∈ ℕ ∧ 𝑛𝑥)))
2059, 204syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ (1(,)+∞)) → (𝑛 ∈ (1...(⌊‘𝑥)) ↔ (𝑛 ∈ ℕ ∧ 𝑛𝑥)))
206205simplbda 655 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛𝑥)
207203, 206eqbrtrd 4824 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 · 𝑛) ≤ 𝑥)
208 1red 10245 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈ ℝ)
209208, 57, 19lemuldivd 12112 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 · 𝑛) ≤ 𝑥 ↔ 1 ≤ (𝑥 / 𝑛)))
210207, 209mpbid 222 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ≤ (𝑥 / 𝑛))
211 1re 10229 . . . . . . . . . . . . . . . . . . 19 1 ∈ ℝ
212 elicopnf 12460 . . . . . . . . . . . . . . . . . . 19 (1 ∈ ℝ → ((𝑥 / 𝑛) ∈ (1[,)+∞) ↔ ((𝑥 / 𝑛) ∈ ℝ ∧ 1 ≤ (𝑥 / 𝑛))))
213211, 212ax-mp 5 . . . . . . . . . . . . . . . . . 18 ((𝑥 / 𝑛) ∈ (1[,)+∞) ↔ ((𝑥 / 𝑛) ∈ ℝ ∧ 1 ≤ (𝑥 / 𝑛)))
21458, 210, 213sylanbrc 701 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ (1[,)+∞))
215 selberg4lem1.2 . . . . . . . . . . . . . . . . . 18 (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((Σ𝑖 ∈ (1...(⌊‘𝑦))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑦 / 𝑖)))) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝐴)
216215ad2antrr 764 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ∀𝑦 ∈ (1[,)+∞)(abs‘((Σ𝑖 ∈ (1...(⌊‘𝑦))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑦 / 𝑖)))) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝐴)
217 fveq2 6350 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 = 𝑚 → (Λ‘𝑖) = (Λ‘𝑚))
218 fveq2 6350 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 = 𝑚 → (log‘𝑖) = (log‘𝑚))
219 oveq2 6819 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 = 𝑚 → (𝑦 / 𝑖) = (𝑦 / 𝑚))
220219fveq2d 6354 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 = 𝑚 → (ψ‘(𝑦 / 𝑖)) = (ψ‘(𝑦 / 𝑚)))
221218, 220oveq12d 6829 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 = 𝑚 → ((log‘𝑖) + (ψ‘(𝑦 / 𝑖))) = ((log‘𝑚) + (ψ‘(𝑦 / 𝑚))))
222217, 221oveq12d 6829 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑖 = 𝑚 → ((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑦 / 𝑖)))) = ((Λ‘𝑚) · ((log‘𝑚) + (ψ‘(𝑦 / 𝑚)))))
223222cbvsumv 14623 . . . . . . . . . . . . . . . . . . . . . . 23 Σ𝑖 ∈ (1...(⌊‘𝑦))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑦 / 𝑖)))) = Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘(𝑦 / 𝑚))))
224 fveq2 6350 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = (𝑥 / 𝑛) → (⌊‘𝑦) = (⌊‘(𝑥 / 𝑛)))
225224oveq2d 6827 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = (𝑥 / 𝑛) → (1...(⌊‘𝑦)) = (1...(⌊‘(𝑥 / 𝑛))))
226 oveq1 6818 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 = (𝑥 / 𝑛) → (𝑦 / 𝑚) = ((𝑥 / 𝑛) / 𝑚))
227226fveq2d 6354 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 = (𝑥 / 𝑛) → (ψ‘(𝑦 / 𝑚)) = (ψ‘((𝑥 / 𝑛) / 𝑚)))
228227oveq2d 6827 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = (𝑥 / 𝑛) → ((log‘𝑚) + (ψ‘(𝑦 / 𝑚))) = ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))
229228oveq2d 6827 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = (𝑥 / 𝑛) → ((Λ‘𝑚) · ((log‘𝑚) + (ψ‘(𝑦 / 𝑚)))) = ((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))))
230229adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑦 = (𝑥 / 𝑛) ∧ 𝑚 ∈ (1...(⌊‘𝑦))) → ((Λ‘𝑚) · ((log‘𝑚) + (ψ‘(𝑦 / 𝑚)))) = ((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))))
231225, 230sumeq12dv 14634 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = (𝑥 / 𝑛) → Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘(𝑦 / 𝑚)))) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))))
232223, 231syl5eq 2804 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = (𝑥 / 𝑛) → Σ𝑖 ∈ (1...(⌊‘𝑦))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑦 / 𝑖)))) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))))
233 id 22 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = (𝑥 / 𝑛) → 𝑦 = (𝑥 / 𝑛))
234232, 233oveq12d 6829 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = (𝑥 / 𝑛) → (Σ𝑖 ∈ (1...(⌊‘𝑦))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑦 / 𝑖)))) / 𝑦) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / (𝑥 / 𝑛)))
235 fveq2 6350 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = (𝑥 / 𝑛) → (log‘𝑦) = (log‘(𝑥 / 𝑛)))
236235oveq2d 6827 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = (𝑥 / 𝑛) → (2 · (log‘𝑦)) = (2 · (log‘(𝑥 / 𝑛))))
237234, 236oveq12d 6829 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = (𝑥 / 𝑛) → ((Σ𝑖 ∈ (1...(⌊‘𝑦))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑦 / 𝑖)))) / 𝑦) − (2 · (log‘𝑦))) = ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / (𝑥 / 𝑛)) − (2 · (log‘(𝑥 / 𝑛)))))
238237fveq2d 6354 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝑥 / 𝑛) → (abs‘((Σ𝑖 ∈ (1...(⌊‘𝑦))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑦 / 𝑖)))) / 𝑦) − (2 · (log‘𝑦)))) = (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / (𝑥 / 𝑛)) − (2 · (log‘(𝑥 / 𝑛))))))
239238breq1d 4812 . . . . . . . . . . . . . . . . . 18 (𝑦 = (𝑥 / 𝑛) → ((abs‘((Σ𝑖 ∈ (1...(⌊‘𝑦))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑦 / 𝑖)))) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝐴 ↔ (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / (𝑥 / 𝑛)) − (2 · (log‘(𝑥 / 𝑛))))) ≤ 𝐴))
240239rspcv 3443 . . . . . . . . . . . . . . . . 17 ((𝑥 / 𝑛) ∈ (1[,)+∞) → (∀𝑦 ∈ (1[,)+∞)(abs‘((Σ𝑖 ∈ (1...(⌊‘𝑦))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑦 / 𝑖)))) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝐴 → (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / (𝑥 / 𝑛)) − (2 · (log‘(𝑥 / 𝑛))))) ≤ 𝐴))
241214, 216, 240sylc 65 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / (𝑥 / 𝑛)) − (2 · (log‘(𝑥 / 𝑛))))) ≤ 𝐴)
242202, 241eqbrtrrd 4826 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) · 𝑛) ≤ 𝐴)
243182, 180, 19lemuldivd 12112 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) · 𝑛) ≤ 𝐴 ↔ (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) ≤ (𝐴 / 𝑛)))
244242, 243mpbid 222 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) ≤ (𝐴 / 𝑛))
245182, 183, 6, 185, 244lemul2ad 11154 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))))) ≤ ((Λ‘𝑛) · (𝐴 / 𝑛)))
24696, 174absmuld 14390 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))))) = ((abs‘(Λ‘𝑛)) · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))))))
2476, 185absidd 14358 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(Λ‘𝑛)) = (Λ‘𝑛))
248247oveq1d 6826 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(Λ‘𝑛)) · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))))) = ((Λ‘𝑛) · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))))))
249246, 248eqtrd 2792 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))))) = ((Λ‘𝑛) · (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))))))
250132ad2antrr 764 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝐴 ∈ ℂ)
251250, 96, 101, 102div12d 11027 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝐴 · ((Λ‘𝑛) / 𝑛)) = ((Λ‘𝑛) · (𝐴 / 𝑛)))
252245, 249, 2513brtr4d 4834 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))))) ≤ (𝐴 · ((Λ‘𝑛) / 𝑛)))
2532, 176, 181, 252fsumle 14728 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(𝐴 · ((Λ‘𝑛) / 𝑛)))
254132adantr 472 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1(,)+∞)) → 𝐴 ∈ ℂ)
2557recnd 10258 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) / 𝑛) ∈ ℂ)
2562, 254, 255fsummulc2 14713 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1(,)+∞)) → (𝐴 · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛)) = Σ𝑛 ∈ (1...(⌊‘𝑥))(𝐴 · ((Λ‘𝑛) / 𝑛)))
257253, 256breqtrrd 4830 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))))) ≤ (𝐴 · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛)))
258172, 177, 173, 179, 257letrd 10384 . . . . . . . . 9 ((𝜑𝑥 ∈ (1(,)+∞)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))))) ≤ (𝐴 · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛)))
259172, 173, 24, 258lediv1dd 12121 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))))) / (log‘𝑥)) ≤ ((𝐴 · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛)) / (log‘𝑥)))
260254, 140, 31, 73divassd 11026 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → ((𝐴 · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛)) / (log‘𝑥)) = (𝐴 · (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥))))
261259, 260breqtrd 4828 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))))) / (log‘𝑥)) ≤ (𝐴 · (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥))))
262171, 31, 73absdivd 14391 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) / (log‘𝑥))) = ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))))) / (abs‘(log‘𝑥))))
26324rpge0d 12067 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1(,)+∞)) → 0 ≤ (log‘𝑥))
26427, 263absidd 14358 . . . . . . . . 9 ((𝜑𝑥 ∈ (1(,)+∞)) → (abs‘(log‘𝑥)) = (log‘𝑥))
265264oveq2d 6827 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))))) / (abs‘(log‘𝑥))) = ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))))) / (log‘𝑥)))
266262, 265eqtrd 2792 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) / (log‘𝑥))) = ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛))))) / (log‘𝑥)))
267128rpge0d 12067 . . . . . . . . 9 ((𝜑𝑥 ∈ (1(,)+∞)) → 0 ≤ 𝐴)
2686, 19, 185divge0d 12103 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ ((Λ‘𝑛) / 𝑛))
2692, 7, 268fsumge0 14724 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1(,)+∞)) → 0 ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛))
270130, 24, 269divge0d 12103 . . . . . . . . 9 ((𝜑𝑥 ∈ (1(,)+∞)) → 0 ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)))
271129, 131, 267, 270mulge0d 10794 . . . . . . . 8 ((𝜑𝑥 ∈ (1(,)+∞)) → 0 ≤ (𝐴 · (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥))))
272163, 271absidd 14358 . . . . . . 7 ((𝜑𝑥 ∈ (1(,)+∞)) → (abs‘(𝐴 · (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)))) = (𝐴 · (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥))))
273261, 266, 2723brtr4d 4834 . . . . . 6 ((𝜑𝑥 ∈ (1(,)+∞)) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) / (log‘𝑥))) ≤ (abs‘(𝐴 · (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)))))
274273adantrr 755 . . . . 5 ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ 1 ≤ 𝑥)) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) / (log‘𝑥))) ≤ (abs‘(𝐴 · (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)))))
275126, 162, 163, 170, 274o1le 14580 . . . 4 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) / 𝑥) − (2 · ((log‘(𝑥 / 𝑛)) / 𝑛)))) / (log‘𝑥))) ∈ 𝑂(1))
276125, 275eqeltrd 2837 . . 3 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / (𝑥 · (log‘𝑥))) − (log‘𝑥)) − ((2 · (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥))) − (log‘𝑥)))) ∈ 𝑂(1))
27771, 76, 276o1dif 14557 . 2 (𝜑 → ((𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / (𝑥 · (log‘𝑥))) − (log‘𝑥))) ∈ 𝑂(1) ↔ (𝑥 ∈ (1(,)+∞) ↦ ((2 · (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥))) − (log‘𝑥))) ∈ 𝑂(1)))
27849, 277mpbird 247 1 (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / (𝑥 · (log‘𝑥))) − (log‘𝑥))) ∈ 𝑂(1))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1630  wcel 2137  wne 2930  wral 3048  wss 3713   class class class wbr 4802  cmpt 4879  cfv 6047  (class class class)co 6811  cc 10124  cr 10125  0cc0 10126  1c1 10127   + caddc 10129   · cmul 10131  +∞cpnf 10261   < clt 10264  cle 10265  cmin 10456   / cdiv 10874  cn 11210  2c2 11260  +crp 12023  (,)cioo 12366  [,)cico 12368  ...cfz 12517  cfl 12783  abscabs 14171  𝑟 crli 14413  𝑂(1)co1 14414  Σcsu 14613  logclog 24498  Λcvma 25015  ψcchp 25016
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-8 2139  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738  ax-rep 4921  ax-sep 4931  ax-nul 4939  ax-pow 4990  ax-pr 5053  ax-un 7112  ax-inf2 8709  ax-cnex 10182  ax-resscn 10183  ax-1cn 10184  ax-icn 10185  ax-addcl 10186  ax-addrcl 10187  ax-mulcl 10188  ax-mulrcl 10189  ax-mulcom 10190  ax-addass 10191  ax-mulass 10192  ax-distr 10193  ax-i2m1 10194  ax-1ne0 10195  ax-1rid 10196  ax-rnegex 10197  ax-rrecex 10198  ax-cnre 10199  ax-pre-lttri 10200  ax-pre-lttrn 10201  ax-pre-ltadd 10202  ax-pre-mulgt0 10203  ax-pre-sup 10204  ax-addf 10205  ax-mulf 10206
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1633  df-fal 1636  df-ex 1852  df-nf 1857  df-sb 2045  df-eu 2609  df-mo 2610  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-ne 2931  df-nel 3034  df-ral 3053  df-rex 3054  df-reu 3055  df-rmo 3056  df-rab 3057  df-v 3340  df-sbc 3575  df-csb 3673  df-dif 3716  df-un 3718  df-in 3720  df-ss 3727  df-pss 3729  df-nul 4057  df-if 4229  df-pw 4302  df-sn 4320  df-pr 4322  df-tp 4324  df-op 4326  df-uni 4587  df-int 4626  df-iun 4672  df-iin 4673  df-br 4803  df-opab 4863  df-mpt 4880  df-tr 4903  df-id 5172  df-eprel 5177  df-po 5185  df-so 5186  df-fr 5223  df-se 5224  df-we 5225  df-xp 5270  df-rel 5271  df-cnv 5272  df-co 5273  df-dm 5274  df-rn 5275  df-res 5276  df-ima 5277  df-pred 5839  df-ord 5885  df-on 5886  df-lim 5887  df-suc 5888  df-iota 6010  df-fun 6049  df-fn 6050  df-f 6051  df-f1 6052  df-fo 6053  df-f1o 6054  df-fv 6055  df-isom 6056  df-riota 6772  df-ov 6814  df-oprab 6815  df-mpt2 6816  df-of 7060  df-om 7229  df-1st 7331  df-2nd 7332  df-supp 7462  df-wrecs 7574  df-recs 7635  df-rdg 7673  df-1o 7727  df-2o 7728  df-oadd 7731  df-er 7909  df-map 8023  df-pm 8024  df-ixp 8073  df-en 8120  df-dom 8121  df-sdom 8122  df-fin 8123  df-fsupp 8439  df-fi 8480  df-sup 8511  df-inf 8512  df-oi 8578  df-card 8953  df-cda 9180  df-pnf 10266  df-mnf 10267  df-xr 10268  df-ltxr 10269  df-le 10270  df-sub 10458  df-neg 10459  df-div 10875  df-nn 11211  df-2 11269  df-3 11270  df-4 11271  df-5 11272  df-6 11273  df-7 11274  df-8 11275  df-9 11276  df-n0 11483  df-xnn0 11554  df-z 11568  df-dec 11684  df-uz 11878  df-q 11980  df-rp 12024  df-xneg 12137  df-xadd 12138  df-xmul 12139  df-ioo 12370  df-ioc 12371  df-ico 12372  df-icc 12373  df-fz 12518  df-fzo 12658  df-fl 12785  df-mod 12861  df-seq 12994  df-exp 13053  df-fac 13253  df-bc 13282  df-hash 13310  df-shft 14004  df-cj 14036  df-re 14037  df-im 14038  df-sqrt 14172  df-abs 14173  df-limsup 14399  df-clim 14416  df-rlim 14417  df-o1 14418  df-lo1 14419  df-sum 14614  df-ef 14995  df-e 14996  df-sin 14997  df-cos 14998  df-pi 15000  df-dvds 15181  df-gcd 15417  df-prm 15586  df-pc 15742  df-struct 16059  df-ndx 16060  df-slot 16061  df-base 16063  df-sets 16064  df-ress 16065  df-plusg 16154  df-mulr 16155  df-starv 16156  df-sca 16157  df-vsca 16158  df-ip 16159  df-tset 16160  df-ple 16161  df-ds 16164  df-unif 16165  df-hom 16166  df-cco 16167  df-rest 16283  df-topn 16284  df-0g 16302  df-gsum 16303  df-topgen 16304  df-pt 16305  df-prds 16308  df-xrs 16362  df-qtop 16367  df-imas 16368  df-xps 16370  df-mre 16446  df-mrc 16447  df-acs 16449  df-mgm 17441  df-sgrp 17483  df-mnd 17494  df-submnd 17535  df-mulg 17740  df-cntz 17948  df-cmn 18393  df-psmet 19938  df-xmet 19939  df-met 19940  df-bl 19941  df-mopn 19942  df-fbas 19943  df-fg 19944  df-cnfld 19947  df-top 20899  df-topon 20916  df-topsp 20937  df-bases 20950  df-cld 21023  df-ntr 21024  df-cls 21025  df-nei 21102  df-lp 21140  df-perf 21141  df-cn 21231  df-cnp 21232  df-haus 21319  df-cmp 21390  df-tx 21565  df-hmeo 21758  df-fil 21849  df-fm 21941  df-flim 21942  df-flf 21943  df-xms 22324  df-ms 22325  df-tms 22326  df-cncf 22880  df-limc 23827  df-dv 23828  df-log 24500  df-cxp 24501  df-em 24916  df-cht 25020  df-vma 25021  df-chp 25022  df-ppi 25023
This theorem is referenced by:  selberg4  25447
  Copyright terms: Public domain W3C validator