Metamath Proof Explorer


Theorem fprodp1s

Description: Multiply in the last term in a finite product. (Contributed by Scott Fenton, 27-Dec-2017)

Ref Expression
Hypotheses fprodp1s.1
|- ( ph -> N e. ( ZZ>= ` M ) )
fprodp1s.2
|- ( ( ph /\ k e. ( M ... ( N + 1 ) ) ) -> A e. CC )
Assertion fprodp1s
|- ( ph -> prod_ k e. ( M ... ( N + 1 ) ) A = ( prod_ k e. ( M ... N ) A x. [_ ( N + 1 ) / k ]_ A ) )

Proof

Step Hyp Ref Expression
1 fprodp1s.1
 |-  ( ph -> N e. ( ZZ>= ` M ) )
2 fprodp1s.2
 |-  ( ( ph /\ k e. ( M ... ( N + 1 ) ) ) -> A e. CC )
3 2 ralrimiva
 |-  ( ph -> A. k e. ( M ... ( N + 1 ) ) A e. CC )
4 nfcsb1v
 |-  F/_ k [_ m / k ]_ A
5 4 nfel1
 |-  F/ k [_ m / k ]_ A e. CC
6 csbeq1a
 |-  ( k = m -> A = [_ m / k ]_ A )
7 6 eleq1d
 |-  ( k = m -> ( A e. CC <-> [_ m / k ]_ A e. CC ) )
8 5 7 rspc
 |-  ( m e. ( M ... ( N + 1 ) ) -> ( A. k e. ( M ... ( N + 1 ) ) A e. CC -> [_ m / k ]_ A e. CC ) )
9 3 8 mpan9
 |-  ( ( ph /\ m e. ( M ... ( N + 1 ) ) ) -> [_ m / k ]_ A e. CC )
10 csbeq1
 |-  ( m = ( N + 1 ) -> [_ m / k ]_ A = [_ ( N + 1 ) / k ]_ A )
11 1 9 10 fprodp1
 |-  ( ph -> prod_ m e. ( M ... ( N + 1 ) ) [_ m / k ]_ A = ( prod_ m e. ( M ... N ) [_ m / k ]_ A x. [_ ( N + 1 ) / k ]_ A ) )
12 nfcv
 |-  F/_ m A
13 12 4 6 cbvprodi
 |-  prod_ k e. ( M ... ( N + 1 ) ) A = prod_ m e. ( M ... ( N + 1 ) ) [_ m / k ]_ A
14 12 4 6 cbvprodi
 |-  prod_ k e. ( M ... N ) A = prod_ m e. ( M ... N ) [_ m / k ]_ A
15 14 oveq1i
 |-  ( prod_ k e. ( M ... N ) A x. [_ ( N + 1 ) / k ]_ A ) = ( prod_ m e. ( M ... N ) [_ m / k ]_ A x. [_ ( N + 1 ) / k ]_ A )
16 11 13 15 3eqtr4g
 |-  ( ph -> prod_ k e. ( M ... ( N + 1 ) ) A = ( prod_ k e. ( M ... N ) A x. [_ ( N + 1 ) / k ]_ A ) )