Metamath Proof Explorer


Definition df-prod

Description: Define the product of a series with an index set of integers A . This definition takes most of the aspects of df-sum 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)

Ref Expression
Assertion df-prod โˆ ๐‘˜ โˆˆ ๐ด ๐ต = ( โ„ฉ ๐‘ฅ ( โˆƒ ๐‘š โˆˆ โ„ค ( ๐ด โІ ( โ„คโ‰ฅ โ€˜ ๐‘š ) โˆง โˆƒ ๐‘› โˆˆ ( โ„คโ‰ฅ โ€˜ ๐‘š ) โˆƒ ๐‘ฆ ( ๐‘ฆ โ‰  0 โˆง seq ๐‘› ( ยท , ( ๐‘˜ โˆˆ โ„ค โ†ฆ if ( ๐‘˜ โˆˆ ๐ด , ๐ต , 1 ) ) ) โ‡ ๐‘ฆ ) โˆง seq ๐‘š ( ยท , ( ๐‘˜ โˆˆ โ„ค โ†ฆ if ( ๐‘˜ โˆˆ ๐ด , ๐ต , 1 ) ) ) โ‡ ๐‘ฅ ) โˆจ โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘“ ( ๐‘“ : ( 1 ... ๐‘š ) โ€“1-1-ontoโ†’ ๐ด โˆง ๐‘ฅ = ( seq 1 ( ยท , ( ๐‘› โˆˆ โ„• โ†ฆ โฆ‹ ( ๐‘“ โ€˜ ๐‘› ) / ๐‘˜ โฆŒ ๐ต ) ) โ€˜ ๐‘š ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 vk โŠข ๐‘˜
1 cA โŠข ๐ด
2 cB โŠข ๐ต
3 1 2 0 cprod โŠข โˆ ๐‘˜ โˆˆ ๐ด ๐ต
4 vx โŠข ๐‘ฅ
5 vm โŠข ๐‘š
6 cz โŠข โ„ค
7 cuz โŠข โ„คโ‰ฅ
8 5 cv โŠข ๐‘š
9 8 7 cfv โŠข ( โ„คโ‰ฅ โ€˜ ๐‘š )
10 1 9 wss โŠข ๐ด โІ ( โ„คโ‰ฅ โ€˜ ๐‘š )
11 vn โŠข ๐‘›
12 vy โŠข ๐‘ฆ
13 12 cv โŠข ๐‘ฆ
14 cc0 โŠข 0
15 13 14 wne โŠข ๐‘ฆ โ‰  0
16 11 cv โŠข ๐‘›
17 cmul โŠข ยท
18 0 cv โŠข ๐‘˜
19 18 1 wcel โŠข ๐‘˜ โˆˆ ๐ด
20 c1 โŠข 1
21 19 2 20 cif โŠข if ( ๐‘˜ โˆˆ ๐ด , ๐ต , 1 )
22 0 6 21 cmpt โŠข ( ๐‘˜ โˆˆ โ„ค โ†ฆ if ( ๐‘˜ โˆˆ ๐ด , ๐ต , 1 ) )
23 17 22 16 cseq โŠข seq ๐‘› ( ยท , ( ๐‘˜ โˆˆ โ„ค โ†ฆ if ( ๐‘˜ โˆˆ ๐ด , ๐ต , 1 ) ) )
24 cli โŠข โ‡
25 23 13 24 wbr โŠข seq ๐‘› ( ยท , ( ๐‘˜ โˆˆ โ„ค โ†ฆ if ( ๐‘˜ โˆˆ ๐ด , ๐ต , 1 ) ) ) โ‡ ๐‘ฆ
26 15 25 wa โŠข ( ๐‘ฆ โ‰  0 โˆง seq ๐‘› ( ยท , ( ๐‘˜ โˆˆ โ„ค โ†ฆ if ( ๐‘˜ โˆˆ ๐ด , ๐ต , 1 ) ) ) โ‡ ๐‘ฆ )
27 26 12 wex โŠข โˆƒ ๐‘ฆ ( ๐‘ฆ โ‰  0 โˆง seq ๐‘› ( ยท , ( ๐‘˜ โˆˆ โ„ค โ†ฆ if ( ๐‘˜ โˆˆ ๐ด , ๐ต , 1 ) ) ) โ‡ ๐‘ฆ )
28 27 11 9 wrex โŠข โˆƒ ๐‘› โˆˆ ( โ„คโ‰ฅ โ€˜ ๐‘š ) โˆƒ ๐‘ฆ ( ๐‘ฆ โ‰  0 โˆง seq ๐‘› ( ยท , ( ๐‘˜ โˆˆ โ„ค โ†ฆ if ( ๐‘˜ โˆˆ ๐ด , ๐ต , 1 ) ) ) โ‡ ๐‘ฆ )
29 17 22 8 cseq โŠข seq ๐‘š ( ยท , ( ๐‘˜ โˆˆ โ„ค โ†ฆ if ( ๐‘˜ โˆˆ ๐ด , ๐ต , 1 ) ) )
30 4 cv โŠข ๐‘ฅ
31 29 30 24 wbr โŠข seq ๐‘š ( ยท , ( ๐‘˜ โˆˆ โ„ค โ†ฆ if ( ๐‘˜ โˆˆ ๐ด , ๐ต , 1 ) ) ) โ‡ ๐‘ฅ
32 10 28 31 w3a โŠข ( ๐ด โІ ( โ„คโ‰ฅ โ€˜ ๐‘š ) โˆง โˆƒ ๐‘› โˆˆ ( โ„คโ‰ฅ โ€˜ ๐‘š ) โˆƒ ๐‘ฆ ( ๐‘ฆ โ‰  0 โˆง seq ๐‘› ( ยท , ( ๐‘˜ โˆˆ โ„ค โ†ฆ if ( ๐‘˜ โˆˆ ๐ด , ๐ต , 1 ) ) ) โ‡ ๐‘ฆ ) โˆง seq ๐‘š ( ยท , ( ๐‘˜ โˆˆ โ„ค โ†ฆ if ( ๐‘˜ โˆˆ ๐ด , ๐ต , 1 ) ) ) โ‡ ๐‘ฅ )
33 32 5 6 wrex โŠข โˆƒ ๐‘š โˆˆ โ„ค ( ๐ด โІ ( โ„คโ‰ฅ โ€˜ ๐‘š ) โˆง โˆƒ ๐‘› โˆˆ ( โ„คโ‰ฅ โ€˜ ๐‘š ) โˆƒ ๐‘ฆ ( ๐‘ฆ โ‰  0 โˆง seq ๐‘› ( ยท , ( ๐‘˜ โˆˆ โ„ค โ†ฆ if ( ๐‘˜ โˆˆ ๐ด , ๐ต , 1 ) ) ) โ‡ ๐‘ฆ ) โˆง seq ๐‘š ( ยท , ( ๐‘˜ โˆˆ โ„ค โ†ฆ if ( ๐‘˜ โˆˆ ๐ด , ๐ต , 1 ) ) ) โ‡ ๐‘ฅ )
34 cn โŠข โ„•
35 vf โŠข ๐‘“
36 35 cv โŠข ๐‘“
37 cfz โŠข ...
38 20 8 37 co โŠข ( 1 ... ๐‘š )
39 38 1 36 wf1o โŠข ๐‘“ : ( 1 ... ๐‘š ) โ€“1-1-ontoโ†’ ๐ด
40 16 36 cfv โŠข ( ๐‘“ โ€˜ ๐‘› )
41 0 40 2 csb โŠข โฆ‹ ( ๐‘“ โ€˜ ๐‘› ) / ๐‘˜ โฆŒ ๐ต
42 11 34 41 cmpt โŠข ( ๐‘› โˆˆ โ„• โ†ฆ โฆ‹ ( ๐‘“ โ€˜ ๐‘› ) / ๐‘˜ โฆŒ ๐ต )
43 17 42 20 cseq โŠข seq 1 ( ยท , ( ๐‘› โˆˆ โ„• โ†ฆ โฆ‹ ( ๐‘“ โ€˜ ๐‘› ) / ๐‘˜ โฆŒ ๐ต ) )
44 8 43 cfv โŠข ( seq 1 ( ยท , ( ๐‘› โˆˆ โ„• โ†ฆ โฆ‹ ( ๐‘“ โ€˜ ๐‘› ) / ๐‘˜ โฆŒ ๐ต ) ) โ€˜ ๐‘š )
45 30 44 wceq โŠข ๐‘ฅ = ( seq 1 ( ยท , ( ๐‘› โˆˆ โ„• โ†ฆ โฆ‹ ( ๐‘“ โ€˜ ๐‘› ) / ๐‘˜ โฆŒ ๐ต ) ) โ€˜ ๐‘š )
46 39 45 wa โŠข ( ๐‘“ : ( 1 ... ๐‘š ) โ€“1-1-ontoโ†’ ๐ด โˆง ๐‘ฅ = ( seq 1 ( ยท , ( ๐‘› โˆˆ โ„• โ†ฆ โฆ‹ ( ๐‘“ โ€˜ ๐‘› ) / ๐‘˜ โฆŒ ๐ต ) ) โ€˜ ๐‘š ) )
47 46 35 wex โŠข โˆƒ ๐‘“ ( ๐‘“ : ( 1 ... ๐‘š ) โ€“1-1-ontoโ†’ ๐ด โˆง ๐‘ฅ = ( seq 1 ( ยท , ( ๐‘› โˆˆ โ„• โ†ฆ โฆ‹ ( ๐‘“ โ€˜ ๐‘› ) / ๐‘˜ โฆŒ ๐ต ) ) โ€˜ ๐‘š ) )
48 47 5 34 wrex โŠข โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘“ ( ๐‘“ : ( 1 ... ๐‘š ) โ€“1-1-ontoโ†’ ๐ด โˆง ๐‘ฅ = ( seq 1 ( ยท , ( ๐‘› โˆˆ โ„• โ†ฆ โฆ‹ ( ๐‘“ โ€˜ ๐‘› ) / ๐‘˜ โฆŒ ๐ต ) ) โ€˜ ๐‘š ) )
49 33 48 wo โŠข ( โˆƒ ๐‘š โˆˆ โ„ค ( ๐ด โІ ( โ„คโ‰ฅ โ€˜ ๐‘š ) โˆง โˆƒ ๐‘› โˆˆ ( โ„คโ‰ฅ โ€˜ ๐‘š ) โˆƒ ๐‘ฆ ( ๐‘ฆ โ‰  0 โˆง seq ๐‘› ( ยท , ( ๐‘˜ โˆˆ โ„ค โ†ฆ if ( ๐‘˜ โˆˆ ๐ด , ๐ต , 1 ) ) ) โ‡ ๐‘ฆ ) โˆง seq ๐‘š ( ยท , ( ๐‘˜ โˆˆ โ„ค โ†ฆ if ( ๐‘˜ โˆˆ ๐ด , ๐ต , 1 ) ) ) โ‡ ๐‘ฅ ) โˆจ โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘“ ( ๐‘“ : ( 1 ... ๐‘š ) โ€“1-1-ontoโ†’ ๐ด โˆง ๐‘ฅ = ( seq 1 ( ยท , ( ๐‘› โˆˆ โ„• โ†ฆ โฆ‹ ( ๐‘“ โ€˜ ๐‘› ) / ๐‘˜ โฆŒ ๐ต ) ) โ€˜ ๐‘š ) ) )
50 49 4 cio โŠข ( โ„ฉ ๐‘ฅ ( โˆƒ ๐‘š โˆˆ โ„ค ( ๐ด โІ ( โ„คโ‰ฅ โ€˜ ๐‘š ) โˆง โˆƒ ๐‘› โˆˆ ( โ„คโ‰ฅ โ€˜ ๐‘š ) โˆƒ ๐‘ฆ ( ๐‘ฆ โ‰  0 โˆง seq ๐‘› ( ยท , ( ๐‘˜ โˆˆ โ„ค โ†ฆ if ( ๐‘˜ โˆˆ ๐ด , ๐ต , 1 ) ) ) โ‡ ๐‘ฆ ) โˆง seq ๐‘š ( ยท , ( ๐‘˜ โˆˆ โ„ค โ†ฆ if ( ๐‘˜ โˆˆ ๐ด , ๐ต , 1 ) ) ) โ‡ ๐‘ฅ ) โˆจ โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘“ ( ๐‘“ : ( 1 ... ๐‘š ) โ€“1-1-ontoโ†’ ๐ด โˆง ๐‘ฅ = ( seq 1 ( ยท , ( ๐‘› โˆˆ โ„• โ†ฆ โฆ‹ ( ๐‘“ โ€˜ ๐‘› ) / ๐‘˜ โฆŒ ๐ต ) ) โ€˜ ๐‘š ) ) ) )
51 3 50 wceq โŠข โˆ ๐‘˜ โˆˆ ๐ด ๐ต = ( โ„ฉ ๐‘ฅ ( โˆƒ ๐‘š โˆˆ โ„ค ( ๐ด โІ ( โ„คโ‰ฅ โ€˜ ๐‘š ) โˆง โˆƒ ๐‘› โˆˆ ( โ„คโ‰ฅ โ€˜ ๐‘š ) โˆƒ ๐‘ฆ ( ๐‘ฆ โ‰  0 โˆง seq ๐‘› ( ยท , ( ๐‘˜ โˆˆ โ„ค โ†ฆ if ( ๐‘˜ โˆˆ ๐ด , ๐ต , 1 ) ) ) โ‡ ๐‘ฆ ) โˆง seq ๐‘š ( ยท , ( ๐‘˜ โˆˆ โ„ค โ†ฆ if ( ๐‘˜ โˆˆ ๐ด , ๐ต , 1 ) ) ) โ‡ ๐‘ฅ ) โˆจ โˆƒ ๐‘š โˆˆ โ„• โˆƒ ๐‘“ ( ๐‘“ : ( 1 ... ๐‘š ) โ€“1-1-ontoโ†’ ๐ด โˆง ๐‘ฅ = ( seq 1 ( ยท , ( ๐‘› โˆˆ โ„• โ†ฆ โฆ‹ ( ๐‘“ โ€˜ ๐‘› ) / ๐‘˜ โฆŒ ๐ต ) ) โ€˜ ๐‘š ) ) ) )