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

Theorem rpvmasum2 20493
Description: A partial result along the lines of rpvmasum 20507. 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
StepHypRef Expression
1 rpvmasum.a . . . . . . 7  |-  ( ph  ->  N  e.  NN )
21adantr 453 . . . . . 6  |-  ( (
ph  /\  x  e.  RR+ )  ->  N  e.  NN )
3 rpvmasum2.g . . . . . . 7  |-  G  =  (DChr `  N )
4 rpvmasum2.d . . . . . . 7  |-  D  =  ( Base `  G
)
53, 4dchrfi 20326 . . . . . 6  |-  ( N  e.  NN  ->  D  e.  Fin )
62, 5syl 17 . . . . 5  |-  ( (
ph  /\  x  e.  RR+ )  ->  D  e.  Fin )
7 fzfid 10913 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  (
1 ... ( |_ `  x ) )  e. 
Fin )
8 rpvmasum.z . . . . . . . . . . . . 13  |-  Z  =  (ℤ/n `  N )
9 eqid 2253 . . . . . . . . . . . . 13  |-  ( Base `  Z )  =  (
Base `  Z )
10 simpr 449 . . . . . . . . . . . . 13  |-  ( (
ph  /\  f  e.  D )  ->  f  e.  D )
113, 8, 4, 9, 10dchrf 20313 . . . . . . . . . . . 12  |-  ( (
ph  /\  f  e.  D )  ->  f : ( Base `  Z
) --> CC )
12 rpvmasum2.u . . . . . . . . . . . . . . 15  |-  U  =  (Unit `  Z )
139, 12unitss 15277 . . . . . . . . . . . . . 14  |-  U  C_  ( Base `  Z )
14 rpvmasum2.b . . . . . . . . . . . . . 14  |-  ( ph  ->  A  e.  U )
1513, 14sseldi 3101 . . . . . . . . . . . . 13  |-  ( ph  ->  A  e.  ( Base `  Z ) )
1615adantr 453 . . . . . . . . . . . 12  |-  ( (
ph  /\  f  e.  D )  ->  A  e.  ( Base `  Z
) )
17 ffvelrn 5515 . . . . . . . . . . . 12  |-  ( ( f : ( Base `  Z ) --> CC  /\  A  e.  ( Base `  Z ) )  -> 
( f `  A
)  e.  CC )
1811, 16, 17syl2anc 645 . . . . . . . . . . 11  |-  ( (
ph  /\  f  e.  D )  ->  (
f `  A )  e.  CC )
1918cjcld 11558 . . . . . . . . . 10  |-  ( (
ph  /\  f  e.  D )  ->  (
* `  ( f `  A ) )  e.  CC )
2019adantlr 698 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  (
* `  ( f `  A ) )  e.  CC )
2120adantrl 699 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
n  e.  ( 1 ... ( |_ `  x ) )  /\  f  e.  D )
)  ->  ( * `  ( f `  A
) )  e.  CC )
2211adantlr 698 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  f : ( Base `  Z
) --> CC )
2322adantlr 698 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  f  e.  D
)  ->  f :
( Base `  Z ) --> CC )
241nnnn0d 9897 . . . . . . . . . . . . . . 15  |-  ( ph  ->  N  e.  NN0 )
25 rpvmasum.l . . . . . . . . . . . . . . . 16  |-  L  =  ( ZRHom `  Z
)
268, 9, 25znzrhfo 16333 . . . . . . . . . . . . . . 15  |-  ( N  e.  NN0  ->  L : ZZ -onto-> ( Base `  Z
) )
27 fof 5308 . . . . . . . . . . . . . . 15  |-  ( L : ZZ -onto-> ( Base `  Z )  ->  L : ZZ --> ( Base `  Z
) )
2824, 26, 273syl 20 . . . . . . . . . . . . . 14  |-  ( ph  ->  L : ZZ --> ( Base `  Z ) )
2928adantr 453 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR+ )  ->  L : ZZ
--> ( Base `  Z
) )
30 elfzelz 10676 . . . . . . . . . . . . 13  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  ZZ )
31 ffvelrn 5515 . . . . . . . . . . . . 13  |-  ( ( L : ZZ --> ( Base `  Z )  /\  n  e.  ZZ )  ->  ( L `  n )  e.  ( Base `  Z
) )
3229, 30, 31syl2an 465 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( L `  n )  e.  (
Base `  Z )
)
3332adantr 453 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  f  e.  D
)  ->  ( L `  n )  e.  (
Base `  Z )
)
34 ffvelrn 5515 . . . . . . . . . . 11  |-  ( ( f : ( Base `  Z ) --> CC  /\  ( L `  n )  e.  ( Base `  Z
) )  ->  (
f `  ( L `  n ) )  e.  CC )
3523, 33, 34syl2anc 645 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  f  e.  D
)  ->  ( f `  ( L `  n
) )  e.  CC )
3635anasss 631 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
n  e.  ( 1 ... ( |_ `  x ) )  /\  f  e.  D )
)  ->  ( f `  ( L `  n
) )  e.  CC )
37 elfznn 10697 . . . . . . . . . . . . . 14  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  NN )
3837adantl 454 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  NN )
39 vmacl 20188 . . . . . . . . . . . . 13  |-  ( n  e.  NN  ->  (Λ `  n )  e.  RR )
4038, 39syl 17 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (Λ `  n
)  e.  RR )
4140, 38nndivred 9674 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  /  n
)  e.  RR )
4241recnd 8741 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  /  n
)  e.  CC )
4342adantrr 700 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
n  e.  ( 1 ... ( |_ `  x ) )  /\  f  e.  D )
)  ->  ( (Λ `  n )  /  n
)  e.  CC )
4436, 43mulcld 8735 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
n  e.  ( 1 ... ( |_ `  x ) )  /\  f  e.  D )
)  ->  ( (
f `  ( L `  n ) )  x.  ( (Λ `  n
)  /  n ) )  e.  CC )
4521, 44mulcld 8735 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
n  e.  ( 1 ... ( |_ `  x ) )  /\  f  e.  D )
)  ->  ( (
* `  ( f `  A ) )  x.  ( ( f `  ( L `  n ) )  x.  ( (Λ `  n )  /  n
) ) )  e.  CC )
4645anass1rs 785 . . . . . 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 12083 . . . . 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 19764 . . . . . . . . 9  |-  ( x  e.  RR+  ->  ( log `  x )  e.  RR )
4948adantl 454 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( log `  x )  e.  RR )
5049recnd 8741 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( log `  x )  e.  CC )
5150adantr 453 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  ( log `  x )  e.  CC )
52 ax-1cn 8675 . . . . . . 7  |-  1  e.  CC
53 neg1cn 9693 . . . . . . . 8  |-  -u 1  e.  CC
54 0cn 8711 . . . . . . . 8  |-  0  e.  CC
5553, 54keepel 3527 . . . . . . 7  |-  if ( f  e.  W ,  -u 1 ,  0 )  e.  CC
5652, 55keepel 3527 . . . . . 6  |-  if ( f  =  .1.  , 
1 ,  if ( f  e.  W ,  -u 1 ,  0 ) )  e.  CC
57 mulcl 8701 . . . . . 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 646 . . . . 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 12127 . . . 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 785 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  n  e.  (
1 ... ( |_ `  x ) ) )  ->  ( ( f `
 ( L `  n ) )  x.  ( (Λ `  n
)  /  n ) )  e.  CC )
617, 60fsumcl 12083 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( f `  ( L `  n ) )  x.  ( (Λ `  n )  /  n
) )  e.  CC )
6220, 61, 58subdid 9115 . . . . . 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 12123 . . . . . . 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 12 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  if ( f  =  .1. 
,  1 ,  if ( f  e.  W ,  -u 1 ,  0 ) )  e.  CC )
6520, 51, 64mul12d 8901 . . . . . . . 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 5718 . . . . . . . . . . 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 5718 . . . . . . . . . . 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 3479 . . . . . . . . . 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 5376 . . . . . . . . . . . . . . . . 17  |-  ( f  =  .1.  ->  (
f `  A )  =  (  .1.  `  A
) )
70 rpvmasum2.1 . . . . . . . . . . . . . . . . . 18  |-  .1.  =  ( 0g `  G )
711ad2antrr 709 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  N  e.  NN )
7214ad2antrr 709 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  A  e.  U )
733, 8, 70, 12, 71, 72dchr1 20328 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  (  .1.  `  A )  =  1 )
7469, 73sylan9eqr 2307 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  f  =  .1.  )  ->  ( f `  A )  =  1 )
7574fveq2d 5381 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  f  =  .1.  )  ->  ( * `  ( f `  A
) )  =  ( * `  1 ) )
76 1re 8717 . . . . . . . . . . . . . . . 16  |-  1  e.  RR
77 cjre 11501 . . . . . . . . . . . . . . . 16  |-  ( 1  e.  RR  ->  (
* `  1 )  =  1 )
7876, 77ax-mp 10 . . . . . . . . . . . . . . 15  |-  ( * `
 1 )  =  1
7975, 78syl6eq 2301 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  f  =  .1.  )  ->  ( * `  ( f `  A
) )  =  1 )
8079oveq1d 5725 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  f  =  .1.  )  ->  ( ( * `
 ( f `  A ) )  x.  1 )  =  ( 1  x.  1 ) )
81 1t1e1 9749 . . . . . . . . . . . . 13  |-  ( 1  x.  1 )  =  1
8280, 81syl6eq 2301 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  f  =  .1.  )  ->  ( ( * `
 ( f `  A ) )  x.  1 )  =  1 )
8382ifeq1da 3495 . . . . . . . . . . 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 2414 . . . . . . . . . . . . 13  |-  ( f  =/=  .1.  <->  -.  f  =  .1.  )
85 oveq2 5718 . . . . . . . . . . . . . . 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 5718 . . . . . . . . . . . . . . 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 3479 . . . . . . . . . . . . . 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 737 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  f  =/=  .1.  )  ->  ph )
89 rpvmasum2.z1 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  f  e.  W )  ->  A  =  ( 1r `  Z ) )
9089fveq2d 5381 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  f  e.  W )  ->  (
f `  A )  =  ( f `  ( 1r `  Z ) ) )
9188, 90sylan 459 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D
)  /\  f  =/=  .1.  )  /\  f  e.  W )  ->  (
f `  A )  =  ( f `  ( 1r `  Z ) ) )
923, 8, 4dchrmhm 20312 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  D  C_  ( (mulGrp `  Z ) MndHom  (mulGrp ` fld ) )
93 simpr 449 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  f  e.  D )
9492, 93sseldi 3101 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  f  e.  ( (mulGrp `  Z
) MndHom  (mulGrp ` fld ) ) )
95 eqid 2253 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  (mulGrp `  Z )  =  (mulGrp `  Z )
96 eqid 2253 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 1r
`  Z )  =  ( 1r `  Z
)
9795, 96rngidval 15178 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 1r
`  Z )  =  ( 0g `  (mulGrp `  Z ) )
98 eqid 2253 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  (mulGrp ` fld )  =  (mulGrp ` fld )
99 cnfld1 16231 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  1  =  ( 1r ` fld )
10098, 99rngidval 15178 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  1  =  ( 0g `  (mulGrp ` fld ) )
10197, 100mhm0 14258 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( f  e.  ( (mulGrp `  Z ) MndHom  (mulGrp ` fld ) )  ->  (
f `  ( 1r `  Z ) )  =  1 )
10294, 101syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  (
f `  ( 1r `  Z ) )  =  1 )
103102ad2antrr 709 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D
)  /\  f  =/=  .1.  )  /\  f  e.  W )  ->  (
f `  ( 1r `  Z ) )  =  1 )
10491, 103eqtrd 2285 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D
)  /\  f  =/=  .1.  )  /\  f  e.  W )  ->  (
f `  A )  =  1 )
105104fveq2d 5381 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D
)  /\  f  =/=  .1.  )  /\  f  e.  W )  ->  (
* `  ( f `  A ) )  =  ( * `  1
) )
106105, 78syl6eq 2301 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D
)  /\  f  =/=  .1.  )  /\  f  e.  W )  ->  (
* `  ( f `  A ) )  =  1 )
107106oveq1d 5725 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D
)  /\  f  =/=  .1.  )  /\  f  e.  W )  ->  (
( * `  (
f `  A )
)  x.  -u 1
)  =  ( 1  x.  -u 1 ) )
10853mulid2i 8720 . . . . . . . . . . . . . . . . 17  |-  ( 1  x.  -u 1 )  = 
-u 1
109107, 108syl6eq 2301 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D
)  /\  f  =/=  .1.  )  /\  f  e.  W )  ->  (
( * `  (
f `  A )
)  x.  -u 1
)  =  -u 1
)
110109ifeq1da 3495 . . . . . . . . . . . . . . 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 453 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  f  =/=  .1.  )  ->  ( * `  ( f `  A
) )  e.  CC )
112111mul01d 8891 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  f  =/=  .1.  )  ->  ( ( * `
 ( f `  A ) )  x.  0 )  =  0 )
113112ifeq2d 3485 . . . . . . . . . . . . . . 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 2285 . . . . . . . . . . . . . 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 2297 . . . . . . . . . . . . 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 464 . . . . . . . . . . . 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 3496 . . . . . . . . . . 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 2285 . . . . . . . . . 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 2297 . . . . . . . . 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 5726 . . . . . . . 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 2285 . . . . . . 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 5728 . . . . . 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 2285 . . . . 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 12053 . . . 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 10913 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( 1 ... ( |_ `  x ) )  e. 
Fin )
126 inss1 3296 . . . . . . . . 9  |-  ( ( 1 ... ( |_
`  x ) )  i^i  T )  C_  ( 1 ... ( |_ `  x ) )
127 ssfi 6968 . . . . . . . . 9  |-  ( ( ( 1 ... ( |_ `  x ) )  e.  Fin  /\  (
( 1 ... ( |_ `  x ) )  i^i  T )  C_  ( 1 ... ( |_ `  x ) ) )  ->  ( (
1 ... ( |_ `  x ) )  i^i 
T )  e.  Fin )
128125, 126, 127sylancl 646 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( (
1 ... ( |_ `  x ) )  i^i 
T )  e.  Fin )
1292phicld 12714 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( phi `  N )  e.  NN )
130129nncnd 9642 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( phi `  N )  e.  CC )
131126a1i 12 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( (
1 ... ( |_ `  x ) )  i^i 
T )  C_  (
1 ... ( |_ `  x ) ) )
132131sselda 3103 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( ( 1 ... ( |_ `  x
) )  i^i  T
) )  ->  n  e.  ( 1 ... ( |_ `  x ) ) )
133132, 42syldan 458 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( ( 1 ... ( |_ `  x
) )  i^i  T
) )  ->  (
(Λ `  n )  /  n )  e.  CC )
134128, 130, 133fsummulc2 12123 . . . . . . 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 453 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( phi `  N )  e.  CC )
136135, 42mulcld 8735 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( phi `  N )  x.  ( (Λ `  n
)  /  n ) )  e.  CC )
137132, 136syldan 458 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( ( 1 ... ( |_ `  x
) )  i^i  T
) )  ->  (
( phi `  N
)  x.  ( (Λ `  n )  /  n
) )  e.  CC )
138137ralrimiva 2588 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  A. n  e.  ( ( 1 ... ( |_ `  x
) )  i^i  T
) ( ( phi `  N )  x.  (
(Λ `  n )  /  n ) )  e.  CC )
139125olcd 384 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( (
1 ... ( |_ `  x ) )  C_  ( ZZ>= `  1 )  \/  ( 1 ... ( |_ `  x ) )  e.  Fin ) )
140 sumss2 12076 . . . . . . . 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 1186 . . . . . . 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 3266 . . . . . . . . . . . . 13  |-  ( n  e.  ( ( 1 ... ( |_ `  x ) )  i^i 
T )  <->  ( n  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  T
) )
143142baib 876 . . . . . . . . . . . 12  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  (
n  e.  ( ( 1 ... ( |_
`  x ) )  i^i  T )  <->  n  e.  T ) )
144143adantl 454 . . . . . . . . . . 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 2317 . . . . . . . . . . . 12  |-  ( n  e.  T  <->  n  e.  ( `' L " { A } ) )
147 ffn 5246 . . . . . . . . . . . . . 14  |-  ( L : ZZ --> ( Base `  Z )  ->  L  Fn  ZZ )
14829, 147syl 17 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR+ )  ->  L  Fn  ZZ )
149 fniniseg 5498 . . . . . . . . . . . . . 14  |-  ( L  Fn  ZZ  ->  (
n  e.  ( `' L " { A } )  <->  ( n  e.  ZZ  /\  ( L `
 n )  =  A ) ) )
150149baibd 880 . . . . . . . . . . . . 13  |-  ( ( L  Fn  ZZ  /\  n  e.  ZZ )  ->  ( n  e.  ( `' L " { A } )  <->  ( L `  n )  =  A ) )
151148, 30, 150syl2an 465 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  e.  ( `' L " { A } )  <->  ( L `  n )  =  A ) )
152146, 151syl5bb 250 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  e.  T  <->  ( L `  n )  =  A ) )
153144, 152bitr2d 247 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( L `  n )  =  A  <->  n  e.  (
( 1 ... ( |_ `  x ) )  i^i  T ) ) )
15442mul02d 8890 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 0  x.  ( (Λ `  n
)  /  n ) )  =  0 )
155153, 154ifbieq2d 3490 . . . . . . . . 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 5717 . . . . . . . . . . 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 5717 . . . . . . . . . . 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 3479 . . . . . . . . . 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 709 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  N  e.  NN )
160159, 5syl 17 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  D  e.  Fin )
16120adantlr 698 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  f  e.  D
)  ->  ( * `  ( f `  A
) )  e.  CC )
16235, 161mulcld 8735 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  f  e.  D
)  ->  ( (
f `  ( L `  n ) )  x.  ( * `  (
f `  A )
) )  e.  CC )
163160, 42, 162fsummulc1 12124 . . . . . . . . . . 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 709 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  A  e.  U )
1653, 4, 8, 9, 12, 159, 32, 164sum2dchr 20345 . . . . . . . . . . . 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 5725 . . . . . . . . . . 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 453 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  f  e.  D
)  ->  ( (Λ `  n )  /  n
)  e.  CC )
168 mulass 8705 . . . . . . . . . . . . . 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 8858 . . . . . . . . . . . . . 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 2285 . . . . . . . . . . . . 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 1187 . . . . . . . . . . . 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 12053 . . . . . . . . . . 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 2293 . . . . . . . . . 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 2299 . . . . . . . . 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 2287 . . . . . . . 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 12053 . . . . . . 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 2289 . . . . . 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 12115 . . . . . 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 2285 . . . . 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 20325 . . . . . . . . . . 11  |-  ( N  e.  NN  ->  G  e.  Abel )
181 ablgrp 14929 . . . . . . . . . . 11  |-  ( G  e.  Abel  ->  G  e. 
Grp )
1822, 180, 1813syl 20 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR+ )  ->  G  e.  Grp )
1834, 70grpidcl 14345 . . . . . . . . . 10  |-  ( G  e.  Grp  ->  .1.  e.  D )
184182, 183syl 17 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR+ )  ->  .1.  e.  D )
18550mulid1d 8732 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( log `  x )  x.  1 )  =  ( log `  x ) )
186185, 50eqeltrd 2327 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( log `  x )  x.  1 )  e.  CC )
187 iftrue 3476 . . . . . . . . . . 11  |-  ( f  =  .1.  ->  if ( f  =  .1. 
,  1 ,  if ( f  e.  W ,  -u 1 ,  0 ) )  =  1 )
188187oveq2d 5726 . . . . . . . . . 10  |-  ( f  =  .1.  ->  (
( log `  x
)  x.  if ( f  =  .1.  , 
1 ,  if ( f  e.  W ,  -u 1 ,  0 ) ) )  =  ( ( log `  x
)  x.  1 ) )
189188sumsn 12090 . . . . . . . . 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 645 . . . . . . . 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 3653 . . . . . . . . . . 11  |-  ( f  e.  ( D  \  {  .1.  } )  <->  ( f  e.  D  /\  f  =/=  .1.  ) )
192 ifnefalse 3478 . . . . . . . . . . . . . . 15  |-  ( f  =/=  .1.  ->  if ( f  =  .1. 
,  1 ,  if ( f  e.  W ,  -u 1 ,  0 ) )  =  if ( f  e.  W ,  -u 1 ,  0 ) )
193192ad2antll 712 . . . . . . . . . . . . . 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 8924 . . . . . . . . . . . . . . 15  |-  ( if ( f  e.  W ,  1 ,  0 )  =  1  ->  -u if ( f  e.  W ,  1 ,  0 )  =  -u
1 )
195 negeq 8924 . . . . . . . . . . . . . . . 16  |-  ( if ( f  e.  W ,  1 ,  0 )  =  0  ->  -u if ( f  e.  W ,  1 ,  0 )  =  -u
0 )
196 neg0 8973 . . . . . . . . . . . . . . . 16  |-  -u 0  =  0
197195, 196syl6eq 2301 . . . . . . . . . . . . . . 15  |-  ( if ( f  e.  W ,  1 ,  0 )  =  0  ->  -u if ( f  e.  W ,  1 ,  0 )  =  0 )
198194, 197ifsb 3479 . . . . . . . . . . . . . 14  |-  -u if ( f  e.  W ,  1 ,  0 )  =  if ( f  e.  W ,  -u 1 ,  0 )
199193, 198syl6eqr 2303 . . . . . . . . . . . . 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 5726 . . . . . . . . . . . 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 453 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
f  e.  D  /\  f  =/=  .1.  ) )  ->  ( log `  x
)  e.  CC )
20252, 54keepel 3527 . . . . . . . . . . . . 13  |-  if ( f  e.  W , 
1 ,  0 )  e.  CC
203 mulneg2 9097 . . . . . . . . . . . . 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 646 . . . . . . . . . . . 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 2285 . . . . . . . . . . 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 463 . . . . . . . . . 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 12053 . . . . . . . . 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 6974 . . . . . . . . . . 11  |-  ( D  e.  Fin  ->  ( D  \  {  .1.  }
)  e.  Fin )
2096, 208syl 17 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( D  \  {  .1.  } )  e.  Fin )
21050adantr 453 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  ( D  \  {  .1.  } ) )  -> 
( log `  x
)  e.  CC )
211 mulcl 8701 . . . . . . . . . . 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 646 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  ( D  \  {  .1.  } ) )  -> 
( ( log `  x
)  x.  if ( f  e.  W , 
1 ,  0 ) )  e.  CC )
213209, 212fsumneg 12126 . . . . . . . . 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 12 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  ( D  \  {  .1.  } ) )  ->  if ( f  e.  W ,  1 ,  0 )  e.  CC )
215209, 50, 214fsummulc2 12123 . . . . . . . . . . 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 3179 . . . . . . . . . . . . . . . . 17  |-  { y  e.  ( D  \  {  .1.  } )  | 
sum_ m  e.  NN  ( ( y `  ( L `  m ) )  /  m )  =  0 }  C_  ( D  \  {  .1.  } )
218216, 217eqsstri 3129 . . . . . . . . . . . . . . . 16  |-  W  C_  ( D  \  {  .1.  } )
219 difss 3220 . . . . . . . . . . . . . . . 16  |-  ( D 
\  {  .1.  }
)  C_  D
220218, 219sstri 3109 . . . . . . . . . . . . . . 15  |-  W  C_  D
221 ssfi 6968 . . . . . . . . . . . . . . 15  |-  ( ( D  e.  Fin  /\  W  C_  D )  ->  W  e.  Fin )
2226, 220, 221sylancl 646 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR+ )  ->  W  e.  Fin )
223 fsumconst 12129 . . . . . . . . . . . . . 14  |-  ( ( W  e.  Fin  /\  1  e.  CC )  -> 
sum_ f  e.  W 
1  =  ( (
# `  W )  x.  1 ) )
224222, 52, 223sylancl 646 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ f  e.  W  1  =  ( ( # `  W
)  x.  1 ) )
225218a1i 12 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR+ )  ->  W  C_  ( D  \  {  .1.  }
) )
22652a1i 12 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  RR+ )  ->  1  e.  CC )
227226ralrimivw 2589 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR+ )  ->  A. f  e.  W  1  e.  CC )
228209olcd 384 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( D  \  {  .1.  }
)  C_  ( ZZ>= ` 
1 )  \/  ( D  \  {  .1.  }
)  e.  Fin )
)
229 sumss2 12076 . . . . . . . . . . . . . 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 1186 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ f  e.  W  1  =  sum_ f  e.  ( D  \  {  .1.  } ) if ( f  e.  W ,  1 ,  0 ) )
231 hashcl 11228 . . . . . . . . . . . . . . . 16  |-  ( W  e.  Fin  ->  ( # `
 W )  e. 
NN0 )
232222, 231syl 17 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( # `  W
)  e.  NN0 )
233232nn0cnd 9899 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( # `  W
)  e.  CC )
234233mulid1d 8732 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( # `
 W )  x.  1 )  =  (
# `  W )
)
235224, 230, 2343eqtr3d 2293 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ f  e.  ( D  \  {  .1.  } ) if ( f  e.  W , 
1 ,  0 )  =  ( # `  W
) )
236235oveq2d 5726 . . . . . . . . . . 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 2287 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ f  e.  ( D  \  {  .1.  } ) ( ( log `  x )  x.  if ( f  e.  W ,  1 ,  0 ) )  =  ( ( log `  x )  x.  ( # `
 W ) ) )
238237negeqd 8926 . . . . . . . . 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 2289 . . . . . . . 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 5728 . . . . . . 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 8735 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( log `  x )  x.  ( # `  W
) )  e.  CC )
242186, 241negsubd 9043 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( (
( log `  x
)  x.  1 )  +  -u ( ( log `  x )  x.  ( # `
 W ) ) )  =  ( ( ( log `  x
)  x.  1 )  -  ( ( log `  x )  x.  ( # `
 W ) ) ) )
243240, 242eqtrd 2285 . . . . . 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 3432 . . . . . . . 8  |-  ( {  .1.  }  i^i  ( D  \  {  .1.  }
) )  =  (/)
245244a1i 12 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( {  .1.  }  i^i  ( D 
\  {  .1.  }
) )  =  (/) )
246 undif2 3436 . . . . . . . 8  |-  ( {  .1.  }  u.  ( D  \  {  .1.  }
) )  =  ( {  .1.  }  u.  D )
247184snssd 3660 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR+ )  ->  {  .1.  } 
C_  D )
248 ssequn1 3255 . . . . . . . . 9  |-  ( {  .1.  }  C_  D  <->  ( {  .1.  }  u.  D )  =  D )
249247, 248sylib 190 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( {  .1.  }  u.  D )  =  D )
250246, 249syl5req 2298 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR+ )  ->  D  =  ( {  .1.  }  u.  ( D  \  {  .1.  } ) ) )
251245, 250, 6, 58fsumsplit 12089 . . . . . 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 9115 . . . . . 6  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( log `  x )  x.  ( 1  -  ( # `
 W ) ) )  =  ( ( ( log `  x
)  x.  1 )  -  ( ( log `  x )  x.  ( # `
 W ) ) ) )
253243, 251, 2523eqtr4rd 2296 . . . . 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 5728 . . . 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 2295 . . 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 4003 . 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 10243 . . . 4  |-  RR+  C_  RR
258257a1i 12 . . 3  |-  ( ph  -> 
RR+  C_  RR )
2591, 5syl 17 . . 3  |-  ( ph  ->  D  e.  Fin )
26018adantlr 698 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  (
f `  A )  e.  CC )
261260cjcld 11558 . . . . 5  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  (
* `  ( f `  A ) )  e.  CC )
26261, 58subcld 9037 . . . . 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 8735 . . . 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 631 . . 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 453 . . . 4  |-  ( ( ( ph  /\  f  e.  D )  /\  x  e.  RR+ )  ->  (
* `  ( f `  A ) )  e.  CC )
266262an32s 782 . . . 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 11970 . . . . 5  |-  ( (
RR+  C_  RR  /\  (
* `  ( f `  A ) )  e.  CC )  ->  (
x  e.  RR+  |->  ( * `
 ( f `  A ) ) )  e.  O ( 1 ) )
268257, 19, 267sylancr 647 . . . 4  |-  ( (
ph  /\  f  e.  D )  ->  (
x  e.  RR+  |->  ( * `
 ( f `  A ) ) )  e.  O ( 1 ) )
269 fveq1 5376 . . . . . . . . . . . 12  |-  ( f  =  .1.  ->  (
f `  ( L `  n ) )  =  (  .1.  `  ( L `  n )
) )
270269oveq1d 5725 . . . . . . . . . . 11  |-  ( f  =  .1.  ->  (
( f `  ( L `  n )
)  x.  ( (Λ `  n )  /  n
) )  =  ( (  .1.  `  ( L `  n )
)  x.  ( (Λ `  n )  /  n
) ) )
271270sumeq2sdv 12054 . . . . . . . . . 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 5728 . . . . . . . . 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 454 . . . . . . . 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 8741 . . . . . . . . . 10  |-  ( x  e.  RR+  ->  ( log `  x )  e.  CC )
275274mulid1d 8732 . . . . . . . . 9  |-  ( x  e.  RR+  ->  ( ( log `  x )  x.  1 )  =  ( log `  x
) )
276275oveq2d 5726 . . . . . . . 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 2305 . . . . . . 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 4003 . . . . . 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 20468 . . . . . . 7  |-  ( ph  ->  ( x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (  .1.  `  ( L `  n ) )  x.  ( (Λ `  n )  /  n
) )  -  ( log `  x ) ) )  e.  O ( 1 ) )
280279ad2antrr 709 . . . . . 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 2327 . . . . 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 5726 . . . . . . . . . 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 5726 . . . . . . . . 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 698 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  f  e.  D )  /\  x  e.  RR+ )  ->  ( log `  x )  e.  CC )
285 mulcom 8703 . . . . . . . . . . . . . . 15  |-  ( ( ( log `  x
)  e.  CC  /\  -u 1  e.  CC )  ->  ( ( log `  x )  x.  -u 1
)  =  ( -u
1  x.  ( log `  x ) ) )
286284, 53, 285sylancl 646 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  f  e.  D )  /\  x  e.  RR+ )  ->  (
( log `  x
)  x.  -u 1
)  =  ( -u
1  x.  ( log `  x ) ) )
287284mulm1d 9111 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  f  e.  D )  /\  x  e.  RR+ )  ->  ( -u 1  x.  ( log `  x ) )  = 
-u ( log `  x
) )
288286, 287eqtrd 2285 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  f  e.  D )  /\  x  e.  RR+ )  ->  (
( log `  x
)  x.  -u 1
)  =  -u ( log `  x ) )
289284mul01d 8891 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  f  e.  D )  /\  x  e.  RR+ )  ->  (
( log `  x
)  x.  0 )  =  0 )
290288, 289ifeq12d 3486 . . . . . . . . . . . 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 5718 . . . . . . . . . . . . 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 5718 . . . . . . . . . . . . 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 3479 . . . . . . . . . . . 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 8924 . . . . . . . . . . . . 13  |-  ( if ( f  e.  W ,  ( log `  x
) ,  0 )  =  ( log `  x
)  ->  -u if ( f  e.  W , 
( log `  x
) ,  0 )  =  -u ( log `  x
) )
295 negeq 8924 . . . . . . . . . . . . . 14  |-  ( if ( f  e.  W ,  ( log `  x
) ,  0 )  =  0  ->  -u if ( f  e.  W ,  ( log `  x
) ,  0 )  =  -u 0 )
296295, 196syl6eq 2301 . . . . . . . . . . . . 13  |-  ( if ( f  e.  W ,  ( log `  x
) ,  0 )  =  0  ->  -u if ( f  e.  W ,  ( log `  x
) ,  0 )  =  0 )
297294, 296ifsb 3479 . . . . . . . . . . . 12  |-  -u if ( f  e.  W ,  ( log `  x
) ,  0 )  =  if ( f  e.  W ,  -u ( log `  x ) ,  0 )
298290, 293, 2973eqtr4g 2310 . . . . . . . . . . 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 5726 . . . . . . . . . 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 782 . . . . . . . . . . 11  |-  ( ( ( ph  /\  f  e.  D )  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( f `  ( L `  n ) )  x.  ( (Λ `  n )  /  n
) )  e.  CC )
301 ifcl 3506 . . . . . . . . . . . 12  |-  ( ( ( log `  x
)  e.  CC  /\  0  e.  CC )  ->  if ( f  e.  W ,  ( log `  x ) ,  0 )  e.  CC )
302284, 54, 301sylancl 646 . . . . . . . . . . 11  |-  ( ( ( ph  /\  f  e.  D )  /\  x  e.  RR+ )  ->  if ( f  e.  W ,  ( log `  x
) ,  0 )  e.  CC )
303300, 302subnegd 9044 . . . . . . . . . 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 2285 . . . . . . . . 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 2307 . . . . . . . 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 782 . . . . . . 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 4003 . . . . . 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 709 . . . . . . . 8  |-  ( ( ( ph  /\  f  e.  D )  /\  f  =/=  .1.  )  ->  N  e.  NN )
309 simplr 734 . . . . . . . 8  |-  ( ( ( ph  /\  f  e.  D )  /\  f  =/=  .1.  )  ->  f  e.  D )
310 simpr 449 . . . . . . . 8  |-  ( ( ( ph  /\  f  e.  D )  /\  f  =/=  .1.  )  ->  f  =/=  .1.  )
311 eqid 2253 . . . . . . . 8  |-  ( a  e.  NN  |->  ( ( f `  ( L `
 a ) )  /  a ) )  =  ( a  e.  NN  |->  ( ( f `
 ( L `  a ) )  / 
a ) )
3128, 25, 308, 3, 4, 70, 309, 310, 311dchrmusumlema 20474 . . . . . . 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 453 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  f  e.  D )  ->  N  e.  NN )
314313ad2antrr 709 . . . . . . . . . . . . 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 453 . . . . . . . . . . . . 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 734 . . . . . . . . . . . . 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 735 . . . . . . . . . . . . 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 743 . . . . . . . . . . . . 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 744 . . . . . . . . . . . . 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 20485 . . . . . . . . . . . 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 3487 . . . . . . . . . . . . . 14  |-  ( ( f  e.  W  <->  t  = 
0 )  ->  if ( f  e.  W ,  ( log `  x
) ,  0 )  =  if ( t  =  0 ,  ( log `  x ) ,  0 ) )
322321oveq2d 5726 . . . . . . . . . . . . 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 4004 . . . . . . . . . . . 12  |-  ( ( f  e.  W  <->  t  = 
0 )  ->  (
x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( f `  ( L `