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 ffvelrnda ⊒ ( ( πœ‘ ∧ π‘š ∈ β„• ) β†’ ( 𝐹 β€˜ π‘š ) ∈ β„‚ )
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 mulid2d ⊒ ( ( ( πœ‘ ∧ ( π‘₯ ∈ ℝ+ ∧ 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 ffvelrnd ⊒ ( ( ( πœ‘ ∧ ( π‘₯ ∈ ℝ+ ∧ 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 ffvelrn ⊒ ( ( 𝐿 : β„€ ⟢ ( 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 mulid2d ⊒ ( ( ( πœ‘ ∧ ( π‘₯ ∈ ℝ+ ∧ 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) )