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

Theorem prodmolem2a 15896
Description: Lemma for prodmo 15898. (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 13956 . . . . . . . . . . 11 (๐œ‘ โ†’ (1...๐‘) โˆˆ Fin)
6 prodmolem2.8 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘“:(1...๐‘)โ€“1-1-ontoโ†’๐ด)
75, 6hasheqf1od 14330 . . . . . . . . . 10 (๐œ‘ โ†’ (โ™ฏโ€˜(1...๐‘)) = (โ™ฏโ€˜๐ด))
8 prodmolem2.5 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘ โˆˆ โ„•)
98nnnn0d 12548 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘ โˆˆ โ„•0)
10 hashfz1 14323 . . . . . . . . . . 11 (๐‘ โˆˆ โ„•0 โ†’ (โ™ฏโ€˜(1...๐‘)) = ๐‘)
119, 10syl 17 . . . . . . . . . 10 (๐œ‘ โ†’ (โ™ฏโ€˜(1...๐‘)) = ๐‘)
127, 11eqtr3d 2769 . . . . . . . . 9 (๐œ‘ โ†’ (โ™ฏโ€˜๐ด) = ๐‘)
1312oveq2d 7430 . . . . . . . 8 (๐œ‘ โ†’ (1...(โ™ฏโ€˜๐ด)) = (1...๐‘))
14 isoeq4 7322 . . . . . . . 8 ((1...(โ™ฏโ€˜๐ด)) = (1...๐‘) โ†’ (๐พ Isom < , < ((1...(โ™ฏโ€˜๐ด)), ๐ด) โ†” ๐พ Isom < , < ((1...๐‘), ๐ด)))
1513, 14syl 17 . . . . . . 7 (๐œ‘ โ†’ (๐พ Isom < , < ((1...(โ™ฏโ€˜๐ด)), ๐ด) โ†” ๐พ Isom < , < ((1...๐‘), ๐ด)))
164, 15mpbid 231 . . . . . 6 (๐œ‘ โ†’ ๐พ Isom < , < ((1...๐‘), ๐ด))
17 isof1o 7325 . . . . . 6 (๐พ Isom < , < ((1...๐‘), ๐ด) โ†’ ๐พ:(1...๐‘)โ€“1-1-ontoโ†’๐ด)
18 f1of 6833 . . . . . 6 (๐พ:(1...๐‘)โ€“1-1-ontoโ†’๐ด โ†’ ๐พ:(1...๐‘)โŸถ๐ด)
1916, 17, 183syl 18 . . . . 5 (๐œ‘ โ†’ ๐พ:(1...๐‘)โŸถ๐ด)
20 nnuz 12881 . . . . . . 7 โ„• = (โ„คโ‰ฅโ€˜1)
218, 20eleqtrdi 2838 . . . . . 6 (๐œ‘ โ†’ ๐‘ โˆˆ (โ„คโ‰ฅโ€˜1))
22 eluzfz2 13527 . . . . . 6 (๐‘ โˆˆ (โ„คโ‰ฅโ€˜1) โ†’ ๐‘ โˆˆ (1...๐‘))
2321, 22syl 17 . . . . 5 (๐œ‘ โ†’ ๐‘ โˆˆ (1...๐‘))
2419, 23ffvelcdmd 7089 . . . 4 (๐œ‘ โ†’ (๐พโ€˜๐‘) โˆˆ ๐ด)
253, 24sseldd 3979 . . 3 (๐œ‘ โ†’ (๐พโ€˜๐‘) โˆˆ (โ„คโ‰ฅโ€˜๐‘€))
263sselda 3978 . . . . . 6 ((๐œ‘ โˆง ๐‘— โˆˆ ๐ด) โ†’ ๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘€))
2716, 17syl 17 . . . . . . . . 9 (๐œ‘ โ†’ ๐พ:(1...๐‘)โ€“1-1-ontoโ†’๐ด)
28 f1ocnvfv2 7280 . . . . . . . . 9 ((๐พ:(1...๐‘)โ€“1-1-ontoโ†’๐ด โˆง ๐‘— โˆˆ ๐ด) โ†’ (๐พโ€˜(โ—ก๐พโ€˜๐‘—)) = ๐‘—)
2927, 28sylan 579 . . . . . . . 8 ((๐œ‘ โˆง ๐‘— โˆˆ ๐ด) โ†’ (๐พโ€˜(โ—ก๐พโ€˜๐‘—)) = ๐‘—)
30 f1ocnv 6845 . . . . . . . . . . . 12 (๐พ:(1...๐‘)โ€“1-1-ontoโ†’๐ด โ†’ โ—ก๐พ:๐ดโ€“1-1-ontoโ†’(1...๐‘))
31 f1of 6833 . . . . . . . . . . . 12 (โ—ก๐พ:๐ดโ€“1-1-ontoโ†’(1...๐‘) โ†’ โ—ก๐พ:๐ดโŸถ(1...๐‘))
3227, 30, 313syl 18 . . . . . . . . . . 11 (๐œ‘ โ†’ โ—ก๐พ:๐ดโŸถ(1...๐‘))
3332ffvelcdmda 7088 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘— โˆˆ ๐ด) โ†’ (โ—ก๐พโ€˜๐‘—) โˆˆ (1...๐‘))
34 elfzle2 13523 . . . . . . . . . 10 ((โ—ก๐พโ€˜๐‘—) โˆˆ (1...๐‘) โ†’ (โ—ก๐พโ€˜๐‘—) โ‰ค ๐‘)
3533, 34syl 17 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘— โˆˆ ๐ด) โ†’ (โ—ก๐พโ€˜๐‘—) โ‰ค ๐‘)
3616adantr 480 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘— โˆˆ ๐ด) โ†’ ๐พ Isom < , < ((1...๐‘), ๐ด))
37 fzssuz 13560 . . . . . . . . . . . . 13 (1...๐‘) โІ (โ„คโ‰ฅโ€˜1)
38 uzssz 12859 . . . . . . . . . . . . . 14 (โ„คโ‰ฅโ€˜1) โІ โ„ค
39 zssre 12581 . . . . . . . . . . . . . 14 โ„ค โІ โ„
4038, 39sstri 3987 . . . . . . . . . . . . 13 (โ„คโ‰ฅโ€˜1) โІ โ„
4137, 40sstri 3987 . . . . . . . . . . . 12 (1...๐‘) โІ โ„
42 ressxr 11274 . . . . . . . . . . . 12 โ„ โІ โ„*
4341, 42sstri 3987 . . . . . . . . . . 11 (1...๐‘) โІ โ„*
4443a1i 11 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘— โˆˆ ๐ด) โ†’ (1...๐‘) โІ โ„*)
45 uzssz 12859 . . . . . . . . . . . . . 14 (โ„คโ‰ฅโ€˜๐‘€) โІ โ„ค
4645, 39sstri 3987 . . . . . . . . . . . . 13 (โ„คโ‰ฅโ€˜๐‘€) โІ โ„
4746, 42sstri 3987 . . . . . . . . . . . 12 (โ„คโ‰ฅโ€˜๐‘€) โІ โ„*
483, 47sstrdi 3990 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐ด โІ โ„*)
4948adantr 480 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘— โˆˆ ๐ด) โ†’ ๐ด โІ โ„*)
5023adantr 480 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘— โˆˆ ๐ด) โ†’ ๐‘ โˆˆ (1...๐‘))
51 leisorel 14439 . . . . . . . . . 10 ((๐พ Isom < , < ((1...๐‘), ๐ด) โˆง ((1...๐‘) โІ โ„* โˆง ๐ด โІ โ„*) โˆง ((โ—ก๐พโ€˜๐‘—) โˆˆ (1...๐‘) โˆง ๐‘ โˆˆ (1...๐‘))) โ†’ ((โ—ก๐พโ€˜๐‘—) โ‰ค ๐‘ โ†” (๐พโ€˜(โ—ก๐พโ€˜๐‘—)) โ‰ค (๐พโ€˜๐‘)))
5236, 44, 49, 33, 50, 51syl122anc 1377 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘— โˆˆ ๐ด) โ†’ ((โ—ก๐พโ€˜๐‘—) โ‰ค ๐‘ โ†” (๐พโ€˜(โ—ก๐พโ€˜๐‘—)) โ‰ค (๐พโ€˜๐‘)))
5335, 52mpbid 231 . . . . . . . 8 ((๐œ‘ โˆง ๐‘— โˆˆ ๐ด) โ†’ (๐พโ€˜(โ—ก๐พโ€˜๐‘—)) โ‰ค (๐พโ€˜๐‘))
5429, 53eqbrtrrd 5166 . . . . . . 7 ((๐œ‘ โˆง ๐‘— โˆˆ ๐ด) โ†’ ๐‘— โ‰ค (๐พโ€˜๐‘))
553, 45sstrdi 3990 . . . . . . . . 9 (๐œ‘ โ†’ ๐ด โІ โ„ค)
5655sselda 3978 . . . . . . . 8 ((๐œ‘ โˆง ๐‘— โˆˆ ๐ด) โ†’ ๐‘— โˆˆ โ„ค)
57 eluzelz 12848 . . . . . . . . . 10 ((๐พโ€˜๐‘) โˆˆ (โ„คโ‰ฅโ€˜๐‘€) โ†’ (๐พโ€˜๐‘) โˆˆ โ„ค)
5825, 57syl 17 . . . . . . . . 9 (๐œ‘ โ†’ (๐พโ€˜๐‘) โˆˆ โ„ค)
5958adantr 480 . . . . . . . 8 ((๐œ‘ โˆง ๐‘— โˆˆ ๐ด) โ†’ (๐พโ€˜๐‘) โˆˆ โ„ค)
60 eluz 12852 . . . . . . . 8 ((๐‘— โˆˆ โ„ค โˆง (๐พโ€˜๐‘) โˆˆ โ„ค) โ†’ ((๐พโ€˜๐‘) โˆˆ (โ„คโ‰ฅโ€˜๐‘—) โ†” ๐‘— โ‰ค (๐พโ€˜๐‘)))
6156, 59, 60syl2anc 583 . . . . . . 7 ((๐œ‘ โˆง ๐‘— โˆˆ ๐ด) โ†’ ((๐พโ€˜๐‘) โˆˆ (โ„คโ‰ฅโ€˜๐‘—) โ†” ๐‘— โ‰ค (๐พโ€˜๐‘)))
6254, 61mpbird 257 . . . . . 6 ((๐œ‘ โˆง ๐‘— โˆˆ ๐ด) โ†’ (๐พโ€˜๐‘) โˆˆ (โ„คโ‰ฅโ€˜๐‘—))
63 elfzuzb 13513 . . . . . 6 (๐‘— โˆˆ (๐‘€...(๐พโ€˜๐‘)) โ†” (๐‘— โˆˆ (โ„คโ‰ฅโ€˜๐‘€) โˆง (๐พโ€˜๐‘) โˆˆ (โ„คโ‰ฅโ€˜๐‘—)))
6426, 62, 63sylanbrc 582 . . . . 5 ((๐œ‘ โˆง ๐‘— โˆˆ ๐ด) โ†’ ๐‘— โˆˆ (๐‘€...(๐พโ€˜๐‘)))
6564ex 412 . . . 4 (๐œ‘ โ†’ (๐‘— โˆˆ ๐ด โ†’ ๐‘— โˆˆ (๐‘€...(๐พโ€˜๐‘))))
6665ssrdv 3984 . . 3 (๐œ‘ โ†’ ๐ด โІ (๐‘€...(๐พโ€˜๐‘)))
671, 2, 25, 66fprodcvg 15892 . 2 (๐œ‘ โ†’ seq๐‘€( ยท , ๐น) โ‡ (seq๐‘€( ยท , ๐น)โ€˜(๐พโ€˜๐‘)))
68 mullid 11229 . . . . 5 (๐‘š โˆˆ โ„‚ โ†’ (1 ยท ๐‘š) = ๐‘š)
6968adantl 481 . . . 4 ((๐œ‘ โˆง ๐‘š โˆˆ โ„‚) โ†’ (1 ยท ๐‘š) = ๐‘š)
70 mulrid 11228 . . . . 5 (๐‘š โˆˆ โ„‚ โ†’ (๐‘š ยท 1) = ๐‘š)
7170adantl 481 . . . 4 ((๐œ‘ โˆง ๐‘š โˆˆ โ„‚) โ†’ (๐‘š ยท 1) = ๐‘š)
72 mulcl 11208 . . . . 5 ((๐‘š โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ โ„‚) โ†’ (๐‘š ยท ๐‘ฅ) โˆˆ โ„‚)
7372adantl 481 . . . 4 ((๐œ‘ โˆง (๐‘š โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ โ„‚)) โ†’ (๐‘š ยท ๐‘ฅ) โˆˆ โ„‚)
74 1cnd 11225 . . . 4 (๐œ‘ โ†’ 1 โˆˆ โ„‚)
7523, 13eleqtrrd 2831 . . . 4 (๐œ‘ โ†’ ๐‘ โˆˆ (1...(โ™ฏโ€˜๐ด)))
76 iftrue 4530 . . . . . . . . . . 11 (๐‘˜ โˆˆ ๐ด โ†’ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1) = ๐ต)
7776adantl 481 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘˜ โˆˆ ๐ด) โ†’ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1) = ๐ต)
7877, 2eqeltrd 2828 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘˜ โˆˆ ๐ด) โ†’ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1) โˆˆ โ„‚)
7978ex 412 . . . . . . . 8 (๐œ‘ โ†’ (๐‘˜ โˆˆ ๐ด โ†’ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1) โˆˆ โ„‚))
80 iffalse 4533 . . . . . . . . 9 (ยฌ ๐‘˜ โˆˆ ๐ด โ†’ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1) = 1)
81 ax-1cn 11182 . . . . . . . . 9 1 โˆˆ โ„‚
8280, 81eqeltrdi 2836 . . . . . . . 8 (ยฌ ๐‘˜ โˆˆ ๐ด โ†’ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1) โˆˆ โ„‚)
8379, 82pm2.61d1 180 . . . . . . 7 (๐œ‘ โ†’ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1) โˆˆ โ„‚)
8483adantr 480 . . . . . 6 ((๐œ‘ โˆง ๐‘˜ โˆˆ โ„ค) โ†’ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1) โˆˆ โ„‚)
8584, 1fmptd 7118 . . . . 5 (๐œ‘ โ†’ ๐น:โ„คโŸถโ„‚)
86 elfzelz 13519 . . . . 5 (๐‘š โˆˆ (๐‘€...(๐พโ€˜(โ™ฏโ€˜๐ด))) โ†’ ๐‘š โˆˆ โ„ค)
87 ffvelcdm 7085 . . . . 5 ((๐น:โ„คโŸถโ„‚ โˆง ๐‘š โˆˆ โ„ค) โ†’ (๐นโ€˜๐‘š) โˆˆ โ„‚)
8885, 86, 87syl2an 595 . . . 4 ((๐œ‘ โˆง ๐‘š โˆˆ (๐‘€...(๐พโ€˜(โ™ฏโ€˜๐ด)))) โ†’ (๐นโ€˜๐‘š) โˆˆ โ„‚)
89 fveqeq2 6900 . . . . . 6 (๐‘˜ = ๐‘š โ†’ ((๐นโ€˜๐‘˜) = 1 โ†” (๐นโ€˜๐‘š) = 1))
90 eldifi 4122 . . . . . . . . 9 (๐‘˜ โˆˆ ((๐‘€...(๐พโ€˜(โ™ฏโ€˜๐ด))) โˆ– ๐ด) โ†’ ๐‘˜ โˆˆ (๐‘€...(๐พโ€˜(โ™ฏโ€˜๐ด))))
9190elfzelzd 13520 . . . . . . . 8 (๐‘˜ โˆˆ ((๐‘€...(๐พโ€˜(โ™ฏโ€˜๐ด))) โˆ– ๐ด) โ†’ ๐‘˜ โˆˆ โ„ค)
92 eldifn 4123 . . . . . . . . . 10 (๐‘˜ โˆˆ ((๐‘€...(๐พโ€˜(โ™ฏโ€˜๐ด))) โˆ– ๐ด) โ†’ ยฌ ๐‘˜ โˆˆ ๐ด)
9392, 80syl 17 . . . . . . . . 9 (๐‘˜ โˆˆ ((๐‘€...(๐พโ€˜(โ™ฏโ€˜๐ด))) โˆ– ๐ด) โ†’ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1) = 1)
9493, 81eqeltrdi 2836 . . . . . . . 8 (๐‘˜ โˆˆ ((๐‘€...(๐พโ€˜(โ™ฏโ€˜๐ด))) โˆ– ๐ด) โ†’ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1) โˆˆ โ„‚)
951fvmpt2 7010 . . . . . . . 8 ((๐‘˜ โˆˆ โ„ค โˆง if(๐‘˜ โˆˆ ๐ด, ๐ต, 1) โˆˆ โ„‚) โ†’ (๐นโ€˜๐‘˜) = if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))
9691, 94, 95syl2anc 583 . . . . . . 7 (๐‘˜ โˆˆ ((๐‘€...(๐พโ€˜(โ™ฏโ€˜๐ด))) โˆ– ๐ด) โ†’ (๐นโ€˜๐‘˜) = if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))
9796, 93eqtrd 2767 . . . . . 6 (๐‘˜ โˆˆ ((๐‘€...(๐พโ€˜(โ™ฏโ€˜๐ด))) โˆ– ๐ด) โ†’ (๐นโ€˜๐‘˜) = 1)
9889, 97vtoclga 3561 . . . . 5 (๐‘š โˆˆ ((๐‘€...(๐พโ€˜(โ™ฏโ€˜๐ด))) โˆ– ๐ด) โ†’ (๐นโ€˜๐‘š) = 1)
9998adantl 481 . . . 4 ((๐œ‘ โˆง ๐‘š โˆˆ ((๐‘€...(๐พโ€˜(โ™ฏโ€˜๐ด))) โˆ– ๐ด)) โ†’ (๐นโ€˜๐‘š) = 1)
100 isof1o 7325 . . . . . . . 8 (๐พ Isom < , < ((1...(โ™ฏโ€˜๐ด)), ๐ด) โ†’ ๐พ:(1...(โ™ฏโ€˜๐ด))โ€“1-1-ontoโ†’๐ด)
101 f1of 6833 . . . . . . . 8 (๐พ:(1...(โ™ฏโ€˜๐ด))โ€“1-1-ontoโ†’๐ด โ†’ ๐พ:(1...(โ™ฏโ€˜๐ด))โŸถ๐ด)
1024, 100, 1013syl 18 . . . . . . 7 (๐œ‘ โ†’ ๐พ:(1...(โ™ฏโ€˜๐ด))โŸถ๐ด)
103102ffvelcdmda 7088 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...(โ™ฏโ€˜๐ด))) โ†’ (๐พโ€˜๐‘ฅ) โˆˆ ๐ด)
104103iftrued 4532 . . . . 5 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...(โ™ฏโ€˜๐ด))) โ†’ if((๐พโ€˜๐‘ฅ) โˆˆ ๐ด, โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต, 1) = โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต)
10555adantr 480 . . . . . . 7 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...(โ™ฏโ€˜๐ด))) โ†’ ๐ด โІ โ„ค)
106105, 103sseldd 3979 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...(โ™ฏโ€˜๐ด))) โ†’ (๐พโ€˜๐‘ฅ) โˆˆ โ„ค)
107 nfv 1910 . . . . . . . . 9 โ„ฒ๐‘˜๐œ‘
108 nfv 1910 . . . . . . . . . . 11 โ„ฒ๐‘˜(๐พโ€˜๐‘ฅ) โˆˆ ๐ด
109 nfcsb1v 3914 . . . . . . . . . . 11 โ„ฒ๐‘˜โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต
110 nfcv 2898 . . . . . . . . . . 11 โ„ฒ๐‘˜1
111108, 109, 110nfif 4554 . . . . . . . . . 10 โ„ฒ๐‘˜if((๐พโ€˜๐‘ฅ) โˆˆ ๐ด, โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต, 1)
112111nfel1 2914 . . . . . . . . 9 โ„ฒ๐‘˜if((๐พโ€˜๐‘ฅ) โˆˆ ๐ด, โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต, 1) โˆˆ โ„‚
113107, 112nfim 1892 . . . . . . . 8 โ„ฒ๐‘˜(๐œ‘ โ†’ if((๐พโ€˜๐‘ฅ) โˆˆ ๐ด, โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต, 1) โˆˆ โ„‚)
114 fvex 6904 . . . . . . . 8 (๐พโ€˜๐‘ฅ) โˆˆ V
115 eleq1 2816 . . . . . . . . . . 11 (๐‘˜ = (๐พโ€˜๐‘ฅ) โ†’ (๐‘˜ โˆˆ ๐ด โ†” (๐พโ€˜๐‘ฅ) โˆˆ ๐ด))
116 csbeq1a 3903 . . . . . . . . . . 11 (๐‘˜ = (๐พโ€˜๐‘ฅ) โ†’ ๐ต = โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต)
117115, 116ifbieq1d 4548 . . . . . . . . . 10 (๐‘˜ = (๐พโ€˜๐‘ฅ) โ†’ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1) = if((๐พโ€˜๐‘ฅ) โˆˆ ๐ด, โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต, 1))
118117eleq1d 2813 . . . . . . . . 9 (๐‘˜ = (๐พโ€˜๐‘ฅ) โ†’ (if(๐‘˜ โˆˆ ๐ด, ๐ต, 1) โˆˆ โ„‚ โ†” if((๐พโ€˜๐‘ฅ) โˆˆ ๐ด, โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต, 1) โˆˆ โ„‚))
119118imbi2d 340 . . . . . . . 8 (๐‘˜ = (๐พโ€˜๐‘ฅ) โ†’ ((๐œ‘ โ†’ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1) โˆˆ โ„‚) โ†” (๐œ‘ โ†’ if((๐พโ€˜๐‘ฅ) โˆˆ ๐ด, โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต, 1) โˆˆ โ„‚)))
120113, 114, 119, 83vtoclf 3547 . . . . . . 7 (๐œ‘ โ†’ if((๐พโ€˜๐‘ฅ) โˆˆ ๐ด, โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต, 1) โˆˆ โ„‚)
121120adantr 480 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...(โ™ฏโ€˜๐ด))) โ†’ if((๐พโ€˜๐‘ฅ) โˆˆ ๐ด, โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต, 1) โˆˆ โ„‚)
122 eleq1 2816 . . . . . . . 8 (๐‘› = (๐พโ€˜๐‘ฅ) โ†’ (๐‘› โˆˆ ๐ด โ†” (๐พโ€˜๐‘ฅ) โˆˆ ๐ด))
123 csbeq1 3892 . . . . . . . 8 (๐‘› = (๐พโ€˜๐‘ฅ) โ†’ โฆ‹๐‘› / ๐‘˜โฆŒ๐ต = โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต)
124122, 123ifbieq1d 4548 . . . . . . 7 (๐‘› = (๐พโ€˜๐‘ฅ) โ†’ if(๐‘› โˆˆ ๐ด, โฆ‹๐‘› / ๐‘˜โฆŒ๐ต, 1) = if((๐พโ€˜๐‘ฅ) โˆˆ ๐ด, โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต, 1))
125 nfcv 2898 . . . . . . . . 9 โ„ฒ๐‘›if(๐‘˜ โˆˆ ๐ด, ๐ต, 1)
126 nfv 1910 . . . . . . . . . 10 โ„ฒ๐‘˜ ๐‘› โˆˆ ๐ด
127 nfcsb1v 3914 . . . . . . . . . 10 โ„ฒ๐‘˜โฆ‹๐‘› / ๐‘˜โฆŒ๐ต
128126, 127, 110nfif 4554 . . . . . . . . 9 โ„ฒ๐‘˜if(๐‘› โˆˆ ๐ด, โฆ‹๐‘› / ๐‘˜โฆŒ๐ต, 1)
129 eleq1 2816 . . . . . . . . . 10 (๐‘˜ = ๐‘› โ†’ (๐‘˜ โˆˆ ๐ด โ†” ๐‘› โˆˆ ๐ด))
130 csbeq1a 3903 . . . . . . . . . 10 (๐‘˜ = ๐‘› โ†’ ๐ต = โฆ‹๐‘› / ๐‘˜โฆŒ๐ต)
131129, 130ifbieq1d 4548 . . . . . . . . 9 (๐‘˜ = ๐‘› โ†’ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1) = if(๐‘› โˆˆ ๐ด, โฆ‹๐‘› / ๐‘˜โฆŒ๐ต, 1))
132125, 128, 131cbvmpt 5253 . . . . . . . 8 (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1)) = (๐‘› โˆˆ โ„ค โ†ฆ if(๐‘› โˆˆ ๐ด, โฆ‹๐‘› / ๐‘˜โฆŒ๐ต, 1))
1331, 132eqtri 2755 . . . . . . 7 ๐น = (๐‘› โˆˆ โ„ค โ†ฆ if(๐‘› โˆˆ ๐ด, โฆ‹๐‘› / ๐‘˜โฆŒ๐ต, 1))
134124, 133fvmptg 6997 . . . . . 6 (((๐พโ€˜๐‘ฅ) โˆˆ โ„ค โˆง if((๐พโ€˜๐‘ฅ) โˆˆ ๐ด, โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต, 1) โˆˆ โ„‚) โ†’ (๐นโ€˜(๐พโ€˜๐‘ฅ)) = if((๐พโ€˜๐‘ฅ) โˆˆ ๐ด, โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต, 1))
135106, 121, 134syl2anc 583 . . . . 5 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...(โ™ฏโ€˜๐ด))) โ†’ (๐นโ€˜(๐พโ€˜๐‘ฅ)) = if((๐พโ€˜๐‘ฅ) โˆˆ ๐ด, โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต, 1))
136 elfznn 13548 . . . . . 6 (๐‘ฅ โˆˆ (1...(โ™ฏโ€˜๐ด)) โ†’ ๐‘ฅ โˆˆ โ„•)
137104, 121eqeltrrd 2829 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...(โ™ฏโ€˜๐ด))) โ†’ โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต โˆˆ โ„‚)
138 fveq2 6891 . . . . . . . 8 (๐‘— = ๐‘ฅ โ†’ (๐พโ€˜๐‘—) = (๐พโ€˜๐‘ฅ))
139138csbeq1d 3893 . . . . . . 7 (๐‘— = ๐‘ฅ โ†’ โฆ‹(๐พโ€˜๐‘—) / ๐‘˜โฆŒ๐ต = โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต)
140 prodmolem2.4 . . . . . . 7 ๐ป = (๐‘— โˆˆ โ„• โ†ฆ โฆ‹(๐พโ€˜๐‘—) / ๐‘˜โฆŒ๐ต)
141139, 140fvmptg 6997 . . . . . 6 ((๐‘ฅ โˆˆ โ„• โˆง โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต โˆˆ โ„‚) โ†’ (๐ปโ€˜๐‘ฅ) = โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต)
142136, 137, 141syl2an2 685 . . . . 5 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...(โ™ฏโ€˜๐ด))) โ†’ (๐ปโ€˜๐‘ฅ) = โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต)
143104, 135, 1423eqtr4rd 2778 . . . 4 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...(โ™ฏโ€˜๐ด))) โ†’ (๐ปโ€˜๐‘ฅ) = (๐นโ€˜(๐พโ€˜๐‘ฅ)))
14469, 71, 73, 74, 4, 75, 3, 88, 99, 143seqcoll 14443 . . 3 (๐œ‘ โ†’ (seq๐‘€( ยท , ๐น)โ€˜(๐พโ€˜๐‘)) = (seq1( ยท , ๐ป)โ€˜๐‘))
145 prodmo.3 . . . 4 ๐บ = (๐‘— โˆˆ โ„• โ†ฆ โฆ‹(๐‘“โ€˜๐‘—) / ๐‘˜โฆŒ๐ต)
1468, 8jca 511 . . . 4 (๐œ‘ โ†’ (๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•))
1471, 2, 145, 140, 146, 6, 27prodmolem3 15895 . . 3 (๐œ‘ โ†’ (seq1( ยท , ๐บ)โ€˜๐‘) = (seq1( ยท , ๐ป)โ€˜๐‘))
148144, 147eqtr4d 2770 . 2 (๐œ‘ โ†’ (seq๐‘€( ยท , ๐น)โ€˜(๐พโ€˜๐‘)) = (seq1( ยท , ๐บ)โ€˜๐‘))
14967, 148breqtrd 5168 1 (๐œ‘ โ†’ seq๐‘€( ยท , ๐น) โ‡ (seq1( ยท , ๐บ)โ€˜๐‘))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 395   = wceq 1534   โˆˆ wcel 2099  โฆ‹csb 3889   โˆ– cdif 3941   โІ wss 3944  ifcif 4524   class class class wbr 5142   โ†ฆ cmpt 5225  โ—กccnv 5671  โŸถwf 6538  โ€“1-1-ontoโ†’wf1o 6541  โ€˜cfv 6542   Isom wiso 6543  (class class class)co 7414  Fincfn 8953  โ„‚cc 11122  โ„cr 11123  1c1 11125   ยท cmul 11129  โ„*cxr 11263   < clt 11264   โ‰ค cle 11265  โ„•cn 12228  โ„•0cn0 12488  โ„คcz 12574  โ„คโ‰ฅcuz 12838  ...cfz 13502  seqcseq 13984  โ™ฏchash 14307   โ‡ cli 15446
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7732  ax-inf2 9650  ax-cnex 11180  ax-resscn 11181  ax-1cn 11182  ax-icn 11183  ax-addcl 11184  ax-addrcl 11185  ax-mulcl 11186  ax-mulrcl 11187  ax-mulcom 11188  ax-addass 11189  ax-mulass 11190  ax-distr 11191  ax-i2m1 11192  ax-1ne0 11193  ax-1rid 11194  ax-rnegex 11195  ax-rrecex 11196  ax-cnre 11197  ax-pre-lttri 11198  ax-pre-lttrn 11199  ax-pre-ltadd 11200  ax-pre-mulgt0 11201
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7863  df-1st 7985  df-2nd 7986  df-frecs 8278  df-wrecs 8309  df-recs 8383  df-rdg 8422  df-1o 8478  df-er 8716  df-en 8954  df-dom 8955  df-sdom 8956  df-fin 8957  df-card 9948  df-pnf 11266  df-mnf 11267  df-xr 11268  df-ltxr 11269  df-le 11270  df-sub 11462  df-neg 11463  df-div 11888  df-nn 12229  df-2 12291  df-n0 12489  df-z 12575  df-uz 12839  df-rp 12993  df-fz 13503  df-fzo 13646  df-seq 13985  df-exp 14045  df-hash 14308  df-cj 15064  df-re 15065  df-im 15066  df-sqrt 15200  df-abs 15201  df-clim 15450
This theorem is referenced by:  prodmolem2  15897  zprod  15899
  Copyright terms: Public domain W3C validator