Metamath Proof Explorer

Theorem dchrvmasumiflem2

Description: Lemma for dchrvmasum . (Contributed by Mario Carneiro, 5-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 )
dchrvmasumif.f ⊒ 𝐹 = ( π‘Ž ∈ β„• ↦ ( ( 𝑋 β€˜ ( 𝐿 β€˜ π‘Ž ) ) / π‘Ž ) )
dchrvmasumif.c ⊒ ( πœ‘ β†’ 𝐢 ∈ ( 0 [,) +∞ ) )
dchrvmasumif.s ⊒ ( πœ‘ β†’ seq 1 ( + , 𝐹 ) ⇝ 𝑆 )
dchrvmasumif.1 ⊒ ( πœ‘ β†’ βˆ€ 𝑦 ∈ ( 1 [,) +∞ ) ( abs β€˜ ( ( seq 1 ( + , 𝐹 ) β€˜ ( ⌊ β€˜ 𝑦 ) ) βˆ’ 𝑆 ) ) ≀ ( 𝐢 / 𝑦 ) )
dchrvmasumif.g ⊒ 𝐾 = ( π‘Ž ∈ β„• ↦ ( ( 𝑋 β€˜ ( 𝐿 β€˜ π‘Ž ) ) Β· ( ( log β€˜ π‘Ž ) / π‘Ž ) ) )
dchrvmasumif.e ⊒ ( πœ‘ β†’ 𝐸 ∈ ( 0 [,) +∞ ) )
dchrvmasumif.t ⊒ ( πœ‘ β†’ seq 1 ( + , 𝐾 ) ⇝ 𝑇 )
dchrvmasumif.2 ⊒ ( πœ‘ β†’ βˆ€ 𝑦 ∈ ( 3 [,) +∞ ) ( abs β€˜ ( ( seq 1 ( + , 𝐾 ) β€˜ ( ⌊ β€˜ 𝑦 ) ) βˆ’ 𝑇 ) ) ≀ ( 𝐸 Β· ( ( log β€˜ 𝑦 ) / 𝑦 ) ) )
Assertion dchrvmasumiflem2 ( πœ‘ β†’ ( π‘₯ ∈ ℝ+ ↦ ( Ξ£ 𝑛 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑛 ) ) Β· ( ( Ξ› β€˜ 𝑛 ) / 𝑛 ) ) + if ( 𝑆 = 0 , ( log β€˜ π‘₯ ) , 0 ) ) ) ∈ 𝑂(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 dchrvmasumif.f ⊒ 𝐹 = ( π‘Ž ∈ β„• ↦ ( ( 𝑋 β€˜ ( 𝐿 β€˜ π‘Ž ) ) / π‘Ž ) )
10 dchrvmasumif.c ⊒ ( πœ‘ β†’ 𝐢 ∈ ( 0 [,) +∞ ) )
11 dchrvmasumif.s ⊒ ( πœ‘ β†’ seq 1 ( + , 𝐹 ) ⇝ 𝑆 )
12 dchrvmasumif.1 ⊒ ( πœ‘ β†’ βˆ€ 𝑦 ∈ ( 1 [,) +∞ ) ( abs β€˜ ( ( seq 1 ( + , 𝐹 ) β€˜ ( ⌊ β€˜ 𝑦 ) ) βˆ’ 𝑆 ) ) ≀ ( 𝐢 / 𝑦 ) )
13 dchrvmasumif.g ⊒ 𝐾 = ( π‘Ž ∈ β„• ↦ ( ( 𝑋 β€˜ ( 𝐿 β€˜ π‘Ž ) ) Β· ( ( log β€˜ π‘Ž ) / π‘Ž ) ) )
14 dchrvmasumif.e ⊒ ( πœ‘ β†’ 𝐸 ∈ ( 0 [,) +∞ ) )
15 dchrvmasumif.t ⊒ ( πœ‘ β†’ seq 1 ( + , 𝐾 ) ⇝ 𝑇 )
16 dchrvmasumif.2 ⊒ ( πœ‘ β†’ βˆ€ 𝑦 ∈ ( 3 [,) +∞ ) ( abs β€˜ ( ( seq 1 ( + , 𝐾 ) β€˜ ( ⌊ β€˜ 𝑦 ) ) βˆ’ 𝑇 ) ) ≀ ( 𝐸 Β· ( ( log β€˜ 𝑦 ) / 𝑦 ) ) )
17 1red ⊒ ( πœ‘ β†’ 1 ∈ ℝ )
18 fzfid ⊒ ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) β†’ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ∈ Fin )
19 7 ad2antrr ⊒ ( ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ) β†’ 𝑋 ∈ 𝐷 )
20 elfzelz ⊒ ( 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) β†’ 𝑑 ∈ β„€ )
21 20 adantl ⊒ ( ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ) β†’ 𝑑 ∈ β„€ )
22 4 1 5 2 19 21 dchrzrhcl ⊒ ( ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ) β†’ ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑑 ) ) ∈ β„‚ )
23 elfznn ⊒ ( 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) β†’ 𝑑 ∈ β„• )
24 23 adantl ⊒ ( ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ) β†’ 𝑑 ∈ β„• )
25 mucl ⊒ ( 𝑑 ∈ β„• β†’ ( ΞΌ β€˜ 𝑑 ) ∈ β„€ )
26 24 25 syl ⊒ ( ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ) β†’ ( ΞΌ β€˜ 𝑑 ) ∈ β„€ )
27 26 zred ⊒ ( ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ) β†’ ( ΞΌ β€˜ 𝑑 ) ∈ ℝ )
28 27 24 nndivred ⊒ ( ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ) β†’ ( ( ΞΌ β€˜ 𝑑 ) / 𝑑 ) ∈ ℝ )
29 28 recnd ⊒ ( ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ) β†’ ( ( ΞΌ β€˜ 𝑑 ) / 𝑑 ) ∈ β„‚ )
30 22 29 mulcld ⊒ ( ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ) β†’ ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑑 ) ) Β· ( ( ΞΌ β€˜ 𝑑 ) / 𝑑 ) ) ∈ β„‚ )
31 18 30 fsumcl ⊒ ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) β†’ Ξ£ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑑 ) ) Β· ( ( ΞΌ β€˜ 𝑑 ) / 𝑑 ) ) ∈ β„‚ )
32 climcl ⊒ ( seq 1 ( + , 𝐹 ) ⇝ 𝑆 β†’ 𝑆 ∈ β„‚ )
33 11 32 syl ⊒ ( πœ‘ β†’ 𝑆 ∈ β„‚ )
34 33 adantr ⊒ ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) β†’ 𝑆 ∈ β„‚ )
35 31 34 mulcld ⊒ ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) β†’ ( Ξ£ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑑 ) ) Β· ( ( ΞΌ β€˜ 𝑑 ) / 𝑑 ) ) Β· 𝑆 ) ∈ β„‚ )
36 0cnd ⊒ ( ( πœ‘ ∧ 𝑆 = 0 ) β†’ 0 ∈ β„‚ )
37 df-ne ⊒ ( 𝑆 β‰  0 ↔ Β¬ 𝑆 = 0 )
38 climcl ⊒ ( seq 1 ( + , 𝐾 ) ⇝ 𝑇 β†’ 𝑇 ∈ β„‚ )
39 15 38 syl ⊒ ( πœ‘ β†’ 𝑇 ∈ β„‚ )
40 39 adantr ⊒ ( ( πœ‘ ∧ 𝑆 β‰  0 ) β†’ 𝑇 ∈ β„‚ )
41 33 adantr ⊒ ( ( πœ‘ ∧ 𝑆 β‰  0 ) β†’ 𝑆 ∈ β„‚ )
42 simpr ⊒ ( ( πœ‘ ∧ 𝑆 β‰  0 ) β†’ 𝑆 β‰  0 )
43 40 41 42 divcld ⊒ ( ( πœ‘ ∧ 𝑆 β‰  0 ) β†’ ( 𝑇 / 𝑆 ) ∈ β„‚ )
44 37 43 sylan2br ⊒ ( ( πœ‘ ∧ Β¬ 𝑆 = 0 ) β†’ ( 𝑇 / 𝑆 ) ∈ β„‚ )
45 36 44 ifclda ⊒ ( πœ‘ β†’ if ( 𝑆 = 0 , 0 , ( 𝑇 / 𝑆 ) ) ∈ β„‚ )
46 45 adantr ⊒ ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) β†’ if ( 𝑆 = 0 , 0 , ( 𝑇 / 𝑆 ) ) ∈ β„‚ )
47 1 2 3 4 5 6 7 8 9 10 11 12 dchrmusum2 ⊒ ( πœ‘ β†’ ( π‘₯ ∈ ℝ+ ↦ ( Ξ£ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑑 ) ) Β· ( ( ΞΌ β€˜ 𝑑 ) / 𝑑 ) ) Β· 𝑆 ) ) ∈ 𝑂(1) )
48 rpssre ⊒ ℝ+ βŠ† ℝ
49 o1const ⊒ ( ( ℝ+ βŠ† ℝ ∧ if ( 𝑆 = 0 , 0 , ( 𝑇 / 𝑆 ) ) ∈ β„‚ ) β†’ ( π‘₯ ∈ ℝ+ ↦ if ( 𝑆 = 0 , 0 , ( 𝑇 / 𝑆 ) ) ) ∈ 𝑂(1) )
50 48 45 49 sylancr ⊒ ( πœ‘ β†’ ( π‘₯ ∈ ℝ+ ↦ if ( 𝑆 = 0 , 0 , ( 𝑇 / 𝑆 ) ) ) ∈ 𝑂(1) )
51 35 46 47 50 o1mul2 ⊒ ( πœ‘ β†’ ( π‘₯ ∈ ℝ+ ↦ ( ( Ξ£ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑑 ) ) Β· ( ( ΞΌ β€˜ 𝑑 ) / 𝑑 ) ) Β· 𝑆 ) Β· if ( 𝑆 = 0 , 0 , ( 𝑇 / 𝑆 ) ) ) ) ∈ 𝑂(1) )
52 fzfid ⊒ ( ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ) β†’ ( 1 ... ( ⌊ β€˜ ( π‘₯ / 𝑑 ) ) ) ∈ Fin )
53 19 adantr ⊒ ( ( ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ) ∧ π‘˜ ∈ ( 1 ... ( ⌊ β€˜ ( π‘₯ / 𝑑 ) ) ) ) β†’ 𝑋 ∈ 𝐷 )
54 elfzelz ⊒ ( π‘˜ ∈ ( 1 ... ( ⌊ β€˜ ( π‘₯ / 𝑑 ) ) ) β†’ π‘˜ ∈ β„€ )
55 54 adantl ⊒ ( ( ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ) ∧ π‘˜ ∈ ( 1 ... ( ⌊ β€˜ ( π‘₯ / 𝑑 ) ) ) ) β†’ π‘˜ ∈ β„€ )
56 4 1 5 2 53 55 dchrzrhcl ⊒ ( ( ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ) ∧ π‘˜ ∈ ( 1 ... ( ⌊ β€˜ ( π‘₯ / 𝑑 ) ) ) ) β†’ ( 𝑋 β€˜ ( 𝐿 β€˜ π‘˜ ) ) ∈ β„‚ )
57 simpr ⊒ ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) β†’ π‘₯ ∈ ℝ+ )
58 23 nnrpd ⊒ ( 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) β†’ 𝑑 ∈ ℝ+ )
59 rpdivcl ⊒ ( ( π‘₯ ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) β†’ ( π‘₯ / 𝑑 ) ∈ ℝ+ )
60 57 58 59 syl2an ⊒ ( ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ) β†’ ( π‘₯ / 𝑑 ) ∈ ℝ+ )
61 elfznn ⊒ ( π‘˜ ∈ ( 1 ... ( ⌊ β€˜ ( π‘₯ / 𝑑 ) ) ) β†’ π‘˜ ∈ β„• )
62 61 nnrpd ⊒ ( π‘˜ ∈ ( 1 ... ( ⌊ β€˜ ( π‘₯ / 𝑑 ) ) ) β†’ π‘˜ ∈ ℝ+ )
63 ifcl ⊒ ( ( ( π‘₯ / 𝑑 ) ∈ ℝ+ ∧ π‘˜ ∈ ℝ+ ) β†’ if ( 𝑆 = 0 , ( π‘₯ / 𝑑 ) , π‘˜ ) ∈ ℝ+ )
64 60 62 63 syl2an ⊒ ( ( ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ) ∧ π‘˜ ∈ ( 1 ... ( ⌊ β€˜ ( π‘₯ / 𝑑 ) ) ) ) β†’ if ( 𝑆 = 0 , ( π‘₯ / 𝑑 ) , π‘˜ ) ∈ ℝ+ )
65 64 relogcld ⊒ ( ( ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ) ∧ π‘˜ ∈ ( 1 ... ( ⌊ β€˜ ( π‘₯ / 𝑑 ) ) ) ) β†’ ( log β€˜ if ( 𝑆 = 0 , ( π‘₯ / 𝑑 ) , π‘˜ ) ) ∈ ℝ )
66 61 adantl ⊒ ( ( ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ) ∧ π‘˜ ∈ ( 1 ... ( ⌊ β€˜ ( π‘₯ / 𝑑 ) ) ) ) β†’ π‘˜ ∈ β„• )
67 65 66 nndivred ⊒ ( ( ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ) ∧ π‘˜ ∈ ( 1 ... ( ⌊ β€˜ ( π‘₯ / 𝑑 ) ) ) ) β†’ ( ( log β€˜ if ( 𝑆 = 0 , ( π‘₯ / 𝑑 ) , π‘˜ ) ) / π‘˜ ) ∈ ℝ )
68 67 recnd ⊒ ( ( ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ) ∧ π‘˜ ∈ ( 1 ... ( ⌊ β€˜ ( π‘₯ / 𝑑 ) ) ) ) β†’ ( ( log β€˜ if ( 𝑆 = 0 , ( π‘₯ / 𝑑 ) , π‘˜ ) ) / π‘˜ ) ∈ β„‚ )
69 56 68 mulcld ⊒ ( ( ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ) ∧ π‘˜ ∈ ( 1 ... ( ⌊ β€˜ ( π‘₯ / 𝑑 ) ) ) ) β†’ ( ( 𝑋 β€˜ ( 𝐿 β€˜ π‘˜ ) ) Β· ( ( log β€˜ if ( 𝑆 = 0 , ( π‘₯ / 𝑑 ) , π‘˜ ) ) / π‘˜ ) ) ∈ β„‚ )
70 52 69 fsumcl ⊒ ( ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ) β†’ Ξ£ π‘˜ ∈ ( 1 ... ( ⌊ β€˜ ( π‘₯ / 𝑑 ) ) ) ( ( 𝑋 β€˜ ( 𝐿 β€˜ π‘˜ ) ) Β· ( ( log β€˜ if ( 𝑆 = 0 , ( π‘₯ / 𝑑 ) , π‘˜ ) ) / π‘˜ ) ) ∈ β„‚ )
71 30 70 mulcld ⊒ ( ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ) β†’ ( ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑑 ) ) Β· ( ( ΞΌ β€˜ 𝑑 ) / 𝑑 ) ) Β· Ξ£ π‘˜ ∈ ( 1 ... ( ⌊ β€˜ ( π‘₯ / 𝑑 ) ) ) ( ( 𝑋 β€˜ ( 𝐿 β€˜ π‘˜ ) ) Β· ( ( log β€˜ if ( 𝑆 = 0 , ( π‘₯ / 𝑑 ) , π‘˜ ) ) / π‘˜ ) ) ) ∈ β„‚ )
72 18 71 fsumcl ⊒ ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) β†’ Ξ£ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ( ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑑 ) ) Β· ( ( ΞΌ β€˜ 𝑑 ) / 𝑑 ) ) Β· Ξ£ π‘˜ ∈ ( 1 ... ( ⌊ β€˜ ( π‘₯ / 𝑑 ) ) ) ( ( 𝑋 β€˜ ( 𝐿 β€˜ π‘˜ ) ) Β· ( ( log β€˜ if ( 𝑆 = 0 , ( π‘₯ / 𝑑 ) , π‘˜ ) ) / π‘˜ ) ) ) ∈ β„‚ )
73 35 46 mulcld ⊒ ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) β†’ ( ( Ξ£ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑑 ) ) Β· ( ( ΞΌ β€˜ 𝑑 ) / 𝑑 ) ) Β· 𝑆 ) Β· if ( 𝑆 = 0 , 0 , ( 𝑇 / 𝑆 ) ) ) ∈ β„‚ )
74 0cn ⊒ 0 ∈ β„‚
75 39 ad2antrr ⊒ ( ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ) β†’ 𝑇 ∈ β„‚ )
76 ifcl ⊒ ( ( 0 ∈ β„‚ ∧ 𝑇 ∈ β„‚ ) β†’ if ( 𝑆 = 0 , 0 , 𝑇 ) ∈ β„‚ )
77 74 75 76 sylancr ⊒ ( ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ) β†’ if ( 𝑆 = 0 , 0 , 𝑇 ) ∈ β„‚ )
78 30 70 77 subdid ⊒ ( ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ) β†’ ( ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑑 ) ) Β· ( ( ΞΌ β€˜ 𝑑 ) / 𝑑 ) ) Β· ( Ξ£ π‘˜ ∈ ( 1 ... ( ⌊ β€˜ ( π‘₯ / 𝑑 ) ) ) ( ( 𝑋 β€˜ ( 𝐿 β€˜ π‘˜ ) ) Β· ( ( log β€˜ if ( 𝑆 = 0 , ( π‘₯ / 𝑑 ) , π‘˜ ) ) / π‘˜ ) ) βˆ’ if ( 𝑆 = 0 , 0 , 𝑇 ) ) ) = ( ( ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑑 ) ) Β· ( ( ΞΌ β€˜ 𝑑 ) / 𝑑 ) ) Β· Ξ£ π‘˜ ∈ ( 1 ... ( ⌊ β€˜ ( π‘₯ / 𝑑 ) ) ) ( ( 𝑋 β€˜ ( 𝐿 β€˜ π‘˜ ) ) Β· ( ( log β€˜ if ( 𝑆 = 0 , ( π‘₯ / 𝑑 ) , π‘˜ ) ) / π‘˜ ) ) ) βˆ’ ( ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑑 ) ) Β· ( ( ΞΌ β€˜ 𝑑 ) / 𝑑 ) ) Β· if ( 𝑆 = 0 , 0 , 𝑇 ) ) ) )
79 78 sumeq2dv ⊒ ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) β†’ Ξ£ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ( ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑑 ) ) Β· ( ( ΞΌ β€˜ 𝑑 ) / 𝑑 ) ) Β· ( Ξ£ π‘˜ ∈ ( 1 ... ( ⌊ β€˜ ( π‘₯ / 𝑑 ) ) ) ( ( 𝑋 β€˜ ( 𝐿 β€˜ π‘˜ ) ) Β· ( ( log β€˜ if ( 𝑆 = 0 , ( π‘₯ / 𝑑 ) , π‘˜ ) ) / π‘˜ ) ) βˆ’ if ( 𝑆 = 0 , 0 , 𝑇 ) ) ) = Ξ£ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ( ( ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑑 ) ) Β· ( ( ΞΌ β€˜ 𝑑 ) / 𝑑 ) ) Β· Ξ£ π‘˜ ∈ ( 1 ... ( ⌊ β€˜ ( π‘₯ / 𝑑 ) ) ) ( ( 𝑋 β€˜ ( 𝐿 β€˜ π‘˜ ) ) Β· ( ( log β€˜ if ( 𝑆 = 0 , ( π‘₯ / 𝑑 ) , π‘˜ ) ) / π‘˜ ) ) ) βˆ’ ( ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑑 ) ) Β· ( ( ΞΌ β€˜ 𝑑 ) / 𝑑 ) ) Β· if ( 𝑆 = 0 , 0 , 𝑇 ) ) ) )
80 30 77 mulcld ⊒ ( ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ) β†’ ( ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑑 ) ) Β· ( ( ΞΌ β€˜ 𝑑 ) / 𝑑 ) ) Β· if ( 𝑆 = 0 , 0 , 𝑇 ) ) ∈ β„‚ )
81 18 71 80 fsumsub ⊒ ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) β†’ Ξ£ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ( ( ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑑 ) ) Β· ( ( ΞΌ β€˜ 𝑑 ) / 𝑑 ) ) Β· Ξ£ π‘˜ ∈ ( 1 ... ( ⌊ β€˜ ( π‘₯ / 𝑑 ) ) ) ( ( 𝑋 β€˜ ( 𝐿 β€˜ π‘˜ ) ) Β· ( ( log β€˜ if ( 𝑆 = 0 , ( π‘₯ / 𝑑 ) , π‘˜ ) ) / π‘˜ ) ) ) βˆ’ ( ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑑 ) ) Β· ( ( ΞΌ β€˜ 𝑑 ) / 𝑑 ) ) Β· if ( 𝑆 = 0 , 0 , 𝑇 ) ) ) = ( Ξ£ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ( ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑑 ) ) Β· ( ( ΞΌ β€˜ 𝑑 ) / 𝑑 ) ) Β· Ξ£ π‘˜ ∈ ( 1 ... ( ⌊ β€˜ ( π‘₯ / 𝑑 ) ) ) ( ( 𝑋 β€˜ ( 𝐿 β€˜ π‘˜ ) ) Β· ( ( log β€˜ if ( 𝑆 = 0 , ( π‘₯ / 𝑑 ) , π‘˜ ) ) / π‘˜ ) ) ) βˆ’ Ξ£ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ( ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑑 ) ) Β· ( ( ΞΌ β€˜ 𝑑 ) / 𝑑 ) ) Β· if ( 𝑆 = 0 , 0 , 𝑇 ) ) ) )
82 31 34 46 mulassd ⊒ ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) β†’ ( ( Ξ£ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑑 ) ) Β· ( ( ΞΌ β€˜ 𝑑 ) / 𝑑 ) ) Β· 𝑆 ) Β· if ( 𝑆 = 0 , 0 , ( 𝑇 / 𝑆 ) ) ) = ( Ξ£ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑑 ) ) Β· ( ( ΞΌ β€˜ 𝑑 ) / 𝑑 ) ) Β· ( 𝑆 Β· if ( 𝑆 = 0 , 0 , ( 𝑇 / 𝑆 ) ) ) ) )
83 ovif2 ⊒ ( 𝑆 Β· if ( 𝑆 = 0 , 0 , ( 𝑇 / 𝑆 ) ) ) = if ( 𝑆 = 0 , ( 𝑆 Β· 0 ) , ( 𝑆 Β· ( 𝑇 / 𝑆 ) ) )
84 33 mul01d ⊒ ( πœ‘ β†’ ( 𝑆 Β· 0 ) = 0 )
85 84 ifeq1d ⊒ ( πœ‘ β†’ if ( 𝑆 = 0 , ( 𝑆 Β· 0 ) , ( 𝑆 Β· ( 𝑇 / 𝑆 ) ) ) = if ( 𝑆 = 0 , 0 , ( 𝑆 Β· ( 𝑇 / 𝑆 ) ) ) )
86 40 41 42 divcan2d ⊒ ( ( πœ‘ ∧ 𝑆 β‰  0 ) β†’ ( 𝑆 Β· ( 𝑇 / 𝑆 ) ) = 𝑇 )
87 37 86 sylan2br ⊒ ( ( πœ‘ ∧ Β¬ 𝑆 = 0 ) β†’ ( 𝑆 Β· ( 𝑇 / 𝑆 ) ) = 𝑇 )
88 87 ifeq2da ⊒ ( πœ‘ β†’ if ( 𝑆 = 0 , 0 , ( 𝑆 Β· ( 𝑇 / 𝑆 ) ) ) = if ( 𝑆 = 0 , 0 , 𝑇 ) )
89 85 88 eqtrd ⊒ ( πœ‘ β†’ if ( 𝑆 = 0 , ( 𝑆 Β· 0 ) , ( 𝑆 Β· ( 𝑇 / 𝑆 ) ) ) = if ( 𝑆 = 0 , 0 , 𝑇 ) )
90 83 89 eqtrid ⊒ ( πœ‘ β†’ ( 𝑆 Β· if ( 𝑆 = 0 , 0 , ( 𝑇 / 𝑆 ) ) ) = if ( 𝑆 = 0 , 0 , 𝑇 ) )
91 90 adantr ⊒ ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) β†’ ( 𝑆 Β· if ( 𝑆 = 0 , 0 , ( 𝑇 / 𝑆 ) ) ) = if ( 𝑆 = 0 , 0 , 𝑇 ) )
92 91 oveq2d ⊒ ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) β†’ ( Ξ£ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑑 ) ) Β· ( ( ΞΌ β€˜ 𝑑 ) / 𝑑 ) ) Β· ( 𝑆 Β· if ( 𝑆 = 0 , 0 , ( 𝑇 / 𝑆 ) ) ) ) = ( Ξ£ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑑 ) ) Β· ( ( ΞΌ β€˜ 𝑑 ) / 𝑑 ) ) Β· if ( 𝑆 = 0 , 0 , 𝑇 ) ) )
93 74 39 76 sylancr ⊒ ( πœ‘ β†’ if ( 𝑆 = 0 , 0 , 𝑇 ) ∈ β„‚ )
94 93 adantr ⊒ ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) β†’ if ( 𝑆 = 0 , 0 , 𝑇 ) ∈ β„‚ )
95 18 94 30 fsummulc1 ⊒ ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) β†’ ( Ξ£ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑑 ) ) Β· ( ( ΞΌ β€˜ 𝑑 ) / 𝑑 ) ) Β· if ( 𝑆 = 0 , 0 , 𝑇 ) ) = Ξ£ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ( ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑑 ) ) Β· ( ( ΞΌ β€˜ 𝑑 ) / 𝑑 ) ) Β· if ( 𝑆 = 0 , 0 , 𝑇 ) ) )
96 82 92 95 3eqtrrd ⊒ ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) β†’ Ξ£ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ( ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑑 ) ) Β· ( ( ΞΌ β€˜ 𝑑 ) / 𝑑 ) ) Β· if ( 𝑆 = 0 , 0 , 𝑇 ) ) = ( ( Ξ£ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑑 ) ) Β· ( ( ΞΌ β€˜ 𝑑 ) / 𝑑 ) ) Β· 𝑆 ) Β· if ( 𝑆 = 0 , 0 , ( 𝑇 / 𝑆 ) ) ) )
97 96 oveq2d ⊒ ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) β†’ ( Ξ£ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ( ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑑 ) ) Β· ( ( ΞΌ β€˜ 𝑑 ) / 𝑑 ) ) Β· Ξ£ π‘˜ ∈ ( 1 ... ( ⌊ β€˜ ( π‘₯ / 𝑑 ) ) ) ( ( 𝑋 β€˜ ( 𝐿 β€˜ π‘˜ ) ) Β· ( ( log β€˜ if ( 𝑆 = 0 , ( π‘₯ / 𝑑 ) , π‘˜ ) ) / π‘˜ ) ) ) βˆ’ Ξ£ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ( ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑑 ) ) Β· ( ( ΞΌ β€˜ 𝑑 ) / 𝑑 ) ) Β· if ( 𝑆 = 0 , 0 , 𝑇 ) ) ) = ( Ξ£ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ( ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑑 ) ) Β· ( ( ΞΌ β€˜ 𝑑 ) / 𝑑 ) ) Β· Ξ£ π‘˜ ∈ ( 1 ... ( ⌊ β€˜ ( π‘₯ / 𝑑 ) ) ) ( ( 𝑋 β€˜ ( 𝐿 β€˜ π‘˜ ) ) Β· ( ( log β€˜ if ( 𝑆 = 0 , ( π‘₯ / 𝑑 ) , π‘˜ ) ) / π‘˜ ) ) ) βˆ’ ( ( Ξ£ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑑 ) ) Β· ( ( ΞΌ β€˜ 𝑑 ) / 𝑑 ) ) Β· 𝑆 ) Β· if ( 𝑆 = 0 , 0 , ( 𝑇 / 𝑆 ) ) ) ) )
98 79 81 97 3eqtrd ⊒ ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) β†’ Ξ£ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ( ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑑 ) ) Β· ( ( ΞΌ β€˜ 𝑑 ) / 𝑑 ) ) Β· ( Ξ£ π‘˜ ∈ ( 1 ... ( ⌊ β€˜ ( π‘₯ / 𝑑 ) ) ) ( ( 𝑋 β€˜ ( 𝐿 β€˜ π‘˜ ) ) Β· ( ( log β€˜ if ( 𝑆 = 0 , ( π‘₯ / 𝑑 ) , π‘˜ ) ) / π‘˜ ) ) βˆ’ if ( 𝑆 = 0 , 0 , 𝑇 ) ) ) = ( Ξ£ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ( ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑑 ) ) Β· ( ( ΞΌ β€˜ 𝑑 ) / 𝑑 ) ) Β· Ξ£ π‘˜ ∈ ( 1 ... ( ⌊ β€˜ ( π‘₯ / 𝑑 ) ) ) ( ( 𝑋 β€˜ ( 𝐿 β€˜ π‘˜ ) ) Β· ( ( log β€˜ if ( 𝑆 = 0 , ( π‘₯ / 𝑑 ) , π‘˜ ) ) / π‘˜ ) ) ) βˆ’ ( ( Ξ£ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑑 ) ) Β· ( ( ΞΌ β€˜ 𝑑 ) / 𝑑 ) ) Β· 𝑆 ) Β· if ( 𝑆 = 0 , 0 , ( 𝑇 / 𝑆 ) ) ) ) )
99 98 mpteq2dva ⊒ ( πœ‘ β†’ ( π‘₯ ∈ ℝ+ ↦ Ξ£ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ( ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑑 ) ) Β· ( ( ΞΌ β€˜ 𝑑 ) / 𝑑 ) ) Β· ( Ξ£ π‘˜ ∈ ( 1 ... ( ⌊ β€˜ ( π‘₯ / 𝑑 ) ) ) ( ( 𝑋 β€˜ ( 𝐿 β€˜ π‘˜ ) ) Β· ( ( log β€˜ if ( 𝑆 = 0 , ( π‘₯ / 𝑑 ) , π‘˜ ) ) / π‘˜ ) ) βˆ’ if ( 𝑆 = 0 , 0 , 𝑇 ) ) ) ) = ( π‘₯ ∈ ℝ+ ↦ ( Ξ£ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ( ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑑 ) ) Β· ( ( ΞΌ β€˜ 𝑑 ) / 𝑑 ) ) Β· Ξ£ π‘˜ ∈ ( 1 ... ( ⌊ β€˜ ( π‘₯ / 𝑑 ) ) ) ( ( 𝑋 β€˜ ( 𝐿 β€˜ π‘˜ ) ) Β· ( ( log β€˜ if ( 𝑆 = 0 , ( π‘₯ / 𝑑 ) , π‘˜ ) ) / π‘˜ ) ) ) βˆ’ ( ( Ξ£ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑑 ) ) Β· ( ( ΞΌ β€˜ 𝑑 ) / 𝑑 ) ) Β· 𝑆 ) Β· if ( 𝑆 = 0 , 0 , ( 𝑇 / 𝑆 ) ) ) ) ) )
100 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 dchrvmasumiflem1 ⊒ ( πœ‘ β†’ ( π‘₯ ∈ ℝ+ ↦ Ξ£ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ( ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑑 ) ) Β· ( ( ΞΌ β€˜ 𝑑 ) / 𝑑 ) ) Β· ( Ξ£ π‘˜ ∈ ( 1 ... ( ⌊ β€˜ ( π‘₯ / 𝑑 ) ) ) ( ( 𝑋 β€˜ ( 𝐿 β€˜ π‘˜ ) ) Β· ( ( log β€˜ if ( 𝑆 = 0 , ( π‘₯ / 𝑑 ) , π‘˜ ) ) / π‘˜ ) ) βˆ’ if ( 𝑆 = 0 , 0 , 𝑇 ) ) ) ) ∈ 𝑂(1) )
101 99 100 eqeltrrd ⊒ ( πœ‘ β†’ ( π‘₯ ∈ ℝ+ ↦ ( Ξ£ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ( ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑑 ) ) Β· ( ( ΞΌ β€˜ 𝑑 ) / 𝑑 ) ) Β· Ξ£ π‘˜ ∈ ( 1 ... ( ⌊ β€˜ ( π‘₯ / 𝑑 ) ) ) ( ( 𝑋 β€˜ ( 𝐿 β€˜ π‘˜ ) ) Β· ( ( log β€˜ if ( 𝑆 = 0 , ( π‘₯ / 𝑑 ) , π‘˜ ) ) / π‘˜ ) ) ) βˆ’ ( ( Ξ£ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑑 ) ) Β· ( ( ΞΌ β€˜ 𝑑 ) / 𝑑 ) ) Β· 𝑆 ) Β· if ( 𝑆 = 0 , 0 , ( 𝑇 / 𝑆 ) ) ) ) ) ∈ 𝑂(1) )
102 72 73 101 o1dif ⊒ ( πœ‘ β†’ ( ( π‘₯ ∈ ℝ+ ↦ Ξ£ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ( ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑑 ) ) Β· ( ( ΞΌ β€˜ 𝑑 ) / 𝑑 ) ) Β· Ξ£ π‘˜ ∈ ( 1 ... ( ⌊ β€˜ ( π‘₯ / 𝑑 ) ) ) ( ( 𝑋 β€˜ ( 𝐿 β€˜ π‘˜ ) ) Β· ( ( log β€˜ if ( 𝑆 = 0 , ( π‘₯ / 𝑑 ) , π‘˜ ) ) / π‘˜ ) ) ) ) ∈ 𝑂(1) ↔ ( π‘₯ ∈ ℝ+ ↦ ( ( Ξ£ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑑 ) ) Β· ( ( ΞΌ β€˜ 𝑑 ) / 𝑑 ) ) Β· 𝑆 ) Β· if ( 𝑆 = 0 , 0 , ( 𝑇 / 𝑆 ) ) ) ) ∈ 𝑂(1) ) )
103 51 102 mpbird ⊒ ( πœ‘ β†’ ( π‘₯ ∈ ℝ+ ↦ Ξ£ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ( ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑑 ) ) Β· ( ( ΞΌ β€˜ 𝑑 ) / 𝑑 ) ) Β· Ξ£ π‘˜ ∈ ( 1 ... ( ⌊ β€˜ ( π‘₯ / 𝑑 ) ) ) ( ( 𝑋 β€˜ ( 𝐿 β€˜ π‘˜ ) ) Β· ( ( log β€˜ if ( 𝑆 = 0 , ( π‘₯ / 𝑑 ) , π‘˜ ) ) / π‘˜ ) ) ) ) ∈ 𝑂(1) )
104 7 ad2antrr ⊒ ( ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ) β†’ 𝑋 ∈ 𝐷 )
105 elfzelz ⊒ ( 𝑛 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) β†’ 𝑛 ∈ β„€ )
106 105 adantl ⊒ ( ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ) β†’ 𝑛 ∈ β„€ )
107 4 1 5 2 104 106 dchrzrhcl ⊒ ( ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ) β†’ ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑛 ) ) ∈ β„‚ )
108 elfznn ⊒ ( 𝑛 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) β†’ 𝑛 ∈ β„• )
109 108 adantl ⊒ ( ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ) β†’ 𝑛 ∈ β„• )
110 vmacl ⊒ ( 𝑛 ∈ β„• β†’ ( Ξ› β€˜ 𝑛 ) ∈ ℝ )
111 nndivre ⊒ ( ( ( Ξ› β€˜ 𝑛 ) ∈ ℝ ∧ 𝑛 ∈ β„• ) β†’ ( ( Ξ› β€˜ 𝑛 ) / 𝑛 ) ∈ ℝ )
112 110 111 mpancom ⊒ ( 𝑛 ∈ β„• β†’ ( ( Ξ› β€˜ 𝑛 ) / 𝑛 ) ∈ ℝ )
113 109 112 syl ⊒ ( ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ) β†’ ( ( Ξ› β€˜ 𝑛 ) / 𝑛 ) ∈ ℝ )
114 113 recnd ⊒ ( ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ) β†’ ( ( Ξ› β€˜ 𝑛 ) / 𝑛 ) ∈ β„‚ )
115 107 114 mulcld ⊒ ( ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ) β†’ ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑛 ) ) Β· ( ( Ξ› β€˜ 𝑛 ) / 𝑛 ) ) ∈ β„‚ )
116 18 115 fsumcl ⊒ ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) β†’ Ξ£ 𝑛 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑛 ) ) Β· ( ( Ξ› β€˜ 𝑛 ) / 𝑛 ) ) ∈ β„‚ )
117 relogcl ⊒ ( π‘₯ ∈ ℝ+ β†’ ( log β€˜ π‘₯ ) ∈ ℝ )
118 117 adantl ⊒ ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) β†’ ( log β€˜ π‘₯ ) ∈ ℝ )
119 118 recnd ⊒ ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) β†’ ( log β€˜ π‘₯ ) ∈ β„‚ )
120 ifcl ⊒ ( ( ( log β€˜ π‘₯ ) ∈ β„‚ ∧ 0 ∈ β„‚ ) β†’ if ( 𝑆 = 0 , ( log β€˜ π‘₯ ) , 0 ) ∈ β„‚ )
121 119 74 120 sylancl ⊒ ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) β†’ if ( 𝑆 = 0 , ( log β€˜ π‘₯ ) , 0 ) ∈ β„‚ )
122 116 121 addcld ⊒ ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) β†’ ( Ξ£ 𝑛 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑛 ) ) Β· ( ( Ξ› β€˜ 𝑛 ) / 𝑛 ) ) + if ( 𝑆 = 0 , ( log β€˜ π‘₯ ) , 0 ) ) ∈ β„‚ )
123 122 abscld ⊒ ( ( πœ‘ ∧ π‘₯ ∈ ℝ+ ) β†’ ( abs β€˜ ( Ξ£ 𝑛 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑛 ) ) Β· ( ( Ξ› β€˜ 𝑛 ) / 𝑛 ) ) + if ( 𝑆 = 0 , ( log β€˜ π‘₯ ) , 0 ) ) ) ∈ ℝ )
124 123 adantrr ⊒ ( ( πœ‘ ∧ ( π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯ ) ) β†’ ( abs β€˜ ( Ξ£ 𝑛 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑛 ) ) Β· ( ( Ξ› β€˜ 𝑛 ) / 𝑛 ) ) + if ( 𝑆 = 0 , ( log β€˜ π‘₯ ) , 0 ) ) ) ∈ ℝ )
125 3 adantr ⊒ ( ( πœ‘ ∧ ( π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯ ) ) β†’ 𝑁 ∈ β„• )
126 7 adantr ⊒ ( ( πœ‘ ∧ ( π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯ ) ) β†’ 𝑋 ∈ 𝐷 )
127 8 adantr ⊒ ( ( πœ‘ ∧ ( π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯ ) ) β†’ 𝑋 β‰  1 )
128 simprl ⊒ ( ( πœ‘ ∧ ( π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯ ) ) β†’ π‘₯ ∈ ℝ+ )
129 simprr ⊒ ( ( πœ‘ ∧ ( π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯ ) ) β†’ 1 ≀ π‘₯ )
130 1 2 125 4 5 6 126 127 128 129 dchrvmasum2if ⊒ ( ( πœ‘ ∧ ( π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯ ) ) β†’ ( Ξ£ 𝑛 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑛 ) ) Β· ( ( Ξ› β€˜ 𝑛 ) / 𝑛 ) ) + if ( 𝑆 = 0 , ( log β€˜ π‘₯ ) , 0 ) ) = Ξ£ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ( ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑑 ) ) Β· ( ( ΞΌ β€˜ 𝑑 ) / 𝑑 ) ) Β· Ξ£ π‘˜ ∈ ( 1 ... ( ⌊ β€˜ ( π‘₯ / 𝑑 ) ) ) ( ( 𝑋 β€˜ ( 𝐿 β€˜ π‘˜ ) ) Β· ( ( log β€˜ if ( 𝑆 = 0 , ( π‘₯ / 𝑑 ) , π‘˜ ) ) / π‘˜ ) ) ) )
131 130 fveq2d ⊒ ( ( πœ‘ ∧ ( π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯ ) ) β†’ ( abs β€˜ ( Ξ£ 𝑛 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑛 ) ) Β· ( ( Ξ› β€˜ 𝑛 ) / 𝑛 ) ) + if ( 𝑆 = 0 , ( log β€˜ π‘₯ ) , 0 ) ) ) = ( abs β€˜ Ξ£ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ( ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑑 ) ) Β· ( ( ΞΌ β€˜ 𝑑 ) / 𝑑 ) ) Β· Ξ£ π‘˜ ∈ ( 1 ... ( ⌊ β€˜ ( π‘₯ / 𝑑 ) ) ) ( ( 𝑋 β€˜ ( 𝐿 β€˜ π‘˜ ) ) Β· ( ( log β€˜ if ( 𝑆 = 0 , ( π‘₯ / 𝑑 ) , π‘˜ ) ) / π‘˜ ) ) ) ) )
132 124 131 eqled ⊒ ( ( πœ‘ ∧ ( π‘₯ ∈ ℝ+ ∧ 1 ≀ π‘₯ ) ) β†’ ( abs β€˜ ( Ξ£ 𝑛 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑛 ) ) Β· ( ( Ξ› β€˜ 𝑛 ) / 𝑛 ) ) + if ( 𝑆 = 0 , ( log β€˜ π‘₯ ) , 0 ) ) ) ≀ ( abs β€˜ Ξ£ 𝑑 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ( ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑑 ) ) Β· ( ( ΞΌ β€˜ 𝑑 ) / 𝑑 ) ) Β· Ξ£ π‘˜ ∈ ( 1 ... ( ⌊ β€˜ ( π‘₯ / 𝑑 ) ) ) ( ( 𝑋 β€˜ ( 𝐿 β€˜ π‘˜ ) ) Β· ( ( log β€˜ if ( 𝑆 = 0 , ( π‘₯ / 𝑑 ) , π‘˜ ) ) / π‘˜ ) ) ) ) )
133 17 103 72 122 132 o1le ⊒ ( πœ‘ β†’ ( π‘₯ ∈ ℝ+ ↦ ( Ξ£ 𝑛 ∈ ( 1 ... ( ⌊ β€˜ π‘₯ ) ) ( ( 𝑋 β€˜ ( 𝐿 β€˜ 𝑛 ) ) Β· ( ( Ξ› β€˜ 𝑛 ) / 𝑛 ) ) + if ( 𝑆 = 0 , ( log β€˜ π‘₯ ) , 0 ) ) ) ∈ 𝑂(1) )