Metamath Proof Explorer

Theorem prodsplit

Description: Product split into two factors, original by Steven Nguyen. (Contributed by metakunt, 21-Apr-2024)

Ref Expression
Hypotheses prodsplit.1 
|- ( ph -> M e. ZZ )
prodsplit.2 
|- ( ph -> N e. ZZ )
prodsplit.3 
|- ( ph -> M <_ N )
prodsplit.4 
|- ( ph -> K e. NN0 )
prodsplit.5 
|- ( ( ph /\ k e. ( M ... ( N + K ) ) ) -> A e. CC )
Assertion prodsplit 
|- ( ph -> prod_ k e. ( M ... ( N + K ) ) A = ( prod_ k e. ( M ... N ) A x. prod_ k e. ( ( N + 1 ) ... ( N + K ) ) A ) )

Proof

Step Hyp Ref Expression
1 prodsplit.1 
 |-  ( ph -> M e. ZZ )
2 prodsplit.2 
 |-  ( ph -> N e. ZZ )
3 prodsplit.3 
 |-  ( ph -> M <_ N )
4 prodsplit.4 
 |-  ( ph -> K e. NN0 )
5 prodsplit.5 
 |-  ( ( ph /\ k e. ( M ... ( N + K ) ) ) -> A e. CC )
6 2 zred 
 |-  ( ph -> N e. RR )
7 6 ltp1d 
 |-  ( ph -> N < ( N + 1 ) )
8 fzdisj 
 |-  ( N < ( N + 1 ) -> ( ( M ... N ) i^i ( ( N + 1 ) ... ( N + K ) ) ) = (/) )
9 7 8 syl 
 |-  ( ph -> ( ( M ... N ) i^i ( ( N + 1 ) ... ( N + K ) ) ) = (/) )
10 4 nn0zd 
 |-  ( ph -> K e. ZZ )
11 2 10 zaddcld 
 |-  ( ph -> ( N + K ) e. ZZ )
12 nn0addge1 
 |-  ( ( N e. RR /\ K e. NN0 ) -> N <_ ( N + K ) )
13 6 4 12 syl2anc 
 |-  ( ph -> N <_ ( N + K ) )
14 1 11 2 3 13 elfzd 
 |-  ( ph -> N e. ( M ... ( N + K ) ) )
15 fzsplit 
 |-  ( N e. ( M ... ( N + K ) ) -> ( M ... ( N + K ) ) = ( ( M ... N ) u. ( ( N + 1 ) ... ( N + K ) ) ) )
16 14 15 syl 
 |-  ( ph -> ( M ... ( N + K ) ) = ( ( M ... N ) u. ( ( N + 1 ) ... ( N + K ) ) ) )
17 fzfid 
 |-  ( ph -> ( M ... ( N + K ) ) e. Fin )
18 9 16 17 5 fprodsplit 
 |-  ( ph -> prod_ k e. ( M ... ( N + K ) ) A = ( prod_ k e. ( M ... N ) A x. prod_ k e. ( ( N + 1 ) ... ( N + K ) ) A ) )