MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fprodser Structured version   Unicode version

Theorem fprodser 13841
Description: A finite product expressed in terms of a partial product of an infinite sequence. The recursive definition of a finite product follows from here. (Contributed by Scott Fenton, 14-Dec-2017.)
Hypotheses
Ref Expression
fprodser.1  |-  ( (
ph  /\  k  e.  ( M ... N ) )  ->  ( F `  k )  =  A )
fprodser.2  |-  ( ph  ->  N  e.  ( ZZ>= `  M ) )
fprodser.3  |-  ( (
ph  /\  k  e.  ( M ... N ) )  ->  A  e.  CC )
Assertion
Ref Expression
fprodser  |-  ( ph  ->  prod_ k  e.  ( M ... N ) A  =  (  seq M (  x.  ,  F ) `  N
) )
Distinct variable groups:    k, F    ph, k    k, M    k, N
Allowed substitution hint:    A( k)

Proof of Theorem fprodser
Dummy variables  j  m  n  p are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 prodfc 13837 . 2  |-  prod_ j  e.  ( M ... N
) ( ( k  e.  ( M ... N )  |->  A ) `
 j )  = 
prod_ k  e.  ( M ... N ) A
2 fveq2 5848 . . . 4  |-  ( j  =  ( ( n  e.  ( 1 ... ( N  +  ( 1  -  M ) ) )  |->  ( n  +  ( M  - 
1 ) ) ) `
 m )  -> 
( ( k  e.  ( M ... N
)  |->  A ) `  j )  =  ( ( k  e.  ( M ... N ) 
|->  A ) `  (
( n  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) 
|->  ( n  +  ( M  -  1 ) ) ) `  m
) ) )
3 fprodser.2 . . . . . . . . 9  |-  ( ph  ->  N  e.  ( ZZ>= `  M ) )
4 eluzelz 11091 . . . . . . . . 9  |-  ( N  e.  ( ZZ>= `  M
)  ->  N  e.  ZZ )
53, 4syl 16 . . . . . . . 8  |-  ( ph  ->  N  e.  ZZ )
65zcnd 10966 . . . . . . 7  |-  ( ph  ->  N  e.  CC )
7 eluzel2 11087 . . . . . . . . 9  |-  ( N  e.  ( ZZ>= `  M
)  ->  M  e.  ZZ )
83, 7syl 16 . . . . . . . 8  |-  ( ph  ->  M  e.  ZZ )
98zcnd 10966 . . . . . . 7  |-  ( ph  ->  M  e.  CC )
10 1cnd 9601 . . . . . . 7  |-  ( ph  ->  1  e.  CC )
116, 9, 10subadd23d 9944 . . . . . 6  |-  ( ph  ->  ( ( N  -  M )  +  1 )  =  ( N  +  ( 1  -  M ) ) )
1211eqcomd 2462 . . . . 5  |-  ( ph  ->  ( N  +  ( 1  -  M ) )  =  ( ( N  -  M )  +  1 ) )
13 uznn0sub 11113 . . . . . . 7  |-  ( N  e.  ( ZZ>= `  M
)  ->  ( N  -  M )  e.  NN0 )
143, 13syl 16 . . . . . 6  |-  ( ph  ->  ( N  -  M
)  e.  NN0 )
15 nn0p1nn 10831 . . . . . 6  |-  ( ( N  -  M )  e.  NN0  ->  ( ( N  -  M )  +  1 )  e.  NN )
1614, 15syl 16 . . . . 5  |-  ( ph  ->  ( ( N  -  M )  +  1 )  e.  NN )
1712, 16eqeltrd 2542 . . . 4  |-  ( ph  ->  ( N  +  ( 1  -  M ) )  e.  NN )
1810, 9pncan3d 9925 . . . . . . . . . . 11  |-  ( ph  ->  ( 1  +  ( M  -  1 ) )  =  M )
196, 10, 9pnpncand 9977 . . . . . . . . . . 11  |-  ( ph  ->  ( ( N  +  ( 1  -  M
) )  +  ( M  -  1 ) )  =  N )
2018, 19oveq12d 6288 . . . . . . . . . 10  |-  ( ph  ->  ( ( 1  +  ( M  -  1 ) ) ... (
( N  +  ( 1  -  M ) )  +  ( M  -  1 ) ) )  =  ( M ... N ) )
2120eleq2d 2524 . . . . . . . . 9  |-  ( ph  ->  ( p  e.  ( ( 1  +  ( M  -  1 ) ) ... ( ( N  +  ( 1  -  M ) )  +  ( M  - 
1 ) ) )  <-> 
p  e.  ( M ... N ) ) )
2221biimpa 482 . . . . . . . 8  |-  ( (
ph  /\  p  e.  ( ( 1  +  ( M  -  1 ) ) ... (
( N  +  ( 1  -  M ) )  +  ( M  -  1 ) ) ) )  ->  p  e.  ( M ... N
) )
23 elfzelz 11691 . . . . . . . . . . . . 13  |-  ( p  e.  ( M ... N )  ->  p  e.  ZZ )
2423zcnd 10966 . . . . . . . . . . . 12  |-  ( p  e.  ( M ... N )  ->  p  e.  CC )
2524adantl 464 . . . . . . . . . . 11  |-  ( (
ph  /\  p  e.  ( M ... N ) )  ->  p  e.  CC )
26 peano2zm 10903 . . . . . . . . . . . . . 14  |-  ( M  e.  ZZ  ->  ( M  -  1 )  e.  ZZ )
278, 26syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  ( M  -  1 )  e.  ZZ )
2827zcnd 10966 . . . . . . . . . . . 12  |-  ( ph  ->  ( M  -  1 )  e.  CC )
2928adantr 463 . . . . . . . . . . 11  |-  ( (
ph  /\  p  e.  ( M ... N ) )  ->  ( M  -  1 )  e.  CC )
3025, 29npcand 9926 . . . . . . . . . 10  |-  ( (
ph  /\  p  e.  ( M ... N ) )  ->  ( (
p  -  ( M  -  1 ) )  +  ( M  - 
1 ) )  =  p )
31 simpr 459 . . . . . . . . . 10  |-  ( (
ph  /\  p  e.  ( M ... N ) )  ->  p  e.  ( M ... N ) )
3230, 31eqeltrd 2542 . . . . . . . . 9  |-  ( (
ph  /\  p  e.  ( M ... N ) )  ->  ( (
p  -  ( M  -  1 ) )  +  ( M  - 
1 ) )  e.  ( M ... N
) )
33 ovex 6298 . . . . . . . . . 10  |-  ( p  -  ( M  - 
1 ) )  e. 
_V
34 oveq1 6277 . . . . . . . . . . 11  |-  ( n  =  ( p  -  ( M  -  1
) )  ->  (
n  +  ( M  -  1 ) )  =  ( ( p  -  ( M  - 
1 ) )  +  ( M  -  1 ) ) )
3534eleq1d 2523 . . . . . . . . . 10  |-  ( n  =  ( p  -  ( M  -  1
) )  ->  (
( n  +  ( M  -  1 ) )  e.  ( M ... N )  <->  ( (
p  -  ( M  -  1 ) )  +  ( M  - 
1 ) )  e.  ( M ... N
) ) )
3633, 35sbcie 3359 . . . . . . . . 9  |-  ( [. ( p  -  ( M  -  1 ) )  /  n ]. ( n  +  ( M  -  1 ) )  e.  ( M ... N )  <->  ( (
p  -  ( M  -  1 ) )  +  ( M  - 
1 ) )  e.  ( M ... N
) )
3732, 36sylibr 212 . . . . . . . 8  |-  ( (
ph  /\  p  e.  ( M ... N ) )  ->  [. ( p  -  ( M  - 
1 ) )  /  n ]. ( n  +  ( M  -  1
) )  e.  ( M ... N ) )
3822, 37syldan 468 . . . . . . 7  |-  ( (
ph  /\  p  e.  ( ( 1  +  ( M  -  1 ) ) ... (
( N  +  ( 1  -  M ) )  +  ( M  -  1 ) ) ) )  ->  [. (
p  -  ( M  -  1 ) )  /  n ]. (
n  +  ( M  -  1 ) )  e.  ( M ... N ) )
3938ralrimiva 2868 . . . . . 6  |-  ( ph  ->  A. p  e.  ( ( 1  +  ( M  -  1 ) ) ... ( ( N  +  ( 1  -  M ) )  +  ( M  - 
1 ) ) )
[. ( p  -  ( M  -  1
) )  /  n ]. ( n  +  ( M  -  1 ) )  e.  ( M ... N ) )
40 1zzd 10891 . . . . . . 7  |-  ( ph  ->  1  e.  ZZ )
4117nnzd 10964 . . . . . . 7  |-  ( ph  ->  ( N  +  ( 1  -  M ) )  e.  ZZ )
42 fzshftral 11770 . . . . . . 7  |-  ( ( 1  e.  ZZ  /\  ( N  +  (
1  -  M ) )  e.  ZZ  /\  ( M  -  1
)  e.  ZZ )  ->  ( A. n  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) ( n  +  ( M  -  1
) )  e.  ( M ... N )  <->  A. p  e.  (
( 1  +  ( M  -  1 ) ) ... ( ( N  +  ( 1  -  M ) )  +  ( M  - 
1 ) ) )
[. ( p  -  ( M  -  1
) )  /  n ]. ( n  +  ( M  -  1 ) )  e.  ( M ... N ) ) )
4340, 41, 27, 42syl3anc 1226 . . . . . 6  |-  ( ph  ->  ( A. n  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) ( n  +  ( M  -  1
) )  e.  ( M ... N )  <->  A. p  e.  (
( 1  +  ( M  -  1 ) ) ... ( ( N  +  ( 1  -  M ) )  +  ( M  - 
1 ) ) )
[. ( p  -  ( M  -  1
) )  /  n ]. ( n  +  ( M  -  1 ) )  e.  ( M ... N ) ) )
4439, 43mpbird 232 . . . . 5  |-  ( ph  ->  A. n  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) ( n  +  ( M  -  1 ) )  e.  ( M ... N ) )
458adantr 463 . . . . . . . . . . 11  |-  ( (
ph  /\  p  e.  ( M ... N ) )  ->  M  e.  ZZ )
465adantr 463 . . . . . . . . . . 11  |-  ( (
ph  /\  p  e.  ( M ... N ) )  ->  N  e.  ZZ )
4723adantl 464 . . . . . . . . . . 11  |-  ( (
ph  /\  p  e.  ( M ... N ) )  ->  p  e.  ZZ )
4827adantr 463 . . . . . . . . . . 11  |-  ( (
ph  /\  p  e.  ( M ... N ) )  ->  ( M  -  1 )  e.  ZZ )
49 fzsubel 11723 . . . . . . . . . . 11  |-  ( ( ( M  e.  ZZ  /\  N  e.  ZZ )  /\  ( p  e.  ZZ  /\  ( M  -  1 )  e.  ZZ ) )  -> 
( p  e.  ( M ... N )  <-> 
( p  -  ( M  -  1 ) )  e.  ( ( M  -  ( M  -  1 ) ) ... ( N  -  ( M  -  1
) ) ) ) )
5045, 46, 47, 48, 49syl22anc 1227 . . . . . . . . . 10  |-  ( (
ph  /\  p  e.  ( M ... N ) )  ->  ( p  e.  ( M ... N
)  <->  ( p  -  ( M  -  1
) )  e.  ( ( M  -  ( M  -  1 ) ) ... ( N  -  ( M  - 
1 ) ) ) ) )
5131, 50mpbid 210 . . . . . . . . 9  |-  ( (
ph  /\  p  e.  ( M ... N ) )  ->  ( p  -  ( M  - 
1 ) )  e.  ( ( M  -  ( M  -  1
) ) ... ( N  -  ( M  -  1 ) ) ) )
529, 10nncand 9927 . . . . . . . . . . 11  |-  ( ph  ->  ( M  -  ( M  -  1 ) )  =  1 )
536, 9, 10subsub2d 9951 . . . . . . . . . . 11  |-  ( ph  ->  ( N  -  ( M  -  1 ) )  =  ( N  +  ( 1  -  M ) ) )
5452, 53oveq12d 6288 . . . . . . . . . 10  |-  ( ph  ->  ( ( M  -  ( M  -  1
) ) ... ( N  -  ( M  -  1 ) ) )  =  ( 1 ... ( N  +  ( 1  -  M
) ) ) )
5554adantr 463 . . . . . . . . 9  |-  ( (
ph  /\  p  e.  ( M ... N ) )  ->  ( ( M  -  ( M  -  1 ) ) ... ( N  -  ( M  -  1
) ) )  =  ( 1 ... ( N  +  ( 1  -  M ) ) ) )
5651, 55eleqtrd 2544 . . . . . . . 8  |-  ( (
ph  /\  p  e.  ( M ... N ) )  ->  ( p  -  ( M  - 
1 ) )  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) )
5730eqcomd 2462 . . . . . . . 8  |-  ( (
ph  /\  p  e.  ( M ... N ) )  ->  p  =  ( ( p  -  ( M  -  1
) )  +  ( M  -  1 ) ) )
5834eqeq2d 2468 . . . . . . . . 9  |-  ( n  =  ( p  -  ( M  -  1
) )  ->  (
p  =  ( n  +  ( M  - 
1 ) )  <->  p  =  ( ( p  -  ( M  -  1
) )  +  ( M  -  1 ) ) ) )
5958rspcev 3207 . . . . . . . 8  |-  ( ( ( p  -  ( M  -  1 ) )  e.  ( 1 ... ( N  +  ( 1  -  M
) ) )  /\  p  =  ( (
p  -  ( M  -  1 ) )  +  ( M  - 
1 ) ) )  ->  E. n  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) p  =  ( n  +  ( M  - 
1 ) ) )
6056, 57, 59syl2anc 659 . . . . . . 7  |-  ( (
ph  /\  p  e.  ( M ... N ) )  ->  E. n  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) p  =  ( n  +  ( M  -  1 ) ) )
61 elfzelz 11691 . . . . . . . . . . . 12  |-  ( n  e.  ( 1 ... ( N  +  ( 1  -  M ) ) )  ->  n  e.  ZZ )
6261zcnd 10966 . . . . . . . . . . 11  |-  ( n  e.  ( 1 ... ( N  +  ( 1  -  M ) ) )  ->  n  e.  CC )
63 elfzelz 11691 . . . . . . . . . . . 12  |-  ( m  e.  ( 1 ... ( N  +  ( 1  -  M ) ) )  ->  m  e.  ZZ )
6463zcnd 10966 . . . . . . . . . . 11  |-  ( m  e.  ( 1 ... ( N  +  ( 1  -  M ) ) )  ->  m  e.  CC )
6562, 64anim12i 564 . . . . . . . . . 10  |-  ( ( n  e.  ( 1 ... ( N  +  ( 1  -  M
) ) )  /\  m  e.  ( 1 ... ( N  +  ( 1  -  M
) ) ) )  ->  ( n  e.  CC  /\  m  e.  CC ) )
66 eqtr2 2481 . . . . . . . . . . 11  |-  ( ( p  =  ( n  +  ( M  - 
1 ) )  /\  p  =  ( m  +  ( M  - 
1 ) ) )  ->  ( n  +  ( M  -  1
) )  =  ( m  +  ( M  -  1 ) ) )
67 simprl 754 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( n  e.  CC  /\  m  e.  CC ) )  ->  n  e.  CC )
68 simprr 755 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( n  e.  CC  /\  m  e.  CC ) )  ->  m  e.  CC )
6928adantr 463 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( n  e.  CC  /\  m  e.  CC ) )  -> 
( M  -  1 )  e.  CC )
7067, 68, 69addcan2d 9773 . . . . . . . . . . 11  |-  ( (
ph  /\  ( n  e.  CC  /\  m  e.  CC ) )  -> 
( ( n  +  ( M  -  1
) )  =  ( m  +  ( M  -  1 ) )  <-> 
n  =  m ) )
7166, 70syl5ib 219 . . . . . . . . . 10  |-  ( (
ph  /\  ( n  e.  CC  /\  m  e.  CC ) )  -> 
( ( p  =  ( n  +  ( M  -  1 ) )  /\  p  =  ( m  +  ( M  -  1 ) ) )  ->  n  =  m ) )
7265, 71sylan2 472 . . . . . . . . 9  |-  ( (
ph  /\  ( n  e.  ( 1 ... ( N  +  ( 1  -  M ) ) )  /\  m  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) ) )  -> 
( ( p  =  ( n  +  ( M  -  1 ) )  /\  p  =  ( m  +  ( M  -  1 ) ) )  ->  n  =  m ) )
7372ralrimivva 2875 . . . . . . . 8  |-  ( ph  ->  A. n  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) A. m  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) ( ( p  =  ( n  +  ( M  -  1 ) )  /\  p  =  ( m  +  ( M  -  1 ) ) )  ->  n  =  m ) )
7473adantr 463 . . . . . . 7  |-  ( (
ph  /\  p  e.  ( M ... N ) )  ->  A. n  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) A. m  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) ( ( p  =  ( n  +  ( M  -  1
) )  /\  p  =  ( m  +  ( M  -  1
) ) )  ->  n  =  m )
)
75 oveq1 6277 . . . . . . . . 9  |-  ( n  =  m  ->  (
n  +  ( M  -  1 ) )  =  ( m  +  ( M  -  1
) ) )
7675eqeq2d 2468 . . . . . . . 8  |-  ( n  =  m  ->  (
p  =  ( n  +  ( M  - 
1 ) )  <->  p  =  ( m  +  ( M  -  1 ) ) ) )
7776reu4 3290 . . . . . . 7  |-  ( E! n  e.  ( 1 ... ( N  +  ( 1  -  M
) ) ) p  =  ( n  +  ( M  -  1
) )  <->  ( E. n  e.  ( 1 ... ( N  +  ( 1  -  M
) ) ) p  =  ( n  +  ( M  -  1
) )  /\  A. n  e.  ( 1 ... ( N  +  ( 1  -  M
) ) ) A. m  e.  ( 1 ... ( N  +  ( 1  -  M
) ) ) ( ( p  =  ( n  +  ( M  -  1 ) )  /\  p  =  ( m  +  ( M  -  1 ) ) )  ->  n  =  m ) ) )
7860, 74, 77sylanbrc 662 . . . . . 6  |-  ( (
ph  /\  p  e.  ( M ... N ) )  ->  E! n  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) p  =  ( n  +  ( M  -  1 ) ) )
7978ralrimiva 2868 . . . . 5  |-  ( ph  ->  A. p  e.  ( M ... N ) E! n  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) p  =  ( n  +  ( M  - 
1 ) ) )
80 eqid 2454 . . . . . 6  |-  ( n  e.  ( 1 ... ( N  +  ( 1  -  M ) ) )  |->  ( n  +  ( M  - 
1 ) ) )  =  ( n  e.  ( 1 ... ( N  +  ( 1  -  M ) ) )  |->  ( n  +  ( M  -  1
) ) )
8180f1ompt 6029 . . . . 5  |-  ( ( n  e.  ( 1 ... ( N  +  ( 1  -  M
) ) )  |->  ( n  +  ( M  -  1 ) ) ) : ( 1 ... ( N  +  ( 1  -  M
) ) ) -1-1-onto-> ( M ... N )  <->  ( A. n  e.  ( 1 ... ( N  +  ( 1  -  M
) ) ) ( n  +  ( M  -  1 ) )  e.  ( M ... N )  /\  A. p  e.  ( M ... N ) E! n  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) p  =  ( n  +  ( M  -  1 ) ) ) )
8244, 79, 81sylanbrc 662 . . . 4  |-  ( ph  ->  ( n  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) 
|->  ( n  +  ( M  -  1 ) ) ) : ( 1 ... ( N  +  ( 1  -  M ) ) ) -1-1-onto-> ( M ... N ) )
83 fprodser.3 . . . . . 6  |-  ( (
ph  /\  k  e.  ( M ... N ) )  ->  A  e.  CC )
84 eqid 2454 . . . . . 6  |-  ( k  e.  ( M ... N )  |->  A )  =  ( k  e.  ( M ... N
)  |->  A )
8583, 84fmptd 6031 . . . . 5  |-  ( ph  ->  ( k  e.  ( M ... N ) 
|->  A ) : ( M ... N ) --> CC )
8685ffvelrnda 6007 . . . 4  |-  ( (
ph  /\  j  e.  ( M ... N ) )  ->  ( (
k  e.  ( M ... N )  |->  A ) `  j )  e.  CC )
87 simpr 459 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) )  ->  m  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) )
88 1zzd 10891 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) )  ->  1  e.  ZZ )
8941adantr 463 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) )  ->  ( N  +  ( 1  -  M ) )  e.  ZZ )
9063adantl 464 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) )  ->  m  e.  ZZ )
9127adantr 463 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) )  ->  ( M  -  1 )  e.  ZZ )
92 fzaddel 11722 . . . . . . . . 9  |-  ( ( ( 1  e.  ZZ  /\  ( N  +  ( 1  -  M ) )  e.  ZZ )  /\  ( m  e.  ZZ  /\  ( M  -  1 )  e.  ZZ ) )  -> 
( m  e.  ( 1 ... ( N  +  ( 1  -  M ) ) )  <-> 
( m  +  ( M  -  1 ) )  e.  ( ( 1  +  ( M  -  1 ) ) ... ( ( N  +  ( 1  -  M ) )  +  ( M  -  1 ) ) ) ) )
9388, 89, 90, 91, 92syl22anc 1227 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) )  ->  (
m  e.  ( 1 ... ( N  +  ( 1  -  M
) ) )  <->  ( m  +  ( M  - 
1 ) )  e.  ( ( 1  +  ( M  -  1 ) ) ... (
( N  +  ( 1  -  M ) )  +  ( M  -  1 ) ) ) ) )
9487, 93mpbid 210 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) )  ->  (
m  +  ( M  -  1 ) )  e.  ( ( 1  +  ( M  - 
1 ) ) ... ( ( N  +  ( 1  -  M
) )  +  ( M  -  1 ) ) ) )
9520adantr 463 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) )  ->  (
( 1  +  ( M  -  1 ) ) ... ( ( N  +  ( 1  -  M ) )  +  ( M  - 
1 ) ) )  =  ( M ... N ) )
9694, 95eleqtrd 2544 . . . . . 6  |-  ( (
ph  /\  m  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) )  ->  (
m  +  ( M  -  1 ) )  e.  ( M ... N ) )
97 fprodser.1 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( M ... N ) )  ->  ( F `  k )  =  A )
9897ralrimiva 2868 . . . . . . 7  |-  ( ph  ->  A. k  e.  ( M ... N ) ( F `  k
)  =  A )
99 nfcsb1v 3436 . . . . . . . . 9  |-  F/_ k [_ ( m  +  ( M  -  1 ) )  /  k ]_ A
10099nfeq2 2633 . . . . . . . 8  |-  F/ k ( F `  (
m  +  ( M  -  1 ) ) )  =  [_ (
m  +  ( M  -  1 ) )  /  k ]_ A
101 fveq2 5848 . . . . . . . . 9  |-  ( k  =  ( m  +  ( M  -  1
) )  ->  ( F `  k )  =  ( F `  ( m  +  ( M  -  1 ) ) ) )
102 csbeq1a 3429 . . . . . . . . 9  |-  ( k  =  ( m  +  ( M  -  1
) )  ->  A  =  [_ ( m  +  ( M  -  1
) )  /  k ]_ A )
103101, 102eqeq12d 2476 . . . . . . . 8  |-  ( k  =  ( m  +  ( M  -  1
) )  ->  (
( F `  k
)  =  A  <->  ( F `  ( m  +  ( M  -  1 ) ) )  =  [_ ( m  +  ( M  -  1 ) )  /  k ]_ A ) )
104100, 103rspc 3201 . . . . . . 7  |-  ( ( m  +  ( M  -  1 ) )  e.  ( M ... N )  ->  ( A. k  e.  ( M ... N ) ( F `  k )  =  A  ->  ( F `  ( m  +  ( M  - 
1 ) ) )  =  [_ ( m  +  ( M  - 
1 ) )  / 
k ]_ A ) )
10598, 104mpan9 467 . . . . . 6  |-  ( (
ph  /\  ( m  +  ( M  - 
1 ) )  e.  ( M ... N
) )  ->  ( F `  ( m  +  ( M  - 
1 ) ) )  =  [_ ( m  +  ( M  - 
1 ) )  / 
k ]_ A )
10696, 105syldan 468 . . . . 5  |-  ( (
ph  /\  m  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) )  ->  ( F `  ( m  +  ( M  - 
1 ) ) )  =  [_ ( m  +  ( M  - 
1 ) )  / 
k ]_ A )
107 f1of 5798 . . . . . . . 8  |-  ( ( n  e.  ( 1 ... ( N  +  ( 1  -  M
) ) )  |->  ( n  +  ( M  -  1 ) ) ) : ( 1 ... ( N  +  ( 1  -  M
) ) ) -1-1-onto-> ( M ... N )  -> 
( n  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) 
|->  ( n  +  ( M  -  1 ) ) ) : ( 1 ... ( N  +  ( 1  -  M ) ) ) --> ( M ... N
) )
10882, 107syl 16 . . . . . . 7  |-  ( ph  ->  ( n  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) 
|->  ( n  +  ( M  -  1 ) ) ) : ( 1 ... ( N  +  ( 1  -  M ) ) ) --> ( M ... N
) )
109 fvco3 5925 . . . . . . 7  |-  ( ( ( n  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) 
|->  ( n  +  ( M  -  1 ) ) ) : ( 1 ... ( N  +  ( 1  -  M ) ) ) --> ( M ... N
)  /\  m  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) )  ->  (
( F  o.  (
n  e.  ( 1 ... ( N  +  ( 1  -  M
) ) )  |->  ( n  +  ( M  -  1 ) ) ) ) `  m
)  =  ( F `
 ( ( n  e.  ( 1 ... ( N  +  ( 1  -  M ) ) )  |->  ( n  +  ( M  - 
1 ) ) ) `
 m ) ) )
110108, 109sylan 469 . . . . . 6  |-  ( (
ph  /\  m  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) )  ->  (
( F  o.  (
n  e.  ( 1 ... ( N  +  ( 1  -  M
) ) )  |->  ( n  +  ( M  -  1 ) ) ) ) `  m
)  =  ( F `
 ( ( n  e.  ( 1 ... ( N  +  ( 1  -  M ) ) )  |->  ( n  +  ( M  - 
1 ) ) ) `
 m ) ) )
111 ovex 6298 . . . . . . . . 9  |-  ( m  +  ( M  - 
1 ) )  e. 
_V
11275, 80, 111fvmpt 5931 . . . . . . . 8  |-  ( m  e.  ( 1 ... ( N  +  ( 1  -  M ) ) )  ->  (
( n  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) 
|->  ( n  +  ( M  -  1 ) ) ) `  m
)  =  ( m  +  ( M  - 
1 ) ) )
113112adantl 464 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) )  ->  (
( n  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) 
|->  ( n  +  ( M  -  1 ) ) ) `  m
)  =  ( m  +  ( M  - 
1 ) ) )
114113fveq2d 5852 . . . . . 6  |-  ( (
ph  /\  m  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) )  ->  ( F `  ( (
n  e.  ( 1 ... ( N  +  ( 1  -  M
) ) )  |->  ( n  +  ( M  -  1 ) ) ) `  m ) )  =  ( F `
 ( m  +  ( M  -  1
) ) ) )
115110, 114eqtrd 2495 . . . . 5  |-  ( (
ph  /\  m  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) )  ->  (
( F  o.  (
n  e.  ( 1 ... ( N  +  ( 1  -  M
) ) )  |->  ( n  +  ( M  -  1 ) ) ) ) `  m
)  =  ( F `
 ( m  +  ( M  -  1
) ) ) )
116113fveq2d 5852 . . . . . 6  |-  ( (
ph  /\  m  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) )  ->  (
( k  e.  ( M ... N ) 
|->  A ) `  (
( n  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) 
|->  ( n  +  ( M  -  1 ) ) ) `  m
) )  =  ( ( k  e.  ( M ... N ) 
|->  A ) `  (
m  +  ( M  -  1 ) ) ) )
11783ralrimiva 2868 . . . . . . . . 9  |-  ( ph  ->  A. k  e.  ( M ... N ) A  e.  CC )
11899nfel1 2632 . . . . . . . . . 10  |-  F/ k
[_ ( m  +  ( M  -  1
) )  /  k ]_ A  e.  CC
119102eleq1d 2523 . . . . . . . . . 10  |-  ( k  =  ( m  +  ( M  -  1
) )  ->  ( A  e.  CC  <->  [_ ( m  +  ( M  - 
1 ) )  / 
k ]_ A  e.  CC ) )
120118, 119rspc 3201 . . . . . . . . 9  |-  ( ( m  +  ( M  -  1 ) )  e.  ( M ... N )  ->  ( A. k  e.  ( M ... N ) A  e.  CC  ->  [_ (
m  +  ( M  -  1 ) )  /  k ]_ A  e.  CC ) )
121117, 120mpan9 467 . . . . . . . 8  |-  ( (
ph  /\  ( m  +  ( M  - 
1 ) )  e.  ( M ... N
) )  ->  [_ (
m  +  ( M  -  1 ) )  /  k ]_ A  e.  CC )
12296, 121syldan 468 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) )  ->  [_ (
m  +  ( M  -  1 ) )  /  k ]_ A  e.  CC )
12384fvmpts 5933 . . . . . . 7  |-  ( ( ( m  +  ( M  -  1 ) )  e.  ( M ... N )  /\  [_ ( m  +  ( M  -  1 ) )  /  k ]_ A  e.  CC )  ->  ( ( k  e.  ( M ... N
)  |->  A ) `  ( m  +  ( M  -  1 ) ) )  =  [_ ( m  +  ( M  -  1 ) )  /  k ]_ A )
12496, 122, 123syl2anc 659 . . . . . 6  |-  ( (
ph  /\  m  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) )  ->  (
( k  e.  ( M ... N ) 
|->  A ) `  (
m  +  ( M  -  1 ) ) )  =  [_ (
m  +  ( M  -  1 ) )  /  k ]_ A
)
125116, 124eqtrd 2495 . . . . 5  |-  ( (
ph  /\  m  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) )  ->  (
( k  e.  ( M ... N ) 
|->  A ) `  (
( n  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) 
|->  ( n  +  ( M  -  1 ) ) ) `  m
) )  =  [_ ( m  +  ( M  -  1 ) )  /  k ]_ A )
126106, 115, 1253eqtr4d 2505 . . . 4  |-  ( (
ph  /\  m  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) )  ->  (
( F  o.  (
n  e.  ( 1 ... ( N  +  ( 1  -  M
) ) )  |->  ( n  +  ( M  -  1 ) ) ) ) `  m
)  =  ( ( k  e.  ( M ... N )  |->  A ) `  ( ( n  e.  ( 1 ... ( N  +  ( 1  -  M
) ) )  |->  ( n  +  ( M  -  1 ) ) ) `  m ) ) )
1272, 17, 82, 86, 126fprod 13833 . . 3  |-  ( ph  ->  prod_ j  e.  ( M ... N ) ( ( k  e.  ( M ... N
)  |->  A ) `  j )  =  (  seq 1 (  x.  ,  ( F  o.  ( n  e.  (
1 ... ( N  +  ( 1  -  M
) ) )  |->  ( n  +  ( M  -  1 ) ) ) ) ) `  ( N  +  (
1  -  M ) ) ) )
128 nnuz 11117 . . . . 5  |-  NN  =  ( ZZ>= `  1 )
12917, 128syl6eleq 2552 . . . 4  |-  ( ph  ->  ( N  +  ( 1  -  M ) )  e.  ( ZZ>= ` 
1 ) )
130129, 27, 115seqshft2 12118 . . 3  |-  ( ph  ->  (  seq 1 (  x.  ,  ( F  o.  ( n  e.  ( 1 ... ( N  +  ( 1  -  M ) ) )  |->  ( n  +  ( M  -  1
) ) ) ) ) `  ( N  +  ( 1  -  M ) ) )  =  (  seq (
1  +  ( M  -  1 ) ) (  x.  ,  F
) `  ( ( N  +  ( 1  -  M ) )  +  ( M  - 
1 ) ) ) )
13118seqeq1d 12098 . . . 4  |-  ( ph  ->  seq ( 1  +  ( M  -  1 ) ) (  x.  ,  F )  =  seq M (  x.  ,  F ) )
132131, 19fveq12d 5854 . . 3  |-  ( ph  ->  (  seq ( 1  +  ( M  - 
1 ) ) (  x.  ,  F ) `
 ( ( N  +  ( 1  -  M ) )  +  ( M  -  1 ) ) )  =  (  seq M (  x.  ,  F ) `
 N ) )
133127, 130, 1323eqtrd 2499 . 2  |-  ( ph  ->  prod_ j  e.  ( M ... N ) ( ( k  e.  ( M ... N
)  |->  A ) `  j )  =  (  seq M (  x.  ,  F ) `  N ) )
1341, 133syl5eqr 2509 1  |-  ( ph  ->  prod_ k  e.  ( M ... N ) A  =  (  seq M (  x.  ,  F ) `  N
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367    = wceq 1398    e. wcel 1823   A.wral 2804   E.wrex 2805   E!wreu 2806   [.wsbc 3324   [_csb 3420    |-> cmpt 4497    o. ccom 4992   -->wf 5566   -1-1-onto->wf1o 5569   ` cfv 5570  (class class class)co 6270   CCcc 9479   1c1 9482    + caddc 9484    x. cmul 9486    - cmin 9796   NNcn 10531   NN0cn0 10791   ZZcz 10860   ZZ>=cuz 11082   ...cfz 11675    seqcseq 12092   prod_cprod 13797
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-rep 4550  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565  ax-inf2 8049  ax-cnex 9537  ax-resscn 9538  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-addrcl 9542  ax-mulcl 9543  ax-mulrcl 9544  ax-mulcom 9545  ax-addass 9546  ax-mulass 9547  ax-distr 9548  ax-i2m1 9549  ax-1ne0 9550  ax-1rid 9551  ax-rnegex 9552  ax-rrecex 9553  ax-cnre 9554  ax-pre-lttri 9555  ax-pre-lttrn 9556  ax-pre-ltadd 9557  ax-pre-mulgt0 9558  ax-pre-sup 9559
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1401  df-fal 1404  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-nel 2652  df-ral 2809  df-rex 2810  df-reu 2811  df-rmo 2812  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-tp 4021  df-op 4023  df-uni 4236  df-int 4272  df-iun 4317  df-br 4440  df-opab 4498  df-mpt 4499  df-tr 4533  df-eprel 4780  df-id 4784  df-po 4789  df-so 4790  df-fr 4827  df-se 4828  df-we 4829  df-ord 4870  df-on 4871  df-lim 4872  df-suc 4873  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578  df-isom 5579  df-riota 6232  df-ov 6273  df-oprab 6274  df-mpt2 6275  df-om 6674  df-1st 6773  df-2nd 6774  df-recs 7034  df-rdg 7068  df-1o 7122  df-oadd 7126  df-er 7303  df-en 7510  df-dom 7511  df-sdom 7512  df-fin 7513  df-sup 7893  df-oi 7927  df-card 8311  df-pnf 9619  df-mnf 9620  df-xr 9621  df-ltxr 9622  df-le 9623  df-sub 9798  df-neg 9799  df-div 10203  df-nn 10532  df-2 10590  df-3 10591  df-n0 10792  df-z 10861  df-uz 11083  df-rp 11222  df-fz 11676  df-fzo 11800  df-seq 12093  df-exp 12152  df-hash 12391  df-cj 13017  df-re 13018  df-im 13019  df-sqrt 13153  df-abs 13154  df-clim 13396  df-prod 13798
This theorem is referenced by:  fprodfac  13862  iprodclim3  13878
  Copyright terms: Public domain W3C validator