Definition df-proddc 12111

Description: Define the product of a series with an index set of integers A. This definition takes most of the aspects of df-sumdc 11914 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.) (Revised by Jim Kingdon, 21-Mar-2024.)

Assertion

Ref

Expression

df-proddc

|- prod_ k e. A B = ( iota x ( E. m e. ZZ ( ( A C_ ( ZZ>= ` m ) /\ A. j e. ( ZZ>= ` m )DECID j e. A ) /\ ( 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 |-> if ( n <_ m , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) ) )

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

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

Detailed syntax breakdown of Definition df-proddc

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3		vk	. . 3 setvar k
4	1, 2, 3	cprod 12110	. 2 class prod_ k e. A B
5		vm	. . . . . . . . . 10 setvar m
6	5	cv 1396	. . . . . . . . 9 class m
7		cuz 9754	. . . . . . . . 9 class ZZ>=
8	6, 7	cfv 5326	. . . . . . . 8 class ( ZZ>= ` m )
9	1, 8	wss 3200	. . . . . . 7 wff A C_ ( ZZ>= ` m )
10		vj	. . . . . . . . . . 11 setvar j
11	10	cv 1396	. . . . . . . . . 10 class j
12	11, 1	wcel 2202	. . . . . . . . 9 wff j e. A
13	12	wdc 841	. . . . . . . 8 wff DECID j e. A
14	13, 10, 8	wral 2510	. . . . . . 7 wff A. j e. ( ZZ>= ` m )DECID j e. A
15	9, 14	wa 104	. . . . . 6 wff ( A C_ ( ZZ>= ` m ) /\ A. j e. ( ZZ>= ` m )DECID j e. A )
16		vy	. . . . . . . . . . . 12 setvar y
17	16	cv 1396	. . . . . . . . . . 11 class y
18		cc0 8031	. . . . . . . . . . 11 class 0
19		cap 8760	. . . . . . . . . . 11 class #
20	17, 18, 19	wbr 4088	. . . . . . . . . 10 wff y # 0
21		cmul 8036	. . . . . . . . . . . 12 class x.
22		cz 9478	. . . . . . . . . . . . 13 class ZZ
23	3	cv 1396	. . . . . . . . . . . . . . 15 class k
24	23, 1	wcel 2202	. . . . . . . . . . . . . 14 wff k e. A
25		c1 8032	. . . . . . . . . . . . . 14 class 1
26	24, 2, 25	cif 3605	. . . . . . . . . . . . 13 class if ( k e. A , B , 1 )
27	3, 22, 26	cmpt 4150	. . . . . . . . . . . 12 class ( k e. ZZ |-> if ( k e. A , B , 1 ) )
28		vn	. . . . . . . . . . . . 13 setvar n
29	28	cv 1396	. . . . . . . . . . . 12 class n
30	21, 27, 29	cseq 10708	. . . . . . . . . . 11 class seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) )
31		cli 11838	. . . . . . . . . . 11 class ~~>
32	30, 17, 31	wbr 4088	. . . . . . . . . 10 wff seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y
33	20, 32	wa 104	. . . . . . . . 9 wff ( y # 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y )
34	33, 16	wex 1540	. . . . . . . 8 wff E. y ( y # 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y )
35	34, 28, 8	wrex 2511	. . . . . . 7 wff E. n e. ( ZZ>= ` m ) E. y ( y # 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y )
36	21, 27, 6	cseq 10708	. . . . . . . 8 class seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) )
37		vx	. . . . . . . . 9 setvar x
38	37	cv 1396	. . . . . . . 8 class x
39	36, 38, 31	wbr 4088	. . . . . . 7 wff seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x
40	35, 39	wa 104	. . . . . 6 wff ( 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 )
41	15, 40	wa 104	. . . . 5 wff ( ( A C_ ( ZZ>= ` m ) /\ A. j e. ( ZZ>= ` m )DECID j e. A ) /\ ( 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 ) )
42	41, 5, 22	wrex 2511	. . . 4 wff E. m e. ZZ ( ( A C_ ( ZZ>= ` m ) /\ A. j e. ( ZZ>= ` m )DECID j e. A ) /\ ( 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 ) )
43		cfz 10242	. . . . . . . . 9 class ...
44	25, 6, 43	co 6017	. . . . . . . 8 class ( 1 ... m )
45		vf	. . . . . . . . 9 setvar f
46	45	cv 1396	. . . . . . . 8 class f
47	44, 1, 46	wf1o 5325	. . . . . . 7 wff f : ( 1 ... m ) -1-1-onto-> A
48		cn 9142	. . . . . . . . . . 11 class NN
49		cle 8214	. . . . . . . . . . . . 13 class <_
50	29, 6, 49	wbr 4088	. . . . . . . . . . . 12 wff n <_ m
51	29, 46	cfv 5326	. . . . . . . . . . . . 13 class ( f ` n )
52	3, 51, 2	csb 3127	. . . . . . . . . . . 12 class [_ ( f ` n ) / k ]_ B
53	50, 52, 25	cif 3605	. . . . . . . . . . 11 class if ( n <_ m , [_ ( f ` n ) / k ]_ B , 1 )
54	28, 48, 53	cmpt 4150	. . . . . . . . . 10 class ( n e. NN |-> if ( n <_ m , [_ ( f ` n ) / k ]_ B , 1 ) )
55	21, 54, 25	cseq 10708	. . . . . . . . 9 class seq 1 ( x. , ( n e. NN |-> if ( n <_ m , [_ ( f ` n ) / k ]_ B , 1 ) ) )
56	6, 55	cfv 5326	. . . . . . . 8 class ( seq 1 ( x. , ( n e. NN |-> if ( n <_ m , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m )
57	38, 56	wceq 1397	. . . . . . 7 wff x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ m , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m )
58	47, 57	wa 104	. . . . . 6 wff ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ m , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) )
59	58, 45	wex 1540	. . . . 5 wff E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ m , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) )
60	59, 5, 48	wrex 2511	. . . 4 wff E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ m , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) )
61	42, 60	wo 715	. . 3 wff ( E. m e. ZZ ( ( A C_ ( ZZ>= ` m ) /\ A. j e. ( ZZ>= ` m )DECID j e. A ) /\ ( 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 |-> if ( n <_ m , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) )
62	61, 37	cio 5284	. 2 class ( iota x ( E. m e. ZZ ( ( A C_ ( ZZ>= ` m ) /\ A. j e. ( ZZ>= ` m )DECID j e. A ) /\ ( 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 |-> if ( n <_ m , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) ) )
63	4, 62	wceq 1397	1 wff prod_ k e. A B = ( iota x ( E. m e. ZZ ( ( A C_ ( ZZ>= ` m ) /\ A. j e. ( ZZ>= ` m )DECID j e. A ) /\ ( 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 |-> if ( n <_ m , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) ) )

This definition is referenced by:  prodeq1f  12112  nfcprod1  12114  nfcprod  12115  prodeq2w  12116  prodeq2  12117  cbvprod  12118  zproddc  12139  fprodseq  12143