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 φNM
fprod1p.2 φkMNA
fprod1p.3 k=MA=B
Assertion fprod1p φk=MNA=Bk=M+1NA

Proof

Step Hyp Ref Expression
1 fprod1p.1 φNM
2 fprod1p.2 φkMNA
3 fprod1p.3 k=MA=B
4 eluzfz1 NMMMN
5 1 4 syl φMMN
6 5 elfzelzd φM
7 fzsn MMM=M
8 6 7 syl φMM=M
9 8 ineq1d φMMM+1N=MM+1N
10 6 zred φM
11 10 ltp1d φM<M+1
12 fzdisj M<M+1MMM+1N=
13 11 12 syl φMMM+1N=
14 9 13 eqtr3d φMM+1N=
15 fzsplit MMNMN=MMM+1N
16 5 15 syl φMN=MMM+1N
17 8 uneq1d φMMM+1N=MM+1N
18 16 17 eqtrd φMN=MM+1N
19 fzfid φMNFin
20 14 18 19 2 fprodsplit φk=MNA=kMAk=M+1NA
21 3 eleq1d k=MAB
22 2 ralrimiva φkMNA
23 21 22 5 rspcdva φB
24 3 prodsn MMNBkMA=B
25 5 23 24 syl2anc φkMA=B
26 25 oveq1d φkMAk=M+1NA=Bk=M+1NA
27 20 26 eqtrd φk=MNA=Bk=M+1NA