pserdv2

Description: The derivative of a power series on its region of convergence. (Contributed by Mario Carneiro, 31-Mar-2015)

	Ref	Expression
Hypotheses	pserf.g	$⊢ G = (x \in ℂ ⟼ (n \in ℕ_{0} ⟼ A (n) x^{n}))$
	pserf.f	$⊢ F = (y \in S ⟼ \sum_{j \in ℕ_{0}} G (y) (j))$
	pserf.a	$⊢ φ \to A : ℕ_{0} ⟶ ℂ$
	pserf.r	$⊢ R = sup (\{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} ℝ^{*} <)$
	psercn.s	$⊢ S = {abs}^{-1} [[0, R)]$
	psercn.m	$⊢ M = if (R \in ℝ, \frac{\|a\| + R}{2}, \|a\| + 1)$
	pserdv.b	$⊢ B = 0 ball (abs \circ -) (\frac{\|a\| + M}{2})$
Assertion	pserdv2	$⊢ φ \to ℂ D F = (y \in S ⟼ \sum_{k \in ℕ} k A (k) y^{k - 1})$

Proof

Step	Hyp	Ref	Expression
1		pserf.g	$⊢ G = (x \in ℂ ⟼ (n \in ℕ_{0} ⟼ A (n) x^{n}))$
2		pserf.f	$⊢ F = (y \in S ⟼ \sum_{j \in ℕ_{0}} G (y) (j))$
3		pserf.a	$⊢ φ \to A : ℕ_{0} ⟶ ℂ$
4		pserf.r	$⊢ R = sup (\{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} ℝ^{*} <)$
5		psercn.s	$⊢ S = {abs}^{-1} [[0, R)]$
6		psercn.m	$⊢ M = if (R \in ℝ, \frac{\|a\| + R}{2}, \|a\| + 1)$
7		pserdv.b	$⊢ B = 0 ball (abs \circ -) (\frac{\|a\| + M}{2})$
8	1 2 3 4 5 6 7	pserdv	$⊢ φ \to ℂ D F = (y \in S ⟼ \sum_{m \in ℕ_{0}} (m + 1) A (m + 1) y^{m})$
9		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
10		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
11		1e0p1	$⊢ 1 = 0 + 1$
12	11	fveq2i	$⊢ ℤ_{\geq 1} = ℤ_{\geq (0 + 1)}$
13	10 12	eqtri	$⊢ ℕ = ℤ_{\geq (0 + 1)}$
14		id	$⊢ k = 1 + m \to k = 1 + m$
15		fveq2	$⊢ k = 1 + m \to A (k) = A (1 + m)$
16	14 15	oveq12d	$⊢ k = 1 + m \to k A (k) = (1 + m) A (1 + m)$
17		oveq1	$⊢ k = 1 + m \to k - 1 = 1 + m - 1$
18	17	oveq2d	$⊢ k = 1 + m \to y^{k - 1} = y^{1 + m - 1}$
19	16 18	oveq12d	$⊢ k = 1 + m \to k A (k) y^{k - 1} = (1 + m) A (1 + m) y^{1 + m - 1}$
20		1zzd	$⊢ (φ \land y \in S) \to 1 \in ℤ$
21		0zd	$⊢ (φ \land y \in S) \to 0 \in ℤ$
22		nncn	$⊢ k \in ℕ \to k \in ℂ$
23	22	adantl	$⊢ ((φ \land y \in S) \land k \in ℕ) \to k \in ℂ$
24	3	adantr	$⊢ (φ \land y \in S) \to A : ℕ_{0} ⟶ ℂ$
25		nnnn0	$⊢ k \in ℕ \to k \in ℕ_{0}$
26		ffvelrn	$⊢ (A : ℕ_{0} ⟶ ℂ \land k \in ℕ_{0}) \to A (k) \in ℂ$
27	24 25 26	syl2an	$⊢ ((φ \land y \in S) \land k \in ℕ) \to A (k) \in ℂ$
28	23 27	mulcld	$⊢ ((φ \land y \in S) \land k \in ℕ) \to k A (k) \in ℂ$
29		cnvimass	$⊢ {abs}^{-1} [[0, R)] \subseteq dom abs$
30		absf	$⊢ abs : ℂ ⟶ ℝ$
31	30	fdmi	$⊢ dom abs = ℂ$
32	29 31	sseqtri	$⊢ {abs}^{-1} [[0, R)] \subseteq ℂ$
33	5 32	eqsstri	$⊢ S \subseteq ℂ$
34	33	a1i	$⊢ φ \to S \subseteq ℂ$
35	34	sselda	$⊢ (φ \land y \in S) \to y \in ℂ$
36		nnm1nn0	$⊢ k \in ℕ \to k - 1 \in ℕ_{0}$
37		expcl	$⊢ (y \in ℂ \land k - 1 \in ℕ_{0}) \to y^{k - 1} \in ℂ$
38	35 36 37	syl2an	$⊢ ((φ \land y \in S) \land k \in ℕ) \to y^{k - 1} \in ℂ$
39	28 38	mulcld	$⊢ ((φ \land y \in S) \land k \in ℕ) \to k A (k) y^{k - 1} \in ℂ$
40	9 13 19 20 21 39	isumshft	$⊢ (φ \land y \in S) \to \sum_{k \in ℕ} k A (k) y^{k - 1} = \sum_{m \in ℕ_{0}} (1 + m) A (1 + m) y^{1 + m - 1}$
41		ax-1cn	$⊢ 1 \in ℂ$
42		nn0cn	$⊢ m \in ℕ_{0} \to m \in ℂ$
43	42	adantl	$⊢ ((φ \land y \in S) \land m \in ℕ_{0}) \to m \in ℂ$
44		addcom	$⊢ (1 \in ℂ \land m \in ℂ) \to 1 + m = m + 1$
45	41 43 44	sylancr	$⊢ ((φ \land y \in S) \land m \in ℕ_{0}) \to 1 + m = m + 1$
46	45	fveq2d	$⊢ ((φ \land y \in S) \land m \in ℕ_{0}) \to A (1 + m) = A (m + 1)$
47	45 46	oveq12d	$⊢ ((φ \land y \in S) \land m \in ℕ_{0}) \to (1 + m) A (1 + m) = (m + 1) A (m + 1)$
48		pncan2	$⊢ (1 \in ℂ \land m \in ℂ) \to 1 + m - 1 = m$
49	41 43 48	sylancr	$⊢ ((φ \land y \in S) \land m \in ℕ_{0}) \to 1 + m - 1 = m$
50	49	oveq2d	$⊢ ((φ \land y \in S) \land m \in ℕ_{0}) \to y^{1 + m - 1} = y^{m}$
51	47 50	oveq12d	$⊢ ((φ \land y \in S) \land m \in ℕ_{0}) \to (1 + m) A (1 + m) y^{1 + m - 1} = (m + 1) A (m + 1) y^{m}$
52	51	sumeq2dv	$⊢ (φ \land y \in S) \to \sum_{m \in ℕ_{0}} (1 + m) A (1 + m) y^{1 + m - 1} = \sum_{m \in ℕ_{0}} (m + 1) A (m + 1) y^{m}$
53	40 52	eqtr2d	$⊢ (φ \land y \in S) \to \sum_{m \in ℕ_{0}} (m + 1) A (m + 1) y^{m} = \sum_{k \in ℕ} k A (k) y^{k - 1}$
54	53	mpteq2dva	$⊢ φ \to (y \in S ⟼ \sum_{m \in ℕ_{0}} (m + 1) A (m + 1) y^{m}) = (y \in S ⟼ \sum_{k \in ℕ} k A (k) y^{k - 1})$
55	8 54	eqtrd	$⊢ φ \to ℂ D F = (y \in S ⟼ \sum_{k \in ℕ} k A (k) y^{k - 1})$

Metamath Proof Explorer

Theorem pserdv2

Proof