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 } ) )