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

Theorem prodmolem2a 15905
Description: Lemma for prodmo 15907. (Contributed by Scott Fenton, 4-Dec-2017.)
Hypotheses
Ref Expression
prodmo.1 ๐น = (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))
prodmo.2 ((๐œ‘ โˆง ๐‘˜ โˆˆ ๐ด) โ†’ ๐ต โˆˆ โ„‚)
prodmo.3 ๐บ = (๐‘— โˆˆ โ„• โ†ฆ โฆ‹(๐‘“โ€˜๐‘—) / ๐‘˜โฆŒ๐ต)
prodmolem2.4 ๐ป = (๐‘— โˆˆ โ„• โ†ฆ โฆ‹(๐พโ€˜๐‘—) / ๐‘˜โฆŒ๐ต)
prodmolem2.5 (๐œ‘ โ†’ ๐‘ โˆˆ โ„•)
prodmolem2.6 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„ค)
prodmolem2.7 (๐œ‘ โ†’ ๐ด โІ (โ„คโ‰ฅโ€˜๐‘€))
prodmolem2.8 (๐œ‘ โ†’ ๐‘“:(1...๐‘)โ€“1-1-ontoโ†’๐ด)
prodmolem2.9 (๐œ‘ โ†’ ๐พ Isom < , < ((1...(โ™ฏโ€˜๐ด)), ๐ด))
Assertion
Ref Expression
prodmolem2a (๐œ‘ โ†’ seq๐‘€( ยท , ๐น) โ‡ (seq1( ยท , ๐บ)โ€˜๐‘))
Distinct variable groups:   ๐ด,๐‘˜   ๐‘˜,๐น   ๐œ‘,๐‘˜   ๐ด,๐‘—   ๐ต,๐‘—   ๐‘“,๐‘—,๐‘˜   ๐‘—,๐บ   ๐‘—,๐‘˜,๐œ‘   ๐‘—,๐พ,๐‘˜   ๐‘—,๐‘€,๐‘˜   ๐‘—,๐‘,๐‘˜
Allowed substitution hints:   ๐œ‘(๐‘“)   ๐ด(๐‘“)   ๐ต(๐‘“,๐‘˜)   ๐น(๐‘“,๐‘—)   ๐บ(๐‘“,๐‘˜)   ๐ป(๐‘“,๐‘—,๐‘˜)   ๐พ(๐‘“)   ๐‘€(๐‘“)   ๐‘(๐‘“)

Proof of Theorem prodmolem2a
Dummy variables ๐‘› ๐‘š ๐‘ฅ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 prodmo.1 . . 3 ๐น = (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))
2 prodmo.2 . . 3 ((๐œ‘ โˆง ๐‘˜ โˆˆ ๐ด) โ†’ ๐ต โˆˆ โ„‚)
3 prodmolem2.7 . . . 4 (๐œ‘ โ†’ ๐ด โІ (โ„คโ‰ฅโ€˜๐‘€))
4 prodmolem2.9 . . . . . . 7 (๐œ‘ โ†’ ๐พ Isom < , < ((1...(โ™ฏโ€˜๐ด)), ๐ด))
5 fzfid 13965 . . . . . . . . . . 11 (๐œ‘ โ†’ (1...๐‘) โˆˆ Fin)
6 prodmolem2.8 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘“:(1...๐‘)โ€“1-1-ontoโ†’๐ด)
75, 6hasheqf1od 14339 . . . . . . . . . 10 (๐œ‘ โ†’ (โ™ฏโ€˜(1...๐‘)) = (โ™ฏโ€˜๐ด))
8 prodmolem2.5 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘ โˆˆ โ„•)
98nnnn0d 12557 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘ โˆˆ โ„•0)
10 hashfz1 14332 . . . . . . . . . . 11 (๐‘ โˆˆ โ„•0 โ†’ (โ™ฏโ€˜(1...๐‘)) = ๐‘)
119, 10syl 17 . . . . . . . . . 10 (๐œ‘ โ†’ (โ™ฏโ€˜(1...๐‘)) = ๐‘)
127, 11eqtr3d 2767 . . . . . . . . 9 (๐œ‘ โ†’ (โ™ฏโ€˜๐ด) = ๐‘)
1312oveq2d 7429 . . . . . . . 8 (๐œ‘ โ†’ (1...(โ™ฏโ€˜๐ด)) = (1...๐‘))
14 isoeq4 7321 . . . . . . . 8 ((1...(โ™ฏโ€˜๐ด)) = (1...๐‘) โ†’ (๐พ Isom < , < ((1...(โ™ฏโ€˜๐ด)), ๐ด) โ†” ๐พ Isom < , < ((1...๐‘), ๐ด)))
1513, 14syl 17 . . . . . . 7 (๐œ‘ โ†’ (๐พ Isom < , < ((1...(โ™ฏโ€˜๐ด)), ๐ด) โ†” ๐พ Isom < , < ((1...๐‘), ๐ด)))
164, 15mpbid 231 . . . . . 6 (๐œ‘ โ†’ ๐พ Isom < , < ((1...๐‘), ๐ด))
17 isof1o 7324 . . . . . 6 (๐พ Isom < , < ((1...๐‘), ๐ด) โ†’ ๐พ:(1...๐‘)โ€“1-1-ontoโ†’๐ด)
18 f1of 6832 . . . . . 6 (๐พ:(1...๐‘)โ€“1-1-ontoโ†’๐ด โ†’ ๐พ:(1...๐‘)โŸถ๐ด)
1916, 17, 183syl 18 . . . . 5 (๐œ‘ โ†’ ๐พ:(1...๐‘)โŸถ๐ด)
20 nnuz 12890 . . . . . . 7 โ„• = (โ„คโ‰ฅโ€˜1)
218, 20eleqtrdi 2835 . . . . . 6 (๐œ‘ โ†’ ๐‘ โˆˆ (โ„คโ‰ฅโ€˜1))
22 eluzfz2 13536 . . . . . 6 (๐‘ โˆˆ (โ„คโ‰ฅโ€˜1) โ†’ ๐‘ โˆˆ (1...๐‘))
2321, 22syl 17 . . . . 5 (๐œ‘ โ†’ ๐‘ โˆˆ (1...๐‘))
2419, 23ffvelcdmd 7088 . . . 4 (๐œ‘ โ†’ (๐พโ€˜๐‘) โˆˆ ๐ด)
253, 24sseldd 3974 . . 3 (๐œ‘ โ†’ (๐พโ€˜๐‘) โˆˆ (โ„คโ‰ฅโ€˜๐‘€))
263sselda 3973 . . . . . 6 ((๐œ‘ โˆง ๐‘— โˆˆ ๐ด) โ†’ ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘€))
2716, 17syl 17 . . . . . . . . 9 (๐œ‘ โ†’ ๐พ:(1...๐‘)โ€“1-1-ontoโ†’๐ด)
28 f1ocnvfv2 7280 . . . . . . . . 9 ((๐พ:(1...๐‘)โ€“1-1-ontoโ†’๐ด โˆง ๐‘— โˆˆ ๐ด) โ†’ (๐พโ€˜(โ—ก๐พโ€˜๐‘—)) = ๐‘—)
2927, 28sylan 578 . . . . . . . 8 ((๐œ‘ โˆง ๐‘— โˆˆ ๐ด) โ†’ (๐พโ€˜(โ—ก๐พโ€˜๐‘—)) = ๐‘—)
30 f1ocnv 6844 . . . . . . . . . . . 12 (๐พ:(1...๐‘)โ€“1-1-ontoโ†’๐ด โ†’ โ—ก๐พ:๐ดโ€“1-1-ontoโ†’(1...๐‘))
31 f1of 6832 . . . . . . . . . . . 12 (โ—ก๐พ:๐ดโ€“1-1-ontoโ†’(1...๐‘) โ†’ โ—ก๐พ:๐ดโŸถ(1...๐‘))
3227, 30, 313syl 18 . . . . . . . . . . 11 (๐œ‘ โ†’ โ—ก๐พ:๐ดโŸถ(1...๐‘))
3332ffvelcdmda 7087 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘— โˆˆ ๐ด) โ†’ (โ—ก๐พโ€˜๐‘—) โˆˆ (1...๐‘))
34 elfzle2 13532 . . . . . . . . . 10 ((โ—ก๐พโ€˜๐‘—) โˆˆ (1...๐‘) โ†’ (โ—ก๐พโ€˜๐‘—) โ‰ค ๐‘)
3533, 34syl 17 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘— โˆˆ ๐ด) โ†’ (โ—ก๐พโ€˜๐‘—) โ‰ค ๐‘)
3616adantr 479 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘— โˆˆ ๐ด) โ†’ ๐พ Isom < , < ((1...๐‘), ๐ด))
37 fzssuz 13569 . . . . . . . . . . . . 13 (1...๐‘) โІ (โ„คโ‰ฅโ€˜1)
38 uzssz 12868 . . . . . . . . . . . . . 14 (โ„คโ‰ฅโ€˜1) โІ โ„ค
39 zssre 12590 . . . . . . . . . . . . . 14 โ„ค โІ โ„
4038, 39sstri 3983 . . . . . . . . . . . . 13 (โ„คโ‰ฅโ€˜1) โІ โ„
4137, 40sstri 3983 . . . . . . . . . . . 12 (1...๐‘) โІ โ„
42 ressxr 11283 . . . . . . . . . . . 12 โ„ โІ โ„*
4341, 42sstri 3983 . . . . . . . . . . 11 (1...๐‘) โІ โ„*
4443a1i 11 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘— โˆˆ ๐ด) โ†’ (1...๐‘) โІ โ„*)
45 uzssz 12868 . . . . . . . . . . . . . 14 (โ„คโ‰ฅโ€˜๐‘€) โІ โ„ค
4645, 39sstri 3983 . . . . . . . . . . . . 13 (โ„คโ‰ฅโ€˜๐‘€) โІ โ„
4746, 42sstri 3983 . . . . . . . . . . . 12 (โ„คโ‰ฅโ€˜๐‘€) โІ โ„*
483, 47sstrdi 3986 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐ด โІ โ„*)
4948adantr 479 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘— โˆˆ ๐ด) โ†’ ๐ด โІ โ„*)
5023adantr 479 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘— โˆˆ ๐ด) โ†’ ๐‘ โˆˆ (1...๐‘))
51 leisorel 14448 . . . . . . . . . 10 ((๐พ Isom < , < ((1...๐‘), ๐ด) โˆง ((1...๐‘) โІ โ„* โˆง ๐ด โІ โ„*) โˆง ((โ—ก๐พโ€˜๐‘—) โˆˆ (1...๐‘) โˆง ๐‘ โˆˆ (1...๐‘))) โ†’ ((โ—ก๐พโ€˜๐‘—) โ‰ค ๐‘ โ†” (๐พโ€˜(โ—ก๐พโ€˜๐‘—)) โ‰ค (๐พโ€˜๐‘)))
5236, 44, 49, 33, 50, 51syl122anc 1376 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘— โˆˆ ๐ด) โ†’ ((โ—ก๐พโ€˜๐‘—) โ‰ค ๐‘ โ†” (๐พโ€˜(โ—ก๐พโ€˜๐‘—)) โ‰ค (๐พโ€˜๐‘)))
5335, 52mpbid 231 . . . . . . . 8 ((๐œ‘ โˆง ๐‘— โˆˆ ๐ด) โ†’ (๐พโ€˜(โ—ก๐พโ€˜๐‘—)) โ‰ค (๐พโ€˜๐‘))
5429, 53eqbrtrrd 5168 . . . . . . 7 ((๐œ‘ โˆง ๐‘— โˆˆ ๐ด) โ†’ ๐‘— โ‰ค (๐พโ€˜๐‘))
553, 45sstrdi 3986 . . . . . . . . 9 (๐œ‘ โ†’ ๐ด โІ โ„ค)
5655sselda 3973 . . . . . . . 8 ((๐œ‘ โˆง ๐‘— โˆˆ ๐ด) โ†’ ๐‘— โˆˆ โ„ค)
57 eluzelz 12857 . . . . . . . . . 10 ((๐พโ€˜๐‘) โˆˆ (โ„คโ‰ฅโ€˜๐‘€) โ†’ (๐พโ€˜๐‘) โˆˆ โ„ค)
5825, 57syl 17 . . . . . . . . 9 (๐œ‘ โ†’ (๐พโ€˜๐‘) โˆˆ โ„ค)
5958adantr 479 . . . . . . . 8 ((๐œ‘ โˆง ๐‘— โˆˆ ๐ด) โ†’ (๐พโ€˜๐‘) โˆˆ โ„ค)
60 eluz 12861 . . . . . . . 8 ((๐‘— โˆˆ โ„ค โˆง (๐พโ€˜๐‘) โˆˆ โ„ค) โ†’ ((๐พโ€˜๐‘) โˆˆ (โ„คโ‰ฅโ€˜๐‘—) โ†” ๐‘— โ‰ค (๐พโ€˜๐‘)))
6156, 59, 60syl2anc 582 . . . . . . 7 ((๐œ‘ โˆง ๐‘— โˆˆ ๐ด) โ†’ ((๐พโ€˜๐‘) โˆˆ (โ„คโ‰ฅโ€˜๐‘—) โ†” ๐‘— โ‰ค (๐พโ€˜๐‘)))
6254, 61mpbird 256 . . . . . 6 ((๐œ‘ โˆง ๐‘— โˆˆ ๐ด) โ†’ (๐พโ€˜๐‘) โˆˆ (โ„คโ‰ฅโ€˜๐‘—))
63 elfzuzb 13522 . . . . . 6 (๐‘— โˆˆ (๐‘€...(๐พโ€˜๐‘)) โ†” (๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘€) โˆง (๐พโ€˜๐‘) โˆˆ (โ„คโ‰ฅโ€˜๐‘—)))
6426, 62, 63sylanbrc 581 . . . . 5 ((๐œ‘ โˆง ๐‘— โˆˆ ๐ด) โ†’ ๐‘— โˆˆ (๐‘€...(๐พโ€˜๐‘)))
6564ex 411 . . . 4 (๐œ‘ โ†’ (๐‘— โˆˆ ๐ด โ†’ ๐‘— โˆˆ (๐‘€...(๐พโ€˜๐‘))))
6665ssrdv 3979 . . 3 (๐œ‘ โ†’ ๐ด โІ (๐‘€...(๐พโ€˜๐‘)))
671, 2, 25, 66fprodcvg 15901 . 2 (๐œ‘ โ†’ seq๐‘€( ยท , ๐น) โ‡ (seq๐‘€( ยท , ๐น)โ€˜(๐พโ€˜๐‘)))
68 mullid 11238 . . . . 5 (๐‘š โˆˆ โ„‚ โ†’ (1 ยท ๐‘š) = ๐‘š)
6968adantl 480 . . . 4 ((๐œ‘ โˆง ๐‘š โˆˆ โ„‚) โ†’ (1 ยท ๐‘š) = ๐‘š)
70 mulrid 11237 . . . . 5 (๐‘š โˆˆ โ„‚ โ†’ (๐‘š ยท 1) = ๐‘š)
7170adantl 480 . . . 4 ((๐œ‘ โˆง ๐‘š โˆˆ โ„‚) โ†’ (๐‘š ยท 1) = ๐‘š)
72 mulcl 11217 . . . . 5 ((๐‘š โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ โ„‚) โ†’ (๐‘š ยท ๐‘ฅ) โˆˆ โ„‚)
7372adantl 480 . . . 4 ((๐œ‘ โˆง (๐‘š โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ โ„‚)) โ†’ (๐‘š ยท ๐‘ฅ) โˆˆ โ„‚)
74 1cnd 11234 . . . 4 (๐œ‘ โ†’ 1 โˆˆ โ„‚)
7523, 13eleqtrrd 2828 . . . 4 (๐œ‘ โ†’ ๐‘ โˆˆ (1...(โ™ฏโ€˜๐ด)))
76 iftrue 4531 . . . . . . . . . . 11 (๐‘˜ โˆˆ ๐ด โ†’ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1) = ๐ต)
7776adantl 480 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ ๐ด) โ†’ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1) = ๐ต)
7877, 2eqeltrd 2825 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ ๐ด) โ†’ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1) โˆˆ โ„‚)
7978ex 411 . . . . . . . 8 (๐œ‘ โ†’ (๐‘˜ โˆˆ ๐ด โ†’ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1) โˆˆ โ„‚))
80 iffalse 4534 . . . . . . . . 9 (ยฌ ๐‘˜ โˆˆ ๐ด โ†’ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1) = 1)
81 ax-1cn 11191 . . . . . . . . 9 1 โˆˆ โ„‚
8280, 81eqeltrdi 2833 . . . . . . . 8 (ยฌ ๐‘˜ โˆˆ ๐ด โ†’ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1) โˆˆ โ„‚)
8379, 82pm2.61d1 180 . . . . . . 7 (๐œ‘ โ†’ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1) โˆˆ โ„‚)
8483adantr 479 . . . . . 6 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„ค) โ†’ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1) โˆˆ โ„‚)
8584, 1fmptd 7117 . . . . 5 (๐œ‘ โ†’ ๐น:โ„คโŸถโ„‚)
86 elfzelz 13528 . . . . 5 (๐‘š โˆˆ (๐‘€...(๐พโ€˜(โ™ฏโ€˜๐ด))) โ†’ ๐‘š โˆˆ โ„ค)
87 ffvelcdm 7084 . . . . 5 ((๐น:โ„คโŸถโ„‚ โˆง ๐‘š โˆˆ โ„ค) โ†’ (๐นโ€˜๐‘š) โˆˆ โ„‚)
8885, 86, 87syl2an 594 . . . 4 ((๐œ‘ โˆง ๐‘š โˆˆ (๐‘€...(๐พโ€˜(โ™ฏโ€˜๐ด)))) โ†’ (๐นโ€˜๐‘š) โˆˆ โ„‚)
89 fveqeq2 6899 . . . . . 6 (๐‘˜ = ๐‘š โ†’ ((๐นโ€˜๐‘˜) = 1 โ†” (๐นโ€˜๐‘š) = 1))
90 eldifi 4120 . . . . . . . . 9 (๐‘˜ โˆˆ ((๐‘€...(๐พโ€˜(โ™ฏโ€˜๐ด))) โˆ– ๐ด) โ†’ ๐‘˜ โˆˆ (๐‘€...(๐พโ€˜(โ™ฏโ€˜๐ด))))
9190elfzelzd 13529 . . . . . . . 8 (๐‘˜ โˆˆ ((๐‘€...(๐พโ€˜(โ™ฏโ€˜๐ด))) โˆ– ๐ด) โ†’ ๐‘˜ โˆˆ โ„ค)
92 eldifn 4121 . . . . . . . . . 10 (๐‘˜ โˆˆ ((๐‘€...(๐พโ€˜(โ™ฏโ€˜๐ด))) โˆ– ๐ด) โ†’ ยฌ ๐‘˜ โˆˆ ๐ด)
9392, 80syl 17 . . . . . . . . 9 (๐‘˜ โˆˆ ((๐‘€...(๐พโ€˜(โ™ฏโ€˜๐ด))) โˆ– ๐ด) โ†’ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1) = 1)
9493, 81eqeltrdi 2833 . . . . . . . 8 (๐‘˜ โˆˆ ((๐‘€...(๐พโ€˜(โ™ฏโ€˜๐ด))) โˆ– ๐ด) โ†’ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1) โˆˆ โ„‚)
951fvmpt2 7009 . . . . . . . 8 ((๐‘˜ โˆˆ โ„ค โˆง if(๐‘˜ โˆˆ ๐ด, ๐ต, 1) โˆˆ โ„‚) โ†’ (๐นโ€˜๐‘˜) = if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))
9691, 94, 95syl2anc 582 . . . . . . 7 (๐‘˜ โˆˆ ((๐‘€...(๐พโ€˜(โ™ฏโ€˜๐ด))) โˆ– ๐ด) โ†’ (๐นโ€˜๐‘˜) = if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))
9796, 93eqtrd 2765 . . . . . 6 (๐‘˜ โˆˆ ((๐‘€...(๐พโ€˜(โ™ฏโ€˜๐ด))) โˆ– ๐ด) โ†’ (๐นโ€˜๐‘˜) = 1)
9889, 97vtoclga 3557 . . . . 5 (๐‘š โˆˆ ((๐‘€...(๐พโ€˜(โ™ฏโ€˜๐ด))) โˆ– ๐ด) โ†’ (๐นโ€˜๐‘š) = 1)
9998adantl 480 . . . 4 ((๐œ‘ โˆง ๐‘š โˆˆ ((๐‘€...(๐พโ€˜(โ™ฏโ€˜๐ด))) โˆ– ๐ด)) โ†’ (๐นโ€˜๐‘š) = 1)
100 isof1o 7324 . . . . . . . 8 (๐พ Isom < , < ((1...(โ™ฏโ€˜๐ด)), ๐ด) โ†’ ๐พ:(1...(โ™ฏโ€˜๐ด))โ€“1-1-ontoโ†’๐ด)
101 f1of 6832 . . . . . . . 8 (๐พ:(1...(โ™ฏโ€˜๐ด))โ€“1-1-ontoโ†’๐ด โ†’ ๐พ:(1...(โ™ฏโ€˜๐ด))โŸถ๐ด)
1024, 100, 1013syl 18 . . . . . . 7 (๐œ‘ โ†’ ๐พ:(1...(โ™ฏโ€˜๐ด))โŸถ๐ด)
103102ffvelcdmda 7087 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...(โ™ฏโ€˜๐ด))) โ†’ (๐พโ€˜๐‘ฅ) โˆˆ ๐ด)
104103iftrued 4533 . . . . 5 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...(โ™ฏโ€˜๐ด))) โ†’ if((๐พโ€˜๐‘ฅ) โˆˆ ๐ด, โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต, 1) = โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต)
10555adantr 479 . . . . . . 7 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...(โ™ฏโ€˜๐ด))) โ†’ ๐ด โІ โ„ค)
106105, 103sseldd 3974 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...(โ™ฏโ€˜๐ด))) โ†’ (๐พโ€˜๐‘ฅ) โˆˆ โ„ค)
107 nfv 1909 . . . . . . . . 9 โ„ฒ๐‘˜๐œ‘
108 nfv 1909 . . . . . . . . . . 11 โ„ฒ๐‘˜(๐พโ€˜๐‘ฅ) โˆˆ ๐ด
109 nfcsb1v 3911 . . . . . . . . . . 11 โ„ฒ๐‘˜โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต
110 nfcv 2892 . . . . . . . . . . 11 โ„ฒ๐‘˜1
111108, 109, 110nfif 4555 . . . . . . . . . 10 โ„ฒ๐‘˜if((๐พโ€˜๐‘ฅ) โˆˆ ๐ด, โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต, 1)
112111nfel1 2909 . . . . . . . . 9 โ„ฒ๐‘˜if((๐พโ€˜๐‘ฅ) โˆˆ ๐ด, โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต, 1) โˆˆ โ„‚
113107, 112nfim 1891 . . . . . . . 8 โ„ฒ๐‘˜(๐œ‘ โ†’ if((๐พโ€˜๐‘ฅ) โˆˆ ๐ด, โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต, 1) โˆˆ โ„‚)
114 fvex 6903 . . . . . . . 8 (๐พโ€˜๐‘ฅ) โˆˆ V
115 eleq1 2813 . . . . . . . . . . 11 (๐‘˜ = (๐พโ€˜๐‘ฅ) โ†’ (๐‘˜ โˆˆ ๐ด โ†” (๐พโ€˜๐‘ฅ) โˆˆ ๐ด))
116 csbeq1a 3900 . . . . . . . . . . 11 (๐‘˜ = (๐พโ€˜๐‘ฅ) โ†’ ๐ต = โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต)
117115, 116ifbieq1d 4549 . . . . . . . . . 10 (๐‘˜ = (๐พโ€˜๐‘ฅ) โ†’ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1) = if((๐พโ€˜๐‘ฅ) โˆˆ ๐ด, โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต, 1))
118117eleq1d 2810 . . . . . . . . 9 (๐‘˜ = (๐พโ€˜๐‘ฅ) โ†’ (if(๐‘˜ โˆˆ ๐ด, ๐ต, 1) โˆˆ โ„‚ โ†” if((๐พโ€˜๐‘ฅ) โˆˆ ๐ด, โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต, 1) โˆˆ โ„‚))
119118imbi2d 339 . . . . . . . 8 (๐‘˜ = (๐พโ€˜๐‘ฅ) โ†’ ((๐œ‘ โ†’ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1) โˆˆ โ„‚) โ†” (๐œ‘ โ†’ if((๐พโ€˜๐‘ฅ) โˆˆ ๐ด, โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต, 1) โˆˆ โ„‚)))
120113, 114, 119, 83vtoclf 3543 . . . . . . 7 (๐œ‘ โ†’ if((๐พโ€˜๐‘ฅ) โˆˆ ๐ด, โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต, 1) โˆˆ โ„‚)
121120adantr 479 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...(โ™ฏโ€˜๐ด))) โ†’ if((๐พโ€˜๐‘ฅ) โˆˆ ๐ด, โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต, 1) โˆˆ โ„‚)
122 eleq1 2813 . . . . . . . 8 (๐‘› = (๐พโ€˜๐‘ฅ) โ†’ (๐‘› โˆˆ ๐ด โ†” (๐พโ€˜๐‘ฅ) โˆˆ ๐ด))
123 csbeq1 3889 . . . . . . . 8 (๐‘› = (๐พโ€˜๐‘ฅ) โ†’ โฆ‹๐‘› / ๐‘˜โฆŒ๐ต = โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต)
124122, 123ifbieq1d 4549 . . . . . . 7 (๐‘› = (๐พโ€˜๐‘ฅ) โ†’ if(๐‘› โˆˆ ๐ด, โฆ‹๐‘› / ๐‘˜โฆŒ๐ต, 1) = if((๐พโ€˜๐‘ฅ) โˆˆ ๐ด, โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต, 1))
125 nfcv 2892 . . . . . . . . 9 โ„ฒ๐‘›if(๐‘˜ โˆˆ ๐ด, ๐ต, 1)
126 nfv 1909 . . . . . . . . . 10 โ„ฒ๐‘˜ ๐‘› โˆˆ ๐ด
127 nfcsb1v 3911 . . . . . . . . . 10 โ„ฒ๐‘˜โฆ‹๐‘› / ๐‘˜โฆŒ๐ต
128126, 127, 110nfif 4555 . . . . . . . . 9 โ„ฒ๐‘˜if(๐‘› โˆˆ ๐ด, โฆ‹๐‘› / ๐‘˜โฆŒ๐ต, 1)
129 eleq1 2813 . . . . . . . . . 10 (๐‘˜ = ๐‘› โ†’ (๐‘˜ โˆˆ ๐ด โ†” ๐‘› โˆˆ ๐ด))
130 csbeq1a 3900 . . . . . . . . . 10 (๐‘˜ = ๐‘› โ†’ ๐ต = โฆ‹๐‘› / ๐‘˜โฆŒ๐ต)
131129, 130ifbieq1d 4549 . . . . . . . . 9 (๐‘˜ = ๐‘› โ†’ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1) = if(๐‘› โˆˆ ๐ด, โฆ‹๐‘› / ๐‘˜โฆŒ๐ต, 1))
132125, 128, 131cbvmpt 5255 . . . . . . . 8 (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1)) = (๐‘› โˆˆ โ„ค โ†ฆ if(๐‘› โˆˆ ๐ด, โฆ‹๐‘› / ๐‘˜โฆŒ๐ต, 1))
1331, 132eqtri 2753 . . . . . . 7 ๐น = (๐‘› โˆˆ โ„ค โ†ฆ if(๐‘› โˆˆ ๐ด, โฆ‹๐‘› / ๐‘˜โฆŒ๐ต, 1))
134124, 133fvmptg 6996 . . . . . 6 (((๐พโ€˜๐‘ฅ) โˆˆ โ„ค โˆง if((๐พโ€˜๐‘ฅ) โˆˆ ๐ด, โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต, 1) โˆˆ โ„‚) โ†’ (๐นโ€˜(๐พโ€˜๐‘ฅ)) = if((๐พโ€˜๐‘ฅ) โˆˆ ๐ด, โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต, 1))
135106, 121, 134syl2anc 582 . . . . 5 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...(โ™ฏโ€˜๐ด))) โ†’ (๐นโ€˜(๐พโ€˜๐‘ฅ)) = if((๐พโ€˜๐‘ฅ) โˆˆ ๐ด, โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต, 1))
136 elfznn 13557 . . . . . 6 (๐‘ฅ โˆˆ (1...(โ™ฏโ€˜๐ด)) โ†’ ๐‘ฅ โˆˆ โ„•)
137104, 121eqeltrrd 2826 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...(โ™ฏโ€˜๐ด))) โ†’ โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต โˆˆ โ„‚)
138 fveq2 6890 . . . . . . . 8 (๐‘— = ๐‘ฅ โ†’ (๐พโ€˜๐‘—) = (๐พโ€˜๐‘ฅ))
139138csbeq1d 3890 . . . . . . 7 (๐‘— = ๐‘ฅ โ†’ โฆ‹(๐พโ€˜๐‘—) / ๐‘˜โฆŒ๐ต = โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต)
140 prodmolem2.4 . . . . . . 7 ๐ป = (๐‘— โˆˆ โ„• โ†ฆ โฆ‹(๐พโ€˜๐‘—) / ๐‘˜โฆŒ๐ต)
141139, 140fvmptg 6996 . . . . . 6 ((๐‘ฅ โˆˆ โ„• โˆง โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต โˆˆ โ„‚) โ†’ (๐ปโ€˜๐‘ฅ) = โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต)
142136, 137, 141syl2an2 684 . . . . 5 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...(โ™ฏโ€˜๐ด))) โ†’ (๐ปโ€˜๐‘ฅ) = โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต)
143104, 135, 1423eqtr4rd 2776 . . . 4 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...(โ™ฏโ€˜๐ด))) โ†’ (๐ปโ€˜๐‘ฅ) = (๐นโ€˜(๐พโ€˜๐‘ฅ)))
14469, 71, 73, 74, 4, 75, 3, 88, 99, 143seqcoll 14452 . . 3 (๐œ‘ โ†’ (seq๐‘€( ยท , ๐น)โ€˜(๐พโ€˜๐‘)) = (seq1( ยท , ๐ป)โ€˜๐‘))
145 prodmo.3 . . . 4 ๐บ = (๐‘— โˆˆ โ„• โ†ฆ โฆ‹(๐‘“โ€˜๐‘—) / ๐‘˜โฆŒ๐ต)
1468, 8jca 510 . . . 4 (๐œ‘ โ†’ (๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•))
1471, 2, 145, 140, 146, 6, 27prodmolem3 15904 . . 3 (๐œ‘ โ†’ (seq1( ยท , ๐บ)โ€˜๐‘) = (seq1( ยท , ๐ป)โ€˜๐‘))
148144, 147eqtr4d 2768 . 2 (๐œ‘ โ†’ (seq๐‘€( ยท , ๐น)โ€˜(๐พโ€˜๐‘)) = (seq1( ยท , ๐บ)โ€˜๐‘))
14967, 148breqtrd 5170 1 (๐œ‘ โ†’ seq๐‘€( ยท , ๐น) โ‡ (seq1( ยท , ๐บ)โ€˜๐‘))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 394   = wceq 1533   โˆˆ wcel 2098  โฆ‹csb 3886   โˆ– cdif 3938   โІ wss 3941  ifcif 4525   class class class wbr 5144   โ†ฆ cmpt 5227  โ—กccnv 5672  โŸถwf 6539  โ€“1-1-ontoโ†’wf1o 6542  โ€˜cfv 6543   Isom wiso 6544  (class class class)co 7413  Fincfn 8957  โ„‚cc 11131  โ„cr 11132  1c1 11134   ยท cmul 11138  โ„*cxr 11272   < clt 11273   โ‰ค cle 11274  โ„•cn 12237  โ„•0cn0 12497  โ„คcz 12583  โ„คโ‰ฅcuz 12847  ...cfz 13511  seqcseq 13993  โ™ฏchash 14316   โ‡ cli 15455
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5281  ax-sep 5295  ax-nul 5302  ax-pow 5360  ax-pr 5424  ax-un 7735  ax-inf2 9659  ax-cnex 11189  ax-resscn 11190  ax-1cn 11191  ax-icn 11192  ax-addcl 11193  ax-addrcl 11194  ax-mulcl 11195  ax-mulrcl 11196  ax-mulcom 11197  ax-addass 11198  ax-mulass 11199  ax-distr 11200  ax-i2m1 11201  ax-1ne0 11202  ax-1rid 11203  ax-rnegex 11204  ax-rrecex 11205  ax-cnre 11206  ax-pre-lttri 11207  ax-pre-lttrn 11208  ax-pre-ltadd 11209  ax-pre-mulgt0 11210
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-pss 3961  df-nul 4320  df-if 4526  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4905  df-int 4946  df-iun 4994  df-br 5145  df-opab 5207  df-mpt 5228  df-tr 5262  df-id 5571  df-eprel 5577  df-po 5585  df-so 5586  df-fr 5628  df-we 5630  df-xp 5679  df-rel 5680  df-cnv 5681  df-co 5682  df-dm 5683  df-rn 5684  df-res 5685  df-ima 5686  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7369  df-ov 7416  df-oprab 7417  df-mpo 7418  df-om 7866  df-1st 7987  df-2nd 7988  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-er 8718  df-en 8958  df-dom 8959  df-sdom 8960  df-fin 8961  df-card 9957  df-pnf 11275  df-mnf 11276  df-xr 11277  df-ltxr 11278  df-le 11279  df-sub 11471  df-neg 11472  df-div 11897  df-nn 12238  df-2 12300  df-n0 12498  df-z 12584  df-uz 12848  df-rp 13002  df-fz 13512  df-fzo 13655  df-seq 13994  df-exp 14054  df-hash 14317  df-cj 15073  df-re 15074  df-im 15075  df-sqrt 15209  df-abs 15210  df-clim 15459
This theorem is referenced by:  prodmolem2  15906  zprod  15908
  Copyright terms: Public domain W3C validator