MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  zprod Structured version   Visualization version   GIF version

Theorem zprod 15812
Description: Series product with index set a subset of the upper integers. (Contributed by Scott Fenton, 5-Dec-2017.)
Hypotheses
Ref Expression
zprod.1 ๐‘ = (โ„คโ‰ฅโ€˜๐‘€)
zprod.2 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„ค)
zprod.3 (๐œ‘ โ†’ โˆƒ๐‘› โˆˆ ๐‘ โˆƒ๐‘ฆ(๐‘ฆ โ‰  0 โˆง seq๐‘›( ยท , ๐น) โ‡ ๐‘ฆ))
zprod.4 (๐œ‘ โ†’ ๐ด โŠ† ๐‘)
zprod.5 ((๐œ‘ โˆง ๐‘˜ โˆˆ ๐‘) โ†’ (๐นโ€˜๐‘˜) = if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))
zprod.6 ((๐œ‘ โˆง ๐‘˜ โˆˆ ๐ด) โ†’ ๐ต โˆˆ โ„‚)
Assertion
Ref Expression
zprod (๐œ‘ โ†’ โˆ๐‘˜ โˆˆ ๐ด ๐ต = ( โ‡ โ€˜seq๐‘€( ยท , ๐น)))
Distinct variable groups:   ๐ด,๐‘˜,๐‘›,๐‘ฆ   ๐ต,๐‘›,๐‘ฆ   ๐‘˜,๐น   ๐‘˜,๐‘›,๐œ‘,๐‘ฆ   ๐‘˜,๐‘€,๐‘ฆ   ๐œ‘,๐‘›,๐‘ฆ   ๐‘›,๐‘
Allowed substitution hints:   ๐ต(๐‘˜)   ๐น(๐‘ฆ,๐‘›)   ๐‘€(๐‘›)   ๐‘(๐‘ฆ,๐‘˜)

Proof of Theorem zprod
Dummy variables ๐‘“ ๐‘” ๐‘– ๐‘— ๐‘š ๐‘ฅ ๐‘ง are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 3simpb 1149 . . . . . . . 8 ((๐ด โŠ† (โ„คโ‰ฅโ€˜๐‘š) โˆง โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ โ‰  0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฆ) โˆง seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฅ) โ†’ (๐ด โŠ† (โ„คโ‰ฅโ€˜๐‘š) โˆง seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฅ))
2 nfcv 2905 . . . . . . . . . . . 12 โ„ฒ๐‘–if(๐‘˜ โˆˆ ๐ด, ๐ต, 1)
3 nfv 1917 . . . . . . . . . . . . 13 โ„ฒ๐‘˜ ๐‘– โˆˆ ๐ด
4 nfcsb1v 3878 . . . . . . . . . . . . 13 โ„ฒ๐‘˜โฆ‹๐‘– / ๐‘˜โฆŒ๐ต
5 nfcv 2905 . . . . . . . . . . . . 13 โ„ฒ๐‘˜1
63, 4, 5nfif 4514 . . . . . . . . . . . 12 โ„ฒ๐‘˜if(๐‘– โˆˆ ๐ด, โฆ‹๐‘– / ๐‘˜โฆŒ๐ต, 1)
7 eleq1w 2820 . . . . . . . . . . . . 13 (๐‘˜ = ๐‘– โ†’ (๐‘˜ โˆˆ ๐ด โ†” ๐‘– โˆˆ ๐ด))
8 csbeq1a 3867 . . . . . . . . . . . . 13 (๐‘˜ = ๐‘– โ†’ ๐ต = โฆ‹๐‘– / ๐‘˜โฆŒ๐ต)
97, 8ifbieq1d 4508 . . . . . . . . . . . 12 (๐‘˜ = ๐‘– โ†’ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1) = if(๐‘– โˆˆ ๐ด, โฆ‹๐‘– / ๐‘˜โฆŒ๐ต, 1))
102, 6, 9cbvmpt 5214 . . . . . . . . . . 11 (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1)) = (๐‘– โˆˆ โ„ค โ†ฆ if(๐‘– โˆˆ ๐ด, โฆ‹๐‘– / ๐‘˜โฆŒ๐ต, 1))
11 simpll 765 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘š โˆˆ โ„ค) โˆง ๐ด โŠ† (โ„คโ‰ฅโ€˜๐‘š)) โ†’ ๐œ‘)
12 zprod.6 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘˜ โˆˆ ๐ด) โ†’ ๐ต โˆˆ โ„‚)
1312ralrimiva 3141 . . . . . . . . . . . . 13 (๐œ‘ โ†’ โˆ€๐‘˜ โˆˆ ๐ด ๐ต โˆˆ โ„‚)
144nfel1 2921 . . . . . . . . . . . . . 14 โ„ฒ๐‘˜โฆ‹๐‘– / ๐‘˜โฆŒ๐ต โˆˆ โ„‚
158eleq1d 2822 . . . . . . . . . . . . . 14 (๐‘˜ = ๐‘– โ†’ (๐ต โˆˆ โ„‚ โ†” โฆ‹๐‘– / ๐‘˜โฆŒ๐ต โˆˆ โ„‚))
1614, 15rspc 3567 . . . . . . . . . . . . 13 (๐‘– โˆˆ ๐ด โ†’ (โˆ€๐‘˜ โˆˆ ๐ด ๐ต โˆˆ โ„‚ โ†’ โฆ‹๐‘– / ๐‘˜โฆŒ๐ต โˆˆ โ„‚))
1713, 16syl5 34 . . . . . . . . . . . 12 (๐‘– โˆˆ ๐ด โ†’ (๐œ‘ โ†’ โฆ‹๐‘– / ๐‘˜โฆŒ๐ต โˆˆ โ„‚))
1811, 17mpan9 507 . . . . . . . . . . 11 ((((๐œ‘ โˆง ๐‘š โˆˆ โ„ค) โˆง ๐ด โŠ† (โ„คโ‰ฅโ€˜๐‘š)) โˆง ๐‘– โˆˆ ๐ด) โ†’ โฆ‹๐‘– / ๐‘˜โฆŒ๐ต โˆˆ โ„‚)
19 simplr 767 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘š โˆˆ โ„ค) โˆง ๐ด โŠ† (โ„คโ‰ฅโ€˜๐‘š)) โ†’ ๐‘š โˆˆ โ„ค)
20 zprod.2 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„ค)
2120ad2antrr 724 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘š โˆˆ โ„ค) โˆง ๐ด โŠ† (โ„คโ‰ฅโ€˜๐‘š)) โ†’ ๐‘€ โˆˆ โ„ค)
22 simpr 485 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘š โˆˆ โ„ค) โˆง ๐ด โŠ† (โ„คโ‰ฅโ€˜๐‘š)) โ†’ ๐ด โŠ† (โ„คโ‰ฅโ€˜๐‘š))
23 zprod.4 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐ด โŠ† ๐‘)
24 zprod.1 . . . . . . . . . . . . 13 ๐‘ = (โ„คโ‰ฅโ€˜๐‘€)
2523, 24sseqtrdi 3992 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐ด โŠ† (โ„คโ‰ฅโ€˜๐‘€))
2625ad2antrr 724 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘š โˆˆ โ„ค) โˆง ๐ด โŠ† (โ„คโ‰ฅโ€˜๐‘š)) โ†’ ๐ด โŠ† (โ„คโ‰ฅโ€˜๐‘€))
2710, 18, 19, 21, 22, 26prodrb 15807 . . . . . . . . . 10 (((๐œ‘ โˆง ๐‘š โˆˆ โ„ค) โˆง ๐ด โŠ† (โ„คโ‰ฅโ€˜๐‘š)) โ†’ (seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฅ โ†” seq๐‘€( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฅ))
2827biimpd 228 . . . . . . . . 9 (((๐œ‘ โˆง ๐‘š โˆˆ โ„ค) โˆง ๐ด โŠ† (โ„คโ‰ฅโ€˜๐‘š)) โ†’ (seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฅ โ†’ seq๐‘€( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฅ))
2928expimpd 454 . . . . . . . 8 ((๐œ‘ โˆง ๐‘š โˆˆ โ„ค) โ†’ ((๐ด โŠ† (โ„คโ‰ฅโ€˜๐‘š) โˆง seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฅ) โ†’ seq๐‘€( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฅ))
301, 29syl5 34 . . . . . . 7 ((๐œ‘ โˆง ๐‘š โˆˆ โ„ค) โ†’ ((๐ด โŠ† (โ„คโ‰ฅโ€˜๐‘š) โˆง โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ โ‰  0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฆ) โˆง seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฅ) โ†’ seq๐‘€( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฅ))
3130rexlimdva 3150 . . . . . 6 (๐œ‘ โ†’ (โˆƒ๐‘š โˆˆ โ„ค (๐ด โŠ† (โ„คโ‰ฅโ€˜๐‘š) โˆง โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ โ‰  0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฆ) โˆง seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฅ) โ†’ seq๐‘€( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฅ))
32 uzssz 12780 . . . . . . . . . . . . . . . . 17 (โ„คโ‰ฅโ€˜๐‘€) โŠ† โ„ค
33 zssre 12502 . . . . . . . . . . . . . . . . 17 โ„ค โŠ† โ„
3432, 33sstri 3951 . . . . . . . . . . . . . . . 16 (โ„คโ‰ฅโ€˜๐‘€) โŠ† โ„
3524, 34eqsstri 3976 . . . . . . . . . . . . . . 15 ๐‘ โŠ† โ„
3623, 35sstrdi 3954 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ๐ด โŠ† โ„)
3736ad2antrr 724 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘š โˆˆ โ„•) โˆง ๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด) โ†’ ๐ด โŠ† โ„)
38 ltso 11231 . . . . . . . . . . . . 13 < Or โ„
39 soss 5563 . . . . . . . . . . . . 13 (๐ด โŠ† โ„ โ†’ ( < Or โ„ โ†’ < Or ๐ด))
4037, 38, 39mpisyl 21 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘š โˆˆ โ„•) โˆง ๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด) โ†’ < Or ๐ด)
41 fzfi 13869 . . . . . . . . . . . . 13 (1...๐‘š) โˆˆ Fin
42 ovex 7386 . . . . . . . . . . . . . . . 16 (1...๐‘š) โˆˆ V
4342f1oen 8909 . . . . . . . . . . . . . . 15 (๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด โ†’ (1...๐‘š) โ‰ˆ ๐ด)
4443adantl 482 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘š โˆˆ โ„•) โˆง ๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด) โ†’ (1...๐‘š) โ‰ˆ ๐ด)
4544ensymd 8941 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘š โˆˆ โ„•) โˆง ๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด) โ†’ ๐ด โ‰ˆ (1...๐‘š))
46 enfii 9129 . . . . . . . . . . . . 13 (((1...๐‘š) โˆˆ Fin โˆง ๐ด โ‰ˆ (1...๐‘š)) โ†’ ๐ด โˆˆ Fin)
4741, 45, 46sylancr 587 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘š โˆˆ โ„•) โˆง ๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด) โ†’ ๐ด โˆˆ Fin)
48 fz1iso 14353 . . . . . . . . . . . 12 (( < Or ๐ด โˆง ๐ด โˆˆ Fin) โ†’ โˆƒ๐‘” ๐‘” Isom < , < ((1...(โ™ฏโ€˜๐ด)), ๐ด))
4940, 47, 48syl2anc 584 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘š โˆˆ โ„•) โˆง ๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด) โ†’ โˆƒ๐‘” ๐‘” Isom < , < ((1...(โ™ฏโ€˜๐ด)), ๐ด))
50 simpll 765 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘š โˆˆ โ„•) โˆง (๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด โˆง ๐‘” Isom < , < ((1...(โ™ฏโ€˜๐ด)), ๐ด))) โ†’ ๐œ‘)
5150, 17mpan9 507 . . . . . . . . . . . . . 14 ((((๐œ‘ โˆง ๐‘š โˆˆ โ„•) โˆง (๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด โˆง ๐‘” Isom < , < ((1...(โ™ฏโ€˜๐ด)), ๐ด))) โˆง ๐‘– โˆˆ ๐ด) โ†’ โฆ‹๐‘– / ๐‘˜โฆŒ๐ต โˆˆ โ„‚)
52 fveq2 6839 . . . . . . . . . . . . . . . . 17 (๐‘› = ๐‘— โ†’ (๐‘“โ€˜๐‘›) = (๐‘“โ€˜๐‘—))
5352csbeq1d 3857 . . . . . . . . . . . . . . . 16 (๐‘› = ๐‘— โ†’ โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ต = โฆ‹(๐‘“โ€˜๐‘—) / ๐‘˜โฆŒ๐ต)
54 csbcow 3868 . . . . . . . . . . . . . . . 16 โฆ‹(๐‘“โ€˜๐‘—) / ๐‘–โฆŒโฆ‹๐‘– / ๐‘˜โฆŒ๐ต = โฆ‹(๐‘“โ€˜๐‘—) / ๐‘˜โฆŒ๐ต
5553, 54eqtr4di 2794 . . . . . . . . . . . . . . 15 (๐‘› = ๐‘— โ†’ โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ต = โฆ‹(๐‘“โ€˜๐‘—) / ๐‘–โฆŒโฆ‹๐‘– / ๐‘˜โฆŒ๐ต)
5655cbvmptv 5216 . . . . . . . . . . . . . 14 (๐‘› โˆˆ โ„• โ†ฆ โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ต) = (๐‘— โˆˆ โ„• โ†ฆ โฆ‹(๐‘“โ€˜๐‘—) / ๐‘–โฆŒโฆ‹๐‘– / ๐‘˜โฆŒ๐ต)
57 eqid 2736 . . . . . . . . . . . . . 14 (๐‘— โˆˆ โ„• โ†ฆ โฆ‹(๐‘”โ€˜๐‘—) / ๐‘–โฆŒโฆ‹๐‘– / ๐‘˜โฆŒ๐ต) = (๐‘— โˆˆ โ„• โ†ฆ โฆ‹(๐‘”โ€˜๐‘—) / ๐‘–โฆŒโฆ‹๐‘– / ๐‘˜โฆŒ๐ต)
58 simplr 767 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘š โˆˆ โ„•) โˆง (๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด โˆง ๐‘” Isom < , < ((1...(โ™ฏโ€˜๐ด)), ๐ด))) โ†’ ๐‘š โˆˆ โ„•)
5920ad2antrr 724 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘š โˆˆ โ„•) โˆง (๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด โˆง ๐‘” Isom < , < ((1...(โ™ฏโ€˜๐ด)), ๐ด))) โ†’ ๐‘€ โˆˆ โ„ค)
6025ad2antrr 724 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘š โˆˆ โ„•) โˆง (๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด โˆง ๐‘” Isom < , < ((1...(โ™ฏโ€˜๐ด)), ๐ด))) โ†’ ๐ด โŠ† (โ„คโ‰ฅโ€˜๐‘€))
61 simprl 769 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘š โˆˆ โ„•) โˆง (๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด โˆง ๐‘” Isom < , < ((1...(โ™ฏโ€˜๐ด)), ๐ด))) โ†’ ๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด)
62 simprr 771 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘š โˆˆ โ„•) โˆง (๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด โˆง ๐‘” Isom < , < ((1...(โ™ฏโ€˜๐ด)), ๐ด))) โ†’ ๐‘” Isom < , < ((1...(โ™ฏโ€˜๐ด)), ๐ด))
6310, 51, 56, 57, 58, 59, 60, 61, 62prodmolem2a 15809 . . . . . . . . . . . . 13 (((๐œ‘ โˆง ๐‘š โˆˆ โ„•) โˆง (๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด โˆง ๐‘” Isom < , < ((1...(โ™ฏโ€˜๐ด)), ๐ด))) โ†’ seq๐‘€( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ต))โ€˜๐‘š))
6463expr 457 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘š โˆˆ โ„•) โˆง ๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด) โ†’ (๐‘” Isom < , < ((1...(โ™ฏโ€˜๐ด)), ๐ด) โ†’ seq๐‘€( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ต))โ€˜๐‘š)))
6564exlimdv 1936 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘š โˆˆ โ„•) โˆง ๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด) โ†’ (โˆƒ๐‘” ๐‘” Isom < , < ((1...(โ™ฏโ€˜๐ด)), ๐ด) โ†’ seq๐‘€( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ต))โ€˜๐‘š)))
6649, 65mpd 15 . . . . . . . . . 10 (((๐œ‘ โˆง ๐‘š โˆˆ โ„•) โˆง ๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด) โ†’ seq๐‘€( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ต))โ€˜๐‘š))
67 breq2 5107 . . . . . . . . . 10 (๐‘ฅ = (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ต))โ€˜๐‘š) โ†’ (seq๐‘€( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฅ โ†” seq๐‘€( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ต))โ€˜๐‘š)))
6866, 67syl5ibrcom 246 . . . . . . . . 9 (((๐œ‘ โˆง ๐‘š โˆˆ โ„•) โˆง ๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด) โ†’ (๐‘ฅ = (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ต))โ€˜๐‘š) โ†’ seq๐‘€( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฅ))
6968expimpd 454 . . . . . . . 8 ((๐œ‘ โˆง ๐‘š โˆˆ โ„•) โ†’ ((๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด โˆง ๐‘ฅ = (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ต))โ€˜๐‘š)) โ†’ seq๐‘€( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฅ))
7069exlimdv 1936 . . . . . . 7 ((๐œ‘ โˆง ๐‘š โˆˆ โ„•) โ†’ (โˆƒ๐‘“(๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด โˆง ๐‘ฅ = (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ต))โ€˜๐‘š)) โ†’ seq๐‘€( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฅ))
7170rexlimdva 3150 . . . . . 6 (๐œ‘ โ†’ (โˆƒ๐‘š โˆˆ โ„• โˆƒ๐‘“(๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด โˆง ๐‘ฅ = (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ต))โ€˜๐‘š)) โ†’ seq๐‘€( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฅ))
7231, 71jaod 857 . . . . 5 (๐œ‘ โ†’ ((โˆƒ๐‘š โˆˆ โ„ค (๐ด โŠ† (โ„คโ‰ฅโ€˜๐‘š) โˆง โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ โ‰  0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฆ) โˆง seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฅ) โˆจ โˆƒ๐‘š โˆˆ โ„• โˆƒ๐‘“(๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด โˆง ๐‘ฅ = (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ต))โ€˜๐‘š))) โ†’ seq๐‘€( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฅ))
7320adantr 481 . . . . . . . 8 ((๐œ‘ โˆง seq๐‘€( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฅ) โ†’ ๐‘€ โˆˆ โ„ค)
7423adantr 481 . . . . . . . 8 ((๐œ‘ โˆง seq๐‘€( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฅ) โ†’ ๐ด โŠ† ๐‘)
75 zprod.3 . . . . . . . . . 10 (๐œ‘ โ†’ โˆƒ๐‘› โˆˆ ๐‘ โˆƒ๐‘ฆ(๐‘ฆ โ‰  0 โˆง seq๐‘›( ยท , ๐น) โ‡ ๐‘ฆ))
7624eleq2i 2829 . . . . . . . . . . . 12 (๐‘› โˆˆ ๐‘ โ†” ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘€))
77 eluzelz 12769 . . . . . . . . . . . . . . . . 17 (๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘€) โ†’ ๐‘› โˆˆ โ„ค)
7877adantl 482 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ ๐‘› โˆˆ โ„ค)
79 uztrn 12777 . . . . . . . . . . . . . . . . . . 19 ((๐‘ง โˆˆ (โ„คโ‰ฅโ€˜๐‘›) โˆง ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ ๐‘ง โˆˆ (โ„คโ‰ฅโ€˜๐‘€))
8079ancoms 459 . . . . . . . . . . . . . . . . . 18 ((๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘€) โˆง ๐‘ง โˆˆ (โ„คโ‰ฅโ€˜๐‘›)) โ†’ ๐‘ง โˆˆ (โ„คโ‰ฅโ€˜๐‘€))
8124eleq2i 2829 . . . . . . . . . . . . . . . . . . . . 21 (๐‘˜ โˆˆ ๐‘ โ†” ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€))
82 zprod.5 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง ๐‘˜ โˆˆ ๐‘) โ†’ (๐นโ€˜๐‘˜) = if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))
8324, 32eqsstri 3976 . . . . . . . . . . . . . . . . . . . . . . . 24 ๐‘ โŠ† โ„ค
8483sseli 3938 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘˜ โˆˆ ๐‘ โ†’ ๐‘˜ โˆˆ โ„ค)
85 iftrue 4490 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (๐‘˜ โˆˆ ๐ด โ†’ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1) = ๐ต)
8685adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((๐œ‘ โˆง ๐‘˜ โˆˆ ๐ด) โ†’ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1) = ๐ต)
8786, 12eqeltrd 2838 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐œ‘ โˆง ๐‘˜ โˆˆ ๐ด) โ†’ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1) โˆˆ โ„‚)
8887ex 413 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐œ‘ โ†’ (๐‘˜ โˆˆ ๐ด โ†’ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1) โˆˆ โ„‚))
89 iffalse 4493 . . . . . . . . . . . . . . . . . . . . . . . . 25 (ยฌ ๐‘˜ โˆˆ ๐ด โ†’ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1) = 1)
90 ax-1cn 11105 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 โˆˆ โ„‚
9189, 90eqeltrdi 2846 . . . . . . . . . . . . . . . . . . . . . . . 24 (ยฌ ๐‘˜ โˆˆ ๐ด โ†’ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1) โˆˆ โ„‚)
9288, 91pm2.61d1 180 . . . . . . . . . . . . . . . . . . . . . . 23 (๐œ‘ โ†’ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1) โˆˆ โ„‚)
93 eqid 2736 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1)) = (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))
9493fvmpt2 6956 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘˜ โˆˆ โ„ค โˆง if(๐‘˜ โˆˆ ๐ด, ๐ต, 1) โˆˆ โ„‚) โ†’ ((๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))โ€˜๐‘˜) = if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))
9584, 92, 94syl2anr 597 . . . . . . . . . . . . . . . . . . . . . 22 ((๐œ‘ โˆง ๐‘˜ โˆˆ ๐‘) โ†’ ((๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))โ€˜๐‘˜) = if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))
9682, 95eqtr4d 2779 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง ๐‘˜ โˆˆ ๐‘) โ†’ (๐นโ€˜๐‘˜) = ((๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))โ€˜๐‘˜))
9781, 96sylan2br 595 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ (๐นโ€˜๐‘˜) = ((๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))โ€˜๐‘˜))
9897ralrimiva 3141 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)(๐นโ€˜๐‘˜) = ((๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))โ€˜๐‘˜))
99 nffvmpt1 6850 . . . . . . . . . . . . . . . . . . . . 21 โ„ฒ๐‘˜((๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))โ€˜๐‘ง)
10099nfeq2 2922 . . . . . . . . . . . . . . . . . . . 20 โ„ฒ๐‘˜(๐นโ€˜๐‘ง) = ((๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))โ€˜๐‘ง)
101 fveq2 6839 . . . . . . . . . . . . . . . . . . . . 21 (๐‘˜ = ๐‘ง โ†’ (๐นโ€˜๐‘˜) = (๐นโ€˜๐‘ง))
102 fveq2 6839 . . . . . . . . . . . . . . . . . . . . 21 (๐‘˜ = ๐‘ง โ†’ ((๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))โ€˜๐‘˜) = ((๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))โ€˜๐‘ง))
103101, 102eqeq12d 2752 . . . . . . . . . . . . . . . . . . . 20 (๐‘˜ = ๐‘ง โ†’ ((๐นโ€˜๐‘˜) = ((๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))โ€˜๐‘˜) โ†” (๐นโ€˜๐‘ง) = ((๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))โ€˜๐‘ง)))
104100, 103rspc 3567 . . . . . . . . . . . . . . . . . . 19 (๐‘ง โˆˆ (โ„คโ‰ฅโ€˜๐‘€) โ†’ (โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)(๐นโ€˜๐‘˜) = ((๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))โ€˜๐‘˜) โ†’ (๐นโ€˜๐‘ง) = ((๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))โ€˜๐‘ง)))
10598, 104mpan9 507 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ๐‘ง โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ (๐นโ€˜๐‘ง) = ((๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))โ€˜๐‘ง))
10680, 105sylan2 593 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘€) โˆง ๐‘ง โˆˆ (โ„คโ‰ฅโ€˜๐‘›))) โ†’ (๐นโ€˜๐‘ง) = ((๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))โ€˜๐‘ง))
107106anassrs 468 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โˆง ๐‘ง โˆˆ (โ„คโ‰ฅโ€˜๐‘›)) โ†’ (๐นโ€˜๐‘ง) = ((๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))โ€˜๐‘ง))
10878, 107seqfeq 13925 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ seq๐‘›( ยท , ๐น) = seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))))
109108breq1d 5113 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ (seq๐‘›( ยท , ๐น) โ‡ ๐‘ฆ โ†” seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฆ))
110109anbi2d 629 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ ((๐‘ฆ โ‰  0 โˆง seq๐‘›( ยท , ๐น) โ‡ ๐‘ฆ) โ†” (๐‘ฆ โ‰  0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฆ)))
111110exbidv 1924 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ (โˆƒ๐‘ฆ(๐‘ฆ โ‰  0 โˆง seq๐‘›( ยท , ๐น) โ‡ ๐‘ฆ) โ†” โˆƒ๐‘ฆ(๐‘ฆ โ‰  0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฆ)))
11276, 111sylan2b 594 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘› โˆˆ ๐‘) โ†’ (โˆƒ๐‘ฆ(๐‘ฆ โ‰  0 โˆง seq๐‘›( ยท , ๐น) โ‡ ๐‘ฆ) โ†” โˆƒ๐‘ฆ(๐‘ฆ โ‰  0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฆ)))
113112rexbidva 3171 . . . . . . . . . 10 (๐œ‘ โ†’ (โˆƒ๐‘› โˆˆ ๐‘ โˆƒ๐‘ฆ(๐‘ฆ โ‰  0 โˆง seq๐‘›( ยท , ๐น) โ‡ ๐‘ฆ) โ†” โˆƒ๐‘› โˆˆ ๐‘ โˆƒ๐‘ฆ(๐‘ฆ โ‰  0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฆ)))
11475, 113mpbid 231 . . . . . . . . 9 (๐œ‘ โ†’ โˆƒ๐‘› โˆˆ ๐‘ โˆƒ๐‘ฆ(๐‘ฆ โ‰  0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฆ))
115114adantr 481 . . . . . . . 8 ((๐œ‘ โˆง seq๐‘€( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฅ) โ†’ โˆƒ๐‘› โˆˆ ๐‘ โˆƒ๐‘ฆ(๐‘ฆ โ‰  0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฆ))
116 simpr 485 . . . . . . . 8 ((๐œ‘ โˆง seq๐‘€( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฅ) โ†’ seq๐‘€( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฅ)
117 fveq2 6839 . . . . . . . . . . . 12 (๐‘š = ๐‘€ โ†’ (โ„คโ‰ฅโ€˜๐‘š) = (โ„คโ‰ฅโ€˜๐‘€))
118117, 24eqtr4di 2794 . . . . . . . . . . 11 (๐‘š = ๐‘€ โ†’ (โ„คโ‰ฅโ€˜๐‘š) = ๐‘)
119118sseq2d 3974 . . . . . . . . . 10 (๐‘š = ๐‘€ โ†’ (๐ด โŠ† (โ„คโ‰ฅโ€˜๐‘š) โ†” ๐ด โŠ† ๐‘))
120118rexeqdv 3312 . . . . . . . . . 10 (๐‘š = ๐‘€ โ†’ (โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ โ‰  0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฆ) โ†” โˆƒ๐‘› โˆˆ ๐‘ โˆƒ๐‘ฆ(๐‘ฆ โ‰  0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฆ)))
121 seqeq1 13901 . . . . . . . . . . 11 (๐‘š = ๐‘€ โ†’ seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) = seq๐‘€( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))))
122121breq1d 5113 . . . . . . . . . 10 (๐‘š = ๐‘€ โ†’ (seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฅ โ†” seq๐‘€( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฅ))
123119, 120, 1223anbi123d 1436 . . . . . . . . 9 (๐‘š = ๐‘€ โ†’ ((๐ด โŠ† (โ„คโ‰ฅโ€˜๐‘š) โˆง โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ โ‰  0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฆ) โˆง seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฅ) โ†” (๐ด โŠ† ๐‘ โˆง โˆƒ๐‘› โˆˆ ๐‘ โˆƒ๐‘ฆ(๐‘ฆ โ‰  0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฆ) โˆง seq๐‘€( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฅ)))
124123rspcev 3579 . . . . . . . 8 ((๐‘€ โˆˆ โ„ค โˆง (๐ด โŠ† ๐‘ โˆง โˆƒ๐‘› โˆˆ ๐‘ โˆƒ๐‘ฆ(๐‘ฆ โ‰  0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฆ) โˆง seq๐‘€( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฅ)) โ†’ โˆƒ๐‘š โˆˆ โ„ค (๐ด โŠ† (โ„คโ‰ฅโ€˜๐‘š) โˆง โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ โ‰  0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฆ) โˆง seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฅ))
12573, 74, 115, 116, 124syl13anc 1372 . . . . . . 7 ((๐œ‘ โˆง seq๐‘€( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฅ) โ†’ โˆƒ๐‘š โˆˆ โ„ค (๐ด โŠ† (โ„คโ‰ฅโ€˜๐‘š) โˆง โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ โ‰  0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฆ) โˆง seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฅ))
126125orcd 871 . . . . . 6 ((๐œ‘ โˆง seq๐‘€( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฅ) โ†’ (โˆƒ๐‘š โˆˆ โ„ค (๐ด โŠ† (โ„คโ‰ฅโ€˜๐‘š) โˆง โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ โ‰  0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฆ) โˆง seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฅ) โˆจ โˆƒ๐‘š โˆˆ โ„• โˆƒ๐‘“(๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด โˆง ๐‘ฅ = (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ต))โ€˜๐‘š))))
127126ex 413 . . . . 5 (๐œ‘ โ†’ (seq๐‘€( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฅ โ†’ (โˆƒ๐‘š โˆˆ โ„ค (๐ด โŠ† (โ„คโ‰ฅโ€˜๐‘š) โˆง โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ โ‰  0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฆ) โˆง seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฅ) โˆจ โˆƒ๐‘š โˆˆ โ„• โˆƒ๐‘“(๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด โˆง ๐‘ฅ = (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ต))โ€˜๐‘š)))))
12872, 127impbid 211 . . . 4 (๐œ‘ โ†’ ((โˆƒ๐‘š โˆˆ โ„ค (๐ด โŠ† (โ„คโ‰ฅโ€˜๐‘š) โˆง โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ โ‰  0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฆ) โˆง seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฅ) โˆจ โˆƒ๐‘š โˆˆ โ„• โˆƒ๐‘“(๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด โˆง ๐‘ฅ = (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ต))โ€˜๐‘š))) โ†” seq๐‘€( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฅ))
12995, 82eqtr4d 2779 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ ๐‘) โ†’ ((๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))โ€˜๐‘˜) = (๐นโ€˜๐‘˜))
13081, 129sylan2br 595 . . . . . . . 8 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ ((๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))โ€˜๐‘˜) = (๐นโ€˜๐‘˜))
131130ralrimiva 3141 . . . . . . 7 (๐œ‘ โ†’ โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)((๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))โ€˜๐‘˜) = (๐นโ€˜๐‘˜))
13299nfeq1 2920 . . . . . . . 8 โ„ฒ๐‘˜((๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))โ€˜๐‘ง) = (๐นโ€˜๐‘ง)
133102, 101eqeq12d 2752 . . . . . . . 8 (๐‘˜ = ๐‘ง โ†’ (((๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))โ€˜๐‘˜) = (๐นโ€˜๐‘˜) โ†” ((๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))โ€˜๐‘ง) = (๐นโ€˜๐‘ง)))
134132, 133rspc 3567 . . . . . . 7 (๐‘ง โˆˆ (โ„คโ‰ฅโ€˜๐‘€) โ†’ (โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)((๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))โ€˜๐‘˜) = (๐นโ€˜๐‘˜) โ†’ ((๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))โ€˜๐‘ง) = (๐นโ€˜๐‘ง)))
135131, 134mpan9 507 . . . . . 6 ((๐œ‘ โˆง ๐‘ง โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ ((๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))โ€˜๐‘ง) = (๐นโ€˜๐‘ง))
13620, 135seqfeq 13925 . . . . 5 (๐œ‘ โ†’ seq๐‘€( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) = seq๐‘€( ยท , ๐น))
137136breq1d 5113 . . . 4 (๐œ‘ โ†’ (seq๐‘€( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฅ โ†” seq๐‘€( ยท , ๐น) โ‡ ๐‘ฅ))
138128, 137bitrd 278 . . 3 (๐œ‘ โ†’ ((โˆƒ๐‘š โˆˆ โ„ค (๐ด โŠ† (โ„คโ‰ฅโ€˜๐‘š) โˆง โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ โ‰  0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฆ) โˆง seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฅ) โˆจ โˆƒ๐‘š โˆˆ โ„• โˆƒ๐‘“(๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด โˆง ๐‘ฅ = (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ต))โ€˜๐‘š))) โ†” seq๐‘€( ยท , ๐น) โ‡ ๐‘ฅ))
139138iotabidv 6477 . 2 (๐œ‘ โ†’ (โ„ฉ๐‘ฅ(โˆƒ๐‘š โˆˆ โ„ค (๐ด โŠ† (โ„คโ‰ฅโ€˜๐‘š) โˆง โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ โ‰  0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฆ) โˆง seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฅ) โˆจ โˆƒ๐‘š โˆˆ โ„• โˆƒ๐‘“(๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด โˆง ๐‘ฅ = (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ต))โ€˜๐‘š)))) = (โ„ฉ๐‘ฅseq๐‘€( ยท , ๐น) โ‡ ๐‘ฅ))
140 df-prod 15781 . 2 โˆ๐‘˜ โˆˆ ๐ด ๐ต = (โ„ฉ๐‘ฅ(โˆƒ๐‘š โˆˆ โ„ค (๐ด โŠ† (โ„คโ‰ฅโ€˜๐‘š) โˆง โˆƒ๐‘› โˆˆ (โ„คโ‰ฅโ€˜๐‘š)โˆƒ๐‘ฆ(๐‘ฆ โ‰  0 โˆง seq๐‘›( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฆ) โˆง seq๐‘š( ยท , (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))) โ‡ ๐‘ฅ) โˆจ โˆƒ๐‘š โˆˆ โ„• โˆƒ๐‘“(๐‘“:(1...๐‘š)โ€“1-1-ontoโ†’๐ด โˆง ๐‘ฅ = (seq1( ยท , (๐‘› โˆˆ โ„• โ†ฆ โฆ‹(๐‘“โ€˜๐‘›) / ๐‘˜โฆŒ๐ต))โ€˜๐‘š))))
141 df-fv 6501 . 2 ( โ‡ โ€˜seq๐‘€( ยท , ๐น)) = (โ„ฉ๐‘ฅseq๐‘€( ยท , ๐น) โ‡ ๐‘ฅ)
142139, 140, 1413eqtr4g 2801 1 (๐œ‘ โ†’ โˆ๐‘˜ โˆˆ ๐ด ๐ต = ( โ‡ โ€˜seq๐‘€( ยท , ๐น)))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 396   โˆจ wo 845   โˆง w3a 1087   = wceq 1541  โˆƒwex 1781   โˆˆ wcel 2106   โ‰  wne 2941  โˆ€wral 3062  โˆƒwrex 3071  โฆ‹csb 3853   โŠ† wss 3908  ifcif 4484   class class class wbr 5103   โ†ฆ cmpt 5186   Or wor 5542  โ„ฉcio 6443  โ€“1-1-ontoโ†’wf1o 6492  โ€˜cfv 6493   Isom wiso 6494  (class class class)co 7353   โ‰ˆ cen 8876  Fincfn 8879  โ„‚cc 11045  โ„cr 11046  0cc0 11047  1c1 11048   ยท cmul 11052   < clt 11185  โ„•cn 12149  โ„คcz 12495  โ„คโ‰ฅcuz 12759  ...cfz 13416  seqcseq 13898  โ™ฏchash 14222   โ‡ cli 15358  โˆcprod 15780
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5240  ax-sep 5254  ax-nul 5261  ax-pow 5318  ax-pr 5382  ax-un 7668  ax-inf2 9573  ax-cnex 11103  ax-resscn 11104  ax-1cn 11105  ax-icn 11106  ax-addcl 11107  ax-addrcl 11108  ax-mulcl 11109  ax-mulrcl 11110  ax-mulcom 11111  ax-addass 11112  ax-mulass 11113  ax-distr 11114  ax-i2m1 11115  ax-1ne0 11116  ax-1rid 11117  ax-rnegex 11118  ax-rrecex 11119  ax-cnre 11120  ax-pre-lttri 11121  ax-pre-lttrn 11122  ax-pre-ltadd 11123  ax-pre-mulgt0 11124
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3351  df-reu 3352  df-rab 3406  df-v 3445  df-sbc 3738  df-csb 3854  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4281  df-if 4485  df-pw 4560  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4864  df-int 4906  df-iun 4954  df-br 5104  df-opab 5166  df-mpt 5187  df-tr 5221  df-id 5529  df-eprel 5535  df-po 5543  df-so 5544  df-fr 5586  df-se 5587  df-we 5588  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6251  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6445  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-isom 6502  df-riota 7309  df-ov 7356  df-oprab 7357  df-mpo 7358  df-om 7799  df-1st 7917  df-2nd 7918  df-frecs 8208  df-wrecs 8239  df-recs 8313  df-rdg 8352  df-1o 8408  df-er 8644  df-en 8880  df-dom 8881  df-sdom 8882  df-fin 8883  df-oi 9442  df-card 9871  df-pnf 11187  df-mnf 11188  df-xr 11189  df-ltxr 11190  df-le 11191  df-sub 11383  df-neg 11384  df-div 11809  df-nn 12150  df-2 12212  df-n0 12410  df-z 12496  df-uz 12760  df-rp 12908  df-fz 13417  df-fzo 13560  df-seq 13899  df-exp 13960  df-hash 14223  df-cj 14976  df-re 14977  df-im 14978  df-sqrt 15112  df-abs 15113  df-clim 15362  df-prod 15781
This theorem is referenced by:  iprod  15813  zprodn0  15814  prodss  15822
  Copyright terms: Public domain W3C validator