Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-proddc Unicode version

Definition df-proddc 11430
 Description: Define the product of a series with an index set of integers . This definition takes most of the aspects of df-sumdc 11233 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 DECID #
Distinct variable groups:   ,,,,,,   ,,,,,,   ,,,,,,
Allowed substitution hints:   ()   ()

Detailed syntax breakdown of Definition df-proddc
StepHypRef Expression
1 cA . . 3
2 cB . . 3
3 vk . . 3
41, 2, 3cprod 11429 . 2
5 vm . . . . . . . . . 10
65cv 1334 . . . . . . . . 9
7 cuz 9422 . . . . . . . . 9
86, 7cfv 5167 . . . . . . . 8
91, 8wss 3102 . . . . . . 7
10 vj . . . . . . . . . . 11
1110cv 1334 . . . . . . . . . 10
1211, 1wcel 2128 . . . . . . . . 9
1312wdc 820 . . . . . . . 8 DECID
1413, 10, 8wral 2435 . . . . . . 7 DECID
159, 14wa 103 . . . . . 6 DECID
16 vy . . . . . . . . . . . 12
1716cv 1334 . . . . . . . . . . 11
18 cc0 7715 . . . . . . . . . . 11
19 cap 8439 . . . . . . . . . . 11 #
2017, 18, 19wbr 3965 . . . . . . . . . 10 #
21 cmul 7720 . . . . . . . . . . . 12
22 cz 9150 . . . . . . . . . . . . 13
233cv 1334 . . . . . . . . . . . . . . 15
2423, 1wcel 2128 . . . . . . . . . . . . . 14
25 c1 7716 . . . . . . . . . . . . . 14
2624, 2, 25cif 3505 . . . . . . . . . . . . 13
273, 22, 26cmpt 4025 . . . . . . . . . . . 12
28 vn . . . . . . . . . . . . 13
2928cv 1334 . . . . . . . . . . . 12
3021, 27, 29cseq 10326 . . . . . . . . . . 11
31 cli 11157 . . . . . . . . . . 11
3230, 17, 31wbr 3965 . . . . . . . . . 10
3320, 32wa 103 . . . . . . . . 9 #
3433, 16wex 1472 . . . . . . . 8 #
3534, 28, 8wrex 2436 . . . . . . 7 #
3621, 27, 6cseq 10326 . . . . . . . 8
37 vx . . . . . . . . 9
3837cv 1334 . . . . . . . 8
3936, 38, 31wbr 3965 . . . . . . 7
4035, 39wa 103 . . . . . 6 #
4115, 40wa 103 . . . . 5 DECID #
4241, 5, 22wrex 2436 . . . 4 DECID #
43 cfz 9894 . . . . . . . . 9
4425, 6, 43co 5818 . . . . . . . 8
45 vf . . . . . . . . 9
4645cv 1334 . . . . . . . 8
4744, 1, 46wf1o 5166 . . . . . . 7
48 cn 8816 . . . . . . . . . . 11
49 cle 7896 . . . . . . . . . . . . 13
5029, 6, 49wbr 3965 . . . . . . . . . . . 12
5129, 46cfv 5167 . . . . . . . . . . . . 13
523, 51, 2csb 3031 . . . . . . . . . . . 12
5350, 52, 25cif 3505 . . . . . . . . . . 11
5428, 48, 53cmpt 4025 . . . . . . . . . 10
5521, 54, 25cseq 10326 . . . . . . . . 9
566, 55cfv 5167 . . . . . . . 8
5738, 56wceq 1335 . . . . . . 7
5847, 57wa 103 . . . . . 6
5958, 45wex 1472 . . . . 5
6059, 5, 48wrex 2436 . . . 4
6142, 60wo 698 . . 3 DECID #
6261, 37cio 5130 . 2 DECID #
634, 62wceq 1335 1 DECID #
 Colors of variables: wff set class This definition is referenced by:  prodeq1f  11431  nfcprod1  11433  nfcprod  11434  prodeq2w  11435  prodeq2  11436  cbvprod  11437  zproddc  11458  fprodseq  11462
 Copyright terms: Public domain W3C validator