This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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