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