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 mulid1d
 |-  ( 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 )