Metamath Proof Explorer

Theorem fmul01lt1lem1

Description: Given a finite multiplication of values between 0 and 1, a value larger than its first element is larger the whole multiplication. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses fmul01lt1lem1.1 
|- F/_ i B
fmul01lt1lem1.2 
|- F/ i ph
fmul01lt1lem1.3 
|- A = seq L ( x. , B )
fmul01lt1lem1.4 
|- ( ph -> L e. ZZ )
fmul01lt1lem1.5 
|- ( ph -> M e. ( ZZ>= ` L ) )
fmul01lt1lem1.6 
|- ( ( ph /\ i e. ( L ... M ) ) -> ( B ` i ) e. RR )
fmul01lt1lem1.7 
|- ( ( ph /\ i e. ( L ... M ) ) -> 0 <_ ( B ` i ) )
fmul01lt1lem1.8 
|- ( ( ph /\ i e. ( L ... M ) ) -> ( B ` i ) <_ 1 )
fmul01lt1lem1.9 
|- ( ph -> E e. RR+ )
fmul01lt1lem1.10 
|- ( ph -> ( B ` L ) < E )
Assertion fmul01lt1lem1 
|- ( ph -> ( A ` M ) < E )

Proof

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