Metamath Proof Explorer

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 ⊢ φ → A ∈ ℝ +
binomcxp.b ⊢ φ → B ∈ ℝ
binomcxp.lt ⊢ φ → B < A
binomcxp.c ⊢ φ → C ∈ ℂ
binomcxplem.f ⊢ F = j ∈ ℕ 0 ⟼ C C 𝑐 j
binomcxplem.s ⊢ S = b ∈ ℂ ⟼ k ∈ ℕ 0 ⟼ F ⁡ k ⁢ b k
binomcxplem.r ⊢ R = sup r ∈ ℝ | seq 0 + S ⁡ r ∈ dom ⁡ ⇝ ℝ * <
binomcxplem.e ⊢ E = b ∈ ℂ ⟼ k ∈ ℕ ⟼ k ⁢ F ⁡ k ⁢ b k − 1
binomcxplem.d ⊢ D = abs -1 0 R
Assertion binomcxplemcvg ⊢ φ ∧ J ∈ D → seq 0 + S ⁡ J ∈ dom ⁡ ⇝ ∧ seq 1 + E ⁡ J ∈ dom ⁡ ⇝

Proof

Step Hyp Ref Expression
1 binomcxp.a ⊢ φ → A ∈ ℝ +
2 binomcxp.b ⊢ φ → B ∈ ℝ
3 binomcxp.lt ⊢ φ → B < A
4 binomcxp.c ⊢ φ → C ∈ ℂ
5 binomcxplem.f ⊢ F = j ∈ ℕ 0 ⟼ C C 𝑐 j
6 binomcxplem.s ⊢ S = b ∈ ℂ ⟼ k ∈ ℕ 0 ⟼ F ⁡ k ⁢ b k
7 binomcxplem.r ⊢ R = sup r ∈ ℝ | seq 0 + S ⁡ r ∈ dom ⁡ ⇝ ℝ * <
8 binomcxplem.e ⊢ E = b ∈ ℂ ⟼ k ∈ ℕ ⟼ k ⁢ F ⁡ k ⁢ b k − 1
9 binomcxplem.d ⊢ D = abs -1 0 R
10 4 adantr ⊢ φ ∧ j ∈ ℕ 0 → C ∈ ℂ
11 simpr ⊢ φ ∧ j ∈ ℕ 0 → j ∈ ℕ 0
12 10 11 bcccl ⊢ φ ∧ j ∈ ℕ 0 → C C 𝑐 j ∈ ℂ
13 12 5 fmptd ⊢ φ → F : ℕ 0 ⟶ ℂ
14 13 adantr ⊢ φ ∧ J ∈ D → F : ℕ 0 ⟶ ℂ
15 9 eleq2i ⊢ J ∈ D ↔ J ∈ abs -1 0 R
16 absf ⊢ abs : ℂ ⟶ ℝ
17 ffn ⊢ abs : ℂ ⟶ ℝ → abs Fn ℂ
18 elpreima ⊢ abs Fn ℂ → J ∈ abs -1 0 R ↔ J ∈ ℂ ∧ J ∈ 0 R
19 16 17 18 mp2b ⊢ J ∈ abs -1 0 R ↔ J ∈ ℂ ∧ J ∈ 0 R
20 15 19 bitri ⊢ J ∈ D ↔ J ∈ ℂ ∧ J ∈ 0 R
21 20 simplbi ⊢ J ∈ D → J ∈ ℂ
22 21 adantl ⊢ φ ∧ J ∈ D → J ∈ ℂ
23 20 simprbi ⊢ J ∈ D → J ∈ 0 R
24 0re ⊢ 0 ∈ ℝ
25 ssrab2 ⊢ r ∈ ℝ | seq 0 + S ⁡ r ∈ dom ⁡ ⇝ ⊆ ℝ
26 ressxr ⊢ ℝ ⊆ ℝ *
27 25 26 sstri ⊢ r ∈ ℝ | seq 0 + S ⁡ r ∈ dom ⁡ ⇝ ⊆ ℝ *
28 supxrcl ⊢ r ∈ ℝ | seq 0 + S ⁡ r ∈ dom ⁡ ⇝ ⊆ ℝ * → sup r ∈ ℝ | seq 0 + S ⁡ r ∈ dom ⁡ ⇝ ℝ * < ∈ ℝ *
29 27 28 ax-mp ⊢ sup r ∈ ℝ | seq 0 + S ⁡ r ∈ dom ⁡ ⇝ ℝ * < ∈ ℝ *
30 7 29 eqeltri ⊢ R ∈ ℝ *
31 elico2 ⊢ 0 ∈ ℝ ∧ R ∈ ℝ * → J ∈ 0 R ↔ J ∈ ℝ ∧ 0 ≤ J ∧ J < R
32 24 30 31 mp2an ⊢ J ∈ 0 R ↔ J ∈ ℝ ∧ 0 ≤ J ∧ J < R
33 32 simp3bi ⊢ J ∈ 0 R → J < R
34 23 33 syl ⊢ J ∈ D → J < R
35 34 adantl ⊢ φ ∧ J ∈ D → J < R
36 6 14 7 22 35 radcnvlt2 ⊢ φ ∧ J ∈ D → seq 0 + S ⁡ J ∈ dom ⁡ ⇝
37 8 a1i ⊢ φ ∧ J ∈ ℂ → E = b ∈ ℂ ⟼ k ∈ ℕ ⟼ k ⁢ F ⁡ k ⁢ b k − 1
38 simplr ⊢ φ ∧ J ∈ ℂ ∧ b = J ∧ k ∈ ℕ → b = J
39 38 oveq1d ⊢ φ ∧ J ∈ ℂ ∧ b = J ∧ k ∈ ℕ → b k − 1 = J k − 1
40 39 oveq2d ⊢ φ ∧ J ∈ ℂ ∧ b = J ∧ k ∈ ℕ → k ⁢ F ⁡ k ⁢ b k − 1 = k ⁢ F ⁡ k ⁢ J k − 1
41 40 mpteq2dva ⊢ φ ∧ J ∈ ℂ ∧ b = J → k ∈ ℕ ⟼ k ⁢ F ⁡ k ⁢ b k − 1 = k ∈ ℕ ⟼ k ⁢ F ⁡ k ⁢ J k − 1
42 simpr ⊢ φ ∧ J ∈ ℂ → J ∈ ℂ
43 nnex ⊢ ℕ ∈ V
44 43 mptex ⊢ k ∈ ℕ ⟼ k ⁢ F ⁡ k ⁢ J k − 1 ∈ V
45 44 a1i ⊢ φ ∧ J ∈ ℂ → k ∈ ℕ ⟼ k ⁢ F ⁡ k ⁢ J k − 1 ∈ V
46 37 41 42 45 fvmptd ⊢ φ ∧ J ∈ ℂ → E ⁡ J = k ∈ ℕ ⟼ k ⁢ F ⁡ k ⁢ J k − 1
47 21 46 sylan2 ⊢ φ ∧ J ∈ D → E ⁡ J = k ∈ ℕ ⟼ k ⁢ F ⁡ k ⁢ J k − 1
48 47 seqeq3d ⊢ φ ∧ J ∈ D → seq 1 + E ⁡ J = seq 1 + k ∈ ℕ ⟼ k ⁢ F ⁡ k ⁢ J k − 1
49 eqid ⊢ k ∈ ℕ ⟼ k ⁢ F ⁡ k ⁢ J k − 1 = k ∈ ℕ ⟼ k ⁢ F ⁡ k ⁢ J k − 1
50 6 7 49 14 22 35 dvradcnv2 ⊢ φ ∧ J ∈ D → seq 1 + k ∈ ℕ ⟼ k ⁢ F ⁡ k ⁢ J k − 1 ∈ dom ⁡ ⇝
51 48 50 eqeltrd ⊢ φ ∧ J ∈ D → seq 1 + E ⁡ J ∈ dom ⁡ ⇝
52 36 51 jca ⊢ φ ∧ J ∈ D → seq 0 + S ⁡ J ∈ dom ⁡ ⇝ ∧ seq 1 + E ⁡ J ∈ dom ⁡ ⇝