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	93 94 96	3jca	$⊢ (φ \land j \in (L + 1 \dots M)) \to (L \in ℤ \land M \in ℤ \land j \in ℤ)$
98	23	adantr	$⊢ (φ \land j \in (L + 1 \dots M)) \to L \in ℝ$
99		peano2re	$⊢ L \in ℝ \to L + 1 \in ℝ$
100	23 99	syl	$⊢ φ \to L + 1 \in ℝ$
101	100	adantr	$⊢ (φ \land j \in (L + 1 \dots M)) \to L + 1 \in ℝ$
102	95	zred	$⊢ j \in (L + 1 \dots M) \to j \in ℝ$
103	102	adantl	$⊢ (φ \land j \in (L + 1 \dots M)) \to j \in ℝ$
104	23	lep1d	$⊢ φ \to L \leq L + 1$
105	104	adantr	$⊢ (φ \land j \in (L + 1 \dots M)) \to L \leq L + 1$
106		elfzle1	$⊢ j \in (L + 1 \dots M) \to L + 1 \leq j$
107	106	adantl	$⊢ (φ \land j \in (L + 1 \dots M)) \to L + 1 \leq j$
108	98 101 103 105 107	letrd	$⊢ (φ \land j \in (L + 1 \dots M)) \to L \leq j$
109		elfzle2	$⊢ j \in (L + 1 \dots M) \to j \leq M$
110	109	adantl	$⊢ (φ \land j \in (L + 1 \dots M)) \to j \leq M$
111	108 110	jca	$⊢ (φ \land j \in (L + 1 \dots M)) \to (L \leq j \land j \leq M)$
112		elfz2	$⊢ j \in (L \dots M) \leftrightarrow ((L \in ℤ \land M \in ℤ \land j \in ℤ) \land (L \leq j \land j \leq M))$
113	97 111 112	sylanbrc	$⊢ (φ \land j \in (L + 1 \dots M)) \to j \in (L \dots M)$
114	113 72	syldan	$⊢ (φ \land j \in (L + 1 \dots M)) \to B (j) \in ℝ$
115	114	adantlr	$⊢ ((φ \land L < M) \land j \in (L + 1 \dots M)) \to B (j) \in ℝ$
116	57 115 36	seqcl	$⊢ (φ \land L < M) \to seq (L + 1) (\times B) (M) \in ℝ$
117	92 116	remulcld	$⊢ (φ \land L < M) \to seq L (\times B) (L) seq (L + 1) (\times B) (M) \in ℝ$
118	9	rpred	$⊢ φ \to E \in ℝ$
119	118	adantr	$⊢ (φ \land L < M) \to E \in ℝ$
120		1red	$⊢ (φ \land L < M) \to 1 \in ℝ$
121		nfcv	$⊢ \underline{Ⅎ} i 0$
122		nfcv	$⊢ \underline{Ⅎ} i \leq$
123	121 122 81	nfbr	$⊢ Ⅎ i 0 \leq B (L)$
124	79 123	nfim	$⊢ Ⅎ i ((φ \land L \in (L \dots M)) \to 0 \leq B (L))$
125	86	breq2d	$⊢ i = L \to (0 \leq B (i) \leftrightarrow 0 \leq B (L))$
126	85 125	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)))$
127	124 126 7	vtoclg1f	$⊢ L \in (L \dots M) \to ((φ \land L \in (L \dots M)) \to 0 \leq B (L))$
128	76 77 127	sylc	$⊢ φ \to 0 \leq B (L)$
129	128 16	breqtrrd	$⊢ φ \to 0 \leq seq L (\times B) (L)$
130	129	adantr	$⊢ (φ \land L < M) \to 0 \leq seq L (\times B) (L)$
131		nfv	$⊢ Ⅎ i L < M$
132	2 131	nfan	$⊢ Ⅎ i (φ \land L < M)$
133		eqid	$⊢ seq (L + 1) (\times B) = seq (L + 1) (\times B)$
134	4	peano2zd	$⊢ φ \to L + 1 \in ℤ$
135	134	adantr	$⊢ (φ \land L < M) \to L + 1 \in ℤ$
136	23	adantr	$⊢ (φ \land L < M) \to L \in ℝ$
137	136 45	gtned	$⊢ (φ \land L < M) \to M \neq L$
138	137	neneqd	$⊢ (φ \land L < M) \to \neg M = L$
139	5	adantr	$⊢ (φ \land L < M) \to M \in ℤ_{\geq L}$
140	139 53	syl	$⊢ (φ \land L < M) \to (M = L \lor M \in ℤ_{\geq (L + 1)})$
141		orel1	$⊢ \neg M = L \to ((M = L \lor M \in ℤ_{\geq (L + 1)}) \to M \in ℤ_{\geq (L + 1)})$
142	138 140 141	sylc	$⊢ (φ \land L < M) \to M \in ℤ_{\geq (L + 1)}$
143	25	adantr	$⊢ (φ \land L < M) \to M \in ℤ$
144	135 143 143	3jca	$⊢ (φ \land L < M) \to (L + 1 \in ℤ \land M \in ℤ \land M \in ℤ)$
145		zltp1le	$⊢ (L \in ℤ \land M \in ℤ) \to (L < M \leftrightarrow L + 1 \leq M)$
146	58 143 145	syl2anc	$⊢ (φ \land L < M) \to (L < M \leftrightarrow L + 1 \leq M)$
147	45 146	mpbid	$⊢ (φ \land L < M) \to L + 1 \leq M$
148	26	adantr	$⊢ (φ \land L < M) \to M \in ℝ$
149	148	leidd	$⊢ (φ \land L < M) \to M \leq M$
150	147 149	jca	$⊢ (φ \land L < M) \to (L + 1 \leq M \land M \leq M)$
151		elfz2	$⊢ M \in (L + 1 \dots M) \leftrightarrow ((L + 1 \in ℤ \land M \in ℤ \land M \in ℤ) \land (L + 1 \leq M \land M \leq M))$
152	144 150 151	sylanbrc	$⊢ (φ \land L < M) \to M \in (L + 1 \dots M)$
153	4	adantr	$⊢ (φ \land i \in (L + 1 \dots M)) \to L \in ℤ$
154	25	adantr	$⊢ (φ \land i \in (L + 1 \dots M)) \to M \in ℤ$
155		elfzelz	$⊢ i \in (L + 1 \dots M) \to i \in ℤ$
156	155	adantl	$⊢ (φ \land i \in (L + 1 \dots M)) \to i \in ℤ$
157	153 154 156	3jca	$⊢ (φ \land i \in (L + 1 \dots M)) \to (L \in ℤ \land M \in ℤ \land i \in ℤ)$
158	23	adantr	$⊢ (φ \land i \in (L + 1 \dots M)) \to L \in ℝ$
159	158 99	syl	$⊢ (φ \land i \in (L + 1 \dots M)) \to L + 1 \in ℝ$
160	155	zred	$⊢ i \in (L + 1 \dots M) \to i \in ℝ$
161	160	adantl	$⊢ (φ \land i \in (L + 1 \dots M)) \to i \in ℝ$
162	104	adantr	$⊢ (φ \land i \in (L + 1 \dots M)) \to L \leq L + 1$
163		elfzle1	$⊢ i \in (L + 1 \dots M) \to L + 1 \leq i$
164	163	adantl	$⊢ (φ \land i \in (L + 1 \dots M)) \to L + 1 \leq i$
165	158 159 161 162 164	letrd	$⊢ (φ \land i \in (L + 1 \dots M)) \to L \leq i$
166		elfzle2	$⊢ i \in (L + 1 \dots M) \to i \leq M$
167	166	adantl	$⊢ (φ \land i \in (L + 1 \dots M)) \to i \leq M$
168	165 167	jca	$⊢ (φ \land i \in (L + 1 \dots M)) \to (L \leq i \land i \leq M)$
169		elfz2	$⊢ i \in (L \dots M) \leftrightarrow ((L \in ℤ \land M \in ℤ \land i \in ℤ) \land (L \leq i \land i \leq M))$
170	157 168 169	sylanbrc	$⊢ (φ \land i \in (L + 1 \dots M)) \to i \in (L \dots M)$
171	170 6	syldan	$⊢ (φ \land i \in (L + 1 \dots M)) \to B (i) \in ℝ$
172	171	adantlr	$⊢ ((φ \land L < M) \land i \in (L + 1 \dots M)) \to B (i) \in ℝ$
173		simpll	$⊢ ((φ \land L < M) \land i \in (L + 1 \dots M)) \to φ$
174	4	ad2antrr	$⊢ ((φ \land L < M) \land i \in (L + 1 \dots M)) \to L \in ℤ$
175	25	ad2antrr	$⊢ ((φ \land L < M) \land i \in (L + 1 \dots M)) \to M \in ℤ$
176	155	adantl	$⊢ ((φ \land L < M) \land i \in (L + 1 \dots M)) \to i \in ℤ$
177	174 175 176	3jca	$⊢ ((φ \land L < M) \land i \in (L + 1 \dots M)) \to (L \in ℤ \land M \in ℤ \land i \in ℤ)$
178	23	ad2antrr	$⊢ ((φ \land L < M) \land i \in (L + 1 \dots M)) \to L \in ℝ$
179	100	ad2antrr	$⊢ ((φ \land L < M) \land i \in (L + 1 \dots M)) \to L + 1 \in ℝ$
180	160	adantl	$⊢ ((φ \land L < M) \land i \in (L + 1 \dots M)) \to i \in ℝ$
181	104	ad2antrr	$⊢ ((φ \land L < M) \land i \in (L + 1 \dots M)) \to L \leq L + 1$
182	163	adantl	$⊢ ((φ \land L < M) \land i \in (L + 1 \dots M)) \to L + 1 \leq i$
183	178 179 180 181 182	letrd	$⊢ ((φ \land L < M) \land i \in (L + 1 \dots M)) \to L \leq i$
184	166	adantl	$⊢ ((φ \land L < M) \land i \in (L + 1 \dots M)) \to i \leq M$
185	183 184	jca	$⊢ ((φ \land L < M) \land i \in (L + 1 \dots M)) \to (L \leq i \land i \leq M)$
186	177 185 169	sylanbrc	$⊢ ((φ \land L < M) \land i \in (L + 1 \dots M)) \to i \in (L \dots M)$
187	173 186 7	syl2anc	$⊢ ((φ \land L < M) \land i \in (L + 1 \dots M)) \to 0 \leq B (i)$
188	173 186 8	syl2anc	$⊢ ((φ \land L < M) \land i \in (L + 1 \dots M)) \to B (i) \leq 1$
189	1 132 133 135 142 152 172 187 188	fmul01	$⊢ (φ \land L < M) \to (0 \leq seq (L + 1) (\times B) (M) \land seq (L + 1) (\times B) (M) \leq 1)$
190	189	simprd	$⊢ (φ \land L < M) \to seq (L + 1) (\times B) (M) \leq 1$
191	116 120 92 130 190	lemul2ad	$⊢ (φ \land L < M) \to seq L (\times B) (L) seq (L + 1) (\times B) (M) \leq seq L (\times B) (L) \cdot 1$
192	91	recnd	$⊢ φ \to seq L (\times B) (L) \in ℂ$
193	192	mulid1d	$⊢ φ \to seq L (\times B) (L) \cdot 1 = seq L (\times B) (L)$
194	193	adantr	$⊢ (φ \land L < M) \to seq L (\times B) (L) \cdot 1 = seq L (\times B) (L)$
195	191 194	breqtrd	$⊢ (φ \land L < M) \to seq L (\times B) (L) seq (L + 1) (\times B) (M) \leq seq L (\times B) (L)$
196	16 10	eqbrtrd	$⊢ φ \to seq L (\times B) (L) < E$
197	196	adantr	$⊢ (φ \land L < M) \to seq L (\times B) (L) < E$
198	117 92 119 195 197	lelttrd	$⊢ (φ \land L < M) \to seq L (\times B) (L) seq (L + 1) (\times B) (M) < E$
199	74 198	eqbrtrd	$⊢ (φ \land L < M) \to seq L (\times B) (M) < E$
200	34 199	eqbrtrid	$⊢ (φ \land L < M) \to A (M) < E$
201	33 200	syldan	$⊢ (φ \land \neg M = L) \to A (M) < E$
202	20 201	pm2.61dan	$⊢ φ \to A (M) < E$

Metamath Proof Explorer

Theorem fmul01lt1lem1

Proof