# Metamath Proof Explorer

## Theorem fmul01lt1lem2

Description: Given a finite multiplication of values betweeen 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 𝑖 𝐵
fmul01lt1lem2.2 𝑖 𝜑
fmul01lt1lem2.3 𝐴 = seq 𝐿 ( · , 𝐵 )
fmul01lt1lem2.4 ( 𝜑𝐿 ∈ ℤ )
fmul01lt1lem2.5 ( 𝜑𝑀 ∈ ( ℤ𝐿 ) )
fmul01lt1lem2.6 ( ( 𝜑𝑖 ∈ ( 𝐿 ... 𝑀 ) ) → ( 𝐵𝑖 ) ∈ ℝ )
fmul01lt1lem2.7 ( ( 𝜑𝑖 ∈ ( 𝐿 ... 𝑀 ) ) → 0 ≤ ( 𝐵𝑖 ) )
fmul01lt1lem2.8 ( ( 𝜑𝑖 ∈ ( 𝐿 ... 𝑀 ) ) → ( 𝐵𝑖 ) ≤ 1 )
fmul01lt1lem2.9 ( 𝜑𝐸 ∈ ℝ+ )
fmul01lt1lem2.10 ( 𝜑𝐽 ∈ ( 𝐿 ... 𝑀 ) )
fmul01lt1lem2.11 ( 𝜑 → ( 𝐵𝐽 ) < 𝐸 )
Assertion fmul01lt1lem2 ( 𝜑 → ( 𝐴𝑀 ) < 𝐸 )

### Proof

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