Metamath Proof Explorer


Theorem fprodser

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)

Ref Expression
Hypotheses 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 fprodser
|- ( ph -> prod_ k e. ( M ... N ) A = ( seq M ( x. , F ) ` N ) )

Proof

Step Hyp Ref Expression
1 fprodser.1
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) = A )
2 fprodser.2
 |-  ( ph -> N e. ( ZZ>= ` M ) )
3 fprodser.3
 |-  ( ( ph /\ k e. ( M ... N ) ) -> A e. CC )
4 prodfc
 |-  prod_ j e. ( M ... N ) ( ( k e. ( M ... N ) |-> A ) ` j ) = prod_ k e. ( M ... N ) A
5 fveq2
 |-  ( 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 ) ) )
6 eluzelz
 |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )
7 2 6 syl
 |-  ( ph -> N e. ZZ )
8 7 zcnd
 |-  ( ph -> N e. CC )
9 eluzel2
 |-  ( N e. ( ZZ>= ` M ) -> M e. ZZ )
10 2 9 syl
 |-  ( ph -> M e. ZZ )
11 10 zcnd
 |-  ( ph -> M e. CC )
12 1cnd
 |-  ( ph -> 1 e. CC )
13 8 11 12 subadd23d
 |-  ( ph -> ( ( N - M ) + 1 ) = ( N + ( 1 - M ) ) )
14 13 eqcomd
 |-  ( ph -> ( N + ( 1 - M ) ) = ( ( N - M ) + 1 ) )
15 uznn0sub
 |-  ( N e. ( ZZ>= ` M ) -> ( N - M ) e. NN0 )
16 2 15 syl
 |-  ( ph -> ( N - M ) e. NN0 )
17 nn0p1nn
 |-  ( ( N - M ) e. NN0 -> ( ( N - M ) + 1 ) e. NN )
18 16 17 syl
 |-  ( ph -> ( ( N - M ) + 1 ) e. NN )
19 14 18 eqeltrd
 |-  ( ph -> ( N + ( 1 - M ) ) e. NN )
20 12 11 pncan3d
 |-  ( ph -> ( 1 + ( M - 1 ) ) = M )
21 8 12 11 pnpncand
 |-  ( ph -> ( ( N + ( 1 - M ) ) + ( M - 1 ) ) = N )
22 20 21 oveq12d
 |-  ( ph -> ( ( 1 + ( M - 1 ) ) ... ( ( N + ( 1 - M ) ) + ( M - 1 ) ) ) = ( M ... N ) )
23 22 eleq2d
 |-  ( ph -> ( p e. ( ( 1 + ( M - 1 ) ) ... ( ( N + ( 1 - M ) ) + ( M - 1 ) ) ) <-> p e. ( M ... N ) ) )
24 23 biimpa
 |-  ( ( ph /\ p e. ( ( 1 + ( M - 1 ) ) ... ( ( N + ( 1 - M ) ) + ( M - 1 ) ) ) ) -> p e. ( M ... N ) )
25 elfzelz
 |-  ( p e. ( M ... N ) -> p e. ZZ )
26 25 zcnd
 |-  ( p e. ( M ... N ) -> p e. CC )
27 26 adantl
 |-  ( ( ph /\ p e. ( M ... N ) ) -> p e. CC )
28 peano2zm
 |-  ( M e. ZZ -> ( M - 1 ) e. ZZ )
29 10 28 syl
 |-  ( ph -> ( M - 1 ) e. ZZ )
30 29 zcnd
 |-  ( ph -> ( M - 1 ) e. CC )
31 30 adantr
 |-  ( ( ph /\ p e. ( M ... N ) ) -> ( M - 1 ) e. CC )
32 27 31 npcand
 |-  ( ( ph /\ p e. ( M ... N ) ) -> ( ( p - ( M - 1 ) ) + ( M - 1 ) ) = p )
33 simpr
 |-  ( ( ph /\ p e. ( M ... N ) ) -> p e. ( M ... N ) )
34 32 33 eqeltrd
 |-  ( ( ph /\ p e. ( M ... N ) ) -> ( ( p - ( M - 1 ) ) + ( M - 1 ) ) e. ( M ... N ) )
35 ovex
 |-  ( p - ( M - 1 ) ) e. _V
36 oveq1
 |-  ( n = ( p - ( M - 1 ) ) -> ( n + ( M - 1 ) ) = ( ( p - ( M - 1 ) ) + ( M - 1 ) ) )
37 36 eleq1d
 |-  ( n = ( p - ( M - 1 ) ) -> ( ( n + ( M - 1 ) ) e. ( M ... N ) <-> ( ( p - ( M - 1 ) ) + ( M - 1 ) ) e. ( M ... N ) ) )
38 35 37 sbcie
 |-  ( [. ( p - ( M - 1 ) ) / n ]. ( n + ( M - 1 ) ) e. ( M ... N ) <-> ( ( p - ( M - 1 ) ) + ( M - 1 ) ) e. ( M ... N ) )
39 34 38 sylibr
 |-  ( ( ph /\ p e. ( M ... N ) ) -> [. ( p - ( M - 1 ) ) / n ]. ( n + ( M - 1 ) ) e. ( M ... N ) )
40 24 39 syldan
 |-  ( ( ph /\ p e. ( ( 1 + ( M - 1 ) ) ... ( ( N + ( 1 - M ) ) + ( M - 1 ) ) ) ) -> [. ( p - ( M - 1 ) ) / n ]. ( n + ( M - 1 ) ) e. ( M ... N ) )
41 40 ralrimiva
 |-  ( ph -> A. p e. ( ( 1 + ( M - 1 ) ) ... ( ( N + ( 1 - M ) ) + ( M - 1 ) ) ) [. ( p - ( M - 1 ) ) / n ]. ( n + ( M - 1 ) ) e. ( M ... N ) )
42 1zzd
 |-  ( ph -> 1 e. ZZ )
43 19 nnzd
 |-  ( ph -> ( N + ( 1 - M ) ) e. ZZ )
44 fzshftral
 |-  ( ( 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 ) ) )
45 42 43 29 44 syl3anc
 |-  ( 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 ) ) )
46 41 45 mpbird
 |-  ( ph -> A. n e. ( 1 ... ( N + ( 1 - M ) ) ) ( n + ( M - 1 ) ) e. ( M ... N ) )
47 10 adantr
 |-  ( ( ph /\ p e. ( M ... N ) ) -> M e. ZZ )
48 7 adantr
 |-  ( ( ph /\ p e. ( M ... N ) ) -> N e. ZZ )
49 25 adantl
 |-  ( ( ph /\ p e. ( M ... N ) ) -> p e. ZZ )
50 29 adantr
 |-  ( ( ph /\ p e. ( M ... N ) ) -> ( M - 1 ) e. ZZ )
51 fzsubel
 |-  ( ( ( 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 ) ) ) ) )
52 47 48 49 50 51 syl22anc
 |-  ( ( ph /\ p e. ( M ... N ) ) -> ( p e. ( M ... N ) <-> ( p - ( M - 1 ) ) e. ( ( M - ( M - 1 ) ) ... ( N - ( M - 1 ) ) ) ) )
53 33 52 mpbid
 |-  ( ( ph /\ p e. ( M ... N ) ) -> ( p - ( M - 1 ) ) e. ( ( M - ( M - 1 ) ) ... ( N - ( M - 1 ) ) ) )
54 11 12 nncand
 |-  ( ph -> ( M - ( M - 1 ) ) = 1 )
55 8 11 12 subsub2d
 |-  ( ph -> ( N - ( M - 1 ) ) = ( N + ( 1 - M ) ) )
56 54 55 oveq12d
 |-  ( ph -> ( ( M - ( M - 1 ) ) ... ( N - ( M - 1 ) ) ) = ( 1 ... ( N + ( 1 - M ) ) ) )
57 56 adantr
 |-  ( ( ph /\ p e. ( M ... N ) ) -> ( ( M - ( M - 1 ) ) ... ( N - ( M - 1 ) ) ) = ( 1 ... ( N + ( 1 - M ) ) ) )
58 53 57 eleqtrd
 |-  ( ( ph /\ p e. ( M ... N ) ) -> ( p - ( M - 1 ) ) e. ( 1 ... ( N + ( 1 - M ) ) ) )
59 32 eqcomd
 |-  ( ( ph /\ p e. ( M ... N ) ) -> p = ( ( p - ( M - 1 ) ) + ( M - 1 ) ) )
60 36 rspceeqv
 |-  ( ( ( 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 ) ) )
61 58 59 60 syl2anc
 |-  ( ( ph /\ p e. ( M ... N ) ) -> E. n e. ( 1 ... ( N + ( 1 - M ) ) ) p = ( n + ( M - 1 ) ) )
62 elfzelz
 |-  ( n e. ( 1 ... ( N + ( 1 - M ) ) ) -> n e. ZZ )
63 62 zcnd
 |-  ( n e. ( 1 ... ( N + ( 1 - M ) ) ) -> n e. CC )
64 elfzelz
 |-  ( m e. ( 1 ... ( N + ( 1 - M ) ) ) -> m e. ZZ )
65 64 zcnd
 |-  ( m e. ( 1 ... ( N + ( 1 - M ) ) ) -> m e. CC )
66 63 65 anim12i
 |-  ( ( n e. ( 1 ... ( N + ( 1 - M ) ) ) /\ m e. ( 1 ... ( N + ( 1 - M ) ) ) ) -> ( n e. CC /\ m e. CC ) )
67 eqtr2
 |-  ( ( p = ( n + ( M - 1 ) ) /\ p = ( m + ( M - 1 ) ) ) -> ( n + ( M - 1 ) ) = ( m + ( M - 1 ) ) )
68 simprl
 |-  ( ( ph /\ ( n e. CC /\ m e. CC ) ) -> n e. CC )
69 simprr
 |-  ( ( ph /\ ( n e. CC /\ m e. CC ) ) -> m e. CC )
70 30 adantr
 |-  ( ( ph /\ ( n e. CC /\ m e. CC ) ) -> ( M - 1 ) e. CC )
71 68 69 70 addcan2d
 |-  ( ( ph /\ ( n e. CC /\ m e. CC ) ) -> ( ( n + ( M - 1 ) ) = ( m + ( M - 1 ) ) <-> n = m ) )
72 67 71 syl5ib
 |-  ( ( ph /\ ( n e. CC /\ m e. CC ) ) -> ( ( p = ( n + ( M - 1 ) ) /\ p = ( m + ( M - 1 ) ) ) -> n = m ) )
73 66 72 sylan2
 |-  ( ( ph /\ ( n e. ( 1 ... ( N + ( 1 - M ) ) ) /\ m e. ( 1 ... ( N + ( 1 - M ) ) ) ) ) -> ( ( p = ( n + ( M - 1 ) ) /\ p = ( m + ( M - 1 ) ) ) -> n = m ) )
74 73 ralrimivva
 |-  ( 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 ) )
75 74 adantr
 |-  ( ( 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 ) )
76 oveq1
 |-  ( n = m -> ( n + ( M - 1 ) ) = ( m + ( M - 1 ) ) )
77 76 eqeq2d
 |-  ( n = m -> ( p = ( n + ( M - 1 ) ) <-> p = ( m + ( M - 1 ) ) ) )
78 77 reu4
 |-  ( 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 ) ) )
79 61 75 78 sylanbrc
 |-  ( ( ph /\ p e. ( M ... N ) ) -> E! n e. ( 1 ... ( N + ( 1 - M ) ) ) p = ( n + ( M - 1 ) ) )
80 79 ralrimiva
 |-  ( ph -> A. p e. ( M ... N ) E! n e. ( 1 ... ( N + ( 1 - M ) ) ) p = ( n + ( M - 1 ) ) )
81 eqid
 |-  ( n e. ( 1 ... ( N + ( 1 - M ) ) ) |-> ( n + ( M - 1 ) ) ) = ( n e. ( 1 ... ( N + ( 1 - M ) ) ) |-> ( n + ( M - 1 ) ) )
82 81 f1ompt
 |-  ( ( 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 ) ) ) )
83 46 80 82 sylanbrc
 |-  ( ph -> ( n e. ( 1 ... ( N + ( 1 - M ) ) ) |-> ( n + ( M - 1 ) ) ) : ( 1 ... ( N + ( 1 - M ) ) ) -1-1-onto-> ( M ... N ) )
84 3 fmpttd
 |-  ( ph -> ( k e. ( M ... N ) |-> A ) : ( M ... N ) --> CC )
85 84 ffvelrnda
 |-  ( ( ph /\ j e. ( M ... N ) ) -> ( ( k e. ( M ... N ) |-> A ) ` j ) e. CC )
86 simpr
 |-  ( ( ph /\ m e. ( 1 ... ( N + ( 1 - M ) ) ) ) -> m e. ( 1 ... ( N + ( 1 - M ) ) ) )
87 1zzd
 |-  ( ( ph /\ m e. ( 1 ... ( N + ( 1 - M ) ) ) ) -> 1 e. ZZ )
88 43 adantr
 |-  ( ( ph /\ m e. ( 1 ... ( N + ( 1 - M ) ) ) ) -> ( N + ( 1 - M ) ) e. ZZ )
89 64 adantl
 |-  ( ( ph /\ m e. ( 1 ... ( N + ( 1 - M ) ) ) ) -> m e. ZZ )
90 29 adantr
 |-  ( ( ph /\ m e. ( 1 ... ( N + ( 1 - M ) ) ) ) -> ( M - 1 ) e. ZZ )
91 fzaddel
 |-  ( ( ( 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 ) ) ) ) )
92 87 88 89 90 91 syl22anc
 |-  ( ( 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 ) ) ) ) )
93 86 92 mpbid
 |-  ( ( ph /\ m e. ( 1 ... ( N + ( 1 - M ) ) ) ) -> ( m + ( M - 1 ) ) e. ( ( 1 + ( M - 1 ) ) ... ( ( N + ( 1 - M ) ) + ( M - 1 ) ) ) )
94 22 adantr
 |-  ( ( ph /\ m e. ( 1 ... ( N + ( 1 - M ) ) ) ) -> ( ( 1 + ( M - 1 ) ) ... ( ( N + ( 1 - M ) ) + ( M - 1 ) ) ) = ( M ... N ) )
95 93 94 eleqtrd
 |-  ( ( ph /\ m e. ( 1 ... ( N + ( 1 - M ) ) ) ) -> ( m + ( M - 1 ) ) e. ( M ... N ) )
96 1 ralrimiva
 |-  ( ph -> A. k e. ( M ... N ) ( F ` k ) = A )
97 nfcsb1v
 |-  F/_ k [_ ( m + ( M - 1 ) ) / k ]_ A
98 97 nfeq2
 |-  F/ k ( F ` ( m + ( M - 1 ) ) ) = [_ ( m + ( M - 1 ) ) / k ]_ A
99 fveq2
 |-  ( k = ( m + ( M - 1 ) ) -> ( F ` k ) = ( F ` ( m + ( M - 1 ) ) ) )
100 csbeq1a
 |-  ( k = ( m + ( M - 1 ) ) -> A = [_ ( m + ( M - 1 ) ) / k ]_ A )
101 99 100 eqeq12d
 |-  ( k = ( m + ( M - 1 ) ) -> ( ( F ` k ) = A <-> ( F ` ( m + ( M - 1 ) ) ) = [_ ( m + ( M - 1 ) ) / k ]_ A ) )
102 98 101 rspc
 |-  ( ( m + ( M - 1 ) ) e. ( M ... N ) -> ( A. k e. ( M ... N ) ( F ` k ) = A -> ( F ` ( m + ( M - 1 ) ) ) = [_ ( m + ( M - 1 ) ) / k ]_ A ) )
103 96 102 mpan9
 |-  ( ( ph /\ ( m + ( M - 1 ) ) e. ( M ... N ) ) -> ( F ` ( m + ( M - 1 ) ) ) = [_ ( m + ( M - 1 ) ) / k ]_ A )
104 95 103 syldan
 |-  ( ( ph /\ m e. ( 1 ... ( N + ( 1 - M ) ) ) ) -> ( F ` ( m + ( M - 1 ) ) ) = [_ ( m + ( M - 1 ) ) / k ]_ A )
105 f1of
 |-  ( ( 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 ) )
106 83 105 syl
 |-  ( ph -> ( n e. ( 1 ... ( N + ( 1 - M ) ) ) |-> ( n + ( M - 1 ) ) ) : ( 1 ... ( N + ( 1 - M ) ) ) --> ( M ... N ) )
107 fvco3
 |-  ( ( ( 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 ) ) )
108 106 107 sylan
 |-  ( ( 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 ) ) )
109 ovex
 |-  ( m + ( M - 1 ) ) e. _V
110 76 81 109 fvmpt
 |-  ( m e. ( 1 ... ( N + ( 1 - M ) ) ) -> ( ( n e. ( 1 ... ( N + ( 1 - M ) ) ) |-> ( n + ( M - 1 ) ) ) ` m ) = ( m + ( M - 1 ) ) )
111 110 adantl
 |-  ( ( ph /\ m e. ( 1 ... ( N + ( 1 - M ) ) ) ) -> ( ( n e. ( 1 ... ( N + ( 1 - M ) ) ) |-> ( n + ( M - 1 ) ) ) ` m ) = ( m + ( M - 1 ) ) )
112 111 fveq2d
 |-  ( ( ph /\ m e. ( 1 ... ( N + ( 1 - M ) ) ) ) -> ( F ` ( ( n e. ( 1 ... ( N + ( 1 - M ) ) ) |-> ( n + ( M - 1 ) ) ) ` m ) ) = ( F ` ( m + ( M - 1 ) ) ) )
113 108 112 eqtrd
 |-  ( ( ph /\ m e. ( 1 ... ( N + ( 1 - M ) ) ) ) -> ( ( F o. ( n e. ( 1 ... ( N + ( 1 - M ) ) ) |-> ( n + ( M - 1 ) ) ) ) ` m ) = ( F ` ( m + ( M - 1 ) ) ) )
114 111 fveq2d
 |-  ( ( 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 ) ) ) )
115 3 ralrimiva
 |-  ( ph -> A. k e. ( M ... N ) A e. CC )
116 97 nfel1
 |-  F/ k [_ ( m + ( M - 1 ) ) / k ]_ A e. CC
117 100 eleq1d
 |-  ( k = ( m + ( M - 1 ) ) -> ( A e. CC <-> [_ ( m + ( M - 1 ) ) / k ]_ A e. CC ) )
118 116 117 rspc
 |-  ( ( m + ( M - 1 ) ) e. ( M ... N ) -> ( A. k e. ( M ... N ) A e. CC -> [_ ( m + ( M - 1 ) ) / k ]_ A e. CC ) )
119 115 118 mpan9
 |-  ( ( ph /\ ( m + ( M - 1 ) ) e. ( M ... N ) ) -> [_ ( m + ( M - 1 ) ) / k ]_ A e. CC )
120 95 119 syldan
 |-  ( ( ph /\ m e. ( 1 ... ( N + ( 1 - M ) ) ) ) -> [_ ( m + ( M - 1 ) ) / k ]_ A e. CC )
121 eqid
 |-  ( k e. ( M ... N ) |-> A ) = ( k e. ( M ... N ) |-> A )
122 121 fvmpts
 |-  ( ( ( 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 )
123 95 120 122 syl2anc
 |-  ( ( ph /\ m e. ( 1 ... ( N + ( 1 - M ) ) ) ) -> ( ( k e. ( M ... N ) |-> A ) ` ( m + ( M - 1 ) ) ) = [_ ( m + ( M - 1 ) ) / k ]_ A )
124 114 123 eqtrd
 |-  ( ( 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 )
125 104 113 124 3eqtr4d
 |-  ( ( 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 ) ) )
126 5 19 83 85 125 fprod
 |-  ( 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 ) ) ) )
127 nnuz
 |-  NN = ( ZZ>= ` 1 )
128 19 127 eleqtrdi
 |-  ( ph -> ( N + ( 1 - M ) ) e. ( ZZ>= ` 1 ) )
129 128 29 113 seqshft2
 |-  ( 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 ) ) ) )
130 20 seqeq1d
 |-  ( ph -> seq ( 1 + ( M - 1 ) ) ( x. , F ) = seq M ( x. , F ) )
131 130 21 fveq12d
 |-  ( ph -> ( seq ( 1 + ( M - 1 ) ) ( x. , F ) ` ( ( N + ( 1 - M ) ) + ( M - 1 ) ) ) = ( seq M ( x. , F ) ` N ) )
132 126 129 131 3eqtrd
 |-  ( ph -> prod_ j e. ( M ... N ) ( ( k e. ( M ... N ) |-> A ) ` j ) = ( seq M ( x. , F ) ` N ) )
133 4 132 eqtr3id
 |-  ( ph -> prod_ k e. ( M ... N ) A = ( seq M ( x. , F ) ` N ) )