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