Theorem dchrisumlem2

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

	Ref	Expression
Hypotheses	rpvmasum.z	|- Z = ( Z/nZ ` 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	dchrisumlem2	|- ( ph -> ( abs ` ( ( seq 1 ( + , F ) ` J ) - ( seq 1 ( + , F ) ` I ) ) ) <_ ( ( 2 x. R ) x. [_ U / n ]_ A ) )

Proof

Step	Hyp	Ref	Expression
1		rpvmasum.z	|- Z = ( Z/nZ ` N )
2		rpvmasum.l	|- L = ( ZRHom ` Z )
3		rpvmasum.a	|- ( ph -> N e. NN )
4		rpvmasum.g	|- G = ( DChr ` N )
5		rpvmasum.d	|- D = ( Base ` G )
6		rpvmasum.1	|- .1. = ( 0g ` G )
7		dchrisum.b	|- ( ph -> X e. D )
8		dchrisum.n1	|- ( ph -> X =/= .1. )
9		dchrisum.2	|- ( n = x -> A = B )
10		dchrisum.3	|- ( ph -> M e. NN )
11		dchrisum.4	|- ( ( ph /\ n e. RR+ ) -> A e. RR )
12		dchrisum.5	|- ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) /\ ( M <_ n /\ n <_ x ) ) -> B <_ A )
13		dchrisum.6	|- ( ph -> ( n e. RR+ |-> A ) ~~>r 0 )
14		dchrisum.7	|- F = ( n e. NN |-> ( ( X ` ( L ` n ) ) x. A ) )
15		dchrisum.9	|- ( ph -> R e. RR )
16		dchrisum.10	|- ( ph -> A. u e. ( 0 ..^ N ) ( abs ` sum_ n e. ( 0 ..^ u ) ( X ` ( L ` n ) ) ) <_ R )
17		dchrisumlem2.1	|- ( ph -> U e. RR+ )
18		dchrisumlem2.2	|- ( ph -> M <_ U )
19		dchrisumlem2.3	|- ( ph -> U <_ ( I + 1 ) )
20		dchrisumlem2.4	|- ( ph -> I e. NN )
21		dchrisumlem2.5	|- ( ph -> J e. ( ZZ>= ` I ) )
22		fzodisj	|- ( ( 1 ..^ ( I + 1 ) ) i^i ( ( I + 1 ) ..^ ( J + 1 ) ) ) = (/)
23	22	a1i	|- ( ph -> ( ( 1 ..^ ( I + 1 ) ) i^i ( ( I + 1 ) ..^ ( J + 1 ) ) ) = (/) )
24	20	peano2nnd	|- ( ph -> ( I + 1 ) e. NN )
25		nnuz	|- NN = ( ZZ>= ` 1 )
26	24 25	eleqtrdi	|- ( ph -> ( I + 1 ) e. ( ZZ>= ` 1 ) )
27		eluzp1p1	|- ( J e. ( ZZ>= ` I ) -> ( J + 1 ) e. ( ZZ>= ` ( I + 1 ) ) )
28	21 27	syl	|- ( ph -> ( J + 1 ) e. ( ZZ>= ` ( I + 1 ) ) )
29		elfzuzb	|- ( ( I + 1 ) e. ( 1 ... ( J + 1 ) ) <-> ( ( I + 1 ) e. ( ZZ>= ` 1 ) /\ ( J + 1 ) e. ( ZZ>= ` ( I + 1 ) ) ) )
30	26 28 29	sylanbrc	|- ( ph -> ( I + 1 ) e. ( 1 ... ( J + 1 ) ) )
31		fzosplit	|- ( ( I + 1 ) e. ( 1 ... ( J + 1 ) ) -> ( 1 ..^ ( J + 1 ) ) = ( ( 1 ..^ ( I + 1 ) ) u. ( ( I + 1 ) ..^ ( J + 1 ) ) ) )
32	30 31	syl	|- ( ph -> ( 1 ..^ ( J + 1 ) ) = ( ( 1 ..^ ( I + 1 ) ) u. ( ( I + 1 ) ..^ ( J + 1 ) ) ) )
33		fzofi	|- ( 1 ..^ ( J + 1 ) ) e. Fin
34	33	a1i	|- ( ph -> ( 1 ..^ ( J + 1 ) ) e. Fin )
35		elfzouz	|- ( i e. ( 1 ..^ ( J + 1 ) ) -> i e. ( ZZ>= ` 1 ) )
36	35 25	eleqtrrdi	|- ( i e. ( 1 ..^ ( J + 1 ) ) -> i e. NN )
37	7	adantr	|- ( ( ph /\ i e. NN ) -> X e. D )
38		nnz	|- ( i e. NN -> i e. ZZ )
39	38	adantl	|- ( ( ph /\ i e. NN ) -> i e. ZZ )
40	4 1 5 2 37 39	dchrzrhcl	|- ( ( ph /\ i e. NN ) -> ( X ` ( L ` i ) ) e. CC )
41	1 2 3 4 5 6 7 8 9 10 11 12 13 14	dchrisumlema	|- ( ph -> ( ( i e. RR+ -> [_ i / n ]_ A e. RR ) /\ ( i e. ( M [,) +oo ) -> 0 <_ [_ i / n ]_ A ) ) )
42	41	simpld	|- ( ph -> ( i e. RR+ -> [_ i / n ]_ A e. RR ) )
43		nnrp	|- ( i e. NN -> i e. RR+ )
44	42 43	impel	|- ( ( ph /\ i e. NN ) -> [_ i / n ]_ A e. RR )
45	44	recnd	|- ( ( ph /\ i e. NN ) -> [_ i / n ]_ A e. CC )
46	40 45	mulcld	|- ( ( ph /\ i e. NN ) -> ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) e. CC )
47	36 46	sylan2	|- ( ( ph /\ i e. ( 1 ..^ ( J + 1 ) ) ) -> ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) e. CC )
48	23 32 34 47	fsumsplit	|- ( 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 ) ) )
49		eluzelz	|- ( J e. ( ZZ>= ` I ) -> J e. ZZ )
50		fzval3	|- ( J e. ZZ -> ( 1 ... J ) = ( 1 ..^ ( J + 1 ) ) )
51	21 49 50	3syl	|- ( ph -> ( 1 ... J ) = ( 1 ..^ ( J + 1 ) ) )
52	51	sumeq1d	|- ( 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 ) )
53	20	nnzd	|- ( ph -> I e. ZZ )
54		fzval3	|- ( I e. ZZ -> ( 1 ... I ) = ( 1 ..^ ( I + 1 ) ) )
55	53 54	syl	|- ( ph -> ( 1 ... I ) = ( 1 ..^ ( I + 1 ) ) )
56	55	sumeq1d	|- ( 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 ) )
57	56	oveq1d	|- ( 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 ) ) )
58	48 52 57	3eqtr4d	|- ( 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 ) ) )
59		elfznn	|- ( i e. ( 1 ... J ) -> i e. NN )
60		simpr	|- ( ( ph /\ i e. NN ) -> i e. NN )
61		nfcv	|- F/_ n i
62		nfcv	|- F/_ n ( X ` ( L ` i ) )
63		nfcv	|- F/_ n x.
64		nfcsb1v	|- F/_ n [_ i / n ]_ A
65	62 63 64	nfov	|- F/_ n ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A )
66		2fveq3	|- ( n = i -> ( X ` ( L ` n ) ) = ( X ` ( L ` i ) ) )
67		csbeq1a	|- ( n = i -> A = [_ i / n ]_ A )
68	66 67	oveq12d	|- ( n = i -> ( ( X ` ( L ` n ) ) x. A ) = ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) )
69	61 65 68 14	fvmptf	|- ( ( i e. NN /\ ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) e. CC ) -> ( F ` i ) = ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) )
70	60 46 69	syl2anc	|- ( ( ph /\ i e. NN ) -> ( F ` i ) = ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) )
71	59 70	sylan2	|- ( ( ph /\ i e. ( 1 ... J ) ) -> ( F ` i ) = ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) )
72	20 25	eleqtrdi	|- ( ph -> I e. ( ZZ>= ` 1 ) )
73		uztrn	|- ( ( J e. ( ZZ>= ` I ) /\ I e. ( ZZ>= ` 1 ) ) -> J e. ( ZZ>= ` 1 ) )
74	21 72 73	syl2anc	|- ( ph -> J e. ( ZZ>= ` 1 ) )
75	59 46	sylan2	|- ( ( ph /\ i e. ( 1 ... J ) ) -> ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) e. CC )
76	71 74 75	fsumser	|- ( ph -> sum_ i e. ( 1 ... J ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) = ( seq 1 ( + , F ) ` J ) )
77	58 76	eqtr3d	|- ( 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 ) )
78		elfznn	|- ( i e. ( 1 ... I ) -> i e. NN )
79	78 70	sylan2	|- ( ( ph /\ i e. ( 1 ... I ) ) -> ( F ` i ) = ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) )
80	78 46	sylan2	|- ( ( ph /\ i e. ( 1 ... I ) ) -> ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) e. CC )
81	79 72 80	fsumser	|- ( ph -> sum_ i e. ( 1 ... I ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) = ( seq 1 ( + , F ) ` I ) )
82	77 81	oveq12d	|- ( 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 ) ) )
83		fzfid	|- ( ph -> ( 1 ... I ) e. Fin )
84	83 80	fsumcl	|- ( ph -> sum_ i e. ( 1 ... I ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) e. CC )
85		fzofi	|- ( ( I + 1 ) ..^ ( J + 1 ) ) e. Fin
86	85	a1i	|- ( ph -> ( ( I + 1 ) ..^ ( J + 1 ) ) e. Fin )
87		ssun2	|- ( ( I + 1 ) ..^ ( J + 1 ) ) C_ ( ( 1 ..^ ( I + 1 ) ) u. ( ( I + 1 ) ..^ ( J + 1 ) ) )
88	87 32	sseqtrrid	|- ( ph -> ( ( I + 1 ) ..^ ( J + 1 ) ) C_ ( 1 ..^ ( J + 1 ) ) )
89	88	sselda	|- ( ( ph /\ i e. ( ( I + 1 ) ..^ ( J + 1 ) ) ) -> i e. ( 1 ..^ ( J + 1 ) ) )
90	89 47	syldan	|- ( ( ph /\ i e. ( ( I + 1 ) ..^ ( J + 1 ) ) ) -> ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) e. CC )
91	86 90	fsumcl	|- ( ph -> sum_ i e. ( ( I + 1 ) ..^ ( J + 1 ) ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) e. CC )
92	84 91	pncan2d	|- ( 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 ) )
93	82 92	eqtr3d	|- ( ph -> ( ( seq 1 ( + , F ) ` J ) - ( seq 1 ( + , F ) ` I ) ) = sum_ i e. ( ( I + 1 ) ..^ ( J + 1 ) ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) )
94	93	fveq2d	|- ( 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 ) ) )
95	91	abscld	|- ( ph -> ( abs ` sum_ i e. ( ( I + 1 ) ..^ ( J + 1 ) ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) ) e. RR )
96		2re	|- 2 e. RR
97	96	a1i	|- ( ph -> 2 e. RR )
98	97 15	remulcld	|- ( ph -> ( 2 x. R ) e. RR )
99	44	ralrimiva	|- ( ph -> A. i e. NN [_ i / n ]_ A e. RR )
100		csbeq1	|- ( i = ( I + 1 ) -> [_ i / n ]_ A = [_ ( I + 1 ) / n ]_ A )
101	100	eleq1d	|- ( i = ( I + 1 ) -> ( [_ i / n ]_ A e. RR <-> [_ ( I + 1 ) / n ]_ A e. RR ) )
102	101	rspcv	|- ( ( I + 1 ) e. NN -> ( A. i e. NN [_ i / n ]_ A e. RR -> [_ ( I + 1 ) / n ]_ A e. RR ) )
103	24 99 102	sylc	|- ( ph -> [_ ( I + 1 ) / n ]_ A e. RR )
104	98 103	remulcld	|- ( ph -> ( ( 2 x. R ) x. [_ ( I + 1 ) / n ]_ A ) e. RR )
105	11	ralrimiva	|- ( ph -> A. n e. RR+ A e. RR )
106		nfcsb1v	|- F/_ n [_ U / n ]_ A
107	106	nfel1	|- F/ n [_ U / n ]_ A e. RR
108		csbeq1a	|- ( n = U -> A = [_ U / n ]_ A )
109	108	eleq1d	|- ( n = U -> ( A e. RR <-> [_ U / n ]_ A e. RR ) )
110	107 109	rspc	|- ( U e. RR+ -> ( A. n e. RR+ A e. RR -> [_ U / n ]_ A e. RR ) )
111	17 105 110	sylc	|- ( ph -> [_ U / n ]_ A e. RR )
112	98 111	remulcld	|- ( ph -> ( ( 2 x. R ) x. [_ U / n ]_ A ) e. RR )
113	74 25	eleqtrrdi	|- ( ph -> J e. NN )
114	113	peano2nnd	|- ( ph -> ( J + 1 ) e. NN )
115	114	nnrpd	|- ( ph -> ( J + 1 ) e. RR+ )
116	1 2 3 4 5 6 7 8 9 10 11 12 13 14	dchrisumlema	|- ( ph -> ( ( ( J + 1 ) e. RR+ -> [_ ( J + 1 ) / n ]_ A e. RR ) /\ ( ( J + 1 ) e. ( M [,) +oo ) -> 0 <_ [_ ( J + 1 ) / n ]_ A ) ) )
117	116	simpld	|- ( ph -> ( ( J + 1 ) e. RR+ -> [_ ( J + 1 ) / n ]_ A e. RR ) )
118	115 117	mpd	|- ( ph -> [_ ( J + 1 ) / n ]_ A e. RR )
119	118	recnd	|- ( ph -> [_ ( J + 1 ) / n ]_ A e. CC )
120		fzofi	|- ( 0 ..^ ( J + 1 ) ) e. Fin
121	120	a1i	|- ( ph -> ( 0 ..^ ( J + 1 ) ) e. Fin )
122		elfzoelz	|- ( n e. ( 0 ..^ ( J + 1 ) ) -> n e. ZZ )
123	7	adantr	|- ( ( ph /\ n e. ZZ ) -> X e. D )
124		simpr	|- ( ( ph /\ n e. ZZ ) -> n e. ZZ )
125	4 1 5 2 123 124	dchrzrhcl	|- ( ( ph /\ n e. ZZ ) -> ( X ` ( L ` n ) ) e. CC )
126	122 125	sylan2	|- ( ( ph /\ n e. ( 0 ..^ ( J + 1 ) ) ) -> ( X ` ( L ` n ) ) e. CC )
127	121 126	fsumcl	|- ( ph -> sum_ n e. ( 0 ..^ ( J + 1 ) ) ( X ` ( L ` n ) ) e. CC )
128	119 127	mulcld	|- ( ph -> ( [_ ( J + 1 ) / n ]_ A x. sum_ n e. ( 0 ..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) e. CC )
129	103	recnd	|- ( ph -> [_ ( I + 1 ) / n ]_ A e. CC )
130		fzofi	|- ( 0 ..^ ( I + 1 ) ) e. Fin
131	130	a1i	|- ( ph -> ( 0 ..^ ( I + 1 ) ) e. Fin )
132		elfzoelz	|- ( n e. ( 0 ..^ ( I + 1 ) ) -> n e. ZZ )
133	132 125	sylan2	|- ( ( ph /\ n e. ( 0 ..^ ( I + 1 ) ) ) -> ( X ` ( L ` n ) ) e. CC )
134	131 133	fsumcl	|- ( ph -> sum_ n e. ( 0 ..^ ( I + 1 ) ) ( X ` ( L ` n ) ) e. CC )
135	129 134	mulcld	|- ( ph -> ( [_ ( I + 1 ) / n ]_ A x. sum_ n e. ( 0 ..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) e. CC )
136	128 135	subcld	|- ( 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 )
137	136	abscld	|- ( 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 )
138	89 36	syl	|- ( ( ph /\ i e. ( ( I + 1 ) ..^ ( J + 1 ) ) ) -> i e. NN )
139		peano2nn	|- ( i e. NN -> ( i + 1 ) e. NN )
140	139	nnrpd	|- ( i e. NN -> ( i + 1 ) e. RR+ )
141		nfcsb1v	|- F/_ n [_ ( i + 1 ) / n ]_ A
142	141	nfel1	|- F/ n [_ ( i + 1 ) / n ]_ A e. RR
143		csbeq1a	|- ( n = ( i + 1 ) -> A = [_ ( i + 1 ) / n ]_ A )
144	143	eleq1d	|- ( n = ( i + 1 ) -> ( A e. RR <-> [_ ( i + 1 ) / n ]_ A e. RR ) )
145	142 144	rspc	|- ( ( i + 1 ) e. RR+ -> ( A. n e. RR+ A e. RR -> [_ ( i + 1 ) / n ]_ A e. RR ) )
146	145	impcom	|- ( ( A. n e. RR+ A e. RR /\ ( i + 1 ) e. RR+ ) -> [_ ( i + 1 ) / n ]_ A e. RR )
147	105 140 146	syl2an	|- ( ( ph /\ i e. NN ) -> [_ ( i + 1 ) / n ]_ A e. RR )
148	147 44	resubcld	|- ( ( ph /\ i e. NN ) -> ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) e. RR )
149	148	recnd	|- ( ( ph /\ i e. NN ) -> ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) e. CC )
150		fzofi	|- ( 0 ..^ ( i + 1 ) ) e. Fin
151	150	a1i	|- ( ph -> ( 0 ..^ ( i + 1 ) ) e. Fin )
152		elfzoelz	|- ( n e. ( 0 ..^ ( i + 1 ) ) -> n e. ZZ )
153	152 125	sylan2	|- ( ( ph /\ n e. ( 0 ..^ ( i + 1 ) ) ) -> ( X ` ( L ` n ) ) e. CC )
154	151 153	fsumcl	|- ( ph -> sum_ n e. ( 0 ..^ ( i + 1 ) ) ( X ` ( L ` n ) ) e. CC )
155	154	adantr	|- ( ( ph /\ i e. NN ) -> sum_ n e. ( 0 ..^ ( i + 1 ) ) ( X ` ( L ` n ) ) e. CC )
156	149 155	mulcld	|- ( ( ph /\ i e. NN ) -> ( ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) x. sum_ n e. ( 0 ..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) e. CC )
157	138 156	syldan	|- ( ( 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 )
158	86 157	fsumcl	|- ( 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 )
159	158	abscld	|- ( 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 )
160	137 159	readdcld	|- ( 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 )
161	40 45	mulcomd	|- ( ( ph /\ i e. NN ) -> ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) = ( [_ i / n ]_ A x. ( X ` ( L ` i ) ) ) )
162		nnnn0	|- ( i e. NN -> i e. NN0 )
163	162	adantl	|- ( ( ph /\ i e. NN ) -> i e. NN0 )
164		nn0uz	|- NN0 = ( ZZ>= ` 0 )
165	163 164	eleqtrdi	|- ( ( ph /\ i e. NN ) -> i e. ( ZZ>= ` 0 ) )
166		elfzelz	|- ( n e. ( 0 ... i ) -> n e. ZZ )
167	125	adantlr	|- ( ( ( ph /\ i e. NN ) /\ n e. ZZ ) -> ( X ` ( L ` n ) ) e. CC )
168	166 167	sylan2	|- ( ( ( ph /\ i e. NN ) /\ n e. ( 0 ... i ) ) -> ( X ` ( L ` n ) ) e. CC )
169	165 168 66	fzosump1	|- ( ( ph /\ i e. NN ) -> sum_ n e. ( 0 ..^ ( i + 1 ) ) ( X ` ( L ` n ) ) = ( sum_ n e. ( 0 ..^ i ) ( X ` ( L ` n ) ) + ( X ` ( L ` i ) ) ) )
170	169	oveq1d	|- ( ( 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 ) ) ) )
171		fzofi	|- ( 0 ..^ i ) e. Fin
172	171	a1i	|- ( ( ph /\ i e. NN ) -> ( 0 ..^ i ) e. Fin )
173		elfzoelz	|- ( n e. ( 0 ..^ i ) -> n e. ZZ )
174	173 167	sylan2	|- ( ( ( ph /\ i e. NN ) /\ n e. ( 0 ..^ i ) ) -> ( X ` ( L ` n ) ) e. CC )
175	172 174	fsumcl	|- ( ( ph /\ i e. NN ) -> sum_ n e. ( 0 ..^ i ) ( X ` ( L ` n ) ) e. CC )
176	175 40	pncan2d	|- ( ( 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 ) ) )
177	170 176	eqtr2d	|- ( ( ph /\ i e. NN ) -> ( X ` ( L ` i ) ) = ( sum_ n e. ( 0 ..^ ( i + 1 ) ) ( X ` ( L ` n ) ) - sum_ n e. ( 0 ..^ i ) ( X ` ( L ` n ) ) ) )
178	177	oveq2d	|- ( ( 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 ) ) ) ) )
179	161 178	eqtrd	|- ( ( 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 ) ) ) ) )
180	138 179	syldan	|- ( ( 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 ) ) ) ) )
181	180	sumeq2dv	|- ( 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 ) ) ) ) )
182		csbeq1	|- ( k = i -> [_ k / n ]_ A = [_ i / n ]_ A )
183		oveq2	|- ( k = i -> ( 0 ..^ k ) = ( 0 ..^ i ) )
184	183	sumeq1d	|- ( k = i -> sum_ n e. ( 0 ..^ k ) ( X ` ( L ` n ) ) = sum_ n e. ( 0 ..^ i ) ( X ` ( L ` n ) ) )
185	182 184	jca	|- ( k = i -> ( [_ k / n ]_ A = [_ i / n ]_ A /\ sum_ n e. ( 0 ..^ k ) ( X ` ( L ` n ) ) = sum_ n e. ( 0 ..^ i ) ( X ` ( L ` n ) ) ) )
186		csbeq1	|- ( k = ( i + 1 ) -> [_ k / n ]_ A = [_ ( i + 1 ) / n ]_ A )
187		oveq2	|- ( k = ( i + 1 ) -> ( 0 ..^ k ) = ( 0 ..^ ( i + 1 ) ) )
188	187	sumeq1d	|- ( k = ( i + 1 ) -> sum_ n e. ( 0 ..^ k ) ( X ` ( L ` n ) ) = sum_ n e. ( 0 ..^ ( i + 1 ) ) ( X ` ( L ` n ) ) )
189	186 188	jca	|- ( 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 ) ) ) )
190		csbeq1	|- ( k = ( I + 1 ) -> [_ k / n ]_ A = [_ ( I + 1 ) / n ]_ A )
191		oveq2	|- ( k = ( I + 1 ) -> ( 0 ..^ k ) = ( 0 ..^ ( I + 1 ) ) )
192	191	sumeq1d	|- ( k = ( I + 1 ) -> sum_ n e. ( 0 ..^ k ) ( X ` ( L ` n ) ) = sum_ n e. ( 0 ..^ ( I + 1 ) ) ( X ` ( L ` n ) ) )
193	190 192	jca	|- ( 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 ) ) ) )
194		csbeq1	|- ( k = ( J + 1 ) -> [_ k / n ]_ A = [_ ( J + 1 ) / n ]_ A )
195		oveq2	|- ( k = ( J + 1 ) -> ( 0 ..^ k ) = ( 0 ..^ ( J + 1 ) ) )
196	195	sumeq1d	|- ( k = ( J + 1 ) -> sum_ n e. ( 0 ..^ k ) ( X ` ( L ` n ) ) = sum_ n e. ( 0 ..^ ( J + 1 ) ) ( X ` ( L ` n ) ) )
197	194 196	jca	|- ( 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 ) ) ) )
198	45	ralrimiva	|- ( ph -> A. i e. NN [_ i / n ]_ A e. CC )
199		elfzuz	|- ( k e. ( ( I + 1 ) ... ( J + 1 ) ) -> k e. ( ZZ>= ` ( I + 1 ) ) )
200		eluznn	|- ( ( ( I + 1 ) e. NN /\ k e. ( ZZ>= ` ( I + 1 ) ) ) -> k e. NN )
201	24 199 200	syl2an	|- ( ( ph /\ k e. ( ( I + 1 ) ... ( J + 1 ) ) ) -> k e. NN )
202		csbeq1	|- ( i = k -> [_ i / n ]_ A = [_ k / n ]_ A )
203	202	eleq1d	|- ( i = k -> ( [_ i / n ]_ A e. CC <-> [_ k / n ]_ A e. CC ) )
204	203	rspccva	|- ( ( A. i e. NN [_ i / n ]_ A e. CC /\ k e. NN ) -> [_ k / n ]_ A e. CC )
205	198 201 204	syl2an2r	|- ( ( ph /\ k e. ( ( I + 1 ) ... ( J + 1 ) ) ) -> [_ k / n ]_ A e. CC )
206		fzofi	|- ( 0 ..^ k ) e. Fin
207	206	a1i	|- ( ph -> ( 0 ..^ k ) e. Fin )
208		elfzoelz	|- ( n e. ( 0 ..^ k ) -> n e. ZZ )
209	208 125	sylan2	|- ( ( ph /\ n e. ( 0 ..^ k ) ) -> ( X ` ( L ` n ) ) e. CC )
210	207 209	fsumcl	|- ( ph -> sum_ n e. ( 0 ..^ k ) ( X ` ( L ` n ) ) e. CC )
211	210	adantr	|- ( ( ph /\ k e. ( ( I + 1 ) ... ( J + 1 ) ) ) -> sum_ n e. ( 0 ..^ k ) ( X ` ( L ` n ) ) e. CC )
212	185 189 193 197 28 205 211	fsumparts	|- ( 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	181 212	eqtrd	|- ( 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	|- ( 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	136 158	abs2dif2d	|- ( 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	|- ( 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	118 103	readdcld	|- ( ph -> ( [_ ( J + 1 ) / n ]_ A + [_ ( I + 1 ) / n ]_ A ) e. RR )
218	217 15	remulcld	|- ( ph -> ( ( [_ ( J + 1 ) / n ]_ A + [_ ( I + 1 ) / n ]_ A ) x. R ) e. RR )
219	182 186 190 194 28 205	telfsumo	|- ( ph -> sum_ i e. ( ( I + 1 ) ..^ ( J + 1 ) ) ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) = ( [_ ( I + 1 ) / n ]_ A - [_ ( J + 1 ) / n ]_ A ) )
220	138 44	syldan	|- ( ( ph /\ i e. ( ( I + 1 ) ..^ ( J + 1 ) ) ) -> [_ i / n ]_ A e. RR )
221	138 147	syldan	|- ( ( ph /\ i e. ( ( I + 1 ) ..^ ( J + 1 ) ) ) -> [_ ( i + 1 ) / n ]_ A e. RR )
222	220 221	resubcld	|- ( ( ph /\ i e. ( ( I + 1 ) ..^ ( J + 1 ) ) ) -> ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) e. RR )
223	86 222	fsumrecl	|- ( ph -> sum_ i e. ( ( I + 1 ) ..^ ( J + 1 ) ) ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) e. RR )
224	219 223	eqeltrrd	|- ( ph -> ( [_ ( I + 1 ) / n ]_ A - [_ ( J + 1 ) / n ]_ A ) e. RR )
225	224 15	remulcld	|- ( ph -> ( ( [_ ( I + 1 ) / n ]_ A - [_ ( J + 1 ) / n ]_ A ) x. R ) e. RR )
226	128	abscld	|- ( ph -> ( abs ` ( [_ ( J + 1 ) / n ]_ A x. sum_ n e. ( 0 ..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) ) e. RR )
227	135	abscld	|- ( ph -> ( abs ` ( [_ ( I + 1 ) / n ]_ A x. sum_ n e. ( 0 ..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) ) e. RR )
228	226 227	readdcld	|- ( 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	128 135	abs2dif2d	|- ( 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	118 15	remulcld	|- ( ph -> ( [_ ( J + 1 ) / n ]_ A x. R ) e. RR )
231	103 15	remulcld	|- ( ph -> ( [_ ( I + 1 ) / n ]_ A x. R ) e. RR )
232	119 127	absmuld	|- ( 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	|- ( i e. ( ZZ>= ` M ) -> i e. RR )
234	233	adantl	|- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> i e. RR )
235		eluzle	|- ( i e. ( ZZ>= ` M ) -> M <_ i )
236	235	adantl	|- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> M <_ i )
237	10	nnred	|- ( ph -> M e. RR )
238	237	adantr	|- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> M e. RR )
239		elicopnf	|- ( M e. RR -> ( i e. ( M [,) +oo ) <-> ( i e. RR /\ M <_ i ) ) )
240	238 239	syl	|- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> ( i e. ( M [,) +oo ) <-> ( i e. RR /\ M <_ i ) ) )
241	234 236 240	mpbir2and	|- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> i e. ( M [,) +oo ) )
242	241	ex	|- ( ph -> ( i e. ( ZZ>= ` M ) -> i e. ( M [,) +oo ) ) )
243	242	ssrdv	|- ( ph -> ( ZZ>= ` M ) C_ ( M [,) +oo ) )
244	10	nnzd	|- ( ph -> M e. ZZ )
245	53	peano2zd	|- ( ph -> ( I + 1 ) e. ZZ )
246	17	rpred	|- ( ph -> U e. RR )
247	24	nnred	|- ( ph -> ( I + 1 ) e. RR )
248	237 246 247 18 19	letrd	|- ( ph -> M <_ ( I + 1 ) )
249		eluz2	|- ( ( I + 1 ) e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ ( I + 1 ) e. ZZ /\ M <_ ( I + 1 ) ) )
250	244 245 248 249	syl3anbrc	|- ( ph -> ( I + 1 ) e. ( ZZ>= ` M ) )
251		uztrn	|- ( ( ( J + 1 ) e. ( ZZ>= ` ( I + 1 ) ) /\ ( I + 1 ) e. ( ZZ>= ` M ) ) -> ( J + 1 ) e. ( ZZ>= ` M ) )
252	28 250 251	syl2anc	|- ( ph -> ( J + 1 ) e. ( ZZ>= ` M ) )
253	243 252	sseldd	|- ( ph -> ( J + 1 ) e. ( M [,) +oo ) )
254	116	simprd	|- ( ph -> ( ( J + 1 ) e. ( M [,) +oo ) -> 0 <_ [_ ( J + 1 ) / n ]_ A ) )
255	253 254	mpd	|- ( ph -> 0 <_ [_ ( J + 1 ) / n ]_ A )
256	118 255	absidd	|- ( ph -> ( abs ` [_ ( J + 1 ) / n ]_ A ) = [_ ( J + 1 ) / n ]_ A )
257	256	oveq1d	|- ( 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 ) ) ) ) )
258	232 257	eqtrd	|- ( 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 ) ) ) ) )
259	127	abscld	|- ( ph -> ( abs ` sum_ n e. ( 0 ..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) e. RR )
260	114	nnnn0d	|- ( ph -> ( J + 1 ) e. NN0 )
261	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16	dchrisumlem1	|- ( ( ph /\ ( J + 1 ) e. NN0 ) -> ( abs ` sum_ n e. ( 0 ..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) <_ R )
262	260 261	mpdan	|- ( ph -> ( abs ` sum_ n e. ( 0 ..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) <_ R )
263	259 15 118 255 262	lemul2ad	|- ( ph -> ( [_ ( J + 1 ) / n ]_ A x. ( abs ` sum_ n e. ( 0 ..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) ) <_ ( [_ ( J + 1 ) / n ]_ A x. R ) )
264	258 263	eqbrtrd	|- ( ph -> ( abs ` ( [_ ( J + 1 ) / n ]_ A x. sum_ n e. ( 0 ..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) ) <_ ( [_ ( J + 1 ) / n ]_ A x. R ) )
265	129 134	absmuld	|- ( 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 ) ) ) ) )
266	243 250	sseldd	|- ( ph -> ( I + 1 ) e. ( M [,) +oo ) )
267	1 2 3 4 5 6 7 8 9 10 11 12 13 14	dchrisumlema	|- ( ph -> ( ( ( I + 1 ) e. RR+ -> [_ ( I + 1 ) / n ]_ A e. RR ) /\ ( ( I + 1 ) e. ( M [,) +oo ) -> 0 <_ [_ ( I + 1 ) / n ]_ A ) ) )
268	267	simprd	|- ( ph -> ( ( I + 1 ) e. ( M [,) +oo ) -> 0 <_ [_ ( I + 1 ) / n ]_ A ) )
269	266 268	mpd	|- ( ph -> 0 <_ [_ ( I + 1 ) / n ]_ A )
270	103 269	absidd	|- ( ph -> ( abs ` [_ ( I + 1 ) / n ]_ A ) = [_ ( I + 1 ) / n ]_ A )
271	270	oveq1d	|- ( 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 ) ) ) ) )
272	265 271	eqtrd	|- ( 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 ) ) ) ) )
273	134	abscld	|- ( ph -> ( abs ` sum_ n e. ( 0 ..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) e. RR )
274	24	nnnn0d	|- ( ph -> ( I + 1 ) e. NN0 )
275	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16	dchrisumlem1	|- ( ( ph /\ ( I + 1 ) e. NN0 ) -> ( abs ` sum_ n e. ( 0 ..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) <_ R )
276	274 275	mpdan	|- ( ph -> ( abs ` sum_ n e. ( 0 ..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) <_ R )
277	273 15 103 269 276	lemul2ad	|- ( ph -> ( [_ ( I + 1 ) / n ]_ A x. ( abs ` sum_ n e. ( 0 ..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) ) <_ ( [_ ( I + 1 ) / n ]_ A x. R ) )
278	272 277	eqbrtrd	|- ( ph -> ( abs ` ( [_ ( I + 1 ) / n ]_ A x. sum_ n e. ( 0 ..^ ( I + 1 ) ) ( X ` ( L ` n ) ) ) ) <_ ( [_ ( I + 1 ) / n ]_ A x. R ) )
279	226 227 230 231 264 278	le2addd	|- ( 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 ) ) )
280	15	recnd	|- ( ph -> R e. CC )
281	119 129 280	adddird	|- ( ph -> ( ( [_ ( J + 1 ) / n ]_ A + [_ ( I + 1 ) / n ]_ A ) x. R ) = ( ( [_ ( J + 1 ) / n ]_ A x. R ) + ( [_ ( I + 1 ) / n ]_ A x. R ) ) )
282	279 281	breqtrrd	|- ( 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 ) )
283	137 228 218 229 282	letrd	|- ( 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 ) )
284	157	abscld	|- ( ( 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 )
285	86 284	fsumrecl	|- ( 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 )
286	86 157	fsumabs	|- ( 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 ) ) ) ) )
287	15	adantr	|- ( ( ph /\ i e. ( ( I + 1 ) ..^ ( J + 1 ) ) ) -> R e. RR )
288	222 287	remulcld	|- ( ( ph /\ i e. ( ( I + 1 ) ..^ ( J + 1 ) ) ) -> ( ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) x. R ) e. RR )
289	138 149	syldan	|- ( ( ph /\ i e. ( ( I + 1 ) ..^ ( J + 1 ) ) ) -> ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) e. CC )
290	154	adantr	|- ( ( ph /\ i e. ( ( I + 1 ) ..^ ( J + 1 ) ) ) -> sum_ n e. ( 0 ..^ ( i + 1 ) ) ( X ` ( L ` n ) ) e. CC )
291	289 290	absmuld	|- ( ( 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 ) ) ) ) )
292		elfzouz	|- ( i e. ( ( I + 1 ) ..^ ( J + 1 ) ) -> i e. ( ZZ>= ` ( I + 1 ) ) )
293		uztrn	|- ( ( i e. ( ZZ>= ` ( I + 1 ) ) /\ ( I + 1 ) e. ( ZZ>= ` M ) ) -> i e. ( ZZ>= ` M ) )
294	292 250 293	syl2anr	|- ( ( ph /\ i e. ( ( I + 1 ) ..^ ( J + 1 ) ) ) -> i e. ( ZZ>= ` M ) )
295		eluznn	|- ( ( M e. NN /\ i e. ( ZZ>= ` M ) ) -> i e. NN )
296	10 295	sylan	|- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> i e. NN )
297	296 140	syl	|- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> ( i + 1 ) e. RR+ )
298	296	nnrpd	|- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> i e. RR+ )
299	12	3expia	|- ( ( ph /\ ( n e. RR+ /\ x e. RR+ ) ) -> ( ( M <_ n /\ n <_ x ) -> B <_ A ) )
300	299	ralrimivva	|- ( ph -> A. n e. RR+ A. x e. RR+ ( ( M <_ n /\ n <_ x ) -> B <_ A ) )
301	300	adantr	|- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> A. n e. RR+ A. x e. RR+ ( ( M <_ n /\ n <_ x ) -> B <_ A ) )
302		nfcv	|- F/_ n RR+
303		nfv	|- F/ n ( M <_ i /\ i <_ x )
304		nfcv	|- F/_ n B
305		nfcv	|- F/_ n <_
306	304 305 64	nfbr	|- F/ n B <_ [_ i / n ]_ A
307	303 306	nfim	|- F/ n ( ( M <_ i /\ i <_ x ) -> B <_ [_ i / n ]_ A )
308	302 307	nfralw	|- F/ n A. x e. RR+ ( ( M <_ i /\ i <_ x ) -> B <_ [_ i / n ]_ A )
309		breq2	|- ( n = i -> ( M <_ n <-> M <_ i ) )
310		breq1	|- ( n = i -> ( n <_ x <-> i <_ x ) )
311	309 310	anbi12d	|- ( n = i -> ( ( M <_ n /\ n <_ x ) <-> ( M <_ i /\ i <_ x ) ) )
312	67	breq2d	|- ( n = i -> ( B <_ A <-> B <_ [_ i / n ]_ A ) )
313	311 312	imbi12d	|- ( n = i -> ( ( ( M <_ n /\ n <_ x ) -> B <_ A ) <-> ( ( M <_ i /\ i <_ x ) -> B <_ [_ i / n ]_ A ) ) )
314	313	ralbidv	|- ( n = i -> ( A. x e. RR+ ( ( M <_ n /\ n <_ x ) -> B <_ A ) <-> A. x e. RR+ ( ( M <_ i /\ i <_ x ) -> B <_ [_ i / n ]_ A ) ) )
315	308 314	rspc	|- ( 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 ) ) )
316	298 301 315	sylc	|- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> A. x e. RR+ ( ( M <_ i /\ i <_ x ) -> B <_ [_ i / n ]_ A ) )
317	234	lep1d	|- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> i <_ ( i + 1 ) )
318	236 317	jca	|- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> ( M <_ i /\ i <_ ( i + 1 ) ) )
319		breq2	|- ( x = ( i + 1 ) -> ( i <_ x <-> i <_ ( i + 1 ) ) )
320	319	anbi2d	|- ( x = ( i + 1 ) -> ( ( M <_ i /\ i <_ x ) <-> ( M <_ i /\ i <_ ( i + 1 ) ) ) )
321		eqvisset	|- ( x = ( i + 1 ) -> ( i + 1 ) e. _V )
322		eqtr3	|- ( ( x = ( i + 1 ) /\ n = ( i + 1 ) ) -> x = n )
323	9	equcoms	|- ( x = n -> A = B )
324	322 323	syl	|- ( ( x = ( i + 1 ) /\ n = ( i + 1 ) ) -> A = B )
325	321 324	csbied	|- ( x = ( i + 1 ) -> [_ ( i + 1 ) / n ]_ A = B )
326	325	eqcomd	|- ( x = ( i + 1 ) -> B = [_ ( i + 1 ) / n ]_ A )
327	326	breq1d	|- ( x = ( i + 1 ) -> ( B <_ [_ i / n ]_ A <-> [_ ( i + 1 ) / n ]_ A <_ [_ i / n ]_ A ) )
328	320 327	imbi12d	|- ( x = ( i + 1 ) -> ( ( ( M <_ i /\ i <_ x ) -> B <_ [_ i / n ]_ A ) <-> ( ( M <_ i /\ i <_ ( i + 1 ) ) -> [_ ( i + 1 ) / n ]_ A <_ [_ i / n ]_ A ) ) )
329	328	rspcv	|- ( ( 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 ) ) )
330	297 316 318 329	syl3c	|- ( ( ph /\ i e. ( ZZ>= ` M ) ) -> [_ ( i + 1 ) / n ]_ A <_ [_ i / n ]_ A )
331	294 330	syldan	|- ( ( ph /\ i e. ( ( I + 1 ) ..^ ( J + 1 ) ) ) -> [_ ( i + 1 ) / n ]_ A <_ [_ i / n ]_ A )
332	221 220 331	abssuble0d	|- ( ( ph /\ i e. ( ( I + 1 ) ..^ ( J + 1 ) ) ) -> ( abs ` ( [_ ( i + 1 ) / n ]_ A - [_ i / n ]_ A ) ) = ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) )
333	332	oveq1d	|- ( ( 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 ) ) ) ) )
334	291 333	eqtrd	|- ( ( 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 ) ) ) ) )
335	290	abscld	|- ( ( ph /\ i e. ( ( I + 1 ) ..^ ( J + 1 ) ) ) -> ( abs ` sum_ n e. ( 0 ..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) e. RR )
336	220 221	subge0d	|- ( ( ph /\ i e. ( ( I + 1 ) ..^ ( J + 1 ) ) ) -> ( 0 <_ ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) <-> [_ ( i + 1 ) / n ]_ A <_ [_ i / n ]_ A ) )
337	331 336	mpbird	|- ( ( ph /\ i e. ( ( I + 1 ) ..^ ( J + 1 ) ) ) -> 0 <_ ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) )
338	138	peano2nnd	|- ( ( ph /\ i e. ( ( I + 1 ) ..^ ( J + 1 ) ) ) -> ( i + 1 ) e. NN )
339	338	nnnn0d	|- ( ( ph /\ i e. ( ( I + 1 ) ..^ ( J + 1 ) ) ) -> ( i + 1 ) e. NN0 )
340	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16	dchrisumlem1	|- ( ( ph /\ ( i + 1 ) e. NN0 ) -> ( abs ` sum_ n e. ( 0 ..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) <_ R )
341	339 340	syldan	|- ( ( ph /\ i e. ( ( I + 1 ) ..^ ( J + 1 ) ) ) -> ( abs ` sum_ n e. ( 0 ..^ ( i + 1 ) ) ( X ` ( L ` n ) ) ) <_ R )
342	335 287 222 337 341	lemul2ad	|- ( ( 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 ) )
343	334 342	eqbrtrd	|- ( ( 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 ) )
344	86 284 288 343	fsumle	|- ( 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 ) )
345	222	recnd	|- ( ( ph /\ i e. ( ( I + 1 ) ..^ ( J + 1 ) ) ) -> ( [_ i / n ]_ A - [_ ( i + 1 ) / n ]_ A ) e. CC )
346	86 280 345	fsummulc1	|- ( 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 ) )
347	219	oveq1d	|- ( 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 ) )
348	346 347	eqtr3d	|- ( 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 ) )
349	344 348	breqtrd	|- ( 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 ) )
350	159 285 225 286 349	letrd	|- ( 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 ) )
351	137 159 218 225 283 350	le2addd	|- ( 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 ) ) )
352	129	2timesd	|- ( ph -> ( 2 x. [_ ( I + 1 ) / n ]_ A ) = ( [_ ( I + 1 ) / n ]_ A + [_ ( I + 1 ) / n ]_ A ) )
353	129 119 129	ppncand	|- ( 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 ) )
354	129 119	addcomd	|- ( ph -> ( [_ ( I + 1 ) / n ]_ A + [_ ( J + 1 ) / n ]_ A ) = ( [_ ( J + 1 ) / n ]_ A + [_ ( I + 1 ) / n ]_ A ) )
355	354	oveq1d	|- ( 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 ) ) )
356	352 353 355	3eqtr2d	|- ( ph -> ( 2 x. [_ ( I + 1 ) / n ]_ A ) = ( ( [_ ( J + 1 ) / n ]_ A + [_ ( I + 1 ) / n ]_ A ) + ( [_ ( I + 1 ) / n ]_ A - [_ ( J + 1 ) / n ]_ A ) ) )
357	356	oveq1d	|- ( 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 ) )
358		2cnd	|- ( ph -> 2 e. CC )
359	358 129 280	mul32d	|- ( ph -> ( ( 2 x. [_ ( I + 1 ) / n ]_ A ) x. R ) = ( ( 2 x. R ) x. [_ ( I + 1 ) / n ]_ A ) )
360	217	recnd	|- ( ph -> ( [_ ( J + 1 ) / n ]_ A + [_ ( I + 1 ) / n ]_ A ) e. CC )
361	224	recnd	|- ( ph -> ( [_ ( I + 1 ) / n ]_ A - [_ ( J + 1 ) / n ]_ A ) e. CC )
362	360 361 280	adddird	|- ( 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 ) ) )
363	357 359 362	3eqtr3d	|- ( 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 ) ) )
364	351 363	breqtrrd	|- ( 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 ) )
365	95 160 104 216 364	letrd	|- ( ph -> ( abs ` sum_ i e. ( ( I + 1 ) ..^ ( J + 1 ) ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) ) <_ ( ( 2 x. R ) x. [_ ( I + 1 ) / n ]_ A ) )
366		2nn0	|- 2 e. NN0
367		nn0ge0	|- ( 2 e. NN0 -> 0 <_ 2 )
368	366 367	mp1i	|- ( ph -> 0 <_ 2 )
369		0red	|- ( ph -> 0 e. RR )
370	127	absge0d	|- ( ph -> 0 <_ ( abs ` sum_ n e. ( 0 ..^ ( J + 1 ) ) ( X ` ( L ` n ) ) ) )
371	369 259 15 370 262	letrd	|- ( ph -> 0 <_ R )
372	97 15 368 371	mulge0d	|- ( ph -> 0 <_ ( 2 x. R ) )
373	24	nnrpd	|- ( ph -> ( I + 1 ) e. RR+ )
374		nfv	|- F/ n ( M <_ U /\ U <_ x )
375	304 305 106	nfbr	|- F/ n B <_ [_ U / n ]_ A
376	374 375	nfim	|- F/ n ( ( M <_ U /\ U <_ x ) -> B <_ [_ U / n ]_ A )
377	302 376	nfralw	|- F/ n A. x e. RR+ ( ( M <_ U /\ U <_ x ) -> B <_ [_ U / n ]_ A )
378		breq2	|- ( n = U -> ( M <_ n <-> M <_ U ) )
379		breq1	|- ( n = U -> ( n <_ x <-> U <_ x ) )
380	378 379	anbi12d	|- ( n = U -> ( ( M <_ n /\ n <_ x ) <-> ( M <_ U /\ U <_ x ) ) )
381	108	breq2d	|- ( n = U -> ( B <_ A <-> B <_ [_ U / n ]_ A ) )
382	380 381	imbi12d	|- ( n = U -> ( ( ( M <_ n /\ n <_ x ) -> B <_ A ) <-> ( ( M <_ U /\ U <_ x ) -> B <_ [_ U / n ]_ A ) ) )
383	382	ralbidv	|- ( n = U -> ( A. x e. RR+ ( ( M <_ n /\ n <_ x ) -> B <_ A ) <-> A. x e. RR+ ( ( M <_ U /\ U <_ x ) -> B <_ [_ U / n ]_ A ) ) )
384	377 383	rspc	|- ( 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 ) ) )
385	17 300 384	sylc	|- ( ph -> A. x e. RR+ ( ( M <_ U /\ U <_ x ) -> B <_ [_ U / n ]_ A ) )
386	18 19	jca	|- ( ph -> ( M <_ U /\ U <_ ( I + 1 ) ) )
387		breq2	|- ( x = ( I + 1 ) -> ( U <_ x <-> U <_ ( I + 1 ) ) )
388	387	anbi2d	|- ( x = ( I + 1 ) -> ( ( M <_ U /\ U <_ x ) <-> ( M <_ U /\ U <_ ( I + 1 ) ) ) )
389		eqvisset	|- ( x = ( I + 1 ) -> ( I + 1 ) e. _V )
390		eqtr3	|- ( ( x = ( I + 1 ) /\ n = ( I + 1 ) ) -> x = n )
391	390 323	syl	|- ( ( x = ( I + 1 ) /\ n = ( I + 1 ) ) -> A = B )
392	389 391	csbied	|- ( x = ( I + 1 ) -> [_ ( I + 1 ) / n ]_ A = B )
393	392	eqcomd	|- ( x = ( I + 1 ) -> B = [_ ( I + 1 ) / n ]_ A )
394	393	breq1d	|- ( x = ( I + 1 ) -> ( B <_ [_ U / n ]_ A <-> [_ ( I + 1 ) / n ]_ A <_ [_ U / n ]_ A ) )
395	388 394	imbi12d	|- ( x = ( I + 1 ) -> ( ( ( M <_ U /\ U <_ x ) -> B <_ [_ U / n ]_ A ) <-> ( ( M <_ U /\ U <_ ( I + 1 ) ) -> [_ ( I + 1 ) / n ]_ A <_ [_ U / n ]_ A ) ) )
396	395	rspcv	|- ( ( 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 ) ) )
397	373 385 386 396	syl3c	|- ( ph -> [_ ( I + 1 ) / n ]_ A <_ [_ U / n ]_ A )
398	103 111 98 372 397	lemul2ad	|- ( ph -> ( ( 2 x. R ) x. [_ ( I + 1 ) / n ]_ A ) <_ ( ( 2 x. R ) x. [_ U / n ]_ A ) )
399	95 104 112 365 398	letrd	|- ( ph -> ( abs ` sum_ i e. ( ( I + 1 ) ..^ ( J + 1 ) ) ( ( X ` ( L ` i ) ) x. [_ i / n ]_ A ) ) <_ ( ( 2 x. R ) x. [_ U / n ]_ A ) )
400	94 399	eqbrtrd	|- ( ph -> ( abs ` ( ( seq 1 ( + , F ) ` J ) - ( seq 1 ( + , F ) ` I ) ) ) <_ ( ( 2 x. R ) x. [_ U / n ]_ A ) )