binomcxplemdvbinom

Description: Lemma for binomcxp . By the power and chain rules, calculate the derivative of ( ( 1 + b ) ^c -u C ) , with respect to b in the disk of convergence D . We later multiply the derivative in the later binomcxplemdvsum by this derivative to show that ( ( 1 + b ) ^c C ) (with a nonnegated C ) and the later sum, since both at b = 0 equal one, are the same. (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)]$
Assertion	binomcxplemdvbinom	$⊢ (φ \land \neg C \in ℕ_{0}) \to \frac{d (b \in D⟼ {(1 + b)}^{- C})}{d_{ℂ} b} = (b \in D ⟼ (- C) {(1 + b)}^{- C - 1})$

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		nfcv	$⊢ \underline{Ⅎ} b {abs}^{-1}$
11		nfcv	$⊢ \underline{Ⅎ} b 0$
12		nfcv	$⊢ \underline{Ⅎ} b [.)$
13		nfcv	$⊢ \underline{Ⅎ} b +$
14		nfmpt1	$⊢ \underline{Ⅎ} b (b \in ℂ ⟼ (k \in ℕ_{0} ⟼ F (k) b^{k}))$
15	6 14	nfcxfr	$⊢ \underline{Ⅎ} b S$
16		nfcv	$⊢ \underline{Ⅎ} b r$
17	15 16	nffv	$⊢ \underline{Ⅎ} b S (r)$
18	11 13 17	nfseq	$⊢ \underline{Ⅎ} b seq 0 (+ S (r))$
19	18	nfel1	$⊢ Ⅎ b seq 0 (+ S (r)) \in dom ⇝$
20		nfcv	$⊢ \underline{Ⅎ} b ℝ$
21	19 20	nfrabw	$⊢ \underline{Ⅎ} b \{r \in ℝ \| seq 0 (+ S (r)) \in dom ⇝\}$
22		nfcv	$⊢ \underline{Ⅎ} b ℝ^{*}$
23		nfcv	$⊢ \underline{Ⅎ} b <$
24	21 22 23	nfsup	$⊢ \underline{Ⅎ} b sup (\{r \in ℝ \| seq 0 (+ S (r)) \in dom ⇝\} ℝ^{*} <)$
25	7 24	nfcxfr	$⊢ \underline{Ⅎ} b R$
26	11 12 25	nfov	$⊢ \underline{Ⅎ} b [0, R)$
27	10 26	nfima	$⊢ \underline{Ⅎ} b {abs}^{-1} [[0, R)]$
28	9 27	nfcxfr	$⊢ \underline{Ⅎ} b D$
29		nfcv	$⊢ \underline{Ⅎ} y D$
30		nfcv	$⊢ \underline{Ⅎ} y {(1 + b)}^{- C}$
31		nfcv	$⊢ \underline{Ⅎ} b {(1 + y)}^{- C}$
32		oveq2	$⊢ b = y \to 1 + b = 1 + y$
33	32	oveq1d	$⊢ b = y \to {(1 + b)}^{- C} = {(1 + y)}^{- C}$
34	28 29 30 31 33	cbvmptf	$⊢ (b \in D ⟼ {(1 + b)}^{- C}) = (y \in D ⟼ {(1 + y)}^{- C})$
35	34	oveq2i	$⊢ \frac{d (b \in D⟼ {(1 + b)}^{- C})}{d_{ℂ} b} = \frac{d (y \in D⟼ {(1 + y)}^{- C})}{d_{ℂ} y}$
36		cnelprrecn	$⊢ ℂ \in \{ℝ, ℂ\}$
37	36	a1i	$⊢ (φ \land \neg C \in ℕ_{0}) \to ℂ \in \{ℝ, ℂ\}$
38		1cnd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land y \in D) \to 1 \in ℂ$
39		cnvimass	$⊢ {abs}^{-1} [[0, R)] \subseteq dom abs$
40	9 39	eqsstri	$⊢ D \subseteq dom abs$
41		absf	$⊢ abs : ℂ ⟶ ℝ$
42	41	fdmi	$⊢ dom abs = ℂ$
43	40 42	sseqtri	$⊢ D \subseteq ℂ$
44	43	a1i	$⊢ (φ \land \neg C \in ℕ_{0}) \to D \subseteq ℂ$
45	44	sselda	$⊢ ((φ \land \neg C \in ℕ_{0}) \land y \in D) \to y \in ℂ$
46	38 45	addcld	$⊢ ((φ \land \neg C \in ℕ_{0}) \land y \in D) \to 1 + y \in ℂ$
47		simpr	$⊢ (((φ \land \neg C \in ℕ_{0}) \land y \in D) \land 1 + y \in ℝ) \to 1 + y \in ℝ$
48		1cnd	$⊢ (((φ \land \neg C \in ℕ_{0}) \land y \in D) \land 1 + y \in ℝ) \to 1 \in ℂ$
49	45	adantr	$⊢ (((φ \land \neg C \in ℕ_{0}) \land y \in D) \land 1 + y \in ℝ) \to y \in ℂ$
50	48 49	pncan2d	$⊢ (((φ \land \neg C \in ℕ_{0}) \land y \in D) \land 1 + y \in ℝ) \to 1 + y - 1 = y$
51		1red	$⊢ (((φ \land \neg C \in ℕ_{0}) \land y \in D) \land 1 + y \in ℝ) \to 1 \in ℝ$
52	47 51	resubcld	$⊢ (((φ \land \neg C \in ℕ_{0}) \land y \in D) \land 1 + y \in ℝ) \to 1 + y - 1 \in ℝ$
53	50 52	eqeltrrd	$⊢ (((φ \land \neg C \in ℕ_{0}) \land y \in D) \land 1 + y \in ℝ) \to y \in ℝ$
54		1pneg1e0	$⊢ 1 + -1 = 0$
55		1red	$⊢ (((φ \land \neg C \in ℕ_{0}) \land y \in D) \land y \in ℝ) \to 1 \in ℝ$
56	55	renegcld	$⊢ (((φ \land \neg C \in ℕ_{0}) \land y \in D) \land y \in ℝ) \to - 1 \in ℝ$
57		simpr	$⊢ (((φ \land \neg C \in ℕ_{0}) \land y \in D) \land y \in ℝ) \to y \in ℝ$
58		ffn	$⊢ abs : ℂ ⟶ ℝ \to abs Fn ℂ$
59		elpreima	$⊢ abs Fn ℂ \to (y \in {abs}^{-1} [[0, R)] \leftrightarrow (y \in ℂ \land \|y\| \in [0, R)))$
60	41 58 59	mp2b	$⊢ y \in {abs}^{-1} [[0, R)] \leftrightarrow (y \in ℂ \land \|y\| \in [0, R))$
61	60	simprbi	$⊢ y \in {abs}^{-1} [[0, R)] \to \|y\| \in [0, R)$
62	61 9	eleq2s	$⊢ y \in D \to \|y\| \in [0, R)$
63		0re	$⊢ 0 \in ℝ$
64		ssrab2	$⊢ \{r \in ℝ \| seq 0 (+ S (r)) \in dom ⇝\} \subseteq ℝ$
65		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
66	64 65	sstri	$⊢ \{r \in ℝ \| seq 0 (+ S (r)) \in dom ⇝\} \subseteq ℝ^{*}$
67		supxrcl	$⊢ \{r \in ℝ \| seq 0 (+ S (r)) \in dom ⇝\} \subseteq ℝ^{} \to sup (\{r \in ℝ \| seq 0 (+ S (r)) \in dom ⇝\} ℝ^{} <) \in ℝ^{*}$
68	66 67	ax-mp	$⊢ sup (\{r \in ℝ \| seq 0 (+ S (r)) \in dom ⇝\} ℝ^{} <) \in ℝ^{}$
69	7 68	eqeltri	$⊢ R \in ℝ^{*}$
70		elico2	$⊢ (0 \in ℝ \land R \in ℝ^{*}) \to (\|y\| \in [0, R) \leftrightarrow (\|y\| \in ℝ \land 0 \leq \|y\| \land \|y\| < R))$
71	63 69 70	mp2an	$⊢ \|y\| \in [0, R) \leftrightarrow (\|y\| \in ℝ \land 0 \leq \|y\| \land \|y\| < R)$
72	62 71	sylib	$⊢ y \in D \to (\|y\| \in ℝ \land 0 \leq \|y\| \land \|y\| < R)$
73	72	simp3d	$⊢ y \in D \to \|y\| < R$
74	73	adantl	$⊢ ((φ \land \neg C \in ℕ_{0}) \land y \in D) \to \|y\| < R$
75	1 2 3 4 5 6 7	binomcxplemradcnv	$⊢ (φ \land \neg C \in ℕ_{0}) \to R = 1$
76	75	adantr	$⊢ ((φ \land \neg C \in ℕ_{0}) \land y \in D) \to R = 1$
77	74 76	breqtrd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land y \in D) \to \|y\| < 1$
78	77	adantr	$⊢ (((φ \land \neg C \in ℕ_{0}) \land y \in D) \land y \in ℝ) \to \|y\| < 1$
79	57 55	absltd	$⊢ (((φ \land \neg C \in ℕ_{0}) \land y \in D) \land y \in ℝ) \to (\|y\| < 1 \leftrightarrow (- 1 < y \land y < 1))$
80	78 79	mpbid	$⊢ (((φ \land \neg C \in ℕ_{0}) \land y \in D) \land y \in ℝ) \to (- 1 < y \land y < 1)$
81	80	simpld	$⊢ (((φ \land \neg C \in ℕ_{0}) \land y \in D) \land y \in ℝ) \to - 1 < y$
82	56 57 55 81	ltadd2dd	$⊢ (((φ \land \neg C \in ℕ_{0}) \land y \in D) \land y \in ℝ) \to 1 + -1 < 1 + y$
83	54 82	eqbrtrrid	$⊢ (((φ \land \neg C \in ℕ_{0}) \land y \in D) \land y \in ℝ) \to 0 < 1 + y$
84	53 83	syldan	$⊢ (((φ \land \neg C \in ℕ_{0}) \land y \in D) \land 1 + y \in ℝ) \to 0 < 1 + y$
85	47 84	elrpd	$⊢ (((φ \land \neg C \in ℕ_{0}) \land y \in D) \land 1 + y \in ℝ) \to 1 + y \in ℝ^{+}$
86	85	ex	$⊢ ((φ \land \neg C \in ℕ_{0}) \land y \in D) \to (1 + y \in ℝ \to 1 + y \in ℝ^{+})$
87		eqid	$⊢ ℂ ∖ (−∞, 0] = ℂ ∖ (−∞, 0]$
88	87	ellogdm	$⊢ 1 + y \in (ℂ ∖ (−∞, 0]) \leftrightarrow (1 + y \in ℂ \land (1 + y \in ℝ \to 1 + y \in ℝ^{+}))$
89	46 86 88	sylanbrc	$⊢ ((φ \land \neg C \in ℕ_{0}) \land y \in D) \to 1 + y \in (ℂ ∖ (−∞, 0])$
90		eldifi	$⊢ x \in (ℂ ∖ (−∞, 0]) \to x \in ℂ$
91	90	adantl	$⊢ ((φ \land \neg C \in ℕ_{0}) \land x \in (ℂ ∖ (−∞, 0])) \to x \in ℂ$
92	4	adantr	$⊢ (φ \land \neg C \in ℕ_{0}) \to C \in ℂ$
93	92	negcld	$⊢ (φ \land \neg C \in ℕ_{0}) \to - C \in ℂ$
94	93	adantr	$⊢ ((φ \land \neg C \in ℕ_{0}) \land x \in (ℂ ∖ (−∞, 0])) \to - C \in ℂ$
95	91 94	cxpcld	$⊢ ((φ \land \neg C \in ℕ_{0}) \land x \in (ℂ ∖ (−∞, 0])) \to x^{- C} \in ℂ$
96		ovexd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land x \in (ℂ ∖ (−∞, 0])) \to (- C) x^{- C - 1} \in V$
97		1cnd	$⊢ ((φ \land \neg C \in ℕ_{0}) \land x \in ℂ) \to 1 \in ℂ$
98		simpr	$⊢ ((φ \land \neg C \in ℕ_{0}) \land x \in ℂ) \to x \in ℂ$
99	97 98	addcld	$⊢ ((φ \land \neg C \in ℕ_{0}) \land x \in ℂ) \to 1 + x \in ℂ$
100		c0ex	$⊢ 0 \in V$
101	100	a1i	$⊢ ((φ \land \neg C \in ℕ_{0}) \land x \in ℂ) \to 0 \in V$
102		1cnd	$⊢ (φ \land \neg C \in ℕ_{0}) \to 1 \in ℂ$
103	37 102	dvmptc	$⊢ (φ \land \neg C \in ℕ_{0}) \to \frac{d (x \in ℂ⟼ 1)}{d_{ℂ} x} = (x \in ℂ ⟼ 0)$
104	37	dvmptid	$⊢ (φ \land \neg C \in ℕ_{0}) \to \frac{d (x \in ℂ⟼ x)}{d_{ℂ} x} = (x \in ℂ ⟼ 1)$
105	37 97 101 103 98 97 104	dvmptadd	$⊢ (φ \land \neg C \in ℕ_{0}) \to \frac{d (x \in ℂ⟼ 1 + x)}{d_{ℂ} x} = (x \in ℂ ⟼ 0 + 1)$
106		0p1e1	$⊢ 0 + 1 = 1$
107	106	mpteq2i	$⊢ (x \in ℂ ⟼ 0 + 1) = (x \in ℂ ⟼ 1)$
108	105 107	eqtrdi	$⊢ (φ \land \neg C \in ℕ_{0}) \to \frac{d (x \in ℂ⟼ 1 + x)}{d_{ℂ} x} = (x \in ℂ ⟼ 1)$
109		fvex	$⊢ TopOpen (ℂ_{fld}) \in V$
110		cnfldtps	$⊢ ℂ_{fld} \in TopSp$
111		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
112		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
113	111 112	tpsuni	$⊢ ℂ_{fld} \in TopSp \to ℂ = ⋃ TopOpen (ℂ_{fld})$
114	110 113	ax-mp	$⊢ ℂ = ⋃ TopOpen (ℂ_{fld})$
115	114	restid	$⊢ TopOpen (ℂ_{fld}) \in V \to TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ = TopOpen (ℂ_{fld})$
116	109 115	ax-mp	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ = TopOpen (ℂ_{fld})$
117	116	eqcomi	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ$
118	112	cnfldtop	$⊢ TopOpen (ℂ_{fld}) \in Top$
119		eqid	$⊢ abs \circ - = abs \circ -$
120	119	cnbl0	$⊢ R \in ℝ^{*} \to {abs}^{-1} [[0, R)] = 0 ball (abs \circ -) R$
121	69 120	ax-mp	$⊢ {abs}^{-1} [[0, R)] = 0 ball (abs \circ -) R$
122	9 121	eqtri	$⊢ D = 0 ball (abs \circ -) R$
123		cnxmet	$⊢ abs \circ - \in ∞Met (ℂ)$
124		0cn	$⊢ 0 \in ℂ$
125	112	cnfldtopn	$⊢ TopOpen (ℂ_{fld}) = MetOpen (abs \circ -)$
126	125	blopn	$⊢ (abs \circ - \in ∞Met (ℂ) \land 0 \in ℂ \land R \in ℝ^{*}) \to 0 ball (abs \circ -) R \in TopOpen (ℂ_{fld})$
127	123 124 69 126	mp3an	$⊢ 0 ball (abs \circ -) R \in TopOpen (ℂ_{fld})$
128	122 127	eqeltri	$⊢ D \in TopOpen (ℂ_{fld})$
129		isopn3i	$⊢ (TopOpen (ℂ_{fld}) \in Top \land D \in TopOpen (ℂ_{fld})) \to int (TopOpen (ℂ_{fld})) (D) = D$
130	118 128 129	mp2an	$⊢ int (TopOpen (ℂ_{fld})) (D) = D$
131	130	a1i	$⊢ (φ \land \neg C \in ℕ_{0}) \to int (TopOpen (ℂ_{fld})) (D) = D$
132	37 99 97 108 44 117 112 131	dvmptres2	$⊢ (φ \land \neg C \in ℕ_{0}) \to \frac{d (x \in D⟼ 1 + x)}{d_{ℂ} x} = (x \in D ⟼ 1)$
133		oveq2	$⊢ x = y \to 1 + x = 1 + y$
134	133	cbvmptv	$⊢ (x \in D ⟼ 1 + x) = (y \in D ⟼ 1 + y)$
135	134	oveq2i	$⊢ \frac{d (x \in D⟼ 1 + x)}{d_{ℂ} x} = \frac{d (y \in D⟼ 1 + y)}{d_{ℂ} y}$
136		eqidd	$⊢ x = y \to 1 = 1$
137	136	cbvmptv	$⊢ (x \in D ⟼ 1) = (y \in D ⟼ 1)$
138	132 135 137	3eqtr3g	$⊢ (φ \land \neg C \in ℕ_{0}) \to \frac{d (y \in D⟼ 1 + y)}{d_{ℂ} y} = (y \in D ⟼ 1)$
139	87	dvcncxp1	$⊢ - C \in ℂ \to \frac{d (x \in (ℂ ∖ (−∞, 0])⟼ x^{- C})}{d_{ℂ} x} = (x \in (ℂ ∖ (−∞, 0]) ⟼ (- C) x^{- C - 1})$
140	93 139	syl	$⊢ (φ \land \neg C \in ℕ_{0}) \to \frac{d (x \in (ℂ ∖ (−∞, 0])⟼ x^{- C})}{d_{ℂ} x} = (x \in (ℂ ∖ (−∞, 0]) ⟼ (- C) x^{- C - 1})$
141		oveq1	$⊢ x = 1 + y \to x^{- C} = {(1 + y)}^{- C}$
142		oveq1	$⊢ x = 1 + y \to x^{- C - 1} = {(1 + y)}^{- C - 1}$
143	142	oveq2d	$⊢ x = 1 + y \to (- C) x^{- C - 1} = (- C) {(1 + y)}^{- C - 1}$
144	37 37 89 38 95 96 138 140 141 143	dvmptco	$⊢ (φ \land \neg C \in ℕ_{0}) \to \frac{d (y \in D⟼ {(1 + y)}^{- C})}{d_{ℂ} y} = (y \in D ⟼ (- C) {(1 + y)}^{- C - 1} \cdot 1)$
145	92	adantr	$⊢ ((φ \land \neg C \in ℕ_{0}) \land y \in D) \to C \in ℂ$
146	145	negcld	$⊢ ((φ \land \neg C \in ℕ_{0}) \land y \in D) \to - C \in ℂ$
147	146 38	subcld	$⊢ ((φ \land \neg C \in ℕ_{0}) \land y \in D) \to - C - 1 \in ℂ$
148	46 147	cxpcld	$⊢ ((φ \land \neg C \in ℕ_{0}) \land y \in D) \to {(1 + y)}^{- C - 1} \in ℂ$
149	146 148	mulcld	$⊢ ((φ \land \neg C \in ℕ_{0}) \land y \in D) \to (- C) {(1 + y)}^{- C - 1} \in ℂ$
150	149	mulid1d	$⊢ ((φ \land \neg C \in ℕ_{0}) \land y \in D) \to (- C) {(1 + y)}^{- C - 1} \cdot 1 = (- C) {(1 + y)}^{- C - 1}$
151	150	mpteq2dva	$⊢ (φ \land \neg C \in ℕ_{0}) \to (y \in D ⟼ (- C) {(1 + y)}^{- C - 1} \cdot 1) = (y \in D ⟼ (- C) {(1 + y)}^{- C - 1})$
152		nfcv	$⊢ \underline{Ⅎ} b (- C) {(1 + y)}^{- C - 1}$
153		nfcv	$⊢ \underline{Ⅎ} y (- C) {(1 + b)}^{- C - 1}$
154		oveq2	$⊢ y = b \to 1 + y = 1 + b$
155	154	oveq1d	$⊢ y = b \to {(1 + y)}^{- C - 1} = {(1 + b)}^{- C - 1}$
156	155	oveq2d	$⊢ y = b \to (- C) {(1 + y)}^{- C - 1} = (- C) {(1 + b)}^{- C - 1}$
157	29 28 152 153 156	cbvmptf	$⊢ (y \in D ⟼ (- C) {(1 + y)}^{- C - 1}) = (b \in D ⟼ (- C) {(1 + b)}^{- C - 1})$
158	157	a1i	$⊢ (φ \land \neg C \in ℕ_{0}) \to (y \in D ⟼ (- C) {(1 + y)}^{- C - 1}) = (b \in D ⟼ (- C) {(1 + b)}^{- C - 1})$
159	144 151 158	3eqtrd	$⊢ (φ \land \neg C \in ℕ_{0}) \to \frac{d (y \in D⟼ {(1 + y)}^{- C})}{d_{ℂ} y} = (b \in D ⟼ (- C) {(1 + b)}^{- C - 1})$
160	35 159	syl5eq	$⊢ (φ \land \neg C \in ℕ_{0}) \to \frac{d (b \in D⟼ {(1 + b)}^{- C})}{d_{ℂ} b} = (b \in D ⟼ (- C) {(1 + b)}^{- C - 1})$

Metamath Proof Explorer

Theorem binomcxplemdvbinom

Proof