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	$⊢ \underline{Ⅎ} i B$
	fmul01lt1lem2.2	$⊢ Ⅎ i φ$
	fmul01lt1lem2.3	$⊢ A = seq L (\times B)$
	fmul01lt1lem2.4	$⊢ φ \to L \in ℤ$
	fmul01lt1lem2.5	$⊢ φ \to M \in ℤ_{\geq L}$
	fmul01lt1lem2.6	$⊢ (φ \land i \in (L \dots M)) \to B (i) \in ℝ$
	fmul01lt1lem2.7	$⊢ (φ \land i \in (L \dots M)) \to 0 \leq B (i)$
	fmul01lt1lem2.8	$⊢ (φ \land i \in (L \dots M)) \to B (i) \leq 1$
	fmul01lt1lem2.9	$⊢ φ \to E \in ℝ^{+}$
	fmul01lt1lem2.10	$⊢ φ \to J \in (L \dots M)$
	fmul01lt1lem2.11	$⊢ φ \to B (J) < E$
Assertion	fmul01lt1lem2	$⊢ φ \to A (M) < E$

Proof

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

Metamath Proof Explorer

Theorem fmul01lt1lem2

Proof