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 ⊢ Ⅎ 𝑖 𝐵
fmul01lt1lem1.2 ⊢ Ⅎ 𝑖 𝜑
fmul01lt1lem1.3 ⊢ 𝐴 = seq 𝐿 ( · , 𝐵 )
fmul01lt1lem1.4 ⊢ ( 𝜑 → 𝐿 ∈ ℤ )
fmul01lt1lem1.5 ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 𝐿 ) )
fmul01lt1lem1.6 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐿 ... 𝑀 ) ) → ( 𝐵 ‘ 𝑖 ) ∈ ℝ )
fmul01lt1lem1.7 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐿 ... 𝑀 ) ) → 0 ≤ ( 𝐵 ‘ 𝑖 ) )
fmul01lt1lem1.8 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐿 ... 𝑀 ) ) → ( 𝐵 ‘ 𝑖 ) ≤ 1 )
fmul01lt1lem1.9 ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
fmul01lt1lem1.10 ⊢ ( 𝜑 → ( 𝐵 ‘ 𝐿 ) < 𝐸 )
Assertion fmul01lt1lem1 ( 𝜑 → ( 𝐴 ‘ 𝑀 ) < 𝐸 )

Proof

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