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 syl6bb ⊢ ( ( ( ( 𝑁 ∈ ℕ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 → 𝑘 ≤ 𝑁 ) ) )