binomcxplemdvsum

Description: Lemma for binomcxp . The derivative of the generalized sum in binomcxplemnn0 . Part of remark "This convergence allows us to apply term-by-term differentiation..." in the Wikibooks proof. (Contributed by Steve Rodriguez, 22-Apr-2020)

	Ref	Expression
Hypotheses	binomcxp.a	$⊢ φ \to A \in ℝ^{+}$
	binomcxp.b	$⊢ φ \to B \in ℝ$
	binomcxp.lt	$⊢ φ \to \|B\| < \|A\|$
	binomcxp.c	$⊢ φ \to C \in ℂ$
	binomcxplem.f	$⊢ F = (j \in ℕ_{0} ⟼ C C_{𝑐} j)$
	binomcxplem.s	$⊢ S = (b \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) b^{k}))$
	binomcxplem.r	$⊢ R = sup (\{r \in ℝ \| seq 0 (+ S (r)) \in dom ⇝\} ℝ^{*} <)$
	binomcxplem.e	$⊢ E = (b \in ℂ ⟼ (k \in ℕ ⟼ k F (k) b^{k - 1}))$
	binomcxplem.d	$⊢ D = {abs}^{-1} [[0, R)]$
	binomcxplem.p	$⊢ P = (b \in D ⟼ \sum_{k \in ℕ_{0}} S (b) (k))$
Assertion	binomcxplemdvsum	$⊢ φ \to ℂ D P = (b \in D ⟼ \sum_{k \in ℕ} E (b) (k))$

Proof

Step	Hyp	Ref	Expression
1		binomcxp.a	$⊢ φ \to A \in ℝ^{+}$
2		binomcxp.b	$⊢ φ \to B \in ℝ$
3		binomcxp.lt	$⊢ φ \to \|B\| < \|A\|$
4		binomcxp.c	$⊢ φ \to C \in ℂ$
5		binomcxplem.f	$⊢ F = (j \in ℕ_{0} ⟼ C C_{𝑐} j)$
6		binomcxplem.s	$⊢ S = (b \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) b^{k}))$
7		binomcxplem.r	$⊢ R = sup (\{r \in ℝ \| seq 0 (+ S (r)) \in dom ⇝\} ℝ^{*} <)$
8		binomcxplem.e	$⊢ E = (b \in ℂ ⟼ (k \in ℕ ⟼ k F (k) b^{k - 1}))$
9		binomcxplem.d	$⊢ D = {abs}^{-1} [[0, R)]$
10		binomcxplem.p	$⊢ P = (b \in D ⟼ \sum_{k \in ℕ_{0}} S (b) (k))$
11		nfcv	$⊢ \underline{Ⅎ} b {abs}^{-1}$
12		nfcv	$⊢ \underline{Ⅎ} b 0$
13		nfcv	$⊢ \underline{Ⅎ} b [.)$
14		nfcv	$⊢ \underline{Ⅎ} b +$
15		nfmpt1	$⊢ \underline{Ⅎ} b (b \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) b^{k}))$
16	6 15	nfcxfr	$⊢ \underline{Ⅎ} b S$
17		nfcv	$⊢ \underline{Ⅎ} b r$
18	16 17	nffv	$⊢ \underline{Ⅎ} b S (r)$
19	12 14 18	nfseq	$⊢ \underline{Ⅎ} b seq 0 (+ S (r))$
20	19	nfel1	$⊢ Ⅎ b seq 0 (+ S (r)) \in dom ⇝$
21		nfcv	$⊢ \underline{Ⅎ} b ℝ$
22	20 21	nfrabw	$⊢ \underline{Ⅎ} b \{r \in ℝ \| seq 0 (+ S (r)) \in dom ⇝\}$
23		nfcv	$⊢ \underline{Ⅎ} b ℝ^{*}$
24		nfcv	$⊢ \underline{Ⅎ} b <$
25	22 23 24	nfsup	$⊢ \underline{Ⅎ} b sup (\{r \in ℝ \| seq 0 (+ S (r)) \in dom ⇝\} ℝ^{*} <)$
26	7 25	nfcxfr	$⊢ \underline{Ⅎ} b R$
27	12 13 26	nfov	$⊢ \underline{Ⅎ} b [0, R)$
28	11 27	nfima	$⊢ \underline{Ⅎ} b {abs}^{-1} [[0, R)]$
29	9 28	nfcxfr	$⊢ \underline{Ⅎ} b D$
30		nfcv	$⊢ \underline{Ⅎ} y D$
31		nfcv	$⊢ \underline{Ⅎ} y \sum_{k \in ℕ_{0}} S (b) (k)$
32		nfcv	$⊢ \underline{Ⅎ} b ℕ_{0}$
33		nfcv	$⊢ \underline{Ⅎ} b y$
34	16 33	nffv	$⊢ \underline{Ⅎ} b S (y)$
35		nfcv	$⊢ \underline{Ⅎ} b m$
36	34 35	nffv	$⊢ \underline{Ⅎ} b S (y) (m)$
37	32 36	nfsum	$⊢ \underline{Ⅎ} b \sum_{m \in ℕ_{0}} S (y) (m)$
38		simpl	$⊢ (b = y \land k \in ℕ_{0}) \to b = y$
39	38	fveq2d	$⊢ (b = y \land k \in ℕ_{0}) \to S (b) = S (y)$
40	39	fveq1d	$⊢ (b = y \land k \in ℕ_{0}) \to S (b) (k) = S (y) (k)$
41	40	sumeq2dv	$⊢ b = y \to \sum_{k \in ℕ_{0}} S (b) (k) = \sum_{k \in ℕ_{0}} S (y) (k)$
42		nfcv	$⊢ \underline{Ⅎ} m S (y) (k)$
43		nfcv	$⊢ \underline{Ⅎ} k ℂ$
44		nfmpt1	$⊢ \underline{Ⅎ} k (k \in ℕ_{0} ⟼ F (k) b^{k})$
45	43 44	nfmpt	$⊢ \underline{Ⅎ} k (b \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) b^{k}))$
46	6 45	nfcxfr	$⊢ \underline{Ⅎ} k S$
47		nfcv	$⊢ \underline{Ⅎ} k y$
48	46 47	nffv	$⊢ \underline{Ⅎ} k S (y)$
49		nfcv	$⊢ \underline{Ⅎ} k m$
50	48 49	nffv	$⊢ \underline{Ⅎ} k S (y) (m)$
51		fveq2	$⊢ k = m \to S (y) (k) = S (y) (m)$
52	42 50 51	cbvsumi	$⊢ \sum_{k \in ℕ_{0}} S (y) (k) = \sum_{m \in ℕ_{0}} S (y) (m)$
53	41 52	eqtrdi	$⊢ b = y \to \sum_{k \in ℕ_{0}} S (b) (k) = \sum_{m \in ℕ_{0}} S (y) (m)$
54	29 30 31 37 53	cbvmptf	$⊢ (b \in D ⟼ \sum_{k \in ℕ_{0}} S (b) (k)) = (y \in D ⟼ \sum_{m \in ℕ_{0}} S (y) (m))$
55	10 54	eqtri	$⊢ P = (y \in D ⟼ \sum_{m \in ℕ_{0}} S (y) (m))$
56		ovexd	$⊢ (φ \land j \in ℕ_{0}) \to C C_{𝑐} j \in V$
57	5	a1i	$⊢ φ \to F = (j \in ℕ_{0} ⟼ C C_{𝑐} j)$
58	5	a1i	$⊢ (φ \land k \in ℕ_{0}) \to F = (j \in ℕ_{0} ⟼ C C_{𝑐} j)$
59		simpr	$⊢ ((φ \land k \in ℕ_{0}) \land j = k) \to j = k$
60	59	oveq2d	$⊢ ((φ \land k \in ℕ_{0}) \land j = k) \to C C_{𝑐} j = C C_{𝑐} k$
61		simpr	$⊢ (φ \land k \in ℕ_{0}) \to k \in ℕ_{0}$
62	4	adantr	$⊢ (φ \land k \in ℕ_{0}) \to C \in ℂ$
63	62 61	bcccl	$⊢ (φ \land k \in ℕ_{0}) \to C C_{𝑐} k \in ℂ$
64	58 60 61 63	fvmptd	$⊢ (φ \land k \in ℕ_{0}) \to F (k) = C C_{𝑐} k$
65	64 63	eqeltrd	$⊢ (φ \land k \in ℕ_{0}) \to F (k) \in ℂ$
66	56 57 65	fmpt2d	$⊢ φ \to F : ℕ_{0} ⟶ ℂ$
67		nfcv	$⊢ \underline{Ⅎ} r ℝ$
68		nfcv	$⊢ \underline{Ⅎ} z ℝ$
69		nfv	$⊢ Ⅎ z seq 0 (+ S (r)) \in dom ⇝$
70		nfcv	$⊢ \underline{Ⅎ} r 0$
71		nfcv	$⊢ \underline{Ⅎ} r +$
72		nfcv	$⊢ \underline{Ⅎ} r (b \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) b^{k}))$
73	6 72	nfcxfr	$⊢ \underline{Ⅎ} r S$
74		nfcv	$⊢ \underline{Ⅎ} r z$
75	73 74	nffv	$⊢ \underline{Ⅎ} r S (z)$
76	70 71 75	nfseq	$⊢ \underline{Ⅎ} r seq 0 (+ S (z))$
77	76	nfel1	$⊢ Ⅎ r seq 0 (+ S (z)) \in dom ⇝$
78		fveq2	$⊢ r = z \to S (r) = S (z)$
79	78	seqeq3d	$⊢ r = z \to seq 0 (+ S (r)) = seq 0 (+ S (z))$
80	79	eleq1d	$⊢ r = z \to (seq 0 (+ S (r)) \in dom ⇝ \leftrightarrow seq 0 (+ S (z)) \in dom ⇝)$
81	67 68 69 77 80	cbvrabw	$⊢ \{r \in ℝ \| seq 0 (+ S (r)) \in dom ⇝\} = \{z \in ℝ \| seq 0 (+ S (z)) \in dom ⇝\}$
82	81	supeq1i	$⊢ sup (\{r \in ℝ \| seq 0 (+ S (r)) \in dom ⇝\} ℝ^{} <) = sup (\{z \in ℝ \| seq 0 (+ S (z)) \in dom ⇝\} ℝ^{} <)$
83	7 82	eqtri	$⊢ R = sup (\{z \in ℝ \| seq 0 (+ S (z)) \in dom ⇝\} ℝ^{*} <)$
84	6	fveq1i	$⊢ S (z) = (b \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) b^{k})) (z)$
85		seqeq3	$⊢ S (z) = (b \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) b^{k})) (z) \to seq 0 (+ S (z)) = seq 0 (+ (b \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) b^{k})) (z))$
86	84 85	ax-mp	$⊢ seq 0 (+ S (z)) = seq 0 (+ (b \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) b^{k})) (z))$
87	86	eleq1i	$⊢ seq 0 (+ S (z)) \in dom ⇝ \leftrightarrow seq 0 (+ (b \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) b^{k})) (z)) \in dom ⇝$
88	87	rabbii	$⊢ \{z \in ℝ \| seq 0 (+ S (z)) \in dom ⇝\} = \{z \in ℝ \| seq 0 (+ (b \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) b^{k})) (z)) \in dom ⇝\}$
89	88	supeq1i	$⊢ sup (\{z \in ℝ \| seq 0 (+ S (z)) \in dom ⇝\} ℝ^{} <) = sup (\{z \in ℝ \| seq 0 (+ (b \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) b^{k})) (z)) \in dom ⇝\} ℝ^{} <)$
90	7 82 89	3eqtrri	$⊢ sup (\{z \in ℝ \| seq 0 (+ (b \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) b^{k})) (z)) \in dom ⇝\} ℝ^{*} <) = R$
91	90	eleq1i	$⊢ sup (\{z \in ℝ \| seq 0 (+ (b \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) b^{k})) (z)) \in dom ⇝\} ℝ^{*} <) \in ℝ \leftrightarrow R \in ℝ$
92	90	oveq2i	$⊢ \|x\| + sup (\{z \in ℝ \| seq 0 (+ (b \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) b^{k})) (z)) \in dom ⇝\} ℝ^{*} <) = \|x\| + R$
93	92	oveq1i	$⊢ \frac{\|x\| + sup (\{z \in ℝ \| seq 0 (+ (b \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) b^{k})) (z)) \in dom ⇝\} ℝ^{*} <)}{2} = \frac{\|x\| + R}{2}$
94		eqid	$⊢ \|x\| + 1 = \|x\| + 1$
95	91 93 94	ifbieq12i	$⊢ if (sup (\{z \in ℝ \| seq 0 (+ (b \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) b^{k})) (z)) \in dom ⇝\} ℝ^{} <) \in ℝ, \frac{\|x\| + sup (\{z \in ℝ \| seq 0 (+ (b \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) b^{k})) (z)) \in dom ⇝\} ℝ^{} <)}{2}, \|x\| + 1) = if (R \in ℝ, \frac{\|x\| + R}{2}, \|x\| + 1)$
96		oveq1	$⊢ w = b \to w^{k} = b^{k}$
97	96	oveq2d	$⊢ w = b \to F (k) w^{k} = F (k) b^{k}$
98	97	mpteq2dv	$⊢ w = b \to (k \in ℕ_{0} ⟼ F (k) w^{k}) = (k \in ℕ_{0} ⟼ F (k) b^{k})$
99	98	cbvmptv	$⊢ (w \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) w^{k})) = (b \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) b^{k}))$
100	99	fveq1i	$⊢ (w \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) w^{k})) (z) = (b \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) b^{k})) (z)$
101		seqeq3	$⊢ (w \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) w^{k})) (z) = (b \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) b^{k})) (z) \to seq 0 (+ (w \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) w^{k})) (z)) = seq 0 (+ (b \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) b^{k})) (z))$
102	100 101	ax-mp	$⊢ seq 0 (+ (w \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) w^{k})) (z)) = seq 0 (+ (b \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) b^{k})) (z))$
103	102	eleq1i	$⊢ seq 0 (+ (w \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) w^{k})) (z)) \in dom ⇝ \leftrightarrow seq 0 (+ (b \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) b^{k})) (z)) \in dom ⇝$
104	103	rabbii	$⊢ \{z \in ℝ \| seq 0 (+ (w \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) w^{k})) (z)) \in dom ⇝\} = \{z \in ℝ \| seq 0 (+ (b \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) b^{k})) (z)) \in dom ⇝\}$
105	104	supeq1i	$⊢ sup (\{z \in ℝ \| seq 0 (+ (w \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) w^{k})) (z)) \in dom ⇝\} ℝ^{} <) = sup (\{z \in ℝ \| seq 0 (+ (b \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) b^{k})) (z)) \in dom ⇝\} ℝ^{} <)$
106	105	eleq1i	$⊢ sup (\{z \in ℝ \| seq 0 (+ (w \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) w^{k})) (z)) \in dom ⇝\} ℝ^{} <) \in ℝ \leftrightarrow sup (\{z \in ℝ \| seq 0 (+ (b \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) b^{k})) (z)) \in dom ⇝\} ℝ^{} <) \in ℝ$
107	105	oveq2i	$⊢ \|x\| + sup (\{z \in ℝ \| seq 0 (+ (w \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) w^{k})) (z)) \in dom ⇝\} ℝ^{} <) = \|x\| + sup (\{z \in ℝ \| seq 0 (+ (b \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) b^{k})) (z)) \in dom ⇝\} ℝ^{} <)$
108	107	oveq1i	$⊢ \frac{\|x\| + sup (\{z \in ℝ \| seq 0 (+ (w \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) w^{k})) (z)) \in dom ⇝\} ℝ^{} <)}{2} = \frac{\|x\| + sup (\{z \in ℝ \| seq 0 (+ (b \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) b^{k})) (z)) \in dom ⇝\} ℝ^{} <)}{2}$
109	106 108 94	ifbieq12i	$⊢ if (sup (\{z \in ℝ \| seq 0 (+ (w \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) w^{k})) (z)) \in dom ⇝\} ℝ^{} <) \in ℝ, \frac{\|x\| + sup (\{z \in ℝ \| seq 0 (+ (w \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) w^{k})) (z)) \in dom ⇝\} ℝ^{} <)}{2}, \|x\| + 1) = if (sup (\{z \in ℝ \| seq 0 (+ (b \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) b^{k})) (z)) \in dom ⇝\} ℝ^{} <) \in ℝ, \frac{\|x\| + sup (\{z \in ℝ \| seq 0 (+ (b \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) b^{k})) (z)) \in dom ⇝\} ℝ^{} <)}{2}, \|x\| + 1)$
110	109	oveq2i	$⊢ \|x\| + if (sup (\{z \in ℝ \| seq 0 (+ (w \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) w^{k})) (z)) \in dom ⇝\} ℝ^{} <) \in ℝ, \frac{\|x\| + sup (\{z \in ℝ \| seq 0 (+ (w \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) w^{k})) (z)) \in dom ⇝\} ℝ^{} <)}{2}, \|x\| + 1) = \|x\| + if (sup (\{z \in ℝ \| seq 0 (+ (b \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) b^{k})) (z)) \in dom ⇝\} ℝ^{} <) \in ℝ, \frac{\|x\| + sup (\{z \in ℝ \| seq 0 (+ (b \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) b^{k})) (z)) \in dom ⇝\} ℝ^{} <)}{2}, \|x\| + 1)$
111	110	oveq1i	$⊢ \frac{\|x\| + if (sup (\{z \in ℝ \| seq 0 (+ (w \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) w^{k})) (z)) \in dom ⇝\} ℝ^{} <) \in ℝ, \frac{\|x\| + sup (\{z \in ℝ \| seq 0 (+ (w \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) w^{k})) (z)) \in dom ⇝\} ℝ^{} <)}{2}, \|x\| + 1)}{2} = \frac{\|x\| + if (sup (\{z \in ℝ \| seq 0 (+ (b \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) b^{k})) (z)) \in dom ⇝\} ℝ^{} <) \in ℝ, \frac{\|x\| + sup (\{z \in ℝ \| seq 0 (+ (b \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) b^{k})) (z)) \in dom ⇝\} ℝ^{} <)}{2}, \|x\| + 1)}{2}$
112	111	oveq2i	$⊢ 0 ball (abs \circ -) (\frac{\|x\| + if (sup (\{z \in ℝ \| seq 0 (+ (w \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) w^{k})) (z)) \in dom ⇝\} ℝ^{} <) \in ℝ, \frac{\|x\| + sup (\{z \in ℝ \| seq 0 (+ (w \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) w^{k})) (z)) \in dom ⇝\} ℝ^{} <)}{2}, \|x\| + 1)}{2}) = 0 ball (abs \circ -) (\frac{\|x\| + if (sup (\{z \in ℝ \| seq 0 (+ (b \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) b^{k})) (z)) \in dom ⇝\} ℝ^{} <) \in ℝ, \frac{\|x\| + sup (\{z \in ℝ \| seq 0 (+ (b \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) b^{k})) (z)) \in dom ⇝\} ℝ^{} <)}{2}, \|x\| + 1)}{2})$
113	6 55 66 83 9 95 112	pserdv2	$⊢ φ \to ℂ D P = (y \in D ⟼ \sum_{n \in ℕ} n F (n) y^{n - 1})$
114		cnvimass	$⊢ {abs}^{-1} [[0, R)] \subseteq dom abs$
115	9 114	eqsstri	$⊢ D \subseteq dom abs$
116		absf	$⊢ abs : ℂ ⟶ ℝ$
117	116	fdmi	$⊢ dom abs = ℂ$
118	115 117	sseqtri	$⊢ D \subseteq ℂ$
119	118	sseli	$⊢ y \in D \to y \in ℂ$
120	8	a1i	$⊢ (φ \land y \in ℂ) \to E = (b \in ℂ ⟼ (k \in ℕ ⟼ k F (k) b^{k - 1}))$
121		simplr	$⊢ (((φ \land y \in ℂ) \land b = y) \land k \in ℕ) \to b = y$
122	121	oveq1d	$⊢ (((φ \land y \in ℂ) \land b = y) \land k \in ℕ) \to b^{k - 1} = y^{k - 1}$
123	122	oveq2d	$⊢ (((φ \land y \in ℂ) \land b = y) \land k \in ℕ) \to k F (k) b^{k - 1} = k F (k) y^{k - 1}$
124	123	mpteq2dva	$⊢ ((φ \land y \in ℂ) \land b = y) \to (k \in ℕ ⟼ k F (k) b^{k - 1}) = (k \in ℕ ⟼ k F (k) y^{k - 1})$
125		simpr	$⊢ (φ \land y \in ℂ) \to y \in ℂ$
126		nnex	$⊢ ℕ \in V$
127	126	mptex	$⊢ (k \in ℕ ⟼ k F (k) y^{k - 1}) \in V$
128	127	a1i	$⊢ (φ \land y \in ℂ) \to (k \in ℕ ⟼ k F (k) y^{k - 1}) \in V$
129	120 124 125 128	fvmptd	$⊢ (φ \land y \in ℂ) \to E (y) = (k \in ℕ ⟼ k F (k) y^{k - 1})$
130	129	adantr	$⊢ ((φ \land y \in ℂ) \land n \in ℕ) \to E (y) = (k \in ℕ ⟼ k F (k) y^{k - 1})$
131		simpr	$⊢ (((φ \land y \in ℂ) \land n \in ℕ) \land k = n) \to k = n$
132	131	fveq2d	$⊢ (((φ \land y \in ℂ) \land n \in ℕ) \land k = n) \to F (k) = F (n)$
133	131 132	oveq12d	$⊢ (((φ \land y \in ℂ) \land n \in ℕ) \land k = n) \to k F (k) = n F (n)$
134	131	oveq1d	$⊢ (((φ \land y \in ℂ) \land n \in ℕ) \land k = n) \to k - 1 = n - 1$
135	134	oveq2d	$⊢ (((φ \land y \in ℂ) \land n \in ℕ) \land k = n) \to y^{k - 1} = y^{n - 1}$
136	133 135	oveq12d	$⊢ (((φ \land y \in ℂ) \land n \in ℕ) \land k = n) \to k F (k) y^{k - 1} = n F (n) y^{n - 1}$
137		simpr	$⊢ ((φ \land y \in ℂ) \land n \in ℕ) \to n \in ℕ$
138		ovexd	$⊢ ((φ \land y \in ℂ) \land n \in ℕ) \to n F (n) y^{n - 1} \in V$
139	130 136 137 138	fvmptd	$⊢ ((φ \land y \in ℂ) \land n \in ℕ) \to E (y) (n) = n F (n) y^{n - 1}$
140	139	sumeq2dv	$⊢ (φ \land y \in ℂ) \to \sum_{n \in ℕ} E (y) (n) = \sum_{n \in ℕ} n F (n) y^{n - 1}$
141	119 140	sylan2	$⊢ (φ \land y \in D) \to \sum_{n \in ℕ} E (y) (n) = \sum_{n \in ℕ} n F (n) y^{n - 1}$
142	141	mpteq2dva	$⊢ φ \to (y \in D ⟼ \sum_{n \in ℕ} E (y) (n)) = (y \in D ⟼ \sum_{n \in ℕ} n F (n) y^{n - 1})$
143	113 142	eqtr4d	$⊢ φ \to ℂ D P = (y \in D ⟼ \sum_{n \in ℕ} E (y) (n))$
144		nfcv	$⊢ \underline{Ⅎ} b ℕ$
145		nfmpt1	$⊢ \underline{Ⅎ} b (b \in ℂ ⟼ (k \in ℕ ⟼ k F (k) b^{k - 1}))$
146	8 145	nfcxfr	$⊢ \underline{Ⅎ} b E$
147	146 33	nffv	$⊢ \underline{Ⅎ} b E (y)$
148		nfcv	$⊢ \underline{Ⅎ} b n$
149	147 148	nffv	$⊢ \underline{Ⅎ} b E (y) (n)$
150	144 149	nfsum	$⊢ \underline{Ⅎ} b \sum_{n \in ℕ} E (y) (n)$
151		nfcv	$⊢ \underline{Ⅎ} y \sum_{k \in ℕ} E (b) (k)$
152		simpl	$⊢ (y = b \land n \in ℕ) \to y = b$
153	152	fveq2d	$⊢ (y = b \land n \in ℕ) \to E (y) = E (b)$
154	153	fveq1d	$⊢ (y = b \land n \in ℕ) \to E (y) (n) = E (b) (n)$
155	154	sumeq2dv	$⊢ y = b \to \sum_{n \in ℕ} E (y) (n) = \sum_{n \in ℕ} E (b) (n)$
156		nfmpt1	$⊢ \underline{Ⅎ} k (k \in ℕ ⟼ k F (k) b^{k - 1})$
157	43 156	nfmpt	$⊢ \underline{Ⅎ} k (b \in ℂ ⟼ (k \in ℕ ⟼ k F (k) b^{k - 1}))$
158	8 157	nfcxfr	$⊢ \underline{Ⅎ} k E$
159		nfcv	$⊢ \underline{Ⅎ} k b$
160	158 159	nffv	$⊢ \underline{Ⅎ} k E (b)$
161		nfcv	$⊢ \underline{Ⅎ} k n$
162	160 161	nffv	$⊢ \underline{Ⅎ} k E (b) (n)$
163		nfcv	$⊢ \underline{Ⅎ} n E (b) (k)$
164		fveq2	$⊢ n = k \to E (b) (n) = E (b) (k)$
165	162 163 164	cbvsumi	$⊢ \sum_{n \in ℕ} E (b) (n) = \sum_{k \in ℕ} E (b) (k)$
166	155 165	eqtrdi	$⊢ y = b \to \sum_{n \in ℕ} E (y) (n) = \sum_{k \in ℕ} E (b) (k)$
167	30 29 150 151 166	cbvmptf	$⊢ (y \in D ⟼ \sum_{n \in ℕ} E (y) (n)) = (b \in D ⟼ \sum_{k \in ℕ} E (b) (k))$
168	143 167	eqtrdi	$⊢ φ \to ℂ D P = (b \in D ⟼ \sum_{k \in ℕ} E (b) (k))$

Metamath Proof Explorer

Theorem binomcxplemdvsum

Proof