MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  plyco0 Structured version   Visualization version   GIF version

Theorem plyco0 26219
Description: Two ways to say that a function on the nonnegative integers has finite support. (Contributed by Mario Carneiro, 22-Jul-2014.)
Assertion
Ref Expression
plyco0 ((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) → ((𝐴 “ (ℤ‘(𝑁 + 1))) = {0} ↔ ∀𝑘 ∈ ℕ0 ((𝐴𝑘) ≠ 0 → 𝑘𝑁)))
Distinct variable groups:   𝐴,𝑘   𝑘,𝑁

Proof of Theorem plyco0
Dummy variable 𝑛 is distinct from all other variables.
StepHypRef Expression
1 simprr 771 . . . . . . 7 ((((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) ∧ (𝐴 “ (ℤ‘(𝑁 + 1))) = {0}) ∧ (𝑘 ∈ ℕ0 ∧ (𝐴𝑘) ≠ 0)) → (𝐴𝑘) ≠ 0)
2 ffun 6731 . . . . . . . . . . . 12 (𝐴:ℕ0⟶ℂ → Fun 𝐴)
32adantl 480 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) → Fun 𝐴)
4 peano2nn0 12564 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ0)
54adantr 479 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) → (𝑁 + 1) ∈ ℕ0)
6 eluznn0 12953 . . . . . . . . . . . . . . 15 (((𝑁 + 1) ∈ ℕ0𝑘 ∈ (ℤ‘(𝑁 + 1))) → 𝑘 ∈ ℕ0)
76ex 411 . . . . . . . . . . . . . 14 ((𝑁 + 1) ∈ ℕ0 → (𝑘 ∈ (ℤ‘(𝑁 + 1)) → 𝑘 ∈ ℕ0))
85, 7syl 17 . . . . . . . . . . . . 13 ((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) → (𝑘 ∈ (ℤ‘(𝑁 + 1)) → 𝑘 ∈ ℕ0))
98ssrdv 3985 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) → (ℤ‘(𝑁 + 1)) ⊆ ℕ0)
10 fdm 6737 . . . . . . . . . . . . 13 (𝐴:ℕ0⟶ℂ → dom 𝐴 = ℕ0)
1110adantl 480 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) → dom 𝐴 = ℕ0)
129, 11sseqtrrd 4021 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) → (ℤ‘(𝑁 + 1)) ⊆ dom 𝐴)
13 funfvima2 7248 . . . . . . . . . . 11 ((Fun 𝐴 ∧ (ℤ‘(𝑁 + 1)) ⊆ dom 𝐴) → (𝑘 ∈ (ℤ‘(𝑁 + 1)) → (𝐴𝑘) ∈ (𝐴 “ (ℤ‘(𝑁 + 1)))))
143, 12, 13syl2anc 582 . . . . . . . . . 10 ((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) → (𝑘 ∈ (ℤ‘(𝑁 + 1)) → (𝐴𝑘) ∈ (𝐴 “ (ℤ‘(𝑁 + 1)))))
1514ad2antrr 724 . . . . . . . . 9 ((((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) ∧ (𝐴 “ (ℤ‘(𝑁 + 1))) = {0}) ∧ (𝑘 ∈ ℕ0 ∧ (𝐴𝑘) ≠ 0)) → (𝑘 ∈ (ℤ‘(𝑁 + 1)) → (𝐴𝑘) ∈ (𝐴 “ (ℤ‘(𝑁 + 1)))))
16 nn0z 12635 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ0𝑁 ∈ ℤ)
1716adantr 479 . . . . . . . . . . . 12 ((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) → 𝑁 ∈ ℤ)
1817peano2zd 12721 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) → (𝑁 + 1) ∈ ℤ)
1918ad2antrr 724 . . . . . . . . . 10 ((((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) ∧ (𝐴 “ (ℤ‘(𝑁 + 1))) = {0}) ∧ (𝑘 ∈ ℕ0 ∧ (𝐴𝑘) ≠ 0)) → (𝑁 + 1) ∈ ℤ)
20 nn0z 12635 . . . . . . . . . . 11 (𝑘 ∈ ℕ0𝑘 ∈ ℤ)
2120ad2antrl 726 . . . . . . . . . 10 ((((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) ∧ (𝐴 “ (ℤ‘(𝑁 + 1))) = {0}) ∧ (𝑘 ∈ ℕ0 ∧ (𝐴𝑘) ≠ 0)) → 𝑘 ∈ ℤ)
22 eluz 12888 . . . . . . . . . 10 (((𝑁 + 1) ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑘 ∈ (ℤ‘(𝑁 + 1)) ↔ (𝑁 + 1) ≤ 𝑘))
2319, 21, 22syl2anc 582 . . . . . . . . 9 ((((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) ∧ (𝐴 “ (ℤ‘(𝑁 + 1))) = {0}) ∧ (𝑘 ∈ ℕ0 ∧ (𝐴𝑘) ≠ 0)) → (𝑘 ∈ (ℤ‘(𝑁 + 1)) ↔ (𝑁 + 1) ≤ 𝑘))
24 simplr 767 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) ∧ (𝐴 “ (ℤ‘(𝑁 + 1))) = {0}) ∧ (𝑘 ∈ ℕ0 ∧ (𝐴𝑘) ≠ 0)) → (𝐴 “ (ℤ‘(𝑁 + 1))) = {0})
2524eleq2d 2812 . . . . . . . . . 10 ((((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) ∧ (𝐴 “ (ℤ‘(𝑁 + 1))) = {0}) ∧ (𝑘 ∈ ℕ0 ∧ (𝐴𝑘) ≠ 0)) → ((𝐴𝑘) ∈ (𝐴 “ (ℤ‘(𝑁 + 1))) ↔ (𝐴𝑘) ∈ {0}))
26 fvex 6914 . . . . . . . . . . 11 (𝐴𝑘) ∈ V
2726elsn 4648 . . . . . . . . . 10 ((𝐴𝑘) ∈ {0} ↔ (𝐴𝑘) = 0)
2825, 27bitrdi 286 . . . . . . . . 9 ((((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) ∧ (𝐴 “ (ℤ‘(𝑁 + 1))) = {0}) ∧ (𝑘 ∈ ℕ0 ∧ (𝐴𝑘) ≠ 0)) → ((𝐴𝑘) ∈ (𝐴 “ (ℤ‘(𝑁 + 1))) ↔ (𝐴𝑘) = 0))
2915, 23, 283imtr3d 292 . . . . . . . 8 ((((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) ∧ (𝐴 “ (ℤ‘(𝑁 + 1))) = {0}) ∧ (𝑘 ∈ ℕ0 ∧ (𝐴𝑘) ≠ 0)) → ((𝑁 + 1) ≤ 𝑘 → (𝐴𝑘) = 0))
3029necon3ad 2943 . . . . . . 7 ((((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) ∧ (𝐴 “ (ℤ‘(𝑁 + 1))) = {0}) ∧ (𝑘 ∈ ℕ0 ∧ (𝐴𝑘) ≠ 0)) → ((𝐴𝑘) ≠ 0 → ¬ (𝑁 + 1) ≤ 𝑘))
311, 30mpd 15 . . . . . 6 ((((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) ∧ (𝐴 “ (ℤ‘(𝑁 + 1))) = {0}) ∧ (𝑘 ∈ ℕ0 ∧ (𝐴𝑘) ≠ 0)) → ¬ (𝑁 + 1) ≤ 𝑘)
32 nn0re 12533 . . . . . . . 8 (𝑘 ∈ ℕ0𝑘 ∈ ℝ)
3332ad2antrl 726 . . . . . . 7 ((((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) ∧ (𝐴 “ (ℤ‘(𝑁 + 1))) = {0}) ∧ (𝑘 ∈ ℕ0 ∧ (𝐴𝑘) ≠ 0)) → 𝑘 ∈ ℝ)
3418zred 12718 . . . . . . . 8 ((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) → (𝑁 + 1) ∈ ℝ)
3534ad2antrr 724 . . . . . . 7 ((((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) ∧ (𝐴 “ (ℤ‘(𝑁 + 1))) = {0}) ∧ (𝑘 ∈ ℕ0 ∧ (𝐴𝑘) ≠ 0)) → (𝑁 + 1) ∈ ℝ)
3633, 35ltnled 11411 . . . . . 6 ((((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) ∧ (𝐴 “ (ℤ‘(𝑁 + 1))) = {0}) ∧ (𝑘 ∈ ℕ0 ∧ (𝐴𝑘) ≠ 0)) → (𝑘 < (𝑁 + 1) ↔ ¬ (𝑁 + 1) ≤ 𝑘))
3731, 36mpbird 256 . . . . 5 ((((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) ∧ (𝐴 “ (ℤ‘(𝑁 + 1))) = {0}) ∧ (𝑘 ∈ ℕ0 ∧ (𝐴𝑘) ≠ 0)) → 𝑘 < (𝑁 + 1))
3817ad2antrr 724 . . . . . 6 ((((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) ∧ (𝐴 “ (ℤ‘(𝑁 + 1))) = {0}) ∧ (𝑘 ∈ ℕ0 ∧ (𝐴𝑘) ≠ 0)) → 𝑁 ∈ ℤ)
39 zleltp1 12665 . . . . . 6 ((𝑘 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘𝑁𝑘 < (𝑁 + 1)))
4021, 38, 39syl2anc 582 . . . . 5 ((((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) ∧ (𝐴 “ (ℤ‘(𝑁 + 1))) = {0}) ∧ (𝑘 ∈ ℕ0 ∧ (𝐴𝑘) ≠ 0)) → (𝑘𝑁𝑘 < (𝑁 + 1)))
4137, 40mpbird 256 . . . 4 ((((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) ∧ (𝐴 “ (ℤ‘(𝑁 + 1))) = {0}) ∧ (𝑘 ∈ ℕ0 ∧ (𝐴𝑘) ≠ 0)) → 𝑘𝑁)
4241expr 455 . . 3 ((((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) ∧ (𝐴 “ (ℤ‘(𝑁 + 1))) = {0}) ∧ 𝑘 ∈ ℕ0) → ((𝐴𝑘) ≠ 0 → 𝑘𝑁))
4342ralrimiva 3136 . 2 (((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) ∧ (𝐴 “ (ℤ‘(𝑁 + 1))) = {0}) → ∀𝑘 ∈ ℕ0 ((𝐴𝑘) ≠ 0 → 𝑘𝑁))
44 simpr 483 . . . . . . . 8 ((∀𝑘 ∈ ℕ0 ((𝐴𝑘) ≠ 0 → 𝑘𝑁) ∧ 𝑛 ∈ (ℤ‘(𝑁 + 1))) → 𝑛 ∈ (ℤ‘(𝑁 + 1)))
45 eluznn0 12953 . . . . . . . 8 (((𝑁 + 1) ∈ ℕ0𝑛 ∈ (ℤ‘(𝑁 + 1))) → 𝑛 ∈ ℕ0)
465, 44, 45syl2an 594 . . . . . . 7 (((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) ∧ (∀𝑘 ∈ ℕ0 ((𝐴𝑘) ≠ 0 → 𝑘𝑁) ∧ 𝑛 ∈ (ℤ‘(𝑁 + 1)))) → 𝑛 ∈ ℕ0)
47 nn0re 12533 . . . . . . . . . . . 12 (𝑁 ∈ ℕ0𝑁 ∈ ℝ)
4847adantr 479 . . . . . . . . . . 11 ((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) → 𝑁 ∈ ℝ)
4948adantr 479 . . . . . . . . . 10 (((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) ∧ (∀𝑘 ∈ ℕ0 ((𝐴𝑘) ≠ 0 → 𝑘𝑁) ∧ 𝑛 ∈ (ℤ‘(𝑁 + 1)))) → 𝑁 ∈ ℝ)
5034adantr 479 . . . . . . . . . 10 (((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) ∧ (∀𝑘 ∈ ℕ0 ((𝐴𝑘) ≠ 0 → 𝑘𝑁) ∧ 𝑛 ∈ (ℤ‘(𝑁 + 1)))) → (𝑁 + 1) ∈ ℝ)
5146nn0red 12585 . . . . . . . . . 10 (((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) ∧ (∀𝑘 ∈ ℕ0 ((𝐴𝑘) ≠ 0 → 𝑘𝑁) ∧ 𝑛 ∈ (ℤ‘(𝑁 + 1)))) → 𝑛 ∈ ℝ)
5249ltp1d 12196 . . . . . . . . . 10 (((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) ∧ (∀𝑘 ∈ ℕ0 ((𝐴𝑘) ≠ 0 → 𝑘𝑁) ∧ 𝑛 ∈ (ℤ‘(𝑁 + 1)))) → 𝑁 < (𝑁 + 1))
53 eluzle 12887 . . . . . . . . . . 11 (𝑛 ∈ (ℤ‘(𝑁 + 1)) → (𝑁 + 1) ≤ 𝑛)
5453ad2antll 727 . . . . . . . . . 10 (((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) ∧ (∀𝑘 ∈ ℕ0 ((𝐴𝑘) ≠ 0 → 𝑘𝑁) ∧ 𝑛 ∈ (ℤ‘(𝑁 + 1)))) → (𝑁 + 1) ≤ 𝑛)
5549, 50, 51, 52, 54ltletrd 11424 . . . . . . . . 9 (((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) ∧ (∀𝑘 ∈ ℕ0 ((𝐴𝑘) ≠ 0 → 𝑘𝑁) ∧ 𝑛 ∈ (ℤ‘(𝑁 + 1)))) → 𝑁 < 𝑛)
5649, 51ltnled 11411 . . . . . . . . 9 (((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) ∧ (∀𝑘 ∈ ℕ0 ((𝐴𝑘) ≠ 0 → 𝑘𝑁) ∧ 𝑛 ∈ (ℤ‘(𝑁 + 1)))) → (𝑁 < 𝑛 ↔ ¬ 𝑛𝑁))
5755, 56mpbid 231 . . . . . . . 8 (((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) ∧ (∀𝑘 ∈ ℕ0 ((𝐴𝑘) ≠ 0 → 𝑘𝑁) ∧ 𝑛 ∈ (ℤ‘(𝑁 + 1)))) → ¬ 𝑛𝑁)
58 fveq2 6901 . . . . . . . . . . . 12 (𝑘 = 𝑛 → (𝐴𝑘) = (𝐴𝑛))
5958neeq1d 2990 . . . . . . . . . . 11 (𝑘 = 𝑛 → ((𝐴𝑘) ≠ 0 ↔ (𝐴𝑛) ≠ 0))
60 breq1 5156 . . . . . . . . . . 11 (𝑘 = 𝑛 → (𝑘𝑁𝑛𝑁))
6159, 60imbi12d 343 . . . . . . . . . 10 (𝑘 = 𝑛 → (((𝐴𝑘) ≠ 0 → 𝑘𝑁) ↔ ((𝐴𝑛) ≠ 0 → 𝑛𝑁)))
62 simprl 769 . . . . . . . . . 10 (((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) ∧ (∀𝑘 ∈ ℕ0 ((𝐴𝑘) ≠ 0 → 𝑘𝑁) ∧ 𝑛 ∈ (ℤ‘(𝑁 + 1)))) → ∀𝑘 ∈ ℕ0 ((𝐴𝑘) ≠ 0 → 𝑘𝑁))
6361, 62, 46rspcdva 3609 . . . . . . . . 9 (((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) ∧ (∀𝑘 ∈ ℕ0 ((𝐴𝑘) ≠ 0 → 𝑘𝑁) ∧ 𝑛 ∈ (ℤ‘(𝑁 + 1)))) → ((𝐴𝑛) ≠ 0 → 𝑛𝑁))
6463necon1bd 2948 . . . . . . . 8 (((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) ∧ (∀𝑘 ∈ ℕ0 ((𝐴𝑘) ≠ 0 → 𝑘𝑁) ∧ 𝑛 ∈ (ℤ‘(𝑁 + 1)))) → (¬ 𝑛𝑁 → (𝐴𝑛) = 0))
6557, 64mpd 15 . . . . . . 7 (((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) ∧ (∀𝑘 ∈ ℕ0 ((𝐴𝑘) ≠ 0 → 𝑘𝑁) ∧ 𝑛 ∈ (ℤ‘(𝑁 + 1)))) → (𝐴𝑛) = 0)
66 ffn 6728 . . . . . . . . 9 (𝐴:ℕ0⟶ℂ → 𝐴 Fn ℕ0)
6766ad2antlr 725 . . . . . . . 8 (((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) ∧ (∀𝑘 ∈ ℕ0 ((𝐴𝑘) ≠ 0 → 𝑘𝑁) ∧ 𝑛 ∈ (ℤ‘(𝑁 + 1)))) → 𝐴 Fn ℕ0)
68 fniniseg 7073 . . . . . . . 8 (𝐴 Fn ℕ0 → (𝑛 ∈ (𝐴 “ {0}) ↔ (𝑛 ∈ ℕ0 ∧ (𝐴𝑛) = 0)))
6967, 68syl 17 . . . . . . 7 (((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) ∧ (∀𝑘 ∈ ℕ0 ((𝐴𝑘) ≠ 0 → 𝑘𝑁) ∧ 𝑛 ∈ (ℤ‘(𝑁 + 1)))) → (𝑛 ∈ (𝐴 “ {0}) ↔ (𝑛 ∈ ℕ0 ∧ (𝐴𝑛) = 0)))
7046, 65, 69mpbir2and 711 . . . . . 6 (((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) ∧ (∀𝑘 ∈ ℕ0 ((𝐴𝑘) ≠ 0 → 𝑘𝑁) ∧ 𝑛 ∈ (ℤ‘(𝑁 + 1)))) → 𝑛 ∈ (𝐴 “ {0}))
7170expr 455 . . . . 5 (((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) ∧ ∀𝑘 ∈ ℕ0 ((𝐴𝑘) ≠ 0 → 𝑘𝑁)) → (𝑛 ∈ (ℤ‘(𝑁 + 1)) → 𝑛 ∈ (𝐴 “ {0})))
7271ssrdv 3985 . . . 4 (((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) ∧ ∀𝑘 ∈ ℕ0 ((𝐴𝑘) ≠ 0 → 𝑘𝑁)) → (ℤ‘(𝑁 + 1)) ⊆ (𝐴 “ {0}))
73 funimass3 7067 . . . . . 6 ((Fun 𝐴 ∧ (ℤ‘(𝑁 + 1)) ⊆ dom 𝐴) → ((𝐴 “ (ℤ‘(𝑁 + 1))) ⊆ {0} ↔ (ℤ‘(𝑁 + 1)) ⊆ (𝐴 “ {0})))
743, 12, 73syl2anc 582 . . . . 5 ((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) → ((𝐴 “ (ℤ‘(𝑁 + 1))) ⊆ {0} ↔ (ℤ‘(𝑁 + 1)) ⊆ (𝐴 “ {0})))
7574adantr 479 . . . 4 (((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) ∧ ∀𝑘 ∈ ℕ0 ((𝐴𝑘) ≠ 0 → 𝑘𝑁)) → ((𝐴 “ (ℤ‘(𝑁 + 1))) ⊆ {0} ↔ (ℤ‘(𝑁 + 1)) ⊆ (𝐴 “ {0})))
7672, 75mpbird 256 . . 3 (((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) ∧ ∀𝑘 ∈ ℕ0 ((𝐴𝑘) ≠ 0 → 𝑘𝑁)) → (𝐴 “ (ℤ‘(𝑁 + 1))) ⊆ {0})
7748ltp1d 12196 . . . . . . . 8 ((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) → 𝑁 < (𝑁 + 1))
7848, 34ltnled 11411 . . . . . . . 8 ((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) → (𝑁 < (𝑁 + 1) ↔ ¬ (𝑁 + 1) ≤ 𝑁))
7977, 78mpbid 231 . . . . . . 7 ((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) → ¬ (𝑁 + 1) ≤ 𝑁)
8079adantr 479 . . . . . 6 (((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) ∧ ∀𝑘 ∈ ℕ0 ((𝐴𝑘) ≠ 0 → 𝑘𝑁)) → ¬ (𝑁 + 1) ≤ 𝑁)
81 fveq2 6901 . . . . . . . . . . 11 (𝑘 = (𝑁 + 1) → (𝐴𝑘) = (𝐴‘(𝑁 + 1)))
8281neeq1d 2990 . . . . . . . . . 10 (𝑘 = (𝑁 + 1) → ((𝐴𝑘) ≠ 0 ↔ (𝐴‘(𝑁 + 1)) ≠ 0))
83 breq1 5156 . . . . . . . . . 10 (𝑘 = (𝑁 + 1) → (𝑘𝑁 ↔ (𝑁 + 1) ≤ 𝑁))
8482, 83imbi12d 343 . . . . . . . . 9 (𝑘 = (𝑁 + 1) → (((𝐴𝑘) ≠ 0 → 𝑘𝑁) ↔ ((𝐴‘(𝑁 + 1)) ≠ 0 → (𝑁 + 1) ≤ 𝑁)))
8584rspcva 3606 . . . . . . . 8 (((𝑁 + 1) ∈ ℕ0 ∧ ∀𝑘 ∈ ℕ0 ((𝐴𝑘) ≠ 0 → 𝑘𝑁)) → ((𝐴‘(𝑁 + 1)) ≠ 0 → (𝑁 + 1) ≤ 𝑁))
865, 85sylan 578 . . . . . . 7 (((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) ∧ ∀𝑘 ∈ ℕ0 ((𝐴𝑘) ≠ 0 → 𝑘𝑁)) → ((𝐴‘(𝑁 + 1)) ≠ 0 → (𝑁 + 1) ≤ 𝑁))
8786necon1bd 2948 . . . . . 6 (((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) ∧ ∀𝑘 ∈ ℕ0 ((𝐴𝑘) ≠ 0 → 𝑘𝑁)) → (¬ (𝑁 + 1) ≤ 𝑁 → (𝐴‘(𝑁 + 1)) = 0))
8880, 87mpd 15 . . . . 5 (((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) ∧ ∀𝑘 ∈ ℕ0 ((𝐴𝑘) ≠ 0 → 𝑘𝑁)) → (𝐴‘(𝑁 + 1)) = 0)
89 uzid 12889 . . . . . . . 8 ((𝑁 + 1) ∈ ℤ → (𝑁 + 1) ∈ (ℤ‘(𝑁 + 1)))
9018, 89syl 17 . . . . . . 7 ((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) → (𝑁 + 1) ∈ (ℤ‘(𝑁 + 1)))
91 funfvima2 7248 . . . . . . . 8 ((Fun 𝐴 ∧ (ℤ‘(𝑁 + 1)) ⊆ dom 𝐴) → ((𝑁 + 1) ∈ (ℤ‘(𝑁 + 1)) → (𝐴‘(𝑁 + 1)) ∈ (𝐴 “ (ℤ‘(𝑁 + 1)))))
923, 12, 91syl2anc 582 . . . . . . 7 ((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) → ((𝑁 + 1) ∈ (ℤ‘(𝑁 + 1)) → (𝐴‘(𝑁 + 1)) ∈ (𝐴 “ (ℤ‘(𝑁 + 1)))))
9390, 92mpd 15 . . . . . 6 ((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) → (𝐴‘(𝑁 + 1)) ∈ (𝐴 “ (ℤ‘(𝑁 + 1))))
9493adantr 479 . . . . 5 (((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) ∧ ∀𝑘 ∈ ℕ0 ((𝐴𝑘) ≠ 0 → 𝑘𝑁)) → (𝐴‘(𝑁 + 1)) ∈ (𝐴 “ (ℤ‘(𝑁 + 1))))
9588, 94eqeltrrd 2827 . . . 4 (((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) ∧ ∀𝑘 ∈ ℕ0 ((𝐴𝑘) ≠ 0 → 𝑘𝑁)) → 0 ∈ (𝐴 “ (ℤ‘(𝑁 + 1))))
9695snssd 4818 . . 3 (((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) ∧ ∀𝑘 ∈ ℕ0 ((𝐴𝑘) ≠ 0 → 𝑘𝑁)) → {0} ⊆ (𝐴 “ (ℤ‘(𝑁 + 1))))
9776, 96eqssd 3997 . 2 (((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) ∧ ∀𝑘 ∈ ℕ0 ((𝐴𝑘) ≠ 0 → 𝑘𝑁)) → (𝐴 “ (ℤ‘(𝑁 + 1))) = {0})
9843, 97impbida 799 1 ((𝑁 ∈ ℕ0𝐴:ℕ0⟶ℂ) → ((𝐴 “ (ℤ‘(𝑁 + 1))) = {0} ↔ ∀𝑘 ∈ ℕ0 ((𝐴𝑘) ≠ 0 → 𝑘𝑁)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394   = wceq 1534  wcel 2099  wne 2930  wral 3051  wss 3947  {csn 4633   class class class wbr 5153  ccnv 5681  dom cdm 5682  cima 5685  Fun wfun 6548   Fn wfn 6549  wf 6550  cfv 6554  (class class class)co 7424  cc 11156  cr 11157  0cc0 11158  1c1 11159   + caddc 11161   < clt 11298  cle 11299  0cn0 12524  cz 12610  cuz 12874
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-sep 5304  ax-nul 5311  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-cnex 11214  ax-resscn 11215  ax-1cn 11216  ax-icn 11217  ax-addcl 11218  ax-addrcl 11219  ax-mulcl 11220  ax-mulrcl 11221  ax-mulcom 11222  ax-addass 11223  ax-mulass 11224  ax-distr 11225  ax-i2m1 11226  ax-1ne0 11227  ax-1rid 11228  ax-rnegex 11229  ax-rrecex 11230  ax-cnre 11231  ax-pre-lttri 11232  ax-pre-lttrn 11233  ax-pre-ltadd 11234  ax-pre-mulgt0 11235
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3967  df-nul 4326  df-if 4534  df-pw 4609  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-iun 5003  df-br 5154  df-opab 5216  df-mpt 5237  df-tr 5271  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6312  df-ord 6379  df-on 6380  df-lim 6381  df-suc 6382  df-iota 6506  df-fun 6556  df-fn 6557  df-f 6558  df-f1 6559  df-fo 6560  df-f1o 6561  df-fv 6562  df-riota 7380  df-ov 7427  df-oprab 7428  df-mpo 7429  df-om 7877  df-2nd 8004  df-frecs 8296  df-wrecs 8327  df-recs 8401  df-rdg 8440  df-er 8734  df-en 8975  df-dom 8976  df-sdom 8977  df-pnf 11300  df-mnf 11301  df-xr 11302  df-ltxr 11303  df-le 11304  df-sub 11496  df-neg 11497  df-nn 12265  df-n0 12525  df-z 12611  df-uz 12875
This theorem is referenced by:  elply2  26223  plyeq0lem  26237  coeeulem  26251  dgrlem  26256  dgrub2  26262  dgrlb  26263  coeeq2  26269  dgrle  26270  coeaddlem  26276  coemullem  26277  coe1termlem  26285  dgreq0  26293  coecj  26306  basellem2  27110
  Copyright terms: Public domain W3C validator