fmul01lt1

Description: Given a finite multiplication of values betweeen 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	fmul01lt1.1	$⊢ \underline{Ⅎ} i B$
	fmul01lt1.2	$⊢ Ⅎ i φ$
	fmul01lt1.3	$⊢ \underline{Ⅎ} j A$
	fmul01lt1.4	$⊢ A = seq 1 (\times B)$
	fmul01lt1.5	$⊢ φ \to M \in ℕ$
	fmul01lt1.6	$⊢ φ \to B : (1 \dots M) ⟶ ℝ$
	fmul01lt1.7	$⊢ (φ \land i \in (1 \dots M)) \to 0 \leq B (i)$
	fmul01lt1.8	$⊢ (φ \land i \in (1 \dots M)) \to B (i) \leq 1$
	fmul01lt1.9	$⊢ φ \to E \in ℝ^{+}$
	fmul01lt1.10	$⊢ φ \to \exists j \in (1 \dots M) B (j) < E$
Assertion	fmul01lt1	$⊢ φ \to A (M) < E$

Proof

Step	Hyp	Ref	Expression
1		fmul01lt1.1	$⊢ \underline{Ⅎ} i B$
2		fmul01lt1.2	$⊢ Ⅎ i φ$
3		fmul01lt1.3	$⊢ \underline{Ⅎ} j A$
4		fmul01lt1.4	$⊢ A = seq 1 (\times B)$
5		fmul01lt1.5	$⊢ φ \to M \in ℕ$
6		fmul01lt1.6	$⊢ φ \to B : (1 \dots M) ⟶ ℝ$
7		fmul01lt1.7	$⊢ (φ \land i \in (1 \dots M)) \to 0 \leq B (i)$
8		fmul01lt1.8	$⊢ (φ \land i \in (1 \dots M)) \to B (i) \leq 1$
9		fmul01lt1.9	$⊢ φ \to E \in ℝ^{+}$
10		fmul01lt1.10	$⊢ φ \to \exists j \in (1 \dots M) B (j) < E$
11		nfv	$⊢ Ⅎ j φ$
12		nfcv	$⊢ \underline{Ⅎ} j M$
13	3 12	nffv	$⊢ \underline{Ⅎ} j A (M)$
14		nfcv	$⊢ \underline{Ⅎ} j <$
15		nfcv	$⊢ \underline{Ⅎ} j E$
16	13 14 15	nfbr	$⊢ Ⅎ j A (M) < E$
17		nfv	$⊢ Ⅎ i j \in (1 \dots M)$
18		nfcv	$⊢ \underline{Ⅎ} i j$
19	1 18	nffv	$⊢ \underline{Ⅎ} i B (j)$
20		nfcv	$⊢ \underline{Ⅎ} i <$
21		nfcv	$⊢ \underline{Ⅎ} i E$
22	19 20 21	nfbr	$⊢ Ⅎ i B (j) < E$
23	2 17 22	nf3an	$⊢ Ⅎ i (φ \land j \in (1 \dots M) \land B (j) < E)$
24		1zzd	$⊢ (φ \land j \in (1 \dots M) \land B (j) < E) \to 1 \in ℤ$
25		elnnuz	$⊢ M \in ℕ \leftrightarrow M \in ℤ_{\geq 1}$
26	5 25	sylib	$⊢ φ \to M \in ℤ_{\geq 1}$
27	26	3ad2ant1	$⊢ (φ \land j \in (1 \dots M) \land B (j) < E) \to M \in ℤ_{\geq 1}$
28	6	ffvelrnda	$⊢ (φ \land i \in (1 \dots M)) \to B (i) \in ℝ$
29	28	3ad2antl1	$⊢ ((φ \land j \in (1 \dots M) \land B (j) < E) \land i \in (1 \dots M)) \to B (i) \in ℝ$
30	7	3ad2antl1	$⊢ ((φ \land j \in (1 \dots M) \land B (j) < E) \land i \in (1 \dots M)) \to 0 \leq B (i)$
31	8	3ad2antl1	$⊢ ((φ \land j \in (1 \dots M) \land B (j) < E) \land i \in (1 \dots M)) \to B (i) \leq 1$
32	9	3ad2ant1	$⊢ (φ \land j \in (1 \dots M) \land B (j) < E) \to E \in ℝ^{+}$
33		simp2	$⊢ (φ \land j \in (1 \dots M) \land B (j) < E) \to j \in (1 \dots M)$
34		simp3	$⊢ (φ \land j \in (1 \dots M) \land B (j) < E) \to B (j) < E$
35	1 23 4 24 27 29 30 31 32 33 34	fmul01lt1lem2	$⊢ (φ \land j \in (1 \dots M) \land B (j) < E) \to A (M) < E$
36	35	3exp	$⊢ φ \to (j \in (1 \dots M) \to (B (j) < E \to A (M) < E))$
37	11 16 36	rexlimd	$⊢ φ \to (\exists j \in (1 \dots M) B (j) < E \to A (M) < E)$
38	10 37	mpd	$⊢ φ \to A (M) < E$

Metamath Proof Explorer

Theorem fmul01lt1

Proof