MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dchrmusum2 Structured version   Unicode version

Theorem dchrmusum2 22630
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.)
Hypotheses
Ref Expression
rpvmasum.z  |-  Z  =  (ℤ/n `  N )
rpvmasum.l  |-  L  =  ( ZRHom `  Z
)
rpvmasum.a  |-  ( ph  ->  N  e.  NN )
rpvmasum.g  |-  G  =  (DChr `  N )
rpvmasum.d  |-  D  =  ( Base `  G
)
rpvmasum.1  |-  .1.  =  ( 0g `  G )
dchrisum.b  |-  ( ph  ->  X  e.  D )
dchrisum.n1  |-  ( ph  ->  X  =/=  .1.  )
dchrisumn0.f  |-  F  =  ( a  e.  NN  |->  ( ( X `  ( L `  a ) )  /  a ) )
dchrisumn0.c  |-  ( ph  ->  C  e.  ( 0 [,) +oo ) )
dchrisumn0.t  |-  ( ph  ->  seq 1 (  +  ,  F )  ~~>  T )
dchrisumn0.1  |-  ( ph  ->  A. y  e.  ( 1 [,) +oo )
( abs `  (
(  seq 1 (  +  ,  F ) `  ( |_ `  y ) )  -  T ) )  <_  ( C  /  y ) )
Assertion
Ref Expression
dchrmusum2  |-  ( ph  ->  ( x  e.  RR+  |->  ( sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( ( X `  ( L `  d ) )  x.  ( ( mmu `  d )  /  d ) )  x.  T ) )  e.  O(1) )
Distinct variable groups:    x, y,  .1.    x, d, y, C    F, d, x, y    a,
d, x, y    x, N, y    ph, d, x    T, d, x, y    x, Z, y    x, D, y    L, a, d, x, y    X, a, d, x, y
Allowed substitution hints:    ph( y, a)    C( a)    D( a, d)    T( a)    .1. ( a, d)    F( a)    G( x, y, a, d)    N( a, d)    Z( a, d)

Proof of Theorem dchrmusum2
Dummy variables  m  n are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 rpssre 10991 . . . 4  |-  RR+  C_  RR
2 ax-1cn 9330 . . . 4  |-  1  e.  CC
3 o1const 13083 . . . 4  |-  ( (
RR+  C_  RR  /\  1  e.  CC )  ->  (
x  e.  RR+  |->  1 )  e.  O(1) )
41, 2, 3mp2an 667 . . 3  |-  ( x  e.  RR+  |->  1 )  e.  O(1)
54a1i 11 . 2  |-  ( ph  ->  ( x  e.  RR+  |->  1 )  e.  O(1) )
62a1i 11 . . 3  |-  ( (
ph  /\  x  e.  RR+ )  ->  1  e.  CC )
7 fzfid 11781 . . . . 5  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( 1 ... ( |_ `  x ) )  e. 
Fin )
8 rpvmasum.g . . . . . . 7  |-  G  =  (DChr `  N )
9 rpvmasum.z . . . . . . 7  |-  Z  =  (ℤ/n `  N )
10 rpvmasum.d . . . . . . 7  |-  D  =  ( Base `  G
)
11 rpvmasum.l . . . . . . 7  |-  L  =  ( ZRHom `  Z
)
12 dchrisum.b . . . . . . . 8  |-  ( ph  ->  X  e.  D )
1312ad2antrr 720 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  X  e.  D )
14 elfzelz 11442 . . . . . . . 8  |-  ( d  e.  ( 1 ... ( |_ `  x
) )  ->  d  e.  ZZ )
1514adantl 463 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  d  e.  ZZ )
168, 9, 10, 11, 13, 15dchrzrhcl 22471 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( X `  ( L `  d
) )  e.  CC )
17 elfznn 11467 . . . . . . . . 9  |-  ( d  e.  ( 1 ... ( |_ `  x
) )  ->  d  e.  NN )
1817adantl 463 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  d  e.  NN )
19 mucl 22366 . . . . . . . . . 10  |-  ( d  e.  NN  ->  (
mmu `  d )  e.  ZZ )
2019zred 10737 . . . . . . . . 9  |-  ( d  e.  NN  ->  (
mmu `  d )  e.  RR )
21 nndivre 10347 . . . . . . . . 9  |-  ( ( ( mmu `  d
)  e.  RR  /\  d  e.  NN )  ->  ( ( mmu `  d )  /  d
)  e.  RR )
2220, 21mpancom 664 . . . . . . . 8  |-  ( d  e.  NN  ->  (
( mmu `  d
)  /  d )  e.  RR )
2318, 22syl 16 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
mmu `  d )  /  d )  e.  RR )
2423recnd 9402 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
mmu `  d )  /  d )  e.  CC )
2516, 24mulcld 9396 . . . . 5  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( X `  ( L `  d ) )  x.  ( ( mmu `  d )  /  d
) )  e.  CC )
267, 25fsumcl 13196 . . . 4  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( ( X `  ( L `  d ) )  x.  ( ( mmu `  d )  /  d ) )  e.  CC )
27 dchrisumn0.t . . . . . 6  |-  ( ph  ->  seq 1 (  +  ,  F )  ~~>  T )
28 climcl 12963 . . . . . 6  |-  (  seq 1 (  +  ,  F )  ~~>  T  ->  T  e.  CC )
2927, 28syl 16 . . . . 5  |-  ( ph  ->  T  e.  CC )
3029adantr 462 . . . 4  |-  ( (
ph  /\  x  e.  RR+ )  ->  T  e.  CC )
3126, 30mulcld 9396 . . 3  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( ( X `  ( L `  d )
)  x.  ( ( mmu `  d )  /  d ) )  x.  T )  e.  CC )
321a1i 11 . . . 4  |-  ( ph  -> 
RR+  C_  RR )
33 subcl 9599 . . . . 5  |-  ( ( 1  e.  CC  /\  ( sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( ( X `  ( L `  d ) )  x.  ( ( mmu `  d )  /  d ) )  x.  T )  e.  CC )  ->  (
1  -  ( sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( ( X `  ( L `  d )
)  x.  ( ( mmu `  d )  /  d ) )  x.  T ) )  e.  CC )
342, 31, 33sylancr 658 . . . 4  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( 1  -  ( sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( ( X `  ( L `  d ) )  x.  ( ( mmu `  d )  /  d ) )  x.  T ) )  e.  CC )
35 1red 9391 . . . 4  |-  ( ph  ->  1  e.  RR )
36 dchrisumn0.c . . . . . 6  |-  ( ph  ->  C  e.  ( 0 [,) +oo ) )
37 elrege0 11382 . . . . . 6  |-  ( C  e.  ( 0 [,) +oo )  <->  ( C  e.  RR  /\  0  <_  C ) )
3836, 37sylib 196 . . . . 5  |-  ( ph  ->  ( C  e.  RR  /\  0  <_  C )
)
3938simpld 456 . . . 4  |-  ( ph  ->  C  e.  RR )
40 fzfid 11781 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( 1 ... ( |_ `  x ) )  e.  Fin )
4125adantlrr 715 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( X `
 ( L `  d ) )  x.  ( ( mmu `  d )  /  d
) )  e.  CC )
42 nnuz 10886 . . . . . . . . . . . 12  |-  NN  =  ( ZZ>= `  1 )
43 1zzd 10667 . . . . . . . . . . . 12  |-  ( ph  ->  1  e.  ZZ )
4412adantr 462 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  m  e.  NN )  ->  X  e.  D )
45 nnz 10658 . . . . . . . . . . . . . . . . 17  |-  ( m  e.  NN  ->  m  e.  ZZ )
4645adantl 463 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  m  e.  NN )  ->  m  e.  ZZ )
478, 9, 10, 11, 44, 46dchrzrhcl 22471 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  m  e.  NN )  ->  ( X `
 ( L `  m ) )  e.  CC )
48 nncn 10320 . . . . . . . . . . . . . . . 16  |-  ( m  e.  NN  ->  m  e.  CC )
4948adantl 463 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  m  e.  NN )  ->  m  e.  CC )
50 nnne0 10344 . . . . . . . . . . . . . . . 16  |-  ( m  e.  NN  ->  m  =/=  0 )
5150adantl 463 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  m  e.  NN )  ->  m  =/=  0 )
5247, 49, 51divcld 10097 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  NN )  ->  ( ( X `  ( L `
 m ) )  /  m )  e.  CC )
53 dchrisumn0.f . . . . . . . . . . . . . . 15  |-  F  =  ( a  e.  NN  |->  ( ( X `  ( L `  a ) )  /  a ) )
54 fveq2 5681 . . . . . . . . . . . . . . . . . 18  |-  ( a  =  m  ->  ( L `  a )  =  ( L `  m ) )
5554fveq2d 5685 . . . . . . . . . . . . . . . . 17  |-  ( a  =  m  ->  ( X `  ( L `  a ) )  =  ( X `  ( L `  m )
) )
56 id 22 . . . . . . . . . . . . . . . . 17  |-  ( a  =  m  ->  a  =  m )
5755, 56oveq12d 6100 . . . . . . . . . . . . . . . 16  |-  ( a  =  m  ->  (
( X `  ( L `  a )
)  /  a )  =  ( ( X `
 ( L `  m ) )  /  m ) )
5857cbvmptv 4373 . . . . . . . . . . . . . . 15  |-  ( a  e.  NN  |->  ( ( X `  ( L `
 a ) )  /  a ) )  =  ( m  e.  NN  |->  ( ( X `
 ( L `  m ) )  /  m ) )
5953, 58eqtri 2455 . . . . . . . . . . . . . 14  |-  F  =  ( m  e.  NN  |->  ( ( X `  ( L `  m ) )  /  m ) )
6052, 59fmptd 5857 . . . . . . . . . . . . 13  |-  ( ph  ->  F : NN --> CC )
6160ffvelrnda 5833 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  NN )  ->  ( F `
 m )  e.  CC )
6242, 43, 61serf 11820 . . . . . . . . . . 11  |-  ( ph  ->  seq 1 (  +  ,  F ) : NN --> CC )
6362ad2antrr 720 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  seq 1 (  +  ,  F ) : NN --> CC )
64 simprl 750 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  x  e.  RR+ )
6564rpred 11017 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  x  e.  RR )
66 nndivre 10347 . . . . . . . . . . . 12  |-  ( ( x  e.  RR  /\  d  e.  NN )  ->  ( x  /  d
)  e.  RR )
6765, 17, 66syl2an 474 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  / 
d )  e.  RR )
6817adantl 463 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  d  e.  NN )
6968nncnd 10328 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  d  e.  CC )
7069mulid2d 9394 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  x.  d )  =  d )
71 fznnfl 11687 . . . . . . . . . . . . . . 15  |-  ( x  e.  RR  ->  (
d  e.  ( 1 ... ( |_ `  x ) )  <->  ( d  e.  NN  /\  d  <_  x ) ) )
7265, 71syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( d  e.  ( 1 ... ( |_
`  x ) )  <-> 
( d  e.  NN  /\  d  <_  x )
) )
7372simplbda 621 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  d  <_  x
)
7470, 73eqbrtrd 4302 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  x.  d )  <_  x
)
75 1red 9391 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  e.  RR )
7665adantr 462 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  x  e.  RR )
7768nnrpd 11016 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  d  e.  RR+ )
7875, 76, 77lemuldivd 11062 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( 1  x.  d )  <_  x 
<->  1  <_  ( x  /  d ) ) )
7974, 78mpbid 210 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  <_  (
x  /  d ) )
80 flge1nn 11653 . . . . . . . . . . 11  |-  ( ( ( x  /  d
)  e.  RR  /\  1  <_  ( x  / 
d ) )  -> 
( |_ `  (
x  /  d ) )  e.  NN )
8167, 79, 80syl2anc 656 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( |_ `  ( x  /  d
) )  e.  NN )
8263, 81ffvelrnd 5834 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  (  seq 1
(  +  ,  F
) `  ( |_ `  ( x  /  d
) ) )  e.  CC )
8341, 82mulcld 9396 . . . . . . . 8  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( ( X `  ( L `
 d ) )  x.  ( ( mmu `  d )  /  d
) )  x.  (  seq 1 (  +  ,  F ) `  ( |_ `  ( x  / 
d ) ) ) )  e.  CC )
8429ad2antrr 720 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  T  e.  CC )
8541, 84mulcld 9396 . . . . . . . 8  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( ( X `  ( L `
 d ) )  x.  ( ( mmu `  d )  /  d
) )  x.  T
)  e.  CC )
8640, 83, 85fsumsub 13240 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( ( ( ( X `
 ( L `  d ) )  x.  ( ( mmu `  d )  /  d
) )  x.  (  seq 1 (  +  ,  F ) `  ( |_ `  ( x  / 
d ) ) ) )  -  ( ( ( X `  ( L `  d )
)  x.  ( ( mmu `  d )  /  d ) )  x.  T ) )  =  ( sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( ( ( X `
 ( L `  d ) )  x.  ( ( mmu `  d )  /  d
) )  x.  (  seq 1 (  +  ,  F ) `  ( |_ `  ( x  / 
d ) ) ) )  -  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( ( ( X `
 ( L `  d ) )  x.  ( ( mmu `  d )  /  d
) )  x.  T
) ) )
8741, 82, 84subdid 9790 . . . . . . . 8  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( ( X `  ( L `
 d ) )  x.  ( ( mmu `  d )  /  d
) )  x.  (
(  seq 1 (  +  ,  F ) `  ( |_ `  ( x  /  d ) ) )  -  T ) )  =  ( ( ( ( X `  ( L `  d ) )  x.  ( ( mmu `  d )  /  d ) )  x.  (  seq 1
(  +  ,  F
) `  ( |_ `  ( x  /  d
) ) ) )  -  ( ( ( X `  ( L `
 d ) )  x.  ( ( mmu `  d )  /  d
) )  x.  T
) ) )
8887sumeq2dv 13166 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( ( ( X `  ( L `  d ) )  x.  ( ( mmu `  d )  /  d ) )  x.  ( (  seq 1 (  +  ,  F ) `  ( |_ `  ( x  / 
d ) ) )  -  T ) )  =  sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( ( ( ( X `  ( L `
 d ) )  x.  ( ( mmu `  d )  /  d
) )  x.  (  seq 1 (  +  ,  F ) `  ( |_ `  ( x  / 
d ) ) ) )  -  ( ( ( X `  ( L `  d )
)  x.  ( ( mmu `  d )  /  d ) )  x.  T ) ) )
8912ad3antrrr 724 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  / 
d ) ) ) )  ->  X  e.  D )
9014ad2antlr 721 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  / 
d ) ) ) )  ->  d  e.  ZZ )
91 elfzelz 11442 . . . . . . . . . . . . . . . . . . 19  |-  ( m  e.  ( 1 ... ( |_ `  (
x  /  d ) ) )  ->  m  e.  ZZ )
9291adantl 463 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  / 
d ) ) ) )  ->  m  e.  ZZ )
938, 9, 10, 11, 89, 90, 92dchrzrhmul 22472 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  / 
d ) ) ) )  ->  ( X `  ( L `  (
d  x.  m ) ) )  =  ( ( X `  ( L `  d )
)  x.  ( X `
 ( L `  m ) ) ) )
9493oveq1d 6097 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  / 
d ) ) ) )  ->  ( ( X `  ( L `  ( d  x.  m
) ) )  / 
( d  x.  m
) )  =  ( ( ( X `  ( L `  d ) )  x.  ( X `
 ( L `  m ) ) )  /  ( d  x.  m ) ) )
9516adantlrr 715 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( X `  ( L `  d ) )  e.  CC )
9695adantr 462 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  / 
d ) ) ) )  ->  ( X `  ( L `  d
) )  e.  CC )
9769adantr 462 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  / 
d ) ) ) )  ->  d  e.  CC )
988, 9, 10, 11, 89, 92dchrzrhcl 22471 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  / 
d ) ) ) )  ->  ( X `  ( L `  m
) )  e.  CC )
99 elfznn 11467 . . . . . . . . . . . . . . . . . . 19  |-  ( m  e.  ( 1 ... ( |_ `  (
x  /  d ) ) )  ->  m  e.  NN )
10099adantl 463 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  / 
d ) ) ) )  ->  m  e.  NN )
101100nncnd 10328 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  / 
d ) ) ) )  ->  m  e.  CC )
10268nnne0d 10356 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  d  =/=  0
)
103102adantr 462 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  / 
d ) ) ) )  ->  d  =/=  0 )
104100nnne0d 10356 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  / 
d ) ) ) )  ->  m  =/=  0 )
10596, 97, 98, 101, 103, 104divmuldivd 10138 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  / 
d ) ) ) )  ->  ( (
( X `  ( L `  d )
)  /  d )  x.  ( ( X `
 ( L `  m ) )  /  m ) )  =  ( ( ( X `
 ( L `  d ) )  x.  ( X `  ( L `  m )
) )  /  (
d  x.  m ) ) )
10694, 105eqtr4d 2470 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  / 
d ) ) ) )  ->  ( ( X `  ( L `  ( d  x.  m
) ) )  / 
( d  x.  m
) )  =  ( ( ( X `  ( L `  d ) )  /  d )  x.  ( ( X `
 ( L `  m ) )  /  m ) ) )
107106oveq2d 6098 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  / 
d ) ) ) )  ->  ( (
mmu `  d )  x.  ( ( X `  ( L `  ( d  x.  m ) ) )  /  ( d  x.  m ) ) )  =  ( ( mmu `  d )  x.  ( ( ( X `  ( L `
 d ) )  /  d )  x.  ( ( X `  ( L `  m ) )  /  m ) ) ) )
10868, 19syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( mmu `  d )  e.  ZZ )
109108zcnd 10738 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( mmu `  d )  e.  CC )
110109adantr 462 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  / 
d ) ) ) )  ->  ( mmu `  d )  e.  CC )
11196, 97, 103divcld 10097 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  / 
d ) ) ) )  ->  ( ( X `  ( L `  d ) )  / 
d )  e.  CC )
11298, 101, 104divcld 10097 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  / 
d ) ) ) )  ->  ( ( X `  ( L `  m ) )  /  m )  e.  CC )
113110, 111, 112mulassd 9399 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  / 
d ) ) ) )  ->  ( (
( mmu `  d
)  x.  ( ( X `  ( L `
 d ) )  /  d ) )  x.  ( ( X `
 ( L `  m ) )  /  m ) )  =  ( ( mmu `  d )  x.  (
( ( X `  ( L `  d ) )  /  d )  x.  ( ( X `
 ( L `  m ) )  /  m ) ) ) )
114110, 96, 97, 103div12d 10133 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  / 
d ) ) ) )  ->  ( (
mmu `  d )  x.  ( ( X `  ( L `  d ) )  /  d ) )  =  ( ( X `  ( L `
 d ) )  x.  ( ( mmu `  d )  /  d
) ) )
115114oveq1d 6097 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  / 
d ) ) ) )  ->  ( (
( mmu `  d
)  x.  ( ( X `  ( L `
 d ) )  /  d ) )  x.  ( ( X `
 ( L `  m ) )  /  m ) )  =  ( ( ( X `
 ( L `  d ) )  x.  ( ( mmu `  d )  /  d
) )  x.  (
( X `  ( L `  m )
)  /  m ) ) )
116107, 113, 1153eqtr2d 2473 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  / 
d ) ) ) )  ->  ( (
mmu `  d )  x.  ( ( X `  ( L `  ( d  x.  m ) ) )  /  ( d  x.  m ) ) )  =  ( ( ( X `  ( L `  d )
)  x.  ( ( mmu `  d )  /  d ) )  x.  ( ( X `
 ( L `  m ) )  /  m ) ) )
117116sumeq2dv 13166 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  sum_ m  e.  ( 1 ... ( |_
`  ( x  / 
d ) ) ) ( ( mmu `  d )  x.  (
( X `  ( L `  ( d  x.  m ) ) )  /  ( d  x.  m ) ) )  =  sum_ m  e.  ( 1 ... ( |_
`  ( x  / 
d ) ) ) ( ( ( X `
 ( L `  d ) )  x.  ( ( mmu `  d )  /  d
) )  x.  (
( X `  ( L `  m )
)  /  m ) ) )
118 fzfid 11781 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1 ... ( |_ `  (
x  /  d ) ) )  e.  Fin )
119 simpll 748 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ph )
120119, 99, 52syl2an 474 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  / 
d ) ) ) )  ->  ( ( X `  ( L `  m ) )  /  m )  e.  CC )
121118, 41, 120fsummulc2 13236 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( ( X `  ( L `
 d ) )  x.  ( ( mmu `  d )  /  d
) )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  d ) ) ) ( ( X `  ( L `
 m ) )  /  m ) )  =  sum_ m  e.  ( 1 ... ( |_
`  ( x  / 
d ) ) ) ( ( ( X `
 ( L `  d ) )  x.  ( ( mmu `  d )  /  d
) )  x.  (
( X `  ( L `  m )
)  /  m ) ) )
122 ovex 6107 . . . . . . . . . . . . . . . 16  |-  ( ( X `  ( L `
 m ) )  /  m )  e. 
_V
12357, 53, 122fvmpt 5764 . . . . . . . . . . . . . . 15  |-  ( m  e.  NN  ->  ( F `  m )  =  ( ( X `
 ( L `  m ) )  /  m ) )
124100, 123syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  /\  m  e.  ( 1 ... ( |_
`  ( x  / 
d ) ) ) )  ->  ( F `  m )  =  ( ( X `  ( L `  m )
)  /  m ) )
12581, 42syl6eleq 2525 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( |_ `  ( x  /  d
) )  e.  (
ZZ>= `  1 ) )
126124, 125, 120fsumser 13193 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  sum_ m  e.  ( 1 ... ( |_
`  ( x  / 
d ) ) ) ( ( X `  ( L `  m ) )  /  m )  =  (  seq 1
(  +  ,  F
) `  ( |_ `  ( x  /  d
) ) ) )
127126oveq2d 6098 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( ( X `  ( L `
 d ) )  x.  ( ( mmu `  d )  /  d
) )  x.  sum_ m  e.  ( 1 ... ( |_ `  (
x  /  d ) ) ) ( ( X `  ( L `
 m ) )  /  m ) )  =  ( ( ( X `  ( L `
 d ) )  x.  ( ( mmu `  d )  /  d
) )  x.  (  seq 1 (  +  ,  F ) `  ( |_ `  ( x  / 
d ) ) ) ) )
128117, 121, 1273eqtr2rd 2474 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( ( X `  ( L `
 d ) )  x.  ( ( mmu `  d )  /  d
) )  x.  (  seq 1 (  +  ,  F ) `  ( |_ `  ( x  / 
d ) ) ) )  =  sum_ m  e.  ( 1 ... ( |_ `  ( x  / 
d ) ) ) ( ( mmu `  d )  x.  (
( X `  ( L `  ( d  x.  m ) ) )  /  ( d  x.  m ) ) ) )
129128sumeq2dv 13166 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( ( ( X `  ( L `  d ) )  x.  ( ( mmu `  d )  /  d ) )  x.  (  seq 1
(  +  ,  F
) `  ( |_ `  ( x  /  d
) ) ) )  =  sum_ d  e.  ( 1 ... ( |_
`  x ) )
sum_ m  e.  (
1 ... ( |_ `  ( x  /  d
) ) ) ( ( mmu `  d
)  x.  ( ( X `  ( L `
 ( d  x.  m ) ) )  /  ( d  x.  m ) ) ) )
130 fveq2 5681 . . . . . . . . . . . . . 14  |-  ( n  =  ( d  x.  m )  ->  ( L `  n )  =  ( L `  ( d  x.  m
) ) )
131130fveq2d 5685 . . . . . . . . . . . . 13  |-  ( n  =  ( d  x.  m )  ->  ( X `  ( L `  n ) )  =  ( X `  ( L `  ( d  x.  m ) ) ) )
132 id 22 . . . . . . . . . . . . 13  |-  ( n  =  ( d  x.  m )  ->  n  =  ( d  x.  m ) )
133131, 132oveq12d 6100 . . . . . . . . . . . 12  |-  ( n  =  ( d  x.  m )  ->  (
( X `  ( L `  n )
)  /  n )  =  ( ( X `
 ( L `  ( d  x.  m
) ) )  / 
( d  x.  m
) ) )
134133oveq2d 6098 . . . . . . . . . . 11  |-  ( n  =  ( d  x.  m )  ->  (
( mmu `  d
)  x.  ( ( X `  ( L `
 n ) )  /  n ) )  =  ( ( mmu `  d )  x.  (
( X `  ( L `  ( d  x.  m ) ) )  /  ( d  x.  m ) ) ) )
135 elrabi 3105 . . . . . . . . . . . . . . 15  |-  ( d  e.  { y  e.  NN  |  y  ||  n }  ->  d  e.  NN )
136135ad2antll 723 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( n  e.  (
1 ... ( |_ `  x ) )  /\  d  e.  { y  e.  NN  |  y  ||  n } ) )  -> 
d  e.  NN )
137136, 19syl 16 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( n  e.  (
1 ... ( |_ `  x ) )  /\  d  e.  { y  e.  NN  |  y  ||  n } ) )  -> 
( mmu `  d
)  e.  ZZ )
138137zcnd 10738 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( n  e.  (
1 ... ( |_ `  x ) )  /\  d  e.  { y  e.  NN  |  y  ||  n } ) )  -> 
( mmu `  d
)  e.  CC )
13912ad2antrr 720 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  X  e.  D
)
140 elfzelz 11442 . . . . . . . . . . . . . . . 16  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  ZZ )
141140adantl 463 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  ZZ )
1428, 9, 10, 11, 139, 141dchrzrhcl 22471 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( X `  ( L `  n ) )  e.  CC )
14317ssriv 3350 . . . . . . . . . . . . . . . . 17  |-  ( 1 ... ( |_ `  x ) )  C_  NN
144143a1i 11 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( 1 ... ( |_ `  x ) ) 
C_  NN )
145144sselda 3346 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  NN )
146145nncnd 10328 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  CC )
147145nnne0d 10356 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  =/=  0
)
148142, 146, 147divcld 10097 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( X `
 ( L `  n ) )  /  n )  e.  CC )
149148adantrr 711 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( n  e.  (
1 ... ( |_ `  x ) )  /\  d  e.  { y  e.  NN  |  y  ||  n } ) )  -> 
( ( X `  ( L `  n ) )  /  n )  e.  CC )
150138, 149mulcld 9396 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( n  e.  (
1 ... ( |_ `  x ) )  /\  d  e.  { y  e.  NN  |  y  ||  n } ) )  -> 
( ( mmu `  d )  x.  (
( X `  ( L `  n )
)  /  n ) )  e.  CC )
151134, 65, 150dvdsflsumcom 22415 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) sum_ d  e.  { y  e.  NN  |  y  ||  n }  ( (
mmu `  d )  x.  ( ( X `  ( L `  n ) )  /  n ) )  =  sum_ d  e.  ( 1 ... ( |_ `  x ) )
sum_ m  e.  (
1 ... ( |_ `  ( x  /  d
) ) ) ( ( mmu `  d
)  x.  ( ( X `  ( L `
 ( d  x.  m ) ) )  /  ( d  x.  m ) ) ) )
152 fveq2 5681 . . . . . . . . . . . . 13  |-  ( n  =  1  ->  ( L `  n )  =  ( L ` 
1 ) )
153152fveq2d 5685 . . . . . . . . . . . 12  |-  ( n  =  1  ->  ( X `  ( L `  n ) )  =  ( X `  ( L `  1 )
) )
154 id 22 . . . . . . . . . . . 12  |-  ( n  =  1  ->  n  =  1 )
155153, 154oveq12d 6100 . . . . . . . . . . 11  |-  ( n  =  1  ->  (
( X `  ( L `  n )
)  /  n )  =  ( ( X `
 ( L ` 
1 ) )  / 
1 ) )
156 simprr 751 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
1  <_  x )
157 flge1nn 11653 . . . . . . . . . . . . . 14  |-  ( ( x  e.  RR  /\  1  <_  x )  -> 
( |_ `  x
)  e.  NN )
15865, 156, 157syl2anc 656 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( |_ `  x
)  e.  NN )
159158, 42syl6eleq 2525 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( |_ `  x
)  e.  ( ZZ>= ` 
1 ) )
160 eluzfz1 11447 . . . . . . . . . . . 12  |-  ( ( |_ `  x )  e.  ( ZZ>= `  1
)  ->  1  e.  ( 1 ... ( |_ `  x ) ) )
161159, 160syl 16 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
1  e.  ( 1 ... ( |_ `  x ) ) )
162155, 40, 144, 161, 148musumsum 22419 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) sum_ d  e.  { y  e.  NN  |  y  ||  n }  ( (
mmu `  d )  x.  ( ( X `  ( L `  n ) )  /  n ) )  =  ( ( X `  ( L `
 1 ) )  /  1 ) )
163129, 151, 1623eqtr2d 2473 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( ( ( X `  ( L `  d ) )  x.  ( ( mmu `  d )  /  d ) )  x.  (  seq 1
(  +  ,  F
) `  ( |_ `  ( x  /  d
) ) ) )  =  ( ( X `
 ( L ` 
1 ) )  / 
1 ) )
1648, 9, 10, 11, 12dchrzrh1 22470 . . . . . . . . . . . 12  |-  ( ph  ->  ( X `  ( L `  1 )
)  =  1 )
165164adantr 462 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( X `  ( L `  1 )
)  =  1 )
166165oveq1d 6097 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ( X `  ( L `  1 ) )  /  1 )  =  ( 1  / 
1 ) )
167 1div1e1 10014 . . . . . . . . . 10  |-  ( 1  /  1 )  =  1
168166, 167syl6eq 2483 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ( X `  ( L `  1 ) )  /  1 )  =  1 )
169163, 168eqtr2d 2468 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
1  =  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( ( ( X `
 ( L `  d ) )  x.  ( ( mmu `  d )  /  d
) )  x.  (  seq 1 (  +  ,  F ) `  ( |_ `  ( x  / 
d ) ) ) ) )
17029adantr 462 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  T  e.  CC )
17140, 170, 41fsummulc1 13237 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( ( X `  ( L `  d ) )  x.  ( ( mmu `  d )  /  d ) )  x.  T )  = 
sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( ( ( X `
 ( L `  d ) )  x.  ( ( mmu `  d )  /  d
) )  x.  T
) )
172169, 171oveq12d 6100 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( 1  -  ( sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( ( X `  ( L `  d )
)  x.  ( ( mmu `  d )  /  d ) )  x.  T ) )  =  ( sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( ( ( X `
 ( L `  d ) )  x.  ( ( mmu `  d )  /  d
) )  x.  (  seq 1 (  +  ,  F ) `  ( |_ `  ( x  / 
d ) ) ) )  -  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( ( ( X `
 ( L `  d ) )  x.  ( ( mmu `  d )  /  d
) )  x.  T
) ) )
17386, 88, 1723eqtr4rd 2478 . . . . . 6  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( 1  -  ( sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( ( X `  ( L `  d )
)  x.  ( ( mmu `  d )  /  d ) )  x.  T ) )  =  sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( ( ( X `
 ( L `  d ) )  x.  ( ( mmu `  d )  /  d
) )  x.  (
(  seq 1 (  +  ,  F ) `  ( |_ `  ( x  /  d ) ) )  -  T ) ) )
174173fveq2d 5685 . . . . 5  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( abs `  (
1  -  ( sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( ( X `  ( L `  d )
)  x.  ( ( mmu `  d )  /  d ) )  x.  T ) ) )  =  ( abs `  sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( ( ( X `
 ( L `  d ) )  x.  ( ( mmu `  d )  /  d
) )  x.  (
(  seq 1 (  +  ,  F ) `  ( |_ `  ( x  /  d ) ) )  -  T ) ) ) )
17582, 84subcld 9709 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (  seq 1 (  +  ,  F ) `  ( |_ `  ( x  / 
d ) ) )  -  T )  e.  CC )
17641, 175mulcld 9396 . . . . . . . 8  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( ( X `  ( L `
 d ) )  x.  ( ( mmu `  d )  /  d
) )  x.  (
(  seq 1 (  +  ,  F ) `  ( |_ `  ( x  /  d ) ) )  -  T ) )  e.  CC )
17740, 176fsumcl 13196 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( ( ( X `  ( L `  d ) )  x.  ( ( mmu `  d )  /  d ) )  x.  ( (  seq 1 (  +  ,  F ) `  ( |_ `  ( x  / 
d ) ) )  -  T ) )  e.  CC )
178177abscld 12908 . . . . . 6  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( abs `  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( ( ( X `  ( L `  d ) )  x.  ( ( mmu `  d )  /  d ) )  x.  ( (  seq 1 (  +  ,  F ) `  ( |_ `  ( x  / 
d ) ) )  -  T ) ) )  e.  RR )
179176abscld 12908 . . . . . . 7  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  (
( ( X `  ( L `  d ) )  x.  ( ( mmu `  d )  /  d ) )  x.  ( (  seq 1 (  +  ,  F ) `  ( |_ `  ( x  / 
d ) ) )  -  T ) ) )  e.  RR )
18040, 179fsumrecl 13197 . . . . . 6  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( abs `  ( ( ( X `  ( L `  d )
)  x.  ( ( mmu `  d )  /  d ) )  x.  ( (  seq 1 (  +  ,  F ) `  ( |_ `  ( x  / 
d ) ) )  -  T ) ) )  e.  RR )
18139adantr 462 . . . . . 6  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  C  e.  RR )
18240, 176fsumabs 13249 . . . . . 6  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( abs `  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( ( ( X `  ( L `  d ) )  x.  ( ( mmu `  d )  /  d ) )  x.  ( (  seq 1 (  +  ,  F ) `  ( |_ `  ( x  / 
d ) ) )  -  T ) ) )  <_  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( abs `  (
( ( X `  ( L `  d ) )  x.  ( ( mmu `  d )  /  d ) )  x.  ( (  seq 1 (  +  ,  F ) `  ( |_ `  ( x  / 
d ) ) )  -  T ) ) ) )
183 reflcl 11632 . . . . . . . . . 10  |-  ( x  e.  RR  ->  ( |_ `  x )  e.  RR )
18465, 183syl 16 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( |_ `  x
)  e.  RR )
185184, 181remulcld 9404 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ( |_ `  x )  x.  C
)  e.  RR )
186185, 64rerpdivcld 11044 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ( ( |_
`  x )  x.  C )  /  x
)  e.  RR )
187181, 64rerpdivcld 11044 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( C  /  x
)  e.  RR )
188187adantr 462 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( C  /  x )  e.  RR )
18941abscld 12908 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  (
( X `  ( L `  d )
)  x.  ( ( mmu `  d )  /  d ) ) )  e.  RR )
19068nnrecred 10357 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  / 
d )  e.  RR )
191175abscld 12908 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  (
(  seq 1 (  +  ,  F ) `  ( |_ `  ( x  /  d ) ) )  -  T ) )  e.  RR )
19277rpred 11017 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  d  e.  RR )
193188, 192remulcld 9404 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( C  /  x )  x.  d )  e.  RR )
19441absge0d 12916 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( abs `  ( ( X `
 ( L `  d ) )  x.  ( ( mmu `  d )  /  d
) ) ) )
195175absge0d 12916 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( abs `  ( (  seq 1 (  +  ,  F ) `  ( |_ `  ( x  / 
d ) ) )  -  T ) ) )
19695abscld 12908 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( X `  ( L `  d ) ) )  e.  RR )
19724adantlrr 715 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( mmu `  d )  /  d
)  e.  CC )
198197abscld 12908 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  (
( mmu `  d
)  /  d ) )  e.  RR )
19995absge0d 12916 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( abs `  ( X `  ( L `  d ) ) ) )
200197absge0d 12916 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  ( abs `  ( ( mmu `  d )  /  d
) ) )
201 eqid 2435 . . . . . . . . . . . . . 14  |-  ( Base `  Z )  =  (
Base `  Z )
20212ad2antrr 720 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  X  e.  D
)
203 rpvmasum.a . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  N  e.  NN )
204203nnnn0d 10626 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  N  e.  NN0 )
2059, 201, 11znzrhfo 17824 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  NN0  ->  L : ZZ -onto-> ( Base `  Z
) )
206 fof 5610 . . . . . . . . . . . . . . . . 17  |-  ( L : ZZ -onto-> ( Base `  Z )  ->  L : ZZ --> ( Base `  Z
) )
207204, 205, 2063syl 20 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  L : ZZ --> ( Base `  Z ) )
208207adantr 462 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  L : ZZ --> ( Base `  Z ) )
209 ffvelrn 5831 . . . . . . . . . . . . . . 15  |-  ( ( L : ZZ --> ( Base `  Z )  /\  d  e.  ZZ )  ->  ( L `  d )  e.  ( Base `  Z
) )
210208, 14, 209syl2an 474 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( L `  d )  e.  (
Base `  Z )
)
2118, 10, 9, 201, 202, 210dchrabs2 22488 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  ( X `  ( L `  d ) ) )  <_  1 )
212109, 69, 102absdivd 12927 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  (
( mmu `  d
)  /  d ) )  =  ( ( abs `  ( mmu `  d ) )  / 
( abs `  d
) ) )
21377rprege0d 11024 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( d  e.  RR  /\  0  <_ 
d ) )
214 absid 12771 . . . . . . . . . . . . . . . . 17  |-  ( ( d  e.  RR  /\  0  <_  d )  -> 
( abs `  d
)  =  d )
215213, 214syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  d
)  =  d )
216215oveq2d 6098 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( mmu `  d
) )  /  ( abs `  d ) )  =  ( ( abs `  ( mmu `  d
) )  /  d
) )
217212, 216eqtrd 2467 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  (
( mmu `  d
)  /  d ) )  =  ( ( abs `  ( mmu `  d ) )  / 
d ) )
218109abscld 12908 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  (
mmu `  d )
)  e.  RR )
219 mule1 22373 . . . . . . . . . . . . . . . 16  |-  ( d  e.  NN  ->  ( abs `  ( mmu `  d ) )  <_ 
1 )
22068, 219syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  (
mmu `  d )
)  <_  1 )
221218, 75, 77, 220lediv1dd 11071 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( mmu `  d
) )  /  d
)  <_  ( 1  /  d ) )
222217, 221eqbrtrd 4302 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  (
( mmu `  d
)  /  d ) )  <_  ( 1  /  d ) )
223196, 75, 198, 190, 199, 200, 211, 222lemul12ad 10265 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( X `  ( L `  d )
) )  x.  ( abs `  ( ( mmu `  d )  /  d
) ) )  <_ 
( 1  x.  (
1  /  d ) ) )
22495, 197absmuld 12926 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  (
( X `  ( L `  d )
)  x.  ( ( mmu `  d )  /  d ) ) )  =  ( ( abs `  ( X `
 ( L `  d ) ) )  x.  ( abs `  (
( mmu `  d
)  /  d ) ) ) )
225190recnd 9402 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  / 
d )  e.  CC )
226225mulid2d 9394 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  x.  ( 1  /  d
) )  =  ( 1  /  d ) )
227226eqcomd 2440 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  / 
d )  =  ( 1  x.  ( 1  /  d ) ) )
228223, 224, 2273brtr4d 4312 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  (
( X `  ( L `  d )
)  x.  ( ( mmu `  d )  /  d ) ) )  <_  ( 1  /  d ) )
229 1re 9375 . . . . . . . . . . . . . . 15  |-  1  e.  RR
230 elicopnf 11375 . . . . . . . . . . . . . . 15  |-  ( 1  e.  RR  ->  (
( x  /  d
)  e.  ( 1 [,) +oo )  <->  ( (
x  /  d )  e.  RR  /\  1  <_  ( x  /  d
) ) ) )
231229, 230ax-mp 5 . . . . . . . . . . . . . 14  |-  ( ( x  /  d )  e.  ( 1 [,) +oo )  <->  ( ( x  /  d )  e.  RR  /\  1  <_ 
( x  /  d
) ) )
23267, 79, 231sylanbrc 659 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  / 
d )  e.  ( 1 [,) +oo )
)
233 dchrisumn0.1 . . . . . . . . . . . . . 14  |-  ( ph  ->  A. y  e.  ( 1 [,) +oo )
( abs `  (
(  seq 1 (  +  ,  F ) `  ( |_ `  y ) )  -  T ) )  <_  ( C  /  y ) )
234233ad2antrr 720 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  A. y  e.  ( 1 [,) +oo )
( abs `  (
(  seq 1 (  +  ,  F ) `  ( |_ `  y ) )  -  T ) )  <_  ( C  /  y ) )
235 fveq2 5681 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  ( x  / 
d )  ->  ( |_ `  y )  =  ( |_ `  (
x  /  d ) ) )
236235fveq2d 5685 . . . . . . . . . . . . . . . . 17  |-  ( y  =  ( x  / 
d )  ->  (  seq 1 (  +  ,  F ) `  ( |_ `  y ) )  =  (  seq 1
(  +  ,  F
) `  ( |_ `  ( x  /  d
) ) ) )
237236oveq1d 6097 . . . . . . . . . . . . . . . 16  |-  ( y  =  ( x  / 
d )  ->  (
(  seq 1 (  +  ,  F ) `  ( |_ `  y ) )  -  T )  =  ( (  seq 1 (  +  ,  F ) `  ( |_ `  ( x  / 
d ) ) )  -  T ) )
238237fveq2d 5685 . . . . . . . . . . . . . . 15  |-  ( y  =  ( x  / 
d )  ->  ( abs `  ( (  seq 1 (  +  ,  F ) `  ( |_ `  y ) )  -  T ) )  =  ( abs `  (
(  seq 1 (  +  ,  F ) `  ( |_ `  ( x  /  d ) ) )  -  T ) ) )
239 oveq2 6090 . . . . . . . . . . . . . . 15  |-  ( y  =  ( x  / 
d )  ->  ( C  /  y )  =  ( C  /  (
x  /  d ) ) )
240238, 239breq12d 4295 . . . . . . . . . . . . . 14  |-  ( y  =  ( x  / 
d )  ->  (
( abs `  (
(  seq 1 (  +  ,  F ) `  ( |_ `  y ) )  -  T ) )  <_  ( C  /  y )  <->  ( abs `  ( (  seq 1
(  +  ,  F
) `  ( |_ `  ( x  /  d
) ) )  -  T ) )  <_ 
( C  /  (
x  /  d ) ) ) )
241240rspcv 3060 . . . . . . . . . . . . 13  |-  ( ( x  /  d )  e.  ( 1 [,) +oo )  ->  ( A. y  e.  ( 1 [,) +oo ) ( abs `  ( (  seq 1 (  +  ,  F ) `  ( |_ `  y ) )  -  T ) )  <_  ( C  /  y )  -> 
( abs `  (
(  seq 1 (  +  ,  F ) `  ( |_ `  ( x  /  d ) ) )  -  T ) )  <_  ( C  /  ( x  / 
d ) ) ) )
242232, 234, 241sylc 60 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  (
(  seq 1 (  +  ,  F ) `  ( |_ `  ( x  /  d ) ) )  -  T ) )  <_  ( C  /  ( x  / 
d ) ) )
243181recnd 9402 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  C  e.  CC )
244243adantr 462 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  C  e.  CC )
245 rpcnne0 10998 . . . . . . . . . . . . . . . 16  |-  ( x  e.  RR+  ->  ( x  e.  CC  /\  x  =/=  0 ) )
246245ad2antrl 722 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( x  e.  CC  /\  x  =/=  0 ) )
247246adantr 462 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( x  e.  CC  /\  x  =/=  0 ) )
248 divdiv2 10033 . . . . . . . . . . . . . 14  |-  ( ( C  e.  CC  /\  ( x  e.  CC  /\  x  =/=  0 )  /\  ( d  e.  CC  /\  d  =/=  0 ) )  -> 
( C  /  (
x  /  d ) )  =  ( ( C  x.  d )  /  x ) )
249244, 247, 69, 102, 248syl112anc 1217 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( C  / 
( x  /  d
) )  =  ( ( C  x.  d
)  /  x ) )
250 div23 10003 . . . . . . . . . . . . . 14  |-  ( ( C  e.  CC  /\  d  e.  CC  /\  (
x  e.  CC  /\  x  =/=  0 ) )  ->  ( ( C  x.  d )  /  x )  =  ( ( C  /  x
)  x.  d ) )
251244, 69, 247, 250syl3anc 1213 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( C  x.  d )  /  x )  =  ( ( C  /  x
)  x.  d ) )
252249, 251eqtrd 2467 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( C  / 
( x  /  d
) )  =  ( ( C  /  x
)  x.  d ) )
253242, 252breqtrd 4306 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  (
(  seq 1 (  +  ,  F ) `  ( |_ `  ( x  /  d ) ) )  -  T ) )  <_  ( ( C  /  x )  x.  d ) )
254189, 190, 191, 193, 194, 195, 228, 253lemul12ad 10265 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( abs `  ( ( X `  ( L `  d ) )  x.  ( ( mmu `  d )  /  d ) ) )  x.  ( abs `  ( (  seq 1
(  +  ,  F
) `  ( |_ `  ( x  /  d
) ) )  -  T ) ) )  <_  ( ( 1  /  d )  x.  ( ( C  /  x )  x.  d
) ) )
25541, 175absmuld 12926 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  (
( ( X `  ( L `  d ) )  x.  ( ( mmu `  d )  /  d ) )  x.  ( (  seq 1 (  +  ,  F ) `  ( |_ `  ( x  / 
d ) ) )  -  T ) ) )  =  ( ( abs `  ( ( X `  ( L `
 d ) )  x.  ( ( mmu `  d )  /  d
) ) )  x.  ( abs `  (
(  seq 1 (  +  ,  F ) `  ( |_ `  ( x  /  d ) ) )  -  T ) ) ) )
256187recnd 9402 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( C  /  x
)  e.  CC )
257256adantr 462 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( C  /  x )  e.  CC )
258257, 69, 102divcan4d 10103 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( ( C  /  x )  x.  d )  / 
d )  =  ( C  /  x ) )
259257, 69mulcld 9396 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( C  /  x )  x.  d )  e.  CC )
260259, 69, 102divrec2d 10101 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( ( C  /  x )  x.  d )  / 
d )  =  ( ( 1  /  d
)  x.  ( ( C  /  x )  x.  d ) ) )
261258, 260eqtr3d 2469 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( C  /  x )  =  ( ( 1  /  d
)  x.  ( ( C  /  x )  x.  d ) ) )
262254, 255, 2613brtr4d 4312 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  d  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( abs `  (
( ( X `  ( L `  d ) )  x.  ( ( mmu `  d )  /  d ) )  x.  ( (  seq 1 (  +  ,  F ) `  ( |_ `  ( x  / 
d ) ) )  -  T ) ) )  <_  ( C  /  x ) )
26340, 179, 188, 262fsumle 13247 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( abs `  ( ( ( X `  ( L `  d )
)  x.  ( ( mmu `  d )  /  d ) )  x.  ( (  seq 1 (  +  ,  F ) `  ( |_ `  ( x  / 
d ) ) )  -  T ) ) )  <_  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( C  /  x
) )
264158nnnn0d 10626 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( |_ `  x
)  e.  NN0 )
265 hashfz1 12103 . . . . . . . . . . 11  |-  ( ( |_ `  x )  e.  NN0  ->  ( # `  ( 1 ... ( |_ `  x ) ) )  =  ( |_
`  x ) )
266264, 265syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( # `  ( 1 ... ( |_ `  x ) ) )  =  ( |_ `  x ) )
267266oveq1d 6097 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ( # `  (
1 ... ( |_ `  x ) ) )  x.  ( C  /  x ) )  =  ( ( |_ `  x )  x.  ( C  /  x ) ) )
268 fsumconst 13242 . . . . . . . . . 10  |-  ( ( ( 1 ... ( |_ `  x ) )  e.  Fin  /\  ( C  /  x )  e.  CC )  ->  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( C  /  x
)  =  ( (
# `  ( 1 ... ( |_ `  x
) ) )  x.  ( C  /  x
) ) )
26940, 256, 268syl2anc 656 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( C  /  x )  =  ( ( # `  ( 1 ... ( |_ `  x ) ) )  x.  ( C  /  x ) ) )
270158nncnd 10328 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( |_ `  x
)  e.  CC )
271 divass 10002 . . . . . . . . . 10  |-  ( ( ( |_ `  x
)  e.  CC  /\  C  e.  CC  /\  (
x  e.  CC  /\  x  =/=  0 ) )  ->  ( ( ( |_ `  x )  x.  C )  /  x )  =  ( ( |_ `  x
)  x.  ( C  /  x ) ) )
272270, 243, 246, 271syl3anc 1213 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ( ( |_
`  x )  x.  C )  /  x
)  =  ( ( |_ `  x )  x.  ( C  /  x ) ) )
273267, 269, 2723eqtr4d 2477 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( C  /  x )  =  ( ( ( |_ `  x )  x.  C )  /  x ) )
274263, 273breqtrd 4306 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( abs `  ( ( ( X `  ( L `  d )
)  x.  ( ( mmu `  d )  /  d ) )  x.  ( (  seq 1 (  +  ,  F ) `  ( |_ `  ( x  / 
d ) ) )  -  T ) ) )  <_  ( (
( |_ `  x
)  x.  C )  /  x ) )
27538adantr 462 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( C  e.  RR  /\  0  <_  C )
)
276 flle 11635 . . . . . . . . . 10  |-  ( x  e.  RR  ->  ( |_ `  x )  <_  x )
27765, 276syl 16 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( |_ `  x
)  <_  x )
278 lemul1a 10173 . . . . . . . . 9  |-  ( ( ( ( |_ `  x )  e.  RR  /\  x  e.  RR  /\  ( C  e.  RR  /\  0  <_  C )
)  /\  ( |_ `  x )  <_  x
)  ->  ( ( |_ `  x )  x.  C )  <_  (
x  x.  C ) )
279184, 65, 275, 277, 278syl31anc 1216 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ( |_ `  x )  x.  C
)  <_  ( x  x.  C ) )
280185, 181, 64ledivmuld 11066 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ( ( ( |_ `  x )  x.  C )  /  x )  <_  C  <->  ( ( |_ `  x
)  x.  C )  <_  ( x  x.  C ) ) )
281279, 280mpbird 232 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ( ( |_
`  x )  x.  C )  /  x
)  <_  C )
282180, 186, 181, 274, 281letrd 9518 . . . . . 6  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( abs `  ( ( ( X `  ( L `  d )
)  x.  ( ( mmu `  d )  /  d ) )  x.  ( (  seq 1 (  +  ,  F ) `  ( |_ `  ( x  / 
d ) ) )  -  T ) ) )  <_  C )
283178, 180, 181, 182, 282letrd 9518 . . . . 5  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( abs `  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( ( ( X `  ( L `  d ) )  x.  ( ( mmu `  d )  /  d ) )  x.  ( (  seq 1 (  +  ,  F ) `  ( |_ `  ( x  / 
d ) ) )  -  T ) ) )  <_  C )
284174, 283eqbrtrd 4302 . . . 4  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( abs `  (
1  -  ( sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( ( X `  ( L `  d )
)  x.  ( ( mmu `  d )  /  d ) )  x.  T ) ) )  <_  C )
28532, 34, 35, 39, 284elo1d 13000 . . 3  |-  ( ph  ->  ( x  e.  RR+  |->  ( 1  -  ( sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( ( X `  ( L `  d )
)  x.  ( ( mmu `  d )  /  d ) )  x.  T ) ) )  e.  O(1) )
2866, 31, 285o1dif 13093 . 2  |-  ( ph  ->  ( ( x  e.  RR+  |->  1 )  e.  O(1)  <-> 
( x  e.  RR+  |->  ( sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( ( X `  ( L `  d ) )  x.  ( ( mmu `  d )  /  d ) )  x.  T ) )  e.  O(1) ) )
2875, 286mpbid 210 1  |-  ( ph  ->  ( x  e.  RR+  |->  ( sum_ d  e.  ( 1 ... ( |_
`  x ) ) ( ( X `  ( L `  d ) )  x.  ( ( mmu `  d )  /  d ) )  x.  T ) )  e.  O(1) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1364    e. wcel 1757    =/= wne 2598   A.wral 2707   {crab 2711    C_ wss 3318   class class class wbr 4282    e. cmpt 4340   -->wf 5404   -onto->wfo 5406   ` cfv 5408  (class class class)co 6082   Fincfn 7300   CCcc 9270   RRcr 9271   0cc0 9272   1c1 9273    + caddc 9275    x. cmul 9277   +oocpnf 9405    <_ cle 9409    - cmin 9585    / cdiv 9983   NNcn 10312   NN0cn0 10569   ZZcz 10636   ZZ>=cuz 10851   RR+crp 10981   [,)cico 11292   ...cfz 11426   |_cfl 11626    seqcseq 11792   #chash 12089   abscabs 12709    ~~> cli 12948   O(1)co1 12950   sum_csu 13149    || cdivides 13520   Basecbs 14159   0gc0g 14363   ZRHomczrh 17775  ℤ/nczn 17778   mmucmu 22319  DChrcdchr 22458
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2416  ax-rep 4393  ax-sep 4403  ax-nul 4411  ax-pow 4460  ax-pr 4521  ax-un 6363  ax-inf2 7837  ax-cnex 9328  ax-resscn 9329  ax-1cn 9330  ax-icn 9331  ax-addcl 9332  ax-addrcl 9333  ax-mulcl 9334  ax-mulrcl 9335  ax-mulcom 9336  ax-addass 9337  ax-mulass 9338  ax-distr 9339  ax-i2m1 9340  ax-1ne0 9341  ax-1rid 9342  ax-rnegex 9343  ax-rrecex 9344  ax-cnre 9345  ax-pre-lttri 9346  ax-pre-lttrn 9347  ax-pre-ltadd 9348  ax-pre-mulgt0 9349  ax-pre-sup 9350  ax-addf 9351  ax-mulf 9352
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-fal 1370  df-ex 1592  df-nf 1595  df-sb 1702  df-eu 2260  df-mo 2261  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-nel 2601  df-ral 2712  df-rex 2713  df-reu 2714  df-rmo 2715  df-rab 2716  df-v 2966  df-sbc 3178  df-csb 3279  df-dif 3321  df-un 3323  df-in 3325  df-ss 3332  df-pss 3334  df-nul 3628  df-if 3782  df-pw 3852  df-sn 3868  df-pr 3870  df-tp 3872  df-op 3874  df-uni 4082  df-int 4119  df-iun 4163  df-iin 4164  df-disj 4253  df-br 4283  df-opab 4341  df-mpt 4342  df-tr 4376  df-eprel 4621  df-id 4625  df-po 4630  df-so 4631  df-fr 4668  df-se 4669  df-we 4670  df-ord 4711  df-on 4712  df-lim 4713  df-suc 4714  df-xp 4835  df-rel 4836  df-cnv 4837  df-co 4838  df-dm 4839  df-rn 4840  df-res 4841  df-ima 4842  df-iota 5371  df-fun 5410  df-fn 5411  df-f 5412  df-f1 5413  df-fo 5414  df-f1o 5415  df-fv 5416  df-isom 5417  df-riota 6041  df-ov 6085  df-oprab 6086  df-mpt2 6087  df-of 6311  df-om 6468  df-1st 6568  df-2nd 6569  df-supp 6682  df-tpos 6736  df-recs 6820  df-rdg 6854  df-1o 6910  df-2o 6911  df-oadd 6914  df-omul 6915  df-er 7091  df-ec 7093  df-qs 7097  df-map 7206  df-pm 7207  df-ixp 7254  df-en 7301  df-dom 7302  df-sdom 7303  df-fin 7304  df-fsupp 7611  df-fi 7651  df-sup 7681  df-oi 7714  df-card 8099  df-acn 8102  df-cda 8327  df-pnf 9410  df-mnf 9411  df-xr 9412  df-ltxr 9413  df-le 9414  df-sub 9587  df-neg 9588  df-div 9984  df-nn 10313  df-2 10370  df-3 10371  df-4 10372  df-5 10373  df-6 10374  df-7 10375  df-8 10376  df-9 10377  df-10 10378  df-n0 10570  df-z 10637  df-dec 10746  df-uz 10852  df-q 10944  df-rp 10982  df-xneg 11079  df-xadd 11080  df-xmul 11081  df-ioo 11294  df-ioc 11295  df-ico 11296  df-icc 11297  df-fz 11427  df-fzo 11535  df-fl 11628  df-mod 11695  df-seq 11793  df-exp 11852  df-fac 12038  df-bc 12065  df-hash 12090  df-shft 12542  df-cj 12574  df-re 12575  df-im 12576  df-sqr 12710  df-abs 12711  df-limsup 12935  df-clim 12952  df-rlim 12953  df-o1 12954  df-lo1 12955  df-sum 13150  df-ef 13338  df-sin 13340  df-cos 13341  df-pi 13343  df-dvds 13521  df-gcd 13676  df-prm 13749  df-pc 13889  df-struct 14161  df-ndx 14162  df-slot 14163  df-base 14164  df-sets 14165  df-ress 14166  df-plusg 14236  df-mulr 14237  df-starv 14238  df-sca 14239  df-vsca 14240  df-ip 14241  df-tset 14242  df-ple 14243  df-ds 14245  df-unif 14246  df-hom 14247  df-cco 14248  df-rest 14346  df-topn 14347  df-0g 14365  df-gsum 14366  df-topgen 14367  df-pt 14368  df-prds 14371  df-xrs 14425  df-qtop 14430  df-imas 14431  df-divs 14432  df-xps 14433  df-mre 14509  df-mrc 14510  df-acs 14512  df-mnd 15400  df-mhm 15449  df-submnd 15450  df-grp 15527  df-minusg 15528  df-sbg 15529  df-mulg 15530  df-subg 15660  df-nsg 15661  df-eqg 15662  df-ghm 15727  df-cntz 15817  df-od 16014  df-cmn 16261  df-abl 16262  df-mgp 16568  df-rng 16582  df-cring 16583  df-ur 16584  df-oppr 16651  df-dvdsr 16669  df-unit 16670  df-invr 16700  df-dvr 16711  df-rnghom 16742  df-drng 16760  df-subrg 16789  df-lmod 16876  df-lss 16938  df-lsp 16977  df-sra 17177  df-rgmod 17178  df-lidl 17179  df-rsp 17180  df-2idl 17238  df-psmet 17655  df-xmet 17656  df-met 17657  df-bl 17658  df-mopn 17659  df-fbas 17660  df-fg 17661  df-cnfld 17665  df-zring 17728  df-zrh 17779  df-zn 17782  df-top 18347  df-bases 18349  df-topon 18350  df-topsp 18351  df-cld 18467  df-ntr 18468  df-cls 18469  df-nei 18546  df-lp 18584  df-perf 18585  df-cn 18675  df-cnp 18676  df-haus 18763  df-tx 18979  df-hmeo 19172  df-fil 19263  df-fm 19355  df-flim 19356  df-flf 19357  df-xms 19739  df-ms 19740  df-tms 19741  df-cncf 20298  df-limc 21185  df-dv 21186  df-log 21895  df-cxp 21896  df-mu 22325  df-dchr 22459
This theorem is referenced by:  dchrvmasumiflem2  22638  dchrmusumlem  22658
  Copyright terms: Public domain W3C validator