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

Theorem dchrvmasumiflem1 22749
Description: Lemma for dchrvmasumif 22751. (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 )
rpvmasum.g  |-  G  =  (DChr `  N )
rpvmasum.d  |-  D  =  ( Base `  G
)
rpvmasum.1  |-  .1.  =  ( 0g `  G )
dchrisum.b  |-  ( ph  ->  X  e.  D )
dchrisum.n1  |-  ( ph  ->  X  =/=  .1.  )
dchrvmasumif.f  |-  F  =  ( a  e.  NN  |->  ( ( X `  ( L `  a ) )  /  a ) )
dchrvmasumif.c  |-  ( ph  ->  C  e.  ( 0 [,) +oo ) )
dchrvmasumif.s  |-  ( ph  ->  seq 1 (  +  ,  F )  ~~>  S )
dchrvmasumif.1  |-  ( ph  ->  A. y  e.  ( 1 [,) +oo )
( abs `  (
(  seq 1 (  +  ,  F ) `  ( |_ `  y ) )  -  S ) )  <_  ( C  /  y ) )
dchrvmasumif.g  |-  K  =  ( a  e.  NN  |->  ( ( X `  ( L `  a ) )  x.  ( ( log `  a )  /  a ) ) )
dchrvmasumif.e  |-  ( ph  ->  E  e.  ( 0 [,) +oo ) )
dchrvmasumif.t  |-  ( ph  ->  seq 1 (  +  ,  K )  ~~>  T )
dchrvmasumif.2  |-  ( ph  ->  A. y  e.  ( 3 [,) +oo )
( abs `  (
(  seq 1 (  +  ,  K ) `  ( |_ `  y ) )  -  T ) )  <_  ( E  x.  ( ( log `  y
)  /  y ) ) )
Assertion
Ref Expression
dchrvmasumiflem1  |-  ( ph  ->  ( x  e.  RR+  |->  sum_ d  e.  ( 1 ... ( |_ `  x ) ) ( ( ( X `  ( L `  d ) )  x.  ( ( mmu `  d )  /  d ) )  x.  ( sum_ k  e.  ( 1 ... ( |_ `  ( x  / 
d ) ) ) ( ( X `  ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  ( x  /  d
) ,  k ) )  /  k ) )  -  if ( S  =  0 ,  0 ,  T ) ) ) )  e.  O(1) )
Distinct variable groups:    x, k,
y,  .1.    x, d, y, C    k, d, F, x, y    a, d, k, x, y    E, d, x, y    k, K, y    k, N, x, y    ph, d, k, x    T, d, x, y    S, d, k, x, y    k, Z, x, y    D, k, x, y    L, a, d, k, x, y    X, a, d, k, x, y
Allowed substitution hints:    ph( y, a)    C( k, a)    D( a, d)    S( a)    T( k, a)    .1. ( a, d)    E( k, a)    F( a)    G( x, y, k, a, d)    K( x, a, d)    N( a, d)    Z( a, d)

Proof of Theorem dchrvmasumiflem1
Dummy variable  m is distinct from all other variables.
StepHypRef Expression
1 rpvmasum.z . 2  |-  Z  =  (ℤ/n `  N )
2 rpvmasum.l . 2  |-  L  =  ( ZRHom `  Z
)
3 rpvmasum.a . 2  |-  ( ph  ->  N  e.  NN )
4 rpvmasum.g . 2  |-  G  =  (DChr `  N )
5 rpvmasum.d . 2  |-  D  =  ( Base `  G
)
6 rpvmasum.1 . 2  |-  .1.  =  ( 0g `  G )
7 dchrisum.b . 2  |-  ( ph  ->  X  e.  D )
8 dchrisum.n1 . 2  |-  ( ph  ->  X  =/=  .1.  )
9 fzfid 11794 . . 3  |-  ( (
ph  /\  m  e.  RR+ )  ->  ( 1 ... ( |_ `  m ) )  e. 
Fin )
10 simpl 457 . . . . 5  |-  ( (
ph  /\  m  e.  RR+ )  ->  ph )
11 elfznn 11477 . . . . 5  |-  ( k  e.  ( 1 ... ( |_ `  m
) )  ->  k  e.  NN )
127adantr 465 . . . . . 6  |-  ( (
ph  /\  k  e.  NN )  ->  X  e.  D )
13 nnz 10667 . . . . . . 7  |-  ( k  e.  NN  ->  k  e.  ZZ )
1413adantl 466 . . . . . 6  |-  ( (
ph  /\  k  e.  NN )  ->  k  e.  ZZ )
154, 1, 5, 2, 12, 14dchrzrhcl 22583 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  ( X `
 ( L `  k ) )  e.  CC )
1610, 11, 15syl2an 477 . . . 4  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( X `  ( L `  k
) )  e.  CC )
17 simpr 461 . . . . . . . 8  |-  ( (
ph  /\  m  e.  RR+ )  ->  m  e.  RR+ )
1811nnrpd 11025 . . . . . . . 8  |-  ( k  e.  ( 1 ... ( |_ `  m
) )  ->  k  e.  RR+ )
19 ifcl 3830 . . . . . . . 8  |-  ( ( m  e.  RR+  /\  k  e.  RR+ )  ->  if ( S  =  0 ,  m ,  k )  e.  RR+ )
2017, 18, 19syl2an 477 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  if ( S  =  0 ,  m ,  k )  e.  RR+ )
2120relogcld 22071 . . . . . 6  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( log `  if ( S  =  0 ,  m ,  k ) )  e.  RR )
2211adantl 466 . . . . . 6  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  k  e.  NN )
2321, 22nndivred 10369 . . . . 5  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k )  e.  RR )
2423recnd 9411 . . . 4  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k )  e.  CC )
2516, 24mulcld 9405 . . 3  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( ( X `  ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  e.  CC )
269, 25fsumcl 13209 . 2  |-  ( (
ph  /\  m  e.  RR+ )  ->  sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( ( X `  ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  e.  CC )
27 fveq2 5690 . . . 4  |-  ( m  =  ( x  / 
d )  ->  ( |_ `  m )  =  ( |_ `  (
x  /  d ) ) )
2827oveq2d 6106 . . 3  |-  ( m  =  ( x  / 
d )  ->  (
1 ... ( |_ `  m ) )  =  ( 1 ... ( |_ `  ( x  / 
d ) ) ) )
29 ifeq1 3794 . . . . . . 7  |-  ( m  =  ( x  / 
d )  ->  if ( S  =  0 ,  m ,  k )  =  if ( S  =  0 ,  ( x  /  d ) ,  k ) )
3029fveq2d 5694 . . . . . 6  |-  ( m  =  ( x  / 
d )  ->  ( log `  if ( S  =  0 ,  m ,  k ) )  =  ( log `  if ( S  =  0 ,  ( x  / 
d ) ,  k ) ) )
3130oveq1d 6105 . . . . 5  |-  ( m  =  ( x  / 
d )  ->  (
( log `  if ( S  =  0 ,  m ,  k ) )  /  k )  =  ( ( log `  if ( S  =  0 ,  ( x  /  d ) ,  k ) )  / 
k ) )
3231oveq2d 6106 . . . 4  |-  ( m  =  ( x  / 
d )  ->  (
( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  =  ( ( X `  ( L `
 k ) )  x.  ( ( log `  if ( S  =  0 ,  ( x  /  d ) ,  k ) )  / 
k ) ) )
3332adantr 465 . . 3  |-  ( ( m  =  ( x  /  d )  /\  k  e.  ( 1 ... ( |_ `  ( x  /  d
) ) ) )  ->  ( ( X `
 ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  =  ( ( X `  ( L `
 k ) )  x.  ( ( log `  if ( S  =  0 ,  ( x  /  d ) ,  k ) )  / 
k ) ) )
3428, 33sumeq12rdv 13183 . 2  |-  ( m  =  ( x  / 
d )  ->  sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( ( X `  ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  =  sum_ k  e.  ( 1 ... ( |_ `  ( x  / 
d ) ) ) ( ( X `  ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  ( x  /  d
) ,  k ) )  /  k ) ) )
35 dchrvmasumif.c . . . 4  |-  ( ph  ->  C  e.  ( 0 [,) +oo ) )
3635adantr 465 . . 3  |-  ( (
ph  /\  S  = 
0 )  ->  C  e.  ( 0 [,) +oo ) )
37 dchrvmasumif.e . . . 4  |-  ( ph  ->  E  e.  ( 0 [,) +oo ) )
3837adantr 465 . . 3  |-  ( (
ph  /\  -.  S  =  0 )  ->  E  e.  ( 0 [,) +oo ) )
3936, 38ifclda 3820 . 2  |-  ( ph  ->  if ( S  =  0 ,  C ,  E )  e.  ( 0 [,) +oo )
)
40 0cn 9377 . . 3  |-  0  e.  CC
41 dchrvmasumif.t . . . 4  |-  ( ph  ->  seq 1 (  +  ,  K )  ~~>  T )
42 climcl 12976 . . . 4  |-  (  seq 1 (  +  ,  K )  ~~>  T  ->  T  e.  CC )
4341, 42syl 16 . . 3  |-  ( ph  ->  T  e.  CC )
44 ifcl 3830 . . 3  |-  ( ( 0  e.  CC  /\  T  e.  CC )  ->  if ( S  =  0 ,  0 ,  T )  e.  CC )
4540, 43, 44sylancr 663 . 2  |-  ( ph  ->  if ( S  =  0 ,  0 ,  T )  e.  CC )
46 nnuz 10895 . . . . . . . . 9  |-  NN  =  ( ZZ>= `  1 )
47 1zzd 10676 . . . . . . . . 9  |-  ( ph  ->  1  e.  ZZ )
48 nncn 10329 . . . . . . . . . . . . 13  |-  ( k  e.  NN  ->  k  e.  CC )
4948adantl 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN )  ->  k  e.  CC )
50 nnne0 10353 . . . . . . . . . . . . 13  |-  ( k  e.  NN  ->  k  =/=  0 )
5150adantl 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN )  ->  k  =/=  0 )
5215, 49, 51divcld 10106 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( X `  ( L `
 k ) )  /  k )  e.  CC )
53 dchrvmasumif.f . . . . . . . . . . . 12  |-  F  =  ( a  e.  NN  |->  ( ( X `  ( L `  a ) )  /  a ) )
54 fveq2 5690 . . . . . . . . . . . . . . 15  |-  ( a  =  k  ->  ( L `  a )  =  ( L `  k ) )
5554fveq2d 5694 . . . . . . . . . . . . . 14  |-  ( a  =  k  ->  ( X `  ( L `  a ) )  =  ( X `  ( L `  k )
) )
56 id 22 . . . . . . . . . . . . . 14  |-  ( a  =  k  ->  a  =  k )
5755, 56oveq12d 6108 . . . . . . . . . . . . 13  |-  ( a  =  k  ->  (
( X `  ( L `  a )
)  /  a )  =  ( ( X `
 ( L `  k ) )  / 
k ) )
5857cbvmptv 4382 . . . . . . . . . . . 12  |-  ( a  e.  NN  |->  ( ( X `  ( L `
 a ) )  /  a ) )  =  ( k  e.  NN  |->  ( ( X `
 ( L `  k ) )  / 
k ) )
5953, 58eqtri 2462 . . . . . . . . . . 11  |-  F  =  ( k  e.  NN  |->  ( ( X `  ( L `  k ) )  /  k ) )
6052, 59fmptd 5866 . . . . . . . . . 10  |-  ( ph  ->  F : NN --> CC )
61 ffvelrn 5840 . . . . . . . . . 10  |-  ( ( F : NN --> CC  /\  k  e.  NN )  ->  ( F `  k
)  e.  CC )
6260, 61sylan 471 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  NN )  ->  ( F `
 k )  e.  CC )
6346, 47, 62serf 11833 . . . . . . . 8  |-  ( ph  ->  seq 1 (  +  ,  F ) : NN --> CC )
6463ad2antrr 725 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =  0 )  ->  seq 1 (  +  ,  F ) : NN --> CC )
65 3re 10394 . . . . . . . . . . 11  |-  3  e.  RR
66 elicopnf 11384 . . . . . . . . . . 11  |-  ( 3  e.  RR  ->  (
m  e.  ( 3 [,) +oo )  <->  ( m  e.  RR  /\  3  <_  m ) ) )
6765, 66mp1i 12 . . . . . . . . . 10  |-  ( ph  ->  ( m  e.  ( 3 [,) +oo )  <->  ( m  e.  RR  /\  3  <_  m ) ) )
6867simprbda 623 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  m  e.  RR )
69 1red 9400 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  1  e.  RR )
7065a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  3  e.  RR )
71 1le3 10537 . . . . . . . . . . 11  |-  1  <_  3
7271a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  1  <_  3 )
7367simplbda 624 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  3  <_  m )
7469, 70, 68, 72, 73letrd 9527 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  1  <_  m )
75 flge1nn 11666 . . . . . . . . 9  |-  ( ( m  e.  RR  /\  1  <_  m )  -> 
( |_ `  m
)  e.  NN )
7668, 74, 75syl2anc 661 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  ( |_ `  m )  e.  NN )
7776adantr 465 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =  0 )  -> 
( |_ `  m
)  e.  NN )
7864, 77ffvelrnd 5843 . . . . . 6  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =  0 )  -> 
(  seq 1 (  +  ,  F ) `  ( |_ `  m ) )  e.  CC )
7978abscld 12921 . . . . 5  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =  0 )  -> 
( abs `  (  seq 1 (  +  ,  F ) `  ( |_ `  m ) ) )  e.  RR )
80 simpl 457 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  ph )
81 0red 9386 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  0  e.  RR )
82 3pos 10414 . . . . . . . . . . 11  |-  0  <  3
8382a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  0  <  3 )
8481, 70, 68, 83, 73ltletrd 9530 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  0  <  m )
8568, 84elrpd 11024 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  m  e.  RR+ )
8680, 85jca 532 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  ( ph  /\  m  e.  RR+ ) )
87 elrege0 11391 . . . . . . . . . 10  |-  ( C  e.  ( 0 [,) +oo )  <->  ( C  e.  RR  /\  0  <_  C ) )
8887simplbi 460 . . . . . . . . 9  |-  ( C  e.  ( 0 [,) +oo )  ->  C  e.  RR )
8935, 88syl 16 . . . . . . . 8  |-  ( ph  ->  C  e.  RR )
90 rerpdivcl 11017 . . . . . . . 8  |-  ( ( C  e.  RR  /\  m  e.  RR+ )  -> 
( C  /  m
)  e.  RR )
9189, 90sylan 471 . . . . . . 7  |-  ( (
ph  /\  m  e.  RR+ )  ->  ( C  /  m )  e.  RR )
9286, 91syl 16 . . . . . 6  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  ( C  /  m )  e.  RR )
9392adantr 465 . . . . 5  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =  0 )  -> 
( C  /  m
)  e.  RR )
9485relogcld 22071 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  ( log `  m )  e.  RR )
9568, 74logge0d 22078 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  0  <_  ( log `  m
) )
9694, 95jca 532 . . . . . 6  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  (
( log `  m
)  e.  RR  /\  0  <_  ( log `  m
) ) )
9796adantr 465 . . . . 5  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =  0 )  -> 
( ( log `  m
)  e.  RR  /\  0  <_  ( log `  m
) ) )
98 oveq2 6098 . . . . . . . 8  |-  ( S  =  0  ->  (
(  seq 1 (  +  ,  F ) `  ( |_ `  m ) )  -  S )  =  ( (  seq 1 (  +  ,  F ) `  ( |_ `  m ) )  -  0 ) )
9963adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  seq 1 (  +  ,  F ) : NN --> CC )
10099, 76ffvelrnd 5843 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  (  seq 1 (  +  ,  F ) `  ( |_ `  m ) )  e.  CC )
101100subid1d 9707 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  (
(  seq 1 (  +  ,  F ) `  ( |_ `  m ) )  -  0 )  =  (  seq 1
(  +  ,  F
) `  ( |_ `  m ) ) )
10298, 101sylan9eqr 2496 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =  0 )  -> 
( (  seq 1
(  +  ,  F
) `  ( |_ `  m ) )  -  S )  =  (  seq 1 (  +  ,  F ) `  ( |_ `  m ) ) )
103102fveq2d 5694 . . . . . 6  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =  0 )  -> 
( abs `  (
(  seq 1 (  +  ,  F ) `  ( |_ `  m ) )  -  S ) )  =  ( abs `  (  seq 1
(  +  ,  F
) `  ( |_ `  m ) ) ) )
104 1re 9384 . . . . . . . . . 10  |-  1  e.  RR
105 elicopnf 11384 . . . . . . . . . 10  |-  ( 1  e.  RR  ->  (
m  e.  ( 1 [,) +oo )  <->  ( m  e.  RR  /\  1  <_  m ) ) )
106104, 105ax-mp 5 . . . . . . . . 9  |-  ( m  e.  ( 1 [,) +oo )  <->  ( m  e.  RR  /\  1  <_  m ) )
10768, 74, 106sylanbrc 664 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  m  e.  ( 1 [,) +oo ) )
108 dchrvmasumif.1 . . . . . . . . 9  |-  ( ph  ->  A. y  e.  ( 1 [,) +oo )
( abs `  (
(  seq 1 (  +  ,  F ) `  ( |_ `  y ) )  -  S ) )  <_  ( C  /  y ) )
109108adantr 465 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  A. y  e.  ( 1 [,) +oo ) ( abs `  (
(  seq 1 (  +  ,  F ) `  ( |_ `  y ) )  -  S ) )  <_  ( C  /  y ) )
110 fveq2 5690 . . . . . . . . . . . . 13  |-  ( y  =  m  ->  ( |_ `  y )  =  ( |_ `  m
) )
111110fveq2d 5694 . . . . . . . . . . . 12  |-  ( y  =  m  ->  (  seq 1 (  +  ,  F ) `  ( |_ `  y ) )  =  (  seq 1
(  +  ,  F
) `  ( |_ `  m ) ) )
112111oveq1d 6105 . . . . . . . . . . 11  |-  ( y  =  m  ->  (
(  seq 1 (  +  ,  F ) `  ( |_ `  y ) )  -  S )  =  ( (  seq 1 (  +  ,  F ) `  ( |_ `  m ) )  -  S ) )
113112fveq2d 5694 . . . . . . . . . 10  |-  ( y  =  m  ->  ( abs `  ( (  seq 1 (  +  ,  F ) `  ( |_ `  y ) )  -  S ) )  =  ( abs `  (
(  seq 1 (  +  ,  F ) `  ( |_ `  m ) )  -  S ) ) )
114 oveq2 6098 . . . . . . . . . 10  |-  ( y  =  m  ->  ( C  /  y )  =  ( C  /  m
) )
115113, 114breq12d 4304 . . . . . . . . 9  |-  ( y  =  m  ->  (
( abs `  (
(  seq 1 (  +  ,  F ) `  ( |_ `  y ) )  -  S ) )  <_  ( C  /  y )  <->  ( abs `  ( (  seq 1
(  +  ,  F
) `  ( |_ `  m ) )  -  S ) )  <_ 
( C  /  m
) ) )
116115rspcv 3068 . . . . . . . 8  |-  ( m  e.  ( 1 [,) +oo )  ->  ( A. y  e.  ( 1 [,) +oo ) ( abs `  ( (  seq 1 (  +  ,  F ) `  ( |_ `  y ) )  -  S ) )  <_  ( C  /  y )  -> 
( abs `  (
(  seq 1 (  +  ,  F ) `  ( |_ `  m ) )  -  S ) )  <_  ( C  /  m ) ) )
117107, 109, 116sylc 60 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  ( abs `  ( (  seq 1 (  +  ,  F ) `  ( |_ `  m ) )  -  S ) )  <_  ( C  /  m ) )
118117adantr 465 . . . . . 6  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =  0 )  -> 
( abs `  (
(  seq 1 (  +  ,  F ) `  ( |_ `  m ) )  -  S ) )  <_  ( C  /  m ) )
119103, 118eqbrtrrd 4313 . . . . 5  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =  0 )  -> 
( abs `  (  seq 1 (  +  ,  F ) `  ( |_ `  m ) ) )  <_  ( C  /  m ) )
120 lemul2a 10183 . . . . 5  |-  ( ( ( ( abs `  (  seq 1 (  +  ,  F ) `  ( |_ `  m ) ) )  e.  RR  /\  ( C  /  m
)  e.  RR  /\  ( ( log `  m
)  e.  RR  /\  0  <_  ( log `  m
) ) )  /\  ( abs `  (  seq 1 (  +  ,  F ) `  ( |_ `  m ) ) )  <_  ( C  /  m ) )  -> 
( ( log `  m
)  x.  ( abs `  (  seq 1
(  +  ,  F
) `  ( |_ `  m ) ) ) )  <_  ( ( log `  m )  x.  ( C  /  m
) ) )
12179, 93, 97, 119, 120syl31anc 1221 . . . 4  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =  0 )  -> 
( ( log `  m
)  x.  ( abs `  (  seq 1
(  +  ,  F
) `  ( |_ `  m ) ) ) )  <_  ( ( log `  m )  x.  ( C  /  m
) ) )
122 iftrue 3796 . . . . . . . . . . . . . . 15  |-  ( S  =  0  ->  if ( S  =  0 ,  m ,  k )  =  m )
123122fveq2d 5694 . . . . . . . . . . . . . 14  |-  ( S  =  0  ->  ( log `  if ( S  =  0 ,  m ,  k ) )  =  ( log `  m
) )
124123oveq1d 6105 . . . . . . . . . . . . 13  |-  ( S  =  0  ->  (
( log `  if ( S  =  0 ,  m ,  k ) )  /  k )  =  ( ( log `  m )  /  k
) )
125124ad2antlr 726 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  /\  k  e.  ( 1 ... ( |_
`  m ) ) )  ->  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k )  =  ( ( log `  m
)  /  k ) )
126125oveq2d 6106 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  /\  k  e.  ( 1 ... ( |_
`  m ) ) )  ->  ( ( X `  ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  =  ( ( X `  ( L `
 k ) )  x.  ( ( log `  m )  /  k
) ) )
12716adantlr 714 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  /\  k  e.  ( 1 ... ( |_
`  m ) ) )  ->  ( X `  ( L `  k
) )  e.  CC )
128 relogcl 22026 . . . . . . . . . . . . . . 15  |-  ( m  e.  RR+  ->  ( log `  m )  e.  RR )
129128adantl 466 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  RR+ )  ->  ( log `  m )  e.  RR )
130129recnd 9411 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  RR+ )  ->  ( log `  m )  e.  CC )
131130ad2antrr 725 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  /\  k  e.  ( 1 ... ( |_
`  m ) ) )  ->  ( log `  m )  e.  CC )
13211adantl 466 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  /\  k  e.  ( 1 ... ( |_
`  m ) ) )  ->  k  e.  NN )
133132nncnd 10337 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  /\  k  e.  ( 1 ... ( |_
`  m ) ) )  ->  k  e.  CC )
134132nnne0d 10365 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  /\  k  e.  ( 1 ... ( |_
`  m ) ) )  ->  k  =/=  0 )
135127, 131, 133, 134div12d 10142 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  /\  k  e.  ( 1 ... ( |_
`  m ) ) )  ->  ( ( X `  ( L `  k ) )  x.  ( ( log `  m
)  /  k ) )  =  ( ( log `  m )  x.  ( ( X `
 ( L `  k ) )  / 
k ) ) )
136126, 135eqtrd 2474 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  /\  k  e.  ( 1 ... ( |_
`  m ) ) )  ->  ( ( X `  ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  =  ( ( log `  m )  x.  ( ( X `
 ( L `  k ) )  / 
k ) ) )
137136sumeq2dv 13179 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  ->  sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( ( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  =  sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( ( log `  m
)  x.  ( ( X `  ( L `
 k ) )  /  k ) ) )
138 iftrue 3796 . . . . . . . . . . 11  |-  ( S  =  0  ->  if ( S  =  0 ,  0 ,  T
)  =  0 )
139138oveq2d 6106 . . . . . . . . . 10  |-  ( S  =  0  ->  ( sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( ( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  -  if ( S  =  0 ,  0 ,  T ) )  =  ( sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( ( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  -  0 ) )
14026subid1d 9707 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  RR+ )  ->  ( sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( ( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  -  0 )  =  sum_ k  e.  ( 1 ... ( |_
`  m ) ) ( ( X `  ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )
141139, 140sylan9eqr 2496 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  -> 
( sum_ k  e.  ( 1 ... ( |_
`  m ) ) ( ( X `  ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  -  if ( S  =  0 ,  0 ,  T ) )  =  sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( ( X `  ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )
142 ovex 6115 . . . . . . . . . . . . . 14  |-  ( ( X `  ( L `
 k ) )  /  k )  e. 
_V
14357, 53, 142fvmpt 5773 . . . . . . . . . . . . 13  |-  ( k  e.  NN  ->  ( F `  k )  =  ( ( X `
 ( L `  k ) )  / 
k ) )
14422, 143syl 16 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( F `  k )  =  ( ( X `  ( L `  k )
)  /  k ) )
14560adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  RR+ )  ->  F : NN
--> CC )
146145, 11, 61syl2an 477 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( F `  k )  e.  CC )
147144, 146eqeltrrd 2517 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( ( X `  ( L `  k ) )  / 
k )  e.  CC )
1489, 130, 147fsummulc2 13250 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  RR+ )  ->  ( ( log `  m )  x. 
sum_ k  e.  ( 1 ... ( |_
`  m ) ) ( ( X `  ( L `  k ) )  /  k ) )  =  sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( ( log `  m
)  x.  ( ( X `  ( L `
 k ) )  /  k ) ) )
149148adantr 465 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  -> 
( ( log `  m
)  x.  sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( ( X `  ( L `  k ) )  /  k ) )  =  sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( ( log `  m
)  x.  ( ( X `  ( L `
 k ) )  /  k ) ) )
150137, 141, 1493eqtr4d 2484 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  -> 
( sum_ k  e.  ( 1 ... ( |_
`  m ) ) ( ( X `  ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  -  if ( S  =  0 ,  0 ,  T ) )  =  ( ( log `  m )  x.  sum_ k  e.  ( 1 ... ( |_
`  m ) ) ( ( X `  ( L `  k ) )  /  k ) ) )
15186, 150sylan 471 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =  0 )  -> 
( sum_ k  e.  ( 1 ... ( |_
`  m ) ) ( ( X `  ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  -  if ( S  =  0 ,  0 ,  T ) )  =  ( ( log `  m )  x.  sum_ k  e.  ( 1 ... ( |_
`  m ) ) ( ( X `  ( L `  k ) )  /  k ) ) )
15286, 144sylan 471 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( F `  k )  =  ( ( X `  ( L `  k )
)  /  k ) )
15376, 46syl6eleq 2532 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  ( |_ `  m )  e.  ( ZZ>= `  1 )
)
15480, 11, 52syl2an 477 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( ( X `  ( L `  k ) )  / 
k )  e.  CC )
155152, 153, 154fsumser 13206 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( ( X `  ( L `  k ) )  /  k )  =  (  seq 1
(  +  ,  F
) `  ( |_ `  m ) ) )
156155adantr 465 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =  0 )  ->  sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( ( X `  ( L `  k )
)  /  k )  =  (  seq 1
(  +  ,  F
) `  ( |_ `  m ) ) )
157156oveq2d 6106 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =  0 )  -> 
( ( log `  m
)  x.  sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( ( X `  ( L `  k ) )  /  k ) )  =  ( ( log `  m )  x.  (  seq 1
(  +  ,  F
) `  ( |_ `  m ) ) ) )
158151, 157eqtrd 2474 . . . . . 6  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =  0 )  -> 
( sum_ k  e.  ( 1 ... ( |_
`  m ) ) ( ( X `  ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  -  if ( S  =  0 ,  0 ,  T ) )  =  ( ( log `  m )  x.  (  seq 1
(  +  ,  F
) `  ( |_ `  m ) ) ) )
159158fveq2d 5694 . . . . 5  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =  0 )  -> 
( abs `  ( sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( ( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  -  if ( S  =  0 ,  0 ,  T ) ) )  =  ( abs `  ( ( log `  m )  x.  (  seq 1
(  +  ,  F
) `  ( |_ `  m ) ) ) ) )
160128ad2antlr 726 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  -> 
( log `  m
)  e.  RR )
161160recnd 9411 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  -> 
( log `  m
)  e.  CC )
16286, 161sylan 471 . . . . . 6  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =  0 )  -> 
( log `  m
)  e.  CC )
163162, 78absmuld 12939 . . . . 5  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =  0 )  -> 
( abs `  (
( log `  m
)  x.  (  seq 1 (  +  ,  F ) `  ( |_ `  m ) ) ) )  =  ( ( abs `  ( log `  m ) )  x.  ( abs `  (  seq 1 (  +  ,  F ) `  ( |_ `  m ) ) ) ) )
16494, 95absidd 12908 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  ( abs `  ( log `  m
) )  =  ( log `  m ) )
165164oveq1d 6105 . . . . . 6  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  (
( abs `  ( log `  m ) )  x.  ( abs `  (  seq 1 (  +  ,  F ) `  ( |_ `  m ) ) ) )  =  ( ( log `  m
)  x.  ( abs `  (  seq 1
(  +  ,  F
) `  ( |_ `  m ) ) ) ) )
166165adantr 465 . . . . 5  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =  0 )  -> 
( ( abs `  ( log `  m ) )  x.  ( abs `  (  seq 1 (  +  ,  F ) `  ( |_ `  m ) ) ) )  =  ( ( log `  m
)  x.  ( abs `  (  seq 1
(  +  ,  F
) `  ( |_ `  m ) ) ) ) )
167159, 163, 1663eqtrd 2478 . . . 4  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =  0 )  -> 
( abs `  ( sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( ( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  -  if ( S  =  0 ,  0 ,  T ) ) )  =  ( ( log `  m
)  x.  ( abs `  (  seq 1
(  +  ,  F
) `  ( |_ `  m ) ) ) ) )
168 iftrue 3796 . . . . . . . 8  |-  ( S  =  0  ->  if ( S  =  0 ,  C ,  E )  =  C )
169168adantl 466 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  ->  if ( S  =  0 ,  C ,  E
)  =  C )
170169oveq1d 6105 . . . . . 6  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  -> 
( if ( S  =  0 ,  C ,  E )  x.  (
( log `  m
)  /  m ) )  =  ( C  x.  ( ( log `  m )  /  m
) ) )
17189recnd 9411 . . . . . . . 8  |-  ( ph  ->  C  e.  CC )
172171ad2antrr 725 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  ->  C  e.  CC )
173 rpcnne0 11007 . . . . . . . 8  |-  ( m  e.  RR+  ->  ( m  e.  CC  /\  m  =/=  0 ) )
174173ad2antlr 726 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  -> 
( m  e.  CC  /\  m  =/=  0 ) )
175 div12 10015 . . . . . . 7  |-  ( ( C  e.  CC  /\  ( log `  m )  e.  CC  /\  (
m  e.  CC  /\  m  =/=  0 ) )  ->  ( C  x.  ( ( log `  m
)  /  m ) )  =  ( ( log `  m )  x.  ( C  /  m ) ) )
176172, 161, 174, 175syl3anc 1218 . . . . . 6  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  -> 
( C  x.  (
( log `  m
)  /  m ) )  =  ( ( log `  m )  x.  ( C  /  m ) ) )
177170, 176eqtrd 2474 . . . . 5  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  -> 
( if ( S  =  0 ,  C ,  E )  x.  (
( log `  m
)  /  m ) )  =  ( ( log `  m )  x.  ( C  /  m ) ) )
17886, 177sylan 471 . . . 4  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =  0 )  -> 
( if ( S  =  0 ,  C ,  E )  x.  (
( log `  m
)  /  m ) )  =  ( ( log `  m )  x.  ( C  /  m ) ) )
179121, 167, 1783brtr4d 4321 . . 3  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =  0 )  -> 
( abs `  ( sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( ( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  -  if ( S  =  0 ,  0 ,  T ) ) )  <_  ( if ( S  =  0 ,  C ,  E
)  x.  ( ( log `  m )  /  m ) ) )
180 dchrvmasumif.2 . . . . . 6  |-  ( ph  ->  A. y  e.  ( 3 [,) +oo )
( abs `  (
(  seq 1 (  +  ,  K ) `  ( |_ `  y ) )  -  T ) )  <_  ( E  x.  ( ( log `  y
)  /  y ) ) )
181110fveq2d 5694 . . . . . . . . . 10  |-  ( y  =  m  ->  (  seq 1 (  +  ,  K ) `  ( |_ `  y ) )  =  (  seq 1
(  +  ,  K
) `  ( |_ `  m ) ) )
182181oveq1d 6105 . . . . . . . . 9  |-  ( y  =  m  ->  (
(  seq 1 (  +  ,  K ) `  ( |_ `  y ) )  -  T )  =  ( (  seq 1 (  +  ,  K ) `  ( |_ `  m ) )  -  T ) )
183182fveq2d 5694 . . . . . . . 8  |-  ( y  =  m  ->  ( abs `  ( (  seq 1 (  +  ,  K ) `  ( |_ `  y ) )  -  T ) )  =  ( abs `  (
(  seq 1 (  +  ,  K ) `  ( |_ `  m ) )  -  T ) ) )
184 fveq2 5690 . . . . . . . . . 10  |-  ( y  =  m  ->  ( log `  y )  =  ( log `  m
) )
185 id 22 . . . . . . . . . 10  |-  ( y  =  m  ->  y  =  m )
186184, 185oveq12d 6108 . . . . . . . . 9  |-  ( y  =  m  ->  (
( log `  y
)  /  y )  =  ( ( log `  m )  /  m
) )
187186oveq2d 6106 . . . . . . . 8  |-  ( y  =  m  ->  ( E  x.  ( ( log `  y )  / 
y ) )  =  ( E  x.  (
( log `  m
)  /  m ) ) )
188183, 187breq12d 4304 . . . . . . 7  |-  ( y  =  m  ->  (
( abs `  (
(  seq 1 (  +  ,  K ) `  ( |_ `  y ) )  -  T ) )  <_  ( E  x.  ( ( log `  y
)  /  y ) )  <->  ( abs `  (
(  seq 1 (  +  ,  K ) `  ( |_ `  m ) )  -  T ) )  <_  ( E  x.  ( ( log `  m
)  /  m ) ) ) )
189188rspccva 3071 . . . . . 6  |-  ( ( A. y  e.  ( 3 [,) +oo )
( abs `  (
(  seq 1 (  +  ,  K ) `  ( |_ `  y ) )  -  T ) )  <_  ( E  x.  ( ( log `  y
)  /  y ) )  /\  m  e.  ( 3 [,) +oo ) )  ->  ( abs `  ( (  seq 1 (  +  ,  K ) `  ( |_ `  m ) )  -  T ) )  <_  ( E  x.  ( ( log `  m
)  /  m ) ) )
190180, 189sylan 471 . . . . 5  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  ( abs `  ( (  seq 1 (  +  ,  K ) `  ( |_ `  m ) )  -  T ) )  <_  ( E  x.  ( ( log `  m
)  /  m ) ) )
191190adantr 465 . . . 4  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =/=  0 )  ->  ( abs `  ( (  seq 1 (  +  ,  K ) `  ( |_ `  m ) )  -  T ) )  <_  ( E  x.  ( ( log `  m
)  /  m ) ) )
192 fveq2 5690 . . . . . . . . . . . 12  |-  ( a  =  k  ->  ( log `  a )  =  ( log `  k
) )
193192, 56oveq12d 6108 . . . . . . . . . . 11  |-  ( a  =  k  ->  (
( log `  a
)  /  a )  =  ( ( log `  k )  /  k
) )
19455, 193oveq12d 6108 . . . . . . . . . 10  |-  ( a  =  k  ->  (
( X `  ( L `  a )
)  x.  ( ( log `  a )  /  a ) )  =  ( ( X `
 ( L `  k ) )  x.  ( ( log `  k
)  /  k ) ) )
195 dchrvmasumif.g . . . . . . . . . 10  |-  K  =  ( a  e.  NN  |->  ( ( X `  ( L `  a ) )  x.  ( ( log `  a )  /  a ) ) )
196 ovex 6115 . . . . . . . . . 10  |-  ( ( X `  ( L `
 k ) )  x.  ( ( log `  k )  /  k
) )  e.  _V
197194, 195, 196fvmpt 5773 . . . . . . . . 9  |-  ( k  e.  NN  ->  ( K `  k )  =  ( ( X `
 ( L `  k ) )  x.  ( ( log `  k
)  /  k ) ) )
19811, 197syl 16 . . . . . . . 8  |-  ( k  e.  ( 1 ... ( |_ `  m
) )  ->  ( K `  k )  =  ( ( X `
 ( L `  k ) )  x.  ( ( log `  k
)  /  k ) ) )
199 ifnefalse 3800 . . . . . . . . . . . . 13  |-  ( S  =/=  0  ->  if ( S  =  0 ,  m ,  k )  =  k )
200199fveq2d 5694 . . . . . . . . . . . 12  |-  ( S  =/=  0  ->  ( log `  if ( S  =  0 ,  m ,  k ) )  =  ( log `  k
) )
201200oveq1d 6105 . . . . . . . . . . 11  |-  ( S  =/=  0  ->  (
( log `  if ( S  =  0 ,  m ,  k ) )  /  k )  =  ( ( log `  k )  /  k
) )
202201oveq2d 6106 . . . . . . . . . 10  |-  ( S  =/=  0  ->  (
( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  =  ( ( X `  ( L `
 k ) )  x.  ( ( log `  k )  /  k
) ) )
203202adantl 466 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =/=  0 )  ->  (
( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  =  ( ( X `  ( L `
 k ) )  x.  ( ( log `  k )  /  k
) ) )
204203eqcomd 2447 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =/=  0 )  ->  (
( X `  ( L `  k )
)  x.  ( ( log `  k )  /  k ) )  =  ( ( X `
 ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )
205198, 204sylan9eqr 2496 . . . . . . 7  |-  ( ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =/=  0
)  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( K `  k )  =  ( ( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )
206153adantr 465 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =/=  0 )  ->  ( |_ `  m )  e.  ( ZZ>= `  1 )
)
207 nnrp 10999 . . . . . . . . . . . . . . . 16  |-  ( k  e.  NN  ->  k  e.  RR+ )
208207adantl 466 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  NN )  ->  k  e.  RR+ )
209208relogcld 22071 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN )  ->  ( log `  k )  e.  RR )
210209recnd 9411 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  NN )  ->  ( log `  k )  e.  CC )
211210, 49, 51divcld 10106 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( log `  k )  /  k )  e.  CC )
21215, 211mulcld 9405 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( X `  ( L `
 k ) )  x.  ( ( log `  k )  /  k
) )  e.  CC )
213194cbvmptv 4382 . . . . . . . . . . . 12  |-  ( a  e.  NN  |->  ( ( X `  ( L `
 a ) )  x.  ( ( log `  a )  /  a
) ) )  =  ( k  e.  NN  |->  ( ( X `  ( L `  k ) )  x.  ( ( log `  k )  /  k ) ) )
214195, 213eqtri 2462 . . . . . . . . . . 11  |-  K  =  ( k  e.  NN  |->  ( ( X `  ( L `  k ) )  x.  ( ( log `  k )  /  k ) ) )
215212, 214fmptd 5866 . . . . . . . . . 10  |-  ( ph  ->  K : NN --> CC )
216215ad2antrr 725 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =/=  0 )  ->  K : NN --> CC )
217 ffvelrn 5840 . . . . . . . . 9  |-  ( ( K : NN --> CC  /\  k  e.  NN )  ->  ( K `  k
)  e.  CC )
218216, 11, 217syl2an 477 . . . . . . . 8  |-  ( ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =/=  0
)  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( K `  k )  e.  CC )
219205, 218eqeltrrd 2517 . . . . . . 7  |-  ( ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =/=  0
)  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( ( X `  ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  e.  CC )
220205, 206, 219fsumser 13206 . . . . . 6  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =/=  0 )  ->  sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( ( X `  ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  =  (  seq 1 (  +  ,  K ) `  ( |_ `  m ) ) )
221 ifnefalse 3800 . . . . . . 7  |-  ( S  =/=  0  ->  if ( S  =  0 ,  0 ,  T
)  =  T )
222221adantl 466 . . . . . 6  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =/=  0 )  ->  if ( S  =  0 ,  0 ,  T
)  =  T )
223220, 222oveq12d 6108 . . . . 5  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =/=  0 )  ->  ( sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( ( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  -  if ( S  =  0 ,  0 ,  T ) )  =  ( (  seq 1 (  +  ,  K ) `  ( |_ `  m ) )  -  T ) )
224223fveq2d 5694 . . . 4  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =/=  0 )  ->  ( abs `  ( sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( ( X `  ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  -  if ( S  =  0 ,  0 ,  T ) ) )  =  ( abs `  ( (  seq 1 (  +  ,  K ) `  ( |_ `  m ) )  -  T ) ) )
225 ifnefalse 3800 . . . . . 6  |-  ( S  =/=  0  ->  if ( S  =  0 ,  C ,  E )  =  E )
226225adantl 466 . . . . 5  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =/=  0 )  ->  if ( S  =  0 ,  C ,  E )  =  E )
227226oveq1d 6105 . . . 4  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =/=  0 )  ->  ( if ( S  =  0 ,  C ,  E
)  x.  ( ( log `  m )  /  m ) )  =  ( E  x.  ( ( log `  m
)  /  m ) ) )
228191, 224, 2273brtr4d 4321 . . 3  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =/=  0 )  ->  ( abs `  ( sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( ( X `  ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  -  if ( S  =  0 ,  0 ,  T ) ) )  <_  ( if ( S  =  0 ,  C ,  E
)  x.  ( ( log `  m )  /  m ) ) )
229179, 228pm2.61dane 2688 . 2  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  ( abs `  ( sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( ( X `  ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  -  if ( S  =  0 ,  0 ,  T ) ) )  <_  ( if ( S  =  0 ,  C ,  E
)  x.  ( ( log `  m )  /  m ) ) )
230 fzfid 11794 . . . 4  |-  ( ph  ->  ( 1 ... 2
)  e.  Fin )
2317adantr 465 . . . . . . 7  |-  ( (
ph  /\  k  e.  ( 1 ... 2
) )  ->  X  e.  D )
232 elfzelz 11452 . . . . . . . 8  |-  ( k  e.  ( 1 ... 2 )  ->  k  e.  ZZ )
233232adantl 466 . . . . . . 7  |-  ( (
ph  /\  k  e.  ( 1 ... 2
) )  ->  k  e.  ZZ )
2344, 1, 5, 2, 231, 233dchrzrhcl 22583 . . . . . 6  |-  ( (
ph  /\  k  e.  ( 1 ... 2
) )  ->  ( X `  ( L `  k ) )  e.  CC )
235234abscld 12921 . . . . 5  |-  ( (
ph  /\  k  e.  ( 1 ... 2
) )  ->  ( abs `  ( X `  ( L `  k ) ) )  e.  RR )
23665, 82elrpii 10993 . . . . . . 7  |-  3  e.  RR+
237 relogcl 22026 . . . . . . 7  |-  ( 3  e.  RR+  ->  ( log `  3 )  e.  RR )
238236, 237ax-mp 5 . . . . . 6  |-  ( log `  3 )  e.  RR
239 elfznn 11477 . . . . . . 7  |-  ( k  e.  ( 1 ... 2 )  ->  k  e.  NN )
240239adantl 466 . . . . . 6  |-  ( (
ph  /\  k  e.  ( 1 ... 2
) )  ->  k  e.  NN )
241 nndivre 10356 . . . . . 6  |-  ( ( ( log `  3
)  e.  RR  /\  k  e.  NN )  ->  ( ( log `  3
)  /  k )  e.  RR )
242238, 240, 241sylancr 663 . . . . 5  |-  ( (
ph  /\  k  e.  ( 1 ... 2
) )  ->  (
( log `  3
)  /  k )  e.  RR )
243235, 242remulcld 9413 . . . 4  |-  ( (
ph  /\  k  e.  ( 1 ... 2
) )  ->  (
( abs `  ( X `  ( L `  k ) ) )  x.  ( ( log `  3 )  / 
k ) )  e.  RR )
244230, 243fsumrecl 13210 . . 3  |-  ( ph  -> 
sum_ k  e.  ( 1 ... 2 ) ( ( abs `  ( X `  ( L `  k ) ) )  x.  ( ( log `  3 )  / 
k ) )  e.  RR )
24545abscld 12921 . . 3  |-  ( ph  ->  ( abs `  if ( S  =  0 ,  0 ,  T
) )  e.  RR )
246244, 245readdcld 9412 . 2  |-  ( ph  ->  ( sum_ k  e.  ( 1 ... 2 ) ( ( abs `  ( X `  ( L `  k ) ) )  x.  ( ( log `  3 )  / 
k ) )  +  ( abs `  if ( S  =  0 ,  0 ,  T
) ) )  e.  RR )
247 simpl 457 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  ph )
24865rexri 9435 . . . . . . . . . . 11  |-  3  e.  RR*
249 elico2 11358 . . . . . . . . . . 11  |-  ( ( 1  e.  RR  /\  3  e.  RR* )  -> 
( m  e.  ( 1 [,) 3 )  <-> 
( m  e.  RR  /\  1  <_  m  /\  m  <  3 ) ) )
250104, 248, 249mp2an 672 . . . . . . . . . 10  |-  ( m  e.  ( 1 [,) 3 )  <->  ( m  e.  RR  /\  1  <_  m  /\  m  <  3
) )
251250simp1bi 1003 . . . . . . . . 9  |-  ( m  e.  ( 1 [,) 3 )  ->  m  e.  RR )
252251adantl 466 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  m  e.  RR )
253 0red 9386 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  0  e.  RR )
254 1red 9400 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  1  e.  RR )
255 0lt1 9861 . . . . . . . . . 10  |-  0  <  1
256255a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  0  <  1 )
257250simp2bi 1004 . . . . . . . . . 10  |-  ( m  e.  ( 1 [,) 3 )  ->  1  <_  m )
258257adantl 466 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  1  <_  m )
259253, 254, 252, 256, 258ltletrd 9530 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  0  <  m )
260252, 259elrpd 11024 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  m  e.  RR+ )
261247, 260jca 532 . . . . . 6  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  ( ph  /\  m  e.  RR+ ) )
26245adantr 465 . . . . . . 7  |-  ( (
ph  /\  m  e.  RR+ )  ->  if ( S  =  0 , 
0 ,  T )  e.  CC )
26326, 262subcld 9718 . . . . . 6  |-  ( (
ph  /\  m  e.  RR+ )  ->  ( sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( ( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  -  if ( S  =  0 ,  0 ,  T ) )  e.  CC )
264261, 263syl 16 . . . . 5  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  ( sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( ( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  -  if ( S  =  0 ,  0 ,  T ) )  e.  CC )
265264abscld 12921 . . . 4  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  ( abs `  ( sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( ( X `  ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  -  if ( S  =  0 ,  0 ,  T ) ) )  e.  RR )
266261, 26syl 16 . . . . . 6  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( ( X `  ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  e.  CC )
267266abscld 12921 . . . . 5  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  ( abs `  sum_ k  e.  ( 1 ... ( |_
`  m ) ) ( ( X `  ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  e.  RR )
268245adantr 465 . . . . 5  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  ( abs `  if ( S  =  0 ,  0 ,  T ) )  e.  RR )
269267, 268readdcld 9412 . . . 4  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  (
( abs `  sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( ( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  +  ( abs `  if ( S  =  0 ,  0 ,  T ) ) )  e.  RR )
270244adantr 465 . . . . 5  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  sum_ k  e.  ( 1 ... 2
) ( ( abs `  ( X `  ( L `  k )
) )  x.  (
( log `  3
)  /  k ) )  e.  RR )
271270, 268readdcld 9412 . . . 4  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  ( sum_ k  e.  ( 1 ... 2 ) ( ( abs `  ( X `  ( L `  k ) ) )  x.  ( ( log `  3 )  / 
k ) )  +  ( abs `  if ( S  =  0 ,  0 ,  T
) ) )  e.  RR )
27226, 262abs2dif2d 12943 . . . . 5  |-  ( (
ph  /\  m  e.  RR+ )  ->  ( abs `  ( sum_ k  e.  ( 1 ... ( |_
`  m ) ) ( ( X `  ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  -  if ( S  =  0 ,  0 ,  T ) ) )  <_  (
( abs `  sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( ( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  +  ( abs `  if ( S  =  0 ,  0 ,  T ) ) ) )
273261, 272syl 16 . . . 4  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  ( abs `  ( sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( ( X `  ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  -  if ( S  =  0 ,  0 ,  T ) ) )  <_  (
( abs `  sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( ( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  +  ( abs `  if ( S  =  0 ,  0 ,  T ) ) ) )
27425abscld 12921 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( abs `  ( ( X `  ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  e.  RR )
2759, 274fsumrecl 13210 . . . . . . 7  |-  ( (
ph  /\  m  e.  RR+ )  ->  sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( abs `  (
( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  e.  RR )
276261, 275syl 16 . . . . . 6  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( abs `  (
( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  e.  RR )
2779, 25fsumabs 13263 . . . . . . 7  |-  ( (
ph  /\  m  e.  RR+ )  ->  ( abs ` 
sum_ k  e.  ( 1 ... ( |_
`  m ) ) ( ( X `  ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  <_  sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( abs `  (
( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) ) )
278261, 277syl 16 . . . . . 6  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  ( abs `  sum_ k  e.  ( 1 ... ( |_
`  m ) ) ( ( X `  ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  <_  sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( abs `  (
( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) ) )
279 fzfid 11794 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  RR+ )  ->  ( 1 ... 2 )  e. 
Fin )
280234adantlr 714 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  ( X `  ( L `  k ) )  e.  CC )
28117adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  m  e.  RR+ )
282239adantl 466 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  k  e.  NN )
283282nnrpd 11025 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  k  e.  RR+ )
284281, 283, 19syl2anc 661 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  if ( S  =  0 ,  m ,  k )  e.  RR+ )
285284relogcld 22071 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  ( log `  if ( S  =  0 ,  m ,  k ) )  e.  RR )
286285, 282nndivred 10369 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  (
( log `  if ( S  =  0 ,  m ,  k ) )  /  k )  e.  RR )
287286recnd 9411 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  (
( log `  if ( S  =  0 ,  m ,  k ) )  /  k )  e.  CC )
288280, 287mulcld 9405 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  (
( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  e.  CC )
289288abscld 12921 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  ( abs `  ( ( X `
 ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  e.  RR )
290279, 289fsumrecl 13210 . . . . . . . 8  |-  ( (
ph  /\  m  e.  RR+ )  ->  sum_ k  e.  ( 1 ... 2
) ( abs `  (
( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  e.  RR )
291261, 290syl 16 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  sum_ k  e.  ( 1 ... 2
) ( abs `  (
( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  e.  RR )
292 fzfid 11794 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  (
1 ... 2 )  e. 
Fin )
293261, 288sylan 471 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  (
( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  e.  CC )
294293abscld 12921 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  ( abs `  ( ( X `
 ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  e.  RR )
295293absge0d 12929 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  0  <_  ( abs `  (
( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) ) )
296252flcld 11647 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  ( |_ `  m )  e.  ZZ )
297 2z 10677 . . . . . . . . . . 11  |-  2  e.  ZZ
298297a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  2  e.  ZZ )
299250simp3bi 1005 . . . . . . . . . . . . . 14  |-  ( m  e.  ( 1 [,) 3 )  ->  m  <  3 )
300299adantl 466 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  m  <  3 )
301 3z 10678 . . . . . . . . . . . . . 14  |-  3  e.  ZZ
302 fllt 11655 . . . . . . . . . . . . . 14  |-  ( ( m  e.  RR  /\  3  e.  ZZ )  ->  ( m  <  3  <->  ( |_ `  m )  <  3 ) )
303252, 301, 302sylancl 662 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  (
m  <  3  <->  ( |_ `  m )  <  3
) )
304300, 303mpbid 210 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  ( |_ `  m )  <  3 )
305 df-3 10380 . . . . . . . . . . . 12  |-  3  =  ( 2  +  1 )
306304, 305syl6breq 4330 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  ( |_ `  m )  < 
( 2  +  1 ) )
307 rpre 10996 . . . . . . . . . . . . . . 15  |-  ( m  e.  RR+  ->  m  e.  RR )
308307adantl 466 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  RR+ )  ->  m  e.  RR )
309308flcld 11647 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  RR+ )  ->  ( |_ `  m )  e.  ZZ )
310 zleltp1 10694 . . . . . . . . . . . . 13  |-  ( ( ( |_ `  m
)  e.  ZZ  /\  2  e.  ZZ )  ->  ( ( |_ `  m )  <_  2  <->  ( |_ `  m )  <  ( 2  +  1 ) ) )
311309, 297, 310sylancl 662 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  RR+ )  ->  ( ( |_ `  m )  <_ 
2  <->  ( |_ `  m )  <  (
2  +  1 ) ) )
312261, 311syl 16 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  (
( |_ `  m
)  <_  2  <->  ( |_ `  m )  <  (
2  +  1 ) ) )
313306, 312mpbird 232 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  ( |_ `  m )  <_ 
2 )
314 eluz2 10866 . . . . . . . . . 10  |-  ( 2  e.  ( ZZ>= `  ( |_ `  m ) )  <-> 
( ( |_ `  m )  e.  ZZ  /\  2  e.  ZZ  /\  ( |_ `  m )  <_  2 ) )
315296, 298, 313, 314syl3anbrc 1172 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  2  e.  ( ZZ>= `  ( |_ `  m ) ) )
316 fzss2 11497 . . . . . . . . 9  |-  ( 2  e.  ( ZZ>= `  ( |_ `  m ) )  ->  ( 1 ... ( |_ `  m
) )  C_  (
1 ... 2 ) )
317315, 316syl 16 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  (
1 ... ( |_ `  m ) )  C_  ( 1 ... 2
) )
318292, 294, 295, 317fsumless 13258 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( abs `  (
( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  <_  sum_ k  e.  ( 1 ... 2
) ( abs `  (
( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) ) )
319243adantlr 714 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  (
( abs `  ( X `  ( L `  k ) ) )  x.  ( ( log `  3 )  / 
k ) )  e.  RR )
320280, 287absmuld 12939 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  ( abs `  ( ( X `
 ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  =  ( ( abs `  ( X `  ( L `  k ) ) )  x.  ( abs `  (
( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) ) )
321261, 320sylan 471 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  ( abs `  ( ( X `
 ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  =  ( ( abs `  ( X `  ( L `  k ) ) )  x.  ( abs `  (
( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) ) )
322261, 286sylan 471 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  (
( log `  if ( S  =  0 ,  m ,  k ) )  /  k )  e.  RR )
323261, 285sylan 471 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  ( log `  if ( S  =  0 ,  m ,  k ) )  e.  RR )
324 log1 22033 . . . . . . . . . . . . . 14  |-  ( log `  1 )  =  0
325 elfzle1 11453 . . . . . . . . . . . . . . . 16  |-  ( k  e.  ( 1 ... 2 )  ->  1  <_  k )
326 breq2 4295 . . . . . . . . . . . . . . . . 17  |-  ( m  =  if ( S  =  0 ,  m ,  k )  -> 
( 1  <_  m  <->  1  <_  if ( S  =  0 ,  m ,  k ) ) )
327 breq2 4295 . . . . . . . . . . . . . . . . 17  |-  ( k  =  if ( S  =  0 ,  m ,  k )  -> 
( 1  <_  k  <->  1  <_  if ( S  =  0 ,  m ,  k ) ) )
328326, 327ifboth 3824 . . . . . . . . . . . . . . . 16  |-  ( ( 1  <_  m  /\  1  <_  k )  -> 
1  <_  if ( S  =  0 ,  m ,  k )
)
329258, 325, 328syl2an 477 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  1  <_  if ( S  =  0 ,  m ,  k ) )
330 1rp 10994 . . . . . . . . . . . . . . . . 17  |-  1  e.  RR+
331 logleb 22051 . . . . . . . . . . . . . . . . 17  |-  ( ( 1  e.  RR+  /\  if ( S  =  0 ,  m ,  k )  e.  RR+ )  ->  (
1  <_  if ( S  =  0 ,  m ,  k )  <->  ( log `  1 )  <_  ( log `  if ( S  =  0 ,  m ,  k ) ) ) )
332330, 284, 331sylancr 663 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  (
1  <_  if ( S  =  0 ,  m ,  k )  <->  ( log `  1 )  <_  ( log `  if ( S  =  0 ,  m ,  k ) ) ) )
333261, 332sylan 471 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  (
1  <_  if ( S  =  0 ,  m ,  k )  <->  ( log `  1 )  <_  ( log `  if ( S  =  0 ,  m ,  k ) ) ) )
334329, 333mpbid 210 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  ( log `  1 )  <_ 
( log `  if ( S  =  0 ,  m ,  k ) ) )
335324, 334syl5eqbrr 4325 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  0  <_  ( log `  if ( S  =  0 ,  m ,  k ) ) )
336283rpregt0d 11032 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  (
k  e.  RR  /\  0  <  k ) )
337261, 336sylan 471 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  (
k  e.  RR  /\  0  <  k ) )
338 divge0 10197 . . . . . . . . . . . . 13  |-  ( ( ( ( log `  if ( S  =  0 ,  m ,  k ) )  e.  RR  /\  0  <_  ( log `  if ( S  =  0 ,  m ,  k ) ) )  /\  (
k  e.  RR  /\  0  <  k ) )  ->  0  <_  (
( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )
339323, 335, 337, 338syl21anc 1217 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  0  <_  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )
340322, 339absidd 12908 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  ( abs `  ( ( log `  if ( S  =  0 ,  m ,  k ) )  / 
k ) )  =  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )
341340, 322eqeltrd 2516 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  ( abs `  ( ( log `  if ( S  =  0 ,  m ,  k ) )  / 
k ) )  e.  RR )
342242adantlr 714 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  (
( log `  3
)  /  k )  e.  RR )
343235adantlr 714 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  ( abs `  ( X `  ( L `  k ) ) )  e.  RR )
344280absge0d 12929 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  0  <_  ( abs `  ( X `  ( L `  k ) ) ) )
345343, 344jca 532 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  (
( abs `  ( X `  ( L `  k ) ) )  e.  RR  /\  0  <_  ( abs `  ( X `  ( L `  k ) ) ) ) )
346261, 345sylan 471 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  (
( abs `  ( X `  ( L `  k ) ) )  e.  RR  /\  0  <_  ( abs `  ( X `  ( L `  k ) ) ) ) )
347299ad2antlr 726 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  m  <  3 )
348282nnred 10336 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  k  e.  RR )
349 2re 10390 . . . . . . . . . . . . . . . . . 18  |-  2  e.  RR
350349a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  2  e.  RR )
35165a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  3  e.  RR )
352 elfzle2 11454 . . . . . . . . . . . . . . . . . 18  |-  ( k  e.  ( 1 ... 2 )  ->  k  <_  2 )
353352adantl 466 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  k  <_  2 )
354 2lt3 10488 . . . . . . . . . . . . . . . . . 18  |-  2  <  3
355354a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  2  <  3 )
356348, 350, 351, 353, 355lelttrd 9528 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  k  <  3 )
357261, 356sylan 471 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  k  <  3 )
358 breq1 4294 . . . . . . . . . . . . . . . 16  |-  ( m  =  if ( S  =  0 ,  m ,  k )  -> 
( m  <  3  <->  if ( S  =  0 ,  m ,  k )  <  3 ) )
359 breq1 4294 . . . . . . . . . . . . . . . 16  |-  ( k  =  if ( S  =  0 ,  m ,  k )  -> 
( k  <  3  <->  if ( S  =  0 ,  m ,  k )  <  3 ) )
360358, 359ifboth 3824 . . . . . . . . . . . . . . 15  |-  ( ( m  <  3  /\  k  <  3 )  ->  if ( S  =  0 ,  m ,  k )  <  3 )
361347, 357, 360syl2anc 661 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  if ( S  =  0 ,  m ,  k )  <  3 )
362284rpred 11026 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  if ( S  =  0 ,  m ,  k )  e.  RR )
363 ltle 9462 . . . . . . . . . . . . . . . 16  |-  ( ( if ( S  =  0 ,  m ,  k )  e.  RR  /\  3  e.  RR )  ->  ( if ( S  =  0 ,  m ,  k )  <  3  ->  if ( S  =  0 ,  m ,  k )  <_  3 ) )
364362, 65, 363sylancl 662 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  ( if ( S  =  0 ,  m ,  k )  <  3  ->  if ( S  =  0 ,  m ,  k )  <_  3 ) )
365261, 364sylan 471 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  ( if ( S  =  0 ,  m ,  k )  <  3  ->  if ( S  =  0 ,  m ,  k )  <_  3 ) )
366361, 365mpd 15 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  if ( S  =  0 ,  m ,  k )  <_  3 )
367 logleb 22051 . . . . . . . . . . . . . . 15  |-  ( ( if ( S  =  0 ,  m ,  k )  e.  RR+  /\  3  e.  RR+ )  ->  ( if ( S  =  0 ,  m ,  k )  <_ 
3  <->  ( log `  if ( S  =  0 ,  m ,  k ) )  <_  ( log `  3 ) ) )
368284, 236, 367sylancl 662 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  ( if ( S  =  0 ,  m ,  k )  <_  3  <->  ( log `  if ( S  =  0 ,  m ,  k ) )  <_ 
( log `  3
) ) )
369261, 368sylan 471 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  ( if ( S  =  0 ,  m ,  k )  <_  3  <->  ( log `  if ( S  =  0 ,  m ,  k ) )  <_ 
( log `  3
) ) )
370366, 369mpbid 210 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  ( log `  if ( S  =  0 ,  m ,  k ) )  <_  ( log `  3
) )
371238a1i 11 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  ( log `  3 )  e.  RR )
372285, 371, 283lediv1d 11068 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  (
( log `  if ( S  =  0 ,  m ,  k ) )  <_  ( log `  3 )  <->  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k )  <_ 
( ( log `  3
)  /  k ) ) )
373261, 372sylan 471 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  (
( log `  if ( S  =  0 ,  m ,  k ) )  <_  ( log `  3 )  <->  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k )  <_ 
( ( log `  3
)  /  k ) ) )
374370, 373mpbid 210 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  (
( log `  if ( S  =  0 ,  m ,  k ) )  /  k )  <_  ( ( log `  3 )  / 
k ) )
375340, 374eqbrtrd 4311 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  ( abs `  ( ( log `  if ( S  =  0 ,  m ,  k ) )  / 
k ) )  <_ 
( ( log `  3
)  /  k ) )
376 lemul2a 10183 . . . . . . . . . 10  |-  ( ( ( ( abs `  (
( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  e.  RR  /\  ( ( log `  3
)  /  k )  e.  RR  /\  (
( abs `  ( X `  ( L `  k ) ) )  e.  RR  /\  0  <_  ( abs `  ( X `  ( L `  k ) ) ) ) )  /\  ( abs `  ( ( log `  if ( S  =  0 ,  m ,  k ) )  / 
k ) )  <_ 
( ( log `  3
)  /  k ) )  ->  ( ( abs `  ( X `  ( L `  k ) ) )  x.  ( abs `  ( ( log `  if ( S  =  0 ,  m ,  k ) )  / 
k ) ) )  <_  ( ( abs `  ( X `  ( L `  k )
) )  x.  (
( log `  3
)  /  k ) ) )
377341, 342, 346, 375, 376syl31anc 1221 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  (
( abs `  ( X `  ( L `  k ) ) )  x.  ( abs `  (
( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  <_  (
( abs `  ( X `  ( L `  k ) ) )  x.  ( ( log `  3 )  / 
k ) ) )
378321, 377eqbrtrd 4311 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  ( abs `  ( ( X `
 ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  <_  (
( abs `  ( X `  ( L `  k ) ) )  x.  ( ( log `  3 )  / 
k ) ) )
379292, 294, 319, 378fsumle 13261 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  sum_ k  e.  ( 1 ... 2
) ( abs `  (
( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  <_  sum_ k  e.  ( 1 ... 2
) ( ( abs `  ( X `  ( L `  k )
) )  x.  (
( log `  3
)  /  k ) ) )
380276, 291, 270, 318, 379letrd 9527 . . . . . 6  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( abs `  (
( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  <_  sum_ k  e.  ( 1 ... 2
) ( ( abs `  ( X `  ( L `  k )
) )  x.  (
( log `  3
)  /  k ) ) )
381267, 276, 270, 278, 380letrd 9527 . . . . 5  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  ( abs `  sum_ k  e.  ( 1 ... ( |_
`  m ) ) ( ( X `  ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  <_  sum_ k  e.  ( 1 ... 2
) ( ( abs `  ( X `  ( L `  k )
) )  x.  (
( log `  3
)  /  k ) ) )
38226abscld 12921 . . . . . . 7  |-  ( (
ph  /\  m  e.  RR+ )  ->  ( abs ` 
sum_ k  e.  ( 1 ... ( |_
`  m ) ) ( ( X `  ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  e.  RR )
383244adantr 465 . . . . . . 7  |-  ( (
ph  /\  m  e.  RR+ )  ->  sum_ k  e.  ( 1 ... 2
) ( ( abs `  ( X `  ( L `  k )
) )  x.  (
( log `  3
)  /  k ) )  e.  RR )
384262abscld 12921 . . . . . . 7  |-  ( (
ph  /\  m  e.  RR+ )  ->  ( abs `  if ( S  =  0 ,  0 ,  T ) )  e.  RR )
385382, 383, 384leadd1d 9932 . . . . . 6  |-  ( (
ph  /\  m  e.  RR+ )  ->  ( ( abs `  sum_ k  e.  ( 1 ... ( |_
`  m ) ) ( ( X `  ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  <_  sum_ k  e.  ( 1 ... 2
) ( ( abs `  ( X `  ( L `  k )
) )  x.  (
( log `  3
)  /  k ) )  <->  ( ( abs `  sum_ k  e.  ( 1 ... ( |_
`  m ) ) ( ( X `  ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  +  ( abs `  if ( S  =  0 ,  0 ,  T ) ) )  <_  ( sum_ k  e.  ( 1 ... 2 ) ( ( abs `  ( X `  ( L `  k ) ) )  x.  ( ( log `  3 )  / 
k ) )  +  ( abs `  if ( S  =  0 ,  0 ,  T
) ) ) ) )
386261, 385syl 16 . . . . 5  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  (
( abs `  sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( ( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  <_  sum_ k  e.  ( 1 ... 2
) ( ( abs `  ( X `  ( L `  k )
) )  x.  (
( log `  3
)  /  k ) )  <->  ( ( abs `  sum_ k  e.  ( 1 ... ( |_
`  m ) ) ( ( X `  ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  +  ( abs `  if ( S  =  0 ,  0 ,  T ) ) )  <_  ( sum_ k  e.  ( 1 ... 2 ) ( ( abs `  ( X `  ( L `  k ) ) )  x.  ( ( log `  3 )  / 
k ) )  +  ( abs `  if ( S  =  0 ,  0 ,  T
) ) ) ) )
387381, 386mpbid 210 . . . 4  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  (
( abs `  sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( ( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  +  ( abs `  if ( S  =  0 ,  0 ,  T ) ) )  <_  ( sum_ k  e.  ( 1 ... 2 ) ( ( abs `  ( X `  ( L `  k ) ) )  x.  ( ( log `  3 )  / 
k ) )  +  ( abs `  if ( S  =  0 ,  0 ,  T
) ) ) )
388265, 269, 271, 273, 387letrd 9527 . . 3  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  ( abs