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