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 
|- ( k = l -> B = C )
fprodex01.a 
|- ( ph -> A e. Fin )
fprodex01.b 
|- ( ( ph /\ k e. A ) -> B e. { 0 , 1 } )
Assertion fprodex01 
|- ( ph -> prod_ k e. A B = if ( A. l e. A C = 1 , 1 , 0 ) )

Proof

Step Hyp Ref Expression
1 fprodex01.1 
 |-  ( k = l -> B = C )
2 fprodex01.a 
 |-  ( ph -> A e. Fin )
3 fprodex01.b 
 |-  ( ( ph /\ k e. A ) -> B e. { 0 , 1 } )
4 1 eqeq1d 
 |-  ( k = l -> ( B = 1 <-> C = 1 ) )
5 4 cbvralvw 
 |-  ( A. k e. A B = 1 <-> A. l e. A C = 1 )
6 5 bilanri 
 |-  ( ( ph /\ A. l e. A C = 1 ) -> A. k e. A B = 1 )
7 6 prodeq2d 
 |-  ( ( ph /\ A. l e. A C = 1 ) -> prod_ k e. A B = prod_ k e. A 1 )
8 prod1 
 |-  ( ( A C_ ( ZZ>= ` 0 ) \/ A e. Fin ) -> prod_ k e. A 1 = 1 )
9 8 olcs 
 |-  ( A e. Fin -> prod_ k e. A 1 = 1 )
10 2 9 syl 
 |-  ( ph -> prod_ k e. A 1 = 1 )
11 10 adantr 
 |-  ( ( ph /\ A. l e. A C = 1 ) -> prod_ k e. A 1 = 1 )
12 7 11 eqtr2d 
 |-  ( ( ph /\ A. l e. A C = 1 ) -> 1 = prod_ k e. A B )
13 nfv 
 |-  F/ l ph
14 nfra1 
 |-  F/ l A. l e. A C = 1
15 14 nfn 
 |-  F/ l -. A. l e. A C = 1
16 13 15 nfan 
 |-  F/ l ( ph /\ -. A. l e. A C = 1 )
17 nfv 
 |-  F/ l prod_ k e. A B = 0
18 2 adantr 
 |-  ( ( ph /\ -. A. l e. A C = 1 ) -> A e. Fin )
19 18 ad2antrr 
 |-  ( ( ( ( ph /\ -. A. l e. A C = 1 ) /\ l e. A ) /\ C = 0 ) -> A e. Fin )
20 pr01ssre 
 |-  { 0 , 1 } C_ RR
21 ax-resscn 
 |-  RR C_ CC
22 20 21 sstri 
 |-  { 0 , 1 } C_ CC
23 22 3 sselid 
 |-  ( ( ph /\ k e. A ) -> B e. CC )
24 23 adantlr 
 |-  ( ( ( ph /\ -. A. l e. A C = 1 ) /\ k e. A ) -> B e. CC )
25 24 adantlr 
 |-  ( ( ( ( ph /\ -. A. l e. A C = 1 ) /\ l e. A ) /\ k e. A ) -> B e. CC )
26 25 adantlr 
 |-  ( ( ( ( ( ph /\ -. A. l e. A C = 1 ) /\ l e. A ) /\ C = 0 ) /\ k e. A ) -> B e. CC )
27 simplr 
 |-  ( ( ( ( ph /\ -. A. l e. A C = 1 ) /\ l e. A ) /\ C = 0 ) -> l e. A )
28 simpr 
 |-  ( ( ( ( ph /\ -. A. l e. A C = 1 ) /\ l e. A ) /\ C = 0 ) -> C = 0 )
29 1 19 26 27 28 fprodeq02 
 |-  ( ( ( ( ph /\ -. A. l e. A C = 1 ) /\ l e. A ) /\ C = 0 ) -> prod_ k e. A B = 0 )
30 rexnal 
 |-  ( E. l e. A -. C = 1 <-> -. A. l e. A C = 1 )
31 30 bilanri 
 |-  ( ( ph /\ -. A. l e. A C = 1 ) -> E. l e. A -. C = 1 )
32 3 ralrimiva 
 |-  ( ph -> A. k e. A B e. { 0 , 1 } )
33 1 eleq1d 
 |-  ( k = l -> ( B e. { 0 , 1 } <-> C e. { 0 , 1 } ) )
34 33 cbvralvw 
 |-  ( A. k e. A B e. { 0 , 1 } <-> A. l e. A C e. { 0 , 1 } )
35 32 34 sylib 
 |-  ( ph -> A. l e. A C e. { 0 , 1 } )
36 35 r19.21bi 
 |-  ( ( ph /\ l e. A ) -> C e. { 0 , 1 } )
37 c0ex 
 |-  0 e. _V
38 1ex 
 |-  1 e. _V
39 37 38 elpr2 
 |-  ( C e. { 0 , 1 } <-> ( C = 0 \/ C = 1 ) )
40 36 39 sylib 
 |-  ( ( ph /\ l e. A ) -> ( C = 0 \/ C = 1 ) )
41 40 orcomd 
 |-  ( ( ph /\ l e. A ) -> ( C = 1 \/ C = 0 ) )
42 41 ord 
 |-  ( ( ph /\ l e. A ) -> ( -. C = 1 -> C = 0 ) )
43 42 reximdva 
 |-  ( ph -> ( E. l e. A -. C = 1 -> E. l e. A C = 0 ) )
44 43 adantr 
 |-  ( ( ph /\ -. A. l e. A C = 1 ) -> ( E. l e. A -. C = 1 -> E. l e. A C = 0 ) )
45 31 44 mpd 
 |-  ( ( ph /\ -. A. l e. A C = 1 ) -> E. l e. A C = 0 )
46 16 17 29 45 r19.29af2 
 |-  ( ( ph /\ -. A. l e. A C = 1 ) -> prod_ k e. A B = 0 )
47 46 eqcomd 
 |-  ( ( ph /\ -. A. l e. A C = 1 ) -> 0 = prod_ k e. A B )
48 12 47 ifeqda 
 |-  ( ph -> if ( A. l e. A C = 1 , 1 , 0 ) = prod_ k e. A B )
49 48 eqcomd 
 |-  ( ph -> prod_ k e. A B = if ( A. l e. A C = 1 , 1 , 0 ) )