Metamath Proof Explorer

Theorem fmul01lt1lem2

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

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

Proof

Step Hyp Ref Expression
1 fmul01lt1lem2.1 
 |-  F/_ i B
2 fmul01lt1lem2.2 
 |-  F/ i ph
3 fmul01lt1lem2.3 
 |-  A = seq L ( x. , B )
4 fmul01lt1lem2.4 
 |-  ( ph -> L e. ZZ )
5 fmul01lt1lem2.5 
 |-  ( ph -> M e. ( ZZ>= ` L ) )
6 fmul01lt1lem2.6 
 |-  ( ( ph /\ i e. ( L ... M ) ) -> ( B ` i ) e. RR )
7 fmul01lt1lem2.7 
 |-  ( ( ph /\ i e. ( L ... M ) ) -> 0 <_ ( B ` i ) )
8 fmul01lt1lem2.8 
 |-  ( ( ph /\ i e. ( L ... M ) ) -> ( B ` i ) <_ 1 )
9 fmul01lt1lem2.9 
 |-  ( ph -> E e. RR+ )
10 fmul01lt1lem2.10 
 |-  ( ph -> J e. ( L ... M ) )
11 fmul01lt1lem2.11 
 |-  ( ph -> ( B ` J ) < E )
12 nfv 
 |-  F/ i J = L
13 2 12 nfan 
 |-  F/ i ( ph /\ J = L )
14 4 adantr 
 |-  ( ( ph /\ J = L ) -> L e. ZZ )
15 5 adantr 
 |-  ( ( ph /\ J = L ) -> M e. ( ZZ>= ` L ) )
16 6 adantlr 
 |-  ( ( ( ph /\ J = L ) /\ i e. ( L ... M ) ) -> ( B ` i ) e. RR )
17 7 adantlr 
 |-  ( ( ( ph /\ J = L ) /\ i e. ( L ... M ) ) -> 0 <_ ( B ` i ) )
18 8 adantlr 
 |-  ( ( ( ph /\ J = L ) /\ i e. ( L ... M ) ) -> ( B ` i ) <_ 1 )
19 9 adantr 
 |-  ( ( ph /\ J = L ) -> E e. RR+ )
20 simpr 
 |-  ( ( ph /\ J = L ) -> J = L )
21 20 fveq2d 
 |-  ( ( ph /\ J = L ) -> ( B ` J ) = ( B ` L ) )
22 11 adantr 
 |-  ( ( ph /\ J = L ) -> ( B ` J ) < E )
23 21 22 eqbrtrrd 
 |-  ( ( ph /\ J = L ) -> ( B ` L ) < E )
24 1 13 3 14 15 16 17 18 19 23 fmul01lt1lem1 
 |-  ( ( ph /\ J = L ) -> ( A ` M ) < E )
25 3 fveq1i 
 |-  ( A ` M ) = ( seq L ( x. , B ) ` M )
26 nfv 
 |-  F/ i a e. ( L ... M )
27 2 26 nfan 
 |-  F/ i ( ph /\ a e. ( L ... M ) )
28 nfcv 
 |-  F/_ i a
29 1 28 nffv 
 |-  F/_ i ( B ` a )
30 29 nfel1 
 |-  F/ i ( B ` a ) e. RR
31 27 30 nfim 
 |-  F/ i ( ( ph /\ a e. ( L ... M ) ) -> ( B ` a ) e. RR )
32 eleq1w 
 |-  ( i = a -> ( i e. ( L ... M ) <-> a e. ( L ... M ) ) )
33 32 anbi2d 
 |-  ( i = a -> ( ( ph /\ i e. ( L ... M ) ) <-> ( ph /\ a e. ( L ... M ) ) ) )
34 fveq2 
 |-  ( i = a -> ( B ` i ) = ( B ` a ) )
35 34 eleq1d 
 |-  ( i = a -> ( ( B ` i ) e. RR <-> ( B ` a ) e. RR ) )
36 33 35 imbi12d 
 |-  ( i = a -> ( ( ( ph /\ i e. ( L ... M ) ) -> ( B ` i ) e. RR ) <-> ( ( ph /\ a e. ( L ... M ) ) -> ( B ` a ) e. RR ) ) )
37 31 36 6 chvarfv 
 |-  ( ( ph /\ a e. ( L ... M ) ) -> ( B ` a ) e. RR )
38 remulcl 
 |-  ( ( a e. RR /\ j e. RR ) -> ( a x. j ) e. RR )
39 38 adantl 
 |-  ( ( ph /\ ( a e. RR /\ j e. RR ) ) -> ( a x. j ) e. RR )
40 5 37 39 seqcl 
 |-  ( ph -> ( seq L ( x. , B ) ` M ) e. RR )
41 40 adantr 
 |-  ( ( ph /\ -. J = L ) -> ( seq L ( x. , B ) ` M ) e. RR )
42 elfzuz3 
 |-  ( J e. ( L ... M ) -> M e. ( ZZ>= ` J ) )
43 10 42 syl 
 |-  ( ph -> M e. ( ZZ>= ` J ) )
44 nfv 
 |-  F/ i a e. ( J ... M )
45 2 44 nfan 
 |-  F/ i ( ph /\ a e. ( J ... M ) )
46 45 30 nfim 
 |-  F/ i ( ( ph /\ a e. ( J ... M ) ) -> ( B ` a ) e. RR )
47 eleq1w 
 |-  ( i = a -> ( i e. ( J ... M ) <-> a e. ( J ... M ) ) )
48 47 anbi2d 
 |-  ( i = a -> ( ( ph /\ i e. ( J ... M ) ) <-> ( ph /\ a e. ( J ... M ) ) ) )
49 48 35 imbi12d 
 |-  ( i = a -> ( ( ( ph /\ i e. ( J ... M ) ) -> ( B ` i ) e. RR ) <-> ( ( ph /\ a e. ( J ... M ) ) -> ( B ` a ) e. RR ) ) )
50 4 adantr 
 |-  ( ( ph /\ i e. ( J ... M ) ) -> L e. ZZ )
51 eluzelz 
 |-  ( M e. ( ZZ>= ` L ) -> M e. ZZ )
52 5 51 syl 
 |-  ( ph -> M e. ZZ )
53 52 adantr 
 |-  ( ( ph /\ i e. ( J ... M ) ) -> M e. ZZ )
54 elfzelz 
 |-  ( i e. ( J ... M ) -> i e. ZZ )
55 54 adantl 
 |-  ( ( ph /\ i e. ( J ... M ) ) -> i e. ZZ )
56 4 zred 
 |-  ( ph -> L e. RR )
57 56 adantr 
 |-  ( ( ph /\ i e. ( J ... M ) ) -> L e. RR )
58 elfzelz 
 |-  ( J e. ( L ... M ) -> J e. ZZ )
59 10 58 syl 
 |-  ( ph -> J e. ZZ )
60 59 zred 
 |-  ( ph -> J e. RR )
61 60 adantr 
 |-  ( ( ph /\ i e. ( J ... M ) ) -> J e. RR )
62 54 zred 
 |-  ( i e. ( J ... M ) -> i e. RR )
63 62 adantl 
 |-  ( ( ph /\ i e. ( J ... M ) ) -> i e. RR )
64 elfzle1 
 |-  ( J e. ( L ... M ) -> L <_ J )
65 10 64 syl 
 |-  ( ph -> L <_ J )
66 65 adantr 
 |-  ( ( ph /\ i e. ( J ... M ) ) -> L <_ J )
67 elfzle1 
 |-  ( i e. ( J ... M ) -> J <_ i )
68 67 adantl 
 |-  ( ( ph /\ i e. ( J ... M ) ) -> J <_ i )
69 57 61 63 66 68 letrd 
 |-  ( ( ph /\ i e. ( J ... M ) ) -> L <_ i )
70 elfzle2 
 |-  ( i e. ( J ... M ) -> i <_ M )
71 70 adantl 
 |-  ( ( ph /\ i e. ( J ... M ) ) -> i <_ M )
72 50 53 55 69 71 elfzd 
 |-  ( ( ph /\ i e. ( J ... M ) ) -> i e. ( L ... M ) )
73 72 6 syldan 
 |-  ( ( ph /\ i e. ( J ... M ) ) -> ( B ` i ) e. RR )
74 46 49 73 chvarfv 
 |-  ( ( ph /\ a e. ( J ... M ) ) -> ( B ` a ) e. RR )
75 43 74 39 seqcl 
 |-  ( ph -> ( seq J ( x. , B ) ` M ) e. RR )
76 75 adantr 
 |-  ( ( ph /\ -. J = L ) -> ( seq J ( x. , B ) ` M ) e. RR )
77 9 rpred 
 |-  ( ph -> E e. RR )
78 77 adantr 
 |-  ( ( ph /\ -. J = L ) -> E e. RR )
79 remulcl 
 |-  ( ( a e. RR /\ b e. RR ) -> ( a x. b ) e. RR )
80 79 adantl 
 |-  ( ( ( ph /\ -. J = L ) /\ ( a e. RR /\ b e. RR ) ) -> ( a x. b ) e. RR )
81 simp1 
 |-  ( ( a e. RR /\ b e. RR /\ c e. RR ) -> a e. RR )
82 81 recnd 
 |-  ( ( a e. RR /\ b e. RR /\ c e. RR ) -> a e. CC )
83 simp2 
 |-  ( ( a e. RR /\ b e. RR /\ c e. RR ) -> b e. RR )
84 83 recnd 
 |-  ( ( a e. RR /\ b e. RR /\ c e. RR ) -> b e. CC )
85 simp3 
 |-  ( ( a e. RR /\ b e. RR /\ c e. RR ) -> c e. RR )
86 85 recnd 
 |-  ( ( a e. RR /\ b e. RR /\ c e. RR ) -> c e. CC )
87 82 84 86 mulassd 
 |-  ( ( a e. RR /\ b e. RR /\ c e. RR ) -> ( ( a x. b ) x. c ) = ( a x. ( b x. c ) ) )
88 87 adantl 
 |-  ( ( ( ph /\ -. J = L ) /\ ( a e. RR /\ b e. RR /\ c e. RR ) ) -> ( ( a x. b ) x. c ) = ( a x. ( b x. c ) ) )
89 59 zcnd 
 |-  ( ph -> J e. CC )
90 1cnd 
 |-  ( ph -> 1 e. CC )
91 89 90 npcand 
 |-  ( ph -> ( ( J - 1 ) + 1 ) = J )
92 91 fveq2d 
 |-  ( ph -> ( ZZ>= ` ( ( J - 1 ) + 1 ) ) = ( ZZ>= ` J ) )
93 43 92 eleqtrrd 
 |-  ( ph -> M e. ( ZZ>= ` ( ( J - 1 ) + 1 ) ) )
94 93 adantr 
 |-  ( ( ph /\ -. J = L ) -> M e. ( ZZ>= ` ( ( J - 1 ) + 1 ) ) )
95 4 adantr 
 |-  ( ( ph /\ -. J = L ) -> L e. ZZ )
96 59 adantr 
 |-  ( ( ph /\ -. J = L ) -> J e. ZZ )
97 1zzd 
 |-  ( ( ph /\ -. J = L ) -> 1 e. ZZ )
98 96 97 zsubcld 
 |-  ( ( ph /\ -. J = L ) -> ( J - 1 ) e. ZZ )
99 simpr 
 |-  ( ( ph /\ -. J = L ) -> -. J = L )
100 eqcom 
 |-  ( J = L <-> L = J )
101 99 100 sylnib 
 |-  ( ( ph /\ -. J = L ) -> -. L = J )
102 56 60 leloed 
 |-  ( ph -> ( L <_ J <-> ( L < J \/ L = J ) ) )
103 65 102 mpbid 
 |-  ( ph -> ( L < J \/ L = J ) )
104 103 adantr 
 |-  ( ( ph /\ -. J = L ) -> ( L < J \/ L = J ) )
105 orel2 
 |-  ( -. L = J -> ( ( L < J \/ L = J ) -> L < J ) )
106 101 104 105 sylc 
 |-  ( ( ph /\ -. J = L ) -> L < J )
107 zltlem1 
 |-  ( ( L e. ZZ /\ J e. ZZ ) -> ( L < J <-> L <_ ( J - 1 ) ) )
108 4 59 107 syl2anc 
 |-  ( ph -> ( L < J <-> L <_ ( J - 1 ) ) )
109 108 adantr 
 |-  ( ( ph /\ -. J = L ) -> ( L < J <-> L <_ ( J - 1 ) ) )
110 106 109 mpbid 
 |-  ( ( ph /\ -. J = L ) -> L <_ ( J - 1 ) )
111 eluz2 
 |-  ( ( J - 1 ) e. ( ZZ>= ` L ) <-> ( L e. ZZ /\ ( J - 1 ) e. ZZ /\ L <_ ( J - 1 ) ) )
112 95 98 110 111 syl3anbrc 
 |-  ( ( ph /\ -. J = L ) -> ( J - 1 ) e. ( ZZ>= ` L ) )
113 nfv 
 |-  F/ i -. J = L
114 2 113 nfan 
 |-  F/ i ( ph /\ -. J = L )
115 114 26 nfan 
 |-  F/ i ( ( ph /\ -. J = L ) /\ a e. ( L ... M ) )
116 115 30 nfim 
 |-  F/ i ( ( ( ph /\ -. J = L ) /\ a e. ( L ... M ) ) -> ( B ` a ) e. RR )
117 32 anbi2d 
 |-  ( i = a -> ( ( ( ph /\ -. J = L ) /\ i e. ( L ... M ) ) <-> ( ( ph /\ -. J = L ) /\ a e. ( L ... M ) ) ) )
118 117 35 imbi12d 
 |-  ( i = a -> ( ( ( ( ph /\ -. J = L ) /\ i e. ( L ... M ) ) -> ( B ` i ) e. RR ) <-> ( ( ( ph /\ -. J = L ) /\ a e. ( L ... M ) ) -> ( B ` a ) e. RR ) ) )
119 6 adantlr 
 |-  ( ( ( ph /\ -. J = L ) /\ i e. ( L ... M ) ) -> ( B ` i ) e. RR )
120 116 118 119 chvarfv 
 |-  ( ( ( ph /\ -. J = L ) /\ a e. ( L ... M ) ) -> ( B ` a ) e. RR )
121 80 88 94 112 120 seqsplit 
 |-  ( ( ph /\ -. J = L ) -> ( seq L ( x. , B ) ` M ) = ( ( seq L ( x. , B ) ` ( J - 1 ) ) x. ( seq ( ( J - 1 ) + 1 ) ( x. , B ) ` M ) ) )
122 91 adantr 
 |-  ( ( ph /\ -. J = L ) -> ( ( J - 1 ) + 1 ) = J )
123 122 seqeq1d 
 |-  ( ( ph /\ -. J = L ) -> seq ( ( J - 1 ) + 1 ) ( x. , B ) = seq J ( x. , B ) )
124 123 fveq1d 
 |-  ( ( ph /\ -. J = L ) -> ( seq ( ( J - 1 ) + 1 ) ( x. , B ) ` M ) = ( seq J ( x. , B ) ` M ) )
125 124 oveq2d 
 |-  ( ( ph /\ -. J = L ) -> ( ( seq L ( x. , B ) ` ( J - 1 ) ) x. ( seq ( ( J - 1 ) + 1 ) ( x. , B ) ` M ) ) = ( ( seq L ( x. , B ) ` ( J - 1 ) ) x. ( seq J ( x. , B ) ` M ) ) )
126 121 125 eqtrd 
 |-  ( ( ph /\ -. J = L ) -> ( seq L ( x. , B ) ` M ) = ( ( seq L ( x. , B ) ` ( J - 1 ) ) x. ( seq J ( x. , B ) ` M ) ) )
127 nfv 
 |-  F/ i a e. ( L ... ( J - 1 ) )
128 114 127 nfan 
 |-  F/ i ( ( ph /\ -. J = L ) /\ a e. ( L ... ( J - 1 ) ) )
129 128 30 nfim 
 |-  F/ i ( ( ( ph /\ -. J = L ) /\ a e. ( L ... ( J - 1 ) ) ) -> ( B ` a ) e. RR )
130 eleq1w 
 |-  ( i = a -> ( i e. ( L ... ( J - 1 ) ) <-> a e. ( L ... ( J - 1 ) ) ) )
131 130 anbi2d 
 |-  ( i = a -> ( ( ( ph /\ -. J = L ) /\ i e. ( L ... ( J - 1 ) ) ) <-> ( ( ph /\ -. J = L ) /\ a e. ( L ... ( J - 1 ) ) ) ) )
132 131 35 imbi12d 
 |-  ( i = a -> ( ( ( ( ph /\ -. J = L ) /\ i e. ( L ... ( J - 1 ) ) ) -> ( B ` i ) e. RR ) <-> ( ( ( ph /\ -. J = L ) /\ a e. ( L ... ( J - 1 ) ) ) -> ( B ` a ) e. RR ) ) )
133 4 adantr 
 |-  ( ( ph /\ i e. ( L ... ( J - 1 ) ) ) -> L e. ZZ )
134 52 adantr 
 |-  ( ( ph /\ i e. ( L ... ( J - 1 ) ) ) -> M e. ZZ )
135 elfzelz 
 |-  ( i e. ( L ... ( J - 1 ) ) -> i e. ZZ )
136 135 adantl 
 |-  ( ( ph /\ i e. ( L ... ( J - 1 ) ) ) -> i e. ZZ )
137 elfzle1 
 |-  ( i e. ( L ... ( J - 1 ) ) -> L <_ i )
138 137 adantl 
 |-  ( ( ph /\ i e. ( L ... ( J - 1 ) ) ) -> L <_ i )
139 135 zred 
 |-  ( i e. ( L ... ( J - 1 ) ) -> i e. RR )
140 139 adantl 
 |-  ( ( ph /\ i e. ( L ... ( J - 1 ) ) ) -> i e. RR )
141 60 adantr 
 |-  ( ( ph /\ i e. ( L ... ( J - 1 ) ) ) -> J e. RR )
142 52 zred 
 |-  ( ph -> M e. RR )
143 142 adantr 
 |-  ( ( ph /\ i e. ( L ... ( J - 1 ) ) ) -> M e. RR )
144 1red 
 |-  ( ph -> 1 e. RR )
145 60 144 resubcld 
 |-  ( ph -> ( J - 1 ) e. RR )
146 145 adantr 
 |-  ( ( ph /\ i e. ( L ... ( J - 1 ) ) ) -> ( J - 1 ) e. RR )
147 elfzle2 
 |-  ( i e. ( L ... ( J - 1 ) ) -> i <_ ( J - 1 ) )
148 147 adantl 
 |-  ( ( ph /\ i e. ( L ... ( J - 1 ) ) ) -> i <_ ( J - 1 ) )
149 60 lem1d 
 |-  ( ph -> ( J - 1 ) <_ J )
150 149 adantr 
 |-  ( ( ph /\ i e. ( L ... ( J - 1 ) ) ) -> ( J - 1 ) <_ J )
151 140 146 141 148 150 letrd 
 |-  ( ( ph /\ i e. ( L ... ( J - 1 ) ) ) -> i <_ J )
152 elfzle2 
 |-  ( J e. ( L ... M ) -> J <_ M )
153 10 152 syl 
 |-  ( ph -> J <_ M )
154 153 adantr 
 |-  ( ( ph /\ i e. ( L ... ( J - 1 ) ) ) -> J <_ M )
155 140 141 143 151 154 letrd 
 |-  ( ( ph /\ i e. ( L ... ( J - 1 ) ) ) -> i <_ M )
156 133 134 136 138 155 elfzd 
 |-  ( ( ph /\ i e. ( L ... ( J - 1 ) ) ) -> i e. ( L ... M ) )
157 156 6 syldan 
 |-  ( ( ph /\ i e. ( L ... ( J - 1 ) ) ) -> ( B ` i ) e. RR )
158 157 adantlr 
 |-  ( ( ( ph /\ -. J = L ) /\ i e. ( L ... ( J - 1 ) ) ) -> ( B ` i ) e. RR )
159 129 132 158 chvarfv 
 |-  ( ( ( ph /\ -. J = L ) /\ a e. ( L ... ( J - 1 ) ) ) -> ( B ` a ) e. RR )
160 38 adantl 
 |-  ( ( ( ph /\ -. J = L ) /\ ( a e. RR /\ j e. RR ) ) -> ( a x. j ) e. RR )
161 112 159 160 seqcl 
 |-  ( ( ph /\ -. J = L ) -> ( seq L ( x. , B ) ` ( J - 1 ) ) e. RR )
162 1red 
 |-  ( ( ph /\ -. J = L ) -> 1 e. RR )
163 eqid 
 |-  seq J ( x. , B ) = seq J ( x. , B )
164 43 adantr 
 |-  ( ( ph /\ -. J = L ) -> M e. ( ZZ>= ` J ) )
165 eluzfz2 
 |-  ( M e. ( ZZ>= ` J ) -> M e. ( J ... M ) )
166 43 165 syl 
 |-  ( ph -> M e. ( J ... M ) )
167 166 adantr 
 |-  ( ( ph /\ -. J = L ) -> M e. ( J ... M ) )
168 73 adantlr 
 |-  ( ( ( ph /\ -. J = L ) /\ i e. ( J ... M ) ) -> ( B ` i ) e. RR )
169 72 7 syldan 
 |-  ( ( ph /\ i e. ( J ... M ) ) -> 0 <_ ( B ` i ) )
170 169 adantlr 
 |-  ( ( ( ph /\ -. J = L ) /\ i e. ( J ... M ) ) -> 0 <_ ( B ` i ) )
171 72 8 syldan 
 |-  ( ( ph /\ i e. ( J ... M ) ) -> ( B ` i ) <_ 1 )
172 171 adantlr 
 |-  ( ( ( ph /\ -. J = L ) /\ i e. ( J ... M ) ) -> ( B ` i ) <_ 1 )
173 1 114 163 96 164 167 168 170 172 fmul01 
 |-  ( ( ph /\ -. J = L ) -> ( 0 <_ ( seq J ( x. , B ) ` M ) /\ ( seq J ( x. , B ) ` M ) <_ 1 ) )
174 173 simpld 
 |-  ( ( ph /\ -. J = L ) -> 0 <_ ( seq J ( x. , B ) ` M ) )
175 eqid 
 |-  seq L ( x. , B ) = seq L ( x. , B )
176 5 adantr 
 |-  ( ( ph /\ -. J = L ) -> M e. ( ZZ>= ` L ) )
177 1zzd 
 |-  ( ph -> 1 e. ZZ )
178 59 177 zsubcld 
 |-  ( ph -> ( J - 1 ) e. ZZ )
179 4 52 178 3jca 
 |-  ( ph -> ( L e. ZZ /\ M e. ZZ /\ ( J - 1 ) e. ZZ ) )
180 179 adantr 
 |-  ( ( ph /\ -. J = L ) -> ( L e. ZZ /\ M e. ZZ /\ ( J - 1 ) e. ZZ ) )
181 145 60 142 3jca 
 |-  ( ph -> ( ( J - 1 ) e. RR /\ J e. RR /\ M e. RR ) )
182 181 adantr 
 |-  ( ( ph /\ -. J = L ) -> ( ( J - 1 ) e. RR /\ J e. RR /\ M e. RR ) )
183 60 adantr 
 |-  ( ( ph /\ -. J = L ) -> J e. RR )
184 183 lem1d 
 |-  ( ( ph /\ -. J = L ) -> ( J - 1 ) <_ J )
185 153 adantr 
 |-  ( ( ph /\ -. J = L ) -> J <_ M )
186 184 185 jca 
 |-  ( ( ph /\ -. J = L ) -> ( ( J - 1 ) <_ J /\ J <_ M ) )
187 letr 
 |-  ( ( ( J - 1 ) e. RR /\ J e. RR /\ M e. RR ) -> ( ( ( J - 1 ) <_ J /\ J <_ M ) -> ( J - 1 ) <_ M ) )
188 182 186 187 sylc 
 |-  ( ( ph /\ -. J = L ) -> ( J - 1 ) <_ M )
189 110 188 jca 
 |-  ( ( ph /\ -. J = L ) -> ( L <_ ( J - 1 ) /\ ( J - 1 ) <_ M ) )
190 elfz2 
 |-  ( ( J - 1 ) e. ( L ... M ) <-> ( ( L e. ZZ /\ M e. ZZ /\ ( J - 1 ) e. ZZ ) /\ ( L <_ ( J - 1 ) /\ ( J - 1 ) <_ M ) ) )
191 180 189 190 sylanbrc 
 |-  ( ( ph /\ -. J = L ) -> ( J - 1 ) e. ( L ... M ) )
192 7 adantlr 
 |-  ( ( ( ph /\ -. J = L ) /\ i e. ( L ... M ) ) -> 0 <_ ( B ` i ) )
193 8 adantlr 
 |-  ( ( ( ph /\ -. J = L ) /\ i e. ( L ... M ) ) -> ( B ` i ) <_ 1 )
194 1 114 175 95 176 191 119 192 193 fmul01 
 |-  ( ( ph /\ -. J = L ) -> ( 0 <_ ( seq L ( x. , B ) ` ( J - 1 ) ) /\ ( seq L ( x. , B ) ` ( J - 1 ) ) <_ 1 ) )
195 194 simprd 
 |-  ( ( ph /\ -. J = L ) -> ( seq L ( x. , B ) ` ( J - 1 ) ) <_ 1 )
196 161 162 76 174 195 lemul1ad 
 |-  ( ( ph /\ -. J = L ) -> ( ( seq L ( x. , B ) ` ( J - 1 ) ) x. ( seq J ( x. , B ) ` M ) ) <_ ( 1 x. ( seq J ( x. , B ) ` M ) ) )
197 126 196 eqbrtrd 
 |-  ( ( ph /\ -. J = L ) -> ( seq L ( x. , B ) ` M ) <_ ( 1 x. ( seq J ( x. , B ) ` M ) ) )
198 76 recnd 
 |-  ( ( ph /\ -. J = L ) -> ( seq J ( x. , B ) ` M ) e. CC )
199 198 mullidd 
 |-  ( ( ph /\ -. J = L ) -> ( 1 x. ( seq J ( x. , B ) ` M ) ) = ( seq J ( x. , B ) ` M ) )
200 197 199 breqtrd 
 |-  ( ( ph /\ -. J = L ) -> ( seq L ( x. , B ) ` M ) <_ ( seq J ( x. , B ) ` M ) )
201 1 2 163 59 43 73 169 171 9 11 fmul01lt1lem1 
 |-  ( ph -> ( seq J ( x. , B ) ` M ) < E )
202 201 adantr 
 |-  ( ( ph /\ -. J = L ) -> ( seq J ( x. , B ) ` M ) < E )
203 41 76 78 200 202 lelttrd 
 |-  ( ( ph /\ -. J = L ) -> ( seq L ( x. , B ) ` M ) < E )
204 25 203 eqbrtrid 
 |-  ( ( ph /\ -. J = L ) -> ( A ` M ) < E )
205 24 204 pm2.61dan 
 |-  ( ph -> ( A ` M ) < E )