This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fprodm1

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

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

Proof

Step Hyp Ref Expression
1 fprodm1.1 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
2 fprodm1.2 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> A e. CC )
3 fprodm1.3 
 |-  ( k = N -> A = B )
4 fzp1nel 
 |-  -. ( ( N - 1 ) + 1 ) e. ( M ... ( N - 1 ) )
5 eluzelz 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )
6 1 5 syl 
 |-  ( ph -> N e. ZZ )
7 6 zcnd 
 |-  ( ph -> N e. CC )
8 1cnd 
 |-  ( ph -> 1 e. CC )
9 7 8 npcand 
 |-  ( ph -> ( ( N - 1 ) + 1 ) = N )
10 9 eleq1d 
 |-  ( ph -> ( ( ( N - 1 ) + 1 ) e. ( M ... ( N - 1 ) ) <-> N e. ( M ... ( N - 1 ) ) ) )
11 4 10 mtbii 
 |-  ( ph -> -. N e. ( M ... ( N - 1 ) ) )
12 disjsn 
 |-  ( ( ( M ... ( N - 1 ) ) i^i { N } ) = (/) <-> -. N e. ( M ... ( N - 1 ) ) )
13 11 12 sylibr 
 |-  ( ph -> ( ( M ... ( N - 1 ) ) i^i { N } ) = (/) )
14 eluzel2 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ZZ )
15 1 14 syl 
 |-  ( ph -> M e. ZZ )
16 peano2zm 
 |-  ( M e. ZZ -> ( M - 1 ) e. ZZ )
17 15 16 syl 
 |-  ( ph -> ( M - 1 ) e. ZZ )
18 15 zcnd 
 |-  ( ph -> M e. CC )
19 18 8 npcand 
 |-  ( ph -> ( ( M - 1 ) + 1 ) = M )
20 19 fveq2d 
 |-  ( ph -> ( ZZ>= ` ( ( M - 1 ) + 1 ) ) = ( ZZ>= ` M ) )
21 1 20 eleqtrrd 
 |-  ( ph -> N e. ( ZZ>= ` ( ( M - 1 ) + 1 ) ) )
22 eluzp1m1 
 |-  ( ( ( M - 1 ) e. ZZ /\ N e. ( ZZ>= ` ( ( M - 1 ) + 1 ) ) ) -> ( N - 1 ) e. ( ZZ>= ` ( M - 1 ) ) )
23 17 21 22 syl2anc 
 |-  ( ph -> ( N - 1 ) e. ( ZZ>= ` ( M - 1 ) ) )
24 fzsuc2 
 |-  ( ( M e. ZZ /\ ( N - 1 ) e. ( ZZ>= ` ( M - 1 ) ) ) -> ( M ... ( ( N - 1 ) + 1 ) ) = ( ( M ... ( N - 1 ) ) u. { ( ( N - 1 ) + 1 ) } ) )
25 15 23 24 syl2anc 
 |-  ( ph -> ( M ... ( ( N - 1 ) + 1 ) ) = ( ( M ... ( N - 1 ) ) u. { ( ( N - 1 ) + 1 ) } ) )
26 9 oveq2d 
 |-  ( ph -> ( M ... ( ( N - 1 ) + 1 ) ) = ( M ... N ) )
27 9 sneqd 
 |-  ( ph -> { ( ( N - 1 ) + 1 ) } = { N } )
28 27 uneq2d 
 |-  ( ph -> ( ( M ... ( N - 1 ) ) u. { ( ( N - 1 ) + 1 ) } ) = ( ( M ... ( N - 1 ) ) u. { N } ) )
29 25 26 28 3eqtr3d 
 |-  ( ph -> ( M ... N ) = ( ( M ... ( N - 1 ) ) u. { N } ) )
30 fzfid 
 |-  ( ph -> ( M ... N ) e. Fin )
31 13 29 30 2 fprodsplit 
 |-  ( ph -> prod_ k e. ( M ... N ) A = ( prod_ k e. ( M ... ( N - 1 ) ) A x. prod_ k e. { N } A ) )
32 3 eleq1d 
 |-  ( k = N -> ( A e. CC <-> B e. CC ) )
33 2 ralrimiva 
 |-  ( ph -> A. k e. ( M ... N ) A e. CC )
34 eluzfz2 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ( M ... N ) )
35 1 34 syl 
 |-  ( ph -> N e. ( M ... N ) )
36 32 33 35 rspcdva 
 |-  ( ph -> B e. CC )
37 3 prodsn 
 |-  ( ( N e. ( ZZ>= ` M ) /\ B e. CC ) -> prod_ k e. { N } A = B )
38 1 36 37 syl2anc 
 |-  ( ph -> prod_ k e. { N } A = B )
39 38 oveq2d 
 |-  ( ph -> ( prod_ k e. ( M ... ( N - 1 ) ) A x. prod_ k e. { N } A ) = ( prod_ k e. ( M ... ( N - 1 ) ) A x. B ) )
40 31 39 eqtrd 
 |-  ( ph -> prod_ k e. ( M ... N ) A = ( prod_ k e. ( M ... ( N - 1 ) ) A x. B ) )