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

Theorem dchrvmasumiflem1 21187
Description: Lemma for dchrvmasumif 21189. (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 11304 . . 3  |-  ( (
ph  /\  m  e.  RR+ )  ->  ( 1 ... ( |_ `  m ) )  e. 
Fin )
10 simpl 444 . . . . 5  |-  ( (
ph  /\  m  e.  RR+ )  ->  ph )
11 elfznn 11072 . . . . 5  |-  ( k  e.  ( 1 ... ( |_ `  m
) )  ->  k  e.  NN )
127adantr 452 . . . . . 6  |-  ( (
ph  /\  k  e.  NN )  ->  X  e.  D )
13 nnz 10295 . . . . . . 7  |-  ( k  e.  NN  ->  k  e.  ZZ )
1413adantl 453 . . . . . 6  |-  ( (
ph  /\  k  e.  NN )  ->  k  e.  ZZ )
154, 1, 5, 2, 12, 14dchrzrhcl 21021 . . . . 5  |-  ( (
ph  /\  k  e.  NN )  ->  ( X `
 ( L `  k ) )  e.  CC )
1610, 11, 15syl2an 464 . . . 4  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( X `  ( L `  k
) )  e.  CC )
17 simpr 448 . . . . . . . 8  |-  ( (
ph  /\  m  e.  RR+ )  ->  m  e.  RR+ )
1811nnrpd 10639 . . . . . . . 8  |-  ( k  e.  ( 1 ... ( |_ `  m
) )  ->  k  e.  RR+ )
19 ifcl 3767 . . . . . . . 8  |-  ( ( m  e.  RR+  /\  k  e.  RR+ )  ->  if ( S  =  0 ,  m ,  k )  e.  RR+ )
2017, 18, 19syl2an 464 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  if ( S  =  0 ,  m ,  k )  e.  RR+ )
2120relogcld 20510 . . . . . 6  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( log `  if ( S  =  0 ,  m ,  k ) )  e.  RR )
2211adantl 453 . . . . . 6  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  k  e.  NN )
2321, 22nndivred 10040 . . . . 5  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k )  e.  RR )
2423recnd 9106 . . . 4  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k )  e.  CC )
2516, 24mulcld 9100 . . 3  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( ( X `  ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  e.  CC )
269, 25fsumcl 12519 . 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 5720 . . . 4  |-  ( m  =  ( x  / 
d )  ->  ( |_ `  m )  =  ( |_ `  (
x  /  d ) ) )
2827oveq2d 6089 . . 3  |-  ( m  =  ( x  / 
d )  ->  (
1 ... ( |_ `  m ) )  =  ( 1 ... ( |_ `  ( x  / 
d ) ) ) )
29 ifeq1 3735 . . . . . . 7  |-  ( m  =  ( x  / 
d )  ->  if ( S  =  0 ,  m ,  k )  =  if ( S  =  0 ,  ( x  /  d ) ,  k ) )
3029fveq2d 5724 . . . . . 6  |-  ( m  =  ( x  / 
d )  ->  ( log `  if ( S  =  0 ,  m ,  k ) )  =  ( log `  if ( S  =  0 ,  ( x  / 
d ) ,  k ) ) )
3130oveq1d 6088 . . . . 5  |-  ( m  =  ( x  / 
d )  ->  (
( log `  if ( S  =  0 ,  m ,  k ) )  /  k )  =  ( ( log `  if ( S  =  0 ,  ( x  /  d ) ,  k ) )  / 
k ) )
3231oveq2d 6089 . . . 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 452 . . 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 12493 . 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 452 . . 3  |-  ( (
ph  /\  S  = 
0 )  ->  C  e.  ( 0 [,)  +oo ) )
37 dchrvmasumif.e . . . 4  |-  ( ph  ->  E  e.  ( 0 [,)  +oo ) )
3837adantr 452 . . 3  |-  ( (
ph  /\  -.  S  =  0 )  ->  E  e.  ( 0 [,)  +oo ) )
3936, 38ifclda 3758 . 2  |-  ( ph  ->  if ( S  =  0 ,  C ,  E )  e.  ( 0 [,)  +oo )
)
40 0cn 9076 . . 3  |-  0  e.  CC
41 dchrvmasumif.t . . . 4  |-  ( ph  ->  seq  1 (  +  ,  K )  ~~>  T )
42 climcl 12285 . . . 4  |-  (  seq  1 (  +  ,  K )  ~~>  T  ->  T  e.  CC )
4341, 42syl 16 . . 3  |-  ( ph  ->  T  e.  CC )
44 ifcl 3767 . . 3  |-  ( ( 0  e.  CC  /\  T  e.  CC )  ->  if ( S  =  0 ,  0 ,  T )  e.  CC )
4540, 43, 44sylancr 645 . 2  |-  ( ph  ->  if ( S  =  0 ,  0 ,  T )  e.  CC )
46 nnuz 10513 . . . . . . . . 9  |-  NN  =  ( ZZ>= `  1 )
47 1z 10303 . . . . . . . . . 10  |-  1  e.  ZZ
4847a1i 11 . . . . . . . . 9  |-  ( ph  ->  1  e.  ZZ )
49 nncn 10000 . . . . . . . . . . . . 13  |-  ( k  e.  NN  ->  k  e.  CC )
5049adantl 453 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN )  ->  k  e.  CC )
51 nnne0 10024 . . . . . . . . . . . . 13  |-  ( k  e.  NN  ->  k  =/=  0 )
5251adantl 453 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN )  ->  k  =/=  0 )
5315, 50, 52divcld 9782 . . . . . . . . . . 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 5720 . . . . . . . . . . . . . . 15  |-  ( a  =  k  ->  ( L `  a )  =  ( L `  k ) )
5655fveq2d 5724 . . . . . . . . . . . . . 14  |-  ( a  =  k  ->  ( X `  ( L `  a ) )  =  ( X `  ( L `  k )
) )
57 id 20 . . . . . . . . . . . . . 14  |-  ( a  =  k  ->  a  =  k )
5856, 57oveq12d 6091 . . . . . . . . . . . . 13  |-  ( a  =  k  ->  (
( X `  ( L `  a )
)  /  a )  =  ( ( X `
 ( L `  k ) )  / 
k ) )
5958cbvmptv 4292 . . . . . . . . . . . 12  |-  ( a  e.  NN  |->  ( ( X `  ( L `
 a ) )  /  a ) )  =  ( k  e.  NN  |->  ( ( X `
 ( L `  k ) )  / 
k ) )
6054, 59eqtri 2455 . . . . . . . . . . 11  |-  F  =  ( k  e.  NN  |->  ( ( X `  ( L `  k ) )  /  k ) )
6153, 60fmptd 5885 . . . . . . . . . 10  |-  ( ph  ->  F : NN --> CC )
62 ffvelrn 5860 . . . . . . . . . 10  |-  ( ( F : NN --> CC  /\  k  e.  NN )  ->  ( F `  k
)  e.  CC )
6361, 62sylan 458 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  NN )  ->  ( F `
 k )  e.  CC )
6446, 48, 63serf 11343 . . . . . . . 8  |-  ( ph  ->  seq  1 (  +  ,  F ) : NN --> CC )
6564ad2antrr 707 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  ( 3 [,)  +oo ) )  /\  S  =  0 )  ->  seq  1 (  +  ,  F ) : NN --> CC )
66 3re 10063 . . . . . . . . . . 11  |-  3  e.  RR
67 elicopnf 10992 . . . . . . . . . . 11  |-  ( 3  e.  RR  ->  (
m  e.  ( 3 [,)  +oo )  <->  ( m  e.  RR  /\  3  <_  m ) ) )
6866, 67mp1i 12 . . . . . . . . . 10  |-  ( ph  ->  ( m  e.  ( 3 [,)  +oo )  <->  ( m  e.  RR  /\  3  <_  m ) ) )
6968simprbda 607 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  m  e.  RR )
70 1re 9082 . . . . . . . . . . 11  |-  1  e.  RR
7170a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  1  e.  RR )
7266a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  3  e.  RR )
73 1lt3 10136 . . . . . . . . . . . 12  |-  1  <  3
7470, 66, 73ltleii 9188 . . . . . . . . . . 11  |-  1  <_  3
7574a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  1  <_  3 )
7668simplbda 608 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  3  <_  m )
7771, 72, 69, 75, 76letrd 9219 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  1  <_  m )
78 flge1nn 11218 . . . . . . . . 9  |-  ( ( m  e.  RR  /\  1  <_  m )  -> 
( |_ `  m
)  e.  NN )
7969, 77, 78syl2anc 643 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  ( |_ `  m )  e.  NN )
8079adantr 452 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  ( 3 [,)  +oo ) )  /\  S  =  0 )  -> 
( |_ `  m
)  e.  NN )
8165, 80ffvelrnd 5863 . . . . . 6  |-  ( ( ( ph  /\  m  e.  ( 3 [,)  +oo ) )  /\  S  =  0 )  -> 
(  seq  1 (  +  ,  F ) `
 ( |_ `  m ) )  e.  CC )
8281abscld 12230 . . . . 5  |-  ( ( ( ph  /\  m  e.  ( 3 [,)  +oo ) )  /\  S  =  0 )  -> 
( abs `  (  seq  1 (  +  ,  F ) `  ( |_ `  m ) ) )  e.  RR )
83 simpl 444 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  ph )
84 0re 9083 . . . . . . . . . . 11  |-  0  e.  RR
8584a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  0  e.  RR )
86 3pos 10076 . . . . . . . . . . 11  |-  0  <  3
8786a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  0  <  3 )
8885, 72, 69, 87, 76ltletrd 9222 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  0  <  m )
8969, 88elrpd 10638 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  m  e.  RR+ )
9083, 89jca 519 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  ( ph  /\  m  e.  RR+ ) )
91 elrege0 10999 . . . . . . . . . 10  |-  ( C  e.  ( 0 [,) 
+oo )  <->  ( C  e.  RR  /\  0  <_  C ) )
9291simplbi 447 . . . . . . . . 9  |-  ( C  e.  ( 0 [,) 
+oo )  ->  C  e.  RR )
9335, 92syl 16 . . . . . . . 8  |-  ( ph  ->  C  e.  RR )
94 rerpdivcl 10631 . . . . . . . 8  |-  ( ( C  e.  RR  /\  m  e.  RR+ )  -> 
( C  /  m
)  e.  RR )
9593, 94sylan 458 . . . . . . 7  |-  ( (
ph  /\  m  e.  RR+ )  ->  ( C  /  m )  e.  RR )
9690, 95syl 16 . . . . . 6  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  ( C  /  m )  e.  RR )
9796adantr 452 . . . . 5  |-  ( ( ( ph  /\  m  e.  ( 3 [,)  +oo ) )  /\  S  =  0 )  -> 
( C  /  m
)  e.  RR )
9889relogcld 20510 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  ( log `  m )  e.  RR )
9969, 77logge0d 20517 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  0  <_  ( log `  m
) )
10098, 99jca 519 . . . . . 6  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  (
( log `  m
)  e.  RR  /\  0  <_  ( log `  m
) ) )
101100adantr 452 . . . . 5  |-  ( ( ( ph  /\  m  e.  ( 3 [,)  +oo ) )  /\  S  =  0 )  -> 
( ( log `  m
)  e.  RR  /\  0  <_  ( log `  m
) ) )
102 oveq2 6081 . . . . . . . 8  |-  ( S  =  0  ->  (
(  seq  1 (  +  ,  F ) `
 ( |_ `  m ) )  -  S )  =  ( (  seq  1 (  +  ,  F ) `
 ( |_ `  m ) )  - 
0 ) )
10364adantr 452 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  seq  1 (  +  ,  F ) : NN --> CC )
104103, 79ffvelrnd 5863 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  (  seq  1 (  +  ,  F ) `  ( |_ `  m ) )  e.  CC )
105104subid1d 9392 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  (
(  seq  1 (  +  ,  F ) `
 ( |_ `  m ) )  - 
0 )  =  (  seq  1 (  +  ,  F ) `  ( |_ `  m ) ) )
106102, 105sylan9eqr 2489 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  ( 3 [,)  +oo ) )  /\  S  =  0 )  -> 
( (  seq  1
(  +  ,  F
) `  ( |_ `  m ) )  -  S )  =  (  seq  1 (  +  ,  F ) `  ( |_ `  m ) ) )
107106fveq2d 5724 . . . . . 6  |-  ( ( ( ph  /\  m  e.  ( 3 [,)  +oo ) )  /\  S  =  0 )  -> 
( abs `  (
(  seq  1 (  +  ,  F ) `
 ( |_ `  m ) )  -  S ) )  =  ( abs `  (  seq  1 (  +  ,  F ) `  ( |_ `  m ) ) ) )
108 elicopnf 10992 . . . . . . . . . 10  |-  ( 1  e.  RR  ->  (
m  e.  ( 1 [,)  +oo )  <->  ( m  e.  RR  /\  1  <_  m ) ) )
10970, 108ax-mp 8 . . . . . . . . 9  |-  ( m  e.  ( 1 [,) 
+oo )  <->  ( m  e.  RR  /\  1  <_  m ) )
11069, 77, 109sylanbrc 646 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  m  e.  ( 1 [,)  +oo ) )
111 dchrvmasumif.1 . . . . . . . . 9  |-  ( ph  ->  A. y  e.  ( 1 [,)  +oo )
( abs `  (
(  seq  1 (  +  ,  F ) `
 ( |_ `  y ) )  -  S ) )  <_ 
( C  /  y
) )
112111adantr 452 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  A. y  e.  ( 1 [,)  +oo ) ( abs `  (
(  seq  1 (  +  ,  F ) `
 ( |_ `  y ) )  -  S ) )  <_ 
( C  /  y
) )
113 fveq2 5720 . . . . . . . . . . . . 13  |-  ( y  =  m  ->  ( |_ `  y )  =  ( |_ `  m
) )
114113fveq2d 5724 . . . . . . . . . . . 12  |-  ( y  =  m  ->  (  seq  1 (  +  ,  F ) `  ( |_ `  y ) )  =  (  seq  1
(  +  ,  F
) `  ( |_ `  m ) ) )
115114oveq1d 6088 . . . . . . . . . . 11  |-  ( y  =  m  ->  (
(  seq  1 (  +  ,  F ) `
 ( |_ `  y ) )  -  S )  =  ( (  seq  1 (  +  ,  F ) `
 ( |_ `  m ) )  -  S ) )
116115fveq2d 5724 . . . . . . . . . 10  |-  ( y  =  m  ->  ( abs `  ( (  seq  1 (  +  ,  F ) `  ( |_ `  y ) )  -  S ) )  =  ( abs `  (
(  seq  1 (  +  ,  F ) `
 ( |_ `  m ) )  -  S ) ) )
117 oveq2 6081 . . . . . . . . . 10  |-  ( y  =  m  ->  ( C  /  y )  =  ( C  /  m
) )
118116, 117breq12d 4217 . . . . . . . . 9  |-  ( y  =  m  ->  (
( abs `  (
(  seq  1 (  +  ,  F ) `
 ( |_ `  y ) )  -  S ) )  <_ 
( C  /  y
)  <->  ( abs `  (
(  seq  1 (  +  ,  F ) `
 ( |_ `  m ) )  -  S ) )  <_ 
( C  /  m
) ) )
119118rspcv 3040 . . . . . . . 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
) ) )
120110, 112, 119sylc 58 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  ( abs `  ( (  seq  1 (  +  ,  F ) `  ( |_ `  m ) )  -  S ) )  <_  ( C  /  m ) )
121120adantr 452 . . . . . 6  |-  ( ( ( ph  /\  m  e.  ( 3 [,)  +oo ) )  /\  S  =  0 )  -> 
( abs `  (
(  seq  1 (  +  ,  F ) `
 ( |_ `  m ) )  -  S ) )  <_ 
( C  /  m
) )
122107, 121eqbrtrrd 4226 . . . . 5  |-  ( ( ( ph  /\  m  e.  ( 3 [,)  +oo ) )  /\  S  =  0 )  -> 
( abs `  (  seq  1 (  +  ,  F ) `  ( |_ `  m ) ) )  <_  ( C  /  m ) )
123 lemul2a 9857 . . . . 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
) ) )
12482, 97, 101, 122, 123syl31anc 1187 . . . 4  |-  ( ( ( ph  /\  m  e.  ( 3 [,)  +oo ) )  /\  S  =  0 )  -> 
( ( log `  m
)  x.  ( abs `  (  seq  1
(  +  ,  F
) `  ( |_ `  m ) ) ) )  <_  ( ( log `  m )  x.  ( C  /  m
) ) )
125 iftrue 3737 . . . . . . . . . . . . . . 15  |-  ( S  =  0  ->  if ( S  =  0 ,  m ,  k )  =  m )
126125fveq2d 5724 . . . . . . . . . . . . . 14  |-  ( S  =  0  ->  ( log `  if ( S  =  0 ,  m ,  k ) )  =  ( log `  m
) )
127126oveq1d 6088 . . . . . . . . . . . . 13  |-  ( S  =  0  ->  (
( log `  if ( S  =  0 ,  m ,  k ) )  /  k )  =  ( ( log `  m )  /  k
) )
128127ad2antlr 708 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  /\  k  e.  ( 1 ... ( |_
`  m ) ) )  ->  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k )  =  ( ( log `  m
)  /  k ) )
129128oveq2d 6089 . . . . . . . . . . 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
) ) )
13016adantlr 696 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  /\  k  e.  ( 1 ... ( |_
`  m ) ) )  ->  ( X `  ( L `  k
) )  e.  CC )
131 relogcl 20465 . . . . . . . . . . . . . . 15  |-  ( m  e.  RR+  ->  ( log `  m )  e.  RR )
132131adantl 453 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  RR+ )  ->  ( log `  m )  e.  RR )
133132recnd 9106 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  RR+ )  ->  ( log `  m )  e.  CC )
134133ad2antrr 707 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  /\  k  e.  ( 1 ... ( |_
`  m ) ) )  ->  ( log `  m )  e.  CC )
13511adantl 453 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  /\  k  e.  ( 1 ... ( |_
`  m ) ) )  ->  k  e.  NN )
136135nncnd 10008 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  /\  k  e.  ( 1 ... ( |_
`  m ) ) )  ->  k  e.  CC )
137135nnne0d 10036 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  /\  k  e.  ( 1 ... ( |_
`  m ) ) )  ->  k  =/=  0 )
138130, 134, 136, 137div12d 9818 . . . . . . . . . . 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 ) ) )
139129, 138eqtrd 2467 . . . . . . . . . 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 ) ) )
140139sumeq2dv 12489 . . . . . . . . 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 ) ) )
141 iftrue 3737 . . . . . . . . . . 11  |-  ( S  =  0  ->  if ( S  =  0 ,  0 ,  T
)  =  0 )
142141oveq2d 6089 . . . . . . . . . 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 ) )
14326subid1d 9392 . . . . . . . . . 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 ) ) )
144142, 143sylan9eqr 2489 . . . . . . . . 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 ) ) )
145 ovex 6098 . . . . . . . . . . . . . 14  |-  ( ( X `  ( L `
 k ) )  /  k )  e. 
_V
14658, 54, 145fvmpt 5798 . . . . . . . . . . . . 13  |-  ( k  e.  NN  ->  ( F `  k )  =  ( ( X `
 ( L `  k ) )  / 
k ) )
14722, 146syl 16 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( F `  k )  =  ( ( X `  ( L `  k )
)  /  k ) )
14861adantr 452 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  RR+ )  ->  F : NN
--> CC )
149148, 11, 62syl2an 464 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( F `  k )  e.  CC )
150147, 149eqeltrrd 2510 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( ( X `  ( L `  k ) )  / 
k )  e.  CC )
1519, 133, 150fsummulc2 12559 . . . . . . . . . 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 ) ) )
152151adantr 452 . . . . . . . . 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 ) ) )
153140, 144, 1523eqtr4d 2477 . . . . . . . 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 ) ) )
15490, 153sylan 458 . . . . . . 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 ) ) )
15590, 147sylan 458 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( 3 [,)  +oo ) )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( F `  k )  =  ( ( X `  ( L `  k )
)  /  k ) )
15679, 46syl6eleq 2525 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  ( |_ `  m )  e.  ( ZZ>= `  1 )
)
15783, 11, 53syl2an 464 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( 3 [,)  +oo ) )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( ( X `  ( L `  k ) )  / 
k )  e.  CC )
158155, 156, 157fsumser 12516 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( ( X `  ( L `  k ) )  /  k )  =  (  seq  1
(  +  ,  F
) `  ( |_ `  m ) ) )
159158adantr 452 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  ( 3 [,)  +oo ) )  /\  S  =  0 )  ->  sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( ( X `  ( L `  k )
)  /  k )  =  (  seq  1
(  +  ,  F
) `  ( |_ `  m ) ) )
160159oveq2d 6089 . . . . . . 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 ) ) ) )
161154, 160eqtrd 2467 . . . . . 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 ) ) ) )
162161fveq2d 5724 . . . . 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 ) ) ) ) )
163131ad2antlr 708 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  -> 
( log `  m
)  e.  RR )
164163recnd 9106 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  -> 
( log `  m
)  e.  CC )
16590, 164sylan 458 . . . . . 6  |-  ( ( ( ph  /\  m  e.  ( 3 [,)  +oo ) )  /\  S  =  0 )  -> 
( log `  m
)  e.  CC )
166165, 81absmuld 12248 . . . . 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 ) ) ) ) )
16798, 99absidd 12217 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  ( abs `  ( log `  m
) )  =  ( log `  m ) )
168167oveq1d 6088 . . . . . 6  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  (
( abs `  ( log `  m ) )  x.  ( abs `  (  seq  1 (  +  ,  F ) `  ( |_ `  m ) ) ) )  =  ( ( log `  m
)  x.  ( abs `  (  seq  1
(  +  ,  F
) `  ( |_ `  m ) ) ) ) )
169168adantr 452 . . . . 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 ) ) ) ) )
170162, 166, 1693eqtrd 2471 . . . 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 ) ) ) ) )
171 iftrue 3737 . . . . . . . 8  |-  ( S  =  0  ->  if ( S  =  0 ,  C ,  E )  =  C )
172171adantl 453 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  ->  if ( S  =  0 ,  C ,  E
)  =  C )
173172oveq1d 6088 . . . . . 6  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  -> 
( if ( S  =  0 ,  C ,  E )  x.  (
( log `  m
)  /  m ) )  =  ( C  x.  ( ( log `  m )  /  m
) ) )
17493recnd 9106 . . . . . . . 8  |-  ( ph  ->  C  e.  CC )
175174ad2antrr 707 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  ->  C  e.  CC )
176 rpcnne0 10621 . . . . . . . 8  |-  ( m  e.  RR+  ->  ( m  e.  CC  /\  m  =/=  0 ) )
177176ad2antlr 708 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  -> 
( m  e.  CC  /\  m  =/=  0 ) )
178 div12 9692 . . . . . . 7  |-  ( ( C  e.  CC  /\  ( log `  m )  e.  CC  /\  (
m  e.  CC  /\  m  =/=  0 ) )  ->  ( C  x.  ( ( log `  m
)  /  m ) )  =  ( ( log `  m )  x.  ( C  /  m ) ) )
179175, 164, 177, 178syl3anc 1184 . . . . . 6  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  -> 
( C  x.  (
( log `  m
)  /  m ) )  =  ( ( log `  m )  x.  ( C  /  m ) ) )
180173, 179eqtrd 2467 . . . . 5  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  S  =  0 )  -> 
( if ( S  =  0 ,  C ,  E )  x.  (
( log `  m
)  /  m ) )  =  ( ( log `  m )  x.  ( C  /  m ) ) )
18190, 180sylan 458 . . . 4  |-  ( ( ( ph  /\  m  e.  ( 3 [,)  +oo ) )  /\  S  =  0 )  -> 
( if ( S  =  0 ,  C ,  E )  x.  (
( log `  m
)  /  m ) )  =  ( ( log `  m )  x.  ( C  /  m ) ) )
182124, 170, 1813brtr4d 4234 . . 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 ) ) )
183 dchrvmasumif.2 . . . . . 6  |-  ( ph  ->  A. y  e.  ( 3 [,)  +oo )
( abs `  (
(  seq  1 (  +  ,  K ) `
 ( |_ `  y ) )  -  T ) )  <_ 
( E  x.  (
( log `  y
)  /  y ) ) )
184113fveq2d 5724 . . . . . . . . . 10  |-  ( y  =  m  ->  (  seq  1 (  +  ,  K ) `  ( |_ `  y ) )  =  (  seq  1
(  +  ,  K
) `  ( |_ `  m ) ) )
185184oveq1d 6088 . . . . . . . . 9  |-  ( y  =  m  ->  (
(  seq  1 (  +  ,  K ) `
 ( |_ `  y ) )  -  T )  =  ( (  seq  1 (  +  ,  K ) `
 ( |_ `  m ) )  -  T ) )
186185fveq2d 5724 . . . . . . . 8  |-  ( y  =  m  ->  ( abs `  ( (  seq  1 (  +  ,  K ) `  ( |_ `  y ) )  -  T ) )  =  ( abs `  (
(  seq  1 (  +  ,  K ) `
 ( |_ `  m ) )  -  T ) ) )
187 fveq2 5720 . . . . . . . . . 10  |-  ( y  =  m  ->  ( log `  y )  =  ( log `  m
) )
188 id 20 . . . . . . . . . 10  |-  ( y  =  m  ->  y  =  m )
189187, 188oveq12d 6091 . . . . . . . . 9  |-  ( y  =  m  ->  (
( log `  y
)  /  y )  =  ( ( log `  m )  /  m
) )
190189oveq2d 6089 . . . . . . . 8  |-  ( y  =  m  ->  ( E  x.  ( ( log `  y )  / 
y ) )  =  ( E  x.  (
( log `  m
)  /  m ) ) )
191186, 190breq12d 4217 . . . . . . 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 ) ) ) )
192191rspccva 3043 . . . . . 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 ) ) )
193183, 192sylan 458 . . . . 5  |-  ( (
ph  /\  m  e.  ( 3 [,)  +oo ) )  ->  ( abs `  ( (  seq  1 (  +  ,  K ) `  ( |_ `  m ) )  -  T ) )  <_  ( E  x.  ( ( log `  m
)  /  m ) ) )
194193adantr 452 . . . 4  |-  ( ( ( ph  /\  m  e.  ( 3 [,)  +oo ) )  /\  S  =/=  0 )  ->  ( abs `  ( (  seq  1 (  +  ,  K ) `  ( |_ `  m ) )  -  T ) )  <_  ( E  x.  ( ( log `  m
)  /  m ) ) )
195 fveq2 5720 . . . . . . . . . . . 12  |-  ( a  =  k  ->  ( log `  a )  =  ( log `  k
) )
196195, 57oveq12d 6091 . . . . . . . . . . 11  |-  ( a  =  k  ->  (
( log `  a
)  /  a )  =  ( ( log `  k )  /  k
) )
19756, 196oveq12d 6091 . . . . . . . . . 10  |-  ( a  =  k  ->  (
( X `  ( L `  a )
)  x.  ( ( log `  a )  /  a ) )  =  ( ( X `
 ( L `  k ) )  x.  ( ( log `  k
)  /  k ) ) )
198 dchrvmasumif.g . . . . . . . . . 10  |-  K  =  ( a  e.  NN  |->  ( ( X `  ( L `  a ) )  x.  ( ( log `  a )  /  a ) ) )
199 ovex 6098 . . . . . . . . . 10  |-  ( ( X `  ( L `
 k ) )  x.  ( ( log `  k )  /  k
) )  e.  _V
200197, 198, 199fvmpt 5798 . . . . . . . . 9  |-  ( k  e.  NN  ->  ( K `  k )  =  ( ( X `
 ( L `  k ) )  x.  ( ( log `  k
)  /  k ) ) )
20111, 200syl 16 . . . . . . . 8  |-  ( k  e.  ( 1 ... ( |_ `  m
) )  ->  ( K `  k )  =  ( ( X `
 ( L `  k ) )  x.  ( ( log `  k
)  /  k ) ) )
202 ifnefalse 3739 . . . . . . . . . . . . 13  |-  ( S  =/=  0  ->  if ( S  =  0 ,  m ,  k )  =  k )
203202fveq2d 5724 . . . . . . . . . . . 12  |-  ( S  =/=  0  ->  ( log `  if ( S  =  0 ,  m ,  k ) )  =  ( log `  k
) )
204203oveq1d 6088 . . . . . . . . . . 11  |-  ( S  =/=  0  ->  (
( log `  if ( S  =  0 ,  m ,  k ) )  /  k )  =  ( ( log `  k )  /  k
) )
205204oveq2d 6089 . . . . . . . . . 10  |-  ( S  =/=  0  ->  (
( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  =  ( ( X `  ( L `
 k ) )  x.  ( ( log `  k )  /  k
) ) )
206205adantl 453 . . . . . . . . 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
) ) )
207206eqcomd 2440 . . . . . . . 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 ) ) )
208201, 207sylan9eqr 2489 . . . . . . 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 ) ) )
209156adantr 452 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  ( 3 [,)  +oo ) )  /\  S  =/=  0 )  ->  ( |_ `  m )  e.  ( ZZ>= `  1 )
)
210 nnrp 10613 . . . . . . . . . . . . . . . 16  |-  ( k  e.  NN  ->  k  e.  RR+ )
211210adantl 453 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  NN )  ->  k  e.  RR+ )
212211relogcld 20510 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  NN )  ->  ( log `  k )  e.  RR )
213212recnd 9106 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  NN )  ->  ( log `  k )  e.  CC )
214213, 50, 52divcld 9782 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( log `  k )  /  k )  e.  CC )
21515, 214mulcld 9100 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( X `  ( L `
 k ) )  x.  ( ( log `  k )  /  k
) )  e.  CC )
216197cbvmptv 4292 . . . . . . . . . . . 12  |-  ( a  e.  NN  |->  ( ( X `  ( L `
 a ) )  x.  ( ( log `  a )  /  a
) ) )  =  ( k  e.  NN  |->  ( ( X `  ( L `  k ) )  x.  ( ( log `  k )  /  k ) ) )
217198, 216eqtri 2455 . . . . . . . . . . 11  |-  K  =  ( k  e.  NN  |->  ( ( X `  ( L `  k ) )  x.  ( ( log `  k )  /  k ) ) )
218215, 217fmptd 5885 . . . . . . . . . 10  |-  ( ph  ->  K : NN --> CC )
219218ad2antrr 707 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( 3 [,)  +oo ) )  /\  S  =/=  0 )  ->  K : NN --> CC )
220 ffvelrn 5860 . . . . . . . . 9  |-  ( ( K : NN --> CC  /\  k  e.  NN )  ->  ( K `  k
)  e.  CC )
221219, 11, 220syl2an 464 . . . . . . . 8  |-  ( ( ( ( ph  /\  m  e.  ( 3 [,)  +oo ) )  /\  S  =/=  0 )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( K `  k )  e.  CC )
222208, 221eqeltrrd 2510 . . . . . . 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 )
223208, 209, 222fsumser 12516 . . . . . 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 ) ) )
224 ifnefalse 3739 . . . . . . 7  |-  ( S  =/=  0  ->  if ( S  =  0 ,  0 ,  T
)  =  T )
225224adantl 453 . . . . . 6  |-  ( ( ( ph  /\  m  e.  ( 3 [,)  +oo ) )  /\  S  =/=  0 )  ->  if ( S  =  0 ,  0 ,  T
)  =  T )
226223, 225oveq12d 6091 . . . . 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 ) )
227226fveq2d 5724 . . . 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 ) ) )
228 ifnefalse 3739 . . . . . 6  |-  ( S  =/=  0  ->  if ( S  =  0 ,  C ,  E )  =  E )
229228adantl 453 . . . . 5  |-  ( ( ( ph  /\  m  e.  ( 3 [,)  +oo ) )  /\  S  =/=  0 )  ->  if ( S  =  0 ,  C ,  E )  =  E )
230229oveq1d 6088 . . . 4  |-  ( ( ( ph  /\  m  e.  ( 3 [,)  +oo ) )  /\  S  =/=  0 )  ->  ( if ( S  =  0 ,  C ,  E
)  x.  ( ( log `  m )  /  m ) )  =  ( E  x.  ( ( log `  m
)  /  m ) ) )
231194, 227, 2303brtr4d 4234 . . 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 ) ) )
232182, 231pm2.61dane 2676 . 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 ) ) )
233 fzfid 11304 . . . 4  |-  ( ph  ->  ( 1 ... 2
)  e.  Fin )
2347adantr 452 . . . . . . 7  |-  ( (
ph  /\  k  e.  ( 1 ... 2
) )  ->  X  e.  D )
235 elfzelz 11051 . . . . . . . 8  |-  ( k  e.  ( 1 ... 2 )  ->  k  e.  ZZ )
236235adantl 453 . . . . . . 7  |-  ( (
ph  /\  k  e.  ( 1 ... 2
) )  ->  k  e.  ZZ )
2374, 1, 5, 2, 234, 236dchrzrhcl 21021 . . . . . 6  |-  ( (
ph  /\  k  e.  ( 1 ... 2
) )  ->  ( X `  ( L `  k ) )  e.  CC )
238237abscld 12230 . . . . 5  |-  ( (
ph  /\  k  e.  ( 1 ... 2
) )  ->  ( abs `  ( X `  ( L `  k ) ) )  e.  RR )
23966, 86elrpii 10607 . . . . . . 7  |-  3  e.  RR+
240 relogcl 20465 . . . . . . 7  |-  ( 3  e.  RR+  ->  ( log `  3 )  e.  RR )
241239, 240ax-mp 8 . . . . . 6  |-  ( log `  3 )  e.  RR
242 elfznn 11072 . . . . . . 7  |-  ( k  e.  ( 1 ... 2 )  ->  k  e.  NN )
243242adantl 453 . . . . . 6  |-  ( (
ph  /\  k  e.  ( 1 ... 2
) )  ->  k  e.  NN )
244 nndivre 10027 . . . . . 6  |-  ( ( ( log `  3
)  e.  RR  /\  k  e.  NN )  ->  ( ( log `  3
)  /  k )  e.  RR )
245241, 243, 244sylancr 645 . . . . 5  |-  ( (
ph  /\  k  e.  ( 1 ... 2
) )  ->  (
( log `  3
)  /  k )  e.  RR )
246238, 245remulcld 9108 . . . 4  |-  ( (
ph  /\  k  e.  ( 1 ... 2
) )  ->  (
( abs `  ( X `  ( L `  k ) ) )  x.  ( ( log `  3 )  / 
k ) )  e.  RR )
247233, 246fsumrecl 12520 . . 3  |-  ( ph  -> 
sum_ k  e.  ( 1 ... 2 ) ( ( abs `  ( X `  ( L `  k ) ) )  x.  ( ( log `  3 )  / 
k ) )  e.  RR )
24845abscld 12230 . . 3  |-  ( ph  ->  ( abs `  if ( S  =  0 ,  0 ,  T
) )  e.  RR )
249247, 248readdcld 9107 . 2  |-  ( ph  ->  ( sum_ k  e.  ( 1 ... 2 ) ( ( abs `  ( X `  ( L `  k ) ) )  x.  ( ( log `  3 )  / 
k ) )  +  ( abs `  if ( S  =  0 ,  0 ,  T
) ) )  e.  RR )
250 simpl 444 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  ph )
25166rexri 9129 . . . . . . . . . . 11  |-  3  e.  RR*
252 elico2 10966 . . . . . . . . . . 11  |-  ( ( 1  e.  RR  /\  3  e.  RR* )  -> 
( m  e.  ( 1 [,) 3 )  <-> 
( m  e.  RR  /\  1  <_  m  /\  m  <  3 ) ) )
25370, 251, 252mp2an 654 . . . . . . . . . 10  |-  ( m  e.  ( 1 [,) 3 )  <->  ( m  e.  RR  /\  1  <_  m  /\  m  <  3
) )
254253simp1bi 972 . . . . . . . . 9  |-  ( m  e.  ( 1 [,) 3 )  ->  m  e.  RR )
255254adantl 453 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  m  e.  RR )
25684a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  0  e.  RR )
25770a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  1  e.  RR )
258 0lt1 9542 . . . . . . . . . 10  |-  0  <  1
259258a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  0  <  1 )
260253simp2bi 973 . . . . . . . . . 10  |-  ( m  e.  ( 1 [,) 3 )  ->  1  <_  m )
261260adantl 453 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  1  <_  m )
262256, 257, 255, 259, 261ltletrd 9222 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  0  <  m )
263255, 262elrpd 10638 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  m  e.  RR+ )
264250, 263jca 519 . . . . . 6  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  ( ph  /\  m  e.  RR+ ) )
26545adantr 452 . . . . . . 7  |-  ( (
ph  /\  m  e.  RR+ )  ->  if ( S  =  0 , 
0 ,  T )  e.  CC )
26626, 265subcld 9403 . . . . . 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 )
267264, 266syl 16 . . . . 5  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  ( sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( ( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  -  if ( S  =  0 ,  0 ,  T ) )  e.  CC )
268267abscld 12230 . . . 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 )
269264, 26syl 16 . . . . . 6  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( ( X `  ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  e.  CC )
270269abscld 12230 . . . . 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 )
271248adantr 452 . . . . 5  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  ( abs `  if ( S  =  0 ,  0 ,  T ) )  e.  RR )
272270, 271readdcld 9107 . . . 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 )
273247adantr 452 . . . . 5  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  sum_ k  e.  ( 1 ... 2
) ( ( abs `  ( X `  ( L `  k )
) )  x.  (
( log `  3
)  /  k ) )  e.  RR )
274273, 271readdcld 9107 . . . 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 )
27526, 265abs2dif2d 12252 . . . . 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 ) ) ) )
276264, 275syl 16 . . . 4  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  ( abs `  ( sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( ( X `  ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  -  if ( S  =  0 ,  0 ,  T ) ) )  <_  (
( abs `  sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( ( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  +  ( abs `  if ( S  =  0 ,  0 ,  T ) ) ) )
27725abscld 12230 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... ( |_ `  m ) ) )  ->  ( abs `  ( ( X `  ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  e.  RR )
2789, 277fsumrecl 12520 . . . . . . 7  |-  ( (
ph  /\  m  e.  RR+ )  ->  sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( abs `  (
( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  e.  RR )
279264, 278syl 16 . . . . . 6  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( abs `  (
( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  e.  RR )
2809, 25fsumabs 12572 . . . . . . 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 ) ) ) )
281264, 280syl 16 . . . . . 6  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  ( abs `  sum_ k  e.  ( 1 ... ( |_
`  m ) ) ( ( X `  ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  <_  sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( abs `  (
( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) ) )
282 fzfid 11304 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  RR+ )  ->  ( 1 ... 2 )  e. 
Fin )
283237adantlr 696 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  ( X `  ( L `  k ) )  e.  CC )
28417adantr 452 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  m  e.  RR+ )
285242adantl 453 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  k  e.  NN )
286285nnrpd 10639 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  k  e.  RR+ )
287284, 286, 19syl2anc 643 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  if ( S  =  0 ,  m ,  k )  e.  RR+ )
288287relogcld 20510 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  ( log `  if ( S  =  0 ,  m ,  k ) )  e.  RR )
289288, 285nndivred 10040 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  (
( log `  if ( S  =  0 ,  m ,  k ) )  /  k )  e.  RR )
290289recnd 9106 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  (
( log `  if ( S  =  0 ,  m ,  k ) )  /  k )  e.  CC )
291283, 290mulcld 9100 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  (
( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  e.  CC )
292291abscld 12230 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  ( abs `  ( ( X `
 ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  e.  RR )
293282, 292fsumrecl 12520 . . . . . . . 8  |-  ( (
ph  /\  m  e.  RR+ )  ->  sum_ k  e.  ( 1 ... 2
) ( abs `  (
( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  e.  RR )
294264, 293syl 16 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  sum_ k  e.  ( 1 ... 2
) ( abs `  (
( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  e.  RR )
295 fzfid 11304 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  (
1 ... 2 )  e. 
Fin )
296264, 291sylan 458 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  (
( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )  e.  CC )
297296abscld 12230 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  ( abs `  ( ( X `
 ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  e.  RR )
298296absge0d 12238 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  0  <_  ( abs `  (
( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) ) )
299255flcld 11199 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  ( |_ `  m )  e.  ZZ )
300 2z 10304 . . . . . . . . . . 11  |-  2  e.  ZZ
301300a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  2  e.  ZZ )
302253simp3bi 974 . . . . . . . . . . . . . 14  |-  ( m  e.  ( 1 [,) 3 )  ->  m  <  3 )
303302adantl 453 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  m  <  3 )
304 3nn 10126 . . . . . . . . . . . . . . 15  |-  3  e.  NN
305304nnzi 10297 . . . . . . . . . . . . . 14  |-  3  e.  ZZ
306 fllt 11207 . . . . . . . . . . . . . 14  |-  ( ( m  e.  RR  /\  3  e.  ZZ )  ->  ( m  <  3  <->  ( |_ `  m )  <  3 ) )
307255, 305, 306sylancl 644 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  (
m  <  3  <->  ( |_ `  m )  <  3
) )
308303, 307mpbid 202 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  ( |_ `  m )  <  3 )
309 df-3 10051 . . . . . . . . . . . 12  |-  3  =  ( 2  +  1 )
310308, 309syl6breq 4243 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  ( |_ `  m )  < 
( 2  +  1 ) )
311 rpre 10610 . . . . . . . . . . . . . . 15  |-  ( m  e.  RR+  ->  m  e.  RR )
312311adantl 453 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  RR+ )  ->  m  e.  RR )
313312flcld 11199 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  RR+ )  ->  ( |_ `  m )  e.  ZZ )
314 zleltp1 10318 . . . . . . . . . . . . 13  |-  ( ( ( |_ `  m
)  e.  ZZ  /\  2  e.  ZZ )  ->  ( ( |_ `  m )  <_  2  <->  ( |_ `  m )  <  ( 2  +  1 ) ) )
315313, 300, 314sylancl 644 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  RR+ )  ->  ( ( |_ `  m )  <_ 
2  <->  ( |_ `  m )  <  (
2  +  1 ) ) )
316264, 315syl 16 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  (
( |_ `  m
)  <_  2  <->  ( |_ `  m )  <  (
2  +  1 ) ) )
317310, 316mpbird 224 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  ( |_ `  m )  <_ 
2 )
318 eluz2 10486 . . . . . . . . . 10  |-  ( 2  e.  ( ZZ>= `  ( |_ `  m ) )  <-> 
( ( |_ `  m )  e.  ZZ  /\  2  e.  ZZ  /\  ( |_ `  m )  <_  2 ) )
319299, 301, 317, 318syl3anbrc 1138 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  2  e.  ( ZZ>= `  ( |_ `  m ) ) )
320 fzss2 11084 . . . . . . . . 9  |-  ( 2  e.  ( ZZ>= `  ( |_ `  m ) )  ->  ( 1 ... ( |_ `  m
) )  C_  (
1 ... 2 ) )
321319, 320syl 16 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  (
1 ... ( |_ `  m ) )  C_  ( 1 ... 2
) )
322295, 297, 298, 321fsumless 12567 . . . . . . 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 ) ) ) )
323246adantlr 696 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  (
( abs `  ( X `  ( L `  k ) ) )  x.  ( ( log `  3 )  / 
k ) )  e.  RR )
324283, 290absmuld 12248 . . . . . . . . . 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 ) ) ) )
325264, 324sylan 458 . . . . . . . . 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 ) ) ) )
326264, 289sylan 458 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  (
( log `  if ( S  =  0 ,  m ,  k ) )  /  k )  e.  RR )
327264, 288sylan 458 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  ( log `  if ( S  =  0 ,  m ,  k ) )  e.  RR )
328 log1 20472 . . . . . . . . . . . . . 14  |-  ( log `  1 )  =  0
329 elfzle1 11052 . . . . . . . . . . . . . . . 16  |-  ( k  e.  ( 1 ... 2 )  ->  1  <_  k )
330 breq2 4208 . . . . . . . . . . . . . . . . 17  |-  ( m  =  if ( S  =  0 ,  m ,  k )  -> 
( 1  <_  m  <->  1  <_  if ( S  =  0 ,  m ,  k ) ) )
331 breq2 4208 . . . . . . . . . . . . . . . . 17  |-  ( k  =  if ( S  =  0 ,  m ,  k )  -> 
( 1  <_  k  <->  1  <_  if ( S  =  0 ,  m ,  k ) ) )
332330, 331ifboth 3762 . . . . . . . . . . . . . . . 16  |-  ( ( 1  <_  m  /\  1  <_  k )  -> 
1  <_  if ( S  =  0 ,  m ,  k )
)
333261, 329, 332syl2an 464 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  1  <_  if ( S  =  0 ,  m ,  k ) )
334 1rp 10608 . . . . . . . . . . . . . . . . 17  |-  1  e.  RR+
335 logleb 20490 . . . . . . . . . . . . . . . . 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 ) ) ) )
336334, 287, 335sylancr 645 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  (
1  <_  if ( S  =  0 ,  m ,  k )  <->  ( log `  1 )  <_  ( log `  if ( S  =  0 ,  m ,  k ) ) ) )
337264, 336sylan 458 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  (
1  <_  if ( S  =  0 ,  m ,  k )  <->  ( log `  1 )  <_  ( log `  if ( S  =  0 ,  m ,  k ) ) ) )
338333, 337mpbid 202 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  ( log `  1 )  <_ 
( log `  if ( S  =  0 ,  m ,  k ) ) )
339328, 338syl5eqbrr 4238 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  0  <_  ( log `  if ( S  =  0 ,  m ,  k ) ) )
340286rpregt0d 10646 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  (
k  e.  RR  /\  0  <  k ) )
341264, 340sylan 458 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  (
k  e.  RR  /\  0  <  k ) )
342 divge0 9871 . . . . . . . . . . . . 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 ) )
343327, 339, 341, 342syl21anc 1183 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  0  <_  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) )
344326, 343absidd 12217 . . . . . . . . . . 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 ) )
345344, 326eqeltrd 2509 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  ( abs `  ( ( log `  if ( S  =  0 ,  m ,  k ) )  / 
k ) )  e.  RR )
346245adantlr 696 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  (
( log `  3
)  /  k )  e.  RR )
347238adantlr 696 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  ( abs `  ( X `  ( L `  k ) ) )  e.  RR )
348283absge0d 12238 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  0  <_  ( abs `  ( X `  ( L `  k ) ) ) )
349347, 348jca 519 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  (
( abs `  ( X `  ( L `  k ) ) )  e.  RR  /\  0  <_  ( abs `  ( X `  ( L `  k ) ) ) ) )
350264, 349sylan 458 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  (
( abs `  ( X `  ( L `  k ) ) )  e.  RR  /\  0  <_  ( abs `  ( X `  ( L `  k ) ) ) ) )
351302ad2antlr 708 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  m  <  3 )
352285nnred 10007 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  k  e.  RR )
353 2re 10061 . . . . . . . . . . . . . . . . . 18  |-  2  e.  RR
354353a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  2  e.  RR )
35566a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  3  e.  RR )
356 elfzle2 11053 . . . . . . . . . . . . . . . . . 18  |-  ( k  e.  ( 1 ... 2 )  ->  k  <_  2 )
357356adantl 453 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  k  <_  2 )
358 2lt3 10135 . . . . . . . . . . . . . . . . . 18  |-  2  <  3
359358a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  2  <  3 )
360352, 354, 355, 357, 359lelttrd 9220 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  k  <  3 )
361264, 360sylan 458 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  k  <  3 )
362 breq1 4207 . . . . . . . . . . . . . . . 16  |-  ( m  =  if ( S  =  0 ,  m ,  k )  -> 
( m  <  3  <->  if ( S  =  0 ,  m ,  k )  <  3 ) )
363 breq1 4207 . . . . . . . . . . . . . . . 16  |-  ( k  =  if ( S  =  0 ,  m ,  k )  -> 
( k  <  3  <->  if ( S  =  0 ,  m ,  k )  <  3 ) )
364362, 363ifboth 3762 . . . . . . . . . . . . . . 15  |-  ( ( m  <  3  /\  k  <  3 )  ->  if ( S  =  0 ,  m ,  k )  <  3 )
365351, 361, 364syl2anc 643 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  if ( S  =  0 ,  m ,  k )  <  3 )
366287rpred 10640 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  if ( S  =  0 ,  m ,  k )  e.  RR )
367 ltle 9155 . . . . . . . . . . . . . . . 16  |-  ( ( if ( S  =  0 ,  m ,  k )  e.  RR  /\  3  e.  RR )  ->  ( if ( S  =  0 ,  m ,  k )  <  3  ->  if ( S  =  0 ,  m ,  k )  <_  3 ) )
368366, 66, 367sylancl 644 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  ( if ( S  =  0 ,  m ,  k )  <  3  ->  if ( S  =  0 ,  m ,  k )  <_  3 ) )
369264, 368sylan 458 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  ( if ( S  =  0 ,  m ,  k )  <  3  ->  if ( S  =  0 ,  m ,  k )  <_  3 ) )
370365, 369mpd 15 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  if ( S  =  0 ,  m ,  k )  <_  3 )
371 logleb 20490 . . . . . . . . . . . . . . 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 ) ) )
372287, 239, 371sylancl 644 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  ( if ( S  =  0 ,  m ,  k )  <_  3  <->  ( log `  if ( S  =  0 ,  m ,  k ) )  <_ 
( log `  3
) ) )
373264, 372sylan 458 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  ( if ( S  =  0 ,  m ,  k )  <_  3  <->  ( log `  if ( S  =  0 ,  m ,  k ) )  <_ 
( log `  3
) ) )
374370, 373mpbid 202 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  ( log `  if ( S  =  0 ,  m ,  k ) )  <_  ( log `  3
) )
375241a1i 11 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  RR+ )  /\  k  e.  ( 1 ... 2
) )  ->  ( log `  3 )  e.  RR )
376288, 375, 286lediv1d 10682 . . . . . . . . . . . . 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 ) ) )
377264, 376sylan 458 . . . . . . . . . . . 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 ) ) )
378374, 377mpbid 202 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  (
( log `  if ( S  =  0 ,  m ,  k ) )  /  k )  <_  ( ( log `  3 )  / 
k ) )
379344, 378eqbrtrd 4224 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( 1 [,) 3
) )  /\  k  e.  ( 1 ... 2
) )  ->  ( abs `  ( ( log `  if ( S  =  0 ,  m ,  k ) )  / 
k ) )  <_ 
( ( log `  3
)  /  k ) )
380 lemul2a 9857 . . . . . . . . . 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 ) ) )
381345, 346, 350, 379, 380syl31anc 1187 . . . . . . . . 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 ) ) )
382325, 381eqbrtrd 4224 . . . . . . . 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 ) ) )
383295, 297, 323, 382fsumle 12570 . . . . . . 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 ) ) )
384279, 294, 273, 322, 383letrd 9219 . . . . . 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 ) ) )
385270, 279, 273, 281, 384letrd 9219 . . . . 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 ) ) )
38626abscld 12230 . . . . . . 7  |-  ( (
ph  /\  m  e.  RR+ )  ->  ( abs ` 
sum_ k  e.  ( 1 ... ( |_
`  m ) ) ( ( X `  ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  e.  RR )
387247adantr 452 . . . . . . 7  |-  ( (
ph  /\  m  e.  RR+ )  ->  sum_ k  e.  ( 1 ... 2
) ( ( abs `  ( X `  ( L `  k )
) )  x.  (
( log `  3
)  /  k ) )  e.  RR )
388265abscld 12230 . . . . . . 7  |-  ( (
ph  /\  m  e.  RR+ )  ->  ( abs `  if ( S  =  0 ,  0 ,  T ) )  e.  RR )
389386, 387, 388leadd1d 9612 . . . . . 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
) ) ) ) )
390264, 389syl 16 . . . . 5  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  (
( abs `  sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( ( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  <_  sum_ k  e.  ( 1 ... 2
) ( ( abs `  ( X `  ( L `  k )
) )  x.  (
( log `  3
)  /  k ) )  <->  ( ( abs `  sum_ k  e.  ( 1 ... ( |_
`  m ) ) ( ( X `  ( L `  k ) )  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  +  ( abs `  if ( S  =  0 ,  0 ,  T ) ) )  <_  ( sum_ k  e.  ( 1 ... 2 ) ( ( abs `  ( X `  ( L `  k ) ) )  x.  ( ( log `  3 )  / 
k ) )  +  ( abs `  if ( S  =  0 ,  0 ,  T
) ) ) ) )
391385, 390mpbid 202 . . . 4  |-  ( (
ph  /\  m  e.  ( 1 [,) 3
) )  ->  (
( abs `  sum_ k  e.  ( 1 ... ( |_ `  m ) ) ( ( X `  ( L `  k )
)  x.  ( ( log `  if ( S  =  0 ,  m ,  k ) )  /  k ) ) )  +  ( abs `  if ( S  =  0 ,  0 ,  T ) ) )  <_  ( sum_ k  e.  ( 1 ... 2 ) ( ( abs `  ( X `  ( L `  k ) ) )  x.  ( ( log `  3 )  / 
k )