Theorem dchrisumlem2 25179

Description: Lemma for dchrisum 25181. 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 12502	. . . . . . . . 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 11037	. . . . . . . . . . 11 |- ( ph -> ( I + 1 ) e. NN )
5		nnuz 11723	. . . . . . . . . . 11 |- NN = ( ZZ>= ` 1 )
6	4, 5	syl6eleq 2711	. . . . . . . . . 10 |- ( ph -> ( I + 1 ) e. ( ZZ>= ` 1 ) )
7		dchrisumlem2.5	. . . . . . . . . . 11 |- ( ph -> J e. ( ZZ>= ` I ) )
8		eluzp1p1 11713	. . . . . . . . . . 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 12336	. . . . . . . . . 10 |- ( ( I + 1 ) e. ( 1 ... ( J + 1 ) ) <-> ( ( I + 1 ) e. ( ZZ>= ` 1 ) /\ ( J + 1 ) e. ( ZZ>= ` ( I + 1 ) ) ) )
11	6, 9, 10	sylanbrc 698	. . . . . . . . 9 |- ( ph -> ( I + 1 ) e. ( 1 ... ( J + 1 ) ) )
12		fzosplit 12501	. . . . . . . . 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 12773	. . . . . . . . 9 |- ( 1..^ ( J + 1 ) ) e. Fin
15	14	a1i 11	. . . . . . . 8 |- ( ph -> ( 1..^ ( J + 1 ) ) e. Fin )
16		elfzouz 12474	. . . . . . . . . 10 |- ( i e. ( 1..^ ( J + 1 ) ) -> i e. ( ZZ>= ` 1 ) )
17	16, 5	syl6eleqr 2712	. . . . . . . . 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 481	. . . . . . . . . . 11 |- ( ( ph /\ i e. NN ) -> X e. D )
24		nnz 11399	. . . . . . . . . . . 12 |- ( i e. NN -> i e. ZZ )
25	24	adantl 482	. . . . . . . . . . 11 |- ( ( ph /\ i e. NN ) -> i e. ZZ )
26	18, 19, 20, 21, 23, 25	dchrzrhcl 24970	. . . . . . . . . 10 |- ( ( ph /\ i e. NN ) -> ( X ` ( L ` i ) ) e. CC )
27		nnrp 11842	. . . . . . . . . . . . 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 25177	. . . . . . . . . . . . . 14 |- ( ph -> ( ( i e. RR+ -> [_ i / n ]_ A e. RR ) /\ ( i e. ( M [,) +oo ) -> 0 <_ [_ i / n ]_ A ) ) )
38	37	simpld 475	. . . . . . . . . . . . 13 |- ( ph -> ( i e. RR+ -> [_ i / n ]_ A e. RR ) )
39	27, 38	syl5 34	. . . . . . . . . . . 12 |- ( ph -> ( i e. NN -> [_ i / n ]_ A e. RR ) )
40	39	imp 445	. . . . . . . . . . 11 |- ( ( ph /\ i e. NN ) -> [_ i / n ]_ A e. RR )
41	40	recnd 10068	. . . . . . . . . 10 |- ( ( ph /\ i e. NN ) -> [_ i / n ]_ A e. CC )
42	26, 41	mulcld 10060	. . . . . . . . 9 |- ( ( ph /\ i e. NN ) -> ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) e. CC )
43	17, 42	sylan2 491	. . . . . . . 8 |- ( ( ph /\ i e. ( 1..^ ( J + 1 ) ) ) -> ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) e. CC )
44	2, 13, 15, 43	fsumsplit 14471	. . . . . . 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 11697	. . . . . . . . 9 |- ( J e. ( ZZ>= ` I ) -> J e. ZZ )
46		fzval3 12536	. . . . . . . . 9 |- ( J e. ZZ -> ( 1 ... J ) = ( 1..^ ( J + 1 ) ) )
47	7, 45, 46	3syl 18	. . . . . . . 8 |- ( ph -> ( 1 ... J ) = ( 1..^ ( J + 1 ) ) )
48	47	sumeq1d 14431	. . . . . . 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 11481	. . . . . . . . . 10 |- ( ph -> I e. ZZ )
50		fzval3 12536	. . . . . . . . . 10 |- ( I e. ZZ -> ( 1 ... I ) = ( 1..^ ( I + 1 ) ) )
51	49, 50	syl 17	. . . . . . . . 9 |- ( ph -> ( 1 ... I ) = ( 1..^ ( I + 1 ) ) )
52	51	sumeq1d 14431	. . . . . . . 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 6665	. . . . . . 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 2666	. . . . . 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 12370	. . . . . . . 8 |- ( i e. ( 1 ... J ) -> i e. NN )
56		simpr 477	. . . . . . . . 9 |- ( ( ph /\ i e. NN ) -> i e. NN )
57		nfcv 2764	. . . . . . . . . 10 |- F/_ n i
58		nfcv 2764	. . . . . . . . . . 11 |- F/_ n ( X ` ( L ` i ) )
59		nfcv 2764	. . . . . . . . . . 11 |- F/_ n x.
60		nfcsb1v 3549	. . . . . . . . . . 11 |- F/_ n [_ i / n ]_ A
61	58, 59, 60	nfov 6676	. . . . . . . . . 10 |- F/_ n ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A )
62		fveq2 6191	. . . . . . . . . . . 12 |- ( n = i -> ( L ` n ) = ( L ` i ) )
63	62	fveq2d 6195	. . . . . . . . . . 11 |- ( n = i -> ( X ` ( L ` n ) ) = ( X ` ( L ` i ) ) )
64		csbeq1a 3542	. . . . . . . . . . 11 |- ( n = i -> A = [_ i / n ]_ A )
65	63, 64	oveq12d 6668	. . . . . . . . . 10 |- ( n = i -> ( ( X ` ( L ` n ) ) x. A ) = ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) )
66	57, 61, 65, 36	fvmptf 6301	. . . . . . . . 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 693	. . . . . . . 8 |- ( ( ph /\ i e. NN ) -> ( F ` i ) = ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) )
68	55, 67	sylan2 491	. . . . . . 7 |- ( ( ph /\ i e. ( 1 ... J ) ) -> ( F ` i ) = ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) )
69	3, 5	syl6eleq 2711	. . . . . . . 8 |- ( ph -> I e. ( ZZ>= ` 1 ) )
70		uztrn 11704	. . . . . . . 8 |- ( ( J e. ( ZZ>= ` I ) /\ I e. ( ZZ>= ` 1 ) ) -> J e. ( ZZ>= ` 1 ) )
71	7, 69, 70	syl2anc 693	. . . . . . 7 |- ( ph -> J e. ( ZZ>= ` 1 ) )
72	55, 42	sylan2 491	. . . . . . 7 |- ( ( ph /\ i e. ( 1 ... J ) ) -> ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) e. CC )
73	68, 71, 72	fsumser 14461	. . . . . 6 |- ( ph -> sum_ i e. ( 1 ... J ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) = ( seq 1 ( + , F ) ` J ) )
74	54, 73	eqtr3d 2658	. . . . 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 12370	. . . . . . 7 |- ( i e. ( 1 ... I ) -> i e. NN )
76	75, 67	sylan2 491	. . . . . 6 |- ( ( ph /\ i e. ( 1 ... I ) ) -> ( F ` i ) = ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) )
77	75, 42	sylan2 491	. . . . . 6 |- ( ( ph /\ i e. ( 1 ... I ) ) -> ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) e. CC )
78	76, 69, 77	fsumser 14461	. . . . 5 |- ( ph -> sum_ i e. ( 1 ... I ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) = ( seq 1 ( + , F ) ` I ) )
79	74, 78	oveq12d 6668	. . . 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 12772	. . . . . 6 |- ( ph -> ( 1 ... I ) e. Fin )
81	80, 77	fsumcl 14464	. . . . 5 |- ( ph -> sum_ i e. ( 1 ... I ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) e. CC )
82		fzofi 12773	. . . . . . 7 |- ( ( I + 1 )..^ ( J + 1 ) ) e. Fin
83	82	a1i 11	. . . . . 6 |- ( ph -> ( ( I + 1 )..^ ( J + 1 ) ) e. Fin )
84		ssun2 3777	. . . . . . . . 9 |- ( ( I + 1 )..^ ( J + 1 ) ) C_ ( ( 1..^ ( I + 1 ) ) u. ( ( I + 1 )..^ ( J + 1 ) ) )
85	84, 13	syl5sseqr 3654	. . . . . . . 8 |- ( ph -> ( ( I + 1 )..^ ( J + 1 ) ) C_ ( 1..^ ( J + 1 ) ) )
86	85	sselda 3603	. . . . . . 7 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> i e. ( 1..^ ( J + 1 ) ) )
87	86, 43	syldan 487	. . . . . 6 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) e. CC )
88	83, 87	fsumcl 14464	. . . . 5 |- ( ph -> sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) e. CC )
89	81, 88	pncan2d 10394	. . . 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 2658	. . 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 6195	. 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 14175	. . 3 |- ( ph -> ( abs ` sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) ) e. RR )
93		2re 11090	. . . . . 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 10070	. . . 4 |- ( ph -> ( 2 x. R ) e. RR )
97	40	ralrimiva 2966	. . . . 5 |- ( ph -> A. i e. NN [_ i / n ]_ A e. RR )
98		csbeq1 3536	. . . . . . 7 |- ( i = ( I + 1 ) -> [_ i / n ]_ A = [_ ( I + 1 ) / n ]_ A )
99	98	eleq1d 2686	. . . . . 6 |- ( i = ( I + 1 ) -> ( [_ i / n ]_ A e. RR <-> [_ ( I + 1 ) / n ]_ A e. RR ) )
100	99	rspcv 3305	. . . . 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 65	. . . 4 |- ( ph -> [_ ( I + 1 ) / n ]_ A e. RR )
102	96, 101	remulcld 10070	. . 3 |- ( ph -> ( ( 2 x. R ) x. [_ ( I + 1 ) / n ]_ A ) e. RR )
103		dchrisumlem2.1	. . . . 5 |- ( ph -> U e. RR+ )
104	33	ralrimiva 2966	. . . . 5 |- ( ph -> A. n e. RR+ A e. RR )
105		nfcsb1v 3549	. . . . . . 7 |- F/_ n [_ U / n ]_ A
106	105	nfel1 2779	. . . . . 6 |- F/ n [_ U / n ]_ A e. RR
107		csbeq1a 3542	. . . . . . 7 |- ( n = U -> A = [_ U / n ]_ A )
108	107	eleq1d 2686	. . . . . 6 |- ( n = U -> ( A e. RR <-> [_ U / n ]_ A e. RR ) )
109	106, 108	rspc 3303	. . . . 5 |- ( U e. RR+ -> ( A. n e. RR+ A e. RR -> [_ U / n ]_ A e. RR ) )
110	103, 104, 109	sylc 65	. . . 4 |- ( ph -> [_ U / n ]_ A e. RR )
111	96, 110	remulcld 10070	. . 3 |- ( ph -> ( ( 2 x. R ) x. [_ U / n ]_ A ) e. RR )
112	71, 5	syl6eleqr 2712	. . . . . . . . . . . 12 |- ( ph -> J e. NN )
113	112	peano2nnd 11037	. . . . . . . . . . 11 |- ( ph -> ( J + 1 ) e. NN )
114	113	nnrpd 11870	. . . . . . . . . 10 |- ( ph -> ( J + 1 ) e. RR+ )
115	19, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36	dchrisumlema 25177	. . . . . . . . . . 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 475	. . . . . . . . . 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 10068	. . . . . . . 8 |- ( ph -> [_ ( J + 1 ) / n ]_ A e. CC )
119		fzofi 12773	. . . . . . . . . 10 |- ( 0..^ ( J + 1 ) ) e. Fin
120	119	a1i 11	. . . . . . . . 9 |- ( ph -> ( 0..^ ( J + 1 ) ) e. Fin )
121		elfzoelz 12470	. . . . . . . . . 10 |- ( n e. ( 0..^ ( J + 1 ) ) -> n e. ZZ )
122	22	adantr 481	. . . . . . . . . . 11 |- ( ( ph /\ n e. ZZ ) -> X e. D )
123		simpr 477	. . . . . . . . . . 11 |- ( ( ph /\ n e. ZZ ) -> n e. ZZ )
124	18, 19, 20, 21, 122, 123	dchrzrhcl 24970	. . . . . . . . . 10 |- ( ( ph /\ n e. ZZ ) -> ( X ` ( L ` n ) ) e. CC )
125	121, 124	sylan2 491	. . . . . . . . 9 |- ( ( ph /\ n e. ( 0..^ ( J + 1 ) ) ) -> ( X ` ( L ` n ) ) e. CC )
126	120, 125	fsumcl 14464	. . . . . . . 8 |- ( ph -> sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) e. CC )
127	118, 126	mulcld 10060	. . . . . . 7 |- ( ph -> ( [_ ( J + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) e. CC )
128	101	recnd 10068	. . . . . . . 8 |- ( ph -> [_ ( I + 1 ) / n ]_ A e. CC )
129		fzofi 12773	. . . . . . . . . 10 |- ( 0..^ ( I + 1 ) ) e. Fin
130	129	a1i 11	. . . . . . . . 9 |- ( ph -> ( 0..^ ( I + 1 ) ) e. Fin )
131		elfzoelz 12470	. . . . . . . . . 10 |- ( n e. ( 0..^ ( I + 1 ) ) -> n e. ZZ )
132	131, 124	sylan2 491	. . . . . . . . 9 |- ( ( ph /\ n e. ( 0..^ ( I + 1 ) ) ) -> ( X ` ( L ` n ) ) e. CC )
133	130, 132	fsumcl 14464	. . . . . . . 8 |- ( ph -> sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) e. CC )
134	128, 133	mulcld 10060	. . . . . . 7 |- ( ph -> ( [_ ( I + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) e. CC )
135	127, 134	subcld 10392	. . . . . 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 14175	. . . . 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 11032	. . . . . . . . . . . . 13 |- ( i e. NN -> ( i + 1 ) e. NN )
139	138	nnrpd 11870	. . . . . . . . . . . 12 |- ( i e. NN -> ( i + 1 ) e. RR+ )
140		nfcsb1v 3549	. . . . . . . . . . . . . . 15 |- F/_ n [_ ( i + 1 ) / n ]_ A
141	140	nfel1 2779	. . . . . . . . . . . . . 14 |- F/ n [_ ( i + 1 ) / n ]_ A e. RR
142		csbeq1a 3542	. . . . . . . . . . . . . . 15 |- ( n = ( i + 1 ) -> A = [_ ( i + 1 ) / n ]_ A )
143	142	eleq1d 2686	. . . . . . . . . . . . . 14 |- ( n = ( i + 1 ) -> ( A e. RR <-> [_ ( i + 1 ) / n ]_ A e. RR ) )
144	141, 143	rspc 3303	. . . . . . . . . . . . 13 |- ( ( i + 1 ) e. RR+ -> ( A. n e. RR+ A e. RR -> [_ ( i + 1 ) / n ]_ A e. RR ) )
145	144	impcom 446	. . . . . . . . . . . 12 |- ( ( A. n e. RR+ A e. RR /\ ( i + 1 ) e. RR+ ) -> [_ ( i + 1 ) / n ]_ A e. RR )
146	104, 139, 145	syl2an 494	. . . . . . . . . . 11 |- ( ( ph /\ i e. NN ) -> [_ ( i + 1 ) / n ]_ A e. RR )
147	146, 40	resubcld 10458	. . . . . . . . . 10 |- ( ( ph /\ i e. NN ) -> ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) e. RR )
148	147	recnd 10068	. . . . . . . . 9 |- ( ( ph /\ i e. NN ) -> ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) e. CC )
149		fzofi 12773	. . . . . . . . . . . 12 |- ( 0..^ ( i + 1 ) ) e. Fin
150	149	a1i 11	. . . . . . . . . . 11 |- ( ph -> ( 0..^ ( i + 1 ) ) e. Fin )
151		elfzoelz 12470	. . . . . . . . . . . 12 |- ( n e. ( 0..^ ( i + 1 ) ) -> n e. ZZ )
152	151, 124	sylan2 491	. . . . . . . . . . 11 |- ( ( ph /\ n e. ( 0..^ ( i + 1 ) ) ) -> ( X ` ( L ` n ) ) e. CC )
153	150, 152	fsumcl 14464	. . . . . . . . . 10 |- ( ph -> sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) e. CC )
154	153	adantr 481	. . . . . . . . 9 |- ( ( ph /\ i e. NN ) -> sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) e. CC )
155	148, 154	mulcld 10060	. . . . . . . 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 487	. . . . . . 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 14464	. . . . . 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 14175	. . . . 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 10069	. . . 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 10061	. . . . . . . . . 10 |- ( ( ph /\ i e. NN ) -> ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) = ( [_ i / n ]_ A x. ( X ` ( L ` i ) ) ) )
161		nnnn0 11299	. . . . . . . . . . . . . . . 16 |- ( i e. NN -> i e. NN0 )
162	161	adantl 482	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. NN ) -> i e. NN0 )
163		nn0uz 11722	. . . . . . . . . . . . . . 15 |- NN0 = ( ZZ>= ` 0 )
164	162, 163	syl6eleq 2711	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. NN ) -> i e. ( ZZ>= ` 0 ) )
165		elfzelz 12342	. . . . . . . . . . . . . . 15 |- ( n e. ( 0 ... i ) -> n e. ZZ )
166	124	adantlr 751	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. NN ) /\ n e. ZZ ) -> ( X ` ( L ` n ) ) e. CC )
167	165, 166	sylan2 491	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. NN ) /\ n e. ( 0 ... i ) ) -> ( X ` ( L ` n ) ) e. CC )
168	164, 167, 63	fzosump1 14481	. . . . . . . . . . . . 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 6665	. . . . . . . . . . . 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 12773	. . . . . . . . . . . . . . 15 |- ( 0..^ i ) e. Fin
171	170	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. NN ) -> ( 0..^ i ) e. Fin )
172		elfzoelz 12470	. . . . . . . . . . . . . . 15 |- ( n e. ( 0..^ i ) -> n e. ZZ )
173	172, 166	sylan2 491	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. NN ) /\ n e. ( 0..^ i ) ) -> ( X ` ( L ` n ) ) e. CC )
174	171, 173	fsumcl 14464	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. NN ) -> sum_ n e. ( 0..^ i ) ( X ` ( L ` n ) ) e. CC )
175	174, 26	pncan2d 10394	. . . . . . . . . . . 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 2657	. . . . . . . . . . 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 6666	. . . . . . . . . 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 2656	. . . . . . . . 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 487	. . . . . . . 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 14433	. . . . . . 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 3536	. . . . . . . . 9 |- ( k = i -> [_ k / n ]_ A = [_ i / n ]_ A )
182		oveq2 6658	. . . . . . . . . 10 |- ( k = i -> ( 0..^ k ) = ( 0..^ i ) )
183	182	sumeq1d 14431	. . . . . . . . 9 |- ( k = i -> sum_ n e. ( 0..^ k ) ( X ` ( L ` n ) ) = sum_ n e. ( 0..^ i ) ( X ` ( L ` n ) ) )
184	181, 183	jca 554	. . . . . . . 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 3536	. . . . . . . . 9 |- ( k = ( i + 1 ) -> [_ k / n ]_ A = [_ ( i + 1 ) / n ]_ A )
186		oveq2 6658	. . . . . . . . . 10 |- ( k = ( i + 1 ) -> ( 0..^ k ) = ( 0..^ ( i + 1 ) ) )
187	186	sumeq1d 14431	. . . . . . . . 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 554	. . . . . . . 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 3536	. . . . . . . . 9 |- ( k = ( I + 1 ) -> [_ k / n ]_ A = [_ ( I + 1 ) / n ]_ A )
190		oveq2 6658	. . . . . . . . . 10 |- ( k = ( I + 1 ) -> ( 0..^ k ) = ( 0..^ ( I + 1 ) ) )
191	190	sumeq1d 14431	. . . . . . . . 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 554	. . . . . . . 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 3536	. . . . . . . . 9 |- ( k = ( J + 1 ) -> [_ k / n ]_ A = [_ ( J + 1 ) / n ]_ A )
194		oveq2 6658	. . . . . . . . . 10 |- ( k = ( J + 1 ) -> ( 0..^ k ) = ( 0..^ ( J + 1 ) ) )
195	194	sumeq1d 14431	. . . . . . . . 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 554	. . . . . . . 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 12338	. . . . . . . . . 10 |- ( k e. ( ( I + 1 ) ... ( J + 1 ) ) -> k e. ( ZZ>= ` ( I + 1 ) ) )
198		eluznn 11758	. . . . . . . . . 10 |- ( ( ( I + 1 ) e. NN /\ k e. ( ZZ>= ` ( I + 1 ) ) ) -> k e. NN )
199	4, 197, 198	syl2an 494	. . . . . . . . 9 |- ( ( ph /\ k e. ( ( I + 1 ) ... ( J + 1 ) ) ) -> k e. NN )
200	41	ralrimiva 2966	. . . . . . . . . 10 |- ( ph -> A. i e. NN [_ i / n ]_ A e. CC )
201		csbeq1 3536	. . . . . . . . . . . 12 |- ( i = k -> [_ i / n ]_ A = [_ k / n ]_ A )
202	201	eleq1d 2686	. . . . . . . . . . 11 |- ( i = k -> ( [_ i / n ]_ A e. CC <-> [_ k / n ]_ A e. CC ) )
203	202	rspccva 3308	. . . . . . . . . 10 |- ( ( A. i e. NN [_ i / n ]_ A e. CC /\ k e. NN ) -> [_ k / n ]_ A e. CC )
204	200, 203	sylan 488	. . . . . . . . 9 |- ( ( ph /\ k e. NN ) -> [_ k / n ]_ A e. CC )
205	199, 204	syldan 487	. . . . . . . 8 |- ( ( ph /\ k e. ( ( I + 1 ) ... ( J + 1 ) ) ) -> [_ k / n ]_ A e. CC )
206		fzofi 12773	. . . . . . . . . . 11 |- ( 0..^ k ) e. Fin
207	206	a1i 11	. . . . . . . . . 10 |- ( ph -> ( 0..^ k ) e. Fin )
208		elfzoelz 12470	. . . . . . . . . . 11 |- ( n e. ( 0..^ k ) -> n e. ZZ )
209	208, 124	sylan2 491	. . . . . . . . . 10 |- ( ( ph /\ n e. ( 0..^ k ) ) -> ( X ` ( L ` n ) ) e. CC )
210	207, 209	fsumcl 14464	. . . . . . . . 9 |- ( ph -> sum_ n e. ( 0..^ k ) ( X ` ( L ` n ) ) e. CC )
211	210	adantr 481	. . . . . . . 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 14538	. . . . . . 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 2656	. . . . . 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 6195	. . . . 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 14197	. . . . 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 4675	. . . 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 10069	. . . . . . 7 |- ( ph -> ( [_ ( J + 1 ) / n ]_ A + [_ ( I + 1 ) / n ]_ A ) e. RR )
218	217, 95	remulcld 10070	. . . . . 6 |- ( ph -> ( ( [_ ( J + 1 ) / n ]_ A + [_ ( I + 1 ) / n ]_ A ) x. R ) e. RR )
219	181, 185, 189, 193, 9, 205	telfsumo 14534	. . . . . . . 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 487	. . . . . . . . . 10 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> [_ i / n ]_ A e. RR )
221	137, 146	syldan 487	. . . . . . . . . 10 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> [_ ( i + 1 ) / n ]_ A e. RR )
222	220, 221	resubcld 10458	. . . . . . . . 9 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) e. RR )
223	83, 222	fsumrecl 14465	. . . . . . . 8 |- ( ph -> sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) e. RR )
224	219, 223	eqeltrrd 2702	. . . . . . 7 |- ( ph -> ( [_ ( I + 1 ) / n ]_ A - [_ ( J + 1 ) / n ]_ A ) e. RR )
225	224, 95	remulcld 10070	. . . . . 6 |- ( ph -> ( ( [_ ( I + 1 ) / n ]_ A - [_ ( J + 1 ) / n ]_ A ) x. R ) e. RR )
226	127	abscld 14175	. . . . . . . 8 |- ( ph -> ( abs ` ( [_ ( J + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) ) e. RR )
227	134	abscld 14175	. . . . . . . 8 |- ( ph -> ( abs ` ( [_ ( I + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) ) e. RR )
228	226, 227	readdcld 10069	. . . . . . 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 14197	. . . . . . 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 10070	. . . . . . . . 9 |- ( ph -> ( [_ ( J + 1 ) / n ]_ A x. R ) e. RR )
231	101, 95	remulcld 10070	. . . . . . . . 9 |- ( ph -> ( [_ ( I + 1 ) / n ]_ A x. R ) e. RR )
232	118, 126	absmuld 14193	. . . . . . . . . . 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 11698	. . . . . . . . . . . . . . . . . . 19 |- ( i e. ( ZZ>= ` M ) -> i e. RR )
234	233	adantl 482	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> i e. RR )
235		eluzle 11700	. . . . . . . . . . . . . . . . . . 19 |- ( i e. ( ZZ>= ` M ) -> M <_ i )
236	235	adantl 482	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> M <_ i )
237	32	nnred 11035	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> M e. RR )
238	237	adantr 481	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> M e. RR )
239		elicopnf 12269	. . . . . . . . . . . . . . . . . . 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 957	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> i e. ( M [,) +oo ) )
242	241	ex 450	. . . . . . . . . . . . . . . 16 |- ( ph -> ( i e. ( ZZ>= ` M ) -> i e. ( M [,) +oo ) ) )
243	242	ssrdv 3609	. . . . . . . . . . . . . . 15 |- ( ph -> ( ZZ>= ` M ) C_ ( M [,) +oo ) )
244	32	nnzd 11481	. . . . . . . . . . . . . . . . 17 |- ( ph -> M e. ZZ )
245	49	peano2zd 11485	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( I + 1 ) e. ZZ )
246	103	rpred 11872	. . . . . . . . . . . . . . . . . 18 |- ( ph -> U e. RR )
247	4	nnred 11035	. . . . . . . . . . . . . . . . . 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 10194	. . . . . . . . . . . . . . . . 17 |- ( ph -> M <_ ( I + 1 ) )
251		eluz2 11693	. . . . . . . . . . . . . . . . 17 |- ( ( I + 1 ) e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ ( I + 1 ) e. ZZ /\ M <_ ( I + 1 ) ) )
252	244, 245, 250, 251	syl3anbrc 1246	. . . . . . . . . . . . . . . 16 |- ( ph -> ( I + 1 ) e. ( ZZ>= ` M ) )
253		uztrn 11704	. . . . . . . . . . . . . . . 16 |- ( ( ( J + 1 ) e. ( ZZ>= ` ( I + 1 ) ) /\ ( I + 1 ) e. ( ZZ>= ` M ) ) -> ( J + 1 ) e. ( ZZ>= ` M ) )
254	9, 252, 253	syl2anc 693	. . . . . . . . . . . . . . 15 |- ( ph -> ( J + 1 ) e. ( ZZ>= ` M ) )
255	243, 254	sseldd 3604	. . . . . . . . . . . . . 14 |- ( ph -> ( J + 1 ) e. ( M [,) +oo ) )
256	115	simprd 479	. . . . . . . . . . . . . 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 14161	. . . . . . . . . . . 12 |- ( ph -> ( abs ` [_ ( J + 1 ) / n ]_ A ) = [_ ( J + 1 ) / n ]_ A )
259	258	oveq1d 6665	. . . . . . . . . . 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 2656	. . . . . . . . . 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 14175	. . . . . . . . . . 11 |- ( ph -> ( abs ` sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) e. RR )
262	113	nnnn0d 11351	. . . . . . . . . . . 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 25178	. . . . . . . . . . . 12 |- ( ( ph /\ ( J + 1 ) e. NN0 ) -> ( abs ` sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) <_ R )
265	262, 264	mpdan 702	. . . . . . . . . . 11 |- ( ph -> ( abs ` sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) <_ R )
266	261, 95, 117, 257, 265	lemul2ad 10964	. . . . . . . . . 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 4675	. . . . . . . . 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 14193	. . . . . . . . . . 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 3604	. . . . . . . . . . . . . 14 |- ( ph -> ( I + 1 ) e. ( M [,) +oo ) )
270	19, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36	dchrisumlema 25177	. . . . . . . . . . . . . . 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 479	. . . . . . . . . . . . . 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 14161	. . . . . . . . . . . 12 |- ( ph -> ( abs ` [_ ( I + 1 ) / n ]_ A ) = [_ ( I + 1 ) / n ]_ A )
274	273	oveq1d 6665	. . . . . . . . . . 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 2656	. . . . . . . . . 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 14175	. . . . . . . . . . 11 |- ( ph -> ( abs ` sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) e. RR )
277	4	nnnn0d 11351	. . . . . . . . . . . 12 |- ( ph -> ( I + 1 ) e. NN0 )
278	19, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36, 95, 263	dchrisumlem1 25178	. . . . . . . . . . . 12 |- ( ( ph /\ ( I + 1 ) e. NN0 ) -> ( abs ` sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) <_ R )
279	277, 278	mpdan 702	. . . . . . . . . . 11 |- ( ph -> ( abs ` sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) <_ R )
280	276, 95, 101, 272, 279	lemul2ad 10964	. . . . . . . . . 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 4675	. . . . . . . . 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 10646	. . . . . . . 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 10068	. . . . . . . . 9 |- ( ph -> R e. CC )
284	118, 128, 283	adddird 10065	. . . . . . . 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 4681	. . . . . . 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 10194	. . . . . 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 14175	. . . . . . . 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 14465	. . . . . . 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 14533	. . . . . . 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 481	. . . . . . . . . 10 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> R e. RR )
291	222, 290	remulcld 10070	. . . . . . . . 9 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) x. R ) e. RR )
292	137, 148	syldan 487	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) e. CC )
293	153	adantr 481	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) e. CC )
294	292, 293	absmuld 14193	. . . . . . . . . . 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 12474	. . . . . . . . . . . . . . 15 |- ( i e. ( ( I + 1 )..^ ( J + 1 ) ) -> i e. ( ZZ>= ` ( I + 1 ) ) )
296		uztrn 11704	. . . . . . . . . . . . . . 15 |- ( ( i e. ( ZZ>= ` ( I + 1 ) ) /\ ( I + 1 ) e. ( ZZ>= ` M ) ) -> i e. ( ZZ>= ` M ) )
297	295, 252, 296	syl2anr 495	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> i e. ( ZZ>= ` M ) )
298		eluznn 11758	. . . . . . . . . . . . . . . . 17 |- ( ( M e. NN /\ i e. ( ZZ>= ` M ) ) -> i e. NN )
299	32, 298	sylan 488	. . . . . . . . . . . . . . . 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 11870	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> i e. RR+ )
302	34	3expia 1267	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) ) -> ( ( M <_ n /\ n <_ x ) -> B <_ A ) )
303	302	ralrimivva 2971	. . . . . . . . . . . . . . . . 17 |- ( ph -> A. n e. RR+ A. x e. RR+ ( ( M <_ n /\ n <_ x ) -> B <_ A ) )
304	303	adantr 481	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> A. n e. RR+ A. x e. RR+ ( ( M <_ n /\ n <_ x ) -> B <_ A ) )
305		nfcv 2764	. . . . . . . . . . . . . . . . . 18 |- F/_ n RR+
306		nfv 1843	. . . . . . . . . . . . . . . . . . 19 |- F/ n ( M <_ i /\ i <_ x )
307		nfcv 2764	. . . . . . . . . . . . . . . . . . . 20 |- F/_ n B
308		nfcv 2764	. . . . . . . . . . . . . . . . . . . 20 |- F/_ n <_
309	307, 308, 60	nfbr 4699	. . . . . . . . . . . . . . . . . . 19 |- F/ n B <_ [_ i / n ]_ A
310	306, 309	nfim 1825	. . . . . . . . . . . . . . . . . 18 |- F/ n ( ( M <_ i /\ i <_ x ) -> B <_ [_ i / n ]_ A )
311	305, 310	nfral 2945	. . . . . . . . . . . . . . . . 17 |- F/ n A. x e. RR+ ( ( M <_ i /\ i <_ x ) -> B <_ [_ i / n ]_ A )
312		breq2 4657	. . . . . . . . . . . . . . . . . . . 20 |- ( n = i -> ( M <_ n <-> M <_ i ) )
313		breq1 4656	. . . . . . . . . . . . . . . . . . . 20 |- ( n = i -> ( n <_ x <-> i <_ x ) )
314	312, 313	anbi12d 747	. . . . . . . . . . . . . . . . . . 19 |- ( n = i -> ( ( M <_ n /\ n <_ x ) <-> ( M <_ i /\ i <_ x ) ) )
315	64	breq2d 4665	. . . . . . . . . . . . . . . . . . 19 |- ( n = i -> ( B <_ A <-> B <_ [_ i / n ]_ A ) )
316	314, 315	imbi12d 334	. . . . . . . . . . . . . . . . . 18 |- ( n = i -> ( ( ( M <_ n /\ n <_ x ) -> B <_ A ) <-> ( ( M <_ i /\ i <_ x ) -> B <_ [_ i / n ]_ A ) ) )
317	316	ralbidv 2986	. . . . . . . . . . . . . . . . 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 3303	. . . . . . . . . . . . . . . 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 65	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> A. x e. RR+ ( ( M <_ i /\ i <_ x ) -> B <_ [_ i / n ]_ A ) )
320	234	lep1d 10955	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> i <_ ( i + 1 ) )
321	236, 320	jca 554	. . . . . . . . . . . . . . 15 |- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> ( M <_ i /\ i <_ ( i + 1 ) ) )
322		breq2 4657	. . . . . . . . . . . . . . . . . 18 |- ( x = ( i + 1 ) -> ( i <_ x <-> i <_ ( i + 1 ) ) )
323	322	anbi2d 740	. . . . . . . . . . . . . . . . 17 |- ( x = ( i + 1 ) -> ( ( M <_ i /\ i <_ x ) <-> ( M <_ i /\ i <_ ( i + 1 ) ) ) )
324		eqvisset 3211	. . . . . . . . . . . . . . . . . . . 20 |- ( x = ( i + 1 ) -> ( i + 1 ) e. _V )
325		eqtr3 2643	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( x = ( i + 1 ) /\ n = ( i + 1 ) ) -> x = n )
326	31	equcoms 1947	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = n -> A = B )
327	325, 326	syl 17	. . . . . . . . . . . . . . . . . . . 20 |- ( ( x = ( i + 1 ) /\ n = ( i + 1 ) ) -> A = B )
328	324, 327	csbied 3560	. . . . . . . . . . . . . . . . . . 19 |- ( x = ( i + 1 ) -> [_ ( i + 1 ) / n ]_ A = B )
329	328	eqcomd 2628	. . . . . . . . . . . . . . . . . 18 |- ( x = ( i + 1 ) -> B = [_ ( i + 1 ) / n ]_ A )
330	329	breq1d 4663	. . . . . . . . . . . . . . . . 17 |- ( x = ( i + 1 ) -> ( B <_ [_ i / n ]_ A <-> [_ ( i + 1 ) / n ]_ A <_ [_ i / n ]_ A ) )
331	323, 330	imbi12d 334	. . . . . . . . . . . . . . . 16 |- ( x = ( i + 1 ) -> ( ( ( M <_ i /\ i <_ x ) -> B <_ [_ i / n ]_ A ) <-> ( ( M <_ i /\ i <_ ( i + 1 ) ) -> [_ ( i + 1 ) / n ]_ A <_ [_ i / n ]_ A ) ) )
332	331	rspcv 3305	. . . . . . . . . . . . . . 15 |- ( ( i + 1 ) e. RR+ -> ( A. x e. RR+ ( ( M <_ i /\ i <_ x ) -> B <_ [_ i / n ]_ A ) -> ( ( M <_ i /\ i <_ ( i + 1 ) ) -> [_ ( i + 1 ) / n ]_ A <_ [_ i / n ]_ A ) ) )
333	300, 319, 321, 332	syl3c 66	. . . . . . . . . . . . . 14 |- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> [_ ( i + 1 ) / n ]_ A <_ [_ i / n ]_ A )
334	297, 333	syldan 487	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> [_ ( i + 1 ) / n ]_ A <_ [_ i / n ]_ A )
335	221, 220, 334	abssuble0d 14171	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( abs ` ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) ) = ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) )
336	335	oveq1d 6665	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( ( abs ` ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) ) x. ( abs ` sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) ) = ( ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) x. ( abs ` sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) ) )
337	294, 336	eqtrd 2656	. . . . . . . . . 10 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( abs ` ( ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) x. sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) ) = ( ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) x. ( abs ` sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) ) )
338	293	abscld 14175	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( abs ` sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) e. RR )
339	220, 221	subge0d 10617	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( 0 <_ ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) <-> [_ ( i + 1 ) / n ]_ A <_ [_ i / n ]_ A ) )
340	334, 339	mpbird 247	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> 0 <_ ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) )
341	137	peano2nnd 11037	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( i + 1 ) e. NN )
342	341	nnnn0d 11351	. . . . . . . . . . . 12 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( i + 1 ) e. NN0 )
343	19, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36, 95, 263	dchrisumlem1 25178	. . . . . . . . . . . 12 |- ( ( ph /\ ( i + 1 ) e. NN0 ) -> ( abs ` sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) <_ R )
344	342, 343	syldan 487	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( abs ` sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) <_ R )
345	338, 290, 222, 340, 344	lemul2ad 10964	. . . . . . . . . 10 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) x. ( abs ` sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) ) <_ ( ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) x. R ) )
346	337, 345	eqbrtrd 4675	. . . . . . . . 9 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( abs ` ( ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) x. sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) ) <_ ( ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) x. R ) )
347	83, 287, 291, 346	fsumle 14531	. . . . . . . 8 |- ( ph -> sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( abs ` ( ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) x. sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) ) <_ sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) x. R ) )
348	222	recnd 10068	. . . . . . . . . 10 |- ( ( ph /\ i e. ( ( I + 1 )..^ ( J + 1 ) ) ) -> ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) e. CC )
349	83, 283, 348	fsummulc1 14517	. . . . . . . . 9 |- ( ph -> ( sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) x. R ) = sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) x. R ) )
350	219	oveq1d 6665	. . . . . . . . 9 |- ( ph -> ( sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) x. R ) = ( ( [_ ( I + 1 ) / n ]_ A - [_ ( J + 1 ) / n ]_ A ) x. R ) )
351	349, 350	eqtr3d 2658	. . . . . . . 8 |- ( ph -> sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) x. R ) = ( ( [_ ( I + 1 ) / n ]_ A - [_ ( J + 1 ) / n ]_ A ) x. R ) )
352	347, 351	breqtrd 4679	. . . . . . 7 |- ( ph -> sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( abs ` ( ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) x. sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) ) <_ ( ( [_ ( I + 1 ) / n ]_ A - [_ ( J + 1 ) / n ]_ A ) x. R ) )
353	158, 288, 225, 289, 352	letrd 10194	. . . . . 6 |- ( ph -> ( abs ` sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) x. sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) ) <_ ( ( [_ ( I + 1 ) / n ]_ A - [_ ( J + 1 ) / n ]_ A ) x. R ) )
354	136, 158, 218, 225, 286, 353	le2addd 10646	. . . . 5 |- ( ph -> ( ( abs ` ( ( [_ ( J + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) - ( [_ ( I + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) ) ) + ( abs ` sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) x. sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) ) ) <_ ( ( ( [_ ( J + 1 ) / n ]_ A + [_ ( I + 1 ) / n ]_ A ) x. R ) + ( ( [_ ( I + 1 ) / n ]_ A - [_ ( J + 1 ) / n ]_ A ) x. R ) ) )
355	128	2timesd 11275	. . . . . . . 8 |- ( ph -> ( 2 x. [_ ( I + 1 ) / n ]_ A ) = ( [_ ( I + 1 ) / n ]_ A + [_ ( I + 1 ) / n ]_ A ) )
356	128, 118, 128	ppncand 10432	. . . . . . . 8 |- ( ph -> ( ( [_ ( I + 1 ) / n ]_ A + [_ ( J + 1 ) / n ]_ A ) + ( [_ ( I + 1 ) / n ]_ A - [_ ( J + 1 ) / n ]_ A ) ) = ( [_ ( I + 1 ) / n ]_ A + [_ ( I + 1 ) / n ]_ A ) )
357	128, 118	addcomd 10238	. . . . . . . . 9 |- ( ph -> ( [_ ( I + 1 ) / n ]_ A + [_ ( J + 1 ) / n ]_ A ) = ( [_ ( J + 1 ) / n ]_ A + [_ ( I + 1 ) / n ]_ A ) )
358	357	oveq1d 6665	. . . . . . . 8 |- ( ph -> ( ( [_ ( I + 1 ) / n ]_ A + [_ ( J + 1 ) / n ]_ A ) + ( [_ ( I + 1 ) / n ]_ A - [_ ( J + 1 ) / n ]_ A ) ) = ( ( [_ ( J + 1 ) / n ]_ A + [_ ( I + 1 ) / n ]_ A ) + ( [_ ( I + 1 ) / n ]_ A - [_ ( J + 1 ) / n ]_ A ) ) )
359	355, 356, 358	3eqtr2d 2662	. . . . . . 7 |- ( ph -> ( 2 x. [_ ( I + 1 ) / n ]_ A ) = ( ( [_ ( J + 1 ) / n ]_ A + [_ ( I + 1 ) / n ]_ A ) + ( [_ ( I + 1 ) / n ]_ A - [_ ( J + 1 ) / n ]_ A ) ) )
360	359	oveq1d 6665	. . . . . 6 |- ( ph -> ( ( 2 x. [_ ( I + 1 ) / n ]_ A ) x. R ) = ( ( ( [_ ( J + 1 ) / n ]_ A + [_ ( I + 1 ) / n ]_ A ) + ( [_ ( I + 1 ) / n ]_ A - [_ ( J + 1 ) / n ]_ A ) ) x. R ) )
361		2cnd 11093	. . . . . . 7 |- ( ph -> 2 e. CC )
362	361, 128, 283	mul32d 10246	. . . . . 6 |- ( ph -> ( ( 2 x. [_ ( I + 1 ) / n ]_ A ) x. R ) = ( ( 2 x. R ) x. [_ ( I + 1 ) / n ]_ A ) )
363	217	recnd 10068	. . . . . . 7 |- ( ph -> ( [_ ( J + 1 ) / n ]_ A + [_ ( I + 1 ) / n ]_ A ) e. CC )
364	224	recnd 10068	. . . . . . 7 |- ( ph -> ( [_ ( I + 1 ) / n ]_ A - [_ ( J + 1 ) / n ]_ A ) e. CC )
365	363, 364, 283	adddird 10065	. . . . . 6 |- ( ph -> ( ( ( [_ ( J + 1 ) / n ]_ A + [_ ( I + 1 ) / n ]_ A ) + ( [_ ( I + 1 ) / n ]_ A - [_ ( J + 1 ) / n ]_ A ) ) x. R ) = ( ( ( [_ ( J + 1 ) / n ]_ A + [_ ( I + 1 ) / n ]_ A ) x. R ) + ( ( [_ ( I + 1 ) / n ]_ A - [_ ( J + 1 ) / n ]_ A ) x. R ) ) )
366	360, 362, 365	3eqtr3d 2664	. . . . 5 |- ( ph -> ( ( 2 x. R ) x. [_ ( I + 1 ) / n ]_ A ) = ( ( ( [_ ( J + 1 ) / n ]_ A + [_ ( I + 1 ) / n ]_ A ) x. R ) + ( ( [_ ( I + 1 ) / n ]_ A - [_ ( J + 1 ) / n ]_ A ) x. R ) ) )
367	354, 366	breqtrrd 4681	. . . 4 |- ( ph -> ( ( abs ` ( ( [_ ( J + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) - ( [_ ( I + 1 ) / n ]_ A x. sum_ n e. ( 0..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) ) ) + ( abs ` sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) x. sum_ n e. ( 0..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) ) ) <_ ( ( 2 x. R ) x. [_ ( I + 1 ) / n ]_ A ) )
368	92, 159, 102, 216, 367	letrd 10194	. . 3 |- ( ph -> ( abs ` sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) ) <_ ( ( 2 x. R ) x. [_ ( I + 1 ) / n ]_ A ) )
369		2nn0 11309	. . . . . 6 |- 2 e. NN0
370		nn0ge0 11318	. . . . . 6 |- ( 2 e. NN0 -> 0 <_ 2 )
371	369, 370	mp1i 13	. . . . 5 |- ( ph -> 0 <_ 2 )
372		0red 10041	. . . . . 6 |- ( ph -> 0 e. RR )
373	126	absge0d 14183	. . . . . 6 |- ( ph -> 0 <_ ( abs ` sum_ n e. ( 0..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) )
374	372, 261, 95, 373, 265	letrd 10194	. . . . 5 |- ( ph -> 0 <_ R )
375	94, 95, 371, 374	mulge0d 10604	. . . 4 |- ( ph -> 0 <_ ( 2 x. R ) )
376	4	nnrpd 11870	. . . . 5 |- ( ph -> ( I + 1 ) e. RR+ )
377		nfv 1843	. . . . . . . . 9 |- F/ n ( M <_ U /\ U <_ x )
378	307, 308, 105	nfbr 4699	. . . . . . . . 9 |- F/ n B <_ [_ U / n ]_ A
379	377, 378	nfim 1825	. . . . . . . 8 |- F/ n ( ( M <_ U /\ U <_ x ) -> B <_ [_ U / n ]_ A )
380	305, 379	nfral 2945	. . . . . . 7 |- F/ n A. x e. RR+ ( ( M <_ U /\ U <_ x ) -> B <_ [_ U / n ]_ A )
381		breq2 4657	. . . . . . . . . 10 |- ( n = U -> ( M <_ n <-> M <_ U ) )
382		breq1 4656	. . . . . . . . . 10 |- ( n = U -> ( n <_ x <-> U <_ x ) )
383	381, 382	anbi12d 747	. . . . . . . . 9 |- ( n = U -> ( ( M <_ n /\ n <_ x ) <-> ( M <_ U /\ U <_ x ) ) )
384	107	breq2d 4665	. . . . . . . . 9 |- ( n = U -> ( B <_ A <-> B <_ [_ U / n ]_ A ) )
385	383, 384	imbi12d 334	. . . . . . . 8 |- ( n = U -> ( ( ( M <_ n /\ n <_ x ) -> B <_ A ) <-> ( ( M <_ U /\ U <_ x ) -> B <_ [_ U / n ]_ A ) ) )
386	385	ralbidv 2986	. . . . . . 7 |- ( n = U -> ( A. x e. RR+ ( ( M <_ n /\ n <_ x ) -> B <_ A ) <-> A. x e. RR+ ( ( M <_ U /\ U <_ x ) -> B <_ [_ U / n ]_ A ) ) )
387	380, 386	rspc 3303	. . . . . 6 |- ( U e. RR+ -> ( A. n e. RR+ A. x e. RR+ ( ( M <_ n /\ n <_ x ) -> B <_ A ) -> A. x e. RR+ ( ( M <_ U /\ U <_ x ) -> B <_ [_ U / n ]_ A ) ) )
388	103, 303, 387	sylc 65	. . . . 5 |- ( ph -> A. x e. RR+ ( ( M <_ U /\ U <_ x ) -> B <_ [_ U / n ]_ A ) )
389	248, 249	jca 554	. . . . 5 |- ( ph -> ( M <_ U /\ U <_ ( I + 1 ) ) )
390		breq2 4657	. . . . . . . 8 |- ( x = ( I + 1 ) -> ( U <_ x <-> U <_ ( I + 1 ) ) )
391	390	anbi2d 740	. . . . . . 7 |- ( x = ( I + 1 ) -> ( ( M <_ U /\ U <_ x ) <-> ( M <_ U /\ U <_ ( I + 1 ) ) ) )
392		eqvisset 3211	. . . . . . . . . 10 |- ( x = ( I + 1 ) -> ( I + 1 ) e. _V )
393		eqtr3 2643	. . . . . . . . . . 11 |- ( ( x = ( I + 1 ) /\ n = ( I + 1 ) ) -> x = n )
394	393, 326	syl 17	. . . . . . . . . 10 |- ( ( x = ( I + 1 ) /\ n = ( I + 1 ) ) -> A = B )
395	392, 394	csbied 3560	. . . . . . . . 9 |- ( x = ( I + 1 ) -> [_ ( I + 1 ) / n ]_ A = B )
396	395	eqcomd 2628	. . . . . . . 8 |- ( x = ( I + 1 ) -> B = [_ ( I + 1 ) / n ]_ A )
397	396	breq1d 4663	. . . . . . 7 |- ( x = ( I + 1 ) -> ( B <_ [_ U / n ]_ A <-> [_ ( I + 1 ) / n ]_ A <_ [_ U / n ]_ A ) )
398	391, 397	imbi12d 334	. . . . . 6 |- ( x = ( I + 1 ) -> ( ( ( M <_ U /\ U <_ x ) -> B <_ [_ U / n ]_ A ) <-> ( ( M <_ U /\ U <_ ( I + 1 ) ) -> [_ ( I + 1 ) / n ]_ A <_ [_ U / n ]_ A ) ) )
399	398	rspcv 3305	. . . . 5 |- ( ( I + 1 ) e. RR+ -> ( A. x e. RR+ ( ( M <_ U /\ U <_ x ) -> B <_ [_ U / n ]_ A ) -> ( ( M <_ U /\ U <_ ( I + 1 ) ) -> [_ ( I + 1 ) / n ]_ A <_ [_ U / n ]_ A ) ) )
400	376, 388, 389, 399	syl3c 66	. . . 4 |- ( ph -> [_ ( I + 1 ) / n ]_ A <_ [_ U / n ]_ A )
401	101, 110, 96, 375, 400	lemul2ad 10964	. . 3 |- ( ph -> ( ( 2 x. R ) x. [_ ( I + 1 ) / n ]_ A ) <_ ( ( 2 x. R ) x. [_ U / n ]_ A ) )
402	92, 102, 111, 368, 401	letrd 10194	. 2 |- ( ph -> ( abs ` sum_ i e. ( ( I + 1 )..^ ( J + 1 ) ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) ) <_ ( ( 2 x. R ) x. [_ U / n ]_ A ) )
403	91, 402	eqbrtrd 4675	1 |- ( ph -> ( abs ` ( ( seq 1 ( + , F ) ` J ) - ( seq 1 ( + , F ) ` I ) ) ) <_ ( ( 2 x. R ) x. [_ U / n ]_ A ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   =/= wne 2794   A.wral 2912   _Vcvv 3200   [_csb 3533   u. cun 3572   i^i cin 3573   (/)c0 3915   class class class wbr 4653   |-> cmpt 4729   ` cfv 5888  (class class class)co 6650   Fincfn 7955   CCcc 9934   RRcr 9935   0cc0 9936   1c1 9937   + caddc 9939   x. cmul 9941   +oocpnf 10071   <_ cle 10075   - cmin 10266   NNcn 11020   2c2 11070   NN0cn0 11292   ZZcz 11377   ZZ>=cuz 11687   RR+crp 11832   [,)cico 12177   ...cfz 12326  ..^cfzo 12465   seqcseq 12801   abscabs 13974   ~~> r crli 14216   sum_csu 14416   Basecbs 15857   0gc0g 16100   ZRHomczrh 19848  ℤ/nℤczn 19851  DChrcdchr 24957

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014  ax-addf 10015  ax-mulf 10016

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-of 6897  df-om 7066  df-1st 7168  df-2nd 7169  df-tpos 7352  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-ec 7744  df-qs 7748  df-map 7859  df-pm 7860  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-sup 8348  df-inf 8349  df-oi 8415  df-card 8765  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-4 11081  df-5 11082  df-6 11083  df-7 11084  df-8 11085  df-9 11086  df-n0 11293  df-xnn0 11364  df-z 11378  df-dec 11494  df-uz 11688  df-rp 11833  df-ico 12181  df-fz 12327  df-fzo 12466  df-fl 12593  df-mod 12669  df-seq 12802  df-exp 12861  df-hash 13118  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-clim 14219  df-rlim 14220  df-sum 14417  df-dvds 14984  df-gcd 15217  df-phi 15471  df-struct 15859  df-ndx 15860  df-slot 15861  df-base 15863  df-sets 15864  df-ress 15865  df-plusg 15954  df-mulr 15955  df-starv 15956  df-sca 15957  df-vsca 15958  df-ip 15959  df-tset 15960  df-ple 15961  df-ds 15964  df-unif 15965  df-0g 16102  df-imas 16168  df-qus 16169  df-mgm 17242  df-sgrp 17284  df-mnd 17295  df-mhm 17335  df-grp 17425  df-minusg 17426  df-sbg 17427  df-mulg 17541  df-subg 17591  df-nsg 17592  df-eqg 17593  df-ghm 17658  df-cmn 18195  df-abl 18196  df-mgp 18490  df-ur 18502  df-ring 18549  df-cring 18550  df-oppr 18623  df-dvdsr 18641  df-unit 18642  df-invr 18672  df-rnghom 18715  df-subrg 18778  df-lmod 18865  df-lss 18933  df-lsp 18972  df-sra 19172  df-rgmod 19173  df-lidl 19174  df-rsp 19175  df-2idl 19232  df-cnfld 19747  df-zring 19819  df-zrh 19852  df-zn 19855  df-dchr 24958

This theorem is referenced by:  dchrisumlem3  25180