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

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

Detailed syntax breakdown of Definition df-prod
StepHypRef Expression
1 cA . . 3
2 cB . . 3
3 vk . . 3
41, 2, 3cprod 13712 . 2
5 vm . . . . . . . . 9
65cv 1394 . . . . . . . 8
7 cuz 11110 . . . . . . . 8
86, 7cfv 5593 . . . . . . 7
91, 8wss 3475 . . . . . 6
10 vy . . . . . . . . . . 11
1110cv 1394 . . . . . . . . . 10
12 cc0 9513 . . . . . . . . . 10
1311, 12wne 2652 . . . . . . . . 9
14 cmul 9518 . . . . . . . . . . 11
15 cz 10889 . . . . . . . . . . . 12
163cv 1394 . . . . . . . . . . . . . 14
1716, 1wcel 1818 . . . . . . . . . . . . 13
18 c1 9514 . . . . . . . . . . . . 13
1917, 2, 18cif 3941 . . . . . . . . . . . 12
203, 15, 19cmpt 4510 . . . . . . . . . . 11
21 vn . . . . . . . . . . . 12
2221cv 1394 . . . . . . . . . . 11
2314, 20, 22cseq 12107 . . . . . . . . . 10
24 cli 13307 . . . . . . . . . 10
2523, 11, 24wbr 4452 . . . . . . . . 9
2613, 25wa 369 . . . . . . . 8
2726, 10wex 1612 . . . . . . 7
2827, 21, 8wrex 2808 . . . . . 6
2914, 20, 6cseq 12107 . . . . . . 7
30 vx . . . . . . . 8
3130cv 1394 . . . . . . 7
3229, 31, 24wbr 4452 . . . . . 6
339, 28, 32w3a 973 . . . . 5
3433, 5, 15wrex 2808 . . . 4
35 cfz 11701 . . . . . . . . 9
3618, 6, 35co 6296 . . . . . . . 8
37 vf . . . . . . . . 9
3837cv 1394 . . . . . . . 8
3936, 1, 38wf1o 5592 . . . . . . 7
40 cn 10561 . . . . . . . . . . 11
4122, 38cfv 5593 . . . . . . . . . . . 12
423, 41, 2csb 3434 . . . . . . . . . . 11
4321, 40, 42cmpt 4510 . . . . . . . . . 10
4414, 43, 18cseq 12107 . . . . . . . . 9
456, 44cfv 5593 . . . . . . . 8
4631, 45wceq 1395 . . . . . . 7
4739, 46wa 369 . . . . . 6
4847, 37wex 1612 . . . . 5
4948, 5, 40wrex 2808 . . . 4
5034, 49wo 368 . . 3
5150, 30cio 5554 . 2
524, 51wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  prodex  13714  prodeq1f  13715  nfcprod1  13717  nfcprod  13718  prodeq2w  13719  prodeq2ii  13720  cbvprod  13722  zprod  13744  fprod  13748
  Copyright terms: Public domain W3C validator