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

Definition df-proddc 11572
Description: Define the product of a series with an index set of integers ๐ด. This definition takes most of the aspects of df-sumdc 11375 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 ๐‘— โˆˆ ๐ด) โˆง (โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ # 0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฆ) โˆง seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฅ)) โˆจ โˆƒ๐‘š โˆˆ โ„• โˆƒ๐‘“(๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด โˆง ๐‘ฅ = (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ if(๐‘› โ‰ค ๐‘š, โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ต, 1)))โ€˜๐‘š))))
Distinct variable groups:   ๐ด,๐‘“,๐‘—,๐‘š,๐‘›,๐‘ฅ,๐‘ฆ   ๐ต,๐‘“,๐‘—,๐‘š,๐‘›,๐‘ฅ,๐‘ฆ   ๐‘“,๐‘˜,๐‘—,๐‘š,๐‘›,๐‘ฅ,๐‘ฆ
Allowed substitution hints:   ๐ด(๐‘˜)   ๐ต(๐‘˜)

Detailed syntax breakdown of Definition df-proddc
StepHypRef Expression
1 cA . . 3 class ๐ด
2 cB . . 3 class ๐ต
3 vk . . 3 setvar ๐‘˜
41, 2, 3cprod 11571 . 2 class โˆ๐‘˜ โˆˆ ๐ด ๐ต
5 vm . . . . . . . . . 10 setvar ๐‘š
65cv 1362 . . . . . . . . 9 class ๐‘š
7 cuz 9541 . . . . . . . . 9 class โ„คโ‰ฅ
86, 7cfv 5228 . . . . . . . 8 class (โ„คโ‰ฅโ€˜๐‘š)
91, 8wss 3141 . . . . . . 7 wff ๐ด โІ (โ„คโ‰ฅโ€˜๐‘š)
10 vj . . . . . . . . . . 11 setvar ๐‘—
1110cv 1362 . . . . . . . . . 10 class ๐‘—
1211, 1wcel 2158 . . . . . . . . 9 wff ๐‘— โˆˆ ๐ด
1312wdc 835 . . . . . . . 8 wff DECID ๐‘— โˆˆ ๐ด
1413, 10, 8wral 2465 . . . . . . 7 wff โˆ€๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘š)DECID ๐‘— โˆˆ ๐ด
159, 14wa 104 . . . . . 6 wff (๐ด โІ (โ„คโ‰ฅโ€˜๐‘š) โˆง โˆ€๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘š)DECID ๐‘— โˆˆ ๐ด)
16 vy . . . . . . . . . . . 12 setvar ๐‘ฆ
1716cv 1362 . . . . . . . . . . 11 class ๐‘ฆ
18 cc0 7824 . . . . . . . . . . 11 class 0
19 cap 8551 . . . . . . . . . . 11 class #
2017, 18, 19wbr 4015 . . . . . . . . . 10 wff ๐‘ฆ # 0
21 cmul 7829 . . . . . . . . . . . 12 class ยท
22 cz 9266 . . . . . . . . . . . . 13 class โ„ค
233cv 1362 . . . . . . . . . . . . . . 15 class ๐‘˜
2423, 1wcel 2158 . . . . . . . . . . . . . 14 wff ๐‘˜ โˆˆ ๐ด
25 c1 7825 . . . . . . . . . . . . . 14 class 1
2624, 2, 25cif 3546 . . . . . . . . . . . . 13 class if(๐‘˜ โˆˆ ๐ด, ๐ต, 1)
273, 22, 26cmpt 4076 . . . . . . . . . . . 12 class (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))
28 vn . . . . . . . . . . . . 13 setvar ๐‘›
2928cv 1362 . . . . . . . . . . . 12 class ๐‘›
3021, 27, 29cseq 10458 . . . . . . . . . . 11 class seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1)))
31 cli 11299 . . . . . . . . . . 11 class โ‡
3230, 17, 31wbr 4015 . . . . . . . . . 10 wff seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฆ
3320, 32wa 104 . . . . . . . . 9 wff (๐‘ฆ # 0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฆ)
3433, 16wex 1502 . . . . . . . 8 wff โˆƒ๐‘ฆ(๐‘ฆ # 0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฆ)
3534, 28, 8wrex 2466 . . . . . . 7 wff โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ # 0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฆ)
3621, 27, 6cseq 10458 . . . . . . . 8 class seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1)))
37 vx . . . . . . . . 9 setvar ๐‘ฅ
3837cv 1362 . . . . . . . 8 class ๐‘ฅ
3936, 38, 31wbr 4015 . . . . . . 7 wff seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฅ
4035, 39wa 104 . . . . . 6 wff (โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ # 0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฆ) โˆง seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฅ)
4115, 40wa 104 . . . . 5 wff ((๐ด โІ (โ„คโ‰ฅโ€˜๐‘š) โˆง โˆ€๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘š)DECID ๐‘— โˆˆ ๐ด) โˆง (โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ # 0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฆ) โˆง seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฅ))
4241, 5, 22wrex 2466 . . . 4 wff โˆƒ๐‘š โˆˆ โ„ค ((๐ด โІ (โ„คโ‰ฅโ€˜๐‘š) โˆง โˆ€๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘š)DECID ๐‘— โˆˆ ๐ด) โˆง (โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ # 0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฆ) โˆง seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฅ))
43 cfz 10021 . . . . . . . . 9 class ...
4425, 6, 43co 5888 . . . . . . . 8 class (1...๐‘š)
45 vf . . . . . . . . 9 setvar ๐‘“
4645cv 1362 . . . . . . . 8 class ๐‘“
4744, 1, 46wf1o 5227 . . . . . . 7 wff ๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด
48 cn 8932 . . . . . . . . . . 11 class โ„•
49 cle 8006 . . . . . . . . . . . . 13 class โ‰ค
5029, 6, 49wbr 4015 . . . . . . . . . . . 12 wff ๐‘› โ‰ค ๐‘š
5129, 46cfv 5228 . . . . . . . . . . . . 13 class (๐‘“โ€˜๐‘›)
523, 51, 2csb 3069 . . . . . . . . . . . 12 class โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ต
5350, 52, 25cif 3546 . . . . . . . . . . 11 class if(๐‘› โ‰ค ๐‘š, โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ต, 1)
5428, 48, 53cmpt 4076 . . . . . . . . . 10 class (๐‘› โˆˆ โ„• โ†ฆ if(๐‘› โ‰ค ๐‘š, โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ต, 1))
5521, 54, 25cseq 10458 . . . . . . . . 9 class seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ if(๐‘› โ‰ค ๐‘š, โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ต, 1)))
566, 55cfv 5228 . . . . . . . 8 class (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ if(๐‘› โ‰ค ๐‘š, โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ต, 1)))โ€˜๐‘š)
5738, 56wceq 1363 . . . . . . 7 wff ๐‘ฅ = (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ if(๐‘› โ‰ค ๐‘š, โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ต, 1)))โ€˜๐‘š)
5847, 57wa 104 . . . . . 6 wff (๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด โˆง ๐‘ฅ = (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ if(๐‘› โ‰ค ๐‘š, โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ต, 1)))โ€˜๐‘š))
5958, 45wex 1502 . . . . 5 wff โˆƒ๐‘“(๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด โˆง ๐‘ฅ = (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ if(๐‘› โ‰ค ๐‘š, โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ต, 1)))โ€˜๐‘š))
6059, 5, 48wrex 2466 . . . 4 wff โˆƒ๐‘š โˆˆ โ„• โˆƒ๐‘“(๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด โˆง ๐‘ฅ = (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ if(๐‘› โ‰ค ๐‘š, โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ต, 1)))โ€˜๐‘š))
6142, 60wo 709 . . 3 wff (โˆƒ๐‘š โˆˆ โ„ค ((๐ด โІ (โ„คโ‰ฅโ€˜๐‘š) โˆง โˆ€๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘š)DECID ๐‘— โˆˆ ๐ด) โˆง (โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ # 0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฆ) โˆง seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฅ)) โˆจ โˆƒ๐‘š โˆˆ โ„• โˆƒ๐‘“(๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด โˆง ๐‘ฅ = (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ if(๐‘› โ‰ค ๐‘š, โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ต, 1)))โ€˜๐‘š)))
6261, 37cio 5188 . 2 class (โ„ฉ๐‘ฅ(โˆƒ๐‘š โˆˆ โ„ค ((๐ด โІ (โ„คโ‰ฅโ€˜๐‘š) โˆง โˆ€๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘š)DECID ๐‘— โˆˆ ๐ด) โˆง (โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ # 0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฆ) โˆง seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฅ)) โˆจ โˆƒ๐‘š โˆˆ โ„• โˆƒ๐‘“(๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด โˆง ๐‘ฅ = (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ if(๐‘› โ‰ค ๐‘š, โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ต, 1)))โ€˜๐‘š))))
634, 62wceq 1363 1 wff โˆ๐‘˜ โˆˆ ๐ด ๐ต = (โ„ฉ๐‘ฅ(โˆƒ๐‘š โˆˆ โ„ค ((๐ด โІ (โ„คโ‰ฅโ€˜๐‘š) โˆง โˆ€๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘š)DECID ๐‘— โˆˆ ๐ด) โˆง (โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ # 0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฆ) โˆง seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฅ)) โˆจ โˆƒ๐‘š โˆˆ โ„• โˆƒ๐‘“(๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด โˆง ๐‘ฅ = (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ if(๐‘› โ‰ค ๐‘š, โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ต, 1)))โ€˜๐‘š))))
Colors of variables: wff set class
This definition is referenced by:  prodeq1f  11573  nfcprod1  11575  nfcprod  11576  prodeq2w  11577  prodeq2  11578  cbvprod  11579  zproddc  11600  fprodseq  11604
  Copyright terms: Public domain W3C validator