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

Theorem rpvmasum2 23822
Description: A partial result along the lines of rpvmasum 23836. 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 465 . . . . . 6  |-  ( (
ph  /\  x  e.  RR+ )  ->  N  e.  NN )
3 rpvmasum2.g . . . . . . 7  |-  G  =  (DChr `  N )
4 rpvmasum2.d . . . . . . 7  |-  D  =  ( Base `  G
)
53, 4dchrfi 23655 . . . . . 6  |-  ( N  e.  NN  ->  D  e.  Fin )
62, 5syl 16 . . . . 5  |-  ( (
ph  /\  x  e.  RR+ )  ->  D  e.  Fin )
7 fzfid 12085 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  (
1 ... ( |_ `  x ) )  e. 
Fin )
8 rpvmasum.z . . . . . . . . . . . . 13  |-  Z  =  (ℤ/n `  N )
9 eqid 2457 . . . . . . . . . . . . 13  |-  ( Base `  Z )  =  (
Base `  Z )
10 simpr 461 . . . . . . . . . . . . 13  |-  ( (
ph  /\  f  e.  D )  ->  f  e.  D )
113, 8, 4, 9, 10dchrf 23642 . . . . . . . . . . . 12  |-  ( (
ph  /\  f  e.  D )  ->  f : ( Base `  Z
) --> CC )
12 rpvmasum2.u . . . . . . . . . . . . . . 15  |-  U  =  (Unit `  Z )
139, 12unitss 17435 . . . . . . . . . . . . . 14  |-  U  C_  ( Base `  Z )
14 rpvmasum2.b . . . . . . . . . . . . . 14  |-  ( ph  ->  A  e.  U )
1513, 14sseldi 3497 . . . . . . . . . . . . 13  |-  ( ph  ->  A  e.  ( Base `  Z ) )
1615adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  f  e.  D )  ->  A  e.  ( Base `  Z
) )
1711, 16ffvelrnd 6033 . . . . . . . . . . 11  |-  ( (
ph  /\  f  e.  D )  ->  (
f `  A )  e.  CC )
1817cjcld 13040 . . . . . . . . . 10  |-  ( (
ph  /\  f  e.  D )  ->  (
* `  ( f `  A ) )  e.  CC )
1918adantlr 714 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  (
* `  ( f `  A ) )  e.  CC )
2019adantrl 715 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
n  e.  ( 1 ... ( |_ `  x ) )  /\  f  e.  D )
)  ->  ( * `  ( f `  A
) )  e.  CC )
2111adantlr 714 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  f : ( Base `  Z
) --> CC )
2221adantlr 714 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  f  e.  D
)  ->  f :
( Base `  Z ) --> CC )
231nnnn0d 10873 . . . . . . . . . . . . . . 15  |-  ( ph  ->  N  e.  NN0 )
24 rpvmasum.l . . . . . . . . . . . . . . . 16  |-  L  =  ( ZRHom `  Z
)
258, 9, 24znzrhfo 18712 . . . . . . . . . . . . . . 15  |-  ( N  e.  NN0  ->  L : ZZ -onto-> ( Base `  Z
) )
26 fof 5801 . . . . . . . . . . . . . . 15  |-  ( L : ZZ -onto-> ( Base `  Z )  ->  L : ZZ --> ( Base `  Z
) )
2723, 25, 263syl 20 . . . . . . . . . . . . . 14  |-  ( ph  ->  L : ZZ --> ( Base `  Z ) )
2827adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR+ )  ->  L : ZZ
--> ( Base `  Z
) )
29 elfzelz 11713 . . . . . . . . . . . . 13  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  ZZ )
30 ffvelrn 6030 . . . . . . . . . . . . 13  |-  ( ( L : ZZ --> ( Base `  Z )  /\  n  e.  ZZ )  ->  ( L `  n )  e.  ( Base `  Z
) )
3128, 29, 30syl2an 477 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( L `  n )  e.  (
Base `  Z )
)
3231adantr 465 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  f  e.  D
)  ->  ( L `  n )  e.  (
Base `  Z )
)
3322, 32ffvelrnd 6033 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  f  e.  D
)  ->  ( f `  ( L `  n
) )  e.  CC )
3433anasss 647 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
n  e.  ( 1 ... ( |_ `  x ) )  /\  f  e.  D )
)  ->  ( f `  ( L `  n
) )  e.  CC )
35 elfznn 11739 . . . . . . . . . . . . . 14  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  NN )
3635adantl 466 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  NN )
37 vmacl 23517 . . . . . . . . . . . . 13  |-  ( n  e.  NN  ->  (Λ `  n )  e.  RR )
3836, 37syl 16 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (Λ `  n
)  e.  RR )
3938, 36nndivred 10605 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  /  n
)  e.  RR )
4039recnd 9639 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  /  n
)  e.  CC )
4140adantrr 716 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
n  e.  ( 1 ... ( |_ `  x ) )  /\  f  e.  D )
)  ->  ( (Λ `  n )  /  n
)  e.  CC )
4234, 41mulcld 9633 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
n  e.  ( 1 ... ( |_ `  x ) )  /\  f  e.  D )
)  ->  ( (
f `  ( L `  n ) )  x.  ( (Λ `  n
)  /  n ) )  e.  CC )
4320, 42mulcld 9633 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
n  e.  ( 1 ... ( |_ `  x ) )  /\  f  e.  D )
)  ->  ( (
* `  ( f `  A ) )  x.  ( ( f `  ( L `  n ) )  x.  ( (Λ `  n )  /  n
) ) )  e.  CC )
4443anass1rs 807 . . . . . 6  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  n  e.  (
1 ... ( |_ `  x ) ) )  ->  ( ( * `
 ( f `  A ) )  x.  ( ( f `  ( L `  n ) )  x.  ( (Λ `  n )  /  n
) ) )  e.  CC )
457, 44fsumcl 13566 . . . . 5  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( * `  ( f `  A
) )  x.  (
( f `  ( L `  n )
)  x.  ( (Λ `  n )  /  n
) ) )  e.  CC )
46 relogcl 23088 . . . . . . . . 9  |-  ( x  e.  RR+  ->  ( log `  x )  e.  RR )
4746adantl 466 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( log `  x )  e.  RR )
4847recnd 9639 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( log `  x )  e.  CC )
4948adantr 465 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  ( log `  x )  e.  CC )
50 ax-1cn 9567 . . . . . . 7  |-  1  e.  CC
51 neg1cn 10660 . . . . . . . 8  |-  -u 1  e.  CC
52 0cn 9605 . . . . . . . 8  |-  0  e.  CC
5351, 52keepel 4012 . . . . . . 7  |-  if ( f  e.  W ,  -u 1 ,  0 )  e.  CC
5450, 53keepel 4012 . . . . . 6  |-  if ( f  =  .1.  , 
1 ,  if ( f  e.  W ,  -u 1 ,  0 ) )  e.  CC
55 mulcl 9593 . . . . . 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 )
5649, 54, 55sylancl 662 . . . . 5  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  (
( log `  x
)  x.  if ( f  =  .1.  , 
1 ,  if ( f  e.  W ,  -u 1 ,  0 ) ) )  e.  CC )
576, 45, 56fsumsub 13614 . . . 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 ) ) ) ) )
5842anass1rs 807 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  n  e.  (
1 ... ( |_ `  x ) ) )  ->  ( ( f `
 ( L `  n ) )  x.  ( (Λ `  n
)  /  n ) )  e.  CC )
597, 58fsumcl 13566 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( f `  ( L `  n ) )  x.  ( (Λ `  n )  /  n
) )  e.  CC )
6019, 59, 56subdid 10033 . . . . . 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 ) ) ) ) ) )
617, 19, 58fsummulc2 13610 . . . . . . 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 ) ) ) )
6254a1i 11 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  if ( f  =  .1. 
,  1 ,  if ( f  e.  W ,  -u 1 ,  0 ) )  e.  CC )
6319, 49, 62mul12d 9806 . . . . . . . 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 ) ) ) ) )
64 ovif2 6379 . . . . . . . . . 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 ) ) )
65 fveq1 5871 . . . . . . . . . . . . . . . . 17  |-  ( f  =  .1.  ->  (
f `  A )  =  (  .1.  `  A
) )
66 rpvmasum2.1 . . . . . . . . . . . . . . . . . 18  |-  .1.  =  ( 0g `  G )
671ad2antrr 725 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  N  e.  NN )
6814ad2antrr 725 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  A  e.  U )
693, 8, 66, 12, 67, 68dchr1 23657 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  (  .1.  `  A )  =  1 )
7065, 69sylan9eqr 2520 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  f  =  .1.  )  ->  ( f `  A )  =  1 )
7170fveq2d 5876 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  f  =  .1.  )  ->  ( * `  ( f `  A
) )  =  ( * `  1 ) )
72 1re 9612 . . . . . . . . . . . . . . . 16  |-  1  e.  RR
73 cjre 12983 . . . . . . . . . . . . . . . 16  |-  ( 1  e.  RR  ->  (
* `  1 )  =  1 )
7472, 73ax-mp 5 . . . . . . . . . . . . . . 15  |-  ( * `
 1 )  =  1
7571, 74syl6eq 2514 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  f  =  .1.  )  ->  ( * `  ( f `  A
) )  =  1 )
7675oveq1d 6311 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  f  =  .1.  )  ->  ( ( * `
 ( f `  A ) )  x.  1 )  =  ( 1  x.  1 ) )
77 1t1e1 10704 . . . . . . . . . . . . 13  |-  ( 1  x.  1 )  =  1
7876, 77syl6eq 2514 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  f  =  .1.  )  ->  ( ( * `
 ( f `  A ) )  x.  1 )  =  1 )
7978ifeq1da 3974 . . . . . . . . . . 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 ) ) ) )
80 df-ne 2654 . . . . . . . . . . . . 13  |-  ( f  =/=  .1.  <->  -.  f  =  .1.  )
81 ovif2 6379 . . . . . . . . . . . . . 14  |-  ( ( * `  ( f `
 A ) )  x.  if ( f  e.  W ,  -u
1 ,  0 ) )  =  if ( f  e.  W , 
( ( * `  ( f `  A
) )  x.  -u 1
) ,  ( ( * `  ( f `
 A ) )  x.  0 ) )
82 simplll 759 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  f  =/=  .1.  )  ->  ph )
83 rpvmasum2.z1 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  f  e.  W )  ->  A  =  ( 1r `  Z ) )
8483fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  f  e.  W )  ->  (
f `  A )  =  ( f `  ( 1r `  Z ) ) )
8582, 84sylan 471 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D
)  /\  f  =/=  .1.  )  /\  f  e.  W )  ->  (
f `  A )  =  ( f `  ( 1r `  Z ) ) )
863, 8, 4dchrmhm 23641 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  D  C_  ( (mulGrp `  Z ) MndHom  (mulGrp ` fld ) )
87 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  f  e.  D )
8886, 87sseldi 3497 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  f  e.  ( (mulGrp `  Z
) MndHom  (mulGrp ` fld ) ) )
89 eqid 2457 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  (mulGrp `  Z )  =  (mulGrp `  Z )
90 eqid 2457 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 1r
`  Z )  =  ( 1r `  Z
)
9189, 90ringidval 17281 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 1r
`  Z )  =  ( 0g `  (mulGrp `  Z ) )
92 eqid 2457 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  (mulGrp ` fld )  =  (mulGrp ` fld )
93 cnfld1 18569 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  1  =  ( 1r ` fld )
9492, 93ringidval 17281 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  1  =  ( 0g `  (mulGrp ` fld ) )
9591, 94mhm0 16100 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( f  e.  ( (mulGrp `  Z ) MndHom  (mulGrp ` fld ) )  ->  (
f `  ( 1r `  Z ) )  =  1 )
9688, 95syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  (
f `  ( 1r `  Z ) )  =  1 )
9796ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D
)  /\  f  =/=  .1.  )  /\  f  e.  W )  ->  (
f `  ( 1r `  Z ) )  =  1 )
9885, 97eqtrd 2498 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D
)  /\  f  =/=  .1.  )  /\  f  e.  W )  ->  (
f `  A )  =  1 )
9998fveq2d 5876 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D
)  /\  f  =/=  .1.  )  /\  f  e.  W )  ->  (
* `  ( f `  A ) )  =  ( * `  1
) )
10099, 74syl6eq 2514 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D
)  /\  f  =/=  .1.  )  /\  f  e.  W )  ->  (
* `  ( f `  A ) )  =  1 )
101100oveq1d 6311 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D
)  /\  f  =/=  .1.  )  /\  f  e.  W )  ->  (
( * `  (
f `  A )
)  x.  -u 1
)  =  ( 1  x.  -u 1 ) )
10251mulid2i 9616 . . . . . . . . . . . . . . . . 17  |-  ( 1  x.  -u 1 )  = 
-u 1
103101, 102syl6eq 2514 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D
)  /\  f  =/=  .1.  )  /\  f  e.  W )  ->  (
( * `  (
f `  A )
)  x.  -u 1
)  =  -u 1
)
104103ifeq1da 3974 . . . . . . . . . . . . . . 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 ) ) )
10519adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  f  =/=  .1.  )  ->  ( * `  ( f `  A
) )  e.  CC )
106105mul01d 9796 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  f  =/=  .1.  )  ->  ( ( * `
 ( f `  A ) )  x.  0 )  =  0 )
107106ifeq2d 3963 . . . . . . . . . . . . . . 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 ) )
108104, 107eqtrd 2498 . . . . . . . . . . . . . 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 ) )
10981, 108syl5eq 2510 . . . . . . . . . . . . 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 ) )
11080, 109sylan2br 476 . . . . . . . . . . . 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 ) )
111110ifeq2da 3975 . . . . . . . . . . 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 ) ) )
11279, 111eqtrd 2498 . . . . . . . . . 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 ) ) )
11364, 112syl5eq 2510 . . . . . . . . 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 ) ) )
114113oveq2d 6312 . . . . . . . 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 ) ) ) )
11563, 114eqtrd 2498 . . . . . . 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 ) ) ) )
11661, 115oveq12d 6314 . . . . . 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 ) ) ) ) )
11760, 116eqtrd 2498 . . . . 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 ) ) ) ) )
118117sumeq2dv 13536 . . . 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 ) ) ) ) )
119 fzfid 12085 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( 1 ... ( |_ `  x ) )  e. 
Fin )
120 inss1 3714 . . . . . . . . 9  |-  ( ( 1 ... ( |_
`  x ) )  i^i  T )  C_  ( 1 ... ( |_ `  x ) )
121 ssfi 7759 . . . . . . . . 9  |-  ( ( ( 1 ... ( |_ `  x ) )  e.  Fin  /\  (
( 1 ... ( |_ `  x ) )  i^i  T )  C_  ( 1 ... ( |_ `  x ) ) )  ->  ( (
1 ... ( |_ `  x ) )  i^i 
T )  e.  Fin )
122119, 120, 121sylancl 662 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( (
1 ... ( |_ `  x ) )  i^i 
T )  e.  Fin )
1232phicld 14313 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( phi `  N )  e.  NN )
124123nncnd 10572 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( phi `  N )  e.  CC )
125120a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( (
1 ... ( |_ `  x ) )  i^i 
T )  C_  (
1 ... ( |_ `  x ) ) )
126125sselda 3499 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( ( 1 ... ( |_ `  x
) )  i^i  T
) )  ->  n  e.  ( 1 ... ( |_ `  x ) ) )
127126, 40syldan 470 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( ( 1 ... ( |_ `  x
) )  i^i  T
) )  ->  (
(Λ `  n )  /  n )  e.  CC )
128122, 124, 127fsummulc2 13610 . . . . . . 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
) ) )
129124adantr 465 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( phi `  N )  e.  CC )
130129, 40mulcld 9633 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( phi `  N )  x.  ( (Λ `  n
)  /  n ) )  e.  CC )
131126, 130syldan 470 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( ( 1 ... ( |_ `  x
) )  i^i  T
) )  ->  (
( phi `  N
)  x.  ( (Λ `  n )  /  n
) )  e.  CC )
132131ralrimiva 2871 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  A. n  e.  ( ( 1 ... ( |_ `  x
) )  i^i  T
) ( ( phi `  N )  x.  (
(Λ `  n )  /  n ) )  e.  CC )
133119olcd 393 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( (
1 ... ( |_ `  x ) )  C_  ( ZZ>= `  1 )  \/  ( 1 ... ( |_ `  x ) )  e.  Fin ) )
134 sumss2 13559 . . . . . . . 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 ) )
135125, 132, 133, 134syl21anc 1227 . . . . . . 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 ) )
136 elin 3683 . . . . . . . . . . . . 13  |-  ( n  e.  ( ( 1 ... ( |_ `  x ) )  i^i 
T )  <->  ( n  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  T
) )
137136baib 903 . . . . . . . . . . . 12  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  (
n  e.  ( ( 1 ... ( |_
`  x ) )  i^i  T )  <->  n  e.  T ) )
138137adantl 466 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  e.  ( ( 1 ... ( |_ `  x
) )  i^i  T
)  <->  n  e.  T
) )
139 rpvmasum2.t . . . . . . . . . . . . 13  |-  T  =  ( `' L " { A } )
140139eleq2i 2535 . . . . . . . . . . . 12  |-  ( n  e.  T  <->  n  e.  ( `' L " { A } ) )
141 ffn 5737 . . . . . . . . . . . . . 14  |-  ( L : ZZ --> ( Base `  Z )  ->  L  Fn  ZZ )
14228, 141syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR+ )  ->  L  Fn  ZZ )
143 fniniseg 6009 . . . . . . . . . . . . . 14  |-  ( L  Fn  ZZ  ->  (
n  e.  ( `' L " { A } )  <->  ( n  e.  ZZ  /\  ( L `
 n )  =  A ) ) )
144143baibd 909 . . . . . . . . . . . . 13  |-  ( ( L  Fn  ZZ  /\  n  e.  ZZ )  ->  ( n  e.  ( `' L " { A } )  <->  ( L `  n )  =  A ) )
145142, 29, 144syl2an 477 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  e.  ( `' L " { A } )  <->  ( L `  n )  =  A ) )
146140, 145syl5bb 257 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  e.  T  <->  ( L `  n )  =  A ) )
147138, 146bitr2d 254 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( L `  n )  =  A  <->  n  e.  (
( 1 ... ( |_ `  x ) )  i^i  T ) ) )
14840mul02d 9795 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 0  x.  ( (Λ `  n
)  /  n ) )  =  0 )
149147, 148ifbieq2d 3969 . . . . . . . . 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 ) )
150 ovif 6378 . . . . . . . . . 10  |-  ( if ( ( L `  n )  =  A ,  ( phi `  N ) ,  0 )  x.  ( (Λ `  n )  /  n
) )  =  if ( ( L `  n )  =  A ,  ( ( phi `  N )  x.  (
(Λ `  n )  /  n ) ) ,  ( 0  x.  (
(Λ `  n )  /  n ) ) )
1511ad2antrr 725 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  N  e.  NN )
152151, 5syl 16 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  D  e.  Fin )
15319adantlr 714 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  f  e.  D
)  ->  ( * `  ( f `  A
) )  e.  CC )
15433, 153mulcld 9633 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  f  e.  D
)  ->  ( (
f `  ( L `  n ) )  x.  ( * `  (
f `  A )
) )  e.  CC )
155152, 40, 154fsummulc1 13611 . . . . . . . . . . 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 ) ) )
15614ad2antrr 725 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  A  e.  U )
1573, 4, 8, 9, 12, 151, 31, 156sum2dchr 23674 . . . . . . . . . . . 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 ) )
158157oveq1d 6311 . . . . . . . . . . 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
) ) )
15940adantr 465 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  f  e.  D
)  ->  ( (Λ `  n )  /  n
)  e.  CC )
160 mulass 9597 . . . . . . . . . . . . . 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 ) ) ) )
161 mul12 9763 . . . . . . . . . . . . . 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
) ) ) )
162160, 161eqtrd 2498 . . . . . . . . . . . . 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 ) ) ) )
16333, 153, 159, 162syl3anc 1228 . . . . . . . . . . . 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 ) ) ) )
164163sumeq2dv 13536 . . . . . . . . . . 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
) ) ) )
165155, 158, 1643eqtr3d 2506 . . . . . . . . . 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 ) ) ) )
166150, 165syl5eqr 2512 . . . . . . . . 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
) ) ) )
167149, 166eqtr3d 2500 . . . . . . . 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 ) ) ) )
168167sumeq2dv 13536 . . . . . . 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
) ) ) )
169128, 135, 1683eqtrd 2502 . . . . . 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 ) ) ) )
170119, 6, 43fsumcom 13601 . . . . . 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 ) ) ) )
171169, 170eqtrd 2498 . . . . 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 ) ) ) )
1723dchrabl 23654 . . . . . . . . . 10  |-  ( N  e.  NN  ->  G  e.  Abel )
173 ablgrp 16929 . . . . . . . . . 10  |-  ( G  e.  Abel  ->  G  e. 
Grp )
1744, 66grpidcl 16204 . . . . . . . . . 10  |-  ( G  e.  Grp  ->  .1.  e.  D )
1752, 172, 173, 1744syl 21 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR+ )  ->  .1.  e.  D )
17648mulid1d 9630 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( log `  x )  x.  1 )  =  ( log `  x ) )
177176, 48eqeltrd 2545 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( log `  x )  x.  1 )  e.  CC )
178 iftrue 3950 . . . . . . . . . . 11  |-  ( f  =  .1.  ->  if ( f  =  .1. 
,  1 ,  if ( f  e.  W ,  -u 1 ,  0 ) )  =  1 )
179178oveq2d 6312 . . . . . . . . . 10  |-  ( f  =  .1.  ->  (
( log `  x
)  x.  if ( f  =  .1.  , 
1 ,  if ( f  e.  W ,  -u 1 ,  0 ) ) )  =  ( ( log `  x
)  x.  1 ) )
180179sumsn 13574 . . . . . . . . 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 ) )
181175, 177, 180syl2anc 661 . . . . . . . 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 ) )
182 eldifsn 4157 . . . . . . . . . . 11  |-  ( f  e.  ( D  \  {  .1.  } )  <->  ( f  e.  D  /\  f  =/=  .1.  ) )
183 ifnefalse 3956 . . . . . . . . . . . . . . 15  |-  ( f  =/=  .1.  ->  if ( f  =  .1. 
,  1 ,  if ( f  e.  W ,  -u 1 ,  0 ) )  =  if ( f  e.  W ,  -u 1 ,  0 ) )
184183ad2antll 728 . . . . . . . . . . . . . 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 ) )
185 negeq 9831 . . . . . . . . . . . . . . 15  |-  ( if ( f  e.  W ,  1 ,  0 )  =  1  ->  -u if ( f  e.  W ,  1 ,  0 )  =  -u
1 )
186 negeq 9831 . . . . . . . . . . . . . . . 16  |-  ( if ( f  e.  W ,  1 ,  0 )  =  0  ->  -u if ( f  e.  W ,  1 ,  0 )  =  -u
0 )
187 neg0 9884 . . . . . . . . . . . . . . . 16  |-  -u 0  =  0
188186, 187syl6eq 2514 . . . . . . . . . . . . . . 15  |-  ( if ( f  e.  W ,  1 ,  0 )  =  0  ->  -u if ( f  e.  W ,  1 ,  0 )  =  0 )
189185, 188ifsb 3957 . . . . . . . . . . . . . 14  |-  -u if ( f  e.  W ,  1 ,  0 )  =  if ( f  e.  W ,  -u 1 ,  0 )
190184, 189syl6eqr 2516 . . . . . . . . . . . . 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 ) )
191190oveq2d 6312 . . . . . . . . . . . 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 ) ) )
19248adantr 465 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
f  e.  D  /\  f  =/=  .1.  ) )  ->  ( log `  x
)  e.  CC )
19350, 52keepel 4012 . . . . . . . . . . . . 13  |-  if ( f  e.  W , 
1 ,  0 )  e.  CC
194 mulneg2 10015 . . . . . . . . . . . . 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 ) ) )
195192, 193, 194sylancl 662 . . . . . . . . . . . 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 ) ) )
196191, 195eqtrd 2498 . . . . . . . . . . 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 ) ) )
197182, 196sylan2b 475 . . . . . . . . . 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 ) ) )
198197sumeq2dv 13536 . . . . . . . . 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 ) ) )
199 diffi 7770 . . . . . . . . . . 11  |-  ( D  e.  Fin  ->  ( D  \  {  .1.  }
)  e.  Fin )
2006, 199syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( D  \  {  .1.  } )  e.  Fin )
20148adantr 465 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  ( D  \  {  .1.  } ) )  -> 
( log `  x
)  e.  CC )
202 mulcl 9593 . . . . . . . . . . 11  |-  ( ( ( log `  x
)  e.  CC  /\  if ( f  e.  W ,  1 ,  0 )  e.  CC )  ->  ( ( log `  x )  x.  if ( f  e.  W ,  1 ,  0 ) )  e.  CC )
203201, 193, 202sylancl 662 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  ( D  \  {  .1.  } ) )  -> 
( ( log `  x
)  x.  if ( f  e.  W , 
1 ,  0 ) )  e.  CC )
204200, 203fsumneg 13613 . . . . . . . . 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 ) ) )
205193a1i 11 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  ( D  \  {  .1.  } ) )  ->  if ( f  e.  W ,  1 ,  0 )  e.  CC )
206200, 48, 205fsummulc2 13610 . . . . . . . . . . 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 ) ) )
207 rpvmasum2.w . . . . . . . . . . . . . . . . 17  |-  W  =  { y  e.  ( D  \  {  .1.  } )  |  sum_ m  e.  NN  ( ( y `
 ( L `  m ) )  /  m )  =  0 }
208 ssrab2 3581 . . . . . . . . . . . . . . . . 17  |-  { y  e.  ( D  \  {  .1.  } )  | 
sum_ m  e.  NN  ( ( y `  ( L `  m ) )  /  m )  =  0 }  C_  ( D  \  {  .1.  } )
209207, 208eqsstri 3529 . . . . . . . . . . . . . . . 16  |-  W  C_  ( D  \  {  .1.  } )
210 difss 3627 . . . . . . . . . . . . . . . 16  |-  ( D 
\  {  .1.  }
)  C_  D
211209, 210sstri 3508 . . . . . . . . . . . . . . 15  |-  W  C_  D
212 ssfi 7759 . . . . . . . . . . . . . . 15  |-  ( ( D  e.  Fin  /\  W  C_  D )  ->  W  e.  Fin )
2136, 211, 212sylancl 662 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR+ )  ->  W  e.  Fin )
214 fsumconst 13616 . . . . . . . . . . . . . 14  |-  ( ( W  e.  Fin  /\  1  e.  CC )  -> 
sum_ f  e.  W 
1  =  ( (
# `  W )  x.  1 ) )
215213, 50, 214sylancl 662 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ f  e.  W  1  =  ( ( # `  W
)  x.  1 ) )
216209a1i 11 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR+ )  ->  W  C_  ( D  \  {  .1.  }
) )
21750a1i 11 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  RR+ )  ->  1  e.  CC )
218217ralrimivw 2872 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR+ )  ->  A. f  e.  W  1  e.  CC )
219200olcd 393 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( D  \  {  .1.  }
)  C_  ( ZZ>= ` 
1 )  \/  ( D  \  {  .1.  }
)  e.  Fin )
)
220 sumss2 13559 . . . . . . . . . . . . . 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 ) )
221216, 218, 219, 220syl21anc 1227 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ f  e.  W  1  =  sum_ f  e.  ( D  \  {  .1.  } ) if ( f  e.  W ,  1 ,  0 ) )
222 hashcl 12430 . . . . . . . . . . . . . . . 16  |-  ( W  e.  Fin  ->  ( # `
 W )  e. 
NN0 )
223213, 222syl 16 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( # `  W
)  e.  NN0 )
224223nn0cnd 10875 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( # `  W
)  e.  CC )
225224mulid1d 9630 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( # `
 W )  x.  1 )  =  (
# `  W )
)
226215, 221, 2253eqtr3d 2506 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ f  e.  ( D  \  {  .1.  } ) if ( f  e.  W , 
1 ,  0 )  =  ( # `  W
) )
227226oveq2d 6312 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( log `  x )  x. 
sum_ f  e.  ( D  \  {  .1.  } ) if ( f  e.  W ,  1 ,  0 ) )  =  ( ( log `  x )  x.  ( # `
 W ) ) )
228206, 227eqtr3d 2500 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ f  e.  ( D  \  {  .1.  } ) ( ( log `  x )  x.  if ( f  e.  W ,  1 ,  0 ) )  =  ( ( log `  x )  x.  ( # `
 W ) ) )
229228negeqd 9833 . . . . . . . . 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 ) ) )
230198, 204, 2293eqtrd 2502 . . . . . . . 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 ) ) )
231181, 230oveq12d 6314 . . . . . . 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 ) ) ) )
23248, 224mulcld 9633 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( log `  x )  x.  ( # `  W
) )  e.  CC )
233177, 232negsubd 9956 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( (
( log `  x
)  x.  1 )  +  -u ( ( log `  x )  x.  ( # `
 W ) ) )  =  ( ( ( log `  x
)  x.  1 )  -  ( ( log `  x )  x.  ( # `
 W ) ) ) )
234231, 233eqtrd 2498 . . . . . 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
) ) ) )
235 disjdif 3903 . . . . . . . 8  |-  ( {  .1.  }  i^i  ( D  \  {  .1.  }
) )  =  (/)
236235a1i 11 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( {  .1.  }  i^i  ( D 
\  {  .1.  }
) )  =  (/) )
237 undif2 3907 . . . . . . . 8  |-  ( {  .1.  }  u.  ( D  \  {  .1.  }
) )  =  ( {  .1.  }  u.  D )
238175snssd 4177 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR+ )  ->  {  .1.  } 
C_  D )
239 ssequn1 3670 . . . . . . . . 9  |-  ( {  .1.  }  C_  D  <->  ( {  .1.  }  u.  D )  =  D )
240238, 239sylib 196 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( {  .1.  }  u.  D )  =  D )
241237, 240syl5req 2511 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR+ )  ->  D  =  ( {  .1.  }  u.  ( D  \  {  .1.  } ) ) )
242236, 241, 6, 56fsumsplit 13573 . . . . . 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 ) ) ) ) )
24348, 217, 224subdid 10033 . . . . . 6  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( log `  x )  x.  ( 1  -  ( # `
 W ) ) )  =  ( ( ( log `  x
)  x.  1 )  -  ( ( log `  x )  x.  ( # `
 W ) ) ) )
244234, 242, 2433eqtr4rd 2509 . . . . 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 ) ) ) )
245171, 244oveq12d 6314 . . . 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 ) ) ) ) )
24657, 118, 2453eqtr4d 2508 . . 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
) ) ) ) )
247246mpteq2dva 4543 . 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
) ) ) ) ) )
248 rpssre 11255 . . . 4  |-  RR+  C_  RR
249248a1i 11 . . 3  |-  ( ph  -> 
RR+  C_  RR )
2501, 5syl 16 . . 3  |-  ( ph  ->  D  e.  Fin )
25117adantlr 714 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  (
f `  A )  e.  CC )
252251cjcld 13040 . . . . 5  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  (
* `  ( f `  A ) )  e.  CC )
25359, 56subcld 9950 . . . . 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 )
254252, 253mulcld 9633 . . . 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 )
255254anasss 647 . . 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 )
25618adantr 465 . . . 4  |-  ( ( ( ph  /\  f  e.  D )  /\  x  e.  RR+ )  ->  (
* `  ( f `  A ) )  e.  CC )
257253an32s 804 . . . 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 )
258 o1const 13453 . . . . 5  |-  ( (
RR+  C_  RR  /\  (
* `  ( f `  A ) )  e.  CC )  ->  (
x  e.  RR+  |->  ( * `
 ( f `  A ) ) )  e.  O(1) )
259248, 18, 258sylancr 663 . . . 4  |-  ( (
ph  /\  f  e.  D )  ->  (
x  e.  RR+  |->  ( * `
 ( f `  A ) ) )  e.  O(1) )
260 fveq1 5871 . . . . . . . . . . . 12  |-  ( f  =  .1.  ->  (
f `  ( L `  n ) )  =  (  .1.  `  ( L `  n )
) )
261260oveq1d 6311 . . . . . . . . . . 11  |-  ( f  =  .1.  ->  (
( f `  ( L `  n )
)  x.  ( (Λ `  n )  /  n
) )  =  ( (  .1.  `  ( L `  n )
)  x.  ( (Λ `  n )  /  n
) ) )
262261sumeq2sdv 13537 . . . . . . . . . 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 ) ) )
263262, 179oveq12d 6314 . . . . . . . . 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 ) ) )
264263adantl 466 . . . . . . . 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 ) ) )
26546recnd 9639 . . . . . . . . . 10  |-  ( x  e.  RR+  ->  ( log `  x )  e.  CC )
266265mulid1d 9630 . . . . . . . . 9  |-  ( x  e.  RR+  ->  ( ( log `  x )  x.  1 )  =  ( log `  x
) )
267266oveq2d 6312 . . . . . . . 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 ) ) )
268264, 267sylan9eq 2518 . . . . . . 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 ) ) )
269268mpteq2dva 4543 . . . . . 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 ) ) ) )
2708, 24, 1, 3, 4, 66rpvmasumlem 23797 . . . . . . 7  |-  ( ph  ->  ( x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (  .1.  `  ( L `  n ) )  x.  ( (Λ `  n )  /  n
) )  -  ( log `  x ) ) )  e.  O(1) )
271270ad2antrr 725 . . . . . 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) )
272269, 271eqeltrd 2545 . . . . 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) )
273183oveq2d 6312 . . . . . . . . . 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 ) ) )
274273oveq2d 6312 . . . . . . . . 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 ) ) ) )
27548adantlr 714 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  f  e.  D )  /\  x  e.  RR+ )  ->  ( log `  x )  e.  CC )
276 mulcom 9595 . . . . . . . . . . . . . . 15  |-  ( ( ( log `  x
)  e.  CC  /\  -u 1  e.  CC )  ->  ( ( log `  x )  x.  -u 1
)  =  ( -u
1  x.  ( log `  x ) ) )
277275, 51, 276sylancl 662 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  f  e.  D )  /\  x  e.  RR+ )  ->  (
( log `  x
)  x.  -u 1
)  =  ( -u
1  x.  ( log `  x ) ) )
278275mulm1d 10029 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  f  e.  D )  /\  x  e.  RR+ )  ->  ( -u 1  x.  ( log `  x ) )  = 
-u ( log `  x
) )
279277, 278eqtrd 2498 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  f  e.  D )  /\  x  e.  RR+ )  ->  (
( log `  x
)  x.  -u 1
)  =  -u ( log `  x ) )
280275mul01d 9796 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  f  e.  D )  /\  x  e.  RR+ )  ->  (
( log `  x
)  x.  0 )  =  0 )
281279, 280ifeq12d 3964 . . . . . . . . . . . 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 ) )
282 ovif2 6379 . . . . . . . . . . . 12  |-  ( ( log `  x )  x.  if ( f  e.  W ,  -u
1 ,  0 ) )  =  if ( f  e.  W , 
( ( log `  x
)  x.  -u 1
) ,  ( ( log `  x )  x.  0 ) )
283 negeq 9831 . . . . . . . . . . . . 13  |-  ( if ( f  e.  W ,  ( log `  x
) ,  0 )  =  ( log `  x
)  ->  -u if ( f  e.  W , 
( log `  x
) ,  0 )  =  -u ( log `  x
) )
284 negeq 9831 . . . . . . . . . . . . . 14  |-  ( if ( f  e.  W ,  ( log `  x
) ,  0 )  =  0  ->  -u if ( f  e.  W ,  ( log `  x
) ,  0 )  =  -u 0 )
285284, 187syl6eq 2514 . . . . . . . . . . . . 13  |-  ( if ( f  e.  W ,  ( log `  x
) ,  0 )  =  0  ->  -u if ( f  e.  W ,  ( log `  x
) ,  0 )  =  0 )
286283, 285ifsb 3957 . . . . . . . . . . . 12  |-  -u if ( f  e.  W ,  ( log `  x
) ,  0 )  =  if ( f  e.  W ,  -u ( log `  x ) ,  0 )
287281, 282, 2863eqtr4g 2523 . . . . . . . . . . 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 ) )
288287oveq2d 6312 . . . . . . . . . 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 ) ) )
28959an32s 804 . . . . . . . . . . 11  |-  ( ( ( ph  /\  f  e.  D )  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( f `  ( L `  n ) )  x.  ( (Λ `  n )  /  n
) )  e.  CC )
290 ifcl 3986 . . . . . . . . . . . 12  |-  ( ( ( log `  x
)  e.  CC  /\  0  e.  CC )  ->  if ( f  e.  W ,  ( log `  x ) ,  0 )  e.  CC )
291275, 52, 290sylancl 662 . . . . . . . . . . 11  |-  ( ( ( ph  /\  f  e.  D )  /\  x  e.  RR+ )  ->  if ( f  e.  W ,  ( log `  x
) ,  0 )  e.  CC )
292289, 291subnegd 9957 . . . . . . . . . 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 ) ) )
293288, 292eqtrd 2498 . . . . . . . . 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 ) ) )
294274, 293sylan9eqr 2520 . . . . . . . 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 ) ) )
295294an32s 804 . . . . . . 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 ) ) )
296295mpteq2dva 4543 . . . . . 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 ) ) ) )
2971ad2antrr 725 . . . . . . . 8  |-  ( ( ( ph  /\  f  e.  D )  /\  f  =/=  .1.  )  ->  N  e.  NN )
298 simplr 755 . . . . . . . 8  |-  ( ( ( ph  /\  f  e.  D )  /\  f  =/=  .1.  )  ->  f  e.  D )
299 simpr 461 . . . . . . . 8  |-  ( ( ( ph  /\  f  e.  D )  /\  f  =/=  .1.  )  ->  f  =/=  .1.  )
300 eqid 2457 . . . . . . . 8  |-  ( a  e.  NN  |->  ( ( f `  ( L `
 a ) )  /  a ) )  =  ( a  e.  NN  |->  ( ( f `
 ( L `  a ) )  / 
a ) )
3018, 24, 297, 3, 4, 66, 298, 299, 300dchrmusumlema 23803 . . . . . . 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
) ) )
3021adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  f  e.  D )  ->  N  e.  NN )
303302ad2antrr 725 . . . . . . . . . . . 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
) ) ) )  ->  N  e.  NN )
304298adantr 465 . . . . . . . . . . . 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.  D
)
305 simplr 755 . . . . . . . . . . . 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  =/=  .1.  )
306 simprl 756 . . . . . . . . . . . 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
) ) ) )  ->  c  e.  ( 0 [,) +oo )
)
307 simprrl 765 . . . . . . . . . . . 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
) ) ) )  ->  seq 1 (  +  ,  ( a  e.  NN  |->  ( ( f `
 ( L `  a ) )  / 
a ) ) )  ~~>  t )
308 simprrr 766 . . . . . . . . . . . 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
) ) ) )  ->  A. y  e.  ( 1 [,) +oo )
( abs `  (
(  seq 1 (  +  ,  ( a  e.  NN  |->  ( ( f `
 ( L `  a ) )  / 
a ) ) ) `
 ( |_ `  y ) )  -  t ) )  <_ 
( c  /  y
) )
3098, 24, 303, 3, 4, 66, 304, 305, 300, 306, 307, 308, 207dchrvmaeq0 23814 . . . . . . . . . . 11  |-  ( ( ( ( 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 ) )
310 ifbi 3965 . . . . . . . . . . . . 13  |-  ( ( f  e.  W  <->  t  = 
0 )  ->  if ( f  e.  W ,  ( log `  x
) ,  0 )  =  if ( t  =  0 ,  ( log `  x ) ,  0 ) )
311310oveq2d 6312 . . . . . . . . . . . 12  |-  ( ( 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 ) ) )
312311mpteq2dv 4544 . . . . . . . . . . 11  |-  ( ( 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 ) ) )  =  ( x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( f `  ( L `
 n ) )  x.  ( (Λ `  n
)  /  n ) )  +  if ( t  =  0 ,  ( log `  x
) ,  0 ) ) ) )
313309, 312syl 16 . . . . . . . . . 10  |-  ( ( ( ( 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
) ) ) )  ->  ( x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( f `  ( L `  n ) )  x.  ( (Λ `  n )  /  n
) )  +  if ( f  e.  W ,  ( log `  x
) ,  0 ) ) )  =  ( x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( f `  ( L `
 n ) )  x.  ( (Λ `  n
)  /  n ) )  +  if ( t  =  0 ,  ( log `  x
) ,  0 ) ) ) )
3148, 24, 303, 3, 4, 66, 304, 305, 300, 306, 307, 308dchrvmasumif 23813 . . . . . . . . . 10  |-  ( ( ( ( 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
) ) ) )  ->  ( x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( f `  ( L `  n ) )  x.  ( (Λ `  n )  /  n
) )  +  if ( t  =  0 ,  ( log `  x
) ,  0 ) ) )  e.  O(1) )
315313, 314eqeltrd 2545 . . . . . . . . 9  |-  ( ( ( ( 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
) ) ) )  ->  ( x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( f `  ( L `  n ) )  x.  ( (Λ `  n )  /  n
) )  +  if ( f  e.  W ,  ( log `  x
) ,  0 ) ) )  e.  O(1) )
316315rexlimdvaa 2950 . . . . . . . 8  |-  ( ( ( ph  /\  f  e.  D )  /\  f  =/=  .1.  )  ->  ( E. c  e.  (
0 [,) +oo )
(  seq