fmul01

Description: Multiplying a finite number of values in [ 0 , 1 ] , gives the final product itself a number in [ 0 , 1 ]. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	fmul01.1	$⊢ \underline{Ⅎ} i B$
	fmul01.2	$⊢ Ⅎ i φ$
	fmul01.3	$⊢ A = seq L (\times B)$
	fmul01.4	$⊢ φ \to L \in ℤ$
	fmul01.5	$⊢ φ \to M \in ℤ_{\geq L}$
	fmul01.6	$⊢ φ \to K \in (L \dots M)$
	fmul01.7	$⊢ (φ \land i \in (L \dots M)) \to B (i) \in ℝ$
	fmul01.8	$⊢ (φ \land i \in (L \dots M)) \to 0 \leq B (i)$
	fmul01.9	$⊢ (φ \land i \in (L \dots M)) \to B (i) \leq 1$
Assertion	fmul01	$⊢ φ \to (0 \leq A (K) \land A (K) \leq 1)$

Proof

Step	Hyp	Ref	Expression
1		fmul01.1	$⊢ \underline{Ⅎ} i B$
2		fmul01.2	$⊢ Ⅎ i φ$
3		fmul01.3	$⊢ A = seq L (\times B)$
4		fmul01.4	$⊢ φ \to L \in ℤ$
5		fmul01.5	$⊢ φ \to M \in ℤ_{\geq L}$
6		fmul01.6	$⊢ φ \to K \in (L \dots M)$
7		fmul01.7	$⊢ (φ \land i \in (L \dots M)) \to B (i) \in ℝ$
8		fmul01.8	$⊢ (φ \land i \in (L \dots M)) \to 0 \leq B (i)$
9		fmul01.9	$⊢ (φ \land i \in (L \dots M)) \to B (i) \leq 1$
10		fveq2	$⊢ k = L \to A (k) = A (L)$
11	10	breq2d	$⊢ k = L \to (0 \leq A (k) \leftrightarrow 0 \leq A (L))$
12	10	breq1d	$⊢ k = L \to (A (k) \leq 1 \leftrightarrow A (L) \leq 1)$
13	11 12	anbi12d	$⊢ k = L \to ((0 \leq A (k) \land A (k) \leq 1) \leftrightarrow (0 \leq A (L) \land A (L) \leq 1))$
14	13	imbi2d	$⊢ k = L \to ((φ \to (0 \leq A (k) \land A (k) \leq 1)) \leftrightarrow (φ \to (0 \leq A (L) \land A (L) \leq 1)))$
15		fveq2	$⊢ k = j \to A (k) = A (j)$
16	15	breq2d	$⊢ k = j \to (0 \leq A (k) \leftrightarrow 0 \leq A (j))$
17	15	breq1d	$⊢ k = j \to (A (k) \leq 1 \leftrightarrow A (j) \leq 1)$
18	16 17	anbi12d	$⊢ k = j \to ((0 \leq A (k) \land A (k) \leq 1) \leftrightarrow (0 \leq A (j) \land A (j) \leq 1))$
19	18	imbi2d	$⊢ k = j \to ((φ \to (0 \leq A (k) \land A (k) \leq 1)) \leftrightarrow (φ \to (0 \leq A (j) \land A (j) \leq 1)))$
20		fveq2	$⊢ k = j + 1 \to A (k) = A (j + 1)$
21	20	breq2d	$⊢ k = j + 1 \to (0 \leq A (k) \leftrightarrow 0 \leq A (j + 1))$
22	20	breq1d	$⊢ k = j + 1 \to (A (k) \leq 1 \leftrightarrow A (j + 1) \leq 1)$
23	21 22	anbi12d	$⊢ k = j + 1 \to ((0 \leq A (k) \land A (k) \leq 1) \leftrightarrow (0 \leq A (j + 1) \land A (j + 1) \leq 1))$
24	23	imbi2d	$⊢ k = j + 1 \to ((φ \to (0 \leq A (k) \land A (k) \leq 1)) \leftrightarrow (φ \to (0 \leq A (j + 1) \land A (j + 1) \leq 1)))$
25		fveq2	$⊢ k = K \to A (k) = A (K)$
26	25	breq2d	$⊢ k = K \to (0 \leq A (k) \leftrightarrow 0 \leq A (K))$
27	25	breq1d	$⊢ k = K \to (A (k) \leq 1 \leftrightarrow A (K) \leq 1)$
28	26 27	anbi12d	$⊢ k = K \to ((0 \leq A (k) \land A (k) \leq 1) \leftrightarrow (0 \leq A (K) \land A (K) \leq 1))$
29	28	imbi2d	$⊢ k = K \to ((φ \to (0 \leq A (k) \land A (k) \leq 1)) \leftrightarrow (φ \to (0 \leq A (K) \land A (K) \leq 1)))$
30	4	zred	$⊢ φ \to L \in ℝ$
31	30	leidd	$⊢ φ \to L \leq L$
32		eluzelz	$⊢ M \in ℤ_{\geq L} \to M \in ℤ$
33	5 32	syl	$⊢ φ \to M \in ℤ$
34		eluz	$⊢ (L \in ℤ \land M \in ℤ) \to (M \in ℤ_{\geq L} \leftrightarrow L \leq M)$
35	4 33 34	syl2anc	$⊢ φ \to (M \in ℤ_{\geq L} \leftrightarrow L \leq M)$
36	5 35	mpbid	$⊢ φ \to L \leq M$
37		elfz	$⊢ (L \in ℤ \land L \in ℤ \land M \in ℤ) \to (L \in (L \dots M) \leftrightarrow (L \leq L \land L \leq M))$
38	4 4 33 37	syl3anc	$⊢ φ \to (L \in (L \dots M) \leftrightarrow (L \leq L \land L \leq M))$
39	31 36 38	mpbir2and	$⊢ φ \to L \in (L \dots M)$
40	39	ancli	$⊢ φ \to (φ \land L \in (L \dots M))$
41		nfv	$⊢ Ⅎ i L \in (L \dots M)$
42	2 41	nfan	$⊢ Ⅎ i (φ \land L \in (L \dots M))$
43		nfcv	$⊢ \underline{Ⅎ} i 0$
44		nfcv	$⊢ \underline{Ⅎ} i \leq$
45		nfcv	$⊢ \underline{Ⅎ} i L$
46	1 45	nffv	$⊢ \underline{Ⅎ} i B (L)$
47	43 44 46	nfbr	$⊢ Ⅎ i 0 \leq B (L)$
48	42 47	nfim	$⊢ Ⅎ i ((φ \land L \in (L \dots M)) \to 0 \leq B (L))$
49		eleq1	$⊢ i = L \to (i \in (L \dots M) \leftrightarrow L \in (L \dots M))$
50	49	anbi2d	$⊢ i = L \to ((φ \land i \in (L \dots M)) \leftrightarrow (φ \land L \in (L \dots M)))$
51		fveq2	$⊢ i = L \to B (i) = B (L)$
52	51	breq2d	$⊢ i = L \to (0 \leq B (i) \leftrightarrow 0 \leq B (L))$
53	50 52	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)))$
54	48 53 8	vtoclg1f	$⊢ L \in (L \dots M) \to ((φ \land L \in (L \dots M)) \to 0 \leq B (L))$
55	39 40 54	sylc	$⊢ φ \to 0 \leq B (L)$
56	3	fveq1i	$⊢ A (L) = seq L (\times B) (L)$
57		seq1	$⊢ L \in ℤ \to seq L (\times B) (L) = B (L)$
58	4 57	syl	$⊢ φ \to seq L (\times B) (L) = B (L)$
59	56 58	syl5eq	$⊢ φ \to A (L) = B (L)$
60	55 59	breqtrrd	$⊢ φ \to 0 \leq A (L)$
61		nfcv	$⊢ \underline{Ⅎ} i 1$
62	46 44 61	nfbr	$⊢ Ⅎ i B (L) \leq 1$
63	42 62	nfim	$⊢ Ⅎ i ((φ \land L \in (L \dots M)) \to B (L) \leq 1)$
64	51	breq1d	$⊢ i = L \to (B (i) \leq 1 \leftrightarrow B (L) \leq 1)$
65	50 64	imbi12d	$⊢ i = L \to (((φ \land i \in (L \dots M)) \to B (i) \leq 1) \leftrightarrow ((φ \land L \in (L \dots M)) \to B (L) \leq 1))$
66	63 65 9	vtoclg1f	$⊢ L \in (L \dots M) \to ((φ \land L \in (L \dots M)) \to B (L) \leq 1)$
67	39 40 66	sylc	$⊢ φ \to B (L) \leq 1$
68	59 67	eqbrtrd	$⊢ φ \to A (L) \leq 1$
69	60 68	jca	$⊢ φ \to (0 \leq A (L) \land A (L) \leq 1)$
70	69	a1i	$⊢ M \in ℤ_{\geq L} \to (φ \to (0 \leq A (L) \land A (L) \leq 1))$
71		elfzouz	$⊢ j \in (L ..^M) \to j \in ℤ_{\geq L}$
72	71	3ad2ant1	$⊢ (j \in (L ..^M) \land (φ \to (0 \leq A (j) \land A (j) \leq 1)) \land φ) \to j \in ℤ_{\geq L}$
73		simpl3	$⊢ ((j \in (L ..^M) \land (φ \to (0 \leq A (j) \land A (j) \leq 1)) \land φ) \land k \in (L \dots j)) \to φ$
74		elfzouz2	$⊢ j \in (L ..^M) \to M \in ℤ_{\geq j}$
75		fzss2	$⊢ M \in ℤ_{\geq j} \to (L \dots j) \subseteq (L \dots M)$
76	74 75	syl	$⊢ j \in (L ..^M) \to (L \dots j) \subseteq (L \dots M)$
77	76	3ad2ant1	$⊢ (j \in (L ..^M) \land (φ \to (0 \leq A (j) \land A (j) \leq 1)) \land φ) \to (L \dots j) \subseteq (L \dots M)$
78	77	sselda	$⊢ ((j \in (L ..^M) \land (φ \to (0 \leq A (j) \land A (j) \leq 1)) \land φ) \land k \in (L \dots j)) \to k \in (L \dots M)$
79		nfv	$⊢ Ⅎ i k \in (L \dots M)$
80	2 79	nfan	$⊢ Ⅎ i (φ \land k \in (L \dots M))$
81		nfcv	$⊢ \underline{Ⅎ} i k$
82	1 81	nffv	$⊢ \underline{Ⅎ} i B (k)$
83	82	nfel1	$⊢ Ⅎ i B (k) \in ℝ$
84	80 83	nfim	$⊢ Ⅎ i ((φ \land k \in (L \dots M)) \to B (k) \in ℝ)$
85		eleq1	$⊢ i = k \to (i \in (L \dots M) \leftrightarrow k \in (L \dots M))$
86	85	anbi2d	$⊢ i = k \to ((φ \land i \in (L \dots M)) \leftrightarrow (φ \land k \in (L \dots M)))$
87		fveq2	$⊢ i = k \to B (i) = B (k)$
88	87	eleq1d	$⊢ i = k \to (B (i) \in ℝ \leftrightarrow B (k) \in ℝ)$
89	86 88	imbi12d	$⊢ i = k \to (((φ \land i \in (L \dots M)) \to B (i) \in ℝ) \leftrightarrow ((φ \land k \in (L \dots M)) \to B (k) \in ℝ))$
90	84 89 7	chvarfv	$⊢ (φ \land k \in (L \dots M)) \to B (k) \in ℝ$
91	73 78 90	syl2anc	$⊢ ((j \in (L ..^M) \land (φ \to (0 \leq A (j) \land A (j) \leq 1)) \land φ) \land k \in (L \dots j)) \to B (k) \in ℝ$
92		remulcl	$⊢ (k \in ℝ \land l \in ℝ) \to k l \in ℝ$
93	92	adantl	$⊢ ((j \in (L ..^M) \land (φ \to (0 \leq A (j) \land A (j) \leq 1)) \land φ) \land (k \in ℝ \land l \in ℝ)) \to k l \in ℝ$
94	72 91 93	seqcl	$⊢ (j \in (L ..^M) \land (φ \to (0 \leq A (j) \land A (j) \leq 1)) \land φ) \to seq L (\times B) (j) \in ℝ$
95		simp3	$⊢ (j \in (L ..^M) \land (φ \to (0 \leq A (j) \land A (j) \leq 1)) \land φ) \to φ$
96		fzofzp1	$⊢ j \in (L ..^M) \to j + 1 \in (L \dots M)$
97	96	3ad2ant1	$⊢ (j \in (L ..^M) \land (φ \to (0 \leq A (j) \land A (j) \leq 1)) \land φ) \to j + 1 \in (L \dots M)$
98		nfv	$⊢ Ⅎ i j + 1 \in (L \dots M)$
99	2 98	nfan	$⊢ Ⅎ i (φ \land j + 1 \in (L \dots M))$
100		nfcv	$⊢ \underline{Ⅎ} i (j + 1)$
101	1 100	nffv	$⊢ \underline{Ⅎ} i B (j + 1)$
102	101	nfel1	$⊢ Ⅎ i B (j + 1) \in ℝ$
103	99 102	nfim	$⊢ Ⅎ i ((φ \land j + 1 \in (L \dots M)) \to B (j + 1) \in ℝ)$
104		eleq1	$⊢ i = j + 1 \to (i \in (L \dots M) \leftrightarrow j + 1 \in (L \dots M))$
105	104	anbi2d	$⊢ i = j + 1 \to ((φ \land i \in (L \dots M)) \leftrightarrow (φ \land j + 1 \in (L \dots M)))$
106		fveq2	$⊢ i = j + 1 \to B (i) = B (j + 1)$
107	106	eleq1d	$⊢ i = j + 1 \to (B (i) \in ℝ \leftrightarrow B (j + 1) \in ℝ)$
108	105 107	imbi12d	$⊢ i = j + 1 \to (((φ \land i \in (L \dots M)) \to B (i) \in ℝ) \leftrightarrow ((φ \land j + 1 \in (L \dots M)) \to B (j + 1) \in ℝ))$
109	103 108 7	vtoclg1f	$⊢ j + 1 \in (L \dots M) \to ((φ \land j + 1 \in (L \dots M)) \to B (j + 1) \in ℝ)$
110	109	anabsi7	$⊢ (φ \land j + 1 \in (L \dots M)) \to B (j + 1) \in ℝ$
111	95 97 110	syl2anc	$⊢ (j \in (L ..^M) \land (φ \to (0 \leq A (j) \land A (j) \leq 1)) \land φ) \to B (j + 1) \in ℝ$
112		pm3.35	$⊢ (φ \land (φ \to (0 \leq A (j) \land A (j) \leq 1))) \to (0 \leq A (j) \land A (j) \leq 1)$
113	112	ancoms	$⊢ ((φ \to (0 \leq A (j) \land A (j) \leq 1)) \land φ) \to (0 \leq A (j) \land A (j) \leq 1)$
114		simpl	$⊢ (0 \leq A (j) \land A (j) \leq 1) \to 0 \leq A (j)$
115	113 114	syl	$⊢ ((φ \to (0 \leq A (j) \land A (j) \leq 1)) \land φ) \to 0 \leq A (j)$
116	115	3adant1	$⊢ (j \in (L ..^M) \land (φ \to (0 \leq A (j) \land A (j) \leq 1)) \land φ) \to 0 \leq A (j)$
117	3	fveq1i	$⊢ A (j) = seq L (\times B) (j)$
118	116 117	breqtrdi	$⊢ (j \in (L ..^M) \land (φ \to (0 \leq A (j) \land A (j) \leq 1)) \land φ) \to 0 \leq seq L (\times B) (j)$
119		simp1	$⊢ (j \in (L ..^M) \land (φ \to (0 \leq A (j) \land A (j) \leq 1)) \land φ) \to j \in (L ..^M)$
120	96	adantl	$⊢ (φ \land j \in (L ..^M)) \to j + 1 \in (L \dots M)$
121		simpl	$⊢ (φ \land j \in (L ..^M)) \to φ$
122	121 120	jca	$⊢ (φ \land j \in (L ..^M)) \to (φ \land j + 1 \in (L \dots M))$
123	43 44 101	nfbr	$⊢ Ⅎ i 0 \leq B (j + 1)$
124	99 123	nfim	$⊢ Ⅎ i ((φ \land j + 1 \in (L \dots M)) \to 0 \leq B (j + 1))$
125	106	breq2d	$⊢ i = j + 1 \to (0 \leq B (i) \leftrightarrow 0 \leq B (j + 1))$
126	105 125	imbi12d	$⊢ i = j + 1 \to (((φ \land i \in (L \dots M)) \to 0 \leq B (i)) \leftrightarrow ((φ \land j + 1 \in (L \dots M)) \to 0 \leq B (j + 1)))$
127	124 126 8	vtoclg1f	$⊢ j + 1 \in (L \dots M) \to ((φ \land j + 1 \in (L \dots M)) \to 0 \leq B (j + 1))$
128	120 122 127	sylc	$⊢ (φ \land j \in (L ..^M)) \to 0 \leq B (j + 1)$
129	95 119 128	syl2anc	$⊢ (j \in (L ..^M) \land (φ \to (0 \leq A (j) \land A (j) \leq 1)) \land φ) \to 0 \leq B (j + 1)$
130	94 111 118 129	mulge0d	$⊢ (j \in (L ..^M) \land (φ \to (0 \leq A (j) \land A (j) \leq 1)) \land φ) \to 0 \leq seq L (\times B) (j) B (j + 1)$
131		seqp1	$⊢ j \in ℤ_{\geq L} \to seq L (\times B) (j + 1) = seq L (\times B) (j) B (j + 1)$
132	72 131	syl	$⊢ (j \in (L ..^M) \land (φ \to (0 \leq A (j) \land A (j) \leq 1)) \land φ) \to seq L (\times B) (j + 1) = seq L (\times B) (j) B (j + 1)$
133	130 132	breqtrrd	$⊢ (j \in (L ..^M) \land (φ \to (0 \leq A (j) \land A (j) \leq 1)) \land φ) \to 0 \leq seq L (\times B) (j + 1)$
134	3	fveq1i	$⊢ A (j + 1) = seq L (\times B) (j + 1)$
135	133 134	breqtrrdi	$⊢ (j \in (L ..^M) \land (φ \to (0 \leq A (j) \land A (j) \leq 1)) \land φ) \to 0 \leq A (j + 1)$
136	94 111	remulcld	$⊢ (j \in (L ..^M) \land (φ \to (0 \leq A (j) \land A (j) \leq 1)) \land φ) \to seq L (\times B) (j) B (j + 1) \in ℝ$
137		1red	$⊢ (j \in (L ..^M) \land (φ \to (0 \leq A (j) \land A (j) \leq 1)) \land φ) \to 1 \in ℝ$
138	95 97	jca	$⊢ (j \in (L ..^M) \land (φ \to (0 \leq A (j) \land A (j) \leq 1)) \land φ) \to (φ \land j + 1 \in (L \dots M))$
139	101 44 61	nfbr	$⊢ Ⅎ i B (j + 1) \leq 1$
140	99 139	nfim	$⊢ Ⅎ i ((φ \land j + 1 \in (L \dots M)) \to B (j + 1) \leq 1)$
141	106	breq1d	$⊢ i = j + 1 \to (B (i) \leq 1 \leftrightarrow B (j + 1) \leq 1)$
142	105 141	imbi12d	$⊢ i = j + 1 \to (((φ \land i \in (L \dots M)) \to B (i) \leq 1) \leftrightarrow ((φ \land j + 1 \in (L \dots M)) \to B (j + 1) \leq 1))$
143	140 142 9	vtoclg1f	$⊢ j + 1 \in (L \dots M) \to ((φ \land j + 1 \in (L \dots M)) \to B (j + 1) \leq 1)$
144	97 138 143	sylc	$⊢ (j \in (L ..^M) \land (φ \to (0 \leq A (j) \land A (j) \leq 1)) \land φ) \to B (j + 1) \leq 1$
145	111 137 94 118 144	lemul2ad	$⊢ (j \in (L ..^M) \land (φ \to (0 \leq A (j) \land A (j) \leq 1)) \land φ) \to seq L (\times B) (j) B (j + 1) \leq seq L (\times B) (j) \cdot 1$
146	94	recnd	$⊢ (j \in (L ..^M) \land (φ \to (0 \leq A (j) \land A (j) \leq 1)) \land φ) \to seq L (\times B) (j) \in ℂ$
147	146	mulid1d	$⊢ (j \in (L ..^M) \land (φ \to (0 \leq A (j) \land A (j) \leq 1)) \land φ) \to seq L (\times B) (j) \cdot 1 = seq L (\times B) (j)$
148	145 147	breqtrd	$⊢ (j \in (L ..^M) \land (φ \to (0 \leq A (j) \land A (j) \leq 1)) \land φ) \to seq L (\times B) (j) B (j + 1) \leq seq L (\times B) (j)$
149		simp2	$⊢ (j \in (L ..^M) \land (φ \to (0 \leq A (j) \land A (j) \leq 1)) \land φ) \to (φ \to (0 \leq A (j) \land A (j) \leq 1))$
150	112	simprd	$⊢ (φ \land (φ \to (0 \leq A (j) \land A (j) \leq 1))) \to A (j) \leq 1$
151	95 149 150	syl2anc	$⊢ (j \in (L ..^M) \land (φ \to (0 \leq A (j) \land A (j) \leq 1)) \land φ) \to A (j) \leq 1$
152	117 151	eqbrtrrid	$⊢ (j \in (L ..^M) \land (φ \to (0 \leq A (j) \land A (j) \leq 1)) \land φ) \to seq L (\times B) (j) \leq 1$
153	136 94 137 148 152	letrd	$⊢ (j \in (L ..^M) \land (φ \to (0 \leq A (j) \land A (j) \leq 1)) \land φ) \to seq L (\times B) (j) B (j + 1) \leq 1$
154	132 153	eqbrtrd	$⊢ (j \in (L ..^M) \land (φ \to (0 \leq A (j) \land A (j) \leq 1)) \land φ) \to seq L (\times B) (j + 1) \leq 1$
155	134 154	eqbrtrid	$⊢ (j \in (L ..^M) \land (φ \to (0 \leq A (j) \land A (j) \leq 1)) \land φ) \to A (j + 1) \leq 1$
156	135 155	jca	$⊢ (j \in (L ..^M) \land (φ \to (0 \leq A (j) \land A (j) \leq 1)) \land φ) \to (0 \leq A (j + 1) \land A (j + 1) \leq 1)$
157	156	3exp	$⊢ j \in (L ..^M) \to ((φ \to (0 \leq A (j) \land A (j) \leq 1)) \to (φ \to (0 \leq A (j + 1) \land A (j + 1) \leq 1)))$
158	14 19 24 29 70 157	fzind2	$⊢ K \in (L \dots M) \to (φ \to (0 \leq A (K) \land A (K) \leq 1))$
159	6 158	mpcom	$⊢ φ \to (0 \leq A (K) \land A (K) \leq 1)$

Metamath Proof Explorer

Theorem fmul01

Proof