Metamath Proof Explorer


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 )