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

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 ⊢ Ⅎ 𝑘 𝜑
fprodle.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
fprodle.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
fprodle.0l3b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 0 ≤ 𝐵 )
fprodle.c ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ℝ )
fprodle.blec ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ≤ 𝐶 )
Assertion fprodle ( 𝜑 → ∏ 𝑘 ∈ 𝐴 𝐵 ≤ ∏ 𝑘 ∈ 𝐴 𝐶 )

Proof

Step Hyp Ref Expression
1 fprodle.kph ⊢ Ⅎ 𝑘 𝜑
2 fprodle.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
3 fprodle.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
4 fprodle.0l3b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 0 ≤ 𝐵 )
5 fprodle.c ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ℝ )
6 fprodle.blec ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ≤ 𝐶 )
7 1red ⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ≠ 0 ) → 1 ∈ ℝ )
8 nfra1 ⊢ Ⅎ 𝑘 ∀ 𝑘 ∈ 𝐴 𝐵 ≠ 0
9 1 8 nfan ⊢ Ⅎ 𝑘 ( 𝜑 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ≠ 0 )
10 2 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ≠ 0 ) → 𝐴 ∈ Fin )
11 5 adantlr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ≠ 0 ) ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ℝ )
12 3 adantlr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ≠ 0 ) ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
13 rspa ⊢ ( ( ∀ 𝑘 ∈ 𝐴 𝐵 ≠ 0 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ≠ 0 )
14 13 adantll ⊢ ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ≠ 0 ) ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ≠ 0 )
15 11 12 14 redivcld ⊢ ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ≠ 0 ) ∧ 𝑘 ∈ 𝐴 ) → ( 𝐶 / 𝐵 ) ∈ ℝ )
16 9 10 15 fprodreclf ⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ≠ 0 ) → ∏ 𝑘 ∈ 𝐴 ( 𝐶 / 𝐵 ) ∈ ℝ )
17 1 2 3 fprodreclf ⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐴 𝐵 ∈ ℝ )
18 17 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ≠ 0 ) → ∏ 𝑘 ∈ 𝐴 𝐵 ∈ ℝ )
19 1 2 3 4 fprodge0 ⊢ ( 𝜑 → 0 ≤ ∏ 𝑘 ∈ 𝐴 𝐵 )
20 19 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ≠ 0 ) → 0 ≤ ∏ 𝑘 ∈ 𝐴 𝐵 )
21 4 adantlr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ≠ 0 ) ∧ 𝑘 ∈ 𝐴 ) → 0 ≤ 𝐵 )
22 12 21 14 ne0gt0d ⊢ ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ≠ 0 ) ∧ 𝑘 ∈ 𝐴 ) → 0 < 𝐵 )
23 12 22 elrpd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ≠ 0 ) ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℝ+ )
24 6 adantlr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ≠ 0 ) ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ≤ 𝐶 )
25 divge1 ⊢ ( ( 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ ∧ 𝐵 ≤ 𝐶 ) → 1 ≤ ( 𝐶 / 𝐵 ) )
26 23 11 24 25 syl3anc ⊢ ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ≠ 0 ) ∧ 𝑘 ∈ 𝐴 ) → 1 ≤ ( 𝐶 / 𝐵 ) )
27 9 10 15 26 fprodge1 ⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ≠ 0 ) → 1 ≤ ∏ 𝑘 ∈ 𝐴 ( 𝐶 / 𝐵 ) )
28 7 16 18 20 27 lemul2ad ⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ≠ 0 ) → ( ∏ 𝑘 ∈ 𝐴 𝐵 · 1 ) ≤ ( ∏ 𝑘 ∈ 𝐴 𝐵 · ∏ 𝑘 ∈ 𝐴 ( 𝐶 / 𝐵 ) ) )
29 3 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
30 1 2 29 fprodclf ⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐴 𝐵 ∈ ℂ )
31 30 mulridd ⊢ ( 𝜑 → ( ∏ 𝑘 ∈ 𝐴 𝐵 · 1 ) = ∏ 𝑘 ∈ 𝐴 𝐵 )
32 31 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ≠ 0 ) → ( ∏ 𝑘 ∈ 𝐴 𝐵 · 1 ) = ∏ 𝑘 ∈ 𝐴 𝐵 )
33 5 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
34 33 adantlr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ≠ 0 ) ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
35 29 adantlr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ≠ 0 ) ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
36 9 10 34 35 14 fproddivf ⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ≠ 0 ) → ∏ 𝑘 ∈ 𝐴 ( 𝐶 / 𝐵 ) = ( ∏ 𝑘 ∈ 𝐴 𝐶 / ∏ 𝑘 ∈ 𝐴 𝐵 ) )
37 36 oveq2d ⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ≠ 0 ) → ( ∏ 𝑘 ∈ 𝐴 𝐵 · ∏ 𝑘 ∈ 𝐴 ( 𝐶 / 𝐵 ) ) = ( ∏ 𝑘 ∈ 𝐴 𝐵 · ( ∏ 𝑘 ∈ 𝐴 𝐶 / ∏ 𝑘 ∈ 𝐴 𝐵 ) ) )
38 1 2 33 fprodclf ⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐴 𝐶 ∈ ℂ )
39 38 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ≠ 0 ) → ∏ 𝑘 ∈ 𝐴 𝐶 ∈ ℂ )
40 30 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ≠ 0 ) → ∏ 𝑘 ∈ 𝐴 𝐵 ∈ ℂ )
41 9 10 35 14 fprodn0f ⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ≠ 0 ) → ∏ 𝑘 ∈ 𝐴 𝐵 ≠ 0 )
42 39 40 41 divcan2d ⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ≠ 0 ) → ( ∏ 𝑘 ∈ 𝐴 𝐵 · ( ∏ 𝑘 ∈ 𝐴 𝐶 / ∏ 𝑘 ∈ 𝐴 𝐵 ) ) = ∏ 𝑘 ∈ 𝐴 𝐶 )
43 37 42 eqtrd ⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ≠ 0 ) → ( ∏ 𝑘 ∈ 𝐴 𝐵 · ∏ 𝑘 ∈ 𝐴 ( 𝐶 / 𝐵 ) ) = ∏ 𝑘 ∈ 𝐴 𝐶 )
44 28 32 43 3brtr3d ⊢ ( ( 𝜑 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ≠ 0 ) → ∏ 𝑘 ∈ 𝐴 𝐵 ≤ ∏ 𝑘 ∈ 𝐴 𝐶 )
45 nne ⊢ ( ¬ 𝐵 ≠ 0 ↔ 𝐵 = 0 )
46 45 rexbii ⊢ ( ∃ 𝑘 ∈ 𝐴 ¬ 𝐵 ≠ 0 ↔ ∃ 𝑘 ∈ 𝐴 𝐵 = 0 )
47 rexnal ⊢ ( ∃ 𝑘 ∈ 𝐴 ¬ 𝐵 ≠ 0 ↔ ¬ ∀ 𝑘 ∈ 𝐴 𝐵 ≠ 0 )
48 nfv ⊢ Ⅎ 𝑗 𝐵 = 0
49 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐵
50 49 nfeq1 ⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐵 = 0
51 csbeq1a ⊢ ( 𝑘 = 𝑗 → 𝐵 = ⦋ 𝑗 / 𝑘 ⦌ 𝐵 )
52 51 eqeq1d ⊢ ( 𝑘 = 𝑗 → ( 𝐵 = 0 ↔ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 = 0 ) )
53 48 50 52 cbvrexw ⊢ ( ∃ 𝑘 ∈ 𝐴 𝐵 = 0 ↔ ∃ 𝑗 ∈ 𝐴 ⦋ 𝑗 / 𝑘 ⦌ 𝐵 = 0 )
54 46 47 53 3bitr3i ⊢ ( ¬ ∀ 𝑘 ∈ 𝐴 𝐵 ≠ 0 ↔ ∃ 𝑗 ∈ 𝐴 ⦋ 𝑗 / 𝑘 ⦌ 𝐵 = 0 )
55 nfv ⊢ Ⅎ 𝑘 𝑗 ∈ 𝐴
56 1 55 50 nf3an ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑗 ∈ 𝐴 ∧ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 = 0 )
57 2 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ∧ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 = 0 ) → 𝐴 ∈ Fin )
58 29 3ad2antl1 ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ∧ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 = 0 ) ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
59 simp2 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ∧ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 = 0 ) → 𝑗 ∈ 𝐴 )
60 52 biimparc ⊢ ( ( ⦋ 𝑗 / 𝑘 ⦌ 𝐵 = 0 ∧ 𝑘 = 𝑗 ) → 𝐵 = 0 )
61 60 3ad2antl3 ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ∧ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 = 0 ) ∧ 𝑘 = 𝑗 ) → 𝐵 = 0 )
62 56 57 58 59 61 fprodeq0g ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ∧ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 = 0 ) → ∏ 𝑘 ∈ 𝐴 𝐵 = 0 )
63 62 rexlimdv3a ⊢ ( 𝜑 → ( ∃ 𝑗 ∈ 𝐴 ⦋ 𝑗 / 𝑘 ⦌ 𝐵 = 0 → ∏ 𝑘 ∈ 𝐴 𝐵 = 0 ) )
64 63 imp ⊢ ( ( 𝜑 ∧ ∃ 𝑗 ∈ 𝐴 ⦋ 𝑗 / 𝑘 ⦌ 𝐵 = 0 ) → ∏ 𝑘 ∈ 𝐴 𝐵 = 0 )
65 0red ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 0 ∈ ℝ )
66 65 3 5 4 6 letrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 0 ≤ 𝐶 )
67 1 2 5 66 fprodge0 ⊢ ( 𝜑 → 0 ≤ ∏ 𝑘 ∈ 𝐴 𝐶 )
68 67 adantr ⊢ ( ( 𝜑 ∧ ∃ 𝑗 ∈ 𝐴 ⦋ 𝑗 / 𝑘 ⦌ 𝐵 = 0 ) → 0 ≤ ∏ 𝑘 ∈ 𝐴 𝐶 )
69 64 68 eqbrtrd ⊢ ( ( 𝜑 ∧ ∃ 𝑗 ∈ 𝐴 ⦋ 𝑗 / 𝑘 ⦌ 𝐵 = 0 ) → ∏ 𝑘 ∈ 𝐴 𝐵 ≤ ∏ 𝑘 ∈ 𝐴 𝐶 )
70 54 69 sylan2b ⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑘 ∈ 𝐴 𝐵 ≠ 0 ) → ∏ 𝑘 ∈ 𝐴 𝐵 ≤ ∏ 𝑘 ∈ 𝐴 𝐶 )
71 44 70 pm2.61dan ⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐴 𝐵 ≤ ∏ 𝑘 ∈ 𝐴 𝐶 )