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 syl6eqr
 |-  ( 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 syl6eq
 |-  ( 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 )