fprodex01

Description: A product of factors equal to zero or one is zero exactly when one of the factors is zero. (Contributed by Thierry Arnoux, 11-Dec-2021)

	Ref	Expression
Hypotheses	fprodex01.1	$⊢ k = l \to B = C$
	fprodex01.a	$⊢ φ \to A \in Fin$
	fprodex01.b	$⊢ (φ \land k \in A) \to B \in \{0, 1\}$
Assertion	fprodex01	$⊢ φ \to \prod_{k \in A} B = if (\forall l \in A C = 1, 1, 0)$

Proof

Step	Hyp	Ref	Expression
1		fprodex01.1	$⊢ k = l \to B = C$
2		fprodex01.a	$⊢ φ \to A \in Fin$
3		fprodex01.b	$⊢ (φ \land k \in A) \to B \in \{0, 1\}$
4	1	eqeq1d	$⊢ k = l \to (B = 1 \leftrightarrow C = 1)$
5	4	cbvralvw	$⊢ \forall k \in A B = 1 \leftrightarrow \forall l \in A C = 1$
6	5	bilanri	$⊢ (φ \land \forall l \in A C = 1) \to \forall k \in A B = 1$
7	6	prodeq2d	$⊢ (φ \land \forall l \in A C = 1) \to \prod_{k \in A} B = \prod_{k \in A} 1$
8		prod1	$⊢ (A \subseteq ℤ_{\geq 0} \lor A \in Fin) \to \prod_{k \in A} 1 = 1$
9	8	olcs	$⊢ A \in Fin \to \prod_{k \in A} 1 = 1$
10	2 9	syl	$⊢ φ \to \prod_{k \in A} 1 = 1$
11	10	adantr	$⊢ (φ \land \forall l \in A C = 1) \to \prod_{k \in A} 1 = 1$
12	7 11	eqtr2d	$⊢ (φ \land \forall l \in A C = 1) \to 1 = \prod_{k \in A} B$
13		nfv	$⊢ Ⅎ l φ$
14		nfra1	$⊢ Ⅎ l \forall l \in A C = 1$
15	14	nfn	$⊢ Ⅎ l \neg \forall l \in A C = 1$
16	13 15	nfan	$⊢ Ⅎ l (φ \land \neg \forall l \in A C = 1)$
17		nfv	$⊢ Ⅎ l \prod_{k \in A} B = 0$
18	2	adantr	$⊢ (φ \land \neg \forall l \in A C = 1) \to A \in Fin$
19	18	ad2antrr	$⊢ (((φ \land \neg \forall l \in A C = 1) \land l \in A) \land C = 0) \to A \in Fin$
20		pr01ssre	$⊢ \{0, 1\} \subseteq ℝ$
21		ax-resscn	$⊢ ℝ \subseteq ℂ$
22	20 21	sstri	$⊢ \{0, 1\} \subseteq ℂ$
23	22 3	sselid	$⊢ (φ \land k \in A) \to B \in ℂ$
24	23	adantlr	$⊢ ((φ \land \neg \forall l \in A C = 1) \land k \in A) \to B \in ℂ$
25	24	adantlr	$⊢ (((φ \land \neg \forall l \in A C = 1) \land l \in A) \land k \in A) \to B \in ℂ$
26	25	adantlr	$⊢ ((((φ \land \neg \forall l \in A C = 1) \land l \in A) \land C = 0) \land k \in A) \to B \in ℂ$
27		simplr	$⊢ (((φ \land \neg \forall l \in A C = 1) \land l \in A) \land C = 0) \to l \in A$
28		simpr	$⊢ (((φ \land \neg \forall l \in A C = 1) \land l \in A) \land C = 0) \to C = 0$
29	1 19 26 27 28	fprodeq02	$⊢ (((φ \land \neg \forall l \in A C = 1) \land l \in A) \land C = 0) \to \prod_{k \in A} B = 0$
30		rexnal	$⊢ \exists l \in A \neg C = 1 \leftrightarrow \neg \forall l \in A C = 1$
31	30	bilanri	$⊢ (φ \land \neg \forall l \in A C = 1) \to \exists l \in A \neg C = 1$
32	3	ralrimiva	$⊢ φ \to \forall k \in A B \in \{0, 1\}$
33	1	eleq1d	$⊢ k = l \to (B \in \{0, 1\} \leftrightarrow C \in \{0, 1\})$
34	33	cbvralvw	$⊢ \forall k \in A B \in \{0, 1\} \leftrightarrow \forall l \in A C \in \{0, 1\}$
35	32 34	sylib	$⊢ φ \to \forall l \in A C \in \{0, 1\}$
36	35	r19.21bi	$⊢ (φ \land l \in A) \to C \in \{0, 1\}$
37		c0ex	$⊢ 0 \in V$
38		1ex	$⊢ 1 \in V$
39	37 38	elpr2	$⊢ C \in \{0, 1\} \leftrightarrow (C = 0 \lor C = 1)$
40	36 39	sylib	$⊢ (φ \land l \in A) \to (C = 0 \lor C = 1)$
41	40	orcomd	$⊢ (φ \land l \in A) \to (C = 1 \lor C = 0)$
42	41	ord	$⊢ (φ \land l \in A) \to (\neg C = 1 \to C = 0)$
43	42	reximdva	$⊢ φ \to (\exists l \in A \neg C = 1 \to \exists l \in A C = 0)$
44	43	adantr	$⊢ (φ \land \neg \forall l \in A C = 1) \to (\exists l \in A \neg C = 1 \to \exists l \in A C = 0)$
45	31 44	mpd	$⊢ (φ \land \neg \forall l \in A C = 1) \to \exists l \in A C = 0$
46	16 17 29 45	r19.29af2	$⊢ (φ \land \neg \forall l \in A C = 1) \to \prod_{k \in A} B = 0$
47	46	eqcomd	$⊢ (φ \land \neg \forall l \in A C = 1) \to 0 = \prod_{k \in A} B$
48	12 47	ifeqda	$⊢ φ \to if (\forall l \in A C = 1, 1, 0) = \prod_{k \in A} B$
49	48	eqcomd	$⊢ φ \to \prod_{k \in A} B = if (\forall l \in A C = 1, 1, 0)$

Metamath Proof Explorer

Theorem fprodex01

Proof