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 ) )