Step | Hyp | Ref
| Expression |
1 | | plyssc 23956 |
. . . . 5
⊢
(Poly‘𝑆)
⊆ (Poly‘ℂ) |
2 | 1 | sseli 3599 |
. . . 4
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹 ∈
(Poly‘ℂ)) |
3 | | elply2 23952 |
. . . . . 6
⊢ (𝐹 ∈ (Poly‘ℂ)
↔ (ℂ ⊆ ℂ ∧ ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((ℂ ∪ {0})
↑𝑚 ℕ0)((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))))) |
4 | 3 | simprbi 480 |
. . . . 5
⊢ (𝐹 ∈ (Poly‘ℂ)
→ ∃𝑛 ∈
ℕ0 ∃𝑎 ∈ ((ℂ ∪ {0})
↑𝑚 ℕ0)((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) |
5 | | rexcom 3099 |
. . . . 5
⊢
(∃𝑛 ∈
ℕ0 ∃𝑎 ∈ ((ℂ ∪ {0})
↑𝑚 ℕ0)((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ↔ ∃𝑎 ∈ ((ℂ ∪ {0})
↑𝑚 ℕ0)∃𝑛 ∈ ℕ0 ((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) |
6 | 4, 5 | sylib 208 |
. . . 4
⊢ (𝐹 ∈ (Poly‘ℂ)
→ ∃𝑎 ∈
((ℂ ∪ {0}) ↑𝑚
ℕ0)∃𝑛 ∈ ℕ0 ((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) |
7 | 2, 6 | syl 17 |
. . 3
⊢ (𝐹 ∈ (Poly‘𝑆) → ∃𝑎 ∈ ((ℂ ∪ {0})
↑𝑚 ℕ0)∃𝑛 ∈ ℕ0 ((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) |
8 | | 0cn 10032 |
. . . . . . 7
⊢ 0 ∈
ℂ |
9 | | snssi 4339 |
. . . . . . 7
⊢ (0 ∈
ℂ → {0} ⊆ ℂ) |
10 | 8, 9 | ax-mp 5 |
. . . . . 6
⊢ {0}
⊆ ℂ |
11 | | ssequn2 3786 |
. . . . . 6
⊢ ({0}
⊆ ℂ ↔ (ℂ ∪ {0}) = ℂ) |
12 | 10, 11 | mpbi 220 |
. . . . 5
⊢ (ℂ
∪ {0}) = ℂ |
13 | 12 | oveq1i 6660 |
. . . 4
⊢ ((ℂ
∪ {0}) ↑𝑚 ℕ0) = (ℂ
↑𝑚 ℕ0) |
14 | 13 | rexeqi 3143 |
. . 3
⊢
(∃𝑎 ∈
((ℂ ∪ {0}) ↑𝑚
ℕ0)∃𝑛 ∈ ℕ0 ((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ↔ ∃𝑎 ∈ (ℂ ↑𝑚
ℕ0)∃𝑛 ∈ ℕ0 ((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) |
15 | 7, 14 | sylib 208 |
. 2
⊢ (𝐹 ∈ (Poly‘𝑆) → ∃𝑎 ∈ (ℂ
↑𝑚 ℕ0)∃𝑛 ∈ ℕ0 ((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) |
16 | | reeanv 3107 |
. . . 4
⊢
(∃𝑛 ∈
ℕ0 ∃𝑚 ∈ ℕ0 (((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ((𝑏 “ (ℤ≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘))))) ↔ (∃𝑛 ∈ ℕ0 ((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ∃𝑚 ∈ ℕ0 ((𝑏 “
(ℤ≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘)))))) |
17 | | simp1l 1085 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑎 ∈ (ℂ ↑𝑚
ℕ0) ∧ 𝑏 ∈ (ℂ ↑𝑚
ℕ0))) ∧ (𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0)
∧ (((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ((𝑏 “ (ℤ≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘)))))) → 𝐹 ∈ (Poly‘𝑆)) |
18 | | simp1rl 1126 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑎 ∈ (ℂ ↑𝑚
ℕ0) ∧ 𝑏 ∈ (ℂ ↑𝑚
ℕ0))) ∧ (𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0)
∧ (((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ((𝑏 “ (ℤ≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘)))))) → 𝑎 ∈ (ℂ ↑𝑚
ℕ0)) |
19 | | simp1rr 1127 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑎 ∈ (ℂ ↑𝑚
ℕ0) ∧ 𝑏 ∈ (ℂ ↑𝑚
ℕ0))) ∧ (𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0)
∧ (((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ((𝑏 “ (ℤ≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘)))))) → 𝑏 ∈ (ℂ ↑𝑚
ℕ0)) |
20 | | simp2l 1087 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑎 ∈ (ℂ ↑𝑚
ℕ0) ∧ 𝑏 ∈ (ℂ ↑𝑚
ℕ0))) ∧ (𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0)
∧ (((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ((𝑏 “ (ℤ≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘)))))) → 𝑛 ∈ ℕ0) |
21 | | simp2r 1088 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑎 ∈ (ℂ ↑𝑚
ℕ0) ∧ 𝑏 ∈ (ℂ ↑𝑚
ℕ0))) ∧ (𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0)
∧ (((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ((𝑏 “ (ℤ≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘)))))) → 𝑚 ∈ ℕ0) |
22 | | simp3ll 1132 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑎 ∈ (ℂ ↑𝑚
ℕ0) ∧ 𝑏 ∈ (ℂ ↑𝑚
ℕ0))) ∧ (𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0)
∧ (((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ((𝑏 “ (ℤ≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘)))))) → (𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0}) |
23 | | simp3rl 1134 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑎 ∈ (ℂ ↑𝑚
ℕ0) ∧ 𝑏 ∈ (ℂ ↑𝑚
ℕ0))) ∧ (𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0)
∧ (((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ((𝑏 “ (ℤ≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘)))))) → (𝑏 “ (ℤ≥‘(𝑚 + 1))) = {0}) |
24 | | simp3lr 1133 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑎 ∈ (ℂ ↑𝑚
ℕ0) ∧ 𝑏 ∈ (ℂ ↑𝑚
ℕ0))) ∧ (𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0)
∧ (((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ((𝑏 “ (ℤ≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘)))))) → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) |
25 | | oveq1 6657 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑤 → (𝑧↑𝑘) = (𝑤↑𝑘)) |
26 | 25 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑤 → ((𝑎‘𝑘) · (𝑧↑𝑘)) = ((𝑎‘𝑘) · (𝑤↑𝑘))) |
27 | 26 | sumeq2sdv 14435 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑤 → Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑤↑𝑘))) |
28 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑗 → (𝑎‘𝑘) = (𝑎‘𝑗)) |
29 | | oveq2 6658 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑗 → (𝑤↑𝑘) = (𝑤↑𝑗)) |
30 | 28, 29 | oveq12d 6668 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑗 → ((𝑎‘𝑘) · (𝑤↑𝑘)) = ((𝑎‘𝑗) · (𝑤↑𝑗))) |
31 | 30 | cbvsumv 14426 |
. . . . . . . . . 10
⊢
Σ𝑘 ∈
(0...𝑛)((𝑎‘𝑘) · (𝑤↑𝑘)) = Σ𝑗 ∈ (0...𝑛)((𝑎‘𝑗) · (𝑤↑𝑗)) |
32 | 27, 31 | syl6eq 2672 |
. . . . . . . . 9
⊢ (𝑧 = 𝑤 → Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)) = Σ𝑗 ∈ (0...𝑛)((𝑎‘𝑗) · (𝑤↑𝑗))) |
33 | 32 | cbvmptv 4750 |
. . . . . . . 8
⊢ (𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) = (𝑤 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑛)((𝑎‘𝑗) · (𝑤↑𝑗))) |
34 | 24, 33 | syl6eq 2672 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑎 ∈ (ℂ ↑𝑚
ℕ0) ∧ 𝑏 ∈ (ℂ ↑𝑚
ℕ0))) ∧ (𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0)
∧ (((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ((𝑏 “ (ℤ≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘)))))) → 𝐹 = (𝑤 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑛)((𝑎‘𝑗) · (𝑤↑𝑗)))) |
35 | | simp3rr 1135 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑎 ∈ (ℂ ↑𝑚
ℕ0) ∧ 𝑏 ∈ (ℂ ↑𝑚
ℕ0))) ∧ (𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0)
∧ (((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ((𝑏 “ (ℤ≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘)))))) → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘)))) |
36 | 25 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑤 → ((𝑏‘𝑘) · (𝑧↑𝑘)) = ((𝑏‘𝑘) · (𝑤↑𝑘))) |
37 | 36 | sumeq2sdv 14435 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑤 → Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑤↑𝑘))) |
38 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑗 → (𝑏‘𝑘) = (𝑏‘𝑗)) |
39 | 38, 29 | oveq12d 6668 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑗 → ((𝑏‘𝑘) · (𝑤↑𝑘)) = ((𝑏‘𝑗) · (𝑤↑𝑗))) |
40 | 39 | cbvsumv 14426 |
. . . . . . . . . 10
⊢
Σ𝑘 ∈
(0...𝑚)((𝑏‘𝑘) · (𝑤↑𝑘)) = Σ𝑗 ∈ (0...𝑚)((𝑏‘𝑗) · (𝑤↑𝑗)) |
41 | 37, 40 | syl6eq 2672 |
. . . . . . . . 9
⊢ (𝑧 = 𝑤 → Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘)) = Σ𝑗 ∈ (0...𝑚)((𝑏‘𝑗) · (𝑤↑𝑗))) |
42 | 41 | cbvmptv 4750 |
. . . . . . . 8
⊢ (𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘))) = (𝑤 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑚)((𝑏‘𝑗) · (𝑤↑𝑗))) |
43 | 35, 42 | syl6eq 2672 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑎 ∈ (ℂ ↑𝑚
ℕ0) ∧ 𝑏 ∈ (ℂ ↑𝑚
ℕ0))) ∧ (𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0)
∧ (((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ((𝑏 “ (ℤ≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘)))))) → 𝐹 = (𝑤 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑚)((𝑏‘𝑗) · (𝑤↑𝑗)))) |
44 | 17, 18, 19, 20, 21, 22, 23, 34, 43 | coeeulem 23980 |
. . . . . 6
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑎 ∈ (ℂ ↑𝑚
ℕ0) ∧ 𝑏 ∈ (ℂ ↑𝑚
ℕ0))) ∧ (𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0)
∧ (((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ((𝑏 “ (ℤ≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘)))))) → 𝑎 = 𝑏) |
45 | 44 | 3expia 1267 |
. . . . 5
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑎 ∈ (ℂ ↑𝑚
ℕ0) ∧ 𝑏 ∈ (ℂ ↑𝑚
ℕ0))) ∧ (𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0))
→ ((((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ((𝑏 “ (ℤ≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘))))) → 𝑎 = 𝑏)) |
46 | 45 | rexlimdvva 3038 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝑎 ∈ (ℂ ↑𝑚
ℕ0) ∧ 𝑏 ∈ (ℂ ↑𝑚
ℕ0))) → (∃𝑛 ∈ ℕ0 ∃𝑚 ∈ ℕ0
(((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ((𝑏 “ (ℤ≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘))))) → 𝑎 = 𝑏)) |
47 | 16, 46 | syl5bir 233 |
. . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝑎 ∈ (ℂ ↑𝑚
ℕ0) ∧ 𝑏 ∈ (ℂ ↑𝑚
ℕ0))) → ((∃𝑛 ∈ ℕ0 ((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ∃𝑚 ∈ ℕ0 ((𝑏 “
(ℤ≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘))))) → 𝑎 = 𝑏)) |
48 | 47 | ralrimivva 2971 |
. 2
⊢ (𝐹 ∈ (Poly‘𝑆) → ∀𝑎 ∈ (ℂ
↑𝑚 ℕ0)∀𝑏 ∈ (ℂ ↑𝑚
ℕ0)((∃𝑛 ∈ ℕ0 ((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ∃𝑚 ∈ ℕ0 ((𝑏 “
(ℤ≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘))))) → 𝑎 = 𝑏)) |
49 | | imaeq1 5461 |
. . . . . . 7
⊢ (𝑎 = 𝑏 → (𝑎 “ (ℤ≥‘(𝑛 + 1))) = (𝑏 “ (ℤ≥‘(𝑛 + 1)))) |
50 | 49 | eqeq1d 2624 |
. . . . . 6
⊢ (𝑎 = 𝑏 → ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ↔ (𝑏 “
(ℤ≥‘(𝑛 + 1))) = {0})) |
51 | | fveq1 6190 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑏 → (𝑎‘𝑘) = (𝑏‘𝑘)) |
52 | 51 | oveq1d 6665 |
. . . . . . . . 9
⊢ (𝑎 = 𝑏 → ((𝑎‘𝑘) · (𝑧↑𝑘)) = ((𝑏‘𝑘) · (𝑧↑𝑘))) |
53 | 52 | sumeq2sdv 14435 |
. . . . . . . 8
⊢ (𝑎 = 𝑏 → Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘))) |
54 | 53 | mpteq2dv 4745 |
. . . . . . 7
⊢ (𝑎 = 𝑏 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘)))) |
55 | 54 | eqeq2d 2632 |
. . . . . 6
⊢ (𝑎 = 𝑏 → (𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) ↔ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘))))) |
56 | 50, 55 | anbi12d 747 |
. . . . 5
⊢ (𝑎 = 𝑏 → (((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ↔ ((𝑏 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘)))))) |
57 | 56 | rexbidv 3052 |
. . . 4
⊢ (𝑎 = 𝑏 → (∃𝑛 ∈ ℕ0 ((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ↔ ∃𝑛 ∈ ℕ0 ((𝑏 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘)))))) |
58 | | oveq1 6657 |
. . . . . . . . 9
⊢ (𝑛 = 𝑚 → (𝑛 + 1) = (𝑚 + 1)) |
59 | 58 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑛 = 𝑚 → (ℤ≥‘(𝑛 + 1)) =
(ℤ≥‘(𝑚 + 1))) |
60 | 59 | imaeq2d 5466 |
. . . . . . 7
⊢ (𝑛 = 𝑚 → (𝑏 “ (ℤ≥‘(𝑛 + 1))) = (𝑏 “ (ℤ≥‘(𝑚 + 1)))) |
61 | 60 | eqeq1d 2624 |
. . . . . 6
⊢ (𝑛 = 𝑚 → ((𝑏 “ (ℤ≥‘(𝑛 + 1))) = {0} ↔ (𝑏 “
(ℤ≥‘(𝑚 + 1))) = {0})) |
62 | | oveq2 6658 |
. . . . . . . . 9
⊢ (𝑛 = 𝑚 → (0...𝑛) = (0...𝑚)) |
63 | 62 | sumeq1d 14431 |
. . . . . . . 8
⊢ (𝑛 = 𝑚 → Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘))) |
64 | 63 | mpteq2dv 4745 |
. . . . . . 7
⊢ (𝑛 = 𝑚 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘)))) |
65 | 64 | eqeq2d 2632 |
. . . . . 6
⊢ (𝑛 = 𝑚 → (𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘))) ↔ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘))))) |
66 | 61, 65 | anbi12d 747 |
. . . . 5
⊢ (𝑛 = 𝑚 → (((𝑏 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘)))) ↔ ((𝑏 “ (ℤ≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘)))))) |
67 | 66 | cbvrexv 3172 |
. . . 4
⊢
(∃𝑛 ∈
ℕ0 ((𝑏
“ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘)))) ↔ ∃𝑚 ∈ ℕ0 ((𝑏 “
(ℤ≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘))))) |
68 | 57, 67 | syl6bb 276 |
. . 3
⊢ (𝑎 = 𝑏 → (∃𝑛 ∈ ℕ0 ((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ↔ ∃𝑚 ∈ ℕ0 ((𝑏 “
(ℤ≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘)))))) |
69 | 68 | reu4 3400 |
. 2
⊢
(∃!𝑎 ∈
(ℂ ↑𝑚 ℕ0)∃𝑛 ∈ ℕ0
((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ↔ (∃𝑎 ∈ (ℂ ↑𝑚
ℕ0)∃𝑛 ∈ ℕ0 ((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ∀𝑎 ∈ (ℂ ↑𝑚
ℕ0)∀𝑏 ∈ (ℂ ↑𝑚
ℕ0)((∃𝑛 ∈ ℕ0 ((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ∃𝑚 ∈ ℕ0 ((𝑏 “
(ℤ≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘))))) → 𝑎 = 𝑏))) |
70 | 15, 48, 69 | sylanbrc 698 |
1
⊢ (𝐹 ∈ (Poly‘𝑆) → ∃!𝑎 ∈ (ℂ
↑𝑚 ℕ0)∃𝑛 ∈ ℕ0 ((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) |