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

Theorem dchrvmasumiflem1 20666
Description: Lemma for dchrvmasumif 20668. (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 11051 . . 3  |-  ( (
ph  /\  m  e.  RR+ )  ->  ( 1 ... ( |_ `  m ) )  e. 
Fin )
10 simpl 443 . . . . 5  |-  ( (
ph  /\  m  e.  RR+ )  ->  ph )
11 elfznn 10835 . . . . 5  |-  ( k  e.  ( 1 ... ( |_ `  m
) )  ->  k  e.  NN )
127adantr 451 . . . . . 6  |-  ( (
ph  /\  k  e.  NN )  ->  X  e.  D )
13 nnz 10061 . . . . . . 7  |-  ( k  e.  NN  ->  k  e.  ZZ )
1413adantl 452 . . . . . 6  |-  ( (
ph  /\  k  e.  NN )  ->  k  e.  ZZ )
154, 1, 5, 2, 12, 14dchrzrhcl 20500 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  ( X `
 ( L `  k ) )  e.  CC )
1610, 11, 15syl2an 463 . . . 4  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( X `  ( L `  k
) )  e.  CC )
17 simpr 447 . . . . . . . 8  |-  ( (
ph  /\  m  e.  RR+ )  ->  m  e.  RR+ )
1811nnrpd 10405 . . . . . . . 8  |-  ( k  e.  ( 1 ... ( |_ `  m
) )  ->  k  e.  RR+ )
19 ifcl 3614 . . . . . . . 8  |-  ( ( m  e.  RR+  /\  k  e.  RR+ )  ->  if ( S  =  0 ,  m ,  k )  e.  RR+ )
2017, 18, 19syl2an 463 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  if ( S  =  0 ,  m ,  k )  e.  RR+ )
2120relogcld 19990 . . . . . 6  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( log `  if ( S  =  0 ,  m ,  k ) )  e.  RR )
2211adantl 452 . . . . . 6  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  k  e.  NN )
2321, 22nndivred 9810 . . . . 5  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k )  e.  RR )
2423recnd 8877 . . . 4  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k )  e.  CC )
2516, 24mulcld 8871 . . 3  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( ( X `  ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  e.  CC )
269, 25fsumcl 12222 . 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 5541 . . . 4  |-  ( m  =  ( x  / 
d )  ->  ( |_ `  m )  =  ( |_ `  (
x  /  d ) ) )
2827oveq2d 5890 . . 3  |-  ( m  =  ( x  / 
d )  ->  (
1 ... ( |_ `  m ) )  =  ( 1 ... ( |_ `  ( x  / 
d ) ) ) )
29 ifeq1 3582 . . . . . . 7  |-  ( m  =  ( x  / 
d )  ->  if ( S  =  0 ,  m ,  k )  =  if ( S  =  0 ,  ( x  /  d ) ,  k ) )
3029fveq2d 5545 . . . . . 6  |-  ( m  =  ( x  / 
d )  ->  ( log `  if ( S  =  0 ,  m ,  k ) )  =  ( log `  if ( S  =  0 ,  ( x  / 
d ) ,  k ) ) )
3130oveq1d 5889 . . . . 5  |-  ( m  =  ( x  / 
d )  ->  (
( log `  if ( S  =  0 ,  m ,  k ) )  /  k )  =  ( ( log `  if ( S  =  0 ,  ( x  /  d ) ,  k ) )  / 
k ) )
3231oveq2d 5890 . . . 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 451 . . 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 12196 . 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 451 . . 3  |-  ( (
ph  /\  S  = 
0 )  ->  C  e.  ( 0 [,)  +oo ) )
37 dchrvmasumif.e . . . 4  |-  ( ph  ->  E  e.  ( 0 [,)  +oo ) )
3837adantr 451 . . 3  |-  ( (
ph  /\  -.  S  =  0 )  ->  E  e.  ( 0 [,)  +oo ) )
3936, 38ifclda 3605 . 2  |-  ( ph  ->  if ( S  =  0 ,  C ,  E )  e.  ( 0 [,)  +oo )
)
40 0cn 8847 . . 3  |-  0  e.  CC
41 dchrvmasumif.t . . . 4  |-  ( ph  ->  seq  1 (  +  ,  K )  ~~>  T )
42 climcl 11989 . . . 4  |-  (  seq  1 (  +  ,  K )  ~~>  T  ->  T  e.  CC )
4341, 42syl 15 . . 3  |-  ( ph  ->  T  e.  CC )
44 ifcl 3614 . . 3  |-  ( ( 0  e.  CC  /\  T  e.  CC )  ->  if ( S  =  0 ,  0 ,  T )  e.  CC )
4540, 43, 44sylancr 644 . 2  |-  ( ph  ->  if ( S  =  0 ,  0 ,  T )  e.  CC )
46 nnuz 10279 . . . . . . . . 9  |-  NN  =  ( ZZ>= `  1 )
47 1z 10069 . . . . . . . . . 10  |-  1  e.  ZZ
4847a1i 10 . . . . . . . . 9  |-  ( ph  ->  1  e.  ZZ )
49 nncn 9770 . . . . . . . . . . . . 13  |-  ( k  e.  NN  ->  k  e.  CC )
5049adantl 452 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN )  ->  k  e.  CC )
51 nnne0 9794 . . . . . . . . . . . . 13  |-  ( k  e.  NN  ->  k  =/=  0 )
5251adantl 452 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN )  ->  k  =/=  0 )
5315, 50, 52divcld 9552 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( X `  ( L `
 k ) )  /  k )  e.  CC )
54 dchrvmasumif.f . . . . . . . . . . . 12  |-  F  =  ( a  e.  NN  |->  ( ( X `  ( L `  a ) )  /  a ) )
55 fveq2 5541 . . . . . . . . . . . . . . 15  |-  ( a  =  k  ->  ( L `  a )  =  ( L `  k ) )
5655fveq2d 5545 . . . . . . . . . . . . . 14  |-  ( a  =  k  ->  ( X `  ( L `  a ) )  =  ( X `  ( L `  k )
) )
57 id 19 . . . . . . . . . . . . . 14  |-  ( a  =  k  ->  a  =  k )
5856, 57oveq12d 5892 . . . . . . . . . . . . 13  |-  ( a  =  k  ->  (
( X `  ( L `  a )
)  /  a )  =  ( ( X `
 ( L `  k ) )  / 
k ) )
5958cbvmptv 4127 . . . . . . . . . . . 12  |-  ( a  e.  NN  |->  ( ( X `  ( L `
 a ) )  /  a ) )  =  ( k  e.  NN  |->  ( ( X `
 ( L `  k ) )  / 
k ) )
6054, 59eqtri 2316 . . . . . . . . . . 11  |-  F  =  ( k  e.  NN  |->  ( ( X `  ( L `  k ) )  /  k ) )
6153, 60fmptd 5700 . . . . . . . . . 10  |-  ( ph  ->  F : NN --> CC )
62 ffvelrn 5679 . . . . . . . . . 10  |-  ( ( F : NN --> CC  /\  k  e.  NN )  ->  ( F `  k
)  e.  CC )
6361, 62sylan 457 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  NN )  ->  ( F `
 k )  e.  CC )
6446, 48, 63serf 11090 . . . . . . . 8  |-  ( ph  ->  seq  1 (  +  ,  F ) : NN --> CC )
6564ad2antrr 706 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  ( 3 [,)  +oo ) )  /\  S  =  0 )  ->  seq  1 (  +  ,  F ) : NN --> CC )
66 3re 9833 . . . . . . . . . . 11  |-  3  e.  RR
67 elicopnf 10755 . . . . . . . . . . 11  |-  ( 3  e.  RR  ->  (
m  e.  ( 3 [,)  +oo )  <->  ( m  e.  RR  /\  3  <_  m ) ) )
6866, 67mp1i 11 . . . . . . . . . 10  |-  ( ph  ->  ( m  e.  ( 3 [,)  +oo )  <->  ( m  e.  RR  /\  3  <_  m ) ) )
6968simprbda 606 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  m  e.  RR )
70 1re 8853 . . . . . . . . . . 11  |-  1  e.  RR
7170a1i 10 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  1  e.  RR )
7266a1i 10 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  3  e.  RR )
73 1lt3 9904 . . . . . . . . . . . 12  |-  1  <  3
7470, 66, 73ltleii 8957 . . . . . . . . . . 11  |-  1  <_  3
7574a1i 10 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  1  <_  3 )
7668simplbda 607 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  3  <_  m )
7771, 72, 69, 75, 76letrd 8989 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  1  <_  m )
78 flge1nn 10965 . . . . . . . . 9  |-  ( ( m  e.  RR  /\  1  <_  m )  -> 
( |_ `  m
)  e.  NN )
7969, 77, 78syl2anc 642 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  ( |_ `  m )  e.  NN )
8079adantr 451 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  ( 3 [,)  +oo ) )  /\  S  =  0 )  -> 
( |_ `  m
)  e.  NN )
81 ffvelrn 5679 . . . . . . 7  |-  ( (  seq  1 (  +  ,  F ) : NN --> CC  /\  ( |_ `  m )  e.  NN )  ->  (  seq  1 (  +  ,  F ) `  ( |_ `  m ) )  e.  CC )
8265, 80, 81syl2anc 642 . . . . . 6  |-  ( ( ( ph  /\  m  e.  ( 3 [,)  +oo ) )  /\  S  =  0 )  -> 
(  seq  1 (  +  ,  F ) `
 ( |_ `  m ) )  e.  CC )
8382abscld 11934 . . . . 5  |-  ( ( ( ph  /\  m  e.  ( 3 [,)  +oo ) )  /\  S  =  0 )  -> 
( abs `  (  seq  1 (  +  ,  F ) `  ( |_ `  m ) ) )  e.  RR )
84 simpl 443 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  ph )
85 0re 8854 . . . . . . . . . . 11  |-  0  e.  RR
8685a1i 10 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  0  e.  RR )
87 3pos 9846 . . . . . . . . . . 11  |-  0  <  3
8887a1i 10 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  0  <  3 )
8986, 72, 69, 88, 76ltletrd 8992 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  0  <  m )
9069, 89elrpd 10404 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  m  e.  RR+ )
9184, 90jca 518 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  ( ph  /\  m  e.  RR+ ) )
92 elrege0 10762 . . . . . . . . . 10  |-  ( C  e.  ( 0 [,) 
+oo )  <->  ( C  e.  RR  /\  0  <_  C ) )
9392simplbi 446 . . . . . . . . 9  |-  ( C  e.  ( 0 [,) 
+oo )  ->  C  e.  RR )
9435, 93syl 15 . . . . . . . 8  |-  ( ph  ->  C  e.  RR )
95 rerpdivcl 10397 . . . . . . . 8  |-  ( ( C  e.  RR  /\  m  e.  RR+ )  -> 
( C  /  m
)  e.  RR )
9694, 95sylan 457 . . . . . . 7  |-  ( (
ph  /\  m  e.  RR+ )  ->  ( C  /  m )  e.  RR )
9791, 96syl 15 . . . . . 6  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  ( C  /  m )  e.  RR )
9897adantr 451 . . . . 5  |-  ( ( ( ph  /\  m  e.  ( 3 [,)  +oo ) )  /\  S  =  0 )  -> 
( C  /  m
)  e.  RR )
9990relogcld 19990 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  ( log `  m )  e.  RR )
10069, 77logge0d 19997 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  0  <_  ( log `  m
) )
10199, 100jca 518 . . . . . 6  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  (
( log `  m
)  e.  RR  /\  0  <_  ( log `  m
) ) )
102101adantr 451 . . . . 5  |-  ( ( ( ph  /\  m  e.  ( 3 [,)  +oo ) )  /\  S  =  0 )  -> 
( ( log `  m
)  e.  RR  /\  0  <_  ( log `  m
) ) )
103 oveq2 5882 . . . . . . . 8  |-  ( S  =  0  ->  (
(  seq  1 (  +  ,  F ) `
 ( |_ `  m ) )  -  S )  =  ( (  seq  1 (  +  ,  F ) `
 ( |_ `  m ) )  - 
0 ) )
10464adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  seq  1 (  +  ,  F ) : NN --> CC )
105104, 79, 81syl2anc 642 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  (  seq  1 (  +  ,  F ) `  ( |_ `  m ) )  e.  CC )
106105subid1d 9162 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  (
(  seq  1 (  +  ,  F ) `
 ( |_ `  m ) )  - 
0 )  =  (  seq  1 (  +  ,  F ) `  ( |_ `  m ) ) )
107103, 106sylan9eqr 2350 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  ( 3 [,)  +oo ) )  /\  S  =  0 )  -> 
( (  seq  1
(  +  ,  F
) `  ( |_ `  m ) )  -  S )  =  (  seq  1 (  +  ,  F ) `  ( |_ `  m ) ) )
108107fveq2d 5545 . . . . . 6  |-  ( ( ( ph  /\  m  e.  ( 3 [,)  +oo ) )  /\  S  =  0 )  -> 
( abs `  (
(  seq  1 (  +  ,  F ) `
 ( |_ `  m ) )  -  S ) )  =  ( abs `  (  seq  1 (  +  ,  F ) `  ( |_ `  m ) ) ) )
109 elicopnf 10755 . . . . . . . . . 10  |-  ( 1  e.  RR  ->  (
m  e.  ( 1 [,)  +oo )  <->  ( m  e.  RR  /\  1  <_  m ) ) )
11070, 109ax-mp 8 . . . . . . . . 9  |-  ( m  e.  ( 1 [,) 
+oo )  <->  ( m  e.  RR  /\  1  <_  m ) )
11169, 77, 110sylanbrc 645 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  m  e.  ( 1 [,)  +oo ) )
112 dchrvmasumif.1 . . . . . . . . 9  |-  ( ph  ->  A. y  e.  ( 1 [,)  +oo )
( abs `  (
(  seq  1 (  +  ,  F ) `
 ( |_ `  y ) )  -  S ) )  <_ 
( C  /  y
) )
113112adantr 451 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  A. y  e.  ( 1 [,)  +oo ) ( abs `  (
(  seq  1 (  +  ,  F ) `
 ( |_ `  y ) )  -  S ) )  <_ 
( C  /  y
) )
114 fveq2 5541 . . . . . . . . . . . . 13  |-  ( y  =  m  ->  ( |_ `  y )  =  ( |_ `  m
) )
115114fveq2d 5545 . . . . . . . . . . . 12  |-  ( y  =  m  ->  (  seq  1 (  +  ,  F ) `  ( |_ `  y ) )  =  (  seq  1
(  +  ,  F
) `  ( |_ `  m ) ) )
116115oveq1d 5889 . . . . . . . . . . 11  |-  ( y  =  m  ->  (
(  seq  1 (  +  ,  F ) `
 ( |_ `  y ) )  -  S )  =  ( (  seq  1 (  +  ,  F ) `
 ( |_ `  m ) )  -  S ) )
117116fveq2d 5545 . . . . . . . . . 10  |-  ( y  =  m  ->  ( abs `  ( (  seq  1 (  +  ,  F ) `  ( |_ `  y ) )  -  S ) )  =  ( abs `  (
(  seq  1 (  +  ,  F ) `
 ( |_ `  m ) )  -  S ) ) )
118 oveq2 5882 . . . . . . . . . 10  |-  ( y  =  m  ->  ( C  /  y )  =  ( C  /  m
) )
119117, 118breq12d 4052 . . . . . . . . 9  |-  ( y  =  m  ->  (
( abs `  (
(  seq  1 (  +  ,  F ) `
 ( |_ `  y ) )  -  S ) )  <_ 
( C  /  y
)  <->  ( abs `  (
(  seq  1 (  +  ,  F ) `
 ( |_ `  m ) )  -  S ) )  <_ 
( C  /  m
) ) )
120119rspcv 2893 . . . . . . . 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
) ) )
121111, 113, 120sylc 56 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  ( abs `  ( (  seq  1 (  +  ,  F ) `  ( |_ `  m ) )  -  S ) )  <_  ( C  /  m ) )
122121adantr 451 . . . . . 6  |-  ( ( ( ph  /\  m  e.  ( 3 [,)  +oo ) )  /\  S  =  0 )  -> 
( abs `  (
(  seq  1 (  +  ,  F ) `
 ( |_ `  m ) )  -  S ) )  <_ 
( C  /  m
) )
123108, 122eqbrtrrd 4061 . . . . 5  |-  ( ( ( ph  /\  m  e.  ( 3 [,)  +oo ) )  /\  S  =  0 )  -> 
( abs `  (  seq  1 (  +  ,  F ) `  ( |_ `  m ) ) )  <_  ( C  /  m ) )
124 lemul2a 9627 . . . . 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
) ) )
12583, 98, 102, 123, 124syl31anc 1185 . . . 4  |-  ( ( ( ph  /\  m  e.  ( 3 [,)  +oo ) )  /\  S  =  0 )  -> 
( ( log `  m
)  x.  ( abs `  (  seq  1
(  +  ,  F
) `  ( |_ `  m ) ) ) )  <_  ( ( log `  m )  x.  ( C  /  m
) ) )
126 iftrue 3584 . . . . . . . . . . . . . . 15  |-  ( S  =  0  ->  if ( S  =  0 ,  m ,  k )  =  m )
127126fveq2d 5545 . . . . . . . . . . . . . 14  |-  ( S  =  0  ->  ( log `  if ( S  =  0 ,  m ,  k ) )  =  ( log `  m
) )
128127oveq1d 5889 . . . . . . . . . . . . 13  |-  ( S  =  0  ->  (
( log `  if ( S  =  0 ,  m ,  k ) )  /  k )  =  ( ( log `  m )  /  k
) )
129128ad2antlr 707 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  /\  k  e.  ( 1 ... ( |_
`  m ) ) )  ->  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k )  =  ( ( log `  m
)  /  k ) )
130129oveq2d 5890 . . . . . . . . . . 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
) ) )
13116adantlr 695 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  /\  k  e.  ( 1 ... ( |_
`  m ) ) )  ->  ( X `  ( L `  k
) )  e.  CC )
132 relogcl 19948 . . . . . . . . . . . . . . 15  |-  ( m  e.  RR+  ->  ( log `  m )  e.  RR )
133132adantl 452 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  RR+ )  ->  ( log `  m )  e.  RR )
134133recnd 8877 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  RR+ )  ->  ( log `  m )  e.  CC )
135134ad2antrr 706 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  /\  k  e.  ( 1 ... ( |_
`  m ) ) )  ->  ( log `  m )  e.  CC )
13611adantl 452 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  /\  k  e.  ( 1 ... ( |_
`  m ) ) )  ->  k  e.  NN )
137136nncnd 9778 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  /\  k  e.  ( 1 ... ( |_
`  m ) ) )  ->  k  e.  CC )
138136nnne0d 9806 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  /\  k  e.  ( 1 ... ( |_
`  m ) ) )  ->  k  =/=  0 )
139131, 135, 137, 138div12d 9588 . . . . . . . . . . 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 ) ) )
140130, 139eqtrd 2328 . . . . . . . . . 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 ) ) )
141140sumeq2dv 12192 . . . . . . . . 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 ) ) )
142 iftrue 3584 . . . . . . . . . . 11  |-  ( S  =  0  ->  if ( S  =  0 ,  0 ,  T
)  =  0 )
143142oveq2d 5890 . . . . . . . . . 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 ) )
14426subid1d 9162 . . . . . . . . . 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 ) ) )
145143, 144sylan9eqr 2350 . . . . . . . . 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 ) ) )
146 ovex 5899 . . . . . . . . . . . . . 14  |-  ( ( X `  ( L `
 k ) )  /  k )  e. 
_V
14758, 54, 146fvmpt 5618 . . . . . . . . . . . . 13  |-  ( k  e.  NN  ->  ( F `  k )  =  ( ( X `
 ( L `  k ) )  / 
k ) )
14822, 147syl 15 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( F `  k )  =  ( ( X `  ( L `  k )
)  /  k ) )
14961adantr 451 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  RR+ )  ->  F : NN
--> CC )
150149, 11, 62syl2an 463 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( F `  k )  e.  CC )
151148, 150eqeltrrd 2371 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( ( X `  ( L `  k ) )  / 
k )  e.  CC )
1529, 134, 151fsummulc2 12262 . . . . . . . . . 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 ) ) )
153152adantr 451 . . . . . . . . 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 ) ) )
154141, 145, 1533eqtr4d 2338 . . . . . . . 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 ) ) )
15591, 154sylan 457 . . . . . . 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 ) ) )
15691, 148sylan 457 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( 3 [,)  +oo ) )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( F `  k )  =  ( ( X `  ( L `  k )
)  /  k ) )
15779, 46syl6eleq 2386 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  ( |_ `  m )  e.  ( ZZ>= `  1 )
)
15884, 11, 53syl2an 463 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( 3 [,)  +oo ) )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( ( X `  ( L `  k ) )  / 
k )  e.  CC )
159156, 157, 158fsumser 12219 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( ( X `  ( L `  k ) )  /  k )  =  (  seq  1
(  +  ,  F
) `  ( |_ `  m ) ) )
160159adantr 451 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  ( 3 [,)  +oo ) )  /\  S  =  0 )  ->  sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( ( X `  ( L `  k )
)  /  k )  =  (  seq  1
(  +  ,  F
) `  ( |_ `  m ) ) )
161160oveq2d 5890 . . . . . . 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 ) ) ) )
162155, 161eqtrd 2328 . . . . . 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 ) ) ) )
163162fveq2d 5545 . . . . 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 ) ) ) ) )
164132ad2antlr 707 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  -> 
( log `  m
)  e.  RR )
165164recnd 8877 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  -> 
( log `  m
)  e.  CC )
16691, 165sylan 457 . . . . . 6  |-  ( ( ( ph  /\  m  e.  ( 3 [,)  +oo ) )  /\  S  =  0 )  -> 
( log `  m
)  e.  CC )
167166, 82absmuld 11952 . . . . 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 ) ) ) ) )
16899, 100absidd 11921 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  ( abs `  ( log `  m
) )  =  ( log `  m ) )
169168oveq1d 5889 . . . . . 6  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  (
( abs `  ( log `  m ) )  x.  ( abs `  (  seq  1 (  +  ,  F ) `  ( |_ `  m ) ) ) )  =  ( ( log `  m
)  x.  ( abs `  (  seq  1
(  +  ,  F
) `  ( |_ `  m ) ) ) ) )
170169adantr 451 . . . . 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 ) ) ) ) )
171163, 167, 1703eqtrd 2332 . . . 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 ) ) ) ) )
172 iftrue 3584 . . . . . . . 8  |-  ( S  =  0  ->  if ( S  =  0 ,  C ,  E )  =  C )
173172adantl 452 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  ->  if ( S  =  0 ,  C ,  E
)  =  C )
174173oveq1d 5889 . . . . . 6  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  -> 
( if ( S  =  0 ,  C ,  E )  x.  (
( log `  m
)  /  m ) )  =  ( C  x.  ( ( log `  m )  /  m
) ) )
17594recnd 8877 . . . . . . . 8  |-  ( ph  ->  C  e.  CC )
176175ad2antrr 706 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  ->  C  e.  CC )
177 rpcnne0 10387 . . . . . . . 8  |-  ( m  e.  RR+  ->  ( m  e.  CC  /\  m  =/=  0 ) )
178177ad2antlr 707 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  -> 
( m  e.  CC  /\  m  =/=  0 ) )
179 div12 9462 . . . . . . 7  |-  ( ( C  e.  CC  /\  ( log `  m )  e.  CC  /\  (
m  e.  CC  /\  m  =/=  0 ) )  ->  ( C  x.  ( ( log `  m
)  /  m ) )  =  ( ( log `  m )  x.  ( C  /  m ) ) )
180176, 165, 178, 179syl3anc 1182 . . . . . 6  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  -> 
( C  x.  (
( log `  m
)  /  m ) )  =  ( ( log `  m )  x.  ( C  /  m ) ) )
181174, 180eqtrd 2328 . . . . 5  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  -> 
( if ( S  =  0 ,  C ,  E )  x.  (
( log `  m
)  /  m ) )  =  ( ( log `  m )  x.  ( C  /  m ) ) )
18291, 181sylan 457 . . . 4  |-  ( ( ( ph  /\  m  e.  ( 3 [,)  +oo ) )  /\  S  =  0 )  -> 
( if ( S  =  0 ,  C ,  E )  x.  (
( log `  m
)  /  m ) )  =  ( ( log `  m )  x.  ( C  /  m ) ) )
183125, 171, 1823brtr4d 4069 . . 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 ) ) )
184 dchrvmasumif.2 . . . . . 6  |-  ( ph  ->  A. y  e.  ( 3 [,)  +oo )
( abs `  (
(  seq  1 (  +  ,  K ) `
 ( |_ `  y ) )  -  T ) )  <_ 
( E  x.  (
( log `  y
)  /  y ) ) )
185114fveq2d 5545 . . . . . . . . . 10  |-  ( y  =  m  ->  (  seq  1 (  +  ,  K ) `  ( |_ `  y ) )  =  (  seq  1
(  +  ,  K
) `  ( |_ `  m ) ) )
186185oveq1d 5889 . . . . . . . . 9  |-  ( y  =  m  ->  (
(  seq  1 (  +  ,  K ) `
 ( |_ `  y ) )  -  T )  =  ( (  seq  1 (  +  ,  K ) `
 ( |_ `  m ) )  -  T ) )
187186fveq2d 5545 . . . . . . . 8  |-  ( y  =  m  ->  ( abs `  ( (  seq  1 (  +  ,  K ) `  ( |_ `  y ) )  -  T ) )  =  ( abs `  (
(  seq  1 (  +  ,  K ) `
 ( |_ `  m ) )  -  T ) ) )
188 fveq2 5541 . . . . . . . . . 10  |-  ( y  =  m  ->  ( log `  y )  =  ( log `  m
) )
189 id 19 . . . . . . . . . 10  |-  ( y  =  m  ->  y  =  m )
190188, 189oveq12d 5892 . . . . . . . . 9  |-  ( y  =  m  ->  (
( log `  y
)  /  y )  =  ( ( log `  m )  /  m
) )
191190oveq2d 5890 . . . . . . . 8  |-  ( y  =  m  ->  ( E  x.  ( ( log `  y )  / 
y ) )  =  ( E  x.  (
( log `  m
)  /  m ) ) )
192187, 191breq12d 4052 . . . . . . 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 ) ) ) )
193192rspccva 2896 . . . . . 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 ) ) )
194184, 193sylan 457 . . . . 5  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  ( abs `  ( (  seq  1 (  +  ,  K ) `  ( |_ `  m ) )  -  T ) )  <_  ( E  x.  ( ( log `  m
)  /  m ) ) )
195194adantr 451 . . . 4  |-  ( ( ( ph  /\  m  e.  ( 3 [,)  +oo ) )  /\  S  =/=  0 )  ->  ( abs `  ( (  seq  1 (  +  ,  K ) `  ( |_ `  m ) )  -  T ) )  <_  ( E  x.  ( ( log `  m
)  /  m ) ) )
196 fveq2 5541 . . . . . . . . . . . 12  |-  ( a  =  k  ->  ( log `  a )  =  ( log `  k
) )
197196, 57oveq12d 5892 . . . . . . . . . . 11  |-  ( a  =  k  ->  (
( log `  a
)  /  a )  =  ( ( log `  k )  /  k
) )
19856, 197oveq12d 5892 . . . . . . . . . 10  |-  ( a  =  k  ->  (
( X `  ( L `  a )
)  x.  ( ( log `  a )  /  a ) )  =  ( ( X `
 ( L `  k ) )  x.  ( ( log `  k
)  /  k ) ) )
199 dchrvmasumif.g . . . . . . . . . 10  |-  K  =  ( a  e.  NN  |->  ( ( X `  ( L `  a ) )  x.  ( ( log `  a )  /  a ) ) )
200 ovex 5899 . . . . . . . . . 10  |-  ( ( X `  ( L `
 k ) )  x.  ( ( log `  k )  /  k
) )  e.  _V
201198, 199, 200fvmpt 5618 . . . . . . . . 9  |-  ( k  e.  NN  ->  ( K `  k )  =  ( ( X `
 ( L `  k ) )  x.  ( ( log `  k
)  /  k ) ) )
20211, 201syl 15 . . . . . . . 8  |-  ( k  e.  ( 1 ... ( |_ `  m
) )  ->  ( K `  k )  =  ( ( X `
 ( L `  k ) )  x.  ( ( log `  k
)  /  k ) ) )
203 ifnefalse 3586 . . . . . . . . . . . . 13  |-  ( S  =/=  0  ->  if ( S  =  0 ,  m ,  k )  =  k )
204203fveq2d 5545 . . . . . . . . . . . 12  |-  ( S  =/=  0  ->  ( log `  if ( S  =  0 ,  m ,  k ) )  =  ( log `  k
) )
205204oveq1d 5889 . . . . . . . . . . 11  |-  ( S  =/=  0  ->  (
( log `  if ( S  =  0 ,  m ,  k ) )  /  k )  =  ( ( log `  k )  /  k
) )
206205oveq2d 5890 . . . . . . . . . 10  |-  ( S  =/=  0  ->  (
( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  =  ( ( X `  ( L `
 k ) )  x.  ( ( log `  k )  /  k
) ) )
207206adantl 452 . . . . . . . . 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
) ) )
208207eqcomd 2301 . . . . . . . 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 ) ) )
209202, 208sylan9eqr 2350 . . . . . . 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 ) ) )
210157adantr 451 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  ( 3 [,)  +oo ) )  /\  S  =/=  0 )  ->  ( |_ `  m )  e.  ( ZZ>= `  1 )
)
211 nnrp 10379 . . . . . . . . . . . . . . . 16  |-  ( k  e.  NN  ->  k  e.  RR+ )
212211adantl 452 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  NN )  ->  k  e.  RR+ )
213212relogcld 19990 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN )  ->  ( log `  k )  e.  RR )
214213recnd 8877 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  NN )  ->  ( log `  k )  e.  CC )
215214, 50, 52divcld 9552 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( log `  k )  /  k )  e.  CC )
21615, 215mulcld 8871 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( X `  ( L `
 k ) )  x.  ( ( log `  k )  /  k
) )  e.  CC )
217198cbvmptv 4127 . . . . . . . . . . . 12  |-  ( a  e.  NN  |->  ( ( X `  ( L `
 a ) )  x.  ( ( log `  a )  /  a
) ) )  =  ( k  e.  NN  |->  ( ( X `  ( L `  k ) )  x.  ( ( log `  k )  /  k ) ) )
218199, 217eqtri 2316 . . . . . . . . . . 11  |-  K  =  ( k  e.  NN  |->  ( ( X `  ( L `  k ) )  x.  ( ( log `  k )  /  k ) ) )
219216, 218fmptd 5700 . . . . . . . . . 10  |-  ( ph  ->  K : NN --> CC )
220219ad2antrr 706 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( 3 [,)  +oo ) )  /\  S  =/=  0 )  ->  K : NN --> CC )
221 ffvelrn 5679 . . . . . . . . 9  |-  ( ( K : NN --> CC  /\  k  e.  NN )  ->  ( K `  k
)  e.  CC )
222220, 11, 221syl2an 463 . . . . . . . 8  |-  ( ( ( ( ph  /\  m  e.  ( 3 [,)  +oo ) )  /\  S  =/=  0 )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( K `  k )  e.  CC )
223209, 222eqeltrrd 2371 . . . . . . 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 )
224209, 210, 223fsumser 12219 . . . . . 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 ) ) )
225 ifnefalse 3586 . . . . . . 7  |-  ( S  =/=  0  ->  if ( S  =  0 ,  0 ,  T
)  =  T )
226225adantl 452 . . . . . 6  |-  ( ( ( ph  /\  m  e.  ( 3 [,)  +oo ) )  /\  S  =/=  0 )  ->  if ( S  =  0 ,  0 ,  T
)  =  T )
227224, 226oveq12d 5892 . . . . 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 ) )
228227fveq2d 5545 . . . 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 ) ) )
229 ifnefalse 3586 . . . . . 6  |-  ( S  =/=  0  ->  if ( S  =  0 ,  C ,  E )  =  E )
230229adantl 452 . . . . 5  |-  ( ( ( ph  /\  m  e.  ( 3 [,)  +oo ) )  /\  S  =/=  0 )  ->  if ( S  =  0 ,  C ,  E )  =  E )
231230oveq1d 5889 . . . 4  |-  ( ( ( ph  /\  m  e.  ( 3 [,)  +oo ) )  /\  S  =/=  0 )  ->  ( if ( S  =  0 ,  C ,  E
)  x.  ( ( log `  m )  /  m ) )  =  ( E  x.  ( ( log `  m
)  /  m ) ) )
232195, 228, 2313brtr4d 4069 . . 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 ) ) )
233183, 232pm2.61dane 2537 . 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 ) ) )
234 fzfid 11051 . . . 4  |-  ( ph  ->  ( 1 ... 2
)  e.  Fin )
2357adantr 451 . . . . . . 7  |-  ( (
ph  /\  k  e.  ( 1 ... 2
) )  ->  X  e.  D )
236 elfzelz 10814 . . . . . . . 8  |-  ( k  e.  ( 1 ... 2 )  ->  k  e.  ZZ )
237236adantl 452 . . . . . . 7  |-  ( (
ph  /\  k  e.  ( 1 ... 2
) )  ->  k  e.  ZZ )
2384, 1, 5, 2, 235, 237dchrzrhcl 20500 . . . . . 6  |-  ( (
ph  /\  k  e.  ( 1 ... 2
) )  ->  ( X `  ( L `  k ) )  e.  CC )
239238abscld 11934 . . . . 5  |-  ( (
ph  /\  k  e.  ( 1 ... 2
) )  ->  ( abs `  ( X `  ( L `  k ) ) )  e.  RR )
24066, 87elrpii 10373 . . . . . . 7  |-  3  e.  RR+
241 relogcl 19948 . . . . . . 7  |-  ( 3  e.  RR+  ->  ( log `  3 )  e.  RR )
242240, 241ax-mp 8 . . . . . 6  |-  ( log `  3 )  e.  RR
243 elfznn 10835 . . . . . . 7  |-  ( k  e.  ( 1 ... 2 )  ->  k  e.  NN )
244243adantl 452 . . . . . 6  |-  ( (
ph  /\  k  e.  ( 1 ... 2
) )  ->  k  e.  NN )
245 nndivre 9797 . . . . . 6  |-  ( ( ( log `  3
)  e.  RR  /\  k  e.  NN )  ->  ( ( log `  3
)  /  k )  e.  RR )
246242, 244, 245sylancr 644 . . . . 5  |-  ( (
ph  /\  k  e.  ( 1 ... 2
) )  ->  (
( log `  3
)  /  k )  e.  RR )
247239, 246remulcld 8879 . . . 4  |-  ( (
ph  /\  k  e.  ( 1 ... 2
) )  ->  (
( abs `  ( X `  ( L `  k ) ) )  x.  ( ( log `  3 )  / 
k ) )  e.  RR )
248234, 247fsumrecl 12223 . . 3  |-  ( ph  -> 
sum_ k  e.  ( 1 ... 2 ) ( ( abs `  ( X `  ( L `  k ) ) )  x.  ( ( log `  3 )  / 
k ) )  e.  RR )
24945abscld 11934 . . 3  |-  ( ph  ->  ( abs `  if ( S  =  0 ,  0 ,  T
) )  e.  RR )
250248, 249readdcld 8878 . 2  |-  ( ph  ->  ( sum_ k  e.  ( 1 ... 2 ) ( ( abs `  ( X `  ( L `  k ) ) )  x.  ( ( log `  3 )  / 
k ) )  +  ( abs `  if ( S  =  0 ,  0 ,  T
) ) )  e.  RR )
251 simpl 443 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  ph )
252 rexr 8893 . . . . . . . . . . . 12  |-  ( 3  e.  RR  ->  3  e.  RR* )
25366, 252ax-mp 8 . . . . . . . . . . 11  |-  3  e.  RR*
254 elico2 10730 . . . . . . . . . . 11  |-  ( ( 1  e.  RR  /\  3  e.  RR* )  -> 
( m  e.  ( 1 [,) 3 )  <-> 
( m  e.  RR  /\  1  <_  m  /\  m  <  3 ) ) )
25570, 253, 254mp2an 653 . . . . . . . . . 10  |-  ( m  e.  ( 1 [,) 3 )  <->  ( m  e.  RR  /\  1  <_  m  /\  m  <  3
) )
256255simp1bi 970 . . . . . . . . 9  |-  ( m  e.  ( 1 [,) 3 )  ->  m  e.  RR )
257256adantl 452 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  m  e.  RR )
25885a1i 10 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  0  e.  RR )
25970a1i 10 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  1  e.  RR )
260 0lt1 9312 . . . . . . . . . 10  |-  0  <  1
261260a1i 10 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  0  <  1 )
262255simp2bi 971 . . . . . . . . . 10  |-  ( m  e.  ( 1 [,) 3 )  ->  1  <_  m )
263262adantl 452 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  1  <_  m )
264258, 259, 257, 261, 263ltletrd 8992 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  0  <  m )
265257, 264elrpd 10404 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  m  e.  RR+ )
266251, 265jca 518 . . . . . 6  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  ( ph  /\  m  e.  RR+ ) )
26745adantr 451 . . . . . . 7  |-  ( (
ph  /\  m  e.  RR+ )  ->  if ( S  =  0 , 
0 ,  T )  e.  CC )
26826, 267subcld 9173 . . . . . 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 )
269266, 268syl 15 . . . . 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 )
270269abscld 11934 . . . 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 )
271266, 26syl 15 . . . . . 6  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( ( X `  ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  e.  CC )
272271abscld 11934 . . . . 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 )
273249adantr 451 . . . . 5  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  ( abs `  if ( S  =  0 ,  0 ,  T ) )  e.  RR )
274272, 273readdcld 8878 . . . 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 )
275248adantr 451 . . . . 5  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  sum_ k  e.  ( 1 ... 2
) ( ( abs `  ( X `  ( L `  k )
) )  x.  (
( log `  3
)  /  k ) )  e.  RR )
276275, 273readdcld 8878 . . . 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 )
27726, 267abs2dif2d 11956 . . . . 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 ) ) ) )
278266, 277syl 15 . . . 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 ) ) ) )
27925abscld 11934 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( abs `  ( ( X `  ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  e.  RR )
2809, 279fsumrecl 12223 . . . . . . 7  |-  ( (
ph  /\  m  e.  RR+ )  ->  sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( abs `  (
( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  e.  RR )
281266, 280syl 15 . . . . . 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 )
2829, 25fsumabs 12275 . . . . . . 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 ) ) ) )
283266, 282syl 15 . . . . . 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 ) ) ) )
284 fzfid 11051 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  RR+ )  ->  ( 1 ... 2 )  e. 
Fin )
285238adantlr 695 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  ( X `  ( L `  k ) )  e.  CC )
28617adantr 451 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  m  e.  RR+ )
287243adantl 452 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  k  e.  NN )
288287nnrpd 10405 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  k  e.  RR+ )
289286, 288, 19syl2anc 642 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  if ( S  =  0 ,  m ,  k )  e.  RR+ )
290289relogcld 19990 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  ( log `  if ( S  =  0 ,  m ,  k ) )  e.  RR )
291290, 287nndivred 9810 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  (
( log `  if ( S  =  0 ,  m ,  k ) )  /  k )  e.  RR )
292291recnd 8877 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  (
( log `  if ( S  =  0 ,  m ,  k ) )  /  k )  e.  CC )
293285, 292mulcld 8871 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  (
( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  e.  CC )
294293abscld 11934 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  ( abs `  ( ( X `
 ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  e.  RR )
295284, 294fsumrecl 12223 . . . . . . . 8  |-  ( (
ph  /\  m  e.  RR+ )  ->  sum_ k  e.  ( 1 ... 2
) ( abs `  (
( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  e.  RR )
296266, 295syl 15 . . . . . . 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 )
297 fzfid 11051 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  (
1 ... 2 )  e. 
Fin )
298266, 293sylan 457 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  (
( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  e.  CC )
299298abscld 11934 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  ( abs `  ( ( X `
 ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  e.  RR )
300298absge0d 11942 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  0  <_  ( abs `  (
( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) ) )
301257flcld 10946 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  ( |_ `  m )  e.  ZZ )
302 2z 10070 . . . . . . . . . . 11  |-  2  e.  ZZ
303302a1i 10 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  2  e.  ZZ )
304255simp3bi 972 . . . . . . . . . . . . . 14  |-  ( m  e.  ( 1 [,) 3 )  ->  m  <  3 )
305304adantl 452 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  m  <  3 )
306 3nn 9894 . . . . . . . . . . . . . . 15  |-  3  e.  NN
307306nnzi 10063 . . . . . . . . . . . . . 14  |-  3  e.  ZZ
308 fllt 10954 . . . . . . . . . . . . . 14  |-  ( ( m  e.  RR  /\  3  e.  ZZ )  ->  ( m  <  3  <->  ( |_ `  m )  <  3 ) )
309257, 307, 308sylancl 643 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  (
m  <  3  <->  ( |_ `  m )  <  3
) )
310305, 309mpbid 201 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  ( |_ `  m )  <  3 )
311 df-3 9821 . . . . . . . . . . . 12  |-  3  =  ( 2  +  1 )
312310, 311syl6breq 4078 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  ( |_ `  m )  < 
( 2  +  1 ) )
313 rpre 10376 . . . . . . . . . . . . . . 15  |-  ( m  e.  RR+  ->  m  e.  RR )
314313adantl 452 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  RR+ )  ->  m  e.  RR )
315314flcld 10946 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  RR+ )  ->  ( |_ `  m )  e.  ZZ )
316 zleltp1 10084 . . . . . . . . . . . . 13  |-  ( ( ( |_ `  m
)  e.  ZZ  /\  2  e.  ZZ )  ->  ( ( |_ `  m )  <_  2  <->  ( |_ `  m )  <  ( 2  +  1 ) ) )
317315, 302, 316sylancl 643 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  RR+ )  ->  ( ( |_ `  m )  <_ 
2  <->  ( |_ `  m )  <  (
2  +  1 ) ) )
318266, 317syl 15 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  (
( |_ `  m
)  <_  2  <->  ( |_ `  m )  <  (
2  +  1 ) ) )
319312, 318mpbird 223 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  ( |_ `  m )  <_ 
2 )
320 eluz2 10252 . . . . . . . . . 10  |-  ( 2  e.  ( ZZ>= `  ( |_ `  m ) )  <-> 
( ( |_ `  m )  e.  ZZ  /\  2  e.  ZZ  /\  ( |_ `  m )  <_  2 ) )
321301, 303, 319, 320syl3anbrc 1136 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  2  e.  ( ZZ>= `  ( |_ `  m ) ) )
322 fzss2 10847 . . . . . . . . 9  |-  ( 2  e.  ( ZZ>= `  ( |_ `  m ) )  ->  ( 1 ... ( |_ `  m
) )  C_  (
1 ... 2 ) )
323321, 322syl 15 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  (
1 ... ( |_ `  m ) )  C_  ( 1 ... 2
) )
324297, 299, 300, 323fsumless 12270 . . . . . . 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 ) ) ) )
325247adantlr 695 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  (
( abs `  ( X `  ( L `  k ) ) )  x.  ( ( log `  3 )  / 
k ) )  e.  RR )
326285, 292absmuld 11952 . . . . . . . . . 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 ) ) ) )
327266, 326sylan 457 . . . . . . . . 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 ) ) ) )
328266, 291sylan 457 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  (
( log `  if ( S  =  0 ,  m ,  k ) )  /  k )  e.  RR )
329266, 290sylan 457 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  ( log `  if ( S  =  0 ,  m ,  k ) )  e.  RR )
330 log1 19955 . . . . . . . . . . . . . 14  |-  ( log `  1 )  =  0
331 elfzle1 10815 . . . . . . . . . . . . . . . 16  |-  ( k  e.  ( 1 ... 2 )  ->  1  <_  k )
332 breq2 4043 . . . . . . . . . . . . . . . . 17  |-  ( m  =  if ( S  =  0 ,  m ,  k )  -> 
( 1  <_  m  <->  1  <_  if ( S  =  0 ,  m ,  k ) ) )
333 breq2 4043 . . . . . . . . . . . . . . . . 17  |-  ( k  =  if ( S  =  0 ,  m ,  k )  -> 
( 1  <_  k  <->  1  <_  if ( S  =  0 ,  m ,  k ) ) )
334332, 333ifboth 3609 . . . . . . . . . . . . . . . 16  |-  ( ( 1  <_  m  /\  1  <_  k )  -> 
1  <_  if ( S  =  0 ,  m ,  k )
)
335263, 331, 334syl2an 463 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  1  <_  if ( S  =  0 ,  m ,  k ) )
336 1rp 10374 . . . . . . . . . . . . . . . . 17  |-  1  e.  RR+
337 logleb 19973 . . . . . . . . . . . . . . . . 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 ) ) ) )
338336, 289, 337sylancr 644 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  (
1  <_  if ( S  =  0 ,  m ,  k )  <->  ( log `  1 )  <_  ( log `  if ( S  =  0 ,  m ,  k ) ) ) )
339266, 338sylan 457 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  (
1  <_  if ( S  =  0 ,  m ,  k )  <->  ( log `  1 )  <_  ( log `  if ( S  =  0 ,  m ,  k ) ) ) )
340335, 339mpbid 201 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  ( log `  1 )  <_ 
( log `  if ( S  =  0 ,  m ,  k ) ) )
341330, 340syl5eqbrr 4073 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  0  <_  ( log `  if ( S  =  0 ,  m ,  k ) ) )
342288rpregt0d 10412 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  (
k  e.  RR  /\  0  <  k ) )
343266, 342sylan 457 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  (
k  e.  RR  /\  0  <  k ) )
344 divge0 9641 . . . . . . . . . . . . 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 ) )
345329, 341, 343, 344syl21anc 1181 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  0  <_  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )
346328, 345absidd 11921 . . . . . . . . . . 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 ) )
347346, 328eqeltrd 2370 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  ( abs `  ( ( log `  if ( S  =  0 ,  m ,  k ) )  / 
k ) )  e.  RR )
348246adantlr 695 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  (
( log `  3
)  /  k )  e.  RR )
349239adantlr 695 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  ( abs `  ( X `  ( L `  k ) ) )  e.  RR )
350285absge0d 11942 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  0  <_  ( abs `  ( X `  ( L `  k ) ) ) )
351349, 350jca 518 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  (
( abs `  ( X `  ( L `  k ) ) )  e.  RR  /\  0  <_  ( abs `  ( X `  ( L `  k ) ) ) ) )
352266, 351sylan 457 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  (
( abs `  ( X `  ( L `  k ) ) )  e.  RR  /\  0  <_  ( abs `  ( X `  ( L `  k ) ) ) ) )
353304ad2antlr 707 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  m  <  3 )
354287nnred 9777 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  k  e.  RR )
355 2re 9831 . . . . . . . . . . . . . . . . . 18  |-  2  e.  RR
356355a1i 10 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  2  e.  RR )
35766a1i 10 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  3  e.  RR )
358 elfzle2 10816 . . . . . . . . . . . . . . . . . 18  |-  ( k  e.  ( 1 ... 2 )  ->  k  <_  2 )
359358adantl 452 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  k  <_  2 )
360 2lt3 9903 . . . . . . . . . . . . . . . . . 18  |-  2  <  3
361360a1i 10 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  2  <  3 )
362354, 356, 357, 359, 361lelttrd 8990 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  k  <  3 )
363266, 362sylan 457 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  k  <  3 )
364 breq1 4042 . . . . . . . . . . . . . . . 16  |-  ( m  =  if ( S  =  0 ,  m ,  k )  -> 
( m  <  3  <->  if ( S  =  0 ,  m ,  k )  <  3 ) )
365 breq1 4042 . . . . . . . . . . . . . . . 16  |-  ( k  =  if ( S  =  0 ,  m ,  k )  -> 
( k  <  3  <->  if ( S  =  0 ,  m ,  k )  <  3 ) )
366364, 365ifboth 3609 . . . . . . . . . . . . . . 15  |-  ( ( m  <  3  /\  k  <  3 )  ->  if ( S  =  0 ,  m ,  k )  <  3 )
367353, 363, 366syl2anc 642 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  if ( S  =  0 ,  m ,  k )  <  3 )
368289rpred 10406 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  if ( S  =  0 ,  m ,  k )  e.  RR )
369 ltle 8926 . . . . . . . . . . . . . . . 16  |-  ( ( if ( S  =  0 ,  m ,  k )  e.  RR  /\  3  e.  RR )  ->  ( if ( S  =  0 ,  m ,  k )  <  3  ->  if ( S  =  0 ,  m ,  k )  <_  3 ) )
370368, 66, 369sylancl 643 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  ( if ( S  =  0 ,  m ,  k )  <  3  ->  if ( S  =  0 ,  m ,  k )  <_  3 ) )
371266, 370sylan 457 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  ( if ( S  =  0 ,  m ,  k )  <  3  ->  if ( S  =  0 ,  m ,  k )  <_  3 ) )
372367, 371mpd 14 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  if ( S  =  0 ,  m ,  k )  <_  3 )
373 logleb 19973 . . . . . . . . . . . . . . 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 ) ) )
374289, 240, 373sylancl 643 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  ( if ( S  =  0 ,  m ,  k )  <_  3  <->  ( log `  if ( S  =  0 ,  m ,  k ) )  <_ 
( log `  3
) ) )
375266, 374sylan 457 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  ( if ( S  =  0 ,  m ,  k )  <_  3  <->  ( log `  if ( S  =  0 ,  m ,  k ) )  <_ 
( log `  3
) ) )
376372, 375mpbid 201 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  ( log `  if ( S  =  0 ,  m ,  k ) )  <_  ( log `  3
) )
377242a1i 10 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  ( log `  3 )  e.  RR )
378290, 377, 288lediv1d 10448 . . . . . . . . . . . . 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 ) ) )
379266, 378sylan 457 . . . . . . . . . . . 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 ) ) )
380376, 379mpbid 201 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  (
( log `  if ( S  =  0 ,  m ,  k ) )  /  k )  <_  ( ( log `  3 )  / 
k ) )
381346, 380eqbrtrd 4059 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  ( abs `  ( ( log `  if ( S  =  0 ,  m ,  k ) )  / 
k ) )  <_ 
( ( log `  3
)  /  k ) )
382 lemul2a 9627 . . . . . . . . . 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 ) ) )
383347, 348, 352, 381, 382syl31anc 1185 . . . . . . . . 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 ) ) )
384327, 383eqbrtrd 4059 . . . . . . . 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 ) ) )
385297, 299, 325, 384fsumle 12273 . . . . . . 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 ) ) )
386281, 296, 275, 324, 385letrd 8989 . . . . . 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 ) ) )
387272, 281, 275, 283, 386letrd 8989 . . . . 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 ) ) )
38826abscld 11934 . . . . . . 7  |-  ( (
ph  /\  m  e.  RR+ )  ->  ( abs ` 
sum_ k  e.  ( 1 ... ( |_
`  m ) ) ( ( X `  ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  e.  RR )
389248adantr 451 . . . . . . 7  |-  ( (
ph  /\  m  e.  RR+ )  ->  sum_ k  e.  ( 1 ... 2
) ( ( abs `  ( X `  ( L `  k )
) )  x.  (
( log `  3
)  /  k ) )  e.  RR )
390267abscld 11934 . . . . . . 7  |-  ( (
ph  /\  m  e.  RR+ )  ->  ( abs `  if ( S  =  0 ,  0 ,  T ) )  e.  RR )
391388, 389, 390leadd1d 9382 . . . . . 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
) ) ) ) )
392266, 391syl 15 . . . . 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
)