dvply1 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > dvply1		Structured version Visualization version GIF version

Theorem dvply1 26454

Description: Derivative of a polynomial, explicit sum version. (Contributed by Stefan O'Rear, 13-Nov-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)

**Hypotheses**
Ref	Expression
dvply1.f	⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))))
dvply1.g	⊢ (𝜑 → 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(𝑁 − 1))((𝐵‘𝑘) · (𝑧↑𝑘))))
dvply1.a	⊢ (𝜑 → 𝐴:ℕ₀⟶ℂ)
dvply1.b	⊢ 𝐵 = (𝑘 ∈ ℕ₀ ↦ ((𝑘 + 1) · (𝐴‘(𝑘 + 1))))
dvply1.n	⊢ (𝜑 → 𝑁 ∈ ℕ₀)

**Assertion**
Ref	Expression
dvply1	⊢ (𝜑 → (ℂ D 𝐹) = 𝐺)

Distinct variable groups: 𝜑,𝑧,𝑘 𝑧,𝐴,𝑘 𝑧,𝐵 𝑘,𝑁,𝑧 Allowed substitution hints: 𝐵(𝑘) 𝐹(𝑧, 𝑘) 𝐺(𝑧, 𝑘)

Proof of Theorem dvply1 Dummy variable 𝑗 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dvply1.f	. . 3 ⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))))
2	1	oveq2d 7426	. 2 ⊢ (𝜑 → (ℂ D 𝐹) = (ℂ D (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))))
3		eqid 2763	. . . . 5 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
4	3	cnfldtopon 24948	. . . 4 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
5	4	toponrestid 23087	. . 3 ⊢ (TopOpen‘ℂ_fld) = ((TopOpen‘ℂ_fld) ↾_t ℂ)
6		cnelprrecn 11197	. . . 4 ⊢ ℂ ∈ {ℝ, ℂ}
7	6	a1i 11	. . 3 ⊢ (𝜑 → ℂ ∈ {ℝ, ℂ})
8	3	cnfldtop 24949	. . . 4 ⊢ (TopOpen‘ℂ_fld) ∈ Top
9		unicntop 24951	. . . . 5 ⊢ ℂ = ∪ (TopOpen‘ℂ_fld)
10	9	topopn 23072	. . . 4 ⊢ ((TopOpen‘ℂ_fld) ∈ Top → ℂ ∈ (TopOpen‘ℂ_fld))
11	8, 10	mp1i 14	. . 3 ⊢ (𝜑 → ℂ ∈ (TopOpen‘ℂ_fld))
12		fzfid 14014	. . 3 ⊢ (𝜑 → (0...𝑁) ∈ Fin)
13		dvply1.a	. . . . . . 7 ⊢ (𝜑 → 𝐴:ℕ₀⟶ℂ)
14		elfznn0 13653	. . . . . . 7 ⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ₀)
15		ffvelcdm 7076	. . . . . . 7 ⊢ ((𝐴:ℕ₀⟶ℂ ∧ 𝑘 ∈ ℕ₀) → (𝐴‘𝑘) ∈ ℂ)
16	13, 14, 15	syl2an 607	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴‘𝑘) ∈ ℂ)
17	16	adantr 485	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑧 ∈ ℂ) → (𝐴‘𝑘) ∈ ℂ)
18		simpr 489	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑧 ∈ ℂ) → 𝑧 ∈ ℂ)
19	14	ad2antlr 739	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑧 ∈ ℂ) → 𝑘 ∈ ℕ₀)
20	18, 19	expcld 14187	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑧 ∈ ℂ) → (𝑧↑𝑘) ∈ ℂ)
21	17, 20	mulcld 11233	. . . 4 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑧 ∈ ℂ) → ((𝐴‘𝑘) · (𝑧↑𝑘)) ∈ ℂ)
22	21	3impa 1127	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) → ((𝐴‘𝑘) · (𝑧↑𝑘)) ∈ ℂ)
23	16	3adant3 1150	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) → (𝐴‘𝑘) ∈ ℂ)
24		0cnd 11203	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 = 0) → 0 ∈ ℂ)
25		simpl2 1211	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) ∧ ¬ 𝑘 = 0) → 𝑘 ∈ (0...𝑁))
26	25, 14	syl 18	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) ∧ ¬ 𝑘 = 0) → 𝑘 ∈ ℕ₀)
27	26	nn0cnd 12571	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) ∧ ¬ 𝑘 = 0) → 𝑘 ∈ ℂ)
28		simpl3 1212	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) ∧ ¬ 𝑘 = 0) → 𝑧 ∈ ℂ)
29		simpr 489	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) ∧ ¬ 𝑘 = 0) → ¬ 𝑘 = 0)
30		elnn0 12510	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ₀ ↔ (𝑘 ∈ ℕ ∨ 𝑘 = 0))
31	26, 30	sylib 221	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) ∧ ¬ 𝑘 = 0) → (𝑘 ∈ ℕ ∨ 𝑘 = 0))
32		orel2 903	. . . . . . . . 9 ⊢ (¬ 𝑘 = 0 → ((𝑘 ∈ ℕ ∨ 𝑘 = 0) → 𝑘 ∈ ℕ))
33	29, 31, 32	sylc 66	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) ∧ ¬ 𝑘 = 0) → 𝑘 ∈ ℕ)
34		nnm1nn0 12549	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → (𝑘 − 1) ∈ ℕ₀)
35	33, 34	syl 18	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) ∧ ¬ 𝑘 = 0) → (𝑘 − 1) ∈ ℕ₀)
36	28, 35	expcld 14187	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) ∧ ¬ 𝑘 = 0) → (𝑧↑(𝑘 − 1)) ∈ ℂ)
37	27, 36	mulcld 11233	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) ∧ ¬ 𝑘 = 0) → (𝑘 · (𝑧↑(𝑘 − 1))) ∈ ℂ)
38	24, 37	ifclda 4523	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) → if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1)))) ∈ ℂ)
39	23, 38	mulcld 11233	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) → ((𝐴‘𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1))))) ∈ ℂ)
40	6	a1i 11	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ℂ ∈ {ℝ, ℂ})
41		c0ex 11204	. . . . . 6 ⊢ 0 ∈ V
42		ovex 7443	. . . . . 6 ⊢ (𝑘 · (𝑧↑(𝑘 − 1))) ∈ V
43	41, 42	ifex 4538	. . . . 5 ⊢ if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1)))) ∈ V
44	43	a1i 11	. . . 4 ⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑧 ∈ ℂ) → if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1)))) ∈ V)
45	14	adantl 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ₀)
46		dvexp2 26122	. . . . 5 ⊢ (𝑘 ∈ ℕ₀ → (ℂ D (𝑧 ∈ ℂ ↦ (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1))))))
47	45, 46	syl 18	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (ℂ D (𝑧 ∈ ℂ ↦ (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1))))))
48	40, 20, 44, 47, 16	dvmptcmul 26132	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (ℂ D (𝑧 ∈ ℂ ↦ ((𝐴‘𝑘) · (𝑧↑𝑘)))) = (𝑧 ∈ ℂ ↦ ((𝐴‘𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1)))))))
49	5, 3, 7, 11, 12, 22, 39, 48	dvmptfsum 26143	. 2 ⊢ (𝜑 → (ℂ D (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1)))))))
50		elfznn 13586	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (1...𝑁) → 𝑘 ∈ ℕ)
51	50	nnne0d 12290	. . . . . . . . . 10 ⊢ (𝑘 ∈ (1...𝑁) → 𝑘 ≠ 0)
52	51	neneqd 2963	. . . . . . . . 9 ⊢ (𝑘 ∈ (1...𝑁) → ¬ 𝑘 = 0)
53	52	adantl 486	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → ¬ 𝑘 = 0)
54	53	iffalsed 4498	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1)))) = (𝑘 · (𝑧↑(𝑘 − 1))))
55	54	oveq2d 7426	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → ((𝐴‘𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1))))) = ((𝐴‘𝑘) · (𝑘 · (𝑧↑(𝑘 − 1)))))
56	55	sumeq2dv 15758	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (1...𝑁)((𝐴‘𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1))))) = Σ𝑘 ∈ (1...𝑁)((𝐴‘𝑘) · (𝑘 · (𝑧↑(𝑘 − 1)))))
57		1eluzge0 12908	. . . . . . 7 ⊢ 1 ∈ (ℤ_≥‘0)
58		fzss1 13596	. . . . . . 7 ⊢ (1 ∈ (ℤ_≥‘0) → (1...𝑁) ⊆ (0...𝑁))
59	57, 58	mp1i 14	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (1...𝑁) ⊆ (0...𝑁))
60	13	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 𝐴:ℕ₀⟶ℂ)
61	50	nnnn0d 12569	. . . . . . . 8 ⊢ (𝑘 ∈ (1...𝑁) → 𝑘 ∈ ℕ₀)
62	60, 61, 15	syl2an 607	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → (𝐴‘𝑘) ∈ ℂ)
63	51	adantl 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → 𝑘 ≠ 0)
64	63	neneqd 2963	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → ¬ 𝑘 = 0)
65	64	iffalsed 4498	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1)))) = (𝑘 · (𝑧↑(𝑘 − 1))))
66	61	adantl 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → 𝑘 ∈ ℕ₀)
67	66	nn0cnd 12571	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → 𝑘 ∈ ℂ)
68		simplr 780	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → 𝑧 ∈ ℂ)
69	50, 34	syl 18	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (1...𝑁) → (𝑘 − 1) ∈ ℕ₀)
70	69	adantl 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → (𝑘 − 1) ∈ ℕ₀)
71	68, 70	expcld 14187	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → (𝑧↑(𝑘 − 1)) ∈ ℂ)
72	67, 71	mulcld 11233	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → (𝑘 · (𝑧↑(𝑘 − 1))) ∈ ℂ)
73	65, 72	eqeltrd 2863	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1)))) ∈ ℂ)
74	62, 73	mulcld 11233	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → ((𝐴‘𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1))))) ∈ ℂ)
75		eldifn 4086	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ((0...𝑁) ∖ (1...𝑁)) → ¬ 𝑘 ∈ (1...𝑁))
76		0p1e1 12365	. . . . . . . . . . . . . 14 ⊢ (0 + 1) = 1
77	76	oveq1i 7420	. . . . . . . . . . . . 13 ⊢ ((0 + 1)...𝑁) = (1...𝑁)
78	77	eleq2i 2855	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ((0 + 1)...𝑁) ↔ 𝑘 ∈ (1...𝑁))
79	75, 78	sylnibr 332	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ((0...𝑁) ∖ (1...𝑁)) → ¬ 𝑘 ∈ ((0 + 1)...𝑁))
80	79	adantl 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...𝑁) ∖ (1...𝑁))) → ¬ 𝑘 ∈ ((0 + 1)...𝑁))
81		eldifi 4085	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ((0...𝑁) ∖ (1...𝑁)) → 𝑘 ∈ (0...𝑁))
82	81	adantl 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...𝑁) ∖ (1...𝑁))) → 𝑘 ∈ (0...𝑁))
83		dvply1.n	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
84		nn0uz 12904	. . . . . . . . . . . . . 14 ⊢ ℕ₀ = (ℤ_≥‘0)
85	83, 84	eleqtrdi 2873	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘0))
86	85	ad2antrr 738	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...𝑁) ∖ (1...𝑁))) → 𝑁 ∈ (ℤ_≥‘0))
87		elfzp12 13636	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘0) → (𝑘 ∈ (0...𝑁) ↔ (𝑘 = 0 ∨ 𝑘 ∈ ((0 + 1)...𝑁))))
88	86, 87	syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...𝑁) ∖ (1...𝑁))) → (𝑘 ∈ (0...𝑁) ↔ (𝑘 = 0 ∨ 𝑘 ∈ ((0 + 1)...𝑁))))
89	82, 88	mpbid 235	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...𝑁) ∖ (1...𝑁))) → (𝑘 = 0 ∨ 𝑘 ∈ ((0 + 1)...𝑁)))
90		orel2 903	. . . . . . . . . 10 ⊢ (¬ 𝑘 ∈ ((0 + 1)...𝑁) → ((𝑘 = 0 ∨ 𝑘 ∈ ((0 + 1)...𝑁)) → 𝑘 = 0))
91	80, 89, 90	sylc 66	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...𝑁) ∖ (1...𝑁))) → 𝑘 = 0)
92	91	iftrued 4495	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...𝑁) ∖ (1...𝑁))) → if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1)))) = 0)
93	92	oveq2d 7426	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...𝑁) ∖ (1...𝑁))) → ((𝐴‘𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1))))) = ((𝐴‘𝑘) · 0))
94	60, 14, 15	syl2an 607	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → (𝐴‘𝑘) ∈ ℂ)
95	94	mul01d 11413	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴‘𝑘) · 0) = 0)
96	81, 95	sylan2 604	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...𝑁) ∖ (1...𝑁))) → ((𝐴‘𝑘) · 0) = 0)
97	93, 96	eqtrd 2798	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...𝑁) ∖ (1...𝑁))) → ((𝐴‘𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1))))) = 0)
98		fzfid 14014	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (0...𝑁) ∈ Fin)
99	59, 74, 97, 98	fsumss 15781	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (1...𝑁)((𝐴‘𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1))))) = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1))))))
100		elfznn0 13653	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ (0...(𝑁 − 1)) → 𝑗 ∈ ℕ₀)
101	100	adantl 486	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 𝑗 ∈ ℕ₀)
102	101	nn0cnd 12571	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 𝑗 ∈ ℂ)
103		ax-1cn 11162	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℂ
104		pncan 11467	. . . . . . . . . . . . 13 ⊢ ((𝑗 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑗 + 1) − 1) = 𝑗)
105	102, 103, 104	sylancl 597	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((𝑗 + 1) − 1) = 𝑗)
106	105	oveq2d 7426	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝑧↑((𝑗 + 1) − 1)) = (𝑧↑𝑗))
107	106	oveq2d 7426	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((𝑗 + 1) · (𝑧↑((𝑗 + 1) − 1))) = ((𝑗 + 1) · (𝑧↑𝑗)))
108	107	oveq2d 7426	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((𝐴‘(𝑗 + 1)) · ((𝑗 + 1) · (𝑧↑((𝑗 + 1) − 1)))) = ((𝐴‘(𝑗 + 1)) · ((𝑗 + 1) · (𝑧↑𝑗))))
109	13	ad2antrr 738	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 𝐴:ℕ₀⟶ℂ)
110		peano2nn0 12548	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ ℕ₀ → (𝑗 + 1) ∈ ℕ₀)
111	100, 110	syl 18	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (0...(𝑁 − 1)) → (𝑗 + 1) ∈ ℕ₀)
112	111	adantl 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝑗 + 1) ∈ ℕ₀)
113	109, 112	ffvelcdmd 7080	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝐴‘(𝑗 + 1)) ∈ ℂ)
114	112	nn0cnd 12571	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝑗 + 1) ∈ ℂ)
115		simplr 780	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 𝑧 ∈ ℂ)
116	115, 101	expcld 14187	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝑧↑𝑗) ∈ ℂ)
117	113, 114, 116	mulassd 11236	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (((𝐴‘(𝑗 + 1)) · (𝑗 + 1)) · (𝑧↑𝑗)) = ((𝐴‘(𝑗 + 1)) · ((𝑗 + 1) · (𝑧↑𝑗))))
118	113, 114	mulcomd 11234	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((𝐴‘(𝑗 + 1)) · (𝑗 + 1)) = ((𝑗 + 1) · (𝐴‘(𝑗 + 1))))
119	118	oveq1d 7425	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (((𝐴‘(𝑗 + 1)) · (𝑗 + 1)) · (𝑧↑𝑗)) = (((𝑗 + 1) · (𝐴‘(𝑗 + 1))) · (𝑧↑𝑗)))
120	108, 117, 119	3eqtr2d 2804	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((𝐴‘(𝑗 + 1)) · ((𝑗 + 1) · (𝑧↑((𝑗 + 1) − 1)))) = (((𝑗 + 1) · (𝐴‘(𝑗 + 1))) · (𝑧↑𝑗)))
121	120	sumeq2dv 15758	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑗 ∈ (0...(𝑁 − 1))((𝐴‘(𝑗 + 1)) · ((𝑗 + 1) · (𝑧↑((𝑗 + 1) − 1)))) = Σ𝑗 ∈ (0...(𝑁 − 1))(((𝑗 + 1) · (𝐴‘(𝑗 + 1))) · (𝑧↑𝑗)))
122		1m1e0 12317	. . . . . . . . 9 ⊢ (1 − 1) = 0
123	122	oveq1i 7420	. . . . . . . 8 ⊢ ((1 − 1)...(𝑁 − 1)) = (0...(𝑁 − 1))
124	123	sumeq1i 15753	. . . . . . 7 ⊢ Σ𝑗 ∈ ((1 − 1)...(𝑁 − 1))((𝐴‘(𝑗 + 1)) · ((𝑗 + 1) · (𝑧↑((𝑗 + 1) − 1)))) = Σ𝑗 ∈ (0...(𝑁 − 1))((𝐴‘(𝑗 + 1)) · ((𝑗 + 1) · (𝑧↑((𝑗 + 1) − 1))))
125		oveq1 7417	. . . . . . . . . 10 ⊢ (𝑘 = 𝑗 → (𝑘 + 1) = (𝑗 + 1))
126		fvoveq1 7433	. . . . . . . . . 10 ⊢ (𝑘 = 𝑗 → (𝐴‘(𝑘 + 1)) = (𝐴‘(𝑗 + 1)))
127	125, 126	oveq12d 7428	. . . . . . . . 9 ⊢ (𝑘 = 𝑗 → ((𝑘 + 1) · (𝐴‘(𝑘 + 1))) = ((𝑗 + 1) · (𝐴‘(𝑗 + 1))))
128		oveq2 7418	. . . . . . . . 9 ⊢ (𝑘 = 𝑗 → (𝑧↑𝑘) = (𝑧↑𝑗))
129	127, 128	oveq12d 7428	. . . . . . . 8 ⊢ (𝑘 = 𝑗 → (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑧↑𝑘)) = (((𝑗 + 1) · (𝐴‘(𝑗 + 1))) · (𝑧↑𝑗)))
130	129	cbvsumv 15752	. . . . . . 7 ⊢ Σ𝑘 ∈ (0...(𝑁 − 1))(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑧↑𝑘)) = Σ𝑗 ∈ (0...(𝑁 − 1))(((𝑗 + 1) · (𝐴‘(𝑗 + 1))) · (𝑧↑𝑗))
131	121, 124, 130	3eqtr4g 2823	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑗 ∈ ((1 − 1)...(𝑁 − 1))((𝐴‘(𝑗 + 1)) · ((𝑗 + 1) · (𝑧↑((𝑗 + 1) − 1)))) = Σ𝑘 ∈ (0...(𝑁 − 1))(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑧↑𝑘)))
132		1zzd 12629	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 1 ∈ ℤ)
133	83	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 𝑁 ∈ ℕ₀)
134	133	nn0zd 12620	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 𝑁 ∈ ℤ)
135	62, 72	mulcld 11233	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → ((𝐴‘𝑘) · (𝑘 · (𝑧↑(𝑘 − 1)))) ∈ ℂ)
136		fveq2 6881	. . . . . . . 8 ⊢ (𝑘 = (𝑗 + 1) → (𝐴‘𝑘) = (𝐴‘(𝑗 + 1)))
137		id 23	. . . . . . . . 9 ⊢ (𝑘 = (𝑗 + 1) → 𝑘 = (𝑗 + 1))
138		oveq1 7417	. . . . . . . . . 10 ⊢ (𝑘 = (𝑗 + 1) → (𝑘 − 1) = ((𝑗 + 1) − 1))
139	138	oveq2d 7426	. . . . . . . . 9 ⊢ (𝑘 = (𝑗 + 1) → (𝑧↑(𝑘 − 1)) = (𝑧↑((𝑗 + 1) − 1)))
140	137, 139	oveq12d 7428	. . . . . . . 8 ⊢ (𝑘 = (𝑗 + 1) → (𝑘 · (𝑧↑(𝑘 − 1))) = ((𝑗 + 1) · (𝑧↑((𝑗 + 1) − 1))))
141	136, 140	oveq12d 7428	. . . . . . 7 ⊢ (𝑘 = (𝑗 + 1) → ((𝐴‘𝑘) · (𝑘 · (𝑧↑(𝑘 − 1)))) = ((𝐴‘(𝑗 + 1)) · ((𝑗 + 1) · (𝑧↑((𝑗 + 1) − 1)))))
142	132, 132, 134, 135, 141	fsumshftm 15837	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (1...𝑁)((𝐴‘𝑘) · (𝑘 · (𝑧↑(𝑘 − 1)))) = Σ𝑗 ∈ ((1 − 1)...(𝑁 − 1))((𝐴‘(𝑗 + 1)) · ((𝑗 + 1) · (𝑧↑((𝑗 + 1) − 1)))))
143		elfznn0 13653	. . . . . . . . . 10 ⊢ (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ ℕ₀)
144	143	adantl 486	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝑘 ∈ ℕ₀)
145		ovex 7443	. . . . . . . . 9 ⊢ ((𝑘 + 1) · (𝐴‘(𝑘 + 1))) ∈ V
146		dvply1.b	. . . . . . . . . 10 ⊢ 𝐵 = (𝑘 ∈ ℕ₀ ↦ ((𝑘 + 1) · (𝐴‘(𝑘 + 1))))
147	146	fvmpt2 7001	. . . . . . . . 9 ⊢ ((𝑘 ∈ ℕ₀ ∧ ((𝑘 + 1) · (𝐴‘(𝑘 + 1))) ∈ V) → (𝐵‘𝑘) = ((𝑘 + 1) · (𝐴‘(𝑘 + 1))))
148	144, 145, 147	sylancl 597	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝐵‘𝑘) = ((𝑘 + 1) · (𝐴‘(𝑘 + 1))))
149	148	oveq1d 7425	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝐵‘𝑘) · (𝑧↑𝑘)) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑧↑𝑘)))
150	149	sumeq2dv 15758	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...(𝑁 − 1))((𝐵‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...(𝑁 − 1))(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑧↑𝑘)))
151	131, 142, 150	3eqtr4d 2808	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (1...𝑁)((𝐴‘𝑘) · (𝑘 · (𝑧↑(𝑘 − 1)))) = Σ𝑘 ∈ (0...(𝑁 − 1))((𝐵‘𝑘) · (𝑧↑𝑘)))
152	56, 99, 151	3eqtr3d 2806	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1))))) = Σ𝑘 ∈ (0...(𝑁 − 1))((𝐵‘𝑘) · (𝑧↑𝑘)))
153	152	mpteq2dva 5204	. . 3 ⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1)))))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(𝑁 − 1))((𝐵‘𝑘) · (𝑧↑𝑘))))
154		dvply1.g	. . 3 ⊢ (𝜑 → 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(𝑁 − 1))((𝐵‘𝑘) · (𝑧↑𝑘))))
155	153, 154	eqtr4d 2801	. 2 ⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1)))))) = 𝐺)
156	2, 49, 155	3eqtrd 2802	1 ⊢ (𝜑 → (ℂ D 𝐹) = 𝐺)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∨ wo 860 ∧ w3a 1103 = wceq 1570 ∈ wcel 2143 ≠ wne 2958 Vcvv 3455 ∖ cdif 3902 ⊆ wss 3905 ifcif 4487 {cpr 4591 ↦ cmpt 5192 ⟶wf 6532 ‘cfv 6536 (class class class)co 7410 ℂcc 11102 ℝcr 11103 0cc0 11104 1c1 11105 + caddc 11107 · cmul 11109 − cmin 11445 ℕcn 12237 ℕ₀cn0 12508 ℤ_≥cuz 12866 ...cfz 13539 ↑cexp 14102 Σcsu 15742 TopOpenctopn 17478 ℂ_fldccnfld 21531 Topctop 23059 D cdv 26031

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-rep 5238 ax-sep 5257 ax-nul 5269 ax-pow 5336 ax-pr 5404 ax-un 7732 ax-inf2 9606 ax-cnex 11160 ax-resscn 11161 ax-1cn 11162 ax-icn 11163 ax-addcl 11164 ax-addrcl 11165 ax-mulcl 11166 ax-mulrcl 11167 ax-mulcom 11168 ax-addass 11169 ax-mulass 11170 ax-distr 11171 ax-i2m1 11172 ax-1ne0 11173 ax-1rid 11174 ax-rnegex 11175 ax-rrecex 11176 ax-cnre 11177 ax-pre-lttri 11178 ax-pre-lttrn 11179 ax-pre-ltadd 11180 ax-pre-mulgt0 11181 ax-pre-sup 11182 ax-addf 11183

This proof depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4488 df-pw 4564 df-sn 4590 df-pr 4592 df-tp 4594 df-op 4596 df-uni 4873 df-int 4913 df-iun 4958 df-iin 4959 df-br 5110 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5556 df-eprel 5561 df-po 5569 df-so 5570 df-fr 5614 df-se 5615 df-we 5616 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-isom 6545 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-of 7674 df-om 7859 df-1st 7982 df-2nd 7983 df-supp 8153 df-frecs 8274 df-wrecs 8305 df-recs 8354 df-rdg 8393 df-1o 8449 df-2o 8450 df-er 8690 df-map 8822 df-pm 8823 df-ixp 8892 df-en 8940 df-dom 8941 df-sdom 8942 df-fin 8943 df-fsupp 9318 df-fi 9367 df-sup 9398 df-inf 9399 df-oi 9468 df-card 9930 df-pnf 11249 df-mnf 11250 df-xr 11251 df-ltxr 11252 df-le 11253 df-sub 11447 df-neg 11448 df-div 11876 df-nn 12238 df-2 12307 df-3 12308 df-4 12309 df-5 12310 df-6 12311 df-7 12312 df-8 12313 df-9 12314 df-n0 12509 df-z 12596 df-dec 12716 df-uz 12867 df-q 12977 df-rp 13021 df-xneg 13141 df-xadd 13142 df-xmul 13143 df-icc 13383 df-fz 13540 df-fzo 13688 df-seq 14043 df-exp 14103 df-hash 14372 df-cj 15155 df-re 15156 df-im 15157 df-sqrt 15291 df-abs 15292 df-clim 15544 df-sum 15743 df-struct 17211 df-sets 17228 df-slot 17246 df-ndx 17258 df-base 17274 df-ress 17295 df-plusg 17327 df-mulr 17328 df-starv 17329 df-sca 17330 df-vsca 17331 df-ip 17332 df-tset 17333 df-ple 17334 df-ds 17336 df-unif 17337 df-hom 17338 df-cco 17339 df-rest 17479 df-topn 17480 df-0g 17498 df-gsum 17499 df-topgen 17500 df-pt 17501 df-prds 17504 df-xrs 17560 df-qtop 17565 df-imas 17566 df-xps 17568 df-mre 17642 df-mrc 17643 df-acs 17645 df-mgm 18702 df-sgrp 18781 df-mnd 18797 df-submnd 18846 df-mulg 19138 df-cntz 19391 df-cmn 19856 df-psmet 21523 df-xmet 21524 df-met 21525 df-bl 21526 df-mopn 21527 df-fbas 21528 df-fg 21529 df-cnfld 21532 df-top 23060 df-topon 23077 df-topsp 23099 df-bases 23112 df-cld 23185 df-ntr 23186 df-cls 23187 df-nei 23264 df-lp 23302 df-perf 23303 df-cn 23393 df-cnp 23394 df-haus 23481 df-tx 23728 df-hmeo 23921 df-fil 24012 df-fm 24104 df-flim 24105 df-flf 24106 df-xms 24486 df-ms 24487 df-tms 24488 df-cncf 25046 df-limc 26034 df-dv 26035

This theorem is used by: dvply2g 26455

W3C validator