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

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 = ( ZZ>= ` M )
zprodn0.2 
|- ( ph -> M e. ZZ )
zprodn0.3 
|- ( ph -> X =/= 0 )
zprodn0.4 
|- ( ph -> seq M ( x. , F ) ~~> X )
zprodn0.5 
|- ( ph -> A C_ Z )
zprodn0.6 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) = if ( k e. A , B , 1 ) )
zprodn0.7 
|- ( ( ph /\ k e. A ) -> B e. CC )
Assertion zprodn0 
|- ( ph -> prod_ k e. A B = X )

Proof

Step Hyp Ref Expression
1 zprodn0.1 
 |-  Z = ( ZZ>= ` M )
2 zprodn0.2 
 |-  ( ph -> M e. ZZ )
3 zprodn0.3 
 |-  ( ph -> X =/= 0 )
4 zprodn0.4 
 |-  ( ph -> seq M ( x. , F ) ~~> X )
5 zprodn0.5 
 |-  ( ph -> A C_ Z )
6 zprodn0.6 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) = if ( k e. A , B , 1 ) )
7 zprodn0.7 
 |-  ( ( ph /\ k e. A ) -> B e. CC )
8 1 2 4 3 ntrivcvgn0 
 |-  ( ph -> E. m e. Z E. x ( x =/= 0 /\ seq m ( x. , F ) ~~> x ) )
9 1 2 8 5 6 7 zprod 
 |-  ( ph -> prod_ k e. A B = ( ~~> ` seq M ( x. , F ) ) )
10 fclim 
 |-  ~~> : dom ~~> --> CC
11 ffun 
 |-  ( ~~> : dom ~~> --> CC -> Fun ~~> )
12 10 11 ax-mp 
 |-  Fun ~~>
13 funbrfv 
 |-  ( Fun ~~> -> ( seq M ( x. , F ) ~~> X -> ( ~~> ` seq M ( x. , F ) ) = X ) )
14 12 4 13 mpsyl 
 |-  ( ph -> ( ~~> ` seq M ( x. , F ) ) = X )
15 9 14 eqtrd 
 |-  ( ph -> prod_ k e. A B = X )