Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-prod Structured version   Unicode version

Definition df-prod 25237
 Description: Define the product of a series with an index set of integers . This definition takes most of the aspects of df-sum 12485 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 25236 . 2
5 vm . . . . . . . . 9
65cv 1652 . . . . . . . 8
7 cuz 10493 . . . . . . . 8
86, 7cfv 5457 . . . . . . 7
91, 8wss 3322 . . . . . 6
10 vy . . . . . . . . . . 11
1110cv 1652 . . . . . . . . . 10
12 cc0 8995 . . . . . . . . . 10
1311, 12wne 2601 . . . . . . . . 9
14 cmul 9000 . . . . . . . . . . 11
15 cz 10287 . . . . . . . . . . . 12
163cv 1652 . . . . . . . . . . . . . 14
1716, 1wcel 1726 . . . . . . . . . . . . 13
18 c1 8996 . . . . . . . . . . . . 13
1917, 2, 18cif 3741 . . . . . . . . . . . 12
203, 15, 19cmpt 4269 . . . . . . . . . . 11
21 vn . . . . . . . . . . . 12
2221cv 1652 . . . . . . . . . . 11
2314, 20, 22cseq 11328 . . . . . . . . . 10
24 cli 12283 . . . . . . . . . 10
2523, 11, 24wbr 4215 . . . . . . . . 9
2613, 25wa 360 . . . . . . . 8
2726, 10wex 1551 . . . . . . 7
2827, 21, 8wrex 2708 . . . . . 6
2914, 20, 6cseq 11328 . . . . . . 7
30 vx . . . . . . . 8
3130cv 1652 . . . . . . 7
3229, 31, 24wbr 4215 . . . . . 6
339, 28, 32w3a 937 . . . . 5
3433, 5, 15wrex 2708 . . . 4
35 cfz 11048 . . . . . . . . 9
3618, 6, 35co 6084 . . . . . . . 8
37 vf . . . . . . . . 9
3837cv 1652 . . . . . . . 8
3936, 1, 38wf1o 5456 . . . . . . 7
40 cn 10005 . . . . . . . . . . 11
4122, 38cfv 5457 . . . . . . . . . . . 12
423, 41, 2csb 3253 . . . . . . . . . . 11
4321, 40, 42cmpt 4269 . . . . . . . . . 10
4414, 43, 18cseq 11328 . . . . . . . . 9
456, 44cfv 5457 . . . . . . . 8
4631, 45wceq 1653 . . . . . . 7
4739, 46wa 360 . . . . . 6
4847, 37wex 1551 . . . . 5
4948, 5, 40wrex 2708 . . . 4
5034, 49wo 359 . . 3
5150, 30cio 5419 . 2
524, 51wceq 1653 1
 Colors of variables: wff set class This definition is referenced by:  prodex  25238  prodeq1f  25239  nfcprod1  25241  nfcprod  25242  prodeq2w  25243  prodeq2ii  25244  cbvprod  25246  zprod  25268  fprod  25272
 Copyright terms: Public domain W3C validator