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

Theorem selberg4r 26246
 Description: Selberg's symmetry formula, using the residual of the second Chebyshev function. Equation 10.6.11 of [Shapiro], p. 430. (Contributed by Mario Carneiro, 30-May-2016.)
Hypothesis
Ref Expression
pntrval.r 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))
Assertion
Ref Expression
selberg4r (𝑥 ∈ (1(,)+∞) ↦ ((((𝑅𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (𝑅‘((𝑥 / 𝑛) / 𝑚)))))) / 𝑥)) ∈ 𝑂(1)
Distinct variable groups:   𝑚,𝑎,𝑛,𝑥   𝑅,𝑚,𝑛,𝑥
Allowed substitution hint:   𝑅(𝑎)

Proof of Theorem selberg4r
StepHypRef Expression
1 elioore 12802 . . . . . . . . . . . . 13 (𝑥 ∈ (1(,)+∞) → 𝑥 ∈ ℝ)
21adantl 486 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ∈ ℝ)
3 1rp 12427 . . . . . . . . . . . . 13 1 ∈ ℝ+
43a1i 11 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 ∈ ℝ+)
5 1red 10673 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 ∈ ℝ)
6 eliooord 12831 . . . . . . . . . . . . . . 15 (𝑥 ∈ (1(,)+∞) → (1 < 𝑥𝑥 < +∞))
76adantl 486 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (1 < 𝑥𝑥 < +∞))
87simpld 499 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 < 𝑥)
95, 2, 8ltled 10819 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 1 ≤ 𝑥)
102, 4, 9rpgecld 12504 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ∈ ℝ+)
11 pntrval.r . . . . . . . . . . . 12 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))
1211pntrval 26238 . . . . . . . . . . 11 (𝑥 ∈ ℝ+ → (𝑅𝑥) = ((ψ‘𝑥) − 𝑥))
1310, 12syl 17 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑅𝑥) = ((ψ‘𝑥) − 𝑥))
1413oveq1d 7166 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑅𝑥) · (log‘𝑥)) = (((ψ‘𝑥) − 𝑥) · (log‘𝑥)))
15 chpcl 25801 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → (ψ‘𝑥) ∈ ℝ)
162, 15syl 17 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (ψ‘𝑥) ∈ ℝ)
1716recnd 10700 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (ψ‘𝑥) ∈ ℂ)
182recnd 10700 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ∈ ℂ)
1910relogcld 25306 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ∈ ℝ)
2019recnd 10700 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ∈ ℂ)
2117, 18, 20subdird 11128 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((ψ‘𝑥) − 𝑥) · (log‘𝑥)) = (((ψ‘𝑥) · (log‘𝑥)) − (𝑥 · (log‘𝑥))))
2214, 21eqtrd 2794 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑅𝑥) · (log‘𝑥)) = (((ψ‘𝑥) · (log‘𝑥)) − (𝑥 · (log‘𝑥))))
2310ad2antrr 726 . . . . . . . . . . . . . . . . . . . . 21 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑥 ∈ ℝ+)
24 elfznn 12978 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
2524adantl 486 . . . . . . . . . . . . . . . . . . . . . . 23 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
2625nnrpd 12463 . . . . . . . . . . . . . . . . . . . . . 22 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ+)
2726adantr 485 . . . . . . . . . . . . . . . . . . . . 21 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑛 ∈ ℝ+)
2823, 27rpdivcld 12482 . . . . . . . . . . . . . . . . . . . 20 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (𝑥 / 𝑛) ∈ ℝ+)
29 elfznn 12978 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛))) → 𝑚 ∈ ℕ)
3029adantl 486 . . . . . . . . . . . . . . . . . . . . 21 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ∈ ℕ)
3130nnrpd 12463 . . . . . . . . . . . . . . . . . . . 20 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ∈ ℝ+)
3228, 31rpdivcld 12482 . . . . . . . . . . . . . . . . . . 19 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((𝑥 / 𝑛) / 𝑚) ∈ ℝ+)
3311pntrval 26238 . . . . . . . . . . . . . . . . . . 19 (((𝑥 / 𝑛) / 𝑚) ∈ ℝ+ → (𝑅‘((𝑥 / 𝑛) / 𝑚)) = ((ψ‘((𝑥 / 𝑛) / 𝑚)) − ((𝑥 / 𝑛) / 𝑚)))
3432, 33syl 17 . . . . . . . . . . . . . . . . . 18 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (𝑅‘((𝑥 / 𝑛) / 𝑚)) = ((ψ‘((𝑥 / 𝑛) / 𝑚)) − ((𝑥 / 𝑛) / 𝑚)))
3534oveq2d 7167 . . . . . . . . . . . . . . . . 17 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((Λ‘𝑚) · (𝑅‘((𝑥 / 𝑛) / 𝑚))) = ((Λ‘𝑚) · ((ψ‘((𝑥 / 𝑛) / 𝑚)) − ((𝑥 / 𝑛) / 𝑚))))
36 vmacl 25795 . . . . . . . . . . . . . . . . . . . 20 (𝑚 ∈ ℕ → (Λ‘𝑚) ∈ ℝ)
3730, 36syl 17 . . . . . . . . . . . . . . . . . . 19 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (Λ‘𝑚) ∈ ℝ)
3837recnd 10700 . . . . . . . . . . . . . . . . . 18 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (Λ‘𝑚) ∈ ℂ)
392adantr 485 . . . . . . . . . . . . . . . . . . . . . . 23 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ)
4039, 25nndivred 11721 . . . . . . . . . . . . . . . . . . . . . 22 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ)
4140adantr 485 . . . . . . . . . . . . . . . . . . . . 21 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (𝑥 / 𝑛) ∈ ℝ)
4241, 30nndivred 11721 . . . . . . . . . . . . . . . . . . . 20 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((𝑥 / 𝑛) / 𝑚) ∈ ℝ)
43 chpcl 25801 . . . . . . . . . . . . . . . . . . . 20 (((𝑥 / 𝑛) / 𝑚) ∈ ℝ → (ψ‘((𝑥 / 𝑛) / 𝑚)) ∈ ℝ)
4442, 43syl 17 . . . . . . . . . . . . . . . . . . 19 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (ψ‘((𝑥 / 𝑛) / 𝑚)) ∈ ℝ)
4544recnd 10700 . . . . . . . . . . . . . . . . . 18 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (ψ‘((𝑥 / 𝑛) / 𝑚)) ∈ ℂ)
4642recnd 10700 . . . . . . . . . . . . . . . . . 18 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((𝑥 / 𝑛) / 𝑚) ∈ ℂ)
4738, 45, 46subdid 11127 . . . . . . . . . . . . . . . . 17 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((Λ‘𝑚) · ((ψ‘((𝑥 / 𝑛) / 𝑚)) − ((𝑥 / 𝑛) / 𝑚))) = (((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚))) − ((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚))))
4835, 47eqtrd 2794 . . . . . . . . . . . . . . . 16 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((Λ‘𝑚) · (𝑅‘((𝑥 / 𝑛) / 𝑚))) = (((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚))) − ((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚))))
4948sumeq2dv 15101 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (𝑅‘((𝑥 / 𝑛) / 𝑚))) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚))) − ((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚))))
50 fzfid 13383 . . . . . . . . . . . . . . . 16 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1...(⌊‘(𝑥 / 𝑛))) ∈ Fin)
5137, 44remulcld 10702 . . . . . . . . . . . . . . . . 17 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚))) ∈ ℝ)
5251recnd 10700 . . . . . . . . . . . . . . . 16 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚))) ∈ ℂ)
5338, 46mulcld 10692 . . . . . . . . . . . . . . . 16 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚)) ∈ ℂ)
5450, 52, 53fsumsub 15184 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚))) − ((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚))) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚))) − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚))))
5549, 54eqtrd 2794 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (𝑅‘((𝑥 / 𝑛) / 𝑚))) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚))) − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚))))
5655oveq2d 7167 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (𝑅‘((𝑥 / 𝑛) / 𝑚)))) = ((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚))) − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚)))))
57 vmacl 25795 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ → (Λ‘𝑛) ∈ ℝ)
5825, 57syl 17 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈ ℝ)
5958recnd 10700 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈ ℂ)
6050, 51fsumrecl 15132 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚))) ∈ ℝ)
6160recnd 10700 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚))) ∈ ℂ)
6250, 53fsumcl 15131 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚)) ∈ ℂ)
6359, 61, 62subdid 11127 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚))) − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚)))) = (((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))) − ((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚)))))
6456, 63eqtrd 2794 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (𝑅‘((𝑥 / 𝑛) / 𝑚)))) = (((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))) − ((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚)))))
6564sumeq2dv 15101 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (𝑅‘((𝑥 / 𝑛) / 𝑚)))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))) − ((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚)))))
66 fzfid 13383 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (1...(⌊‘𝑥)) ∈ Fin)
6758, 60remulcld 10702 . . . . . . . . . . . . 13 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))) ∈ ℝ)
6867recnd 10700 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))) ∈ ℂ)
6959, 62mulcld 10692 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚))) ∈ ℂ)
7066, 68, 69fsumsub 15184 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))) − ((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚)))))
7165, 70eqtrd 2794 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (𝑅‘((𝑥 / 𝑛) / 𝑚)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚)))))
7271oveq2d 7167 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (𝑅‘((𝑥 / 𝑛) / 𝑚))))) = ((2 / (log‘𝑥)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚))))))
73 2re 11741 . . . . . . . . . . . . 13 2 ∈ ℝ
7473a1i 11 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 2 ∈ ℝ)
752, 8rplogcld 25312 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ∈ ℝ+)
7674, 75rerpdivcld 12496 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (2 / (log‘𝑥)) ∈ ℝ)
7776recnd 10700 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (2 / (log‘𝑥)) ∈ ℂ)
7866, 67fsumrecl 15132 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))) ∈ ℝ)
7978recnd 10700 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))) ∈ ℂ)
8066, 69fsumcl 15131 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚))) ∈ ℂ)
8177, 79, 80subdid 11127 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚))))) = (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚))))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚))))))
8272, 81eqtrd 2794 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (𝑅‘((𝑥 / 𝑛) / 𝑚))))) = (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚))))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚))))))
8322, 82oveq12d 7169 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑅𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (𝑅‘((𝑥 / 𝑛) / 𝑚)))))) = ((((ψ‘𝑥) · (log‘𝑥)) − (𝑥 · (log‘𝑥))) − (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚))))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚)))))))
8416, 19remulcld 10702 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((ψ‘𝑥) · (log‘𝑥)) ∈ ℝ)
8584recnd 10700 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((ψ‘𝑥) · (log‘𝑥)) ∈ ℂ)
8618, 20mulcld 10692 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ∈ ℂ)
8776, 78remulcld 10702 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚))))) ∈ ℝ)
8887recnd 10700 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚))))) ∈ ℂ)
8977, 80mulcld 10692 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚)))) ∈ ℂ)
9085, 86, 88, 89sub4d 11077 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((ψ‘𝑥) · (log‘𝑥)) − (𝑥 · (log‘𝑥))) − (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚))))) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚)))))) = ((((ψ‘𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))))) − ((𝑥 · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚)))))))
9183, 90eqtrd 2794 . . . . . 6 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑅𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (𝑅‘((𝑥 / 𝑛) / 𝑚)))))) = ((((ψ‘𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))))) − ((𝑥 · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚)))))))
9291oveq1d 7166 . . . . 5 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((𝑅𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (𝑅‘((𝑥 / 𝑛) / 𝑚)))))) / 𝑥) = (((((ψ‘𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))))) − ((𝑥 · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚)))))) / 𝑥))
9384, 87resubcld 11099 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((ψ‘𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))))) ∈ ℝ)
9493recnd 10700 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((ψ‘𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))))) ∈ ℂ)
952, 19remulcld 10702 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ∈ ℝ)
9637, 42remulcld 10702 . . . . . . . . . . . . 13 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚)) ∈ ℝ)
9750, 96fsumrecl 15132 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚)) ∈ ℝ)
9858, 97remulcld 10702 . . . . . . . . . . 11 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚))) ∈ ℝ)
9966, 98fsumrecl 15132 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚))) ∈ ℝ)
10076, 99remulcld 10702 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚)))) ∈ ℝ)
10195, 100resubcld 11099 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑥 · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚))))) ∈ ℝ)
102101recnd 10700 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑥 · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚))))) ∈ ℂ)
10310rpne0d 12470 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ≠ 0)
10494, 102, 18, 103divsubdird 11486 . . . . . 6 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((((ψ‘𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))))) − ((𝑥 · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚)))))) / 𝑥) = (((((ψ‘𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))))) / 𝑥) − (((𝑥 · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚))))) / 𝑥)))
10595recnd 10700 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ∈ ℂ)
10699recnd 10700 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚))) ∈ ℂ)
10777, 106mulcld 10692 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚)))) ∈ ℂ)
108105, 107, 18, 103divsubdird 11486 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑥 · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚))))) / 𝑥) = (((𝑥 · (log‘𝑥)) / 𝑥) − (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚)))) / 𝑥)))
10920, 18, 103divcan3d 11452 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((𝑥 · (log‘𝑥)) / 𝑥) = (log‘𝑥))
11077, 106, 18, 103divassd 11482 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚)))) / 𝑥) = ((2 / (log‘𝑥)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚))) / 𝑥)))
11198recnd 10700 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚))) ∈ ℂ)
11266, 18, 111, 103fsumdivc 15182 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚))) / 𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚))) / 𝑥))
11341recnd 10700 . . . . . . . . . . . . . . . . . . . . . 22 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (𝑥 / 𝑛) ∈ ℂ)
11430nncnd 11683 . . . . . . . . . . . . . . . . . . . . . 22 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ∈ ℂ)
11530nnne0d 11717 . . . . . . . . . . . . . . . . . . . . . 22 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ≠ 0)
116113, 38, 114, 115div12d 11483 . . . . . . . . . . . . . . . . . . . . 21 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((𝑥 / 𝑛) · ((Λ‘𝑚) / 𝑚)) = ((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚)))
11718adantr 485 . . . . . . . . . . . . . . . . . . . . . . 23 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℂ)
118117adantr 485 . . . . . . . . . . . . . . . . . . . . . 22 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑥 ∈ ℂ)
11925nncnd 11683 . . . . . . . . . . . . . . . . . . . . . . 23 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℂ)
120119adantr 485 . . . . . . . . . . . . . . . . . . . . . 22 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑛 ∈ ℂ)
12137, 30nndivred 11721 . . . . . . . . . . . . . . . . . . . . . . 23 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((Λ‘𝑚) / 𝑚) ∈ ℝ)
122121recnd 10700 . . . . . . . . . . . . . . . . . . . . . 22 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((Λ‘𝑚) / 𝑚) ∈ ℂ)
12325nnne0d 11717 . . . . . . . . . . . . . . . . . . . . . . 23 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ≠ 0)
124123adantr 485 . . . . . . . . . . . . . . . . . . . . . 22 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑛 ≠ 0)
125118, 120, 122, 124div32d 11470 . . . . . . . . . . . . . . . . . . . . 21 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((𝑥 / 𝑛) · ((Λ‘𝑚) / 𝑚)) = (𝑥 · (((Λ‘𝑚) / 𝑚) / 𝑛)))
126116, 125eqtr3d 2796 . . . . . . . . . . . . . . . . . . . 20 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚)) = (𝑥 · (((Λ‘𝑚) / 𝑚) / 𝑛)))
127126oveq1d 7166 . . . . . . . . . . . . . . . . . . 19 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚)) / 𝑥) = ((𝑥 · (((Λ‘𝑚) / 𝑚) / 𝑛)) / 𝑥))
12825adantr 485 . . . . . . . . . . . . . . . . . . . . . 22 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑛 ∈ ℕ)
129121, 128nndivred 11721 . . . . . . . . . . . . . . . . . . . . 21 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (((Λ‘𝑚) / 𝑚) / 𝑛) ∈ ℝ)
130129recnd 10700 . . . . . . . . . . . . . . . . . . . 20 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (((Λ‘𝑚) / 𝑚) / 𝑛) ∈ ℂ)
131103adantr 485 . . . . . . . . . . . . . . . . . . . . 21 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ≠ 0)
132131adantr 485 . . . . . . . . . . . . . . . . . . . 20 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑥 ≠ 0)
133130, 118, 132divcan3d 11452 . . . . . . . . . . . . . . . . . . 19 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((𝑥 · (((Λ‘𝑚) / 𝑚) / 𝑛)) / 𝑥) = (((Λ‘𝑚) / 𝑚) / 𝑛))
134127, 133eqtrd 2794 . . . . . . . . . . . . . . . . . 18 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚)) / 𝑥) = (((Λ‘𝑚) / 𝑚) / 𝑛))
135134sumeq2dv 15101 . . . . . . . . . . . . . . . . 17 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚)) / 𝑥) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(((Λ‘𝑚) / 𝑚) / 𝑛))
13696recnd 10700 . . . . . . . . . . . . . . . . . 18 ((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚)) ∈ ℂ)
13750, 117, 136, 131fsumdivc 15182 . . . . . . . . . . . . . . . . 17 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚)) / 𝑥) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚)) / 𝑥))
13850, 119, 122, 123fsumdivc 15182 . . . . . . . . . . . . . . . . 17 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) / 𝑛) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(((Λ‘𝑚) / 𝑚) / 𝑛))
139135, 137, 1383eqtr4d 2804 . . . . . . . . . . . . . . . 16 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚)) / 𝑥) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) / 𝑛))
140139oveq2d 7167 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚)) / 𝑥)) = ((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) / 𝑛)))
14197recnd 10700 . . . . . . . . . . . . . . . 16 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚)) ∈ ℂ)
14259, 141, 117, 131divassd 11482 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚))) / 𝑥) = ((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚)) / 𝑥)))
14350, 121fsumrecl 15132 . . . . . . . . . . . . . . . . 17 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) ∈ ℝ)
144143recnd 10700 . . . . . . . . . . . . . . . 16 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) ∈ ℂ)
14559, 119, 144, 123div32d 11470 . . . . . . . . . . . . . . 15 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) = ((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) / 𝑛)))
146140, 142, 1453eqtr4d 2804 . . . . . . . . . . . . . 14 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚))) / 𝑥) = (((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)))
147146sumeq2dv 15101 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚))) / 𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)))
148112, 147eqtrd 2794 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚))) / 𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)))
149148oveq2d 7167 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚))) / 𝑥)) = ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚))))
150110, 149eqtrd 2794 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚)))) / 𝑥) = ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚))))
151109, 150oveq12d 7169 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑥 · (log‘𝑥)) / 𝑥) − (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚)))) / 𝑥)) = ((log‘𝑥) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)))))
152108, 151eqtrd 2794 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((𝑥 · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚))))) / 𝑥) = ((log‘𝑥) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)))))
153152oveq2d 7167 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((((ψ‘𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))))) / 𝑥) − (((𝑥 · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚))))) / 𝑥)) = (((((ψ‘𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))))) / 𝑥) − ((log‘𝑥) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚))))))
15494, 18, 103divcld 11447 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((ψ‘𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))))) / 𝑥) ∈ ℂ)
15558, 25nndivred 11721 . . . . . . . . . . . 12 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) / 𝑛) ∈ ℝ)
156155, 143remulcld 10702 . . . . . . . . . . 11 (((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) ∈ ℝ)
15766, 156fsumrecl 15132 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) ∈ ℝ)
15876, 157remulcld 10702 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚))) ∈ ℝ)
159158recnd 10700 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚))) ∈ ℂ)
160154, 20, 159subsub2d 11057 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((((ψ‘𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))))) / 𝑥) − ((log‘𝑥) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚))))) = (((((ψ‘𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))))) / 𝑥) + (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚))) − (log‘𝑥))))
161153, 160eqtrd 2794 . . . . . 6 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((((ψ‘𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))))) / 𝑥) − (((𝑥 · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚))))) / 𝑥)) = (((((ψ‘𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))))) / 𝑥) + (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚))) − (log‘𝑥))))
162104, 161eqtrd 2794 . . . . 5 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((((ψ‘𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))))) − ((𝑥 · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((𝑥 / 𝑛) / 𝑚)))))) / 𝑥) = (((((ψ‘𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))))) / 𝑥) + (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚))) − (log‘𝑥))))
16392, 162eqtrd 2794 . . . 4 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((𝑅𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (𝑅‘((𝑥 / 𝑛) / 𝑚)))))) / 𝑥) = (((((ψ‘𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))))) / 𝑥) + (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚))) − (log‘𝑥))))
164163mpteq2dva 5128 . . 3 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((((𝑅𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (𝑅‘((𝑥 / 𝑛) / 𝑚)))))) / 𝑥)) = (𝑥 ∈ (1(,)+∞) ↦ (((((ψ‘𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))))) / 𝑥) + (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚))) − (log‘𝑥)))))
16593, 10rerpdivcld 12496 . . . 4 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((((ψ‘𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))))) / 𝑥) ∈ ℝ)
166158, 19resubcld 11099 . . . 4 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚))) − (log‘𝑥)) ∈ ℝ)
167 selberg4 26237 . . . . 5 (𝑥 ∈ (1(,)+∞) ↦ ((((ψ‘𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))))) / 𝑥)) ∈ 𝑂(1)
168167a1i 11 . . . 4 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((((ψ‘𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))))) / 𝑥)) ∈ 𝑂(1))
169 2cnd 11745 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 2 ∈ ℂ)
170157, 75rerpdivcld 12496 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥)) ∈ ℝ)
171170recnd 10700 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥)) ∈ ℂ)
17219rehalfcld 11914 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((log‘𝑥) / 2) ∈ ℝ)
173172recnd 10700 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((log‘𝑥) / 2) ∈ ℂ)
174169, 171, 173subdid 11127 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (2 · ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥)) − ((log‘𝑥) / 2))) = ((2 · (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥))) − (2 · ((log‘𝑥) / 2))))
175157recnd 10700 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) ∈ ℂ)
17675rpne0d 12470 . . . . . . . . . 10 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (log‘𝑥) ≠ 0)
177169, 20, 175, 176div32d 11470 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚))) = (2 · (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥))))
178177eqcomd 2765 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (2 · (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥))) = ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚))))
179 2ne0 11771 . . . . . . . . . 10 2 ≠ 0
180179a1i 11 . . . . . . . . 9 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → 2 ≠ 0)
18120, 169, 180divcan2d 11449 . . . . . . . 8 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (2 · ((log‘𝑥) / 2)) = (log‘𝑥))
182178, 181oveq12d 7169 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((2 · (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥))) − (2 · ((log‘𝑥) / 2))) = (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚))) − (log‘𝑥)))
183174, 182eqtrd 2794 . . . . . 6 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → (2 · ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥)) − ((log‘𝑥) / 2))) = (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚))) − (log‘𝑥)))
184183mpteq2dva 5128 . . . . 5 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (2 · ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥)) − ((log‘𝑥) / 2)))) = (𝑥 ∈ (1(,)+∞) ↦ (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚))) − (log‘𝑥))))
185170, 172resubcld 11099 . . . . . 6 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥)) − ((log‘𝑥) / 2)) ∈ ℝ)
186 ioossre 12833 . . . . . . 7 (1(,)+∞) ⊆ ℝ
187 2cnd 11745 . . . . . . 7 (⊤ → 2 ∈ ℂ)
188 o1const 15017 . . . . . . 7 (((1(,)+∞) ⊆ ℝ ∧ 2 ∈ ℂ) → (𝑥 ∈ (1(,)+∞) ↦ 2) ∈ 𝑂(1))
189186, 187, 188sylancr 591 . . . . . 6 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ 2) ∈ 𝑂(1))
190 2vmadivsum 26217 . . . . . . 7 (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥)) − ((log‘𝑥) / 2))) ∈ 𝑂(1)
191190a1i 11 . . . . . 6 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥)) − ((log‘𝑥) / 2))) ∈ 𝑂(1))
19274, 185, 189, 191o1mul2 15022 . . . . 5 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (2 · ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥)) − ((log‘𝑥) / 2)))) ∈ 𝑂(1))
193184, 192eqeltrrd 2854 . . . 4 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚))) − (log‘𝑥))) ∈ 𝑂(1))
194165, 166, 168, 193o1add2 15021 . . 3 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ (((((ψ‘𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))))) / 𝑥) + (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚))) − (log‘𝑥)))) ∈ 𝑂(1))
195164, 194eqeltrd 2853 . 2 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((((𝑅𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (𝑅‘((𝑥 / 𝑛) / 𝑚)))))) / 𝑥)) ∈ 𝑂(1))
196195mptru 1546 1 (𝑥 ∈ (1(,)+∞) ↦ ((((𝑅𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (𝑅‘((𝑥 / 𝑛) / 𝑚)))))) / 𝑥)) ∈ 𝑂(1)
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 400   = wceq 1539  ⊤wtru 1540   ∈ wcel 2112   ≠ wne 2952   ⊆ wss 3859   class class class wbr 5033   ↦ cmpt 5113  ‘cfv 6336  (class class class)co 7151  ℂcc 10566  ℝcr 10567  0cc0 10568  1c1 10569   + caddc 10571   · cmul 10573  +∞cpnf 10703   < clt 10706   − cmin 10901   / cdiv 11328  ℕcn 11667  2c2 11722  ℝ+crp 12423  (,)cioo 12772  ...cfz 12932  ⌊cfl 13202  𝑂(1)co1 14884  Σcsu 15083  logclog 25238  Λcvma 25769  ψcchp 25770 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5235  ax-pr 5299  ax-un 7460  ax-inf2 9130  ax-cnex 10624  ax-resscn 10625  ax-1cn 10626  ax-icn 10627  ax-addcl 10628  ax-addrcl 10629  ax-mulcl 10630  ax-mulrcl 10631  ax-mulcom 10632  ax-addass 10633  ax-mulass 10634  ax-distr 10635  ax-i2m1 10636  ax-1ne0 10637  ax-1rid 10638  ax-rnegex 10639  ax-rrecex 10640  ax-cnre 10641  ax-pre-lttri 10642  ax-pre-lttrn 10643  ax-pre-ltadd 10644  ax-pre-mulgt0 10645  ax-pre-sup 10646  ax-addf 10647  ax-mulf 10648 This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-nel 3057  df-ral 3076  df-rex 3077  df-reu 3078  df-rmo 3079  df-rab 3080  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-pss 3878  df-nul 4227  df-if 4422  df-pw 4497  df-sn 4524  df-pr 4526  df-tp 4528  df-op 4530  df-uni 4800  df-int 4840  df-iun 4886  df-iin 4887  df-disj 4999  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5431  df-eprel 5436  df-po 5444  df-so 5445  df-fr 5484  df-se 5485  df-we 5486  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-pred 6127  df-ord 6173  df-on 6174  df-lim 6175  df-suc 6176  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-isom 6345  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-of 7406  df-om 7581  df-1st 7694  df-2nd 7695  df-supp 7837  df-wrecs 7958  df-recs 8019  df-rdg 8057  df-1o 8113  df-2o 8114  df-oadd 8117  df-er 8300  df-map 8419  df-pm 8420  df-ixp 8481  df-en 8529  df-dom 8530  df-sdom 8531  df-fin 8532  df-fsupp 8860  df-fi 8901  df-sup 8932  df-inf 8933  df-oi 9000  df-dju 9356  df-card 9394  df-pnf 10708  df-mnf 10709  df-xr 10710  df-ltxr 10711  df-le 10712  df-sub 10903  df-neg 10904  df-div 11329  df-nn 11668  df-2 11730  df-3 11731  df-4 11732  df-5 11733  df-6 11734  df-7 11735  df-8 11736  df-9 11737  df-n0 11928  df-xnn0 12000  df-z 12014  df-dec 12131  df-uz 12276  df-q 12382  df-rp 12424  df-xneg 12541  df-xadd 12542  df-xmul 12543  df-ioo 12776  df-ioc 12777  df-ico 12778  df-icc 12779  df-fz 12933  df-fzo 13076  df-fl 13204  df-mod 13280  df-seq 13412  df-exp 13473  df-fac 13677  df-bc 13706  df-hash 13734  df-shft 14467  df-cj 14499  df-re 14500  df-im 14501  df-sqrt 14635  df-abs 14636  df-limsup 14869  df-clim 14886  df-rlim 14887  df-o1 14888  df-lo1 14889  df-sum 15084  df-ef 15462  df-e 15463  df-sin 15464  df-cos 15465  df-tan 15466  df-pi 15467  df-dvds 15649  df-gcd 15887  df-prm 16061  df-pc 16222  df-struct 16536  df-ndx 16537  df-slot 16538  df-base 16540  df-sets 16541  df-ress 16542  df-plusg 16629  df-mulr 16630  df-starv 16631  df-sca 16632  df-vsca 16633  df-ip 16634  df-tset 16635  df-ple 16636  df-ds 16638  df-unif 16639  df-hom 16640  df-cco 16641  df-rest 16747  df-topn 16748  df-0g 16766  df-gsum 16767  df-topgen 16768  df-pt 16769  df-prds 16772  df-xrs 16826  df-qtop 16831  df-imas 16832  df-xps 16834  df-mre 16908  df-mrc 16909  df-acs 16911  df-mgm 17911  df-sgrp 17960  df-mnd 17971  df-submnd 18016  df-mulg 18285  df-cntz 18507  df-cmn 18968  df-psmet 20151  df-xmet 20152  df-met 20153  df-bl 20154  df-mopn 20155  df-fbas 20156  df-fg 20157  df-cnfld 20160  df-top 21587  df-topon 21604  df-topsp 21626  df-bases 21639  df-cld 21712  df-ntr 21713  df-cls 21714  df-nei 21791  df-lp 21829  df-perf 21830  df-cn 21920  df-cnp 21921  df-haus 22008  df-cmp 22080  df-tx 22255  df-hmeo 22448  df-fil 22539  df-fm 22631  df-flim 22632  df-flf 22633  df-xms 23015  df-ms 23016  df-tms 23017  df-cncf 23572  df-limc 24558  df-dv 24559  df-ulm 25064  df-log 25240  df-cxp 25241  df-atan 25545  df-em 25670  df-cht 25774  df-vma 25775  df-chp 25776  df-ppi 25777  df-mu 25778 This theorem is referenced by:  selberg34r  26247
 Copyright terms: Public domain W3C validator