Theorem 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	⊢ ( 𝑘 = 𝑙 → 𝐵 = 𝐶 )
	fprodex01.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	fprodex01.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ { 0 , 1 } )
Assertion	fprodex01	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐴 𝐵 = if ( ∀ 𝑙 ∈ 𝐴 𝐶 = 1 , 1 , 0 ) )

Proof

Step	Hyp	Ref	Expression
1		fprodex01.1	⊢ ( 𝑘 = 𝑙 → 𝐵 = 𝐶 )
2		fprodex01.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
3		fprodex01.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ { 0 , 1 } )
4		simpr	⊢ ( ( 𝜑 ∧ ∀ 𝑙 ∈ 𝐴 𝐶 = 1 ) → ∀ 𝑙 ∈ 𝐴 𝐶 = 1 )
5	1	eqeq1d	⊢ ( 𝑘 = 𝑙 → ( 𝐵 = 1 ↔ 𝐶 = 1 ) )
6	5	cbvralvw	⊢ ( ∀ 𝑘 ∈ 𝐴 𝐵 = 1 ↔ ∀ 𝑙 ∈ 𝐴 𝐶 = 1 )
7	4 6	sylibr	⊢ ( ( 𝜑 ∧ ∀ 𝑙 ∈ 𝐴 𝐶 = 1 ) → ∀ 𝑘 ∈ 𝐴 𝐵 = 1 )
8	7	prodeq2d	⊢ ( ( 𝜑 ∧ ∀ 𝑙 ∈ 𝐴 𝐶 = 1 ) → ∏ 𝑘 ∈ 𝐴 𝐵 = ∏ 𝑘 ∈ 𝐴 1 )
9		prod1	⊢ ( ( 𝐴 ⊆ ( ℤ≥ ‘ 0 ) ∨ 𝐴 ∈ Fin ) → ∏ 𝑘 ∈ 𝐴 1 = 1 )
10	9	olcs	⊢ ( 𝐴 ∈ Fin → ∏ 𝑘 ∈ 𝐴 1 = 1 )
11	2 10	syl	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐴 1 = 1 )
12	11	adantr	⊢ ( ( 𝜑 ∧ ∀ 𝑙 ∈ 𝐴 𝐶 = 1 ) → ∏ 𝑘 ∈ 𝐴 1 = 1 )
13	8 12	eqtr2d	⊢ ( ( 𝜑 ∧ ∀ 𝑙 ∈ 𝐴 𝐶 = 1 ) → 1 = ∏ 𝑘 ∈ 𝐴 𝐵 )
14		nfv	⊢ Ⅎ 𝑙 𝜑
15		nfra1	⊢ Ⅎ 𝑙 ∀ 𝑙 ∈ 𝐴 𝐶 = 1
16	15	nfn	⊢ Ⅎ 𝑙 ¬ ∀ 𝑙 ∈ 𝐴 𝐶 = 1
17	14 16	nfan	⊢ Ⅎ 𝑙 ( 𝜑 ∧ ¬ ∀ 𝑙 ∈ 𝐴 𝐶 = 1 )
18		nfv	⊢ Ⅎ 𝑙 ∏ 𝑘 ∈ 𝐴 𝐵 = 0
19	2	adantr	⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑙 ∈ 𝐴 𝐶 = 1 ) → 𝐴 ∈ Fin )
20	19	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ¬ ∀ 𝑙 ∈ 𝐴 𝐶 = 1 ) ∧ 𝑙 ∈ 𝐴 ) ∧ 𝐶 = 0 ) → 𝐴 ∈ Fin )
21		pr01ssre	⊢ { 0 , 1 } ⊆ ℝ
22		ax-resscn	⊢ ℝ ⊆ ℂ
23	21 22	sstri	⊢ { 0 , 1 } ⊆ ℂ
24	23 3	sseldi	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
25	24	adantlr	⊢ ( ( ( 𝜑 ∧ ¬ ∀ 𝑙 ∈ 𝐴 𝐶 = 1 ) ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
26	25	adantlr	⊢ ( ( ( ( 𝜑 ∧ ¬ ∀ 𝑙 ∈ 𝐴 𝐶 = 1 ) ∧ 𝑙 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
27	26	adantlr	⊢ ( ( ( ( ( 𝜑 ∧ ¬ ∀ 𝑙 ∈ 𝐴 𝐶 = 1 ) ∧ 𝑙 ∈ 𝐴 ) ∧ 𝐶 = 0 ) ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
28		simplr	⊢ ( ( ( ( 𝜑 ∧ ¬ ∀ 𝑙 ∈ 𝐴 𝐶 = 1 ) ∧ 𝑙 ∈ 𝐴 ) ∧ 𝐶 = 0 ) → 𝑙 ∈ 𝐴 )
29		simpr	⊢ ( ( ( ( 𝜑 ∧ ¬ ∀ 𝑙 ∈ 𝐴 𝐶 = 1 ) ∧ 𝑙 ∈ 𝐴 ) ∧ 𝐶 = 0 ) → 𝐶 = 0 )
30	1 20 27 28 29	fprodeq02	⊢ ( ( ( ( 𝜑 ∧ ¬ ∀ 𝑙 ∈ 𝐴 𝐶 = 1 ) ∧ 𝑙 ∈ 𝐴 ) ∧ 𝐶 = 0 ) → ∏ 𝑘 ∈ 𝐴 𝐵 = 0 )
31		rexnal	⊢ ( ∃ 𝑙 ∈ 𝐴 ¬ 𝐶 = 1 ↔ ¬ ∀ 𝑙 ∈ 𝐴 𝐶 = 1 )
32	31	biimpri	⊢ ( ¬ ∀ 𝑙 ∈ 𝐴 𝐶 = 1 → ∃ 𝑙 ∈ 𝐴 ¬ 𝐶 = 1 )
33	32	adantl	⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑙 ∈ 𝐴 𝐶 = 1 ) → ∃ 𝑙 ∈ 𝐴 ¬ 𝐶 = 1 )
34	3	ralrimiva	⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 𝐵 ∈ { 0 , 1 } )
35	1	eleq1d	⊢ ( 𝑘 = 𝑙 → ( 𝐵 ∈ { 0 , 1 } ↔ 𝐶 ∈ { 0 , 1 } ) )
36	35	cbvralvw	⊢ ( ∀ 𝑘 ∈ 𝐴 𝐵 ∈ { 0 , 1 } ↔ ∀ 𝑙 ∈ 𝐴 𝐶 ∈ { 0 , 1 } )
37	34 36	sylib	⊢ ( 𝜑 → ∀ 𝑙 ∈ 𝐴 𝐶 ∈ { 0 , 1 } )
38	37	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑙 ∈ 𝐴 ) → 𝐶 ∈ { 0 , 1 } )
39		c0ex	⊢ 0 ∈ V
40		1ex	⊢ 1 ∈ V
41	39 40	elpr2	⊢ ( 𝐶 ∈ { 0 , 1 } ↔ ( 𝐶 = 0 ∨ 𝐶 = 1 ) )
42	38 41	sylib	⊢ ( ( 𝜑 ∧ 𝑙 ∈ 𝐴 ) → ( 𝐶 = 0 ∨ 𝐶 = 1 ) )
43	42	orcomd	⊢ ( ( 𝜑 ∧ 𝑙 ∈ 𝐴 ) → ( 𝐶 = 1 ∨ 𝐶 = 0 ) )
44	43	ord	⊢ ( ( 𝜑 ∧ 𝑙 ∈ 𝐴 ) → ( ¬ 𝐶 = 1 → 𝐶 = 0 ) )
45	44	reximdva	⊢ ( 𝜑 → ( ∃ 𝑙 ∈ 𝐴 ¬ 𝐶 = 1 → ∃ 𝑙 ∈ 𝐴 𝐶 = 0 ) )
46	45	adantr	⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑙 ∈ 𝐴 𝐶 = 1 ) → ( ∃ 𝑙 ∈ 𝐴 ¬ 𝐶 = 1 → ∃ 𝑙 ∈ 𝐴 𝐶 = 0 ) )
47	33 46	mpd	⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑙 ∈ 𝐴 𝐶 = 1 ) → ∃ 𝑙 ∈ 𝐴 𝐶 = 0 )
48	17 18 30 47	r19.29af2	⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑙 ∈ 𝐴 𝐶 = 1 ) → ∏ 𝑘 ∈ 𝐴 𝐵 = 0 )
49	48	eqcomd	⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑙 ∈ 𝐴 𝐶 = 1 ) → 0 = ∏ 𝑘 ∈ 𝐴 𝐵 )
50	13 49	ifeqda	⊢ ( 𝜑 → if ( ∀ 𝑙 ∈ 𝐴 𝐶 = 1 , 1 , 0 ) = ∏ 𝑘 ∈ 𝐴 𝐵 )
51	50	eqcomd	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐴 𝐵 = if ( ∀ 𝑙 ∈ 𝐴 𝐶 = 1 , 1 , 0 ) )