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

Proof

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

Metamath Proof Explorer

Theorem fmul01lt1lem1

Proof