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

Theorem dchrisumlem2 20633
Description: Lemma for dchrisum 20635. 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
StepHypRef Expression
1 fzodisj 10894 . . . . . . . . 9  |-  ( ( 1..^ ( I  + 
1 ) )  i^i  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  =  (/)
21a1i 12 . . . . . . . 8  |-  ( ph  ->  ( ( 1..^ ( I  +  1 ) )  i^i  ( ( I  +  1 )..^ ( J  +  1 ) ) )  =  (/) )
3 dchrisumlem2.4 . . . . . . . . . . . 12  |-  ( ph  ->  I  e.  NN )
43peano2nnd 9758 . . . . . . . . . . 11  |-  ( ph  ->  ( I  +  1 )  e.  NN )
5 nnuz 10258 . . . . . . . . . . 11  |-  NN  =  ( ZZ>= `  1 )
64, 5syl6eleq 2374 . . . . . . . . . 10  |-  ( ph  ->  ( I  +  1 )  e.  ( ZZ>= ` 
1 ) )
7 dchrisumlem2.5 . . . . . . . . . . 11  |-  ( ph  ->  J  e.  ( ZZ>= `  I ) )
8 eluzp1p1 10248 . . . . . . . . . . 11  |-  ( J  e.  ( ZZ>= `  I
)  ->  ( J  +  1 )  e.  ( ZZ>= `  ( I  +  1 ) ) )
97, 8syl 17 . . . . . . . . . 10  |-  ( ph  ->  ( J  +  1 )  e.  ( ZZ>= `  ( I  +  1
) ) )
10 elfzuzb 10786 . . . . . . . . . 10  |-  ( ( I  +  1 )  e.  ( 1 ... ( J  +  1 ) )  <->  ( (
I  +  1 )  e.  ( ZZ>= `  1
)  /\  ( J  +  1 )  e.  ( ZZ>= `  ( I  +  1 ) ) ) )
116, 9, 10sylanbrc 648 . . . . . . . . 9  |-  ( ph  ->  ( I  +  1 )  e.  ( 1 ... ( J  + 
1 ) ) )
12 fzosplit 10893 . . . . . . . . 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 11030 . . . . . . . . 9  |-  ( 1..^ ( J  +  1 ) )  e.  Fin
1514a1i 12 . . . . . . . 8  |-  ( ph  ->  ( 1..^ ( J  +  1 ) )  e.  Fin )
16 elfzouz 10873 . . . . . . . . . 10  |-  ( i  e.  ( 1..^ ( J  +  1 ) )  ->  i  e.  ( ZZ>= `  1 )
)
1716, 5syl6eleqr 2375 . . . . . . . . 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 453 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  NN )  ->  X  e.  D )
24 nnz 10040 . . . . . . . . . . . 12  |-  ( i  e.  NN  ->  i  e.  ZZ )
2524adantl 454 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  NN )  ->  i  e.  ZZ )
2618, 19, 20, 21, 23, 25dchrzrhcl 20478 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  NN )  ->  ( X `
 ( L `  i ) )  e.  CC )
27 nnrp 10358 . . . . . . . . . . . . 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 20631 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( i  e.  RR+  ->  [_ i  /  n ]_ A  e.  RR )  /\  ( i  e.  ( M [,)  +oo )  ->  0  <_  [_ i  /  n ]_ A ) ) )
3837simpld 447 . . . . . . . . . . . . 13  |-  ( ph  ->  ( i  e.  RR+  ->  [_ i  /  n ]_ A  e.  RR ) )
3927, 38syl5 30 . . . . . . . . . . . 12  |-  ( ph  ->  ( i  e.  NN  ->  [_ i  /  n ]_ A  e.  RR ) )
4039imp 420 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  NN )  ->  [_ i  /  n ]_ A  e.  RR )
4140recnd 8856 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  NN )  ->  [_ i  /  n ]_ A  e.  CC )
4226, 41mulcld 8850 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  NN )  ->  ( ( X `  ( L `
 i ) )  x.  [_ i  /  n ]_ A )  e.  CC )
4317, 42sylan2 462 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 1..^ ( J  + 
1 ) ) )  ->  ( ( X `
 ( L `  i ) )  x. 
[_ i  /  n ]_ A )  e.  CC )
442, 13, 15, 43fsumsplit 12206 . . . . . . 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 10233 . . . . . . . . 9  |-  ( J  e.  ( ZZ>= `  I
)  ->  J  e.  ZZ )
46 fzval3 10905 . . . . . . . . 9  |-  ( J  e.  ZZ  ->  (
1 ... J )  =  ( 1..^ ( J  +  1 ) ) )
477, 45, 463syl 20 . . . . . . . 8  |-  ( ph  ->  ( 1 ... J
)  =  ( 1..^ ( J  +  1 ) ) )
4847sumeq1d 12168 . . . . . . 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 10111 . . . . . . . . . 10  |-  ( ph  ->  I  e.  ZZ )
50 fzval3 10905 . . . . . . . . . 10  |-  ( I  e.  ZZ  ->  (
1 ... I )  =  ( 1..^ ( I  +  1 ) ) )
5149, 50syl 17 . . . . . . . . 9  |-  ( ph  ->  ( 1 ... I
)  =  ( 1..^ ( I  +  1 ) ) )
5251sumeq1d 12168 . . . . . . . 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 5834 . . . . . . 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 2326 . . . . . 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 10813 . . . . . . . 8  |-  ( i  e.  ( 1 ... J )  ->  i  e.  NN )
56 simpr 449 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  NN )  ->  i  e.  NN )
57 nfcv 2420 . . . . . . . . . 10  |-  F/_ n
i
58 nfcv 2420 . . . . . . . . . . 11  |-  F/_ n
( X `  ( L `  i )
)
59 nfcv 2420 . . . . . . . . . . 11  |-  F/_ n  x.
6057nfcsb1 3113 . . . . . . . . . . 11  |-  F/_ n [_ i  /  n ]_ A
6158, 59, 60nfov 5842 . . . . . . . . . 10  |-  F/_ n
( ( X `  ( L `  i ) )  x.  [_ i  /  n ]_ A )
62 fveq2 5485 . . . . . . . . . . . 12  |-  ( n  =  i  ->  ( L `  n )  =  ( L `  i ) )
6362fveq2d 5489 . . . . . . . . . . 11  |-  ( n  =  i  ->  ( X `  ( L `  n ) )  =  ( X `  ( L `  i )
) )
64 csbeq1a 3090 . . . . . . . . . . 11  |-  ( n  =  i  ->  A  =  [_ i  /  n ]_ A )
6563, 64oveq12d 5837 . . . . . . . . . 10  |-  ( n  =  i  ->  (
( X `  ( L `  n )
)  x.  A )  =  ( ( X `
 ( L `  i ) )  x. 
[_ i  /  n ]_ A ) )
6657, 61, 65, 36fvmptf 5577 . . . . . . . . 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 645 . . . . . . . 8  |-  ( (
ph  /\  i  e.  NN )  ->  ( F `
 i )  =  ( ( X `  ( L `  i ) )  x.  [_ i  /  n ]_ A ) )
6855, 67sylan2 462 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 1 ... J
) )  ->  ( F `  i )  =  ( ( X `
 ( L `  i ) )  x. 
[_ i  /  n ]_ A ) )
693, 5syl6eleq 2374 . . . . . . . 8  |-  ( ph  ->  I  e.  ( ZZ>= ` 
1 ) )
70 uztrn 10239 . . . . . . . 8  |-  ( ( J  e.  ( ZZ>= `  I )  /\  I  e.  ( ZZ>= `  1 )
)  ->  J  e.  ( ZZ>= `  1 )
)
717, 69, 70syl2anc 645 . . . . . . 7  |-  ( ph  ->  J  e.  ( ZZ>= ` 
1 ) )
7255, 42sylan2 462 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 1 ... J
) )  ->  (
( X `  ( L `  i )
)  x.  [_ i  /  n ]_ A )  e.  CC )
7368, 71, 72fsumser 12197 . . . . . 6  |-  ( ph  -> 
sum_ i  e.  ( 1 ... J ) ( ( X `  ( L `  i ) )  x.  [_ i  /  n ]_ A )  =  (  seq  1
(  +  ,  F
) `  J )
)
7454, 73eqtr3d 2318 . . . . 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 10813 . . . . . . 7  |-  ( i  e.  ( 1 ... I )  ->  i  e.  NN )
7675, 67sylan2 462 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 1 ... I
) )  ->  ( F `  i )  =  ( ( X `
 ( L `  i ) )  x. 
[_ i  /  n ]_ A ) )
7775, 42sylan2 462 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 1 ... I
) )  ->  (
( X `  ( L `  i )
)  x.  [_ i  /  n ]_ A )  e.  CC )
7876, 69, 77fsumser 12197 . . . . 5  |-  ( ph  -> 
sum_ i  e.  ( 1 ... I ) ( ( X `  ( L `  i ) )  x.  [_ i  /  n ]_ A )  =  (  seq  1
(  +  ,  F
) `  I )
)
7974, 78oveq12d 5837 . . . 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 11029 . . . . . 6  |-  ( ph  ->  ( 1 ... I
)  e.  Fin )
8180, 77fsumcl 12200 . . . . 5  |-  ( ph  -> 
sum_ i  e.  ( 1 ... I ) ( ( X `  ( L `  i ) )  x.  [_ i  /  n ]_ A )  e.  CC )
82 fzofi 11030 . . . . . . 7  |-  ( ( I  +  1 )..^ ( J  +  1 ) )  e.  Fin
8382a1i 12 . . . . . 6  |-  ( ph  ->  ( ( I  + 
1 )..^ ( J  +  1 ) )  e.  Fin )
84 ssun2 3340 . . . . . . . . 9  |-  ( ( I  +  1 )..^ ( J  +  1 ) )  C_  (
( 1..^ ( I  +  1 ) )  u.  ( ( I  +  1 )..^ ( J  +  1 ) ) )
8584, 13syl5sseqr 3228 . . . . . . . 8  |-  ( ph  ->  ( ( I  + 
1 )..^ ( J  +  1 ) ) 
C_  ( 1..^ ( J  +  1 ) ) )
8685sselda 3181 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  i  e.  ( 1..^ ( J  + 
1 ) ) )
8786, 43syldan 458 . . . . . 6  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  ( ( X `  ( L `  i ) )  x. 
[_ i  /  n ]_ A )  e.  CC )
8883, 87fsumcl 12200 . . . . 5  |-  ( ph  -> 
sum_ i  e.  ( ( I  +  1 )..^ ( J  + 
1 ) ) ( ( X `  ( L `  i )
)  x.  [_ i  /  n ]_ A )  e.  CC )
8981, 88pncan2d 9154 . . . 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 2318 . . 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 5489 . 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 11912 . . 3  |-  ( ph  ->  ( abs `  sum_ i  e.  ( (
I  +  1 )..^ ( J  +  1 ) ) ( ( X `  ( L `
 i ) )  x.  [_ i  /  n ]_ A ) )  e.  RR )
93 2re 9810 . . . . . 6  |-  2  e.  RR
9493a1i 12 . . . . 5  |-  ( ph  ->  2  e.  RR )
95 dchrisum.9 . . . . 5  |-  ( ph  ->  R  e.  RR )
9694, 95remulcld 8858 . . . 4  |-  ( ph  ->  ( 2  x.  R
)  e.  RR )
9740ralrimiva 2627 . . . . 5  |-  ( ph  ->  A. i  e.  NN  [_ i  /  n ]_ A  e.  RR )
98 csbeq1 3085 . . . . . . 7  |-  ( i  =  ( I  + 
1 )  ->  [_ i  /  n ]_ A  = 
[_ ( I  + 
1 )  /  n ]_ A )
9998eleq1d 2350 . . . . . 6  |-  ( i  =  ( I  + 
1 )  ->  ( [_ i  /  n ]_ A  e.  RR  <->  [_ ( I  +  1 )  /  n ]_ A  e.  RR )
)
10099rspcv 2881 . . . . 5  |-  ( ( I  +  1 )  e.  NN  ->  ( A. i  e.  NN  [_ i  /  n ]_ A  e.  RR  ->  [_ ( I  +  1 )  /  n ]_ A  e.  RR )
)
1014, 97, 100sylc 58 . . . 4  |-  ( ph  ->  [_ ( I  + 
1 )  /  n ]_ A  e.  RR )
10296, 101remulcld 8858 . . 3  |-  ( ph  ->  ( ( 2  x.  R )  x.  [_ ( I  +  1
)  /  n ]_ A )  e.  RR )
103 dchrisumlem2.1 . . . . 5  |-  ( ph  ->  U  e.  RR+ )
10433ralrimiva 2627 . . . . 5  |-  ( ph  ->  A. n  e.  RR+  A  e.  RR )
105 nfcsb1v 3114 . . . . . . 7  |-  F/_ n [_ U  /  n ]_ A
106105nfel1 2430 . . . . . 6  |-  F/ n [_ U  /  n ]_ A  e.  RR
107 csbeq1a 3090 . . . . . . 7  |-  ( n  =  U  ->  A  =  [_ U  /  n ]_ A )
108107eleq1d 2350 . . . . . 6  |-  ( n  =  U  ->  ( A  e.  RR  <->  [_ U  /  n ]_ A  e.  RR ) )
109106, 108rspc 2879 . . . . 5  |-  ( U  e.  RR+  ->  ( A. n  e.  RR+  A  e.  RR  ->  [_ U  /  n ]_ A  e.  RR ) )
110103, 104, 109sylc 58 . . . 4  |-  ( ph  ->  [_ U  /  n ]_ A  e.  RR )
11196, 110remulcld 8858 . . 3  |-  ( ph  ->  ( ( 2  x.  R )  x.  [_ U  /  n ]_ A
)  e.  RR )
11271, 5syl6eleqr 2375 . . . . . . . . . . . 12  |-  ( ph  ->  J  e.  NN )
113112peano2nnd 9758 . . . . . . . . . . 11  |-  ( ph  ->  ( J  +  1 )  e.  NN )
114113nnrpd 10384 . . . . . . . . . 10  |-  ( ph  ->  ( J  +  1 )  e.  RR+ )
11519, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36dchrisumlema 20631 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( J  +  1 )  e.  RR+  ->  [_ ( J  + 
1 )  /  n ]_ A  e.  RR )  /\  ( ( J  +  1 )  e.  ( M [,)  +oo )  ->  0  <_  [_ ( J  +  1 )  /  n ]_ A
) ) )
116115simpld 447 . . . . . . . . . 10  |-  ( ph  ->  ( ( J  + 
1 )  e.  RR+  ->  [_ ( J  + 
1 )  /  n ]_ A  e.  RR ) )
117114, 116mpd 16 . . . . . . . . 9  |-  ( ph  ->  [_ ( J  + 
1 )  /  n ]_ A  e.  RR )
118117recnd 8856 . . . . . . . 8  |-  ( ph  ->  [_ ( J  + 
1 )  /  n ]_ A  e.  CC )
119 fzofi 11030 . . . . . . . . . 10  |-  ( 0..^ ( J  +  1 ) )  e.  Fin
120119a1i 12 . . . . . . . . 9  |-  ( ph  ->  ( 0..^ ( J  +  1 ) )  e.  Fin )
121 elfzoelz 10869 . . . . . . . . . 10  |-  ( n  e.  ( 0..^ ( J  +  1 ) )  ->  n  e.  ZZ )
12222adantr 453 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  ZZ )  ->  X  e.  D )
123 simpr 449 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  ZZ )  ->  n  e.  ZZ )
12418, 19, 20, 21, 122, 123dchrzrhcl 20478 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ZZ )  ->  ( X `
 ( L `  n ) )  e.  CC )
125121, 124sylan2 462 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 0..^ ( J  + 
1 ) ) )  ->  ( X `  ( L `  n ) )  e.  CC )
126120, 125fsumcl 12200 . . . . . . . 8  |-  ( ph  -> 
sum_ n  e.  (
0..^ ( J  + 
1 ) ) ( X `  ( L `
 n ) )  e.  CC )
127118, 126mulcld 8850 . . . . . . 7  |-  ( ph  ->  ( [_ ( J  +  1 )  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( J  +  1 ) ) ( X `  ( L `  n ) ) )  e.  CC )
128101recnd 8856 . . . . . . . 8  |-  ( ph  ->  [_ ( I  + 
1 )  /  n ]_ A  e.  CC )
129 fzofi 11030 . . . . . . . . . 10  |-  ( 0..^ ( I  +  1 ) )  e.  Fin
130129a1i 12 . . . . . . . . 9  |-  ( ph  ->  ( 0..^ ( I  +  1 ) )  e.  Fin )
131 elfzoelz 10869 . . . . . . . . . 10  |-  ( n  e.  ( 0..^ ( I  +  1 ) )  ->  n  e.  ZZ )
132131, 124sylan2 462 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 0..^ ( I  + 
1 ) ) )  ->  ( X `  ( L `  n ) )  e.  CC )
133130, 132fsumcl 12200 . . . . . . . 8  |-  ( ph  -> 
sum_ n  e.  (
0..^ ( I  + 
1 ) ) ( X `  ( L `
 n ) )  e.  CC )
134128, 133mulcld 8850 . . . . . . 7  |-  ( ph  ->  ( [_ ( I  +  1 )  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( I  +  1 ) ) ( X `  ( L `  n ) ) )  e.  CC )
135127, 134subcld 9152 . . . . . 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 11912 . . . . 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 9753 . . . . . . . . . . . . 13  |-  ( i  e.  NN  ->  (
i  +  1 )  e.  NN )
139138nnrpd 10384 . . . . . . . . . . . 12  |-  ( i  e.  NN  ->  (
i  +  1 )  e.  RR+ )
140 nfcsb1v 3114 . . . . . . . . . . . . . . 15  |-  F/_ n [_ ( i  +  1 )  /  n ]_ A
141140nfel1 2430 . . . . . . . . . . . . . 14  |-  F/ n [_ ( i  +  1 )  /  n ]_ A  e.  RR
142 csbeq1a 3090 . . . . . . . . . . . . . . 15  |-  ( n  =  ( i  +  1 )  ->  A  =  [_ ( i  +  1 )  /  n ]_ A )
143142eleq1d 2350 . . . . . . . . . . . . . 14  |-  ( n  =  ( i  +  1 )  ->  ( A  e.  RR  <->  [_ ( i  +  1 )  /  n ]_ A  e.  RR ) )
144141, 143rspc 2879 . . . . . . . . . . . . 13  |-  ( ( i  +  1 )  e.  RR+  ->  ( A. n  e.  RR+  A  e.  RR  ->  [_ ( i  +  1 )  /  n ]_ A  e.  RR ) )
145144impcom 421 . . . . . . . . . . . 12  |-  ( ( A. n  e.  RR+  A  e.  RR  /\  (
i  +  1 )  e.  RR+ )  ->  [_ (
i  +  1 )  /  n ]_ A  e.  RR )
146104, 139, 145syl2an 465 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  NN )  ->  [_ (
i  +  1 )  /  n ]_ A  e.  RR )
147146, 40resubcld 9206 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  NN )  ->  ( [_ ( i  +  1 )  /  n ]_ A  -  [_ i  /  n ]_ A )  e.  RR )
148147recnd 8856 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  NN )  ->  ( [_ ( i  +  1 )  /  n ]_ A  -  [_ i  /  n ]_ A )  e.  CC )
149 fzofi 11030 . . . . . . . . . . . 12  |-  ( 0..^ ( i  +  1 ) )  e.  Fin
150149a1i 12 . . . . . . . . . . 11  |-  ( ph  ->  ( 0..^ ( i  +  1 ) )  e.  Fin )
151 elfzoelz 10869 . . . . . . . . . . . 12  |-  ( n  e.  ( 0..^ ( i  +  1 ) )  ->  n  e.  ZZ )
152151, 124sylan2 462 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  ( 0..^ ( i  +  1 ) ) )  ->  ( X `  ( L `  n ) )  e.  CC )
153150, 152fsumcl 12200 . . . . . . . . . 10  |-  ( ph  -> 
sum_ n  e.  (
0..^ ( i  +  1 ) ) ( X `  ( L `
 n ) )  e.  CC )
154153adantr 453 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  NN )  ->  sum_ n  e.  ( 0..^ ( i  +  1 ) ) ( X `  ( L `  n )
)  e.  CC )
155148, 154mulcld 8850 . . . . . . . 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 458 . . . . . . 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 12200 . . . . . 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 11912 . . . . 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 8857 . . . 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 8851 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  NN )  ->  ( ( X `  ( L `
 i ) )  x.  [_ i  /  n ]_ A )  =  ( [_ i  /  n ]_ A  x.  ( X `  ( L `  i ) ) ) )
161 nnnn0 9967 . . . . . . . . . . . . . . . 16  |-  ( i  e.  NN  ->  i  e.  NN0 )
162161adantl 454 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  NN )  ->  i  e. 
NN0 )
163 nn0uz 10257 . . . . . . . . . . . . . . 15  |-  NN0  =  ( ZZ>= `  0 )
164162, 163syl6eleq 2374 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  NN )  ->  i  e.  ( ZZ>= `  0 )
)
165 elfzelz 10792 . . . . . . . . . . . . . . 15  |-  ( n  e.  ( 0 ... i )  ->  n  e.  ZZ )
166124adantlr 698 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  NN )  /\  n  e.  ZZ )  ->  ( X `  ( L `  n ) )  e.  CC )
167165, 166sylan2 462 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  NN )  /\  n  e.  ( 0 ... i
) )  ->  ( X `  ( L `  n ) )  e.  CC )
168164, 167, 63fzosump1 12211 . . . . . . . . . . . . 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 5834 . . . . . . . . . . . 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 11030 . . . . . . . . . . . . . . 15  |-  ( 0..^ i )  e.  Fin
171170a1i 12 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  NN )  ->  ( 0..^ i )  e.  Fin )
172 elfzoelz 10869 . . . . . . . . . . . . . . 15  |-  ( n  e.  ( 0..^ i )  ->  n  e.  ZZ )
173172, 166sylan2 462 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  NN )  /\  n  e.  ( 0..^ i ) )  ->  ( X `  ( L `  n
) )  e.  CC )
174171, 173fsumcl 12200 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  NN )  ->  sum_ n  e.  ( 0..^ i ) ( X `  ( L `  n )
)  e.  CC )
175174, 26pncan2d 9154 . . . . . . . . . . . 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 2317 . . . . . . . . . . 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 5835 . . . . . . . . . 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 2316 . . . . . . . . 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 458 . . . . . . . 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 12170 . . . . . . 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 3085 . . . . . . . . 9  |-  ( k  =  i  ->  [_ k  /  n ]_ A  = 
[_ i  /  n ]_ A )
182 oveq2 5827 . . . . . . . . . 10  |-  ( k  =  i  ->  (
0..^ k )  =  ( 0..^ i ) )
183182sumeq1d 12168 . . . . . . . . 9  |-  ( k  =  i  ->  sum_ n  e.  ( 0..^ k ) ( X `  ( L `  n )
)  =  sum_ n  e.  ( 0..^ i ) ( X `  ( L `  n )
) )
184181, 183jca 520 . . . . . . . 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 3085 . . . . . . . . 9  |-  ( k  =  ( i  +  1 )  ->  [_ k  /  n ]_ A  = 
[_ ( i  +  1 )  /  n ]_ A )
186 oveq2 5827 . . . . . . . . . 10  |-  ( k  =  ( i  +  1 )  ->  (
0..^ k )  =  ( 0..^ ( i  +  1 ) ) )
187186sumeq1d 12168 . . . . . . . . 9  |-  ( k  =  ( i  +  1 )  ->  sum_ n  e.  ( 0..^ k ) ( X `  ( L `  n )
)  =  sum_ n  e.  ( 0..^ ( i  +  1 ) ) ( X `  ( L `  n )
) )
188185, 187jca 520 . . . . . . . 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 3085 . . . . . . . . 9  |-  ( k  =  ( I  + 
1 )  ->  [_ k  /  n ]_ A  = 
[_ ( I  + 
1 )  /  n ]_ A )
190 oveq2 5827 . . . . . . . . . 10  |-  ( k  =  ( I  + 
1 )  ->  (
0..^ k )  =  ( 0..^ ( I  +  1 ) ) )
191190sumeq1d 12168 . . . . . . . . 9  |-  ( k  =  ( I  + 
1 )  ->  sum_ n  e.  ( 0..^ k ) ( X `  ( L `  n )
)  =  sum_ n  e.  ( 0..^ ( I  +  1 ) ) ( X `  ( L `  n )
) )
192189, 191jca 520 . . . . . . . 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 3085 . . . . . . . . 9  |-  ( k  =  ( J  + 
1 )  ->  [_ k  /  n ]_ A  = 
[_ ( J  + 
1 )  /  n ]_ A )
194 oveq2 5827 . . . . . . . . . 10  |-  ( k  =  ( J  + 
1 )  ->  (
0..^ k )  =  ( 0..^ ( J  +  1 ) ) )
195194sumeq1d 12168 . . . . . . . . 9  |-  ( k  =  ( J  + 
1 )  ->  sum_ n  e.  ( 0..^ k ) ( X `  ( L `  n )
)  =  sum_ n  e.  ( 0..^ ( J  +  1 ) ) ( X `  ( L `  n )
) )
196193, 195jca 520 . . . . . . . 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 10788 . . . . . . . . . 10  |-  ( k  e.  ( ( I  +  1 ) ... ( J  +  1 ) )  ->  k  e.  ( ZZ>= `  ( I  +  1 ) ) )
1985uztrn2 10240 . . . . . . . . . 10  |-  ( ( ( I  +  1 )  e.  NN  /\  k  e.  ( ZZ>= `  ( I  +  1
) ) )  -> 
k  e.  NN )
1994, 197, 198syl2an 465 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( ( I  + 
1 ) ... ( J  +  1 ) ) )  ->  k  e.  NN )
20041ralrimiva 2627 . . . . . . . . . 10  |-  ( ph  ->  A. i  e.  NN  [_ i  /  n ]_ A  e.  CC )
201 csbeq1 3085 . . . . . . . . . . . 12  |-  ( i  =  k  ->  [_ i  /  n ]_ A  = 
[_ k  /  n ]_ A )
202201eleq1d 2350 . . . . . . . . . . 11  |-  ( i  =  k  ->  ( [_ i  /  n ]_ A  e.  CC  <->  [_ k  /  n ]_ A  e.  CC )
)
203202rspccva 2884 . . . . . . . . . 10  |-  ( ( A. i  e.  NN  [_ i  /  n ]_ A  e.  CC  /\  k  e.  NN )  ->  [_ k  /  n ]_ A  e.  CC )
204200, 203sylan 459 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  NN )  ->  [_ k  /  n ]_ A  e.  CC )
205199, 204syldan 458 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( ( I  + 
1 ) ... ( J  +  1 ) ) )  ->  [_ k  /  n ]_ A  e.  CC )
206 fzofi 11030 . . . . . . . . . . 11  |-  ( 0..^ k )  e.  Fin
207206a1i 12 . . . . . . . . . 10  |-  ( ph  ->  ( 0..^ k )  e.  Fin )
208 elfzoelz 10869 . . . . . . . . . . 11  |-  ( n  e.  ( 0..^ k )  ->  n  e.  ZZ )
209208, 124sylan2 462 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( 0..^ k ) )  ->  ( X `  ( L `  n ) )  e.  CC )
210207, 209fsumcl 12200 . . . . . . . . 9  |-  ( ph  -> 
sum_ n  e.  (
0..^ k ) ( X `  ( L `
 n ) )  e.  CC )
211210adantr 453 . . . . . . . 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 12258 . . . . . . 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 2316 . . . . . 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 5489 . . . . 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 11934 . . . . 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 4044 . . . 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 8857 . . . . . . 7  |-  ( ph  ->  ( [_ ( J  +  1 )  /  n ]_ A  +  [_ ( I  +  1
)  /  n ]_ A )  e.  RR )
218217, 95remulcld 8858 . . . . . 6  |-  ( ph  ->  ( ( [_ ( J  +  1 )  /  n ]_ A  +  [_ ( I  + 
1 )  /  n ]_ A )  x.  R
)  e.  RR )
219181, 185, 189, 193, 9, 205fsumtscopo 12254 . . . . . . . 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 458 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  [_ i  /  n ]_ A  e.  RR )
221137, 146syldan 458 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  [_ ( i  +  1 )  /  n ]_ A  e.  RR )
222220, 221resubcld 9206 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  ( [_ i  /  n ]_ A  -  [_ ( i  +  1 )  /  n ]_ A )  e.  RR )
22383, 222fsumrecl 12201 . . . . . . . 8  |-  ( ph  -> 
sum_ i  e.  ( ( I  +  1 )..^ ( J  + 
1 ) ) (
[_ i  /  n ]_ A  -  [_ (
i  +  1 )  /  n ]_ A
)  e.  RR )
224219, 223eqeltrrd 2359 . . . . . . 7  |-  ( ph  ->  ( [_ ( I  +  1 )  /  n ]_ A  -  [_ ( J  +  1
)  /  n ]_ A )  e.  RR )
225224, 95remulcld 8858 . . . . . 6  |-  ( ph  ->  ( ( [_ (
I  +  1 )  /  n ]_ A  -  [_ ( J  + 
1 )  /  n ]_ A )  x.  R
)  e.  RR )
226127abscld 11912 . . . . . . . 8  |-  ( ph  ->  ( abs `  ( [_ ( J  +  1 )  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( J  +  1 ) ) ( X `  ( L `  n )
) ) )  e.  RR )
227134abscld 11912 . . . . . . . 8  |-  ( ph  ->  ( abs `  ( [_ ( I  +  1 )  /  n ]_ A  x.  sum_ n  e.  ( 0..^ ( I  +  1 ) ) ( X `  ( L `  n )
) ) )  e.  RR )
228226, 227readdcld 8857 . . . . . . 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 11934 . . . . . . 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 8858 . . . . . . . . 9  |-  ( ph  ->  ( [_ ( J  +  1 )  /  n ]_ A  x.  R
)  e.  RR )
231101, 95remulcld 8858 . . . . . . . . 9  |-  ( ph  ->  ( [_ ( I  +  1 )  /  n ]_ A  x.  R
)  e.  RR )
232118, 126absmuld 11930 . . . . . . . . . . 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 10234 . . . . . . . . . . . . . . . . . . 19  |-  ( i  e.  ( ZZ>= `  M
)  ->  i  e.  RR )
234233adantl 454 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  i  e.  RR )
235 eluzle 10235 . . . . . . . . . . . . . . . . . . 19  |-  ( i  e.  ( ZZ>= `  M
)  ->  M  <_  i )
236235adantl 454 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  M  <_  i )
23732nnred 9756 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  M  e.  RR )
238237adantr 453 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  M  e.  RR )
239 elicopnf 10733 . . . . . . . . . . . . . . . . . . 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 893 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  i  e.  ( M [,)  +oo )
)
242241ex 425 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( i  e.  (
ZZ>= `  M )  -> 
i  e.  ( M [,)  +oo ) ) )
243242ssrdv 3186 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ZZ>= `  M )  C_  ( M [,)  +oo ) )
24432nnzd 10111 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  M  e.  ZZ )
24549peano2zd 10115 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( I  +  1 )  e.  ZZ )
246103rpred 10385 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  U  e.  RR )
2474nnred 9756 . . . . . . . . . . . . . . . . . 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 8968 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  M  <_  ( I  +  1 ) )
251 eluz2 10231 . . . . . . . . . . . . . . . . 17  |-  ( ( I  +  1 )  e.  ( ZZ>= `  M
)  <->  ( M  e.  ZZ  /\  ( I  +  1 )  e.  ZZ  /\  M  <_ 
( I  +  1 ) ) )
252244, 245, 250, 251syl3anbrc 1141 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( I  +  1 )  e.  ( ZZ>= `  M ) )
253 uztrn 10239 . . . . . . . . . . . . . . . 16  |-  ( ( ( J  +  1 )  e.  ( ZZ>= `  ( I  +  1
) )  /\  (
I  +  1 )  e.  ( ZZ>= `  M
) )  ->  ( J  +  1 )  e.  ( ZZ>= `  M
) )
2549, 252, 253syl2anc 645 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( J  +  1 )  e.  ( ZZ>= `  M ) )
255243, 254sseldd 3182 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( J  +  1 )  e.  ( M [,)  +oo ) )
256115simprd 451 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( J  + 
1 )  e.  ( M [,)  +oo )  ->  0  <_  [_ ( J  +  1 )  /  n ]_ A ) )
257255, 256mpd 16 . . . . . . . . . . . . 13  |-  ( ph  ->  0  <_  [_ ( J  +  1 )  /  n ]_ A )
258117, 257absidd 11899 . . . . . . . . . . . 12  |-  ( ph  ->  ( abs `  [_ ( J  +  1 )  /  n ]_ A
)  =  [_ ( J  +  1 )  /  n ]_ A
)
259258oveq1d 5834 . . . . . . . . . . 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 2316 . . . . . . . . . 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 11912 . . . . . . . . . . 11  |-  ( ph  ->  ( abs `  sum_ n  e.  ( 0..^ ( J  +  1 ) ) ( X `  ( L `  n ) ) )  e.  RR )
262113nnnn0d 10013 . . . . . . . . . . . 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 20632 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( J  +  1 )  e. 
NN0 )  ->  ( abs `  sum_ n  e.  ( 0..^ ( J  + 
1 ) ) ( X `  ( L `
 n ) ) )  <_  R )
265262, 264mpdan 652 . . . . . . . . . . 11  |-  ( ph  ->  ( abs `  sum_ n  e.  ( 0..^ ( J  +  1 ) ) ( X `  ( L `  n ) ) )  <_  R
)
266261, 95, 117, 257, 265lemul2ad 9692 . . . . . . . . . 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 4044 . . . . . . . . 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 11930 . . . . . . . . . . 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 3182 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( I  +  1 )  e.  ( M [,)  +oo ) )
27019, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36dchrisumlema 20631 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( I  +  1 )  e.  RR+  ->  [_ ( I  + 
1 )  /  n ]_ A  e.  RR )  /\  ( ( I  +  1 )  e.  ( M [,)  +oo )  ->  0  <_  [_ (
I  +  1 )  /  n ]_ A
) ) )
271270simprd 451 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( I  + 
1 )  e.  ( M [,)  +oo )  ->  0  <_  [_ ( I  +  1 )  /  n ]_ A ) )
272269, 271mpd 16 . . . . . . . . . . . . 13  |-  ( ph  ->  0  <_  [_ ( I  +  1 )  /  n ]_ A )
273101, 272absidd 11899 . . . . . . . . . . . 12  |-  ( ph  ->  ( abs `  [_ (
I  +  1 )  /  n ]_ A
)  =  [_ (
I  +  1 )  /  n ]_ A
)
274273oveq1d 5834 . . . . . . . . . . 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 2316 . . . . . . . . . 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 11912 . . . . . . . . . . 11  |-  ( ph  ->  ( abs `  sum_ n  e.  ( 0..^ ( I  +  1 ) ) ( X `  ( L `  n ) ) )  e.  RR )
2774nnnn0d 10013 . . . . . . . . . . . 12  |-  ( ph  ->  ( I  +  1 )  e.  NN0 )
27819, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36, 95, 263dchrisumlem1 20632 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( I  +  1 )  e. 
NN0 )  ->  ( abs `  sum_ n  e.  ( 0..^ ( I  + 
1 ) ) ( X `  ( L `
 n ) ) )  <_  R )
279277, 278mpdan 652 . . . . . . . . . . 11  |-  ( ph  ->  ( abs `  sum_ n  e.  ( 0..^ ( I  +  1 ) ) ( X `  ( L `  n ) ) )  <_  R
)
280276, 95, 101, 272, 279lemul2ad 9692 . . . . . . . . . 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 4044 . . . . . . . . 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 9385 . . . . . . . 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 8856 . . . . . . . . 9  |-  ( ph  ->  R  e.  CC )
284118, 128, 283adddird 8855 . . . . . . . 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 4050 . . . . . . 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 8968 . . . . . 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 11912 . . . . . . . 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 12201 . . . . . . 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 12253 . . . . . . 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 453 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  R  e.  RR )
291222, 290remulcld 8858 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  ( ( [_ i  /  n ]_ A  -  [_ (
i  +  1 )  /  n ]_ A
)  x.  R )  e.  RR )
292137, 148syldan 458 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  ( [_ ( i  +  1 )  /  n ]_ A  -  [_ i  /  n ]_ A )  e.  CC )
293153adantr 453 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  sum_ n  e.  ( 0..^ ( i  +  1 ) ) ( X `  ( L `  n )
)  e.  CC )
294292, 293absmuld 11930 . . . . . . . . . . 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 10873 . . . . . . . . . . . . . . 15  |-  ( i  e.  ( ( I  +  1 )..^ ( J  +  1 ) )  ->  i  e.  ( ZZ>= `  ( I  +  1 ) ) )
296 uztrn 10239 . . . . . . . . . . . . . . 15  |-  ( ( i  e.  ( ZZ>= `  ( I  +  1
) )  /\  (
I  +  1 )  e.  ( ZZ>= `  M
) )  ->  i  e.  ( ZZ>= `  M )
)
297295, 252, 296syl2anr 466 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  i  e.  ( ZZ>= `  M )
)
2985uztrn2 10240 . . . . . . . . . . . . . . . . 17  |-  ( ( M  e.  NN  /\  i  e.  ( ZZ>= `  M ) )  -> 
i  e.  NN )
29932, 298sylan 459 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  i  e.  NN )
300299, 139syl 17 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  ( i  +  1 )  e.  RR+ )
301299nnrpd 10384 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  i  e.  RR+ )
302343expia 1158 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( n  e.  RR+  /\  x  e.  RR+ ) )  ->  (
( M  <_  n  /\  n  <_  x )  ->  B  <_  A
) )
303302ralrimivva 2636 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  A. n  e.  RR+  A. x  e.  RR+  (
( M  <_  n  /\  n  <_  x )  ->  B  <_  A
) )
304303adantr 453 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  A. n  e.  RR+  A. x  e.  RR+  ( ( M  <_  n  /\  n  <_  x
)  ->  B  <_  A ) )
305 nfcv 2420 . . . . . . . . . . . . . . . . . 18  |-  F/_ n RR+
306 nfv 1610 . . . . . . . . . . . . . . . . . . 19  |-  F/ n
( M  <_  i  /\  i  <_  x )
307 nfcv 2420 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ n B
308 nfcv 2420 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ n  <_
309307, 308, 60nfbr 4068 . . . . . . . . . . . . . . . . . . 19  |-  F/ n  B  <_  [_ i  /  n ]_ A
310306, 309nfim 1773 . . . . . . . . . . . . . . . . . 18  |-  F/ n
( ( M  <_ 
i  /\  i  <_  x )  ->  B  <_  [_ i  /  n ]_ A )
311305, 310nfral 2597 . . . . . . . . . . . . . . . . 17  |-  F/ n A. x  e.  RR+  (
( M  <_  i  /\  i  <_  x )  ->  B  <_  [_ i  /  n ]_ A )
312 breq2 4028 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  i  ->  ( M  <_  n  <->  M  <_  i ) )
313 breq1 4027 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  i  ->  (
n  <_  x  <->  i  <_  x ) )
314312, 313anbi12d 694 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  i  ->  (
( M  <_  n  /\  n  <_  x )  <-> 
( M  <_  i  /\  i  <_  x ) ) )
31564breq2d 4036 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  i  ->  ( B  <_  A  <->  B  <_  [_ i  /  n ]_ A ) )
316314, 315imbi12d 313 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  i  ->  (
( ( M  <_  n  /\  n  <_  x
)  ->  B  <_  A )  <->  ( ( M  <_  i  /\  i  <_  x )  ->  B  <_  [_ i  /  n ]_ A ) ) )
317316ralbidv 2564 . . . . . . . . . . . . . . . . 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 2879 . . . . . . . . . . . . . . . 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 58 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  A. x  e.  RR+  ( ( M  <_  i  /\  i  <_  x )  ->  B  <_  [_ i  /  n ]_ A ) )
320234lep1d 9683 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  i  <_  ( i  +  1 ) )
321236, 320jca 520 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  ( M  <_  i  /\  i  <_ 
( i  +  1 ) ) )
322 breq2 4028 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  ( i  +  1 )  ->  (
i  <_  x  <->  i  <_  ( i  +  1 ) ) )
323322anbi2d 687 . . . . . . . . . . . . . . . . 17  |-  ( x  =  ( i  +  1 )  ->  (
( M  <_  i  /\  i  <_  x )  <-> 
( M  <_  i  /\  i  <_  ( i  +  1 ) ) ) )
324 ovex 5844 . . . . . . . . . . . . . . . . . . . . 21  |-  ( i  +  1 )  e. 
_V
325324a1i 12 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  ( i  +  1 )  ->  (
i  +  1 )  e.  _V )
326 eqtr3 2303 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  =  ( i  +  1 )  /\  n  =  ( i  +  1 ) )  ->  x  =  n )
32731eqcoms 2287 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  n  ->  A  =  B )
328326, 327syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  =  ( i  +  1 )  /\  n  =  ( i  +  1 ) )  ->  A  =  B )
329325, 328csbied 3124 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  ( i  +  1 )  ->  [_ (
i  +  1 )  /  n ]_ A  =  B )
330329eqcomd 2289 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  ( i  +  1 )  ->  B  =  [_ ( i  +  1 )  /  n ]_ A )
331330breq1d 4034 . . . . . . . . . . . . . . . . 17  |-  ( x  =  ( i  +  1 )  ->  ( B  <_  [_ i  /  n ]_ A  <->  [_ ( i  +  1 )  /  n ]_ A  <_  [_ i  /  n ]_ A ) )
332323, 331imbi12d 313 . . . . . . . . . . . . . . . 16  |-  ( x  =  ( i  +  1 )  ->  (
( ( M  <_ 
i  /\  i  <_  x )  ->  B  <_  [_ i  /  n ]_ A )  <->  ( ( M  <_  i  /\  i  <_  ( i  +  1 ) )  ->  [_ (
i  +  1 )  /  n ]_ A  <_  [_ i  /  n ]_ A ) ) )
333332rspcv 2881 . . . . . . . . . . . . . . 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 ) ) )
334300, 319, 321, 333syl3c 59 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( ZZ>= `  M )
)  ->  [_ ( i  +  1 )  /  n ]_ A  <_  [_ i  /  n ]_ A )
335297, 334syldan 458 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  [_ ( i  +  1 )  /  n ]_ A  <_  [_ i  /  n ]_ A )
336221, 220, 335abssuble0d 11909 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  ( abs `  ( [_ ( i  +  1 )  /  n ]_ A  -  [_ i  /  n ]_ A
) )  =  (
[_ i  /  n ]_ A  -  [_ (
i  +  1 )  /  n ]_ A
) )
337336oveq1d 5834 . . . . . . . . . . 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 ) ) ) ) )
338294, 337eqtrd 2316 . . . . . . . . . 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 ) ) ) ) )
339293abscld 11912 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  ( abs ` 
sum_ n  e.  (
0..^ ( i  +  1 ) ) ( X `  ( L `
 n ) ) )  e.  RR )
340220, 221subge0d 9357 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  ( 0  <_  ( [_ i  /  n ]_ A  -  [_ ( i  +  1 )  /  n ]_ A )  <->  [_ ( i  +  1 )  /  n ]_ A  <_  [_ i  /  n ]_ A ) )
341335, 340mpbird 225 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  0  <_  (
[_ i  /  n ]_ A  -  [_ (
i  +  1 )  /  n ]_ A
) )
342137peano2nnd 9758 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  ( i  +  1 )  e.  NN )
343342nnnn0d 10013 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  ( i  +  1 )  e. 
NN0 )
34419, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36, 95, 263dchrisumlem1 20632 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( i  +  1 )  e. 
NN0 )  ->  ( abs `  sum_ n  e.  ( 0..^ ( i  +  1 ) ) ( X `  ( L `
 n ) ) )  <_  R )
345343, 344syldan 458 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  ( abs ` 
sum_ n  e.  (
0..^ ( i  +  1 ) ) ( X `  ( L `
 n ) ) )  <_  R )
346339, 290, 222, 341, 345lemul2ad 9692 . . . . . . . . . 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 ) )
347338, 346eqbrtrd 4044 . . . . . . . . 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
) )
34883, 287, 291, 347fsumle 12251 . . . . . . . 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
) )
349222recnd 8856 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( ( I  + 
1 )..^ ( J  +  1 ) ) )  ->  ( [_ i  /  n ]_ A  -  [_ ( i  +  1 )  /  n ]_ A )  e.  CC )
35083, 283, 349fsummulc1 12241 . . . . . . . . 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
) )
351219oveq1d 5834 . . . . . . . . 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 ) )
352350, 351eqtr3d 2318 . . . . . . . 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 ) )
353348, 352breqtrd 4048 . . . . . . 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 ) )
354158, 288, 225, 289, 353letrd 8968 . . . . . 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 ) )
355136, 158, 218, 225, 286, 354le2addd 9385 . . . . 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
) ) )
3561282timesd 9949 . . . . . . . 8  |-  ( ph  ->  ( 2  x.  [_ ( I  +  1
)  /  n ]_ A )  =  (
[_ ( I  + 
1 )  /  n ]_ A  +  [_ (
I  +  1 )  /  n ]_ A
) )
357128, 118, 128ppncand 9192 . . . . . . . 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
) )
358128, 118addcomd 9009 . . . . . . . . 9  |-  ( ph  ->  ( [_ ( I  +  1 )  /  n ]_ A  +  [_ ( J  +  1
)  /  n ]_ A )  =  (
[_ ( J  + 
1 )  /  n ]_ A  +  [_ (
I  +  1 )  /  n ]_ A
) )
359358oveq1d 5834 . . . . . . . 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
) ) )
360356, 357, 3593eqtr2d 2322 . . . . . . 7  |-  ( ph  ->  ( 2  x.  [_ ( I  +  1
)  /  n ]_ A )  =  ( ( [_ ( J  +  1 )  /  n ]_ A  +  [_ ( I  +  1
)  /  n ]_ A )  +  (
[_ ( I  + 
1 )  /  n ]_ A  -  [_ ( J  +  1 )  /  n ]_ A
) ) )
361360oveq1d 5834 . . . . . 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
) )
362 2cn 9811 . . . . . . . 8  |-  2  e.  CC
363362a1i 12 . . . . . . 7  |-  ( ph  ->  2  e.  CC )
364363, 128, 283mul32d 9017 . . . . . 6  |-  ( ph  ->  ( ( 2  x. 
[_ ( I  + 
1 )  /  n ]_ A )  x.  R
)  =  ( ( 2  x.  R )  x.  [_ ( I  +  1 )  /  n ]_ A ) )
365217recnd 8856 . . . . . . 7  |-  ( ph  ->  ( [_ ( J  +  1 )  /  n ]_ A  +  [_ ( I  +  1
)  /  n ]_ A )  e.  CC )
366224recnd 8856 . . . . . . 7  |-  ( ph  ->  ( [_ ( I  +  1 )  /  n ]_ A  -  [_ ( J  +  1
)  /  n ]_ A )  e.  CC )
367365, 366, 283adddird 8855 . . . . . 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 ) ) )
368361, 364, 3673eqtr3d 2324 . . . . 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 ) ) )
369355, 368breqtrrd 4050 . . . 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 ) )
37092, 159, 102, 216, 369letrd 8968 . . 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 ) )
371 2nn0 9977 . . . . . 6  |-  2  e.  NN0
372 nn0ge0 9986 . . . . . 6  |-  ( 2  e.  NN0  ->  0  <_ 
2 )
373371, 372mp1i 13 . . . . 5  |-  ( ph  ->  0  <_  2 )
374 0re 8833 . . . . . . 7  |-  0  e.  RR
375374a1i 12 . . . . . 6  |-  ( ph  ->  0  e.  RR )
376126absge0d 11920 . . . . . 6  |-  ( ph  ->  0  <_  ( abs ` 
sum_ n  e.  (
0..^ ( J  + 
1 ) ) ( X `  ( L `
 n ) ) ) )
377375, 261, 95, 376, 265letrd 8968 . . . . 5  |-  ( ph  ->  0  <_  R )
37894, 95, 373, 377mulge0d 9344 . . . 4  |-  ( ph  ->  0  <_  ( 2  x.  R ) )
3794nnrpd 10384 . . . . 5  |-  ( ph  ->  ( I  +  1 )  e.  RR+ )
380 nfv 1610 . . . . . . . . 9  |-  F/ n
( M  <_  U  /\  U  <_  x )
381307, 308, 105nfbr 4068 . . . . . . . . 9  |-  F/ n  B  <_  [_ U  /  n ]_ A
382380, 381nfim 1773 . . . . . . . 8  |-  F/ n
( ( M  <_  U  /\  U  <_  x
)  ->  B  <_  [_ U  /  n ]_ A )
383305, 382nfral 2597 . . . . . . 7  |-  F/ n A. x  e.  RR+  (
( M  <_  U  /\  U  <_  x )  ->  B  <_  [_ U  /  n ]_ A )
384 breq2 4028 . . . . . . . . . 10  |-  ( n  =  U  ->  ( M  <_  n  <->  M  <_  U ) )
385 breq1 4027 . . . . . . . . . 10  |-  ( n  =  U  ->  (
n  <_  x  <->  U  <_  x ) )
386384, 385anbi12d 694 . . . . . . . . 9  |-  ( n  =  U  ->  (
( M  <_  n  /\  n  <_  x )  <-> 
( M  <_  U  /\  U  <_  x ) ) )
387107breq2d 4036 . . . . . . . . 9  |-  ( n  =  U  ->  ( B  <_  A  <->  B  <_  [_ U  /  n ]_ A ) )
388386, 387imbi12d 313 . . . . . . . 8  |-  ( n  =  U  ->  (
( ( M  <_  n  /\  n  <_  x
)  ->  B  <_  A )  <->  ( ( M  <_  U  /\  U  <_  x )  ->  B  <_  [_ U  /  n ]_ A ) ) )
389388ralbidv 2564 . . . . . . 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 ) ) )
390383, 389rspc 2879 . . . . . 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 ) ) )
391103, 303, 390sylc 58 . . . . 5  |-  ( ph  ->  A. x  e.  RR+  ( ( M  <_  U  /\  U  <_  x
)  ->  B  <_  [_ U  /  n ]_ A ) )
392248, 249jca 520 . . . . 5  |-  ( ph  ->  ( M  <_  U  /\  U  <_  ( I  +  1 ) ) )
393 breq2 4028 . . . . . . . 8  |-  ( x  =  ( I  + 
1 )  ->  ( U  <_  x  <->  U  <_  ( I  +  1 ) ) )
394393anbi2d 687 . . . . . . 7  |-  ( x  =  ( I  + 
1 )  ->  (
( M  <_  U  /\  U  <_  x )  <-> 
( M  <_  U  /\  U  <_  ( I  +  1 ) ) ) )
395 ovex 5844 . . . . . . . . . . 11  |-  ( I  +  1 )  e. 
_V
396395a1i 12 . . . . . . . . . 10  |-  ( x  =  ( I  + 
1 )  ->  (
I  +  1 )  e.  _V )
397 eqtr3 2303 . . . . . . . . . . 11  |-  ( ( x  =  ( I  +  1 )  /\  n  =  ( I  +  1 ) )  ->  x  =  n )
398397, 327syl 17 . . . . . . . . . 10  |-  ( ( x  =  ( I  +  1 )  /\  n  =  ( I  +  1 ) )  ->  A  =  B )
399396, 398csbied 3124 . . . . . . . . 9  |-  ( x  =  ( I  + 
1 )  ->  [_ (
I  +  1 )  /  n ]_ A  =  B )
400399eqcomd 2289 . . . . . . . 8  |-  ( x  =  ( I  + 
1 )  ->  B  =  [_ ( I  + 
1 )  /  n ]_ A )
401400breq1d 4034 . . . . . . 7  |-  ( x  =  ( I  + 
1 )  ->  ( B  <_  [_ U  /  n ]_ A  <->  [_ ( I  + 
1 )  /  n ]_ A  <_  [_ U  /  n ]_ A ) )
402394, 401imbi12d 313 . . . . . 6  |-  ( x  =  ( I  + 
1 )  ->  (
( ( M  <_  U  /\  U  <_  x
)  ->  B  <_  [_ U  /  n ]_ A )  <->  ( ( M  <_  U  /\  U  <_  ( I  +  1 ) )  ->  [_ (
I  +  1 )  /  n ]_ A  <_  [_ U  /  n ]_ A ) ) )
403402rspcv 2881 . . . . 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 ) ) )
404379, 391, 392, 403syl3c 59 . . . 4  |-  ( ph  ->  [_ ( I  + 
1 )  /  n ]_ A  <_  [_ U  /  n ]_ A )
405101, 110, 96, 378, 404lemul2ad 9692 . . 3  |-  ( ph  ->  ( ( 2  x.  R )  x.  [_ ( I  +  1
)  /  n ]_ A )  <_  (
( 2  x.  R
)  x.  [_ U  /  n ]_ A ) )
40692, 102, 111, 370, 405letrd 8968 . 2  |-  ( ph  ->  ( abs `  sum_ i  e.  ( (
I  +  1 )..^ ( J  +  1 ) ) ( ( X `  ( L `
 i ) )  x.  [_ i  /  n ]_ A ) )  <_  ( ( 2  x.  R )  x. 
[_ U  /  n ]_ A ) )
40791, 406eqbrtrd 4044 1  |-  ( ph  ->  ( abs `  (
(  seq  1 (  +  ,  F ) `
 J )  -  (  seq  1 (  +  ,  F ) `  I ) ) )  <_  ( ( 2  x.  R )  x. 
[_ U  /  n ]_ A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <->