# 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 ${⊢}\underset{_}{Ⅎ}{i}\phantom{\rule{.4em}{0ex}}{B}$
fmul01lt1lem2.2 ${⊢}Ⅎ{i}\phantom{\rule{.4em}{0ex}}{\phi }$
fmul01lt1lem2.3 ${⊢}{A}=seq{L}\left(×,{B}\right)$
fmul01lt1lem2.4 ${⊢}{\phi }\to {L}\in ℤ$
fmul01lt1lem2.5 ${⊢}{\phi }\to {M}\in {ℤ}_{\ge {L}}$
fmul01lt1lem2.6 ${⊢}\left({\phi }\wedge {i}\in \left({L}\dots {M}\right)\right)\to {B}\left({i}\right)\in ℝ$
fmul01lt1lem2.7 ${⊢}\left({\phi }\wedge {i}\in \left({L}\dots {M}\right)\right)\to 0\le {B}\left({i}\right)$
fmul01lt1lem2.8 ${⊢}\left({\phi }\wedge {i}\in \left({L}\dots {M}\right)\right)\to {B}\left({i}\right)\le 1$
fmul01lt1lem2.9 ${⊢}{\phi }\to {E}\in {ℝ}^{+}$
fmul01lt1lem2.10 ${⊢}{\phi }\to {J}\in \left({L}\dots {M}\right)$
fmul01lt1lem2.11 ${⊢}{\phi }\to {B}\left({J}\right)<{E}$
Assertion fmul01lt1lem2 ${⊢}{\phi }\to {A}\left({M}\right)<{E}$

### Proof

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