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

Theorem rpvmasum2 21198
Description: A partial result along the lines of rpvmasum 21212. 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 452 . . . . . 6  |-  ( (
ph  /\  x  e.  RR+ )  ->  N  e.  NN )
3 rpvmasum2.g . . . . . . 7  |-  G  =  (DChr `  N )
4 rpvmasum2.d . . . . . . 7  |-  D  =  ( Base `  G
)
53, 4dchrfi 21031 . . . . . 6  |-  ( N  e.  NN  ->  D  e.  Fin )
62, 5syl 16 . . . . 5  |-  ( (
ph  /\  x  e.  RR+ )  ->  D  e.  Fin )
7 fzfid 11304 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  (
1 ... ( |_ `  x ) )  e. 
Fin )
8 rpvmasum.z . . . . . . . . . . . . 13  |-  Z  =  (ℤ/n `  N )
9 eqid 2435 . . . . . . . . . . . . 13  |-  ( Base `  Z )  =  (
Base `  Z )
10 simpr 448 . . . . . . . . . . . . 13  |-  ( (
ph  /\  f  e.  D )  ->  f  e.  D )
113, 8, 4, 9, 10dchrf 21018 . . . . . . . . . . . 12  |-  ( (
ph  /\  f  e.  D )  ->  f : ( Base `  Z
) --> CC )
12 rpvmasum2.u . . . . . . . . . . . . . . 15  |-  U  =  (Unit `  Z )
139, 12unitss 15757 . . . . . . . . . . . . . 14  |-  U  C_  ( Base `  Z )
14 rpvmasum2.b . . . . . . . . . . . . . 14  |-  ( ph  ->  A  e.  U )
1513, 14sseldi 3338 . . . . . . . . . . . . 13  |-  ( ph  ->  A  e.  ( Base `  Z ) )
1615adantr 452 . . . . . . . . . . . 12  |-  ( (
ph  /\  f  e.  D )  ->  A  e.  ( Base `  Z
) )
1711, 16ffvelrnd 5863 . . . . . . . . . . 11  |-  ( (
ph  /\  f  e.  D )  ->  (
f `  A )  e.  CC )
1817cjcld 11993 . . . . . . . . . 10  |-  ( (
ph  /\  f  e.  D )  ->  (
* `  ( f `  A ) )  e.  CC )
1918adantlr 696 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  (
* `  ( f `  A ) )  e.  CC )
2019adantrl 697 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
n  e.  ( 1 ... ( |_ `  x ) )  /\  f  e.  D )
)  ->  ( * `  ( f `  A
) )  e.  CC )
2111adantlr 696 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  f : ( Base `  Z
) --> CC )
2221adantlr 696 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  f  e.  D
)  ->  f :
( Base `  Z ) --> CC )
231nnnn0d 10266 . . . . . . . . . . . . . . 15  |-  ( ph  ->  N  e.  NN0 )
24 rpvmasum.l . . . . . . . . . . . . . . . 16  |-  L  =  ( ZRHom `  Z
)
258, 9, 24znzrhfo 16820 . . . . . . . . . . . . . . 15  |-  ( N  e.  NN0  ->  L : ZZ -onto-> ( Base `  Z
) )
26 fof 5645 . . . . . . . . . . . . . . 15  |-  ( L : ZZ -onto-> ( Base `  Z )  ->  L : ZZ --> ( Base `  Z
) )
2723, 25, 263syl 19 . . . . . . . . . . . . . 14  |-  ( ph  ->  L : ZZ --> ( Base `  Z ) )
2827adantr 452 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR+ )  ->  L : ZZ
--> ( Base `  Z
) )
29 elfzelz 11051 . . . . . . . . . . . . 13  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  ZZ )
30 ffvelrn 5860 . . . . . . . . . . . . 13  |-  ( ( L : ZZ --> ( Base `  Z )  /\  n  e.  ZZ )  ->  ( L `  n )  e.  ( Base `  Z
) )
3128, 29, 30syl2an 464 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( L `  n )  e.  (
Base `  Z )
)
3231adantr 452 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  f  e.  D
)  ->  ( L `  n )  e.  (
Base `  Z )
)
3322, 32ffvelrnd 5863 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  f  e.  D
)  ->  ( f `  ( L `  n
) )  e.  CC )
3433anasss 629 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
n  e.  ( 1 ... ( |_ `  x ) )  /\  f  e.  D )
)  ->  ( f `  ( L `  n
) )  e.  CC )
35 elfznn 11072 . . . . . . . . . . . . . 14  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  NN )
3635adantl 453 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  NN )
37 vmacl 20893 . . . . . . . . . . . . 13  |-  ( n  e.  NN  ->  (Λ `  n )  e.  RR )
3836, 37syl 16 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (Λ `  n
)  e.  RR )
3938, 36nndivred 10040 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  /  n
)  e.  RR )
4039recnd 9106 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  /  n
)  e.  CC )
4140adantrr 698 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
n  e.  ( 1 ... ( |_ `  x ) )  /\  f  e.  D )
)  ->  ( (Λ `  n )  /  n
)  e.  CC )
4234, 41mulcld 9100 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
n  e.  ( 1 ... ( |_ `  x ) )  /\  f  e.  D )
)  ->  ( (
f `  ( L `  n ) )  x.  ( (Λ `  n
)  /  n ) )  e.  CC )
4320, 42mulcld 9100 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
n  e.  ( 1 ... ( |_ `  x ) )  /\  f  e.  D )
)  ->  ( (
* `  ( f `  A ) )  x.  ( ( f `  ( L `  n ) )  x.  ( (Λ `  n )  /  n
) ) )  e.  CC )
4443anass1rs 783 . . . . . 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 12519 . . . . 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 20465 . . . . . . . . 9  |-  ( x  e.  RR+  ->  ( log `  x )  e.  RR )
4746adantl 453 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( log `  x )  e.  RR )
4847recnd 9106 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( log `  x )  e.  CC )
4948adantr 452 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  ( log `  x )  e.  CC )
50 ax-1cn 9040 . . . . . . 7  |-  1  e.  CC
51 neg1cn 10059 . . . . . . . 8  |-  -u 1  e.  CC
52 0cn 9076 . . . . . . . 8  |-  0  e.  CC
5351, 52keepel 3788 . . . . . . 7  |-  if ( f  e.  W ,  -u 1 ,  0 )  e.  CC
5450, 53keepel 3788 . . . . . 6  |-  if ( f  =  .1.  , 
1 ,  if ( f  e.  W ,  -u 1 ,  0 ) )  e.  CC
55 mulcl 9066 . . . . . 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 644 . . . . 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 12563 . . . 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 783 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  n  e.  (
1 ... ( |_ `  x ) ) )  ->  ( ( f `
 ( L `  n ) )  x.  ( (Λ `  n
)  /  n ) )  e.  CC )
597, 58fsumcl 12519 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( f `  ( L `  n ) )  x.  ( (Λ `  n )  /  n
) )  e.  CC )
6019, 59, 56subdid 9481 . . . . . 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 12559 . . . . . . 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 9267 . . . . . . . 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 oveq2 6081 . . . . . . . . . . 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 ) )
65 oveq2 6081 . . . . . . . . . . 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 ) ) )
6664, 65ifsb 3740 . . . . . . . . . 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 ) ) )
67 fveq1 5719 . . . . . . . . . . . . . . . . 17  |-  ( f  =  .1.  ->  (
f `  A )  =  (  .1.  `  A
) )
68 rpvmasum2.1 . . . . . . . . . . . . . . . . . 18  |-  .1.  =  ( 0g `  G )
691ad2antrr 707 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  N  e.  NN )
7014ad2antrr 707 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  A  e.  U )
713, 8, 68, 12, 69, 70dchr1 21033 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  (  .1.  `  A )  =  1 )
7267, 71sylan9eqr 2489 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  f  =  .1.  )  ->  ( f `  A )  =  1 )
7372fveq2d 5724 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  f  =  .1.  )  ->  ( * `  ( f `  A
) )  =  ( * `  1 ) )
74 1re 9082 . . . . . . . . . . . . . . . 16  |-  1  e.  RR
75 cjre 11936 . . . . . . . . . . . . . . . 16  |-  ( 1  e.  RR  ->  (
* `  1 )  =  1 )
7674, 75ax-mp 8 . . . . . . . . . . . . . . 15  |-  ( * `
 1 )  =  1
7773, 76syl6eq 2483 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  f  =  .1.  )  ->  ( * `  ( f `  A
) )  =  1 )
7877oveq1d 6088 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  f  =  .1.  )  ->  ( ( * `
 ( f `  A ) )  x.  1 )  =  ( 1  x.  1 ) )
79 1t1e1 10118 . . . . . . . . . . . . 13  |-  ( 1  x.  1 )  =  1
8078, 79syl6eq 2483 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  f  =  .1.  )  ->  ( ( * `
 ( f `  A ) )  x.  1 )  =  1 )
8180ifeq1da 3756 . . . . . . . . . . 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 ) ) ) )
82 df-ne 2600 . . . . . . . . . . . . 13  |-  ( f  =/=  .1.  <->  -.  f  =  .1.  )
83 oveq2 6081 . . . . . . . . . . . . . . 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
) )
84 oveq2 6081 . . . . . . . . . . . . . . 15  |-  ( if ( f  e.  W ,  -u 1 ,  0 )  =  0  -> 
( ( * `  ( f `  A
) )  x.  if ( f  e.  W ,  -u 1 ,  0 ) )  =  ( ( * `  (
f `  A )
)  x.  0 ) )
8583, 84ifsb 3740 . . . . . . . . . . . . . 14  |-  ( ( * `  ( f `
 A ) )  x.  if ( f  e.  W ,  -u
1 ,  0 ) )  =  if ( f  e.  W , 
( ( * `  ( f `  A
) )  x.  -u 1
) ,  ( ( * `  ( f `
 A ) )  x.  0 ) )
86 simplll 735 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  f  =/=  .1.  )  ->  ph )
87 rpvmasum2.z1 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  f  e.  W )  ->  A  =  ( 1r `  Z ) )
8887fveq2d 5724 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  f  e.  W )  ->  (
f `  A )  =  ( f `  ( 1r `  Z ) ) )
8986, 88sylan 458 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D
)  /\  f  =/=  .1.  )  /\  f  e.  W )  ->  (
f `  A )  =  ( f `  ( 1r `  Z ) ) )
903, 8, 4dchrmhm 21017 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  D  C_  ( (mulGrp `  Z ) MndHom  (mulGrp ` fld ) )
91 simpr 448 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  f  e.  D )
9290, 91sseldi 3338 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  f  e.  ( (mulGrp `  Z
) MndHom  (mulGrp ` fld ) ) )
93 eqid 2435 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  (mulGrp `  Z )  =  (mulGrp `  Z )
94 eqid 2435 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 1r
`  Z )  =  ( 1r `  Z
)
9593, 94rngidval 15658 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 1r
`  Z )  =  ( 0g `  (mulGrp `  Z ) )
96 eqid 2435 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  (mulGrp ` fld )  =  (mulGrp ` fld )
97 cnfld1 16718 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  1  =  ( 1r ` fld )
9896, 97rngidval 15658 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  1  =  ( 0g `  (mulGrp ` fld ) )
9995, 98mhm0 14738 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( f  e.  ( (mulGrp `  Z ) MndHom  (mulGrp ` fld ) )  ->  (
f `  ( 1r `  Z ) )  =  1 )
10092, 99syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  (
f `  ( 1r `  Z ) )  =  1 )
101100ad2antrr 707 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D
)  /\  f  =/=  .1.  )  /\  f  e.  W )  ->  (
f `  ( 1r `  Z ) )  =  1 )
10289, 101eqtrd 2467 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D
)  /\  f  =/=  .1.  )  /\  f  e.  W )  ->  (
f `  A )  =  1 )
103102fveq2d 5724 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D
)  /\  f  =/=  .1.  )  /\  f  e.  W )  ->  (
* `  ( f `  A ) )  =  ( * `  1
) )
104103, 76syl6eq 2483 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D
)  /\  f  =/=  .1.  )  /\  f  e.  W )  ->  (
* `  ( f `  A ) )  =  1 )
105104oveq1d 6088 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D
)  /\  f  =/=  .1.  )  /\  f  e.  W )  ->  (
( * `  (
f `  A )
)  x.  -u 1
)  =  ( 1  x.  -u 1 ) )
10651mulid2i 9085 . . . . . . . . . . . . . . . . 17  |-  ( 1  x.  -u 1 )  = 
-u 1
107105, 106syl6eq 2483 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D
)  /\  f  =/=  .1.  )  /\  f  e.  W )  ->  (
( * `  (
f `  A )
)  x.  -u 1
)  =  -u 1
)
108107ifeq1da 3756 . . . . . . . . . . . . . . 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 ) ) )
10919adantr 452 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  f  =/=  .1.  )  ->  ( * `  ( f `  A
) )  e.  CC )
110109mul01d 9257 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  f  =/=  .1.  )  ->  ( ( * `
 ( f `  A ) )  x.  0 )  =  0 )
111110ifeq2d 3746 . . . . . . . . . . . . . . 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 ) )
112108, 111eqtrd 2467 . . . . . . . . . . . . . 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 ) )
11385, 112syl5eq 2479 . . . . . . . . . . . . 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 ) )
11482, 113sylan2br 463 . . . . . . . . . . . 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 ) )
115114ifeq2da 3757 . . . . . . . . . . 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 ) ) )
11681, 115eqtrd 2467 . . . . . . . . . 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 ) ) )
11766, 116syl5eq 2479 . . . . . . . . 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 ) ) )
118117oveq2d 6089 . . . . . . . 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 ) ) ) )
11963, 118eqtrd 2467 . . . . . . 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 ) ) ) )
12061, 119oveq12d 6091 . . . . . 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 ) ) ) ) )
12160, 120eqtrd 2467 . . . . 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 ) ) ) ) )
122121sumeq2dv 12489 . . . 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 ) ) ) ) )
123 fzfid 11304 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( 1 ... ( |_ `  x ) )  e. 
Fin )
124 inss1 3553 . . . . . . . . 9  |-  ( ( 1 ... ( |_
`  x ) )  i^i  T )  C_  ( 1 ... ( |_ `  x ) )
125 ssfi 7321 . . . . . . . . 9  |-  ( ( ( 1 ... ( |_ `  x ) )  e.  Fin  /\  (
( 1 ... ( |_ `  x ) )  i^i  T )  C_  ( 1 ... ( |_ `  x ) ) )  ->  ( (
1 ... ( |_ `  x ) )  i^i 
T )  e.  Fin )
126123, 124, 125sylancl 644 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( (
1 ... ( |_ `  x ) )  i^i 
T )  e.  Fin )
1272phicld 13153 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( phi `  N )  e.  NN )
128127nncnd 10008 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( phi `  N )  e.  CC )
129124a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( (
1 ... ( |_ `  x ) )  i^i 
T )  C_  (
1 ... ( |_ `  x ) ) )
130129sselda 3340 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( ( 1 ... ( |_ `  x
) )  i^i  T
) )  ->  n  e.  ( 1 ... ( |_ `  x ) ) )
131130, 40syldan 457 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( ( 1 ... ( |_ `  x
) )  i^i  T
) )  ->  (
(Λ `  n )  /  n )  e.  CC )
132126, 128, 131fsummulc2 12559 . . . . . . 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
) ) )
133128adantr 452 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( phi `  N )  e.  CC )
134133, 40mulcld 9100 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( phi `  N )  x.  ( (Λ `  n
)  /  n ) )  e.  CC )
135130, 134syldan 457 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( ( 1 ... ( |_ `  x
) )  i^i  T
) )  ->  (
( phi `  N
)  x.  ( (Λ `  n )  /  n
) )  e.  CC )
136135ralrimiva 2781 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  A. n  e.  ( ( 1 ... ( |_ `  x
) )  i^i  T
) ( ( phi `  N )  x.  (
(Λ `  n )  /  n ) )  e.  CC )
137123olcd 383 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( (
1 ... ( |_ `  x ) )  C_  ( ZZ>= `  1 )  \/  ( 1 ... ( |_ `  x ) )  e.  Fin ) )
138 sumss2 12512 . . . . . . . 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 ) )
139129, 136, 137, 138syl21anc 1183 . . . . . . 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 ) )
140 elin 3522 . . . . . . . . . . . . 13  |-  ( n  e.  ( ( 1 ... ( |_ `  x ) )  i^i 
T )  <->  ( n  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  T
) )
141140baib 872 . . . . . . . . . . . 12  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  (
n  e.  ( ( 1 ... ( |_
`  x ) )  i^i  T )  <->  n  e.  T ) )
142141adantl 453 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  e.  ( ( 1 ... ( |_ `  x
) )  i^i  T
)  <->  n  e.  T
) )
143 rpvmasum2.t . . . . . . . . . . . . 13  |-  T  =  ( `' L " { A } )
144143eleq2i 2499 . . . . . . . . . . . 12  |-  ( n  e.  T  <->  n  e.  ( `' L " { A } ) )
145 ffn 5583 . . . . . . . . . . . . . 14  |-  ( L : ZZ --> ( Base `  Z )  ->  L  Fn  ZZ )
14628, 145syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR+ )  ->  L  Fn  ZZ )
147 fniniseg 5843 . . . . . . . . . . . . . 14  |-  ( L  Fn  ZZ  ->  (
n  e.  ( `' L " { A } )  <->  ( n  e.  ZZ  /\  ( L `
 n )  =  A ) ) )
148147baibd 876 . . . . . . . . . . . . 13  |-  ( ( L  Fn  ZZ  /\  n  e.  ZZ )  ->  ( n  e.  ( `' L " { A } )  <->  ( L `  n )  =  A ) )
149146, 29, 148syl2an 464 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  e.  ( `' L " { A } )  <->  ( L `  n )  =  A ) )
150144, 149syl5bb 249 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  e.  T  <->  ( L `  n )  =  A ) )
151142, 150bitr2d 246 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( L `  n )  =  A  <->  n  e.  (
( 1 ... ( |_ `  x ) )  i^i  T ) ) )
15240mul02d 9256 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 0  x.  ( (Λ `  n
)  /  n ) )  =  0 )
153151, 152ifbieq2d 3751 . . . . . . . . 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 ) )
154 oveq1 6080 . . . . . . . . . . 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
) ) )
155 oveq1 6080 . . . . . . . . . . 11  |-  ( if ( ( L `  n )  =  A ,  ( phi `  N ) ,  0 )  =  0  -> 
( if ( ( L `  n )  =  A ,  ( phi `  N ) ,  0 )  x.  ( (Λ `  n
)  /  n ) )  =  ( 0  x.  ( (Λ `  n
)  /  n ) ) )
156154, 155ifsb 3740 . . . . . . . . . 10  |-  ( if ( ( L `  n )  =  A ,  ( phi `  N ) ,  0 )  x.  ( (Λ `  n )  /  n
) )  =  if ( ( L `  n )  =  A ,  ( ( phi `  N )  x.  (
(Λ `  n )  /  n ) ) ,  ( 0  x.  (
(Λ `  n )  /  n ) ) )
1571ad2antrr 707 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  N  e.  NN )
158157, 5syl 16 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  D  e.  Fin )
15919adantlr 696 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  f  e.  D
)  ->  ( * `  ( f `  A
) )  e.  CC )
16033, 159mulcld 9100 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  f  e.  D
)  ->  ( (
f `  ( L `  n ) )  x.  ( * `  (
f `  A )
) )  e.  CC )
161158, 40, 160fsummulc1 12560 . . . . . . . . . . 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 ) ) )
16214ad2antrr 707 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  A  e.  U )
1633, 4, 8, 9, 12, 157, 31, 162sum2dchr 21050 . . . . . . . . . . . 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 ) )
164163oveq1d 6088 . . . . . . . . . . 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
) ) )
16540adantr 452 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  f  e.  D
)  ->  ( (Λ `  n )  /  n
)  e.  CC )
166 mulass 9070 . . . . . . . . . . . . . 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 ) ) ) )
167 mul12 9224 . . . . . . . . . . . . . 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
) ) ) )
168166, 167eqtrd 2467 . . . . . . . . . . . . 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 ) ) ) )
16933, 159, 165, 168syl3anc 1184 . . . . . . . . . . . 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 ) ) ) )
170169sumeq2dv 12489 . . . . . . . . . . 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
) ) ) )
171161, 164, 1703eqtr3d 2475 . . . . . . . . . 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 ) ) ) )
172156, 171syl5eqr 2481 . . . . . . . . 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
) ) ) )
173153, 172eqtr3d 2469 . . . . . . . 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 ) ) ) )
174173sumeq2dv 12489 . . . . . . 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
) ) ) )
175132, 139, 1743eqtrd 2471 . . . . . 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 ) ) ) )
176123, 6, 43fsumcom 12551 . . . . . 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 ) ) ) )
177175, 176eqtrd 2467 . . . . 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 ) ) ) )
1783dchrabl 21030 . . . . . . . . . . 11  |-  ( N  e.  NN  ->  G  e.  Abel )
179 ablgrp 15409 . . . . . . . . . . 11  |-  ( G  e.  Abel  ->  G  e. 
Grp )
1802, 178, 1793syl 19 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR+ )  ->  G  e.  Grp )
1814, 68grpidcl 14825 . . . . . . . . . 10  |-  ( G  e.  Grp  ->  .1.  e.  D )
182180, 181syl 16 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR+ )  ->  .1.  e.  D )
18348mulid1d 9097 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( log `  x )  x.  1 )  =  ( log `  x ) )
184183, 48eqeltrd 2509 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( log `  x )  x.  1 )  e.  CC )
185 iftrue 3737 . . . . . . . . . . 11  |-  ( f  =  .1.  ->  if ( f  =  .1. 
,  1 ,  if ( f  e.  W ,  -u 1 ,  0 ) )  =  1 )
186185oveq2d 6089 . . . . . . . . . 10  |-  ( f  =  .1.  ->  (
( log `  x
)  x.  if ( f  =  .1.  , 
1 ,  if ( f  e.  W ,  -u 1 ,  0 ) ) )  =  ( ( log `  x
)  x.  1 ) )
187186sumsn 12526 . . . . . . . . 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 ) )
188182, 184, 187syl2anc 643 . . . . . . . 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 ) )
189 eldifsn 3919 . . . . . . . . . . 11  |-  ( f  e.  ( D  \  {  .1.  } )  <->  ( f  e.  D  /\  f  =/=  .1.  ) )
190 ifnefalse 3739 . . . . . . . . . . . . . . 15  |-  ( f  =/=  .1.  ->  if ( f  =  .1. 
,  1 ,  if ( f  e.  W ,  -u 1 ,  0 ) )  =  if ( f  e.  W ,  -u 1 ,  0 ) )
191190ad2antll 710 . . . . . . . . . . . . . 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 ) )
192 negeq 9290 . . . . . . . . . . . . . . 15  |-  ( if ( f  e.  W ,  1 ,  0 )  =  1  ->  -u if ( f  e.  W ,  1 ,  0 )  =  -u
1 )
193 negeq 9290 . . . . . . . . . . . . . . . 16  |-  ( if ( f  e.  W ,  1 ,  0 )  =  0  ->  -u if ( f  e.  W ,  1 ,  0 )  =  -u
0 )
194 neg0 9339 . . . . . . . . . . . . . . . 16  |-  -u 0  =  0
195193, 194syl6eq 2483 . . . . . . . . . . . . . . 15  |-  ( if ( f  e.  W ,  1 ,  0 )  =  0  ->  -u if ( f  e.  W ,  1 ,  0 )  =  0 )
196192, 195ifsb 3740 . . . . . . . . . . . . . 14  |-  -u if ( f  e.  W ,  1 ,  0 )  =  if ( f  e.  W ,  -u 1 ,  0 )
197191, 196syl6eqr 2485 . . . . . . . . . . . . 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 ) )
198197oveq2d 6089 . . . . . . . . . . . 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 ) ) )
19948adantr 452 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
f  e.  D  /\  f  =/=  .1.  ) )  ->  ( log `  x
)  e.  CC )
20050, 52keepel 3788 . . . . . . . . . . . . 13  |-  if ( f  e.  W , 
1 ,  0 )  e.  CC
201 mulneg2 9463 . . . . . . . . . . . . 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 ) ) )
202199, 200, 201sylancl 644 . . . . . . . . . . . 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 ) ) )
203198, 202eqtrd 2467 . . . . . . . . . . 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 ) ) )
204189, 203sylan2b 462 . . . . . . . . . 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 ) ) )
205204sumeq2dv 12489 . . . . . . . . 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 ) ) )
206 diffi 7331 . . . . . . . . . . 11  |-  ( D  e.  Fin  ->  ( D  \  {  .1.  }
)  e.  Fin )
2076, 206syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( D  \  {  .1.  } )  e.  Fin )
20848adantr 452 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  ( D  \  {  .1.  } ) )  -> 
( log `  x
)  e.  CC )
209 mulcl 9066 . . . . . . . . . . 11  |-  ( ( ( log `  x
)  e.  CC  /\  if ( f  e.  W ,  1 ,  0 )  e.  CC )  ->  ( ( log `  x )  x.  if ( f  e.  W ,  1 ,  0 ) )  e.  CC )
210208, 200, 209sylancl 644 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  ( D  \  {  .1.  } ) )  -> 
( ( log `  x
)  x.  if ( f  e.  W , 
1 ,  0 ) )  e.  CC )
211207, 210fsumneg 12562 . . . . . . . . 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 ) ) )
212200a1i 11 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  ( D  \  {  .1.  } ) )  ->  if ( f  e.  W ,  1 ,  0 )  e.  CC )
213207, 48, 212fsummulc2 12559 . . . . . . . . . . 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 ) ) )
214 rpvmasum2.w . . . . . . . . . . . . . . . . 17  |-  W  =  { y  e.  ( D  \  {  .1.  } )  |  sum_ m  e.  NN  ( ( y `
 ( L `  m ) )  /  m )  =  0 }
215 ssrab2 3420 . . . . . . . . . . . . . . . . 17  |-  { y  e.  ( D  \  {  .1.  } )  | 
sum_ m  e.  NN  ( ( y `  ( L `  m ) )  /  m )  =  0 }  C_  ( D  \  {  .1.  } )
216214, 215eqsstri 3370 . . . . . . . . . . . . . . . 16  |-  W  C_  ( D  \  {  .1.  } )
217 difss 3466 . . . . . . . . . . . . . . . 16  |-  ( D 
\  {  .1.  }
)  C_  D
218216, 217sstri 3349 . . . . . . . . . . . . . . 15  |-  W  C_  D
219 ssfi 7321 . . . . . . . . . . . . . . 15  |-  ( ( D  e.  Fin  /\  W  C_  D )  ->  W  e.  Fin )
2206, 218, 219sylancl 644 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR+ )  ->  W  e.  Fin )
221 fsumconst 12565 . . . . . . . . . . . . . 14  |-  ( ( W  e.  Fin  /\  1  e.  CC )  -> 
sum_ f  e.  W 
1  =  ( (
# `  W )  x.  1 ) )
222220, 50, 221sylancl 644 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ f  e.  W  1  =  ( ( # `  W
)  x.  1 ) )
223216a1i 11 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR+ )  ->  W  C_  ( D  \  {  .1.  }
) )
22450a1i 11 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  RR+ )  ->  1  e.  CC )
225224ralrimivw 2782 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR+ )  ->  A. f  e.  W  1  e.  CC )
226207olcd 383 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( D  \  {  .1.  }
)  C_  ( ZZ>= ` 
1 )  \/  ( D  \  {  .1.  }
)  e.  Fin )
)
227 sumss2 12512 . . . . . . . . . . . . . 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 ) )
228223, 225, 226, 227syl21anc 1183 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ f  e.  W  1  =  sum_ f  e.  ( D  \  {  .1.  } ) if ( f  e.  W ,  1 ,  0 ) )
229 hashcl 11631 . . . . . . . . . . . . . . . 16  |-  ( W  e.  Fin  ->  ( # `
 W )  e. 
NN0 )
230220, 229syl 16 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( # `  W
)  e.  NN0 )
231230nn0cnd 10268 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( # `  W
)  e.  CC )
232231mulid1d 9097 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( # `
 W )  x.  1 )  =  (
# `  W )
)
233222, 228, 2323eqtr3d 2475 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ f  e.  ( D  \  {  .1.  } ) if ( f  e.  W , 
1 ,  0 )  =  ( # `  W
) )
234233oveq2d 6089 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( log `  x )  x. 
sum_ f  e.  ( D  \  {  .1.  } ) if ( f  e.  W ,  1 ,  0 ) )  =  ( ( log `  x )  x.  ( # `
 W ) ) )
235213, 234eqtr3d 2469 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ f  e.  ( D  \  {  .1.  } ) ( ( log `  x )  x.  if ( f  e.  W ,  1 ,  0 ) )  =  ( ( log `  x )  x.  ( # `
 W ) ) )
236235negeqd 9292 . . . . . . . . 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 ) ) )
237205, 211, 2363eqtrd 2471 . . . . . . . 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 ) ) )
238188, 237oveq12d 6091 . . . . . . 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 ) ) ) )
23948, 231mulcld 9100 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( log `  x )  x.  ( # `  W
) )  e.  CC )
240184, 239negsubd 9409 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( (
( log `  x
)  x.  1 )  +  -u ( ( log `  x )  x.  ( # `
 W ) ) )  =  ( ( ( log `  x
)  x.  1 )  -  ( ( log `  x )  x.  ( # `
 W ) ) ) )
241238, 240eqtrd 2467 . . . . . 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
) ) ) )
242 disjdif 3692 . . . . . . . 8  |-  ( {  .1.  }  i^i  ( D  \  {  .1.  }
) )  =  (/)
243242a1i 11 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( {  .1.  }  i^i  ( D 
\  {  .1.  }
) )  =  (/) )
244 undif2 3696 . . . . . . . 8  |-  ( {  .1.  }  u.  ( D  \  {  .1.  }
) )  =  ( {  .1.  }  u.  D )
245182snssd 3935 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR+ )  ->  {  .1.  } 
C_  D )
246 ssequn1 3509 . . . . . . . . 9  |-  ( {  .1.  }  C_  D  <->  ( {  .1.  }  u.  D )  =  D )
247245, 246sylib 189 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( {  .1.  }  u.  D )  =  D )
248244, 247syl5req 2480 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR+ )  ->  D  =  ( {  .1.  }  u.  ( D  \  {  .1.  } ) ) )
249243, 248, 6, 56fsumsplit 12525 . . . . . 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 ) ) ) ) )
25048, 224, 231subdid 9481 . . . . . 6  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( log `  x )  x.  ( 1  -  ( # `
 W ) ) )  =  ( ( ( log `  x
)  x.  1 )  -  ( ( log `  x )  x.  ( # `
 W ) ) ) )
251241, 249, 2503eqtr4rd 2478 . . . . 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 ) ) ) )
252177, 251oveq12d 6091 . . . 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 ) ) ) ) )
25357, 122, 2523eqtr4d 2477 . . 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
) ) ) ) )
254253mpteq2dva 4287 . 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
) ) ) ) ) )
255 rpssre 10614 . . . 4  |-  RR+  C_  RR
256255a1i 11 . . 3  |-  ( ph  -> 
RR+  C_  RR )
2571, 5syl 16 . . 3  |-  ( ph  ->  D  e.  Fin )
25817adantlr 696 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  (
f `  A )  e.  CC )
259258cjcld 11993 . . . . 5  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  (
* `  ( f `  A ) )  e.  CC )
26059, 56subcld 9403 . . . . 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 )
261259, 260mulcld 9100 . . . 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 )
262261anasss 629 . . 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 )
26318adantr 452 . . . 4  |-  ( ( ( ph  /\  f  e.  D )  /\  x  e.  RR+ )  ->  (
* `  ( f `  A ) )  e.  CC )
264260an32s 780 . . . 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 )
265 o1const 12405 . . . . 5  |-  ( (
RR+  C_  RR  /\  (
* `  ( f `  A ) )  e.  CC )  ->  (
x  e.  RR+  |->  ( * `
 ( f `  A ) ) )  e.  O ( 1 ) )
266255, 18, 265sylancr 645 . . . 4  |-  ( (
ph  /\  f  e.  D )  ->  (
x  e.  RR+  |->  ( * `
 ( f `  A ) ) )  e.  O ( 1 ) )
267 fveq1 5719 . . . . . . . . . . . 12  |-  ( f  =  .1.  ->  (
f `  ( L `  n ) )  =  (  .1.  `  ( L `  n )
) )
268267oveq1d 6088 . . . . . . . . . . 11  |-  ( f  =  .1.  ->  (
( f `  ( L `  n )
)  x.  ( (Λ `  n )  /  n
) )  =  ( (  .1.  `  ( L `  n )
)  x.  ( (Λ `  n )  /  n
) ) )
269268sumeq2sdv 12490 . . . . . . . . . 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 ) ) )
270269, 186oveq12d 6091 . . . . . . . . 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 ) ) )
271270adantl 453 . . . . . . . 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 ) ) )
27246recnd 9106 . . . . . . . . . 10  |-  ( x  e.  RR+  ->  ( log `  x )  e.  CC )
273272mulid1d 9097 . . . . . . . . 9  |-  ( x  e.  RR+  ->  ( ( log `  x )  x.  1 )  =  ( log `  x
) )
274273oveq2d 6089 . . . . . . . 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 ) ) )
275271, 274sylan9eq 2487 . . . . . . 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 ) ) )
276275mpteq2dva 4287 . . . . . 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 ) ) ) )
2778, 24, 1, 3, 4, 68rpvmasumlem 21173 . . . . . . 7  |-  ( ph  ->  ( x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (  .1.  `  ( L `  n ) )  x.  ( (Λ `  n )  /  n
) )  -  ( log `  x ) ) )  e.  O ( 1 ) )
278277ad2antrr 707 . . . . . 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 ) )
279276, 278eqeltrd 2509 . . . . 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 ) )
280190oveq2d 6089 . . . . . . . . . 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 ) ) )
281280oveq2d 6089 . . . . . . . . 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 ) ) ) )
28248adantlr 696 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  f  e.  D )  /\  x  e.  RR+ )  ->  ( log `  x )  e.  CC )
283 mulcom 9068 . . . . . . . . . . . . . . 15  |-  ( ( ( log `  x
)  e.  CC  /\  -u 1  e.  CC )  ->  ( ( log `  x )  x.  -u 1
)  =  ( -u
1  x.  ( log `  x ) ) )
284282, 51, 283sylancl 644 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  f  e.  D )  /\  x  e.  RR+ )  ->  (
( log `  x
)  x.  -u 1
)  =  ( -u
1  x.  ( log `  x ) ) )
285282mulm1d 9477 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  f  e.  D )  /\  x  e.  RR+ )  ->  ( -u 1  x.  ( log `  x ) )  = 
-u ( log `  x
) )
286284, 285eqtrd 2467 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  f  e.  D )  /\  x  e.  RR+ )  ->  (
( log `  x
)  x.  -u 1
)  =  -u ( log `  x ) )
287282mul01d 9257 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  f  e.  D )  /\  x  e.  RR+ )  ->  (
( log `  x
)  x.  0 )  =  0 )
288286, 287ifeq12d 3747 . . . . . . . . . . . 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 ) )
289 oveq2 6081 . . . . . . . . . . . . 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 ) )
290 oveq2 6081 . . . . . . . . . . . . 13  |-  ( if ( f  e.  W ,  -u 1 ,  0 )  =  0  -> 
( ( log `  x
)  x.  if ( f  e.  W ,  -u 1 ,  0 ) )  =  ( ( log `  x )  x.  0 ) )
291289, 290ifsb 3740 . . . . . . . . . . . 12  |-  ( ( log `  x )  x.  if ( f  e.  W ,  -u
1 ,  0 ) )  =  if ( f  e.  W , 
( ( log `  x
)  x.  -u 1
) ,  ( ( log `  x )  x.  0 ) )
292 negeq 9290 . . . . . . . . . . . . 13  |-  ( if ( f  e.  W ,  ( log `  x
) ,  0 )  =  ( log `  x
)  ->  -u if ( f  e.  W , 
( log `  x
) ,  0 )  =  -u ( log `  x
) )
293 negeq 9290 . . . . . . . . . . . . . 14  |-  ( if ( f  e.  W ,  ( log `  x
) ,  0 )  =  0  ->  -u if ( f  e.  W ,  ( log `  x
) ,  0 )  =  -u 0 )
294293, 194syl6eq 2483 . . . . . . . . . . . . 13  |-  ( if ( f  e.  W ,  ( log `  x
) ,  0 )  =  0  ->  -u if ( f  e.  W ,  ( log `  x
) ,  0 )  =  0 )
295292, 294ifsb 3740 . . . . . . . . . . . 12  |-  -u if ( f  e.  W ,  ( log `  x
) ,  0 )  =  if ( f  e.  W ,  -u ( log `  x ) ,  0 )
296288, 291, 2953eqtr4g 2492 . . . . . . . . . . 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 ) )
297296oveq2d 6089 . . . . . . . . . 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 ) ) )
29859an32s 780 . . . . . . . . . . 11  |-  ( ( ( ph  /\  f  e.  D )  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( f `  ( L `  n ) )  x.  ( (Λ `  n )  /  n
) )  e.  CC )
299 ifcl 3767 . . . . . . . . . . . 12  |-  ( ( ( log `  x
)  e.  CC  /\  0  e.  CC )  ->  if ( f  e.  W ,  ( log `  x ) ,  0 )  e.  CC )
300282, 52, 299sylancl 644 . . . . . . . . . . 11  |-  ( ( ( ph  /\  f  e.  D )  /\  x  e.  RR+ )  ->  if ( f  e.  W ,  ( log `  x
) ,  0 )  e.  CC )
301298, 300subnegd 9410 . . . . . . . . . 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 ) ) )
302297, 301eqtrd 2467 . . . . . . . . 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 ) ) )
303281, 302sylan9eqr 2489 . . . . . . . 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 ) ) )
304303an32s 780 . . . . . . 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 ) ) )
305304mpteq2dva 4287 . . . . . 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 ) ) ) )
3061ad2antrr 707 . . . . . . . 8  |-  ( ( ( ph  /\  f  e.  D )  /\  f  =/=  .1.  )  ->  N  e.  NN )
307 simplr 732 . . . . . . . 8  |-  ( ( ( ph  /\  f  e.  D )  /\  f  =/=  .1.  )  ->  f  e.  D )
308 simpr 448 . . . . . . . 8  |-  ( ( ( ph  /\  f  e.  D )  /\  f  =/=  .1.  )  ->  f  =/=  .1.  )
309 eqid 2435 . . . . . . . 8  |-  ( a  e.  NN  |->  ( ( f `  ( L `
 a ) )  /  a ) )  =  ( a  e.  NN  |->  ( ( f `
 ( L `  a ) )  / 
a ) )
3108, 24, 306, 3, 4, 68, 307, 308, 309dchrmusumlema 21179 . . . . . . 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 ) ) )
3111adantr 452 . . . . . . . . . . . . 13  |-  ( (
ph  /\  f  e.  D )  ->  N  e.  NN )
312311ad2antrr 707 . . . . . . . . . . . 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 )
313307adantr 452 . . . . . . . . . . . 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 )
314 simplr 732 . . . . . . . . . . . 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.  )
315 simprl 733 . . . . . . . . . . . 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 ) )
316 simprrl 741 . . . . . . . . . . . 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 )
317 simprrr 742 . . . . . . . . . . . 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 ) )
3188, 24, 312, 3, 4, 68, 313, 314, 309, 315, 316, 317, 214dchrvmaeq0 21190 . . . . . . . . . . 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 ) )
319 ifbi 3748 . . . . . . . . . . . . 13  |-  ( ( f  e.  W  <->  t  = 
0 )  ->  if ( f  e.  W ,  ( log `  x
) ,  0 )  =  if ( t  =  0 ,  ( log `  x ) ,  0 ) )
320319oveq2d 6089 . . . . . . . . . . . 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 ) ) )
321320mpteq2dv 4288 . . . . . . . . . . 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 ) ) ) )
322318, 321syl 16 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  f  e.  D )  /\  f  =/=  .1.  )  /\  ( c  e.  ( 0 [,)  +oo )  /\  (  seq  1
(  +  ,  ( a  e.  NN  |->  ( ( f `  ( L `  a )
)  /  a ) ) )  ~~>  t  /\  A. y