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

Theorem rpvmasum2 20661
Description: A partial result along the lines of rpvmasum 20675. The sum of the von Mangoldt function over those integers  n  ==  A (mod  N) is asymptotic to  ( 1  -  M
) ( log x  /  phi ( x ) )  +  O ( 1 ), where  M is the number of non-principal Dirichlet characters with  sum_ n  e.  NN ,  X ( n )  /  n  =  0. Our goal is to show this set is empty. Equation 9.4.3 of [Shapiro], p. 375. (Contributed by Mario Carneiro, 5-May-2016.)
Hypotheses
Ref Expression
rpvmasum.z  |-  Z  =  (ℤ/n `  N )
rpvmasum.l  |-  L  =  ( ZRHom `  Z
)
rpvmasum.a  |-  ( ph  ->  N  e.  NN )
rpvmasum2.g  |-  G  =  (DChr `  N )
rpvmasum2.d  |-  D  =  ( Base `  G
)
rpvmasum2.1  |-  .1.  =  ( 0g `  G )
rpvmasum2.w  |-  W  =  { y  e.  ( D  \  {  .1.  } )  |  sum_ m  e.  NN  ( ( y `
 ( L `  m ) )  /  m )  =  0 }
rpvmasum2.u  |-  U  =  (Unit `  Z )
rpvmasum2.b  |-  ( ph  ->  A  e.  U )
rpvmasum2.t  |-  T  =  ( `' L " { A } )
rpvmasum2.z1  |-  ( (
ph  /\  f  e.  W )  ->  A  =  ( 1r `  Z ) )
Assertion
Ref Expression
rpvmasum2  |-  ( ph  ->  ( x  e.  RR+  |->  ( ( ( phi `  N )  x.  sum_ n  e.  ( ( 1 ... ( |_ `  x ) )  i^i 
T ) ( (Λ `  n )  /  n
) )  -  (
( log `  x
)  x.  ( 1  -  ( # `  W
) ) ) ) )  e.  O ( 1 ) )
Distinct variable groups:    m, n, x, y, f,  .1.    A, f, m, x, y    f, G    f, N, m, n, x, y    ph, f, m, n, x    T, m, n, x, y    U, m, n, x    f, W, x    f, Z, m, n, x, y    D, f, m, n, x, y   
f, L, m, n, x, y    A, n
Allowed substitution hints:    ph( y)    T( f)    U( y, f)    G( x, y, m, n)    W( y, m, n)

Proof of Theorem rpvmasum2
Dummy variables  c 
t  a are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 rpvmasum.a . . . . . . 7  |-  ( ph  ->  N  e.  NN )
21adantr 451 . . . . . 6  |-  ( (
ph  /\  x  e.  RR+ )  ->  N  e.  NN )
3 rpvmasum2.g . . . . . . 7  |-  G  =  (DChr `  N )
4 rpvmasum2.d . . . . . . 7  |-  D  =  ( Base `  G
)
53, 4dchrfi 20494 . . . . . 6  |-  ( N  e.  NN  ->  D  e.  Fin )
62, 5syl 15 . . . . 5  |-  ( (
ph  /\  x  e.  RR+ )  ->  D  e.  Fin )
7 fzfid 11035 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  (
1 ... ( |_ `  x ) )  e. 
Fin )
8 rpvmasum.z . . . . . . . . . . . . 13  |-  Z  =  (ℤ/n `  N )
9 eqid 2283 . . . . . . . . . . . . 13  |-  ( Base `  Z )  =  (
Base `  Z )
10 simpr 447 . . . . . . . . . . . . 13  |-  ( (
ph  /\  f  e.  D )  ->  f  e.  D )
113, 8, 4, 9, 10dchrf 20481 . . . . . . . . . . . 12  |-  ( (
ph  /\  f  e.  D )  ->  f : ( Base `  Z
) --> CC )
12 rpvmasum2.u . . . . . . . . . . . . . . 15  |-  U  =  (Unit `  Z )
139, 12unitss 15442 . . . . . . . . . . . . . 14  |-  U  C_  ( Base `  Z )
14 rpvmasum2.b . . . . . . . . . . . . . 14  |-  ( ph  ->  A  e.  U )
1513, 14sseldi 3178 . . . . . . . . . . . . 13  |-  ( ph  ->  A  e.  ( Base `  Z ) )
1615adantr 451 . . . . . . . . . . . 12  |-  ( (
ph  /\  f  e.  D )  ->  A  e.  ( Base `  Z
) )
17 ffvelrn 5663 . . . . . . . . . . . 12  |-  ( ( f : ( Base `  Z ) --> CC  /\  A  e.  ( Base `  Z ) )  -> 
( f `  A
)  e.  CC )
1811, 16, 17syl2anc 642 . . . . . . . . . . 11  |-  ( (
ph  /\  f  e.  D )  ->  (
f `  A )  e.  CC )
1918cjcld 11681 . . . . . . . . . 10  |-  ( (
ph  /\  f  e.  D )  ->  (
* `  ( f `  A ) )  e.  CC )
2019adantlr 695 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  (
* `  ( f `  A ) )  e.  CC )
2120adantrl 696 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
n  e.  ( 1 ... ( |_ `  x ) )  /\  f  e.  D )
)  ->  ( * `  ( f `  A
) )  e.  CC )
2211adantlr 695 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  f : ( Base `  Z
) --> CC )
2322adantlr 695 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  f  e.  D
)  ->  f :
( Base `  Z ) --> CC )
241nnnn0d 10018 . . . . . . . . . . . . . . 15  |-  ( ph  ->  N  e.  NN0 )
25 rpvmasum.l . . . . . . . . . . . . . . . 16  |-  L  =  ( ZRHom `  Z
)
268, 9, 25znzrhfo 16501 . . . . . . . . . . . . . . 15  |-  ( N  e.  NN0  ->  L : ZZ -onto-> ( Base `  Z
) )
27 fof 5451 . . . . . . . . . . . . . . 15  |-  ( L : ZZ -onto-> ( Base `  Z )  ->  L : ZZ --> ( Base `  Z
) )
2824, 26, 273syl 18 . . . . . . . . . . . . . 14  |-  ( ph  ->  L : ZZ --> ( Base `  Z ) )
2928adantr 451 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR+ )  ->  L : ZZ
--> ( Base `  Z
) )
30 elfzelz 10798 . . . . . . . . . . . . 13  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  ZZ )
31 ffvelrn 5663 . . . . . . . . . . . . 13  |-  ( ( L : ZZ --> ( Base `  Z )  /\  n  e.  ZZ )  ->  ( L `  n )  e.  ( Base `  Z
) )
3229, 30, 31syl2an 463 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( L `  n )  e.  (
Base `  Z )
)
3332adantr 451 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  f  e.  D
)  ->  ( L `  n )  e.  (
Base `  Z )
)
34 ffvelrn 5663 . . . . . . . . . . 11  |-  ( ( f : ( Base `  Z ) --> CC  /\  ( L `  n )  e.  ( Base `  Z
) )  ->  (
f `  ( L `  n ) )  e.  CC )
3523, 33, 34syl2anc 642 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  f  e.  D
)  ->  ( f `  ( L `  n
) )  e.  CC )
3635anasss 628 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
n  e.  ( 1 ... ( |_ `  x ) )  /\  f  e.  D )
)  ->  ( f `  ( L `  n
) )  e.  CC )
37 elfznn 10819 . . . . . . . . . . . . . 14  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  NN )
3837adantl 452 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  NN )
39 vmacl 20356 . . . . . . . . . . . . 13  |-  ( n  e.  NN  ->  (Λ `  n )  e.  RR )
4038, 39syl 15 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (Λ `  n
)  e.  RR )
4140, 38nndivred 9794 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  /  n
)  e.  RR )
4241recnd 8861 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  /  n
)  e.  CC )
4342adantrr 697 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
n  e.  ( 1 ... ( |_ `  x ) )  /\  f  e.  D )
)  ->  ( (Λ `  n )  /  n
)  e.  CC )
4436, 43mulcld 8855 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
n  e.  ( 1 ... ( |_ `  x ) )  /\  f  e.  D )
)  ->  ( (
f `  ( L `  n ) )  x.  ( (Λ `  n
)  /  n ) )  e.  CC )
4521, 44mulcld 8855 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
n  e.  ( 1 ... ( |_ `  x ) )  /\  f  e.  D )
)  ->  ( (
* `  ( f `  A ) )  x.  ( ( f `  ( L `  n ) )  x.  ( (Λ `  n )  /  n
) ) )  e.  CC )
4645anass1rs 782 . . . . . 6  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  n  e.  (
1 ... ( |_ `  x ) ) )  ->  ( ( * `
 ( f `  A ) )  x.  ( ( f `  ( L `  n ) )  x.  ( (Λ `  n )  /  n
) ) )  e.  CC )
477, 46fsumcl 12206 . . . . 5  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( * `  ( f `  A
) )  x.  (
( f `  ( L `  n )
)  x.  ( (Λ `  n )  /  n
) ) )  e.  CC )
48 relogcl 19932 . . . . . . . . 9  |-  ( x  e.  RR+  ->  ( log `  x )  e.  RR )
4948adantl 452 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( log `  x )  e.  RR )
5049recnd 8861 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( log `  x )  e.  CC )
5150adantr 451 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  ( log `  x )  e.  CC )
52 ax-1cn 8795 . . . . . . 7  |-  1  e.  CC
53 neg1cn 9813 . . . . . . . 8  |-  -u 1  e.  CC
54 0cn 8831 . . . . . . . 8  |-  0  e.  CC
5553, 54keepel 3622 . . . . . . 7  |-  if ( f  e.  W ,  -u 1 ,  0 )  e.  CC
5652, 55keepel 3622 . . . . . 6  |-  if ( f  =  .1.  , 
1 ,  if ( f  e.  W ,  -u 1 ,  0 ) )  e.  CC
57 mulcl 8821 . . . . . 6  |-  ( ( ( log `  x
)  e.  CC  /\  if ( f  =  .1. 
,  1 ,  if ( f  e.  W ,  -u 1 ,  0 ) )  e.  CC )  ->  ( ( log `  x )  x.  if ( f  =  .1. 
,  1 ,  if ( f  e.  W ,  -u 1 ,  0 ) ) )  e.  CC )
5851, 56, 57sylancl 643 . . . . 5  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  (
( log `  x
)  x.  if ( f  =  .1.  , 
1 ,  if ( f  e.  W ,  -u 1 ,  0 ) ) )  e.  CC )
596, 47, 58fsumsub 12250 . . . 4  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ f  e.  D  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( * `  ( f `  A
) )  x.  (
( f `  ( L `  n )
)  x.  ( (Λ `  n )  /  n
) ) )  -  ( ( log `  x
)  x.  if ( f  =  .1.  , 
1 ,  if ( f  e.  W ,  -u 1 ,  0 ) ) ) )  =  ( sum_ f  e.  D  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( * `  (
f `  A )
)  x.  ( ( f `  ( L `
 n ) )  x.  ( (Λ `  n
)  /  n ) ) )  -  sum_ f  e.  D  (
( log `  x
)  x.  if ( f  =  .1.  , 
1 ,  if ( f  e.  W ,  -u 1 ,  0 ) ) ) ) )
6044anass1rs 782 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  n  e.  (
1 ... ( |_ `  x ) ) )  ->  ( ( f `
 ( L `  n ) )  x.  ( (Λ `  n
)  /  n ) )  e.  CC )
617, 60fsumcl 12206 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( f `  ( L `  n ) )  x.  ( (Λ `  n )  /  n
) )  e.  CC )
6220, 61, 58subdid 9235 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  (
( * `  (
f `  A )
)  x.  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( f `  ( L `
 n ) )  x.  ( (Λ `  n
)  /  n ) )  -  ( ( log `  x )  x.  if ( f  =  .1.  ,  1 ,  if ( f  e.  W ,  -u
1 ,  0 ) ) ) ) )  =  ( ( ( * `  ( f `
 A ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( f `  ( L `  n ) )  x.  ( (Λ `  n )  /  n
) ) )  -  ( ( * `  ( f `  A
) )  x.  (
( log `  x
)  x.  if ( f  =  .1.  , 
1 ,  if ( f  e.  W ,  -u 1 ,  0 ) ) ) ) ) )
637, 20, 60fsummulc2 12246 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  (
( * `  (
f `  A )
)  x.  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( f `  ( L `  n ) )  x.  ( (Λ `  n )  /  n
) ) )  = 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( * `  (
f `  A )
)  x.  ( ( f `  ( L `
 n ) )  x.  ( (Λ `  n
)  /  n ) ) ) )
6456a1i 10 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  if ( f  =  .1. 
,  1 ,  if ( f  e.  W ,  -u 1 ,  0 ) )  e.  CC )
6520, 51, 64mul12d 9021 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  (
( * `  (
f `  A )
)  x.  ( ( log `  x )  x.  if ( f  =  .1.  ,  1 ,  if ( f  e.  W ,  -u
1 ,  0 ) ) ) )  =  ( ( log `  x
)  x.  ( ( * `  ( f `
 A ) )  x.  if ( f  =  .1.  ,  1 ,  if ( f  e.  W ,  -u
1 ,  0 ) ) ) ) )
66 oveq2 5866 . . . . . . . . . . 11  |-  ( if ( f  =  .1. 
,  1 ,  if ( f  e.  W ,  -u 1 ,  0 ) )  =  1  ->  ( ( * `
 ( f `  A ) )  x.  if ( f  =  .1.  ,  1 ,  if ( f  e.  W ,  -u 1 ,  0 ) ) )  =  ( ( * `  ( f `
 A ) )  x.  1 ) )
67 oveq2 5866 . . . . . . . . . . 11  |-  ( if ( f  =  .1. 
,  1 ,  if ( f  e.  W ,  -u 1 ,  0 ) )  =  if ( f  e.  W ,  -u 1 ,  0 )  ->  ( (
* `  ( f `  A ) )  x.  if ( f  =  .1.  ,  1 ,  if ( f  e.  W ,  -u 1 ,  0 ) ) )  =  ( ( * `  ( f `
 A ) )  x.  if ( f  e.  W ,  -u
1 ,  0 ) ) )
6866, 67ifsb 3574 . . . . . . . . . 10  |-  ( ( * `  ( f `
 A ) )  x.  if ( f  =  .1.  ,  1 ,  if ( f  e.  W ,  -u
1 ,  0 ) ) )  =  if ( f  =  .1. 
,  ( ( * `
 ( f `  A ) )  x.  1 ) ,  ( ( * `  (
f `  A )
)  x.  if ( f  e.  W ,  -u 1 ,  0 ) ) )
69 fveq1 5524 . . . . . . . . . . . . . . . . 17  |-  ( f  =  .1.  ->  (
f `  A )  =  (  .1.  `  A
) )
70 rpvmasum2.1 . . . . . . . . . . . . . . . . . 18  |-  .1.  =  ( 0g `  G )
711ad2antrr 706 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  N  e.  NN )
7214ad2antrr 706 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  A  e.  U )
733, 8, 70, 12, 71, 72dchr1 20496 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  (  .1.  `  A )  =  1 )
7469, 73sylan9eqr 2337 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  f  =  .1.  )  ->  ( f `  A )  =  1 )
7574fveq2d 5529 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  f  =  .1.  )  ->  ( * `  ( f `  A
) )  =  ( * `  1 ) )
76 1re 8837 . . . . . . . . . . . . . . . 16  |-  1  e.  RR
77 cjre 11624 . . . . . . . . . . . . . . . 16  |-  ( 1  e.  RR  ->  (
* `  1 )  =  1 )
7876, 77ax-mp 8 . . . . . . . . . . . . . . 15  |-  ( * `
 1 )  =  1
7975, 78syl6eq 2331 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  f  =  .1.  )  ->  ( * `  ( f `  A
) )  =  1 )
8079oveq1d 5873 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  f  =  .1.  )  ->  ( ( * `
 ( f `  A ) )  x.  1 )  =  ( 1  x.  1 ) )
81 1t1e1 9870 . . . . . . . . . . . . 13  |-  ( 1  x.  1 )  =  1
8280, 81syl6eq 2331 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  f  =  .1.  )  ->  ( ( * `
 ( f `  A ) )  x.  1 )  =  1 )
8382ifeq1da 3590 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  if ( f  =  .1. 
,  ( ( * `
 ( f `  A ) )  x.  1 ) ,  ( ( * `  (
f `  A )
)  x.  if ( f  e.  W ,  -u 1 ,  0 ) ) )  =  if ( f  =  .1. 
,  1 ,  ( ( * `  (
f `  A )
)  x.  if ( f  e.  W ,  -u 1 ,  0 ) ) ) )
84 df-ne 2448 . . . . . . . . . . . . 13  |-  ( f  =/=  .1.  <->  -.  f  =  .1.  )
85 oveq2 5866 . . . . . . . . . . . . . . 15  |-  ( if ( f  e.  W ,  -u 1 ,  0 )  =  -u 1  ->  ( ( * `  ( f `  A
) )  x.  if ( f  e.  W ,  -u 1 ,  0 ) )  =  ( ( * `  (
f `  A )
)  x.  -u 1
) )
86 oveq2 5866 . . . . . . . . . . . . . . 15  |-  ( if ( f  e.  W ,  -u 1 ,  0 )  =  0  -> 
( ( * `  ( f `  A
) )  x.  if ( f  e.  W ,  -u 1 ,  0 ) )  =  ( ( * `  (
f `  A )
)  x.  0 ) )
8785, 86ifsb 3574 . . . . . . . . . . . . . 14  |-  ( ( * `  ( f `
 A ) )  x.  if ( f  e.  W ,  -u
1 ,  0 ) )  =  if ( f  e.  W , 
( ( * `  ( f `  A
) )  x.  -u 1
) ,  ( ( * `  ( f `
 A ) )  x.  0 ) )
88 simplll 734 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  f  =/=  .1.  )  ->  ph )
89 rpvmasum2.z1 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  f  e.  W )  ->  A  =  ( 1r `  Z ) )
9089fveq2d 5529 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  f  e.  W )  ->  (
f `  A )  =  ( f `  ( 1r `  Z ) ) )
9188, 90sylan 457 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D
)  /\  f  =/=  .1.  )  /\  f  e.  W )  ->  (
f `  A )  =  ( f `  ( 1r `  Z ) ) )
923, 8, 4dchrmhm 20480 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  D  C_  ( (mulGrp `  Z ) MndHom  (mulGrp ` fld ) )
93 simpr 447 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  f  e.  D )
9492, 93sseldi 3178 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  f  e.  ( (mulGrp `  Z
) MndHom  (mulGrp ` fld ) ) )
95 eqid 2283 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  (mulGrp `  Z )  =  (mulGrp `  Z )
96 eqid 2283 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 1r
`  Z )  =  ( 1r `  Z
)
9795, 96rngidval 15343 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 1r
`  Z )  =  ( 0g `  (mulGrp `  Z ) )
98 eqid 2283 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  (mulGrp ` fld )  =  (mulGrp ` fld )
99 cnfld1 16399 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  1  =  ( 1r ` fld )
10098, 99rngidval 15343 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  1  =  ( 0g `  (mulGrp ` fld ) )
10197, 100mhm0 14423 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( f  e.  ( (mulGrp `  Z ) MndHom  (mulGrp ` fld ) )  ->  (
f `  ( 1r `  Z ) )  =  1 )
10294, 101syl 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  (
f `  ( 1r `  Z ) )  =  1 )
103102ad2antrr 706 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D
)  /\  f  =/=  .1.  )  /\  f  e.  W )  ->  (
f `  ( 1r `  Z ) )  =  1 )
10491, 103eqtrd 2315 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D
)  /\  f  =/=  .1.  )  /\  f  e.  W )  ->  (
f `  A )  =  1 )
105104fveq2d 5529 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D
)  /\  f  =/=  .1.  )  /\  f  e.  W )  ->  (
* `  ( f `  A ) )  =  ( * `  1
) )
106105, 78syl6eq 2331 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D
)  /\  f  =/=  .1.  )  /\  f  e.  W )  ->  (
* `  ( f `  A ) )  =  1 )
107106oveq1d 5873 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D
)  /\  f  =/=  .1.  )  /\  f  e.  W )  ->  (
( * `  (
f `  A )
)  x.  -u 1
)  =  ( 1  x.  -u 1 ) )
10853mulid2i 8840 . . . . . . . . . . . . . . . . 17  |-  ( 1  x.  -u 1 )  = 
-u 1
109107, 108syl6eq 2331 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D
)  /\  f  =/=  .1.  )  /\  f  e.  W )  ->  (
( * `  (
f `  A )
)  x.  -u 1
)  =  -u 1
)
110109ifeq1da 3590 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  f  =/=  .1.  )  ->  if ( f  e.  W ,  ( ( * `  (
f `  A )
)  x.  -u 1
) ,  ( ( * `  ( f `
 A ) )  x.  0 ) )  =  if ( f  e.  W ,  -u
1 ,  ( ( * `  ( f `
 A ) )  x.  0 ) ) )
11120adantr 451 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  f  =/=  .1.  )  ->  ( * `  ( f `  A
) )  e.  CC )
112111mul01d 9011 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  f  =/=  .1.  )  ->  ( ( * `
 ( f `  A ) )  x.  0 )  =  0 )
113112ifeq2d 3580 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  f  =/=  .1.  )  ->  if ( f  e.  W ,  -u
1 ,  ( ( * `  ( f `
 A ) )  x.  0 ) )  =  if ( f  e.  W ,  -u
1 ,  0 ) )
114110, 113eqtrd 2315 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  f  =/=  .1.  )  ->  if ( f  e.  W ,  ( ( * `  (
f `  A )
)  x.  -u 1
) ,  ( ( * `  ( f `
 A ) )  x.  0 ) )  =  if ( f  e.  W ,  -u
1 ,  0 ) )
11587, 114syl5eq 2327 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  f  =/=  .1.  )  ->  ( ( * `
 ( f `  A ) )  x.  if ( f  e.  W ,  -u 1 ,  0 ) )  =  if ( f  e.  W ,  -u
1 ,  0 ) )
11684, 115sylan2br 462 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  -.  f  =  .1.  )  ->  ( (
* `  ( f `  A ) )  x.  if ( f  e.  W ,  -u 1 ,  0 ) )  =  if ( f  e.  W ,  -u
1 ,  0 ) )
117116ifeq2da 3591 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  if ( f  =  .1. 
,  1 ,  ( ( * `  (
f `  A )
)  x.  if ( f  e.  W ,  -u 1 ,  0 ) ) )  =  if ( f  =  .1. 
,  1 ,  if ( f  e.  W ,  -u 1 ,  0 ) ) )
11883, 117eqtrd 2315 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  if ( f  =  .1. 
,  ( ( * `
 ( f `  A ) )  x.  1 ) ,  ( ( * `  (
f `  A )
)  x.  if ( f  e.  W ,  -u 1 ,  0 ) ) )  =  if ( f  =  .1. 
,  1 ,  if ( f  e.  W ,  -u 1 ,  0 ) ) )
11968, 118syl5eq 2327 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  (
( * `  (
f `  A )
)  x.  if ( f  =  .1.  , 
1 ,  if ( f  e.  W ,  -u 1 ,  0 ) ) )  =  if ( f  =  .1. 
,  1 ,  if ( f  e.  W ,  -u 1 ,  0 ) ) )
120119oveq2d 5874 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  (
( log `  x
)  x.  ( ( * `  ( f `
 A ) )  x.  if ( f  =  .1.  ,  1 ,  if ( f  e.  W ,  -u
1 ,  0 ) ) ) )  =  ( ( log `  x
)  x.  if ( f  =  .1.  , 
1 ,  if ( f  e.  W ,  -u 1 ,  0 ) ) ) )
12165, 120eqtrd 2315 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  (
( * `  (
f `  A )
)  x.  ( ( log `  x )  x.  if ( f  =  .1.  ,  1 ,  if ( f  e.  W ,  -u
1 ,  0 ) ) ) )  =  ( ( log `  x
)  x.  if ( f  =  .1.  , 
1 ,  if ( f  e.  W ,  -u 1 ,  0 ) ) ) )
12263, 121oveq12d 5876 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  (
( ( * `  ( f `  A
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( f `  ( L `
 n ) )  x.  ( (Λ `  n
)  /  n ) ) )  -  (
( * `  (
f `  A )
)  x.  ( ( log `  x )  x.  if ( f  =  .1.  ,  1 ,  if ( f  e.  W ,  -u
1 ,  0 ) ) ) ) )  =  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( * `  ( f `  A
) )  x.  (
( f `  ( L `  n )
)  x.  ( (Λ `  n )  /  n
) ) )  -  ( ( log `  x
)  x.  if ( f  =  .1.  , 
1 ,  if ( f  e.  W ,  -u 1 ,  0 ) ) ) ) )
12362, 122eqtrd 2315 . . . . 5  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  (
( * `  (
f `  A )
)  x.  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( f `  ( L `
 n ) )  x.  ( (Λ `  n
)  /  n ) )  -  ( ( log `  x )  x.  if ( f  =  .1.  ,  1 ,  if ( f  e.  W ,  -u
1 ,  0 ) ) ) ) )  =  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( * `  ( f `  A
) )  x.  (
( f `  ( L `  n )
)  x.  ( (Λ `  n )  /  n
) ) )  -  ( ( log `  x
)  x.  if ( f  =  .1.  , 
1 ,  if ( f  e.  W ,  -u 1 ,  0 ) ) ) ) )
124123sumeq2dv 12176 . . . 4  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ f  e.  D  ( ( * `
 ( f `  A ) )  x.  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( f `  ( L `  n ) )  x.  ( (Λ `  n )  /  n
) )  -  (
( log `  x
)  x.  if ( f  =  .1.  , 
1 ,  if ( f  e.  W ,  -u 1 ,  0 ) ) ) ) )  =  sum_ f  e.  D  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( * `  ( f `  A
) )  x.  (
( f `  ( L `  n )
)  x.  ( (Λ `  n )  /  n
) ) )  -  ( ( log `  x
)  x.  if ( f  =  .1.  , 
1 ,  if ( f  e.  W ,  -u 1 ,  0 ) ) ) ) )
125 fzfid 11035 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( 1 ... ( |_ `  x ) )  e. 
Fin )
126 inss1 3389 . . . . . . . . 9  |-  ( ( 1 ... ( |_
`  x ) )  i^i  T )  C_  ( 1 ... ( |_ `  x ) )
127 ssfi 7083 . . . . . . . . 9  |-  ( ( ( 1 ... ( |_ `  x ) )  e.  Fin  /\  (
( 1 ... ( |_ `  x ) )  i^i  T )  C_  ( 1 ... ( |_ `  x ) ) )  ->  ( (
1 ... ( |_ `  x ) )  i^i 
T )  e.  Fin )
128125, 126, 127sylancl 643 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( (
1 ... ( |_ `  x ) )  i^i 
T )  e.  Fin )
1292phicld 12840 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( phi `  N )  e.  NN )
130129nncnd 9762 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( phi `  N )  e.  CC )
131126a1i 10 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( (
1 ... ( |_ `  x ) )  i^i 
T )  C_  (
1 ... ( |_ `  x ) ) )
132131sselda 3180 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( ( 1 ... ( |_ `  x
) )  i^i  T
) )  ->  n  e.  ( 1 ... ( |_ `  x ) ) )
133132, 42syldan 456 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( ( 1 ... ( |_ `  x
) )  i^i  T
) )  ->  (
(Λ `  n )  /  n )  e.  CC )
134128, 130, 133fsummulc2 12246 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( phi `  N )  x. 
sum_ n  e.  (
( 1 ... ( |_ `  x ) )  i^i  T ) ( (Λ `  n )  /  n ) )  = 
sum_ n  e.  (
( 1 ... ( |_ `  x ) )  i^i  T ) ( ( phi `  N
)  x.  ( (Λ `  n )  /  n
) ) )
135130adantr 451 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( phi `  N )  e.  CC )
136135, 42mulcld 8855 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( phi `  N )  x.  ( (Λ `  n
)  /  n ) )  e.  CC )
137132, 136syldan 456 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( ( 1 ... ( |_ `  x
) )  i^i  T
) )  ->  (
( phi `  N
)  x.  ( (Λ `  n )  /  n
) )  e.  CC )
138137ralrimiva 2626 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  A. n  e.  ( ( 1 ... ( |_ `  x
) )  i^i  T
) ( ( phi `  N )  x.  (
(Λ `  n )  /  n ) )  e.  CC )
139125olcd 382 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( (
1 ... ( |_ `  x ) )  C_  ( ZZ>= `  1 )  \/  ( 1 ... ( |_ `  x ) )  e.  Fin ) )
140 sumss2 12199 . . . . . . . 8  |-  ( ( ( ( ( 1 ... ( |_ `  x ) )  i^i 
T )  C_  (
1 ... ( |_ `  x ) )  /\  A. n  e.  ( ( 1 ... ( |_
`  x ) )  i^i  T ) ( ( phi `  N
)  x.  ( (Λ `  n )  /  n
) )  e.  CC )  /\  ( ( 1 ... ( |_ `  x ) )  C_  ( ZZ>= `  1 )  \/  ( 1 ... ( |_ `  x ) )  e.  Fin ) )  ->  sum_ n  e.  ( ( 1 ... ( |_ `  x ) )  i^i  T ) ( ( phi `  N
)  x.  ( (Λ `  n )  /  n
) )  =  sum_ n  e.  ( 1 ... ( |_ `  x
) ) if ( n  e.  ( ( 1 ... ( |_
`  x ) )  i^i  T ) ,  ( ( phi `  N )  x.  (
(Λ `  n )  /  n ) ) ,  0 ) )
141131, 138, 139, 140syl21anc 1181 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ n  e.  ( ( 1 ... ( |_ `  x
) )  i^i  T
) ( ( phi `  N )  x.  (
(Λ `  n )  /  n ) )  = 
sum_ n  e.  (
1 ... ( |_ `  x ) ) if ( n  e.  ( ( 1 ... ( |_ `  x ) )  i^i  T ) ,  ( ( phi `  N )  x.  (
(Λ `  n )  /  n ) ) ,  0 ) )
142 elin 3358 . . . . . . . . . . . . 13  |-  ( n  e.  ( ( 1 ... ( |_ `  x ) )  i^i 
T )  <->  ( n  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  T
) )
143142baib 871 . . . . . . . . . . . 12  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  (
n  e.  ( ( 1 ... ( |_
`  x ) )  i^i  T )  <->  n  e.  T ) )
144143adantl 452 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  e.  ( ( 1 ... ( |_ `  x
) )  i^i  T
)  <->  n  e.  T
) )
145 rpvmasum2.t . . . . . . . . . . . . 13  |-  T  =  ( `' L " { A } )
146145eleq2i 2347 . . . . . . . . . . . 12  |-  ( n  e.  T  <->  n  e.  ( `' L " { A } ) )
147 ffn 5389 . . . . . . . . . . . . . 14  |-  ( L : ZZ --> ( Base `  Z )  ->  L  Fn  ZZ )
14829, 147syl 15 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR+ )  ->  L  Fn  ZZ )
149 fniniseg 5646 . . . . . . . . . . . . . 14  |-  ( L  Fn  ZZ  ->  (
n  e.  ( `' L " { A } )  <->  ( n  e.  ZZ  /\  ( L `
 n )  =  A ) ) )
150149baibd 875 . . . . . . . . . . . . 13  |-  ( ( L  Fn  ZZ  /\  n  e.  ZZ )  ->  ( n  e.  ( `' L " { A } )  <->  ( L `  n )  =  A ) )
151148, 30, 150syl2an 463 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  e.  ( `' L " { A } )  <->  ( L `  n )  =  A ) )
152146, 151syl5bb 248 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  e.  T  <->  ( L `  n )  =  A ) )
153144, 152bitr2d 245 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( L `  n )  =  A  <->  n  e.  (
( 1 ... ( |_ `  x ) )  i^i  T ) ) )
15442mul02d 9010 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 0  x.  ( (Λ `  n
)  /  n ) )  =  0 )
155153, 154ifbieq2d 3585 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  if (
( L `  n
)  =  A , 
( ( phi `  N )  x.  (
(Λ `  n )  /  n ) ) ,  ( 0  x.  (
(Λ `  n )  /  n ) ) )  =  if ( n  e.  ( ( 1 ... ( |_ `  x ) )  i^i 
T ) ,  ( ( phi `  N
)  x.  ( (Λ `  n )  /  n
) ) ,  0 ) )
156 oveq1 5865 . . . . . . . . . . 11  |-  ( if ( ( L `  n )  =  A ,  ( phi `  N ) ,  0 )  =  ( phi `  N )  ->  ( if ( ( L `  n )  =  A ,  ( phi `  N ) ,  0 )  x.  ( (Λ `  n )  /  n
) )  =  ( ( phi `  N
)  x.  ( (Λ `  n )  /  n
) ) )
157 oveq1 5865 . . . . . . . . . . 11  |-  ( if ( ( L `  n )  =  A ,  ( phi `  N ) ,  0 )  =  0  -> 
( if ( ( L `  n )  =  A ,  ( phi `  N ) ,  0 )  x.  ( (Λ `  n
)  /  n ) )  =  ( 0  x.  ( (Λ `  n
)  /  n ) ) )
158156, 157ifsb 3574 . . . . . . . . . 10  |-  ( if ( ( L `  n )  =  A ,  ( phi `  N ) ,  0 )  x.  ( (Λ `  n )  /  n
) )  =  if ( ( L `  n )  =  A ,  ( ( phi `  N )  x.  (
(Λ `  n )  /  n ) ) ,  ( 0  x.  (
(Λ `  n )  /  n ) ) )
1591ad2antrr 706 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  N  e.  NN )
160159, 5syl 15 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  D  e.  Fin )
16120adantlr 695 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  f  e.  D
)  ->  ( * `  ( f `  A
) )  e.  CC )
16235, 161mulcld 8855 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  f  e.  D
)  ->  ( (
f `  ( L `  n ) )  x.  ( * `  (
f `  A )
) )  e.  CC )
163160, 42, 162fsummulc1 12247 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( sum_ f  e.  D  (
( f `  ( L `  n )
)  x.  ( * `
 ( f `  A ) ) )  x.  ( (Λ `  n
)  /  n ) )  =  sum_ f  e.  D  ( (
( f `  ( L `  n )
)  x.  ( * `
 ( f `  A ) ) )  x.  ( (Λ `  n
)  /  n ) ) )
16414ad2antrr 706 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  A  e.  U )
1653, 4, 8, 9, 12, 159, 32, 164sum2dchr 20513 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  sum_ f  e.  D  ( ( f `
 ( L `  n ) )  x.  ( * `  (
f `  A )
) )  =  if ( ( L `  n )  =  A ,  ( phi `  N ) ,  0 ) )
166165oveq1d 5873 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( sum_ f  e.  D  (
( f `  ( L `  n )
)  x.  ( * `
 ( f `  A ) ) )  x.  ( (Λ `  n
)  /  n ) )  =  ( if ( ( L `  n )  =  A ,  ( phi `  N ) ,  0 )  x.  ( (Λ `  n )  /  n
) ) )
16742adantr 451 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  f  e.  D
)  ->  ( (Λ `  n )  /  n
)  e.  CC )
168 mulass 8825 . . . . . . . . . . . . . 14  |-  ( ( ( f `  ( L `  n )
)  e.  CC  /\  ( * `  (
f `  A )
)  e.  CC  /\  ( (Λ `  n )  /  n )  e.  CC )  ->  ( ( ( f `  ( L `
 n ) )  x.  ( * `  ( f `  A
) ) )  x.  ( (Λ `  n
)  /  n ) )  =  ( ( f `  ( L `
 n ) )  x.  ( ( * `
 ( f `  A ) )  x.  ( (Λ `  n
)  /  n ) ) ) )
169 mul12 8978 . . . . . . . . . . . . . 14  |-  ( ( ( f `  ( L `  n )
)  e.  CC  /\  ( * `  (
f `  A )
)  e.  CC  /\  ( (Λ `  n )  /  n )  e.  CC )  ->  ( ( f `
 ( L `  n ) )  x.  ( ( * `  ( f `  A
) )  x.  (
(Λ `  n )  /  n ) ) )  =  ( ( * `
 ( f `  A ) )  x.  ( ( f `  ( L `  n ) )  x.  ( (Λ `  n )  /  n
) ) ) )
170168, 169eqtrd 2315 . . . . . . . . . . . . 13  |-  ( ( ( f `  ( L `  n )
)  e.  CC  /\  ( * `  (
f `  A )
)  e.  CC  /\  ( (Λ `  n )  /  n )  e.  CC )  ->  ( ( ( f `  ( L `
 n ) )  x.  ( * `  ( f `  A
) ) )  x.  ( (Λ `  n
)  /  n ) )  =  ( ( * `  ( f `
 A ) )  x.  ( ( f `
 ( L `  n ) )  x.  ( (Λ `  n
)  /  n ) ) ) )
17135, 161, 167, 170syl3anc 1182 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  f  e.  D
)  ->  ( (
( f `  ( L `  n )
)  x.  ( * `
 ( f `  A ) ) )  x.  ( (Λ `  n
)  /  n ) )  =  ( ( * `  ( f `
 A ) )  x.  ( ( f `
 ( L `  n ) )  x.  ( (Λ `  n
)  /  n ) ) ) )
172171sumeq2dv 12176 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  sum_ f  e.  D  ( ( ( f `  ( L `
 n ) )  x.  ( * `  ( f `  A
) ) )  x.  ( (Λ `  n
)  /  n ) )  =  sum_ f  e.  D  ( (
* `  ( f `  A ) )  x.  ( ( f `  ( L `  n ) )  x.  ( (Λ `  n )  /  n
) ) ) )
173163, 166, 1723eqtr3d 2323 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( if ( ( L `  n )  =  A ,  ( phi `  N ) ,  0 )  x.  ( (Λ `  n )  /  n
) )  =  sum_ f  e.  D  (
( * `  (
f `  A )
)  x.  ( ( f `  ( L `
 n ) )  x.  ( (Λ `  n
)  /  n ) ) ) )
174158, 173syl5eqr 2329 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  if (
( L `  n
)  =  A , 
( ( phi `  N )  x.  (
(Λ `  n )  /  n ) ) ,  ( 0  x.  (
(Λ `  n )  /  n ) ) )  =  sum_ f  e.  D  ( ( * `  ( f `  A
) )  x.  (
( f `  ( L `  n )
)  x.  ( (Λ `  n )  /  n
) ) ) )
175155, 174eqtr3d 2317 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  if (
n  e.  ( ( 1 ... ( |_
`  x ) )  i^i  T ) ,  ( ( phi `  N )  x.  (
(Λ `  n )  /  n ) ) ,  0 )  =  sum_ f  e.  D  (
( * `  (
f `  A )
)  x.  ( ( f `  ( L `
 n ) )  x.  ( (Λ `  n
)  /  n ) ) ) )
176175sumeq2dv 12176 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) if ( n  e.  ( ( 1 ... ( |_ `  x
) )  i^i  T
) ,  ( ( phi `  N )  x.  ( (Λ `  n
)  /  n ) ) ,  0 )  =  sum_ n  e.  ( 1 ... ( |_
`  x ) )
sum_ f  e.  D  ( ( * `  ( f `  A
) )  x.  (
( f `  ( L `  n )
)  x.  ( (Λ `  n )  /  n
) ) ) )
177134, 141, 1763eqtrd 2319 . . . . . 6  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( phi `  N )  x. 
sum_ n  e.  (
( 1 ... ( |_ `  x ) )  i^i  T ) ( (Λ `  n )  /  n ) )  = 
sum_ n  e.  (
1 ... ( |_ `  x ) ) sum_ f  e.  D  (
( * `  (
f `  A )
)  x.  ( ( f `  ( L `
 n ) )  x.  ( (Λ `  n
)  /  n ) ) ) )
178125, 6, 45fsumcom 12238 . . . . . 6  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) )
sum_ f  e.  D  ( ( * `  ( f `  A
) )  x.  (
( f `  ( L `  n )
)  x.  ( (Λ `  n )  /  n
) ) )  = 
sum_ f  e.  D  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( * `  (
f `  A )
)  x.  ( ( f `  ( L `
 n ) )  x.  ( (Λ `  n
)  /  n ) ) ) )
179177, 178eqtrd 2315 . . . . 5  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( phi `  N )  x. 
sum_ n  e.  (
( 1 ... ( |_ `  x ) )  i^i  T ) ( (Λ `  n )  /  n ) )  = 
sum_ f  e.  D  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( * `  (
f `  A )
)  x.  ( ( f `  ( L `
 n ) )  x.  ( (Λ `  n
)  /  n ) ) ) )
1803dchrabl 20493 . . . . . . . . . . 11  |-  ( N  e.  NN  ->  G  e.  Abel )
181 ablgrp 15094 . . . . . . . . . . 11  |-  ( G  e.  Abel  ->  G  e. 
Grp )
1822, 180, 1813syl 18 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR+ )  ->  G  e.  Grp )
1834, 70grpidcl 14510 . . . . . . . . . 10  |-  ( G  e.  Grp  ->  .1.  e.  D )
184182, 183syl 15 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR+ )  ->  .1.  e.  D )
18550mulid1d 8852 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( log `  x )  x.  1 )  =  ( log `  x ) )
186185, 50eqeltrd 2357 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( log `  x )  x.  1 )  e.  CC )
187 iftrue 3571 . . . . . . . . . . 11  |-  ( f  =  .1.  ->  if ( f  =  .1. 
,  1 ,  if ( f  e.  W ,  -u 1 ,  0 ) )  =  1 )
188187oveq2d 5874 . . . . . . . . . 10  |-  ( f  =  .1.  ->  (
( log `  x
)  x.  if ( f  =  .1.  , 
1 ,  if ( f  e.  W ,  -u 1 ,  0 ) ) )  =  ( ( log `  x
)  x.  1 ) )
189188sumsn 12213 . . . . . . . . 9  |-  ( (  .1.  e.  D  /\  ( ( log `  x
)  x.  1 )  e.  CC )  ->  sum_ f  e.  {  .1.  }  ( ( log `  x
)  x.  if ( f  =  .1.  , 
1 ,  if ( f  e.  W ,  -u 1 ,  0 ) ) )  =  ( ( log `  x
)  x.  1 ) )
190184, 186, 189syl2anc 642 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ f  e. 
{  .1.  }  (
( log `  x
)  x.  if ( f  =  .1.  , 
1 ,  if ( f  e.  W ,  -u 1 ,  0 ) ) )  =  ( ( log `  x
)  x.  1 ) )
191 eldifsn 3749 . . . . . . . . . . 11  |-  ( f  e.  ( D  \  {  .1.  } )  <->  ( f  e.  D  /\  f  =/=  .1.  ) )
192 ifnefalse 3573 . . . . . . . . . . . . . . 15  |-  ( f  =/=  .1.  ->  if ( f  =  .1. 
,  1 ,  if ( f  e.  W ,  -u 1 ,  0 ) )  =  if ( f  e.  W ,  -u 1 ,  0 ) )
193192ad2antll 709 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
f  e.  D  /\  f  =/=  .1.  ) )  ->  if ( f  =  .1.  ,  1 ,  if ( f  e.  W ,  -u
1 ,  0 ) )  =  if ( f  e.  W ,  -u 1 ,  0 ) )
194 negeq 9044 . . . . . . . . . . . . . . 15  |-  ( if ( f  e.  W ,  1 ,  0 )  =  1  ->  -u if ( f  e.  W ,  1 ,  0 )  =  -u
1 )
195 negeq 9044 . . . . . . . . . . . . . . . 16  |-  ( if ( f  e.  W ,  1 ,  0 )  =  0  ->  -u if ( f  e.  W ,  1 ,  0 )  =  -u
0 )
196 neg0 9093 . . . . . . . . . . . . . . . 16  |-  -u 0  =  0
197195, 196syl6eq 2331 . . . . . . . . . . . . . . 15  |-  ( if ( f  e.  W ,  1 ,  0 )  =  0  ->  -u if ( f  e.  W ,  1 ,  0 )  =  0 )
198194, 197ifsb 3574 . . . . . . . . . . . . . 14  |-  -u if ( f  e.  W ,  1 ,  0 )  =  if ( f  e.  W ,  -u 1 ,  0 )
199193, 198syl6eqr 2333 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
f  e.  D  /\  f  =/=  .1.  ) )  ->  if ( f  =  .1.  ,  1 ,  if ( f  e.  W ,  -u
1 ,  0 ) )  =  -u if ( f  e.  W ,  1 ,  0 ) )
200199oveq2d 5874 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
f  e.  D  /\  f  =/=  .1.  ) )  ->  ( ( log `  x )  x.  if ( f  =  .1. 
,  1 ,  if ( f  e.  W ,  -u 1 ,  0 ) ) )  =  ( ( log `  x
)  x.  -u if ( f  e.  W ,  1 ,  0 ) ) )
20150adantr 451 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
f  e.  D  /\  f  =/=  .1.  ) )  ->  ( log `  x
)  e.  CC )
20252, 54keepel 3622 . . . . . . . . . . . . 13  |-  if ( f  e.  W , 
1 ,  0 )  e.  CC
203 mulneg2 9217 . . . . . . . . . . . . 13  |-  ( ( ( log `  x
)  e.  CC  /\  if ( f  e.  W ,  1 ,  0 )  e.  CC )  ->  ( ( log `  x )  x.  -u if ( f  e.  W ,  1 ,  0 ) )  =  -u ( ( log `  x
)  x.  if ( f  e.  W , 
1 ,  0 ) ) )
204201, 202, 203sylancl 643 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
f  e.  D  /\  f  =/=  .1.  ) )  ->  ( ( log `  x )  x.  -u if ( f  e.  W ,  1 ,  0 ) )  =  -u ( ( log `  x
)  x.  if ( f  e.  W , 
1 ,  0 ) ) )
205200, 204eqtrd 2315 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
f  e.  D  /\  f  =/=  .1.  ) )  ->  ( ( log `  x )  x.  if ( f  =  .1. 
,  1 ,  if ( f  e.  W ,  -u 1 ,  0 ) ) )  = 
-u ( ( log `  x )  x.  if ( f  e.  W ,  1 ,  0 ) ) )
206191, 205sylan2b 461 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  ( D  \  {  .1.  } ) )  -> 
( ( log `  x
)  x.  if ( f  =  .1.  , 
1 ,  if ( f  e.  W ,  -u 1 ,  0 ) ) )  =  -u ( ( log `  x
)  x.  if ( f  e.  W , 
1 ,  0 ) ) )
207206sumeq2dv 12176 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ f  e.  ( D  \  {  .1.  } ) ( ( log `  x )  x.  if ( f  =  .1.  ,  1 ,  if ( f  e.  W ,  -u
1 ,  0 ) ) )  =  sum_ f  e.  ( D  \  {  .1.  } )
-u ( ( log `  x )  x.  if ( f  e.  W ,  1 ,  0 ) ) )
208 diffi 7089 . . . . . . . . . . 11  |-  ( D  e.  Fin  ->  ( D  \  {  .1.  }
)  e.  Fin )
2096, 208syl 15 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( D  \  {  .1.  } )  e.  Fin )
21050adantr 451 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  ( D  \  {  .1.  } ) )  -> 
( log `  x
)  e.  CC )
211 mulcl 8821 . . . . . . . . . . 11  |-  ( ( ( log `  x
)  e.  CC  /\  if ( f  e.  W ,  1 ,  0 )  e.  CC )  ->  ( ( log `  x )  x.  if ( f  e.  W ,  1 ,  0 ) )  e.  CC )
212210, 202, 211sylancl 643 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  ( D  \  {  .1.  } ) )  -> 
( ( log `  x
)  x.  if ( f  e.  W , 
1 ,  0 ) )  e.  CC )
213209, 212fsumneg 12249 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ f  e.  ( D  \  {  .1.  } ) -u (
( log `  x
)  x.  if ( f  e.  W , 
1 ,  0 ) )  =  -u sum_ f  e.  ( D  \  {  .1.  } ) ( ( log `  x )  x.  if ( f  e.  W ,  1 ,  0 ) ) )
214202a1i 10 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  ( D  \  {  .1.  } ) )  ->  if ( f  e.  W ,  1 ,  0 )  e.  CC )
215209, 50, 214fsummulc2 12246 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( log `  x )  x. 
sum_ f  e.  ( D  \  {  .1.  } ) if ( f  e.  W ,  1 ,  0 ) )  =  sum_ f  e.  ( D  \  {  .1.  } ) ( ( log `  x )  x.  if ( f  e.  W ,  1 ,  0 ) ) )
216 rpvmasum2.w . . . . . . . . . . . . . . . . 17  |-  W  =  { y  e.  ( D  \  {  .1.  } )  |  sum_ m  e.  NN  ( ( y `
 ( L `  m ) )  /  m )  =  0 }
217 ssrab2 3258 . . . . . . . . . . . . . . . . 17  |-  { y  e.  ( D  \  {  .1.  } )  | 
sum_ m  e.  NN  ( ( y `  ( L `  m ) )  /  m )  =  0 }  C_  ( D  \  {  .1.  } )
218216, 217eqsstri 3208 . . . . . . . . . . . . . . . 16  |-  W  C_  ( D  \  {  .1.  } )
219 difss 3303 . . . . . . . . . . . . . . . 16  |-  ( D 
\  {  .1.  }
)  C_  D
220218, 219sstri 3188 . . . . . . . . . . . . . . 15  |-  W  C_  D
221 ssfi 7083 . . . . . . . . . . . . . . 15  |-  ( ( D  e.  Fin  /\  W  C_  D )  ->  W  e.  Fin )
2226, 220, 221sylancl 643 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR+ )  ->  W  e.  Fin )
223 fsumconst 12252 . . . . . . . . . . . . . 14  |-  ( ( W  e.  Fin  /\  1  e.  CC )  -> 
sum_ f  e.  W 
1  =  ( (
# `  W )  x.  1 ) )
224222, 52, 223sylancl 643 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ f  e.  W  1  =  ( ( # `  W
)  x.  1 ) )
225218a1i 10 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR+ )  ->  W  C_  ( D  \  {  .1.  }
) )
22652a1i 10 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  RR+ )  ->  1  e.  CC )
227226ralrimivw 2627 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR+ )  ->  A. f  e.  W  1  e.  CC )
228209olcd 382 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( D  \  {  .1.  }
)  C_  ( ZZ>= ` 
1 )  \/  ( D  \  {  .1.  }
)  e.  Fin )
)
229 sumss2 12199 . . . . . . . . . . . . . 14  |-  ( ( ( W  C_  ( D  \  {  .1.  }
)  /\  A. f  e.  W  1  e.  CC )  /\  (
( D  \  {  .1.  } )  C_  ( ZZ>=
`  1 )  \/  ( D  \  {  .1.  } )  e.  Fin ) )  ->  sum_ f  e.  W  1  =  sum_ f  e.  ( D 
\  {  .1.  }
) if ( f  e.  W ,  1 ,  0 ) )
230225, 227, 228, 229syl21anc 1181 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ f  e.  W  1  =  sum_ f  e.  ( D  \  {  .1.  } ) if ( f  e.  W ,  1 ,  0 ) )
231 hashcl 11350 . . . . . . . . . . . . . . . 16  |-  ( W  e.  Fin  ->  ( # `
 W )  e. 
NN0 )
232222, 231syl 15 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( # `  W
)  e.  NN0 )
233232nn0cnd 10020 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( # `  W
)  e.  CC )
234233mulid1d 8852 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( # `
 W )  x.  1 )  =  (
# `  W )
)
235224, 230, 2343eqtr3d 2323 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ f  e.  ( D  \  {  .1.  } ) if ( f  e.  W , 
1 ,  0 )  =  ( # `  W
) )
236235oveq2d 5874 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( log `  x )  x. 
sum_ f  e.  ( D  \  {  .1.  } ) if ( f  e.  W ,  1 ,  0 ) )  =  ( ( log `  x )  x.  ( # `
 W ) ) )
237215, 236eqtr3d 2317 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ f  e.  ( D  \  {  .1.  } ) ( ( log `  x )  x.  if ( f  e.  W ,  1 ,  0 ) )  =  ( ( log `  x )  x.  ( # `
 W ) ) )
238237negeqd 9046 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR+ )  ->  -u sum_ f  e.  ( D  \  {  .1.  } ) ( ( log `  x )  x.  if ( f  e.  W ,  1 ,  0 ) )  =  -u ( ( log `  x )  x.  ( # `
 W ) ) )
239207, 213, 2383eqtrd 2319 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ f  e.  ( D  \  {  .1.  } ) ( ( log `  x )  x.  if ( f  =  .1.  ,  1 ,  if ( f  e.  W ,  -u
1 ,  0 ) ) )  =  -u ( ( log `  x
)  x.  ( # `  W ) ) )
240190, 239oveq12d 5876 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( sum_ f  e.  {  .1.  }  ( ( log `  x
)  x.  if ( f  =  .1.  , 
1 ,  if ( f  e.  W ,  -u 1 ,  0 ) ) )  +  sum_ f  e.  ( D  \  {  .1.  } ) ( ( log `  x
)  x.  if ( f  =  .1.  , 
1 ,  if ( f  e.  W ,  -u 1 ,  0 ) ) ) )  =  ( ( ( log `  x )  x.  1 )  +  -u (
( log `  x
)  x.  ( # `  W ) ) ) )
24150, 233mulcld 8855 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( log `  x )  x.  ( # `  W
) )  e.  CC )
242186, 241negsubd 9163 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( (
( log `  x
)  x.  1 )  +  -u ( ( log `  x )  x.  ( # `
 W ) ) )  =  ( ( ( log `  x
)  x.  1 )  -  ( ( log `  x )  x.  ( # `
 W ) ) ) )
243240, 242eqtrd 2315 . . . . . 6  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( sum_ f  e.  {  .1.  }  ( ( log `  x
)  x.  if ( f  =  .1.  , 
1 ,  if ( f  e.  W ,  -u 1 ,  0 ) ) )  +  sum_ f  e.  ( D  \  {  .1.  } ) ( ( log `  x
)  x.  if ( f  =  .1.  , 
1 ,  if ( f  e.  W ,  -u 1 ,  0 ) ) ) )  =  ( ( ( log `  x )  x.  1 )  -  ( ( log `  x )  x.  ( # `  W
) ) ) )
244 disjdif 3526 . . . . . . . 8  |-  ( {  .1.  }  i^i  ( D  \  {  .1.  }
) )  =  (/)
245244a1i 10 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( {  .1.  }  i^i  ( D 
\  {  .1.  }
) )  =  (/) )
246 undif2 3530 . . . . . . . 8  |-  ( {  .1.  }  u.  ( D  \  {  .1.  }
) )  =  ( {  .1.  }  u.  D )
247184snssd 3760 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR+ )  ->  {  .1.  } 
C_  D )
248 ssequn1 3345 . . . . . . . . 9  |-  ( {  .1.  }  C_  D  <->  ( {  .1.  }  u.  D )  =  D )
249247, 248sylib 188 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( {  .1.  }  u.  D )  =  D )
250246, 249syl5req 2328 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR+ )  ->  D  =  ( {  .1.  }  u.  ( D  \  {  .1.  } ) ) )
251245, 250, 6, 58fsumsplit 12212 . . . . . 6  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ f  e.  D  ( ( log `  x )  x.  if ( f  =  .1. 
,  1 ,  if ( f  e.  W ,  -u 1 ,  0 ) ) )  =  ( sum_ f  e.  {  .1.  }  ( ( log `  x )  x.  if ( f  =  .1. 
,  1 ,  if ( f  e.  W ,  -u 1 ,  0 ) ) )  + 
sum_ f  e.  ( D  \  {  .1.  } ) ( ( log `  x )  x.  if ( f  =  .1. 
,  1 ,  if ( f  e.  W ,  -u 1 ,  0 ) ) ) ) )
25250, 226, 233subdid 9235 . . . . . 6  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( log `  x )  x.  ( 1  -  ( # `
 W ) ) )  =  ( ( ( log `  x
)  x.  1 )  -  ( ( log `  x )  x.  ( # `
 W ) ) ) )
253243, 251, 2523eqtr4rd 2326 . . . . 5  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( log `  x )  x.  ( 1  -  ( # `
 W ) ) )  =  sum_ f  e.  D  ( ( log `  x )  x.  if ( f  =  .1.  ,  1 ,  if ( f  e.  W ,  -u 1 ,  0 ) ) ) )
254179, 253oveq12d 5876 . . . 4  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( (
( phi `  N
)  x.  sum_ n  e.  ( ( 1 ... ( |_ `  x
) )  i^i  T
) ( (Λ `  n
)  /  n ) )  -  ( ( log `  x )  x.  ( 1  -  ( # `  W
) ) ) )  =  ( sum_ f  e.  D  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( * `  ( f `  A
) )  x.  (
( f `  ( L `  n )
)  x.  ( (Λ `  n )  /  n
) ) )  -  sum_ f  e.  D  ( ( log `  x
)  x.  if ( f  =  .1.  , 
1 ,  if ( f  e.  W ,  -u 1 ,  0 ) ) ) ) )
25559, 124, 2543eqtr4d 2325 . . 3  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ f  e.  D  ( ( * `
 ( f `  A ) )  x.  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( f `  ( L `  n ) )  x.  ( (Λ `  n )  /  n
) )  -  (
( log `  x
)  x.  if ( f  =  .1.  , 
1 ,  if ( f  e.  W ,  -u 1 ,  0 ) ) ) ) )  =  ( ( ( phi `  N )  x.  sum_ n  e.  ( ( 1 ... ( |_ `  x ) )  i^i  T ) ( (Λ `  n )  /  n ) )  -  ( ( log `  x
)  x.  ( 1  -  ( # `  W
) ) ) ) )
256255mpteq2dva 4106 . 2  |-  ( ph  ->  ( x  e.  RR+  |->  sum_ f  e.  D  ( ( * `  (
f `  A )
)  x.  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( f `  ( L `
 n ) )  x.  ( (Λ `  n
)  /  n ) )  -  ( ( log `  x )  x.  if ( f  =  .1.  ,  1 ,  if ( f  e.  W ,  -u
1 ,  0 ) ) ) ) ) )  =  ( x  e.  RR+  |->  ( ( ( phi `  N
)  x.  sum_ n  e.  ( ( 1 ... ( |_ `  x
) )  i^i  T
) ( (Λ `  n
)  /  n ) )  -  ( ( log `  x )  x.  ( 1  -  ( # `  W
) ) ) ) ) )
257 rpssre 10364 . . . 4  |-  RR+  C_  RR
258257a1i 10 . . 3  |-  ( ph  -> 
RR+  C_  RR )
2591, 5syl 15 . . 3  |-  ( ph  ->  D  e.  Fin )
26018adantlr 695 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  (
f `  A )  e.  CC )
261260cjcld 11681 . . . . 5  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  (
* `  ( f `  A ) )  e.  CC )
26261, 58subcld 9157 . . . . 5  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( f `  ( L `  n )
)  x.  ( (Λ `  n )  /  n
) )  -  (
( log `  x
)  x.  if ( f  =  .1.  , 
1 ,  if ( f  e.  W ,  -u 1 ,  0 ) ) ) )  e.  CC )
263261, 262mulcld 8855 . . . 4  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  (
( * `  (
f `  A )
)  x.  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( f `  ( L `
 n ) )  x.  ( (Λ `  n
)  /  n ) )  -  ( ( log `  x )  x.  if ( f  =  .1.  ,  1 ,  if ( f  e.  W ,  -u
1 ,  0 ) ) ) ) )  e.  CC )
264263anasss 628 . . 3  |-  ( (
ph  /\  ( x  e.  RR+  /\  f  e.  D ) )  -> 
( ( * `  ( f `  A
) )  x.  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( f `  ( L `  n )
)  x.  ( (Λ `  n )  /  n
) )  -  (
( log `  x
)  x.  if ( f  =  .1.  , 
1 ,  if ( f  e.  W ,  -u 1 ,  0 ) ) ) ) )  e.  CC )
26519adantr 451 . . . 4  |-  ( ( ( ph  /\  f  e.  D )  /\  x  e.  RR+ )  ->  (
* `  ( f `  A ) )  e.  CC )
266262an32s 779 . . . 4  |-  ( ( ( ph  /\  f  e.  D )  /\  x  e.  RR+ )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( f `  ( L `  n )
)  x.  ( (Λ `  n )  /  n
) )  -  (
( log `  x
)  x.  if ( f  =  .1.  , 
1 ,  if ( f  e.  W ,  -u 1 ,  0 ) ) ) )  e.  CC )
267 o1const 12093 . . . . 5  |-  ( (
RR+  C_  RR  /\  (
* `  ( f `  A ) )  e.  CC )  ->  (
x  e.  RR+  |->  ( * `
 ( f `  A ) ) )  e.  O ( 1 ) )
268257, 19, 267sylancr 644 . . . 4  |-  ( (
ph  /\  f  e.  D )  ->  (
x  e.  RR+  |->  ( * `
 ( f `  A ) ) )  e.  O ( 1 ) )
269 fveq1 5524 . . . . . . . . . . . 12  |-  ( f  =  .1.  ->  (
f `  ( L `  n ) )  =  (  .1.  `  ( L `  n )
) )
270269oveq1d 5873 . . . . . . . . . . 11  |-  ( f  =  .1.  ->  (
( f `  ( L `  n )
)  x.  ( (Λ `  n )  /  n
) )  =  ( (  .1.  `  ( L `  n )
)  x.  ( (Λ `  n )  /  n
) ) )
271270sumeq2sdv 12177 . . . . . . . . . 10  |-  ( f  =  .1.  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( f `  ( L `  n ) )  x.  ( (Λ `  n )  /  n
) )  =  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (  .1.  `  ( L `  n ) )  x.  ( (Λ `  n
)  /  n ) ) )
272271, 188oveq12d 5876 . . . . . . . . 9  |-  ( f  =  .1.  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( f `  ( L `  n )
)  x.  ( (Λ `  n )  /  n
) )  -  (
( log `  x
)  x.  if ( f  =  .1.  , 
1 ,  if ( f  e.  W ,  -u 1 ,  0 ) ) ) )  =  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (  .1.  `  ( L `  n ) )  x.  ( (Λ `  n )  /  n
) )  -  (
( log `  x
)  x.  1 ) ) )
273272adantl 452 . . . . . . . 8  |-  ( ( ( ph  /\  f  e.  D )  /\  f  =  .1.  )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( f `  ( L `  n )
)  x.  ( (Λ `  n )  /  n
) )  -  (
( log `  x
)  x.  if ( f  =  .1.  , 
1 ,  if ( f  e.  W ,  -u 1 ,  0 ) ) ) )  =  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (  .1.  `  ( L `  n ) )  x.  ( (Λ `  n )  /  n
) )  -  (
( log `  x
)  x.  1 ) ) )
27448recnd 8861 . . . . . . . . . 10  |-  ( x  e.  RR+  ->  ( log `  x )  e.  CC )
275274mulid1d 8852 . . . . . . . . 9  |-  ( x  e.  RR+  ->  ( ( log `  x )  x.  1 )  =  ( log `  x
) )
276275oveq2d 5874 . . . . . . . 8  |-  ( x  e.  RR+  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (  .1.  `  ( L `  n ) )  x.  ( (Λ `  n
)  /  n ) )  -  ( ( log `  x )  x.  1 ) )  =  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (  .1.  `  ( L `  n ) )  x.  ( (Λ `  n )  /  n
) )  -  ( log `  x ) ) )
277273, 276sylan9eq 2335 . . . . . . 7  |-  ( ( ( ( ph  /\  f  e.  D )  /\  f  =  .1.  )  /\  x  e.  RR+ )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( f `  ( L `  n ) )  x.  ( (Λ `  n )  /  n
) )  -  (
( log `  x
)  x.  if ( f  =  .1.  , 
1 ,  if ( f  e.  W ,  -u 1 ,  0 ) ) ) )  =  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (  .1.  `  ( L `  n ) )  x.  ( (Λ `  n )  /  n
) )  -  ( log `  x ) ) )
278277mpteq2dva 4106 . . . . . 6  |-  ( ( ( ph  /\  f  e.  D )  /\  f  =  .1.  )  ->  (
x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( f `  ( L `
 n ) )  x.  ( (Λ `  n
)  /  n ) )  -  ( ( log `  x )  x.  if ( f  =  .1.  ,  1 ,  if ( f  e.  W ,  -u
1 ,  0 ) ) ) ) )  =  ( x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (  .1.  `  ( L `  n ) )  x.  ( (Λ `  n )  /  n
) )  -  ( log `  x ) ) ) )
2798, 25, 1, 3, 4, 70rpvmasumlem 20636 . . . . . . 7  |-  ( ph  ->  ( x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (  .1.  `  ( L `  n ) )  x.  ( (Λ `  n )  /  n
) )  -  ( log `  x ) ) )  e.  O ( 1 ) )
280279ad2antrr 706 . . . . . 6  |-  ( ( ( ph  /\  f  e.  D )  /\  f  =  .1.  )  ->  (
x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (  .1.  `  ( L `  n ) )  x.  ( (Λ `  n
)  /  n ) )  -  ( log `  x ) ) )  e.  O ( 1 ) )
281278, 280eqeltrd 2357 . . . . 5  |-  ( ( ( ph  /\  f  e.  D )  /\  f  =  .1.  )  ->  (
x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( f `  ( L `
 n ) )  x.  ( (Λ `  n
)  /  n ) )  -  ( ( log `  x )  x.  if ( f  =  .1.  ,  1 ,  if ( f  e.  W ,  -u
1 ,  0 ) ) ) ) )  e.  O ( 1 ) )
282192oveq2d 5874 . . . . . . . . . 10  |-  ( f  =/=  .1.  ->  (
( log `  x
)  x.  if ( f  =  .1.  , 
1 ,  if ( f  e.  W ,  -u 1 ,  0 ) ) )  =  ( ( log `  x
)  x.  if ( f  e.  W ,  -u 1 ,  0 ) ) )
283282oveq2d 5874 . . . . . . . . 9  |-  ( f  =/=  .1.  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( f `  ( L `  n )
)  x.  ( (Λ `  n )  /  n
) )  -  (
( log `  x
)  x.  if ( f  =  .1.  , 
1 ,  if ( f  e.  W ,  -u 1 ,  0 ) ) ) )  =  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( f `  ( L `  n ) )  x.  ( (Λ `  n )  /  n
) )  -  (
( log `  x
)  x.  if ( f  e.  W ,  -u 1 ,  0 ) ) ) )
28450adantlr 695 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  f  e.  D )  /\  x  e.  RR+ )  ->  ( log `  x )  e.  CC )
285 mulcom 8823 . . . . . . . . . . . . . . 15  |-  ( ( ( log `  x
)  e.  CC  /\  -u 1  e.  CC )  ->  ( ( log `  x )  x.  -u 1
)  =  ( -u
1  x.  ( log `  x ) ) )
286284, 53, 285sylancl 643 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  f  e.  D )  /\  x  e.  RR+ )  ->  (
( log `  x
)  x.  -u 1
)  =  ( -u
1  x.  ( log `  x ) ) )
287284mulm1d 9231 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  f  e.  D )  /\  x  e.  RR+ )  ->  ( -u 1  x.  ( log `  x ) )  = 
-u ( log `  x
) )
288286, 287eqtrd 2315 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  f  e.  D )  /\  x  e.  RR+ )  ->  (
( log `  x
)  x.  -u 1
)  =  -u ( log `  x ) )
289284mul01d 9011 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  f  e.  D )  /\  x  e.  RR+ )  ->  (
( log `  x
)  x.  0 )  =  0 )
290288, 289ifeq12d 3581 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  f  e.  D )  /\  x  e.  RR+ )  ->  if ( f  e.  W ,  ( ( log `  x )  x.  -u 1
) ,  ( ( log `  x )  x.  0 ) )  =  if ( f  e.  W ,  -u ( log `  x ) ,  0 ) )
291 oveq2 5866 . . . . . . . . . . . . 13  |-  ( if ( f  e.  W ,  -u 1 ,  0 )  =  -u 1  ->  ( ( log `  x
)  x.  if ( f  e.  W ,  -u 1 ,  0 ) )  =  ( ( log `  x )  x.  -u 1 ) )
292 oveq2 5866 . . . . . . . . . . . . 13  |-  ( if ( f  e.  W ,  -u 1 ,  0 )  =  0  -> 
( ( log `  x
)  x.  if ( f  e.  W ,  -u 1 ,  0 ) )  =  ( ( log `  x )  x.  0 ) )
293291, 292ifsb 3574 . . . . . . . . . . . 12  |-  ( ( log `  x )  x.  if ( f  e.  W ,  -u
1 ,  0 ) )  =  if ( f  e.  W , 
( ( log `  x
)  x.  -u 1
) ,  ( ( log `  x )  x.  0 ) )
294 negeq 9044 . . . . . . . . . . . . 13  |-  ( if ( f  e.  W ,  ( log `  x
) ,  0 )  =  ( log `  x
)  ->  -u if ( f  e.  W , 
( log `  x
) ,  0 )  =  -u ( log `  x
) )
295 negeq 9044 . . . . . . . . . . . . . 14  |-  ( if ( f  e.  W ,  ( log `  x
) ,  0 )  =  0  ->  -u if ( f  e.  W ,  ( log `  x
) ,  0 )  =  -u 0 )
296295, 196syl6eq 2331 . . . . . . . . . . . . 13  |-  ( if ( f  e.  W ,  ( log `  x
) ,  0 )  =  0  ->  -u if ( f  e.  W ,  ( log `  x
) ,  0 )  =  0 )
297294, 296ifsb 3574 . . . . . . . . . . . 12  |-  -u if ( f  e.  W ,  ( log `  x
) ,  0 )  =  if ( f  e.  W ,  -u ( log `  x ) ,  0 )
298290, 293, 2973eqtr4g 2340 . . . . . . . . . . 11  |-  ( ( ( ph  /\  f  e.  D )  /\  x  e.  RR+ )  ->  (
( log `  x
)  x.  if ( f  e.  W ,  -u 1 ,  0 ) )  =  -u if ( f  e.  W ,  ( log `  x
) ,  0 ) )
299298oveq2d 5874 . . . . . . . . . 10  |-  ( ( ( ph  /\  f  e.  D )  /\  x  e.  RR+ )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( f `  ( L `  n )
)  x.  ( (Λ `  n )  /  n
) )  -  (
( log `  x
)  x.  if ( f  e.  W ,  -u 1 ,  0 ) ) )  =  (
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( f `  ( L `  n )
)  x.  ( (Λ `  n )  /  n
) )  -  -u if ( f  e.  W ,  ( log `  x
) ,  0 ) ) )
30061an32s 779 . . . . . . . . . . 11  |-  ( ( ( ph  /\  f  e.  D )  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( f `  ( L `  n ) )  x.  ( (Λ `  n )  /  n
) )  e.  CC )
301 ifcl 3601 . . . . . . . . . . . 12  |-  ( ( ( log `  x
)  e.  CC  /\  0  e.  CC )  ->  if ( f  e.  W ,  ( log `  x ) ,  0 )  e.  CC )
302284, 54, 301sylancl 643 . . . . . . . . . . 11  |-  ( ( ( ph  /\  f  e.  D )  /\  x  e.  RR+ )  ->  if ( f  e.  W ,  ( log `  x
) ,  0 )  e.  CC )
303300, 302subnegd 9164 . . . . . . . . . 10  |-  ( ( ( ph  /\  f  e.  D )  /\  x  e.  RR+ )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( f `  ( L `  n )
)  x.  ( (Λ `  n )  /  n
) )  -  -u if ( f  e.  W ,  ( log `  x
) ,  0 ) )  =  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( f `  ( L `
 n ) )  x.  ( (Λ `  n
)  /  n ) )  +  if ( f  e.  W , 
( log `  x
) ,  0 ) ) )
304299, 303eqtrd 2315 . . . . . . . . 9  |-  ( ( ( ph  /\  f  e.  D )  /\  x  e.  RR+ )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( f `  ( L `  n )
)  x.  ( (Λ `  n )  /  n
) )  -  (
( log `  x
)  x.  if ( f  e.  W ,  -u 1 ,  0 ) ) )  =  (
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( f `  ( L `  n )
)  x.  ( (Λ `  n )  /  n
) )  +  if ( f  e.  W ,  ( log `  x
) ,  0 ) ) )
305283, 304sylan9eqr 2337 . . . . . . . 8  |-  ( ( ( ( ph  /\  f  e.  D )  /\  x  e.  RR+ )  /\  f  =/=  .1.  )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( f `  ( L `  n ) )  x.  ( (Λ `  n )  /  n
) )  -  (
( log `  x
)  x.  if ( f  =  .1.  , 
1 ,  if ( f  e.  W ,  -u 1 ,  0 ) ) ) )  =  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( f `  ( L `  n ) )  x.  ( (Λ `  n )  /  n
) )  +  if ( f  e.  W ,  ( log `  x
) ,  0 ) ) )
306305an32s 779 . . . . . . 7  |-  ( ( ( ( ph  /\  f  e.  D )  /\  f  =/=  .1.  )  /\  x  e.  RR+ )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( f `  ( L `  n ) )  x.  ( (Λ `  n )  /  n
) )  -  (
( log `  x
)  x.  if ( f  =  .1.  , 
1 ,  if ( f  e.  W ,  -u 1 ,  0 ) ) ) )  =  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( f `  ( L `  n ) )  x.  ( (Λ `  n )  /  n
) )  +  if ( f  e.  W ,  ( log `  x
) ,  0 ) ) )
307306mpteq2dva 4106 . . . . . 6  |-  ( ( ( ph  /\  f  e.  D )  /\  f  =/=  .1.  )  ->  (
x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( f `  ( L `
 n ) )  x.  ( (Λ `  n
)  /  n ) )  -  ( ( log `  x )  x.  if ( f  =  .1.  ,  1 ,  if ( f  e.  W ,  -u
1 ,  0 ) ) ) ) )  =  ( x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( f `  ( L `  n ) )  x.  ( (Λ `  n )  /  n
) )  +  if ( f  e.  W ,  ( log `  x
) ,  0 ) ) ) )
3081ad2antrr 706 . . . . . . . 8  |-  ( ( ( ph  /\  f  e.  D )  /\  f  =/=  .1.  )  ->  N  e.  NN )
309 simplr 731 . . . . . . . 8  |-  ( ( ( ph  /\  f  e.  D )  /\  f  =/=  .1.  )  ->  f  e.  D )
310 simpr 447 . . . . . . . 8  |-  ( ( ( ph  /\  f  e.  D )  /\  f  =/=  .1.  )  ->  f  =/=  .1.  )
311 eqid 2283 . . . . . . . 8  |-  ( a  e.  NN  |->  ( ( f `  ( L `
 a ) )  /  a ) )  =  ( a  e.  NN  |->  ( ( f `
 ( L `  a ) )  / 
a ) )
3128, 25, 308, 3, 4, 70, 309, 310, 311dchrmusumlema 20642 . . . . . . 7  |-  ( ( ( ph  /\  f  e.  D )  /\  f  =/=  .1.  )  ->  E. t E. c  e.  (
0 [,)  +oo ) (  seq  1 (  +  ,  ( a  e.  NN  |->  ( ( f `
 ( L `  a ) )  / 
a ) ) )  ~~>  t  /\  A. y  e.  ( 1 [,)  +oo ) ( abs `  (
(  seq  1 (  +  ,  ( a  e.  NN  |->  ( ( f `  ( L `
 a ) )  /  a ) ) ) `  ( |_
`  y ) )  -  t ) )  <_  ( c  / 
y ) ) )
3131adantr 451 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  f  e.  D )  ->  N  e.  NN )
314313ad2antrr 706 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  f  e.  D )  /\  f  =/=  .1.  )  /\  ( c  e.  ( 0 [,)  +oo )  /\  (  seq  1
(  +  ,  ( a  e.  NN  |->  ( ( f `  ( L `  a )
)  /  a ) ) )  ~~>  t  /\  A. y  e.  ( 1 [,)  +oo ) ( abs `  ( (  seq  1
(  +  ,  ( a  e.  NN  |->  ( ( f `  ( L `  a )
)  /  a ) ) ) `  ( |_ `  y ) )  -  t ) )  <_  ( c  / 
y ) ) ) )  ->  N  e.  NN )
315309adantr 451 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  f  e.  D )  /\  f  =/=  .1.  )  /\  ( c  e.  ( 0 [,)  +oo )  /\  (  seq  1
(  +  ,  ( a  e.  NN  |->  ( ( f `  ( L `  a )
)  /  a ) ) )  ~~>  t  /\  A. y  e.  ( 1 [,)  +oo ) ( abs `  ( (  seq  1
(  +  ,  ( a  e.  NN  |->  ( ( f `  ( L `  a )
)  /  a ) ) ) `  ( |_ `  y ) )  -  t ) )  <_  ( c  / 
y ) ) ) )  ->  f  e.  D )
316 simplr 731 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  f  e.  D )  /\  f  =/=  .1.  )  /\  ( c  e.  ( 0 [,)  +oo )  /\  (  seq  1
(  +  ,  ( a  e.  NN  |->  ( ( f `  ( L `  a )
)  /  a ) ) )  ~~>  t  /\  A. y  e.  ( 1 [,)  +oo ) ( abs `  ( (  seq  1
(  +  ,  ( a  e.  NN  |->  ( ( f `  ( L `  a )
)  /  a ) ) ) `  ( |_ `  y ) )  -  t ) )  <_  ( c  / 
y ) ) ) )  ->  f  =/=  .1.  )
317 simprl 732 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  f  e.  D )  /\  f  =/=  .1.  )  /\  ( c  e.  ( 0 [,)  +oo )  /\  (  seq  1
(  +  ,  ( a  e.  NN  |->  ( ( f `  ( L `  a )
)  /  a ) ) )  ~~>  t  /\  A. y  e.  ( 1 [,)  +oo ) ( abs `  ( (  seq  1
(  +  ,  ( a  e.  NN  |->  ( ( f `  ( L `  a )
)  /  a ) ) ) `  ( |_ `  y ) )  -  t ) )  <_  ( c  / 
y ) ) ) )  ->  c  e.  ( 0 [,)  +oo ) )
318 simprrl 740 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  f  e.  D )  /\  f  =/=  .1.  )  /\  ( c  e.  ( 0 [,)  +oo )  /\  (  seq  1
(  +  ,  ( a  e.  NN  |->  ( ( f `  ( L `  a )
)  /  a ) ) )  ~~>  t  /\  A. y  e.  ( 1 [,)  +oo ) ( abs `  ( (  seq  1
(  +  ,  ( a  e.  NN  |->  ( ( f `  ( L `  a )
)  /  a ) ) ) `  ( |_ `  y ) )  -  t ) )  <_  ( c  / 
y ) ) ) )  ->  seq  1
(  +  ,  ( a  e.  NN  |->  ( ( f `  ( L `  a )
)  /  a ) ) )  ~~>  t )
319 simprrr 741 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  f  e.  D )  /\  f  =/=  .1.  )  /\  ( c  e.  ( 0 [,)  +oo )  /\  (  seq  1
(  +  ,  ( a  e.  NN  |->  ( ( f `  ( L `  a )
)  /  a ) ) )  ~~>  t  /\  A. y  e.  ( 1 [,)  +oo ) ( abs `  ( (  seq  1
(  +  ,  ( a  e.  NN  |->  ( ( f `  ( L `  a )
)  /  a ) ) ) `  ( |_ `  y ) )  -  t ) )  <_  ( c  / 
y ) ) ) )  ->  A. y  e.  ( 1 [,)  +oo ) ( abs `  (
(  seq  1 (  +  ,  ( a  e.  NN  |->  ( ( f `  ( L `
 a ) )  /  a ) ) ) `  ( |_
`  y ) )  -  t ) )  <_  ( c  / 
y ) )
3208, 25, 314, 3, 4, 70, 315, 316, 311, 317, 318, 319, 216dchrvmaeq0 20653 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  f  e.  D )  /\  f  =/=  .1.  )  /\  ( c  e.  ( 0 [,)  +oo )  /\  (  seq  1
(  +  ,  ( a  e.  NN  |->  ( ( f `  ( L `  a )
)  /  a ) ) )  ~~>  t  /\  A. y  e.  ( 1 [,)  +oo ) ( abs `  ( (  seq  1
(  +  ,  ( a  e.  NN  |->  ( ( f `  ( L `  a )
)  /  a ) ) ) `  ( |_ `  y ) )  -  t ) )  <_  ( c  / 
y ) ) ) )  ->  ( f  e.  W  <->  t  =  0 ) )
321 ifbi 3582 . . . . . . . . . . . . . 14  |-  ( ( f  e.  W  <->  t  = 
0 )  ->  if ( f  e.  W ,  ( log `  x
) ,  0 )  =  if ( t  =  0 ,  ( log `  x ) ,  0 ) )
322321oveq2d 5874 . . . . . . . . . . . . 13  |-  ( ( f  e.  W  <->  t  = 
0 )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( f `  ( L `  n )
)  x.  ( (Λ `  n )  /  n
) )  +  if ( f  e.  W ,  ( log `  x
) ,  0 ) )  =  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( f `  ( L `
 n ) )  x.  ( (Λ `  n
)  /  n ) )  +  if ( t  =  0 ,  ( log `  x
) ,  0 ) ) )
323322mpteq2dv 4107 . . . . . . . . . . . 12  |-  ( ( f  e.  W  <->  t  = 
0 )  ->  (
x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( f `  ( L `
 n ) )  x.  ( (Λ `  n
)  /  n ) )  +  if ( f  e.  W , 
( log `  x
) ,  0