Metamath Proof Explorer


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