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

Theorem dchrisumlem2 23948
Description: Lemma for dchrisum 23950. 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 11804 . . . . . . . . 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 10513 . . . . . . . . . . 11  |-  ( ph  ->  ( I  +  1 )  e.  NN )
5 nnuz 11080 . . . . . . . . . . 11  |-  NN  =  ( ZZ>= `  1 )
64, 5syl6eleq 2500 . . . . . . . . . 10  |-  ( ph  ->  ( I  +  1 )  e.  ( ZZ>= ` 
1 ) )
7 dchrisumlem2.5 . . . . . . . . . . 11  |-  ( ph  ->  J  e.  ( ZZ>= `  I ) )
8 eluzp1p1 11070 . . . . . . . . . . 11  |-  ( J  e.  ( ZZ>= `  I
)  ->  ( J  +  1 )  e.  ( ZZ>= `  ( I  +  1 ) ) )
97, 8syl 17 . . . . . . . . . 10  |-  ( ph  ->  ( J  +  1 )  e.  ( ZZ>= `  ( I  +  1
) ) )
10 elfzuzb 11653 . . . . . . . . . 10  |-  ( ( I  +  1 )  e.  ( 1 ... ( J  +  1 ) )  <->  ( (
I  +  1 )  e.  ( ZZ>= `  1
)  /\  ( J  +  1 )  e.  ( ZZ>= `  ( I  +  1 ) ) ) )
116, 9, 10sylanbrc 662 . . . . . . . . 9  |-  ( ph  ->  ( I  +  1 )  e.  ( 1 ... ( J  + 
1 ) ) )
12 fzosplit 11803 . . . . . . . . 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 12038 . . . . . . . . 9  |-  ( 1..^ ( J  +  1 ) )  e.  Fin
1514a1i 11 . . . . . . . 8  |-  ( ph  ->  ( 1..^ ( J  +  1 ) )  e.  Fin )
16 elfzouz 11776 . . . . . . . . . 10  |-  ( i  e.  ( 1..^ ( J  +  1 ) )  ->  i  e.  ( ZZ>= `  1 )
)
1716, 5syl6eleqr 2501 . . . . . . . . 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 463 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  NN )  ->  X  e.  D )
24 nnz 10847 . . . . . . . . . . . 12  |-  ( i  e.  NN  ->  i  e.  ZZ )
2524adantl 464 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  NN )  ->  i  e.  ZZ )
2618, 19, 20, 21, 23, 25dchrzrhcl 23793 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  NN )  ->  ( X `
 ( L `  i ) )  e.  CC )
27 nnrp 11192 . . . . . . . . . . . . 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 23946 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( i  e.  RR+  ->  [_ i  /  n ]_ A  e.  RR )  /\  ( i  e.  ( M [,) +oo )  ->  0  <_  [_ i  /  n ]_ A ) ) )
3837simpld 457 . . . . . . . . . . . . 13  |-  ( ph  ->  ( i  e.  RR+  ->  [_ i  /  n ]_ A  e.  RR ) )
3927, 38syl5 30 . . . . . . . . . . . 12  |-  ( ph  ->  ( i  e.  NN  ->  [_ i  /  n ]_ A  e.  RR ) )
4039imp 427 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  NN )  ->  [_ i  /  n ]_ A  e.  RR )
4140recnd 9572 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  NN )  ->  [_ i  /  n ]_ A  e.  CC )
4226, 41mulcld 9566 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  NN )  ->  ( ( X `  ( L `
 i ) )  x.  [_ i  /  n ]_ A )  e.  CC )
4317, 42sylan2 472 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 1..^ ( J  + 
1 ) ) )  ->  ( ( X `
 ( L `  i ) )  x. 
[_ i  /  n ]_ A )  e.  CC )
442, 13, 15, 43fsumsplit 13618 . . . . . . 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 11054 . . . . . . . . 9  |-  ( J  e.  ( ZZ>= `  I
)  ->  J  e.  ZZ )
46 fzval3 11834 . . . . . . . . 9  |-  ( J  e.  ZZ  ->  (
1 ... J )  =  ( 1..^ ( J  +  1 ) ) )
477, 45, 463syl 20 . . . . . . . 8  |-  ( ph  ->  ( 1 ... J
)  =  ( 1..^ ( J  +  1 ) ) )
4847sumeq1d 13579 . . . . . . 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 10927 . . . . . . . . . 10  |-  ( ph  ->  I  e.  ZZ )
50 fzval3 11834 . . . . . . . . . 10  |-  ( I  e.  ZZ  ->  (
1 ... I )  =  ( 1..^ ( I  +  1 ) ) )
5149, 50syl 17 . . . . . . . . 9  |-  ( ph  ->  ( 1 ... I
)  =  ( 1..^ ( I  +  1 ) ) )
5251sumeq1d 13579 . . . . . . . 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 6249 . . . . . . 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 2453 . . . . . 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 11685 . . . . . . . 8  |-  ( i  e.  ( 1 ... J )  ->  i  e.  NN )
56 simpr 459 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  NN )  ->  i  e.  NN )
57 nfcv 2564 . . . . . . . . . 10  |-  F/_ n
i
58 nfcv 2564 . . . . . . . . . . 11  |-  F/_ n
( X `  ( L `  i )
)
59 nfcv 2564 . . . . . . . . . . 11  |-  F/_ n  x.
60 nfcsb1v 3388 . . . . . . . . . . 11  |-  F/_ n [_ i  /  n ]_ A
6158, 59, 60nfov 6260 . . . . . . . . . 10  |-  F/_ n
( ( X `  ( L `  i ) )  x.  [_ i  /  n ]_ A )
62 fveq2 5805 . . . . . . . . . . . 12  |-  ( n  =  i  ->  ( L `  n )  =  ( L `  i ) )
6362fveq2d 5809 . . . . . . . . . . 11  |-  ( n  =  i  ->  ( X `  ( L `  n ) )  =  ( X `  ( L `  i )
) )
64 csbeq1a 3381 . . . . . . . . . . 11  |-  ( n  =  i  ->  A  =  [_ i  /  n ]_ A )
6563, 64oveq12d 6252 . . . . . . . . . 10  |-  ( n  =  i  ->  (
( X `  ( L `  n )
)  x.  A )  =  ( ( X `
 ( L `  i ) )  x. 
[_ i  /  n ]_ A ) )
6657, 61, 65, 36fvmptf 5906 . . . . . . . . 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 659 . . . . . . . 8  |-  ( (
ph  /\  i  e.  NN )  ->  ( F `
 i )  =  ( ( X `  ( L `  i ) )  x.  [_ i  /  n ]_ A ) )
6855, 67sylan2 472 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 1 ... J
) )  ->  ( F `  i )  =  ( ( X `
 ( L `  i ) )  x. 
[_ i  /  n ]_ A ) )
693, 5syl6eleq 2500 . . . . . . . 8  |-  ( ph  ->  I  e.  ( ZZ>= ` 
1 ) )
70 uztrn 11061 . . . . . . . 8  |-  ( ( J  e.  ( ZZ>= `  I )  /\  I  e.  ( ZZ>= `  1 )
)  ->  J  e.  ( ZZ>= `  1 )
)
717, 69, 70syl2anc 659 . . . . . . 7  |-  ( ph  ->  J  e.  ( ZZ>= ` 
1 ) )
7255, 42sylan2 472 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 1 ... J
) )  ->  (
( X `  ( L `  i )
)  x.  [_ i  /  n ]_ A )  e.  CC )
7368, 71, 72fsumser 13608 . . . . . 6  |-  ( ph  -> 
sum_ i  e.  ( 1 ... J ) ( ( X `  ( L `  i ) )  x.  [_ i  /  n ]_ A )  =  (  seq 1
(  +  ,  F
) `  J )
)
7454, 73eqtr3d 2445 . . . . 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 11685 . . . . . . 7  |-  ( i  e.  ( 1 ... I )  ->  i  e.  NN )
7675, 67sylan2 472 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 1 ... I
) )  ->  ( F `  i )  =  ( ( X `
 ( L `  i ) )  x. 
[_ i  /  n ]_ A ) )
7775, 42sylan2 472 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 1 ... I
) )  ->  (
( X `  ( L `  i )
)  x.  [_ i  /  n ]_ A )  e.  CC )
7876, 69, 77fsumser 13608 . . . . 5  |-  ( ph  -> 
sum_ i  e.  ( 1 ... I ) ( ( X `  ( L `  i ) )  x.  [_ i  /  n ]_ A )  =  (  seq 1
(  +  ,  F
) `  I )
)
7974, 78oveq12d 6252 . . . 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 12037 . . . . . 6  |-  ( ph  ->  ( 1 ... I
)  e.  Fin )
8180, 77fsumcl 13611 . . . . 5  |-  ( ph  -> 
sum_ i  e.  ( 1 ... I ) ( ( X `  ( L `  i ) )  x.  [_ i  /  n ]_ A )  e.  CC )
82 fzofi 12038 . . . . . . 7  |-  ( ( I  +  1 )..^ ( J  +  1 ) )  e.  Fin
8382a1i 11 . . . . . 6  |-  ( ph  ->  ( ( I  + 
1 )..^ ( J  +  1 ) )  e.  Fin )
84 ssun2 3606 . . . . . . . . 9  |-  ( ( I  +  1 )..^ ( J  +  1 ) )  C_  (
( 1..^ ( I  +  1 ) )  u.  ( ( I  +  1 )..^ ( J  +  1 ) ) )
8584, 13syl5sseqr 3490 . . . . . . . 8  |-  ( ph  ->  ( ( I  + 
1 )..^ ( J  +  1 ) ) 
C_  ( 1..^ ( J  +  1 ) ) )
8685sselda 3441 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  i  e.  ( 1..^ ( J  + 
1 ) ) )
8786, 43syldan 468 . . . . . 6  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  ( ( X `  ( L `  i ) )  x. 
[_ i  /  n ]_ A )  e.  CC )
8883, 87fsumcl 13611 . . . . 5  |-  ( ph  -> 
sum_ i  e.  ( ( I  +  1 )..^ ( J  + 
1 ) ) ( ( X `  ( L `  i )
)  x.  [_ i  /  n ]_ A )  e.  CC )
8981, 88pncan2d 9889 . . . 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 2445 . . 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 5809 . 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 13323 . . 3  |-  ( ph  ->  ( abs `  sum_ i  e.  ( (
I  +  1 )..^ ( J  +  1 ) ) ( ( X `  ( L `
 i ) )  x.  [_ i  /  n ]_ A ) )  e.  RR )
93 2re 10566 . . . . . 6  |-  2  e.  RR
9493a1i 11 . . . . 5  |-  ( ph  ->  2  e.  RR )
95 dchrisum.9 . . . . 5  |-  ( ph  ->  R  e.  RR )
9694, 95remulcld 9574 . . . 4  |-  ( ph  ->  ( 2  x.  R
)  e.  RR )
9740ralrimiva 2817 . . . . 5  |-  ( ph  ->  A. i  e.  NN  [_ i  /  n ]_ A  e.  RR )
98 csbeq1 3375 . . . . . . 7  |-  ( i  =  ( I  + 
1 )  ->  [_ i  /  n ]_ A  = 
[_ ( I  + 
1 )  /  n ]_ A )
9998eleq1d 2471 . . . . . 6  |-  ( i  =  ( I  + 
1 )  ->  ( [_ i  /  n ]_ A  e.  RR  <->  [_ ( I  +  1 )  /  n ]_ A  e.  RR )
)
10099rspcv 3155 . . . . 5  |-  ( ( I  +  1 )  e.  NN  ->  ( A. i  e.  NN  [_ i  /  n ]_ A  e.  RR  ->  [_ ( I  +  1 )  /  n ]_ A  e.  RR )
)
1014, 97, 100sylc 59 . . . 4  |-  ( ph  ->  [_ ( I  + 
1 )  /  n ]_ A  e.  RR )
10296, 101remulcld 9574 . . 3  |-  ( ph  ->  ( ( 2  x.  R )  x.  [_ ( I  +  1
)  /  n ]_ A )  e.  RR )
103 dchrisumlem2.1 . . . . 5  |-  ( ph  ->  U  e.  RR+ )
10433ralrimiva 2817 . . . . 5  |-  ( ph  ->  A. n  e.  RR+  A  e.  RR )
105 nfcsb1v 3388 . . . . . . 7  |-  F/_ n [_ U  /  n ]_ A
106105nfel1 2580 . . . . . 6  |-  F/ n [_ U  /  n ]_ A  e.  RR
107 csbeq1a 3381 . . . . . . 7  |-  ( n  =  U  ->  A  =  [_ U  /  n ]_ A )
108107eleq1d 2471 . . . . . 6  |-  ( n  =  U  ->  ( A  e.  RR  <->  [_ U  /  n ]_ A  e.  RR ) )
109106, 108rspc 3153 . . . . 5  |-  ( U  e.  RR+  ->  ( A. n  e.  RR+  A  e.  RR  ->  [_ U  /  n ]_ A  e.  RR ) )
110103, 104, 109sylc 59 . . . 4  |-  ( ph  ->  [_ U  /  n ]_ A  e.  RR )
11196, 110remulcld 9574 . . 3  |-  ( ph  ->  ( ( 2  x.  R )  x.  [_ U  /  n ]_ A
)  e.  RR )
11271, 5syl6eleqr 2501 . . . . . . . . . . . 12  |-  ( ph  ->  J  e.  NN )
113112peano2nnd 10513 . . . . . . . . . . 11  |-  ( ph  ->  ( J  +  1 )  e.  NN )
114113nnrpd 11220 . . . . . . . . . 10  |-  ( ph  ->  ( J  +  1 )  e.  RR+ )
11519, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36dchrisumlema 23946 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( J  +  1 )  e.  RR+  ->  [_ ( J  + 
1 )  /  n ]_ A  e.  RR )  /\  ( ( J  +  1 )  e.  ( M [,) +oo )  ->  0  <_  [_ ( J  +  1 )  /  n ]_ A
) ) )
116115simpld 457 . . . . . . . . . 10  |-  ( ph  ->  ( ( J  + 
1 )  e.  RR+  ->  [_ ( J  + 
1 )  /  n ]_ A  e.  RR ) )
117114, 116mpd 15 . . . . . . . . 9  |-  ( ph  ->  [_ ( J  + 
1 )  /  n ]_ A  e.  RR )
118117recnd 9572 . . . . . . . 8  |-  ( ph  ->  [_ ( J  + 
1 )  /  n ]_ A  e.  CC )
119 fzofi 12038 . . . . . . . . . 10  |-  ( 0..^ ( J  +  1 ) )  e.  Fin
120119a1i 11 . . . . . . . . 9  |-  ( ph  ->  ( 0..^ ( J  +  1 ) )  e.  Fin )
121 elfzoelz 11772 . . . . . . . . . 10  |-  ( n  e.  ( 0..^ ( J  +  1 ) )  ->  n  e.  ZZ )
12222adantr 463 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  ZZ )  ->  X  e.  D )
123 simpr 459 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  ZZ )  ->  n  e.  ZZ )
12418, 19, 20, 21, 122, 123dchrzrhcl 23793 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ZZ )  ->  ( X `
 ( L `  n ) )  e.  CC )
125121, 124sylan2 472 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 0..^ ( J  + 
1 ) ) )  ->  ( X `  ( L `  n ) )  e.  CC )
126120, 125fsumcl 13611 . . . . . . . 8  |-  ( ph  -> 
sum_ n  e.  (
0..^ ( J  + 
1 ) ) ( X `  ( L `
 n ) )  e.  CC )
127118, 126mulcld 9566 . . . . . . 7  |-  ( ph  ->  ( [_ ( J  +  1 )  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( J  +  1 ) ) ( X `  ( L `  n ) ) )  e.  CC )
128101recnd 9572 . . . . . . . 8  |-  ( ph  ->  [_ ( I  + 
1 )  /  n ]_ A  e.  CC )
129 fzofi 12038 . . . . . . . . . 10  |-  ( 0..^ ( I  +  1 ) )  e.  Fin
130129a1i 11 . . . . . . . . 9  |-  ( ph  ->  ( 0..^ ( I  +  1 ) )  e.  Fin )
131 elfzoelz 11772 . . . . . . . . . 10  |-  ( n  e.  ( 0..^ ( I  +  1 ) )  ->  n  e.  ZZ )
132131, 124sylan2 472 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 0..^ ( I  + 
1 ) ) )  ->  ( X `  ( L `  n ) )  e.  CC )
133130, 132fsumcl 13611 . . . . . . . 8  |-  ( ph  -> 
sum_ n  e.  (
0..^ ( I  + 
1 ) ) ( X `  ( L `
 n ) )  e.  CC )
134128, 133mulcld 9566 . . . . . . 7  |-  ( ph  ->  ( [_ ( I  +  1 )  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( I  +  1 ) ) ( X `  ( L `  n ) ) )  e.  CC )
135127, 134subcld 9887 . . . . . 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 13323 . . . . 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 10508 . . . . . . . . . . . . 13  |-  ( i  e.  NN  ->  (
i  +  1 )  e.  NN )
139138nnrpd 11220 . . . . . . . . . . . 12  |-  ( i  e.  NN  ->  (
i  +  1 )  e.  RR+ )
140 nfcsb1v 3388 . . . . . . . . . . . . . . 15  |-  F/_ n [_ ( i  +  1 )  /  n ]_ A
141140nfel1 2580 . . . . . . . . . . . . . 14  |-  F/ n [_ ( i  +  1 )  /  n ]_ A  e.  RR
142 csbeq1a 3381 . . . . . . . . . . . . . . 15  |-  ( n  =  ( i  +  1 )  ->  A  =  [_ ( i  +  1 )  /  n ]_ A )
143142eleq1d 2471 . . . . . . . . . . . . . 14  |-  ( n  =  ( i  +  1 )  ->  ( A  e.  RR  <->  [_ ( i  +  1 )  /  n ]_ A  e.  RR ) )
144141, 143rspc 3153 . . . . . . . . . . . . 13  |-  ( ( i  +  1 )  e.  RR+  ->  ( A. n  e.  RR+  A  e.  RR  ->  [_ ( i  +  1 )  /  n ]_ A  e.  RR ) )
145144impcom 428 . . . . . . . . . . . 12  |-  ( ( A. n  e.  RR+  A  e.  RR  /\  (
i  +  1 )  e.  RR+ )  ->  [_ (
i  +  1 )  /  n ]_ A  e.  RR )
146104, 139, 145syl2an 475 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  NN )  ->  [_ (
i  +  1 )  /  n ]_ A  e.  RR )
147146, 40resubcld 9948 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  NN )  ->  ( [_ ( i  +  1 )  /  n ]_ A  -  [_ i  /  n ]_ A )  e.  RR )
148147recnd 9572 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  NN )  ->  ( [_ ( i  +  1 )  /  n ]_ A  -  [_ i  /  n ]_ A )  e.  CC )
149 fzofi 12038 . . . . . . . . . . . 12  |-  ( 0..^ ( i  +  1 ) )  e.  Fin
150149a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  ( 0..^ ( i  +  1 ) )  e.  Fin )
151 elfzoelz 11772 . . . . . . . . . . . 12  |-  ( n  e.  ( 0..^ ( i  +  1 ) )  ->  n  e.  ZZ )
152151, 124sylan2 472 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  ( 0..^ ( i  +  1 ) ) )  ->  ( X `  ( L `  n ) )  e.  CC )
153150, 152fsumcl 13611 . . . . . . . . . 10  |-  ( ph  -> 
sum_ n  e.  (
0..^ ( i  +  1 ) ) ( X `  ( L `
 n ) )  e.  CC )
154153adantr 463 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  NN )  ->  sum_ n  e.  ( 0..^ ( i  +  1 ) ) ( X `  ( L `  n )
)  e.  CC )
155148, 154mulcld 9566 . . . . . . . 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 468 . . . . . . 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 13611 . . . . . 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 13323 . . . . 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 9573 . . . 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 9567 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  NN )  ->  ( ( X `  ( L `
 i ) )  x.  [_ i  /  n ]_ A )  =  ( [_ i  /  n ]_ A  x.  ( X `  ( L `  i ) ) ) )
161 nnnn0 10763 . . . . . . . . . . . . . . . 16  |-  ( i  e.  NN  ->  i  e.  NN0 )
162161adantl 464 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  NN )  ->  i  e. 
NN0 )
163 nn0uz 11079 . . . . . . . . . . . . . . 15  |-  NN0  =  ( ZZ>= `  0 )
164162, 163syl6eleq 2500 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  NN )  ->  i  e.  ( ZZ>= `  0 )
)
165 elfzelz 11659 . . . . . . . . . . . . . . 15  |-  ( n  e.  ( 0 ... i )  ->  n  e.  ZZ )
166124adantlr 713 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  NN )  /\  n  e.  ZZ )  ->  ( X `  ( L `  n ) )  e.  CC )
167165, 166sylan2 472 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  NN )  /\  n  e.  ( 0 ... i
) )  ->  ( X `  ( L `  n ) )  e.  CC )
168164, 167, 63fzosump1 13625 . . . . . . . . . . . . 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 6249 . . . . . . . . . . . 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 12038 . . . . . . . . . . . . . . 15  |-  ( 0..^ i )  e.  Fin
171170a1i 11 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  NN )  ->  ( 0..^ i )  e.  Fin )
172 elfzoelz 11772 . . . . . . . . . . . . . . 15  |-  ( n  e.  ( 0..^ i )  ->  n  e.  ZZ )
173172, 166sylan2 472 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  NN )  /\  n  e.  ( 0..^ i ) )  ->  ( X `  ( L `  n
) )  e.  CC )
174171, 173fsumcl 13611 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  NN )  ->  sum_ n  e.  ( 0..^ i ) ( X `  ( L `  n )
)  e.  CC )
175174, 26pncan2d 9889 . . . . . . . . . . . 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 2444 . . . . . . . . . . 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 6250 . . . . . . . . . 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 2443 . . . . . . . . 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 468 . . . . . . . 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 13581 . . . . . . 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 3375 . . . . . . . . 9  |-  ( k  =  i  ->  [_ k  /  n ]_ A  = 
[_ i  /  n ]_ A )
182 oveq2 6242 . . . . . . . . . 10  |-  ( k  =  i  ->  (
0..^ k )  =  ( 0..^ i ) )
183182sumeq1d 13579 . . . . . . . . 9  |-  ( k  =  i  ->  sum_ n  e.  ( 0..^ k ) ( X `  ( L `  n )
)  =  sum_ n  e.  ( 0..^ i ) ( X `  ( L `  n )
) )
184181, 183jca 530 . . . . . . . 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 3375 . . . . . . . . 9  |-  ( k  =  ( i  +  1 )  ->  [_ k  /  n ]_ A  = 
[_ ( i  +  1 )  /  n ]_ A )
186 oveq2 6242 . . . . . . . . . 10  |-  ( k  =  ( i  +  1 )  ->  (
0..^ k )  =  ( 0..^ ( i  +  1 ) ) )
187186sumeq1d 13579 . . . . . . . . 9  |-  ( k  =  ( i  +  1 )  ->  sum_ n  e.  ( 0..^ k ) ( X `  ( L `  n )
)  =  sum_ n  e.  ( 0..^ ( i  +  1 ) ) ( X `  ( L `  n )
) )
188185, 187jca 530 . . . . . . . 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 3375 . . . . . . . . 9  |-  ( k  =  ( I  + 
1 )  ->  [_ k  /  n ]_ A  = 
[_ ( I  + 
1 )  /  n ]_ A )
190 oveq2 6242 . . . . . . . . . 10  |-  ( k  =  ( I  + 
1 )  ->  (
0..^ k )  =  ( 0..^ ( I  +  1 ) ) )
191190sumeq1d 13579 . . . . . . . . 9  |-  ( k  =  ( I  + 
1 )  ->  sum_ n  e.  ( 0..^ k ) ( X `  ( L `  n )
)  =  sum_ n  e.  ( 0..^ ( I  +  1 ) ) ( X `  ( L `  n )
) )
192189, 191jca 530 . . . . . . . 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 3375 . . . . . . . . 9  |-  ( k  =  ( J  + 
1 )  ->  [_ k  /  n ]_ A  = 
[_ ( J  + 
1 )  /  n ]_ A )
194 oveq2 6242 . . . . . . . . . 10  |-  ( k  =  ( J  + 
1 )  ->  (
0..^ k )  =  ( 0..^ ( J  +  1 ) ) )
195194sumeq1d 13579 . . . . . . . . 9  |-  ( k  =  ( J  + 
1 )  ->  sum_ n  e.  ( 0..^ k ) ( X `  ( L `  n )
)  =  sum_ n  e.  ( 0..^ ( J  +  1 ) ) ( X `  ( L `  n )
) )
196193, 195jca 530 . . . . . . . 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 11655 . . . . . . . . . 10  |-  ( k  e.  ( ( I  +  1 ) ... ( J  +  1 ) )  ->  k  e.  ( ZZ>= `  ( I  +  1 ) ) )
198 eluznn 11115 . . . . . . . . . 10  |-  ( ( ( I  +  1 )  e.  NN  /\  k  e.  ( ZZ>= `  ( I  +  1
) ) )  -> 
k  e.  NN )
1994, 197, 198syl2an 475 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( ( I  + 
1 ) ... ( J  +  1 ) ) )  ->  k  e.  NN )
20041ralrimiva 2817 . . . . . . . . . 10  |-  ( ph  ->  A. i  e.  NN  [_ i  /  n ]_ A  e.  CC )
201 csbeq1 3375 . . . . . . . . . . . 12  |-  ( i  =  k  ->  [_ i  /  n ]_ A  = 
[_ k  /  n ]_ A )
202201eleq1d 2471 . . . . . . . . . . 11  |-  ( i  =  k  ->  ( [_ i  /  n ]_ A  e.  CC  <->  [_ k  /  n ]_ A  e.  CC )
)
203202rspccva 3158 . . . . . . . . . 10  |-  ( ( A. i  e.  NN  [_ i  /  n ]_ A  e.  CC  /\  k  e.  NN )  ->  [_ k  /  n ]_ A  e.  CC )
204200, 203sylan 469 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  NN )  ->  [_ k  /  n ]_ A  e.  CC )
205199, 204syldan 468 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( ( I  + 
1 ) ... ( J  +  1 ) ) )  ->  [_ k  /  n ]_ A  e.  CC )
206 fzofi 12038 . . . . . . . . . . 11  |-  ( 0..^ k )  e.  Fin
207206a1i 11 . . . . . . . . . 10  |-  ( ph  ->  ( 0..^ k )  e.  Fin )
208 elfzoelz 11772 . . . . . . . . . . 11  |-  ( n  e.  ( 0..^ k )  ->  n  e.  ZZ )
209208, 124sylan2 472 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( 0..^ k ) )  ->  ( X `  ( L `  n ) )  e.  CC )
210207, 209fsumcl 13611 . . . . . . . . 9  |-  ( ph  -> 
sum_ n  e.  (
0..^ k ) ( X `  ( L `
 n ) )  e.  CC )
211210adantr 463 . . . . . . . 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 13678 . . . . . . 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 2443 . . . . . 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 5809 . . . . 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 13345 . . . . 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 4414 . . . 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 9573 . . . . . . 7  |-  ( ph  ->  ( [_ ( J  +  1 )  /  n ]_ A  +  [_ ( I  +  1
)  /  n ]_ A )  e.  RR )
218217, 95remulcld 9574 . . . . . 6  |-  ( ph  ->  ( ( [_ ( J  +  1 )  /  n ]_ A  +  [_ ( I  + 
1 )  /  n ]_ A )  x.  R
)  e.  RR )
219181, 185, 189, 193, 9, 205telfsumo 13674 . . . . . . . 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 468 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  [_ i  /  n ]_ A  e.  RR )
221137, 146syldan 468 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  [_ ( i  +  1 )  /  n ]_ A  e.  RR )
222220, 221resubcld 9948 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  ( [_ i  /  n ]_ A  -  [_ ( i  +  1 )  /  n ]_ A )  e.  RR )
22383, 222fsumrecl 13612 . . . . . . . 8  |-  ( ph  -> 
sum_ i  e.  ( ( I  +  1 )..^ ( J  + 
1 ) ) (
[_ i  /  n ]_ A  -  [_ (
i  +  1 )  /  n ]_ A
)  e.  RR )
224219, 223eqeltrrd 2491 . . . . . . 7  |-  ( ph  ->  ( [_ ( I  +  1 )  /  n ]_ A  -  [_ ( J  +  1
)  /  n ]_ A )  e.  RR )
225224, 95remulcld 9574 . . . . . 6  |-  ( ph  ->  ( ( [_ (
I  +  1 )  /  n ]_ A  -  [_ ( J  + 
1 )  /  n ]_ A )  x.  R
)  e.  RR )
226127abscld 13323 . . . . . . . 8  |-  ( ph  ->  ( abs `  ( [_ ( J  +  1 )  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( J  +  1 ) ) ( X `  ( L `  n )
) ) )  e.  RR )
227134abscld 13323 . . . . . . . 8  |-  ( ph  ->  ( abs `  ( [_ ( I  +  1 )  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( I  +  1 ) ) ( X `  ( L `  n )
) ) )  e.  RR )
228226, 227readdcld 9573 . . . . . . 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 13345 . . . . . . 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 9574 . . . . . . . . 9  |-  ( ph  ->  ( [_ ( J  +  1 )  /  n ]_ A  x.  R
)  e.  RR )
231101, 95remulcld 9574 . . . . . . . . 9  |-  ( ph  ->  ( [_ ( I  +  1 )  /  n ]_ A  x.  R
)  e.  RR )
232118, 126absmuld 13341 . . . . . . . . . . 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 11055 . . . . . . . . . . . . . . . . . . 19  |-  ( i  e.  ( ZZ>= `  M
)  ->  i  e.  RR )
234233adantl 464 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  i  e.  RR )
235 eluzle 11057 . . . . . . . . . . . . . . . . . . 19  |-  ( i  e.  ( ZZ>= `  M
)  ->  M  <_  i )
236235adantl 464 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  M  <_  i )
23732nnred 10511 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  M  e.  RR )
238237adantr 463 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  M  e.  RR )
239 elicopnf 11591 . . . . . . . . . . . . . . . . . . 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 923 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  i  e.  ( M [,) +oo )
)
242241ex 432 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( i  e.  (
ZZ>= `  M )  -> 
i  e.  ( M [,) +oo ) ) )
243242ssrdv 3447 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ZZ>= `  M )  C_  ( M [,) +oo ) )
24432nnzd 10927 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  M  e.  ZZ )
24549peano2zd 10931 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( I  +  1 )  e.  ZZ )
246103rpred 11222 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  U  e.  RR )
2474nnred 10511 . . . . . . . . . . . . . . . . . 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 9693 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  M  <_  ( I  +  1 ) )
251 eluz2 11051 . . . . . . . . . . . . . . . . 17  |-  ( ( I  +  1 )  e.  ( ZZ>= `  M
)  <->  ( M  e.  ZZ  /\  ( I  +  1 )  e.  ZZ  /\  M  <_ 
( I  +  1 ) ) )
252244, 245, 250, 251syl3anbrc 1181 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( I  +  1 )  e.  ( ZZ>= `  M ) )
253 uztrn 11061 . . . . . . . . . . . . . . . 16  |-  ( ( ( J  +  1 )  e.  ( ZZ>= `  ( I  +  1
) )  /\  (
I  +  1 )  e.  ( ZZ>= `  M
) )  ->  ( J  +  1 )  e.  ( ZZ>= `  M
) )
2549, 252, 253syl2anc 659 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( J  +  1 )  e.  ( ZZ>= `  M ) )
255243, 254sseldd 3442 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( J  +  1 )  e.  ( M [,) +oo ) )
256115simprd 461 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( J  + 
1 )  e.  ( M [,) +oo )  ->  0  <_  [_ ( J  +  1 )  /  n ]_ A ) )
257255, 256mpd 15 . . . . . . . . . . . . 13  |-  ( ph  ->  0  <_  [_ ( J  +  1 )  /  n ]_ A )
258117, 257absidd 13310 . . . . . . . . . . . 12  |-  ( ph  ->  ( abs `  [_ ( J  +  1 )  /  n ]_ A
)  =  [_ ( J  +  1 )  /  n ]_ A
)
259258oveq1d 6249 . . . . . . . . . . 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 2443 . . . . . . . . . 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 13323 . . . . . . . . . . 11  |-  ( ph  ->  ( abs `  sum_ n  e.  ( 0..^ ( J  +  1 ) ) ( X `  ( L `  n ) ) )  e.  RR )
262113nnnn0d 10813 . . . . . . . . . . . 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 23947 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( J  +  1 )  e. 
NN0 )  ->  ( abs `  sum_ n  e.  ( 0..^ ( J  + 
1 ) ) ( X `  ( L `
 n ) ) )  <_  R )
265262, 264mpdan 666 . . . . . . . . . . 11  |-  ( ph  ->  ( abs `  sum_ n  e.  ( 0..^ ( J  +  1 ) ) ( X `  ( L `  n ) ) )  <_  R
)
266261, 95, 117, 257, 265lemul2ad 10446 . . . . . . . . . 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 4414 . . . . . . . . 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 13341 . . . . . . . . . . 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 3442 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( I  +  1 )  e.  ( M [,) +oo ) )
27019, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36dchrisumlema 23946 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( I  +  1 )  e.  RR+  ->  [_ ( I  + 
1 )  /  n ]_ A  e.  RR )  /\  ( ( I  +  1 )  e.  ( M [,) +oo )  ->  0  <_  [_ (
I  +  1 )  /  n ]_ A
) ) )
271270simprd 461 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( I  + 
1 )  e.  ( M [,) +oo )  ->  0  <_  [_ ( I  +  1 )  /  n ]_ A ) )
272269, 271mpd 15 . . . . . . . . . . . . 13  |-  ( ph  ->  0  <_  [_ ( I  +  1 )  /  n ]_ A )
273101, 272absidd 13310 . . . . . . . . . . . 12  |-  ( ph  ->  ( abs `  [_ (
I  +  1 )  /  n ]_ A
)  =  [_ (
I  +  1 )  /  n ]_ A
)
274273oveq1d 6249 . . . . . . . . . . 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 2443 . . . . . . . . . 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 13323 . . . . . . . . . . 11  |-  ( ph  ->  ( abs `  sum_ n  e.  ( 0..^ ( I  +  1 ) ) ( X `  ( L `  n ) ) )  e.  RR )
2774nnnn0d 10813 . . . . . . . . . . . 12  |-  ( ph  ->  ( I  +  1 )  e.  NN0 )
27819, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36, 95, 263dchrisumlem1 23947 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( I  +  1 )  e. 
NN0 )  ->  ( abs `  sum_ n  e.  ( 0..^ ( I  + 
1 ) ) ( X `  ( L `
 n ) ) )  <_  R )
279277, 278mpdan 666 . . . . . . . . . . 11  |-  ( ph  ->  ( abs `  sum_ n  e.  ( 0..^ ( I  +  1 ) ) ( X `  ( L `  n ) ) )  <_  R
)
280276, 95, 101, 272, 279lemul2ad 10446 . . . . . . . . . 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 4414 . . . . . . . . 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 10130 . . . . . . . 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 9572 . . . . . . . . 9  |-  ( ph  ->  R  e.  CC )
284118, 128, 283adddird 9571 . . . . . . . 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 4420 . . . . . . 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 9693 . . . . . 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 13323 . . . . . . . 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 13612 . . . . . . 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 13673 . . . . . . 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 463 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  R  e.  RR )
291222, 290remulcld 9574 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  ( ( [_ i  /  n ]_ A  -  [_ (
i  +  1 )  /  n ]_ A
)  x.  R )  e.  RR )
292137, 148syldan 468 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  ( [_ ( i  +  1 )  /  n ]_ A  -  [_ i  /  n ]_ A )  e.  CC )
293153adantr 463 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  sum_ n  e.  ( 0..^ ( i  +  1 ) ) ( X `  ( L `  n )
)  e.  CC )
294292, 293absmuld 13341 . . . . . . . . . . 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 11776 . . . . . . . . . . . . . . 15  |-  ( i  e.  ( ( I  +  1 )..^ ( J  +  1 ) )  ->  i  e.  ( ZZ>= `  ( I  +  1 ) ) )
296 uztrn 11061 . . . . . . . . . . . . . . 15  |-  ( ( i  e.  ( ZZ>= `  ( I  +  1
) )  /\  (
I  +  1 )  e.  ( ZZ>= `  M
) )  ->  i  e.  ( ZZ>= `  M )
)
297295, 252, 296syl2anr 476 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  i  e.  ( ZZ>= `  M )
)
298 eluznn 11115 . . . . . . . . . . . . . . . . 17  |-  ( ( M  e.  NN  /\  i  e.  ( ZZ>= `  M ) )  -> 
i  e.  NN )
29932, 298sylan 469 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  i  e.  NN )
300299, 139syl 17 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  ( i  +  1 )  e.  RR+ )
301299nnrpd 11220 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  i  e.  RR+ )
302343expia 1199 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( n  e.  RR+  /\  x  e.  RR+ ) )  ->  (
( M  <_  n  /\  n  <_  x )  ->  B  <_  A
) )
303302ralrimivva 2824 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  A. n  e.  RR+  A. x  e.  RR+  (
( M  <_  n  /\  n  <_  x )  ->  B  <_  A
) )
304303adantr 463 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  A. n  e.  RR+  A. x  e.  RR+  ( ( M  <_  n  /\  n  <_  x
)  ->  B  <_  A ) )
305 nfcv 2564 . . . . . . . . . . . . . . . . . 18  |-  F/_ n RR+
306 nfv 1728 . . . . . . . . . . . . . . . . . . 19  |-  F/ n
( M  <_  i  /\  i  <_  x )
307 nfcv 2564 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ n B
308 nfcv 2564 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ n  <_
309307, 308, 60nfbr 4438 . . . . . . . . . . . . . . . . . . 19  |-  F/ n  B  <_  [_ i  /  n ]_ A
310306, 309nfim 1948 . . . . . . . . . . . . . . . . . 18  |-  F/ n
( ( M  <_ 
i  /\  i  <_  x )  ->  B  <_  [_ i  /  n ]_ A )
311305, 310nfral 2789 . . . . . . . . . . . . . . . . 17  |-  F/ n A. x  e.  RR+  (
( M  <_  i  /\  i  <_  x )  ->  B  <_  [_ i  /  n ]_ A )
312 breq2 4398 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  i  ->  ( M  <_  n  <->  M  <_  i ) )
313 breq1 4397 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  i  ->  (
n  <_  x  <->  i  <_  x ) )
314312, 313anbi12d 709 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  i  ->  (
( M  <_  n  /\  n  <_  x )  <-> 
( M  <_  i  /\  i  <_  x ) ) )
31564breq2d 4406 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  i  ->  ( B  <_  A  <->  B  <_  [_ i  /  n ]_ A ) )
316314, 315imbi12d 318 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  i  ->  (
( ( M  <_  n  /\  n  <_  x
)  ->  B  <_  A )  <->  ( ( M  <_  i  /\  i  <_  x )  ->  B  <_  [_ i  /  n ]_ A ) ) )
317316ralbidv 2842 . . . . . . . . . . . . . . . . 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 3153 . . . . . . . . . . . . . . . 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 59 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  A. x  e.  RR+  ( ( M  <_  i  /\  i  <_  x )  ->  B  <_  [_ i  /  n ]_ A ) )
320234lep1d 10437 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  i  <_  ( i  +  1 ) )
321236, 320jca 530 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  ( M  <_  i  /\  i  <_ 
( i  +  1 ) ) )
322 breq2 4398 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  ( i  +  1 )  ->  (
i  <_  x  <->  i  <_  ( i  +  1 ) ) )
323322anbi2d 702 . . . . . . . . . . . . . . . . 17  |-  ( x  =  ( i  +  1 )  ->  (
( M  <_  i  /\  i  <_  x )  <-> 
( M  <_  i  /\  i  <_  ( i  +  1 ) ) ) )
324 eqvisset 3066 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  ( i  +  1 )  ->  (
i  +  1 )  e.  _V )
325 eqtr3 2430 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  =  ( i  +  1 )  /\  n  =  ( i  +  1 ) )  ->  x  =  n )
32631equcoms 1819 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  n  ->  A  =  B )
327325, 326syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  =  ( i  +  1 )  /\  n  =  ( i  +  1 ) )  ->  A  =  B )
328324, 327csbied 3399 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  ( i  +  1 )  ->  [_ (
i  +  1 )  /  n ]_ A  =  B )
329328eqcomd 2410 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  ( i  +  1 )  ->  B  =  [_ ( i  +  1 )  /  n ]_ A )
330329breq1d 4404 . . . . . . . . . . . . . . . . 17  |-  ( x  =  ( i  +  1 )  ->  ( B  <_  [_ i  /  n ]_ A  <->  [_ ( i  +  1 )  /  n ]_ A  <_  [_ i  /  n ]_ A ) )
331323, 330imbi12d 318 . . . . . . . . . . . . . . . 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 3155 . . . . . . . . . . . . . . 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 60 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  [_ ( i  +  1 )  /  n ]_ A  <_  [_ i  /  n ]_ A )
334297, 333syldan 468 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  [_ ( i  +  1 )  /  n ]_ A  <_  [_ i  /  n ]_ A )
335221, 220, 334abssuble0d 13320 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  ( abs `  ( [_ ( i  +  1 )  /  n ]_ A  -  [_ i  /  n ]_ A
) )  =  (
[_ i  /  n ]_ A  -  [_ (
i  +  1 )  /  n ]_ A
) )
336335oveq1d 6249 . . . . . . . . . . 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 2443 . . . . . . . . . 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 13323 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  ( abs ` 
sum_ n  e.  (
0..^ ( i  +  1 ) ) ( X `  ( L `
 n ) ) )  e.  RR )
339220, 221subge0d 10102 . . . . . . . . . . . 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 232 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  0  <_  (
[_ i  /  n ]_ A  -  [_ (
i  +  1 )  /  n ]_ A
) )
341137peano2nnd 10513 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  ( i  +  1 )  e.  NN )
342341nnnn0d 10813 . . . . . . . . . . . 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 23947 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( i  +  1 )  e. 
NN0 )  ->  ( abs `  sum_ n  e.  ( 0..^ ( i  +  1 ) ) ( X `  ( L `
 n ) ) )  <_  R )
344342, 343syldan 468 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  ( abs ` 
sum_ n  e.  (
0..^ ( i  +  1 ) ) ( X `  ( L `
 n ) ) )  <_  R )
345338, 290, 222, 340, 344lemul2ad 10446 . . . . . . . . . 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 4414 . . . . . . . . 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 13671 . . . . . . . 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 9572 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  ( [_ i  /  n ]_ A  -  [_ ( i  +  1 )  /  n ]_ A )  e.  CC )
34983, 283, 348fsummulc1 13658 . . . . . . . . 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 6249 . . . . . . . . 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 2445 . . . . . . . 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 4418 . . . . . . 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 9693 . . . . . 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 10130 . . . . 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 10742 . . . . . . . 8  |-  ( ph  ->  ( 2  x.  [_ ( I  +  1
)  /  n ]_ A )  =  (
[_ ( I  + 
1 )  /  n ]_ A  +  [_ (
I  +  1 )  /  n ]_ A
) )
356128, 118, 128ppncand 9927 . . . . . . . 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 9736 . . . . . . . . 9  |-  ( ph  ->  ( [_ ( I  +  1 )  /  n ]_ A  +  [_ ( J  +  1
)  /  n ]_ A )  =  (
[_ ( J  + 
1 )  /  n ]_ A  +  [_ (
I  +  1 )  /  n ]_ A
) )
358357oveq1d 6249 . . . . . . . 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 2449 . . . . . . 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 6249 . . . . . 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 10569 . . . . . . 7  |-  ( ph  ->  2  e.  CC )
362361, 128, 283mul32d 9744 . . . . . 6  |-  ( ph  ->  ( ( 2  x. 
[_ ( I  + 
1 )  /  n ]_ A )  x.  R
)  =  ( ( 2  x.  R )  x.  [_ ( I  +  1 )  /  n ]_ A ) )
363217recnd 9572 . . . . . . 7  |-  ( ph  ->  ( [_ ( J  +  1 )  /  n ]_ A  +  [_ ( I  +  1
)  /  n ]_ A )  e.  CC )
364224recnd 9572 . . . . . . 7  |-  ( ph  ->  ( [_ ( I  +  1 )  /  n ]_ A  -  [_ ( J  +  1
)  /  n ]_ A )  e.  CC )
365363, 364, 283adddird 9571 . . . . . 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 2451 . . . . 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 4420 . . . 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 9693 . . 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 10773 . . . . . 6  |-  2  e.  NN0
370 nn0ge0 10782 . . . . . 6  |-  ( 2  e.  NN0  ->  0  <_ 
2 )
371369, 370mp1i 13 . . . . 5  |-  ( ph  ->  0  <_  2 )
372 0red 9547 . . . . . 6  |-  ( ph  ->  0  e.  RR )
373126absge0d 13331 . . . . . 6  |-  ( ph  ->  0  <_  ( abs ` 
sum_ n  e.  (
0..^ ( J  + 
1 ) ) ( X `  ( L `
 n ) ) ) )
374372, 261, 95, 373, 265letrd 9693 . . . . 5  |-  ( ph  ->  0  <_  R )
37594, 95, 371, 374mulge0d 10089 . . . 4  |-  ( ph  ->  0  <_  ( 2  x.  R ) )
3764nnrpd 11220 . . . . 5  |-  ( ph  ->  ( I  +  1 )  e.  RR+ )
377 nfv 1728 . . . . . . . . 9  |-  F/ n
( M  <_  U  /\  U  <_  x )
378307, 308, 105nfbr 4438 . . . . . . . . 9  |-  F/ n  B  <_  [_ U  /  n ]_ A
379377, 378nfim 1948 . . . . . . . 8  |-  F/ n
( ( M  <_  U  /\  U  <_  x
)  ->  B  <_  [_ U  /  n ]_ A )
380305, 379nfral 2789 . . . . . . 7  |-  F/ n A. x  e.  RR+  (
( M  <_  U  /\  U  <_  x )  ->  B  <_  [_ U  /  n ]_ A )
381 breq2 4398 . . . . . . . . . 10  |-  ( n  =  U  ->  ( M  <_  n  <->  M  <_  U ) )
382 breq1 4397 . . . . . . . . . 10  |-  ( n  =  U  ->  (
n  <_  x  <->  U  <_  x ) )
383381, 382anbi12d 709 . . . . . . . . 9  |-  ( n  =  U  ->  (
( M  <_  n  /\  n  <_  x )  <-> 
( M  <_  U  /\  U  <_  x ) ) )
384107breq2d 4406 . . . . . . . . 9  |-  ( n  =  U  ->  ( B  <_  A  <->  B  <_  [_ U  /  n ]_ A ) )
385383, 384imbi12d 318 . . . . . . . 8  |-  ( n  =  U  ->  (
( ( M  <_  n  /\  n  <_  x
)  ->  B  <_  A )  <->  ( ( M  <_  U  /\  U  <_  x )  ->  B  <_  [_ U  /  n ]_ A ) ) )
386385ralbidv 2842 . . . . . . 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 3153 . . . . . 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 59 . . . . 5  |-  ( ph  ->  A. x  e.  RR+  ( ( M  <_  U  /\  U  <_  x
)  ->  B  <_  [_ U  /  n ]_ A ) )
389248, 249jca 530 . . . . 5  |-  ( ph  ->  ( M  <_  U  /\  U  <_  ( I  +  1 ) ) )
390 breq2 4398 . . . . . . . 8  |-  ( x  =  ( I  + 
1 )  ->  ( U  <_  x  <->  U  <_  ( I  +  1 ) ) )
391390anbi2d 702 . . . . . . 7  |-  ( x  =  ( I  + 
1 )  ->  (
( M  <_  U  /\  U  <_  x )  <-> 
( M  <_  U  /\  U  <_  ( I  +  1 ) ) ) )
392 eqvisset 3066 . . . . . . . . . 10  |-  ( x  =  ( I  + 
1 )  ->  (
I  +  1 )  e.  _V )
393 eqtr3 2430 . . . . . . . . . . 11  |-  ( ( x  =  ( I  +  1 )  /\  n  =  ( I  +  1 ) )  ->  x  =  n )
394393, 326syl 17 . . . . . . . . . 10  |-  ( ( x  =  ( I  +  1 )  /\  n  =  ( I  +  1 ) )  ->  A  =  B )
395392, 394csbied 3399 . . . . . . . . 9  |-  ( x  =  ( I  + 
1 )  ->  [_ (
I  +  1 )  /  n ]_ A  =  B )
396395eqcomd 2410 . . . . . . . 8  |-  ( x  =  ( I  + 
1 )  ->  B  =  [_ ( I  + 
1 )  /  n ]_ A )
397396breq1d 4404 . . . . . . 7  |-  ( x  =  ( I  + 
1 )  ->  ( B  <_  [_ U  /  n ]_ A  <->  [_ ( I  + 
1 )  /  n ]_ A  <_  [_ U  /  n ]_ A ) )
398391, 397imbi12d 318 . . . . . 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 3155 . . . . 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 60 . . . 4  |-  ( ph  ->  [_ ( I  + 
1 )  /  n ]_ A  <_  [_ U  /  n ]_ A )
401101, 110, 96, 375, 400lemul2ad 10446 . . 3  |-  ( ph  ->  ( ( 2  x.  R )  x.  [_ ( I  +  1
)  /  n ]_ A )  <_  (
( 2  x.  R
)  x.  [_ U  /  n ]_ A ) )
40292, 102, 111, 368, 401letrd 9693 . 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 4414 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 184    /\ wa 367    /\ w3a 974    = wceq 1405    e. wcel 1842    =/= wne 2598   A.wral 2753   _Vcvv 3058   [_csb 3372    u. cun 3411    i^i cin 3412   (/)c0 3737   class class class wbr 4394    |-> cmpt 4452   ` cfv 5525  (class class class)co 6234   Fincfn 7474   CCcc 9440   RRcr 9441   0cc0 9442   1c1 9443    + caddc 9445    x. cmul 9447   +oocpnf 9575    <_ cle 9579    - cmin 9761   NNcn 10496   2c2 10546   NN0cn0 10756   ZZcz 10825   ZZ>=cuz 11045   RR+crp 11183   [,)cico 11502   ...cfz 11643  ..^cfzo 11767    seqcseq 12061   abscabs 13123    ~~> r crli 13364   sum_csu 13564   Basecbs 14733   0gc0g 14946   ZRHomczrh 18729  ℤ/nczn 18732  DChrcdchr