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
`|- F/ k ph`
fprodge0.a
`|- ( ph -> A e. Fin )`
fprodge0.b
`|- ( ( ph /\ k e. A ) -> B e. RR )`
fprodge0.0leb
`|- ( ( ph /\ k e. A ) -> 0 <_ B )`
Assertion fprodge0
`|- ( ph -> 0 <_ prod_ k e. A B )`

Proof

Step Hyp Ref Expression
1 fprodge0.kph
` |-  F/ k ph`
2 fprodge0.a
` |-  ( ph -> A e. Fin )`
3 fprodge0.b
` |-  ( ( ph /\ k e. A ) -> B e. RR )`
4 fprodge0.0leb
` |-  ( ( ph /\ k e. A ) -> 0 <_ B )`
5 0xr
` |-  0 e. RR*`
6 pnfxr
` |-  +oo e. RR*`
7 rge0ssre
` |-  ( 0 [,) +oo ) C_ RR`
8 ax-resscn
` |-  RR C_ CC`
9 7 8 sstri
` |-  ( 0 [,) +oo ) C_ CC`
10 9 a1i
` |-  ( ph -> ( 0 [,) +oo ) C_ CC )`
11 ge0mulcl
` |-  ( ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) -> ( x x. y ) e. ( 0 [,) +oo ) )`
` |-  ( ( ph /\ ( x e. ( 0 [,) +oo ) /\ y e. ( 0 [,) +oo ) ) ) -> ( x x. y ) e. ( 0 [,) +oo ) )`
13 elrege0
` |-  ( B e. ( 0 [,) +oo ) <-> ( B e. RR /\ 0 <_ B ) )`
14 3 4 13 sylanbrc
` |-  ( ( ph /\ k e. A ) -> B e. ( 0 [,) +oo ) )`
15 1re
` |-  1 e. RR`
16 0le1
` |-  0 <_ 1`
17 ltpnf
` |-  ( 1 e. RR -> 1 < +oo )`
18 15 17 ax-mp
` |-  1 < +oo`
19 0re
` |-  0 e. RR`
20 elico2
` |-  ( ( 0 e. RR /\ +oo e. RR* ) -> ( 1 e. ( 0 [,) +oo ) <-> ( 1 e. RR /\ 0 <_ 1 /\ 1 < +oo ) ) )`
21 19 6 20 mp2an
` |-  ( 1 e. ( 0 [,) +oo ) <-> ( 1 e. RR /\ 0 <_ 1 /\ 1 < +oo ) )`
22 15 16 18 21 mpbir3an
` |-  1 e. ( 0 [,) +oo )`
23 22 a1i
` |-  ( ph -> 1 e. ( 0 [,) +oo ) )`
24 1 10 12 2 14 23 fprodcllemf
` |-  ( ph -> prod_ k e. A B e. ( 0 [,) +oo ) )`
25 icogelb
` |-  ( ( 0 e. RR* /\ +oo e. RR* /\ prod_ k e. A B e. ( 0 [,) +oo ) ) -> 0 <_ prod_ k e. A B )`
26 5 6 24 25 mp3an12i
` |-  ( ph -> 0 <_ prod_ k e. A B )`