Theorem 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	⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
	binomcxp.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	binomcxp.lt	⊢ ( 𝜑 → ( abs ‘ 𝐵 ) < ( abs ‘ 𝐴 ) )
	binomcxp.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
	binomcxplem.f	⊢ 𝐹 = ( 𝑗 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑗 ) )
	binomcxplem.s	⊢ 𝑆 = ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑏 ↑ 𝑘 ) ) ) )
	binomcxplem.r	⊢ 𝑅 = sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑆 ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < )
	binomcxplem.e	⊢ 𝐸 = ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ ↦ ( ( 𝑘 · ( 𝐹 ‘ 𝑘 ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) ) )
	binomcxplem.d	⊢ 𝐷 = ( ◡ abs “ ( 0 [,) 𝑅 ) )
Assertion	binomcxplemcvg	⊢ ( ( 𝜑 ∧ 𝐽 ∈ 𝐷 ) → ( seq 0 ( + , ( 𝑆 ‘ 𝐽 ) ) ∈ dom ⇝ ∧ seq 1 ( + , ( 𝐸 ‘ 𝐽 ) ) ∈ dom ⇝ ) )

Proof

Step	Hyp	Ref	Expression
1		binomcxp.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
2		binomcxp.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		binomcxp.lt	⊢ ( 𝜑 → ( abs ‘ 𝐵 ) < ( abs ‘ 𝐴 ) )
4		binomcxp.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
5		binomcxplem.f	⊢ 𝐹 = ( 𝑗 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑗 ) )
6		binomcxplem.s	⊢ 𝑆 = ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑏 ↑ 𝑘 ) ) ) )
7		binomcxplem.r	⊢ 𝑅 = sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑆 ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < )
8		binomcxplem.e	⊢ 𝐸 = ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ ↦ ( ( 𝑘 · ( 𝐹 ‘ 𝑘 ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) ) )
9		binomcxplem.d	⊢ 𝐷 = ( ◡ abs “ ( 0 [,) 𝑅 ) )
10	4	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → 𝐶 ∈ ℂ )
11		simpr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → 𝑗 ∈ ℕ0 )
12	10 11	bcccl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 𝐶 C𝑐 𝑗 ) ∈ ℂ )
13	12 5	fmptd	⊢ ( 𝜑 → 𝐹 : ℕ0 ⟶ ℂ )
14	13	adantr	⊢ ( ( 𝜑 ∧ 𝐽 ∈ 𝐷 ) → 𝐹 : ℕ0 ⟶ ℂ )
15	9	eleq2i	⊢ ( 𝐽 ∈ 𝐷 ↔ 𝐽 ∈ ( ◡ abs “ ( 0 [,) 𝑅 ) ) )
16		absf	⊢ abs : ℂ ⟶ ℝ
17		ffn	⊢ ( abs : ℂ ⟶ ℝ → abs Fn ℂ )
18		elpreima	⊢ ( abs Fn ℂ → ( 𝐽 ∈ ( ◡ abs “ ( 0 [,) 𝑅 ) ) ↔ ( 𝐽 ∈ ℂ ∧ ( abs ‘ 𝐽 ) ∈ ( 0 [,) 𝑅 ) ) ) )
19	16 17 18	mp2b	⊢ ( 𝐽 ∈ ( ◡ abs “ ( 0 [,) 𝑅 ) ) ↔ ( 𝐽 ∈ ℂ ∧ ( abs ‘ 𝐽 ) ∈ ( 0 [,) 𝑅 ) ) )
20	15 19	bitri	⊢ ( 𝐽 ∈ 𝐷 ↔ ( 𝐽 ∈ ℂ ∧ ( abs ‘ 𝐽 ) ∈ ( 0 [,) 𝑅 ) ) )
21	20	simplbi	⊢ ( 𝐽 ∈ 𝐷 → 𝐽 ∈ ℂ )
22	21	adantl	⊢ ( ( 𝜑 ∧ 𝐽 ∈ 𝐷 ) → 𝐽 ∈ ℂ )
23	20	simprbi	⊢ ( 𝐽 ∈ 𝐷 → ( abs ‘ 𝐽 ) ∈ ( 0 [,) 𝑅 ) )
24		0re	⊢ 0 ∈ ℝ
25		ssrab2	⊢ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑆 ‘ 𝑟 ) ) ∈ dom ⇝ } ⊆ ℝ
26		ressxr	⊢ ℝ ⊆ ℝ*
27	25 26	sstri	⊢ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑆 ‘ 𝑟 ) ) ∈ dom ⇝ } ⊆ ℝ*
28		supxrcl	⊢ ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑆 ‘ 𝑟 ) ) ∈ dom ⇝ } ⊆ ℝ* → sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑆 ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ℝ* )
29	27 28	ax-mp	⊢ sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑆 ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ℝ*
30	7 29	eqeltri	⊢ 𝑅 ∈ ℝ*
31		elico2	⊢ ( ( 0 ∈ ℝ ∧ 𝑅 ∈ ℝ* ) → ( ( abs ‘ 𝐽 ) ∈ ( 0 [,) 𝑅 ) ↔ ( ( abs ‘ 𝐽 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝐽 ) ∧ ( abs ‘ 𝐽 ) < 𝑅 ) ) )
32	24 30 31	mp2an	⊢ ( ( abs ‘ 𝐽 ) ∈ ( 0 [,) 𝑅 ) ↔ ( ( abs ‘ 𝐽 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝐽 ) ∧ ( abs ‘ 𝐽 ) < 𝑅 ) )
33	32	simp3bi	⊢ ( ( abs ‘ 𝐽 ) ∈ ( 0 [,) 𝑅 ) → ( abs ‘ 𝐽 ) < 𝑅 )
34	23 33	syl	⊢ ( 𝐽 ∈ 𝐷 → ( abs ‘ 𝐽 ) < 𝑅 )
35	34	adantl	⊢ ( ( 𝜑 ∧ 𝐽 ∈ 𝐷 ) → ( abs ‘ 𝐽 ) < 𝑅 )
36	6 14 7 22 35	radcnvlt2	⊢ ( ( 𝜑 ∧ 𝐽 ∈ 𝐷 ) → seq 0 ( + , ( 𝑆 ‘ 𝐽 ) ) ∈ dom ⇝ )
37	8	a1i	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℂ ) → 𝐸 = ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ ↦ ( ( 𝑘 · ( 𝐹 ‘ 𝑘 ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) ) ) )
38		simplr	⊢ ( ( ( ( 𝜑 ∧ 𝐽 ∈ ℂ ) ∧ 𝑏 = 𝐽 ) ∧ 𝑘 ∈ ℕ ) → 𝑏 = 𝐽 )
39	38	oveq1d	⊢ ( ( ( ( 𝜑 ∧ 𝐽 ∈ ℂ ) ∧ 𝑏 = 𝐽 ) ∧ 𝑘 ∈ ℕ ) → ( 𝑏 ↑ ( 𝑘 − 1 ) ) = ( 𝐽 ↑ ( 𝑘 − 1 ) ) )
40	39	oveq2d	⊢ ( ( ( ( 𝜑 ∧ 𝐽 ∈ ℂ ) ∧ 𝑏 = 𝐽 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑘 · ( 𝐹 ‘ 𝑘 ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) = ( ( 𝑘 · ( 𝐹 ‘ 𝑘 ) ) · ( 𝐽 ↑ ( 𝑘 − 1 ) ) ) )
41	40	mpteq2dva	⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℂ ) ∧ 𝑏 = 𝐽 ) → ( 𝑘 ∈ ℕ ↦ ( ( 𝑘 · ( 𝐹 ‘ 𝑘 ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) ) = ( 𝑘 ∈ ℕ ↦ ( ( 𝑘 · ( 𝐹 ‘ 𝑘 ) ) · ( 𝐽 ↑ ( 𝑘 − 1 ) ) ) ) )
42		simpr	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℂ ) → 𝐽 ∈ ℂ )
43		nnex	⊢ ℕ ∈ V
44	43	mptex	⊢ ( 𝑘 ∈ ℕ ↦ ( ( 𝑘 · ( 𝐹 ‘ 𝑘 ) ) · ( 𝐽 ↑ ( 𝑘 − 1 ) ) ) ) ∈ V
45	44	a1i	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℂ ) → ( 𝑘 ∈ ℕ ↦ ( ( 𝑘 · ( 𝐹 ‘ 𝑘 ) ) · ( 𝐽 ↑ ( 𝑘 − 1 ) ) ) ) ∈ V )
46	37 41 42 45	fvmptd	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℂ ) → ( 𝐸 ‘ 𝐽 ) = ( 𝑘 ∈ ℕ ↦ ( ( 𝑘 · ( 𝐹 ‘ 𝑘 ) ) · ( 𝐽 ↑ ( 𝑘 − 1 ) ) ) ) )
47	21 46	sylan2	⊢ ( ( 𝜑 ∧ 𝐽 ∈ 𝐷 ) → ( 𝐸 ‘ 𝐽 ) = ( 𝑘 ∈ ℕ ↦ ( ( 𝑘 · ( 𝐹 ‘ 𝑘 ) ) · ( 𝐽 ↑ ( 𝑘 − 1 ) ) ) ) )
48	47	seqeq3d	⊢ ( ( 𝜑 ∧ 𝐽 ∈ 𝐷 ) → seq 1 ( + , ( 𝐸 ‘ 𝐽 ) ) = seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( ( 𝑘 · ( 𝐹 ‘ 𝑘 ) ) · ( 𝐽 ↑ ( 𝑘 − 1 ) ) ) ) ) )
49		eqid	⊢ ( 𝑘 ∈ ℕ ↦ ( ( 𝑘 · ( 𝐹 ‘ 𝑘 ) ) · ( 𝐽 ↑ ( 𝑘 − 1 ) ) ) ) = ( 𝑘 ∈ ℕ ↦ ( ( 𝑘 · ( 𝐹 ‘ 𝑘 ) ) · ( 𝐽 ↑ ( 𝑘 − 1 ) ) ) )
50	6 7 49 14 22 35	dvradcnv2	⊢ ( ( 𝜑 ∧ 𝐽 ∈ 𝐷 ) → seq 1 ( + , ( 𝑘 ∈ ℕ ↦ ( ( 𝑘 · ( 𝐹 ‘ 𝑘 ) ) · ( 𝐽 ↑ ( 𝑘 − 1 ) ) ) ) ) ∈ dom ⇝ )
51	48 50	eqeltrd	⊢ ( ( 𝜑 ∧ 𝐽 ∈ 𝐷 ) → seq 1 ( + , ( 𝐸 ‘ 𝐽 ) ) ∈ dom ⇝ )
52	36 51	jca	⊢ ( ( 𝜑 ∧ 𝐽 ∈ 𝐷 ) → ( seq 0 ( + , ( 𝑆 ‘ 𝐽 ) ) ∈ dom ⇝ ∧ seq 1 ( + , ( 𝐸 ‘ 𝐽 ) ) ∈ dom ⇝ ) )