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

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 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 sselid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
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 ) )