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

Metamath Proof Explorer

Theorem fprodge1

Description: If all of the terms of a finite product are greater than or equal to 1 , so is the product. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses fprodge1.ph 
|- F/ k ph
fprodge1.a 
|- ( ph -> A e. Fin )
fprodge1.b 
|- ( ( ph /\ k e. A ) -> B e. RR )
fprodge1.ge 
|- ( ( ph /\ k e. A ) -> 1 <_ B )
Assertion fprodge1 
|- ( ph -> 1 <_ prod_ k e. A B )

Proof

Step Hyp Ref Expression
1 fprodge1.ph 
 |-  F/ k ph
2 fprodge1.a 
 |-  ( ph -> A e. Fin )
3 fprodge1.b 
 |-  ( ( ph /\ k e. A ) -> B e. RR )
4 fprodge1.ge 
 |-  ( ( ph /\ k e. A ) -> 1 <_ B )
5 1xr 
 |-  1 e. RR*
6 pnfxr 
 |-  +oo e. RR*
7 1re 
 |-  1 e. RR
8 icossre 
 |-  ( ( 1 e. RR /\ +oo e. RR* ) -> ( 1 [,) +oo ) C_ RR )
9 7 6 8 mp2an 
 |-  ( 1 [,) +oo ) C_ RR
10 ax-resscn 
 |-  RR C_ CC
11 9 10 sstri 
 |-  ( 1 [,) +oo ) C_ CC
12 11 a1i 
 |-  ( ph -> ( 1 [,) +oo ) C_ CC )
13 5 a1i 
 |-  ( ( x e. ( 1 [,) +oo ) /\ y e. ( 1 [,) +oo ) ) -> 1 e. RR* )
14 6 a1i 
 |-  ( ( x e. ( 1 [,) +oo ) /\ y e. ( 1 [,) +oo ) ) -> +oo e. RR* )
15 9 sseli 
 |-  ( x e. ( 1 [,) +oo ) -> x e. RR )
16 15 adantr 
 |-  ( ( x e. ( 1 [,) +oo ) /\ y e. ( 1 [,) +oo ) ) -> x e. RR )
17 9 sseli 
 |-  ( y e. ( 1 [,) +oo ) -> y e. RR )
18 17 adantl 
 |-  ( ( x e. ( 1 [,) +oo ) /\ y e. ( 1 [,) +oo ) ) -> y e. RR )
19 16 18 remulcld 
 |-  ( ( x e. ( 1 [,) +oo ) /\ y e. ( 1 [,) +oo ) ) -> ( x x. y ) e. RR )
20 19 rexrd 
 |-  ( ( x e. ( 1 [,) +oo ) /\ y e. ( 1 [,) +oo ) ) -> ( x x. y ) e. RR* )
21 1t1e1 
 |-  ( 1 x. 1 ) = 1
22 7 a1i 
 |-  ( ( x e. ( 1 [,) +oo ) /\ y e. ( 1 [,) +oo ) ) -> 1 e. RR )
23 0le1 
 |-  0 <_ 1
24 23 a1i 
 |-  ( ( x e. ( 1 [,) +oo ) /\ y e. ( 1 [,) +oo ) ) -> 0 <_ 1 )
25 icogelb 
 |-  ( ( 1 e. RR* /\ +oo e. RR* /\ x e. ( 1 [,) +oo ) ) -> 1 <_ x )
26 5 6 25 mp3an12 
 |-  ( x e. ( 1 [,) +oo ) -> 1 <_ x )
27 26 adantr 
 |-  ( ( x e. ( 1 [,) +oo ) /\ y e. ( 1 [,) +oo ) ) -> 1 <_ x )
28 icogelb 
 |-  ( ( 1 e. RR* /\ +oo e. RR* /\ y e. ( 1 [,) +oo ) ) -> 1 <_ y )
29 5 6 28 mp3an12 
 |-  ( y e. ( 1 [,) +oo ) -> 1 <_ y )
30 29 adantl 
 |-  ( ( x e. ( 1 [,) +oo ) /\ y e. ( 1 [,) +oo ) ) -> 1 <_ y )
31 22 16 22 18 24 24 27 30 lemul12ad 
 |-  ( ( x e. ( 1 [,) +oo ) /\ y e. ( 1 [,) +oo ) ) -> ( 1 x. 1 ) <_ ( x x. y ) )
32 21 31 eqbrtrrid 
 |-  ( ( x e. ( 1 [,) +oo ) /\ y e. ( 1 [,) +oo ) ) -> 1 <_ ( x x. y ) )
33 19 ltpnfd 
 |-  ( ( x e. ( 1 [,) +oo ) /\ y e. ( 1 [,) +oo ) ) -> ( x x. y ) < +oo )
34 13 14 20 32 33 elicod 
 |-  ( ( x e. ( 1 [,) +oo ) /\ y e. ( 1 [,) +oo ) ) -> ( x x. y ) e. ( 1 [,) +oo ) )
35 34 adantl 
 |-  ( ( ph /\ ( x e. ( 1 [,) +oo ) /\ y e. ( 1 [,) +oo ) ) ) -> ( x x. y ) e. ( 1 [,) +oo ) )
36 5 a1i 
 |-  ( ( ph /\ k e. A ) -> 1 e. RR* )
37 6 a1i 
 |-  ( ( ph /\ k e. A ) -> +oo e. RR* )
38 3 rexrd 
 |-  ( ( ph /\ k e. A ) -> B e. RR* )
39 3 ltpnfd 
 |-  ( ( ph /\ k e. A ) -> B < +oo )
40 36 37 38 4 39 elicod 
 |-  ( ( ph /\ k e. A ) -> B e. ( 1 [,) +oo ) )
41 1le1 
 |-  1 <_ 1
42 ltpnf 
 |-  ( 1 e. RR -> 1 < +oo )
43 7 42 ax-mp 
 |-  1 < +oo
44 elico2 
 |-  ( ( 1 e. RR /\ +oo e. RR* ) -> ( 1 e. ( 1 [,) +oo ) <-> ( 1 e. RR /\ 1 <_ 1 /\ 1 < +oo ) ) )
45 7 6 44 mp2an 
 |-  ( 1 e. ( 1 [,) +oo ) <-> ( 1 e. RR /\ 1 <_ 1 /\ 1 < +oo ) )
46 7 41 43 45 mpbir3an 
 |-  1 e. ( 1 [,) +oo )
47 46 a1i 
 |-  ( ph -> 1 e. ( 1 [,) +oo ) )
48 1 12 35 2 40 47 fprodcllemf 
 |-  ( ph -> prod_ k e. A B e. ( 1 [,) +oo ) )
49 icogelb 
 |-  ( ( 1 e. RR* /\ +oo e. RR* /\ prod_ k e. A B e. ( 1 [,) +oo ) ) -> 1 <_ prod_ k e. A B )
50 5 6 48 49 mp3an12i 
 |-  ( ph -> 1 <_ prod_ k e. A B )