Metamath Proof Explorer


Theorem zprodn0

Description: Nonzero series product with index set a subset of the upper integers. (Contributed by Scott Fenton, 6-Dec-2017)

Ref Expression
Hypotheses zprodn0.1 Z=M
zprodn0.2 φM
zprodn0.3 φX0
zprodn0.4 φseqM×FX
zprodn0.5 φAZ
zprodn0.6 φkZFk=ifkAB1
zprodn0.7 φkAB
Assertion zprodn0 φkAB=X

Proof

Step Hyp Ref Expression
1 zprodn0.1 Z=M
2 zprodn0.2 φM
3 zprodn0.3 φX0
4 zprodn0.4 φseqM×FX
5 zprodn0.5 φAZ
6 zprodn0.6 φkZFk=ifkAB1
7 zprodn0.7 φkAB
8 1 2 4 3 ntrivcvgn0 φmZxx0seqm×Fx
9 1 2 8 5 6 7 zprod φkAB=seqM×F
10 fclim :dom
11 ffun :domFun
12 10 11 ax-mp Fun
13 funbrfv FunseqM×FXseqM×F=X
14 12 4 13 mpsyl φseqM×F=X
15 9 14 eqtrd φkAB=X