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

Metamath Proof Explorer

Theorem fmul01

Proof