Metamath Proof Explorer

Theorem suppssfz

Description: Condition for a function over the nonnegative integers to have a support contained in a finite set of sequential integers. (Contributed by AV, 9-Oct-2019)

Ref Expression
Hypotheses suppssfz.z 
|- ( ph -> Z e. V )
suppssfz.f 
|- ( ph -> F e. ( B ^m NN0 ) )
suppssfz.s 
|- ( ph -> S e. NN0 )
suppssfz.b 
|- ( ph -> A. x e. NN0 ( S < x -> ( F ` x ) = Z ) )
Assertion suppssfz 
|- ( ph -> ( F supp Z ) C_ ( 0 ... S ) )

Proof

Step Hyp Ref Expression
1 suppssfz.z 
 |-  ( ph -> Z e. V )
2 suppssfz.f 
 |-  ( ph -> F e. ( B ^m NN0 ) )
3 suppssfz.s 
 |-  ( ph -> S e. NN0 )
4 suppssfz.b 
 |-  ( ph -> A. x e. NN0 ( S < x -> ( F ` x ) = Z ) )
5 elmapfn 
 |-  ( F e. ( B ^m NN0 ) -> F Fn NN0 )
6 2 5 syl 
 |-  ( ph -> F Fn NN0 )
7 nn0ex 
 |-  NN0 e. _V
8 7 a1i 
 |-  ( ph -> NN0 e. _V )
9 6 8 1 3jca 
 |-  ( ph -> ( F Fn NN0 /\ NN0 e. _V /\ Z e. V ) )
10 9 adantr 
 |-  ( ( ph /\ A. x e. NN0 ( S < x -> ( F ` x ) = Z ) ) -> ( F Fn NN0 /\ NN0 e. _V /\ Z e. V ) )
11 elsuppfn 
 |-  ( ( F Fn NN0 /\ NN0 e. _V /\ Z e. V ) -> ( n e. ( F supp Z ) <-> ( n e. NN0 /\ ( F ` n ) =/= Z ) ) )
12 10 11 syl 
 |-  ( ( ph /\ A. x e. NN0 ( S < x -> ( F ` x ) = Z ) ) -> ( n e. ( F supp Z ) <-> ( n e. NN0 /\ ( F ` n ) =/= Z ) ) )
13 breq2 
 |-  ( x = n -> ( S < x <-> S < n ) )
14 fveqeq2 
 |-  ( x = n -> ( ( F ` x ) = Z <-> ( F ` n ) = Z ) )
15 13 14 imbi12d 
 |-  ( x = n -> ( ( S < x -> ( F ` x ) = Z ) <-> ( S < n -> ( F ` n ) = Z ) ) )
16 15 rspcva 
 |-  ( ( n e. NN0 /\ A. x e. NN0 ( S < x -> ( F ` x ) = Z ) ) -> ( S < n -> ( F ` n ) = Z ) )
17 simplr 
 |-  ( ( ( ph /\ n e. NN0 ) /\ -. S < n ) -> n e. NN0 )
18 3 adantr 
 |-  ( ( ph /\ n e. NN0 ) -> S e. NN0 )
19 18 adantr 
 |-  ( ( ( ph /\ n e. NN0 ) /\ -. S < n ) -> S e. NN0 )
20 nn0re 
 |-  ( n e. NN0 -> n e. RR )
21 nn0re 
 |-  ( S e. NN0 -> S e. RR )
22 3 21 syl 
 |-  ( ph -> S e. RR )
23 lenlt 
 |-  ( ( n e. RR /\ S e. RR ) -> ( n <_ S <-> -. S < n ) )
24 20 22 23 syl2anr 
 |-  ( ( ph /\ n e. NN0 ) -> ( n <_ S <-> -. S < n ) )
25 24 biimpar 
 |-  ( ( ( ph /\ n e. NN0 ) /\ -. S < n ) -> n <_ S )
26 elfz2nn0 
 |-  ( n e. ( 0 ... S ) <-> ( n e. NN0 /\ S e. NN0 /\ n <_ S ) )
27 17 19 25 26 syl3anbrc 
 |-  ( ( ( ph /\ n e. NN0 ) /\ -. S < n ) -> n e. ( 0 ... S ) )
28 27 a1d 
 |-  ( ( ( ph /\ n e. NN0 ) /\ -. S < n ) -> ( ( F ` n ) =/= Z -> n e. ( 0 ... S ) ) )
29 28 ex 
 |-  ( ( ph /\ n e. NN0 ) -> ( -. S < n -> ( ( F ` n ) =/= Z -> n e. ( 0 ... S ) ) ) )
30 eqneqall 
 |-  ( ( F ` n ) = Z -> ( ( F ` n ) =/= Z -> n e. ( 0 ... S ) ) )
31 30 a1i 
 |-  ( ( ph /\ n e. NN0 ) -> ( ( F ` n ) = Z -> ( ( F ` n ) =/= Z -> n e. ( 0 ... S ) ) ) )
32 29 31 jad 
 |-  ( ( ph /\ n e. NN0 ) -> ( ( S < n -> ( F ` n ) = Z ) -> ( ( F ` n ) =/= Z -> n e. ( 0 ... S ) ) ) )
33 32 com23 
 |-  ( ( ph /\ n e. NN0 ) -> ( ( F ` n ) =/= Z -> ( ( S < n -> ( F ` n ) = Z ) -> n e. ( 0 ... S ) ) ) )
34 33 ex 
 |-  ( ph -> ( n e. NN0 -> ( ( F ` n ) =/= Z -> ( ( S < n -> ( F ` n ) = Z ) -> n e. ( 0 ... S ) ) ) ) )
35 34 com14 
 |-  ( ( S < n -> ( F ` n ) = Z ) -> ( n e. NN0 -> ( ( F ` n ) =/= Z -> ( ph -> n e. ( 0 ... S ) ) ) ) )
36 16 35 syl 
 |-  ( ( n e. NN0 /\ A. x e. NN0 ( S < x -> ( F ` x ) = Z ) ) -> ( n e. NN0 -> ( ( F ` n ) =/= Z -> ( ph -> n e. ( 0 ... S ) ) ) ) )
37 36 ex 
 |-  ( n e. NN0 -> ( A. x e. NN0 ( S < x -> ( F ` x ) = Z ) -> ( n e. NN0 -> ( ( F ` n ) =/= Z -> ( ph -> n e. ( 0 ... S ) ) ) ) ) )
38 37 pm2.43a 
 |-  ( n e. NN0 -> ( A. x e. NN0 ( S < x -> ( F ` x ) = Z ) -> ( ( F ` n ) =/= Z -> ( ph -> n e. ( 0 ... S ) ) ) ) )
39 38 com23 
 |-  ( n e. NN0 -> ( ( F ` n ) =/= Z -> ( A. x e. NN0 ( S < x -> ( F ` x ) = Z ) -> ( ph -> n e. ( 0 ... S ) ) ) ) )
40 39 imp 
 |-  ( ( n e. NN0 /\ ( F ` n ) =/= Z ) -> ( A. x e. NN0 ( S < x -> ( F ` x ) = Z ) -> ( ph -> n e. ( 0 ... S ) ) ) )
41 40 com13 
 |-  ( ph -> ( A. x e. NN0 ( S < x -> ( F ` x ) = Z ) -> ( ( n e. NN0 /\ ( F ` n ) =/= Z ) -> n e. ( 0 ... S ) ) ) )
42 41 imp 
 |-  ( ( ph /\ A. x e. NN0 ( S < x -> ( F ` x ) = Z ) ) -> ( ( n e. NN0 /\ ( F ` n ) =/= Z ) -> n e. ( 0 ... S ) ) )
43 12 42 sylbid 
 |-  ( ( ph /\ A. x e. NN0 ( S < x -> ( F ` x ) = Z ) ) -> ( n e. ( F supp Z ) -> n e. ( 0 ... S ) ) )
44 43 ssrdv 
 |-  ( ( ph /\ A. x e. NN0 ( S < x -> ( F ` x ) = Z ) ) -> ( F supp Z ) C_ ( 0 ... S ) )
45 4 44 mpdan 
 |-  ( ph -> ( F supp Z ) C_ ( 0 ... S ) )