Metamath Proof Explorer

Theorem dchrvmasumlem3

Description: Lemma for dchrvmasum . (Contributed by Mario Carneiro, 3-May-2016)

Ref Expression
Hypotheses rpvmasum.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
rpvmasum.l ⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
rpvmasum.a ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
rpvmasum.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
rpvmasum.d ⊢ 𝐷 = ( Base ‘ 𝐺 )
rpvmasum.1 ⊢ 1 = ( 0g ‘ 𝐺 )
dchrisum.b ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
dchrisum.n1 ⊢ ( 𝜑 → 𝑋 ≠ 1 )
dchrvmasum.f ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) → 𝐹 ∈ ℂ )
dchrvmasum.g ⊢ ( 𝑚 = ( 𝑥 / 𝑑 ) → 𝐹 = 𝐾 )
dchrvmasum.c ⊢ ( 𝜑 → 𝐶 ∈ ( 0 [,) +∞ ) )
dchrvmasum.t ⊢ ( 𝜑 → 𝑇 ∈ ℂ )
dchrvmasum.1 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) → ( abs ‘ ( 𝐹 − 𝑇 ) ) ≤ ( 𝐶 · ( ( log ‘ 𝑚 ) / 𝑚 ) ) )
dchrvmasum.r ⊢ ( 𝜑 → 𝑅 ∈ ℝ )
dchrvmasum.2 ⊢ ( 𝜑 → ∀ 𝑚 ∈ ( 1 [,) 3 ) ( abs ‘ ( 𝐹 − 𝑇 ) ) ≤ 𝑅 )
Assertion dchrvmasumlem3 ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( 𝐾 − 𝑇 ) ) ) ∈ 𝑂(1) )

Proof

Step Hyp Ref Expression
1 rpvmasum.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
2 rpvmasum.l ⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
3 rpvmasum.a ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4 rpvmasum.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
5 rpvmasum.d ⊢ 𝐷 = ( Base ‘ 𝐺 )
6 rpvmasum.1 ⊢ 1 = ( 0g ‘ 𝐺 )
7 dchrisum.b ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
8 dchrisum.n1 ⊢ ( 𝜑 → 𝑋 ≠ 1 )
9 dchrvmasum.f ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) → 𝐹 ∈ ℂ )
10 dchrvmasum.g ⊢ ( 𝑚 = ( 𝑥 / 𝑑 ) → 𝐹 = 𝐾 )
11 dchrvmasum.c ⊢ ( 𝜑 → 𝐶 ∈ ( 0 [,) +∞ ) )
12 dchrvmasum.t ⊢ ( 𝜑 → 𝑇 ∈ ℂ )
13 dchrvmasum.1 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) → ( abs ‘ ( 𝐹 − 𝑇 ) ) ≤ ( 𝐶 · ( ( log ‘ 𝑚 ) / 𝑚 ) ) )
14 dchrvmasum.r ⊢ ( 𝜑 → 𝑅 ∈ ℝ )
15 dchrvmasum.2 ⊢ ( 𝜑 → ∀ 𝑚 ∈ ( 1 [,) 3 ) ( abs ‘ ( 𝐹 − 𝑇 ) ) ≤ 𝑅 )
16 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
17 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 dchrvmasumlem2 ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝐾 − 𝑇 ) ) / 𝑑 ) ) ∈ 𝑂(1) )
18 fzfid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
19 10 eleq1d ⊢ ( 𝑚 = ( 𝑥 / 𝑑 ) → ( 𝐹 ∈ ℂ ↔ 𝐾 ∈ ℂ ) )
20 9 ralrimiva ⊢ ( 𝜑 → ∀ 𝑚 ∈ ℝ+ 𝐹 ∈ ℂ )
21 20 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ∀ 𝑚 ∈ ℝ+ 𝐹 ∈ ℂ )
22 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ+ )
23 elfznn ⊢ ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑑 ∈ ℕ )
24 23 nnrpd ⊢ ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑑 ∈ ℝ+ )
25 rpdivcl ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) → ( 𝑥 / 𝑑 ) ∈ ℝ+ )
26 22 24 25 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑑 ) ∈ ℝ+ )
27 19 21 26 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝐾 ∈ ℂ )
28 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑇 ∈ ℂ )
29 27 28 subcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐾 − 𝑇 ) ∈ ℂ )
30 29 abscld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( 𝐾 − 𝑇 ) ) ∈ ℝ )
31 23 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑑 ∈ ℕ )
32 30 31 nndivred ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( 𝐾 − 𝑇 ) ) / 𝑑 ) ∈ ℝ )
33 18 32 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝐾 − 𝑇 ) ) / 𝑑 ) ∈ ℝ )
34 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑋 ∈ 𝐷 )
35 elfzelz ⊢ ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑑 ∈ ℤ )
36 35 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑑 ∈ ℤ )
37 4 1 5 2 34 36 dchrzrhcl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) ∈ ℂ )
38 mucl ⊢ ( 𝑑 ∈ ℕ → ( μ ‘ 𝑑 ) ∈ ℤ )
39 31 38 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( μ ‘ 𝑑 ) ∈ ℤ )
40 39 zred ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( μ ‘ 𝑑 ) ∈ ℝ )
41 40 31 nndivred ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( μ ‘ 𝑑 ) / 𝑑 ) ∈ ℝ )
42 41 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( μ ‘ 𝑑 ) / 𝑑 ) ∈ ℂ )
43 37 42 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) ∈ ℂ )
44 43 29 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( 𝐾 − 𝑇 ) ) ∈ ℂ )
45 18 44 fsumcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( 𝐾 − 𝑇 ) ) ∈ ℂ )
46 45 abscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( abs ‘ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( 𝐾 − 𝑇 ) ) ) ∈ ℝ )
47 33 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝐾 − 𝑇 ) ) / 𝑑 ) ∈ ℂ )
48 47 abscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( abs ‘ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝐾 − 𝑇 ) ) / 𝑑 ) ) ∈ ℝ )
49 44 abscld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( 𝐾 − 𝑇 ) ) ) ∈ ℝ )
50 18 49 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( 𝐾 − 𝑇 ) ) ) ∈ ℝ )
51 18 44 fsumabs ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( abs ‘ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( 𝐾 − 𝑇 ) ) ) ≤ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( 𝐾 − 𝑇 ) ) ) )
52 43 abscld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) ) ∈ ℝ )
53 31 nnrecred ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 / 𝑑 ) ∈ ℝ )
54 29 absge0d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( abs ‘ ( 𝐾 − 𝑇 ) ) )
55 37 42 absmuld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) ) = ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) ) · ( abs ‘ ( ( μ ‘ 𝑑 ) / 𝑑 ) ) ) )
56 37 abscld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) ) ∈ ℝ )
57 1red ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 1 ∈ ℝ )
58 42 abscld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( μ ‘ 𝑑 ) / 𝑑 ) ) ∈ ℝ )
59 37 absge0d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) ) )
60 42 absge0d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( abs ‘ ( ( μ ‘ 𝑑 ) / 𝑑 ) ) )
61 eqid ⊢ ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 )
62 3 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
63 1 61 2 znzrhfo ⊢ ( 𝑁 ∈ ℕ0 → 𝐿 : ℤ –onto→ ( Base ‘ 𝑍 ) )
64 62 63 syl ⊢ ( 𝜑 → 𝐿 : ℤ –onto→ ( Base ‘ 𝑍 ) )
65 fof ⊢ ( 𝐿 : ℤ –onto→ ( Base ‘ 𝑍 ) → 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) )
66 64 65 syl ⊢ ( 𝜑 → 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) )
67 66 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) )
68 67 36 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐿 ‘ 𝑑 ) ∈ ( Base ‘ 𝑍 ) )
69 4 5 1 61 34 68 dchrabs2 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) ) ≤ 1 )
70 40 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( μ ‘ 𝑑 ) ∈ ℂ )
71 31 nncnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑑 ∈ ℂ )
72 31 nnne0d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑑 ≠ 0 )
73 70 71 72 absdivd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( μ ‘ 𝑑 ) / 𝑑 ) ) = ( ( abs ‘ ( μ ‘ 𝑑 ) ) / ( abs ‘ 𝑑 ) ) )
74 31 nnrpd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑑 ∈ ℝ+ )
75 74 rprege0d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑑 ∈ ℝ ∧ 0 ≤ 𝑑 ) )
76 absid ⊢ ( ( 𝑑 ∈ ℝ ∧ 0 ≤ 𝑑 ) → ( abs ‘ 𝑑 ) = 𝑑 )
77 75 76 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ 𝑑 ) = 𝑑 )
78 77 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( μ ‘ 𝑑 ) ) / ( abs ‘ 𝑑 ) ) = ( ( abs ‘ ( μ ‘ 𝑑 ) ) / 𝑑 ) )
79 73 78 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( μ ‘ 𝑑 ) / 𝑑 ) ) = ( ( abs ‘ ( μ ‘ 𝑑 ) ) / 𝑑 ) )
80 70 abscld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( μ ‘ 𝑑 ) ) ∈ ℝ )
81 mule1 ⊢ ( 𝑑 ∈ ℕ → ( abs ‘ ( μ ‘ 𝑑 ) ) ≤ 1 )
82 31 81 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( μ ‘ 𝑑 ) ) ≤ 1 )
83 80 57 74 82 lediv1dd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( μ ‘ 𝑑 ) ) / 𝑑 ) ≤ ( 1 / 𝑑 ) )
84 79 83 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( μ ‘ 𝑑 ) / 𝑑 ) ) ≤ ( 1 / 𝑑 ) )
85 56 57 58 53 59 60 69 84 lemul12ad ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) ) · ( abs ‘ ( ( μ ‘ 𝑑 ) / 𝑑 ) ) ) ≤ ( 1 · ( 1 / 𝑑 ) ) )
86 53 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 / 𝑑 ) ∈ ℂ )
87 86 mulid2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 · ( 1 / 𝑑 ) ) = ( 1 / 𝑑 ) )
88 85 87 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) ) · ( abs ‘ ( ( μ ‘ 𝑑 ) / 𝑑 ) ) ) ≤ ( 1 / 𝑑 ) )
89 55 88 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) ) ≤ ( 1 / 𝑑 ) )
90 52 53 30 54 89 lemul1ad ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) ) · ( abs ‘ ( 𝐾 − 𝑇 ) ) ) ≤ ( ( 1 / 𝑑 ) · ( abs ‘ ( 𝐾 − 𝑇 ) ) ) )
91 43 29 absmuld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( 𝐾 − 𝑇 ) ) ) = ( ( abs ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) ) · ( abs ‘ ( 𝐾 − 𝑇 ) ) ) )
92 30 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( 𝐾 − 𝑇 ) ) ∈ ℂ )
93 92 71 72 divrec2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( 𝐾 − 𝑇 ) ) / 𝑑 ) = ( ( 1 / 𝑑 ) · ( abs ‘ ( 𝐾 − 𝑇 ) ) ) )
94 90 91 93 3brtr4d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( 𝐾 − 𝑇 ) ) ) ≤ ( ( abs ‘ ( 𝐾 − 𝑇 ) ) / 𝑑 ) )
95 18 49 32 94 fsumle ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( 𝐾 − 𝑇 ) ) ) ≤ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝐾 − 𝑇 ) ) / 𝑑 ) )
96 46 50 33 51 95 letrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( abs ‘ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( 𝐾 − 𝑇 ) ) ) ≤ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝐾 − 𝑇 ) ) / 𝑑 ) )
97 33 leabsd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝐾 − 𝑇 ) ) / 𝑑 ) ≤ ( abs ‘ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝐾 − 𝑇 ) ) / 𝑑 ) ) )
98 46 33 48 96 97 letrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( abs ‘ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( 𝐾 − 𝑇 ) ) ) ≤ ( abs ‘ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝐾 − 𝑇 ) ) / 𝑑 ) ) )
99 98 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( 𝐾 − 𝑇 ) ) ) ≤ ( abs ‘ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝐾 − 𝑇 ) ) / 𝑑 ) ) )
100 16 17 33 45 99 o1le ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( 𝐾 − 𝑇 ) ) ) ∈ 𝑂(1) )