Metamath Proof Explorer

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