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

Step	Hyp	Ref	Expression
1		fzodisj 10894	. . . . . . . . 9 |- ( ( 1..^ ( I + 1 ) ) i^i ( ( I + 1 )..^ ( J + 1 ) ) ) = (/)
2	1	a1i 12	. . . . . . . 8 |- ( ph -> ( ( 1..^ ( I + 1 ) ) i^i ( ( I + 1 )..^ ( J + 1 ) ) ) = (/) )
3		dchrisumlem2.4	. . . . . . . . . . . 12 |- ( ph -> I e. NN )
4	3	peano2nnd 9758	. . . . . . . . . . 11 |- ( ph -> ( I + 1 ) e. NN )
5		nnuz 10258	. . . . . . . . . . 11 |- NN = ( ZZ>= ` 1 )
6	4, 5	syl6eleq 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 ) ) )
9	7, 8	syl 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 ) ) ) )
11	6, 9, 10	sylanbrc 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 ) ) ) )
13	11, 12	syl 17	. . . . . . . 8 |- ( ph -> ( 1..^ ( J + 1 ) ) = ( ( 1..^ ( I + 1 ) ) u. ( ( I + 1 )..^ ( J + 1 ) ) ) )
14		fzofi 11030	. . . . . . . . 9 |- ( 1..^ ( J + 1 ) ) e. Fin
15	14	a1i 12	. . . . . . . 8 |- ( ph -> ( 1..^ ( J + 1 ) ) e. Fin )
16		elfzouz 10873	. . . . . . . . . 10 |- ( i e. ( 1..^ ( J + 1 ) ) -> i e. ( ZZ>= ` 1 ) )
17	16, 5	syl6eleqr 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 )
23	22	adantr 453	. . . . . . . . . . 11 |- ( ( ph /\ i e. NN ) -> X e. D )
24		nnz 10040	. . . . . . . . . . . 12 |- ( i e. NN -> i e. ZZ )
25	24	adantl 454	. . . . . . . . . . 11 |- ( ( ph /\ i e. NN ) -> i e. ZZ )
26	18, 19, 20, 21, 23, 25	dchrzrhcl 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 ) )
37	19, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36	dchrisumlema 20631	. . . . . . . . . . . . . 14 |- ( ph -> ( ( i e. RR+ -> [_ i / n ]_ A e. RR ) /\ ( i e. ( M [,) +oo ) -> 0 <_ [_ i / n ]_ A ) ) )
38	37	simpld 447	. . . . . . . . . . . . 13 |- ( ph -> ( i e. RR+ -> [_ i / n ]_ A e. RR ) )
39	27, 38	syl5 30	. . . . . . . . . . . 12 |- ( ph -> ( i e. NN -> [_ i / n ]_ A e. RR ) )
40	39	imp 420	. . . . . . . . . . 11 |- ( ( ph /\ i e. NN ) -> [_ i / n ]_ A e. RR )
41	40	recnd 8856	. . . . . . . . . 10 |- ( ( ph /\ i e. NN ) -> [_ i / n ]_ A e. CC )
42	26, 41	mulcld 8850	. . . . . . . . 9 |- ( ( ph /\ i e. NN ) -> ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) e. CC )
43	17, 42	sylan2 462	. . . . . . . 8 |- ( ( ph /\ i e. ( 1..^ ( J + 1 ) ) ) -> ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) e. CC )
44	2, 13, 15, 43	fsumsplit 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 ) ) )
47	7, 45, 46	3syl 20	. . . . . . . 8 |- ( ph -> ( 1 ... J ) = ( 1..^ ( J + 1 ) ) )
48	47	sumeq1d 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 ) )
49	3	nnzd 10111	. . . . . . . . . 10 |- ( ph -> I e. ZZ )
50		fzval3 10905	. . . . . . . . . 10 |- ( I e. ZZ -> ( 1 ... I ) = ( 1..^ ( I + 1 ) ) )
51	49, 50	syl 17	. . . . . . . . 9 |- ( ph -> ( 1 ... I ) = ( 1..^ ( I + 1 ) ) )
52	51	sumeq1d 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 ) )
53	52	oveq1d 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 ) ) )
54	44, 48, 53	3eqtr4d 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.
60	57	nfcsb1 3113	. . . . . . . . . . 11 |- F/_ n [_ i / n ]_ A
61	58, 59, 60	nfov 5842	. . . . . . . . . 10 |- F/_ n ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A )
62		fveq2 5485	. . . . . . . . . . . 12 |- ( n = i -> ( L ` n ) = ( L ` i ) )
63	62	fveq2d 5489	. . . . . . . . . . 11 |- ( n = i -> ( X ` ( L ` n ) ) = ( X ` ( L ` i ) ) )
64		csbeq1a 3090	. . . . . . . . . . 11 |- ( n = i -> A = [_ i / n ]_ A )
65	63, 64	oveq12d 5837	. . . . . . . . . 10 |- ( n = i -> ( ( X ` ( L ` n ) ) x. A ) = ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) )
66	57, 61, 65, 36	fvmptf 5577	. . . . . . . . 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 645	. . . . . . . 8 |- ( ( ph /\ i e. NN ) -> ( F ` i ) = ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) )
68	55, 67	sylan2 462	. . . . . . 7 |- ( ( ph /\ i e. ( 1 ... J ) ) -> ( F ` i ) = ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) )
69	3, 5	syl6eleq 2374	. . . . . . . 8 |- ( ph -> I e. ( ZZ>= ` 1 ) )
70		uztrn 10239	. . . . . . . 8 |- ( ( J e. ( ZZ>= ` I ) /\ I e. ( ZZ>= ` 1 ) ) -> J e. ( ZZ>= ` 1 ) )
71	7, 69, 70	syl2anc 645	. . . . . . 7 |- ( ph -> J e. ( ZZ>= ` 1 ) )
72	55, 42	sylan2 462	. . . . . . 7 |- ( ( ph /\ i e. ( 1 ... J ) ) -> ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) e. CC )
73	68, 71, 72	fsumser 12197	. . . . . 6 |- ( ph -> sum_ i e. ( 1 ... J ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) = ( seq 1 ( + , F ) ` J ) )
74	54, 73	eqtr3d 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 )
76	75, 67	sylan2 462	. . . . . 6 |- ( ( ph /\ i e. ( 1 ... I ) ) -> ( F ` i ) = ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) )
77	75, 42	sylan2 462	. . . . . 6 |- ( ( ph /\ i e. ( 1 ... I ) ) -> ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) e. CC )
78	76, 69, 77	fsumser 12197	. . . . 5 |- ( ph -> sum_ i e. ( 1 ... I ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) = ( seq 1 ( + , F ) ` I ) )
79	74, 78	oveq12d 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 )
81	80, 77	fsumcl 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
83	82	a1i 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 ) ) )
85	84, 13	syl5sseqr 3228	. . . . . . . 8 |- ( ph -> ( ( I + 1 )..^ ( J + 1 ) ) C_ ( 1..^ ( J + 1 ) ) )
86	85	sselda 3181	. . . . . . 7 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> i e. ( 1..^ ( J + 1 ) ) )
87	86, 43	syldan 458	. . . . . 6 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) e. CC )
88	83, 87	fsumcl 12200	. . . . 5 |- ( ph -> sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) e. CC )
89	81, 88	pncan2d 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 ) )
90	79, 89	eqtr3d 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 ) )
91	90	fveq2d 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 ) ) )
92	88	abscld 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
94	93	a1i 12	. . . . 5 |- ( ph -> 2 e. RR )
95		dchrisum.9	. . . . 5 |- ( ph -> R e. RR )
96	94, 95	remulcld 8858	. . . 4 |- ( ph -> ( 2 x. R ) e. RR )
97	40	ralrimiva 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 )
99	98	eleq1d 2350	. . . . . 6 |- ( i = ( I + 1 ) -> ( [_ i / n ]_ A e. RR <-> [_ ( I + 1 ) / n ]_ A e. RR ) )
100	99	rspcv 2881	. . . . 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 58	. . . 4 |- ( ph -> [_ ( I + 1 ) / n ]_ A e. RR )
102	96, 101	remulcld 8858	. . 3 |- ( ph -> ( ( 2 x. R ) x. [_ ( I + 1 ) / n ]_ A ) e. RR )
103		dchrisumlem2.1	. . . . 5 |- ( ph -> U e. RR+ )
104	33	ralrimiva 2627	. . . . 5 |- ( ph -> A. n e. RR+ A e. RR )
105		nfcsb1v 3114	. . . . . . 7 |- F/_ n [_ U / n ]_ A
106	105	nfel1 2430	. . . . . 6 |- F/ n [_ U / n ]_ A e. RR
107		csbeq1a 3090	. . . . . . 7 |- ( n = U -> A = [_ U / n ]_ A )
108	107	eleq1d 2350	. . . . . 6 |- ( n = U -> ( A e. RR <-> [_ U / n ]_ A e. RR ) )
109	106, 108	rspc 2879	. . . . 5 |- ( U e. RR+ -> ( A. n e. RR+ A e. RR -> [_ U / n ]_ A e. RR ) )
110	103, 104, 109	sylc 58	. . . 4 |- ( ph -> [_ U / n ]_ A e. RR )
111	96, 110	remulcld 8858	. . 3 |- ( ph -> ( ( 2 x. R ) x. [_ U / n ]_ A ) e. RR )
112	71, 5	syl6eleqr 2375	. . . . . . . . . . . 12 |- ( ph -> J e. NN )
113	112	peano2nnd 9758	. . . . . . . . . . 11 |- ( ph -> ( J + 1 ) e. NN )
114	113	nnrpd 10384	. . . . . . . . . 10 |- ( ph -> ( J + 1 ) e. RR+ )
115	19, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36	dchrisumlema 20631	. . . . . . . . . . 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 447	. . . . . . . . . 10 |- ( ph -> ( ( J + 1 ) e. RR+ -> [_ ( J + 1 ) / n ]_ A e. RR ) )
117	114, 116	mpd 16	. . . . . . . . 9 |- ( ph -> [_ ( J + 1 ) / n ]_ A e. RR )
118	117	recnd 8856	. . . . . . . 8 |- ( ph -> [_ ( J + 1 ) / n ]_ A e. CC )
119		fzofi 11030	. . . . . . . . . 10 |- ( 0..^ ( J + 1 ) ) e. Fin
120	119	a1i 12	. . . . . . . . 9 |- ( ph -> ( 0..^ ( J + 1 ) ) e. Fin )
121		elfzoelz 10869	. . . . . . . . . 10 |- ( n e. ( 0..^ ( J + 1 ) ) -> n e. ZZ )
122	22	adantr 453	. . . . . . . . . . 11 |- ( ( ph /\ n e. ZZ ) -> X e. D )
123		simpr 449	. . . . . . . . . . 11 |- ( ( ph /\ n e. ZZ ) -> n e. ZZ )
124	18, 19, 20, 21, 122, 123	dchrzrhcl 20478	. . . . . . . . . 10 |- ( ( ph /\ n e. ZZ ) -> ( X ` ( L ` n ) ) e. CC )
125	121, 124	sylan2 462	. . . . . . . . 9 |- ( ( ph /\ n e. ( 0..^ ( J + 1 ) ) ) -> ( X ` ( L ` n ) ) e. CC )
126	120, 125	fsumcl 12200	. . . . . . . 8 |- ( ph -> sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) e. CC )
127	118, 126	mulcld 8850	. . . . . . 7 |- ( ph -> ( [_ ( J + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) e. CC )
128	101	recnd 8856	. . . . . . . 8 |- ( ph -> [_ ( I + 1 ) / n ]_ A e. CC )
129		fzofi 11030	. . . . . . . . . 10 |- ( 0..^ ( I + 1 ) ) e. Fin
130	129	a1i 12	. . . . . . . . 9 |- ( ph -> ( 0..^ ( I + 1 ) ) e. Fin )
131		elfzoelz 10869	. . . . . . . . . 10 |- ( n e. ( 0..^ ( I + 1 ) ) -> n e. ZZ )
132	131, 124	sylan2 462	. . . . . . . . 9 |- ( ( ph /\ n e. ( 0..^ ( I + 1 ) ) ) -> ( X ` ( L ` n ) ) e. CC )
133	130, 132	fsumcl 12200	. . . . . . . 8 |- ( ph -> sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) e. CC )
134	128, 133	mulcld 8850	. . . . . . 7 |- ( ph -> ( [_ ( I + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) e. CC )
135	127, 134	subcld 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 )
136	135	abscld 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 )
137	86, 17	syl 17	. . . . . . . 8 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> i e. NN )
138		peano2nn 9753	. . . . . . . . . . . . 13 |- ( i e. NN -> ( i + 1 ) e. NN )
139	138	nnrpd 10384	. . . . . . . . . . . 12 |- ( i e. NN -> ( i + 1 ) e. RR+ )
140		nfcsb1v 3114	. . . . . . . . . . . . . . 15 |- F/_ n [_ ( i + 1 ) / n ]_ A
141	140	nfel1 2430	. . . . . . . . . . . . . 14 |- F/ n [_ ( i + 1 ) / n ]_ A e. RR
142		csbeq1a 3090	. . . . . . . . . . . . . . 15 |- ( n = ( i + 1 ) -> A = [_ ( i + 1 ) / n ]_ A )
143	142	eleq1d 2350	. . . . . . . . . . . . . 14 |- ( n = ( i + 1 ) -> ( A e. RR <-> [_ ( i + 1 ) / n ]_ A e. RR ) )
144	141, 143	rspc 2879	. . . . . . . . . . . . 13 |- ( ( i + 1 ) e. RR+ -> ( A. n e. RR+ A e. RR -> [_ ( i + 1 ) / n ]_ A e. RR ) )
145	144	impcom 421	. . . . . . . . . . . 12 |- ( ( A. n e. RR+ A e. RR /\ ( i + 1 ) e. RR+ ) -> [_ ( i + 1 ) / n ]_ A e. RR )
146	104, 139, 145	syl2an 465	. . . . . . . . . . 11 |- ( ( ph /\ i e. NN ) -> [_ ( i + 1 ) / n ]_ A e. RR )
147	146, 40	resubcld 9206	. . . . . . . . . 10 |- ( ( ph /\ i e. NN ) -> ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) e. RR )
148	147	recnd 8856	. . . . . . . . 9 |- ( ( ph /\ i e. NN ) -> ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) e. CC )
149		fzofi 11030	. . . . . . . . . . . 12 |- ( 0..^ ( i + 1 ) ) e. Fin
150	149	a1i 12	. . . . . . . . . . 11 |- ( ph -> ( 0..^ ( i + 1 ) ) e. Fin )
151		elfzoelz 10869	. . . . . . . . . . . 12 |- ( n e. ( 0..^ ( i + 1 ) ) -> n e. ZZ )
152	151, 124	sylan2 462	. . . . . . . . . . 11 |- ( ( ph /\ n e. ( 0..^ ( i + 1 ) ) ) -> ( X ` ( L ` n ) ) e. CC )
153	150, 152	fsumcl 12200	. . . . . . . . . 10 |- ( ph -> sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) e. CC )
154	153	adantr 453	. . . . . . . . 9 |- ( ( ph /\ i e. NN ) -> sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) e. CC )
155	148, 154	mulcld 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 )
156	137, 155	syldan 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 )
157	83, 156	fsumcl 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 )
158	157	abscld 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 )
159	136, 158	readdcld 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 )
160	26, 41	mulcomd 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 )
162	161	adantl 454	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. NN ) -> i e. NN0 )
163		nn0uz 10257	. . . . . . . . . . . . . . 15 |- NN0 = ( ZZ>= ` 0 )
164	162, 163	syl6eleq 2374	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. NN ) -> i e. ( ZZ>= ` 0 ) )
165		elfzelz 10792	. . . . . . . . . . . . . . 15 |- ( n e. ( 0 ... i ) -> n e. ZZ )
166	124	adantlr 698	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. NN ) /\ n e. ZZ ) -> ( X ` ( L ` n ) ) e. CC )
167	165, 166	sylan2 462	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. NN ) /\ n e. ( 0 ... i ) ) -> ( X ` ( L ` n ) ) e. CC )
168	164, 167, 63	fzosump1 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 ) ) ) )
169	168	oveq1d 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
171	170	a1i 12	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. NN ) -> ( 0..^ i ) e. Fin )
172		elfzoelz 10869	. . . . . . . . . . . . . . 15 |- ( n e. ( 0..^ i ) -> n e. ZZ )
173	172, 166	sylan2 462	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. NN ) /\ n e. ( 0..^ i ) ) -> ( X ` ( L ` n ) ) e. CC )
174	171, 173	fsumcl 12200	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. NN ) -> sum_ n e. ( 0..^ i ) ( X ` ( L ` n ) ) e. CC )
175	174, 26	pncan2d 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 ) ) )
176	169, 175	eqtr2d 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 ) ) ) )
177	176	oveq2d 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 ) ) ) ) )
178	160, 177	eqtrd 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 ) ) ) ) )
179	137, 178	syldan 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 ) ) ) ) )
180	179	sumeq2dv 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 ) )
183	182	sumeq1d 12168	. . . . . . . . 9 |- ( k = i -> sum_ n e. ( 0..^ k ) ( X ` ( L ` n ) ) = sum_ n e. ( 0..^ i ) ( X ` ( L ` n ) ) )
184	181, 183	jca 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 ) ) )
187	186	sumeq1d 12168	. . . . . . . . 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 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 ) ) )
191	190	sumeq1d 12168	. . . . . . . . 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 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 ) ) )
195	194	sumeq1d 12168	. . . . . . . . 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 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 ) ) )
198	5	uztrn2 10240	. . . . . . . . . 10 |- ( ( ( I + 1 ) e. NN /\ k e. ( ZZ>= ` ( I + 1 ) ) ) -> k e. NN )
199	4, 197, 198	syl2an 465	. . . . . . . . 9 |- ( ( ph /\ k e. ( ( I + 1 ) ... ( J + 1 ) ) ) -> k e. NN )
200	41	ralrimiva 2627	. . . . . . . . . 10 |- ( ph -> A. i e. NN [_ i / n ]_ A e. CC )
201		csbeq1 3085	. . . . . . . . . . . 12 |- ( i = k -> [_ i / n ]_ A = [_ k / n ]_ A )
202	201	eleq1d 2350	. . . . . . . . . . 11 |- ( i = k -> ( [_ i / n ]_ A e. CC <-> [_ k / n ]_ A e. CC ) )
203	202	rspccva 2884	. . . . . . . . . 10 |- ( ( A. i e. NN [_ i / n ]_ A e. CC /\ k e. NN ) -> [_ k / n ]_ A e. CC )
204	200, 203	sylan 459	. . . . . . . . 9 |- ( ( ph /\ k e. NN ) -> [_ k / n ]_ A e. CC )
205	199, 204	syldan 458	. . . . . . . 8 |- ( ( ph /\ k e. ( ( I + 1 ) ... ( J + 1 ) ) ) -> [_ k / n ]_ A e. CC )
206		fzofi 11030	. . . . . . . . . . 11 |- ( 0..^ k ) e. Fin
207	206	a1i 12	. . . . . . . . . 10 |- ( ph -> ( 0..^ k ) e. Fin )
208		elfzoelz 10869	. . . . . . . . . . 11 |- ( n e. ( 0..^ k ) -> n e. ZZ )
209	208, 124	sylan2 462	. . . . . . . . . 10 |- ( ( ph /\ n e. ( 0..^ k ) ) -> ( X ` ( L ` n ) ) e. CC )
210	207, 209	fsumcl 12200	. . . . . . . . 9 |- ( ph -> sum_ n e. ( 0..^ k ) ( X ` ( L ` n ) ) e. CC )
211	210	adantr 453	. . . . . . . 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 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 ) ) ) ) )
213	180, 212	eqtrd 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 ) ) ) ) )
214	213	fveq2d 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 ) ) ) ) ) )
215	135, 157	abs2dif2d 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 ) ) ) ) ) )
216	214, 215	eqbrtrd 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 ) ) ) ) ) )
217	117, 101	readdcld 8857	. . . . . . 7 |- ( ph -> ( [_ ( J + 1 ) / n ]_ A + [_ ( I + 1 ) / n ]_ A ) e. RR )
218	217, 95	remulcld 8858	. . . . . 6 |- ( ph -> ( ( [_ ( J + 1 ) / n ]_ A + [_ ( I + 1 ) / n ]_ A ) x. R ) e. RR )
219	181, 185, 189, 193, 9, 205	fsumtscopo 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 ) )
220	137, 40	syldan 458	. . . . . . . . . 10 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> [_ i / n ]_ A e. RR )
221	137, 146	syldan 458	. . . . . . . . . 10 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> [_ ( i + 1 ) / n ]_ A e. RR )
222	220, 221	resubcld 9206	. . . . . . . . 9 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) e. RR )
223	83, 222	fsumrecl 12201	. . . . . . . 8 |- ( ph -> sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) e. RR )
224	219, 223	eqeltrrd 2359	. . . . . . 7 |- ( ph -> ( [_ ( I + 1 ) / n ]_ A - [_ ( J + 1 ) / n ]_ A ) e. RR )
225	224, 95	remulcld 8858	. . . . . 6 |- ( ph -> ( ( [_ ( I + 1 ) / n ]_ A - [_ ( J + 1 ) / n ]_ A ) x. R ) e. RR )
226	127	abscld 11912	. . . . . . . 8 |- ( ph -> ( abs ` ( [_ ( J + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) ) e. RR )
227	134	abscld 11912	. . . . . . . 8 |- ( ph -> ( abs ` ( [_ ( I + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) ) e. RR )
228	226, 227	readdcld 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 )
229	127, 134	abs2dif2d 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 ) ) ) ) ) )
230	117, 95	remulcld 8858	. . . . . . . . 9 |- ( ph -> ( [_ ( J + 1 ) / n ]_ A x. R ) e. RR )
231	101, 95	remulcld 8858	. . . . . . . . 9 |- ( ph -> ( [_ ( I + 1 ) / n ]_ A x. R ) e. RR )
232	118, 126	absmuld 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 )
234	233	adantl 454	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> i e. RR )
235		eluzle 10235	. . . . . . . . . . . . . . . . . . 19 |- ( i e. ( ZZ>= ` M ) -> M <_ i )
236	235	adantl 454	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> M <_ i )
237	32	nnred 9756	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> M e. RR )
238	237	adantr 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 ) ) )
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 893	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> i e. ( M [,) +oo ) )
242	241	ex 425	. . . . . . . . . . . . . . . 16 |- ( ph -> ( i e. ( ZZ>= ` M ) -> i e. ( M [,) +oo ) ) )
243	242	ssrdv 3186	. . . . . . . . . . . . . . 15 |- ( ph -> ( ZZ>= ` M ) C_ ( M [,) +oo ) )
244	32	nnzd 10111	. . . . . . . . . . . . . . . . 17 |- ( ph -> M e. ZZ )
245	49	peano2zd 10115	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( I + 1 ) e. ZZ )
246	103	rpred 10385	. . . . . . . . . . . . . . . . . 18 |- ( ph -> U e. RR )
247	4	nnred 9756	. . . . . . . . . . . . . . . . . 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 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 ) ) )
252	244, 245, 250, 251	syl3anbrc 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 ) )
254	9, 252, 253	syl2anc 645	. . . . . . . . . . . . . . 15 |- ( ph -> ( J + 1 ) e. ( ZZ>= ` M ) )
255	243, 254	sseldd 3182	. . . . . . . . . . . . . 14 |- ( ph -> ( J + 1 ) e. ( M [,) +oo ) )
256	115	simprd 451	. . . . . . . . . . . . . 14 |- ( ph -> ( ( J + 1 ) e. ( M [,) +oo ) -> 0 <_ [_ ( J + 1 ) / n ]_ A ) )
257	255, 256	mpd 16	. . . . . . . . . . . . 13 |- ( ph -> 0 <_ [_ ( J + 1 ) / n ]_ A )
258	117, 257	absidd 11899	. . . . . . . . . . . 12 |- ( ph -> ( abs ` [_ ( J + 1 ) / n ]_ A ) = [_ ( J + 1 ) / n ]_ A )
259	258	oveq1d 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 ) ) ) ) )
260	232, 259	eqtrd 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 ) ) ) ) )
261	126	abscld 11912	. . . . . . . . . . 11 |- ( ph -> ( abs ` sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) e. RR )
262	113	nnnn0d 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 )
264	19, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36, 95, 263	dchrisumlem1 20632	. . . . . . . . . . . 12 |- ( ( ph /\ ( J + 1 ) e. NN0 ) -> ( abs ` sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) <_ R )
265	262, 264	mpdan 652	. . . . . . . . . . 11 |- ( ph -> ( abs ` sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) <_ R )
266	261, 95, 117, 257, 265	lemul2ad 9692	. . . . . . . . . 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 4044	. . . . . . . . 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 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 ) ) ) ) )
269	243, 252	sseldd 3182	. . . . . . . . . . . . . 14 |- ( ph -> ( I + 1 ) e. ( M [,) +oo ) )
270	19, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36	dchrisumlema 20631	. . . . . . . . . . . . . . 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 451	. . . . . . . . . . . . . 14 |- ( ph -> ( ( I + 1 ) e. ( M [,) +oo ) -> 0 <_ [_ ( I + 1 ) / n ]_ A ) )
272	269, 271	mpd 16	. . . . . . . . . . . . 13 |- ( ph -> 0 <_ [_ ( I + 1 ) / n ]_ A )
273	101, 272	absidd 11899	. . . . . . . . . . . 12 |- ( ph -> ( abs ` [_ ( I + 1 ) / n ]_ A ) = [_ ( I + 1 ) / n ]_ A )
274	273	oveq1d 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 ) ) ) ) )
275	268, 274	eqtrd 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 ) ) ) ) )
276	133	abscld 11912	. . . . . . . . . . 11 |- ( ph -> ( abs ` sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) e. RR )
277	4	nnnn0d 10013	. . . . . . . . . . . 12 |- ( ph -> ( I + 1 ) e. NN0 )
278	19, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36, 95, 263	dchrisumlem1 20632	. . . . . . . . . . . 12 |- ( ( ph /\ ( I + 1 ) e. NN0 ) -> ( abs ` sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) <_ R )
279	277, 278	mpdan 652	. . . . . . . . . . 11 |- ( ph -> ( abs ` sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) <_ R )
280	276, 95, 101, 272, 279	lemul2ad 9692	. . . . . . . . . 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 4044	. . . . . . . . 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 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 ) ) )
283	95	recnd 8856	. . . . . . . . 9 |- ( ph -> R e. CC )
284	118, 128, 283	adddird 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 ) ) )
285	282, 284	breqtrrd 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 ) )
286	136, 228, 218, 229, 285	letrd 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 ) )
287	156	abscld 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 )
288	83, 287	fsumrecl 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 )
289	83, 156	fsumabs 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 ) ) ) ) )
290	95	adantr 453	. . . . . . . . . 10 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> R e. RR )
291	222, 290	remulcld 8858	. . . . . . . . 9 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) x. R ) e. RR )
292	137, 148	syldan 458	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) e. CC )
293	153	adantr 453	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) e. CC )
294	292, 293	absmuld 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 ) )
297	295, 252, 296	syl2anr 466	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> i e. ( ZZ>= ` M ) )
298	5	uztrn2 10240	. . . . . . . . . . . . . . . . 17 |- ( ( M e. NN /\ i e. ( ZZ>= ` M ) ) -> i e. NN )
299	32, 298	sylan 459	. . . . . . . . . . . . . . . 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 10384	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> i e. RR+ )
302	34	3expia 1158	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) ) -> ( ( M <_ n /\ n <_ x ) -> B <_ A ) )
303	302	ralrimivva 2636	. . . . . . . . . . . . . . . . 17 |- ( ph -> A. n e. RR+ A. x e. RR+ ( ( M <_ n /\ n <_ x ) -> B <_ A ) )
304	303	adantr 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 <_
309	307, 308, 60	nfbr 4068	. . . . . . . . . . . . . . . . . . 19 |- F/ n B <_ [_ i / n ]_ A
310	306, 309	nfim 1773	. . . . . . . . . . . . . . . . . 18 |- F/ n ( ( M <_ i /\ i <_ x ) -> B <_ [_ i / n ]_ A )
311	305, 310	nfral 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 ) )
314	312, 313	anbi12d 694	. . . . . . . . . . . . . . . . . . 19 |- ( n = i -> ( ( M <_ n /\ n <_ x ) <-> ( M <_ i /\ i <_ x ) ) )
315	64	breq2d 4036	. . . . . . . . . . . . . . . . . . 19 |- ( n = i -> ( B <_ A <-> B <_ [_ i / n ]_ A ) )
316	314, 315	imbi12d 313	. . . . . . . . . . . . . . . . . 18 |- ( n = i -> ( ( ( M <_ n /\ n <_ x ) -> B <_ A ) <-> ( ( M <_ i /\ i <_ x ) -> B <_ [_ i / n ]_ A ) ) )
317	316	ralbidv 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 ) ) )
318	311, 317	rspc 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 ) ) )
319	301, 304, 318	sylc 58	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> A. x e. RR+ ( ( M <_ i /\ i <_ x ) -> B <_ [_ i / n ]_ A ) )
320	234	lep1d 9683	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> i <_ ( i + 1 ) )
321	236, 320	jca 520	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> ( M <_ i /\ i <_ ( i + 1 ) ) )
322		breq2 4028	. . . . . . . . . . . . . . . . . 18 |- ( x = ( i + 1 ) -> ( i <_ x <-> i <_ ( i + 1 ) ) )
323	322	anbi2d 687	. . . . . . . . . . . . . . . . 17 |- ( x = ( i + 1 ) -> ( ( M <_ i /\ i <_ x ) <-> ( M <_ i /\ i <_ ( i + 1 ) ) ) )
324		ovex 5844	. . . . . . . . . . . . . . . . . . . . 21 |- ( i + 1 ) e. _V
325	324	a1i 12	. . . . . . . . . . . . . . . . . . . 20 |- ( x = ( i + 1 ) -> ( i + 1 ) e. _V )
326		eqtr3 2303	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( x = ( i + 1 ) /\ n = ( i + 1 ) ) -> x = n )
327	31	eqcoms 2287	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = n -> A = B )
328	326, 327	syl 17	. . . . . . . . . . . . . . . . . . . 20 |- ( ( x = ( i + 1 ) /\ n = ( i + 1 ) ) -> A = B )
329	325, 328	csbied 3124	. . . . . . . . . . . . . . . . . . 19 |- ( x = ( i + 1 ) -> [_ ( i + 1 ) / n ]_ A = B )
330	329	eqcomd 2289	. . . . . . . . . . . . . . . . . 18 |- ( x = ( i + 1 ) -> B = [_ ( i + 1 ) / n ]_ A )
331	330	breq1d 4034	. . . . . . . . . . . . . . . . 17 |- ( x = ( i + 1 ) -> ( B <_ [_ i / n ]_ A <-> [_ ( i + 1 ) / n ]_ A <_ [_ i / n ]_ A ) )
332	323, 331	imbi12d 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 ) ) )
333	332	rspcv 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 ) ) )
334	300, 319, 321, 333	syl3c 59	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> [_ ( i + 1 ) / n ]_ A <_ [_ i / n ]_ A )
335	297, 334	syldan 458	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> [_ ( i + 1 ) / n ]_ A <_ [_ i / n ]_ A )
336	221, 220, 335	abssuble0d 11909	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( abs ` ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) ) = ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) )
337	336	oveq1d 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 ) ) ) ) )
338	294, 337	eqtrd 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 ) ) ) ) )
339	293	abscld 11912	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( abs ` sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) e. RR )
340	220, 221	subge0d 9357	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( 0 <_ ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) <-> [_ ( i + 1 ) / n ]_ A <_ [_ i / n ]_ A ) )
341	335, 340	mpbird 225	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> 0 <_ ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) )
342	137	peano2nnd 9758	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( i + 1 ) e. NN )
343	342	nnnn0d 10013	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( i + 1 ) e. NN0 )
344	19, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36, 95, 263	dchrisumlem1 20632	. . . . . . . . . . . 12 |- ( ( ph /\ ( i + 1 ) e. NN0 ) -> ( abs ` sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) <_ R )
345	343, 344	syldan 458	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( abs ` sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) <_ R )
346	339, 290, 222, 341, 345	lemul2ad 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 ) )
347	338, 346	eqbrtrd 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 ) )
348	83, 287, 291, 347	fsumle 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 ) )
349	222	recnd 8856	. . . . . . . . . 10 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) e. CC )
350	83, 283, 349	fsummulc1 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 ) )
351	219	oveq1d 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 ) )
352	350, 351	eqtr3d 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 ) )
353	348, 352	breqtrd 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 ) )
354	158, 288, 225, 289, 353	letrd 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 ) )
355	136, 158, 218, 225, 286, 354	le2addd 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 ) ) )
356	128	2timesd 9949	. . . . . . . 8 |- ( ph -> ( 2 x. [_ ( I + 1 ) / n ]_ A ) = ( [_ ( I + 1 ) / n ]_ A + [_ ( I + 1 ) / n ]_ A ) )
357	128, 118, 128	ppncand 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 ) )
358	128, 118	addcomd 9009	. . . . . . . . 9 |- ( ph -> ( [_ ( I + 1 ) / n ]_ A + [_ ( J + 1 ) / n ]_ A ) = ( [_ ( J + 1 ) / n ]_ A + [_ ( I + 1 ) / n ]_ A ) )
359	358	oveq1d 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 ) ) )
360	356, 357, 359	3eqtr2d 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 ) ) )
361	360	oveq1d 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
363	362	a1i 12	. . . . . . 7 |- ( ph -> 2 e. CC )
364	363, 128, 283	mul32d 9017	. . . . . 6 |- ( ph -> ( ( 2 x. [_ ( I + 1 ) / n ]_ A ) x. R ) = ( ( 2 x. R ) x. [_ ( I + 1 ) / n ]_ A ) )
365	217	recnd 8856	. . . . . . 7 |- ( ph -> ( [_ ( J + 1 ) / n ]_ A + [_ ( I + 1 ) / n ]_ A ) e. CC )
366	224	recnd 8856	. . . . . . 7 |- ( ph -> ( [_ ( I + 1 ) / n ]_ A - [_ ( J + 1 ) / n ]_ A ) e. CC )
367	365, 366, 283	adddird 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 ) ) )
368	361, 364, 367	3eqtr3d 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 ) ) )
369	355, 368	breqtrrd 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 ) )
370	92, 159, 102, 216, 369	letrd 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 )
373	371, 372	mp1i 13	. . . . 5 |- ( ph -> 0 <_ 2 )
374		0re 8833	. . . . . . 7 |- 0 e. RR
375	374	a1i 12	. . . . . 6 |- ( ph -> 0 e. RR )
376	126	absge0d 11920	. . . . . 6 |- ( ph -> 0 <_ ( abs ` sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) )
377	375, 261, 95, 376, 265	letrd 8968	. . . . 5 |- ( ph -> 0 <_ R )
378	94, 95, 373, 377	mulge0d 9344	. . . 4 |- ( ph -> 0 <_ ( 2 x. R ) )
379	4	nnrpd 10384	. . . . 5 |- ( ph -> ( I + 1 ) e. RR+ )
380		nfv 1610	. . . . . . . . 9 |- F/ n ( M <_ U /\ U <_ x )
381	307, 308, 105	nfbr 4068	. . . . . . . . 9 |- F/ n B <_ [_ U / n ]_ A
382	380, 381	nfim 1773	. . . . . . . 8 |- F/ n ( ( M <_ U /\ U <_ x ) -> B <_ [_ U / n ]_ A )
383	305, 382	nfral 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 ) )
386	384, 385	anbi12d 694	. . . . . . . . 9 |- ( n = U -> ( ( M <_ n /\ n <_ x ) <-> ( M <_ U /\ U <_ x ) ) )
387	107	breq2d 4036	. . . . . . . . 9 |- ( n = U -> ( B <_ A <-> B <_ [_ U / n ]_ A ) )
388	386, 387	imbi12d 313	. . . . . . . 8 |- ( n = U -> ( ( ( M <_ n /\ n <_ x ) -> B <_ A ) <-> ( ( M <_ U /\ U <_ x ) -> B <_ [_ U / n ]_ A ) ) )
389	388	ralbidv 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 ) ) )
390	383, 389	rspc 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 ) ) )
391	103, 303, 390	sylc 58	. . . . 5 |- ( ph -> A. x e. RR+ ( ( M <_ U /\ U <_ x ) -> B <_ [_ U / n ]_ A ) )
392	248, 249	jca 520	. . . . 5 |- ( ph -> ( M <_ U /\ U <_ ( I + 1 ) ) )
393		breq2 4028	. . . . . . . 8 |- ( x = ( I + 1 ) -> ( U <_ x <-> U <_ ( I + 1 ) ) )
394	393	anbi2d 687	. . . . . . 7 |- ( x = ( I + 1 ) -> ( ( M <_ U /\ U <_ x ) <-> ( M <_ U /\ U <_ ( I + 1 ) ) ) )
395		ovex 5844	. . . . . . . . . . 11 |- ( I + 1 ) e. _V
396	395	a1i 12	. . . . . . . . . 10 |- ( x = ( I + 1 ) -> ( I + 1 ) e. _V )
397		eqtr3 2303	. . . . . . . . . . 11 |- ( ( x = ( I + 1 ) /\ n = ( I + 1 ) ) -> x = n )
398	397, 327	syl 17	. . . . . . . . . 10 |- ( ( x = ( I + 1 ) /\ n = ( I + 1 ) ) -> A = B )
399	396, 398	csbied 3124	. . . . . . . . 9 |- ( x = ( I + 1 ) -> [_ ( I + 1 ) / n ]_ A = B )
400	399	eqcomd 2289	. . . . . . . 8 |- ( x = ( I + 1 ) -> B = [_ ( I + 1 ) / n ]_ A )
401	400	breq1d 4034	. . . . . . 7 |- ( x = ( I + 1 ) -> ( B <_ [_ U / n ]_ A <-> [_ ( I + 1 ) / n ]_ A <_ [_ U / n ]_ A ) )
402	394, 401	imbi12d 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 ) ) )
403	402	rspcv 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 ) ) )
404	379, 391, 392, 403	syl3c 59	. . . 4 |- ( ph -> [_ ( I + 1 ) / n ]_ A <_ [_ U / n ]_ A )
405	101, 110, 96, 378, 404	lemul2ad 9692	. . 3 |- ( ph -> ( ( 2 x. R ) x. [_ ( I + 1 ) / n ]_ A ) <_ ( ( 2 x. R ) x. [_ U / n ]_ A ) )
406	92, 102, 111, 370, 405	letrd 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 ) )
407	91, 406	eqbrtrd 4044	1 |- ( ph -> ( abs ` ( ( seq 1 ( + , F ) ` J ) - ( seq 1 ( + , F ) ` I ) ) ) <_ ( ( 2 x. R ) x. [_ U / n