Metamath Proof Explorer


Theorem plyco0

Description: Two ways to say that a function on the nonnegative integers has finite support. (Contributed by Mario Carneiro, 22-Jul-2014)

Ref Expression
Assertion plyco0
|- ( ( N e. NN0 /\ A : NN0 --> CC ) -> ( ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } <-> A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) ) )

Proof

Step Hyp Ref Expression
1 simprr
 |-  ( ( ( ( N e. NN0 /\ A : NN0 --> CC ) /\ ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } ) /\ ( k e. NN0 /\ ( A ` k ) =/= 0 ) ) -> ( A ` k ) =/= 0 )
2 ffun
 |-  ( A : NN0 --> CC -> Fun A )
3 2 adantl
 |-  ( ( N e. NN0 /\ A : NN0 --> CC ) -> Fun A )
4 peano2nn0
 |-  ( N e. NN0 -> ( N + 1 ) e. NN0 )
5 4 adantr
 |-  ( ( N e. NN0 /\ A : NN0 --> CC ) -> ( N + 1 ) e. NN0 )
6 eluznn0
 |-  ( ( ( N + 1 ) e. NN0 /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> k e. NN0 )
7 6 ex
 |-  ( ( N + 1 ) e. NN0 -> ( k e. ( ZZ>= ` ( N + 1 ) ) -> k e. NN0 ) )
8 5 7 syl
 |-  ( ( N e. NN0 /\ A : NN0 --> CC ) -> ( k e. ( ZZ>= ` ( N + 1 ) ) -> k e. NN0 ) )
9 8 ssrdv
 |-  ( ( N e. NN0 /\ A : NN0 --> CC ) -> ( ZZ>= ` ( N + 1 ) ) C_ NN0 )
10 fdm
 |-  ( A : NN0 --> CC -> dom A = NN0 )
11 10 adantl
 |-  ( ( N e. NN0 /\ A : NN0 --> CC ) -> dom A = NN0 )
12 9 11 sseqtrrd
 |-  ( ( N e. NN0 /\ A : NN0 --> CC ) -> ( ZZ>= ` ( N + 1 ) ) C_ dom A )
13 funfvima2
 |-  ( ( Fun A /\ ( ZZ>= ` ( N + 1 ) ) C_ dom A ) -> ( k e. ( ZZ>= ` ( N + 1 ) ) -> ( A ` k ) e. ( A " ( ZZ>= ` ( N + 1 ) ) ) ) )
14 3 12 13 syl2anc
 |-  ( ( N e. NN0 /\ A : NN0 --> CC ) -> ( k e. ( ZZ>= ` ( N + 1 ) ) -> ( A ` k ) e. ( A " ( ZZ>= ` ( N + 1 ) ) ) ) )
15 14 ad2antrr
 |-  ( ( ( ( N e. NN0 /\ A : NN0 --> CC ) /\ ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } ) /\ ( k e. NN0 /\ ( A ` k ) =/= 0 ) ) -> ( k e. ( ZZ>= ` ( N + 1 ) ) -> ( A ` k ) e. ( A " ( ZZ>= ` ( N + 1 ) ) ) ) )
16 nn0z
 |-  ( N e. NN0 -> N e. ZZ )
17 16 adantr
 |-  ( ( N e. NN0 /\ A : NN0 --> CC ) -> N e. ZZ )
18 17 peano2zd
 |-  ( ( N e. NN0 /\ A : NN0 --> CC ) -> ( N + 1 ) e. ZZ )
19 18 ad2antrr
 |-  ( ( ( ( N e. NN0 /\ A : NN0 --> CC ) /\ ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } ) /\ ( k e. NN0 /\ ( A ` k ) =/= 0 ) ) -> ( N + 1 ) e. ZZ )
20 nn0z
 |-  ( k e. NN0 -> k e. ZZ )
21 20 ad2antrl
 |-  ( ( ( ( N e. NN0 /\ A : NN0 --> CC ) /\ ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } ) /\ ( k e. NN0 /\ ( A ` k ) =/= 0 ) ) -> k e. ZZ )
22 eluz
 |-  ( ( ( N + 1 ) e. ZZ /\ k e. ZZ ) -> ( k e. ( ZZ>= ` ( N + 1 ) ) <-> ( N + 1 ) <_ k ) )
23 19 21 22 syl2anc
 |-  ( ( ( ( N e. NN0 /\ A : NN0 --> CC ) /\ ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } ) /\ ( k e. NN0 /\ ( A ` k ) =/= 0 ) ) -> ( k e. ( ZZ>= ` ( N + 1 ) ) <-> ( N + 1 ) <_ k ) )
24 simplr
 |-  ( ( ( ( N e. NN0 /\ A : NN0 --> CC ) /\ ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } ) /\ ( k e. NN0 /\ ( A ` k ) =/= 0 ) ) -> ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )
25 24 eleq2d
 |-  ( ( ( ( N e. NN0 /\ A : NN0 --> CC ) /\ ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } ) /\ ( k e. NN0 /\ ( A ` k ) =/= 0 ) ) -> ( ( A ` k ) e. ( A " ( ZZ>= ` ( N + 1 ) ) ) <-> ( A ` k ) e. { 0 } ) )
26 fvex
 |-  ( A ` k ) e. _V
27 26 elsn
 |-  ( ( A ` k ) e. { 0 } <-> ( A ` k ) = 0 )
28 25 27 bitrdi
 |-  ( ( ( ( N e. NN0 /\ A : NN0 --> CC ) /\ ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } ) /\ ( k e. NN0 /\ ( A ` k ) =/= 0 ) ) -> ( ( A ` k ) e. ( A " ( ZZ>= ` ( N + 1 ) ) ) <-> ( A ` k ) = 0 ) )
29 15 23 28 3imtr3d
 |-  ( ( ( ( N e. NN0 /\ A : NN0 --> CC ) /\ ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } ) /\ ( k e. NN0 /\ ( A ` k ) =/= 0 ) ) -> ( ( N + 1 ) <_ k -> ( A ` k ) = 0 ) )
30 29 necon3ad
 |-  ( ( ( ( N e. NN0 /\ A : NN0 --> CC ) /\ ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } ) /\ ( k e. NN0 /\ ( A ` k ) =/= 0 ) ) -> ( ( A ` k ) =/= 0 -> -. ( N + 1 ) <_ k ) )
31 1 30 mpd
 |-  ( ( ( ( N e. NN0 /\ A : NN0 --> CC ) /\ ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } ) /\ ( k e. NN0 /\ ( A ` k ) =/= 0 ) ) -> -. ( N + 1 ) <_ k )
32 nn0re
 |-  ( k e. NN0 -> k e. RR )
33 32 ad2antrl
 |-  ( ( ( ( N e. NN0 /\ A : NN0 --> CC ) /\ ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } ) /\ ( k e. NN0 /\ ( A ` k ) =/= 0 ) ) -> k e. RR )
34 18 zred
 |-  ( ( N e. NN0 /\ A : NN0 --> CC ) -> ( N + 1 ) e. RR )
35 34 ad2antrr
 |-  ( ( ( ( N e. NN0 /\ A : NN0 --> CC ) /\ ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } ) /\ ( k e. NN0 /\ ( A ` k ) =/= 0 ) ) -> ( N + 1 ) e. RR )
36 33 35 ltnled
 |-  ( ( ( ( N e. NN0 /\ A : NN0 --> CC ) /\ ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } ) /\ ( k e. NN0 /\ ( A ` k ) =/= 0 ) ) -> ( k < ( N + 1 ) <-> -. ( N + 1 ) <_ k ) )
37 31 36 mpbird
 |-  ( ( ( ( N e. NN0 /\ A : NN0 --> CC ) /\ ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } ) /\ ( k e. NN0 /\ ( A ` k ) =/= 0 ) ) -> k < ( N + 1 ) )
38 17 ad2antrr
 |-  ( ( ( ( N e. NN0 /\ A : NN0 --> CC ) /\ ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } ) /\ ( k e. NN0 /\ ( A ` k ) =/= 0 ) ) -> N e. ZZ )
39 zleltp1
 |-  ( ( k e. ZZ /\ N e. ZZ ) -> ( k <_ N <-> k < ( N + 1 ) ) )
40 21 38 39 syl2anc
 |-  ( ( ( ( N e. NN0 /\ A : NN0 --> CC ) /\ ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } ) /\ ( k e. NN0 /\ ( A ` k ) =/= 0 ) ) -> ( k <_ N <-> k < ( N + 1 ) ) )
41 37 40 mpbird
 |-  ( ( ( ( N e. NN0 /\ A : NN0 --> CC ) /\ ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } ) /\ ( k e. NN0 /\ ( A ` k ) =/= 0 ) ) -> k <_ N )
42 41 expr
 |-  ( ( ( ( N e. NN0 /\ A : NN0 --> CC ) /\ ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } ) /\ k e. NN0 ) -> ( ( A ` k ) =/= 0 -> k <_ N ) )
43 42 ralrimiva
 |-  ( ( ( N e. NN0 /\ A : NN0 --> CC ) /\ ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } ) -> A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) )
44 simpr
 |-  ( ( A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) /\ n e. ( ZZ>= ` ( N + 1 ) ) ) -> n e. ( ZZ>= ` ( N + 1 ) ) )
45 eluznn0
 |-  ( ( ( N + 1 ) e. NN0 /\ n e. ( ZZ>= ` ( N + 1 ) ) ) -> n e. NN0 )
46 5 44 45 syl2an
 |-  ( ( ( N e. NN0 /\ A : NN0 --> CC ) /\ ( A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) /\ n e. ( ZZ>= ` ( N + 1 ) ) ) ) -> n e. NN0 )
47 nn0re
 |-  ( N e. NN0 -> N e. RR )
48 47 adantr
 |-  ( ( N e. NN0 /\ A : NN0 --> CC ) -> N e. RR )
49 48 adantr
 |-  ( ( ( N e. NN0 /\ A : NN0 --> CC ) /\ ( A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) /\ n e. ( ZZ>= ` ( N + 1 ) ) ) ) -> N e. RR )
50 34 adantr
 |-  ( ( ( N e. NN0 /\ A : NN0 --> CC ) /\ ( A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) /\ n e. ( ZZ>= ` ( N + 1 ) ) ) ) -> ( N + 1 ) e. RR )
51 46 nn0red
 |-  ( ( ( N e. NN0 /\ A : NN0 --> CC ) /\ ( A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) /\ n e. ( ZZ>= ` ( N + 1 ) ) ) ) -> n e. RR )
52 49 ltp1d
 |-  ( ( ( N e. NN0 /\ A : NN0 --> CC ) /\ ( A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) /\ n e. ( ZZ>= ` ( N + 1 ) ) ) ) -> N < ( N + 1 ) )
53 eluzle
 |-  ( n e. ( ZZ>= ` ( N + 1 ) ) -> ( N + 1 ) <_ n )
54 53 ad2antll
 |-  ( ( ( N e. NN0 /\ A : NN0 --> CC ) /\ ( A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) /\ n e. ( ZZ>= ` ( N + 1 ) ) ) ) -> ( N + 1 ) <_ n )
55 49 50 51 52 54 ltletrd
 |-  ( ( ( N e. NN0 /\ A : NN0 --> CC ) /\ ( A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) /\ n e. ( ZZ>= ` ( N + 1 ) ) ) ) -> N < n )
56 49 51 ltnled
 |-  ( ( ( N e. NN0 /\ A : NN0 --> CC ) /\ ( A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) /\ n e. ( ZZ>= ` ( N + 1 ) ) ) ) -> ( N < n <-> -. n <_ N ) )
57 55 56 mpbid
 |-  ( ( ( N e. NN0 /\ A : NN0 --> CC ) /\ ( A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) /\ n e. ( ZZ>= ` ( N + 1 ) ) ) ) -> -. n <_ N )
58 fveq2
 |-  ( k = n -> ( A ` k ) = ( A ` n ) )
59 58 neeq1d
 |-  ( k = n -> ( ( A ` k ) =/= 0 <-> ( A ` n ) =/= 0 ) )
60 breq1
 |-  ( k = n -> ( k <_ N <-> n <_ N ) )
61 59 60 imbi12d
 |-  ( k = n -> ( ( ( A ` k ) =/= 0 -> k <_ N ) <-> ( ( A ` n ) =/= 0 -> n <_ N ) ) )
62 simprl
 |-  ( ( ( N e. NN0 /\ A : NN0 --> CC ) /\ ( A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) /\ n e. ( ZZ>= ` ( N + 1 ) ) ) ) -> A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) )
63 61 62 46 rspcdva
 |-  ( ( ( N e. NN0 /\ A : NN0 --> CC ) /\ ( A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) /\ n e. ( ZZ>= ` ( N + 1 ) ) ) ) -> ( ( A ` n ) =/= 0 -> n <_ N ) )
64 63 necon1bd
 |-  ( ( ( N e. NN0 /\ A : NN0 --> CC ) /\ ( A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) /\ n e. ( ZZ>= ` ( N + 1 ) ) ) ) -> ( -. n <_ N -> ( A ` n ) = 0 ) )
65 57 64 mpd
 |-  ( ( ( N e. NN0 /\ A : NN0 --> CC ) /\ ( A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) /\ n e. ( ZZ>= ` ( N + 1 ) ) ) ) -> ( A ` n ) = 0 )
66 ffn
 |-  ( A : NN0 --> CC -> A Fn NN0 )
67 66 ad2antlr
 |-  ( ( ( N e. NN0 /\ A : NN0 --> CC ) /\ ( A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) /\ n e. ( ZZ>= ` ( N + 1 ) ) ) ) -> A Fn NN0 )
68 fniniseg
 |-  ( A Fn NN0 -> ( n e. ( `' A " { 0 } ) <-> ( n e. NN0 /\ ( A ` n ) = 0 ) ) )
69 67 68 syl
 |-  ( ( ( N e. NN0 /\ A : NN0 --> CC ) /\ ( A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) /\ n e. ( ZZ>= ` ( N + 1 ) ) ) ) -> ( n e. ( `' A " { 0 } ) <-> ( n e. NN0 /\ ( A ` n ) = 0 ) ) )
70 46 65 69 mpbir2and
 |-  ( ( ( N e. NN0 /\ A : NN0 --> CC ) /\ ( A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) /\ n e. ( ZZ>= ` ( N + 1 ) ) ) ) -> n e. ( `' A " { 0 } ) )
71 70 expr
 |-  ( ( ( N e. NN0 /\ A : NN0 --> CC ) /\ A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) ) -> ( n e. ( ZZ>= ` ( N + 1 ) ) -> n e. ( `' A " { 0 } ) ) )
72 71 ssrdv
 |-  ( ( ( N e. NN0 /\ A : NN0 --> CC ) /\ A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) ) -> ( ZZ>= ` ( N + 1 ) ) C_ ( `' A " { 0 } ) )
73 funimass3
 |-  ( ( Fun A /\ ( ZZ>= ` ( N + 1 ) ) C_ dom A ) -> ( ( A " ( ZZ>= ` ( N + 1 ) ) ) C_ { 0 } <-> ( ZZ>= ` ( N + 1 ) ) C_ ( `' A " { 0 } ) ) )
74 3 12 73 syl2anc
 |-  ( ( N e. NN0 /\ A : NN0 --> CC ) -> ( ( A " ( ZZ>= ` ( N + 1 ) ) ) C_ { 0 } <-> ( ZZ>= ` ( N + 1 ) ) C_ ( `' A " { 0 } ) ) )
75 74 adantr
 |-  ( ( ( N e. NN0 /\ A : NN0 --> CC ) /\ A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) ) -> ( ( A " ( ZZ>= ` ( N + 1 ) ) ) C_ { 0 } <-> ( ZZ>= ` ( N + 1 ) ) C_ ( `' A " { 0 } ) ) )
76 72 75 mpbird
 |-  ( ( ( N e. NN0 /\ A : NN0 --> CC ) /\ A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) ) -> ( A " ( ZZ>= ` ( N + 1 ) ) ) C_ { 0 } )
77 48 ltp1d
 |-  ( ( N e. NN0 /\ A : NN0 --> CC ) -> N < ( N + 1 ) )
78 48 34 ltnled
 |-  ( ( N e. NN0 /\ A : NN0 --> CC ) -> ( N < ( N + 1 ) <-> -. ( N + 1 ) <_ N ) )
79 77 78 mpbid
 |-  ( ( N e. NN0 /\ A : NN0 --> CC ) -> -. ( N + 1 ) <_ N )
80 79 adantr
 |-  ( ( ( N e. NN0 /\ A : NN0 --> CC ) /\ A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) ) -> -. ( N + 1 ) <_ N )
81 fveq2
 |-  ( k = ( N + 1 ) -> ( A ` k ) = ( A ` ( N + 1 ) ) )
82 81 neeq1d
 |-  ( k = ( N + 1 ) -> ( ( A ` k ) =/= 0 <-> ( A ` ( N + 1 ) ) =/= 0 ) )
83 breq1
 |-  ( k = ( N + 1 ) -> ( k <_ N <-> ( N + 1 ) <_ N ) )
84 82 83 imbi12d
 |-  ( k = ( N + 1 ) -> ( ( ( A ` k ) =/= 0 -> k <_ N ) <-> ( ( A ` ( N + 1 ) ) =/= 0 -> ( N + 1 ) <_ N ) ) )
85 84 rspcva
 |-  ( ( ( N + 1 ) e. NN0 /\ A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) ) -> ( ( A ` ( N + 1 ) ) =/= 0 -> ( N + 1 ) <_ N ) )
86 5 85 sylan
 |-  ( ( ( N e. NN0 /\ A : NN0 --> CC ) /\ A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) ) -> ( ( A ` ( N + 1 ) ) =/= 0 -> ( N + 1 ) <_ N ) )
87 86 necon1bd
 |-  ( ( ( N e. NN0 /\ A : NN0 --> CC ) /\ A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) ) -> ( -. ( N + 1 ) <_ N -> ( A ` ( N + 1 ) ) = 0 ) )
88 80 87 mpd
 |-  ( ( ( N e. NN0 /\ A : NN0 --> CC ) /\ A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) ) -> ( A ` ( N + 1 ) ) = 0 )
89 uzid
 |-  ( ( N + 1 ) e. ZZ -> ( N + 1 ) e. ( ZZ>= ` ( N + 1 ) ) )
90 18 89 syl
 |-  ( ( N e. NN0 /\ A : NN0 --> CC ) -> ( N + 1 ) e. ( ZZ>= ` ( N + 1 ) ) )
91 funfvima2
 |-  ( ( Fun A /\ ( ZZ>= ` ( N + 1 ) ) C_ dom A ) -> ( ( N + 1 ) e. ( ZZ>= ` ( N + 1 ) ) -> ( A ` ( N + 1 ) ) e. ( A " ( ZZ>= ` ( N + 1 ) ) ) ) )
92 3 12 91 syl2anc
 |-  ( ( N e. NN0 /\ A : NN0 --> CC ) -> ( ( N + 1 ) e. ( ZZ>= ` ( N + 1 ) ) -> ( A ` ( N + 1 ) ) e. ( A " ( ZZ>= ` ( N + 1 ) ) ) ) )
93 90 92 mpd
 |-  ( ( N e. NN0 /\ A : NN0 --> CC ) -> ( A ` ( N + 1 ) ) e. ( A " ( ZZ>= ` ( N + 1 ) ) ) )
94 93 adantr
 |-  ( ( ( N e. NN0 /\ A : NN0 --> CC ) /\ A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) ) -> ( A ` ( N + 1 ) ) e. ( A " ( ZZ>= ` ( N + 1 ) ) ) )
95 88 94 eqeltrrd
 |-  ( ( ( N e. NN0 /\ A : NN0 --> CC ) /\ A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) ) -> 0 e. ( A " ( ZZ>= ` ( N + 1 ) ) ) )
96 95 snssd
 |-  ( ( ( N e. NN0 /\ A : NN0 --> CC ) /\ A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) ) -> { 0 } C_ ( A " ( ZZ>= ` ( N + 1 ) ) ) )
97 76 96 eqssd
 |-  ( ( ( N e. NN0 /\ A : NN0 --> CC ) /\ A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) ) -> ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )
98 43 97 impbida
 |-  ( ( N e. NN0 /\ A : NN0 --> CC ) -> ( ( A " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } <-> A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ N ) ) )