Definition df-prod 14636

Description: Define the product of a series with an index set of integers A. This definition takes most of the aspects of df-sum 14417 and adapts them for multiplication instead of addition. However, we insist that in the infinite case, there is a nonzero tail of the sequence. This ensures that the convergence criteria match those of infinite sums. (Contributed by Scott Fenton, 4-Dec-2017.)

Assertion

Ref	Expression
df-prod	|- prod_ k e. A B = ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) )

Distinct variable groups:   f, k, m, n, x, y   A, f, m, n, x, y   B, f, m, n, x, y

Allowed substitution hints:   A( k)   B( k)

Detailed syntax breakdown of Definition df-prod

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3		vk	. . 3 setvar k
4	1, 2, 3	cprod 14635	. 2 class prod_ k e. A B
5		vm	. . . . . . . . 9 setvar m
6	5	cv 1482	. . . . . . . 8 class m
7		cuz 11687	. . . . . . . 8 class ZZ>=
8	6, 7	cfv 5888	. . . . . . 7 class ( ZZ>= ` m )
9	1, 8	wss 3574	. . . . . 6 wff A C_ ( ZZ>= ` m )
10		vy	. . . . . . . . . . 11 setvar y
11	10	cv 1482	. . . . . . . . . 10 class y
12		cc0 9936	. . . . . . . . . 10 class 0
13	11, 12	wne 2794	. . . . . . . . 9 wff y =/= 0
14		cmul 9941	. . . . . . . . . . 11 class x.
15		cz 11377	. . . . . . . . . . . 12 class ZZ
16	3	cv 1482	. . . . . . . . . . . . . 14 class k
17	16, 1	wcel 1990	. . . . . . . . . . . . 13 wff k e. A
18		c1 9937	. . . . . . . . . . . . 13 class 1
19	17, 2, 18	cif 4086	. . . . . . . . . . . 12 class if ( k e. A , B , 1 )
20	3, 15, 19	cmpt 4729	. . . . . . . . . . 11 class ( k e. ZZ |-> if ( k e. A , B , 1 ) )
21		vn	. . . . . . . . . . . 12 setvar n
22	21	cv 1482	. . . . . . . . . . 11 class n
23	14, 20, 22	cseq 12801	. . . . . . . . . 10 class seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) )
24		cli 14215	. . . . . . . . . 10 class ~~>
25	23, 11, 24	wbr 4653	. . . . . . . . 9 wff seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y
26	13, 25	wa 384	. . . . . . . 8 wff ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y )
27	26, 10	wex 1704	. . . . . . 7 wff E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y )
28	27, 21, 8	wrex 2913	. . . . . 6 wff E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y )
29	14, 20, 6	cseq 12801	. . . . . . 7 class seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) )
30		vx	. . . . . . . 8 setvar x
31	30	cv 1482	. . . . . . 7 class x
32	29, 31, 24	wbr 4653	. . . . . 6 wff seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x
33	9, 28, 32	w3a 1037	. . . . 5 wff ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x )
34	33, 5, 15	wrex 2913	. . . 4 wff E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x )
35		cfz 12326	. . . . . . . . 9 class ...
36	18, 6, 35	co 6650	. . . . . . . 8 class ( 1 ... m )
37		vf	. . . . . . . . 9 setvar f
38	37	cv 1482	. . . . . . . 8 class f
39	36, 1, 38	wf1o 5887	. . . . . . 7 wff f : ( 1 ... m ) -1-1-onto-> A
40		cn 11020	. . . . . . . . . . 11 class NN
41	22, 38	cfv 5888	. . . . . . . . . . . 12 class ( f ` n )
42	3, 41, 2	csb 3533	. . . . . . . . . . 11 class [_ ( f ` n ) / k ]_ B
43	21, 40, 42	cmpt 4729	. . . . . . . . . 10 class ( n e. NN |-> [_ ( f ` n ) / k ]_ B )
44	14, 43, 18	cseq 12801	. . . . . . . . 9 class seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) )
45	6, 44	cfv 5888	. . . . . . . 8 class ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m )
46	31, 45	wceq 1483	. . . . . . 7 wff x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m )
47	39, 46	wa 384	. . . . . 6 wff ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) )
48	47, 37	wex 1704	. . . . 5 wff E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) )
49	48, 5, 40	wrex 2913	. . . 4 wff E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) )
50	34, 49	wo 383	. . 3 wff ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) )
51	50, 30	cio 5849	. 2 class ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) )
52	4, 51	wceq 1483	1 wff prod_ k e. A B = ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) )

This definition is referenced by:  prodex  14637  prodeq1f  14638  nfcprod1  14640  nfcprod  14641  prodeq2w  14642  prodeq2ii  14643  cbvprod  14645  zprod  14667  fprod  14671