Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fprodser Structured version   Unicode version

Theorem fprodser 29049
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 29045 . 2  |-  prod_ j  e.  ( M ... N
) ( ( k  e.  ( M ... N )  |->  A ) `
 j )  = 
prod_ k  e.  ( M ... N ) A
2 fveq2 5852 . . . 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 11094 . . . . . . . . 9  |-  ( N  e.  ( ZZ>= `  M
)  ->  N  e.  ZZ )
53, 4syl 16 . . . . . . . 8  |-  ( ph  ->  N  e.  ZZ )
65zcnd 10970 . . . . . . 7  |-  ( ph  ->  N  e.  CC )
7 eluzel2 11090 . . . . . . . . 9  |-  ( N  e.  ( ZZ>= `  M
)  ->  M  e.  ZZ )
83, 7syl 16 . . . . . . . 8  |-  ( ph  ->  M  e.  ZZ )
98zcnd 10970 . . . . . . 7  |-  ( ph  ->  M  e.  CC )
10 1cnd 9610 . . . . . . 7  |-  ( ph  ->  1  e.  CC )
116, 9, 10subadd23d 9953 . . . . . 6  |-  ( ph  ->  ( ( N  -  M )  +  1 )  =  ( N  +  ( 1  -  M ) ) )
1211eqcomd 2449 . . . . 5  |-  ( ph  ->  ( N  +  ( 1  -  M ) )  =  ( ( N  -  M )  +  1 ) )
13 uznn0sub 11116 . . . . . . 7  |-  ( N  e.  ( ZZ>= `  M
)  ->  ( N  -  M )  e.  NN0 )
143, 13syl 16 . . . . . 6  |-  ( ph  ->  ( N  -  M
)  e.  NN0 )
15 nn0p1nn 10836 . . . . . 6  |-  ( ( N  -  M )  e.  NN0  ->  ( ( N  -  M )  +  1 )  e.  NN )
1614, 15syl 16 . . . . 5  |-  ( ph  ->  ( ( N  -  M )  +  1 )  e.  NN )
1712, 16eqeltrd 2529 . . . 4  |-  ( ph  ->  ( N  +  ( 1  -  M ) )  e.  NN )
1810, 9pncan3d 9934 . . . . . . . . . . 11  |-  ( ph  ->  ( 1  +  ( M  -  1 ) )  =  M )
196, 10, 9pnpncand 28981 . . . . . . . . . . 11  |-  ( ph  ->  ( ( N  +  ( 1  -  M
) )  +  ( M  -  1 ) )  =  N )
2018, 19oveq12d 6295 . . . . . . . . . 10  |-  ( ph  ->  ( ( 1  +  ( M  -  1 ) ) ... (
( N  +  ( 1  -  M ) )  +  ( M  -  1 ) ) )  =  ( M ... N ) )
2120eleq2d 2511 . . . . . . . . 9  |-  ( ph  ->  ( p  e.  ( ( 1  +  ( M  -  1 ) ) ... ( ( N  +  ( 1  -  M ) )  +  ( M  - 
1 ) ) )  <-> 
p  e.  ( M ... N ) ) )
2221biimpa 484 . . . . . . . 8  |-  ( (
ph  /\  p  e.  ( ( 1  +  ( M  -  1 ) ) ... (
( N  +  ( 1  -  M ) )  +  ( M  -  1 ) ) ) )  ->  p  e.  ( M ... N
) )
23 elfzelz 11692 . . . . . . . . . . . . 13  |-  ( p  e.  ( M ... N )  ->  p  e.  ZZ )
2423zcnd 10970 . . . . . . . . . . . 12  |-  ( p  e.  ( M ... N )  ->  p  e.  CC )
2524adantl 466 . . . . . . . . . . 11  |-  ( (
ph  /\  p  e.  ( M ... N ) )  ->  p  e.  CC )
26 peano2zm 10908 . . . . . . . . . . . . . 14  |-  ( M  e.  ZZ  ->  ( M  -  1 )  e.  ZZ )
278, 26syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  ( M  -  1 )  e.  ZZ )
2827zcnd 10970 . . . . . . . . . . . 12  |-  ( ph  ->  ( M  -  1 )  e.  CC )
2928adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  p  e.  ( M ... N ) )  ->  ( M  -  1 )  e.  CC )
3025, 29npcand 9935 . . . . . . . . . 10  |-  ( (
ph  /\  p  e.  ( M ... N ) )  ->  ( (
p  -  ( M  -  1 ) )  +  ( M  - 
1 ) )  =  p )
31 simpr 461 . . . . . . . . . 10  |-  ( (
ph  /\  p  e.  ( M ... N ) )  ->  p  e.  ( M ... N ) )
3230, 31eqeltrd 2529 . . . . . . . . 9  |-  ( (
ph  /\  p  e.  ( M ... N ) )  ->  ( (
p  -  ( M  -  1 ) )  +  ( M  - 
1 ) )  e.  ( M ... N
) )
33 ovex 6305 . . . . . . . . . 10  |-  ( p  -  ( M  - 
1 ) )  e. 
_V
34 oveq1 6284 . . . . . . . . . . 11  |-  ( n  =  ( p  -  ( M  -  1
) )  ->  (
n  +  ( M  -  1 ) )  =  ( ( p  -  ( M  - 
1 ) )  +  ( M  -  1 ) ) )
3534eleq1d 2510 . . . . . . . . . 10  |-  ( n  =  ( p  -  ( M  -  1
) )  ->  (
( n  +  ( M  -  1 ) )  e.  ( M ... N )  <->  ( (
p  -  ( M  -  1 ) )  +  ( M  - 
1 ) )  e.  ( M ... N
) ) )
3633, 35sbcie 3346 . . . . . . . . 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 470 . . . . . . 7  |-  ( (
ph  /\  p  e.  ( ( 1  +  ( M  -  1 ) ) ... (
( N  +  ( 1  -  M ) )  +  ( M  -  1 ) ) ) )  ->  [. (
p  -  ( M  -  1 ) )  /  n ]. (
n  +  ( M  -  1 ) )  e.  ( M ... N ) )
3938ralrimiva 2855 . . . . . 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 10896 . . . . . . 7  |-  ( ph  ->  1  e.  ZZ )
4117nnzd 10968 . . . . . . 7  |-  ( ph  ->  ( N  +  ( 1  -  M ) )  e.  ZZ )
42 fzshftral 11769 . . . . . . 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 1227 . . . . . 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 465 . . . . . . . . . . 11  |-  ( (
ph  /\  p  e.  ( M ... N ) )  ->  M  e.  ZZ )
465adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  p  e.  ( M ... N ) )  ->  N  e.  ZZ )
4723adantl 466 . . . . . . . . . . 11  |-  ( (
ph  /\  p  e.  ( M ... N ) )  ->  p  e.  ZZ )
4827adantr 465 . . . . . . . . . . 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 1228 . . . . . . . . . 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 9936 . . . . . . . . . . 11  |-  ( ph  ->  ( M  -  ( M  -  1 ) )  =  1 )
536, 9, 10subsub2d 9960 . . . . . . . . . . 11  |-  ( ph  ->  ( N  -  ( M  -  1 ) )  =  ( N  +  ( 1  -  M ) ) )
5452, 53oveq12d 6295 . . . . . . . . . 10  |-  ( ph  ->  ( ( M  -  ( M  -  1
) ) ... ( N  -  ( M  -  1 ) ) )  =  ( 1 ... ( N  +  ( 1  -  M
) ) ) )
5554adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  p  e.  ( M ... N ) )  ->  ( ( M  -  ( M  -  1 ) ) ... ( N  -  ( M  -  1
) ) )  =  ( 1 ... ( N  +  ( 1  -  M ) ) ) )
5651, 55eleqtrd 2531 . . . . . . . 8  |-  ( (
ph  /\  p  e.  ( M ... N ) )  ->  ( p  -  ( M  - 
1 ) )  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) )
5730eqcomd 2449 . . . . . . . 8  |-  ( (
ph  /\  p  e.  ( M ... N ) )  ->  p  =  ( ( p  -  ( M  -  1
) )  +  ( M  -  1 ) ) )
5834eqeq2d 2455 . . . . . . . . 9  |-  ( n  =  ( p  -  ( M  -  1
) )  ->  (
p  =  ( n  +  ( M  - 
1 ) )  <->  p  =  ( ( p  -  ( M  -  1
) )  +  ( M  -  1 ) ) ) )
5958rspcev 3194 . . . . . . . 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 661 . . . . . . 7  |-  ( (
ph  /\  p  e.  ( M ... N ) )  ->  E. n  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) p  =  ( n  +  ( M  -  1 ) ) )
61 elfzelz 11692 . . . . . . . . . . . 12  |-  ( n  e.  ( 1 ... ( N  +  ( 1  -  M ) ) )  ->  n  e.  ZZ )
6261zcnd 10970 . . . . . . . . . . 11  |-  ( n  e.  ( 1 ... ( N  +  ( 1  -  M ) ) )  ->  n  e.  CC )
63 elfzelz 11692 . . . . . . . . . . . 12  |-  ( m  e.  ( 1 ... ( N  +  ( 1  -  M ) ) )  ->  m  e.  ZZ )
6463zcnd 10970 . . . . . . . . . . 11  |-  ( m  e.  ( 1 ... ( N  +  ( 1  -  M ) ) )  ->  m  e.  CC )
6562, 64anim12i 566 . . . . . . . . . 10  |-  ( ( n  e.  ( 1 ... ( N  +  ( 1  -  M
) ) )  /\  m  e.  ( 1 ... ( N  +  ( 1  -  M
) ) ) )  ->  ( n  e.  CC  /\  m  e.  CC ) )
66 eqtr2 2468 . . . . . . . . . . 11  |-  ( ( p  =  ( n  +  ( M  - 
1 ) )  /\  p  =  ( m  +  ( M  - 
1 ) ) )  ->  ( n  +  ( M  -  1
) )  =  ( m  +  ( M  -  1 ) ) )
67 simprl 755 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( n  e.  CC  /\  m  e.  CC ) )  ->  n  e.  CC )
68 simprr 756 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( n  e.  CC  /\  m  e.  CC ) )  ->  m  e.  CC )
6928adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( n  e.  CC  /\  m  e.  CC ) )  -> 
( M  -  1 )  e.  CC )
7067, 68, 69addcan2d 9782 . . . . . . . . . . 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 474 . . . . . . . . 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 2862 . . . . . . . 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 465 . . . . . . 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 6284 . . . . . . . . 9  |-  ( n  =  m  ->  (
n  +  ( M  -  1 ) )  =  ( m  +  ( M  -  1
) ) )
7675eqeq2d 2455 . . . . . . . 8  |-  ( n  =  m  ->  (
p  =  ( n  +  ( M  - 
1 ) )  <->  p  =  ( m  +  ( M  -  1 ) ) ) )
7776reu4 3277 . . . . . . 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 664 . . . . . 6  |-  ( (
ph  /\  p  e.  ( M ... N ) )  ->  E! n  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) p  =  ( n  +  ( M  -  1 ) ) )
7978ralrimiva 2855 . . . . 5  |-  ( ph  ->  A. p  e.  ( M ... N ) E! n  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) p  =  ( n  +  ( M  - 
1 ) ) )
80 eqid 2441 . . . . . 6  |-  ( n  e.  ( 1 ... ( N  +  ( 1  -  M ) ) )  |->  ( n  +  ( M  - 
1 ) ) )  =  ( n  e.  ( 1 ... ( N  +  ( 1  -  M ) ) )  |->  ( n  +  ( M  -  1
) ) )
8180f1ompt 6034 . . . . 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 664 . . . 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 2441 . . . . . 6  |-  ( k  e.  ( M ... N )  |->  A )  =  ( k  e.  ( M ... N
)  |->  A )
8583, 84fmptd 6036 . . . . 5  |-  ( ph  ->  ( k  e.  ( M ... N ) 
|->  A ) : ( M ... N ) --> CC )
8685ffvelrnda 6012 . . . 4  |-  ( (
ph  /\  j  e.  ( M ... N ) )  ->  ( (
k  e.  ( M ... N )  |->  A ) `  j )  e.  CC )
87 simpr 461 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) )  ->  m  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) )
88 1zzd 10896 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) )  ->  1  e.  ZZ )
8941adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) )  ->  ( N  +  ( 1  -  M ) )  e.  ZZ )
9063adantl 466 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) )  ->  m  e.  ZZ )
9127adantr 465 . . . . . . . . 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 1228 . . . . . . . 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 465 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) )  ->  (
( 1  +  ( M  -  1 ) ) ... ( ( N  +  ( 1  -  M ) )  +  ( M  - 
1 ) ) )  =  ( M ... N ) )
9694, 95eleqtrd 2531 . . . . . 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 2855 . . . . . . 7  |-  ( ph  ->  A. k  e.  ( M ... N ) ( F `  k
)  =  A )
99 nfcsb1v 3433 . . . . . . . . 9  |-  F/_ k [_ ( m  +  ( M  -  1 ) )  /  k ]_ A
10099nfeq2 2620 . . . . . . . 8  |-  F/ k ( F `  (
m  +  ( M  -  1 ) ) )  =  [_ (
m  +  ( M  -  1 ) )  /  k ]_ A
101 fveq2 5852 . . . . . . . . 9  |-  ( k  =  ( m  +  ( M  -  1
) )  ->  ( F `  k )  =  ( F `  ( m  +  ( M  -  1 ) ) ) )
102 csbeq1a 3426 . . . . . . . . 9  |-  ( k  =  ( m  +  ( M  -  1
) )  ->  A  =  [_ ( m  +  ( M  -  1
) )  /  k ]_ A )
103101, 102eqeq12d 2463 . . . . . . . 8  |-  ( k  =  ( m  +  ( M  -  1
) )  ->  (
( F `  k
)  =  A  <->  ( F `  ( m  +  ( M  -  1 ) ) )  =  [_ ( m  +  ( M  -  1 ) )  /  k ]_ A ) )
104100, 103rspc 3188 . . . . . . 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 469 . . . . . 6  |-  ( (
ph  /\  ( m  +  ( M  - 
1 ) )  e.  ( M ... N
) )  ->  ( F `  ( m  +  ( M  - 
1 ) ) )  =  [_ ( m  +  ( M  - 
1 ) )  / 
k ]_ A )
10696, 105syldan 470 . . . . 5  |-  ( (
ph  /\  m  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) )  ->  ( F `  ( m  +  ( M  - 
1 ) ) )  =  [_ ( m  +  ( M  - 
1 ) )  / 
k ]_ A )
107 f1of 5802 . . . . . . . 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 5931 . . . . . . 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 471 . . . . . 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 6305 . . . . . . . . 9  |-  ( m  +  ( M  - 
1 ) )  e. 
_V
11275, 80, 111fvmpt 5937 . . . . . . . 8  |-  ( m  e.  ( 1 ... ( N  +  ( 1  -  M ) ) )  ->  (
( n  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) 
|->  ( n  +  ( M  -  1 ) ) ) `  m
)  =  ( m  +  ( M  - 
1 ) ) )
113112adantl 466 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) )  ->  (
( n  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) 
|->  ( n  +  ( M  -  1 ) ) ) `  m
)  =  ( m  +  ( M  - 
1 ) ) )
114113fveq2d 5856 . . . . . 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 2482 . . . . 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 5856 . . . . . 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 2855 . . . . . . . . 9  |-  ( ph  ->  A. k  e.  ( M ... N ) A  e.  CC )
11899nfel1 2619 . . . . . . . . . 10  |-  F/ k
[_ ( m  +  ( M  -  1
) )  /  k ]_ A  e.  CC
119102eleq1d 2510 . . . . . . . . . 10  |-  ( k  =  ( m  +  ( M  -  1
) )  ->  ( A  e.  CC  <->  [_ ( m  +  ( M  - 
1 ) )  / 
k ]_ A  e.  CC ) )
120118, 119rspc 3188 . . . . . . . . 9  |-  ( ( m  +  ( M  -  1 ) )  e.  ( M ... N )  ->  ( A. k  e.  ( M ... N ) A  e.  CC  ->  [_ (
m  +  ( M  -  1 ) )  /  k ]_ A  e.  CC ) )
121117, 120mpan9 469 . . . . . . . 8  |-  ( (
ph  /\  ( m  +  ( M  - 
1 ) )  e.  ( M ... N
) )  ->  [_ (
m  +  ( M  -  1 ) )  /  k ]_ A  e.  CC )
12296, 121syldan 470 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) )  ->  [_ (
m  +  ( M  -  1 ) )  /  k ]_ A  e.  CC )
12384fvmpts 5939 . . . . . . 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 661 . . . . . 6  |-  ( (
ph  /\  m  e.  ( 1 ... ( N  +  ( 1  -  M ) ) ) )  ->  (
( k  e.  ( M ... N ) 
|->  A ) `  (
m  +  ( M  -  1 ) ) )  =  [_ (
m  +  ( M  -  1 ) )  /  k ]_ A
)
125116, 124eqtrd 2482 . . . . 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 2492 . . . 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 29041 . . 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 11120 . . . . 5  |-  NN  =  ( ZZ>= `  1 )
12917, 128syl6eleq 2539 . . . 4  |-  ( ph  ->  ( N  +  ( 1  -  M ) )  e.  ( ZZ>= ` 
1 ) )
130129, 27, 115seqshft2 12107 . . 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 12087 . . . 4  |-  ( ph  ->  seq ( 1  +  ( M  -  1 ) ) (  x.  ,  F )  =  seq M (  x.  ,  F ) )
132131, 19fveq12d 5858 . . 3  |-  ( ph  ->  (  seq ( 1  +  ( M  - 
1 ) ) (  x.  ,  F ) `
 ( ( N  +  ( 1  -  M ) )  +  ( M  -  1 ) ) )  =  (  seq M (  x.  ,  F ) `
 N ) )
133127, 130, 1323eqtrd 2486 . 2  |-  ( ph  ->  prod_ j  e.  ( M ... N ) ( ( k  e.  ( M ... N
)  |->  A ) `  j )  =  (  seq M (  x.  ,  F ) `  N ) )
1341, 133syl5eqr 2496 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 369    = wceq 1381    e. wcel 1802   A.wral 2791   E.wrex 2792   E!wreu 2793   [.wsbc 3311   [_csb 3417    |-> cmpt 4491    o. ccom 4989   -->wf 5570   -1-1-onto->wf1o 5573   ` cfv 5574  (class class class)co 6277   CCcc 9488   1c1 9491    + caddc 9493    x. cmul 9495    - cmin 9805   NNcn 10537   NN0cn0 10796   ZZcz 10865   ZZ>=cuz 11085   ...cfz 11676    seqcseq 12081   prod_cprod 29005
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-rep 4544  ax-sep 4554  ax-nul 4562  ax-pow 4611  ax-pr 4672  ax-un 6573  ax-inf2 8056  ax-cnex 9546  ax-resscn 9547  ax-1cn 9548  ax-icn 9549  ax-addcl 9550  ax-addrcl 9551  ax-mulcl 9552  ax-mulrcl 9553  ax-mulcom 9554  ax-addass 9555  ax-mulass 9556  ax-distr 9557  ax-i2m1 9558  ax-1ne0 9559  ax-1rid 9560  ax-rnegex 9561  ax-rrecex 9562  ax-cnre 9563  ax-pre-lttri 9564  ax-pre-lttrn 9565  ax-pre-ltadd 9566  ax-pre-mulgt0 9567  ax-pre-sup 9568
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 973  df-3an 974  df-tru 1384  df-fal 1387  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-nel 2639  df-ral 2796  df-rex 2797  df-reu 2798  df-rmo 2799  df-rab 2800  df-v 3095  df-sbc 3312  df-csb 3418  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-pss 3474  df-nul 3768  df-if 3923  df-pw 3995  df-sn 4011  df-pr 4013  df-tp 4015  df-op 4017  df-uni 4231  df-int 4268  df-iun 4313  df-br 4434  df-opab 4492  df-mpt 4493  df-tr 4527  df-eprel 4777  df-id 4781  df-po 4786  df-so 4787  df-fr 4824  df-se 4825  df-we 4826  df-ord 4867  df-on 4868  df-lim 4869  df-suc 4870  df-xp 4991  df-rel 4992  df-cnv 4993  df-co 4994  df-dm 4995  df-rn 4996  df-res 4997  df-ima 4998  df-iota 5537  df-fun 5576  df-fn 5577  df-f 5578  df-f1 5579  df-fo 5580  df-f1o 5581  df-fv 5582  df-isom 5583  df-riota 6238  df-ov 6280  df-oprab 6281  df-mpt2 6282  df-om 6682  df-1st 6781  df-2nd 6782  df-recs 7040  df-rdg 7074  df-1o 7128  df-oadd 7132  df-er 7309  df-en 7515  df-dom 7516  df-sdom 7517  df-fin 7518  df-sup 7899  df-oi 7933  df-card 8318  df-pnf 9628  df-mnf 9629  df-xr 9630  df-ltxr 9631  df-le 9632  df-sub 9807  df-neg 9808  df-div 10208  df-nn 10538  df-2 10595  df-3 10596  df-n0 10797  df-z 10866  df-uz 11086  df-rp 11225  df-fz 11677  df-fzo 11799  df-seq 12082  df-exp 12141  df-hash 12380  df-cj 12906  df-re 12907  df-im 12908  df-sqrt 13042  df-abs 13043  df-clim 13285  df-prod 29006
This theorem is referenced by:  fprodfac  29070  iprodclim3  29087
  Copyright terms: Public domain W3C validator