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 ) )`