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