This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem coelem

Description: Lemma for properties of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Assertion coelem ⊢ F ∈ Poly ⁡ S → coeff ⁡ F ∈ ℂ ℕ 0 ∧ ∃ n ∈ ℕ 0 coeff ⁡ F ℤ ≥ n + 1 = 0 ∧ F = z ∈ ℂ ⟼ ∑ k = 0 n coeff ⁡ F ⁡ k ⁢ z k

Proof

Step Hyp Ref Expression
1 coeval ⊢ F ∈ Poly ⁡ S → coeff ⁡ F = ι a ∈ ℂ ℕ 0 | ∃ n ∈ ℕ 0 a ℤ ≥ n + 1 = 0 ∧ F = z ∈ ℂ ⟼ ∑ k = 0 n a ⁡ k ⁢ z k
2 coeeu ⊢ F ∈ Poly ⁡ S → ∃! a ∈ ℂ ℕ 0 ∃ n ∈ ℕ 0 a ℤ ≥ n + 1 = 0 ∧ F = z ∈ ℂ ⟼ ∑ k = 0 n a ⁡ k ⁢ z k
3 riotacl2 ⊢ ∃! a ∈ ℂ ℕ 0 ∃ n ∈ ℕ 0 a ℤ ≥ n + 1 = 0 ∧ F = z ∈ ℂ ⟼ ∑ k = 0 n a ⁡ k ⁢ z k → ι a ∈ ℂ ℕ 0 | ∃ n ∈ ℕ 0 a ℤ ≥ n + 1 = 0 ∧ F = z ∈ ℂ ⟼ ∑ k = 0 n a ⁡ k ⁢ z k ∈ a ∈ ℂ ℕ 0 | ∃ n ∈ ℕ 0 a ℤ ≥ n + 1 = 0 ∧ F = z ∈ ℂ ⟼ ∑ k = 0 n a ⁡ k ⁢ z k
4 2 3 syl ⊢ F ∈ Poly ⁡ S → ι a ∈ ℂ ℕ 0 | ∃ n ∈ ℕ 0 a ℤ ≥ n + 1 = 0 ∧ F = z ∈ ℂ ⟼ ∑ k = 0 n a ⁡ k ⁢ z k ∈ a ∈ ℂ ℕ 0 | ∃ n ∈ ℕ 0 a ℤ ≥ n + 1 = 0 ∧ F = z ∈ ℂ ⟼ ∑ k = 0 n a ⁡ k ⁢ z k
5 1 4 eqeltrd ⊢ F ∈ Poly ⁡ S → coeff ⁡ F ∈ a ∈ ℂ ℕ 0 | ∃ n ∈ ℕ 0 a ℤ ≥ n + 1 = 0 ∧ F = z ∈ ℂ ⟼ ∑ k = 0 n a ⁡ k ⁢ z k
6 imaeq1 ⊢ a = coeff ⁡ F → a ℤ ≥ n + 1 = coeff ⁡ F ℤ ≥ n + 1
7 6 eqeq1d ⊢ a = coeff ⁡ F → a ℤ ≥ n + 1 = 0 ↔ coeff ⁡ F ℤ ≥ n + 1 = 0
8 fveq1 ⊢ a = coeff ⁡ F → a ⁡ k = coeff ⁡ F ⁡ k
9 8 oveq1d ⊢ a = coeff ⁡ F → a ⁡ k ⁢ z k = coeff ⁡ F ⁡ k ⁢ z k
10 9 sumeq2sdv ⊢ a = coeff ⁡ F → ∑ k = 0 n a ⁡ k ⁢ z k = ∑ k = 0 n coeff ⁡ F ⁡ k ⁢ z k
11 10 mpteq2dv ⊢ a = coeff ⁡ F → z ∈ ℂ ⟼ ∑ k = 0 n a ⁡ k ⁢ z k = z ∈ ℂ ⟼ ∑ k = 0 n coeff ⁡ F ⁡ k ⁢ z k
12 11 eqeq2d ⊢ a = coeff ⁡ F → F = z ∈ ℂ ⟼ ∑ k = 0 n a ⁡ k ⁢ z k ↔ F = z ∈ ℂ ⟼ ∑ k = 0 n coeff ⁡ F ⁡ k ⁢ z k
13 7 12 anbi12d ⊢ a = coeff ⁡ F → a ℤ ≥ n + 1 = 0 ∧ F = z ∈ ℂ ⟼ ∑ k = 0 n a ⁡ k ⁢ z k ↔ coeff ⁡ F ℤ ≥ n + 1 = 0 ∧ F = z ∈ ℂ ⟼ ∑ k = 0 n coeff ⁡ F ⁡ k ⁢ z k
14 13 rexbidv ⊢ a = coeff ⁡ F → ∃ n ∈ ℕ 0 a ℤ ≥ n + 1 = 0 ∧ F = z ∈ ℂ ⟼ ∑ k = 0 n a ⁡ k ⁢ z k ↔ ∃ n ∈ ℕ 0 coeff ⁡ F ℤ ≥ n + 1 = 0 ∧ F = z ∈ ℂ ⟼ ∑ k = 0 n coeff ⁡ F ⁡ k ⁢ z k
15 14 elrab ⊢ coeff ⁡ F ∈ a ∈ ℂ ℕ 0 | ∃ n ∈ ℕ 0 a ℤ ≥ n + 1 = 0 ∧ F = z ∈ ℂ ⟼ ∑ k = 0 n a ⁡ k ⁢ z k ↔ coeff ⁡ F ∈ ℂ ℕ 0 ∧ ∃ n ∈ ℕ 0 coeff ⁡ F ℤ ≥ n + 1 = 0 ∧ F = z ∈ ℂ ⟼ ∑ k = 0 n coeff ⁡ F ⁡ k ⁢ z k
16 5 15 sylib ⊢ F ∈ Poly ⁡ S → coeff ⁡ F ∈ ℂ ℕ 0 ∧ ∃ n ∈ ℕ 0 coeff ⁡ F ℤ ≥ n + 1 = 0 ∧ F = z ∈ ℂ ⟼ ∑ k = 0 n coeff ⁡ F ⁡ k ⁢ z k