Metamath Proof Explorer

Theorem fprod1p

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

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

Proof

Step Hyp Ref Expression
1 fprod1p.1 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
2 fprod1p.2 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> A e. CC )
3 fprod1p.3 
 |-  ( k = M -> A = B )
4 eluzfz1 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ( M ... N ) )
5 1 4 syl 
 |-  ( ph -> M e. ( M ... N ) )
6 elfzelz 
 |-  ( M e. ( M ... N ) -> M e. ZZ )
7 5 6 syl 
 |-  ( ph -> M e. ZZ )
8 fzsn 
 |-  ( M e. ZZ -> ( M ... M ) = { M } )
9 7 8 syl 
 |-  ( ph -> ( M ... M ) = { M } )
10 9 ineq1d 
 |-  ( ph -> ( ( M ... M ) i^i ( ( M + 1 ) ... N ) ) = ( { M } i^i ( ( M + 1 ) ... N ) ) )
11 7 zred 
 |-  ( ph -> M e. RR )
12 11 ltp1d 
 |-  ( ph -> M < ( M + 1 ) )
13 fzdisj 
 |-  ( M < ( M + 1 ) -> ( ( M ... M ) i^i ( ( M + 1 ) ... N ) ) = (/) )
14 12 13 syl 
 |-  ( ph -> ( ( M ... M ) i^i ( ( M + 1 ) ... N ) ) = (/) )
15 10 14 eqtr3d 
 |-  ( ph -> ( { M } i^i ( ( M + 1 ) ... N ) ) = (/) )
16 fzsplit 
 |-  ( M e. ( M ... N ) -> ( M ... N ) = ( ( M ... M ) u. ( ( M + 1 ) ... N ) ) )
17 5 16 syl 
 |-  ( ph -> ( M ... N ) = ( ( M ... M ) u. ( ( M + 1 ) ... N ) ) )
18 9 uneq1d 
 |-  ( ph -> ( ( M ... M ) u. ( ( M + 1 ) ... N ) ) = ( { M } u. ( ( M + 1 ) ... N ) ) )
19 17 18 eqtrd 
 |-  ( ph -> ( M ... N ) = ( { M } u. ( ( M + 1 ) ... N ) ) )
20 fzfid 
 |-  ( ph -> ( M ... N ) e. Fin )
21 15 19 20 2 fprodsplit 
 |-  ( ph -> prod_ k e. ( M ... N ) A = ( prod_ k e. { M } A x. prod_ k e. ( ( M + 1 ) ... N ) A ) )
22 3 eleq1d 
 |-  ( k = M -> ( A e. CC <-> B e. CC ) )
23 2 ralrimiva 
 |-  ( ph -> A. k e. ( M ... N ) A e. CC )
24 22 23 5 rspcdva 
 |-  ( ph -> B e. CC )
25 3 prodsn 
 |-  ( ( M e. ( M ... N ) /\ B e. CC ) -> prod_ k e. { M } A = B )
26 5 24 25 syl2anc 
 |-  ( ph -> prod_ k e. { M } A = B )
27 26 oveq1d 
 |-  ( ph -> ( prod_ k e. { M } A x. prod_ k e. ( ( M + 1 ) ... N ) A ) = ( B x. prod_ k e. ( ( M + 1 ) ... N ) A ) )
28 21 27 eqtrd 
 |-  ( ph -> prod_ k e. ( M ... N ) A = ( B x. prod_ k e. ( ( M + 1 ) ... N ) A ) )