# Metamath Proof Explorer

## 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 ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{\phi }$
fprodge0.a ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
fprodge0.b ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in ℝ$
fprodge0.0leb ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to 0\le {B}$
Assertion fprodge0 ${⊢}{\phi }\to 0\le \prod _{{k}\in {A}}{B}$

### Proof

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