binomcxplemcvg

Description: Lemma for binomcxp . The sum in binomcxplemnn0 and its derivative (see the next theorem, binomcxplemdvsum ) converge, as long as their base J is within the disk of convergence. 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)]$
Assertion	binomcxplemcvg	$⊢ (φ \land J \in D) \to (seq 0 (+ S (J)) \in dom ⇝ \land seq 1 (+ E (J)) \in dom ⇝)$

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	4	adantr	$⊢ (φ \land j \in ℕ_{0}) \to C \in ℂ$
11		simpr	$⊢ (φ \land j \in ℕ_{0}) \to j \in ℕ_{0}$
12	10 11	bcccl	$⊢ (φ \land j \in ℕ_{0}) \to C C_{𝑐} j \in ℂ$
13	12 5	fmptd	$⊢ φ \to F : ℕ_{0} ⟶ ℂ$
14	13	adantr	$⊢ (φ \land J \in D) \to F : ℕ_{0} ⟶ ℂ$
15	9	eleq2i	$⊢ J \in D \leftrightarrow J \in {abs}^{-1} [[0, R)]$
16		absf	$⊢ abs : ℂ ⟶ ℝ$
17		ffn	$⊢ abs : ℂ ⟶ ℝ \to abs Fn ℂ$
18		elpreima	$⊢ abs Fn ℂ \to (J \in {abs}^{-1} [[0, R)] \leftrightarrow (J \in ℂ \land \|J\| \in [0, R)))$
19	16 17 18	mp2b	$⊢ J \in {abs}^{-1} [[0, R)] \leftrightarrow (J \in ℂ \land \|J\| \in [0, R))$
20	15 19	bitri	$⊢ J \in D \leftrightarrow (J \in ℂ \land \|J\| \in [0, R))$
21	20	simplbi	$⊢ J \in D \to J \in ℂ$
22	21	adantl	$⊢ (φ \land J \in D) \to J \in ℂ$
23	20	simprbi	$⊢ J \in D \to \|J\| \in [0, R)$
24		0re	$⊢ 0 \in ℝ$
25		ssrab2	$⊢ \{r \in ℝ \| seq 0 (+ S (r)) \in dom ⇝\} \subseteq ℝ$
26		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
27	25 26	sstri	$⊢ \{r \in ℝ \| seq 0 (+ S (r)) \in dom ⇝\} \subseteq ℝ^{*}$
28		supxrcl	$⊢ \{r \in ℝ \| seq 0 (+ S (r)) \in dom ⇝\} \subseteq ℝ^{} \to sup (\{r \in ℝ \| seq 0 (+ S (r)) \in dom ⇝\} ℝ^{} <) \in ℝ^{*}$
29	27 28	ax-mp	$⊢ sup (\{r \in ℝ \| seq 0 (+ S (r)) \in dom ⇝\} ℝ^{} <) \in ℝ^{}$
30	7 29	eqeltri	$⊢ R \in ℝ^{*}$
31		elico2	$⊢ (0 \in ℝ \land R \in ℝ^{*}) \to (\|J\| \in [0, R) \leftrightarrow (\|J\| \in ℝ \land 0 \leq \|J\| \land \|J\| < R))$
32	24 30 31	mp2an	$⊢ \|J\| \in [0, R) \leftrightarrow (\|J\| \in ℝ \land 0 \leq \|J\| \land \|J\| < R)$
33	32	simp3bi	$⊢ \|J\| \in [0, R) \to \|J\| < R$
34	23 33	syl	$⊢ J \in D \to \|J\| < R$
35	34	adantl	$⊢ (φ \land J \in D) \to \|J\| < R$
36	6 14 7 22 35	radcnvlt2	$⊢ (φ \land J \in D) \to seq 0 (+ S (J)) \in dom ⇝$
37	8	a1i	$⊢ (φ \land J \in ℂ) \to E = (b \in ℂ ⟼ (k \in ℕ ⟼ k F (k) b^{k - 1}))$
38		simplr	$⊢ (((φ \land J \in ℂ) \land b = J) \land k \in ℕ) \to b = J$
39	38	oveq1d	$⊢ (((φ \land J \in ℂ) \land b = J) \land k \in ℕ) \to b^{k - 1} = J^{k - 1}$
40	39	oveq2d	$⊢ (((φ \land J \in ℂ) \land b = J) \land k \in ℕ) \to k F (k) b^{k - 1} = k F (k) J^{k - 1}$
41	40	mpteq2dva	$⊢ ((φ \land J \in ℂ) \land b = J) \to (k \in ℕ ⟼ k F (k) b^{k - 1}) = (k \in ℕ ⟼ k F (k) J^{k - 1})$
42		simpr	$⊢ (φ \land J \in ℂ) \to J \in ℂ$
43		nnex	$⊢ ℕ \in V$
44	43	mptex	$⊢ (k \in ℕ ⟼ k F (k) J^{k - 1}) \in V$
45	44	a1i	$⊢ (φ \land J \in ℂ) \to (k \in ℕ ⟼ k F (k) J^{k - 1}) \in V$
46	37 41 42 45	fvmptd	$⊢ (φ \land J \in ℂ) \to E (J) = (k \in ℕ ⟼ k F (k) J^{k - 1})$
47	21 46	sylan2	$⊢ (φ \land J \in D) \to E (J) = (k \in ℕ ⟼ k F (k) J^{k - 1})$
48	47	seqeq3d	$⊢ (φ \land J \in D) \to seq 1 (+ E (J)) = seq 1 (+ (k \in ℕ ⟼ k F (k) J^{k - 1}))$
49		eqid	$⊢ (k \in ℕ ⟼ k F (k) J^{k - 1}) = (k \in ℕ ⟼ k F (k) J^{k - 1})$
50	6 7 49 14 22 35	dvradcnv2	$⊢ (φ \land J \in D) \to seq 1 (+ (k \in ℕ ⟼ k F (k) J^{k - 1})) \in dom ⇝$
51	48 50	eqeltrd	$⊢ (φ \land J \in D) \to seq 1 (+ E (J)) \in dom ⇝$
52	36 51	jca	$⊢ (φ \land J \in D) \to (seq 0 (+ S (J)) \in dom ⇝ \land seq 1 (+ E (J)) \in dom ⇝)$

Metamath Proof Explorer

Theorem binomcxplemcvg

Proof