# 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 𝑘 𝜑
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 ≤ ∏ 𝑘𝐴 𝐵 )