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

Theorem dchrisumlem2 24320
Description: Lemma for dchrisum 24322. Lemma 9.4.1 of [Shapiro], p. 377. (Contributed by Mario Carneiro, 2-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.  )
dchrisum.2  |-  ( n  =  x  ->  A  =  B )
dchrisum.3  |-  ( ph  ->  M  e.  NN )
dchrisum.4  |-  ( (
ph  /\  n  e.  RR+ )  ->  A  e.  RR )
dchrisum.5  |-  ( (
ph  /\  ( n  e.  RR+  /\  x  e.  RR+ )  /\  ( M  <_  n  /\  n  <_  x ) )  ->  B  <_  A )
dchrisum.6  |-  ( ph  ->  ( n  e.  RR+  |->  A )  ~~> r  0 )
dchrisum.7  |-  F  =  ( n  e.  NN  |->  ( ( X `  ( L `  n ) )  x.  A ) )
dchrisum.9  |-  ( ph  ->  R  e.  RR )
dchrisum.10  |-  ( ph  ->  A. u  e.  ( 0..^ N ) ( abs `  sum_ n  e.  ( 0..^ u ) ( X `  ( L `  n )
) )  <_  R
)
dchrisumlem2.1  |-  ( ph  ->  U  e.  RR+ )
dchrisumlem2.2  |-  ( ph  ->  M  <_  U )
dchrisumlem2.3  |-  ( ph  ->  U  <_  ( I  +  1 ) )
dchrisumlem2.4  |-  ( ph  ->  I  e.  NN )
dchrisumlem2.5  |-  ( ph  ->  J  e.  ( ZZ>= `  I ) )
Assertion
Ref Expression
dchrisumlem2  |-  ( ph  ->  ( abs `  (
(  seq 1 (  +  ,  F ) `  J )  -  (  seq 1 (  +  ,  F ) `  I
) ) )  <_ 
( ( 2  x.  R )  x.  [_ U  /  n ]_ A
) )
Distinct variable groups:    u, n, x    .1. , n, x    n, F, u, x    n, I, u, x    n, J, u, x    x, A   
n, N, u, x    ph, n, u, x    R, n, u, x    U, n, u, x    B, n   
n, Z, x    D, n, x    n, L, u, x    n, M, u, x    n, X, u, x
Allowed substitution hints:    A( u, n)    B( x, u)    D( u)    .1. (
u)    G( x, u, n)    Z( u)

Proof of Theorem dchrisumlem2
Dummy variables  k 
i are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fzodisj 11954 . . . . . . . . 9  |-  ( ( 1..^ ( I  + 
1 ) )  i^i  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  =  (/)
21a1i 11 . . . . . . . 8  |-  ( ph  ->  ( ( 1..^ ( I  +  1 ) )  i^i  ( ( I  +  1 )..^ ( J  +  1 ) ) )  =  (/) )
3 dchrisumlem2.4 . . . . . . . . . . . 12  |-  ( ph  ->  I  e.  NN )
43peano2nnd 10628 . . . . . . . . . . 11  |-  ( ph  ->  ( I  +  1 )  e.  NN )
5 nnuz 11196 . . . . . . . . . . 11  |-  NN  =  ( ZZ>= `  1 )
64, 5syl6eleq 2521 . . . . . . . . . 10  |-  ( ph  ->  ( I  +  1 )  e.  ( ZZ>= ` 
1 ) )
7 dchrisumlem2.5 . . . . . . . . . . 11  |-  ( ph  ->  J  e.  ( ZZ>= `  I ) )
8 eluzp1p1 11186 . . . . . . . . . . 11  |-  ( J  e.  ( ZZ>= `  I
)  ->  ( J  +  1 )  e.  ( ZZ>= `  ( I  +  1 ) ) )
97, 8syl 17 . . . . . . . . . 10  |-  ( ph  ->  ( J  +  1 )  e.  ( ZZ>= `  ( I  +  1
) ) )
10 elfzuzb 11796 . . . . . . . . . 10  |-  ( ( I  +  1 )  e.  ( 1 ... ( J  +  1 ) )  <->  ( (
I  +  1 )  e.  ( ZZ>= `  1
)  /\  ( J  +  1 )  e.  ( ZZ>= `  ( I  +  1 ) ) ) )
116, 9, 10sylanbrc 669 . . . . . . . . 9  |-  ( ph  ->  ( I  +  1 )  e.  ( 1 ... ( J  + 
1 ) ) )
12 fzosplit 11953 . . . . . . . . 9  |-  ( ( I  +  1 )  e.  ( 1 ... ( J  +  1 ) )  ->  (
1..^ ( J  + 
1 ) )  =  ( ( 1..^ ( I  +  1 ) )  u.  ( ( I  +  1 )..^ ( J  +  1 ) ) ) )
1311, 12syl 17 . . . . . . . 8  |-  ( ph  ->  ( 1..^ ( J  +  1 ) )  =  ( ( 1..^ ( I  +  1 ) )  u.  (
( I  +  1 )..^ ( J  + 
1 ) ) ) )
14 fzofi 12188 . . . . . . . . 9  |-  ( 1..^ ( J  +  1 ) )  e.  Fin
1514a1i 11 . . . . . . . 8  |-  ( ph  ->  ( 1..^ ( J  +  1 ) )  e.  Fin )
16 elfzouz 11926 . . . . . . . . . 10  |-  ( i  e.  ( 1..^ ( J  +  1 ) )  ->  i  e.  ( ZZ>= `  1 )
)
1716, 5syl6eleqr 2522 . . . . . . . . 9  |-  ( i  e.  ( 1..^ ( J  +  1 ) )  ->  i  e.  NN )
18 rpvmasum.g . . . . . . . . . . 11  |-  G  =  (DChr `  N )
19 rpvmasum.z . . . . . . . . . . 11  |-  Z  =  (ℤ/n `  N )
20 rpvmasum.d . . . . . . . . . . 11  |-  D  =  ( Base `  G
)
21 rpvmasum.l . . . . . . . . . . 11  |-  L  =  ( ZRHom `  Z
)
22 dchrisum.b . . . . . . . . . . . 12  |-  ( ph  ->  X  e.  D )
2322adantr 467 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  NN )  ->  X  e.  D )
24 nnz 10961 . . . . . . . . . . . 12  |-  ( i  e.  NN  ->  i  e.  ZZ )
2524adantl 468 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  NN )  ->  i  e.  ZZ )
2618, 19, 20, 21, 23, 25dchrzrhcl 24165 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  NN )  ->  ( X `
 ( L `  i ) )  e.  CC )
27 nnrp 11313 . . . . . . . . . . . . 13  |-  ( i  e.  NN  ->  i  e.  RR+ )
28 rpvmasum.a . . . . . . . . . . . . . . 15  |-  ( ph  ->  N  e.  NN )
29 rpvmasum.1 . . . . . . . . . . . . . . 15  |-  .1.  =  ( 0g `  G )
30 dchrisum.n1 . . . . . . . . . . . . . . 15  |-  ( ph  ->  X  =/=  .1.  )
31 dchrisum.2 . . . . . . . . . . . . . . 15  |-  ( n  =  x  ->  A  =  B )
32 dchrisum.3 . . . . . . . . . . . . . . 15  |-  ( ph  ->  M  e.  NN )
33 dchrisum.4 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  RR+ )  ->  A  e.  RR )
34 dchrisum.5 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( n  e.  RR+  /\  x  e.  RR+ )  /\  ( M  <_  n  /\  n  <_  x ) )  ->  B  <_  A )
35 dchrisum.6 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( n  e.  RR+  |->  A )  ~~> r  0 )
36 dchrisum.7 . . . . . . . . . . . . . . 15  |-  F  =  ( n  e.  NN  |->  ( ( X `  ( L `  n ) )  x.  A ) )
3719, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36dchrisumlema 24318 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( i  e.  RR+  ->  [_ i  /  n ]_ A  e.  RR )  /\  ( i  e.  ( M [,) +oo )  ->  0  <_  [_ i  /  n ]_ A ) ) )
3837simpld 461 . . . . . . . . . . . . 13  |-  ( ph  ->  ( i  e.  RR+  ->  [_ i  /  n ]_ A  e.  RR ) )
3927, 38syl5 34 . . . . . . . . . . . 12  |-  ( ph  ->  ( i  e.  NN  ->  [_ i  /  n ]_ A  e.  RR ) )
4039imp 431 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  NN )  ->  [_ i  /  n ]_ A  e.  RR )
4140recnd 9671 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  NN )  ->  [_ i  /  n ]_ A  e.  CC )
4226, 41mulcld 9665 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  NN )  ->  ( ( X `  ( L `
 i ) )  x.  [_ i  /  n ]_ A )  e.  CC )
4317, 42sylan2 477 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 1..^ ( J  + 
1 ) ) )  ->  ( ( X `
 ( L `  i ) )  x. 
[_ i  /  n ]_ A )  e.  CC )
442, 13, 15, 43fsumsplit 13799 . . . . . . 7  |-  ( ph  -> 
sum_ i  e.  ( 1..^ ( J  + 
1 ) ) ( ( X `  ( L `  i )
)  x.  [_ i  /  n ]_ A )  =  ( sum_ i  e.  ( 1..^ ( I  +  1 ) ) ( ( X `  ( L `  i ) )  x.  [_ i  /  n ]_ A )  +  sum_ i  e.  ( ( I  +  1 )..^ ( J  + 
1 ) ) ( ( X `  ( L `  i )
)  x.  [_ i  /  n ]_ A ) ) )
45 eluzelz 11170 . . . . . . . . 9  |-  ( J  e.  ( ZZ>= `  I
)  ->  J  e.  ZZ )
46 fzval3 11984 . . . . . . . . 9  |-  ( J  e.  ZZ  ->  (
1 ... J )  =  ( 1..^ ( J  +  1 ) ) )
477, 45, 463syl 18 . . . . . . . 8  |-  ( ph  ->  ( 1 ... J
)  =  ( 1..^ ( J  +  1 ) ) )
4847sumeq1d 13760 . . . . . . 7  |-  ( ph  -> 
sum_ i  e.  ( 1 ... J ) ( ( X `  ( L `  i ) )  x.  [_ i  /  n ]_ A )  =  sum_ i  e.  ( 1..^ ( J  + 
1 ) ) ( ( X `  ( L `  i )
)  x.  [_ i  /  n ]_ A ) )
493nnzd 11041 . . . . . . . . . 10  |-  ( ph  ->  I  e.  ZZ )
50 fzval3 11984 . . . . . . . . . 10  |-  ( I  e.  ZZ  ->  (
1 ... I )  =  ( 1..^ ( I  +  1 ) ) )
5149, 50syl 17 . . . . . . . . 9  |-  ( ph  ->  ( 1 ... I
)  =  ( 1..^ ( I  +  1 ) ) )
5251sumeq1d 13760 . . . . . . . 8  |-  ( ph  -> 
sum_ i  e.  ( 1 ... I ) ( ( X `  ( L `  i ) )  x.  [_ i  /  n ]_ A )  =  sum_ i  e.  ( 1..^ ( I  + 
1 ) ) ( ( X `  ( L `  i )
)  x.  [_ i  /  n ]_ A ) )
5352oveq1d 6318 . . . . . . 7  |-  ( ph  ->  ( sum_ i  e.  ( 1 ... I ) ( ( X `  ( L `  i ) )  x.  [_ i  /  n ]_ A )  +  sum_ i  e.  ( ( I  +  1 )..^ ( J  + 
1 ) ) ( ( X `  ( L `  i )
)  x.  [_ i  /  n ]_ A ) )  =  ( sum_ i  e.  ( 1..^ ( I  +  1 ) ) ( ( X `  ( L `
 i ) )  x.  [_ i  /  n ]_ A )  + 
sum_ i  e.  ( ( I  +  1 )..^ ( J  + 
1 ) ) ( ( X `  ( L `  i )
)  x.  [_ i  /  n ]_ A ) ) )
5444, 48, 533eqtr4d 2474 . . . . . 6  |-  ( ph  -> 
sum_ i  e.  ( 1 ... J ) ( ( X `  ( L `  i ) )  x.  [_ i  /  n ]_ A )  =  ( sum_ i  e.  ( 1 ... I
) ( ( X `
 ( L `  i ) )  x. 
[_ i  /  n ]_ A )  +  sum_ i  e.  ( (
I  +  1 )..^ ( J  +  1 ) ) ( ( X `  ( L `
 i ) )  x.  [_ i  /  n ]_ A ) ) )
55 elfznn 11830 . . . . . . . 8  |-  ( i  e.  ( 1 ... J )  ->  i  e.  NN )
56 simpr 463 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  NN )  ->  i  e.  NN )
57 nfcv 2585 . . . . . . . . . 10  |-  F/_ n
i
58 nfcv 2585 . . . . . . . . . . 11  |-  F/_ n
( X `  ( L `  i )
)
59 nfcv 2585 . . . . . . . . . . 11  |-  F/_ n  x.
60 nfcsb1v 3412 . . . . . . . . . . 11  |-  F/_ n [_ i  /  n ]_ A
6158, 59, 60nfov 6329 . . . . . . . . . 10  |-  F/_ n
( ( X `  ( L `  i ) )  x.  [_ i  /  n ]_ A )
62 fveq2 5879 . . . . . . . . . . . 12  |-  ( n  =  i  ->  ( L `  n )  =  ( L `  i ) )
6362fveq2d 5883 . . . . . . . . . . 11  |-  ( n  =  i  ->  ( X `  ( L `  n ) )  =  ( X `  ( L `  i )
) )
64 csbeq1a 3405 . . . . . . . . . . 11  |-  ( n  =  i  ->  A  =  [_ i  /  n ]_ A )
6563, 64oveq12d 6321 . . . . . . . . . 10  |-  ( n  =  i  ->  (
( X `  ( L `  n )
)  x.  A )  =  ( ( X `
 ( L `  i ) )  x. 
[_ i  /  n ]_ A ) )
6657, 61, 65, 36fvmptf 5980 . . . . . . . . 9  |-  ( ( i  e.  NN  /\  ( ( X `  ( L `  i ) )  x.  [_ i  /  n ]_ A )  e.  CC )  -> 
( F `  i
)  =  ( ( X `  ( L `
 i ) )  x.  [_ i  /  n ]_ A ) )
6756, 42, 66syl2anc 666 . . . . . . . 8  |-  ( (
ph  /\  i  e.  NN )  ->  ( F `
 i )  =  ( ( X `  ( L `  i ) )  x.  [_ i  /  n ]_ A ) )
6855, 67sylan2 477 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 1 ... J
) )  ->  ( F `  i )  =  ( ( X `
 ( L `  i ) )  x. 
[_ i  /  n ]_ A ) )
693, 5syl6eleq 2521 . . . . . . . 8  |-  ( ph  ->  I  e.  ( ZZ>= ` 
1 ) )
70 uztrn 11177 . . . . . . . 8  |-  ( ( J  e.  ( ZZ>= `  I )  /\  I  e.  ( ZZ>= `  1 )
)  ->  J  e.  ( ZZ>= `  1 )
)
717, 69, 70syl2anc 666 . . . . . . 7  |-  ( ph  ->  J  e.  ( ZZ>= ` 
1 ) )
7255, 42sylan2 477 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 1 ... J
) )  ->  (
( X `  ( L `  i )
)  x.  [_ i  /  n ]_ A )  e.  CC )
7368, 71, 72fsumser 13789 . . . . . 6  |-  ( ph  -> 
sum_ i  e.  ( 1 ... J ) ( ( X `  ( L `  i ) )  x.  [_ i  /  n ]_ A )  =  (  seq 1
(  +  ,  F
) `  J )
)
7454, 73eqtr3d 2466 . . . . 5  |-  ( ph  ->  ( sum_ i  e.  ( 1 ... I ) ( ( X `  ( L `  i ) )  x.  [_ i  /  n ]_ A )  +  sum_ i  e.  ( ( I  +  1 )..^ ( J  + 
1 ) ) ( ( X `  ( L `  i )
)  x.  [_ i  /  n ]_ A ) )  =  (  seq 1 (  +  ,  F ) `  J
) )
75 elfznn 11830 . . . . . . 7  |-  ( i  e.  ( 1 ... I )  ->  i  e.  NN )
7675, 67sylan2 477 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 1 ... I
) )  ->  ( F `  i )  =  ( ( X `
 ( L `  i ) )  x. 
[_ i  /  n ]_ A ) )
7775, 42sylan2 477 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 1 ... I
) )  ->  (
( X `  ( L `  i )
)  x.  [_ i  /  n ]_ A )  e.  CC )
7876, 69, 77fsumser 13789 . . . . 5  |-  ( ph  -> 
sum_ i  e.  ( 1 ... I ) ( ( X `  ( L `  i ) )  x.  [_ i  /  n ]_ A )  =  (  seq 1
(  +  ,  F
) `  I )
)
7974, 78oveq12d 6321 . . . 4  |-  ( ph  ->  ( ( sum_ i  e.  ( 1 ... I
) ( ( X `
 ( L `  i ) )  x. 
[_ i  /  n ]_ A )  +  sum_ i  e.  ( (
I  +  1 )..^ ( J  +  1 ) ) ( ( X `  ( L `
 i ) )  x.  [_ i  /  n ]_ A ) )  -  sum_ i  e.  ( 1 ... I ) ( ( X `  ( L `  i ) )  x.  [_ i  /  n ]_ A ) )  =  ( (  seq 1 (  +  ,  F ) `  J )  -  (  seq 1 (  +  ,  F ) `  I
) ) )
80 fzfid 12187 . . . . . 6  |-  ( ph  ->  ( 1 ... I
)  e.  Fin )
8180, 77fsumcl 13792 . . . . 5  |-  ( ph  -> 
sum_ i  e.  ( 1 ... I ) ( ( X `  ( L `  i ) )  x.  [_ i  /  n ]_ A )  e.  CC )
82 fzofi 12188 . . . . . . 7  |-  ( ( I  +  1 )..^ ( J  +  1 ) )  e.  Fin
8382a1i 11 . . . . . 6  |-  ( ph  ->  ( ( I  + 
1 )..^ ( J  +  1 ) )  e.  Fin )
84 ssun2 3631 . . . . . . . . 9  |-  ( ( I  +  1 )..^ ( J  +  1 ) )  C_  (
( 1..^ ( I  +  1 ) )  u.  ( ( I  +  1 )..^ ( J  +  1 ) ) )
8584, 13syl5sseqr 3514 . . . . . . . 8  |-  ( ph  ->  ( ( I  + 
1 )..^ ( J  +  1 ) ) 
C_  ( 1..^ ( J  +  1 ) ) )
8685sselda 3465 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  i  e.  ( 1..^ ( J  + 
1 ) ) )
8786, 43syldan 473 . . . . . 6  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  ( ( X `  ( L `  i ) )  x. 
[_ i  /  n ]_ A )  e.  CC )
8883, 87fsumcl 13792 . . . . 5  |-  ( ph  -> 
sum_ i  e.  ( ( I  +  1 )..^ ( J  + 
1 ) ) ( ( X `  ( L `  i )
)  x.  [_ i  /  n ]_ A )  e.  CC )
8981, 88pncan2d 9990 . . . 4  |-  ( ph  ->  ( ( sum_ i  e.  ( 1 ... I
) ( ( X `
 ( L `  i ) )  x. 
[_ i  /  n ]_ A )  +  sum_ i  e.  ( (
I  +  1 )..^ ( J  +  1 ) ) ( ( X `  ( L `
 i ) )  x.  [_ i  /  n ]_ A ) )  -  sum_ i  e.  ( 1 ... I ) ( ( X `  ( L `  i ) )  x.  [_ i  /  n ]_ A ) )  =  sum_ i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) ( ( X `  ( L `  i ) )  x.  [_ i  /  n ]_ A ) )
9079, 89eqtr3d 2466 . . 3  |-  ( ph  ->  ( (  seq 1
(  +  ,  F
) `  J )  -  (  seq 1
(  +  ,  F
) `  I )
)  =  sum_ i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) ( ( X `  ( L `  i ) )  x.  [_ i  /  n ]_ A ) )
9190fveq2d 5883 . 2  |-  ( ph  ->  ( abs `  (
(  seq 1 (  +  ,  F ) `  J )  -  (  seq 1 (  +  ,  F ) `  I
) ) )  =  ( abs `  sum_ i  e.  ( (
I  +  1 )..^ ( J  +  1 ) ) ( ( X `  ( L `
 i ) )  x.  [_ i  /  n ]_ A ) ) )
9288abscld 13491 . . 3  |-  ( ph  ->  ( abs `  sum_ i  e.  ( (
I  +  1 )..^ ( J  +  1 ) ) ( ( X `  ( L `
 i ) )  x.  [_ i  /  n ]_ A ) )  e.  RR )
93 2re 10681 . . . . . 6  |-  2  e.  RR
9493a1i 11 . . . . 5  |-  ( ph  ->  2  e.  RR )
95 dchrisum.9 . . . . 5  |-  ( ph  ->  R  e.  RR )
9694, 95remulcld 9673 . . . 4  |-  ( ph  ->  ( 2  x.  R
)  e.  RR )
9740ralrimiva 2840 . . . . 5  |-  ( ph  ->  A. i  e.  NN  [_ i  /  n ]_ A  e.  RR )
98 csbeq1 3399 . . . . . . 7  |-  ( i  =  ( I  + 
1 )  ->  [_ i  /  n ]_ A  = 
[_ ( I  + 
1 )  /  n ]_ A )
9998eleq1d 2492 . . . . . 6  |-  ( i  =  ( I  + 
1 )  ->  ( [_ i  /  n ]_ A  e.  RR  <->  [_ ( I  +  1 )  /  n ]_ A  e.  RR )
)
10099rspcv 3179 . . . . 5  |-  ( ( I  +  1 )  e.  NN  ->  ( A. i  e.  NN  [_ i  /  n ]_ A  e.  RR  ->  [_ ( I  +  1 )  /  n ]_ A  e.  RR )
)
1014, 97, 100sylc 63 . . . 4  |-  ( ph  ->  [_ ( I  + 
1 )  /  n ]_ A  e.  RR )
10296, 101remulcld 9673 . . 3  |-  ( ph  ->  ( ( 2  x.  R )  x.  [_ ( I  +  1
)  /  n ]_ A )  e.  RR )
103 dchrisumlem2.1 . . . . 5  |-  ( ph  ->  U  e.  RR+ )
10433ralrimiva 2840 . . . . 5  |-  ( ph  ->  A. n  e.  RR+  A  e.  RR )
105 nfcsb1v 3412 . . . . . . 7  |-  F/_ n [_ U  /  n ]_ A
106105nfel1 2601 . . . . . 6  |-  F/ n [_ U  /  n ]_ A  e.  RR
107 csbeq1a 3405 . . . . . . 7  |-  ( n  =  U  ->  A  =  [_ U  /  n ]_ A )
108107eleq1d 2492 . . . . . 6  |-  ( n  =  U  ->  ( A  e.  RR  <->  [_ U  /  n ]_ A  e.  RR ) )
109106, 108rspc 3177 . . . . 5  |-  ( U  e.  RR+  ->  ( A. n  e.  RR+  A  e.  RR  ->  [_ U  /  n ]_ A  e.  RR ) )
110103, 104, 109sylc 63 . . . 4  |-  ( ph  ->  [_ U  /  n ]_ A  e.  RR )
11196, 110remulcld 9673 . . 3  |-  ( ph  ->  ( ( 2  x.  R )  x.  [_ U  /  n ]_ A
)  e.  RR )
11271, 5syl6eleqr 2522 . . . . . . . . . . . 12  |-  ( ph  ->  J  e.  NN )
113112peano2nnd 10628 . . . . . . . . . . 11  |-  ( ph  ->  ( J  +  1 )  e.  NN )
114113nnrpd 11341 . . . . . . . . . 10  |-  ( ph  ->  ( J  +  1 )  e.  RR+ )
11519, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36dchrisumlema 24318 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( J  +  1 )  e.  RR+  ->  [_ ( J  + 
1 )  /  n ]_ A  e.  RR )  /\  ( ( J  +  1 )  e.  ( M [,) +oo )  ->  0  <_  [_ ( J  +  1 )  /  n ]_ A
) ) )
116115simpld 461 . . . . . . . . . 10  |-  ( ph  ->  ( ( J  + 
1 )  e.  RR+  ->  [_ ( J  + 
1 )  /  n ]_ A  e.  RR ) )
117114, 116mpd 15 . . . . . . . . 9  |-  ( ph  ->  [_ ( J  + 
1 )  /  n ]_ A  e.  RR )
118117recnd 9671 . . . . . . . 8  |-  ( ph  ->  [_ ( J  + 
1 )  /  n ]_ A  e.  CC )
119 fzofi 12188 . . . . . . . . . 10  |-  ( 0..^ ( J  +  1 ) )  e.  Fin
120119a1i 11 . . . . . . . . 9  |-  ( ph  ->  ( 0..^ ( J  +  1 ) )  e.  Fin )
121 elfzoelz 11922 . . . . . . . . . 10  |-  ( n  e.  ( 0..^ ( J  +  1 ) )  ->  n  e.  ZZ )
12222adantr 467 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  ZZ )  ->  X  e.  D )
123 simpr 463 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  ZZ )  ->  n  e.  ZZ )
12418, 19, 20, 21, 122, 123dchrzrhcl 24165 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ZZ )  ->  ( X `
 ( L `  n ) )  e.  CC )
125121, 124sylan2 477 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 0..^ ( J  + 
1 ) ) )  ->  ( X `  ( L `  n ) )  e.  CC )
126120, 125fsumcl 13792 . . . . . . . 8  |-  ( ph  -> 
sum_ n  e.  (
0..^ ( J  + 
1 ) ) ( X `  ( L `
 n ) )  e.  CC )
127118, 126mulcld 9665 . . . . . . 7  |-  ( ph  ->  ( [_ ( J  +  1 )  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( J  +  1 ) ) ( X `  ( L `  n ) ) )  e.  CC )
128101recnd 9671 . . . . . . . 8  |-  ( ph  ->  [_ ( I  + 
1 )  /  n ]_ A  e.  CC )
129 fzofi 12188 . . . . . . . . . 10  |-  ( 0..^ ( I  +  1 ) )  e.  Fin
130129a1i 11 . . . . . . . . 9  |-  ( ph  ->  ( 0..^ ( I  +  1 ) )  e.  Fin )
131 elfzoelz 11922 . . . . . . . . . 10  |-  ( n  e.  ( 0..^ ( I  +  1 ) )  ->  n  e.  ZZ )
132131, 124sylan2 477 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 0..^ ( I  + 
1 ) ) )  ->  ( X `  ( L `  n ) )  e.  CC )
133130, 132fsumcl 13792 . . . . . . . 8  |-  ( ph  -> 
sum_ n  e.  (
0..^ ( I  + 
1 ) ) ( X `  ( L `
 n ) )  e.  CC )
134128, 133mulcld 9665 . . . . . . 7  |-  ( ph  ->  ( [_ ( I  +  1 )  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( I  +  1 ) ) ( X `  ( L `  n ) ) )  e.  CC )
135127, 134subcld 9988 . . . . . 6  |-  ( ph  ->  ( ( [_ ( J  +  1 )  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( J  + 
1 ) ) ( X `  ( L `
 n ) ) )  -  ( [_ ( I  +  1
)  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( I  +  1 ) ) ( X `  ( L `  n )
) ) )  e.  CC )
136135abscld 13491 . . . . 5  |-  ( ph  ->  ( abs `  (
( [_ ( J  + 
1 )  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( J  +  1 ) ) ( X `  ( L `  n )
) )  -  ( [_ ( I  +  1 )  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( I  +  1 ) ) ( X `  ( L `  n )
) ) ) )  e.  RR )
13786, 17syl 17 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  i  e.  NN )
138 peano2nn 10623 . . . . . . . . . . . . 13  |-  ( i  e.  NN  ->  (
i  +  1 )  e.  NN )
139138nnrpd 11341 . . . . . . . . . . . 12  |-  ( i  e.  NN  ->  (
i  +  1 )  e.  RR+ )
140 nfcsb1v 3412 . . . . . . . . . . . . . . 15  |-  F/_ n [_ ( i  +  1 )  /  n ]_ A
141140nfel1 2601 . . . . . . . . . . . . . 14  |-  F/ n [_ ( i  +  1 )  /  n ]_ A  e.  RR
142 csbeq1a 3405 . . . . . . . . . . . . . . 15  |-  ( n  =  ( i  +  1 )  ->  A  =  [_ ( i  +  1 )  /  n ]_ A )
143142eleq1d 2492 . . . . . . . . . . . . . 14  |-  ( n  =  ( i  +  1 )  ->  ( A  e.  RR  <->  [_ ( i  +  1 )  /  n ]_ A  e.  RR ) )
144141, 143rspc 3177 . . . . . . . . . . . . 13  |-  ( ( i  +  1 )  e.  RR+  ->  ( A. n  e.  RR+  A  e.  RR  ->  [_ ( i  +  1 )  /  n ]_ A  e.  RR ) )
145144impcom 432 . . . . . . . . . . . 12  |-  ( ( A. n  e.  RR+  A  e.  RR  /\  (
i  +  1 )  e.  RR+ )  ->  [_ (
i  +  1 )  /  n ]_ A  e.  RR )
146104, 139, 145syl2an 480 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  NN )  ->  [_ (
i  +  1 )  /  n ]_ A  e.  RR )
147146, 40resubcld 10049 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  NN )  ->  ( [_ ( i  +  1 )  /  n ]_ A  -  [_ i  /  n ]_ A )  e.  RR )
148147recnd 9671 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  NN )  ->  ( [_ ( i  +  1 )  /  n ]_ A  -  [_ i  /  n ]_ A )  e.  CC )
149 fzofi 12188 . . . . . . . . . . . 12  |-  ( 0..^ ( i  +  1 ) )  e.  Fin
150149a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  ( 0..^ ( i  +  1 ) )  e.  Fin )
151 elfzoelz 11922 . . . . . . . . . . . 12  |-  ( n  e.  ( 0..^ ( i  +  1 ) )  ->  n  e.  ZZ )
152151, 124sylan2 477 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  ( 0..^ ( i  +  1 ) ) )  ->  ( X `  ( L `  n ) )  e.  CC )
153150, 152fsumcl 13792 . . . . . . . . . 10  |-  ( ph  -> 
sum_ n  e.  (
0..^ ( i  +  1 ) ) ( X `  ( L `
 n ) )  e.  CC )
154153adantr 467 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  NN )  ->  sum_ n  e.  ( 0..^ ( i  +  1 ) ) ( X `  ( L `  n )
)  e.  CC )
155148, 154mulcld 9665 . . . . . . . 8  |-  ( (
ph  /\  i  e.  NN )  ->  ( (
[_ ( i  +  1 )  /  n ]_ A  -  [_ i  /  n ]_ A )  x.  sum_ n  e.  ( 0..^ ( i  +  1 ) ) ( X `  ( L `
 n ) ) )  e.  CC )
156137, 155syldan 473 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  ( ( [_ ( i  +  1 )  /  n ]_ A  -  [_ i  /  n ]_ A )  x. 
sum_ n  e.  (
0..^ ( i  +  1 ) ) ( X `  ( L `
 n ) ) )  e.  CC )
15783, 156fsumcl 13792 . . . . . 6  |-  ( ph  -> 
sum_ i  e.  ( ( I  +  1 )..^ ( J  + 
1 ) ) ( ( [_ ( i  +  1 )  /  n ]_ A  -  [_ i  /  n ]_ A
)  x.  sum_ n  e.  ( 0..^ ( i  +  1 ) ) ( X `  ( L `  n )
) )  e.  CC )
158157abscld 13491 . . . . 5  |-  ( ph  ->  ( abs `  sum_ i  e.  ( (
I  +  1 )..^ ( J  +  1 ) ) ( (
[_ ( i  +  1 )  /  n ]_ A  -  [_ i  /  n ]_ A )  x.  sum_ n  e.  ( 0..^ ( i  +  1 ) ) ( X `  ( L `
 n ) ) ) )  e.  RR )
159136, 158readdcld 9672 . . . 4  |-  ( ph  ->  ( ( abs `  (
( [_ ( J  + 
1 )  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( J  +  1 ) ) ( X `  ( L `  n )
) )  -  ( [_ ( I  +  1 )  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( I  +  1 ) ) ( X `  ( L `  n )
) ) ) )  +  ( abs `  sum_ i  e.  ( (
I  +  1 )..^ ( J  +  1 ) ) ( (
[_ ( i  +  1 )  /  n ]_ A  -  [_ i  /  n ]_ A )  x.  sum_ n  e.  ( 0..^ ( i  +  1 ) ) ( X `  ( L `
 n ) ) ) ) )  e.  RR )
16026, 41mulcomd 9666 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  NN )  ->  ( ( X `  ( L `
 i ) )  x.  [_ i  /  n ]_ A )  =  ( [_ i  /  n ]_ A  x.  ( X `  ( L `  i ) ) ) )
161 nnnn0 10878 . . . . . . . . . . . . . . . 16  |-  ( i  e.  NN  ->  i  e.  NN0 )
162161adantl 468 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  NN )  ->  i  e. 
NN0 )
163 nn0uz 11195 . . . . . . . . . . . . . . 15  |-  NN0  =  ( ZZ>= `  0 )
164162, 163syl6eleq 2521 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  NN )  ->  i  e.  ( ZZ>= `  0 )
)
165 elfzelz 11802 . . . . . . . . . . . . . . 15  |-  ( n  e.  ( 0 ... i )  ->  n  e.  ZZ )
166124adantlr 720 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  NN )  /\  n  e.  ZZ )  ->  ( X `  ( L `  n ) )  e.  CC )
167165, 166sylan2 477 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  NN )  /\  n  e.  ( 0 ... i
) )  ->  ( X `  ( L `  n ) )  e.  CC )
168164, 167, 63fzosump1 13806 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  NN )  ->  sum_ n  e.  ( 0..^ ( i  +  1 ) ) ( X `  ( L `  n )
)  =  ( sum_ n  e.  ( 0..^ i ) ( X `  ( L `  n ) )  +  ( X `
 ( L `  i ) ) ) )
169168oveq1d 6318 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  NN )  ->  ( sum_ n  e.  ( 0..^ ( i  +  1 ) ) ( X `  ( L `  n ) )  -  sum_ n  e.  ( 0..^ i ) ( X `  ( L `  n )
) )  =  ( ( sum_ n  e.  ( 0..^ i ) ( X `  ( L `
 n ) )  +  ( X `  ( L `  i ) ) )  -  sum_ n  e.  ( 0..^ i ) ( X `  ( L `  n ) ) ) )
170 fzofi 12188 . . . . . . . . . . . . . . 15  |-  ( 0..^ i )  e.  Fin
171170a1i 11 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  NN )  ->  ( 0..^ i )  e.  Fin )
172 elfzoelz 11922 . . . . . . . . . . . . . . 15  |-  ( n  e.  ( 0..^ i )  ->  n  e.  ZZ )
173172, 166sylan2 477 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  NN )  /\  n  e.  ( 0..^ i ) )  ->  ( X `  ( L `  n
) )  e.  CC )
174171, 173fsumcl 13792 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  NN )  ->  sum_ n  e.  ( 0..^ i ) ( X `  ( L `  n )
)  e.  CC )
175174, 26pncan2d 9990 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  NN )  ->  ( (
sum_ n  e.  (
0..^ i ) ( X `  ( L `
 n ) )  +  ( X `  ( L `  i ) ) )  -  sum_ n  e.  ( 0..^ i ) ( X `  ( L `  n ) ) )  =  ( X `  ( L `
 i ) ) )
176169, 175eqtr2d 2465 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  NN )  ->  ( X `
 ( L `  i ) )  =  ( sum_ n  e.  ( 0..^ ( i  +  1 ) ) ( X `  ( L `
 n ) )  -  sum_ n  e.  ( 0..^ i ) ( X `  ( L `
 n ) ) ) )
177176oveq2d 6319 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  NN )  ->  ( [_ i  /  n ]_ A  x.  ( X `  ( L `  i )
) )  =  (
[_ i  /  n ]_ A  x.  ( sum_ n  e.  ( 0..^ ( i  +  1 ) ) ( X `
 ( L `  n ) )  -  sum_ n  e.  ( 0..^ i ) ( X `
 ( L `  n ) ) ) ) )
178160, 177eqtrd 2464 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  NN )  ->  ( ( X `  ( L `
 i ) )  x.  [_ i  /  n ]_ A )  =  ( [_ i  /  n ]_ A  x.  ( sum_ n  e.  ( 0..^ ( i  +  1 ) ) ( X `
 ( L `  n ) )  -  sum_ n  e.  ( 0..^ i ) ( X `
 ( L `  n ) ) ) ) )
179137, 178syldan 473 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  ( ( X `  ( L `  i ) )  x. 
[_ i  /  n ]_ A )  =  (
[_ i  /  n ]_ A  x.  ( sum_ n  e.  ( 0..^ ( i  +  1 ) ) ( X `
 ( L `  n ) )  -  sum_ n  e.  ( 0..^ i ) ( X `
 ( L `  n ) ) ) ) )
180179sumeq2dv 13762 . . . . . . 7  |-  ( ph  -> 
sum_ i  e.  ( ( I  +  1 )..^ ( J  + 
1 ) ) ( ( X `  ( L `  i )
)  x.  [_ i  /  n ]_ A )  =  sum_ i  e.  ( ( I  +  1 )..^ ( J  + 
1 ) ) (
[_ i  /  n ]_ A  x.  ( sum_ n  e.  ( 0..^ ( i  +  1 ) ) ( X `
 ( L `  n ) )  -  sum_ n  e.  ( 0..^ i ) ( X `
 ( L `  n ) ) ) ) )
181 csbeq1 3399 . . . . . . . . 9  |-  ( k  =  i  ->  [_ k  /  n ]_ A  = 
[_ i  /  n ]_ A )
182 oveq2 6311 . . . . . . . . . 10  |-  ( k  =  i  ->  (
0..^ k )  =  ( 0..^ i ) )
183182sumeq1d 13760 . . . . . . . . 9  |-  ( k  =  i  ->  sum_ n  e.  ( 0..^ k ) ( X `  ( L `  n )
)  =  sum_ n  e.  ( 0..^ i ) ( X `  ( L `  n )
) )
184181, 183jca 535 . . . . . . . 8  |-  ( k  =  i  ->  ( [_ k  /  n ]_ A  =  [_ i  /  n ]_ A  /\  sum_
n  e.  ( 0..^ k ) ( X `
 ( L `  n ) )  = 
sum_ n  e.  (
0..^ i ) ( X `  ( L `
 n ) ) ) )
185 csbeq1 3399 . . . . . . . . 9  |-  ( k  =  ( i  +  1 )  ->  [_ k  /  n ]_ A  = 
[_ ( i  +  1 )  /  n ]_ A )
186 oveq2 6311 . . . . . . . . . 10  |-  ( k  =  ( i  +  1 )  ->  (
0..^ k )  =  ( 0..^ ( i  +  1 ) ) )
187186sumeq1d 13760 . . . . . . . . 9  |-  ( k  =  ( i  +  1 )  ->  sum_ n  e.  ( 0..^ k ) ( X `  ( L `  n )
)  =  sum_ n  e.  ( 0..^ ( i  +  1 ) ) ( X `  ( L `  n )
) )
188185, 187jca 535 . . . . . . . 8  |-  ( k  =  ( i  +  1 )  ->  ( [_ k  /  n ]_ A  =  [_ (
i  +  1 )  /  n ]_ A  /\  sum_ n  e.  ( 0..^ k ) ( X `  ( L `
 n ) )  =  sum_ n  e.  ( 0..^ ( i  +  1 ) ) ( X `  ( L `
 n ) ) ) )
189 csbeq1 3399 . . . . . . . . 9  |-  ( k  =  ( I  + 
1 )  ->  [_ k  /  n ]_ A  = 
[_ ( I  + 
1 )  /  n ]_ A )
190 oveq2 6311 . . . . . . . . . 10  |-  ( k  =  ( I  + 
1 )  ->  (
0..^ k )  =  ( 0..^ ( I  +  1 ) ) )
191190sumeq1d 13760 . . . . . . . . 9  |-  ( k  =  ( I  + 
1 )  ->  sum_ n  e.  ( 0..^ k ) ( X `  ( L `  n )
)  =  sum_ n  e.  ( 0..^ ( I  +  1 ) ) ( X `  ( L `  n )
) )
192189, 191jca 535 . . . . . . . 8  |-  ( k  =  ( I  + 
1 )  ->  ( [_ k  /  n ]_ A  =  [_ (
I  +  1 )  /  n ]_ A  /\  sum_ n  e.  ( 0..^ k ) ( X `  ( L `
 n ) )  =  sum_ n  e.  ( 0..^ ( I  + 
1 ) ) ( X `  ( L `
 n ) ) ) )
193 csbeq1 3399 . . . . . . . . 9  |-  ( k  =  ( J  + 
1 )  ->  [_ k  /  n ]_ A  = 
[_ ( J  + 
1 )  /  n ]_ A )
194 oveq2 6311 . . . . . . . . . 10  |-  ( k  =  ( J  + 
1 )  ->  (
0..^ k )  =  ( 0..^ ( J  +  1 ) ) )
195194sumeq1d 13760 . . . . . . . . 9  |-  ( k  =  ( J  + 
1 )  ->  sum_ n  e.  ( 0..^ k ) ( X `  ( L `  n )
)  =  sum_ n  e.  ( 0..^ ( J  +  1 ) ) ( X `  ( L `  n )
) )
196193, 195jca 535 . . . . . . . 8  |-  ( k  =  ( J  + 
1 )  ->  ( [_ k  /  n ]_ A  =  [_ ( J  +  1 )  /  n ]_ A  /\  sum_ n  e.  ( 0..^ k ) ( X `  ( L `
 n ) )  =  sum_ n  e.  ( 0..^ ( J  + 
1 ) ) ( X `  ( L `
 n ) ) ) )
197 elfzuz 11798 . . . . . . . . . 10  |-  ( k  e.  ( ( I  +  1 ) ... ( J  +  1 ) )  ->  k  e.  ( ZZ>= `  ( I  +  1 ) ) )
198 eluznn 11231 . . . . . . . . . 10  |-  ( ( ( I  +  1 )  e.  NN  /\  k  e.  ( ZZ>= `  ( I  +  1
) ) )  -> 
k  e.  NN )
1994, 197, 198syl2an 480 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( ( I  + 
1 ) ... ( J  +  1 ) ) )  ->  k  e.  NN )
20041ralrimiva 2840 . . . . . . . . . 10  |-  ( ph  ->  A. i  e.  NN  [_ i  /  n ]_ A  e.  CC )
201 csbeq1 3399 . . . . . . . . . . . 12  |-  ( i  =  k  ->  [_ i  /  n ]_ A  = 
[_ k  /  n ]_ A )
202201eleq1d 2492 . . . . . . . . . . 11  |-  ( i  =  k  ->  ( [_ i  /  n ]_ A  e.  CC  <->  [_ k  /  n ]_ A  e.  CC )
)
203202rspccva 3182 . . . . . . . . . 10  |-  ( ( A. i  e.  NN  [_ i  /  n ]_ A  e.  CC  /\  k  e.  NN )  ->  [_ k  /  n ]_ A  e.  CC )
204200, 203sylan 474 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  NN )  ->  [_ k  /  n ]_ A  e.  CC )
205199, 204syldan 473 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( ( I  + 
1 ) ... ( J  +  1 ) ) )  ->  [_ k  /  n ]_ A  e.  CC )
206 fzofi 12188 . . . . . . . . . . 11  |-  ( 0..^ k )  e.  Fin
207206a1i 11 . . . . . . . . . 10  |-  ( ph  ->  ( 0..^ k )  e.  Fin )
208 elfzoelz 11922 . . . . . . . . . . 11  |-  ( n  e.  ( 0..^ k )  ->  n  e.  ZZ )
209208, 124sylan2 477 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( 0..^ k ) )  ->  ( X `  ( L `  n ) )  e.  CC )
210207, 209fsumcl 13792 . . . . . . . . 9  |-  ( ph  -> 
sum_ n  e.  (
0..^ k ) ( X `  ( L `
 n ) )  e.  CC )
211210adantr 467 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( ( I  + 
1 ) ... ( J  +  1 ) ) )  ->  sum_ n  e.  ( 0..^ k ) ( X `  ( L `  n )
)  e.  CC )
212184, 188, 192, 196, 9, 205, 211fsumparts 13859 . . . . . . 7  |-  ( ph  -> 
sum_ i  e.  ( ( I  +  1 )..^ ( J  + 
1 ) ) (
[_ i  /  n ]_ A  x.  ( sum_ n  e.  ( 0..^ ( i  +  1 ) ) ( X `
 ( L `  n ) )  -  sum_ n  e.  ( 0..^ i ) ( X `
 ( L `  n ) ) ) )  =  ( ( ( [_ ( J  +  1 )  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( J  +  1 ) ) ( X `  ( L `  n ) ) )  -  ( [_ ( I  +  1 )  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( I  +  1 ) ) ( X `  ( L `  n )
) ) )  -  sum_ i  e.  ( ( I  +  1 )..^ ( J  +  1 ) ) ( (
[_ ( i  +  1 )  /  n ]_ A  -  [_ i  /  n ]_ A )  x.  sum_ n  e.  ( 0..^ ( i  +  1 ) ) ( X `  ( L `
 n ) ) ) ) )
213180, 212eqtrd 2464 . . . . . 6  |-  ( ph  -> 
sum_ i  e.  ( ( I  +  1 )..^ ( J  + 
1 ) ) ( ( X `  ( L `  i )
)  x.  [_ i  /  n ]_ A )  =  ( ( (
[_ ( J  + 
1 )  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( J  +  1 ) ) ( X `  ( L `  n )
) )  -  ( [_ ( I  +  1 )  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( I  +  1 ) ) ( X `  ( L `  n )
) ) )  -  sum_ i  e.  ( ( I  +  1 )..^ ( J  +  1 ) ) ( (
[_ ( i  +  1 )  /  n ]_ A  -  [_ i  /  n ]_ A )  x.  sum_ n  e.  ( 0..^ ( i  +  1 ) ) ( X `  ( L `
 n ) ) ) ) )
214213fveq2d 5883 . . . . 5  |-  ( ph  ->  ( abs `  sum_ i  e.  ( (
I  +  1 )..^ ( J  +  1 ) ) ( ( X `  ( L `
 i ) )  x.  [_ i  /  n ]_ A ) )  =  ( abs `  (
( ( [_ ( J  +  1 )  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( J  + 
1 ) ) ( X `  ( L `
 n ) ) )  -  ( [_ ( I  +  1
)  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( I  +  1 ) ) ( X `  ( L `  n )
) ) )  -  sum_ i  e.  ( ( I  +  1 )..^ ( J  +  1 ) ) ( (
[_ ( i  +  1 )  /  n ]_ A  -  [_ i  /  n ]_ A )  x.  sum_ n  e.  ( 0..^ ( i  +  1 ) ) ( X `  ( L `
 n ) ) ) ) ) )
215135, 157abs2dif2d 13513 . . . . 5  |-  ( ph  ->  ( abs `  (
( ( [_ ( J  +  1 )  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( J  + 
1 ) ) ( X `  ( L `
 n ) ) )  -  ( [_ ( I  +  1
)  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( I  +  1 ) ) ( X `  ( L `  n )
) ) )  -  sum_ i  e.  ( ( I  +  1 )..^ ( J  +  1 ) ) ( (
[_ ( i  +  1 )  /  n ]_ A  -  [_ i  /  n ]_ A )  x.  sum_ n  e.  ( 0..^ ( i  +  1 ) ) ( X `  ( L `
 n ) ) ) ) )  <_ 
( ( abs `  (
( [_ ( J  + 
1 )  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( J  +  1 ) ) ( X `  ( L `  n )
) )  -  ( [_ ( I  +  1 )  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( I  +  1 ) ) ( X `  ( L `  n )
) ) ) )  +  ( abs `  sum_ i  e.  ( (
I  +  1 )..^ ( J  +  1 ) ) ( (
[_ ( i  +  1 )  /  n ]_ A  -  [_ i  /  n ]_ A )  x.  sum_ n  e.  ( 0..^ ( i  +  1 ) ) ( X `  ( L `
 n ) ) ) ) ) )
216214, 215eqbrtrd 4442 . . . 4  |-  ( ph  ->  ( abs `  sum_ i  e.  ( (
I  +  1 )..^ ( J  +  1 ) ) ( ( X `  ( L `
 i ) )  x.  [_ i  /  n ]_ A ) )  <_  ( ( abs `  ( ( [_ ( J  +  1 )  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( J  + 
1 ) ) ( X `  ( L `
 n ) ) )  -  ( [_ ( I  +  1
)  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( I  +  1 ) ) ( X `  ( L `  n )
) ) ) )  +  ( abs `  sum_ i  e.  ( (
I  +  1 )..^ ( J  +  1 ) ) ( (
[_ ( i  +  1 )  /  n ]_ A  -  [_ i  /  n ]_ A )  x.  sum_ n  e.  ( 0..^ ( i  +  1 ) ) ( X `  ( L `
 n ) ) ) ) ) )
217117, 101readdcld 9672 . . . . . . 7  |-  ( ph  ->  ( [_ ( J  +  1 )  /  n ]_ A  +  [_ ( I  +  1
)  /  n ]_ A )  e.  RR )
218217, 95remulcld 9673 . . . . . 6  |-  ( ph  ->  ( ( [_ ( J  +  1 )  /  n ]_ A  +  [_ ( I  + 
1 )  /  n ]_ A )  x.  R
)  e.  RR )
219181, 185, 189, 193, 9, 205telfsumo 13855 . . . . . . . 8  |-  ( ph  -> 
sum_ i  e.  ( ( I  +  1 )..^ ( J  + 
1 ) ) (
[_ i  /  n ]_ A  -  [_ (
i  +  1 )  /  n ]_ A
)  =  ( [_ ( I  +  1
)  /  n ]_ A  -  [_ ( J  +  1 )  /  n ]_ A ) )
220137, 40syldan 473 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  [_ i  /  n ]_ A  e.  RR )
221137, 146syldan 473 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  [_ ( i  +  1 )  /  n ]_ A  e.  RR )
222220, 221resubcld 10049 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  ( [_ i  /  n ]_ A  -  [_ ( i  +  1 )  /  n ]_ A )  e.  RR )
22383, 222fsumrecl 13793 . . . . . . . 8  |-  ( ph  -> 
sum_ i  e.  ( ( I  +  1 )..^ ( J  + 
1 ) ) (
[_ i  /  n ]_ A  -  [_ (
i  +  1 )  /  n ]_ A
)  e.  RR )
224219, 223eqeltrrd 2512 . . . . . . 7  |-  ( ph  ->  ( [_ ( I  +  1 )  /  n ]_ A  -  [_ ( J  +  1
)  /  n ]_ A )  e.  RR )
225224, 95remulcld 9673 . . . . . 6  |-  ( ph  ->  ( ( [_ (
I  +  1 )  /  n ]_ A  -  [_ ( J  + 
1 )  /  n ]_ A )  x.  R
)  e.  RR )
226127abscld 13491 . . . . . . . 8  |-  ( ph  ->  ( abs `  ( [_ ( J  +  1 )  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( J  +  1 ) ) ( X `  ( L `  n )
) ) )  e.  RR )
227134abscld 13491 . . . . . . . 8  |-  ( ph  ->  ( abs `  ( [_ ( I  +  1 )  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( I  +  1 ) ) ( X `  ( L `  n )
) ) )  e.  RR )
228226, 227readdcld 9672 . . . . . . 7  |-  ( ph  ->  ( ( abs `  ( [_ ( J  +  1 )  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( J  +  1 ) ) ( X `  ( L `  n )
) ) )  +  ( abs `  ( [_ ( I  +  1 )  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( I  +  1 ) ) ( X `  ( L `  n )
) ) ) )  e.  RR )
229127, 134abs2dif2d 13513 . . . . . . 7  |-  ( ph  ->  ( abs `  (
( [_ ( J  + 
1 )  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( J  +  1 ) ) ( X `  ( L `  n )
) )  -  ( [_ ( I  +  1 )  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( I  +  1 ) ) ( X `  ( L `  n )
) ) ) )  <_  ( ( abs `  ( [_ ( J  +  1 )  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( J  +  1 ) ) ( X `  ( L `  n ) ) ) )  +  ( abs `  ( [_ ( I  +  1 )  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( I  +  1 ) ) ( X `  ( L `  n )
) ) ) ) )
230117, 95remulcld 9673 . . . . . . . . 9  |-  ( ph  ->  ( [_ ( J  +  1 )  /  n ]_ A  x.  R
)  e.  RR )
231101, 95remulcld 9673 . . . . . . . . 9  |-  ( ph  ->  ( [_ ( I  +  1 )  /  n ]_ A  x.  R
)  e.  RR )
232118, 126absmuld 13509 . . . . . . . . . . 11  |-  ( ph  ->  ( abs `  ( [_ ( J  +  1 )  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( J  +  1 ) ) ( X `  ( L `  n )
) ) )  =  ( ( abs `  [_ ( J  +  1 )  /  n ]_ A
)  x.  ( abs `  sum_ n  e.  ( 0..^ ( J  + 
1 ) ) ( X `  ( L `
 n ) ) ) ) )
233 eluzelre 11171 . . . . . . . . . . . . . . . . . . 19  |-  ( i  e.  ( ZZ>= `  M
)  ->  i  e.  RR )
234233adantl 468 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  i  e.  RR )
235 eluzle 11173 . . . . . . . . . . . . . . . . . . 19  |-  ( i  e.  ( ZZ>= `  M
)  ->  M  <_  i )
236235adantl 468 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  M  <_  i )
23732nnred 10626 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  M  e.  RR )
238237adantr 467 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  M  e.  RR )
239 elicopnf 11732 . . . . . . . . . . . . . . . . . . 19  |-  ( M  e.  RR  ->  (
i  e.  ( M [,) +oo )  <->  ( i  e.  RR  /\  M  <_ 
i ) ) )
240238, 239syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  ( i  e.  ( M [,) +oo ) 
<->  ( i  e.  RR  /\  M  <_  i )
) )
241234, 236, 240mpbir2and 931 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  i  e.  ( M [,) +oo )
)
242241ex 436 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( i  e.  (
ZZ>= `  M )  -> 
i  e.  ( M [,) +oo ) ) )
243242ssrdv 3471 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ZZ>= `  M )  C_  ( M [,) +oo ) )
24432nnzd 11041 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  M  e.  ZZ )
24549peano2zd 11045 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( I  +  1 )  e.  ZZ )
246103rpred 11343 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  U  e.  RR )
2474nnred 10626 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( I  +  1 )  e.  RR )
248 dchrisumlem2.2 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  M  <_  U )
249 dchrisumlem2.3 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  U  <_  ( I  +  1 ) )
250237, 246, 247, 248, 249letrd 9794 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  M  <_  ( I  +  1 ) )
251 eluz2 11167 . . . . . . . . . . . . . . . . 17  |-  ( ( I  +  1 )  e.  ( ZZ>= `  M
)  <->  ( M  e.  ZZ  /\  ( I  +  1 )  e.  ZZ  /\  M  <_ 
( I  +  1 ) ) )
252244, 245, 250, 251syl3anbrc 1190 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( I  +  1 )  e.  ( ZZ>= `  M ) )
253 uztrn 11177 . . . . . . . . . . . . . . . 16  |-  ( ( ( J  +  1 )  e.  ( ZZ>= `  ( I  +  1
) )  /\  (
I  +  1 )  e.  ( ZZ>= `  M
) )  ->  ( J  +  1 )  e.  ( ZZ>= `  M
) )
2549, 252, 253syl2anc 666 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( J  +  1 )  e.  ( ZZ>= `  M ) )
255243, 254sseldd 3466 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( J  +  1 )  e.  ( M [,) +oo ) )
256115simprd 465 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( J  + 
1 )  e.  ( M [,) +oo )  ->  0  <_  [_ ( J  +  1 )  /  n ]_ A ) )
257255, 256mpd 15 . . . . . . . . . . . . 13  |-  ( ph  ->  0  <_  [_ ( J  +  1 )  /  n ]_ A )
258117, 257absidd 13478 . . . . . . . . . . . 12  |-  ( ph  ->  ( abs `  [_ ( J  +  1 )  /  n ]_ A
)  =  [_ ( J  +  1 )  /  n ]_ A
)
259258oveq1d 6318 . . . . . . . . . . 11  |-  ( ph  ->  ( ( abs `  [_ ( J  +  1 )  /  n ]_ A
)  x.  ( abs `  sum_ n  e.  ( 0..^ ( J  + 
1 ) ) ( X `  ( L `
 n ) ) ) )  =  (
[_ ( J  + 
1 )  /  n ]_ A  x.  ( abs `  sum_ n  e.  ( 0..^ ( J  + 
1 ) ) ( X `  ( L `
 n ) ) ) ) )
260232, 259eqtrd 2464 . . . . . . . . . 10  |-  ( ph  ->  ( abs `  ( [_ ( J  +  1 )  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( J  +  1 ) ) ( X `  ( L `  n )
) ) )  =  ( [_ ( J  +  1 )  /  n ]_ A  x.  ( abs `  sum_ n  e.  ( 0..^ ( J  + 
1 ) ) ( X `  ( L `
 n ) ) ) ) )
261126abscld 13491 . . . . . . . . . . 11  |-  ( ph  ->  ( abs `  sum_ n  e.  ( 0..^ ( J  +  1 ) ) ( X `  ( L `  n ) ) )  e.  RR )
262113nnnn0d 10927 . . . . . . . . . . . 12  |-  ( ph  ->  ( J  +  1 )  e.  NN0 )
263 dchrisum.10 . . . . . . . . . . . . 13  |-  ( ph  ->  A. u  e.  ( 0..^ N ) ( abs `  sum_ n  e.  ( 0..^ u ) ( X `  ( L `  n )
) )  <_  R
)
26419, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36, 95, 263dchrisumlem1 24319 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( J  +  1 )  e. 
NN0 )  ->  ( abs `  sum_ n  e.  ( 0..^ ( J  + 
1 ) ) ( X `  ( L `
 n ) ) )  <_  R )
265262, 264mpdan 673 . . . . . . . . . . 11  |-  ( ph  ->  ( abs `  sum_ n  e.  ( 0..^ ( J  +  1 ) ) ( X `  ( L `  n ) ) )  <_  R
)
266261, 95, 117, 257, 265lemul2ad 10549 . . . . . . . . . 10  |-  ( ph  ->  ( [_ ( J  +  1 )  /  n ]_ A  x.  ( abs `  sum_ n  e.  ( 0..^ ( J  + 
1 ) ) ( X `  ( L `
 n ) ) ) )  <_  ( [_ ( J  +  1 )  /  n ]_ A  x.  R )
)
267260, 266eqbrtrd 4442 . . . . . . . . 9  |-  ( ph  ->  ( abs `  ( [_ ( J  +  1 )  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( J  +  1 ) ) ( X `  ( L `  n )
) ) )  <_ 
( [_ ( J  + 
1 )  /  n ]_ A  x.  R
) )
268128, 133absmuld 13509 . . . . . . . . . . 11  |-  ( ph  ->  ( abs `  ( [_ ( I  +  1 )  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( I  +  1 ) ) ( X `  ( L `  n )
) ) )  =  ( ( abs `  [_ (
I  +  1 )  /  n ]_ A
)  x.  ( abs `  sum_ n  e.  ( 0..^ ( I  + 
1 ) ) ( X `  ( L `
 n ) ) ) ) )
269243, 252sseldd 3466 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( I  +  1 )  e.  ( M [,) +oo ) )
27019, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36dchrisumlema 24318 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( I  +  1 )  e.  RR+  ->  [_ ( I  + 
1 )  /  n ]_ A  e.  RR )  /\  ( ( I  +  1 )  e.  ( M [,) +oo )  ->  0  <_  [_ (
I  +  1 )  /  n ]_ A
) ) )
271270simprd 465 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( I  + 
1 )  e.  ( M [,) +oo )  ->  0  <_  [_ ( I  +  1 )  /  n ]_ A ) )
272269, 271mpd 15 . . . . . . . . . . . . 13  |-  ( ph  ->  0  <_  [_ ( I  +  1 )  /  n ]_ A )
273101, 272absidd 13478 . . . . . . . . . . . 12  |-  ( ph  ->  ( abs `  [_ (
I  +  1 )  /  n ]_ A
)  =  [_ (
I  +  1 )  /  n ]_ A
)
274273oveq1d 6318 . . . . . . . . . . 11  |-  ( ph  ->  ( ( abs `  [_ (
I  +  1 )  /  n ]_ A
)  x.  ( abs `  sum_ n  e.  ( 0..^ ( I  + 
1 ) ) ( X `  ( L `
 n ) ) ) )  =  (
[_ ( I  + 
1 )  /  n ]_ A  x.  ( abs `  sum_ n  e.  ( 0..^ ( I  + 
1 ) ) ( X `  ( L `
 n ) ) ) ) )
275268, 274eqtrd 2464 . . . . . . . . . 10  |-  ( ph  ->  ( abs `  ( [_ ( I  +  1 )  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( I  +  1 ) ) ( X `  ( L `  n )
) ) )  =  ( [_ ( I  +  1 )  /  n ]_ A  x.  ( abs `  sum_ n  e.  ( 0..^ ( I  + 
1 ) ) ( X `  ( L `
 n ) ) ) ) )
276133abscld 13491 . . . . . . . . . . 11  |-  ( ph  ->  ( abs `  sum_ n  e.  ( 0..^ ( I  +  1 ) ) ( X `  ( L `  n ) ) )  e.  RR )
2774nnnn0d 10927 . . . . . . . . . . . 12  |-  ( ph  ->  ( I  +  1 )  e.  NN0 )
27819, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36, 95, 263dchrisumlem1 24319 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( I  +  1 )  e. 
NN0 )  ->  ( abs `  sum_ n  e.  ( 0..^ ( I  + 
1 ) ) ( X `  ( L `
 n ) ) )  <_  R )
279277, 278mpdan 673 . . . . . . . . . . 11  |-  ( ph  ->  ( abs `  sum_ n  e.  ( 0..^ ( I  +  1 ) ) ( X `  ( L `  n ) ) )  <_  R
)
280276, 95, 101, 272, 279lemul2ad 10549 . . . . . . . . . 10  |-  ( ph  ->  ( [_ ( I  +  1 )  /  n ]_ A  x.  ( abs `  sum_ n  e.  ( 0..^ ( I  + 
1 ) ) ( X `  ( L `
 n ) ) ) )  <_  ( [_ ( I  +  1 )  /  n ]_ A  x.  R )
)
281275, 280eqbrtrd 4442 . . . . . . . . 9  |-  ( ph  ->  ( abs `  ( [_ ( I  +  1 )  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( I  +  1 ) ) ( X `  ( L `  n )
) ) )  <_ 
( [_ ( I  + 
1 )  /  n ]_ A  x.  R
) )
282226, 227, 230, 231, 267, 281le2addd 10234 . . . . . . . 8  |-  ( ph  ->  ( ( abs `  ( [_ ( J  +  1 )  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( J  +  1 ) ) ( X `  ( L `  n )
) ) )  +  ( abs `  ( [_ ( I  +  1 )  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( I  +  1 ) ) ( X `  ( L `  n )
) ) ) )  <_  ( ( [_ ( J  +  1
)  /  n ]_ A  x.  R )  +  ( [_ (
I  +  1 )  /  n ]_ A  x.  R ) ) )
28395recnd 9671 . . . . . . . . 9  |-  ( ph  ->  R  e.  CC )
284118, 128, 283adddird 9670 . . . . . . . 8  |-  ( ph  ->  ( ( [_ ( J  +  1 )  /  n ]_ A  +  [_ ( I  + 
1 )  /  n ]_ A )  x.  R
)  =  ( (
[_ ( J  + 
1 )  /  n ]_ A  x.  R
)  +  ( [_ ( I  +  1
)  /  n ]_ A  x.  R )
) )
285282, 284breqtrrd 4448 . . . . . . 7  |-  ( ph  ->  ( ( abs `  ( [_ ( J  +  1 )  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( J  +  1 ) ) ( X `  ( L `  n )
) ) )  +  ( abs `  ( [_ ( I  +  1 )  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( I  +  1 ) ) ( X `  ( L `  n )
) ) ) )  <_  ( ( [_ ( J  +  1
)  /  n ]_ A  +  [_ ( I  +  1 )  /  n ]_ A )  x.  R ) )
286136, 228, 218, 229, 285letrd 9794 . . . . . 6  |-  ( ph  ->  ( abs `  (
( [_ ( J  + 
1 )  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( J  +  1 ) ) ( X `  ( L `  n )
) )  -  ( [_ ( I  +  1 )  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( I  +  1 ) ) ( X `  ( L `  n )
) ) ) )  <_  ( ( [_ ( J  +  1
)  /  n ]_ A  +  [_ ( I  +  1 )  /  n ]_ A )  x.  R ) )
287156abscld 13491 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  ( abs `  ( ( [_ (
i  +  1 )  /  n ]_ A  -  [_ i  /  n ]_ A )  x.  sum_ n  e.  ( 0..^ ( i  +  1 ) ) ( X `  ( L `  n ) ) ) )  e.  RR )
28883, 287fsumrecl 13793 . . . . . . 7  |-  ( ph  -> 
sum_ i  e.  ( ( I  +  1 )..^ ( J  + 
1 ) ) ( abs `  ( (
[_ ( i  +  1 )  /  n ]_ A  -  [_ i  /  n ]_ A )  x.  sum_ n  e.  ( 0..^ ( i  +  1 ) ) ( X `  ( L `
 n ) ) ) )  e.  RR )
28983, 156fsumabs 13854 . . . . . . 7  |-  ( ph  ->  ( abs `  sum_ i  e.  ( (
I  +  1 )..^ ( J  +  1 ) ) ( (
[_ ( i  +  1 )  /  n ]_ A  -  [_ i  /  n ]_ A )  x.  sum_ n  e.  ( 0..^ ( i  +  1 ) ) ( X `  ( L `
 n ) ) ) )  <_  sum_ i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) ( abs `  (
( [_ ( i  +  1 )  /  n ]_ A  -  [_ i  /  n ]_ A )  x.  sum_ n  e.  ( 0..^ ( i  +  1 ) ) ( X `  ( L `
 n ) ) ) ) )
29095adantr 467 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  R  e.  RR )
291222, 290remulcld 9673 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  ( ( [_ i  /  n ]_ A  -  [_ (
i  +  1 )  /  n ]_ A
)  x.  R )  e.  RR )
292137, 148syldan 473 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  ( [_ ( i  +  1 )  /  n ]_ A  -  [_ i  /  n ]_ A )  e.  CC )
293153adantr 467 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  sum_ n  e.  ( 0..^ ( i  +  1 ) ) ( X `  ( L `  n )
)  e.  CC )
294292, 293absmuld 13509 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  ( abs `  ( ( [_ (
i  +  1 )  /  n ]_ A  -  [_ i  /  n ]_ A )  x.  sum_ n  e.  ( 0..^ ( i  +  1 ) ) ( X `  ( L `  n ) ) ) )  =  ( ( abs `  ( [_ ( i  +  1 )  /  n ]_ A  -  [_ i  /  n ]_ A ) )  x.  ( abs `  sum_ n  e.  ( 0..^ ( i  +  1 ) ) ( X `  ( L `  n ) ) ) ) )
295 elfzouz 11926 . . . . . . . . . . . . . . 15  |-  ( i  e.  ( ( I  +  1 )..^ ( J  +  1 ) )  ->  i  e.  ( ZZ>= `  ( I  +  1 ) ) )
296 uztrn 11177 . . . . . . . . . . . . . . 15  |-  ( ( i  e.  ( ZZ>= `  ( I  +  1
) )  /\  (
I  +  1 )  e.  ( ZZ>= `  M
) )  ->  i  e.  ( ZZ>= `  M )
)
297295, 252, 296syl2anr 481 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  i  e.  ( ZZ>= `  M )
)
298 eluznn 11231 . . . . . . . . . . . . . . . . 17  |-  ( ( M  e.  NN  /\  i  e.  ( ZZ>= `  M ) )  -> 
i  e.  NN )
29932, 298sylan 474 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  i  e.  NN )
300299, 139syl 17 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  ( i  +  1 )  e.  RR+ )
301299nnrpd 11341 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  i  e.  RR+ )
302343expia 1208 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( n  e.  RR+  /\  x  e.  RR+ ) )  ->  (
( M  <_  n  /\  n  <_  x )  ->  B  <_  A
) )
303302ralrimivva 2847 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  A. n  e.  RR+  A. x  e.  RR+  (
( M  <_  n  /\  n  <_  x )  ->  B  <_  A
) )
304303adantr 467 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  A. n  e.  RR+  A. x  e.  RR+  ( ( M  <_  n  /\  n  <_  x
)  ->  B  <_  A ) )
305 nfcv 2585 . . . . . . . . . . . . . . . . . 18  |-  F/_ n RR+
306 nfv 1752 . . . . . . . . . . . . . . . . . . 19  |-  F/ n
( M  <_  i  /\  i  <_  x )
307 nfcv 2585 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ n B
308 nfcv 2585 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ n  <_
309307, 308, 60nfbr 4466 . . . . . . . . . . . . . . . . . . 19  |-  F/ n  B  <_  [_ i  /  n ]_ A
310306, 309nfim 1977 . . . . . . . . . . . . . . . . . 18  |-  F/ n
( ( M  <_ 
i  /\  i  <_  x )  ->  B  <_  [_ i  /  n ]_ A )
311305, 310nfral 2812 . . . . . . . . . . . . . . . . 17  |-  F/ n A. x  e.  RR+  (
( M  <_  i  /\  i  <_  x )  ->  B  <_  [_ i  /  n ]_ A )
312 breq2 4425 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  i  ->  ( M  <_  n  <->  M  <_  i ) )
313 breq1 4424 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  i  ->  (
n  <_  x  <->  i  <_  x ) )
314312, 313anbi12d 716 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  i  ->  (
( M  <_  n  /\  n  <_  x )  <-> 
( M  <_  i  /\  i  <_  x ) ) )
31564breq2d 4433 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  i  ->  ( B  <_  A  <->  B  <_  [_ i  /  n ]_ A ) )
316314, 315imbi12d 322 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  i  ->  (
( ( M  <_  n  /\  n  <_  x
)  ->  B  <_  A )  <->  ( ( M  <_  i  /\  i  <_  x )  ->  B  <_  [_ i  /  n ]_ A ) ) )
317316ralbidv 2865 . . . . . . . . . . . . . . . . 17  |-  ( n  =  i  ->  ( A. x  e.  RR+  (
( M  <_  n  /\  n  <_  x )  ->  B  <_  A
)  <->  A. x  e.  RR+  ( ( M  <_ 
i  /\  i  <_  x )  ->  B  <_  [_ i  /  n ]_ A ) ) )
318311, 317rspc 3177 . . . . . . . . . . . . . . . 16  |-  ( i  e.  RR+  ->  ( A. n  e.  RR+  A. x  e.  RR+  ( ( M  <_  n  /\  n  <_  x )  ->  B  <_  A )  ->  A. x  e.  RR+  ( ( M  <_  i  /\  i  <_  x )  ->  B  <_  [_ i  /  n ]_ A ) ) )
319301, 304, 318sylc 63 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  A. x  e.  RR+  ( ( M  <_  i  /\  i  <_  x )  ->  B  <_  [_ i  /  n ]_ A ) )
320234lep1d 10540 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  i  <_  ( i  +  1 ) )
321236, 320jca 535 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  ( M  <_  i  /\  i  <_ 
( i  +  1 ) ) )
322 breq2 4425 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  ( i  +  1 )  ->  (
i  <_  x  <->  i  <_  ( i  +  1 ) ) )
323322anbi2d 709 . . . . . . . . . . . . . . . . 17  |-  ( x  =  ( i  +  1 )  ->  (
( M  <_  i  /\  i  <_  x )  <-> 
( M  <_  i  /\  i  <_  ( i  +  1 ) ) ) )
324 eqvisset 3090 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  ( i  +  1 )  ->  (
i  +  1 )  e.  _V )
325 eqtr3 2451 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  =  ( i  +  1 )  /\  n  =  ( i  +  1 ) )  ->  x  =  n )
32631equcoms 1846 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  n  ->  A  =  B )
327325, 326syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  =  ( i  +  1 )  /\  n  =  ( i  +  1 ) )  ->  A  =  B )
328324, 327csbied 3423 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  ( i  +  1 )  ->  [_ (
i  +  1 )  /  n ]_ A  =  B )
329328eqcomd 2431 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  ( i  +  1 )  ->  B  =  [_ ( i  +  1 )  /  n ]_ A )
330329breq1d 4431 . . . . . . . . . . . . . . . . 17  |-  ( x  =  ( i  +  1 )  ->  ( B  <_  [_ i  /  n ]_ A  <->  [_ ( i  +  1 )  /  n ]_ A  <_  [_ i  /  n ]_ A ) )
331323, 330imbi12d 322 . . . . . . . . . . . . . . . 16  |-  ( x  =  ( i  +  1 )  ->  (
( ( M  <_ 
i  /\  i  <_  x )  ->  B  <_  [_ i  /  n ]_ A )  <->  ( ( M  <_  i  /\  i  <_  ( i  +  1 ) )  ->  [_ (
i  +  1 )  /  n ]_ A  <_  [_ i  /  n ]_ A ) ) )
332331rspcv 3179 . . . . . . . . . . . . . . 15  |-  ( ( i  +  1 )  e.  RR+  ->  ( A. x  e.  RR+  ( ( M  <_  i  /\  i  <_  x )  ->  B  <_  [_ i  /  n ]_ A )  ->  (
( M  <_  i  /\  i  <_  ( i  +  1 ) )  ->  [_ ( i  +  1 )  /  n ]_ A  <_  [_ i  /  n ]_ A ) ) )
333300, 319, 321, 332syl3c 64 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  [_ ( i  +  1 )  /  n ]_ A  <_  [_ i  /  n ]_ A )
334297, 333syldan 473 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  [_ ( i  +  1 )  /  n ]_ A  <_  [_ i  /  n ]_ A )
335221, 220, 334abssuble0d 13488 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  ( abs `  ( [_ ( i  +  1 )  /  n ]_ A  -  [_ i  /  n ]_ A
) )  =  (
[_ i  /  n ]_ A  -  [_ (
i  +  1 )  /  n ]_ A
) )
336335oveq1d 6318 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  ( ( abs `  ( [_ (
i  +  1 )  /  n ]_ A  -  [_ i  /  n ]_ A ) )  x.  ( abs `  sum_ n  e.  ( 0..^ ( i  +  1 ) ) ( X `  ( L `  n ) ) ) )  =  ( ( [_ i  /  n ]_ A  -  [_ ( i  +  1 )  /  n ]_ A )  x.  ( abs `  sum_ n  e.  ( 0..^ ( i  +  1 ) ) ( X `  ( L `
 n ) ) ) ) )
337294, 336eqtrd 2464 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  ( abs `  ( ( [_ (
i  +  1 )  /  n ]_ A  -  [_ i  /  n ]_ A )  x.  sum_ n  e.  ( 0..^ ( i  +  1 ) ) ( X `  ( L `  n ) ) ) )  =  ( ( [_ i  /  n ]_ A  -  [_ ( i  +  1 )  /  n ]_ A )  x.  ( abs `  sum_ n  e.  ( 0..^ ( i  +  1 ) ) ( X `  ( L `
 n ) ) ) ) )
338293abscld 13491 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  ( abs ` 
sum_ n  e.  (
0..^ ( i  +  1 ) ) ( X `  ( L `
 n ) ) )  e.  RR )
339220, 221subge0d 10205 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  ( 0  <_  ( [_ i  /  n ]_ A  -  [_ ( i  +  1 )  /  n ]_ A )  <->  [_ ( i  +  1 )  /  n ]_ A  <_  [_ i  /  n ]_ A ) )
340334, 339mpbird 236 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  0  <_  (
[_ i  /  n ]_ A  -  [_ (
i  +  1 )  /  n ]_ A
) )
341137peano2nnd 10628 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  ( i  +  1 )  e.  NN )
342341nnnn0d 10927 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  ( i  +  1 )  e. 
NN0 )
34319, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36, 95, 263dchrisumlem1 24319 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( i  +  1 )  e. 
NN0 )  ->  ( abs `  sum_ n  e.  ( 0..^ ( i  +  1 ) ) ( X `  ( L `
 n ) ) )  <_  R )
344342, 343syldan 473 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  ( abs ` 
sum_ n  e.  (
0..^ ( i  +  1 ) ) ( X `  ( L `
 n ) ) )  <_  R )
345338, 290, 222, 340, 344lemul2ad 10549 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  ( ( [_ i  /  n ]_ A  -  [_ (
i  +  1 )  /  n ]_ A
)  x.  ( abs `  sum_ n  e.  ( 0..^ ( i  +  1 ) ) ( X `  ( L `
 n ) ) ) )  <_  (
( [_ i  /  n ]_ A  -  [_ (
i  +  1 )  /  n ]_ A
)  x.  R ) )
346337, 345eqbrtrd 4442 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  ( abs `  ( ( [_ (
i  +  1 )  /  n ]_ A  -  [_ i  /  n ]_ A )  x.  sum_ n  e.  ( 0..^ ( i  +  1 ) ) ( X `  ( L `  n ) ) ) )  <_ 
( ( [_ i  /  n ]_ A  -  [_ ( i  +  1 )  /  n ]_ A )  x.  R
) )
34783, 287, 291, 346fsumle 13852 . . . . . . . 8  |-  ( ph  -> 
sum_ i  e.  ( ( I  +  1 )..^ ( J  + 
1 ) ) ( abs `  ( (
[_ ( i  +  1 )  /  n ]_ A  -  [_ i  /  n ]_ A )  x.  sum_ n  e.  ( 0..^ ( i  +  1 ) ) ( X `  ( L `
 n ) ) ) )  <_  sum_ i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) ( ( [_ i  /  n ]_ A  -  [_ ( i  +  1 )  /  n ]_ A )  x.  R
) )
348222recnd 9671 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  ( [_ i  /  n ]_ A  -  [_ ( i  +  1 )  /  n ]_ A )  e.  CC )
34983, 283, 348fsummulc1 13839 . . . . . . . . 9  |-  ( ph  ->  ( sum_ i  e.  ( ( I  +  1 )..^ ( J  + 
1 ) ) (
[_ i  /  n ]_ A  -  [_ (
i  +  1 )  /  n ]_ A
)  x.  R )  =  sum_ i  e.  ( ( I  +  1 )..^ ( J  + 
1 ) ) ( ( [_ i  /  n ]_ A  -  [_ ( i  +  1 )  /  n ]_ A )  x.  R
) )
350219oveq1d 6318 . . . . . . . . 9  |-  ( ph  ->  ( sum_ i  e.  ( ( I  +  1 )..^ ( J  + 
1 ) ) (
[_ i  /  n ]_ A  -  [_ (
i  +  1 )  /  n ]_ A
)  x.  R )  =  ( ( [_ ( I  +  1
)  /  n ]_ A  -  [_ ( J  +  1 )  /  n ]_ A )  x.  R ) )
351349, 350eqtr3d 2466 . . . . . . . 8  |-  ( ph  -> 
sum_ i  e.  ( ( I  +  1 )..^ ( J  + 
1 ) ) ( ( [_ i  /  n ]_ A  -  [_ ( i  +  1 )  /  n ]_ A )  x.  R
)  =  ( (
[_ ( I  + 
1 )  /  n ]_ A  -  [_ ( J  +  1 )  /  n ]_ A
)  x.  R ) )
352347, 351breqtrd 4446 . . . . . . 7  |-  ( ph  -> 
sum_ i  e.  ( ( I  +  1 )..^ ( J  + 
1 ) ) ( abs `  ( (
[_ ( i  +  1 )  /  n ]_ A  -  [_ i  /  n ]_ A )  x.  sum_ n  e.  ( 0..^ ( i  +  1 ) ) ( X `  ( L `
 n ) ) ) )  <_  (
( [_ ( I  + 
1 )  /  n ]_ A  -  [_ ( J  +  1 )  /  n ]_ A
)  x.  R ) )
353158, 288, 225, 289, 352letrd 9794 . . . . . 6  |-  ( ph  ->  ( abs `  sum_ i  e.  ( (
I  +  1 )..^ ( J  +  1 ) ) ( (
[_ ( i  +  1 )  /  n ]_ A  -  [_ i  /  n ]_ A )  x.  sum_ n  e.  ( 0..^ ( i  +  1 ) ) ( X `  ( L `
 n ) ) ) )  <_  (
( [_ ( I  + 
1 )  /  n ]_ A  -  [_ ( J  +  1 )  /  n ]_ A
)  x.  R ) )
354136, 158, 218, 225, 286, 353le2addd 10234 . . . . 5  |-  ( ph  ->  ( ( abs `  (
( [_ ( J  + 
1 )  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( J  +  1 ) ) ( X `  ( L `  n )
) )  -  ( [_ ( I  +  1 )  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( I  +  1 ) ) ( X `  ( L `  n )
) ) ) )  +  ( abs `  sum_ i  e.  ( (
I  +  1 )..^ ( J  +  1 ) ) ( (
[_ ( i  +  1 )  /  n ]_ A  -  [_ i  /  n ]_ A )  x.  sum_ n  e.  ( 0..^ ( i  +  1 ) ) ( X `  ( L `
 n ) ) ) ) )  <_ 
( ( ( [_ ( J  +  1
)  /  n ]_ A  +  [_ ( I  +  1 )  /  n ]_ A )  x.  R )  +  ( ( [_ ( I  +  1 )  /  n ]_ A  -  [_ ( J  +  1
)  /  n ]_ A )  x.  R
) ) )
3551282timesd 10857 . . . . . . . 8  |-  ( ph  ->  ( 2  x.  [_ ( I  +  1
)  /  n ]_ A )  =  (
[_ ( I  + 
1 )  /  n ]_ A  +  [_ (
I  +  1 )  /  n ]_ A
) )
356128, 118, 128ppncand 10028 . . . . . . . 8  |-  ( ph  ->  ( ( [_ (
I  +  1 )  /  n ]_ A  +  [_ ( J  + 
1 )  /  n ]_ A )  +  (
[_ ( I  + 
1 )  /  n ]_ A  -  [_ ( J  +  1 )  /  n ]_ A
) )  =  (
[_ ( I  + 
1 )  /  n ]_ A  +  [_ (
I  +  1 )  /  n ]_ A
) )
357128, 118addcomd 9837 . . . . . . . . 9  |-  ( ph  ->  ( [_ ( I  +  1 )  /  n ]_ A  +  [_ ( J  +  1
)  /  n ]_ A )  =  (
[_ ( J  + 
1 )  /  n ]_ A  +  [_ (
I  +  1 )  /  n ]_ A
) )
358357oveq1d 6318 . . . . . . . 8  |-  ( ph  ->  ( ( [_ (
I  +  1 )  /  n ]_ A  +  [_ ( J  + 
1 )  /  n ]_ A )  +  (
[_ ( I  + 
1 )  /  n ]_ A  -  [_ ( J  +  1 )  /  n ]_ A
) )  =  ( ( [_ ( J  +  1 )  /  n ]_ A  +  [_ ( I  +  1
)  /  n ]_ A )  +  (
[_ ( I  + 
1 )  /  n ]_ A  -  [_ ( J  +  1 )  /  n ]_ A
) ) )
359355, 356, 3583eqtr2d 2470 . . . . . . 7  |-  ( ph  ->  ( 2  x.  [_ ( I  +  1
)  /  n ]_ A )  =  ( ( [_ ( J  +  1 )  /  n ]_ A  +  [_ ( I  +  1
)  /  n ]_ A )  +  (
[_ ( I  + 
1 )  /  n ]_ A  -  [_ ( J  +  1 )  /  n ]_ A
) ) )
360359oveq1d 6318 . . . . . 6  |-  ( ph  ->  ( ( 2  x. 
[_ ( I  + 
1 )  /  n ]_ A )  x.  R
)  =  ( ( ( [_ ( J  +  1 )  /  n ]_ A  +  [_ ( I  +  1
)  /  n ]_ A )  +  (
[_ ( I  + 
1 )  /  n ]_ A  -  [_ ( J  +  1 )  /  n ]_ A
) )  x.  R
) )
361 2cnd 10684 . . . . . . 7  |-  ( ph  ->  2  e.  CC )
362361, 128, 283mul32d 9845 . . . . . 6  |-  ( ph  ->  ( ( 2  x. 
[_ ( I  + 
1 )  /  n ]_ A )  x.  R
)  =  ( ( 2  x.  R )  x.  [_ ( I  +  1 )  /  n ]_ A ) )
363217recnd 9671 . . . . . . 7  |-  ( ph  ->  ( [_ ( J  +  1 )  /  n ]_ A  +  [_ ( I  +  1
)  /  n ]_ A )  e.  CC )
364224recnd 9671 . . . . . . 7  |-  ( ph  ->  ( [_ ( I  +  1 )  /  n ]_ A  -  [_ ( J  +  1
)  /  n ]_ A )  e.  CC )
365363, 364, 283adddird 9670 . . . . . 6  |-  ( ph  ->  ( ( ( [_ ( J  +  1
)  /  n ]_ A  +  [_ ( I  +  1 )  /  n ]_ A )  +  ( [_ ( I  +  1 )  /  n ]_ A  -  [_ ( J  +  1
)  /  n ]_ A ) )  x.  R )  =  ( ( ( [_ ( J  +  1 )  /  n ]_ A  +  [_ ( I  + 
1 )  /  n ]_ A )  x.  R
)  +  ( (
[_ ( I  + 
1 )  /  n ]_ A  -  [_ ( J  +  1 )  /  n ]_ A
)  x.  R ) ) )
366360, 362, 3653eqtr3d 2472 . . . . 5  |-  ( ph  ->  ( ( 2  x.  R )  x.  [_ ( I  +  1
)  /  n ]_ A )  =  ( ( ( [_ ( J  +  1 )  /  n ]_ A  +  [_ ( I  + 
1 )  /  n ]_ A )  x.  R
)  +  ( (
[_ ( I  + 
1 )  /  n ]_ A  -  [_ ( J  +  1 )  /  n ]_ A
)  x.  R ) ) )
367354, 366breqtrrd 4448 . . . 4  |-  ( ph  ->  ( ( abs `  (
( [_ ( J  + 
1 )  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( J  +  1 ) ) ( X `  ( L `  n )
) )  -  ( [_ ( I  +  1 )  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( I  +  1 ) ) ( X `  ( L `  n )
) ) ) )  +  ( abs `  sum_ i  e.  ( (
I  +  1 )..^ ( J  +  1 ) ) ( (
[_ ( i  +  1 )  /  n ]_ A  -  [_ i  /  n ]_ A )  x.  sum_ n  e.  ( 0..^ ( i  +  1 ) ) ( X `  ( L `
 n ) ) ) ) )  <_ 
( ( 2  x.  R )  x.  [_ ( I  +  1
)  /  n ]_ A ) )
36892, 159, 102, 216, 367letrd 9794 . . 3  |-  ( ph  ->  ( abs `  sum_ i  e.  ( (
I  +  1 )..^ ( J  +  1 ) ) ( ( X `  ( L `
 i ) )  x.  [_ i  /  n ]_ A ) )  <_  ( ( 2  x.  R )  x. 
[_ ( I  + 
1 )  /  n ]_ A ) )
369 2nn0 10888 . . . . . 6  |-  2  e.  NN0
370 nn0ge0 10897 . . . . . 6  |-  ( 2  e.  NN0  ->  0  <_ 
2 )
371369, 370mp1i 13 . . . . 5  |-  ( ph  ->  0  <_  2 )
372 0red 9646 . . . . . 6  |-  ( ph  ->  0  e.  RR )
373126absge0d 13499 . . . . . 6  |-  ( ph  ->  0  <_  ( abs ` 
sum_ n  e.  (
0..^ ( J  + 
1 ) ) ( X `  ( L `
 n ) ) ) )
374372, 261, 95, 373, 265letrd 9794 . . . . 5  |-  ( ph  ->  0  <_  R )
37594, 95, 371, 374mulge0d 10192 . . . 4  |-  ( ph  ->  0  <_  ( 2  x.  R ) )
3764nnrpd 11341 . . . . 5  |-  ( ph  ->  ( I  +  1 )  e.  RR+ )
377 nfv 1752 . . . . . . . . 9  |-  F/ n
( M  <_  U  /\  U  <_  x )
378307, 308, 105nfbr 4466 . . . . . . . . 9  |-  F/ n  B  <_  [_ U  /  n ]_ A
379377, 378nfim 1977 . . . . . . . 8  |-  F/ n
( ( M  <_  U  /\  U  <_  x
)  ->  B  <_  [_ U  /  n ]_ A )
380305, 379nfral 2812 . . . . . . 7  |-  F/ n A. x  e.  RR+  (
( M  <_  U  /\  U  <_  x )  ->  B  <_  [_ U  /  n ]_ A )
381 breq2 4425 . . . . . . . . . 10  |-  ( n  =  U  ->  ( M  <_  n  <->  M  <_  U ) )
382 breq1 4424 . . . . . . . . . 10  |-  ( n  =  U  ->  (
n  <_  x  <->  U  <_  x ) )
383381, 382anbi12d 716 . . . . . . . . 9  |-  ( n  =  U  ->  (
( M  <_  n  /\  n  <_  x )  <-> 
( M  <_  U  /\  U  <_  x ) ) )
384107breq2d 4433 . . . . . . . . 9  |-  ( n  =  U  ->  ( B  <_  A  <->  B  <_  [_ U  /  n ]_ A ) )
385383, 384imbi12d 322 . . . . . . . 8  |-  ( n  =  U  ->  (
( ( M  <_  n  /\  n  <_  x
)  ->  B  <_  A )  <->  ( ( M  <_  U  /\  U  <_  x )  ->  B  <_  [_ U  /  n ]_ A ) ) )
386385ralbidv 2865 . . . . . . 7  |-  ( n  =  U  ->  ( A. x  e.  RR+  (
( M  <_  n  /\  n  <_  x )  ->  B  <_  A
)  <->  A. x  e.  RR+  ( ( M  <_  U  /\  U  <_  x
)  ->  B  <_  [_ U  /  n ]_ A ) ) )
387380, 386rspc 3177 . . . . . 6  |-  ( U  e.  RR+  ->  ( A. n  e.  RR+  A. x  e.  RR+  ( ( M  <_  n  /\  n  <_  x )  ->  B  <_  A )  ->  A. x  e.  RR+  ( ( M  <_  U  /\  U  <_  x )  ->  B  <_  [_ U  /  n ]_ A ) ) )
388103, 303, 387sylc 63 . . . . 5  |-  ( ph  ->  A. x  e.  RR+  ( ( M  <_  U  /\  U  <_  x
)  ->  B  <_  [_ U  /  n ]_ A ) )
389248, 249jca 535 . . . . 5  |-  ( ph  ->  ( M  <_  U  /\  U  <_  ( I  +  1 ) ) )
390 breq2 4425 . . . . . . . 8  |-  ( x  =  ( I  + 
1 )  ->  ( U  <_  x  <->  U  <_  ( I  +  1 ) ) )
391390anbi2d 709 . . . . . . 7  |-  ( x  =  ( I  + 
1 )  ->  (
( M  <_  U  /\  U  <_  x )  <-> 
( M  <_  U  /\  U  <_  ( I  +  1 ) ) ) )
392 eqvisset 3090 . . . . . . . . . 10  |-  ( x  =  ( I  + 
1 )  ->  (
I  +  1 )  e.  _V )
393 eqtr3 2451 . . . . . . . . . . 11  |-  ( ( x  =  ( I  +  1 )  /\  n  =  ( I  +  1 ) )  ->  x  =  n )
394393, 326syl 17 . . . . . . . . . 10  |-  ( ( x  =  ( I  +  1 )  /\  n  =  ( I  +  1 ) )  ->  A  =  B )
395392, 394csbied 3423 . . . . . . . . 9  |-  ( x  =  ( I  + 
1 )  ->  [_ (
I  +  1 )  /  n ]_ A  =  B )
396395eqcomd 2431 . . . . . . . 8  |-  ( x  =  ( I  + 
1 )  ->  B  =  [_ ( I  + 
1 )  /  n ]_ A )
397396breq1d 4431 . . . . . . 7  |-  ( x  =  ( I  + 
1 )  ->  ( B  <_  [_ U  /  n ]_ A  <->  [_ ( I  + 
1 )  /  n ]_ A  <_  [_ U  /  n ]_ A ) )
398391, 397imbi12d 322 . . . . . 6  |-  ( x  =  ( I  + 
1 )  ->  (
( ( M  <_  U  /\  U  <_  x
)  ->  B  <_  [_ U  /  n ]_ A )  <->  ( ( M  <_  U  /\  U  <_  ( I  +  1 ) )  ->  [_ (
I  +  1 )  /  n ]_ A  <_  [_ U  /  n ]_ A ) ) )
399398rspcv 3179 . . . . 5  |-  ( ( I  +  1 )  e.  RR+  ->  ( A. x  e.  RR+  ( ( M  <_  U  /\  U  <_  x )  ->  B  <_  [_ U  /  n ]_ A )  ->  (
( M  <_  U  /\  U  <_  ( I  +  1 ) )  ->  [_ ( I  + 
1 )  /  n ]_ A  <_  [_ U  /  n ]_ A ) ) )
400376, 388, 389, 399syl3c 64 . . . 4  |-  ( ph  ->  [_ ( I  + 
1 )  /  n ]_ A  <_  [_ U  /  n ]_ A )
401101, 110, 96, 375, 400lemul2ad 10549 . . 3  |-  ( ph  ->  ( ( 2  x.  R )  x.  [_ ( I  +  1
)  /  n ]_ A )  <_  (
( 2  x.  R
)  x.  [_ U  /  n ]_ A ) )
40292, 102, 111, 368, 401letrd 9794 . 2  |-  ( ph  ->  ( abs `  sum_ i  e.  ( (
I  +  1 )..^ ( J  +  1 ) ) ( ( X `  ( L `
 i ) )  x.  [_ i  /  n ]_ A ) )  <_  ( ( 2  x.  R )  x. 
[_ U  /  n ]_ A ) )
40391, 402eqbrtrd 4442 1  |-  ( ph  ->  ( abs `  (
(  seq 1 (  +  ,  F ) `  J )  -  (  seq 1 (  +  ,  F ) `  I
) ) )  <_ 
( ( 2  x.  R )  x.  [_ U  /  n ]_ A
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    /\ wa 371    /\ w3a 983    = wceq 1438    e. wcel 1869    =/= wne 2619   A.wral 2776   _Vcvv 3082   [_csb 3396    u. cun 3435    i^i cin 3436   (/)c0 3762   class class class wbr 4421    |-> cmpt 4480   ` cfv 5599  (class class class)co 6303   Fincfn 7575   CCcc 9539   RRcr 9540   0cc0 9541   1c1 9542    + caddc 9544    x. cmul 9546   +oocpnf 9674    <_ cle 9678    - cmin 9862   NNcn 10611   2c2 10661   NN0cn0 10871   ZZcz 10939   ZZ>=cuz 11161   RR+crp 11304   [,)cico 11639   ...cfz 11786  ..^cfzo 11917    seqcseq 12214   abscabs 13291    ~~> r crli 13542   sum_csu 13745   Basecbs 15114   0gc0g 15331   ZRHomczrh 19063  ℤ/nczn 19066  DChrcdchr 24152