Theorem fprodge0

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

	Ref	Expression
Hypotheses	fprodge0.kph	⊢ Ⅎ 𝑘 𝜑
	fprodge0.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	fprodge0.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
	fprodge0.0leb	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 0 ≤ 𝐵 )
Assertion	fprodge0	⊢ ( 𝜑 → 0 ≤ ∏ 𝑘 ∈ 𝐴 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		fprodge0.kph	⊢ Ⅎ 𝑘 𝜑
2		fprodge0.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
3		fprodge0.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
4		fprodge0.0leb	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 0 ≤ 𝐵 )
5		0xr	⊢ 0 ∈ ℝ*
6		pnfxr	⊢ +∞ ∈ ℝ*
7		rge0ssre	⊢ ( 0 [,) +∞ ) ⊆ ℝ
8		ax-resscn	⊢ ℝ ⊆ ℂ
9	7 8	sstri	⊢ ( 0 [,) +∞ ) ⊆ ℂ
10	9	a1i	⊢ ( 𝜑 → ( 0 [,) +∞ ) ⊆ ℂ )
11		ge0mulcl	⊢ ( ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) → ( 𝑥 · 𝑦 ) ∈ ( 0 [,) +∞ ) )
12	11	adantl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) ) → ( 𝑥 · 𝑦 ) ∈ ( 0 [,) +∞ ) )
13		elrege0	⊢ ( 𝐵 ∈ ( 0 [,) +∞ ) ↔ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) )
14	3 4 13	sylanbrc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,) +∞ ) )
15		1re	⊢ 1 ∈ ℝ
16		0le1	⊢ 0 ≤ 1
17		ltpnf	⊢ ( 1 ∈ ℝ → 1 < +∞ )
18	15 17	ax-mp	⊢ 1 < +∞
19		0re	⊢ 0 ∈ ℝ
20		elico2	⊢ ( ( 0 ∈ ℝ ∧ +∞ ∈ ℝ* ) → ( 1 ∈ ( 0 [,) +∞ ) ↔ ( 1 ∈ ℝ ∧ 0 ≤ 1 ∧ 1 < +∞ ) ) )
21	19 6 20	mp2an	⊢ ( 1 ∈ ( 0 [,) +∞ ) ↔ ( 1 ∈ ℝ ∧ 0 ≤ 1 ∧ 1 < +∞ ) )
22	15 16 18 21	mpbir3an	⊢ 1 ∈ ( 0 [,) +∞ )
23	22	a1i	⊢ ( 𝜑 → 1 ∈ ( 0 [,) +∞ ) )
24	1 10 12 2 14 23	fprodcllemf	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,) +∞ ) )
25		icogelb	⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ ∏ 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,) +∞ ) ) → 0 ≤ ∏ 𝑘 ∈ 𝐴 𝐵 )
26	5 6 24 25	mp3an12i	⊢ ( 𝜑 → 0 ≤ ∏ 𝑘 ∈ 𝐴 𝐵 )