Metamath Proof Explorer


Theorem fmul01lt1lem1

Description: Given a finite multiplication of values betweeen 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 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 )