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 ) )
12 11 adantl 
 |-  ( ( 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 )