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

Theorem rpvmasum2 21211
Description: A partial result along the lines of rpvmasum 21225. 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 453 . . . . . 6  |-  ( (
ph  /\  x  e.  RR+ )  ->  N  e.  NN )
3 rpvmasum2.g . . . . . . 7  |-  G  =  (DChr `  N )
4 rpvmasum2.d . . . . . . 7  |-  D  =  ( Base `  G
)
53, 4dchrfi 21044 . . . . . 6  |-  ( N  e.  NN  ->  D  e.  Fin )
62, 5syl 16 . . . . 5  |-  ( (
ph  /\  x  e.  RR+ )  ->  D  e.  Fin )
7 fzfid 11317 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  (
1 ... ( |_ `  x ) )  e. 
Fin )
8 rpvmasum.z . . . . . . . . . . . . 13  |-  Z  =  (ℤ/n `  N )
9 eqid 2438 . . . . . . . . . . . . 13  |-  ( Base `  Z )  =  (
Base `  Z )
10 simpr 449 . . . . . . . . . . . . 13  |-  ( (
ph  /\  f  e.  D )  ->  f  e.  D )
113, 8, 4, 9, 10dchrf 21031 . . . . . . . . . . . 12  |-  ( (
ph  /\  f  e.  D )  ->  f : ( Base `  Z
) --> CC )
12 rpvmasum2.u . . . . . . . . . . . . . . 15  |-  U  =  (Unit `  Z )
139, 12unitss 15770 . . . . . . . . . . . . . 14  |-  U  C_  ( Base `  Z )
14 rpvmasum2.b . . . . . . . . . . . . . 14  |-  ( ph  ->  A  e.  U )
1513, 14sseldi 3348 . . . . . . . . . . . . 13  |-  ( ph  ->  A  e.  ( Base `  Z ) )
1615adantr 453 . . . . . . . . . . . 12  |-  ( (
ph  /\  f  e.  D )  ->  A  e.  ( Base `  Z
) )
1711, 16ffvelrnd 5874 . . . . . . . . . . 11  |-  ( (
ph  /\  f  e.  D )  ->  (
f `  A )  e.  CC )
1817cjcld 12006 . . . . . . . . . 10  |-  ( (
ph  /\  f  e.  D )  ->  (
* `  ( f `  A ) )  e.  CC )
1918adantlr 697 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  (
* `  ( f `  A ) )  e.  CC )
2019adantrl 698 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
n  e.  ( 1 ... ( |_ `  x ) )  /\  f  e.  D )
)  ->  ( * `  ( f `  A
) )  e.  CC )
2111adantlr 697 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  f : ( Base `  Z
) --> CC )
2221adantlr 697 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  f  e.  D
)  ->  f :
( Base `  Z ) --> CC )
231nnnn0d 10279 . . . . . . . . . . . . . . 15  |-  ( ph  ->  N  e.  NN0 )
24 rpvmasum.l . . . . . . . . . . . . . . . 16  |-  L  =  ( ZRHom `  Z
)
258, 9, 24znzrhfo 16833 . . . . . . . . . . . . . . 15  |-  ( N  e.  NN0  ->  L : ZZ -onto-> ( Base `  Z
) )
26 fof 5656 . . . . . . . . . . . . . . 15  |-  ( L : ZZ -onto-> ( Base `  Z )  ->  L : ZZ --> ( Base `  Z
) )
2723, 25, 263syl 19 . . . . . . . . . . . . . 14  |-  ( ph  ->  L : ZZ --> ( Base `  Z ) )
2827adantr 453 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR+ )  ->  L : ZZ
--> ( Base `  Z
) )
29 elfzelz 11064 . . . . . . . . . . . . 13  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  ZZ )
30 ffvelrn 5871 . . . . . . . . . . . . 13  |-  ( ( L : ZZ --> ( Base `  Z )  /\  n  e.  ZZ )  ->  ( L `  n )  e.  ( Base `  Z
) )
3128, 29, 30syl2an 465 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( L `  n )  e.  (
Base `  Z )
)
3231adantr 453 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  f  e.  D
)  ->  ( L `  n )  e.  (
Base `  Z )
)
3322, 32ffvelrnd 5874 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  f  e.  D
)  ->  ( f `  ( L `  n
) )  e.  CC )
3433anasss 630 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
n  e.  ( 1 ... ( |_ `  x ) )  /\  f  e.  D )
)  ->  ( f `  ( L `  n
) )  e.  CC )
35 elfznn 11085 . . . . . . . . . . . . . 14  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  NN )
3635adantl 454 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  NN )
37 vmacl 20906 . . . . . . . . . . . . 13  |-  ( n  e.  NN  ->  (Λ `  n )  e.  RR )
3836, 37syl 16 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (Λ `  n
)  e.  RR )
3938, 36nndivred 10053 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  /  n
)  e.  RR )
4039recnd 9119 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  /  n
)  e.  CC )
4140adantrr 699 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
n  e.  ( 1 ... ( |_ `  x ) )  /\  f  e.  D )
)  ->  ( (Λ `  n )  /  n
)  e.  CC )
4234, 41mulcld 9113 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
n  e.  ( 1 ... ( |_ `  x ) )  /\  f  e.  D )
)  ->  ( (
f `  ( L `  n ) )  x.  ( (Λ `  n
)  /  n ) )  e.  CC )
4320, 42mulcld 9113 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
n  e.  ( 1 ... ( |_ `  x ) )  /\  f  e.  D )
)  ->  ( (
* `  ( f `  A ) )  x.  ( ( f `  ( L `  n ) )  x.  ( (Λ `  n )  /  n
) ) )  e.  CC )
4443anass1rs 784 . . . . . 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 12532 . . . . 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 20478 . . . . . . . . 9  |-  ( x  e.  RR+  ->  ( log `  x )  e.  RR )
4746adantl 454 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( log `  x )  e.  RR )
4847recnd 9119 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( log `  x )  e.  CC )
4948adantr 453 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  ( log `  x )  e.  CC )
50 ax-1cn 9053 . . . . . . 7  |-  1  e.  CC
51 neg1cn 10072 . . . . . . . 8  |-  -u 1  e.  CC
52 0cn 9089 . . . . . . . 8  |-  0  e.  CC
5351, 52keepel 3798 . . . . . . 7  |-  if ( f  e.  W ,  -u 1 ,  0 )  e.  CC
5450, 53keepel 3798 . . . . . 6  |-  if ( f  =  .1.  , 
1 ,  if ( f  e.  W ,  -u 1 ,  0 ) )  e.  CC
55 mulcl 9079 . . . . . 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 645 . . . . 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 12576 . . . 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 784 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  n  e.  (
1 ... ( |_ `  x ) ) )  ->  ( ( f `
 ( L `  n ) )  x.  ( (Λ `  n
)  /  n ) )  e.  CC )
597, 58fsumcl 12532 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( f `  ( L `  n ) )  x.  ( (Λ `  n )  /  n
) )  e.  CC )
6019, 59, 56subdid 9494 . . . . . 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 12572 . . . . . . 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 9280 . . . . . . . 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 6092 . . . . . . . . . . 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 6092 . . . . . . . . . . 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 3750 . . . . . . . . . 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 5730 . . . . . . . . . . . . . . . . 17  |-  ( f  =  .1.  ->  (
f `  A )  =  (  .1.  `  A
) )
68 rpvmasum2.1 . . . . . . . . . . . . . . . . . 18  |-  .1.  =  ( 0g `  G )
691ad2antrr 708 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  N  e.  NN )
7014ad2antrr 708 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  A  e.  U )
713, 8, 68, 12, 69, 70dchr1 21046 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  (  .1.  `  A )  =  1 )
7267, 71sylan9eqr 2492 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  f  =  .1.  )  ->  ( f `  A )  =  1 )
7372fveq2d 5735 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  f  =  .1.  )  ->  ( * `  ( f `  A
) )  =  ( * `  1 ) )
74 1re 9095 . . . . . . . . . . . . . . . 16  |-  1  e.  RR
75 cjre 11949 . . . . . . . . . . . . . . . 16  |-  ( 1  e.  RR  ->  (
* `  1 )  =  1 )
7674, 75ax-mp 5 . . . . . . . . . . . . . . 15  |-  ( * `
 1 )  =  1
7773, 76syl6eq 2486 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  f  =  .1.  )  ->  ( * `  ( f `  A
) )  =  1 )
7877oveq1d 6099 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  f  =  .1.  )  ->  ( ( * `
 ( f `  A ) )  x.  1 )  =  ( 1  x.  1 ) )
79 1t1e1 10131 . . . . . . . . . . . . 13  |-  ( 1  x.  1 )  =  1
8078, 79syl6eq 2486 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  f  =  .1.  )  ->  ( ( * `
 ( f `  A ) )  x.  1 )  =  1 )
8180ifeq1da 3766 . . . . . . . . . . 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 2603 . . . . . . . . . . . . 13  |-  ( f  =/=  .1.  <->  -.  f  =  .1.  )
83 oveq2 6092 . . . . . . . . . . . . . . 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 6092 . . . . . . . . . . . . . . 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 3750 . . . . . . . . . . . . . 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 736 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  f  =/=  .1.  )  ->  ph )
87 rpvmasum2.z1 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  f  e.  W )  ->  A  =  ( 1r `  Z ) )
8887fveq2d 5735 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  f  e.  W )  ->  (
f `  A )  =  ( f `  ( 1r `  Z ) ) )
8986, 88sylan 459 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D
)  /\  f  =/=  .1.  )  /\  f  e.  W )  ->  (
f `  A )  =  ( f `  ( 1r `  Z ) ) )
903, 8, 4dchrmhm 21030 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  D  C_  ( (mulGrp `  Z ) MndHom  (mulGrp ` fld ) )
91 simpr 449 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  f  e.  D )
9290, 91sseldi 3348 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  f  e.  ( (mulGrp `  Z
) MndHom  (mulGrp ` fld ) ) )
93 eqid 2438 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  (mulGrp `  Z )  =  (mulGrp `  Z )
94 eqid 2438 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 1r
`  Z )  =  ( 1r `  Z
)
9593, 94rngidval 15671 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 1r
`  Z )  =  ( 0g `  (mulGrp `  Z ) )
96 eqid 2438 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  (mulGrp ` fld )  =  (mulGrp ` fld )
97 cnfld1 16731 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  1  =  ( 1r ` fld )
9896, 97rngidval 15671 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  1  =  ( 0g `  (mulGrp ` fld ) )
9995, 98mhm0 14751 . . . . . . . . . . . . . . . . . . . . . . 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 708 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D
)  /\  f  =/=  .1.  )  /\  f  e.  W )  ->  (
f `  ( 1r `  Z ) )  =  1 )
10289, 101eqtrd 2470 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D
)  /\  f  =/=  .1.  )  /\  f  e.  W )  ->  (
f `  A )  =  1 )
103102fveq2d 5735 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D
)  /\  f  =/=  .1.  )  /\  f  e.  W )  ->  (
* `  ( f `  A ) )  =  ( * `  1
) )
104103, 76syl6eq 2486 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D
)  /\  f  =/=  .1.  )  /\  f  e.  W )  ->  (
* `  ( f `  A ) )  =  1 )
105104oveq1d 6099 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D
)  /\  f  =/=  .1.  )  /\  f  e.  W )  ->  (
( * `  (
f `  A )
)  x.  -u 1
)  =  ( 1  x.  -u 1 ) )
10651mulid2i 9098 . . . . . . . . . . . . . . . . 17  |-  ( 1  x.  -u 1 )  = 
-u 1
107105, 106syl6eq 2486 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D
)  /\  f  =/=  .1.  )  /\  f  e.  W )  ->  (
( * `  (
f `  A )
)  x.  -u 1
)  =  -u 1
)
108107ifeq1da 3766 . . . . . . . . . . . . . . 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 453 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  f  =/=  .1.  )  ->  ( * `  ( f `  A
) )  e.  CC )
110109mul01d 9270 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  f  =/=  .1.  )  ->  ( ( * `
 ( f `  A ) )  x.  0 )  =  0 )
111110ifeq2d 3756 . . . . . . . . . . . . . . 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 2470 . . . . . . . . . . . . . 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 2482 . . . . . . . . . . . . 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 464 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  /\  -.  f  =  .1.  )  ->  ( (
* `  ( f `  A ) )  x.  if ( f  e.  W ,  -u 1 ,  0 ) )  =  if ( f  e.  W ,  -u
1 ,  0 ) )
115114ifeq2da 3767 . . . . . . . . . . 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 2470 . . . . . . . . . 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 2482 . . . . . . . . 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 6100 . . . . . . . 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 2470 . . . . . . 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 6102 . . . . . 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 2470 . . . . 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 12502 . . . 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 11317 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( 1 ... ( |_ `  x ) )  e. 
Fin )
124 inss1 3563 . . . . . . . . 9  |-  ( ( 1 ... ( |_
`  x ) )  i^i  T )  C_  ( 1 ... ( |_ `  x ) )
125 ssfi 7332 . . . . . . . . 9  |-  ( ( ( 1 ... ( |_ `  x ) )  e.  Fin  /\  (
( 1 ... ( |_ `  x ) )  i^i  T )  C_  ( 1 ... ( |_ `  x ) ) )  ->  ( (
1 ... ( |_ `  x ) )  i^i 
T )  e.  Fin )
126123, 124, 125sylancl 645 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( (
1 ... ( |_ `  x ) )  i^i 
T )  e.  Fin )
1272phicld 13166 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( phi `  N )  e.  NN )
128127nncnd 10021 . . . . . . . 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 3350 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( ( 1 ... ( |_ `  x
) )  i^i  T
) )  ->  n  e.  ( 1 ... ( |_ `  x ) ) )
131130, 40syldan 458 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( ( 1 ... ( |_ `  x
) )  i^i  T
) )  ->  (
(Λ `  n )  /  n )  e.  CC )
132126, 128, 131fsummulc2 12572 . . . . . . 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 453 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( phi `  N )  e.  CC )
134133, 40mulcld 9113 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( phi `  N )  x.  ( (Λ `  n
)  /  n ) )  e.  CC )
135130, 134syldan 458 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( ( 1 ... ( |_ `  x
) )  i^i  T
) )  ->  (
( phi `  N
)  x.  ( (Λ `  n )  /  n
) )  e.  CC )
136135ralrimiva 2791 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  A. n  e.  ( ( 1 ... ( |_ `  x
) )  i^i  T
) ( ( phi `  N )  x.  (
(Λ `  n )  /  n ) )  e.  CC )
137123olcd 384 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( (
1 ... ( |_ `  x ) )  C_  ( ZZ>= `  1 )  \/  ( 1 ... ( |_ `  x ) )  e.  Fin ) )
138 sumss2 12525 . . . . . . . 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 1184 . . . . . . 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 3532 . . . . . . . . . . . . 13  |-  ( n  e.  ( ( 1 ... ( |_ `  x ) )  i^i 
T )  <->  ( n  e.  ( 1 ... ( |_ `  x ) )  /\  n  e.  T
) )
141140baib 873 . . . . . . . . . . . 12  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  (
n  e.  ( ( 1 ... ( |_
`  x ) )  i^i  T )  <->  n  e.  T ) )
142141adantl 454 . . . . . . . . . . 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 2502 . . . . . . . . . . . 12  |-  ( n  e.  T  <->  n  e.  ( `' L " { A } ) )
145 ffn 5594 . . . . . . . . . . . . . 14  |-  ( L : ZZ --> ( Base `  Z )  ->  L  Fn  ZZ )
14628, 145syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR+ )  ->  L  Fn  ZZ )
147 fniniseg 5854 . . . . . . . . . . . . . 14  |-  ( L  Fn  ZZ  ->  (
n  e.  ( `' L " { A } )  <->  ( n  e.  ZZ  /\  ( L `
 n )  =  A ) ) )
148147baibd 877 . . . . . . . . . . . . 13  |-  ( ( L  Fn  ZZ  /\  n  e.  ZZ )  ->  ( n  e.  ( `' L " { A } )  <->  ( L `  n )  =  A ) )
149146, 29, 148syl2an 465 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  e.  ( `' L " { A } )  <->  ( L `  n )  =  A ) )
150144, 149syl5bb 250 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( n  e.  T  <->  ( L `  n )  =  A ) )
151142, 150bitr2d 247 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( L `  n )  =  A  <->  n  e.  (
( 1 ... ( |_ `  x ) )  i^i  T ) ) )
15240mul02d 9269 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 0  x.  ( (Λ `  n
)  /  n ) )  =  0 )
153151, 152ifbieq2d 3761 . . . . . . . . 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 6091 . . . . . . . . . . 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 6091 . . . . . . . . . . 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 3750 . . . . . . . . . 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 708 . . . . . . . . . . . . 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 697 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  f  e.  D
)  ->  ( * `  ( f `  A
) )  e.  CC )
16033, 159mulcld 9113 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  f  e.  D
)  ->  ( (
f `  ( L `  n ) )  x.  ( * `  (
f `  A )
) )  e.  CC )
161158, 40, 160fsummulc1 12573 . . . . . . . . . . 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 708 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  A  e.  U )
1633, 4, 8, 9, 12, 157, 31, 162sum2dchr 21063 . . . . . . . . . . . 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 6099 . . . . . . . . . . 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 453 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR+ )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  f  e.  D
)  ->  ( (Λ `  n )  /  n
)  e.  CC )
166 mulass 9083 . . . . . . . . . . . . . 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 9237 . . . . . . . . . . . . . 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 2470 . . . . . . . . . . . . 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 1185 . . . . . . . . . . . 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 12502 . . . . . . . . . . 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 2478 . . . . . . . . . 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 2484 . . . . . . . . 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 2472 . . . . . . . 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 12502 . . . . . . 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 2474 . . . . . 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 12564 . . . . . 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 2470 . . . . 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 21043 . . . . . . . . . 10  |-  ( N  e.  NN  ->  G  e.  Abel )
179 ablgrp 15422 . . . . . . . . . 10  |-  ( G  e.  Abel  ->  G  e. 
Grp )
1804, 68grpidcl 14838 . . . . . . . . . 10  |-  ( G  e.  Grp  ->  .1.  e.  D )
1812, 178, 179, 1804syl 20 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR+ )  ->  .1.  e.  D )
18248mulid1d 9110 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( log `  x )  x.  1 )  =  ( log `  x ) )
183182, 48eqeltrd 2512 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( log `  x )  x.  1 )  e.  CC )
184 iftrue 3747 . . . . . . . . . . 11  |-  ( f  =  .1.  ->  if ( f  =  .1. 
,  1 ,  if ( f  e.  W ,  -u 1 ,  0 ) )  =  1 )
185184oveq2d 6100 . . . . . . . . . 10  |-  ( f  =  .1.  ->  (
( log `  x
)  x.  if ( f  =  .1.  , 
1 ,  if ( f  e.  W ,  -u 1 ,  0 ) ) )  =  ( ( log `  x
)  x.  1 ) )
186185sumsn 12539 . . . . . . . . 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 ) )
187181, 183, 186syl2anc 644 . . . . . . . 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 ) )
188 eldifsn 3929 . . . . . . . . . . 11  |-  ( f  e.  ( D  \  {  .1.  } )  <->  ( f  e.  D  /\  f  =/=  .1.  ) )
189 ifnefalse 3749 . . . . . . . . . . . . . . 15  |-  ( f  =/=  .1.  ->  if ( f  =  .1. 
,  1 ,  if ( f  e.  W ,  -u 1 ,  0 ) )  =  if ( f  e.  W ,  -u 1 ,  0 ) )
190189ad2antll 711 . . . . . . . . . . . . . 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 ) )
191 negeq 9303 . . . . . . . . . . . . . . 15  |-  ( if ( f  e.  W ,  1 ,  0 )  =  1  ->  -u if ( f  e.  W ,  1 ,  0 )  =  -u
1 )
192 negeq 9303 . . . . . . . . . . . . . . . 16  |-  ( if ( f  e.  W ,  1 ,  0 )  =  0  ->  -u if ( f  e.  W ,  1 ,  0 )  =  -u
0 )
193 neg0 9352 . . . . . . . . . . . . . . . 16  |-  -u 0  =  0
194192, 193syl6eq 2486 . . . . . . . . . . . . . . 15  |-  ( if ( f  e.  W ,  1 ,  0 )  =  0  ->  -u if ( f  e.  W ,  1 ,  0 )  =  0 )
195191, 194ifsb 3750 . . . . . . . . . . . . . 14  |-  -u if ( f  e.  W ,  1 ,  0 )  =  if ( f  e.  W ,  -u 1 ,  0 )
196190, 195syl6eqr 2488 . . . . . . . . . . . . 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 ) )
197196oveq2d 6100 . . . . . . . . . . . 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 ) ) )
19848adantr 453 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  (
f  e.  D  /\  f  =/=  .1.  ) )  ->  ( log `  x
)  e.  CC )
19950, 52keepel 3798 . . . . . . . . . . . . 13  |-  if ( f  e.  W , 
1 ,  0 )  e.  CC
200 mulneg2 9476 . . . . . . . . . . . . 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 ) ) )
201198, 199, 200sylancl 645 . . . . . . . . . . . 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 ) ) )
202197, 201eqtrd 2470 . . . . . . . . . . 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 ) ) )
203188, 202sylan2b 463 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  ( D  \  {  .1.  } ) )  -> 
( ( log `  x
)  x.  if ( f  =  .1.  , 
1 ,  if ( f  e.  W ,  -u 1 ,  0 ) ) )  =  -u ( ( log `  x
)  x.  if ( f  e.  W , 
1 ,  0 ) ) )
204203sumeq2dv 12502 . . . . . . . . 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 ) ) )
205 diffi 7342 . . . . . . . . . . 11  |-  ( D  e.  Fin  ->  ( D  \  {  .1.  }
)  e.  Fin )
2066, 205syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( D  \  {  .1.  } )  e.  Fin )
20748adantr 453 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  ( D  \  {  .1.  } ) )  -> 
( log `  x
)  e.  CC )
208 mulcl 9079 . . . . . . . . . . 11  |-  ( ( ( log `  x
)  e.  CC  /\  if ( f  e.  W ,  1 ,  0 )  e.  CC )  ->  ( ( log `  x )  x.  if ( f  e.  W ,  1 ,  0 ) )  e.  CC )
209207, 199, 208sylancl 645 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  ( D  \  {  .1.  } ) )  -> 
( ( log `  x
)  x.  if ( f  e.  W , 
1 ,  0 ) )  e.  CC )
210206, 209fsumneg 12575 . . . . . . . . 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 ) ) )
211199a1i 11 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  ( D  \  {  .1.  } ) )  ->  if ( f  e.  W ,  1 ,  0 )  e.  CC )
212206, 48, 211fsummulc2 12572 . . . . . . . . . . 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 ) ) )
213 rpvmasum2.w . . . . . . . . . . . . . . . . 17  |-  W  =  { y  e.  ( D  \  {  .1.  } )  |  sum_ m  e.  NN  ( ( y `
 ( L `  m ) )  /  m )  =  0 }
214 ssrab2 3430 . . . . . . . . . . . . . . . . 17  |-  { y  e.  ( D  \  {  .1.  } )  | 
sum_ m  e.  NN  ( ( y `  ( L `  m ) )  /  m )  =  0 }  C_  ( D  \  {  .1.  } )
215213, 214eqsstri 3380 . . . . . . . . . . . . . . . 16  |-  W  C_  ( D  \  {  .1.  } )
216 difss 3476 . . . . . . . . . . . . . . . 16  |-  ( D 
\  {  .1.  }
)  C_  D
217215, 216sstri 3359 . . . . . . . . . . . . . . 15  |-  W  C_  D
218 ssfi 7332 . . . . . . . . . . . . . . 15  |-  ( ( D  e.  Fin  /\  W  C_  D )  ->  W  e.  Fin )
2196, 217, 218sylancl 645 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR+ )  ->  W  e.  Fin )
220 fsumconst 12578 . . . . . . . . . . . . . 14  |-  ( ( W  e.  Fin  /\  1  e.  CC )  -> 
sum_ f  e.  W 
1  =  ( (
# `  W )  x.  1 ) )
221219, 50, 220sylancl 645 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ f  e.  W  1  =  ( ( # `  W
)  x.  1 ) )
222215a1i 11 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR+ )  ->  W  C_  ( D  \  {  .1.  }
) )
22350a1i 11 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  RR+ )  ->  1  e.  CC )
224223ralrimivw 2792 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR+ )  ->  A. f  e.  W  1  e.  CC )
225206olcd 384 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( D  \  {  .1.  }
)  C_  ( ZZ>= ` 
1 )  \/  ( D  \  {  .1.  }
)  e.  Fin )
)
226 sumss2 12525 . . . . . . . . . . . . . 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 ) )
227222, 224, 225, 226syl21anc 1184 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ f  e.  W  1  =  sum_ f  e.  ( D  \  {  .1.  } ) if ( f  e.  W ,  1 ,  0 ) )
228 hashcl 11644 . . . . . . . . . . . . . . . 16  |-  ( W  e.  Fin  ->  ( # `
 W )  e. 
NN0 )
229219, 228syl 16 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( # `  W
)  e.  NN0 )
230229nn0cnd 10281 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( # `  W
)  e.  CC )
231230mulid1d 9110 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( # `
 W )  x.  1 )  =  (
# `  W )
)
232221, 227, 2313eqtr3d 2478 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ f  e.  ( D  \  {  .1.  } ) if ( f  e.  W , 
1 ,  0 )  =  ( # `  W
) )
233232oveq2d 6100 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( log `  x )  x. 
sum_ f  e.  ( D  \  {  .1.  } ) if ( f  e.  W ,  1 ,  0 ) )  =  ( ( log `  x )  x.  ( # `
 W ) ) )
234212, 233eqtr3d 2472 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ f  e.  ( D  \  {  .1.  } ) ( ( log `  x )  x.  if ( f  e.  W ,  1 ,  0 ) )  =  ( ( log `  x )  x.  ( # `
 W ) ) )
235234negeqd 9305 . . . . . . . . 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 ) ) )
236204, 210, 2353eqtrd 2474 . . . . . . . 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 ) ) )
237187, 236oveq12d 6102 . . . . . . 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 ) ) ) )
23848, 230mulcld 9113 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( log `  x )  x.  ( # `  W
) )  e.  CC )
239183, 238negsubd 9422 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( (
( log `  x
)  x.  1 )  +  -u ( ( log `  x )  x.  ( # `
 W ) ) )  =  ( ( ( log `  x
)  x.  1 )  -  ( ( log `  x )  x.  ( # `
 W ) ) ) )
240237, 239eqtrd 2470 . . . . . 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
) ) ) )
241 disjdif 3702 . . . . . . . 8  |-  ( {  .1.  }  i^i  ( D  \  {  .1.  }
) )  =  (/)
242241a1i 11 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( {  .1.  }  i^i  ( D 
\  {  .1.  }
) )  =  (/) )
243 undif2 3706 . . . . . . . 8  |-  ( {  .1.  }  u.  ( D  \  {  .1.  }
) )  =  ( {  .1.  }  u.  D )
244181snssd 3945 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR+ )  ->  {  .1.  } 
C_  D )
245 ssequn1 3519 . . . . . . . . 9  |-  ( {  .1.  }  C_  D  <->  ( {  .1.  }  u.  D )  =  D )
246244, 245sylib 190 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( {  .1.  }  u.  D )  =  D )
247243, 246syl5req 2483 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR+ )  ->  D  =  ( {  .1.  }  u.  ( D  \  {  .1.  } ) ) )
248242, 247, 6, 56fsumsplit 12538 . . . . . 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 ) ) ) ) )
24948, 223, 230subdid 9494 . . . . . 6  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( log `  x )  x.  ( 1  -  ( # `
 W ) ) )  =  ( ( ( log `  x
)  x.  1 )  -  ( ( log `  x )  x.  ( # `
 W ) ) ) )
250240, 248, 2493eqtr4rd 2481 . . . . 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 ) ) ) )
251177, 250oveq12d 6102 . . . 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 ) ) ) ) )
25257, 122, 2513eqtr4d 2480 . . 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
) ) ) ) )
253252mpteq2dva 4298 . 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
) ) ) ) ) )
254 rpssre 10627 . . . 4  |-  RR+  C_  RR
255254a1i 11 . . 3  |-  ( ph  -> 
RR+  C_  RR )
2561, 5syl 16 . . 3  |-  ( ph  ->  D  e.  Fin )
25717adantlr 697 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  (
f `  A )  e.  CC )
258257cjcld 12006 . . . . 5  |-  ( ( ( ph  /\  x  e.  RR+ )  /\  f  e.  D )  ->  (
* `  ( f `  A ) )  e.  CC )
25959, 56subcld 9416 . . . . 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 )
260258, 259mulcld 9113 . . . 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 )
261260anasss 630 . . 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 )
26218adantr 453 . . . 4  |-  ( ( ( ph  /\  f  e.  D )  /\  x  e.  RR+ )  ->  (
* `  ( f `  A ) )  e.  CC )
263259an32s 781 . . . 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 )
264 o1const 12418 . . . . 5  |-  ( (
RR+  C_  RR  /\  (
* `  ( f `  A ) )  e.  CC )  ->  (
x  e.  RR+  |->  ( * `
 ( f `  A ) ) )  e.  O ( 1 ) )
265254, 18, 264sylancr 646 . . . 4  |-  ( (
ph  /\  f  e.  D )  ->  (
x  e.  RR+  |->  ( * `
 ( f `  A ) ) )  e.  O ( 1 ) )
266 fveq1 5730 . . . . . . . . . . . 12  |-  ( f  =  .1.  ->  (
f `  ( L `  n ) )  =  (  .1.  `  ( L `  n )
) )
267266oveq1d 6099 . . . . . . . . . . 11  |-  ( f  =  .1.  ->  (
( f `  ( L `  n )
)  x.  ( (Λ `  n )  /  n
) )  =  ( (  .1.  `  ( L `  n )
)  x.  ( (Λ `  n )  /  n
) ) )
268267sumeq2sdv 12503 . . . . . . . . . 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 ) ) )
269268, 185oveq12d 6102 . . . . . . . . 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 ) ) )
270269adantl 454 . . . . . . . 8  |-  ( ( ( ph  /\  f  e.  D )  /\  f  =  .1.  )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( f `  ( L `  n )
)  x.  ( (Λ `  n )  /  n
) )  -  (
( log `  x
)  x.  if ( f  =  .1.  , 
1 ,  if ( f  e.  W ,  -u 1 ,  0 ) ) ) )  =  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (  .1.  `  ( L `  n ) )  x.  ( (Λ `  n )  /  n
) )  -  (
( log `  x
)  x.  1 ) ) )
27146recnd 9119 . . . . . . . . . 10  |-  ( x  e.  RR+  ->  ( log `  x )  e.  CC )
272271mulid1d 9110 . . . . . . . . 9  |-  ( x  e.  RR+  ->  ( ( log `  x )  x.  1 )  =  ( log `  x
) )
273272oveq2d 6100 . . . . . . . 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 ) ) )
274270, 273sylan9eq 2490 . . . . . . 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 ) ) )
275274mpteq2dva 4298 . . . . . 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 ) ) ) )
2768, 24, 1, 3, 4, 68rpvmasumlem 21186 . . . . . . 7  |-  ( ph  ->  ( x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (  .1.  `  ( L `  n ) )  x.  ( (Λ `  n )  /  n
) )  -  ( log `  x ) ) )  e.  O ( 1 ) )
277276ad2antrr 708 . . . . . 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 ) )
278275, 277eqeltrd 2512 . . . . 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 ) )
279189oveq2d 6100 . . . . . . . . . 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 ) ) )
280279oveq2d 6100 . . . . . . . . 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 ) ) ) )
28148adantlr 697 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  f  e.  D )  /\  x  e.  RR+ )  ->  ( log `  x )  e.  CC )
282 mulcom 9081 . . . . . . . . . . . . . . 15  |-  ( ( ( log `  x
)  e.  CC  /\  -u 1  e.  CC )  ->  ( ( log `  x )  x.  -u 1
)  =  ( -u
1  x.  ( log `  x ) ) )
283281, 51, 282sylancl 645 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  f  e.  D )  /\  x  e.  RR+ )  ->  (
( log `  x
)  x.  -u 1
)  =  ( -u
1  x.  ( log `  x ) ) )
284281mulm1d 9490 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  f  e.  D )  /\  x  e.  RR+ )  ->  ( -u 1  x.  ( log `  x ) )  = 
-u ( log `  x
) )
285283, 284eqtrd 2470 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  f  e.  D )  /\  x  e.  RR+ )  ->  (
( log `  x
)  x.  -u 1
)  =  -u ( log `  x ) )
286281mul01d 9270 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  f  e.  D )  /\  x  e.  RR+ )  ->  (
( log `  x
)  x.  0 )  =  0 )
287285, 286ifeq12d 3757 . . . . . . . . . . . 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 ) )
288 oveq2 6092 . . . . . . . . . . . . 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 ) )
289 oveq2 6092 . . . . . . . . . . . . 13  |-  ( if ( f  e.  W ,  -u 1 ,  0 )  =  0  -> 
( ( log `  x
)  x.  if ( f  e.  W ,  -u 1 ,  0 ) )  =  ( ( log `  x )  x.  0 ) )
290288, 289ifsb 3750 . . . . . . . . . . . 12  |-  ( ( log `  x )  x.  if ( f  e.  W ,  -u
1 ,  0 ) )  =  if ( f  e.  W , 
( ( log `  x
)  x.  -u 1
) ,  ( ( log `  x )  x.  0 ) )
291 negeq 9303 . . . . . . . . . . . . 13  |-  ( if ( f  e.  W ,  ( log `  x
) ,  0 )  =  ( log `  x
)  ->  -u if ( f  e.  W , 
( log `  x
) ,  0 )  =  -u ( log `  x
) )
292 negeq 9303 . . . . . . . . . . . . . 14  |-  ( if ( f  e.  W ,  ( log `  x
) ,  0 )  =  0  ->  -u if ( f  e.  W ,  ( log `  x
) ,  0 )  =  -u 0 )
293292, 193syl6eq 2486 . . . . . . . . . . . . 13  |-  ( if ( f  e.  W ,  ( log `  x
) ,  0 )  =  0  ->  -u if ( f  e.  W ,  ( log `  x
) ,  0 )  =  0 )
294291, 293ifsb 3750 . . . . . . . . . . . 12  |-  -u if ( f  e.  W ,  ( log `  x
) ,  0 )  =  if ( f  e.  W ,  -u ( log `  x ) ,  0 )
295287, 290, 2943eqtr4g 2495 . . . . . . . . . . 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 ) )
296295oveq2d 6100 . . . . . . . . . 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 ) ) )
29759an32s 781 . . . . . . . . . . 11  |-  ( ( ( ph  /\  f  e.  D )  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( f `  ( L `  n ) )  x.  ( (Λ `  n )  /  n
) )  e.  CC )
298 ifcl 3777 . . . . . . . . . . . 12  |-  ( ( ( log `  x
)  e.  CC  /\  0  e.  CC )  ->  if ( f  e.  W ,  ( log `  x ) ,  0 )  e.  CC )
299281, 52, 298sylancl 645 . . . . . . . . . . 11  |-  ( ( ( ph  /\  f  e.  D )  /\  x  e.  RR+ )  ->  if ( f  e.  W ,  ( log `  x
) ,  0 )  e.  CC )
300297, 299subnegd 9423 . . . . . . . . . 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 ) ) )
301296, 300eqtrd 2470 . . . . . . . . 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 ) ) )
302280, 301sylan9eqr 2492 . . . . . . . 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 ) ) )
303302an32s 781 . . . . . . 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 ) ) )
304303mpteq2dva 4298 . . . . . 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 ) ) ) )
3051ad2antrr 708 . . . . . . . 8  |-  ( ( ( ph  /\  f  e.  D )  /\  f  =/=  .1.  )  ->  N  e.  NN )
306 simplr 733 . . . . . . . 8  |-  ( ( ( ph  /\  f  e.  D )  /\  f  =/=  .1.  )  ->  f  e.  D )
307 simpr 449 . . . . . . . 8  |-  ( ( ( ph  /\  f  e.  D )  /\  f  =/=  .1.  )  ->  f  =/=  .1.  )
308 eqid 2438 . . . . . . . 8  |-  ( a  e.  NN  |->  ( ( f `  ( L `
 a ) )  /  a ) )  =  ( a  e.  NN  |->  ( ( f `
 ( L `  a ) )  / 
a ) )
3098, 24, 305, 3, 4, 68, 306, 307, 308dchrmusumlema 21192 . . . . . . 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 ) ) )
3101adantr 453 . . . . . . . . . . . . 13  |-  ( (
ph  /\  f  e.  D )  ->  N  e.  NN )
311310ad2antrr 708 . . . . . . . . . . . 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 )
312306adantr 453 . . . . . . . . . . . 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 )
313 simplr 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 ) ) ) )  ->  f  =/=  .1.  )
314 simprl 734 . . . . . . . . . . . 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 ) )
315 simprrl 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 ) ) ) )  ->  seq  1
(  +  ,  ( a  e.  NN  |->  ( ( f `  ( L `  a )
)  /  a ) ) )  ~~>  t )
316 simprrr 743 . . . . . . . . . . . 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 ) )
3178, 24, 311, 3, 4, 68, 312, 313, 308, 314, 315, 316, 213dchrvmaeq0 21203 . . . . . . . . . . 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 ) )
318 ifbi 3758 . . . . . . . . . . . . 13  |-  ( ( f  e.  W  <->  t  = 
0 )  ->  if ( f  e.  W ,  ( log `  x
) ,  0 )  =  if ( t  =  0 ,  ( log `  x ) ,  0 ) )
319318oveq2d 6100 . . . . . . . . . . . 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 ) ) )
320319mpteq2dv 4299 . . . . . . . . . . 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 ) ) ) )
321317, 320syl 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