dchrisumlem2

	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 ) )

Metamath Proof Explorer

Theorem dchrisumlem2

Proof