fprodge0

Description: If all the terms of a finite product are nonnegative, so is the product. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Step	Hyp	Ref	Expression
1		fprodge0.kph	$⊢ Ⅎ k φ$
2		fprodge0.a	$⊢ φ \to A \in Fin$
3		fprodge0.b	$⊢ (φ \land k \in A) \to B \in ℝ$
4		fprodge0.0leb	$⊢ (φ \land k \in A) \to 0 \leq B$
5		0xr	$⊢ 0 \in ℝ^{*}$
6		pnfxr	$⊢ +∞ \in ℝ^{*}$
7		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
8		ax-resscn	$⊢ ℝ \subseteq ℂ$
9	7 8	sstri	$⊢ [0, +∞) \subseteq ℂ$
10	9	a1i	$⊢ φ \to [0, +∞) \subseteq ℂ$
11		ge0mulcl	$⊢ (x \in [0, +∞) \land y \in [0, +∞)) \to x y \in [0, +∞)$
12	11	adantl	$⊢ (φ \land (x \in [0, +∞) \land y \in [0, +∞))) \to x y \in [0, +∞)$
13		elrege0	$⊢ B \in [0, +∞) \leftrightarrow (B \in ℝ \land 0 \leq B)$
14	3 4 13	sylanbrc	$⊢ (φ \land k \in A) \to B \in [0, +∞)$
15		1re	$⊢ 1 \in ℝ$
16		0le1	$⊢ 0 \leq 1$
17		ltpnf	$⊢ 1 \in ℝ \to 1 < +∞$
18	15 17	ax-mp	$⊢ 1 < +∞$
19		0re	$⊢ 0 \in ℝ$
20		elico2	$⊢ (0 \in ℝ \land +∞ \in ℝ^{*}) \to (1 \in [0, +∞) \leftrightarrow (1 \in ℝ \land 0 \leq 1 \land 1 < +∞))$
21	19 6 20	mp2an	$⊢ 1 \in [0, +∞) \leftrightarrow (1 \in ℝ \land 0 \leq 1 \land 1 < +∞)$
22	15 16 18 21	mpbir3an	$⊢ 1 \in [0, +∞)$
23	22	a1i	$⊢ φ \to 1 \in [0, +∞)$
24	1 10 12 2 14 23	fprodcllemf	$⊢ φ \to \prod_{k \in A} B \in [0, +∞)$
25		icogelb	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{} \land \prod_{k \in A} B \in [0, +∞)) \to 0 \leq \prod_{k \in A} B$
26	5 6 24 25	mp3an12i	$⊢ φ \to 0 \leq \prod_{k \in A} B$

Metamath Proof Explorer