Theorem dchrisumlem2 22871

Description: Lemma for dchrisum 22873. 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 11699	. . . . . . . . 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 10449	. . . . . . . . . . 11 |- ( ph -> ( I + 1 ) e. NN )
5		nnuz 11006	. . . . . . . . . . 11 |- NN = ( ZZ>= ` 1 )
6	4, 5	syl6eleq 2552	. . . . . . . . . 10 |- ( ph -> ( I + 1 ) e. ( ZZ>= ` 1 ) )
7		dchrisumlem2.5	. . . . . . . . . . 11 |- ( ph -> J e. ( ZZ>= ` I ) )
8		eluzp1p1 10996	. . . . . . . . . . 11 |- ( J e. ( ZZ>= ` I ) -> ( J + 1 ) e. ( ZZ>= ` ( I + 1 ) ) )
9	7, 8	syl 16	. . . . . . . . . 10 |- ( ph -> ( J + 1 ) e. ( ZZ>= ` ( I + 1 ) ) )
10		elfzuzb 11563	. . . . . . . . . 10 |- ( ( I + 1 ) e. ( 1 ... ( J + 1 ) ) <-> ( ( I + 1 ) e. ( ZZ>= ` 1 ) /\ ( J + 1 ) e. ( ZZ>= ` ( I + 1 ) ) ) )
11	6, 9, 10	sylanbrc 664	. . . . . . . . 9 |- ( ph -> ( I + 1 ) e. ( 1 ... ( J + 1 ) ) )
12		fzosplit 11698	. . . . . . . . 9 |- ( ( I + 1 ) e. ( 1 ... ( J + 1 ) ) -> ( 1..^ ( J + 1 ) ) = ( ( 1..^ ( I + 1 ) ) u. ( ( I + 1 )..^ ( J + 1 ) ) ) )
13	11, 12	syl 16	. . . . . . . 8 |- ( ph -> ( 1..^ ( J + 1 ) ) = ( ( 1..^ ( I + 1 ) ) u. ( ( I + 1 )..^ ( J + 1 ) ) ) )
14		fzofi 11912	. . . . . . . . 9 |- ( 1..^ ( J + 1 ) ) e. Fin
15	14	a1i 11	. . . . . . . 8 |- ( ph -> ( 1..^ ( J + 1 ) ) e. Fin )
16		elfzouz 11673	. . . . . . . . . 10 |- ( i e. ( 1..^ ( J + 1 ) ) -> i e. ( ZZ>= ` 1 ) )
17	16, 5	syl6eleqr 2553	. . . . . . . . 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 465	. . . . . . . . . . 11 |- ( ( ph /\ i e. NN ) -> X e. D )
24		nnz 10778	. . . . . . . . . . . 12 |- ( i e. NN -> i e. ZZ )
25	24	adantl 466	. . . . . . . . . . 11 |- ( ( ph /\ i e. NN ) -> i e. ZZ )
26	18, 19, 20, 21, 23, 25	dchrzrhcl 22716	. . . . . . . . . 10 |- ( ( ph /\ i e. NN ) -> ( X ` ( L ` i ) ) e. CC )
27		nnrp 11110	. . . . . . . . . . . . 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 22869	. . . . . . . . . . . . . 14 |- ( ph -> ( ( i e. RR+ -> [_ i / n ]_ A e. RR ) /\ ( i e. ( M [,) +oo ) -> 0 <_ [_ i / n ]_ A ) ) )
38	37	simpld 459	. . . . . . . . . . . . 13 |- ( ph -> ( i e. RR+ -> [_ i / n ]_ A e. RR ) )
39	27, 38	syl5 32	. . . . . . . . . . . 12 |- ( ph -> ( i e. NN -> [_ i / n ]_ A e. RR ) )
40	39	imp 429	. . . . . . . . . . 11 |- ( ( ph /\ i e. NN ) -> [_ i / n ]_ A e. RR )
41	40	recnd 9522	. . . . . . . . . 10 |- ( ( ph /\ i e. NN ) -> [_ i / n ]_ A e. CC )
42	26, 41	mulcld 9516	. . . . . . . . 9 |- ( ( ph /\ i e. NN ) -> ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) e. CC )
43	17, 42	sylan2 474	. . . . . . . 8 |- ( ( ph /\ i e. ( 1..^ ( J + 1 ) ) ) -> ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) e. CC )
44	2, 13, 15, 43	fsumsplit 13333	. . . . . . 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 10980	. . . . . . . . 9 |- ( J e. ( ZZ>= ` I ) -> J e. ZZ )
46		fzval3 11721	. . . . . . . . 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 13295	. . . . . . 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 10856	. . . . . . . . . 10 |- ( ph -> I e. ZZ )
50		fzval3 11721	. . . . . . . . . 10 |- ( I e. ZZ -> ( 1 ... I ) = ( 1..^ ( I + 1 ) ) )
51	49, 50	syl 16	. . . . . . . . 9 |- ( ph -> ( 1 ... I ) = ( 1..^ ( I + 1 ) ) )
52	51	sumeq1d 13295	. . . . . . . 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 6214	. . . . . . 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 2505	. . . . . 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 11594	. . . . . . . 8 |- ( i e. ( 1 ... J ) -> i e. NN )
56		simpr 461	. . . . . . . . 9 |- ( ( ph /\ i e. NN ) -> i e. NN )
57		nfcv 2616	. . . . . . . . . 10 |- F/_ n i
58		nfcv 2616	. . . . . . . . . . 11 |- F/_ n ( X ` ( L ` i ) )
59		nfcv 2616	. . . . . . . . . . 11 |- F/_ n x.
60		nfcsb1v 3410	. . . . . . . . . . 11 |- F/_ n [_ i / n ]_ A
61	58, 59, 60	nfov 6222	. . . . . . . . . 10 |- F/_ n ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A )
62		fveq2 5798	. . . . . . . . . . . 12 |- ( n = i -> ( L ` n ) = ( L ` i ) )
63	62	fveq2d 5802	. . . . . . . . . . 11 |- ( n = i -> ( X ` ( L ` n ) ) = ( X ` ( L ` i ) ) )
64		csbeq1a 3403	. . . . . . . . . . 11 |- ( n = i -> A = [_ i / n ]_ A )
65	63, 64	oveq12d 6217	. . . . . . . . . 10 |- ( n = i -> ( ( X ` ( L ` n ) ) x. A ) = ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) )
66	57, 61, 65, 36	fvmptf 5898	. . . . . . . . 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 661	. . . . . . . 8 |- ( ( ph /\ i e. NN ) -> ( F ` i ) = ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) )
68	55, 67	sylan2 474	. . . . . . 7 |- ( ( ph /\ i e. ( 1 ... J ) ) -> ( F ` i ) = ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) )
69	3, 5	syl6eleq 2552	. . . . . . . 8 |- ( ph -> I e. ( ZZ>= ` 1 ) )
70		uztrn 10987	. . . . . . . 8 |- ( ( J e. ( ZZ>= ` I ) /\ I e. ( ZZ>= ` 1 ) ) -> J e. ( ZZ>= ` 1 ) )
71	7, 69, 70	syl2anc 661	. . . . . . 7 |- ( ph -> J e. ( ZZ>= ` 1 ) )
72	55, 42	sylan2 474	. . . . . . 7 |- ( ( ph /\ i e. ( 1 ... J ) ) -> ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) e. CC )
73	68, 71, 72	fsumser 13324	. . . . . 6 |- ( ph -> sum_ i e. ( 1 ... J ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) = ( seq 1 ( + , F ) ` J ) )
74	54, 73	eqtr3d 2497	. . . . 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 11594	. . . . . . 7 |- ( i e. ( 1 ... I ) -> i e. NN )
76	75, 67	sylan2 474	. . . . . 6 |- ( ( ph /\ i e. ( 1 ... I ) ) -> ( F ` i ) = ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) )
77	75, 42	sylan2 474	. . . . . 6 |- ( ( ph /\ i e. ( 1 ... I ) ) -> ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) e. CC )
78	76, 69, 77	fsumser 13324	. . . . 5 |- ( ph -> sum_ i e. ( 1 ... I ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) = ( seq 1 ( + , F ) ` I ) )
79	74, 78	oveq12d 6217	. . . 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 11911	. . . . . 6 |- ( ph -> ( 1 ... I ) e. Fin )
81	80, 77	fsumcl 13327	. . . . 5 |- ( ph -> sum_ i e. ( 1 ... I ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) e. CC )
82		fzofi 11912	. . . . . . 7 |- ( ( I + 1 )..^ ( J + 1 ) ) e. Fin
83	82	a1i 11	. . . . . 6 |- ( ph -> ( ( I + 1 )..^ ( J + 1 ) ) e. Fin )
84		ssun2 3627	. . . . . . . . 9 |- ( ( I + 1 )..^ ( J + 1 ) ) C_ ( ( 1..^ ( I + 1 ) ) u. ( ( I + 1 )..^ ( J + 1 ) ) )
85	84, 13	syl5sseqr 3512	. . . . . . . 8 |- ( ph -> ( ( I + 1 )..^ ( J + 1 ) ) C_ ( 1..^ ( J + 1 ) ) )
86	85	sselda 3463	. . . . . . 7 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> i e. ( 1..^ ( J + 1 ) ) )
87	86, 43	syldan 470	. . . . . 6 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) e. CC )
88	83, 87	fsumcl 13327	. . . . 5 |- ( ph -> sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) e. CC )
89	81, 88	pncan2d 9831	. . . 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 2497	. . 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 5802	. 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 13039	. . 3 |- ( ph -> ( abs ` sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) ) e. RR )
93		2re 10501	. . . . . 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 9524	. . . 4 |- ( ph -> ( 2 x. R ) e. RR )
97	40	ralrimiva 2829	. . . . 5 |- ( ph -> A. i e. NN [_ i / n ]_ A e. RR )
98		csbeq1 3397	. . . . . . 7 |- ( i = ( I + 1 ) -> [_ i / n ]_ A = [_ ( I + 1 ) / n ]_ A )
99	98	eleq1d 2523	. . . . . 6 |- ( i = ( I + 1 ) -> ( [_ i / n ]_ A e. RR <-> [_ ( I + 1 ) / n ]_ A e. RR ) )
100	99	rspcv 3173	. . . . 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 60	. . . 4 |- ( ph -> [_ ( I + 1 ) / n ]_ A e. RR )
102	96, 101	remulcld 9524	. . 3 |- ( ph -> ( ( 2 x. R ) x. [_ ( I + 1 ) / n ]_ A ) e. RR )
103		dchrisumlem2.1	. . . . 5 |- ( ph -> U e. RR+ )
104	33	ralrimiva 2829	. . . . 5 |- ( ph -> A. n e. RR+ A e. RR )
105		nfcsb1v 3410	. . . . . . 7 |- F/_ n [_ U / n ]_ A
106	105	nfel1 2631	. . . . . 6 |- F/ n [_ U / n ]_ A e. RR
107		csbeq1a 3403	. . . . . . 7 |- ( n = U -> A = [_ U / n ]_ A )
108	107	eleq1d 2523	. . . . . 6 |- ( n = U -> ( A e. RR <-> [_ U / n ]_ A e. RR ) )
109	106, 108	rspc 3171	. . . . 5 |- ( U e. RR+ -> ( A. n e. RR+ A e. RR -> [_ U / n ]_ A e. RR ) )
110	103, 104, 109	sylc 60	. . . 4 |- ( ph -> [_ U / n ]_ A e. RR )
111	96, 110	remulcld 9524	. . 3 |- ( ph -> ( ( 2 x. R ) x. [_ U / n ]_ A ) e. RR )
112	71, 5	syl6eleqr 2553	. . . . . . . . . . . 12 |- ( ph -> J e. NN )
113	112	peano2nnd 10449	. . . . . . . . . . 11 |- ( ph -> ( J + 1 ) e. NN )
114	113	nnrpd 11136	. . . . . . . . . 10 |- ( ph -> ( J + 1 ) e. RR+ )
115	19, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36	dchrisumlema 22869	. . . . . . . . . . 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 459	. . . . . . . . . 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 9522	. . . . . . . 8 |- ( ph -> [_ ( J + 1 ) / n ]_ A e. CC )
119		fzofi 11912	. . . . . . . . . 10 |- ( 0..^ ( J + 1 ) ) e. Fin
120	119	a1i 11	. . . . . . . . 9 |- ( ph -> ( 0..^ ( J + 1 ) ) e. Fin )
121		elfzoelz 11669	. . . . . . . . . 10 |- ( n e. ( 0..^ ( J + 1 ) ) -> n e. ZZ )
122	22	adantr 465	. . . . . . . . . . 11 |- ( ( ph /\ n e. ZZ ) -> X e. D )
123		simpr 461	. . . . . . . . . . 11 |- ( ( ph /\ n e. ZZ ) -> n e. ZZ )
124	18, 19, 20, 21, 122, 123	dchrzrhcl 22716	. . . . . . . . . 10 |- ( ( ph /\ n e. ZZ ) -> ( X ` ( L ` n ) ) e. CC )
125	121, 124	sylan2 474	. . . . . . . . 9 |- ( ( ph /\ n e. ( 0..^ ( J + 1 ) ) ) -> ( X ` ( L ` n ) ) e. CC )
126	120, 125	fsumcl 13327	. . . . . . . 8 |- ( ph -> sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) e. CC )
127	118, 126	mulcld 9516	. . . . . . 7 |- ( ph -> ( [_ ( J + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) e. CC )
128	101	recnd 9522	. . . . . . . 8 |- ( ph -> [_ ( I + 1 ) / n ]_ A e. CC )
129		fzofi 11912	. . . . . . . . . 10 |- ( 0..^ ( I + 1 ) ) e. Fin
130	129	a1i 11	. . . . . . . . 9 |- ( ph -> ( 0..^ ( I + 1 ) ) e. Fin )
131		elfzoelz 11669	. . . . . . . . . 10 |- ( n e. ( 0..^ ( I + 1 ) ) -> n e. ZZ )
132	131, 124	sylan2 474	. . . . . . . . 9 |- ( ( ph /\ n e. ( 0..^ ( I + 1 ) ) ) -> ( X ` ( L ` n ) ) e. CC )
133	130, 132	fsumcl 13327	. . . . . . . 8 |- ( ph -> sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) e. CC )
134	128, 133	mulcld 9516	. . . . . . 7 |- ( ph -> ( [_ ( I + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) e. CC )
135	127, 134	subcld 9829	. . . . . 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 13039	. . . . 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 16	. . . . . . . 8 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> i e. NN )
138		peano2nn 10444	. . . . . . . . . . . . 13 |- ( i e. NN -> ( i + 1 ) e. NN )
139	138	nnrpd 11136	. . . . . . . . . . . 12 |- ( i e. NN -> ( i + 1 ) e. RR+ )
140		nfcsb1v 3410	. . . . . . . . . . . . . . 15 |- F/_ n [_ ( i + 1 ) / n ]_ A
141	140	nfel1 2631	. . . . . . . . . . . . . 14 |- F/ n [_ ( i + 1 ) / n ]_ A e. RR
142		csbeq1a 3403	. . . . . . . . . . . . . . 15 |- ( n = ( i + 1 ) -> A = [_ ( i + 1 ) / n ]_ A )
143	142	eleq1d 2523	. . . . . . . . . . . . . 14 |- ( n = ( i + 1 ) -> ( A e. RR <-> [_ ( i + 1 ) / n ]_ A e. RR ) )
144	141, 143	rspc 3171	. . . . . . . . . . . . 13 |- ( ( i + 1 ) e. RR+ -> ( A. n e. RR+ A e. RR -> [_ ( i + 1 ) / n ]_ A e. RR ) )
145	144	impcom 430	. . . . . . . . . . . 12 |- ( ( A. n e. RR+ A e. RR /\ ( i + 1 ) e. RR+ ) -> [_ ( i + 1 ) / n ]_ A e. RR )
146	104, 139, 145	syl2an 477	. . . . . . . . . . 11 |- ( ( ph /\ i e. NN ) -> [_ ( i + 1 ) / n ]_ A e. RR )
147	146, 40	resubcld 9886	. . . . . . . . . 10 |- ( ( ph /\ i e. NN ) -> ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) e. RR )
148	147	recnd 9522	. . . . . . . . 9 |- ( ( ph /\ i e. NN ) -> ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) e. CC )
149		fzofi 11912	. . . . . . . . . . . 12 |- ( 0..^ ( i + 1 ) ) e. Fin
150	149	a1i 11	. . . . . . . . . . 11 |- ( ph -> ( 0..^ ( i + 1 ) ) e. Fin )
151		elfzoelz 11669	. . . . . . . . . . . 12 |- ( n e. ( 0..^ ( i + 1 ) ) -> n e. ZZ )
152	151, 124	sylan2 474	. . . . . . . . . . 11 |- ( ( ph /\ n e. ( 0..^ ( i + 1 ) ) ) -> ( X ` ( L ` n ) ) e. CC )
153	150, 152	fsumcl 13327	. . . . . . . . . 10 |- ( ph -> sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) e. CC )
154	153	adantr 465	. . . . . . . . 9 |- ( ( ph /\ i e. NN ) -> sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) e. CC )
155	148, 154	mulcld 9516	. . . . . . . 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 470	. . . . . . 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 13327	. . . . . 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 13039	. . . . 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 9523	. . . 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 9517	. . . . . . . . . 10 |- ( ( ph /\ i e. NN ) -> ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) = ( [_ i / n ]_ A x. ( X ` ( L ` i ) ) ) )
161		nnnn0 10696	. . . . . . . . . . . . . . . 16 |- ( i e. NN -> i e. NN0 )
162	161	adantl 466	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. NN ) -> i e. NN0 )
163		nn0uz 11005	. . . . . . . . . . . . . . 15 |- NN0 = ( ZZ>= ` 0 )
164	162, 163	syl6eleq 2552	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. NN ) -> i e. ( ZZ>= ` 0 ) )
165		elfzelz 11569	. . . . . . . . . . . . . . 15 |- ( n e. ( 0 ... i ) -> n e. ZZ )
166	124	adantlr 714	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. NN ) /\ n e. ZZ ) -> ( X ` ( L ` n ) ) e. CC )
167	165, 166	sylan2 474	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. NN ) /\ n e. ( 0 ... i ) ) -> ( X ` ( L ` n ) ) e. CC )
168	164, 167, 63	fzosump1 13338	. . . . . . . . . . . . 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 6214	. . . . . . . . . . . 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 11912	. . . . . . . . . . . . . . 15 |- ( 0..^ i ) e. Fin
171	170	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. NN ) -> ( 0..^ i ) e. Fin )
172		elfzoelz 11669	. . . . . . . . . . . . . . 15 |- ( n e. ( 0..^ i ) -> n e. ZZ )
173	172, 166	sylan2 474	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. NN ) /\ n e. ( 0..^ i ) ) -> ( X ` ( L ` n ) ) e. CC )
174	171, 173	fsumcl 13327	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. NN ) -> sum_ n e. ( 0..^ i ) ( X ` ( L ` n ) ) e. CC )
175	174, 26	pncan2d 9831	. . . . . . . . . . . 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 2496	. . . . . . . . . . 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 6215	. . . . . . . . . 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 2495	. . . . . . . . 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 470	. . . . . . . 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 13297	. . . . . . 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 3397	. . . . . . . . 9 |- ( k = i -> [_ k / n ]_ A = [_ i / n ]_ A )
182		oveq2 6207	. . . . . . . . . 10 |- ( k = i -> ( 0..^ k ) = ( 0..^ i ) )
183	182	sumeq1d 13295	. . . . . . . . 9 |- ( k = i -> sum_ n e. ( 0..^ k ) ( X ` ( L ` n ) ) = sum_ n e. ( 0..^ i ) ( X ` ( L ` n ) ) )
184	181, 183	jca 532	. . . . . . . 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 3397	. . . . . . . . 9 |- ( k = ( i + 1 ) -> [_ k / n ]_ A = [_ ( i + 1 ) / n ]_ A )
186		oveq2 6207	. . . . . . . . . 10 |- ( k = ( i + 1 ) -> ( 0..^ k ) = ( 0..^ ( i + 1 ) ) )
187	186	sumeq1d 13295	. . . . . . . . 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 532	. . . . . . . 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 3397	. . . . . . . . 9 |- ( k = ( I + 1 ) -> [_ k / n ]_ A = [_ ( I + 1 ) / n ]_ A )
190		oveq2 6207	. . . . . . . . . 10 |- ( k = ( I + 1 ) -> ( 0..^ k ) = ( 0..^ ( I + 1 ) ) )
191	190	sumeq1d 13295	. . . . . . . . 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 532	. . . . . . . 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 3397	. . . . . . . . 9 |- ( k = ( J + 1 ) -> [_ k / n ]_ A = [_ ( J + 1 ) / n ]_ A )
194		oveq2 6207	. . . . . . . . . 10 |- ( k = ( J + 1 ) -> ( 0..^ k ) = ( 0..^ ( J + 1 ) ) )
195	194	sumeq1d 13295	. . . . . . . . 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 532	. . . . . . . 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 11565	. . . . . . . . . 10 |- ( k e. ( ( I + 1 ) ... ( J + 1 ) ) -> k e. ( ZZ>= ` ( I + 1 ) ) )
198		eluznn 11035	. . . . . . . . . 10 |- ( ( ( I + 1 ) e. NN /\ k e. ( ZZ>= ` ( I + 1 ) ) ) -> k e. NN )
199	4, 197, 198	syl2an 477	. . . . . . . . 9 |- ( ( ph /\ k e. ( ( I + 1 ) ... ( J + 1 ) ) ) -> k e. NN )
200	41	ralrimiva 2829	. . . . . . . . . 10 |- ( ph -> A. i e. NN [_ i / n ]_ A e. CC )
201		csbeq1 3397	. . . . . . . . . . . 12 |- ( i = k -> [_ i / n ]_ A = [_ k / n ]_ A )
202	201	eleq1d 2523	. . . . . . . . . . 11 |- ( i = k -> ( [_ i / n ]_ A e. CC <-> [_ k / n ]_ A e. CC ) )
203	202	rspccva 3176	. . . . . . . . . 10 |- ( ( A. i e. NN [_ i / n ]_ A e. CC /\ k e. NN ) -> [_ k / n ]_ A e. CC )
204	200, 203	sylan 471	. . . . . . . . 9 |- ( ( ph /\ k e. NN ) -> [_ k / n ]_ A e. CC )
205	199, 204	syldan 470	. . . . . . . 8 |- ( ( ph /\ k e. ( ( I + 1 ) ... ( J + 1 ) ) ) -> [_ k / n ]_ A e. CC )
206		fzofi 11912	. . . . . . . . . . 11 |- ( 0..^ k ) e. Fin
207	206	a1i 11	. . . . . . . . . 10 |- ( ph -> ( 0..^ k ) e. Fin )
208		elfzoelz 11669	. . . . . . . . . . 11 |- ( n e. ( 0..^ k ) -> n e. ZZ )
209	208, 124	sylan2 474	. . . . . . . . . 10 |- ( ( ph /\ n e. ( 0..^ k ) ) -> ( X ` ( L ` n ) ) e. CC )
210	207, 209	fsumcl 13327	. . . . . . . . 9 |- ( ph -> sum_ n e. ( 0..^ k ) ( X ` ( L ` n ) ) e. CC )
211	210	adantr 465	. . . . . . . 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 13386	. . . . . . 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 2495	. . . . . 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 5802	. . . . 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 13061	. . . . 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 4419	. . . 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 9523	. . . . . . 7 |- ( ph -> ( [_ ( J + 1 ) / n ]_ A + [_ ( I + 1 ) / n ]_ A ) e. RR )
218	217, 95	remulcld 9524	. . . . . 6 |- ( ph -> ( ( [_ ( J + 1 ) / n ]_ A + [_ ( I + 1 ) / n ]_ A ) x. R ) e. RR )
219	181, 185, 189, 193, 9, 205	fsumtscopo 13382	. . . . . . . 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 470	. . . . . . . . . 10 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> [_ i / n ]_ A e. RR )
221	137, 146	syldan 470	. . . . . . . . . 10 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> [_ ( i + 1 ) / n ]_ A e. RR )
222	220, 221	resubcld 9886	. . . . . . . . 9 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) e. RR )
223	83, 222	fsumrecl 13328	. . . . . . . 8 |- ( ph -> sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) e. RR )
224	219, 223	eqeltrrd 2543	. . . . . . 7 |- ( ph -> ( [_ ( I + 1 ) / n ]_ A - [_ ( J + 1 ) / n ]_ A ) e. RR )
225	224, 95	remulcld 9524	. . . . . 6 |- ( ph -> ( ( [_ ( I + 1 ) / n ]_ A - [_ ( J + 1 ) / n ]_ A ) x. R ) e. RR )
226	127	abscld 13039	. . . . . . . 8 |- ( ph -> ( abs ` ( [_ ( J + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) ) e. RR )
227	134	abscld 13039	. . . . . . . 8 |- ( ph -> ( abs ` ( [_ ( I + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) ) e. RR )
228	226, 227	readdcld 9523	. . . . . . 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 13061	. . . . . . 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 9524	. . . . . . . . 9 |- ( ph -> ( [_ ( J + 1 ) / n ]_ A x. R ) e. RR )
231	101, 95	remulcld 9524	. . . . . . . . 9 |- ( ph -> ( [_ ( I + 1 ) / n ]_ A x. R ) e. RR )
232	118, 126	absmuld 13057	. . . . . . . . . . 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 10981	. . . . . . . . . . . . . . . . . . 19 |- ( i e. ( ZZ>= ` M ) -> i e. RR )
234	233	adantl 466	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> i e. RR )
235		eluzle 10983	. . . . . . . . . . . . . . . . . . 19 |- ( i e. ( ZZ>= ` M ) -> M <_ i )
236	235	adantl 466	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> M <_ i )
237	32	nnred 10447	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> M e. RR )
238	237	adantr 465	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> M e. RR )
239		elicopnf 11501	. . . . . . . . . . . . . . . . . . 19 |- ( M e. RR -> ( i e. ( M [,) +oo ) <-> ( i e. RR /\ M <_ i ) ) )
240	238, 239	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> ( i e. ( M [,) +oo ) <-> ( i e. RR /\ M <_ i ) ) )
241	234, 236, 240	mpbir2and 913	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> i e. ( M [,) +oo ) )
242	241	ex 434	. . . . . . . . . . . . . . . 16 |- ( ph -> ( i e. ( ZZ>= ` M ) -> i e. ( M [,) +oo ) ) )
243	242	ssrdv 3469	. . . . . . . . . . . . . . 15 |- ( ph -> ( ZZ>= ` M ) C_ ( M [,) +oo ) )
244	32	nnzd 10856	. . . . . . . . . . . . . . . . 17 |- ( ph -> M e. ZZ )
245	49	peano2zd 10860	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( I + 1 ) e. ZZ )
246	103	rpred 11137	. . . . . . . . . . . . . . . . . 18 |- ( ph -> U e. RR )
247	4	nnred 10447	. . . . . . . . . . . . . . . . . 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 9638	. . . . . . . . . . . . . . . . 17 |- ( ph -> M <_ ( I + 1 ) )
251		eluz2 10977	. . . . . . . . . . . . . . . . 17 |- ( ( I + 1 ) e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ ( I + 1 ) e. ZZ /\ M <_ ( I + 1 ) ) )
252	244, 245, 250, 251	syl3anbrc 1172	. . . . . . . . . . . . . . . 16 |- ( ph -> ( I + 1 ) e. ( ZZ>= ` M ) )
253		uztrn 10987	. . . . . . . . . . . . . . . 16 |- ( ( ( J + 1 ) e. ( ZZ>= ` ( I + 1 ) ) /\ ( I + 1 ) e. ( ZZ>= ` M ) ) -> ( J + 1 ) e. ( ZZ>= ` M ) )
254	9, 252, 253	syl2anc 661	. . . . . . . . . . . . . . 15 |- ( ph -> ( J + 1 ) e. ( ZZ>= ` M ) )
255	243, 254	sseldd 3464	. . . . . . . . . . . . . 14 |- ( ph -> ( J + 1 ) e. ( M [,) +oo ) )
256	115	simprd 463	. . . . . . . . . . . . . 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 13026	. . . . . . . . . . . 12 |- ( ph -> ( abs ` [_ ( J + 1 ) / n ]_ A ) = [_ ( J + 1 ) / n ]_ A )
259	258	oveq1d 6214	. . . . . . . . . . 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 2495	. . . . . . . . . 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 13039	. . . . . . . . . . 11 |- ( ph -> ( abs ` sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) e. RR )
262	113	nnnn0d 10746	. . . . . . . . . . . 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 22870	. . . . . . . . . . . 12 |- ( ( ph /\ ( J + 1 ) e. NN0 ) -> ( abs ` sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) <_ R )
265	262, 264	mpdan 668	. . . . . . . . . . 11 |- ( ph -> ( abs ` sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) <_ R )
266	261, 95, 117, 257, 265	lemul2ad 10383	. . . . . . . . . 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 4419	. . . . . . . . 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 13057	. . . . . . . . . . 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 3464	. . . . . . . . . . . . . 14 |- ( ph -> ( I + 1 ) e. ( M [,) +oo ) )
270	19, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36	dchrisumlema 22869	. . . . . . . . . . . . . . 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 463	. . . . . . . . . . . . . 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 13026	. . . . . . . . . . . 12 |- ( ph -> ( abs ` [_ ( I + 1 ) / n ]_ A ) = [_ ( I + 1 ) / n ]_ A )
274	273	oveq1d 6214	. . . . . . . . . . 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 2495	. . . . . . . . . 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 13039	. . . . . . . . . . 11 |- ( ph -> ( abs ` sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) e. RR )
277	4	nnnn0d 10746	. . . . . . . . . . . 12 |- ( ph -> ( I + 1 ) e. NN0 )
278	19, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36, 95, 263	dchrisumlem1 22870	. . . . . . . . . . . 12 |- ( ( ph /\ ( I + 1 ) e. NN0 ) -> ( abs ` sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) <_ R )
279	277, 278	mpdan 668	. . . . . . . . . . 11 |- ( ph -> ( abs ` sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) <_ R )
280	276, 95, 101, 272, 279	lemul2ad 10383	. . . . . . . . . 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 4419	. . . . . . . . 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 10067	. . . . . . . 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 9522	. . . . . . . . 9 |- ( ph -> R e. CC )
284	118, 128, 283	adddird 9521	. . . . . . . 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 4425	. . . . . . 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 9638	. . . . . 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 13039	. . . . . . . 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 13328	. . . . . . 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 13381	. . . . . . 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 465	. . . . . . . . . 10 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> R e. RR )
291	222, 290	remulcld 9524	. . . . . . . . 9 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) x. R ) e. RR )
292	137, 148	syldan 470	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) e. CC )
293	153	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) e. CC )
294	292, 293	absmuld 13057	. . . . . . . . . . 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 11673	. . . . . . . . . . . . . . 15 |- ( i e. ( ( I + 1 )..^ ( J + 1 ) ) -> i e. ( ZZ>= ` ( I + 1 ) ) )
296		uztrn 10987	. . . . . . . . . . . . . . 15 |- ( ( i e. ( ZZ>= ` ( I + 1 ) ) /\ ( I + 1 ) e. ( ZZ>= ` M ) ) -> i e. ( ZZ>= ` M ) )
297	295, 252, 296	syl2anr 478	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> i e. ( ZZ>= ` M ) )
298		eluznn 11035	. . . . . . . . . . . . . . . . 17 |- ( ( M e. NN /\ i e. ( ZZ>= ` M ) ) -> i e. NN )
299	32, 298	sylan 471	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> i e. NN )
300	299, 139	syl 16	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> ( i + 1 ) e. RR+ )
301	299	nnrpd 11136	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> i e. RR+ )
302	34	3expia 1190	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) ) -> ( ( M <_ n /\ n <_ x ) -> B <_ A ) )
303	302	ralrimivva 2912	. . . . . . . . . . . . . . . . 17 |- ( ph -> A. n e. RR+ A. x e. RR+ ( ( M <_ n /\ n <_ x ) -> B <_ A ) )
304	303	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> A. n e. RR+ A. x e. RR+ ( ( M <_ n /\ n <_ x ) -> B <_ A ) )
305		nfcv 2616	. . . . . . . . . . . . . . . . . 18 |- F/_ n RR+
306		nfv 1674	. . . . . . . . . . . . . . . . . . 19 |- F/ n ( M <_ i /\ i <_ x )
307		nfcv 2616	. . . . . . . . . . . . . . . . . . . 20 |- F/_ n B
308		nfcv 2616	. . . . . . . . . . . . . . . . . . . 20 |- F/_ n <_
309	307, 308, 60	nfbr 4443	. . . . . . . . . . . . . . . . . . 19 |- F/ n B <_ [_ i / n ]_ A
310	306, 309	nfim 1858	. . . . . . . . . . . . . . . . . 18 |- F/ n ( ( M <_ i /\ i <_ x ) -> B <_ [_ i / n ]_ A )
311	305, 310	nfral 2886	. . . . . . . . . . . . . . . . 17 |- F/ n A. x e. RR+ ( ( M <_ i /\ i <_ x ) -> B <_ [_ i / n ]_ A )
312		breq2 4403	. . . . . . . . . . . . . . . . . . . 20 |- ( n = i -> ( M <_ n <-> M <_ i ) )
313		breq1 4402	. . . . . . . . . . . . . . . . . . . 20 |- ( n = i -> ( n <_ x <-> i <_ x ) )
314	312, 313	anbi12d 710	. . . . . . . . . . . . . . . . . . 19 |- ( n = i -> ( ( M <_ n /\ n <_ x ) <-> ( M <_ i /\ i <_ x ) ) )
315	64	breq2d 4411	. . . . . . . . . . . . . . . . . . 19 |- ( n = i -> ( B <_ A <-> B <_ [_ i / n ]_ A ) )
316	314, 315	imbi12d 320	. . . . . . . . . . . . . . . . . 18 |- ( n = i -> ( ( ( M <_ n /\ n <_ x ) -> B <_ A ) <-> ( ( M <_ i /\ i <_ x ) -> B <_ [_ i / n ]_ A ) ) )
317	316	ralbidv 2845	. . . . . . . . . . . . . . . . 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 3171	. . . . . . . . . . . . . . . 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 60	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> A. x e. RR+ ( ( M <_ i /\ i <_ x ) -> B <_ [_ i / n ]_ A ) )
320	234	lep1d 10374	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> i <_ ( i + 1 ) )
321	236, 320	jca 532	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> ( M <_ i /\ i <_ ( i + 1 ) ) )
322		breq2 4403	. . . . . . . . . . . . . . . . . 18 |- ( x = ( i + 1 ) -> ( i <_ x <-> i <_ ( i + 1 ) ) )
323	322	anbi2d 703	. . . . . . . . . . . . . . . . 17 |- ( x = ( i + 1 ) -> ( ( M <_ i /\ i <_ x ) <-> ( M <_ i /\ i <_ ( i + 1 ) ) ) )
324		ovex 6224	. . . . . . . . . . . . . . . . . . . . 21 |- ( i + 1 ) e. _V
325	324	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( x = ( i + 1 ) -> ( i + 1 ) e. _V )
326		eqtr3 2482	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( x = ( i + 1 ) /\ n = ( i + 1 ) ) -> x = n )
327	31	equcoms 1735	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = n -> A = B )
328	326, 327	syl 16	. . . . . . . . . . . . . . . . . . . 20 |- ( ( x = ( i + 1 ) /\ n = ( i + 1 ) ) -> A = B )
329	325, 328	csbied 3421	. . . . . . . . . . . . . . . . . . 19 |- ( x = ( i + 1 ) -> [_ ( i + 1 ) / n ]_ A = B )
330	329	eqcomd 2462	. . . . . . . . . . . . . . . . . 18 |- ( x = ( i + 1 ) -> B = [_ ( i + 1 ) / n ]_ A )
331	330	breq1d 4409	. . . . . . . . . . . . . . . . 17 |- ( x = ( i + 1 ) -> ( B <_ [_ i / n ]_ A <-> [_ ( i + 1 ) / n ]_ A <_ [_ i / n ]_ A ) )
332	323, 331	imbi12d 320	. . . . . . . . . . . . . . . 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 3173	. . . . . . . . . . . . . . 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 61	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> [_ ( i + 1 ) / n ]_ A <_ [_ i / n ]_ A )
335	297, 334	syldan 470	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> [_ ( i + 1 ) / n ]_ A <_ [_ i / n ]_ A )
336	221, 220, 335	abssuble0d 13036	. . . . . . . . . . . 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 6214	. . . . . . . . . . 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 2495	. . . . . . . . . 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 13039	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( abs ` sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) e. RR )
340	220, 221	subge0d 10039	. . . . . . . . . . . 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 232	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> 0 <_ ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) )
342	137	peano2nnd 10449	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( i + 1 ) e. NN )
343	342	nnnn0d 10746	. . . . . . . . . . . 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 22870	. . . . . . . . . . . 12 |- ( ( ph /\ ( i + 1 ) e. NN0 ) -> ( abs ` sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) <_ R )
345	343, 344	syldan 470	. . . . . . . . . . 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 10383	. . . . . . . . . 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 4419	. . . . . . . . 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 13379	. . . . . . . 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 9522	. . . . . . . . . 10 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) e. CC )
350	83, 283, 349	fsummulc1 13369	. . . . . . . . 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 6214	. . . . . . . . 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 2497	. . . . . . . 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 4423	. . . . . . 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 9638	. . . . . 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 10067	. . . . 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 10677	. . . . . . . 8 |- ( ph -> ( 2 x. [_ ( I + 1 ) / n ]_ A ) = ( [_ ( I + 1 ) / n ]_ A + [_ ( I + 1 ) / n ]_ A ) )
357	128, 118, 128	ppncand 9869	. . . . . . . 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 9681	. . . . . . . . 9 |- ( ph -> ( [_ ( I + 1 ) / n ]_ A + [_ ( J + 1 ) / n ]_ A ) = ( [_ ( J + 1 ) / n ]_ A + [_ ( I + 1 ) / n ]_ A ) )
359	358	oveq1d 6214	. . . . . . . 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 2501	. . . . . . 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 6214	. . . . . 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		2cnd 10504	. . . . . . 7 |- ( ph -> 2 e. CC )
363	362, 128, 283	mul32d 9689	. . . . . 6 |- ( ph -> ( ( 2 x. [_ ( I + 1 ) / n ]_ A ) x. R ) = ( ( 2 x. R ) x. [_ ( I + 1 ) / n ]_ A ) )
364	217	recnd 9522	. . . . . . 7 |- ( ph -> ( [_ ( J + 1 ) / n ]_ A + [_ ( I + 1 ) / n ]_ A ) e. CC )
365	224	recnd 9522	. . . . . . 7 |- ( ph -> ( [_ ( I + 1 ) / n ]_ A - [_ ( J + 1 ) / n ]_ A ) e. CC )
366	364, 365, 283	adddird 9521	. . . . . 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 ) ) )
367	361, 363, 366	3eqtr3d 2503	. . . . 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 ) ) )
368	355, 367	breqtrrd 4425	. . . 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 ) )
369	92, 159, 102, 216, 368	letrd 9638	. . 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 ) )
370		2nn0 10706	. . . . . 6 |- 2 e. NN0
371		nn0ge0 10715	. . . . . 6 |- ( 2 e. NN0 -> 0 <_ 2 )
372	370, 371	mp1i 12	. . . . 5 |- ( ph -> 0 <_ 2 )
373		0red 9497	. . . . . 6 |- ( ph -> 0 e. RR )
374	126	absge0d 13047	. . . . . 6 |- ( ph -> 0 <_ ( abs ` sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) )
375	373, 261, 95, 374, 265	letrd 9638	. . . . 5 |- ( ph -> 0 <_ R )
376	94, 95, 372, 375	mulge0d 10026	. . . 4 |- ( ph -> 0 <_ ( 2 x. R ) )
377	4	nnrpd 11136	. . . . 5 |- ( ph -> ( I + 1 ) e. RR+ )
378		nfv 1674	. . . . . . . . 9 |- F/ n ( M <_ U /\ U <_ x )
379	307, 308, 105	nfbr 4443	. . . . . . . . 9 |- F/ n B <_ [_ U / n ]_ A
380	378, 379	nfim 1858	. . . . . . . 8 |- F/ n ( ( M <_ U /\ U <_ x ) -> B <_ [_ U / n ]_ A )
381	305, 380	nfral 2886	. . . . . . 7 |- F/ n A. x e. RR+ ( ( M <_ U /\ U <_ x ) -> B <_ [_ U / n ]_ A )
382		breq2 4403	. . . . . . . . . 10 |- ( n = U -> ( M <_ n <-> M <_ U ) )
383		breq1 4402	. . . . . . . . . 10 |- ( n = U -> ( n <_ x <-> U <_ x ) )
384	382, 383	anbi12d 710	. . . . . . . . 9 |- ( n = U -> ( ( M <_ n /\ n <_ x ) <-> ( M <_ U /\ U <_ x ) ) )
385	107	breq2d 4411	. . . . . . . . 9 |- ( n = U -> ( B <_ A <-> B <_ [_ U / n ]_ A ) )
386	384, 385	imbi12d 320	. . . . . . . 8 |- ( n = U -> ( ( ( M <_ n /\ n <_ x ) -> B <_ A ) <-> ( ( M <_ U /\ U <_ x ) -> B <_ [_ U / n ]_ A ) ) )
387	386	ralbidv 2845	. . . . . . 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 ) ) )
388	381, 387	rspc 3171	. . . . . 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 ) ) )
389	103, 303, 388	sylc 60	. . . . 5 |- ( ph -> A. x e. RR+ ( ( M <_ U /\ U <_ x ) -> B <_ [_ U / n ]_ A ) )
390	248, 249	jca 532	. . . . 5 |- ( ph -> ( M <_ U /\ U <_ ( I + 1 ) ) )
391		breq2 4403	. . . . . . . 8 |- ( x = ( I + 1 ) -> ( U <_ x <-> U <_ ( I + 1 ) ) )
392	391	anbi2d 703	. . . . . . 7 |- ( x = ( I + 1 ) -> ( ( M <_ U /\ U <_ x ) <-> ( M <_ U /\ U <_ ( I + 1 ) ) ) )
393		ovex 6224	. . . . . . . . . . 11 |- ( I + 1 ) e. _V
394	393	a1i 11	. . . . . . . . . 10 |- ( x = ( I + 1 ) -> ( I + 1 ) e. _V )
395		eqtr3 2482	. . . . . . . . . . 11 |- ( ( x = ( I + 1 ) /\ n = ( I + 1 ) ) -> x = n )
396	395, 327	syl 16	. . . . . . . . . 10 |- ( ( x = ( I + 1 ) /\ n = ( I + 1 ) ) -> A = B )
397	394, 396	csbied 3421	. . . . . . . . 9 |- ( x = ( I + 1 ) -> [_ ( I + 1 ) / n ]_ A = B )
398	397	eqcomd 2462	. . . . . . . 8 |- ( x = ( I + 1 ) -> B = [_ ( I + 1 ) / n ]_ A )
399	398	breq1d 4409	. . . . . . 7 |- ( x = ( I + 1 ) -> ( B <_ [_ U / n ]_ A <-> [_ ( I + 1 ) / n ]_ A <_ [_ U / n ]_ A ) )
400	392, 399	imbi12d 320	. . . . . 6 |- ( x = ( I + 1 ) -> ( ( ( M <_ U /\ U <_ x ) -> B <_ [_ U / n ]_ A ) <-> ( ( M <_ U /\ U <_ ( I + 1 ) ) -> [_ ( I + 1 ) / n ]_ A <_ [_ U / n ]_ A ) ) )
401	400	rspcv 3173	. . . . 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 ) ) )
402	377, 389, 390, 401	syl3c 61	. . . 4 |- ( ph -> [_ ( I + 1 ) / n ]_ A <_ [_ U / n ]_ A )
403	101, 110, 96, 376, 402	lemul2ad 10383	. . 3 |- ( ph -> ( ( 2 x. R ) x. [_ ( I + 1 ) / n ]_ A ) <_ ( ( 2 x. R ) x. [_ U / n ]_ A ) )
404	92, 102, 111, 369, 403	letrd 9638	. 2 |- ( ph -> ( abs ` sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) ) <_ ( ( 2 x. R ) x. [_ U / n ]_ A ) )
405	91, 404	eqbrtrd 4419	1 |- ( ph -> ( abs ` ( ( seq 1 ( + , F ) ` J ) - ( seq 1 ( + , F ) ` I ) ) ) <_ ( ( 2 x. R ) x. [_ U / n ]_ A ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   /\ w3a 965   = wceq 1370   e. wcel 1758   =/= wne 2647   A.wral 2798   _Vcvv 3076   [_csb 3394   u. cun 3433   i^i cin 3434   (/)c0 3744   class class class wbr 4399   |-> cmpt 4457   ` cfv 5525  (class class class)co 6199   Fincfn 7419   CCcc 9390   RRcr 9391   0cc0 9392   1c1 9393   + caddc 9395   x. cmul 9397   +oocpnf 9525   <_ cle 9529   - cmin 9705   NNcn 10432   2c2 10481   NN0cn0 10689   ZZcz 10756   ZZ>=cuz 10971   RR+crp 11101   [,)cico 11412