Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-prod Structured version   Unicode version

Definition df-prod 13772
 Description: Define the product of a series with an index set of integers . This definition takes most of the aspects of df-sum 13565 and adapts them for multiplication instead of addition. However, we insist that in the infinite case, there is a non-zero 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
Distinct variable groups:   ,,,,,   ,,,,,   ,,,,,
Allowed substitution hints:   ()   ()

Detailed syntax breakdown of Definition df-prod
StepHypRef Expression
1 cA . . 3
2 cB . . 3
3 vk . . 3
41, 2, 3cprod 13771 . 2
5 vm . . . . . . . . 9
65cv 1404 . . . . . . . 8
7 cuz 11045 . . . . . . . 8
86, 7cfv 5525 . . . . . . 7
91, 8wss 3413 . . . . . 6
10 vy . . . . . . . . . . 11
1110cv 1404 . . . . . . . . . 10
12 cc0 9442 . . . . . . . . . 10
1311, 12wne 2598 . . . . . . . . 9
14 cmul 9447 . . . . . . . . . . 11
15 cz 10825 . . . . . . . . . . . 12
163cv 1404 . . . . . . . . . . . . . 14
1716, 1wcel 1842 . . . . . . . . . . . . 13
18 c1 9443 . . . . . . . . . . . . 13
1917, 2, 18cif 3884 . . . . . . . . . . . 12
203, 15, 19cmpt 4452 . . . . . . . . . . 11
21 vn . . . . . . . . . . . 12
2221cv 1404 . . . . . . . . . . 11
2314, 20, 22cseq 12061 . . . . . . . . . 10
24 cli 13363 . . . . . . . . . 10
2523, 11, 24wbr 4394 . . . . . . . . 9
2613, 25wa 367 . . . . . . . 8
2726, 10wex 1633 . . . . . . 7
2827, 21, 8wrex 2754 . . . . . 6
2914, 20, 6cseq 12061 . . . . . . 7
30 vx . . . . . . . 8
3130cv 1404 . . . . . . 7
3229, 31, 24wbr 4394 . . . . . 6
339, 28, 32w3a 974 . . . . 5
3433, 5, 15wrex 2754 . . . 4
35 cfz 11643 . . . . . . . . 9
3618, 6, 35co 6234 . . . . . . . 8
37 vf . . . . . . . . 9
3837cv 1404 . . . . . . . 8
3936, 1, 38wf1o 5524 . . . . . . 7
40 cn 10496 . . . . . . . . . . 11
4122, 38cfv 5525 . . . . . . . . . . . 12
423, 41, 2csb 3372 . . . . . . . . . . 11
4321, 40, 42cmpt 4452 . . . . . . . . . 10
4414, 43, 18cseq 12061 . . . . . . . . 9
456, 44cfv 5525 . . . . . . . 8
4631, 45wceq 1405 . . . . . . 7
4739, 46wa 367 . . . . . 6
4847, 37wex 1633 . . . . 5
4948, 5, 40wrex 2754 . . . 4
5034, 49wo 366 . . 3
5150, 30cio 5487 . 2
524, 51wceq 1405 1
 Colors of variables: wff setvar class This definition is referenced by:  prodex  13773  prodeq1f  13774  nfcprod1  13776  nfcprod  13777  prodeq2w  13778  prodeq2ii  13779  cbvprod  13781  zprod  13803  fprod  13807
 Copyright terms: Public domain W3C validator