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

Theorem dchrvmasumiflem1 20650
Description: Lemma for dchrvmasumif 20652. (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 11035 . . 3  |-  ( (
ph  /\  m  e.  RR+ )  ->  ( 1 ... ( |_ `  m ) )  e. 
Fin )
10 simpl 443 . . . . 5  |-  ( (
ph  /\  m  e.  RR+ )  ->  ph )
11 elfznn 10819 . . . . 5  |-  ( k  e.  ( 1 ... ( |_ `  m
) )  ->  k  e.  NN )
127adantr 451 . . . . . 6  |-  ( (
ph  /\  k  e.  NN )  ->  X  e.  D )
13 nnz 10045 . . . . . . 7  |-  ( k  e.  NN  ->  k  e.  ZZ )
1413adantl 452 . . . . . 6  |-  ( (
ph  /\  k  e.  NN )  ->  k  e.  ZZ )
154, 1, 5, 2, 12, 14dchrzrhcl 20484 . . . . 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 10389 . . . . . . . 8  |-  ( k  e.  ( 1 ... ( |_ `  m
) )  ->  k  e.  RR+ )
19 ifcl 3601 . . . . . . . 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 19974 . . . . . 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 9794 . . . . 5  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k )  e.  RR )
2423recnd 8861 . . . 4  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k )  e.  CC )
2516, 24mulcld 8855 . . 3  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( ( X `  ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  e.  CC )
269, 25fsumcl 12206 . 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 5525 . . . 4  |-  ( m  =  ( x  / 
d )  ->  ( |_ `  m )  =  ( |_ `  (
x  /  d ) ) )
2827oveq2d 5874 . . 3  |-  ( m  =  ( x  / 
d )  ->  (
1 ... ( |_ `  m ) )  =  ( 1 ... ( |_ `  ( x  / 
d ) ) ) )
29 ifeq1 3569 . . . . . . 7  |-  ( m  =  ( x  / 
d )  ->  if ( S  =  0 ,  m ,  k )  =  if ( S  =  0 ,  ( x  /  d ) ,  k ) )
3029fveq2d 5529 . . . . . 6  |-  ( m  =  ( x  / 
d )  ->  ( log `  if ( S  =  0 ,  m ,  k ) )  =  ( log `  if ( S  =  0 ,  ( x  / 
d ) ,  k ) ) )
3130oveq1d 5873 . . . . 5  |-  ( m  =  ( x  / 
d )  ->  (
( log `  if ( S  =  0 ,  m ,  k ) )  /  k )  =  ( ( log `  if ( S  =  0 ,  ( x  /  d ) ,  k ) )  / 
k ) )
3231oveq2d 5874 . . . 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 12180 . 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 3592 . 2  |-  ( ph  ->  if ( S  =  0 ,  C ,  E )  e.  ( 0 [,)  +oo )
)
40 0cn 8831 . . 3  |-  0  e.  CC
41 dchrvmasumif.t . . . 4  |-  ( ph  ->  seq  1 (  +  ,  K )  ~~>  T )
42 climcl 11973 . . . 4  |-  (  seq  1 (  +  ,  K )  ~~>  T  ->  T  e.  CC )
4341, 42syl 15 . . 3  |-  ( ph  ->  T  e.  CC )
44 ifcl 3601 . . 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 10263 . . . . . . . . 9  |-  NN  =  ( ZZ>= `  1 )
47 1z 10053 . . . . . . . . . 10  |-  1  e.  ZZ
4847a1i 10 . . . . . . . . 9  |-  ( ph  ->  1  e.  ZZ )
49 nncn 9754 . . . . . . . . . . . . 13  |-  ( k  e.  NN  ->  k  e.  CC )
5049adantl 452 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN )  ->  k  e.  CC )
51 nnne0 9778 . . . . . . . . . . . . 13  |-  ( k  e.  NN  ->  k  =/=  0 )
5251adantl 452 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN )  ->  k  =/=  0 )
5315, 50, 52divcld 9536 . . . . . . . . . . 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 5525 . . . . . . . . . . . . . . 15  |-  ( a  =  k  ->  ( L `  a )  =  ( L `  k ) )
5655fveq2d 5529 . . . . . . . . . . . . . 14  |-  ( a  =  k  ->  ( X `  ( L `  a ) )  =  ( X `  ( L `  k )
) )
57 id 19 . . . . . . . . . . . . . 14  |-  ( a  =  k  ->  a  =  k )
5856, 57oveq12d 5876 . . . . . . . . . . . . 13  |-  ( a  =  k  ->  (
( X `  ( L `  a )
)  /  a )  =  ( ( X `
 ( L `  k ) )  / 
k ) )
5958cbvmptv 4111 . . . . . . . . . . . 12  |-  ( a  e.  NN  |->  ( ( X `  ( L `
 a ) )  /  a ) )  =  ( k  e.  NN  |->  ( ( X `
 ( L `  k ) )  / 
k ) )
6054, 59eqtri 2303 . . . . . . . . . . 11  |-  F  =  ( k  e.  NN  |->  ( ( X `  ( L `  k ) )  /  k ) )
6153, 60fmptd 5684 . . . . . . . . . 10  |-  ( ph  ->  F : NN --> CC )
62 ffvelrn 5663 . . . . . . . . . 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 11074 . . . . . . . 8  |-  ( ph  ->  seq  1 (  +  ,  F ) : NN --> CC )
6564ad2antrr 706 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  ( 3 [,)  +oo ) )  /\  S  =  0 )  ->  seq  1 (  +  ,  F ) : NN --> CC )
66 3re 9817 . . . . . . . . . . 11  |-  3  e.  RR
67 elicopnf 10739 . . . . . . . . . . 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 8837 . . . . . . . . . . 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 9888 . . . . . . . . . . . 12  |-  1  <  3
7470, 66, 73ltleii 8941 . . . . . . . . . . 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 8973 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  1  <_  m )
78 flge1nn 10949 . . . . . . . . 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 5663 . . . . . . 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 11918 . . . . 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 8838 . . . . . . . . . . 11  |-  0  e.  RR
8685a1i 10 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  0  e.  RR )
87 3pos 9830 . . . . . . . . . . 11  |-  0  <  3
8887a1i 10 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  0  <  3 )
8986, 72, 69, 88, 76ltletrd 8976 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  0  <  m )
9069, 89elrpd 10388 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  m  e.  RR+ )
9184, 90jca 518 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  ( ph  /\  m  e.  RR+ ) )
92 elrege0 10746 . . . . . . . . . 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 10381 . . . . . . . 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 19974 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  ( log `  m )  e.  RR )
10069, 77logge0d 19981 . . . . . . 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 5866 . . . . . . . 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 9146 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  (
(  seq  1 (  +  ,  F ) `
 ( |_ `  m ) )  - 
0 )  =  (  seq  1 (  +  ,  F ) `  ( |_ `  m ) ) )
107103, 106sylan9eqr 2337 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  ( 3 [,)  +oo ) )  /\  S  =  0 )  -> 
( (  seq  1
(  +  ,  F
) `  ( |_ `  m ) )  -  S )  =  (  seq  1 (  +  ,  F ) `  ( |_ `  m ) ) )
108107fveq2d 5529 . . . . . 6  |-  ( ( ( ph  /\  m  e.  ( 3 [,)  +oo ) )  /\  S  =  0 )  -> 
( abs `  (
(  seq  1 (  +  ,  F ) `
 ( |_ `  m ) )  -  S ) )  =  ( abs `  (  seq  1 (  +  ,  F ) `  ( |_ `  m ) ) ) )
109 elicopnf 10739 . . . . . . . . . 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 5525 . . . . . . . . . . . . 13  |-  ( y  =  m  ->  ( |_ `  y )  =  ( |_ `  m
) )
115114fveq2d 5529 . . . . . . . . . . . 12  |-  ( y  =  m  ->  (  seq  1 (  +  ,  F ) `  ( |_ `  y ) )  =  (  seq  1
(  +  ,  F
) `  ( |_ `  m ) ) )
116115oveq1d 5873 . . . . . . . . . . 11  |-  ( y  =  m  ->  (
(  seq  1 (  +  ,  F ) `
 ( |_ `  y ) )  -  S )  =  ( (  seq  1 (  +  ,  F ) `
 ( |_ `  m ) )  -  S ) )
117116fveq2d 5529 . . . . . . . . . 10  |-  ( y  =  m  ->  ( abs `  ( (  seq  1 (  +  ,  F ) `  ( |_ `  y ) )  -  S ) )  =  ( abs `  (
(  seq  1 (  +  ,  F ) `
 ( |_ `  m ) )  -  S ) ) )
118 oveq2 5866 . . . . . . . . . 10  |-  ( y  =  m  ->  ( C  /  y )  =  ( C  /  m
) )
119117, 118breq12d 4036 . . . . . . . . 9  |-  ( y  =  m  ->  (
( abs `  (
(  seq  1 (  +  ,  F ) `
 ( |_ `  y ) )  -  S ) )  <_ 
( C  /  y
)  <->  ( abs `  (
(  seq  1 (  +  ,  F ) `
 ( |_ `  m ) )  -  S ) )  <_ 
( C  /  m
) ) )
120119rspcv 2880 . . . . . . . 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 4045 . . . . 5  |-  ( ( ( ph  /\  m  e.  ( 3 [,)  +oo ) )  /\  S  =  0 )  -> 
( abs `  (  seq  1 (  +  ,  F ) `  ( |_ `  m ) ) )  <_  ( C  /  m ) )
124 lemul2a 9611 . . . . 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 3571 . . . . . . . . . . . . . . 15  |-  ( S  =  0  ->  if ( S  =  0 ,  m ,  k )  =  m )
127126fveq2d 5529 . . . . . . . . . . . . . 14  |-  ( S  =  0  ->  ( log `  if ( S  =  0 ,  m ,  k ) )  =  ( log `  m
) )
128127oveq1d 5873 . . . . . . . . . . . . 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 5874 . . . . . . . . . . 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 19932 . . . . . . . . . . . . . . 15  |-  ( m  e.  RR+  ->  ( log `  m )  e.  RR )
133132adantl 452 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  RR+ )  ->  ( log `  m )  e.  RR )
134133recnd 8861 . . . . . . . . . . . . 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 9762 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  /\  k  e.  ( 1 ... ( |_
`  m ) ) )  ->  k  e.  CC )
138136nnne0d 9790 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  /\  k  e.  ( 1 ... ( |_
`  m ) ) )  ->  k  =/=  0 )
139131, 135, 137, 138div12d 9572 . . . . . . . . . . 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 2315 . . . . . . . . . 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 12176 . . . . . . . . 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 3571 . . . . . . . . . . 11  |-  ( S  =  0  ->  if ( S  =  0 ,  0 ,  T
)  =  0 )
143142oveq2d 5874 . . . . . . . . . 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 9146 . . . . . . . . . 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 2337 . . . . . . . . 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 5883 . . . . . . . . . . . . . 14  |-  ( ( X `  ( L `
 k ) )  /  k )  e. 
_V
14758, 54, 146fvmpt 5602 . . . . . . . . . . . . 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 2358 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( ( X `  ( L `  k ) )  / 
k )  e.  CC )
1529, 134, 151fsummulc2 12246 . . . . . . . . . 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 2325 . . . . . . . 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 2373 . . . . . . . . . 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 12203 . . . . . . . . 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 5874 . . . . . . 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 2315 . . . . . 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 5529 . . . . 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 8861 . . . . . . 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 11936 . . . . 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 11905 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  ( abs `  ( log `  m
) )  =  ( log `  m ) )
169168oveq1d 5873 . . . . . 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 2319 . . . 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 3571 . . . . . . . 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 5873 . . . . . 6  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  -> 
( if ( S  =  0 ,  C ,  E )  x.  (
( log `  m
)  /  m ) )  =  ( C  x.  ( ( log `  m )  /  m
) ) )
17594recnd 8861 . . . . . . . 8  |-  ( ph  ->  C  e.  CC )
176175ad2antrr 706 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  ->  C  e.  CC )
177 rpcnne0 10371 . . . . . . . 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 9446 . . . . . . 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 2315 . . . . 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 4053 . . 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 5529 . . . . . . . . . 10  |-  ( y  =  m  ->  (  seq  1 (  +  ,  K ) `  ( |_ `  y ) )  =  (  seq  1
(  +  ,  K
) `  ( |_ `  m ) ) )
186185oveq1d 5873 . . . . . . . . 9  |-  ( y  =  m  ->  (
(  seq  1 (  +  ,  K ) `
 ( |_ `  y ) )  -  T )  =  ( (  seq  1 (  +  ,  K ) `
 ( |_ `  m ) )  -  T ) )
187186fveq2d 5529 . . . . . . . 8  |-  ( y  =  m  ->  ( abs `  ( (  seq  1 (  +  ,  K ) `  ( |_ `  y ) )  -  T ) )  =  ( abs `  (
(  seq  1 (  +  ,  K ) `
 ( |_ `  m ) )  -  T ) ) )
188 fveq2 5525 . . . . . . . . . 10  |-  ( y  =  m  ->  ( log `  y )  =  ( log `  m
) )
189 id 19 . . . . . . . . . 10  |-  ( y  =  m  ->  y  =  m )
190188, 189oveq12d 5876 . . . . . . . . 9  |-  ( y  =  m  ->  (
( log `  y
)  /  y )  =  ( ( log `  m )  /  m
) )
191190oveq2d 5874 . . . . . . . 8  |-  ( y  =  m  ->  ( E  x.  ( ( log `  y )  / 
y ) )  =  ( E  x.  (
( log `  m
)  /  m ) ) )
192187, 191breq12d 4036 . . . . . . 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 2883 . . . . . 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 5525 . . . . . . . . . . . 12  |-  ( a  =  k  ->  ( log `  a )  =  ( log `  k
) )
197196, 57oveq12d 5876 . . . . . . . . . . 11  |-  ( a  =  k  ->  (
( log `  a
)  /  a )  =  ( ( log `  k )  /  k
) )
19856, 197oveq12d 5876 . . . . . . . . . 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 5883 . . . . . . . . . 10  |-  ( ( X `  ( L `
 k ) )  x.  ( ( log `  k )  /  k
) )  e.  _V
201198, 199, 200fvmpt 5602 . . . . . . . . 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 3573 . . . . . . . . . . . . 13  |-  ( S  =/=  0  ->  if ( S  =  0 ,  m ,  k )  =  k )
204203fveq2d 5529 . . . . . . . . . . . 12  |-  ( S  =/=  0  ->  ( log `  if ( S  =  0 ,  m ,  k ) )  =  ( log `  k
) )
205204oveq1d 5873 . . . . . . . . . . 11  |-  ( S  =/=  0  ->  (
( log `  if ( S  =  0 ,  m ,  k ) )  /  k )  =  ( ( log `  k )  /  k
) )
206205oveq2d 5874 . . . . . . . . . 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 2288 . . . . . . . 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 2337 . . . . . . 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 10363 . . . . . . . . . . . . . . . 16  |-  ( k  e.  NN  ->  k  e.  RR+ )
212211adantl 452 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  NN )  ->  k  e.  RR+ )
213212relogcld 19974 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN )  ->  ( log `  k )  e.  RR )
214213recnd 8861 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  NN )  ->  ( log `  k )  e.  CC )
215214, 50, 52divcld 9536 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( log `  k )  /  k )  e.  CC )
21615, 215mulcld 8855 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( X `  ( L `
 k ) )  x.  ( ( log `  k )  /  k
) )  e.  CC )
217198cbvmptv 4111 . . . . . . . . . . . 12  |-  ( a  e.  NN  |->  ( ( X `  ( L `
 a ) )  x.  ( ( log `  a )  /  a
) ) )  =  ( k  e.  NN  |->  ( ( X `  ( L `  k ) )  x.  ( ( log `  k )  /  k ) ) )
218199, 217eqtri 2303 . . . . . . . . . . 11  |-  K  =  ( k  e.  NN  |->  ( ( X `  ( L `  k ) )  x.  ( ( log `  k )  /  k ) ) )
219216, 218fmptd 5684 . . . . . . . . . 10  |-  ( ph  ->  K : NN --> CC )
220219ad2antrr 706 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( 3 [,)  +oo ) )  /\  S  =/=  0 )  ->  K : NN --> CC )
221 ffvelrn 5663 . . . . . . . . 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 2358 . . . . . . 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 12203 . . . . . 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 3573 . . . . . . 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 5876 . . . . 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 5529 . . . 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 3573 . . . . . 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 5873 . . . 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 4053 . . 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 2524 . 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 11035 . . . 4  |-  ( ph  ->  ( 1 ... 2
)  e.  Fin )
2357adantr 451 . . . . . . 7  |-  ( (
ph  /\  k  e.  ( 1 ... 2
) )  ->  X  e.  D )
236 elfzelz 10798 . . . . . . . 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 20484 . . . . . 6  |-  ( (
ph  /\  k  e.  ( 1 ... 2
) )  ->  ( X `  ( L `  k ) )  e.  CC )
239238abscld 11918 . . . . 5  |-  ( (
ph  /\  k  e.  ( 1 ... 2
) )  ->  ( abs `  ( X `  ( L `  k ) ) )  e.  RR )
24066, 87elrpii 10357 . . . . . . 7  |-  3  e.  RR+
241 relogcl 19932 . . . . . . 7  |-  ( 3  e.  RR+  ->  ( log `  3 )  e.  RR )
242240, 241ax-mp 8 . . . . . 6  |-  ( log `  3 )  e.  RR
243 elfznn 10819 . . . . . . 7  |-  ( k  e.  ( 1 ... 2 )  ->  k  e.  NN )
244243adantl 452 . . . . . 6  |-  ( (
ph  /\  k  e.  ( 1 ... 2
) )  ->  k  e.  NN )
245 nndivre 9781 . . . . . 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 8863 . . . 4  |-  ( (
ph  /\  k  e.  ( 1 ... 2
) )  ->  (
( abs `  ( X `  ( L `  k ) ) )  x.  ( ( log `  3 )  / 
k ) )  e.  RR )
248234, 247fsumrecl 12207 . . 3  |-  ( ph  -> 
sum_ k  e.  ( 1 ... 2 ) ( ( abs `  ( X `  ( L `  k ) ) )  x.  ( ( log `  3 )  / 
k ) )  e.  RR )
24945abscld 11918 . . 3  |-  ( ph  ->  ( abs `  if ( S  =  0 ,  0 ,  T
) )  e.  RR )
250248, 249readdcld 8862 . 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 8877 . . . . . . . . . . . 12  |-  ( 3  e.  RR  ->  3  e.  RR* )
25366, 252ax-mp 8 . . . . . . . . . . 11  |-  3  e.  RR*
254 elico2 10714 . . . . . . . . . . 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 9296 . . . . . . . . . 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 8976 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  0  <  m )
265257, 264elrpd 10388 . . . . . . 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 9157 . . . . . 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 11918 . . . 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 11918 . . . . 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 8862 . . . 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 8862 . . . 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 11940 . . . . 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 11918 . . . . . . . 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 12207 . . . . . . 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 12259 . . . . . . 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 11035 . . . . . . . . 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 10389 . . . . . . . . . . . . . . 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 19974 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  ( log `  if ( S  =  0 ,  m ,  k ) )  e.  RR )
291290, 287nndivred 9794 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  (
( log `  if ( S  =  0 ,  m ,  k ) )  /  k )  e.  RR )
292291recnd 8861 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  (
( log `  if ( S  =  0 ,  m ,  k ) )  /  k )  e.  CC )
293285, 292mulcld 8855 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  (
( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  e.  CC )
294293abscld 11918 . . . . . . . . 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 12207 . . . . . . . 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 11035 . . . . . . . 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 11918 . . . . . . . 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 11926 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  0  <_  ( abs `  (
( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) ) )
301257flcld 10930 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  ( |_ `  m )  e.  ZZ )
302 2z 10054 . . . . . . . . . . 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 9878 . . . . . . . . . . . . . . 15  |-  3  e.  NN
307306nnzi 10047 . . . . . . . . . . . . . 14  |-  3  e.  ZZ
308 fllt 10938 . . . . . . . . . . . . . 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 9805 . . . . . . . . . . . 12  |-  3  =  ( 2  +  1 )
312310, 311syl6breq 4062 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  ( |_ `  m )  < 
( 2  +  1 ) )
313 rpre 10360 . . . . . . . . . . . . . . 15  |-  ( m  e.  RR+  ->  m  e.  RR )
314313adantl 452 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  RR+ )  ->  m  e.  RR )
315314flcld 10930 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  RR+ )  ->  ( |_ `  m )  e.  ZZ )
316 zleltp1 10068 . . . . . . . . . . . . 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 10236 . . . . . . . . . 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 10831 . . . . . . . . 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 12254 . . . . . . 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 11936 . . . . . . . . . 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 19939 . . . . . . . . . . . . . 14  |-  ( log `  1 )  =  0
331 elfzle1 10799 . . . . . . . . . . . . . . . 16  |-  ( k  e.  ( 1 ... 2 )  ->  1  <_  k )
332 breq2 4027 . . . . . . . . . . . . . . . . 17  |-  ( m  =  if ( S  =  0 ,  m ,  k )  -> 
( 1  <_  m  <->  1  <_  if ( S  =  0 ,  m ,  k ) ) )
333 breq2 4027 . . . . . . . . . . . . . . . . 17  |-  ( k  =  if ( S  =  0 ,  m ,  k )  -> 
( 1  <_  k  <->  1  <_  if ( S  =  0 ,  m ,  k ) ) )
334332, 333ifboth 3596 . . . . . . . . . . . . . . . 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 10358 . . . . . . . . . . . . . . . . 17  |-  1  e.  RR+
337 logleb 19957 . . . . . . . . . . . . . . . . 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 4057 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  0  <_  ( log `  if ( S  =  0 ,  m ,  k ) ) )
342288rpregt0d 10396 . . . . . . . . . . . . . 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 9625 . . . . . . . . . . . . 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 11905 . . . . . . . . . . 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 2357 . . . . . . . . . 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 11926 . . . . . . . . . . . 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 9761 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  k  e.  RR )
355 2re 9815 . . . . . . . . . . . . . . . . . 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 10800 . . . . . . . . . . . . . . . . . 18  |-  ( k  e.  ( 1 ... 2 )  ->  k  <_  2 )
359358adantl 452 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  k  <_  2 )
360 2lt3 9887 . . . . . . . . . . . . . . . . . 18  |-  2  <  3
361360a1i 10 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  2  <  3 )
362354, 356, 357, 359, 361lelttrd 8974 . . . . . . . . . . . . . . . 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 4026 . . . . . . . . . . . . . . . 16  |-  ( m  =  if ( S  =  0 ,  m ,  k )  -> 
( m  <  3  <->  if ( S  =  0 ,  m ,  k )  <  3 ) )
365 breq1 4026 . . . . . . . . . . . . . . . 16  |-  ( k  =  if ( S  =  0 ,  m ,  k )  -> 
( k  <  3  <->  if ( S  =  0 ,  m ,  k )  <  3 ) )
366364, 365ifboth 3596 . . . . . . . . . . . . . . 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 10390 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  if ( S  =  0 ,  m ,  k )  e.  RR )
369 ltle 8910 . . . . . . . . . . . . . . . 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 19957 . . . . . . . . . . . . . . 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 10432 . . . . . . . . . . . . 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 4043 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  ( abs `  ( ( log `  if ( S  =  0 ,  m ,  k ) )  / 
k ) )  <_ 
( ( log `  3
)  /  k ) )
382 lemul2a 9611 . . . . . . . . . 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 4043 . . . . . . . 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 12257 . . . . . . 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 8973 . . . . . 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 8973 . . . . 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 11918 . . . . . . 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 11918 . . . . . . 7  |-  ( (
ph  /\  m  e.  RR+ )  ->  ( abs `  if ( S  =  0 ,  0 ,  T ) )  e.  RR )
391388, 389, 390leadd1d 9366 . . . . . 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  =