Step | Hyp | Ref
| Expression |
1 | | elply2 23952 |
. . . 4
⊢ (𝐹 ∈ (Poly‘𝑆) ↔ (𝑆 ⊆ ℂ ∧ ∃𝑛 ∈ ℕ0
∃𝑎 ∈ ((𝑆 ∪ {0})
↑𝑚 ℕ0)((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))))) |
2 | 1 | simprbi 480 |
. . 3
⊢ (𝐹 ∈ (Poly‘𝑆) → ∃𝑛 ∈ ℕ0
∃𝑎 ∈ ((𝑆 ∪ {0})
↑𝑚 ℕ0)((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) |
3 | | simplrr 801 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0)) |
4 | | simpll 790 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → 𝐹 ∈ (Poly‘𝑆)) |
5 | | plybss 23950 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝑆 ⊆ ℂ) |
6 | 4, 5 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → 𝑆 ⊆ ℂ) |
7 | | 0cnd 10033 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → 0 ∈
ℂ) |
8 | 7 | snssd 4340 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → {0} ⊆
ℂ) |
9 | 6, 8 | unssd 3789 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → (𝑆 ∪ {0}) ⊆
ℂ) |
10 | | cnex 10017 |
. . . . . . . . 9
⊢ ℂ
∈ V |
11 | | ssexg 4804 |
. . . . . . . . 9
⊢ (((𝑆 ∪ {0}) ⊆ ℂ
∧ ℂ ∈ V) → (𝑆 ∪ {0}) ∈ V) |
12 | 9, 10, 11 | sylancl 694 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → (𝑆 ∪ {0}) ∈ V) |
13 | | nn0ex 11298 |
. . . . . . . 8
⊢
ℕ0 ∈ V |
14 | | elmapg 7870 |
. . . . . . . 8
⊢ (((𝑆 ∪ {0}) ∈ V ∧
ℕ0 ∈ V) → (𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0) ↔ 𝑎:ℕ0⟶(𝑆 ∪ {0}))) |
15 | 12, 13, 14 | sylancl 694 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → (𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0) ↔ 𝑎:ℕ0⟶(𝑆 ∪ {0}))) |
16 | 3, 15 | mpbid 222 |
. . . . . 6
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → 𝑎:ℕ0⟶(𝑆 ∪ {0})) |
17 | | dgrval.1 |
. . . . . . . 8
⊢ 𝐴 = (coeff‘𝐹) |
18 | | simplrl 800 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → 𝑛 ∈ ℕ0) |
19 | 16, 9 | fssd 6057 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → 𝑎:ℕ0⟶ℂ) |
20 | | simprl 794 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → (𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0}) |
21 | | simprr 796 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) |
22 | 4, 18, 19, 20, 21 | coeeq 23983 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → (coeff‘𝐹) = 𝑎) |
23 | 17, 22 | syl5req 2669 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → 𝑎 = 𝐴) |
24 | 23 | feq1d 6030 |
. . . . . 6
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → (𝑎:ℕ0⟶(𝑆 ∪ {0}) ↔ 𝐴:ℕ0⟶(𝑆 ∪ {0}))) |
25 | 16, 24 | mpbid 222 |
. . . . 5
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → 𝐴:ℕ0⟶(𝑆 ∪ {0})) |
26 | 25 | ex 450 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) → (((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) → 𝐴:ℕ0⟶(𝑆 ∪ {0}))) |
27 | 26 | rexlimdvva 3038 |
. . 3
⊢ (𝐹 ∈ (Poly‘𝑆) → (∃𝑛 ∈ ℕ0
∃𝑎 ∈ ((𝑆 ∪ {0})
↑𝑚 ℕ0)((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) → 𝐴:ℕ0⟶(𝑆 ∪ {0}))) |
28 | 2, 27 | mpd 15 |
. 2
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐴:ℕ0⟶(𝑆 ∪ {0})) |
29 | | nn0ssz 11398 |
. . 3
⊢
ℕ0 ⊆ ℤ |
30 | | ffn 6045 |
. . . . . . . . . . . . . . 15
⊢ (𝑎:ℕ0⟶ℂ →
𝑎 Fn
ℕ0) |
31 | | elpreima 6337 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 Fn ℕ0 →
(𝑥 ∈ (◡𝑎 “ (ℂ ∖ {0})) ↔ (𝑥 ∈ ℕ0
∧ (𝑎‘𝑥) ∈ (ℂ ∖
{0})))) |
32 | 19, 30, 31 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → (𝑥 ∈ (◡𝑎 “ (ℂ ∖ {0})) ↔ (𝑥 ∈ ℕ0
∧ (𝑎‘𝑥) ∈ (ℂ ∖
{0})))) |
33 | 32 | biimpa 501 |
. . . . . . . . . . . . 13
⊢ ((((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) ∧ 𝑥 ∈ (◡𝑎 “ (ℂ ∖ {0}))) →
(𝑥 ∈
ℕ0 ∧ (𝑎‘𝑥) ∈ (ℂ ∖
{0}))) |
34 | 33 | simprd 479 |
. . . . . . . . . . . 12
⊢ ((((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) ∧ 𝑥 ∈ (◡𝑎 “ (ℂ ∖ {0}))) →
(𝑎‘𝑥) ∈ (ℂ ∖
{0})) |
35 | | eldifsni 4320 |
. . . . . . . . . . . 12
⊢ ((𝑎‘𝑥) ∈ (ℂ ∖ {0}) → (𝑎‘𝑥) ≠ 0) |
36 | 34, 35 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) ∧ 𝑥 ∈ (◡𝑎 “ (ℂ ∖ {0}))) →
(𝑎‘𝑥) ≠ 0) |
37 | 33 | simpld 475 |
. . . . . . . . . . . 12
⊢ ((((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) ∧ 𝑥 ∈ (◡𝑎 “ (ℂ ∖ {0}))) → 𝑥 ∈
ℕ0) |
38 | | plyco0 23948 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ ℕ0
∧ 𝑎:ℕ0⟶ℂ) →
((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ↔ ∀𝑥 ∈ ℕ0
((𝑎‘𝑥) ≠ 0 → 𝑥 ≤ 𝑛))) |
39 | 18, 19, 38 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ↔
∀𝑥 ∈
ℕ0 ((𝑎‘𝑥) ≠ 0 → 𝑥 ≤ 𝑛))) |
40 | 20, 39 | mpbid 222 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → ∀𝑥 ∈ ℕ0 ((𝑎‘𝑥) ≠ 0 → 𝑥 ≤ 𝑛)) |
41 | 40 | r19.21bi 2932 |
. . . . . . . . . . . 12
⊢ ((((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) ∧ 𝑥 ∈ ℕ0) → ((𝑎‘𝑥) ≠ 0 → 𝑥 ≤ 𝑛)) |
42 | 37, 41 | syldan 487 |
. . . . . . . . . . 11
⊢ ((((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) ∧ 𝑥 ∈ (◡𝑎 “ (ℂ ∖ {0}))) →
((𝑎‘𝑥) ≠ 0 → 𝑥 ≤ 𝑛)) |
43 | 36, 42 | mpd 15 |
. . . . . . . . . 10
⊢ ((((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) ∧ 𝑥 ∈ (◡𝑎 “ (ℂ ∖ {0}))) → 𝑥 ≤ 𝑛) |
44 | 43 | ralrimiva 2966 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → ∀𝑥 ∈ (◡𝑎 “ (ℂ ∖ {0}))𝑥 ≤ 𝑛) |
45 | 23 | cnveqd 5298 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → ◡𝑎 = ◡𝐴) |
46 | 45 | imaeq1d 5465 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → (◡𝑎 “ (ℂ ∖ {0})) = (◡𝐴 “ (ℂ ∖
{0}))) |
47 | 46 | raleqdv 3144 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → (∀𝑥 ∈ (◡𝑎 “ (ℂ ∖ {0}))𝑥 ≤ 𝑛 ↔ ∀𝑥 ∈ (◡𝐴 “ (ℂ ∖ {0}))𝑥 ≤ 𝑛)) |
48 | 44, 47 | mpbid 222 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → ∀𝑥 ∈ (◡𝐴 “ (ℂ ∖ {0}))𝑥 ≤ 𝑛) |
49 | 48 | ex 450 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) → (((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) → ∀𝑥 ∈ (◡𝐴 “ (ℂ ∖ {0}))𝑥 ≤ 𝑛)) |
50 | 49 | expr 643 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑛 ∈ ℕ0) → (𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0) → (((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) → ∀𝑥 ∈ (◡𝐴 “ (ℂ ∖ {0}))𝑥 ≤ 𝑛))) |
51 | 50 | rexlimdv 3030 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑛 ∈ ℕ0) →
(∃𝑎 ∈ ((𝑆 ∪ {0})
↑𝑚 ℕ0)((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) → ∀𝑥 ∈ (◡𝐴 “ (ℂ ∖ {0}))𝑥 ≤ 𝑛)) |
52 | 51 | reximdva 3017 |
. . . 4
⊢ (𝐹 ∈ (Poly‘𝑆) → (∃𝑛 ∈ ℕ0
∃𝑎 ∈ ((𝑆 ∪ {0})
↑𝑚 ℕ0)((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) → ∃𝑛 ∈ ℕ0 ∀𝑥 ∈ (◡𝐴 “ (ℂ ∖ {0}))𝑥 ≤ 𝑛)) |
53 | 2, 52 | mpd 15 |
. . 3
⊢ (𝐹 ∈ (Poly‘𝑆) → ∃𝑛 ∈ ℕ0
∀𝑥 ∈ (◡𝐴 “ (ℂ ∖ {0}))𝑥 ≤ 𝑛) |
54 | | ssrexv 3667 |
. . 3
⊢
(ℕ0 ⊆ ℤ → (∃𝑛 ∈ ℕ0 ∀𝑥 ∈ (◡𝐴 “ (ℂ ∖ {0}))𝑥 ≤ 𝑛 → ∃𝑛 ∈ ℤ ∀𝑥 ∈ (◡𝐴 “ (ℂ ∖ {0}))𝑥 ≤ 𝑛)) |
55 | 29, 53, 54 | mpsyl 68 |
. 2
⊢ (𝐹 ∈ (Poly‘𝑆) → ∃𝑛 ∈ ℤ ∀𝑥 ∈ (◡𝐴 “ (ℂ ∖ {0}))𝑥 ≤ 𝑛) |
56 | 28, 55 | jca 554 |
1
⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐴:ℕ0⟶(𝑆 ∪ {0}) ∧ ∃𝑛 ∈ ℤ ∀𝑥 ∈ (◡𝐴 “ (ℂ ∖ {0}))𝑥 ≤ 𝑛)) |