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

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