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

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		simpl	⊢ ( ( 𝑏 = 𝑥 ∧ 𝑘 ∈ ℕ0 ) → 𝑏 = 𝑥 )
9	8	oveq1d	⊢ ( ( 𝑏 = 𝑥 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑏 ↑ 𝑘 ) = ( 𝑥 ↑ 𝑘 ) )
10	9	oveq2d	⊢ ( ( 𝑏 = 𝑥 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐹 ‘ 𝑘 ) · ( 𝑏 ↑ 𝑘 ) ) = ( ( 𝐹 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) )
11	10	mpteq2dva	⊢ ( 𝑏 = 𝑥 → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑏 ↑ 𝑘 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) ) )
12		fveq2	⊢ ( 𝑘 = 𝑦 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑦 ) )
13		oveq2	⊢ ( 𝑘 = 𝑦 → ( 𝑥 ↑ 𝑘 ) = ( 𝑥 ↑ 𝑦 ) )
14	12 13	oveq12d	⊢ ( 𝑘 = 𝑦 → ( ( 𝐹 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) = ( ( 𝐹 ‘ 𝑦 ) · ( 𝑥 ↑ 𝑦 ) ) )
15	14	cbvmptv	⊢ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑥 ↑ 𝑘 ) ) ) = ( 𝑦 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑦 ) · ( 𝑥 ↑ 𝑦 ) ) )
16	11 15	eqtrdi	⊢ ( 𝑏 = 𝑥 → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑏 ↑ 𝑘 ) ) ) = ( 𝑦 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑦 ) · ( 𝑥 ↑ 𝑦 ) ) ) )
17	16	cbvmptv	⊢ ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑏 ↑ 𝑘 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑦 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑦 ) · ( 𝑥 ↑ 𝑦 ) ) ) )
18	6 17	eqtri	⊢ 𝑆 = ( 𝑥 ∈ ℂ ↦ ( 𝑦 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑦 ) · ( 𝑥 ↑ 𝑦 ) ) ) )
19	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑗 ∈ ℕ0 ) → 𝐶 ∈ ℂ )
20		simpr	⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑗 ∈ ℕ0 ) → 𝑗 ∈ ℕ0 )
21	19 20	bcccl	⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑗 ∈ ℕ0 ) → ( 𝐶 C𝑐 𝑗 ) ∈ ℂ )
22	21 5	fmptd	⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → 𝐹 : ℕ0 ⟶ ℂ )
23		fvoveq1	⊢ ( 𝑘 = 𝑖 → ( 𝐹 ‘ ( 𝑘 + 1 ) ) = ( 𝐹 ‘ ( 𝑖 + 1 ) ) )
24		fveq2	⊢ ( 𝑘 = 𝑖 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑖 ) )
25	23 24	oveq12d	⊢ ( 𝑘 = 𝑖 → ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹 ‘ 𝑘 ) ) = ( ( 𝐹 ‘ ( 𝑖 + 1 ) ) / ( 𝐹 ‘ 𝑖 ) ) )
26	25	fveq2d	⊢ ( 𝑘 = 𝑖 → ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹 ‘ 𝑘 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ ( 𝑖 + 1 ) ) / ( 𝐹 ‘ 𝑖 ) ) ) )
27	26	cbvmptv	⊢ ( 𝑘 ∈ ℕ0 ↦ ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹 ‘ 𝑘 ) ) ) ) = ( 𝑖 ∈ ℕ0 ↦ ( abs ‘ ( ( 𝐹 ‘ ( 𝑖 + 1 ) ) / ( 𝐹 ‘ 𝑖 ) ) ) )
28		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
29		0nn0	⊢ 0 ∈ ℕ0
30	29	a1i	⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → 0 ∈ ℕ0 )
31	5	a1i	⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑖 ∈ ℕ0 ) → 𝐹 = ( 𝑗 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑗 ) ) )
32		simpr	⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑗 = 𝑖 ) → 𝑗 = 𝑖 )
33	32	oveq2d	⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑗 = 𝑖 ) → ( 𝐶 C𝑐 𝑗 ) = ( 𝐶 C𝑐 𝑖 ) )
34		simpr	⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑖 ∈ ℕ0 ) → 𝑖 ∈ ℕ0 )
35		ovexd	⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑖 ∈ ℕ0 ) → ( 𝐶 C𝑐 𝑖 ) ∈ V )
36	31 33 34 35	fvmptd	⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑖 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑖 ) = ( 𝐶 C𝑐 𝑖 ) )
37		elfznn0	⊢ ( 𝐶 ∈ ( 0 ... ( 𝑖 − 1 ) ) → 𝐶 ∈ ℕ0 )
38	37	con3i	⊢ ( ¬ 𝐶 ∈ ℕ0 → ¬ 𝐶 ∈ ( 0 ... ( 𝑖 − 1 ) ) )
39	38	ad2antlr	⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑖 ∈ ℕ0 ) → ¬ 𝐶 ∈ ( 0 ... ( 𝑖 − 1 ) ) )
40	4	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → 𝐶 ∈ ℂ )
41		simpr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → 𝑖 ∈ ℕ0 )
42	40 41	bcc0	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝐶 C𝑐 𝑖 ) = 0 ↔ 𝐶 ∈ ( 0 ... ( 𝑖 − 1 ) ) ) )
43	42	necon3abid	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝐶 C𝑐 𝑖 ) ≠ 0 ↔ ¬ 𝐶 ∈ ( 0 ... ( 𝑖 − 1 ) ) ) )
44	43	adantlr	⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝐶 C𝑐 𝑖 ) ≠ 0 ↔ ¬ 𝐶 ∈ ( 0 ... ( 𝑖 − 1 ) ) ) )
45	39 44	mpbird	⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑖 ∈ ℕ0 ) → ( 𝐶 C𝑐 𝑖 ) ≠ 0 )
46	36 45	eqnetrd	⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑖 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑖 ) ≠ 0 )
47	1 2 3 4 5	binomcxplemfrat	⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( 𝑘 ∈ ℕ0 ↦ ( abs ‘ ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) / ( 𝐹 ‘ 𝑘 ) ) ) ) ⇝ 1 )
48		ax-1ne0	⊢ 1 ≠ 0
49	48	a1i	⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → 1 ≠ 0 )
50	18 22 7 27 28 30 46 47 49	radcnvrat	⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → 𝑅 = ( 1 / 1 ) )
51		1div1e1	⊢ ( 1 / 1 ) = 1
52	50 51	eqtrdi	⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → 𝑅 = 1 )