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 )`
` |-  ( ( 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 ) )`
` |-  ( ( ( 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 )`
` |-  ( ( ( ( # ` 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 )`
` |-  ( ( ( # ` 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 )`