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

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

Proof of Theorem prodmodclem2a
Dummy variables ๐‘ ๐‘š ๐‘ฅ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 prodmo.1 . . 3 ๐น = (๐‘˜ โˆˆ โ„ค โ†ฆ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1))
2 prodmo.2 . . 3 ((๐œ‘ โˆง ๐‘˜ โˆˆ ๐ด) โ†’ ๐ต โˆˆ โ„‚)
3 prodmodclem2a.dc . . 3 ((๐œ‘ โˆง ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ DECID ๐‘˜ โˆˆ ๐ด)
4 prodmolem2.7 . . . 4 (๐œ‘ โ†’ ๐ด โŠ† (โ„คโ‰ฅโ€˜๐‘€))
5 prodmolem2.9 . . . . . . 7 (๐œ‘ โ†’ ๐พ Isom < , < ((1...(โ™ฏโ€˜๐ด)), ๐ด))
6 1zzd 9279 . . . . . . . . . . . 12 (๐œ‘ โ†’ 1 โˆˆ โ„ค)
7 prodmolem2.5 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐‘ โˆˆ โ„•)
87nnzd 9373 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘ โˆˆ โ„ค)
96, 8fzfigd 10430 . . . . . . . . . . 11 (๐œ‘ โ†’ (1...๐‘) โˆˆ Fin)
10 prodmolem2.8 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘“:(1...๐‘)โ€“1-1-ontoโ†’๐ด)
119, 10fihasheqf1od 10768 . . . . . . . . . 10 (๐œ‘ โ†’ (โ™ฏโ€˜(1...๐‘)) = (โ™ฏโ€˜๐ด))
127nnnn0d 9228 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘ โˆˆ โ„•0)
13 hashfz1 10762 . . . . . . . . . . 11 (๐‘ โˆˆ โ„•0 โ†’ (โ™ฏโ€˜(1...๐‘)) = ๐‘)
1412, 13syl 14 . . . . . . . . . 10 (๐œ‘ โ†’ (โ™ฏโ€˜(1...๐‘)) = ๐‘)
1511, 14eqtr3d 2212 . . . . . . . . 9 (๐œ‘ โ†’ (โ™ฏโ€˜๐ด) = ๐‘)
1615oveq2d 5890 . . . . . . . 8 (๐œ‘ โ†’ (1...(โ™ฏโ€˜๐ด)) = (1...๐‘))
17 isoeq4 5804 . . . . . . . 8 ((1...(โ™ฏโ€˜๐ด)) = (1...๐‘) โ†’ (๐พ Isom < , < ((1...(โ™ฏโ€˜๐ด)), ๐ด) โ†” ๐พ Isom < , < ((1...๐‘), ๐ด)))
1816, 17syl 14 . . . . . . 7 (๐œ‘ โ†’ (๐พ Isom < , < ((1...(โ™ฏโ€˜๐ด)), ๐ด) โ†” ๐พ Isom < , < ((1...๐‘), ๐ด)))
195, 18mpbid 147 . . . . . 6 (๐œ‘ โ†’ ๐พ Isom < , < ((1...๐‘), ๐ด))
20 isof1o 5807 . . . . . 6 (๐พ Isom < , < ((1...๐‘), ๐ด) โ†’ ๐พ:(1...๐‘)โ€“1-1-ontoโ†’๐ด)
21 f1of 5461 . . . . . 6 (๐พ:(1...๐‘)โ€“1-1-ontoโ†’๐ด โ†’ ๐พ:(1...๐‘)โŸถ๐ด)
2219, 20, 213syl 17 . . . . 5 (๐œ‘ โ†’ ๐พ:(1...๐‘)โŸถ๐ด)
23 nnuz 9562 . . . . . . 7 โ„• = (โ„คโ‰ฅโ€˜1)
247, 23eleqtrdi 2270 . . . . . 6 (๐œ‘ โ†’ ๐‘ โˆˆ (โ„คโ‰ฅโ€˜1))
25 eluzfz2 10031 . . . . . 6 (๐‘ โˆˆ (โ„คโ‰ฅโ€˜1) โ†’ ๐‘ โˆˆ (1...๐‘))
2624, 25syl 14 . . . . 5 (๐œ‘ โ†’ ๐‘ โˆˆ (1...๐‘))
2722, 26ffvelcdmd 5652 . . . 4 (๐œ‘ โ†’ (๐พโ€˜๐‘) โˆˆ ๐ด)
284, 27sseldd 3156 . . 3 (๐œ‘ โ†’ (๐พโ€˜๐‘) โˆˆ (โ„คโ‰ฅโ€˜๐‘€))
294sselda 3155 . . . . . 6 ((๐œ‘ โˆง ๐‘ โˆˆ ๐ด) โ†’ ๐‘ โˆˆ (โ„คโ‰ฅโ€˜๐‘€))
3019, 20syl 14 . . . . . . . . 9 (๐œ‘ โ†’ ๐พ:(1...๐‘)โ€“1-1-ontoโ†’๐ด)
31 f1ocnvfv2 5778 . . . . . . . . 9 ((๐พ:(1...๐‘)โ€“1-1-ontoโ†’๐ด โˆง ๐‘ โˆˆ ๐ด) โ†’ (๐พโ€˜(โ—ก๐พโ€˜๐‘)) = ๐‘)
3230, 31sylan 283 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ โˆˆ ๐ด) โ†’ (๐พโ€˜(โ—ก๐พโ€˜๐‘)) = ๐‘)
33 f1ocnv 5474 . . . . . . . . . . . 12 (๐พ:(1...๐‘)โ€“1-1-ontoโ†’๐ด โ†’ โ—ก๐พ:๐ดโ€“1-1-ontoโ†’(1...๐‘))
34 f1of 5461 . . . . . . . . . . . 12 (โ—ก๐พ:๐ดโ€“1-1-ontoโ†’(1...๐‘) โ†’ โ—ก๐พ:๐ดโŸถ(1...๐‘))
3530, 33, 343syl 17 . . . . . . . . . . 11 (๐œ‘ โ†’ โ—ก๐พ:๐ดโŸถ(1...๐‘))
3635ffvelcdmda 5651 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ โˆˆ ๐ด) โ†’ (โ—ก๐พโ€˜๐‘) โˆˆ (1...๐‘))
37 elfzle2 10027 . . . . . . . . . 10 ((โ—ก๐พโ€˜๐‘) โˆˆ (1...๐‘) โ†’ (โ—ก๐พโ€˜๐‘) โ‰ค ๐‘)
3836, 37syl 14 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ โˆˆ ๐ด) โ†’ (โ—ก๐พโ€˜๐‘) โ‰ค ๐‘)
3919adantr 276 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ โˆˆ ๐ด) โ†’ ๐พ Isom < , < ((1...๐‘), ๐ด))
40 fzssuz 10064 . . . . . . . . . . . . 13 (1...๐‘) โŠ† (โ„คโ‰ฅโ€˜1)
41 uzssz 9546 . . . . . . . . . . . . . 14 (โ„คโ‰ฅโ€˜1) โŠ† โ„ค
42 zssre 9259 . . . . . . . . . . . . . 14 โ„ค โŠ† โ„
4341, 42sstri 3164 . . . . . . . . . . . . 13 (โ„คโ‰ฅโ€˜1) โŠ† โ„
4440, 43sstri 3164 . . . . . . . . . . . 12 (1...๐‘) โŠ† โ„
45 ressxr 8000 . . . . . . . . . . . 12 โ„ โŠ† โ„*
4644, 45sstri 3164 . . . . . . . . . . 11 (1...๐‘) โŠ† โ„*
4746a1i 9 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ โˆˆ ๐ด) โ†’ (1...๐‘) โŠ† โ„*)
48 uzssz 9546 . . . . . . . . . . . . . 14 (โ„คโ‰ฅโ€˜๐‘€) โŠ† โ„ค
4948, 42sstri 3164 . . . . . . . . . . . . 13 (โ„คโ‰ฅโ€˜๐‘€) โŠ† โ„
5049, 45sstri 3164 . . . . . . . . . . . 12 (โ„คโ‰ฅโ€˜๐‘€) โŠ† โ„*
514, 50sstrdi 3167 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐ด โŠ† โ„*)
5251adantr 276 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ โˆˆ ๐ด) โ†’ ๐ด โŠ† โ„*)
5326adantr 276 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ โˆˆ ๐ด) โ†’ ๐‘ โˆˆ (1...๐‘))
54 leisorel 10816 . . . . . . . . . 10 ((๐พ Isom < , < ((1...๐‘), ๐ด) โˆง ((1...๐‘) โŠ† โ„* โˆง ๐ด โŠ† โ„*) โˆง ((โ—ก๐พโ€˜๐‘) โˆˆ (1...๐‘) โˆง ๐‘ โˆˆ (1...๐‘))) โ†’ ((โ—ก๐พโ€˜๐‘) โ‰ค ๐‘ โ†” (๐พโ€˜(โ—ก๐พโ€˜๐‘)) โ‰ค (๐พโ€˜๐‘)))
5539, 47, 52, 36, 53, 54syl122anc 1247 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ โˆˆ ๐ด) โ†’ ((โ—ก๐พโ€˜๐‘) โ‰ค ๐‘ โ†” (๐พโ€˜(โ—ก๐พโ€˜๐‘)) โ‰ค (๐พโ€˜๐‘)))
5638, 55mpbid 147 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ โˆˆ ๐ด) โ†’ (๐พโ€˜(โ—ก๐พโ€˜๐‘)) โ‰ค (๐พโ€˜๐‘))
5732, 56eqbrtrrd 4027 . . . . . . 7 ((๐œ‘ โˆง ๐‘ โˆˆ ๐ด) โ†’ ๐‘ โ‰ค (๐พโ€˜๐‘))
584, 48sstrdi 3167 . . . . . . . . 9 (๐œ‘ โ†’ ๐ด โŠ† โ„ค)
5958sselda 3155 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ โˆˆ ๐ด) โ†’ ๐‘ โˆˆ โ„ค)
6048, 28sselid 3153 . . . . . . . . 9 (๐œ‘ โ†’ (๐พโ€˜๐‘) โˆˆ โ„ค)
6160adantr 276 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ โˆˆ ๐ด) โ†’ (๐พโ€˜๐‘) โˆˆ โ„ค)
62 eluz 9540 . . . . . . . 8 ((๐‘ โˆˆ โ„ค โˆง (๐พโ€˜๐‘) โˆˆ โ„ค) โ†’ ((๐พโ€˜๐‘) โˆˆ (โ„คโ‰ฅโ€˜๐‘) โ†” ๐‘ โ‰ค (๐พโ€˜๐‘)))
6359, 61, 62syl2anc 411 . . . . . . 7 ((๐œ‘ โˆง ๐‘ โˆˆ ๐ด) โ†’ ((๐พโ€˜๐‘) โˆˆ (โ„คโ‰ฅโ€˜๐‘) โ†” ๐‘ โ‰ค (๐พโ€˜๐‘)))
6457, 63mpbird 167 . . . . . 6 ((๐œ‘ โˆง ๐‘ โˆˆ ๐ด) โ†’ (๐พโ€˜๐‘) โˆˆ (โ„คโ‰ฅโ€˜๐‘))
65 elfzuzb 10018 . . . . . 6 (๐‘ โˆˆ (๐‘€...(๐พโ€˜๐‘)) โ†” (๐‘ โˆˆ (โ„คโ‰ฅโ€˜๐‘€) โˆง (๐พโ€˜๐‘) โˆˆ (โ„คโ‰ฅโ€˜๐‘)))
6629, 64, 65sylanbrc 417 . . . . 5 ((๐œ‘ โˆง ๐‘ โˆˆ ๐ด) โ†’ ๐‘ โˆˆ (๐‘€...(๐พโ€˜๐‘)))
6766ex 115 . . . 4 (๐œ‘ โ†’ (๐‘ โˆˆ ๐ด โ†’ ๐‘ โˆˆ (๐‘€...(๐พโ€˜๐‘))))
6867ssrdv 3161 . . 3 (๐œ‘ โ†’ ๐ด โŠ† (๐‘€...(๐พโ€˜๐‘)))
691, 2, 3, 28, 68fproddccvg 11579 . 2 (๐œ‘ โ†’ seq๐‘€( ยท , ๐น) โ‡ (seq๐‘€( ยท , ๐น)โ€˜(๐พโ€˜๐‘)))
70 mullid 7954 . . . . 5 (๐‘š โˆˆ โ„‚ โ†’ (1 ยท ๐‘š) = ๐‘š)
7170adantl 277 . . . 4 ((๐œ‘ โˆง ๐‘š โˆˆ โ„‚) โ†’ (1 ยท ๐‘š) = ๐‘š)
72 mulrid 7953 . . . . 5 (๐‘š โˆˆ โ„‚ โ†’ (๐‘š ยท 1) = ๐‘š)
7372adantl 277 . . . 4 ((๐œ‘ โˆง ๐‘š โˆˆ โ„‚) โ†’ (๐‘š ยท 1) = ๐‘š)
74 mulcl 7937 . . . . 5 ((๐‘š โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ โ„‚) โ†’ (๐‘š ยท ๐‘ฅ) โˆˆ โ„‚)
7574adantl 277 . . . 4 ((๐œ‘ โˆง (๐‘š โˆˆ โ„‚ โˆง ๐‘ฅ โˆˆ โ„‚)) โ†’ (๐‘š ยท ๐‘ฅ) โˆˆ โ„‚)
76 1cnd 7972 . . . 4 (๐œ‘ โ†’ 1 โˆˆ โ„‚)
7726, 16eleqtrrd 2257 . . . 4 (๐œ‘ โ†’ ๐‘ โˆˆ (1...(โ™ฏโ€˜๐ด)))
78 eluzelz 9536 . . . . . 6 (๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘€) โ†’ ๐‘š โˆˆ โ„ค)
79 simpr 110 . . . . . . . 8 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โˆง ๐‘š โˆˆ ๐ด) โ†’ ๐‘š โˆˆ ๐ด)
802ralrimiva 2550 . . . . . . . . 9 (๐œ‘ โ†’ โˆ€๐‘˜ โˆˆ ๐ด ๐ต โˆˆ โ„‚)
8180ad2antrr 488 . . . . . . . 8 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โˆง ๐‘š โˆˆ ๐ด) โ†’ โˆ€๐‘˜ โˆˆ ๐ด ๐ต โˆˆ โ„‚)
82 nfcsb1v 3090 . . . . . . . . . 10 โ„ฒ๐‘˜โฆ‹๐‘š / ๐‘˜โฆŒ๐ต
8382nfel1 2330 . . . . . . . . 9 โ„ฒ๐‘˜โฆ‹๐‘š / ๐‘˜โฆŒ๐ต โˆˆ โ„‚
84 csbeq1a 3066 . . . . . . . . . 10 (๐‘˜ = ๐‘š โ†’ ๐ต = โฆ‹๐‘š / ๐‘˜โฆŒ๐ต)
8584eleq1d 2246 . . . . . . . . 9 (๐‘˜ = ๐‘š โ†’ (๐ต โˆˆ โ„‚ โ†” โฆ‹๐‘š / ๐‘˜โฆŒ๐ต โˆˆ โ„‚))
8683, 85rspc 2835 . . . . . . . 8 (๐‘š โˆˆ ๐ด โ†’ (โˆ€๐‘˜ โˆˆ ๐ด ๐ต โˆˆ โ„‚ โ†’ โฆ‹๐‘š / ๐‘˜โฆŒ๐ต โˆˆ โ„‚))
8779, 81, 86sylc 62 . . . . . . 7 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โˆง ๐‘š โˆˆ ๐ด) โ†’ โฆ‹๐‘š / ๐‘˜โฆŒ๐ต โˆˆ โ„‚)
88 1cnd 7972 . . . . . . 7 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โˆง ยฌ ๐‘š โˆˆ ๐ด) โ†’ 1 โˆˆ โ„‚)
89 eleq1 2240 . . . . . . . . 9 (๐‘˜ = ๐‘š โ†’ (๐‘˜ โˆˆ ๐ด โ†” ๐‘š โˆˆ ๐ด))
9089dcbid 838 . . . . . . . 8 (๐‘˜ = ๐‘š โ†’ (DECID ๐‘˜ โˆˆ ๐ด โ†” DECID ๐‘š โˆˆ ๐ด))
913ralrimiva 2550 . . . . . . . . 9 (๐œ‘ โ†’ โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)DECID ๐‘˜ โˆˆ ๐ด)
9291adantr 276 . . . . . . . 8 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ โˆ€๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜๐‘€)DECID ๐‘˜ โˆˆ ๐ด)
93 simpr 110 . . . . . . . 8 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘€))
9490, 92, 93rspcdva 2846 . . . . . . 7 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ DECID ๐‘š โˆˆ ๐ด)
9587, 88, 94ifcldadc 3563 . . . . . 6 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ if(๐‘š โˆˆ ๐ด, โฆ‹๐‘š / ๐‘˜โฆŒ๐ต, 1) โˆˆ โ„‚)
96 nfcv 2319 . . . . . . 7 โ„ฒ๐‘˜๐‘š
97 nfv 1528 . . . . . . . 8 โ„ฒ๐‘˜ ๐‘š โˆˆ ๐ด
98 nfcv 2319 . . . . . . . 8 โ„ฒ๐‘˜1
9997, 82, 98nfif 3562 . . . . . . 7 โ„ฒ๐‘˜if(๐‘š โˆˆ ๐ด, โฆ‹๐‘š / ๐‘˜โฆŒ๐ต, 1)
10089, 84ifbieq1d 3556 . . . . . . 7 (๐‘˜ = ๐‘š โ†’ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1) = if(๐‘š โˆˆ ๐ด, โฆ‹๐‘š / ๐‘˜โฆŒ๐ต, 1))
10196, 99, 100, 1fvmptf 5608 . . . . . 6 ((๐‘š โˆˆ โ„ค โˆง if(๐‘š โˆˆ ๐ด, โฆ‹๐‘š / ๐‘˜โฆŒ๐ต, 1) โˆˆ โ„‚) โ†’ (๐นโ€˜๐‘š) = if(๐‘š โˆˆ ๐ด, โฆ‹๐‘š / ๐‘˜โฆŒ๐ต, 1))
10278, 95, 101syl2an2 594 . . . . 5 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ (๐นโ€˜๐‘š) = if(๐‘š โˆˆ ๐ด, โฆ‹๐‘š / ๐‘˜โฆŒ๐ต, 1))
103102, 95eqeltrd 2254 . . . 4 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜๐‘€)) โ†’ (๐นโ€˜๐‘š) โˆˆ โ„‚)
104 prodmodclem2.4 . . . . . 6 ๐ป = (๐‘— โˆˆ โ„• โ†ฆ if(๐‘— โ‰ค (โ™ฏโ€˜๐ด), โฆ‹(๐พโ€˜๐‘—) / ๐‘˜โฆŒ๐ต, 1))
105 breq1 4006 . . . . . . 7 (๐‘— = ๐‘š โ†’ (๐‘— โ‰ค (โ™ฏโ€˜๐ด) โ†” ๐‘š โ‰ค (โ™ฏโ€˜๐ด)))
106 fveq2 5515 . . . . . . . 8 (๐‘— = ๐‘š โ†’ (๐พโ€˜๐‘—) = (๐พโ€˜๐‘š))
107106csbeq1d 3064 . . . . . . 7 (๐‘— = ๐‘š โ†’ โฆ‹(๐พโ€˜๐‘—) / ๐‘˜โฆŒ๐ต = โฆ‹(๐พโ€˜๐‘š) / ๐‘˜โฆŒ๐ต)
108105, 107ifbieq1d 3556 . . . . . 6 (๐‘— = ๐‘š โ†’ if(๐‘— โ‰ค (โ™ฏโ€˜๐ด), โฆ‹(๐พโ€˜๐‘—) / ๐‘˜โฆŒ๐ต, 1) = if(๐‘š โ‰ค (โ™ฏโ€˜๐ด), โฆ‹(๐พโ€˜๐‘š) / ๐‘˜โฆŒ๐ต, 1))
109 elnnuz 9563 . . . . . . . 8 (๐‘š โˆˆ โ„• โ†” ๐‘š โˆˆ (โ„คโ‰ฅโ€˜1))
110109biimpri 133 . . . . . . 7 (๐‘š โˆˆ (โ„คโ‰ฅโ€˜1) โ†’ ๐‘š โˆˆ โ„•)
111110adantl 277 . . . . . 6 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜1)) โ†’ ๐‘š โˆˆ โ„•)
11222ad2antrr 488 . . . . . . . . 9 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜1)) โˆง ๐‘š โ‰ค (โ™ฏโ€˜๐ด)) โ†’ ๐พ:(1...๐‘)โŸถ๐ด)
113 1zzd 9279 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜1)) โˆง ๐‘š โ‰ค (โ™ฏโ€˜๐ด)) โ†’ 1 โˆˆ โ„ค)
1148ad2antrr 488 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜1)) โˆง ๐‘š โ‰ค (โ™ฏโ€˜๐ด)) โ†’ ๐‘ โˆˆ โ„ค)
115 eluzelz 9536 . . . . . . . . . . . 12 (๐‘š โˆˆ (โ„คโ‰ฅโ€˜1) โ†’ ๐‘š โˆˆ โ„ค)
116115ad2antlr 489 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜1)) โˆง ๐‘š โ‰ค (โ™ฏโ€˜๐ด)) โ†’ ๐‘š โˆˆ โ„ค)
117113, 114, 1163jca 1177 . . . . . . . . . 10 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜1)) โˆง ๐‘š โ‰ค (โ™ฏโ€˜๐ด)) โ†’ (1 โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘š โˆˆ โ„ค))
118 eluzle 9539 . . . . . . . . . . . 12 (๐‘š โˆˆ (โ„คโ‰ฅโ€˜1) โ†’ 1 โ‰ค ๐‘š)
119118ad2antlr 489 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜1)) โˆง ๐‘š โ‰ค (โ™ฏโ€˜๐ด)) โ†’ 1 โ‰ค ๐‘š)
120 simpr 110 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜1)) โˆง ๐‘š โ‰ค (โ™ฏโ€˜๐ด)) โ†’ ๐‘š โ‰ค (โ™ฏโ€˜๐ด))
12115ad2antrr 488 . . . . . . . . . . . 12 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜1)) โˆง ๐‘š โ‰ค (โ™ฏโ€˜๐ด)) โ†’ (โ™ฏโ€˜๐ด) = ๐‘)
122120, 121breqtrd 4029 . . . . . . . . . . 11 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜1)) โˆง ๐‘š โ‰ค (โ™ฏโ€˜๐ด)) โ†’ ๐‘š โ‰ค ๐‘)
123119, 122jca 306 . . . . . . . . . 10 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜1)) โˆง ๐‘š โ‰ค (โ™ฏโ€˜๐ด)) โ†’ (1 โ‰ค ๐‘š โˆง ๐‘š โ‰ค ๐‘))
124 elfz2 10014 . . . . . . . . . 10 (๐‘š โˆˆ (1...๐‘) โ†” ((1 โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘š โˆˆ โ„ค) โˆง (1 โ‰ค ๐‘š โˆง ๐‘š โ‰ค ๐‘)))
125117, 123, 124sylanbrc 417 . . . . . . . . 9 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜1)) โˆง ๐‘š โ‰ค (โ™ฏโ€˜๐ด)) โ†’ ๐‘š โˆˆ (1...๐‘))
126112, 125ffvelcdmd 5652 . . . . . . . 8 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜1)) โˆง ๐‘š โ‰ค (โ™ฏโ€˜๐ด)) โ†’ (๐พโ€˜๐‘š) โˆˆ ๐ด)
12780ad2antrr 488 . . . . . . . 8 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜1)) โˆง ๐‘š โ‰ค (โ™ฏโ€˜๐ด)) โ†’ โˆ€๐‘˜ โˆˆ ๐ด ๐ต โˆˆ โ„‚)
128 nfcsb1v 3090 . . . . . . . . . 10 โ„ฒ๐‘˜โฆ‹(๐พโ€˜๐‘š) / ๐‘˜โฆŒ๐ต
129128nfel1 2330 . . . . . . . . 9 โ„ฒ๐‘˜โฆ‹(๐พโ€˜๐‘š) / ๐‘˜โฆŒ๐ต โˆˆ โ„‚
130 csbeq1a 3066 . . . . . . . . . 10 (๐‘˜ = (๐พโ€˜๐‘š) โ†’ ๐ต = โฆ‹(๐พโ€˜๐‘š) / ๐‘˜โฆŒ๐ต)
131130eleq1d 2246 . . . . . . . . 9 (๐‘˜ = (๐พโ€˜๐‘š) โ†’ (๐ต โˆˆ โ„‚ โ†” โฆ‹(๐พโ€˜๐‘š) / ๐‘˜โฆŒ๐ต โˆˆ โ„‚))
132129, 131rspc 2835 . . . . . . . 8 ((๐พโ€˜๐‘š) โˆˆ ๐ด โ†’ (โˆ€๐‘˜ โˆˆ ๐ด ๐ต โˆˆ โ„‚ โ†’ โฆ‹(๐พโ€˜๐‘š) / ๐‘˜โฆŒ๐ต โˆˆ โ„‚))
133126, 127, 132sylc 62 . . . . . . 7 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜1)) โˆง ๐‘š โ‰ค (โ™ฏโ€˜๐ด)) โ†’ โฆ‹(๐พโ€˜๐‘š) / ๐‘˜โฆŒ๐ต โˆˆ โ„‚)
134 1cnd 7972 . . . . . . 7 (((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜1)) โˆง ยฌ ๐‘š โ‰ค (โ™ฏโ€˜๐ด)) โ†’ 1 โˆˆ โ„‚)
135111nnzd 9373 . . . . . . . 8 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜1)) โ†’ ๐‘š โˆˆ โ„ค)
13615, 8eqeltrd 2254 . . . . . . . . 9 (๐œ‘ โ†’ (โ™ฏโ€˜๐ด) โˆˆ โ„ค)
137136adantr 276 . . . . . . . 8 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜1)) โ†’ (โ™ฏโ€˜๐ด) โˆˆ โ„ค)
138 zdcle 9328 . . . . . . . 8 ((๐‘š โˆˆ โ„ค โˆง (โ™ฏโ€˜๐ด) โˆˆ โ„ค) โ†’ DECID ๐‘š โ‰ค (โ™ฏโ€˜๐ด))
139135, 137, 138syl2anc 411 . . . . . . 7 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜1)) โ†’ DECID ๐‘š โ‰ค (โ™ฏโ€˜๐ด))
140133, 134, 139ifcldadc 3563 . . . . . 6 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜1)) โ†’ if(๐‘š โ‰ค (โ™ฏโ€˜๐ด), โฆ‹(๐พโ€˜๐‘š) / ๐‘˜โฆŒ๐ต, 1) โˆˆ โ„‚)
141104, 108, 111, 140fvmptd3 5609 . . . . 5 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜1)) โ†’ (๐ปโ€˜๐‘š) = if(๐‘š โ‰ค (โ™ฏโ€˜๐ด), โฆ‹(๐พโ€˜๐‘š) / ๐‘˜โฆŒ๐ต, 1))
142141, 140eqeltrd 2254 . . . 4 ((๐œ‘ โˆง ๐‘š โˆˆ (โ„คโ‰ฅโ€˜1)) โ†’ (๐ปโ€˜๐‘š) โˆˆ โ„‚)
143 eldifi 3257 . . . . . . 7 (๐‘š โˆˆ ((๐‘€...(๐พโ€˜(โ™ฏโ€˜๐ด))) โˆ– ๐ด) โ†’ ๐‘š โˆˆ (๐‘€...(๐พโ€˜(โ™ฏโ€˜๐ด))))
144 elfzelz 10024 . . . . . . 7 (๐‘š โˆˆ (๐‘€...(๐พโ€˜(โ™ฏโ€˜๐ด))) โ†’ ๐‘š โˆˆ โ„ค)
145143, 144syl 14 . . . . . 6 (๐‘š โˆˆ ((๐‘€...(๐พโ€˜(โ™ฏโ€˜๐ด))) โˆ– ๐ด) โ†’ ๐‘š โˆˆ โ„ค)
146 eldifn 3258 . . . . . . . . 9 (๐‘š โˆˆ ((๐‘€...(๐พโ€˜(โ™ฏโ€˜๐ด))) โˆ– ๐ด) โ†’ ยฌ ๐‘š โˆˆ ๐ด)
147146iffalsed 3544 . . . . . . . 8 (๐‘š โˆˆ ((๐‘€...(๐พโ€˜(โ™ฏโ€˜๐ด))) โˆ– ๐ด) โ†’ if(๐‘š โˆˆ ๐ด, โฆ‹๐‘š / ๐‘˜โฆŒ๐ต, 1) = 1)
148 ax-1cn 7903 . . . . . . . 8 1 โˆˆ โ„‚
149147, 148eqeltrdi 2268 . . . . . . 7 (๐‘š โˆˆ ((๐‘€...(๐พโ€˜(โ™ฏโ€˜๐ด))) โˆ– ๐ด) โ†’ if(๐‘š โˆˆ ๐ด, โฆ‹๐‘š / ๐‘˜โฆŒ๐ต, 1) โˆˆ โ„‚)
150149adantl 277 . . . . . 6 ((๐œ‘ โˆง ๐‘š โˆˆ ((๐‘€...(๐พโ€˜(โ™ฏโ€˜๐ด))) โˆ– ๐ด)) โ†’ if(๐‘š โˆˆ ๐ด, โฆ‹๐‘š / ๐‘˜โฆŒ๐ต, 1) โˆˆ โ„‚)
151145, 150, 101syl2an2 594 . . . . 5 ((๐œ‘ โˆง ๐‘š โˆˆ ((๐‘€...(๐พโ€˜(โ™ฏโ€˜๐ด))) โˆ– ๐ด)) โ†’ (๐นโ€˜๐‘š) = if(๐‘š โˆˆ ๐ด, โฆ‹๐‘š / ๐‘˜โฆŒ๐ต, 1))
152147adantl 277 . . . . 5 ((๐œ‘ โˆง ๐‘š โˆˆ ((๐‘€...(๐พโ€˜(โ™ฏโ€˜๐ด))) โˆ– ๐ด)) โ†’ if(๐‘š โˆˆ ๐ด, โฆ‹๐‘š / ๐‘˜โฆŒ๐ต, 1) = 1)
153151, 152eqtrd 2210 . . . 4 ((๐œ‘ โˆง ๐‘š โˆˆ ((๐‘€...(๐พโ€˜(โ™ฏโ€˜๐ด))) โˆ– ๐ด)) โ†’ (๐นโ€˜๐‘š) = 1)
154 elfzle2 10027 . . . . . . 7 (๐‘ฅ โˆˆ (1...(โ™ฏโ€˜๐ด)) โ†’ ๐‘ฅ โ‰ค (โ™ฏโ€˜๐ด))
155154adantl 277 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...(โ™ฏโ€˜๐ด))) โ†’ ๐‘ฅ โ‰ค (โ™ฏโ€˜๐ด))
156155iftrued 3541 . . . . 5 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...(โ™ฏโ€˜๐ด))) โ†’ if(๐‘ฅ โ‰ค (โ™ฏโ€˜๐ด), โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต, 1) = โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต)
157 breq1 4006 . . . . . . 7 (๐‘— = ๐‘ฅ โ†’ (๐‘— โ‰ค (โ™ฏโ€˜๐ด) โ†” ๐‘ฅ โ‰ค (โ™ฏโ€˜๐ด)))
158 fveq2 5515 . . . . . . . 8 (๐‘— = ๐‘ฅ โ†’ (๐พโ€˜๐‘—) = (๐พโ€˜๐‘ฅ))
159158csbeq1d 3064 . . . . . . 7 (๐‘— = ๐‘ฅ โ†’ โฆ‹(๐พโ€˜๐‘—) / ๐‘˜โฆŒ๐ต = โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต)
160157, 159ifbieq1d 3556 . . . . . 6 (๐‘— = ๐‘ฅ โ†’ if(๐‘— โ‰ค (โ™ฏโ€˜๐ด), โฆ‹(๐พโ€˜๐‘—) / ๐‘˜โฆŒ๐ต, 1) = if(๐‘ฅ โ‰ค (โ™ฏโ€˜๐ด), โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต, 1))
161 elfznn 10053 . . . . . . 7 (๐‘ฅ โˆˆ (1...(โ™ฏโ€˜๐ด)) โ†’ ๐‘ฅ โˆˆ โ„•)
162161adantl 277 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...(โ™ฏโ€˜๐ด))) โ†’ ๐‘ฅ โˆˆ โ„•)
16322adantr 276 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...(โ™ฏโ€˜๐ด))) โ†’ ๐พ:(1...๐‘)โŸถ๐ด)
164 simpr 110 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...(โ™ฏโ€˜๐ด))) โ†’ ๐‘ฅ โˆˆ (1...(โ™ฏโ€˜๐ด)))
16515adantr 276 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...(โ™ฏโ€˜๐ด))) โ†’ (โ™ฏโ€˜๐ด) = ๐‘)
166165oveq2d 5890 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...(โ™ฏโ€˜๐ด))) โ†’ (1...(โ™ฏโ€˜๐ด)) = (1...๐‘))
167164, 166eleqtrd 2256 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...(โ™ฏโ€˜๐ด))) โ†’ ๐‘ฅ โˆˆ (1...๐‘))
168163, 167ffvelcdmd 5652 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...(โ™ฏโ€˜๐ด))) โ†’ (๐พโ€˜๐‘ฅ) โˆˆ ๐ด)
16980adantr 276 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...(โ™ฏโ€˜๐ด))) โ†’ โˆ€๐‘˜ โˆˆ ๐ด ๐ต โˆˆ โ„‚)
170 nfcsb1v 3090 . . . . . . . . . 10 โ„ฒ๐‘˜โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต
171170nfel1 2330 . . . . . . . . 9 โ„ฒ๐‘˜โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต โˆˆ โ„‚
172 csbeq1a 3066 . . . . . . . . . 10 (๐‘˜ = (๐พโ€˜๐‘ฅ) โ†’ ๐ต = โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต)
173172eleq1d 2246 . . . . . . . . 9 (๐‘˜ = (๐พโ€˜๐‘ฅ) โ†’ (๐ต โˆˆ โ„‚ โ†” โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต โˆˆ โ„‚))
174171, 173rspc 2835 . . . . . . . 8 ((๐พโ€˜๐‘ฅ) โˆˆ ๐ด โ†’ (โˆ€๐‘˜ โˆˆ ๐ด ๐ต โˆˆ โ„‚ โ†’ โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต โˆˆ โ„‚))
175168, 169, 174sylc 62 . . . . . . 7 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...(โ™ฏโ€˜๐ด))) โ†’ โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต โˆˆ โ„‚)
176156, 175eqeltrd 2254 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...(โ™ฏโ€˜๐ด))) โ†’ if(๐‘ฅ โ‰ค (โ™ฏโ€˜๐ด), โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต, 1) โˆˆ โ„‚)
177104, 160, 162, 176fvmptd3 5609 . . . . 5 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...(โ™ฏโ€˜๐ด))) โ†’ (๐ปโ€˜๐‘ฅ) = if(๐‘ฅ โ‰ค (โ™ฏโ€˜๐ด), โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต, 1))
1784adantr 276 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...(โ™ฏโ€˜๐ด))) โ†’ ๐ด โŠ† (โ„คโ‰ฅโ€˜๐‘€))
179178, 48sstrdi 3167 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...(โ™ฏโ€˜๐ด))) โ†’ ๐ด โŠ† โ„ค)
180179, 168sseldd 3156 . . . . . . 7 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...(โ™ฏโ€˜๐ด))) โ†’ (๐พโ€˜๐‘ฅ) โˆˆ โ„ค)
181168iftrued 3541 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...(โ™ฏโ€˜๐ด))) โ†’ if((๐พโ€˜๐‘ฅ) โˆˆ ๐ด, โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต, 1) = โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต)
182181, 175eqeltrd 2254 . . . . . . 7 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...(โ™ฏโ€˜๐ด))) โ†’ if((๐พโ€˜๐‘ฅ) โˆˆ ๐ด, โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต, 1) โˆˆ โ„‚)
183 nfcv 2319 . . . . . . . 8 โ„ฒ๐‘˜(๐พโ€˜๐‘ฅ)
184 nfv 1528 . . . . . . . . 9 โ„ฒ๐‘˜(๐พโ€˜๐‘ฅ) โˆˆ ๐ด
185184, 170, 98nfif 3562 . . . . . . . 8 โ„ฒ๐‘˜if((๐พโ€˜๐‘ฅ) โˆˆ ๐ด, โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต, 1)
186 eleq1 2240 . . . . . . . . 9 (๐‘˜ = (๐พโ€˜๐‘ฅ) โ†’ (๐‘˜ โˆˆ ๐ด โ†” (๐พโ€˜๐‘ฅ) โˆˆ ๐ด))
187186, 172ifbieq1d 3556 . . . . . . . 8 (๐‘˜ = (๐พโ€˜๐‘ฅ) โ†’ if(๐‘˜ โˆˆ ๐ด, ๐ต, 1) = if((๐พโ€˜๐‘ฅ) โˆˆ ๐ด, โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต, 1))
188183, 185, 187, 1fvmptf 5608 . . . . . . 7 (((๐พโ€˜๐‘ฅ) โˆˆ โ„ค โˆง if((๐พโ€˜๐‘ฅ) โˆˆ ๐ด, โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต, 1) โˆˆ โ„‚) โ†’ (๐นโ€˜(๐พโ€˜๐‘ฅ)) = if((๐พโ€˜๐‘ฅ) โˆˆ ๐ด, โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต, 1))
189180, 182, 188syl2anc 411 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...(โ™ฏโ€˜๐ด))) โ†’ (๐นโ€˜(๐พโ€˜๐‘ฅ)) = if((๐พโ€˜๐‘ฅ) โˆˆ ๐ด, โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต, 1))
190189, 181eqtrd 2210 . . . . 5 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...(โ™ฏโ€˜๐ด))) โ†’ (๐นโ€˜(๐พโ€˜๐‘ฅ)) = โฆ‹(๐พโ€˜๐‘ฅ) / ๐‘˜โฆŒ๐ต)
191156, 177, 1903eqtr4d 2220 . . . 4 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...(โ™ฏโ€˜๐ด))) โ†’ (๐ปโ€˜๐‘ฅ) = (๐นโ€˜(๐พโ€˜๐‘ฅ)))
19271, 73, 75, 76, 5, 77, 4, 103, 142, 153, 191seq3coll 10821 . . 3 (๐œ‘ โ†’ (seq๐‘€( ยท , ๐น)โ€˜(๐พโ€˜๐‘)) = (seq1( ยท , ๐ป)โ€˜๐‘))
193 prodmodc.3 . . . 4 ๐บ = (๐‘— โˆˆ โ„• โ†ฆ if(๐‘— โ‰ค (โ™ฏโ€˜๐ด), โฆ‹(๐‘“โ€˜๐‘—) / ๐‘˜โฆŒ๐ต, 1))
1947, 7jca 306 . . . 4 (๐œ‘ โ†’ (๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•))
1951, 2, 193, 104, 194, 10, 30prodmodclem3 11582 . . 3 (๐œ‘ โ†’ (seq1( ยท , ๐บ)โ€˜๐‘) = (seq1( ยท , ๐ป)โ€˜๐‘))
196192, 195eqtr4d 2213 . 2 (๐œ‘ โ†’ (seq๐‘€( ยท , ๐น)โ€˜(๐พโ€˜๐‘)) = (seq1( ยท , ๐บ)โ€˜๐‘))
19769, 196breqtrd 4029 1 (๐œ‘ โ†’ seq๐‘€( ยท , ๐น) โ‡ (seq1( ยท , ๐บ)โ€˜๐‘))
Colors of variables: wff set class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โˆง wa 104   โ†” wb 105  DECID wdc 834   โˆง w3a 978   = wceq 1353   โˆˆ wcel 2148  โˆ€wral 2455  โฆ‹csb 3057   โˆ– cdif 3126   โŠ† wss 3129  ifcif 3534   class class class wbr 4003   โ†ฆ cmpt 4064  โ—กccnv 4625  โŸถwf 5212  โ€“1-1-ontoโ†’wf1o 5215  โ€˜cfv 5216   Isom wiso 5217  (class class class)co 5874  โ„‚cc 7808  โ„cr 7809  1c1 7811   ยท cmul 7815  โ„*cxr 7990   < clt 7991   โ‰ค cle 7992  โ„•cn 8918  โ„•0cn0 9175  โ„คcz 9252  โ„คโ‰ฅcuz 9527  ...cfz 10007  seqcseq 10444  โ™ฏchash 10754   โ‡ cli 11285
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4118  ax-sep 4121  ax-nul 4129  ax-pow 4174  ax-pr 4209  ax-un 4433  ax-setind 4536  ax-iinf 4587  ax-cnex 7901  ax-resscn 7902  ax-1cn 7903  ax-1re 7904  ax-icn 7905  ax-addcl 7906  ax-addrcl 7907  ax-mulcl 7908  ax-mulrcl 7909  ax-addcom 7910  ax-mulcom 7911  ax-addass 7912  ax-mulass 7913  ax-distr 7914  ax-i2m1 7915  ax-0lt1 7916  ax-1rid 7917  ax-0id 7918  ax-rnegex 7919  ax-precex 7920  ax-cnre 7921  ax-pre-ltirr 7922  ax-pre-ltwlin 7923  ax-pre-lttrn 7924  ax-pre-apti 7925  ax-pre-ltadd 7926  ax-pre-mulgt0 7927  ax-pre-mulext 7928
This theorem depends on definitions:  df-bi 117  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rmo 2463  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-if 3535  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-int 3845  df-iun 3888  df-br 4004  df-opab 4065  df-mpt 4066  df-tr 4102  df-id 4293  df-po 4296  df-iso 4297  df-iord 4366  df-on 4368  df-ilim 4369  df-suc 4371  df-iom 4590  df-xp 4632  df-rel 4633  df-cnv 4634  df-co 4635  df-dm 4636  df-rn 4637  df-res 4638  df-ima 4639  df-iota 5178  df-fun 5218  df-fn 5219  df-f 5220  df-f1 5221  df-fo 5222  df-f1o 5223  df-fv 5224  df-isom 5225  df-riota 5830  df-ov 5877  df-oprab 5878  df-mpo 5879  df-1st 6140  df-2nd 6141  df-recs 6305  df-frec 6391  df-1o 6416  df-er 6534  df-en 6740  df-dom 6741  df-fin 6742  df-pnf 7993  df-mnf 7994  df-xr 7995  df-ltxr 7996  df-le 7997  df-sub 8129  df-neg 8130  df-reap 8531  df-ap 8538  df-div 8629  df-inn 8919  df-2 8977  df-n0 9176  df-z 9253  df-uz 9528  df-rp 9653  df-fz 10008  df-fzo 10142  df-seqfrec 10445  df-exp 10519  df-ihash 10755  df-cj 10850  df-rsqrt 11006  df-abs 11007  df-clim 11286
This theorem is referenced by:  prodmodclem2  11584  zproddc  11586
  Copyright terms: Public domain W3C validator