fprodge1

Description: If all of the terms of a finite product are greater than or equal to 1 , so is the product. (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	fprodge1.ph	$⊢ Ⅎ k φ$
	fprodge1.a	$⊢ φ \to A \in Fin$
	fprodge1.b	$⊢ (φ \land k \in A) \to B \in ℝ$
	fprodge1.ge	$⊢ (φ \land k \in A) \to 1 \leq B$
Assertion	fprodge1	$⊢ φ \to 1 \leq \prod_{k \in A} B$

Proof

Step	Hyp	Ref	Expression
1		fprodge1.ph	$⊢ Ⅎ k φ$
2		fprodge1.a	$⊢ φ \to A \in Fin$
3		fprodge1.b	$⊢ (φ \land k \in A) \to B \in ℝ$
4		fprodge1.ge	$⊢ (φ \land k \in A) \to 1 \leq B$
5		1xr	$⊢ 1 \in ℝ^{*}$
6		pnfxr	$⊢ +∞ \in ℝ^{*}$
7		1re	$⊢ 1 \in ℝ$
8		icossre	$⊢ (1 \in ℝ \land +∞ \in ℝ^{*}) \to [1, +∞) \subseteq ℝ$
9	7 6 8	mp2an	$⊢ [1, +∞) \subseteq ℝ$
10		ax-resscn	$⊢ ℝ \subseteq ℂ$
11	9 10	sstri	$⊢ [1, +∞) \subseteq ℂ$
12	11	a1i	$⊢ φ \to [1, +∞) \subseteq ℂ$
13	5	a1i	$⊢ (x \in [1, +∞) \land y \in [1, +∞)) \to 1 \in ℝ^{*}$
14	6	a1i	$⊢ (x \in [1, +∞) \land y \in [1, +∞)) \to +∞ \in ℝ^{*}$
15	9	sseli	$⊢ x \in [1, +∞) \to x \in ℝ$
16	15	adantr	$⊢ (x \in [1, +∞) \land y \in [1, +∞)) \to x \in ℝ$
17	9	sseli	$⊢ y \in [1, +∞) \to y \in ℝ$
18	17	adantl	$⊢ (x \in [1, +∞) \land y \in [1, +∞)) \to y \in ℝ$
19	16 18	remulcld	$⊢ (x \in [1, +∞) \land y \in [1, +∞)) \to x y \in ℝ$
20	19	rexrd	$⊢ (x \in [1, +∞) \land y \in [1, +∞)) \to x y \in ℝ^{*}$
21		1t1e1	$⊢ 1 \cdot 1 = 1$
22	7	a1i	$⊢ (x \in [1, +∞) \land y \in [1, +∞)) \to 1 \in ℝ$
23		0le1	$⊢ 0 \leq 1$
24	23	a1i	$⊢ (x \in [1, +∞) \land y \in [1, +∞)) \to 0 \leq 1$
25		icogelb	$⊢ (1 \in ℝ^{} \land +∞ \in ℝ^{} \land x \in [1, +∞)) \to 1 \leq x$
26	5 6 25	mp3an12	$⊢ x \in [1, +∞) \to 1 \leq x$
27	26	adantr	$⊢ (x \in [1, +∞) \land y \in [1, +∞)) \to 1 \leq x$
28		icogelb	$⊢ (1 \in ℝ^{} \land +∞ \in ℝ^{} \land y \in [1, +∞)) \to 1 \leq y$
29	5 6 28	mp3an12	$⊢ y \in [1, +∞) \to 1 \leq y$
30	29	adantl	$⊢ (x \in [1, +∞) \land y \in [1, +∞)) \to 1 \leq y$
31	22 16 22 18 24 24 27 30	lemul12ad	$⊢ (x \in [1, +∞) \land y \in [1, +∞)) \to 1 \cdot 1 \leq x y$
32	21 31	eqbrtrrid	$⊢ (x \in [1, +∞) \land y \in [1, +∞)) \to 1 \leq x y$
33	19	ltpnfd	$⊢ (x \in [1, +∞) \land y \in [1, +∞)) \to x y < +∞$
34	13 14 20 32 33	elicod	$⊢ (x \in [1, +∞) \land y \in [1, +∞)) \to x y \in [1, +∞)$
35	34	adantl	$⊢ (φ \land (x \in [1, +∞) \land y \in [1, +∞))) \to x y \in [1, +∞)$
36	5	a1i	$⊢ (φ \land k \in A) \to 1 \in ℝ^{*}$
37	6	a1i	$⊢ (φ \land k \in A) \to +∞ \in ℝ^{*}$
38	3	rexrd	$⊢ (φ \land k \in A) \to B \in ℝ^{*}$
39	3	ltpnfd	$⊢ (φ \land k \in A) \to B < +∞$
40	36 37 38 4 39	elicod	$⊢ (φ \land k \in A) \to B \in [1, +∞)$
41		1le1	$⊢ 1 \leq 1$
42		ltpnf	$⊢ 1 \in ℝ \to 1 < +∞$
43	7 42	ax-mp	$⊢ 1 < +∞$
44		elico2	$⊢ (1 \in ℝ \land +∞ \in ℝ^{*}) \to (1 \in [1, +∞) \leftrightarrow (1 \in ℝ \land 1 \leq 1 \land 1 < +∞))$
45	7 6 44	mp2an	$⊢ 1 \in [1, +∞) \leftrightarrow (1 \in ℝ \land 1 \leq 1 \land 1 < +∞)$
46	7 41 43 45	mpbir3an	$⊢ 1 \in [1, +∞)$
47	46	a1i	$⊢ φ \to 1 \in [1, +∞)$
48	1 12 35 2 40 47	fprodcllemf	$⊢ φ \to \prod_{k \in A} B \in [1, +∞)$
49		icogelb	$⊢ (1 \in ℝ^{} \land +∞ \in ℝ^{} \land \prod_{k \in A} B \in [1, +∞)) \to 1 \leq \prod_{k \in A} B$
50	5 6 48 49	mp3an12i	$⊢ φ \to 1 \leq \prod_{k \in A} B$

Metamath Proof Explorer

Theorem fprodge1

Proof