Metamath Proof Explorer

Theorem fprodle

Description: If all the terms of two finite products are nonnegative and compare, so do the two products. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses fprodle.kph 
|- F/ k ph
fprodle.a 
|- ( ph -> A e. Fin )
fprodle.b 
|- ( ( ph /\ k e. A ) -> B e. RR )
fprodle.0l3b 
|- ( ( ph /\ k e. A ) -> 0 <_ B )
fprodle.c 
|- ( ( ph /\ k e. A ) -> C e. RR )
fprodle.blec 
|- ( ( ph /\ k e. A ) -> B <_ C )
Assertion fprodle 
|- ( ph -> prod_ k e. A B <_ prod_ k e. A C )

Proof

Step Hyp Ref Expression
1 fprodle.kph 
 |-  F/ k ph
2 fprodle.a 
 |-  ( ph -> A e. Fin )
3 fprodle.b 
 |-  ( ( ph /\ k e. A ) -> B e. RR )
4 fprodle.0l3b 
 |-  ( ( ph /\ k e. A ) -> 0 <_ B )
5 fprodle.c 
 |-  ( ( ph /\ k e. A ) -> C e. RR )
6 fprodle.blec 
 |-  ( ( ph /\ k e. A ) -> B <_ C )
7 1red 
 |-  ( ( ph /\ A. k e. A B =/= 0 ) -> 1 e. RR )
8 nfra1 
 |-  F/ k A. k e. A B =/= 0
9 1 8 nfan 
 |-  F/ k ( ph /\ A. k e. A B =/= 0 )
10 2 adantr 
 |-  ( ( ph /\ A. k e. A B =/= 0 ) -> A e. Fin )
11 5 adantlr 
 |-  ( ( ( ph /\ A. k e. A B =/= 0 ) /\ k e. A ) -> C e. RR )
12 3 adantlr 
 |-  ( ( ( ph /\ A. k e. A B =/= 0 ) /\ k e. A ) -> B e. RR )
13 rspa 
 |-  ( ( A. k e. A B =/= 0 /\ k e. A ) -> B =/= 0 )
14 13 adantll 
 |-  ( ( ( ph /\ A. k e. A B =/= 0 ) /\ k e. A ) -> B =/= 0 )
15 11 12 14 redivcld 
 |-  ( ( ( ph /\ A. k e. A B =/= 0 ) /\ k e. A ) -> ( C / B ) e. RR )
16 9 10 15 fprodreclf 
 |-  ( ( ph /\ A. k e. A B =/= 0 ) -> prod_ k e. A ( C / B ) e. RR )
17 1 2 3 fprodreclf 
 |-  ( ph -> prod_ k e. A B e. RR )
18 17 adantr 
 |-  ( ( ph /\ A. k e. A B =/= 0 ) -> prod_ k e. A B e. RR )
19 1 2 3 4 fprodge0 
 |-  ( ph -> 0 <_ prod_ k e. A B )
20 19 adantr 
 |-  ( ( ph /\ A. k e. A B =/= 0 ) -> 0 <_ prod_ k e. A B )
21 4 adantlr 
 |-  ( ( ( ph /\ A. k e. A B =/= 0 ) /\ k e. A ) -> 0 <_ B )
22 12 21 14 ne0gt0d 
 |-  ( ( ( ph /\ A. k e. A B =/= 0 ) /\ k e. A ) -> 0 < B )
23 12 22 elrpd 
 |-  ( ( ( ph /\ A. k e. A B =/= 0 ) /\ k e. A ) -> B e. RR+ )
24 6 adantlr 
 |-  ( ( ( ph /\ A. k e. A B =/= 0 ) /\ k e. A ) -> B <_ C )
25 divge1 
 |-  ( ( B e. RR+ /\ C e. RR /\ B <_ C ) -> 1 <_ ( C / B ) )
26 23 11 24 25 syl3anc 
 |-  ( ( ( ph /\ A. k e. A B =/= 0 ) /\ k e. A ) -> 1 <_ ( C / B ) )
27 9 10 15 26 fprodge1 
 |-  ( ( ph /\ A. k e. A B =/= 0 ) -> 1 <_ prod_ k e. A ( C / B ) )
28 7 16 18 20 27 lemul2ad 
 |-  ( ( ph /\ A. k e. A B =/= 0 ) -> ( prod_ k e. A B x. 1 ) <_ ( prod_ k e. A B x. prod_ k e. A ( C / B ) ) )
29 3 recnd 
 |-  ( ( ph /\ k e. A ) -> B e. CC )
30 1 2 29 fprodclf 
 |-  ( ph -> prod_ k e. A B e. CC )
31 30 mulridd 
 |-  ( ph -> ( prod_ k e. A B x. 1 ) = prod_ k e. A B )
32 31 adantr 
 |-  ( ( ph /\ A. k e. A B =/= 0 ) -> ( prod_ k e. A B x. 1 ) = prod_ k e. A B )
33 5 recnd 
 |-  ( ( ph /\ k e. A ) -> C e. CC )
34 33 adantlr 
 |-  ( ( ( ph /\ A. k e. A B =/= 0 ) /\ k e. A ) -> C e. CC )
35 29 adantlr 
 |-  ( ( ( ph /\ A. k e. A B =/= 0 ) /\ k e. A ) -> B e. CC )
36 9 10 34 35 14 fproddivf 
 |-  ( ( ph /\ A. k e. A B =/= 0 ) -> prod_ k e. A ( C / B ) = ( prod_ k e. A C / prod_ k e. A B ) )
37 36 oveq2d 
 |-  ( ( ph /\ A. k e. A B =/= 0 ) -> ( prod_ k e. A B x. prod_ k e. A ( C / B ) ) = ( prod_ k e. A B x. ( prod_ k e. A C / prod_ k e. A B ) ) )
38 1 2 33 fprodclf 
 |-  ( ph -> prod_ k e. A C e. CC )
39 38 adantr 
 |-  ( ( ph /\ A. k e. A B =/= 0 ) -> prod_ k e. A C e. CC )
40 30 adantr 
 |-  ( ( ph /\ A. k e. A B =/= 0 ) -> prod_ k e. A B e. CC )
41 9 10 35 14 fprodn0f 
 |-  ( ( ph /\ A. k e. A B =/= 0 ) -> prod_ k e. A B =/= 0 )
42 39 40 41 divcan2d 
 |-  ( ( ph /\ A. k e. A B =/= 0 ) -> ( prod_ k e. A B x. ( prod_ k e. A C / prod_ k e. A B ) ) = prod_ k e. A C )
43 37 42 eqtrd 
 |-  ( ( ph /\ A. k e. A B =/= 0 ) -> ( prod_ k e. A B x. prod_ k e. A ( C / B ) ) = prod_ k e. A C )
44 28 32 43 3brtr3d 
 |-  ( ( ph /\ A. k e. A B =/= 0 ) -> prod_ k e. A B <_ prod_ k e. A C )
45 nne 
 |-  ( -. B =/= 0 <-> B = 0 )
46 45 rexbii 
 |-  ( E. k e. A -. B =/= 0 <-> E. k e. A B = 0 )
47 rexnal 
 |-  ( E. k e. A -. B =/= 0 <-> -. A. k e. A B =/= 0 )
48 nfv 
 |-  F/ j B = 0
49 nfcsb1v 
 |-  F/_ k [_ j / k ]_ B
50 49 nfeq1 
 |-  F/ k [_ j / k ]_ B = 0
51 csbeq1a 
 |-  ( k = j -> B = [_ j / k ]_ B )
52 51 eqeq1d 
 |-  ( k = j -> ( B = 0 <-> [_ j / k ]_ B = 0 ) )
53 48 50 52 cbvrexw 
 |-  ( E. k e. A B = 0 <-> E. j e. A [_ j / k ]_ B = 0 )
54 46 47 53 3bitr3i 
 |-  ( -. A. k e. A B =/= 0 <-> E. j e. A [_ j / k ]_ B = 0 )
55 nfv 
 |-  F/ k j e. A
56 1 55 50 nf3an 
 |-  F/ k ( ph /\ j e. A /\ [_ j / k ]_ B = 0 )
57 2 3ad2ant1 
 |-  ( ( ph /\ j e. A /\ [_ j / k ]_ B = 0 ) -> A e. Fin )
58 29 3ad2antl1 
 |-  ( ( ( ph /\ j e. A /\ [_ j / k ]_ B = 0 ) /\ k e. A ) -> B e. CC )
59 simp2 
 |-  ( ( ph /\ j e. A /\ [_ j / k ]_ B = 0 ) -> j e. A )
60 52 biimparc 
 |-  ( ( [_ j / k ]_ B = 0 /\ k = j ) -> B = 0 )
61 60 3ad2antl3 
 |-  ( ( ( ph /\ j e. A /\ [_ j / k ]_ B = 0 ) /\ k = j ) -> B = 0 )
62 56 57 58 59 61 fprodeq0g 
 |-  ( ( ph /\ j e. A /\ [_ j / k ]_ B = 0 ) -> prod_ k e. A B = 0 )
63 62 rexlimdv3a 
 |-  ( ph -> ( E. j e. A [_ j / k ]_ B = 0 -> prod_ k e. A B = 0 ) )
64 63 imp 
 |-  ( ( ph /\ E. j e. A [_ j / k ]_ B = 0 ) -> prod_ k e. A B = 0 )
65 0red 
 |-  ( ( ph /\ k e. A ) -> 0 e. RR )
66 65 3 5 4 6 letrd 
 |-  ( ( ph /\ k e. A ) -> 0 <_ C )
67 1 2 5 66 fprodge0 
 |-  ( ph -> 0 <_ prod_ k e. A C )
68 67 adantr 
 |-  ( ( ph /\ E. j e. A [_ j / k ]_ B = 0 ) -> 0 <_ prod_ k e. A C )
69 64 68 eqbrtrd 
 |-  ( ( ph /\ E. j e. A [_ j / k ]_ B = 0 ) -> prod_ k e. A B <_ prod_ k e. A C )
70 54 69 sylan2b 
 |-  ( ( ph /\ -. A. k e. A B =/= 0 ) -> prod_ k e. A B <_ prod_ k e. A C )
71 44 70 pm2.61dan 
 |-  ( ph -> prod_ k e. A B <_ prod_ k e. A C )