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 φ
fprodge0.a ⊢ φ → A ∈ Fin
fprodge0.b ⊢ φ ∧ k ∈ A → B ∈ ℝ
fprodge0.0leb ⊢ φ ∧ k ∈ A → 0 ≤ B
Assertion fprodge0 ⊢ φ → 0 ≤ ∏ k ∈ A B

Proof

Step Hyp Ref Expression
1 fprodge0.kph ⊢ Ⅎ k φ
2 fprodge0.a ⊢ φ → A ∈ Fin
3 fprodge0.b ⊢ φ ∧ k ∈ A → B ∈ ℝ
4 fprodge0.0leb ⊢ φ ∧ k ∈ A → 0 ≤ B
5 0xr ⊢ 0 ∈ ℝ *
6 pnfxr ⊢ +∞ ∈ ℝ *
7 rge0ssre ⊢ 0 +∞ ⊆ ℝ
8 ax-resscn ⊢ ℝ ⊆ ℂ
9 7 8 sstri ⊢ 0 +∞ ⊆ ℂ
10 9 a1i ⊢ φ → 0 +∞ ⊆ ℂ
11 ge0mulcl ⊢ x ∈ 0 +∞ ∧ y ∈ 0 +∞ → x ⁢ y ∈ 0 +∞
12 11 adantl ⊢ φ ∧ x ∈ 0 +∞ ∧ y ∈ 0 +∞ → x ⁢ y ∈ 0 +∞
13 elrege0 ⊢ B ∈ 0 +∞ ↔ B ∈ ℝ ∧ 0 ≤ B
14 3 4 13 sylanbrc ⊢ φ ∧ k ∈ A → B ∈ 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 ⊢ φ → ∏ k ∈ A B ∈ 0 +∞
25 icogelb ⊢ 0 ∈ ℝ * ∧ +∞ ∈ ℝ * ∧ ∏ k ∈ A B ∈ 0 +∞ → 0 ≤ ∏ k ∈ A B
26 5 6 24 25 mp3an12i ⊢ φ → 0 ≤ ∏ k ∈ A B