Theorem binomcxplemradcnv

Description: Lemma for binomcxp . By binomcxplemfrat and radcnvrat the radius of convergence of power series sum_ k e. NN0 ( ( Fk ) x. ( b ^ k ) ) is one. (Contributed by Steve Rodriguez, 22-Apr-2020)

	Ref	Expression
Hypotheses	binomcxp.a	$$⊢\phi \to A\in {ℝ}^{+}$$
	binomcxp.b	$$⊢\phi \to B\in ℝ$$
	binomcxp.lt	$$⊢\phi \to \left|B\right|<\left|A\right|$$
	binomcxp.c	$$⊢\phi \to C\in ℂ$$
	binomcxplem.f	$$⊢F=\left(j\in {\mathbb{N}}_0⟼C{C}_{𝑐}j\right)$$
	binomcxplem.s	$$⊢S=\left(b\in ℂ⟼\left(k\in {\mathbb{N}}_0⟼F\left(k\right)b^k\right)\right)$$
	binomcxplem.r	$$⊢R=sup\left(\left\{r\in ℝ|seq0\left(+,S\left(r\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)$$
Assertion	binomcxplemradcnv	$$⊢\left(\phi \wedge \neg C\in {\mathbb{N}}_0\right)\to R=1$$

Proof

Step	Hyp	Ref	Expression
1		binomcxp.a	$$⊢\phi \to A\in {ℝ}^{+}$$
2		binomcxp.b	$$⊢\phi \to B\in ℝ$$
3		binomcxp.lt	$$⊢\phi \to \left|B\right|<\left|A\right|$$
4		binomcxp.c	$$⊢\phi \to C\in ℂ$$
5		binomcxplem.f	$$⊢F=\left(j\in {\mathbb{N}}_0⟼C{C}_{𝑐}j\right)$$
6		binomcxplem.s	$$⊢S=\left(b\in ℂ⟼\left(k\in {\mathbb{N}}_0⟼F\left(k\right)b^k\right)\right)$$
7		binomcxplem.r	$$⊢R=sup\left(\left\{r\in ℝ|seq0\left(+,S\left(r\right)\right)\in \mathrm{dom}⇝\right\},{ℝ}^{*},<\right)$$
8		simpl	$$⊢\left(b=x\wedge k\in {\mathbb{N}}_0\right)\to b=x$$
9	8	oveq1d	$$⊢\left(b=x\wedge k\in {\mathbb{N}}_0\right)\to b^k=x^k$$
10	9	oveq2d	$$⊢\left(b=x\wedge k\in {\mathbb{N}}_0\right)\to F\left(k\right)b^k=F\left(k\right)x^k$$
11	10	mpteq2dva	$$⊢b=x\to \left(k\in {\mathbb{N}}_0⟼F\left(k\right)b^k\right)=\left(k\in {\mathbb{N}}_0⟼F\left(k\right)x^k\right)$$
12		fveq2	$$⊢k=y\to F\left(k\right)=F\left(y\right)$$
13		oveq2	$$⊢k=y\to x^k=x^y$$
14	12 13	oveq12d	$$⊢k=y\to F\left(k\right)x^k=F\left(y\right)x^y$$
15	14	cbvmptv	$$⊢\left(k\in {\mathbb{N}}_0⟼F\left(k\right)x^k\right)=\left(y\in {\mathbb{N}}_0⟼F\left(y\right)x^y\right)$$
16	11 15	eqtrdi	$$⊢b=x\to \left(k\in {\mathbb{N}}_0⟼F\left(k\right)b^k\right)=\left(y\in {\mathbb{N}}_0⟼F\left(y\right)x^y\right)$$
17	16	cbvmptv	$$⊢\left(b\in ℂ⟼\left(k\in {\mathbb{N}}_0⟼F\left(k\right)b^k\right)\right)=\left(x\in ℂ⟼\left(y\in {\mathbb{N}}_0⟼F\left(y\right)x^y\right)\right)$$
18	6 17	eqtri	$$⊢S=\left(x\in ℂ⟼\left(y\in {\mathbb{N}}_0⟼F\left(y\right)x^y\right)\right)$$
19	4	ad2antrr	$$⊢\left(\left(\phi \wedge \neg C\in {\mathbb{N}}_0\right)\wedge j\in {\mathbb{N}}_0\right)\to C\in ℂ$$
20		simpr	$$⊢\left(\left(\phi \wedge \neg C\in {\mathbb{N}}_0\right)\wedge j\in {\mathbb{N}}_0\right)\to j\in {\mathbb{N}}_0$$
21	19 20	bcccl	$$⊢\left(\left(\phi \wedge \neg C\in {\mathbb{N}}_0\right)\wedge j\in {\mathbb{N}}_0\right)\to C{C}_{𝑐}j\in ℂ$$
22	21 5	fmptd	$$⊢\left(\phi \wedge \neg C\in {\mathbb{N}}_0\right)\to F:{\mathbb{N}}_0⟶ℂ$$
23		fvoveq1	$$⊢k=i\to F\left(k+1\right)=F\left(i+1\right)$$
24		fveq2	$$⊢k=i\to F\left(k\right)=F\left(i\right)$$
25	23 24	oveq12d	$$⊢k=i\to \frac{F\left(k+1\right)}{F\left(k\right)}=\frac{F\left(i+1\right)}{F\left(i\right)}$$
26	25	fveq2d	$$⊢k=i\to \left|\frac{F\left(k+1\right)}{F\left(k\right)}\right|=\left|\frac{F\left(i+1\right)}{F\left(i\right)}\right|$$
27	26	cbvmptv	$$⊢\left(k\in {\mathbb{N}}_0⟼\left|\frac{F\left(k+1\right)}{F\left(k\right)}\right|\right)=\left(i\in {\mathbb{N}}_0⟼\left|\frac{F\left(i+1\right)}{F\left(i\right)}\right|\right)$$
28		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
29		0nn0	$$⊢0\in {\mathbb{N}}_0$$
30	29	a1i	$$⊢\left(\phi \wedge \neg C\in {\mathbb{N}}_0\right)\to 0\in {\mathbb{N}}_0$$
31	5	a1i	$$⊢\left(\left(\phi \wedge \neg C\in {\mathbb{N}}_0\right)\wedge i\in {\mathbb{N}}_0\right)\to F=\left(j\in {\mathbb{N}}_0⟼C{C}_{𝑐}j\right)$$
32		simpr	$$⊢\left(\left(\left(\phi \wedge \neg C\in {\mathbb{N}}_0\right)\wedge i\in {\mathbb{N}}_0\right)\wedge j=i\right)\to j=i$$
33	32	oveq2d	$$⊢\left(\left(\left(\phi \wedge \neg C\in {\mathbb{N}}_0\right)\wedge i\in {\mathbb{N}}_0\right)\wedge j=i\right)\to C{C}_{𝑐}j=C{C}_{𝑐}i$$
34		simpr	$$⊢\left(\left(\phi \wedge \neg C\in {\mathbb{N}}_0\right)\wedge i\in {\mathbb{N}}_0\right)\to i\in {\mathbb{N}}_0$$
35		ovexd	$$⊢\left(\left(\phi \wedge \neg C\in {\mathbb{N}}_0\right)\wedge i\in {\mathbb{N}}_0\right)\to C{C}_{𝑐}i\in \mathrm{V}$$
36	31 33 34 35	fvmptd	$$⊢\left(\left(\phi \wedge \neg C\in {\mathbb{N}}_0\right)\wedge i\in {\mathbb{N}}_0\right)\to F\left(i\right)=C{C}_{𝑐}i$$
37		elfznn0	$$⊢C\in \left(0\dots i-1\right)\to C\in {\mathbb{N}}_0$$
38	37	con3i	$$⊢\neg C\in {\mathbb{N}}_0\to \neg C\in \left(0\dots i-1\right)$$
39	38	ad2antlr	$$⊢\left(\left(\phi \wedge \neg C\in {\mathbb{N}}_0\right)\wedge i\in {\mathbb{N}}_0\right)\to \neg C\in \left(0\dots i-1\right)$$
40	4	adantr	$$⊢\left(\phi \wedge i\in {\mathbb{N}}_0\right)\to C\in ℂ$$
41		simpr	$$⊢\left(\phi \wedge i\in {\mathbb{N}}_0\right)\to i\in {\mathbb{N}}_0$$
42	40 41	bcc0	$$⊢\left(\phi \wedge i\in {\mathbb{N}}_0\right)\to \left(C{C}_{𝑐}i=0\leftrightarrow C\in \left(0\dots i-1\right)\right)$$
43	42	necon3abid	$$⊢\left(\phi \wedge i\in {\mathbb{N}}_0\right)\to \left(C{C}_{𝑐}i\ne 0\leftrightarrow \neg C\in \left(0\dots i-1\right)\right)$$
44	43	adantlr	$$⊢\left(\left(\phi \wedge \neg C\in {\mathbb{N}}_0\right)\wedge i\in {\mathbb{N}}_0\right)\to \left(C{C}_{𝑐}i\ne 0\leftrightarrow \neg C\in \left(0\dots i-1\right)\right)$$
45	39 44	mpbird	$$⊢\left(\left(\phi \wedge \neg C\in {\mathbb{N}}_0\right)\wedge i\in {\mathbb{N}}_0\right)\to C{C}_{𝑐}i\ne 0$$
46	36 45	eqnetrd	$$⊢\left(\left(\phi \wedge \neg C\in {\mathbb{N}}_0\right)\wedge i\in {\mathbb{N}}_0\right)\to F\left(i\right)\ne 0$$
47	1 2 3 4 5	binomcxplemfrat	$$⊢\left(\phi \wedge \neg C\in {\mathbb{N}}_0\right)\to \left(k\in {\mathbb{N}}_0⟼\left|\frac{F\left(k+1\right)}{F\left(k\right)}\right|\right)⇝1$$
48		ax-1ne0	$$⊢1\ne 0$$
49	48	a1i	$$⊢\left(\phi \wedge \neg C\in {\mathbb{N}}_0\right)\to 1\ne 0$$
50	18 22 7 27 28 30 46 47 49	radcnvrat	$$⊢\left(\phi \wedge \neg C\in {\mathbb{N}}_0\right)\to R=\frac{1}{1}$$
51		1div1e1	$$⊢\frac{1}{1}=1$$
52	50 51	eqtrdi	$$⊢\left(\phi \wedge \neg C\in {\mathbb{N}}_0\right)\to R=1$$