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	$⊢ Ⅎ k φ$
	fprodle.a	$⊢ φ \to A \in Fin$
	fprodle.b	$⊢ (φ \land k \in A) \to B \in ℝ$
	fprodle.0l3b	$⊢ (φ \land k \in A) \to 0 \leq B$
	fprodle.c	$⊢ (φ \land k \in A) \to C \in ℝ$
	fprodle.blec	$⊢ (φ \land k \in A) \to B \leq C$
Assertion	fprodle	$⊢ φ \to \prod_{k \in A} B \leq \prod_{k \in A} C$

Proof

Step	Hyp	Ref	Expression
1		fprodle.kph	$⊢ Ⅎ k φ$
2		fprodle.a	$⊢ φ \to A \in Fin$
3		fprodle.b	$⊢ (φ \land k \in A) \to B \in ℝ$
4		fprodle.0l3b	$⊢ (φ \land k \in A) \to 0 \leq B$
5		fprodle.c	$⊢ (φ \land k \in A) \to C \in ℝ$
6		fprodle.blec	$⊢ (φ \land k \in A) \to B \leq C$
7		1red	$⊢ (φ \land \forall k \in A B \neq 0) \to 1 \in ℝ$
8		nfra1	$⊢ Ⅎ k \forall k \in A B \neq 0$
9	1 8	nfan	$⊢ Ⅎ k (φ \land \forall k \in A B \neq 0)$
10	2	adantr	$⊢ (φ \land \forall k \in A B \neq 0) \to A \in Fin$
11	5	adantlr	$⊢ ((φ \land \forall k \in A B \neq 0) \land k \in A) \to C \in ℝ$
12	3	adantlr	$⊢ ((φ \land \forall k \in A B \neq 0) \land k \in A) \to B \in ℝ$
13		rspa	$⊢ (\forall k \in A B \neq 0 \land k \in A) \to B \neq 0$
14	13	adantll	$⊢ ((φ \land \forall k \in A B \neq 0) \land k \in A) \to B \neq 0$
15	11 12 14	redivcld	$⊢ ((φ \land \forall k \in A B \neq 0) \land k \in A) \to \frac{C}{B} \in ℝ$
16	9 10 15	fprodreclf	$⊢ (φ \land \forall k \in A B \neq 0) \to \prod_{k \in A} (\frac{C}{B}) \in ℝ$
17	1 2 3	fprodreclf	$⊢ φ \to \prod_{k \in A} B \in ℝ$
18	17	adantr	$⊢ (φ \land \forall k \in A B \neq 0) \to \prod_{k \in A} B \in ℝ$
19	1 2 3 4	fprodge0	$⊢ φ \to 0 \leq \prod_{k \in A} B$
20	19	adantr	$⊢ (φ \land \forall k \in A B \neq 0) \to 0 \leq \prod_{k \in A} B$
21	4	adantlr	$⊢ ((φ \land \forall k \in A B \neq 0) \land k \in A) \to 0 \leq B$
22	12 21 14	ne0gt0d	$⊢ ((φ \land \forall k \in A B \neq 0) \land k \in A) \to 0 < B$
23	12 22	elrpd	$⊢ ((φ \land \forall k \in A B \neq 0) \land k \in A) \to B \in ℝ^{+}$
24	6	adantlr	$⊢ ((φ \land \forall k \in A B \neq 0) \land k \in A) \to B \leq C$
25		divge1	$⊢ (B \in ℝ^{+} \land C \in ℝ \land B \leq C) \to 1 \leq \frac{C}{B}$
26	23 11 24 25	syl3anc	$⊢ ((φ \land \forall k \in A B \neq 0) \land k \in A) \to 1 \leq \frac{C}{B}$
27	9 10 15 26	fprodge1	$⊢ (φ \land \forall k \in A B \neq 0) \to 1 \leq \prod_{k \in A} (\frac{C}{B})$
28	7 16 18 20 27	lemul2ad	$⊢ (φ \land \forall k \in A B \neq 0) \to \prod_{k \in A} B \cdot 1 \leq \prod_{k \in A} B \prod_{k \in A} (\frac{C}{B})$
29	3	recnd	$⊢ (φ \land k \in A) \to B \in ℂ$
30	1 2 29	fprodclf	$⊢ φ \to \prod_{k \in A} B \in ℂ$
31	30	mulid1d	$⊢ φ \to \prod_{k \in A} B \cdot 1 = \prod_{k \in A} B$
32	31	adantr	$⊢ (φ \land \forall k \in A B \neq 0) \to \prod_{k \in A} B \cdot 1 = \prod_{k \in A} B$
33	5	recnd	$⊢ (φ \land k \in A) \to C \in ℂ$
34	33	adantlr	$⊢ ((φ \land \forall k \in A B \neq 0) \land k \in A) \to C \in ℂ$
35	29	adantlr	$⊢ ((φ \land \forall k \in A B \neq 0) \land k \in A) \to B \in ℂ$
36	9 10 34 35 14	fproddivf	$⊢ (φ \land \forall k \in A B \neq 0) \to \prod_{k \in A} (\frac{C}{B}) = \frac{\prod_{k \in A} C}{\prod_{k \in A} B}$
37	36	oveq2d	$⊢ (φ \land \forall k \in A B \neq 0) \to \prod_{k \in A} B \prod_{k \in A} (\frac{C}{B}) = \prod_{k \in A} B (\frac{\prod_{k \in A} C}{\prod_{k \in A} B})$
38	1 2 33	fprodclf	$⊢ φ \to \prod_{k \in A} C \in ℂ$
39	38	adantr	$⊢ (φ \land \forall k \in A B \neq 0) \to \prod_{k \in A} C \in ℂ$
40	30	adantr	$⊢ (φ \land \forall k \in A B \neq 0) \to \prod_{k \in A} B \in ℂ$
41	9 10 35 14	fprodn0f	$⊢ (φ \land \forall k \in A B \neq 0) \to \prod_{k \in A} B \neq 0$
42	39 40 41	divcan2d	$⊢ (φ \land \forall k \in A B \neq 0) \to \prod_{k \in A} B (\frac{\prod_{k \in A} C}{\prod_{k \in A} B}) = \prod_{k \in A} C$
43	37 42	eqtrd	$⊢ (φ \land \forall k \in A B \neq 0) \to \prod_{k \in A} B \prod_{k \in A} (\frac{C}{B}) = \prod_{k \in A} C$
44	28 32 43	3brtr3d	$⊢ (φ \land \forall k \in A B \neq 0) \to \prod_{k \in A} B \leq \prod_{k \in A} C$
45		nne	$⊢ \neg B \neq 0 \leftrightarrow B = 0$
46	45	rexbii	$⊢ \exists k \in A \neg B \neq 0 \leftrightarrow \exists k \in A B = 0$
47		rexnal	$⊢ \exists k \in A \neg B \neq 0 \leftrightarrow \neg \forall k \in A B \neq 0$
48		nfv	$⊢ Ⅎ j B = 0$
49		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ j / k ⦌ B$
50	49	nfeq1	$⊢ Ⅎ k ⦋ j / k ⦌ B = 0$
51		csbeq1a	$⊢ k = j \to B = ⦋ j / k ⦌ B$
52	51	eqeq1d	$⊢ k = j \to (B = 0 \leftrightarrow ⦋ j / k ⦌ B = 0)$
53	48 50 52	cbvrexw	$⊢ \exists k \in A B = 0 \leftrightarrow \exists j \in A ⦋ j / k ⦌ B = 0$
54	46 47 53	3bitr3i	$⊢ \neg \forall k \in A B \neq 0 \leftrightarrow \exists j \in A ⦋ j / k ⦌ B = 0$
55		nfv	$⊢ Ⅎ k j \in A$
56	1 55 50	nf3an	$⊢ Ⅎ k (φ \land j \in A \land ⦋ j / k ⦌ B = 0)$
57	2	3ad2ant1	$⊢ (φ \land j \in A \land ⦋ j / k ⦌ B = 0) \to A \in Fin$
58	29	3ad2antl1	$⊢ ((φ \land j \in A \land ⦋ j / k ⦌ B = 0) \land k \in A) \to B \in ℂ$
59		simp2	$⊢ (φ \land j \in A \land ⦋ j / k ⦌ B = 0) \to j \in A$
60	52	biimparc	$⊢ (⦋ j / k ⦌ B = 0 \land k = j) \to B = 0$
61	60	3ad2antl3	$⊢ ((φ \land j \in A \land ⦋ j / k ⦌ B = 0) \land k = j) \to B = 0$
62	56 57 58 59 61	fprodeq0g	$⊢ (φ \land j \in A \land ⦋ j / k ⦌ B = 0) \to \prod_{k \in A} B = 0$
63	62	rexlimdv3a	$⊢ φ \to (\exists j \in A ⦋ j / k ⦌ B = 0 \to \prod_{k \in A} B = 0)$
64	63	imp	$⊢ (φ \land \exists j \in A ⦋ j / k ⦌ B = 0) \to \prod_{k \in A} B = 0$
65		0red	$⊢ (φ \land k \in A) \to 0 \in ℝ$
66	65 3 5 4 6	letrd	$⊢ (φ \land k \in A) \to 0 \leq C$
67	1 2 5 66	fprodge0	$⊢ φ \to 0 \leq \prod_{k \in A} C$
68	67	adantr	$⊢ (φ \land \exists j \in A ⦋ j / k ⦌ B = 0) \to 0 \leq \prod_{k \in A} C$
69	64 68	eqbrtrd	$⊢ (φ \land \exists j \in A ⦋ j / k ⦌ B = 0) \to \prod_{k \in A} B \leq \prod_{k \in A} C$
70	54 69	sylan2b	$⊢ (φ \land \neg \forall k \in A B \neq 0) \to \prod_{k \in A} B \leq \prod_{k \in A} C$
71	44 70	pm2.61dan	$⊢ φ \to \prod_{k \in A} B \leq \prod_{k \in A} C$

Metamath Proof Explorer

Theorem fprodle

Proof