Step | Hyp | Ref
| Expression |
1 | | elply2 23756 |
. . . 4
⊢ (𝐹 ∈ (Poly‘𝑆) ↔ (𝑆 ⊆ ℂ ∧ ∃𝑛 ∈ ℕ0
∃𝑎 ∈ ((𝑆 ∪ {0})
↑𝑚 ℕ0)((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))))) |
2 | 1 | simprbi 479 |
. . 3
⊢ (𝐹 ∈ (Poly‘𝑆) → ∃𝑛 ∈ ℕ0
∃𝑎 ∈ ((𝑆 ∪ {0})
↑𝑚 ℕ0)((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) |
3 | | simplrr 797 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0)) |
4 | | simpll 786 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → 𝐹 ∈ (Poly‘𝑆)) |
5 | | plybss 23754 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝑆 ⊆ ℂ) |
6 | 4, 5 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → 𝑆 ⊆ ℂ) |
7 | | 0cnd 9912 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → 0 ∈
ℂ) |
8 | 7 | snssd 4281 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → {0} ⊆
ℂ) |
9 | 6, 8 | unssd 3751 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → (𝑆 ∪ {0}) ⊆
ℂ) |
10 | | cnex 9896 |
. . . . . . . . 9
⊢ ℂ
∈ V |
11 | | ssexg 4732 |
. . . . . . . . 9
⊢ (((𝑆 ∪ {0}) ⊆ ℂ
∧ ℂ ∈ V) → (𝑆 ∪ {0}) ∈ V) |
12 | 9, 10, 11 | sylancl 693 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → (𝑆 ∪ {0}) ∈ V) |
13 | | nn0ex 11175 |
. . . . . . . 8
⊢
ℕ0 ∈ V |
14 | | elmapg 7757 |
. . . . . . . 8
⊢ (((𝑆 ∪ {0}) ∈ V ∧
ℕ0 ∈ V) → (𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0) ↔ 𝑎:ℕ0⟶(𝑆 ∪ {0}))) |
15 | 12, 13, 14 | sylancl 693 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → (𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0) ↔ 𝑎:ℕ0⟶(𝑆 ∪ {0}))) |
16 | 3, 15 | mpbid 221 |
. . . . . 6
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → 𝑎:ℕ0⟶(𝑆 ∪ {0})) |
17 | | dgrval.1 |
. . . . . . . 8
⊢ 𝐴 = (coeff‘𝐹) |
18 | | simplrl 796 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → 𝑛 ∈ ℕ0) |
19 | 16, 9 | fssd 5970 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → 𝑎:ℕ0⟶ℂ) |
20 | | simprl 790 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → (𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0}) |
21 | | simprr 792 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) |
22 | 4, 18, 19, 20, 21 | coeeq 23787 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → (coeff‘𝐹) = 𝑎) |
23 | 17, 22 | syl5req 2657 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → 𝑎 = 𝐴) |
24 | 23 | feq1d 5943 |
. . . . . 6
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → (𝑎:ℕ0⟶(𝑆 ∪ {0}) ↔ 𝐴:ℕ0⟶(𝑆 ∪ {0}))) |
25 | 16, 24 | mpbid 221 |
. . . . 5
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → 𝐴:ℕ0⟶(𝑆 ∪ {0})) |
26 | 25 | ex 449 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) → (((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) → 𝐴:ℕ0⟶(𝑆 ∪ {0}))) |
27 | 26 | rexlimdvva 3020 |
. . 3
⊢ (𝐹 ∈ (Poly‘𝑆) → (∃𝑛 ∈ ℕ0
∃𝑎 ∈ ((𝑆 ∪ {0})
↑𝑚 ℕ0)((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) → 𝐴:ℕ0⟶(𝑆 ∪ {0}))) |
28 | 2, 27 | mpd 15 |
. 2
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐴:ℕ0⟶(𝑆 ∪ {0})) |
29 | | nn0ssz 11275 |
. . 3
⊢
ℕ0 ⊆ ℤ |
30 | | ffn 5958 |
. . . . . . . . . . . . . . 15
⊢ (𝑎:ℕ0⟶ℂ →
𝑎 Fn
ℕ0) |
31 | | elpreima 6245 |
. . . . . . . . . . . . . . 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 500 |
. . . . . . . . . . . . 13
⊢ ((((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) ∧ 𝑥 ∈ (◡𝑎 “ (ℂ ∖ {0}))) →
(𝑥 ∈
ℕ0 ∧ (𝑎‘𝑥) ∈ (ℂ ∖
{0}))) |
34 | 33 | simprd 478 |
. . . . . . . . . . . 12
⊢ ((((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) ∧ 𝑥 ∈ (◡𝑎 “ (ℂ ∖ {0}))) →
(𝑎‘𝑥) ∈ (ℂ ∖
{0})) |
35 | | eldifsni 4261 |
. . . . . . . . . . . 12
⊢ ((𝑎‘𝑥) ∈ (ℂ ∖ {0}) → (𝑎‘𝑥) ≠ 0) |
36 | 34, 35 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) ∧ 𝑥 ∈ (◡𝑎 “ (ℂ ∖ {0}))) →
(𝑎‘𝑥) ≠ 0) |
37 | 33 | simpld 474 |
. . . . . . . . . . . 12
⊢ ((((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) ∧ 𝑥 ∈ (◡𝑎 “ (ℂ ∖ {0}))) → 𝑥 ∈
ℕ0) |
38 | | plyco0 23752 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ ℕ0
∧ 𝑎:ℕ0⟶ℂ) →
((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ↔ ∀𝑥 ∈ ℕ0
((𝑎‘𝑥) ≠ 0 → 𝑥 ≤ 𝑛))) |
39 | 18, 19, 38 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ↔
∀𝑥 ∈
ℕ0 ((𝑎‘𝑥) ≠ 0 → 𝑥 ≤ 𝑛))) |
40 | 20, 39 | mpbid 221 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → ∀𝑥 ∈ ℕ0 ((𝑎‘𝑥) ≠ 0 → 𝑥 ≤ 𝑛)) |
41 | 40 | r19.21bi 2916 |
. . . . . . . . . . . 12
⊢ ((((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) ∧ 𝑥 ∈ ℕ0) → ((𝑎‘𝑥) ≠ 0 → 𝑥 ≤ 𝑛)) |
42 | 37, 41 | syldan 486 |
. . . . . . . . . . 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 2949 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → ∀𝑥 ∈ (◡𝑎 “ (ℂ ∖ {0}))𝑥 ≤ 𝑛) |
45 | 23 | cnveqd 5220 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → ◡𝑎 = ◡𝐴) |
46 | 45 | imaeq1d 5384 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → (◡𝑎 “ (ℂ ∖ {0})) = (◡𝐴 “ (ℂ ∖
{0}))) |
47 | 46 | raleqdv 3121 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → (∀𝑥 ∈ (◡𝑎 “ (ℂ ∖ {0}))𝑥 ≤ 𝑛 ↔ ∀𝑥 ∈ (◡𝐴 “ (ℂ ∖ {0}))𝑥 ≤ 𝑛)) |
48 | 44, 47 | mpbid 221 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) ∧ ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) → ∀𝑥 ∈ (◡𝐴 “ (ℂ ∖ {0}))𝑥 ≤ 𝑛) |
49 | 48 | ex 449 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝑛 ∈ ℕ0 ∧ 𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0))) → (((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) → ∀𝑥 ∈ (◡𝐴 “ (ℂ ∖ {0}))𝑥 ≤ 𝑛)) |
50 | 49 | expr 641 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑛 ∈ ℕ0) → (𝑎 ∈ ((𝑆 ∪ {0}) ↑𝑚
ℕ0) → (((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) → ∀𝑥 ∈ (◡𝐴 “ (ℂ ∖ {0}))𝑥 ≤ 𝑛))) |
51 | 50 | rexlimdv 3012 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑛 ∈ ℕ0) →
(∃𝑎 ∈ ((𝑆 ∪ {0})
↑𝑚 ℕ0)((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) → ∀𝑥 ∈ (◡𝐴 “ (ℂ ∖ {0}))𝑥 ≤ 𝑛)) |
52 | 51 | reximdva 3000 |
. . . 4
⊢ (𝐹 ∈ (Poly‘𝑆) → (∃𝑛 ∈ ℕ0
∃𝑎 ∈ ((𝑆 ∪ {0})
↑𝑚 ℕ0)((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) → ∃𝑛 ∈ ℕ0 ∀𝑥 ∈ (◡𝐴 “ (ℂ ∖ {0}))𝑥 ≤ 𝑛)) |
53 | 2, 52 | mpd 15 |
. . 3
⊢ (𝐹 ∈ (Poly‘𝑆) → ∃𝑛 ∈ ℕ0
∀𝑥 ∈ (◡𝐴 “ (ℂ ∖ {0}))𝑥 ≤ 𝑛) |
54 | | ssrexv 3630 |
. . 3
⊢
(ℕ0 ⊆ ℤ → (∃𝑛 ∈ ℕ0 ∀𝑥 ∈ (◡𝐴 “ (ℂ ∖ {0}))𝑥 ≤ 𝑛 → ∃𝑛 ∈ ℤ ∀𝑥 ∈ (◡𝐴 “ (ℂ ∖ {0}))𝑥 ≤ 𝑛)) |
55 | 29, 53, 54 | mpsyl 66 |
. 2
⊢ (𝐹 ∈ (Poly‘𝑆) → ∃𝑛 ∈ ℤ ∀𝑥 ∈ (◡𝐴 “ (ℂ ∖ {0}))𝑥 ≤ 𝑛) |
56 | 28, 55 | jca 553 |
1
⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐴:ℕ0⟶(𝑆 ∪ {0}) ∧ ∃𝑛 ∈ ℤ ∀𝑥 ∈ (◡𝐴 “ (ℂ ∖ {0}))𝑥 ≤ 𝑛)) |