| Step | Hyp | Ref
| Expression |
| 1 | | plyssc 26239 |
. . . . 5
⊢
(Poly‘𝑆)
⊆ (Poly‘ℂ) |
| 2 | 1 | sseli 3979 |
. . . 4
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹 ∈
(Poly‘ℂ)) |
| 3 | | elply2 26235 |
. . . . . 6
⊢ (𝐹 ∈ (Poly‘ℂ)
↔ (ℂ ⊆ ℂ ∧ ∃𝑛 ∈ ℕ0 ∃𝑎 ∈ ((ℂ ∪ {0})
↑m ℕ0)((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))))) |
| 4 | 3 | simprbi 496 |
. . . . 5
⊢ (𝐹 ∈ (Poly‘ℂ)
→ ∃𝑛 ∈
ℕ0 ∃𝑎 ∈ ((ℂ ∪ {0})
↑m ℕ0)((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) |
| 5 | | rexcom 3290 |
. . . . 5
⊢
(∃𝑛 ∈
ℕ0 ∃𝑎 ∈ ((ℂ ∪ {0})
↑m ℕ0)((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ↔ ∃𝑎 ∈ ((ℂ ∪ {0})
↑m ℕ0)∃𝑛 ∈ ℕ0 ((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) |
| 6 | 4, 5 | sylib 218 |
. . . 4
⊢ (𝐹 ∈ (Poly‘ℂ)
→ ∃𝑎 ∈
((ℂ ∪ {0}) ↑m ℕ0)∃𝑛 ∈ ℕ0
((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) |
| 7 | 2, 6 | syl 17 |
. . 3
⊢ (𝐹 ∈ (Poly‘𝑆) → ∃𝑎 ∈ ((ℂ ∪ {0})
↑m ℕ0)∃𝑛 ∈ ℕ0 ((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) |
| 8 | | 0cn 11253 |
. . . . . . 7
⊢ 0 ∈
ℂ |
| 9 | | snssi 4808 |
. . . . . . 7
⊢ (0 ∈
ℂ → {0} ⊆ ℂ) |
| 10 | 8, 9 | ax-mp 5 |
. . . . . 6
⊢ {0}
⊆ ℂ |
| 11 | | ssequn2 4189 |
. . . . . 6
⊢ ({0}
⊆ ℂ ↔ (ℂ ∪ {0}) = ℂ) |
| 12 | 10, 11 | mpbi 230 |
. . . . 5
⊢ (ℂ
∪ {0}) = ℂ |
| 13 | 12 | oveq1i 7441 |
. . . 4
⊢ ((ℂ
∪ {0}) ↑m ℕ0) = (ℂ
↑m ℕ0) |
| 14 | 13 | rexeqi 3325 |
. . 3
⊢
(∃𝑎 ∈
((ℂ ∪ {0}) ↑m ℕ0)∃𝑛 ∈ ℕ0
((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ↔ ∃𝑎 ∈ (ℂ ↑m
ℕ0)∃𝑛 ∈ ℕ0 ((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) |
| 15 | 7, 14 | sylib 218 |
. 2
⊢ (𝐹 ∈ (Poly‘𝑆) → ∃𝑎 ∈ (ℂ
↑m ℕ0)∃𝑛 ∈ ℕ0 ((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) |
| 16 | | reeanv 3229 |
. . . 4
⊢
(∃𝑛 ∈
ℕ0 ∃𝑚 ∈ ℕ0 (((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ((𝑏 “ (ℤ≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘))))) ↔ (∃𝑛 ∈ ℕ0 ((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ∃𝑚 ∈ ℕ0 ((𝑏 “
(ℤ≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘)))))) |
| 17 | | simp1l 1198 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑎 ∈ (ℂ ↑m
ℕ0) ∧ 𝑏 ∈ (ℂ ↑m
ℕ0))) ∧ (𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0)
∧ (((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ((𝑏 “ (ℤ≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘)))))) → 𝐹 ∈ (Poly‘𝑆)) |
| 18 | | simp1rl 1239 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑎 ∈ (ℂ ↑m
ℕ0) ∧ 𝑏 ∈ (ℂ ↑m
ℕ0))) ∧ (𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0)
∧ (((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ((𝑏 “ (ℤ≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘)))))) → 𝑎 ∈ (ℂ ↑m
ℕ0)) |
| 19 | | simp1rr 1240 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑎 ∈ (ℂ ↑m
ℕ0) ∧ 𝑏 ∈ (ℂ ↑m
ℕ0))) ∧ (𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0)
∧ (((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ((𝑏 “ (ℤ≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘)))))) → 𝑏 ∈ (ℂ ↑m
ℕ0)) |
| 20 | | simp2l 1200 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑎 ∈ (ℂ ↑m
ℕ0) ∧ 𝑏 ∈ (ℂ ↑m
ℕ0))) ∧ (𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0)
∧ (((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ((𝑏 “ (ℤ≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘)))))) → 𝑛 ∈ ℕ0) |
| 21 | | simp2r 1201 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑎 ∈ (ℂ ↑m
ℕ0) ∧ 𝑏 ∈ (ℂ ↑m
ℕ0))) ∧ (𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0)
∧ (((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ((𝑏 “ (ℤ≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘)))))) → 𝑚 ∈ ℕ0) |
| 22 | | simp3ll 1245 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑎 ∈ (ℂ ↑m
ℕ0) ∧ 𝑏 ∈ (ℂ ↑m
ℕ0))) ∧ (𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0)
∧ (((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ((𝑏 “ (ℤ≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘)))))) → (𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0}) |
| 23 | | simp3rl 1247 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑎 ∈ (ℂ ↑m
ℕ0) ∧ 𝑏 ∈ (ℂ ↑m
ℕ0))) ∧ (𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0)
∧ (((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ((𝑏 “ (ℤ≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘)))))) → (𝑏 “ (ℤ≥‘(𝑚 + 1))) = {0}) |
| 24 | | simp3lr 1246 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑎 ∈ (ℂ ↑m
ℕ0) ∧ 𝑏 ∈ (ℂ ↑m
ℕ0))) ∧ (𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0)
∧ (((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ((𝑏 “ (ℤ≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘)))))) → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) |
| 25 | | oveq1 7438 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑤 → (𝑧↑𝑘) = (𝑤↑𝑘)) |
| 26 | 25 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑤 → ((𝑎‘𝑘) · (𝑧↑𝑘)) = ((𝑎‘𝑘) · (𝑤↑𝑘))) |
| 27 | 26 | sumeq2sdv 15739 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑤 → Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑤↑𝑘))) |
| 28 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑗 → (𝑎‘𝑘) = (𝑎‘𝑗)) |
| 29 | | oveq2 7439 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑗 → (𝑤↑𝑘) = (𝑤↑𝑗)) |
| 30 | 28, 29 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑗 → ((𝑎‘𝑘) · (𝑤↑𝑘)) = ((𝑎‘𝑗) · (𝑤↑𝑗))) |
| 31 | 30 | cbvsumv 15732 |
. . . . . . . . . 10
⊢
Σ𝑘 ∈
(0...𝑛)((𝑎‘𝑘) · (𝑤↑𝑘)) = Σ𝑗 ∈ (0...𝑛)((𝑎‘𝑗) · (𝑤↑𝑗)) |
| 32 | 27, 31 | eqtrdi 2793 |
. . . . . . . . 9
⊢ (𝑧 = 𝑤 → Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)) = Σ𝑗 ∈ (0...𝑛)((𝑎‘𝑗) · (𝑤↑𝑗))) |
| 33 | 32 | cbvmptv 5255 |
. . . . . . . 8
⊢ (𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) = (𝑤 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑛)((𝑎‘𝑗) · (𝑤↑𝑗))) |
| 34 | 24, 33 | eqtrdi 2793 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑎 ∈ (ℂ ↑m
ℕ0) ∧ 𝑏 ∈ (ℂ ↑m
ℕ0))) ∧ (𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0)
∧ (((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ((𝑏 “ (ℤ≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘)))))) → 𝐹 = (𝑤 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑛)((𝑎‘𝑗) · (𝑤↑𝑗)))) |
| 35 | | simp3rr 1248 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑎 ∈ (ℂ ↑m
ℕ0) ∧ 𝑏 ∈ (ℂ ↑m
ℕ0))) ∧ (𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0)
∧ (((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ((𝑏 “ (ℤ≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘)))))) → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘)))) |
| 36 | 25 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑤 → ((𝑏‘𝑘) · (𝑧↑𝑘)) = ((𝑏‘𝑘) · (𝑤↑𝑘))) |
| 37 | 36 | sumeq2sdv 15739 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑤 → Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑤↑𝑘))) |
| 38 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑗 → (𝑏‘𝑘) = (𝑏‘𝑗)) |
| 39 | 38, 29 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑗 → ((𝑏‘𝑘) · (𝑤↑𝑘)) = ((𝑏‘𝑗) · (𝑤↑𝑗))) |
| 40 | 39 | cbvsumv 15732 |
. . . . . . . . . 10
⊢
Σ𝑘 ∈
(0...𝑚)((𝑏‘𝑘) · (𝑤↑𝑘)) = Σ𝑗 ∈ (0...𝑚)((𝑏‘𝑗) · (𝑤↑𝑗)) |
| 41 | 37, 40 | eqtrdi 2793 |
. . . . . . . . 9
⊢ (𝑧 = 𝑤 → Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘)) = Σ𝑗 ∈ (0...𝑚)((𝑏‘𝑗) · (𝑤↑𝑗))) |
| 42 | 41 | cbvmptv 5255 |
. . . . . . . 8
⊢ (𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘))) = (𝑤 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑚)((𝑏‘𝑗) · (𝑤↑𝑗))) |
| 43 | 35, 42 | eqtrdi 2793 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑎 ∈ (ℂ ↑m
ℕ0) ∧ 𝑏 ∈ (ℂ ↑m
ℕ0))) ∧ (𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0)
∧ (((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ((𝑏 “ (ℤ≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘)))))) → 𝐹 = (𝑤 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑚)((𝑏‘𝑗) · (𝑤↑𝑗)))) |
| 44 | 17, 18, 19, 20, 21, 22, 23, 34, 43 | coeeulem 26263 |
. . . . . 6
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑎 ∈ (ℂ ↑m
ℕ0) ∧ 𝑏 ∈ (ℂ ↑m
ℕ0))) ∧ (𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0)
∧ (((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ((𝑏 “ (ℤ≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘)))))) → 𝑎 = 𝑏) |
| 45 | 44 | 3expia 1122 |
. . . . 5
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (𝑎 ∈ (ℂ ↑m
ℕ0) ∧ 𝑏 ∈ (ℂ ↑m
ℕ0))) ∧ (𝑛 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0))
→ ((((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ((𝑏 “ (ℤ≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘))))) → 𝑎 = 𝑏)) |
| 46 | 45 | rexlimdvva 3213 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝑎 ∈ (ℂ ↑m
ℕ0) ∧ 𝑏 ∈ (ℂ ↑m
ℕ0))) → (∃𝑛 ∈ ℕ0 ∃𝑚 ∈ ℕ0
(((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ((𝑏 “ (ℤ≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘))))) → 𝑎 = 𝑏)) |
| 47 | 16, 46 | biimtrrid 243 |
. . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (𝑎 ∈ (ℂ ↑m
ℕ0) ∧ 𝑏 ∈ (ℂ ↑m
ℕ0))) → ((∃𝑛 ∈ ℕ0 ((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ∃𝑚 ∈ ℕ0 ((𝑏 “
(ℤ≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘))))) → 𝑎 = 𝑏)) |
| 48 | 47 | ralrimivva 3202 |
. 2
⊢ (𝐹 ∈ (Poly‘𝑆) → ∀𝑎 ∈ (ℂ
↑m ℕ0)∀𝑏 ∈ (ℂ ↑m
ℕ0)((∃𝑛 ∈ ℕ0 ((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ∃𝑚 ∈ ℕ0 ((𝑏 “
(ℤ≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘))))) → 𝑎 = 𝑏)) |
| 49 | | imaeq1 6073 |
. . . . . . 7
⊢ (𝑎 = 𝑏 → (𝑎 “ (ℤ≥‘(𝑛 + 1))) = (𝑏 “ (ℤ≥‘(𝑛 + 1)))) |
| 50 | 49 | eqeq1d 2739 |
. . . . . 6
⊢ (𝑎 = 𝑏 → ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ↔ (𝑏 “
(ℤ≥‘(𝑛 + 1))) = {0})) |
| 51 | | fveq1 6905 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑏 → (𝑎‘𝑘) = (𝑏‘𝑘)) |
| 52 | 51 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝑎 = 𝑏 → ((𝑎‘𝑘) · (𝑧↑𝑘)) = ((𝑏‘𝑘) · (𝑧↑𝑘))) |
| 53 | 52 | sumeq2sdv 15739 |
. . . . . . . 8
⊢ (𝑎 = 𝑏 → Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘))) |
| 54 | 53 | mpteq2dv 5244 |
. . . . . . 7
⊢ (𝑎 = 𝑏 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘)))) |
| 55 | 54 | eqeq2d 2748 |
. . . . . 6
⊢ (𝑎 = 𝑏 → (𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) ↔ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘))))) |
| 56 | 50, 55 | anbi12d 632 |
. . . . 5
⊢ (𝑎 = 𝑏 → (((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ↔ ((𝑏 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘)))))) |
| 57 | 56 | rexbidv 3179 |
. . . 4
⊢ (𝑎 = 𝑏 → (∃𝑛 ∈ ℕ0 ((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ↔ ∃𝑛 ∈ ℕ0 ((𝑏 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘)))))) |
| 58 | | fvoveq1 7454 |
. . . . . . . 8
⊢ (𝑛 = 𝑚 → (ℤ≥‘(𝑛 + 1)) =
(ℤ≥‘(𝑚 + 1))) |
| 59 | 58 | imaeq2d 6078 |
. . . . . . 7
⊢ (𝑛 = 𝑚 → (𝑏 “ (ℤ≥‘(𝑛 + 1))) = (𝑏 “ (ℤ≥‘(𝑚 + 1)))) |
| 60 | 59 | eqeq1d 2739 |
. . . . . 6
⊢ (𝑛 = 𝑚 → ((𝑏 “ (ℤ≥‘(𝑛 + 1))) = {0} ↔ (𝑏 “
(ℤ≥‘(𝑚 + 1))) = {0})) |
| 61 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑛 = 𝑚 → (0...𝑛) = (0...𝑚)) |
| 62 | 61 | sumeq1d 15736 |
. . . . . . . 8
⊢ (𝑛 = 𝑚 → Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘))) |
| 63 | 62 | mpteq2dv 5244 |
. . . . . . 7
⊢ (𝑛 = 𝑚 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘)))) |
| 64 | 63 | eqeq2d 2748 |
. . . . . 6
⊢ (𝑛 = 𝑚 → (𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘))) ↔ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘))))) |
| 65 | 60, 64 | anbi12d 632 |
. . . . 5
⊢ (𝑛 = 𝑚 → (((𝑏 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘)))) ↔ ((𝑏 “ (ℤ≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘)))))) |
| 66 | 65 | cbvrexvw 3238 |
. . . 4
⊢
(∃𝑛 ∈
ℕ0 ((𝑏
“ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑏‘𝑘) · (𝑧↑𝑘)))) ↔ ∃𝑚 ∈ ℕ0 ((𝑏 “
(ℤ≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘))))) |
| 67 | 57, 66 | bitrdi 287 |
. . 3
⊢ (𝑎 = 𝑏 → (∃𝑛 ∈ ℕ0 ((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ↔ ∃𝑚 ∈ ℕ0 ((𝑏 “
(ℤ≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘)))))) |
| 68 | 67 | reu4 3737 |
. 2
⊢
(∃!𝑎 ∈
(ℂ ↑m ℕ0)∃𝑛 ∈ ℕ0 ((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ↔ (∃𝑎 ∈ (ℂ ↑m
ℕ0)∃𝑛 ∈ ℕ0 ((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ∀𝑎 ∈ (ℂ ↑m
ℕ0)∀𝑏 ∈ (ℂ ↑m
ℕ0)((∃𝑛 ∈ ℕ0 ((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))) ∧ ∃𝑚 ∈ ℕ0 ((𝑏 “
(ℤ≥‘(𝑚 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑚)((𝑏‘𝑘) · (𝑧↑𝑘))))) → 𝑎 = 𝑏))) |
| 69 | 15, 48, 68 | sylanbrc 583 |
1
⊢ (𝐹 ∈ (Poly‘𝑆) → ∃!𝑎 ∈ (ℂ
↑m ℕ0)∃𝑛 ∈ ℕ0 ((𝑎 “
(ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))) |