pserdv

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	pserdv	$⊢ φ \to ℂ D F = (y \in S ⟼ \sum_{k \in ℕ_{0}} (k + 1) A (k + 1) y^{k})$

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		dvfcn	$⊢ F_{ℂ}^{'} : dom F_{ℂ}^{'} ⟶ ℂ$
9		ssidd	$⊢ φ \to ℂ \subseteq ℂ$
10	1 2 3 4 5 6	psercn	$⊢ φ \to F : S \underset{cn}{⟶} ℂ$
11		cncff	$⊢ F : S \underset{cn}{⟶} ℂ \to F : S ⟶ ℂ$
12	10 11	syl	$⊢ φ \to F : S ⟶ ℂ$
13		cnvimass	$⊢ {abs}^{-1} [[0, R)] \subseteq dom abs$
14		absf	$⊢ abs : ℂ ⟶ ℝ$
15	14	fdmi	$⊢ dom abs = ℂ$
16	13 15	sseqtri	$⊢ {abs}^{-1} [[0, R)] \subseteq ℂ$
17	5 16	eqsstri	$⊢ S \subseteq ℂ$
18	17	a1i	$⊢ φ \to S \subseteq ℂ$
19	9 12 18	dvbss	$⊢ φ \to dom F_{ℂ}^{'} \subseteq S$
20		ssidd	$⊢ (φ \land a \in S) \to ℂ \subseteq ℂ$
21	12	adantr	$⊢ (φ \land a \in S) \to F : S ⟶ ℂ$
22	17	a1i	$⊢ (φ \land a \in S) \to S \subseteq ℂ$
23		cnxmet	$⊢ abs \circ - \in ∞Met (ℂ)$
24		0cnd	$⊢ (φ \land a \in S) \to 0 \in ℂ$
25	18	sselda	$⊢ (φ \land a \in S) \to a \in ℂ$
26	25	abscld	$⊢ (φ \land a \in S) \to \|a\| \in ℝ$
27	1 2 3 4 5 6	psercnlem1	$⊢ (φ \land a \in S) \to (M \in ℝ^{+} \land \|a\| < M \land M < R)$
28	27	simp1d	$⊢ (φ \land a \in S) \to M \in ℝ^{+}$
29	28	rpred	$⊢ (φ \land a \in S) \to M \in ℝ$
30	26 29	readdcld	$⊢ (φ \land a \in S) \to \|a\| + M \in ℝ$
31		0red	$⊢ (φ \land a \in S) \to 0 \in ℝ$
32	25	absge0d	$⊢ (φ \land a \in S) \to 0 \leq \|a\|$
33	26 28	ltaddrpd	$⊢ (φ \land a \in S) \to \|a\| < \|a\| + M$
34	31 26 30 32 33	lelttrd	$⊢ (φ \land a \in S) \to 0 < \|a\| + M$
35	30 34	elrpd	$⊢ (φ \land a \in S) \to \|a\| + M \in ℝ^{+}$
36	35	rphalfcld	$⊢ (φ \land a \in S) \to \frac{\|a\| + M}{2} \in ℝ^{+}$
37	36	rpxrd	$⊢ (φ \land a \in S) \to \frac{\|a\| + M}{2} \in ℝ^{*}$
38		blssm	$⊢ (abs \circ - \in ∞Met (ℂ) \land 0 \in ℂ \land \frac{\|a\| + M}{2} \in ℝ^{*}) \to 0 ball (abs \circ -) (\frac{\|a\| + M}{2}) \subseteq ℂ$
39	23 24 37 38	mp3an2i	$⊢ (φ \land a \in S) \to 0 ball (abs \circ -) (\frac{\|a\| + M}{2}) \subseteq ℂ$
40	7 39	eqsstrid	$⊢ (φ \land a \in S) \to B \subseteq ℂ$
41		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
42	41	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
43	42	toponrestid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ$
44	41 43	dvres	$⊢ ((ℂ \subseteq ℂ \land F : S ⟶ ℂ) \land (S \subseteq ℂ \land B \subseteq ℂ)) \to ℂ D ({F ↾}_{B}) = {F_{ℂ}^{'} ↾}_{int (TopOpen (ℂ_{fld})) (B)}$
45	20 21 22 40 44	syl22anc	$⊢ (φ \land a \in S) \to ℂ D ({F ↾}_{B}) = {F_{ℂ}^{'} ↾}_{int (TopOpen (ℂ_{fld})) (B)}$
46		resss	$⊢ {F_{ℂ}^{'} ↾}_{int (TopOpen (ℂ_{fld})) (B)} \subseteq ℂ D F$
47	45 46	eqsstrdi	$⊢ (φ \land a \in S) \to ℂ D ({F ↾}_{B}) \subseteq ℂ D F$
48		dmss	$⊢ ℂ D ({F ↾}_{B}) \subseteq ℂ D F \to dom {({F ↾}_{B})}_{ℂ}^{'} \subseteq dom F_{ℂ}^{'}$
49	47 48	syl	$⊢ (φ \land a \in S) \to dom {({F ↾}_{B})}_{ℂ}^{'} \subseteq dom F_{ℂ}^{'}$
50	1 2 3 4 5 6	pserdvlem1	$⊢ (φ \land a \in S) \to (\frac{\|a\| + M}{2} \in ℝ^{+} \land \|a\| < \frac{\|a\| + M}{2} \land \frac{\|a\| + M}{2} < R)$
51	1 2 3 4 5 50	psercnlem2	$⊢ (φ \land a \in S) \to (a \in (0 ball (abs \circ -) (\frac{\|a\| + M}{2})) \land 0 ball (abs \circ -) (\frac{\|a\| + M}{2}) \subseteq {abs}^{-1} [[0, \frac{\|a\| + M}{2}]] \land {abs}^{-1} [[0, \frac{\|a\| + M}{2}]] \subseteq S)$
52	51	simp1d	$⊢ (φ \land a \in S) \to a \in (0 ball (abs \circ -) (\frac{\|a\| + M}{2}))$
53	52 7	eleqtrrdi	$⊢ (φ \land a \in S) \to a \in B$
54	1 2 3 4 5 6 7	pserdvlem2	$⊢ (φ \land a \in S) \to ℂ D ({F ↾}_{B}) = (y \in B ⟼ \sum_{k \in ℕ_{0}} (k + 1) A (k + 1) y^{k})$
55	54	dmeqd	$⊢ (φ \land a \in S) \to dom {({F ↾}_{B})}_{ℂ}^{'} = dom (y \in B ⟼ \sum_{k \in ℕ_{0}} (k + 1) A (k + 1) y^{k})$
56		dmmptg	$⊢ \forall y \in B \sum_{k \in ℕ_{0}} (k + 1) A (k + 1) y^{k} \in V \to dom (y \in B ⟼ \sum_{k \in ℕ_{0}} (k + 1) A (k + 1) y^{k}) = B$
57		sumex	$⊢ \sum_{k \in ℕ_{0}} (k + 1) A (k + 1) y^{k} \in V$
58	57	a1i	$⊢ y \in B \to \sum_{k \in ℕ_{0}} (k + 1) A (k + 1) y^{k} \in V$
59	56 58	mprg	$⊢ dom (y \in B ⟼ \sum_{k \in ℕ_{0}} (k + 1) A (k + 1) y^{k}) = B$
60	55 59	eqtrdi	$⊢ (φ \land a \in S) \to dom {({F ↾}_{B})}_{ℂ}^{'} = B$
61	53 60	eleqtrrd	$⊢ (φ \land a \in S) \to a \in dom {({F ↾}_{B})}_{ℂ}^{'}$
62	49 61	sseldd	$⊢ (φ \land a \in S) \to a \in dom F_{ℂ}^{'}$
63	19 62	eqelssd	$⊢ φ \to dom F_{ℂ}^{'} = S$
64	63	feq2d	$⊢ φ \to (F_{ℂ}^{'} : dom F_{ℂ}^{'} ⟶ ℂ \leftrightarrow F_{ℂ}^{'} : S ⟶ ℂ)$
65	8 64	mpbii	$⊢ φ \to F_{ℂ}^{'} : S ⟶ ℂ$
66	65	feqmptd	$⊢ φ \to ℂ D F = (a \in S ⟼ F_{ℂ}^{'} (a))$
67		ffun	$⊢ F_{ℂ}^{'} : dom F_{ℂ}^{'} ⟶ ℂ \to Fun F_{ℂ}^{'}$
68	8 67	mp1i	$⊢ (φ \land a \in S) \to Fun F_{ℂ}^{'}$
69		funssfv	$⊢ (Fun F_{ℂ}^{'} \land ℂ D ({F ↾}_{B}) \subseteq ℂ D F \land a \in dom {({F ↾}_{B})}_{ℂ}^{'}) \to F_{ℂ}^{'} (a) = {({F ↾}_{B})}_{ℂ}^{'} (a)$
70	68 47 61 69	syl3anc	$⊢ (φ \land a \in S) \to F_{ℂ}^{'} (a) = {({F ↾}_{B})}_{ℂ}^{'} (a)$
71	54	fveq1d	$⊢ (φ \land a \in S) \to {({F ↾}_{B})}_{ℂ}^{'} (a) = (y \in B ⟼ \sum_{k \in ℕ_{0}} (k + 1) A (k + 1) y^{k}) (a)$
72		oveq1	$⊢ y = a \to y^{k} = a^{k}$
73	72	oveq2d	$⊢ y = a \to (k + 1) A (k + 1) y^{k} = (k + 1) A (k + 1) a^{k}$
74	73	sumeq2sdv	$⊢ y = a \to \sum_{k \in ℕ_{0}} (k + 1) A (k + 1) y^{k} = \sum_{k \in ℕ_{0}} (k + 1) A (k + 1) a^{k}$
75		eqid	$⊢ (y \in B ⟼ \sum_{k \in ℕ_{0}} (k + 1) A (k + 1) y^{k}) = (y \in B ⟼ \sum_{k \in ℕ_{0}} (k + 1) A (k + 1) y^{k})$
76		sumex	$⊢ \sum_{k \in ℕ_{0}} (k + 1) A (k + 1) a^{k} \in V$
77	74 75 76	fvmpt	$⊢ a \in B \to (y \in B ⟼ \sum_{k \in ℕ_{0}} (k + 1) A (k + 1) y^{k}) (a) = \sum_{k \in ℕ_{0}} (k + 1) A (k + 1) a^{k}$
78	53 77	syl	$⊢ (φ \land a \in S) \to (y \in B ⟼ \sum_{k \in ℕ_{0}} (k + 1) A (k + 1) y^{k}) (a) = \sum_{k \in ℕ_{0}} (k + 1) A (k + 1) a^{k}$
79	70 71 78	3eqtrd	$⊢ (φ \land a \in S) \to F_{ℂ}^{'} (a) = \sum_{k \in ℕ_{0}} (k + 1) A (k + 1) a^{k}$
80	79	mpteq2dva	$⊢ φ \to (a \in S ⟼ F_{ℂ}^{'} (a)) = (a \in S ⟼ \sum_{k \in ℕ_{0}} (k + 1) A (k + 1) a^{k})$
81	66 80	eqtrd	$⊢ φ \to ℂ D F = (a \in S ⟼ \sum_{k \in ℕ_{0}} (k + 1) A (k + 1) a^{k})$
82		oveq1	$⊢ a = y \to a^{k} = y^{k}$
83	82	oveq2d	$⊢ a = y \to (k + 1) A (k + 1) a^{k} = (k + 1) A (k + 1) y^{k}$
84	83	sumeq2sdv	$⊢ a = y \to \sum_{k \in ℕ_{0}} (k + 1) A (k + 1) a^{k} = \sum_{k \in ℕ_{0}} (k + 1) A (k + 1) y^{k}$
85	84	cbvmptv	$⊢ (a \in S ⟼ \sum_{k \in ℕ_{0}} (k + 1) A (k + 1) a^{k}) = (y \in S ⟼ \sum_{k \in ℕ_{0}} (k + 1) A (k + 1) y^{k})$
86	81 85	eqtrdi	$⊢ φ \to ℂ D F = (y \in S ⟼ \sum_{k \in ℕ_{0}} (k + 1) A (k + 1) y^{k})$

Metamath Proof Explorer

Theorem pserdv

Proof