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

Theorem dchrvmasumiflem1 23884
Description: Lemma for dchrvmasumif 23886. (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 12065 . . 3  |-  ( (
ph  /\  m  e.  RR+ )  ->  ( 1 ... ( |_ `  m ) )  e. 
Fin )
10 simpl 455 . . . . 5  |-  ( (
ph  /\  m  e.  RR+ )  ->  ph )
11 elfznn 11717 . . . . 5  |-  ( k  e.  ( 1 ... ( |_ `  m
) )  ->  k  e.  NN )
127adantr 463 . . . . . 6  |-  ( (
ph  /\  k  e.  NN )  ->  X  e.  D )
13 nnz 10882 . . . . . . 7  |-  ( k  e.  NN  ->  k  e.  ZZ )
1413adantl 464 . . . . . 6  |-  ( (
ph  /\  k  e.  NN )  ->  k  e.  ZZ )
154, 1, 5, 2, 12, 14dchrzrhcl 23718 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  ( X `
 ( L `  k ) )  e.  CC )
1610, 11, 15syl2an 475 . . . 4  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( X `  ( L `  k
) )  e.  CC )
17 simpr 459 . . . . . . . 8  |-  ( (
ph  /\  m  e.  RR+ )  ->  m  e.  RR+ )
1811nnrpd 11257 . . . . . . . 8  |-  ( k  e.  ( 1 ... ( |_ `  m
) )  ->  k  e.  RR+ )
19 ifcl 3971 . . . . . . . 8  |-  ( ( m  e.  RR+  /\  k  e.  RR+ )  ->  if ( S  =  0 ,  m ,  k )  e.  RR+ )
2017, 18, 19syl2an 475 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  if ( S  =  0 ,  m ,  k )  e.  RR+ )
2120relogcld 23176 . . . . . 6  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( log `  if ( S  =  0 ,  m ,  k ) )  e.  RR )
2211adantl 464 . . . . . 6  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  k  e.  NN )
2321, 22nndivred 10580 . . . . 5  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k )  e.  RR )
2423recnd 9611 . . . 4  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k )  e.  CC )
2516, 24mulcld 9605 . . 3  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( ( X `  ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  e.  CC )
269, 25fsumcl 13637 . 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 5848 . . . 4  |-  ( m  =  ( x  / 
d )  ->  ( |_ `  m )  =  ( |_ `  (
x  /  d ) ) )
2827oveq2d 6286 . . 3  |-  ( m  =  ( x  / 
d )  ->  (
1 ... ( |_ `  m ) )  =  ( 1 ... ( |_ `  ( x  / 
d ) ) ) )
29 ifeq1 3933 . . . . . . 7  |-  ( m  =  ( x  / 
d )  ->  if ( S  =  0 ,  m ,  k )  =  if ( S  =  0 ,  ( x  /  d ) ,  k ) )
3029fveq2d 5852 . . . . . 6  |-  ( m  =  ( x  / 
d )  ->  ( log `  if ( S  =  0 ,  m ,  k ) )  =  ( log `  if ( S  =  0 ,  ( x  / 
d ) ,  k ) ) )
3130oveq1d 6285 . . . . 5  |-  ( m  =  ( x  / 
d )  ->  (
( log `  if ( S  =  0 ,  m ,  k ) )  /  k )  =  ( ( log `  if ( S  =  0 ,  ( x  /  d ) ,  k ) )  / 
k ) )
3231oveq2d 6286 . . . 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 463 . . 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 13611 . 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 . . 3  |-  ( ph  ->  C  e.  ( 0 [,) +oo ) )
36 dchrvmasumif.e . . 3  |-  ( ph  ->  E  e.  ( 0 [,) +oo ) )
3735, 36ifcld 3972 . 2  |-  ( ph  ->  if ( S  =  0 ,  C ,  E )  e.  ( 0 [,) +oo )
)
38 0cn 9577 . . 3  |-  0  e.  CC
39 dchrvmasumif.t . . . 4  |-  ( ph  ->  seq 1 (  +  ,  K )  ~~>  T )
40 climcl 13404 . . . 4  |-  (  seq 1 (  +  ,  K )  ~~>  T  ->  T  e.  CC )
4139, 40syl 16 . . 3  |-  ( ph  ->  T  e.  CC )
42 ifcl 3971 . . 3  |-  ( ( 0  e.  CC  /\  T  e.  CC )  ->  if ( S  =  0 ,  0 ,  T )  e.  CC )
4338, 41, 42sylancr 661 . 2  |-  ( ph  ->  if ( S  =  0 ,  0 ,  T )  e.  CC )
44 nnuz 11117 . . . . . . . . 9  |-  NN  =  ( ZZ>= `  1 )
45 1zzd 10891 . . . . . . . . 9  |-  ( ph  ->  1  e.  ZZ )
46 nncn 10539 . . . . . . . . . . . . 13  |-  ( k  e.  NN  ->  k  e.  CC )
4746adantl 464 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN )  ->  k  e.  CC )
48 nnne0 10564 . . . . . . . . . . . . 13  |-  ( k  e.  NN  ->  k  =/=  0 )
4948adantl 464 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN )  ->  k  =/=  0 )
5015, 47, 49divcld 10316 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( X `  ( L `
 k ) )  /  k )  e.  CC )
51 dchrvmasumif.f . . . . . . . . . . . 12  |-  F  =  ( a  e.  NN  |->  ( ( X `  ( L `  a ) )  /  a ) )
52 fveq2 5848 . . . . . . . . . . . . . . 15  |-  ( a  =  k  ->  ( L `  a )  =  ( L `  k ) )
5352fveq2d 5852 . . . . . . . . . . . . . 14  |-  ( a  =  k  ->  ( X `  ( L `  a ) )  =  ( X `  ( L `  k )
) )
54 id 22 . . . . . . . . . . . . . 14  |-  ( a  =  k  ->  a  =  k )
5553, 54oveq12d 6288 . . . . . . . . . . . . 13  |-  ( a  =  k  ->  (
( X `  ( L `  a )
)  /  a )  =  ( ( X `
 ( L `  k ) )  / 
k ) )
5655cbvmptv 4530 . . . . . . . . . . . 12  |-  ( a  e.  NN  |->  ( ( X `  ( L `
 a ) )  /  a ) )  =  ( k  e.  NN  |->  ( ( X `
 ( L `  k ) )  / 
k ) )
5751, 56eqtri 2483 . . . . . . . . . . 11  |-  F  =  ( k  e.  NN  |->  ( ( X `  ( L `  k ) )  /  k ) )
5850, 57fmptd 6031 . . . . . . . . . 10  |-  ( ph  ->  F : NN --> CC )
59 ffvelrn 6005 . . . . . . . . . 10  |-  ( ( F : NN --> CC  /\  k  e.  NN )  ->  ( F `  k
)  e.  CC )
6058, 59sylan 469 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  NN )  ->  ( F `
 k )  e.  CC )
6144, 45, 60serf 12117 . . . . . . . 8  |-  ( ph  ->  seq 1 (  +  ,  F ) : NN --> CC )
6261ad2antrr 723 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =  0 )  ->  seq 1 (  +  ,  F ) : NN --> CC )
63 3re 10605 . . . . . . . . . . 11  |-  3  e.  RR
64 elicopnf 11623 . . . . . . . . . . 11  |-  ( 3  e.  RR  ->  (
m  e.  ( 3 [,) +oo )  <->  ( m  e.  RR  /\  3  <_  m ) ) )
6563, 64mp1i 12 . . . . . . . . . 10  |-  ( ph  ->  ( m  e.  ( 3 [,) +oo )  <->  ( m  e.  RR  /\  3  <_  m ) ) )
6665simprbda 621 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  m  e.  RR )
67 1red 9600 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  1  e.  RR )
6863a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  3  e.  RR )
69 1le3 10748 . . . . . . . . . . 11  |-  1  <_  3
7069a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  1  <_  3 )
7165simplbda 622 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  3  <_  m )
7267, 68, 66, 70, 71letrd 9728 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  1  <_  m )
73 flge1nn 11937 . . . . . . . . 9  |-  ( ( m  e.  RR  /\  1  <_  m )  -> 
( |_ `  m
)  e.  NN )
7466, 72, 73syl2anc 659 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  ( |_ `  m )  e.  NN )
7574adantr 463 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =  0 )  -> 
( |_ `  m
)  e.  NN )
7662, 75ffvelrnd 6008 . . . . . 6  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =  0 )  -> 
(  seq 1 (  +  ,  F ) `  ( |_ `  m ) )  e.  CC )
7776abscld 13349 . . . . 5  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =  0 )  -> 
( abs `  (  seq 1 (  +  ,  F ) `  ( |_ `  m ) ) )  e.  RR )
78 simpl 455 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  ph )
79 0red 9586 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  0  e.  RR )
80 3pos 10625 . . . . . . . . . . 11  |-  0  <  3
8180a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  0  <  3 )
8279, 68, 66, 81, 71ltletrd 9731 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  0  <  m )
8366, 82elrpd 11256 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  m  e.  RR+ )
8478, 83jca 530 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  ( ph  /\  m  e.  RR+ ) )
85 elrege0 11630 . . . . . . . . . 10  |-  ( C  e.  ( 0 [,) +oo )  <->  ( C  e.  RR  /\  0  <_  C ) )
8685simplbi 458 . . . . . . . . 9  |-  ( C  e.  ( 0 [,) +oo )  ->  C  e.  RR )
8735, 86syl 16 . . . . . . . 8  |-  ( ph  ->  C  e.  RR )
88 rerpdivcl 11249 . . . . . . . 8  |-  ( ( C  e.  RR  /\  m  e.  RR+ )  -> 
( C  /  m
)  e.  RR )
8987, 88sylan 469 . . . . . . 7  |-  ( (
ph  /\  m  e.  RR+ )  ->  ( C  /  m )  e.  RR )
9084, 89syl 16 . . . . . 6  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  ( C  /  m )  e.  RR )
9190adantr 463 . . . . 5  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =  0 )  -> 
( C  /  m
)  e.  RR )
9283relogcld 23176 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  ( log `  m )  e.  RR )
9366, 72logge0d 23183 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  0  <_  ( log `  m
) )
9492, 93jca 530 . . . . . 6  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  (
( log `  m
)  e.  RR  /\  0  <_  ( log `  m
) ) )
9594adantr 463 . . . . 5  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =  0 )  -> 
( ( log `  m
)  e.  RR  /\  0  <_  ( log `  m
) ) )
96 oveq2 6278 . . . . . . . 8  |-  ( S  =  0  ->  (
(  seq 1 (  +  ,  F ) `  ( |_ `  m ) )  -  S )  =  ( (  seq 1 (  +  ,  F ) `  ( |_ `  m ) )  -  0 ) )
9761adantr 463 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  seq 1 (  +  ,  F ) : NN --> CC )
9897, 74ffvelrnd 6008 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  (  seq 1 (  +  ,  F ) `  ( |_ `  m ) )  e.  CC )
9998subid1d 9911 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  (
(  seq 1 (  +  ,  F ) `  ( |_ `  m ) )  -  0 )  =  (  seq 1
(  +  ,  F
) `  ( |_ `  m ) ) )
10096, 99sylan9eqr 2517 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =  0 )  -> 
( (  seq 1
(  +  ,  F
) `  ( |_ `  m ) )  -  S )  =  (  seq 1 (  +  ,  F ) `  ( |_ `  m ) ) )
101100fveq2d 5852 . . . . . 6  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =  0 )  -> 
( abs `  (
(  seq 1 (  +  ,  F ) `  ( |_ `  m ) )  -  S ) )  =  ( abs `  (  seq 1
(  +  ,  F
) `  ( |_ `  m ) ) ) )
102 1re 9584 . . . . . . . . . 10  |-  1  e.  RR
103 elicopnf 11623 . . . . . . . . . 10  |-  ( 1  e.  RR  ->  (
m  e.  ( 1 [,) +oo )  <->  ( m  e.  RR  /\  1  <_  m ) ) )
104102, 103ax-mp 5 . . . . . . . . 9  |-  ( m  e.  ( 1 [,) +oo )  <->  ( m  e.  RR  /\  1  <_  m ) )
10566, 72, 104sylanbrc 662 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  m  e.  ( 1 [,) +oo ) )
106 dchrvmasumif.1 . . . . . . . . 9  |-  ( ph  ->  A. y  e.  ( 1 [,) +oo )
( abs `  (
(  seq 1 (  +  ,  F ) `  ( |_ `  y ) )  -  S ) )  <_  ( C  /  y ) )
107106adantr 463 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  A. y  e.  ( 1 [,) +oo ) ( abs `  (
(  seq 1 (  +  ,  F ) `  ( |_ `  y ) )  -  S ) )  <_  ( C  /  y ) )
108 fveq2 5848 . . . . . . . . . . . . 13  |-  ( y  =  m  ->  ( |_ `  y )  =  ( |_ `  m
) )
109108fveq2d 5852 . . . . . . . . . . . 12  |-  ( y  =  m  ->  (  seq 1 (  +  ,  F ) `  ( |_ `  y ) )  =  (  seq 1
(  +  ,  F
) `  ( |_ `  m ) ) )
110109oveq1d 6285 . . . . . . . . . . 11  |-  ( y  =  m  ->  (
(  seq 1 (  +  ,  F ) `  ( |_ `  y ) )  -  S )  =  ( (  seq 1 (  +  ,  F ) `  ( |_ `  m ) )  -  S ) )
111110fveq2d 5852 . . . . . . . . . 10  |-  ( y  =  m  ->  ( abs `  ( (  seq 1 (  +  ,  F ) `  ( |_ `  y ) )  -  S ) )  =  ( abs `  (
(  seq 1 (  +  ,  F ) `  ( |_ `  m ) )  -  S ) ) )
112 oveq2 6278 . . . . . . . . . 10  |-  ( y  =  m  ->  ( C  /  y )  =  ( C  /  m
) )
113111, 112breq12d 4452 . . . . . . . . 9  |-  ( y  =  m  ->  (
( abs `  (
(  seq 1 (  +  ,  F ) `  ( |_ `  y ) )  -  S ) )  <_  ( C  /  y )  <->  ( abs `  ( (  seq 1
(  +  ,  F
) `  ( |_ `  m ) )  -  S ) )  <_ 
( C  /  m
) ) )
114113rspcv 3203 . . . . . . . 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 ) ) )
115105, 107, 114sylc 60 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  ( abs `  ( (  seq 1 (  +  ,  F ) `  ( |_ `  m ) )  -  S ) )  <_  ( C  /  m ) )
116115adantr 463 . . . . . 6  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =  0 )  -> 
( abs `  (
(  seq 1 (  +  ,  F ) `  ( |_ `  m ) )  -  S ) )  <_  ( C  /  m ) )
117101, 116eqbrtrrd 4461 . . . . 5  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =  0 )  -> 
( abs `  (  seq 1 (  +  ,  F ) `  ( |_ `  m ) ) )  <_  ( C  /  m ) )
118 lemul2a 10393 . . . . 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
) ) )
11977, 91, 95, 117, 118syl31anc 1229 . . . 4  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =  0 )  -> 
( ( log `  m
)  x.  ( abs `  (  seq 1
(  +  ,  F
) `  ( |_ `  m ) ) ) )  <_  ( ( log `  m )  x.  ( C  /  m
) ) )
120 iftrue 3935 . . . . . . . . . . . . . . 15  |-  ( S  =  0  ->  if ( S  =  0 ,  m ,  k )  =  m )
121120fveq2d 5852 . . . . . . . . . . . . . 14  |-  ( S  =  0  ->  ( log `  if ( S  =  0 ,  m ,  k ) )  =  ( log `  m
) )
122121oveq1d 6285 . . . . . . . . . . . . 13  |-  ( S  =  0  ->  (
( log `  if ( S  =  0 ,  m ,  k ) )  /  k )  =  ( ( log `  m )  /  k
) )
123122ad2antlr 724 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  /\  k  e.  ( 1 ... ( |_
`  m ) ) )  ->  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k )  =  ( ( log `  m
)  /  k ) )
124123oveq2d 6286 . . . . . . . . . . 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
) ) )
12516adantlr 712 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  /\  k  e.  ( 1 ... ( |_
`  m ) ) )  ->  ( X `  ( L `  k
) )  e.  CC )
126 relogcl 23129 . . . . . . . . . . . . . . 15  |-  ( m  e.  RR+  ->  ( log `  m )  e.  RR )
127126adantl 464 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  RR+ )  ->  ( log `  m )  e.  RR )
128127recnd 9611 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  RR+ )  ->  ( log `  m )  e.  CC )
129128ad2antrr 723 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  /\  k  e.  ( 1 ... ( |_
`  m ) ) )  ->  ( log `  m )  e.  CC )
13011adantl 464 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  /\  k  e.  ( 1 ... ( |_
`  m ) ) )  ->  k  e.  NN )
131130nncnd 10547 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  /\  k  e.  ( 1 ... ( |_
`  m ) ) )  ->  k  e.  CC )
132130nnne0d 10576 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  /\  k  e.  ( 1 ... ( |_
`  m ) ) )  ->  k  =/=  0 )
133125, 129, 131, 132div12d 10352 . . . . . . . . . . 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 ) ) )
134124, 133eqtrd 2495 . . . . . . . . . 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 ) ) )
135134sumeq2dv 13607 . . . . . . . . 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 ) ) )
136 iftrue 3935 . . . . . . . . . . 11  |-  ( S  =  0  ->  if ( S  =  0 ,  0 ,  T
)  =  0 )
137136oveq2d 6286 . . . . . . . . . 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 ) )
13826subid1d 9911 . . . . . . . . . 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 ) ) )
139137, 138sylan9eqr 2517 . . . . . . . . 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 ) ) )
140 ovex 6298 . . . . . . . . . . . . . 14  |-  ( ( X `  ( L `
 k ) )  /  k )  e. 
_V
14155, 51, 140fvmpt 5931 . . . . . . . . . . . . 13  |-  ( k  e.  NN  ->  ( F `  k )  =  ( ( X `
 ( L `  k ) )  / 
k ) )
14222, 141syl 16 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( F `  k )  =  ( ( X `  ( L `  k )
)  /  k ) )
14358adantr 463 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  RR+ )  ->  F : NN
--> CC )
144143, 11, 59syl2an 475 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( F `  k )  e.  CC )
145142, 144eqeltrrd 2543 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( ( X `  ( L `  k ) )  / 
k )  e.  CC )
1469, 128, 145fsummulc2 13681 . . . . . . . . . 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 ) ) )
147146adantr 463 . . . . . . . . 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 ) ) )
148135, 139, 1473eqtr4d 2505 . . . . . . . 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 ) ) )
14984, 148sylan 469 . . . . . . 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 ) ) )
15084, 142sylan 469 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( F `  k )  =  ( ( X `  ( L `  k )
)  /  k ) )
15174, 44syl6eleq 2552 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  ( |_ `  m )  e.  ( ZZ>= `  1 )
)
15278, 11, 50syl2an 475 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( ( X `  ( L `  k ) )  / 
k )  e.  CC )
153150, 151, 152fsumser 13634 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( ( X `  ( L `  k ) )  /  k )  =  (  seq 1
(  +  ,  F
) `  ( |_ `  m ) ) )
154153adantr 463 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =  0 )  ->  sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( ( X `  ( L `  k )
)  /  k )  =  (  seq 1
(  +  ,  F
) `  ( |_ `  m ) ) )
155154oveq2d 6286 . . . . . . 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 ) ) ) )
156149, 155eqtrd 2495 . . . . . 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 ) ) ) )
157156fveq2d 5852 . . . . 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 ) ) ) ) )
158126ad2antlr 724 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  -> 
( log `  m
)  e.  RR )
159158recnd 9611 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  -> 
( log `  m
)  e.  CC )
16084, 159sylan 469 . . . . . 6  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =  0 )  -> 
( log `  m
)  e.  CC )
161160, 76absmuld 13367 . . . . 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 ) ) ) ) )
16292, 93absidd 13336 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  ( abs `  ( log `  m
) )  =  ( log `  m ) )
163162oveq1d 6285 . . . . . 6  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  (
( abs `  ( log `  m ) )  x.  ( abs `  (  seq 1 (  +  ,  F ) `  ( |_ `  m ) ) ) )  =  ( ( log `  m
)  x.  ( abs `  (  seq 1
(  +  ,  F
) `  ( |_ `  m ) ) ) ) )
164163adantr 463 . . . . 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 ) ) ) ) )
165157, 161, 1643eqtrd 2499 . . . 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 ) ) ) ) )
166 iftrue 3935 . . . . . . . 8  |-  ( S  =  0  ->  if ( S  =  0 ,  C ,  E )  =  C )
167166adantl 464 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  ->  if ( S  =  0 ,  C ,  E
)  =  C )
168167oveq1d 6285 . . . . . 6  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  -> 
( if ( S  =  0 ,  C ,  E )  x.  (
( log `  m
)  /  m ) )  =  ( C  x.  ( ( log `  m )  /  m
) ) )
16987recnd 9611 . . . . . . . 8  |-  ( ph  ->  C  e.  CC )
170169ad2antrr 723 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  ->  C  e.  CC )
171 rpcnne0 11238 . . . . . . . 8  |-  ( m  e.  RR+  ->  ( m  e.  CC  /\  m  =/=  0 ) )
172171ad2antlr 724 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  -> 
( m  e.  CC  /\  m  =/=  0 ) )
173 div12 10225 . . . . . . 7  |-  ( ( C  e.  CC  /\  ( log `  m )  e.  CC  /\  (
m  e.  CC  /\  m  =/=  0 ) )  ->  ( C  x.  ( ( log `  m
)  /  m ) )  =  ( ( log `  m )  x.  ( C  /  m ) ) )
174170, 159, 172, 173syl3anc 1226 . . . . . 6  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  -> 
( C  x.  (
( log `  m
)  /  m ) )  =  ( ( log `  m )  x.  ( C  /  m ) ) )
175168, 174eqtrd 2495 . . . . 5  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  -> 
( if ( S  =  0 ,  C ,  E )  x.  (
( log `  m
)  /  m ) )  =  ( ( log `  m )  x.  ( C  /  m ) ) )
17684, 175sylan 469 . . . 4  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =  0 )  -> 
( if ( S  =  0 ,  C ,  E )  x.  (
( log `  m
)  /  m ) )  =  ( ( log `  m )  x.  ( C  /  m ) ) )
177119, 165, 1763brtr4d 4469 . . 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 ) ) )
178 dchrvmasumif.2 . . . . . 6  |-  ( ph  ->  A. y  e.  ( 3 [,) +oo )
( abs `  (
(  seq 1 (  +  ,  K ) `  ( |_ `  y ) )  -  T ) )  <_  ( E  x.  ( ( log `  y
)  /  y ) ) )
179108fveq2d 5852 . . . . . . . . . 10  |-  ( y  =  m  ->  (  seq 1 (  +  ,  K ) `  ( |_ `  y ) )  =  (  seq 1
(  +  ,  K
) `  ( |_ `  m ) ) )
180179oveq1d 6285 . . . . . . . . 9  |-  ( y  =  m  ->  (
(  seq 1 (  +  ,  K ) `  ( |_ `  y ) )  -  T )  =  ( (  seq 1 (  +  ,  K ) `  ( |_ `  m ) )  -  T ) )
181180fveq2d 5852 . . . . . . . 8  |-  ( y  =  m  ->  ( abs `  ( (  seq 1 (  +  ,  K ) `  ( |_ `  y ) )  -  T ) )  =  ( abs `  (
(  seq 1 (  +  ,  K ) `  ( |_ `  m ) )  -  T ) ) )
182 fveq2 5848 . . . . . . . . . 10  |-  ( y  =  m  ->  ( log `  y )  =  ( log `  m
) )
183 id 22 . . . . . . . . . 10  |-  ( y  =  m  ->  y  =  m )
184182, 183oveq12d 6288 . . . . . . . . 9  |-  ( y  =  m  ->  (
( log `  y
)  /  y )  =  ( ( log `  m )  /  m
) )
185184oveq2d 6286 . . . . . . . 8  |-  ( y  =  m  ->  ( E  x.  ( ( log `  y )  / 
y ) )  =  ( E  x.  (
( log `  m
)  /  m ) ) )
186181, 185breq12d 4452 . . . . . . 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 ) ) ) )
187186rspccva 3206 . . . . . 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 ) ) )
188178, 187sylan 469 . . . . 5  |-  ( (
ph  /\  m  e.  ( 3 [,) +oo ) )  ->  ( abs `  ( (  seq 1 (  +  ,  K ) `  ( |_ `  m ) )  -  T ) )  <_  ( E  x.  ( ( log `  m
)  /  m ) ) )
189188adantr 463 . . . 4  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =/=  0 )  ->  ( abs `  ( (  seq 1 (  +  ,  K ) `  ( |_ `  m ) )  -  T ) )  <_  ( E  x.  ( ( log `  m
)  /  m ) ) )
190 fveq2 5848 . . . . . . . . . . . 12  |-  ( a  =  k  ->  ( log `  a )  =  ( log `  k
) )
191190, 54oveq12d 6288 . . . . . . . . . . 11  |-  ( a  =  k  ->  (
( log `  a
)  /  a )  =  ( ( log `  k )  /  k
) )
19253, 191oveq12d 6288 . . . . . . . . . 10  |-  ( a  =  k  ->  (
( X `  ( L `  a )
)  x.  ( ( log `  a )  /  a ) )  =  ( ( X `
 ( L `  k ) )  x.  ( ( log `  k
)  /  k ) ) )
193 dchrvmasumif.g . . . . . . . . . 10  |-  K  =  ( a  e.  NN  |->  ( ( X `  ( L `  a ) )  x.  ( ( log `  a )  /  a ) ) )
194 ovex 6298 . . . . . . . . . 10  |-  ( ( X `  ( L `
 k ) )  x.  ( ( log `  k )  /  k
) )  e.  _V
195192, 193, 194fvmpt 5931 . . . . . . . . 9  |-  ( k  e.  NN  ->  ( K `  k )  =  ( ( X `
 ( L `  k ) )  x.  ( ( log `  k
)  /  k ) ) )
19611, 195syl 16 . . . . . . . 8  |-  ( k  e.  ( 1 ... ( |_ `  m
) )  ->  ( K `  k )  =  ( ( X `
 ( L `  k ) )  x.  ( ( log `  k
)  /  k ) ) )
197 ifnefalse 3941 . . . . . . . . . . . . 13  |-  ( S  =/=  0  ->  if ( S  =  0 ,  m ,  k )  =  k )
198197fveq2d 5852 . . . . . . . . . . . 12  |-  ( S  =/=  0  ->  ( log `  if ( S  =  0 ,  m ,  k ) )  =  ( log `  k
) )
199198oveq1d 6285 . . . . . . . . . . 11  |-  ( S  =/=  0  ->  (
( log `  if ( S  =  0 ,  m ,  k ) )  /  k )  =  ( ( log `  k )  /  k
) )
200199oveq2d 6286 . . . . . . . . . 10  |-  ( S  =/=  0  ->  (
( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  =  ( ( X `  ( L `
 k ) )  x.  ( ( log `  k )  /  k
) ) )
201200adantl 464 . . . . . . . . 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
) ) )
202201eqcomd 2462 . . . . . . . 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 ) ) )
203196, 202sylan9eqr 2517 . . . . . . 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 ) ) )
204151adantr 463 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =/=  0 )  ->  ( |_ `  m )  e.  ( ZZ>= `  1 )
)
205 nnrp 11230 . . . . . . . . . . . . . . . 16  |-  ( k  e.  NN  ->  k  e.  RR+ )
206205adantl 464 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  NN )  ->  k  e.  RR+ )
207206relogcld 23176 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN )  ->  ( log `  k )  e.  RR )
208207recnd 9611 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  NN )  ->  ( log `  k )  e.  CC )
209208, 47, 49divcld 10316 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( log `  k )  /  k )  e.  CC )
21015, 209mulcld 9605 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( X `  ( L `
 k ) )  x.  ( ( log `  k )  /  k
) )  e.  CC )
211192cbvmptv 4530 . . . . . . . . . . . 12  |-  ( a  e.  NN  |->  ( ( X `  ( L `
 a ) )  x.  ( ( log `  a )  /  a
) ) )  =  ( k  e.  NN  |->  ( ( X `  ( L `  k ) )  x.  ( ( log `  k )  /  k ) ) )
212193, 211eqtri 2483 . . . . . . . . . . 11  |-  K  =  ( k  e.  NN  |->  ( ( X `  ( L `  k ) )  x.  ( ( log `  k )  /  k ) ) )
213210, 212fmptd 6031 . . . . . . . . . 10  |-  ( ph  ->  K : NN --> CC )
214213ad2antrr 723 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =/=  0 )  ->  K : NN --> CC )
215 ffvelrn 6005 . . . . . . . . 9  |-  ( ( K : NN --> CC  /\  k  e.  NN )  ->  ( K `  k
)  e.  CC )
216214, 11, 215syl2an 475 . . . . . . . 8  |-  ( ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =/=  0
)  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( K `  k )  e.  CC )
217203, 216eqeltrrd 2543 . . . . . . 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 )
218203, 204, 217fsumser 13634 . . . . . 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 ) ) )
219 ifnefalse 3941 . . . . . . 7  |-  ( S  =/=  0  ->  if ( S  =  0 ,  0 ,  T
)  =  T )
220219adantl 464 . . . . . 6  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =/=  0 )  ->  if ( S  =  0 ,  0 ,  T
)  =  T )
221218, 220oveq12d 6288 . . . . 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 ) )
222221fveq2d 5852 . . . 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 ) ) )
223 ifnefalse 3941 . . . . . 6  |-  ( S  =/=  0  ->  if ( S  =  0 ,  C ,  E )  =  E )
224223adantl 464 . . . . 5  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =/=  0 )  ->  if ( S  =  0 ,  C ,  E )  =  E )
225224oveq1d 6285 . . . 4  |-  ( ( ( ph  /\  m  e.  ( 3 [,) +oo ) )  /\  S  =/=  0 )  ->  ( if ( S  =  0 ,  C ,  E
)  x.  ( ( log `  m )  /  m ) )  =  ( E  x.  ( ( log `  m
)  /  m ) ) )
226189, 222, 2253brtr4d 4469 . . 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 ) ) )
227177, 226pm2.61dane 2772 . 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 ) ) )
228 fzfid 12065 . . . 4  |-  ( ph  ->  ( 1 ... 2
)  e.  Fin )
2297adantr 463 . . . . . . 7  |-  ( (
ph  /\  k  e.  ( 1 ... 2
) )  ->  X  e.  D )
230 elfzelz 11691 . . . . . . . 8  |-  ( k  e.  ( 1 ... 2 )  ->  k  e.  ZZ )
231230adantl 464 . . . . . . 7  |-  ( (
ph  /\  k  e.  ( 1 ... 2
) )  ->  k  e.  ZZ )
2324, 1, 5, 2, 229, 231dchrzrhcl 23718 . . . . . 6  |-  ( (
ph  /\  k  e.  ( 1 ... 2
) )  ->  ( X `  ( L `  k ) )  e.  CC )
233232abscld 13349 . . . . 5  |-  ( (
ph  /\  k  e.  ( 1 ... 2
) )  ->  ( abs `  ( X `  ( L `  k ) ) )  e.  RR )
23463, 80elrpii 11224 . . . . . . 7  |-  3  e.  RR+
235 relogcl 23129 . . . . . . 7  |-  ( 3  e.  RR+  ->  ( log `  3 )  e.  RR )
236234, 235ax-mp 5 . . . . . 6  |-  ( log `  3 )  e.  RR
237 elfznn 11717 . . . . . . 7  |-  ( k  e.  ( 1 ... 2 )  ->  k  e.  NN )
238237adantl 464 . . . . . 6  |-  ( (
ph  /\  k  e.  ( 1 ... 2
) )  ->  k  e.  NN )
239 nndivre 10567 . . . . . 6  |-  ( ( ( log `  3
)  e.  RR  /\  k  e.  NN )  ->  ( ( log `  3
)  /  k )  e.  RR )
240236, 238, 239sylancr 661 . . . . 5  |-  ( (
ph  /\  k  e.  ( 1 ... 2
) )  ->  (
( log `  3
)  /  k )  e.  RR )
241233, 240remulcld 9613 . . . 4  |-  ( (
ph  /\  k  e.  ( 1 ... 2
) )  ->  (
( abs `  ( X `  ( L `  k ) ) )  x.  ( ( log `  3 )  / 
k ) )  e.  RR )
242228, 241fsumrecl 13638 . . 3  |-  ( ph  -> 
sum_ k  e.  ( 1 ... 2 ) ( ( abs `  ( X `  ( L `  k ) ) )  x.  ( ( log `  3 )  / 
k ) )  e.  RR )
24343abscld 13349 . . 3  |-  ( ph  ->  ( abs `  if ( S  =  0 ,  0 ,  T
) )  e.  RR )
244242, 243readdcld 9612 . 2  |-  ( ph  ->  ( sum_ k  e.  ( 1 ... 2 ) ( ( abs `  ( X `  ( L `  k ) ) )  x.  ( ( log `  3 )  / 
k ) )  +  ( abs `  if ( S  =  0 ,  0 ,  T
) ) )  e.  RR )
245 simpl 455 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  ph )
24663rexri 9635 . . . . . . . . . . 11  |-  3  e.  RR*
247 elico2 11591 . . . . . . . . . . 11  |-  ( ( 1  e.  RR  /\  3  e.  RR* )  -> 
( m  e.  ( 1 [,) 3 )  <-> 
( m  e.  RR  /\  1  <_  m  /\  m  <  3 ) ) )
248102, 246, 247mp2an 670 . . . . . . . . . 10  |-  ( m  e.  ( 1 [,) 3 )  <->  ( m  e.  RR  /\  1  <_  m  /\  m  <  3
) )
249248simp1bi 1009 . . . . . . . . 9  |-  ( m  e.  ( 1 [,) 3 )  ->  m  e.  RR )
250249adantl 464 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  m  e.  RR )
251 0red 9586 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  0  e.  RR )
252 1red 9600 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  1  e.  RR )
253 0lt1 10071 . . . . . . . . . 10  |-  0  <  1
254253a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  0  <  1 )
255248simp2bi 1010 . . . . . . . . . 10  |-  ( m  e.  ( 1 [,) 3 )  ->  1  <_  m )
256255adantl 464 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  1  <_  m )
257251, 252, 250, 254, 256ltletrd 9731 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  0  <  m )
258250, 257elrpd 11256 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  m  e.  RR+ )
259245, 258jca 530 . . . . . 6  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  ( ph  /\  m  e.  RR+ ) )
26043adantr 463 . . . . . . 7  |-  ( (
ph  /\  m  e.  RR+ )  ->  if ( S  =  0 , 
0 ,  T )  e.  CC )
26126, 260subcld 9922 . . . . . 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 )
262259, 261syl 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 )
263262abscld 13349 . . . 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 )
264259, 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 )
265264abscld 13349 . . . . 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 )
266243adantr 463 . . . . 5  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  ( abs `  if ( S  =  0 ,  0 ,  T ) )  e.  RR )
267265, 266readdcld 9612 . . . 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 )
268242adantr 463 . . . . 5  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  sum_ k  e.  ( 1 ... 2
) ( ( abs `  ( X `  ( L `  k )
) )  x.  (
( log `  3
)  /  k ) )  e.  RR )
269268, 266readdcld 9612 . . . 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 )
27026, 260abs2dif2d 13371 . . . . 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 ) ) ) )
271259, 270syl 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 ) ) ) )
27225abscld 13349 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( abs `  ( ( X `  ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  e.  RR )
2739, 272fsumrecl 13638 . . . . . . 7  |-  ( (
ph  /\  m  e.  RR+ )  ->  sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( abs `  (
( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  e.  RR )
274259, 273syl 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 )
2759, 25fsumabs 13697 . . . . . . 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 ) ) ) )
276259, 275syl 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 ) ) ) )
277 fzfid 12065 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  RR+ )  ->  ( 1 ... 2 )  e. 
Fin )
278232adantlr 712 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  ( X `  ( L `  k ) )  e.  CC )
27917adantr 463 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  m  e.  RR+ )
280237adantl 464 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  k  e.  NN )
281280nnrpd 11257 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  k  e.  RR+ )
282279, 281ifcld 3972 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  if ( S  =  0 ,  m ,  k )  e.  RR+ )
283282relogcld 23176 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  ( log `  if ( S  =  0 ,  m ,  k ) )  e.  RR )
284283, 280nndivred 10580 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  (
( log `  if ( S  =  0 ,  m ,  k ) )  /  k )  e.  RR )
285284recnd 9611 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  (
( log `  if ( S  =  0 ,  m ,  k ) )  /  k )  e.  CC )
286278, 285mulcld 9605 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  (
( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  e.  CC )
287286abscld 13349 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  ( abs `  ( ( X `
 ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  e.  RR )
288277, 287fsumrecl 13638 . . . . . . . 8  |-  ( (
ph  /\  m  e.  RR+ )  ->  sum_ k  e.  ( 1 ... 2
) ( abs `  (
( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  e.  RR )
289259, 288syl 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 )
290 fzfid 12065 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  (
1 ... 2 )  e. 
Fin )
291259, 286sylan 469 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  (
( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  e.  CC )
292291abscld 13349 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  ( abs `  ( ( X `
 ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  e.  RR )
293291absge0d 13357 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  0  <_  ( abs `  (
( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) ) )
294250flcld 11916 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  ( |_ `  m )  e.  ZZ )
295 2z 10892 . . . . . . . . . . 11  |-  2  e.  ZZ
296295a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  2  e.  ZZ )
297248simp3bi 1011 . . . . . . . . . . . . . 14  |-  ( m  e.  ( 1 [,) 3 )  ->  m  <  3 )
298297adantl 464 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  m  <  3 )
299 3z 10893 . . . . . . . . . . . . . 14  |-  3  e.  ZZ
300 fllt 11924 . . . . . . . . . . . . . 14  |-  ( ( m  e.  RR  /\  3  e.  ZZ )  ->  ( m  <  3  <->  ( |_ `  m )  <  3 ) )
301250, 299, 300sylancl 660 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  (
m  <  3  <->  ( |_ `  m )  <  3
) )
302298, 301mpbid 210 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  ( |_ `  m )  <  3 )
303 df-3 10591 . . . . . . . . . . . 12  |-  3  =  ( 2  +  1 )
304302, 303syl6breq 4478 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  ( |_ `  m )  < 
( 2  +  1 ) )
305 rpre 11227 . . . . . . . . . . . . . . 15  |-  ( m  e.  RR+  ->  m  e.  RR )
306305adantl 464 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  RR+ )  ->  m  e.  RR )
307306flcld 11916 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  RR+ )  ->  ( |_ `  m )  e.  ZZ )
308 zleltp1 10910 . . . . . . . . . . . . 13  |-  ( ( ( |_ `  m
)  e.  ZZ  /\  2  e.  ZZ )  ->  ( ( |_ `  m )  <_  2  <->  ( |_ `  m )  <  ( 2  +  1 ) ) )
309307, 295, 308sylancl 660 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  RR+ )  ->  ( ( |_ `  m )  <_ 
2  <->  ( |_ `  m )  <  (
2  +  1 ) ) )
310259, 309syl 16 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  (
( |_ `  m
)  <_  2  <->  ( |_ `  m )  <  (
2  +  1 ) ) )
311304, 310mpbird 232 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  ( |_ `  m )  <_ 
2 )
312 eluz2 11088 . . . . . . . . . 10  |-  ( 2  e.  ( ZZ>= `  ( |_ `  m ) )  <-> 
( ( |_ `  m )  e.  ZZ  /\  2  e.  ZZ  /\  ( |_ `  m )  <_  2 ) )
313294, 296, 311, 312syl3anbrc 1178 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  2  e.  ( ZZ>= `  ( |_ `  m ) ) )
314 fzss2 11727 . . . . . . . . 9  |-  ( 2  e.  ( ZZ>= `  ( |_ `  m ) )  ->  ( 1 ... ( |_ `  m
) )  C_  (
1 ... 2 ) )
315313, 314syl 16 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  (
1 ... ( |_ `  m ) )  C_  ( 1 ... 2
) )
316290, 292, 293, 315fsumless 13692 . . . . . . 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 ) ) ) )
317241adantlr 712 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  (
( abs `  ( X `  ( L `  k ) ) )  x.  ( ( log `  3 )  / 
k ) )  e.  RR )
318278, 285absmuld 13367 . . . . . . . . . 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 ) ) ) )
319259, 318sylan 469 . . . . . . . . 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 ) ) ) )
320259, 284sylan 469 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  (
( log `  if ( S  =  0 ,  m ,  k ) )  /  k )  e.  RR )
321259, 283sylan 469 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  ( log `  if ( S  =  0 ,  m ,  k ) )  e.  RR )
322 log1 23139 . . . . . . . . . . . . . 14  |-  ( log `  1 )  =  0
323 elfzle1 11692 . . . . . . . . . . . . . . . 16  |-  ( k  e.  ( 1 ... 2 )  ->  1  <_  k )
324 breq2 4443 . . . . . . . . . . . . . . . . 17  |-  ( m  =  if ( S  =  0 ,  m ,  k )  -> 
( 1  <_  m  <->  1  <_  if ( S  =  0 ,  m ,  k ) ) )
325 breq2 4443 . . . . . . . . . . . . . . . . 17  |-  ( k  =  if ( S  =  0 ,  m ,  k )  -> 
( 1  <_  k  <->  1  <_  if ( S  =  0 ,  m ,  k ) ) )
326324, 325ifboth 3965 . . . . . . . . . . . . . . . 16  |-  ( ( 1  <_  m  /\  1  <_  k )  -> 
1  <_  if ( S  =  0 ,  m ,  k )
)
327256, 323, 326syl2an 475 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  1  <_  if ( S  =  0 ,  m ,  k ) )
328 1rp 11225 . . . . . . . . . . . . . . . . 17  |-  1  e.  RR+
329 logleb 23156 . . . . . . . . . . . . . . . . 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 ) ) ) )
330328, 282, 329sylancr 661 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  (
1  <_  if ( S  =  0 ,  m ,  k )  <->  ( log `  1 )  <_  ( log `  if ( S  =  0 ,  m ,  k ) ) ) )
331259, 330sylan 469 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  (
1  <_  if ( S  =  0 ,  m ,  k )  <->  ( log `  1 )  <_  ( log `  if ( S  =  0 ,  m ,  k ) ) ) )
332327, 331mpbid 210 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  ( log `  1 )  <_ 
( log `  if ( S  =  0 ,  m ,  k ) ) )
333322, 332syl5eqbrr 4473 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  0  <_  ( log `  if ( S  =  0 ,  m ,  k ) ) )
334281rpregt0d 11265 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  (
k  e.  RR  /\  0  <  k ) )
335259, 334sylan 469 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  (
k  e.  RR  /\  0  <  k ) )
336 divge0 10407 . . . . . . . . . . . . 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 ) )
337321, 333, 335, 336syl21anc 1225 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  0  <_  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )
338320, 337absidd 13336 . . . . . . . . . . 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 ) )
339338, 320eqeltrd 2542 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  ( abs `  ( ( log `  if ( S  =  0 ,  m ,  k ) )  / 
k ) )  e.  RR )
340240adantlr 712 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  (
( log `  3
)  /  k )  e.  RR )
341233adantlr 712 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  ( abs `  ( X `  ( L `  k ) ) )  e.  RR )
342278absge0d 13357 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  0  <_  ( abs `  ( X `  ( L `  k ) ) ) )
343341, 342jca 530 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  (
( abs `  ( X `  ( L `  k ) ) )  e.  RR  /\  0  <_  ( abs `  ( X `  ( L `  k ) ) ) ) )
344259, 343sylan 469 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  (
( abs `  ( X `  ( L `  k ) ) )  e.  RR  /\  0  <_  ( abs `  ( X `  ( L `  k ) ) ) ) )
345297ad2antlr 724 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  m  <  3 )
346280nnred 10546 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  k  e.  RR )
347 2re 10601 . . . . . . . . . . . . . . . . . 18  |-  2  e.  RR
348347a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  2  e.  RR )
34963a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  3  e.  RR )
350 elfzle2 11693 . . . . . . . . . . . . . . . . . 18  |-  ( k  e.  ( 1 ... 2 )  ->  k  <_  2 )
351350adantl 464 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  k  <_  2 )
352 2lt3 10699 . . . . . . . . . . . . . . . . . 18  |-  2  <  3
353352a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  2  <  3 )
354346, 348, 349, 351, 353lelttrd 9729 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  k  <  3 )
355259, 354sylan 469 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  k  <  3 )
356 breq1 4442 . . . . . . . . . . . . . . . 16  |-  ( m  =  if ( S  =  0 ,  m ,  k )  -> 
( m  <  3  <->  if ( S  =  0 ,  m ,  k )  <  3 ) )
357 breq1 4442 . . . . . . . . . . . . . . . 16  |-  ( k  =  if ( S  =  0 ,  m ,  k )  -> 
( k  <  3  <->  if ( S  =  0 ,  m ,  k )  <  3 ) )
358356, 357ifboth 3965 . . . . . . . . . . . . . . 15  |-  ( ( m  <  3  /\  k  <  3 )  ->  if ( S  =  0 ,  m ,  k )  <  3 )
359345, 355, 358syl2anc 659 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  if ( S  =  0 ,  m ,  k )  <  3 )
360282rpred 11259 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  if ( S  =  0 ,  m ,  k )  e.  RR )
361 ltle 9662 . . . . . . . . . . . . . . . 16  |-  ( ( if ( S  =  0 ,  m ,  k )  e.  RR  /\  3  e.  RR )  ->  ( if ( S  =  0 ,  m ,  k )  <  3  ->  if ( S  =  0 ,  m ,  k )  <_  3 ) )
362360, 63, 361sylancl 660 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  ( if ( S  =  0 ,  m ,  k )  <  3  ->  if ( S  =  0 ,  m ,  k )  <_  3 ) )
363259, 362sylan 469 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  ( if ( S  =  0 ,  m ,  k )  <  3  ->  if ( S  =  0 ,  m ,  k )  <_  3 ) )
364359, 363mpd 15 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  if ( S  =  0 ,  m ,  k )  <_  3 )
365 logleb 23156 . . . . . . . . . . . . . . 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 ) ) )
366282, 234, 365sylancl 660 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  ( if ( S  =  0 ,  m ,  k )  <_  3  <->  ( log `  if ( S  =  0 ,  m ,  k ) )  <_ 
( log `  3
) ) )
367259, 366sylan 469 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  ( if ( S  =  0 ,  m ,  k )  <_  3  <->  ( log `  if ( S  =  0 ,  m ,  k ) )  <_ 
( log `  3
) ) )
368364, 367mpbid 210 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  ( log `  if ( S  =  0 ,  m ,  k ) )  <_  ( log `  3
) )
369236a1i 11 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  ( log `  3 )  e.  RR )
370283, 369, 281lediv1d 11301 . . . . . . . . . . . . 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 ) ) )
371259, 370sylan 469 . . . . . . . . . . . 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 ) ) )
372368, 371mpbid 210 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  (
( log `  if ( S  =  0 ,  m ,  k ) )  /  k )  <_  ( ( log `  3 )  / 
k ) )
373338, 372eqbrtrd 4459 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  ( abs `  ( ( log `  if ( S  =  0 ,  m ,  k ) )  / 
k ) )  <_ 
( ( log `  3
)  /  k ) )
374 lemul2a 10393 . . . . . . . . . 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 ) ) )
375339, 340, 344, 373, 374syl31anc 1229 . . . . . . . . 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 ) ) )
376319, 375eqbrtrd 4459 . . . . . . . 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 ) ) )
377290, 292, 317, 376fsumle 13695 . . . . . . 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 ) ) )
378274, 289, 268, 316, 377letrd 9728 . . . . . 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 ) ) )
379265, 274, 268, 276, 378letrd 9728 . . . . 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 ) ) )
38026abscld 13349 . . . . . . 7  |-  ( (
ph  /\  m  e.  RR+ )  ->  ( abs ` 
sum_ k  e.  ( 1 ... ( |_
`  m ) ) ( ( X `  ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  e.  RR )
381242adantr 463 . . . . . . 7  |-  ( (
ph  /\  m  e.  RR+ )  ->  sum_ k  e.  ( 1 ... 2
) ( ( abs `  ( X `  ( L `  k )
) )  x.  (
( log `  3
)  /  k ) )  e.  RR )
382260abscld 13349 . . . . . . 7  |-  ( (
ph  /\  m  e.  RR+ )  ->  ( abs `  if ( S  =  0 ,  0 ,  T ) )  e.  RR )
383380, 381, 382leadd1d 10142 . . . . . 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
) ) ) ) )
384259, 383syl 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
) ) ) ) )
385379, 384mpbid 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
) ) ) )
386263, 267, 269, 271, 385letrd 9728 . . 3  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  ( abs `  ( sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( ( X `  ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  -  if (