Metamath Proof Explorer

Theorem selbergr

Description: Selberg's symmetry formula, using the residual of the second Chebyshev function. Equation 10.6.2 of Shapiro, p. 428. (Contributed by Mario Carneiro, 16-Apr-2016)

Ref Expression
Hypothesis pntrval.r ⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
Assertion selbergr ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( 𝑅 ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) ) ∈ 𝑂(1)

Proof

Step Hyp Ref Expression
1 pntrval.r ⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
2 reex ⊢ ℝ ∈ V
3 rpssre ⊢ ℝ+ ⊆ ℝ
4 2 3 ssexi ⊢ ℝ+ ∈ V
5 4 a1i ⊢ ( ⊤ → ℝ+ ∈ V )
6 ovexd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ∈ V )
7 ovexd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) − ( log ‘ 𝑥 ) ) ∈ V )
8 eqidd ⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) )
9 eqidd ⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) − ( log ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) − ( log ‘ 𝑥 ) ) ) )
10 5 6 7 8 9 offval2 ⊢ ( ⊤ → ( ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∘f − ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) − ( log ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) − ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) − ( log ‘ 𝑥 ) ) ) ) )
11 10 mptru ⊢ ( ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∘f − ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) − ( log ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) − ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) − ( log ‘ 𝑥 ) ) ) )
12 1 pntrf ⊢ 𝑅 : ℝ+ ⟶ ℝ
13 12 ffvelrni ⊢ ( 𝑥 ∈ ℝ+ → ( 𝑅 ‘ 𝑥 ) ∈ ℝ )
14 13 recnd ⊢ ( 𝑥 ∈ ℝ+ → ( 𝑅 ‘ 𝑥 ) ∈ ℂ )
15 relogcl ⊢ ( 𝑥 ∈ ℝ+ → ( log ‘ 𝑥 ) ∈ ℝ )
16 15 recnd ⊢ ( 𝑥 ∈ ℝ+ → ( log ‘ 𝑥 ) ∈ ℂ )
17 14 16 mulcld ⊢ ( 𝑥 ∈ ℝ+ → ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ∈ ℂ )
18 fzfid ⊢ ( 𝑥 ∈ ℝ+ → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
19 elfznn ⊢ ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑑 ∈ ℕ )
20 19 adantl ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑑 ∈ ℕ )
21 vmacl ⊢ ( 𝑑 ∈ ℕ → ( Λ ‘ 𝑑 ) ∈ ℝ )
22 20 21 syl ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑑 ) ∈ ℝ )
23 22 recnd ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑑 ) ∈ ℂ )
24 rpre ⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ )
25 nndivre ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑑 ∈ ℕ ) → ( 𝑥 / 𝑑 ) ∈ ℝ )
26 24 19 25 syl2an ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑑 ) ∈ ℝ )
27 chpcl ⊢ ( ( 𝑥 / 𝑑 ) ∈ ℝ → ( ψ ‘ ( 𝑥 / 𝑑 ) ) ∈ ℝ )
28 26 27 syl ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ψ ‘ ( 𝑥 / 𝑑 ) ) ∈ ℝ )
29 28 recnd ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ψ ‘ ( 𝑥 / 𝑑 ) ) ∈ ℂ )
30 23 29 mulcld ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ∈ ℂ )
31 18 30 fsumcl ⊢ ( 𝑥 ∈ ℝ+ → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ∈ ℂ )
32 17 31 addcld ⊢ ( 𝑥 ∈ ℝ+ → ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) ∈ ℂ )
33 rpcn ⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℂ )
34 rpne0 ⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ≠ 0 )
35 32 33 34 divcld ⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) ∈ ℂ )
36 22 20 nndivred ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑑 ) / 𝑑 ) ∈ ℝ )
37 36 recnd ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑑 ) / 𝑑 ) ∈ ℂ )
38 18 37 fsumcl ⊢ ( 𝑥 ∈ ℝ+ → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) ∈ ℂ )
39 35 38 16 nnncan2d ⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( log ‘ 𝑥 ) ) − ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) − ( log ‘ 𝑥 ) ) ) = ( ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) )
40 chpcl ⊢ ( 𝑥 ∈ ℝ → ( ψ ‘ 𝑥 ) ∈ ℝ )
41 24 40 syl ⊢ ( 𝑥 ∈ ℝ+ → ( ψ ‘ 𝑥 ) ∈ ℝ )
42 41 recnd ⊢ ( 𝑥 ∈ ℝ+ → ( ψ ‘ 𝑥 ) ∈ ℂ )
43 42 16 mulcld ⊢ ( 𝑥 ∈ ℝ+ → ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ∈ ℂ )
44 43 31 addcld ⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) ∈ ℂ )
45 44 33 34 divcld ⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) ∈ ℂ )
46 45 16 16 subsub4d ⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( log ‘ 𝑥 ) ) − ( log ‘ 𝑥 ) ) = ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( ( log ‘ 𝑥 ) + ( log ‘ 𝑥 ) ) ) )
47 1 pntrval ⊢ ( 𝑥 ∈ ℝ+ → ( 𝑅 ‘ 𝑥 ) = ( ( ψ ‘ 𝑥 ) − 𝑥 ) )
48 47 oveq1d ⊢ ( 𝑥 ∈ ℝ+ → ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) = ( ( ( ψ ‘ 𝑥 ) − 𝑥 ) · ( log ‘ 𝑥 ) ) )
49 42 33 16 subdird ⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ψ ‘ 𝑥 ) − 𝑥 ) · ( log ‘ 𝑥 ) ) = ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( 𝑥 · ( log ‘ 𝑥 ) ) ) )
50 48 49 eqtrd ⊢ ( 𝑥 ∈ ℝ+ → ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) = ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( 𝑥 · ( log ‘ 𝑥 ) ) ) )
51 50 oveq1d ⊢ ( 𝑥 ∈ ℝ+ → ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) = ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( 𝑥 · ( log ‘ 𝑥 ) ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) )
52 33 16 mulcld ⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 · ( log ‘ 𝑥 ) ) ∈ ℂ )
53 43 31 52 addsubd ⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) − ( 𝑥 · ( log ‘ 𝑥 ) ) ) = ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( 𝑥 · ( log ‘ 𝑥 ) ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) )
54 51 53 eqtr4d ⊢ ( 𝑥 ∈ ℝ+ → ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) = ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) − ( 𝑥 · ( log ‘ 𝑥 ) ) ) )
55 54 oveq1d ⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) = ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) − ( 𝑥 · ( log ‘ 𝑥 ) ) ) / 𝑥 ) )
56 rpcnne0 ⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) )
57 divsubdir ⊢ ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) ∈ ℂ ∧ ( 𝑥 · ( log ‘ 𝑥 ) ) ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ) → ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) − ( 𝑥 · ( log ‘ 𝑥 ) ) ) / 𝑥 ) = ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( ( 𝑥 · ( log ‘ 𝑥 ) ) / 𝑥 ) ) )
58 44 52 56 57 syl3anc ⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) − ( 𝑥 · ( log ‘ 𝑥 ) ) ) / 𝑥 ) = ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( ( 𝑥 · ( log ‘ 𝑥 ) ) / 𝑥 ) ) )
59 16 33 34 divcan3d ⊢ ( 𝑥 ∈ ℝ+ → ( ( 𝑥 · ( log ‘ 𝑥 ) ) / 𝑥 ) = ( log ‘ 𝑥 ) )
60 59 oveq2d ⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( ( 𝑥 · ( log ‘ 𝑥 ) ) / 𝑥 ) ) = ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( log ‘ 𝑥 ) ) )
61 55 58 60 3eqtrd ⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) = ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( log ‘ 𝑥 ) ) )
62 61 oveq1d ⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( log ‘ 𝑥 ) ) = ( ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( log ‘ 𝑥 ) ) − ( log ‘ 𝑥 ) ) )
63 16 2timesd ⊢ ( 𝑥 ∈ ℝ+ → ( 2 · ( log ‘ 𝑥 ) ) = ( ( log ‘ 𝑥 ) + ( log ‘ 𝑥 ) ) )
64 63 oveq2d ⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) = ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( ( log ‘ 𝑥 ) + ( log ‘ 𝑥 ) ) ) )
65 46 62 64 3eqtr4d ⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( log ‘ 𝑥 ) ) = ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) )
66 65 oveq1d ⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( log ‘ 𝑥 ) ) − ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) − ( log ‘ 𝑥 ) ) ) = ( ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) − ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) − ( log ‘ 𝑥 ) ) ) )
67 33 38 mulcld ⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) ∈ ℂ )
68 divsubdir ⊢ ( ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) ∈ ℂ ∧ ( 𝑥 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ) → ( ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) − ( 𝑥 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) ) / 𝑥 ) = ( ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( ( 𝑥 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) / 𝑥 ) ) )
69 32 67 56 68 syl3anc ⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) − ( 𝑥 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) ) / 𝑥 ) = ( ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( ( 𝑥 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) / 𝑥 ) ) )
70 17 31 67 addsubassd ⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) − ( 𝑥 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) ) = ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) − ( 𝑥 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) ) ) )
71 33 adantr ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ℂ )
72 71 37 mulcld ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 · ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) ∈ ℂ )
73 18 30 72 fsumsub ⊢ ( 𝑥 ∈ ℝ+ → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) − ( 𝑥 · ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) ) = ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) − Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝑥 · ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) ) )
74 26 recnd ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑑 ) ∈ ℂ )
75 23 29 74 subdid ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑑 ) · ( ( ψ ‘ ( 𝑥 / 𝑑 ) ) − ( 𝑥 / 𝑑 ) ) ) = ( ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) − ( ( Λ ‘ 𝑑 ) · ( 𝑥 / 𝑑 ) ) ) )
76 19 nnrpd ⊢ ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑑 ∈ ℝ+ )
77 rpdivcl ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) → ( 𝑥 / 𝑑 ) ∈ ℝ+ )
78 76 77 sylan2 ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑑 ) ∈ ℝ+ )
79 1 pntrval ⊢ ( ( 𝑥 / 𝑑 ) ∈ ℝ+ → ( 𝑅 ‘ ( 𝑥 / 𝑑 ) ) = ( ( ψ ‘ ( 𝑥 / 𝑑 ) ) − ( 𝑥 / 𝑑 ) ) )
80 78 79 syl ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑅 ‘ ( 𝑥 / 𝑑 ) ) = ( ( ψ ‘ ( 𝑥 / 𝑑 ) ) − ( 𝑥 / 𝑑 ) ) )
81 80 oveq2d ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑑 ) · ( 𝑅 ‘ ( 𝑥 / 𝑑 ) ) ) = ( ( Λ ‘ 𝑑 ) · ( ( ψ ‘ ( 𝑥 / 𝑑 ) ) − ( 𝑥 / 𝑑 ) ) ) )
82 20 nnrpd ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑑 ∈ ℝ+ )
83 rpcnne0 ⊢ ( 𝑑 ∈ ℝ+ → ( 𝑑 ∈ ℂ ∧ 𝑑 ≠ 0 ) )
84 82 83 syl ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑑 ∈ ℂ ∧ 𝑑 ≠ 0 ) )
85 div12 ⊢ ( ( 𝑥 ∈ ℂ ∧ ( Λ ‘ 𝑑 ) ∈ ℂ ∧ ( 𝑑 ∈ ℂ ∧ 𝑑 ≠ 0 ) ) → ( 𝑥 · ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) = ( ( Λ ‘ 𝑑 ) · ( 𝑥 / 𝑑 ) ) )
86 71 23 84 85 syl3anc ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 · ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) = ( ( Λ ‘ 𝑑 ) · ( 𝑥 / 𝑑 ) ) )
87 86 oveq2d ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) − ( 𝑥 · ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) ) = ( ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) − ( ( Λ ‘ 𝑑 ) · ( 𝑥 / 𝑑 ) ) ) )
88 75 81 87 3eqtr4d ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑑 ) · ( 𝑅 ‘ ( 𝑥 / 𝑑 ) ) ) = ( ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) − ( 𝑥 · ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) ) )
89 88 sumeq2dv ⊢ ( 𝑥 ∈ ℝ+ → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( 𝑅 ‘ ( 𝑥 / 𝑑 ) ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) − ( 𝑥 · ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) ) )
90 18 33 37 fsummulc2 ⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝑥 · ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) )
91 90 oveq2d ⊢ ( 𝑥 ∈ ℝ+ → ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) − ( 𝑥 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) ) = ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) − Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝑥 · ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) ) )
92 73 89 91 3eqtr4rd ⊢ ( 𝑥 ∈ ℝ+ → ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) − ( 𝑥 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( 𝑅 ‘ ( 𝑥 / 𝑑 ) ) ) )
93 92 oveq2d ⊢ ( 𝑥 ∈ ℝ+ → ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) − ( 𝑥 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) ) ) = ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( 𝑅 ‘ ( 𝑥 / 𝑑 ) ) ) ) )
94 70 93 eqtrd ⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) − ( 𝑥 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) ) = ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( 𝑅 ‘ ( 𝑥 / 𝑑 ) ) ) ) )
95 94 oveq1d ⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) − ( 𝑥 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) ) / 𝑥 ) = ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( 𝑅 ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) )
96 38 33 34 divcan3d ⊢ ( 𝑥 ∈ ℝ+ → ( ( 𝑥 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) / 𝑥 ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) )
97 96 oveq2d ⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( ( 𝑥 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) / 𝑥 ) ) = ( ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) )
98 69 95 97 3eqtr3rd ⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) ) = ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( 𝑅 ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) )
99 39 66 98 3eqtr3d ⊢ ( 𝑥 ∈ ℝ+ → ( ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) − ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) − ( log ‘ 𝑥 ) ) ) = ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( 𝑅 ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) )
100 99 mpteq2ia ⊢ ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) − ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) − ( log ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( 𝑅 ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) )
101 11 100 eqtri ⊢ ( ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∘f − ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) − ( log ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( 𝑅 ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) )
102 selberg2 ⊢ ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1)
103 vmadivsum ⊢ ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1)
104 o1sub ⊢ ( ( ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) ∧ ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) ) → ( ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∘f − ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) − ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )
105 102 103 104 mp2an ⊢ ( ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( ψ ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∘f − ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) / 𝑑 ) − ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1)
106 101 105 eqeltrri ⊢ ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( 𝑅 ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑑 ) · ( 𝑅 ‘ ( 𝑥 / 𝑑 ) ) ) ) / 𝑥 ) ) ∈ 𝑂(1)