Step |
Hyp |
Ref |
Expression |
1 |
|
fmul01lt1lem1.1 |
|- F/_ i B |
2 |
|
fmul01lt1lem1.2 |
|- F/ i ph |
3 |
|
fmul01lt1lem1.3 |
|- A = seq L ( x. , B ) |
4 |
|
fmul01lt1lem1.4 |
|- ( ph -> L e. ZZ ) |
5 |
|
fmul01lt1lem1.5 |
|- ( ph -> M e. ( ZZ>= ` L ) ) |
6 |
|
fmul01lt1lem1.6 |
|- ( ( ph /\ i e. ( L ... M ) ) -> ( B ` i ) e. RR ) |
7 |
|
fmul01lt1lem1.7 |
|- ( ( ph /\ i e. ( L ... M ) ) -> 0 <_ ( B ` i ) ) |
8 |
|
fmul01lt1lem1.8 |
|- ( ( ph /\ i e. ( L ... M ) ) -> ( B ` i ) <_ 1 ) |
9 |
|
fmul01lt1lem1.9 |
|- ( ph -> E e. RR+ ) |
10 |
|
fmul01lt1lem1.10 |
|- ( ph -> ( B ` L ) < E ) |
11 |
|
simpr |
|- ( ( ph /\ M = L ) -> M = L ) |
12 |
11
|
fveq2d |
|- ( ( ph /\ M = L ) -> ( A ` M ) = ( A ` L ) ) |
13 |
3
|
a1i |
|- ( ( ph /\ M = L ) -> A = seq L ( x. , B ) ) |
14 |
13
|
fveq1d |
|- ( ( ph /\ M = L ) -> ( A ` L ) = ( seq L ( x. , B ) ` L ) ) |
15 |
|
seq1 |
|- ( L e. ZZ -> ( seq L ( x. , B ) ` L ) = ( B ` L ) ) |
16 |
4 15
|
syl |
|- ( ph -> ( seq L ( x. , B ) ` L ) = ( B ` L ) ) |
17 |
16
|
adantr |
|- ( ( ph /\ M = L ) -> ( seq L ( x. , B ) ` L ) = ( B ` L ) ) |
18 |
12 14 17
|
3eqtrd |
|- ( ( ph /\ M = L ) -> ( A ` M ) = ( B ` L ) ) |
19 |
10
|
adantr |
|- ( ( ph /\ M = L ) -> ( B ` L ) < E ) |
20 |
18 19
|
eqbrtrd |
|- ( ( ph /\ M = L ) -> ( A ` M ) < E ) |
21 |
|
simpr |
|- ( ( ph /\ -. M = L ) -> -. M = L ) |
22 |
21
|
neqned |
|- ( ( ph /\ -. M = L ) -> M =/= L ) |
23 |
4
|
zred |
|- ( ph -> L e. RR ) |
24 |
|
eluzelz |
|- ( M e. ( ZZ>= ` L ) -> M e. ZZ ) |
25 |
5 24
|
syl |
|- ( ph -> M e. ZZ ) |
26 |
25
|
zred |
|- ( ph -> M e. RR ) |
27 |
|
eluzle |
|- ( M e. ( ZZ>= ` L ) -> L <_ M ) |
28 |
5 27
|
syl |
|- ( ph -> L <_ M ) |
29 |
23 26 28
|
3jca |
|- ( ph -> ( L e. RR /\ M e. RR /\ L <_ M ) ) |
30 |
29
|
adantr |
|- ( ( ph /\ -. M = L ) -> ( L e. RR /\ M e. RR /\ L <_ M ) ) |
31 |
|
leltne |
|- ( ( L e. RR /\ M e. RR /\ L <_ M ) -> ( L < M <-> M =/= L ) ) |
32 |
30 31
|
syl |
|- ( ( ph /\ -. M = L ) -> ( L < M <-> M =/= L ) ) |
33 |
22 32
|
mpbird |
|- ( ( ph /\ -. M = L ) -> L < M ) |
34 |
3
|
fveq1i |
|- ( A ` M ) = ( seq L ( x. , B ) ` M ) |
35 |
|
remulcl |
|- ( ( j e. RR /\ k e. RR ) -> ( j x. k ) e. RR ) |
36 |
35
|
adantl |
|- ( ( ( ph /\ L < M ) /\ ( j e. RR /\ k e. RR ) ) -> ( j x. k ) e. RR ) |
37 |
|
recn |
|- ( j e. RR -> j e. CC ) |
38 |
37
|
3ad2ant1 |
|- ( ( j e. RR /\ k e. RR /\ l e. RR ) -> j e. CC ) |
39 |
|
recn |
|- ( k e. RR -> k e. CC ) |
40 |
39
|
3ad2ant2 |
|- ( ( j e. RR /\ k e. RR /\ l e. RR ) -> k e. CC ) |
41 |
|
recn |
|- ( l e. RR -> l e. CC ) |
42 |
41
|
3ad2ant3 |
|- ( ( j e. RR /\ k e. RR /\ l e. RR ) -> l e. CC ) |
43 |
38 40 42
|
mulassd |
|- ( ( j e. RR /\ k e. RR /\ l e. RR ) -> ( ( j x. k ) x. l ) = ( j x. ( k x. l ) ) ) |
44 |
43
|
adantl |
|- ( ( ( ph /\ L < M ) /\ ( j e. RR /\ k e. RR /\ l e. RR ) ) -> ( ( j x. k ) x. l ) = ( j x. ( k x. l ) ) ) |
45 |
|
simpr |
|- ( ( ph /\ L < M ) -> L < M ) |
46 |
45
|
olcd |
|- ( ( ph /\ L < M ) -> ( M < L \/ L < M ) ) |
47 |
26 23
|
jca |
|- ( ph -> ( M e. RR /\ L e. RR ) ) |
48 |
47
|
adantr |
|- ( ( ph /\ L < M ) -> ( M e. RR /\ L e. RR ) ) |
49 |
|
lttri2 |
|- ( ( M e. RR /\ L e. RR ) -> ( M =/= L <-> ( M < L \/ L < M ) ) ) |
50 |
48 49
|
syl |
|- ( ( ph /\ L < M ) -> ( M =/= L <-> ( M < L \/ L < M ) ) ) |
51 |
46 50
|
mpbird |
|- ( ( ph /\ L < M ) -> M =/= L ) |
52 |
51
|
neneqd |
|- ( ( ph /\ L < M ) -> -. M = L ) |
53 |
|
uzp1 |
|- ( M e. ( ZZ>= ` L ) -> ( M = L \/ M e. ( ZZ>= ` ( L + 1 ) ) ) ) |
54 |
5 53
|
syl |
|- ( ph -> ( M = L \/ M e. ( ZZ>= ` ( L + 1 ) ) ) ) |
55 |
54
|
adantr |
|- ( ( ph /\ L < M ) -> ( M = L \/ M e. ( ZZ>= ` ( L + 1 ) ) ) ) |
56 |
55
|
ord |
|- ( ( ph /\ L < M ) -> ( -. M = L -> M e. ( ZZ>= ` ( L + 1 ) ) ) ) |
57 |
52 56
|
mpd |
|- ( ( ph /\ L < M ) -> M e. ( ZZ>= ` ( L + 1 ) ) ) |
58 |
4
|
adantr |
|- ( ( ph /\ L < M ) -> L e. ZZ ) |
59 |
|
uzid |
|- ( L e. ZZ -> L e. ( ZZ>= ` L ) ) |
60 |
58 59
|
syl |
|- ( ( ph /\ L < M ) -> L e. ( ZZ>= ` L ) ) |
61 |
|
nfv |
|- F/ i j e. ( L ... M ) |
62 |
2 61
|
nfan |
|- F/ i ( ph /\ j e. ( L ... M ) ) |
63 |
|
nfcv |
|- F/_ i j |
64 |
1 63
|
nffv |
|- F/_ i ( B ` j ) |
65 |
64
|
nfel1 |
|- F/ i ( B ` j ) e. RR |
66 |
62 65
|
nfim |
|- F/ i ( ( ph /\ j e. ( L ... M ) ) -> ( B ` j ) e. RR ) |
67 |
|
eleq1 |
|- ( i = j -> ( i e. ( L ... M ) <-> j e. ( L ... M ) ) ) |
68 |
67
|
anbi2d |
|- ( i = j -> ( ( ph /\ i e. ( L ... M ) ) <-> ( ph /\ j e. ( L ... M ) ) ) ) |
69 |
|
fveq2 |
|- ( i = j -> ( B ` i ) = ( B ` j ) ) |
70 |
69
|
eleq1d |
|- ( i = j -> ( ( B ` i ) e. RR <-> ( B ` j ) e. RR ) ) |
71 |
68 70
|
imbi12d |
|- ( i = j -> ( ( ( ph /\ i e. ( L ... M ) ) -> ( B ` i ) e. RR ) <-> ( ( ph /\ j e. ( L ... M ) ) -> ( B ` j ) e. RR ) ) ) |
72 |
66 71 6
|
chvarfv |
|- ( ( ph /\ j e. ( L ... M ) ) -> ( B ` j ) e. RR ) |
73 |
72
|
adantlr |
|- ( ( ( ph /\ L < M ) /\ j e. ( L ... M ) ) -> ( B ` j ) e. RR ) |
74 |
36 44 57 60 73
|
seqsplit |
|- ( ( ph /\ L < M ) -> ( seq L ( x. , B ) ` M ) = ( ( seq L ( x. , B ) ` L ) x. ( seq ( L + 1 ) ( x. , B ) ` M ) ) ) |
75 |
|
eluzfz1 |
|- ( M e. ( ZZ>= ` L ) -> L e. ( L ... M ) ) |
76 |
5 75
|
syl |
|- ( ph -> L e. ( L ... M ) ) |
77 |
76
|
ancli |
|- ( ph -> ( ph /\ L e. ( L ... M ) ) ) |
78 |
|
nfv |
|- F/ i L e. ( L ... M ) |
79 |
2 78
|
nfan |
|- F/ i ( ph /\ L e. ( L ... M ) ) |
80 |
|
nfcv |
|- F/_ i L |
81 |
1 80
|
nffv |
|- F/_ i ( B ` L ) |
82 |
81
|
nfel1 |
|- F/ i ( B ` L ) e. RR |
83 |
79 82
|
nfim |
|- F/ i ( ( ph /\ L e. ( L ... M ) ) -> ( B ` L ) e. RR ) |
84 |
|
eleq1 |
|- ( i = L -> ( i e. ( L ... M ) <-> L e. ( L ... M ) ) ) |
85 |
84
|
anbi2d |
|- ( i = L -> ( ( ph /\ i e. ( L ... M ) ) <-> ( ph /\ L e. ( L ... M ) ) ) ) |
86 |
|
fveq2 |
|- ( i = L -> ( B ` i ) = ( B ` L ) ) |
87 |
86
|
eleq1d |
|- ( i = L -> ( ( B ` i ) e. RR <-> ( B ` L ) e. RR ) ) |
88 |
85 87
|
imbi12d |
|- ( i = L -> ( ( ( ph /\ i e. ( L ... M ) ) -> ( B ` i ) e. RR ) <-> ( ( ph /\ L e. ( L ... M ) ) -> ( B ` L ) e. RR ) ) ) |
89 |
83 88 6
|
vtoclg1f |
|- ( L e. ( L ... M ) -> ( ( ph /\ L e. ( L ... M ) ) -> ( B ` L ) e. RR ) ) |
90 |
76 77 89
|
sylc |
|- ( ph -> ( B ` L ) e. RR ) |
91 |
16 90
|
eqeltrd |
|- ( ph -> ( seq L ( x. , B ) ` L ) e. RR ) |
92 |
91
|
adantr |
|- ( ( ph /\ L < M ) -> ( seq L ( x. , B ) ` L ) e. RR ) |
93 |
4
|
adantr |
|- ( ( ph /\ j e. ( ( L + 1 ) ... M ) ) -> L e. ZZ ) |
94 |
25
|
adantr |
|- ( ( ph /\ j e. ( ( L + 1 ) ... M ) ) -> M e. ZZ ) |
95 |
|
elfzelz |
|- ( j e. ( ( L + 1 ) ... M ) -> j e. ZZ ) |
96 |
95
|
adantl |
|- ( ( ph /\ j e. ( ( L + 1 ) ... M ) ) -> j e. ZZ ) |
97 |
23
|
adantr |
|- ( ( ph /\ j e. ( ( L + 1 ) ... M ) ) -> L e. RR ) |
98 |
|
peano2re |
|- ( L e. RR -> ( L + 1 ) e. RR ) |
99 |
23 98
|
syl |
|- ( ph -> ( L + 1 ) e. RR ) |
100 |
99
|
adantr |
|- ( ( ph /\ j e. ( ( L + 1 ) ... M ) ) -> ( L + 1 ) e. RR ) |
101 |
95
|
zred |
|- ( j e. ( ( L + 1 ) ... M ) -> j e. RR ) |
102 |
101
|
adantl |
|- ( ( ph /\ j e. ( ( L + 1 ) ... M ) ) -> j e. RR ) |
103 |
23
|
lep1d |
|- ( ph -> L <_ ( L + 1 ) ) |
104 |
103
|
adantr |
|- ( ( ph /\ j e. ( ( L + 1 ) ... M ) ) -> L <_ ( L + 1 ) ) |
105 |
|
elfzle1 |
|- ( j e. ( ( L + 1 ) ... M ) -> ( L + 1 ) <_ j ) |
106 |
105
|
adantl |
|- ( ( ph /\ j e. ( ( L + 1 ) ... M ) ) -> ( L + 1 ) <_ j ) |
107 |
97 100 102 104 106
|
letrd |
|- ( ( ph /\ j e. ( ( L + 1 ) ... M ) ) -> L <_ j ) |
108 |
|
elfzle2 |
|- ( j e. ( ( L + 1 ) ... M ) -> j <_ M ) |
109 |
108
|
adantl |
|- ( ( ph /\ j e. ( ( L + 1 ) ... M ) ) -> j <_ M ) |
110 |
93 94 96 107 109
|
elfzd |
|- ( ( ph /\ j e. ( ( L + 1 ) ... M ) ) -> j e. ( L ... M ) ) |
111 |
110 72
|
syldan |
|- ( ( ph /\ j e. ( ( L + 1 ) ... M ) ) -> ( B ` j ) e. RR ) |
112 |
111
|
adantlr |
|- ( ( ( ph /\ L < M ) /\ j e. ( ( L + 1 ) ... M ) ) -> ( B ` j ) e. RR ) |
113 |
57 112 36
|
seqcl |
|- ( ( ph /\ L < M ) -> ( seq ( L + 1 ) ( x. , B ) ` M ) e. RR ) |
114 |
92 113
|
remulcld |
|- ( ( ph /\ L < M ) -> ( ( seq L ( x. , B ) ` L ) x. ( seq ( L + 1 ) ( x. , B ) ` M ) ) e. RR ) |
115 |
9
|
rpred |
|- ( ph -> E e. RR ) |
116 |
115
|
adantr |
|- ( ( ph /\ L < M ) -> E e. RR ) |
117 |
|
1red |
|- ( ( ph /\ L < M ) -> 1 e. RR ) |
118 |
|
nfcv |
|- F/_ i 0 |
119 |
|
nfcv |
|- F/_ i <_ |
120 |
118 119 81
|
nfbr |
|- F/ i 0 <_ ( B ` L ) |
121 |
79 120
|
nfim |
|- F/ i ( ( ph /\ L e. ( L ... M ) ) -> 0 <_ ( B ` L ) ) |
122 |
86
|
breq2d |
|- ( i = L -> ( 0 <_ ( B ` i ) <-> 0 <_ ( B ` L ) ) ) |
123 |
85 122
|
imbi12d |
|- ( i = L -> ( ( ( ph /\ i e. ( L ... M ) ) -> 0 <_ ( B ` i ) ) <-> ( ( ph /\ L e. ( L ... M ) ) -> 0 <_ ( B ` L ) ) ) ) |
124 |
121 123 7
|
vtoclg1f |
|- ( L e. ( L ... M ) -> ( ( ph /\ L e. ( L ... M ) ) -> 0 <_ ( B ` L ) ) ) |
125 |
76 77 124
|
sylc |
|- ( ph -> 0 <_ ( B ` L ) ) |
126 |
125 16
|
breqtrrd |
|- ( ph -> 0 <_ ( seq L ( x. , B ) ` L ) ) |
127 |
126
|
adantr |
|- ( ( ph /\ L < M ) -> 0 <_ ( seq L ( x. , B ) ` L ) ) |
128 |
|
nfv |
|- F/ i L < M |
129 |
2 128
|
nfan |
|- F/ i ( ph /\ L < M ) |
130 |
|
eqid |
|- seq ( L + 1 ) ( x. , B ) = seq ( L + 1 ) ( x. , B ) |
131 |
4
|
peano2zd |
|- ( ph -> ( L + 1 ) e. ZZ ) |
132 |
131
|
adantr |
|- ( ( ph /\ L < M ) -> ( L + 1 ) e. ZZ ) |
133 |
23
|
adantr |
|- ( ( ph /\ L < M ) -> L e. RR ) |
134 |
133 45
|
gtned |
|- ( ( ph /\ L < M ) -> M =/= L ) |
135 |
134
|
neneqd |
|- ( ( ph /\ L < M ) -> -. M = L ) |
136 |
5
|
adantr |
|- ( ( ph /\ L < M ) -> M e. ( ZZ>= ` L ) ) |
137 |
136 53
|
syl |
|- ( ( ph /\ L < M ) -> ( M = L \/ M e. ( ZZ>= ` ( L + 1 ) ) ) ) |
138 |
|
orel1 |
|- ( -. M = L -> ( ( M = L \/ M e. ( ZZ>= ` ( L + 1 ) ) ) -> M e. ( ZZ>= ` ( L + 1 ) ) ) ) |
139 |
135 137 138
|
sylc |
|- ( ( ph /\ L < M ) -> M e. ( ZZ>= ` ( L + 1 ) ) ) |
140 |
25
|
adantr |
|- ( ( ph /\ L < M ) -> M e. ZZ ) |
141 |
|
zltp1le |
|- ( ( L e. ZZ /\ M e. ZZ ) -> ( L < M <-> ( L + 1 ) <_ M ) ) |
142 |
58 140 141
|
syl2anc |
|- ( ( ph /\ L < M ) -> ( L < M <-> ( L + 1 ) <_ M ) ) |
143 |
45 142
|
mpbid |
|- ( ( ph /\ L < M ) -> ( L + 1 ) <_ M ) |
144 |
26
|
adantr |
|- ( ( ph /\ L < M ) -> M e. RR ) |
145 |
144
|
leidd |
|- ( ( ph /\ L < M ) -> M <_ M ) |
146 |
132 140 140 143 145
|
elfzd |
|- ( ( ph /\ L < M ) -> M e. ( ( L + 1 ) ... M ) ) |
147 |
4
|
adantr |
|- ( ( ph /\ i e. ( ( L + 1 ) ... M ) ) -> L e. ZZ ) |
148 |
25
|
adantr |
|- ( ( ph /\ i e. ( ( L + 1 ) ... M ) ) -> M e. ZZ ) |
149 |
|
elfzelz |
|- ( i e. ( ( L + 1 ) ... M ) -> i e. ZZ ) |
150 |
149
|
adantl |
|- ( ( ph /\ i e. ( ( L + 1 ) ... M ) ) -> i e. ZZ ) |
151 |
23
|
adantr |
|- ( ( ph /\ i e. ( ( L + 1 ) ... M ) ) -> L e. RR ) |
152 |
151 98
|
syl |
|- ( ( ph /\ i e. ( ( L + 1 ) ... M ) ) -> ( L + 1 ) e. RR ) |
153 |
149
|
zred |
|- ( i e. ( ( L + 1 ) ... M ) -> i e. RR ) |
154 |
153
|
adantl |
|- ( ( ph /\ i e. ( ( L + 1 ) ... M ) ) -> i e. RR ) |
155 |
103
|
adantr |
|- ( ( ph /\ i e. ( ( L + 1 ) ... M ) ) -> L <_ ( L + 1 ) ) |
156 |
|
elfzle1 |
|- ( i e. ( ( L + 1 ) ... M ) -> ( L + 1 ) <_ i ) |
157 |
156
|
adantl |
|- ( ( ph /\ i e. ( ( L + 1 ) ... M ) ) -> ( L + 1 ) <_ i ) |
158 |
151 152 154 155 157
|
letrd |
|- ( ( ph /\ i e. ( ( L + 1 ) ... M ) ) -> L <_ i ) |
159 |
|
elfzle2 |
|- ( i e. ( ( L + 1 ) ... M ) -> i <_ M ) |
160 |
159
|
adantl |
|- ( ( ph /\ i e. ( ( L + 1 ) ... M ) ) -> i <_ M ) |
161 |
147 148 150 158 160
|
elfzd |
|- ( ( ph /\ i e. ( ( L + 1 ) ... M ) ) -> i e. ( L ... M ) ) |
162 |
161 6
|
syldan |
|- ( ( ph /\ i e. ( ( L + 1 ) ... M ) ) -> ( B ` i ) e. RR ) |
163 |
162
|
adantlr |
|- ( ( ( ph /\ L < M ) /\ i e. ( ( L + 1 ) ... M ) ) -> ( B ` i ) e. RR ) |
164 |
|
simpll |
|- ( ( ( ph /\ L < M ) /\ i e. ( ( L + 1 ) ... M ) ) -> ph ) |
165 |
4
|
ad2antrr |
|- ( ( ( ph /\ L < M ) /\ i e. ( ( L + 1 ) ... M ) ) -> L e. ZZ ) |
166 |
25
|
ad2antrr |
|- ( ( ( ph /\ L < M ) /\ i e. ( ( L + 1 ) ... M ) ) -> M e. ZZ ) |
167 |
149
|
adantl |
|- ( ( ( ph /\ L < M ) /\ i e. ( ( L + 1 ) ... M ) ) -> i e. ZZ ) |
168 |
23
|
ad2antrr |
|- ( ( ( ph /\ L < M ) /\ i e. ( ( L + 1 ) ... M ) ) -> L e. RR ) |
169 |
99
|
ad2antrr |
|- ( ( ( ph /\ L < M ) /\ i e. ( ( L + 1 ) ... M ) ) -> ( L + 1 ) e. RR ) |
170 |
153
|
adantl |
|- ( ( ( ph /\ L < M ) /\ i e. ( ( L + 1 ) ... M ) ) -> i e. RR ) |
171 |
103
|
ad2antrr |
|- ( ( ( ph /\ L < M ) /\ i e. ( ( L + 1 ) ... M ) ) -> L <_ ( L + 1 ) ) |
172 |
156
|
adantl |
|- ( ( ( ph /\ L < M ) /\ i e. ( ( L + 1 ) ... M ) ) -> ( L + 1 ) <_ i ) |
173 |
168 169 170 171 172
|
letrd |
|- ( ( ( ph /\ L < M ) /\ i e. ( ( L + 1 ) ... M ) ) -> L <_ i ) |
174 |
159
|
adantl |
|- ( ( ( ph /\ L < M ) /\ i e. ( ( L + 1 ) ... M ) ) -> i <_ M ) |
175 |
165 166 167 173 174
|
elfzd |
|- ( ( ( ph /\ L < M ) /\ i e. ( ( L + 1 ) ... M ) ) -> i e. ( L ... M ) ) |
176 |
164 175 7
|
syl2anc |
|- ( ( ( ph /\ L < M ) /\ i e. ( ( L + 1 ) ... M ) ) -> 0 <_ ( B ` i ) ) |
177 |
164 175 8
|
syl2anc |
|- ( ( ( ph /\ L < M ) /\ i e. ( ( L + 1 ) ... M ) ) -> ( B ` i ) <_ 1 ) |
178 |
1 129 130 132 139 146 163 176 177
|
fmul01 |
|- ( ( ph /\ L < M ) -> ( 0 <_ ( seq ( L + 1 ) ( x. , B ) ` M ) /\ ( seq ( L + 1 ) ( x. , B ) ` M ) <_ 1 ) ) |
179 |
178
|
simprd |
|- ( ( ph /\ L < M ) -> ( seq ( L + 1 ) ( x. , B ) ` M ) <_ 1 ) |
180 |
113 117 92 127 179
|
lemul2ad |
|- ( ( ph /\ L < M ) -> ( ( seq L ( x. , B ) ` L ) x. ( seq ( L + 1 ) ( x. , B ) ` M ) ) <_ ( ( seq L ( x. , B ) ` L ) x. 1 ) ) |
181 |
91
|
recnd |
|- ( ph -> ( seq L ( x. , B ) ` L ) e. CC ) |
182 |
181
|
mulid1d |
|- ( ph -> ( ( seq L ( x. , B ) ` L ) x. 1 ) = ( seq L ( x. , B ) ` L ) ) |
183 |
182
|
adantr |
|- ( ( ph /\ L < M ) -> ( ( seq L ( x. , B ) ` L ) x. 1 ) = ( seq L ( x. , B ) ` L ) ) |
184 |
180 183
|
breqtrd |
|- ( ( ph /\ L < M ) -> ( ( seq L ( x. , B ) ` L ) x. ( seq ( L + 1 ) ( x. , B ) ` M ) ) <_ ( seq L ( x. , B ) ` L ) ) |
185 |
16 10
|
eqbrtrd |
|- ( ph -> ( seq L ( x. , B ) ` L ) < E ) |
186 |
185
|
adantr |
|- ( ( ph /\ L < M ) -> ( seq L ( x. , B ) ` L ) < E ) |
187 |
114 92 116 184 186
|
lelttrd |
|- ( ( ph /\ L < M ) -> ( ( seq L ( x. , B ) ` L ) x. ( seq ( L + 1 ) ( x. , B ) ` M ) ) < E ) |
188 |
74 187
|
eqbrtrd |
|- ( ( ph /\ L < M ) -> ( seq L ( x. , B ) ` M ) < E ) |
189 |
34 188
|
eqbrtrid |
|- ( ( ph /\ L < M ) -> ( A ` M ) < E ) |
190 |
33 189
|
syldan |
|- ( ( ph /\ -. M = L ) -> ( A ` M ) < E ) |
191 |
20 190
|
pm2.61dan |
|- ( ph -> ( A ` M ) < E ) |