Metamath Proof Explorer

Theorem fprodp1

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

Ref Expression
Hypotheses fprodp1.1 
|- ( ph -> N e. ( ZZ>= ` M ) )
fprodp1.2 
|- ( ( ph /\ k e. ( M ... ( N + 1 ) ) ) -> A e. CC )
fprodp1.3 
|- ( k = ( N + 1 ) -> A = B )
Assertion fprodp1 
|- ( ph -> prod_ k e. ( M ... ( N + 1 ) ) A = ( prod_ k e. ( M ... N ) A x. B ) )

Proof

Step Hyp Ref Expression
1 fprodp1.1 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
2 fprodp1.2 
 |-  ( ( ph /\ k e. ( M ... ( N + 1 ) ) ) -> A e. CC )
3 fprodp1.3 
 |-  ( k = ( N + 1 ) -> A = B )
4 peano2uz 
 |-  ( N e. ( ZZ>= ` M ) -> ( N + 1 ) e. ( ZZ>= ` M ) )
5 1 4 syl 
 |-  ( ph -> ( N + 1 ) e. ( ZZ>= ` M ) )
6 5 2 3 fprodm1 
 |-  ( ph -> prod_ k e. ( M ... ( N + 1 ) ) A = ( prod_ k e. ( M ... ( ( N + 1 ) - 1 ) ) A x. B ) )
7 eluzelz 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )
8 1 7 syl 
 |-  ( ph -> N e. ZZ )
9 8 zcnd 
 |-  ( ph -> N e. CC )
10 1cnd 
 |-  ( ph -> 1 e. CC )
11 9 10 pncand 
 |-  ( ph -> ( ( N + 1 ) - 1 ) = N )
12 11 oveq2d 
 |-  ( ph -> ( M ... ( ( N + 1 ) - 1 ) ) = ( M ... N ) )
13 12 prodeq1d 
 |-  ( ph -> prod_ k e. ( M ... ( ( N + 1 ) - 1 ) ) A = prod_ k e. ( M ... N ) A )
14 13 oveq1d 
 |-  ( ph -> ( prod_ k e. ( M ... ( ( N + 1 ) - 1 ) ) A x. B ) = ( prod_ k e. ( M ... N ) A x. B ) )
15 6 14 eqtrd 
 |-  ( ph -> prod_ k e. ( M ... ( N + 1 ) ) A = ( prod_ k e. ( M ... N ) A x. B ) )