Metamath Proof Explorer

Theorem prod1

Description: Any product of one over a valid set is one. (Contributed by Scott Fenton, 7-Dec-2017)

Ref Expression
Assertion prod1 
|- ( ( A C_ ( ZZ>= ` M ) \/ A e. Fin ) -> prod_ k e. A 1 = 1 )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( ZZ>= ` M ) = ( ZZ>= ` M )
2 simpr 
 |-  ( ( A C_ ( ZZ>= ` M ) /\ M e. ZZ ) -> M e. ZZ )
3 ax-1ne0 
 |-  1 =/= 0
4 3 a1i 
 |-  ( ( A C_ ( ZZ>= ` M ) /\ M e. ZZ ) -> 1 =/= 0 )
5 1 prodfclim1 
 |-  ( M e. ZZ -> seq M ( x. , ( ( ZZ>= ` M ) X. { 1 } ) ) ~~> 1 )
6 5 adantl 
 |-  ( ( A C_ ( ZZ>= ` M ) /\ M e. ZZ ) -> seq M ( x. , ( ( ZZ>= ` M ) X. { 1 } ) ) ~~> 1 )
7 simpl 
 |-  ( ( A C_ ( ZZ>= ` M ) /\ M e. ZZ ) -> A C_ ( ZZ>= ` M ) )
8 1ex 
 |-  1 e. _V
9 8 fvconst2 
 |-  ( k e. ( ZZ>= ` M ) -> ( ( ( ZZ>= ` M ) X. { 1 } ) ` k ) = 1 )
10 ifid 
 |-  if ( k e. A , 1 , 1 ) = 1
11 9 10 eqtr4di 
 |-  ( k e. ( ZZ>= ` M ) -> ( ( ( ZZ>= ` M ) X. { 1 } ) ` k ) = if ( k e. A , 1 , 1 ) )
12 11 adantl 
 |-  ( ( ( A C_ ( ZZ>= ` M ) /\ M e. ZZ ) /\ k e. ( ZZ>= ` M ) ) -> ( ( ( ZZ>= ` M ) X. { 1 } ) ` k ) = if ( k e. A , 1 , 1 ) )
13 1cnd 
 |-  ( ( ( A C_ ( ZZ>= ` M ) /\ M e. ZZ ) /\ k e. A ) -> 1 e. CC )
14 1 2 4 6 7 12 13 zprodn0 
 |-  ( ( A C_ ( ZZ>= ` M ) /\ M e. ZZ ) -> prod_ k e. A 1 = 1 )
15 uzf 
 |-  ZZ>= : ZZ --> ~P ZZ
16 15 fdmi 
 |-  dom ZZ>= = ZZ
17 16 eleq2i 
 |-  ( M e. dom ZZ>= <-> M e. ZZ )
18 ndmfv 
 |-  ( -. M e. dom ZZ>= -> ( ZZ>= ` M ) = (/) )
19 17 18 sylnbir 
 |-  ( -. M e. ZZ -> ( ZZ>= ` M ) = (/) )
20 19 sseq2d 
 |-  ( -. M e. ZZ -> ( A C_ ( ZZ>= ` M ) <-> A C_ (/) ) )
21 20 biimpac 
 |-  ( ( A C_ ( ZZ>= ` M ) /\ -. M e. ZZ ) -> A C_ (/) )
22 ss0 
 |-  ( A C_ (/) -> A = (/) )
23 prodeq1 
 |-  ( A = (/) -> prod_ k e. A 1 = prod_ k e. (/) 1 )
24 prod0 
 |-  prod_ k e. (/) 1 = 1
25 23 24 eqtrdi 
 |-  ( A = (/) -> prod_ k e. A 1 = 1 )
26 21 22 25 3syl 
 |-  ( ( A C_ ( ZZ>= ` M ) /\ -. M e. ZZ ) -> prod_ k e. A 1 = 1 )
27 14 26 pm2.61dan 
 |-  ( A C_ ( ZZ>= ` M ) -> prod_ k e. A 1 = 1 )
28 fz1f1o 
 |-  ( A e. Fin -> ( A = (/) \/ ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) )
29 eqidd 
 |-  ( k = ( f ` j ) -> 1 = 1 )
30 simpl 
 |-  ( ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> ( # ` A ) e. NN )
31 simpr 
 |-  ( ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> f : ( 1 ... ( # ` A ) ) -1-1-onto-> A )
32 1cnd 
 |-  ( ( ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) /\ k e. A ) -> 1 e. CC )
33 elfznn 
 |-  ( j e. ( 1 ... ( # ` A ) ) -> j e. NN )
34 8 fvconst2 
 |-  ( j e. NN -> ( ( NN X. { 1 } ) ` j ) = 1 )
35 33 34 syl 
 |-  ( j e. ( 1 ... ( # ` A ) ) -> ( ( NN X. { 1 } ) ` j ) = 1 )
36 35 adantl 
 |-  ( ( ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) /\ j e. ( 1 ... ( # ` A ) ) ) -> ( ( NN X. { 1 } ) ` j ) = 1 )
37 29 30 31 32 36 fprod 
 |-  ( ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> prod_ k e. A 1 = ( seq 1 ( x. , ( NN X. { 1 } ) ) ` ( # ` A ) ) )
38 nnuz 
 |-  NN = ( ZZ>= ` 1 )
39 38 prodf1 
 |-  ( ( # ` A ) e. NN -> ( seq 1 ( x. , ( NN X. { 1 } ) ) ` ( # ` A ) ) = 1 )
40 39 adantr 
 |-  ( ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> ( seq 1 ( x. , ( NN X. { 1 } ) ) ` ( # ` A ) ) = 1 )
41 37 40 eqtrd 
 |-  ( ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> prod_ k e. A 1 = 1 )
42 41 ex 
 |-  ( ( # ` A ) e. NN -> ( f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> prod_ k e. A 1 = 1 ) )
43 42 exlimdv 
 |-  ( ( # ` A ) e. NN -> ( E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> prod_ k e. A 1 = 1 ) )
44 43 imp 
 |-  ( ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> prod_ k e. A 1 = 1 )
45 25 44 jaoi 
 |-  ( ( A = (/) \/ ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> prod_ k e. A 1 = 1 )
46 28 45 syl 
 |-  ( A e. Fin -> prod_ k e. A 1 = 1 )
47 27 46 jaoi 
 |-  ( ( A C_ ( ZZ>= ` M ) \/ A e. Fin ) -> prod_ k e. A 1 = 1 )