Metamath Proof Explorer

Theorem prodf1f

Description: A one-valued infinite product is equal to the constant one function. (Contributed by Scott Fenton, 5-Dec-2017)

Ref Expression
Hypothesis prodf1.1 
|- Z = ( ZZ>= ` M )
Assertion prodf1f 
|- ( M e. ZZ -> seq M ( x. , ( Z X. { 1 } ) ) = ( Z X. { 1 } ) )

Proof

Step Hyp Ref Expression
1 prodf1.1 
 |-  Z = ( ZZ>= ` M )
2 1 prodf1 
 |-  ( k e. Z -> ( seq M ( x. , ( Z X. { 1 } ) ) ` k ) = 1 )
3 1ex 
 |-  1 e. _V
4 3 fvconst2 
 |-  ( k e. Z -> ( ( Z X. { 1 } ) ` k ) = 1 )
5 2 4 eqtr4d 
 |-  ( k e. Z -> ( seq M ( x. , ( Z X. { 1 } ) ) ` k ) = ( ( Z X. { 1 } ) ` k ) )
6 5 rgen 
 |-  A. k e. Z ( seq M ( x. , ( Z X. { 1 } ) ) ` k ) = ( ( Z X. { 1 } ) ` k )
7 seqfn 
 |-  ( M e. ZZ -> seq M ( x. , ( Z X. { 1 } ) ) Fn ( ZZ>= ` M ) )
8 1 fneq2i 
 |-  ( seq M ( x. , ( Z X. { 1 } ) ) Fn Z <-> seq M ( x. , ( Z X. { 1 } ) ) Fn ( ZZ>= ` M ) )
9 7 8 sylibr 
 |-  ( M e. ZZ -> seq M ( x. , ( Z X. { 1 } ) ) Fn Z )
10 3 fconst 
 |-  ( Z X. { 1 } ) : Z --> { 1 }
11 ffn 
 |-  ( ( Z X. { 1 } ) : Z --> { 1 } -> ( Z X. { 1 } ) Fn Z )
12 10 11 ax-mp 
 |-  ( Z X. { 1 } ) Fn Z
13 eqfnfv 
 |-  ( ( seq M ( x. , ( Z X. { 1 } ) ) Fn Z /\ ( Z X. { 1 } ) Fn Z ) -> ( seq M ( x. , ( Z X. { 1 } ) ) = ( Z X. { 1 } ) <-> A. k e. Z ( seq M ( x. , ( Z X. { 1 } ) ) ` k ) = ( ( Z X. { 1 } ) ` k ) ) )
14 9 12 13 sylancl 
 |-  ( M e. ZZ -> ( seq M ( x. , ( Z X. { 1 } ) ) = ( Z X. { 1 } ) <-> A. k e. Z ( seq M ( x. , ( Z X. { 1 } ) ) ` k ) = ( ( Z X. { 1 } ) ` k ) ) )
15 6 14 mpbiri 
 |-  ( M e. ZZ -> seq M ( x. , ( Z X. { 1 } ) ) = ( Z X. { 1 } ) )