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 ( ( 𝑁 ∈ ℕ0𝐴 : ℕ0 ⟶ ℂ ) → ( ( 𝐴 “ ( ℤ ‘ ( 𝑁 + 1 ) ) ) = { 0 } ↔ ∀ 𝑘 ∈ ℕ0 ( ( 𝐴𝑘 ) ≠ 0 → 𝑘𝑁 ) ) )

Proof

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