Metamath Proof Explorer


Theorem fsuppmapnn0fz

Description: If a function over the nonnegative integers is finitely supported, then there is an upper bound for a finite set of sequential integers containing the support of the function. (Contributed by AV, 30-Sep-2019) (Proof shortened by AV, 6-Oct-2019)

Ref Expression
Assertion fsuppmapnn0fz
|- ( ( F e. ( R ^m NN0 ) /\ Z e. V ) -> ( F finSupp Z -> E. m e. NN0 ( F supp Z ) C_ ( 0 ... m ) ) )

Proof

Step Hyp Ref Expression
1 fsuppmapnn0ub
 |-  ( ( F e. ( R ^m NN0 ) /\ Z e. V ) -> ( F finSupp Z -> E. m e. NN0 A. x e. NN0 ( m < x -> ( F ` x ) = Z ) ) )
2 simpllr
 |-  ( ( ( ( F e. ( R ^m NN0 ) /\ Z e. V ) /\ m e. NN0 ) /\ A. x e. NN0 ( m < x -> ( F ` x ) = Z ) ) -> Z e. V )
3 simplll
 |-  ( ( ( ( F e. ( R ^m NN0 ) /\ Z e. V ) /\ m e. NN0 ) /\ A. x e. NN0 ( m < x -> ( F ` x ) = Z ) ) -> F e. ( R ^m NN0 ) )
4 simplr
 |-  ( ( ( ( F e. ( R ^m NN0 ) /\ Z e. V ) /\ m e. NN0 ) /\ A. x e. NN0 ( m < x -> ( F ` x ) = Z ) ) -> m e. NN0 )
5 simpr
 |-  ( ( ( ( F e. ( R ^m NN0 ) /\ Z e. V ) /\ m e. NN0 ) /\ A. x e. NN0 ( m < x -> ( F ` x ) = Z ) ) -> A. x e. NN0 ( m < x -> ( F ` x ) = Z ) )
6 2 3 4 5 suppssfz
 |-  ( ( ( ( F e. ( R ^m NN0 ) /\ Z e. V ) /\ m e. NN0 ) /\ A. x e. NN0 ( m < x -> ( F ` x ) = Z ) ) -> ( F supp Z ) C_ ( 0 ... m ) )
7 6 ex
 |-  ( ( ( F e. ( R ^m NN0 ) /\ Z e. V ) /\ m e. NN0 ) -> ( A. x e. NN0 ( m < x -> ( F ` x ) = Z ) -> ( F supp Z ) C_ ( 0 ... m ) ) )
8 7 reximdva
 |-  ( ( F e. ( R ^m NN0 ) /\ Z e. V ) -> ( E. m e. NN0 A. x e. NN0 ( m < x -> ( F ` x ) = Z ) -> E. m e. NN0 ( F supp Z ) C_ ( 0 ... m ) ) )
9 1 8 syld
 |-  ( ( F e. ( R ^m NN0 ) /\ Z e. V ) -> ( F finSupp Z -> E. m e. NN0 ( F supp Z ) C_ ( 0 ... m ) ) )