This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dchrmusum2

Description: The sum of the Möbius function multiplied by a non-principal Dirichlet character, divided by n , is bounded, provided that T =/= 0 . Lemma 9.4.2 of Shapiro, p. 380. (Contributed by Mario Carneiro, 4-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 )
dchrisumn0.f ⊢ 𝐹 = ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) )
dchrisumn0.c ⊢ ( 𝜑 → 𝐶 ∈ ( 0 [,) +∞ ) )
dchrisumn0.t ⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) ⇝ 𝑇 )
dchrisumn0.1 ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑇 ) ) ≤ ( 𝐶 / 𝑦 ) )
Assertion dchrmusum2 ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑑 ∈ ( 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 dchrisumn0.f ⊢ 𝐹 = ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) )
10 dchrisumn0.c ⊢ ( 𝜑 → 𝐶 ∈ ( 0 [,) +∞ ) )
11 dchrisumn0.t ⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) ⇝ 𝑇 )
12 dchrisumn0.1 ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑇 ) ) ≤ ( 𝐶 / 𝑦 ) )
13 rpssre ⊢ ℝ+ ⊆ ℝ
14 ax-1cn ⊢ 1 ∈ ℂ
15 o1const ⊢ ( ( ℝ+ ⊆ ℝ ∧ 1 ∈ ℂ ) → ( 𝑥 ∈ ℝ+ ↦ 1 ) ∈ 𝑂(1) )
16 13 14 15 mp2an ⊢ ( 𝑥 ∈ ℝ+ ↦ 1 ) ∈ 𝑂(1)
17 16 a1i ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ 1 ) ∈ 𝑂(1) )
18 14 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 1 ∈ ℂ )
19 fzfid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
20 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑋 ∈ 𝐷 )
21 elfzelz ⊢ ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑑 ∈ ℤ )
22 21 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑑 ∈ ℤ )
23 4 1 5 2 20 22 dchrzrhcl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) ∈ ℂ )
24 elfznn ⊢ ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑑 ∈ ℕ )
25 24 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑑 ∈ ℕ )
26 mucl ⊢ ( 𝑑 ∈ ℕ → ( μ ‘ 𝑑 ) ∈ ℤ )
27 26 zred ⊢ ( 𝑑 ∈ ℕ → ( μ ‘ 𝑑 ) ∈ ℝ )
28 nndivre ⊢ ( ( ( μ ‘ 𝑑 ) ∈ ℝ ∧ 𝑑 ∈ ℕ ) → ( ( μ ‘ 𝑑 ) / 𝑑 ) ∈ ℝ )
29 27 28 mpancom ⊢ ( 𝑑 ∈ ℕ → ( ( μ ‘ 𝑑 ) / 𝑑 ) ∈ ℝ )
30 25 29 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( μ ‘ 𝑑 ) / 𝑑 ) ∈ ℝ )
31 30 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( μ ‘ 𝑑 ) / 𝑑 ) ∈ ℂ )
32 23 31 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) ∈ ℂ )
33 19 32 fsumcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) ∈ ℂ )
34 climcl ⊢ ( seq 1 ( + , 𝐹 ) ⇝ 𝑇 → 𝑇 ∈ ℂ )
35 11 34 syl ⊢ ( 𝜑 → 𝑇 ∈ ℂ )
36 35 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑇 ∈ ℂ )
37 33 36 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · 𝑇 ) ∈ ℂ )
38 13 a1i ⊢ ( 𝜑 → ℝ+ ⊆ ℝ )
39 subcl ⊢ ( ( 1 ∈ ℂ ∧ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · 𝑇 ) ∈ ℂ ) → ( 1 − ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · 𝑇 ) ) ∈ ℂ )
40 14 37 39 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 1 − ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · 𝑇 ) ) ∈ ℂ )
41 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
42 elrege0 ⊢ ( 𝐶 ∈ ( 0 [,) +∞ ) ↔ ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) )
43 10 42 sylib ⊢ ( 𝜑 → ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) )
44 43 simpld ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
45 fzfid ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
46 32 adantlrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) ∈ ℂ )
47 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
48 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
49 7 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝑋 ∈ 𝐷 )
50 nnz ⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℤ )
51 50 adantl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℤ )
52 4 1 5 2 49 51 dchrzrhcl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ∈ ℂ )
53 nncn ⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℂ )
54 53 adantl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℂ )
55 nnne0 ⊢ ( 𝑚 ∈ ℕ → 𝑚 ≠ 0 )
56 55 adantl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → 𝑚 ≠ 0 )
57 52 54 56 divcld ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ∈ ℂ )
58 2fveq3 ⊢ ( 𝑎 = 𝑚 → ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) = ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) )
59 id ⊢ ( 𝑎 = 𝑚 → 𝑎 = 𝑚 )
60 58 59 oveq12d ⊢ ( 𝑎 = 𝑚 → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) )
61 60 cbvmptv ⊢ ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) ) = ( 𝑚 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) )
62 9 61 eqtri ⊢ 𝐹 = ( 𝑚 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) )
63 57 62 fmptd ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ℂ )
64 63 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐹 ‘ 𝑚 ) ∈ ℂ )
65 47 48 64 serf ⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) : ℕ ⟶ ℂ )
66 65 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → seq 1 ( + , 𝐹 ) : ℕ ⟶ ℂ )
67 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 𝑥 ∈ ℝ+ )
68 67 rpred ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 𝑥 ∈ ℝ )
69 nndivre ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑑 ∈ ℕ ) → ( 𝑥 / 𝑑 ) ∈ ℝ )
70 68 24 69 syl2an ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑑 ) ∈ ℝ )
71 24 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑑 ∈ ℕ )
72 71 nncnd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑑 ∈ ℂ )
73 72 mullidd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 · 𝑑 ) = 𝑑 )
74 fznnfl ⊢ ( 𝑥 ∈ ℝ → ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ↔ ( 𝑑 ∈ ℕ ∧ 𝑑 ≤ 𝑥 ) ) )
75 68 74 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ↔ ( 𝑑 ∈ ℕ ∧ 𝑑 ≤ 𝑥 ) ) )
76 75 simplbda ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑑 ≤ 𝑥 )
77 73 76 eqbrtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 · 𝑑 ) ≤ 𝑥 )
78 1red ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 1 ∈ ℝ )
79 68 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ℝ )
80 71 nnrpd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑑 ∈ ℝ+ )
81 78 79 80 lemuldivd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 1 · 𝑑 ) ≤ 𝑥 ↔ 1 ≤ ( 𝑥 / 𝑑 ) ) )
82 77 81 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 1 ≤ ( 𝑥 / 𝑑 ) )
83 flge1nn ⊢ ( ( ( 𝑥 / 𝑑 ) ∈ ℝ ∧ 1 ≤ ( 𝑥 / 𝑑 ) ) → ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ∈ ℕ )
84 70 82 83 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ∈ ℕ )
85 66 84 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ∈ ℂ )
86 46 85 mulcld ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) ∈ ℂ )
87 35 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑇 ∈ ℂ )
88 46 87 mulcld ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · 𝑇 ) ∈ ℂ )
89 45 86 88 fsumsub ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) − ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · 𝑇 ) ) = ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) − Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · 𝑇 ) ) )
90 46 85 87 subdid ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) − 𝑇 ) ) = ( ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) − ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · 𝑇 ) ) )
91 90 sumeq2dv ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) − 𝑇 ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) − ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · 𝑇 ) ) )
92 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → 𝑋 ∈ 𝐷 )
93 21 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → 𝑑 ∈ ℤ )
94 elfzelz ⊢ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) → 𝑚 ∈ ℤ )
95 94 adantl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → 𝑚 ∈ ℤ )
96 4 1 5 2 92 93 95 dchrzrhmul ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ) )
97 96 oveq1d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) / ( 𝑑 · 𝑚 ) ) = ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ) / ( 𝑑 · 𝑚 ) ) )
98 23 adantlrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) ∈ ℂ )
99 98 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) ∈ ℂ )
100 72 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → 𝑑 ∈ ℂ )
101 4 1 5 2 92 95 dchrzrhcl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ∈ ℂ )
102 elfznn ⊢ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) → 𝑚 ∈ ℕ )
103 102 adantl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → 𝑚 ∈ ℕ )
104 103 nncnd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → 𝑚 ∈ ℂ )
105 71 nnne0d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑑 ≠ 0 )
106 105 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → 𝑑 ≠ 0 )
107 103 nnne0d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → 𝑚 ≠ 0 )
108 99 100 101 104 106 107 divmuldivd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) / 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) = ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ) / ( 𝑑 · 𝑚 ) ) )
109 97 108 eqtr4d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) / ( 𝑑 · 𝑚 ) ) = ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) / 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) )
110 109 oveq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → ( ( μ ‘ 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) / ( 𝑑 · 𝑚 ) ) ) = ( ( μ ‘ 𝑑 ) · ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) / 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) )
111 71 26 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( μ ‘ 𝑑 ) ∈ ℤ )
112 111 zcnd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( μ ‘ 𝑑 ) ∈ ℂ )
113 112 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → ( μ ‘ 𝑑 ) ∈ ℂ )
114 99 100 106 divcld ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) / 𝑑 ) ∈ ℂ )
115 101 104 107 divcld ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ∈ ℂ )
116 113 114 115 mulassd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → ( ( ( μ ‘ 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) / 𝑑 ) ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) = ( ( μ ‘ 𝑑 ) · ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) / 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) ) )
117 113 99 100 106 div12d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → ( ( μ ‘ 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) / 𝑑 ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) )
118 117 oveq1d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → ( ( ( μ ‘ 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) / 𝑑 ) ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) = ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) )
119 110 116 118 3eqtr2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → ( ( μ ‘ 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) / ( 𝑑 · 𝑚 ) ) ) = ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) )
120 119 sumeq2dv ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( μ ‘ 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) / ( 𝑑 · 𝑚 ) ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) )
121 fzfid ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ∈ Fin )
122 simpll ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝜑 )
123 122 102 57 syl2an ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ∈ ℂ )
124 121 46 123 fsummulc2 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) )
125 ovex ⊢ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ∈ V
126 60 9 125 fvmpt ⊢ ( 𝑚 ∈ ℕ → ( 𝐹 ‘ 𝑚 ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) )
127 103 126 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → ( 𝐹 ‘ 𝑚 ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) )
128 84 47 eleqtrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ∈ ( ℤ≥ ‘ 1 ) )
129 127 128 123 fsumser ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) = ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) )
130 129 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) / 𝑚 ) ) = ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) )
131 120 124 130 3eqtr2rd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( μ ‘ 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) / ( 𝑑 · 𝑚 ) ) ) )
132 131 sumeq2dv ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( μ ‘ 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) / ( 𝑑 · 𝑚 ) ) ) )
133 2fveq3 ⊢ ( 𝑛 = ( 𝑑 · 𝑚 ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) )
134 id ⊢ ( 𝑛 = ( 𝑑 · 𝑚 ) → 𝑛 = ( 𝑑 · 𝑚 ) )
135 133 134 oveq12d ⊢ ( 𝑛 = ( 𝑑 · 𝑚 ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) / 𝑛 ) = ( ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) / ( 𝑑 · 𝑚 ) ) )
136 135 oveq2d ⊢ ( 𝑛 = ( 𝑑 · 𝑚 ) → ( ( μ ‘ 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) / 𝑛 ) ) = ( ( μ ‘ 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) / ( 𝑑 · 𝑚 ) ) ) )
137 elrabi ⊢ ( 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } → 𝑑 ∈ ℕ )
138 137 ad2antll ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) ) → 𝑑 ∈ ℕ )
139 138 26 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) ) → ( μ ‘ 𝑑 ) ∈ ℤ )
140 139 zcnd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) ) → ( μ ‘ 𝑑 ) ∈ ℂ )
141 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑋 ∈ 𝐷 )
142 elfzelz ⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℤ )
143 142 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℤ )
144 4 1 5 2 141 143 dchrzrhcl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ∈ ℂ )
145 fz1ssnn ⊢ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ⊆ ℕ
146 145 a1i ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ⊆ ℕ )
147 146 sselda ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℕ )
148 147 nncnd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℂ )
149 147 nnne0d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ≠ 0 )
150 144 148 149 divcld ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) / 𝑛 ) ∈ ℂ )
151 150 adantrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) / 𝑛 ) ∈ ℂ )
152 140 151 mulcld ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) ) → ( ( μ ‘ 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) / 𝑛 ) ) ∈ ℂ )
153 136 68 152 dvdsflsumcom ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( μ ‘ 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) / 𝑛 ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( μ ‘ 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) / ( 𝑑 · 𝑚 ) ) ) )
154 2fveq3 ⊢ ( 𝑛 = 1 → ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = ( 𝑋 ‘ ( 𝐿 ‘ 1 ) ) )
155 id ⊢ ( 𝑛 = 1 → 𝑛 = 1 )
156 154 155 oveq12d ⊢ ( 𝑛 = 1 → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) / 𝑛 ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 1 ) ) / 1 ) )
157 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 1 ≤ 𝑥 )
158 flge1nn ⊢ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) → ( ⌊ ‘ 𝑥 ) ∈ ℕ )
159 68 157 158 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ⌊ ‘ 𝑥 ) ∈ ℕ )
160 159 47 eleqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ⌊ ‘ 𝑥 ) ∈ ( ℤ≥ ‘ 1 ) )
161 eluzfz1 ⊢ ( ( ⌊ ‘ 𝑥 ) ∈ ( ℤ≥ ‘ 1 ) → 1 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) )
162 160 161 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 1 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) )
163 156 45 146 162 150 musumsum ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( μ ‘ 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) / 𝑛 ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 1 ) ) / 1 ) )
164 132 153 163 3eqtr2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 1 ) ) / 1 ) )
165 4 1 5 2 7 dchrzrh1 ⊢ ( 𝜑 → ( 𝑋 ‘ ( 𝐿 ‘ 1 ) ) = 1 )
166 165 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 1 ) ) = 1 )
167 166 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 1 ) ) / 1 ) = ( 1 / 1 ) )
168 1div1e1 ⊢ ( 1 / 1 ) = 1
169 167 168 eqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 1 ) ) / 1 ) = 1 )
170 164 169 eqtr2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 1 = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) )
171 35 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 𝑇 ∈ ℂ )
172 45 171 46 fsummulc1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · 𝑇 ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · 𝑇 ) )
173 170 172 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 1 − ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · 𝑇 ) ) = ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) − Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · 𝑇 ) ) )
174 89 91 173 3eqtr4rd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 1 − ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · 𝑇 ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) − 𝑇 ) ) )
175 174 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ ( 1 − ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · 𝑇 ) ) ) = ( abs ‘ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) − 𝑇 ) ) ) )
176 85 87 subcld ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) − 𝑇 ) ∈ ℂ )
177 46 176 mulcld ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) − 𝑇 ) ) ∈ ℂ )
178 45 177 fsumcl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) − 𝑇 ) ) ∈ ℂ )
179 178 abscld ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) − 𝑇 ) ) ) ∈ ℝ )
180 177 abscld ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) − 𝑇 ) ) ) ∈ ℝ )
181 45 180 fsumrecl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) − 𝑇 ) ) ) ∈ ℝ )
182 44 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 𝐶 ∈ ℝ )
183 45 177 fsumabs ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) − 𝑇 ) ) ) ≤ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) − 𝑇 ) ) ) )
184 reflcl ⊢ ( 𝑥 ∈ ℝ → ( ⌊ ‘ 𝑥 ) ∈ ℝ )
185 68 184 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ⌊ ‘ 𝑥 ) ∈ ℝ )
186 185 182 remulcld ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( ⌊ ‘ 𝑥 ) · 𝐶 ) ∈ ℝ )
187 186 67 rerpdivcld ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( ( ⌊ ‘ 𝑥 ) · 𝐶 ) / 𝑥 ) ∈ ℝ )
188 182 67 rerpdivcld ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 𝐶 / 𝑥 ) ∈ ℝ )
189 188 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐶 / 𝑥 ) ∈ ℝ )
190 46 abscld ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) ) ∈ ℝ )
191 71 nnrecred ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 / 𝑑 ) ∈ ℝ )
192 176 abscld ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) − 𝑇 ) ) ∈ ℝ )
193 80 rpred ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑑 ∈ ℝ )
194 189 193 remulcld ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝐶 / 𝑥 ) · 𝑑 ) ∈ ℝ )
195 46 absge0d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( abs ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) ) )
196 176 absge0d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) − 𝑇 ) ) )
197 98 abscld ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) ) ∈ ℝ )
198 31 adantlrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( μ ‘ 𝑑 ) / 𝑑 ) ∈ ℂ )
199 198 abscld ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( μ ‘ 𝑑 ) / 𝑑 ) ) ∈ ℝ )
200 98 absge0d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) ) )
201 198 absge0d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( abs ‘ ( ( μ ‘ 𝑑 ) / 𝑑 ) ) )
202 eqid ⊢ ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 )
203 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑋 ∈ 𝐷 )
204 3 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
205 1 202 2 znzrhfo ⊢ ( 𝑁 ∈ ℕ0 → 𝐿 : ℤ –onto→ ( Base ‘ 𝑍 ) )
206 fof ⊢ ( 𝐿 : ℤ –onto→ ( Base ‘ 𝑍 ) → 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) )
207 204 205 206 3syl ⊢ ( 𝜑 → 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) )
208 207 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) )
209 ffvelcdm ⊢ ( ( 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) ∧ 𝑑 ∈ ℤ ) → ( 𝐿 ‘ 𝑑 ) ∈ ( Base ‘ 𝑍 ) )
210 208 21 209 syl2an ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐿 ‘ 𝑑 ) ∈ ( Base ‘ 𝑍 ) )
211 4 5 1 202 203 210 dchrabs2 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) ) ≤ 1 )
212 112 72 105 absdivd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( μ ‘ 𝑑 ) / 𝑑 ) ) = ( ( abs ‘ ( μ ‘ 𝑑 ) ) / ( abs ‘ 𝑑 ) ) )
213 80 rprege0d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑑 ∈ ℝ ∧ 0 ≤ 𝑑 ) )
214 absid ⊢ ( ( 𝑑 ∈ ℝ ∧ 0 ≤ 𝑑 ) → ( abs ‘ 𝑑 ) = 𝑑 )
215 213 214 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ 𝑑 ) = 𝑑 )
216 215 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( μ ‘ 𝑑 ) ) / ( abs ‘ 𝑑 ) ) = ( ( abs ‘ ( μ ‘ 𝑑 ) ) / 𝑑 ) )
217 212 216 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( μ ‘ 𝑑 ) / 𝑑 ) ) = ( ( abs ‘ ( μ ‘ 𝑑 ) ) / 𝑑 ) )
218 112 abscld ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( μ ‘ 𝑑 ) ) ∈ ℝ )
219 mule1 ⊢ ( 𝑑 ∈ ℕ → ( abs ‘ ( μ ‘ 𝑑 ) ) ≤ 1 )
220 71 219 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( μ ‘ 𝑑 ) ) ≤ 1 )
221 218 78 80 220 lediv1dd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( μ ‘ 𝑑 ) ) / 𝑑 ) ≤ ( 1 / 𝑑 ) )
222 217 221 eqbrtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( μ ‘ 𝑑 ) / 𝑑 ) ) ≤ ( 1 / 𝑑 ) )
223 197 78 199 191 200 201 211 222 lemul12ad ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) ) · ( abs ‘ ( ( μ ‘ 𝑑 ) / 𝑑 ) ) ) ≤ ( 1 · ( 1 / 𝑑 ) ) )
224 98 198 absmuld ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) ) = ( ( abs ‘ ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) ) · ( abs ‘ ( ( μ ‘ 𝑑 ) / 𝑑 ) ) ) )
225 191 recnd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 / 𝑑 ) ∈ ℂ )
226 225 mullidd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 · ( 1 / 𝑑 ) ) = ( 1 / 𝑑 ) )
227 226 eqcomd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 / 𝑑 ) = ( 1 · ( 1 / 𝑑 ) ) )
228 223 224 227 3brtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) ) ≤ ( 1 / 𝑑 ) )
229 2fveq3 ⊢ ( 𝑦 = ( 𝑥 / 𝑑 ) → ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) = ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) )
230 229 fvoveq1d ⊢ ( 𝑦 = ( 𝑥 / 𝑑 ) → ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑇 ) ) = ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) − 𝑇 ) ) )
231 oveq2 ⊢ ( 𝑦 = ( 𝑥 / 𝑑 ) → ( 𝐶 / 𝑦 ) = ( 𝐶 / ( 𝑥 / 𝑑 ) ) )
232 230 231 breq12d ⊢ ( 𝑦 = ( 𝑥 / 𝑑 ) → ( ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑇 ) ) ≤ ( 𝐶 / 𝑦 ) ↔ ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) − 𝑇 ) ) ≤ ( 𝐶 / ( 𝑥 / 𝑑 ) ) ) )
233 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑇 ) ) ≤ ( 𝐶 / 𝑦 ) )
234 1re ⊢ 1 ∈ ℝ
235 elicopnf ⊢ ( 1 ∈ ℝ → ( ( 𝑥 / 𝑑 ) ∈ ( 1 [,) +∞ ) ↔ ( ( 𝑥 / 𝑑 ) ∈ ℝ ∧ 1 ≤ ( 𝑥 / 𝑑 ) ) ) )
236 234 235 ax-mp ⊢ ( ( 𝑥 / 𝑑 ) ∈ ( 1 [,) +∞ ) ↔ ( ( 𝑥 / 𝑑 ) ∈ ℝ ∧ 1 ≤ ( 𝑥 / 𝑑 ) ) )
237 70 82 236 sylanbrc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑑 ) ∈ ( 1 [,) +∞ ) )
238 232 233 237 rspcdva ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) − 𝑇 ) ) ≤ ( 𝐶 / ( 𝑥 / 𝑑 ) ) )
239 182 recnd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 𝐶 ∈ ℂ )
240 239 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝐶 ∈ ℂ )
241 rpcnne0 ⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) )
242 241 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) )
243 242 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) )
244 divdiv2 ⊢ ( ( 𝐶 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ∧ ( 𝑑 ∈ ℂ ∧ 𝑑 ≠ 0 ) ) → ( 𝐶 / ( 𝑥 / 𝑑 ) ) = ( ( 𝐶 · 𝑑 ) / 𝑥 ) )
245 240 243 72 105 244 syl112anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐶 / ( 𝑥 / 𝑑 ) ) = ( ( 𝐶 · 𝑑 ) / 𝑥 ) )
246 div23 ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝑑 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ) → ( ( 𝐶 · 𝑑 ) / 𝑥 ) = ( ( 𝐶 / 𝑥 ) · 𝑑 ) )
247 240 72 243 246 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝐶 · 𝑑 ) / 𝑥 ) = ( ( 𝐶 / 𝑥 ) · 𝑑 ) )
248 245 247 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐶 / ( 𝑥 / 𝑑 ) ) = ( ( 𝐶 / 𝑥 ) · 𝑑 ) )
249 238 248 breqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) − 𝑇 ) ) ≤ ( ( 𝐶 / 𝑥 ) · 𝑑 ) )
250 190 191 192 194 195 196 228 249 lemul12ad ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) ) · ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) − 𝑇 ) ) ) ≤ ( ( 1 / 𝑑 ) · ( ( 𝐶 / 𝑥 ) · 𝑑 ) ) )
251 46 176 absmuld ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) − 𝑇 ) ) ) = ( ( abs ‘ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) ) · ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) − 𝑇 ) ) ) )
252 188 recnd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 𝐶 / 𝑥 ) ∈ ℂ )
253 252 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐶 / 𝑥 ) ∈ ℂ )
254 253 72 105 divcan4d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝐶 / 𝑥 ) · 𝑑 ) / 𝑑 ) = ( 𝐶 / 𝑥 ) )
255 253 72 mulcld ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝐶 / 𝑥 ) · 𝑑 ) ∈ ℂ )
256 255 72 105 divrec2d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝐶 / 𝑥 ) · 𝑑 ) / 𝑑 ) = ( ( 1 / 𝑑 ) · ( ( 𝐶 / 𝑥 ) · 𝑑 ) ) )
257 254 256 eqtr3d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐶 / 𝑥 ) = ( ( 1 / 𝑑 ) · ( ( 𝐶 / 𝑥 ) · 𝑑 ) ) )
258 250 251 257 3brtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) − 𝑇 ) ) ) ≤ ( 𝐶 / 𝑥 ) )
259 45 180 189 258 fsumle ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) − 𝑇 ) ) ) ≤ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝐶 / 𝑥 ) )
260 159 nnnn0d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ⌊ ‘ 𝑥 ) ∈ ℕ0 )
261 hashfz1 ⊢ ( ( ⌊ ‘ 𝑥 ) ∈ ℕ0 → ( ♯ ‘ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) = ( ⌊ ‘ 𝑥 ) )
262 260 261 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ♯ ‘ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) = ( ⌊ ‘ 𝑥 ) )
263 262 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( ♯ ‘ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) · ( 𝐶 / 𝑥 ) ) = ( ( ⌊ ‘ 𝑥 ) · ( 𝐶 / 𝑥 ) ) )
264 fsumconst ⊢ ( ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin ∧ ( 𝐶 / 𝑥 ) ∈ ℂ ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝐶 / 𝑥 ) = ( ( ♯ ‘ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) · ( 𝐶 / 𝑥 ) ) )
265 45 252 264 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝐶 / 𝑥 ) = ( ( ♯ ‘ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) · ( 𝐶 / 𝑥 ) ) )
266 159 nncnd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ⌊ ‘ 𝑥 ) ∈ ℂ )
267 divass ⊢ ( ( ( ⌊ ‘ 𝑥 ) ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ) → ( ( ( ⌊ ‘ 𝑥 ) · 𝐶 ) / 𝑥 ) = ( ( ⌊ ‘ 𝑥 ) · ( 𝐶 / 𝑥 ) ) )
268 266 239 242 267 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( ( ⌊ ‘ 𝑥 ) · 𝐶 ) / 𝑥 ) = ( ( ⌊ ‘ 𝑥 ) · ( 𝐶 / 𝑥 ) ) )
269 263 265 268 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝐶 / 𝑥 ) = ( ( ( ⌊ ‘ 𝑥 ) · 𝐶 ) / 𝑥 ) )
270 259 269 breqtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) − 𝑇 ) ) ) ≤ ( ( ( ⌊ ‘ 𝑥 ) · 𝐶 ) / 𝑥 ) )
271 43 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) )
272 flle ⊢ ( 𝑥 ∈ ℝ → ( ⌊ ‘ 𝑥 ) ≤ 𝑥 )
273 68 272 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ⌊ ‘ 𝑥 ) ≤ 𝑥 )
274 lemul1a ⊢ ( ( ( ( ⌊ ‘ 𝑥 ) ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ) ∧ ( ⌊ ‘ 𝑥 ) ≤ 𝑥 ) → ( ( ⌊ ‘ 𝑥 ) · 𝐶 ) ≤ ( 𝑥 · 𝐶 ) )
275 185 68 271 273 274 syl31anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( ⌊ ‘ 𝑥 ) · 𝐶 ) ≤ ( 𝑥 · 𝐶 ) )
276 186 182 67 ledivmuld ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( ( ( ⌊ ‘ 𝑥 ) · 𝐶 ) / 𝑥 ) ≤ 𝐶 ↔ ( ( ⌊ ‘ 𝑥 ) · 𝐶 ) ≤ ( 𝑥 · 𝐶 ) ) )
277 275 276 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( ( ⌊ ‘ 𝑥 ) · 𝐶 ) / 𝑥 ) ≤ 𝐶 )
278 181 187 182 270 277 letrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) − 𝑇 ) ) ) ≤ 𝐶 )
279 179 181 182 183 278 letrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) − 𝑇 ) ) ) ≤ 𝐶 )
280 175 279 eqbrtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ ( 1 − ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · 𝑇 ) ) ) ≤ 𝐶 )
281 38 40 41 44 280 elo1d ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( 1 − ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · 𝑇 ) ) ) ∈ 𝑂(1) )
282 18 37 281 o1dif ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℝ+ ↦ 1 ) ∈ 𝑂(1) ↔ ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · 𝑇 ) ) ∈ 𝑂(1) ) )
283 17 282 mpbid ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · 𝑇 ) ) ∈ 𝑂(1) )