Theorem dchrisumlem2 24320

Description: Lemma for dchrisum 24322. Lemma 9.4.1 of [Shapiro], p. 377. (Contributed by Mario Carneiro, 2-May-2016.)

Hypotheses

Ref	Expression
rpvmasum.z	|- Z = (ℤ/nℤ ` N )
rpvmasum.l	|- L = ( ZRHom ` Z )
rpvmasum.a	|- ( ph -> N e. NN )
rpvmasum.g	|- G = (DChr ` N )
rpvmasum.d	|- D = ( Base ` G )
rpvmasum.1	|- .1. = ( 0g ` G )
dchrisum.b	|- ( ph -> X e. D )
dchrisum.n1	|- ( ph -> X =/= .1. )
dchrisum.2	|- ( n = x -> A = B )
dchrisum.3	|- ( ph -> M e. NN )
dchrisum.4	|- ( ( ph /\ n e. RR+ ) -> A e. RR )
dchrisum.5	|- ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) /\ ( M <_ n /\ n <_ x ) ) -> B <_ A )
dchrisum.6	|- ( ph -> ( n e. RR+ |-> A ) ~~> r 0 )
dchrisum.7	|- F = ( n e. NN |-> ( ( X ` ( L ` n ) ) x. A ) )
dchrisum.9	|- ( ph -> R e. RR )
dchrisum.10	|- ( ph -> A. u e. ( 0..^ N ) ( abs ` sum_ n e. ( 0..^ u ) ( X ` ( L ` n ) ) ) <_ R )
dchrisumlem2.1	|- ( ph -> U e. RR+ )
dchrisumlem2.2	|- ( ph -> M <_ U )
dchrisumlem2.3	|- ( ph -> U <_ ( I + 1 ) )
dchrisumlem2.4	|- ( ph -> I e. NN )
dchrisumlem2.5	|- ( ph -> J e. ( ZZ>= ` I ) )

Assertion

Ref	Expression
dchrisumlem2	|- ( ph -> ( abs ` ( ( seq 1 ( + , F ) ` J ) - ( seq 1 ( + , F ) ` I ) ) ) <_ ( ( 2 x. R ) x. [_ U / n ]_ A ) )

Distinct variable groups:   u, n, x   .1. , n, x   n, F, u, x   n, I, u, x   n, J, u, x   x, A   n, N, u, x   ph, n, u, x   R, n, u, x   U, n, u, x   B, n   n, Z, x   D, n, x   n, L, u, x   n, M, u, x   n, X, u, x

Allowed substitution hints:   A( u, n)   B( x, u)   D( u)   .1. ( u)   G( x, u, n)   Z( u)

Proof of Theorem dchrisumlem2

Dummy variables k i are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fzodisj 11954	. . . . . . . . 9 |- ( ( 1..^ ( I + 1 ) ) i^i ( ( I + 1 )..^ ( J + 1 ) ) ) = (/)
2	1	a1i 11	. . . . . . . 8 |- ( ph -> ( ( 1..^ ( I + 1 ) ) i^i ( ( I + 1 )..^ ( J + 1 ) ) ) = (/) )
3		dchrisumlem2.4	. . . . . . . . . . . 12 |- ( ph -> I e. NN )
4	3	peano2nnd 10628	. . . . . . . . . . 11 |- ( ph -> ( I + 1 ) e. NN )
5		nnuz 11196	. . . . . . . . . . 11 |- NN = ( ZZ>= ` 1 )
6	4, 5	syl6eleq 2521	. . . . . . . . . 10 |- ( ph -> ( I + 1 ) e. ( ZZ>= ` 1 ) )
7		dchrisumlem2.5	. . . . . . . . . . 11 |- ( ph -> J e. ( ZZ>= ` I ) )
8		eluzp1p1 11186	. . . . . . . . . . 11 |- ( J e. ( ZZ>= ` I ) -> ( J + 1 ) e. ( ZZ>= ` ( I + 1 ) ) )
9	7, 8	syl 17	. . . . . . . . . 10 |- ( ph -> ( J + 1 ) e. ( ZZ>= ` ( I + 1 ) ) )
10		elfzuzb 11796	. . . . . . . . . 10 |- ( ( I + 1 ) e. ( 1 ... ( J + 1 ) ) <-> ( ( I + 1 ) e. ( ZZ>= ` 1 ) /\ ( J + 1 ) e. ( ZZ>= ` ( I + 1 ) ) ) )
11	6, 9, 10	sylanbrc 669	. . . . . . . . 9 |- ( ph -> ( I + 1 ) e. ( 1 ... ( J + 1 ) ) )
12		fzosplit 11953	. . . . . . . . 9 |- ( ( I + 1 ) e. ( 1 ... ( J + 1 ) ) -> ( 1..^ ( J + 1 ) ) = ( ( 1..^ ( I + 1 ) ) u. ( ( I + 1 )..^ ( J + 1 ) ) ) )
13	11, 12	syl 17	. . . . . . . 8 |- ( ph -> ( 1..^ ( J + 1 ) ) = ( ( 1..^ ( I + 1 ) ) u. ( ( I + 1 )..^ ( J + 1 ) ) ) )
14		fzofi 12188	. . . . . . . . 9 |- ( 1..^ ( J + 1 ) ) e. Fin
15	14	a1i 11	. . . . . . . 8 |- ( ph -> ( 1..^ ( J + 1 ) ) e. Fin )
16		elfzouz 11926	. . . . . . . . . 10 |- ( i e. ( 1..^ ( J + 1 ) ) -> i e. ( ZZ>= ` 1 ) )
17	16, 5	syl6eleqr 2522	. . . . . . . . 9 |- ( i e. ( 1..^ ( J + 1 ) ) -> i e. NN )
18		rpvmasum.g	. . . . . . . . . . 11 |- G = (DChr ` N )
19		rpvmasum.z	. . . . . . . . . . 11 |- Z = (ℤ/nℤ ` N )
20		rpvmasum.d	. . . . . . . . . . 11 |- D = ( Base ` G )
21		rpvmasum.l	. . . . . . . . . . 11 |- L = ( ZRHom ` Z )
22		dchrisum.b	. . . . . . . . . . . 12 |- ( ph -> X e. D )
23	22	adantr 467	. . . . . . . . . . 11 |- ( ( ph /\ i e. NN ) -> X e. D )
24		nnz 10961	. . . . . . . . . . . 12 |- ( i e. NN -> i e. ZZ )
25	24	adantl 468	. . . . . . . . . . 11 |- ( ( ph /\ i e. NN ) -> i e. ZZ )
26	18, 19, 20, 21, 23, 25	dchrzrhcl 24165	. . . . . . . . . 10 |- ( ( ph /\ i e. NN ) -> ( X ` ( L ` i ) ) e. CC )
27		nnrp 11313	. . . . . . . . . . . . 13 |- ( i e. NN -> i e. RR+ )
28		rpvmasum.a	. . . . . . . . . . . . . . 15 |- ( ph -> N e. NN )
29		rpvmasum.1	. . . . . . . . . . . . . . 15 |- .1. = ( 0g ` G )
30		dchrisum.n1	. . . . . . . . . . . . . . 15 |- ( ph -> X =/= .1. )
31		dchrisum.2	. . . . . . . . . . . . . . 15 |- ( n = x -> A = B )
32		dchrisum.3	. . . . . . . . . . . . . . 15 |- ( ph -> M e. NN )
33		dchrisum.4	. . . . . . . . . . . . . . 15 |- ( ( ph /\ n e. RR+ ) -> A e. RR )
34		dchrisum.5	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) /\ ( M <_ n /\ n <_ x ) ) -> B <_ A )
35		dchrisum.6	. . . . . . . . . . . . . . 15 |- ( ph -> ( n e. RR+ |-> A ) ~~> r 0 )
36		dchrisum.7	. . . . . . . . . . . . . . 15 |- F = ( n e. NN |-> ( ( X ` ( L ` n ) ) x. A ) )
37	19, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36	dchrisumlema 24318	. . . . . . . . . . . . . 14 |- ( ph -> ( ( i e. RR+ -> [_ i / n ]_ A e. RR ) /\ ( i e. ( M [,) +oo ) -> 0 <_ [_ i / n ]_ A ) ) )
38	37	simpld 461	. . . . . . . . . . . . 13 |- ( ph -> ( i e. RR+ -> [_ i / n ]_ A e. RR ) )
39	27, 38	syl5 34	. . . . . . . . . . . 12 |- ( ph -> ( i e. NN -> [_ i / n ]_ A e. RR ) )
40	39	imp 431	. . . . . . . . . . 11 |- ( ( ph /\ i e. NN ) -> [_ i / n ]_ A e. RR )
41	40	recnd 9671	. . . . . . . . . 10 |- ( ( ph /\ i e. NN ) -> [_ i / n ]_ A e. CC )
42	26, 41	mulcld 9665	. . . . . . . . 9 |- ( ( ph /\ i e. NN ) -> ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) e. CC )
43	17, 42	sylan2 477	. . . . . . . 8 |- ( ( ph /\ i e. ( 1..^ ( J + 1 ) ) ) -> ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) e. CC )
44	2, 13, 15, 43	fsumsplit 13799	. . . . . . 7 |- ( ph -> sum_ i e. ( 1..^ ( J + 1 ) ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) = ( sum_ i e. ( 1..^ ( I + 1 ) ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) + sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) ) )
45		eluzelz 11170	. . . . . . . . 9 |- ( J e. ( ZZ>= ` I ) -> J e. ZZ )
46		fzval3 11984	. . . . . . . . 9 |- ( J e. ZZ -> ( 1 ... J ) = ( 1..^ ( J + 1 ) ) )
47	7, 45, 46	3syl 18	. . . . . . . 8 |- ( ph -> ( 1 ... J ) = ( 1..^ ( J + 1 ) ) )
48	47	sumeq1d 13760	. . . . . . 7 |- ( ph -> sum_ i e. ( 1 ... J ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) = sum_ i e. ( 1..^ ( J + 1 ) ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) )
49	3	nnzd 11041	. . . . . . . . . 10 |- ( ph -> I e. ZZ )
50		fzval3 11984	. . . . . . . . . 10 |- ( I e. ZZ -> ( 1 ... I ) = ( 1..^ ( I + 1 ) ) )
51	49, 50	syl 17	. . . . . . . . 9 |- ( ph -> ( 1 ... I ) = ( 1..^ ( I + 1 ) ) )
52	51	sumeq1d 13760	. . . . . . . 8 |- ( ph -> sum_ i e. ( 1 ... I ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) = sum_ i e. ( 1..^ ( I + 1 ) ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) )
53	52	oveq1d 6318	. . . . . . 7 |- ( ph -> ( sum_ i e. ( 1 ... I ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) + sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) ) = ( sum_ i e. ( 1..^ ( I + 1 ) ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) + sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) ) )
54	44, 48, 53	3eqtr4d 2474	. . . . . 6 |- ( ph -> sum_ i e. ( 1 ... J ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) = ( sum_ i e. ( 1 ... I ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) + sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) ) )
55		elfznn 11830	. . . . . . . 8 |- ( i e. ( 1 ... J ) -> i e. NN )
56		simpr 463	. . . . . . . . 9 |- ( ( ph /\ i e. NN ) -> i e. NN )
57		nfcv 2585	. . . . . . . . . 10 |- F/_ n i
58		nfcv 2585	. . . . . . . . . . 11 |- F/_ n ( X ` ( L ` i ) )
59		nfcv 2585	. . . . . . . . . . 11 |- F/_ n x.
60		nfcsb1v 3412	. . . . . . . . . . 11 |- F/_ n [_ i / n ]_ A
61	58, 59, 60	nfov 6329	. . . . . . . . . 10 |- F/_ n ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A )
62		fveq2 5879	. . . . . . . . . . . 12 |- ( n = i -> ( L ` n ) = ( L ` i ) )
63	62	fveq2d 5883	. . . . . . . . . . 11 |- ( n = i -> ( X ` ( L ` n ) ) = ( X ` ( L ` i ) ) )
64		csbeq1a 3405	. . . . . . . . . . 11 |- ( n = i -> A = [_ i / n ]_ A )
65	63, 64	oveq12d 6321	. . . . . . . . . 10 |- ( n = i -> ( ( X ` ( L ` n ) ) x. A ) = ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) )
66	57, 61, 65, 36	fvmptf 5980	. . . . . . . . 9 |- ( ( i e. NN /\ ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) e. CC ) -> ( F ` i ) = ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) )
67	56, 42, 66	syl2anc 666	. . . . . . . 8 |- ( ( ph /\ i e. NN ) -> ( F ` i ) = ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) )
68	55, 67	sylan2 477	. . . . . . 7 |- ( ( ph /\ i e. ( 1 ... J ) ) -> ( F ` i ) = ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) )
69	3, 5	syl6eleq 2521	. . . . . . . 8 |- ( ph -> I e. ( ZZ>= ` 1 ) )
70		uztrn 11177	. . . . . . . 8 |- ( ( J e. ( ZZ>= ` I ) /\ I e. ( ZZ>= ` 1 ) ) -> J e. ( ZZ>= ` 1 ) )
71	7, 69, 70	syl2anc 666	. . . . . . 7 |- ( ph -> J e. ( ZZ>= ` 1 ) )
72	55, 42	sylan2 477	. . . . . . 7 |- ( ( ph /\ i e. ( 1 ... J ) ) -> ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) e. CC )
73	68, 71, 72	fsumser 13789	. . . . . 6 |- ( ph -> sum_ i e. ( 1 ... J ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) = ( seq 1 ( + , F ) ` J ) )
74	54, 73	eqtr3d 2466	. . . . 5 |- ( ph -> ( sum_ i e. ( 1 ... I ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) + sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) ) = ( seq 1 ( + , F ) ` J ) )
75		elfznn 11830	. . . . . . 7 |- ( i e. ( 1 ... I ) -> i e. NN )
76	75, 67	sylan2 477	. . . . . 6 |- ( ( ph /\ i e. ( 1 ... I ) ) -> ( F ` i ) = ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) )
77	75, 42	sylan2 477	. . . . . 6 |- ( ( ph /\ i e. ( 1 ... I ) ) -> ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) e. CC )
78	76, 69, 77	fsumser 13789	. . . . 5 |- ( ph -> sum_ i e. ( 1 ... I ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) = ( seq 1 ( + , F ) ` I ) )
79	74, 78	oveq12d 6321	. . . 4 |- ( ph -> ( ( sum_ i e. ( 1 ... I ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) + sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) ) - sum_ i e. ( 1 ... I ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) ) = ( ( seq 1 ( + , F ) ` J ) - ( seq 1 ( + , F ) ` I ) ) )
80		fzfid 12187	. . . . . 6 |- ( ph -> ( 1 ... I ) e. Fin )
81	80, 77	fsumcl 13792	. . . . 5 |- ( ph -> sum_ i e. ( 1 ... I ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) e. CC )
82		fzofi 12188	. . . . . . 7 |- ( ( I + 1 )..^ ( J + 1 ) ) e. Fin
83	82	a1i 11	. . . . . 6 |- ( ph -> ( ( I + 1 )..^ ( J + 1 ) ) e. Fin )
84		ssun2 3631	. . . . . . . . 9 |- ( ( I + 1 )..^ ( J + 1 ) ) C_ ( ( 1..^ ( I + 1 ) ) u. ( ( I + 1 )..^ ( J + 1 ) ) )
85	84, 13	syl5sseqr 3514	. . . . . . . 8 |- ( ph -> ( ( I + 1 )..^ ( J + 1 ) ) C_ ( 1..^ ( J + 1 ) ) )
86	85	sselda 3465	. . . . . . 7 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> i e. ( 1..^ ( J + 1 ) ) )
87	86, 43	syldan 473	. . . . . 6 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) e. CC )
88	83, 87	fsumcl 13792	. . . . 5 |- ( ph -> sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) e. CC )
89	81, 88	pncan2d 9990	. . . 4 |- ( ph -> ( ( sum_ i e. ( 1 ... I ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) + sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) ) - sum_ i e. ( 1 ... I ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) ) = sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) )
90	79, 89	eqtr3d 2466	. . 3 |- ( ph -> ( ( seq 1 ( + , F ) ` J ) - ( seq 1 ( + , F ) ` I ) ) = sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) )
91	90	fveq2d 5883	. 2 |- ( ph -> ( abs ` ( ( seq 1 ( + , F ) ` J ) - ( seq 1 ( + , F ) ` I ) ) ) = ( abs ` sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) ) )
92	88	abscld 13491	. . 3 |- ( ph -> ( abs ` sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) ) e. RR )
93		2re 10681	. . . . . 6 |- 2 e. RR
94	93	a1i 11	. . . . 5 |- ( ph -> 2 e. RR )
95		dchrisum.9	. . . . 5 |- ( ph -> R e. RR )
96	94, 95	remulcld 9673	. . . 4 |- ( ph -> ( 2 x. R ) e. RR )
97	40	ralrimiva 2840	. . . . 5 |- ( ph -> A. i e. NN [_ i / n ]_ A e. RR )
98		csbeq1 3399	. . . . . . 7 |- ( i = ( I + 1 ) -> [_ i / n ]_ A = [_ ( I + 1 ) / n ]_ A )
99	98	eleq1d 2492	. . . . . 6 |- ( i = ( I + 1 ) -> ( [_ i / n ]_ A e. RR <-> [_ ( I + 1 ) / n ]_ A e. RR ) )
100	99	rspcv 3179	. . . . 5 |- ( ( I + 1 ) e. NN -> ( A. i e. NN [_ i / n ]_ A e. RR -> [_ ( I + 1 ) / n ]_ A e. RR ) )
101	4, 97, 100	sylc 63	. . . 4 |- ( ph -> [_ ( I + 1 ) / n ]_ A e. RR )
102	96, 101	remulcld 9673	. . 3 |- ( ph -> ( ( 2 x. R ) x. [_ ( I + 1 ) / n ]_ A ) e. RR )
103		dchrisumlem2.1	. . . . 5 |- ( ph -> U e. RR+ )
104	33	ralrimiva 2840	. . . . 5 |- ( ph -> A. n e. RR+ A e. RR )
105		nfcsb1v 3412	. . . . . . 7 |- F/_ n [_ U / n ]_ A
106	105	nfel1 2601	. . . . . 6 |- F/ n [_ U / n ]_ A e. RR
107		csbeq1a 3405	. . . . . . 7 |- ( n = U -> A = [_ U / n ]_ A )
108	107	eleq1d 2492	. . . . . 6 |- ( n = U -> ( A e. RR <-> [_ U / n ]_ A e. RR ) )
109	106, 108	rspc 3177	. . . . 5 |- ( U e. RR+ -> ( A. n e. RR+ A e. RR -> [_ U / n ]_ A e. RR ) )
110	103, 104, 109	sylc 63	. . . 4 |- ( ph -> [_ U / n ]_ A e. RR )
111	96, 110	remulcld 9673	. . 3 |- ( ph -> ( ( 2 x. R ) x. [_ U / n ]_ A ) e. RR )
112	71, 5	syl6eleqr 2522	. . . . . . . . . . . 12 |- ( ph -> J e. NN )
113	112	peano2nnd 10628	. . . . . . . . . . 11 |- ( ph -> ( J + 1 ) e. NN )
114	113	nnrpd 11341	. . . . . . . . . 10 |- ( ph -> ( J + 1 ) e. RR+ )
115	19, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36	dchrisumlema 24318	. . . . . . . . . . 11 |- ( ph -> ( ( ( J + 1 ) e. RR+ -> [_ ( J + 1 ) / n ]_ A e. RR ) /\ ( ( J + 1 ) e. ( M [,) +oo ) -> 0 <_ [_ ( J + 1 ) / n ]_ A ) ) )
116	115	simpld 461	. . . . . . . . . 10 |- ( ph -> ( ( J + 1 ) e. RR+ -> [_ ( J + 1 ) / n ]_ A e. RR ) )
117	114, 116	mpd 15	. . . . . . . . 9 |- ( ph -> [_ ( J + 1 ) / n ]_ A e. RR )
118	117	recnd 9671	. . . . . . . 8 |- ( ph -> [_ ( J + 1 ) / n ]_ A e. CC )
119		fzofi 12188	. . . . . . . . . 10 |- ( 0..^ ( J + 1 ) ) e. Fin
120	119	a1i 11	. . . . . . . . 9 |- ( ph -> ( 0..^ ( J + 1 ) ) e. Fin )
121		elfzoelz 11922	. . . . . . . . . 10 |- ( n e. ( 0..^ ( J + 1 ) ) -> n e. ZZ )
122	22	adantr 467	. . . . . . . . . . 11 |- ( ( ph /\ n e. ZZ ) -> X e. D )
123		simpr 463	. . . . . . . . . . 11 |- ( ( ph /\ n e. ZZ ) -> n e. ZZ )
124	18, 19, 20, 21, 122, 123	dchrzrhcl 24165	. . . . . . . . . 10 |- ( ( ph /\ n e. ZZ ) -> ( X ` ( L ` n ) ) e. CC )
125	121, 124	sylan2 477	. . . . . . . . 9 |- ( ( ph /\ n e. ( 0..^ ( J + 1 ) ) ) -> ( X ` ( L ` n ) ) e. CC )
126	120, 125	fsumcl 13792	. . . . . . . 8 |- ( ph -> sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) e. CC )
127	118, 126	mulcld 9665	. . . . . . 7 |- ( ph -> ( [_ ( J + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) e. CC )
128	101	recnd 9671	. . . . . . . 8 |- ( ph -> [_ ( I + 1 ) / n ]_ A e. CC )
129		fzofi 12188	. . . . . . . . . 10 |- ( 0..^ ( I + 1 ) ) e. Fin
130	129	a1i 11	. . . . . . . . 9 |- ( ph -> ( 0..^ ( I + 1 ) ) e. Fin )
131		elfzoelz 11922	. . . . . . . . . 10 |- ( n e. ( 0..^ ( I + 1 ) ) -> n e. ZZ )
132	131, 124	sylan2 477	. . . . . . . . 9 |- ( ( ph /\ n e. ( 0..^ ( I + 1 ) ) ) -> ( X ` ( L ` n ) ) e. CC )
133	130, 132	fsumcl 13792	. . . . . . . 8 |- ( ph -> sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) e. CC )
134	128, 133	mulcld 9665	. . . . . . 7 |- ( ph -> ( [_ ( I + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) e. CC )
135	127, 134	subcld 9988	. . . . . 6 |- ( ph -> ( ( [_ ( J + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) - ( [_ ( I + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) ) e. CC )
136	135	abscld 13491	. . . . 5 |- ( ph -> ( abs ` ( ( [_ ( J + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) - ( [_ ( I + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) ) ) e. RR )
137	86, 17	syl 17	. . . . . . . 8 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> i e. NN )
138		peano2nn 10623	. . . . . . . . . . . . 13 |- ( i e. NN -> ( i + 1 ) e. NN )
139	138	nnrpd 11341	. . . . . . . . . . . 12 |- ( i e. NN -> ( i + 1 ) e. RR+ )
140		nfcsb1v 3412	. . . . . . . . . . . . . . 15 |- F/_ n [_ ( i + 1 ) / n ]_ A
141	140	nfel1 2601	. . . . . . . . . . . . . 14 |- F/ n [_ ( i + 1 ) / n ]_ A e. RR
142		csbeq1a 3405	. . . . . . . . . . . . . . 15 |- ( n = ( i + 1 ) -> A = [_ ( i + 1 ) / n ]_ A )
143	142	eleq1d 2492	. . . . . . . . . . . . . 14 |- ( n = ( i + 1 ) -> ( A e. RR <-> [_ ( i + 1 ) / n ]_ A e. RR ) )
144	141, 143	rspc 3177	. . . . . . . . . . . . 13 |- ( ( i + 1 ) e. RR+ -> ( A. n e. RR+ A e. RR -> [_ ( i + 1 ) / n ]_ A e. RR ) )
145	144	impcom 432	. . . . . . . . . . . 12 |- ( ( A. n e. RR+ A e. RR /\ ( i + 1 ) e. RR+ ) -> [_ ( i + 1 ) / n ]_ A e. RR )
146	104, 139, 145	syl2an 480	. . . . . . . . . . 11 |- ( ( ph /\ i e. NN ) -> [_ ( i + 1 ) / n ]_ A e. RR )
147	146, 40	resubcld 10049	. . . . . . . . . 10 |- ( ( ph /\ i e. NN ) -> ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) e. RR )
148	147	recnd 9671	. . . . . . . . 9 |- ( ( ph /\ i e. NN ) -> ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) e. CC )
149		fzofi 12188	. . . . . . . . . . . 12 |- ( 0..^ ( i + 1 ) ) e. Fin
150	149	a1i 11	. . . . . . . . . . 11 |- ( ph -> ( 0..^ ( i + 1 ) ) e. Fin )
151		elfzoelz 11922	. . . . . . . . . . . 12 |- ( n e. ( 0..^ ( i + 1 ) ) -> n e. ZZ )
152	151, 124	sylan2 477	. . . . . . . . . . 11 |- ( ( ph /\ n e. ( 0..^ ( i + 1 ) ) ) -> ( X ` ( L ` n ) ) e. CC )
153	150, 152	fsumcl 13792	. . . . . . . . . 10 |- ( ph -> sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) e. CC )
154	153	adantr 467	. . . . . . . . 9 |- ( ( ph /\ i e. NN ) -> sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) e. CC )
155	148, 154	mulcld 9665	. . . . . . . 8 |- ( ( ph /\ i e. NN ) -> ( ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) x. sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) e. CC )
156	137, 155	syldan 473	. . . . . . 7 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) x. sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) e. CC )
157	83, 156	fsumcl 13792	. . . . . 6 |- ( ph -> sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) x. sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) e. CC )
158	157	abscld 13491	. . . . 5 |- ( ph -> ( abs ` sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) x. sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) ) e. RR )
159	136, 158	readdcld 9672	. . . 4 |- ( ph -> ( ( abs ` ( ( [_ ( J + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) - ( [_ ( I + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) ) ) + ( abs ` sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) x. sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) ) ) e. RR )
160	26, 41	mulcomd 9666	. . . . . . . . . 10 |- ( ( ph /\ i e. NN ) -> ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) = ( [_ i / n ]_ A x. ( X ` ( L ` i ) ) ) )
161		nnnn0 10878	. . . . . . . . . . . . . . . 16 |- ( i e. NN -> i e. NN0 )
162	161	adantl 468	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. NN ) -> i e. NN0 )
163		nn0uz 11195	. . . . . . . . . . . . . . 15 |- NN0 = ( ZZ>= ` 0 )
164	162, 163	syl6eleq 2521	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. NN ) -> i e. ( ZZ>= ` 0 ) )
165		elfzelz 11802	. . . . . . . . . . . . . . 15 |- ( n e. ( 0 ... i ) -> n e. ZZ )
166	124	adantlr 720	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. NN ) /\ n e. ZZ ) -> ( X ` ( L ` n ) ) e. CC )
167	165, 166	sylan2 477	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. NN ) /\ n e. ( 0 ... i ) ) -> ( X ` ( L ` n ) ) e. CC )
168	164, 167, 63	fzosump1 13806	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. NN ) -> sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) = ( sum_ n e. ( 0..^ i ) ( X ` ( L ` n ) ) + ( X ` ( L ` i ) ) ) )
169	168	oveq1d 6318	. . . . . . . . . . . 12 |- ( ( ph /\ i e. NN ) -> ( sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) - sum_ n e. ( 0..^ i ) ( X ` ( L ` n ) ) ) = ( ( sum_ n e. ( 0..^ i ) ( X ` ( L ` n ) ) + ( X ` ( L ` i ) ) ) - sum_ n e. ( 0..^ i ) ( X ` ( L ` n ) ) ) )
170		fzofi 12188	. . . . . . . . . . . . . . 15 |- ( 0..^ i ) e. Fin
171	170	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. NN ) -> ( 0..^ i ) e. Fin )
172		elfzoelz 11922	. . . . . . . . . . . . . . 15 |- ( n e. ( 0..^ i ) -> n e. ZZ )
173	172, 166	sylan2 477	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. NN ) /\ n e. ( 0..^ i ) ) -> ( X ` ( L ` n ) ) e. CC )
174	171, 173	fsumcl 13792	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. NN ) -> sum_ n e. ( 0..^ i ) ( X ` ( L ` n ) ) e. CC )
175	174, 26	pncan2d 9990	. . . . . . . . . . . 12 |- ( ( ph /\ i e. NN ) -> ( ( sum_ n e. ( 0..^ i ) ( X ` ( L ` n ) ) + ( X ` ( L ` i ) ) ) - sum_ n e. ( 0..^ i ) ( X ` ( L ` n ) ) ) = ( X ` ( L ` i ) ) )
176	169, 175	eqtr2d 2465	. . . . . . . . . . 11 |- ( ( ph /\ i e. NN ) -> ( X ` ( L ` i ) ) = ( sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) - sum_ n e. ( 0..^ i ) ( X ` ( L ` n ) ) ) )
177	176	oveq2d 6319	. . . . . . . . . 10 |- ( ( ph /\ i e. NN ) -> ( [_ i / n ]_ A x. ( X ` ( L ` i ) ) ) = ( [_ i / n ]_ A x. ( sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) - sum_ n e. ( 0..^ i ) ( X ` ( L ` n ) ) ) ) )
178	160, 177	eqtrd 2464	. . . . . . . . 9 |- ( ( ph /\ i e. NN ) -> ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) = ( [_ i / n ]_ A x. ( sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) - sum_ n e. ( 0..^ i ) ( X ` ( L ` n ) ) ) ) )
179	137, 178	syldan 473	. . . . . . . 8 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) = ( [_ i / n ]_ A x. ( sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) - sum_ n e. ( 0..^ i ) ( X ` ( L ` n ) ) ) ) )
180	179	sumeq2dv 13762	. . . . . . 7 |- ( ph -> sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) = sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( [_ i / n ]_ A x. ( sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) - sum_ n e. ( 0..^ i ) ( X ` ( L ` n ) ) ) ) )
181		csbeq1 3399	. . . . . . . . 9 |- ( k = i -> [_ k / n ]_ A = [_ i / n ]_ A )
182		oveq2 6311	. . . . . . . . . 10 |- ( k = i -> ( 0..^ k ) = ( 0..^ i ) )
183	182	sumeq1d 13760	. . . . . . . . 9 |- ( k = i -> sum_ n e. ( 0..^ k ) ( X ` ( L ` n ) ) = sum_ n e. ( 0..^ i ) ( X ` ( L ` n ) ) )
184	181, 183	jca 535	. . . . . . . 8 |- ( k = i -> ( [_ k / n ]_ A = [_ i / n ]_ A /\ sum_ n e. ( 0..^ k ) ( X ` ( L ` n ) ) = sum_ n e. ( 0..^ i ) ( X ` ( L ` n ) ) ) )
185		csbeq1 3399	. . . . . . . . 9 |- ( k = ( i + 1 ) -> [_ k / n ]_ A = [_ ( i + 1 ) / n ]_ A )
186		oveq2 6311	. . . . . . . . . 10 |- ( k = ( i + 1 ) -> ( 0..^ k ) = ( 0..^ ( i + 1 ) ) )
187	186	sumeq1d 13760	. . . . . . . . 9 |- ( k = ( i + 1 ) -> sum_ n e. ( 0..^ k ) ( X ` ( L ` n ) ) = sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) )
188	185, 187	jca 535	. . . . . . . 8 |- ( k = ( i + 1 ) -> ( [_ k / n ]_ A = [_ ( i + 1 ) / n ]_ A /\ sum_ n e. ( 0..^ k ) ( X ` ( L ` n ) ) = sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) )
189		csbeq1 3399	. . . . . . . . 9 |- ( k = ( I + 1 ) -> [_ k / n ]_ A = [_ ( I + 1 ) / n ]_ A )
190		oveq2 6311	. . . . . . . . . 10 |- ( k = ( I + 1 ) -> ( 0..^ k ) = ( 0..^ ( I + 1 ) ) )
191	190	sumeq1d 13760	. . . . . . . . 9 |- ( k = ( I + 1 ) -> sum_ n e. ( 0..^ k ) ( X ` ( L ` n ) ) = sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) )
192	189, 191	jca 535	. . . . . . . 8 |- ( k = ( I + 1 ) -> ( [_ k / n ]_ A = [_ ( I + 1 ) / n ]_ A /\ sum_ n e. ( 0..^ k ) ( X ` ( L ` n ) ) = sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) )
193		csbeq1 3399	. . . . . . . . 9 |- ( k = ( J + 1 ) -> [_ k / n ]_ A = [_ ( J + 1 ) / n ]_ A )
194		oveq2 6311	. . . . . . . . . 10 |- ( k = ( J + 1 ) -> ( 0..^ k ) = ( 0..^ ( J + 1 ) ) )
195	194	sumeq1d 13760	. . . . . . . . 9 |- ( k = ( J + 1 ) -> sum_ n e. ( 0..^ k ) ( X ` ( L ` n ) ) = sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) )
196	193, 195	jca 535	. . . . . . . 8 |- ( k = ( J + 1 ) -> ( [_ k / n ]_ A = [_ ( J + 1 ) / n ]_ A /\ sum_ n e. ( 0..^ k ) ( X ` ( L ` n ) ) = sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) )
197		elfzuz 11798	. . . . . . . . . 10 |- ( k e. ( ( I + 1 ) ... ( J + 1 ) ) -> k e. ( ZZ>= ` ( I + 1 ) ) )
198		eluznn 11231	. . . . . . . . . 10 |- ( ( ( I + 1 ) e. NN /\ k e. ( ZZ>= ` ( I + 1 ) ) ) -> k e. NN )
199	4, 197, 198	syl2an 480	. . . . . . . . 9 |- ( ( ph /\ k e. ( ( I + 1 ) ... ( J + 1 ) ) ) -> k e. NN )
200	41	ralrimiva 2840	. . . . . . . . . 10 |- ( ph -> A. i e. NN [_ i / n ]_ A e. CC )
201		csbeq1 3399	. . . . . . . . . . . 12 |- ( i = k -> [_ i / n ]_ A = [_ k / n ]_ A )
202	201	eleq1d 2492	. . . . . . . . . . 11 |- ( i = k -> ( [_ i / n ]_ A e. CC <-> [_ k / n ]_ A e. CC ) )
203	202	rspccva 3182	. . . . . . . . . 10 |- ( ( A. i e. NN [_ i / n ]_ A e. CC /\ k e. NN ) -> [_ k / n ]_ A e. CC )
204	200, 203	sylan 474	. . . . . . . . 9 |- ( ( ph /\ k e. NN ) -> [_ k / n ]_ A e. CC )
205	199, 204	syldan 473	. . . . . . . 8 |- ( ( ph /\ k e. ( ( I + 1 ) ... ( J + 1 ) ) ) -> [_ k / n ]_ A e. CC )
206		fzofi 12188	. . . . . . . . . . 11 |- ( 0..^ k ) e. Fin
207	206	a1i 11	. . . . . . . . . 10 |- ( ph -> ( 0..^ k ) e. Fin )
208		elfzoelz 11922	. . . . . . . . . . 11 |- ( n e. ( 0..^ k ) -> n e. ZZ )
209	208, 124	sylan2 477	. . . . . . . . . 10 |- ( ( ph /\ n e. ( 0..^ k ) ) -> ( X ` ( L ` n ) ) e. CC )
210	207, 209	fsumcl 13792	. . . . . . . . 9 |- ( ph -> sum_ n e. ( 0..^ k ) ( X ` ( L ` n ) ) e. CC )
211	210	adantr 467	. . . . . . . 8 |- ( ( ph /\ k e. ( ( I + 1 ) ... ( J + 1 ) ) ) -> sum_ n e. ( 0..^ k ) ( X ` ( L ` n ) ) e. CC )
212	184, 188, 192, 196, 9, 205, 211	fsumparts 13859	. . . . . . 7 |- ( ph -> sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( [_ i / n ]_ A x. ( sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) - sum_ n e. ( 0..^ i ) ( X ` ( L ` n ) ) ) ) = ( ( ( [_ ( J + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) - ( [_ ( I + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) ) - sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) x. sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) ) )
213	180, 212	eqtrd 2464	. . . . . 6 |- ( ph -> sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) = ( ( ( [_ ( J + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) - ( [_ ( I + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) ) - sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) x. sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) ) )
214	213	fveq2d 5883	. . . . 5 |- ( ph -> ( abs ` sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) ) = ( abs ` ( ( ( [_ ( J + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) - ( [_ ( I + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) ) - sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) x. sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) ) ) )
215	135, 157	abs2dif2d 13513	. . . . 5 |- ( ph -> ( abs ` ( ( ( [_ ( J + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) - ( [_ ( I + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) ) - sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) x. sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) ) ) <_ ( ( abs ` ( ( [_ ( J + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) - ( [_ ( I + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) ) ) + ( abs ` sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) x. sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) ) ) )
216	214, 215	eqbrtrd 4442	. . . 4 |- ( ph -> ( abs ` sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) ) <_ ( ( abs ` ( ( [_ ( J + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) - ( [_ ( I + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) ) ) + ( abs ` sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) x. sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) ) ) )
217	117, 101	readdcld 9672	. . . . . . 7 |- ( ph -> ( [_ ( J + 1 ) / n ]_ A + [_ ( I + 1 ) / n ]_ A ) e. RR )
218	217, 95	remulcld 9673	. . . . . 6 |- ( ph -> ( ( [_ ( J + 1 ) / n ]_ A + [_ ( I + 1 ) / n ]_ A ) x. R ) e. RR )
219	181, 185, 189, 193, 9, 205	telfsumo 13855	. . . . . . . 8 |- ( ph -> sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) = ( [_ ( I + 1 ) / n ]_ A - [_ ( J + 1 ) / n ]_ A ) )
220	137, 40	syldan 473	. . . . . . . . . 10 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> [_ i / n ]_ A e. RR )
221	137, 146	syldan 473	. . . . . . . . . 10 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> [_ ( i + 1 ) / n ]_ A e. RR )
222	220, 221	resubcld 10049	. . . . . . . . 9 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) e. RR )
223	83, 222	fsumrecl 13793	. . . . . . . 8 |- ( ph -> sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) e. RR )
224	219, 223	eqeltrrd 2512	. . . . . . 7 |- ( ph -> ( [_ ( I + 1 ) / n ]_ A - [_ ( J + 1 ) / n ]_ A ) e. RR )
225	224, 95	remulcld 9673	. . . . . 6 |- ( ph -> ( ( [_ ( I + 1 ) / n ]_ A - [_ ( J + 1 ) / n ]_ A ) x. R ) e. RR )
226	127	abscld 13491	. . . . . . . 8 |- ( ph -> ( abs ` ( [_ ( J + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) ) e. RR )
227	134	abscld 13491	. . . . . . . 8 |- ( ph -> ( abs ` ( [_ ( I + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) ) e. RR )
228	226, 227	readdcld 9672	. . . . . . 7 |- ( ph -> ( ( abs ` ( [_ ( J + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) ) + ( abs ` ( [_ ( I + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) ) ) e. RR )
229	127, 134	abs2dif2d 13513	. . . . . . 7 |- ( ph -> ( abs ` ( ( [_ ( J + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) - ( [_ ( I + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) ) ) <_ ( ( abs ` ( [_ ( J + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) ) + ( abs ` ( [_ ( I + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) ) ) )
230	117, 95	remulcld 9673	. . . . . . . . 9 |- ( ph -> ( [_ ( J + 1 ) / n ]_ A x. R ) e. RR )
231	101, 95	remulcld 9673	. . . . . . . . 9 |- ( ph -> ( [_ ( I + 1 ) / n ]_ A x. R ) e. RR )
232	118, 126	absmuld 13509	. . . . . . . . . . 11 |- ( ph -> ( abs ` ( [_ ( J + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) ) = ( ( abs ` [_ ( J + 1 ) / n ]_ A ) x. ( abs ` sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) ) )
233		eluzelre 11171	. . . . . . . . . . . . . . . . . . 19 |- ( i e. ( ZZ>= ` M ) -> i e. RR )
234	233	adantl 468	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> i e. RR )
235		eluzle 11173	. . . . . . . . . . . . . . . . . . 19 |- ( i e. ( ZZ>= ` M ) -> M <_ i )
236	235	adantl 468	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> M <_ i )
237	32	nnred 10626	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> M e. RR )
238	237	adantr 467	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> M e. RR )
239		elicopnf 11732	. . . . . . . . . . . . . . . . . . 19 |- ( M e. RR -> ( i e. ( M [,) +oo ) <-> ( i e. RR /\ M <_ i ) ) )
240	238, 239	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> ( i e. ( M [,) +oo ) <-> ( i e. RR /\ M <_ i ) ) )
241	234, 236, 240	mpbir2and 931	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> i e. ( M [,) +oo ) )
242	241	ex 436	. . . . . . . . . . . . . . . 16 |- ( ph -> ( i e. ( ZZ>= ` M ) -> i e. ( M [,) +oo ) ) )
243	242	ssrdv 3471	. . . . . . . . . . . . . . 15 |- ( ph -> ( ZZ>= ` M ) C_ ( M [,) +oo ) )
244	32	nnzd 11041	. . . . . . . . . . . . . . . . 17 |- ( ph -> M e. ZZ )
245	49	peano2zd 11045	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( I + 1 ) e. ZZ )
246	103	rpred 11343	. . . . . . . . . . . . . . . . . 18 |- ( ph -> U e. RR )
247	4	nnred 10626	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( I + 1 ) e. RR )
248		dchrisumlem2.2	. . . . . . . . . . . . . . . . . 18 |- ( ph -> M <_ U )
249		dchrisumlem2.3	. . . . . . . . . . . . . . . . . 18 |- ( ph -> U <_ ( I + 1 ) )
250	237, 246, 247, 248, 249	letrd 9794	. . . . . . . . . . . . . . . . 17 |- ( ph -> M <_ ( I + 1 ) )
251		eluz2 11167	. . . . . . . . . . . . . . . . 17 |- ( ( I + 1 ) e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ ( I + 1 ) e. ZZ /\ M <_ ( I + 1 ) ) )
252	244, 245, 250, 251	syl3anbrc 1190	. . . . . . . . . . . . . . . 16 |- ( ph -> ( I + 1 ) e. ( ZZ>= ` M ) )
253		uztrn 11177	. . . . . . . . . . . . . . . 16 |- ( ( ( J + 1 ) e. ( ZZ>= ` ( I + 1 ) ) /\ ( I + 1 ) e. ( ZZ>= ` M ) ) -> ( J + 1 ) e. ( ZZ>= ` M ) )
254	9, 252, 253	syl2anc 666	. . . . . . . . . . . . . . 15 |- ( ph -> ( J + 1 ) e. ( ZZ>= ` M ) )
255	243, 254	sseldd 3466	. . . . . . . . . . . . . 14 |- ( ph -> ( J + 1 ) e. ( M [,) +oo ) )
256	115	simprd 465	. . . . . . . . . . . . . 14 |- ( ph -> ( ( J + 1 ) e. ( M [,) +oo ) -> 0 <_ [_ ( J + 1 ) / n ]_ A ) )
257	255, 256	mpd 15	. . . . . . . . . . . . 13 |- ( ph -> 0 <_ [_ ( J + 1 ) / n ]_ A )
258	117, 257	absidd 13478	. . . . . . . . . . . 12 |- ( ph -> ( abs ` [_ ( J + 1 ) / n ]_ A ) = [_ ( J + 1 ) / n ]_ A )
259	258	oveq1d 6318	. . . . . . . . . . 11 |- ( ph -> ( ( abs ` [_ ( J + 1 ) / n ]_ A ) x. ( abs ` sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) ) = ( [_ ( J + 1 ) / n ]_ A x. ( abs ` sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) ) )
260	232, 259	eqtrd 2464	. . . . . . . . . 10 |- ( ph -> ( abs ` ( [_ ( J + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) ) = ( [_ ( J + 1 ) / n ]_ A x. ( abs ` sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) ) )
261	126	abscld 13491	. . . . . . . . . . 11 |- ( ph -> ( abs ` sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) e. RR )
262	113	nnnn0d 10927	. . . . . . . . . . . 12 |- ( ph -> ( J + 1 ) e. NN0 )
263		dchrisum.10	. . . . . . . . . . . . 13 |- ( ph -> A. u e. ( 0..^ N ) ( abs ` sum_ n e. ( 0..^ u ) ( X ` ( L ` n ) ) ) <_ R )
264	19, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36, 95, 263	dchrisumlem1 24319	. . . . . . . . . . . 12 |- ( ( ph /\ ( J + 1 ) e. NN0 ) -> ( abs ` sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) <_ R )
265	262, 264	mpdan 673	. . . . . . . . . . 11 |- ( ph -> ( abs ` sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) <_ R )
266	261, 95, 117, 257, 265	lemul2ad 10549	. . . . . . . . . 10 |- ( ph -> ( [_ ( J + 1 ) / n ]_ A x. ( abs ` sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) ) <_ ( [_ ( J + 1 ) / n ]_ A x. R ) )
267	260, 266	eqbrtrd 4442	. . . . . . . . 9 |- ( ph -> ( abs ` ( [_ ( J + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) ) <_ ( [_ ( J + 1 ) / n ]_ A x. R ) )
268	128, 133	absmuld 13509	. . . . . . . . . . 11 |- ( ph -> ( abs ` ( [_ ( I + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) ) = ( ( abs ` [_ ( I + 1 ) / n ]_ A ) x. ( abs ` sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) ) )
269	243, 252	sseldd 3466	. . . . . . . . . . . . . 14 |- ( ph -> ( I + 1 ) e. ( M [,) +oo ) )
270	19, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36	dchrisumlema 24318	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( ( I + 1 ) e. RR+ -> [_ ( I + 1 ) / n ]_ A e. RR ) /\ ( ( I + 1 ) e. ( M [,) +oo ) -> 0 <_ [_ ( I + 1 ) / n ]_ A ) ) )
271	270	simprd 465	. . . . . . . . . . . . . 14 |- ( ph -> ( ( I + 1 ) e. ( M [,) +oo ) -> 0 <_ [_ ( I + 1 ) / n ]_ A ) )
272	269, 271	mpd 15	. . . . . . . . . . . . 13 |- ( ph -> 0 <_ [_ ( I + 1 ) / n ]_ A )
273	101, 272	absidd 13478	. . . . . . . . . . . 12 |- ( ph -> ( abs ` [_ ( I + 1 ) / n ]_ A ) = [_ ( I + 1 ) / n ]_ A )
274	273	oveq1d 6318	. . . . . . . . . . 11 |- ( ph -> ( ( abs ` [_ ( I + 1 ) / n ]_ A ) x. ( abs ` sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) ) = ( [_ ( I + 1 ) / n ]_ A x. ( abs ` sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) ) )
275	268, 274	eqtrd 2464	. . . . . . . . . 10 |- ( ph -> ( abs ` ( [_ ( I + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) ) = ( [_ ( I + 1 ) / n ]_ A x. ( abs ` sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) ) )
276	133	abscld 13491	. . . . . . . . . . 11 |- ( ph -> ( abs ` sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) e. RR )
277	4	nnnn0d 10927	. . . . . . . . . . . 12 |- ( ph -> ( I + 1 ) e. NN0 )
278	19, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36, 95, 263	dchrisumlem1 24319	. . . . . . . . . . . 12 |- ( ( ph /\ ( I + 1 ) e. NN0 ) -> ( abs ` sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) <_ R )
279	277, 278	mpdan 673	. . . . . . . . . . 11 |- ( ph -> ( abs ` sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) <_ R )
280	276, 95, 101, 272, 279	lemul2ad 10549	. . . . . . . . . 10 |- ( ph -> ( [_ ( I + 1 ) / n ]_ A x. ( abs ` sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) ) <_ ( [_ ( I + 1 ) / n ]_ A x. R ) )
281	275, 280	eqbrtrd 4442	. . . . . . . . 9 |- ( ph -> ( abs ` ( [_ ( I + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) ) <_ ( [_ ( I + 1 ) / n ]_ A x. R ) )
282	226, 227, 230, 231, 267, 281	le2addd 10234	. . . . . . . 8 |- ( ph -> ( ( abs ` ( [_ ( J + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) ) + ( abs ` ( [_ ( I + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) ) ) <_ ( ( [_ ( J + 1 ) / n ]_ A x. R ) + ( [_ ( I + 1 ) / n ]_ A x. R ) ) )
283	95	recnd 9671	. . . . . . . . 9 |- ( ph -> R e. CC )
284	118, 128, 283	adddird 9670	. . . . . . . 8 |- ( ph -> ( ( [_ ( J + 1 ) / n ]_ A + [_ ( I + 1 ) / n ]_ A ) x. R ) = ( ( [_ ( J + 1 ) / n ]_ A x. R ) + ( [_ ( I + 1 ) / n ]_ A x. R ) ) )
285	282, 284	breqtrrd 4448	. . . . . . 7 |- ( ph -> ( ( abs ` ( [_ ( J + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) ) + ( abs ` ( [_ ( I + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) ) ) <_ ( ( [_ ( J + 1 ) / n ]_ A + [_ ( I + 1 ) / n ]_ A ) x. R ) )
286	136, 228, 218, 229, 285	letrd 9794	. . . . . 6 |- ( ph -> ( abs ` ( ( [_ ( J + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) - ( [_ ( I + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) ) ) <_ ( ( [_ ( J + 1 ) / n ]_ A + [_ ( I + 1 ) / n ]_ A ) x. R ) )
287	156	abscld 13491	. . . . . . . 8 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( abs ` ( ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) x. sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) ) e. RR )
288	83, 287	fsumrecl 13793	. . . . . . 7 |- ( ph -> sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( abs ` ( ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) x. sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) ) e. RR )
289	83, 156	fsumabs 13854	. . . . . . 7 |- ( ph -> ( abs ` sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) x. sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) ) <_ sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( abs ` ( ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) x. sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) ) )
290	95	adantr 467	. . . . . . . . . 10 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> R e. RR )
291	222, 290	remulcld 9673	. . . . . . . . 9 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) x. R ) e. RR )
292	137, 148	syldan 473	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) e. CC )
293	153	adantr 467	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) e. CC )
294	292, 293	absmuld 13509	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( abs ` ( ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) x. sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) ) = ( ( abs ` ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) ) x. ( abs ` sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) ) )
295		elfzouz 11926	. . . . . . . . . . . . . . 15 |- ( i e. ( ( I + 1 )..^ ( J + 1 ) ) -> i e. ( ZZ>= ` ( I + 1 ) ) )
296		uztrn 11177	. . . . . . . . . . . . . . 15 |- ( ( i e. ( ZZ>= ` ( I + 1 ) ) /\ ( I + 1 ) e. ( ZZ>= ` M ) ) -> i e. ( ZZ>= ` M ) )
297	295, 252, 296	syl2anr 481	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> i e. ( ZZ>= ` M ) )
298		eluznn 11231	. . . . . . . . . . . . . . . . 17 |- ( ( M e. NN /\ i e. ( ZZ>= ` M ) ) -> i e. NN )
299	32, 298	sylan 474	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> i e. NN )
300	299, 139	syl 17	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> ( i + 1 ) e. RR+ )
301	299	nnrpd 11341	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> i e. RR+ )
302	34	3expia 1208	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) ) -> ( ( M <_ n /\ n <_ x ) -> B <_ A ) )
303	302	ralrimivva 2847	. . . . . . . . . . . . . . . . 17 |- ( ph -> A. n e. RR+ A. x e. RR+ ( ( M <_ n /\ n <_ x ) -> B <_ A ) )
304	303	adantr 467	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> A. n e. RR+ A. x e. RR+ ( ( M <_ n /\ n <_ x ) -> B <_ A ) )
305		nfcv 2585	. . . . . . . . . . . . . . . . . 18 |- F/_ n RR+
306		nfv 1752	. . . . . . . . . . . . . . . . . . 19 |- F/ n ( M <_ i /\ i <_ x )
307		nfcv 2585	. . . . . . . . . . . . . . . . . . . 20 |- F/_ n B
308		nfcv 2585	. . . . . . . . . . . . . . . . . . . 20 |- F/_ n <_
309	307, 308, 60	nfbr 4466	. . . . . . . . . . . . . . . . . . 19 |- F/ n B <_ [_ i / n ]_ A
310	306, 309	nfim 1977	. . . . . . . . . . . . . . . . . 18 |- F/ n ( ( M <_ i /\ i <_ x ) -> B <_ [_ i / n ]_ A )
311	305, 310	nfral 2812	. . . . . . . . . . . . . . . . 17 |- F/ n A. x e. RR+ ( ( M <_ i /\ i <_ x ) -> B <_ [_ i / n ]_ A )
312		breq2 4425	. . . . . . . . . . . . . . . . . . . 20 |- ( n = i -> ( M <_ n <-> M <_ i ) )
313		breq1 4424	. . . . . . . . . . . . . . . . . . . 20 |- ( n = i -> ( n <_ x <-> i <_ x ) )
314	312, 313	anbi12d 716	. . . . . . . . . . . . . . . . . . 19 |- ( n = i -> ( ( M <_ n /\ n <_ x ) <-> ( M <_ i /\ i <_ x ) ) )
315	64	breq2d 4433	. . . . . . . . . . . . . . . . . . 19 |- ( n = i -> ( B <_ A <-> B <_ [_ i / n ]_ A ) )
316	314, 315	imbi12d 322	. . . . . . . . . . . . . . . . . 18 |- ( n = i -> ( ( ( M <_ n /\ n <_ x ) -> B <_ A ) <-> ( ( M <_ i /\ i <_ x ) -> B <_ [_ i / n ]_ A ) ) )
317	316	ralbidv 2865	. . . . . . . . . . . . . . . . 17 |- ( n = i -> ( A. x e. RR+ ( ( M <_ n /\ n <_ x ) -> B <_ A ) <-> A. x e. RR+ ( ( M <_ i /\ i <_ x ) -> B <_ [_ i / n ]_ A ) ) )
318	311, 317	rspc 3177	. . . . . . . . . . . . . . . 16 |- ( i e. RR+ -> ( A. n e. RR+ A. x e. RR+ ( ( M <_ n /\ n <_ x ) -> B <_ A ) -> A. x e. RR+ ( ( M <_ i /\ i <_ x ) -> B <_ [_ i / n ]_ A ) ) )
319	301, 304, 318	sylc 63	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> A. x e. RR+ ( ( M <_ i /\ i <_ x ) -> B <_ [_ i / n ]_ A ) )
320	234	lep1d 10540	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> i <_ ( i + 1 ) )
321	236, 320	jca 535	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> ( M <_ i /\ i <_ ( i + 1 ) ) )
322		breq2 4425	. . . . . . . . . . . . . . . . . 18 |- ( x = ( i + 1 ) -> ( i <_ x <-> i <_ ( i + 1 ) ) )
323	322	anbi2d 709	. . . . . . . . . . . . . . . . 17 |- ( x = ( i + 1 ) -> ( ( M <_ i /\ i <_ x ) <-> ( M <_ i /\ i <_ ( i + 1 ) ) ) )
324		eqvisset 3090	. . . . . . . . . . . . . . . . . . . 20 |- ( x = ( i + 1 ) -> ( i + 1 ) e. _V )
325		eqtr3 2451	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( x = ( i + 1 ) /\ n = ( i + 1 ) ) -> x = n )
326	31	equcoms 1846	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = n -> A = B )
327	325, 326	syl 17	. . . . . . . . . . . . . . . . . . . 20 |- ( ( x = ( i + 1 ) /\ n = ( i + 1 ) ) -> A = B )
328	324, 327	csbied 3423	. . . . . . . . . . . . . . . . . . 19 |- ( x = ( i + 1 ) -> [_ ( i + 1 ) / n ]_ A = B )
329	328	eqcomd 2431	. . . . . . . . . . . . . . . . . 18 |- ( x = ( i + 1 ) -> B = [_ ( i + 1 ) / n ]_ A )
330	329	breq1d 4431	. . . . . . . . . . . . . . . . 17 |- ( x = ( i + 1 ) -> ( B <_ [_ i / n ]_ A <-> [_ ( i + 1 ) / n ]_ A <_ [_ i / n ]_ A ) )
331	323, 330	imbi12d 322	. . . . . . . . . . . . . . . 16 |- ( x = ( i + 1 ) -> ( ( ( M <_ i /\ i <_ x ) -> B <_ [_ i / n ]_ A ) <-> ( ( M <_ i /\ i <_ ( i + 1 ) ) -> [_ ( i + 1 ) / n ]_ A <_ [_ i / n ]_ A ) ) )
332	331	rspcv 3179	. . . . . . . . . . . . . . 15 |- ( ( i + 1 ) e. RR+ -> ( A. x e. RR+ ( ( M <_ i /\ i <_ x ) -> B <_ [_ i / n ]_ A ) -> ( ( M <_ i /\ i <_ ( i + 1 ) ) -> [_ ( i + 1 ) / n ]_ A <_ [_ i / n ]_ A ) ) )
333	300, 319, 321, 332	syl3c 64	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> [_ ( i + 1 ) / n ]_ A <_ [_ i / n ]_ A )
334	297, 333	syldan 473	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> [_ ( i + 1 ) / n ]_ A <_ [_ i / n ]_ A )
335	221, 220, 334	abssuble0d 13488	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( abs ` ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) ) = ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) )
336	335	oveq1d 6318	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( ( abs ` ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) ) x. ( abs ` sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) ) = ( ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) x. ( abs ` sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) ) )
337	294, 336	eqtrd 2464	. . . . . . . . . 10 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( abs ` ( ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) x. sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) ) = ( ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) x. ( abs ` sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) ) )
338	293	abscld 13491	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( abs ` sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) e. RR )
339	220, 221	subge0d 10205	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( 0 <_ ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) <-> [_ ( i + 1 ) / n ]_ A <_ [_ i / n ]_ A ) )
340	334, 339	mpbird 236	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> 0 <_ ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) )
341	137	peano2nnd 10628	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( i + 1 ) e. NN )
342	341	nnnn0d 10927	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( i + 1 ) e. NN0 )
343	19, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36, 95, 263	dchrisumlem1 24319	. . . . . . . . . . . 12 |- ( ( ph /\ ( i + 1 ) e. NN0 ) -> ( abs ` sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) <_ R )
344	342, 343	syldan 473	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( abs ` sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) <_ R )
345	338, 290, 222, 340, 344	lemul2ad 10549	. . . . . . . . . 10 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) x. ( abs ` sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) ) <_ ( ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) x. R ) )
346	337, 345	eqbrtrd 4442	. . . . . . . . 9 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( abs ` ( ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) x. sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) ) <_ ( ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) x. R ) )
347	83, 287, 291, 346	fsumle 13852	. . . . . . . 8 |- ( ph -> sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( abs ` ( ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) x. sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) ) <_ sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) x. R ) )
348	222	recnd 9671	. . . . . . . . . 10 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) e. CC )
349	83, 283, 348	fsummulc1 13839	. . . . . . . . 9 |- ( ph -> ( sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) x. R ) = sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) x. R ) )
350	219	oveq1d 6318	. . . . . . . . 9 |- ( ph -> ( sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) x. R ) = ( ( [_ ( I + 1 ) / n ]_ A - [_ ( J + 1 ) / n ]_ A ) x. R ) )
351	349, 350	eqtr3d 2466	. . . . . . . 8 |- ( ph -> sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) x. R ) = ( ( [_ ( I + 1 ) / n ]_ A - [_ ( J + 1 ) / n ]_ A ) x. R ) )
352	347, 351	breqtrd 4446	. . . . . . 7 |- ( ph -> sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( abs ` ( ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) x. sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) ) <_ ( ( [_ ( I + 1 ) / n ]_ A - [_ ( J + 1 ) / n ]_ A ) x. R ) )
353	158, 288, 225, 289, 352	letrd 9794	. . . . . 6 |- ( ph -> ( abs ` sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) x. sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) ) <_ ( ( [_ ( I + 1 ) / n ]_ A - [_ ( J + 1 ) / n ]_ A ) x. R ) )
354	136, 158, 218, 225, 286, 353	le2addd 10234	. . . . 5 |- ( ph -> ( ( abs ` ( ( [_ ( J + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) - ( [_ ( I + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) ) ) + ( abs ` sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) x. sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) ) ) <_ ( ( ( [_ ( J + 1 ) / n ]_ A + [_ ( I + 1 ) / n ]_ A ) x. R ) + ( ( [_ ( I + 1 ) / n ]_ A - [_ ( J + 1 ) / n ]_ A ) x. R ) ) )
355	128	2timesd 10857	. . . . . . . 8 |- ( ph -> ( 2 x. [_ ( I + 1 ) / n ]_ A ) = ( [_ ( I + 1 ) / n ]_ A + [_ ( I + 1 ) / n ]_ A ) )
356	128, 118, 128	ppncand 10028	. . . . . . . 8 |- ( ph -> ( ( [_ ( I + 1 ) / n ]_ A + [_ ( J + 1 ) / n ]_ A ) + ( [_ ( I + 1 ) / n ]_ A - [_ ( J + 1 ) / n ]_ A ) ) = ( [_ ( I + 1 ) / n ]_ A + [_ ( I + 1 ) / n ]_ A ) )
357	128, 118	addcomd 9837	. . . . . . . . 9 |- ( ph -> ( [_ ( I + 1 ) / n ]_ A + [_ ( J + 1 ) / n ]_ A ) = ( [_ ( J + 1 ) / n ]_ A + [_ ( I + 1 ) / n ]_ A ) )
358	357	oveq1d 6318	. . . . . . . 8 |- ( ph -> ( ( [_ ( I + 1 ) / n ]_ A + [_ ( J + 1 ) / n ]_ A ) + ( [_ ( I + 1 ) / n ]_ A - [_ ( J + 1 ) / n ]_ A ) ) = ( ( [_ ( J + 1 ) / n ]_ A + [_ ( I + 1 ) / n ]_ A ) + ( [_ ( I + 1 ) / n ]_ A - [_ ( J + 1 ) / n ]_ A ) ) )
359	355, 356, 358	3eqtr2d 2470	. . . . . . 7 |- ( ph -> ( 2 x. [_ ( I + 1 ) / n ]_ A ) = ( ( [_ ( J + 1 ) / n ]_ A + [_ ( I + 1 ) / n ]_ A ) + ( [_ ( I + 1 ) / n ]_ A - [_ ( J + 1 ) / n ]_ A ) ) )
360	359	oveq1d 6318	. . . . . 6 |- ( ph -> ( ( 2 x. [_ ( I + 1 ) / n ]_ A ) x. R ) = ( ( ( [_ ( J + 1 ) / n ]_ A + [_ ( I + 1 ) / n ]_ A ) + ( [_ ( I + 1 ) / n ]_ A - [_ ( J + 1 ) / n ]_ A ) ) x. R ) )
361		2cnd 10684	. . . . . . 7 |- ( ph -> 2 e. CC )
362	361, 128, 283	mul32d 9845	. . . . . 6 |- ( ph -> ( ( 2 x. [_ ( I + 1 ) / n ]_ A ) x. R ) = ( ( 2 x. R ) x. [_ ( I + 1 ) / n ]_ A ) )
363	217	recnd 9671	. . . . . . 7 |- ( ph -> ( [_ ( J + 1 ) / n ]_ A + [_ ( I + 1 ) / n ]_ A ) e. CC )
364	224	recnd 9671	. . . . . . 7 |- ( ph -> ( [_ ( I + 1 ) / n ]_ A - [_ ( J + 1 ) / n ]_ A ) e. CC )
365	363, 364, 283	adddird 9670	. . . . . 6 |- ( ph -> ( ( ( [_ ( J + 1 ) / n ]_ A + [_ ( I + 1 ) / n ]_ A ) + ( [_ ( I + 1 ) / n ]_ A - [_ ( J + 1 ) / n ]_ A ) ) x. R ) = ( ( ( [_ ( J + 1 ) / n ]_ A + [_ ( I + 1 ) / n ]_ A ) x. R ) + ( ( [_ ( I + 1 ) / n ]_ A - [_ ( J + 1 ) / n ]_ A ) x. R ) ) )
366	360, 362, 365	3eqtr3d 2472	. . . . 5 |- ( ph -> ( ( 2 x. R ) x. [_ ( I + 1 ) / n ]_ A ) = ( ( ( [_ ( J + 1 ) / n ]_ A + [_ ( I + 1 ) / n ]_ A ) x. R ) + ( ( [_ ( I + 1 ) / n ]_ A - [_ ( J + 1 ) / n ]_ A ) x. R ) ) )
367	354, 366	breqtrrd 4448	. . . 4 |- ( ph -> ( ( abs ` ( ( [_ ( J + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) - ( [_ ( I + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) ) ) + ( abs ` sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) x. sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) ) ) <_ ( ( 2 x. R ) x. [_ ( I + 1 ) / n ]_ A ) )
368	92, 159, 102, 216, 367	letrd 9794	. . 3 |- ( ph -> ( abs ` sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) ) <_ ( ( 2 x. R ) x. [_ ( I + 1 ) / n ]_ A ) )
369		2nn0 10888	. . . . . 6 |- 2 e. NN0
370		nn0ge0 10897	. . . . . 6 |- ( 2 e. NN0 -> 0 <_ 2 )
371	369, 370	mp1i 13	. . . . 5 |- ( ph -> 0 <_ 2 )
372		0red 9646	. . . . . 6 |- ( ph -> 0 e. RR )
373	126	absge0d 13499	. . . . . 6 |- ( ph -> 0 <_ ( abs ` sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) )
374	372, 261, 95, 373, 265	letrd 9794	. . . . 5 |- ( ph -> 0 <_ R )
375	94, 95, 371, 374	mulge0d 10192	. . . 4 |- ( ph -> 0 <_ ( 2 x. R ) )
376	4	nnrpd 11341	. . . . 5 |- ( ph -> ( I + 1 ) e. RR+ )
377		nfv 1752	. . . . . . . . 9 |- F/ n ( M <_ U /\ U <_ x )
378	307, 308, 105	nfbr 4466	. . . . . . . . 9 |- F/ n B <_ [_ U / n ]_ A
379	377, 378	nfim 1977	. . . . . . . 8 |- F/ n ( ( M <_ U /\ U <_ x ) -> B <_ [_ U / n ]_ A )
380	305, 379	nfral 2812	. . . . . . 7 |- F/ n A. x e. RR+ ( ( M <_ U /\ U <_ x ) -> B <_ [_ U / n ]_ A )
381		breq2 4425	. . . . . . . . . 10 |- ( n = U -> ( M <_ n <-> M <_ U ) )
382		breq1 4424	. . . . . . . . . 10 |- ( n = U -> ( n <_ x <-> U <_ x ) )
383	381, 382	anbi12d 716	. . . . . . . . 9 |- ( n = U -> ( ( M <_ n /\ n <_ x ) <-> ( M <_ U /\ U <_ x ) ) )
384	107	breq2d 4433	. . . . . . . . 9 |- ( n = U -> ( B <_ A <-> B <_ [_ U / n ]_ A ) )
385	383, 384	imbi12d 322	. . . . . . . 8 |- ( n = U -> ( ( ( M <_ n /\ n <_ x ) -> B <_ A ) <-> ( ( M <_ U /\ U <_ x ) -> B <_ [_ U / n ]_ A ) ) )
386	385	ralbidv 2865	. . . . . . 7 |- ( n = U -> ( A. x e. RR+ ( ( M <_ n /\ n <_ x ) -> B <_ A ) <-> A. x e. RR+ ( ( M <_ U /\ U <_ x ) -> B <_ [_ U / n ]_ A ) ) )
387	380, 386	rspc 3177	. . . . . 6 |- ( U e. RR+ -> ( A. n e. RR+ A. x e. RR+ ( ( M <_ n /\ n <_ x ) -> B <_ A ) -> A. x e. RR+ ( ( M <_ U /\ U <_ x ) -> B <_ [_ U / n ]_ A ) ) )
388	103, 303, 387	sylc 63	. . . . 5 |- ( ph -> A. x e. RR+ ( ( M <_ U /\ U <_ x ) -> B <_ [_ U / n ]_ A ) )
389	248, 249	jca 535	. . . . 5 |- ( ph -> ( M <_ U /\ U <_ ( I + 1 ) ) )
390		breq2 4425	. . . . . . . 8 |- ( x = ( I + 1 ) -> ( U <_ x <-> U <_ ( I + 1 ) ) )
391	390	anbi2d 709	. . . . . . 7 |- ( x = ( I + 1 ) -> ( ( M <_ U /\ U <_ x ) <-> ( M <_ U /\ U <_ ( I + 1 ) ) ) )
392		eqvisset 3090	. . . . . . . . . 10 |- ( x = ( I + 1 ) -> ( I + 1 ) e. _V )
393		eqtr3 2451	. . . . . . . . . . 11 |- ( ( x = ( I + 1 ) /\ n = ( I + 1 ) ) -> x = n )
394	393, 326	syl 17	. . . . . . . . . 10 |- ( ( x = ( I + 1 ) /\ n = ( I + 1 ) ) -> A = B )
395	392, 394	csbied 3423	. . . . . . . . 9 |- ( x = ( I + 1 ) -> [_ ( I + 1 ) / n ]_ A = B )
396	395	eqcomd 2431	. . . . . . . 8 |- ( x = ( I + 1 ) -> B = [_ ( I + 1 ) / n ]_ A )
397	396	breq1d 4431	. . . . . . 7 |- ( x = ( I + 1 ) -> ( B <_ [_ U / n ]_ A <-> [_ ( I + 1 ) / n ]_ A <_ [_ U / n ]_ A ) )
398	391, 397	imbi12d 322	. . . . . 6 |- ( x = ( I + 1 ) -> ( ( ( M <_ U /\ U <_ x ) -> B <_ [_ U / n ]_ A ) <-> ( ( M <_ U /\ U <_ ( I + 1 ) ) -> [_ ( I + 1 ) / n ]_ A <_ [_ U / n ]_ A ) ) )
399	398	rspcv 3179	. . . . 5 |- ( ( I + 1 ) e. RR+ -> ( A. x e. RR+ ( ( M <_ U /\ U <_ x ) -> B <_ [_ U / n ]_ A ) -> ( ( M <_ U /\ U <_ ( I + 1 ) ) -> [_ ( I + 1 ) / n ]_ A <_ [_ U / n ]_ A ) ) )
400	376, 388, 389, 399	syl3c 64	. . . 4 |- ( ph -> [_ ( I + 1 ) / n ]_ A <_ [_ U / n ]_ A )
401	101, 110, 96, 375, 400	lemul2ad 10549	. . 3 |- ( ph -> ( ( 2 x. R ) x. [_ ( I + 1 ) / n ]_ A ) <_ ( ( 2 x. R ) x. [_ U / n ]_ A ) )
402	92, 102, 111, 368, 401	letrd 9794	. 2 |- ( ph -> ( abs ` sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) ) <_ ( ( 2 x. R ) x. [_ U / n ]_ A ) )
403	91, 402	eqbrtrd 4442	1 |- ( ph -> ( abs ` ( ( seq 1 ( + , F ) ` J ) - ( seq 1 ( + , F ) ` I ) ) ) <_ ( ( 2 x. R ) x. [_ U / n ]_ A ) )

Syntax hints:   -> wi 4   <-> wb 188   /\ wa 371   /\ w3a 983   = wceq 1438   e. wcel 1869   =/= wne 2619   A.wral 2776   _Vcvv 3082   [_csb 3396   u. cun 3435   i^i cin 3436   (/)c0 3762   class class class wbr 4421   |-> cmpt 4480   ` cfv 5599  (class class class)co 6303   Fincfn 7575   CCcc 9539   RRcr 9540   0cc0 9541   1c1 9542   + caddc 9544   x. cmul 9546   +oocpnf 9674   <_ cle 9678   - cmin 9862   NNcn 10611   2c2 10661   NN0cn0 10871   ZZcz 10939   ZZ>=cuz 11161   RR+crp 11304   [,)cico 11639   ...cfz 11786  ..^cfzo 11917   seqcseq 12214   abscabs 13291   ~~> r crli 13542   sum_csu 13745   Basecbs 15114   0gc0g 15331   ZRHomczrh 19063  ℤ/nℤczn 19066  DChrcdchr 24152