Mathbox for Steve Rodriguez < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  binomcxplemdvsum Structured version   Visualization version   GIF version

Theorem binomcxplemdvsum 41102
 Description: Lemma for binomcxp 41104. The derivative of the generalized sum in binomcxplemnn0 41096. Part of remark "This convergence allows us to apply term-by-term differentiation..." in the Wikibooks proof. (Contributed by Steve Rodriguez, 22-Apr-2020.)
Hypotheses
Ref Expression
binomcxp.a (𝜑𝐴 ∈ ℝ+)
binomcxp.b (𝜑𝐵 ∈ ℝ)
binomcxp.lt (𝜑 → (abs‘𝐵) < (abs‘𝐴))
binomcxp.c (𝜑𝐶 ∈ ℂ)
binomcxplem.f 𝐹 = (𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗))
binomcxplem.s 𝑆 = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑏𝑘))))
binomcxplem.r 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑆𝑟)) ∈ dom ⇝ }, ℝ*, < )
binomcxplem.e 𝐸 = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹𝑘)) · (𝑏↑(𝑘 − 1)))))
binomcxplem.d 𝐷 = (abs “ (0[,)𝑅))
binomcxplem.p 𝑃 = (𝑏𝐷 ↦ Σ𝑘 ∈ ℕ0 ((𝑆𝑏)‘𝑘))
Assertion
Ref Expression
binomcxplemdvsum (𝜑 → (ℂ D 𝑃) = (𝑏𝐷 ↦ Σ𝑘 ∈ ℕ ((𝐸𝑏)‘𝑘)))
Distinct variable groups:   𝑘,𝑏,𝐹   𝜑,𝑏,𝑘   𝑟,𝑏,𝑘,𝐹   𝑗,𝑘,𝜑   𝐶,𝑗
Allowed substitution hints:   𝜑(𝑟)   𝐴(𝑗,𝑘,𝑟,𝑏)   𝐵(𝑗,𝑘,𝑟,𝑏)   𝐶(𝑘,𝑟,𝑏)   𝐷(𝑗,𝑘,𝑟,𝑏)   𝑃(𝑗,𝑘,𝑟,𝑏)   𝑅(𝑗,𝑘,𝑟,𝑏)   𝑆(𝑗,𝑘,𝑟,𝑏)   𝐸(𝑗,𝑘,𝑟,𝑏)   𝐹(𝑗)

Proof of Theorem binomcxplemdvsum
Dummy variables 𝑚 𝑛 𝑥 𝑦 𝑧 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 binomcxplem.s . . . 4 𝑆 = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑏𝑘))))
2 binomcxplem.p . . . . 5 𝑃 = (𝑏𝐷 ↦ Σ𝑘 ∈ ℕ0 ((𝑆𝑏)‘𝑘))
3 binomcxplem.d . . . . . . 7 𝐷 = (abs “ (0[,)𝑅))
4 nfcv 2955 . . . . . . . 8 𝑏abs
5 nfcv 2955 . . . . . . . . 9 𝑏0
6 nfcv 2955 . . . . . . . . 9 𝑏[,)
7 binomcxplem.r . . . . . . . . . 10 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑆𝑟)) ∈ dom ⇝ }, ℝ*, < )
8 nfcv 2955 . . . . . . . . . . . . . 14 𝑏 +
9 nfmpt1 5129 . . . . . . . . . . . . . . . 16 𝑏(𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑏𝑘))))
101, 9nfcxfr 2953 . . . . . . . . . . . . . . 15 𝑏𝑆
11 nfcv 2955 . . . . . . . . . . . . . . 15 𝑏𝑟
1210, 11nffv 6656 . . . . . . . . . . . . . 14 𝑏(𝑆𝑟)
135, 8, 12nfseq 13377 . . . . . . . . . . . . 13 𝑏seq0( + , (𝑆𝑟))
1413nfel1 2971 . . . . . . . . . . . 12 𝑏seq0( + , (𝑆𝑟)) ∈ dom ⇝
15 nfcv 2955 . . . . . . . . . . . 12 𝑏
1614, 15nfrabw 3338 . . . . . . . . . . 11 𝑏{𝑟 ∈ ℝ ∣ seq0( + , (𝑆𝑟)) ∈ dom ⇝ }
17 nfcv 2955 . . . . . . . . . . 11 𝑏*
18 nfcv 2955 . . . . . . . . . . 11 𝑏 <
1916, 17, 18nfsup 8902 . . . . . . . . . 10 𝑏sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑆𝑟)) ∈ dom ⇝ }, ℝ*, < )
207, 19nfcxfr 2953 . . . . . . . . 9 𝑏𝑅
215, 6, 20nfov 7166 . . . . . . . 8 𝑏(0[,)𝑅)
224, 21nfima 5905 . . . . . . 7 𝑏(abs “ (0[,)𝑅))
233, 22nfcxfr 2953 . . . . . 6 𝑏𝐷
24 nfcv 2955 . . . . . 6 𝑦𝐷
25 nfcv 2955 . . . . . 6 𝑦Σ𝑘 ∈ ℕ0 ((𝑆𝑏)‘𝑘)
26 nfcv 2955 . . . . . . 7 𝑏0
27 nfcv 2955 . . . . . . . . 9 𝑏𝑦
2810, 27nffv 6656 . . . . . . . 8 𝑏(𝑆𝑦)
29 nfcv 2955 . . . . . . . 8 𝑏𝑚
3028, 29nffv 6656 . . . . . . 7 𝑏((𝑆𝑦)‘𝑚)
3126, 30nfsum 15042 . . . . . 6 𝑏Σ𝑚 ∈ ℕ0 ((𝑆𝑦)‘𝑚)
32 simpl 486 . . . . . . . . . 10 ((𝑏 = 𝑦𝑘 ∈ ℕ0) → 𝑏 = 𝑦)
3332fveq2d 6650 . . . . . . . . 9 ((𝑏 = 𝑦𝑘 ∈ ℕ0) → (𝑆𝑏) = (𝑆𝑦))
3433fveq1d 6648 . . . . . . . 8 ((𝑏 = 𝑦𝑘 ∈ ℕ0) → ((𝑆𝑏)‘𝑘) = ((𝑆𝑦)‘𝑘))
3534sumeq2dv 15055 . . . . . . 7 (𝑏 = 𝑦 → Σ𝑘 ∈ ℕ0 ((𝑆𝑏)‘𝑘) = Σ𝑘 ∈ ℕ0 ((𝑆𝑦)‘𝑘))
36 nfcv 2955 . . . . . . . 8 𝑚((𝑆𝑦)‘𝑘)
37 nfcv 2955 . . . . . . . . . . . 12 𝑘
38 nfmpt1 5129 . . . . . . . . . . . 12 𝑘(𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑏𝑘)))
3937, 38nfmpt 5128 . . . . . . . . . . 11 𝑘(𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑏𝑘))))
401, 39nfcxfr 2953 . . . . . . . . . 10 𝑘𝑆
41 nfcv 2955 . . . . . . . . . 10 𝑘𝑦
4240, 41nffv 6656 . . . . . . . . 9 𝑘(𝑆𝑦)
43 nfcv 2955 . . . . . . . . 9 𝑘𝑚
4442, 43nffv 6656 . . . . . . . 8 𝑘((𝑆𝑦)‘𝑚)
45 fveq2 6646 . . . . . . . 8 (𝑘 = 𝑚 → ((𝑆𝑦)‘𝑘) = ((𝑆𝑦)‘𝑚))
4636, 44, 45cbvsumi 15049 . . . . . . 7 Σ𝑘 ∈ ℕ0 ((𝑆𝑦)‘𝑘) = Σ𝑚 ∈ ℕ0 ((𝑆𝑦)‘𝑚)
4735, 46eqtrdi 2849 . . . . . 6 (𝑏 = 𝑦 → Σ𝑘 ∈ ℕ0 ((𝑆𝑏)‘𝑘) = Σ𝑚 ∈ ℕ0 ((𝑆𝑦)‘𝑚))
4823, 24, 25, 31, 47cbvmptf 5130 . . . . 5 (𝑏𝐷 ↦ Σ𝑘 ∈ ℕ0 ((𝑆𝑏)‘𝑘)) = (𝑦𝐷 ↦ Σ𝑚 ∈ ℕ0 ((𝑆𝑦)‘𝑚))
492, 48eqtri 2821 . . . 4 𝑃 = (𝑦𝐷 ↦ Σ𝑚 ∈ ℕ0 ((𝑆𝑦)‘𝑚))
50 ovexd 7171 . . . . 5 ((𝜑𝑗 ∈ ℕ0) → (𝐶C𝑐𝑗) ∈ V)
51 binomcxplem.f . . . . . 6 𝐹 = (𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗))
5251a1i 11 . . . . 5 (𝜑𝐹 = (𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗)))
5351a1i 11 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → 𝐹 = (𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗)))
54 simpr 488 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 = 𝑘) → 𝑗 = 𝑘)
5554oveq2d 7152 . . . . . . 7 (((𝜑𝑘 ∈ ℕ0) ∧ 𝑗 = 𝑘) → (𝐶C𝑐𝑗) = (𝐶C𝑐𝑘))
56 simpr 488 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0)
57 binomcxp.c . . . . . . . . 9 (𝜑𝐶 ∈ ℂ)
5857adantr 484 . . . . . . . 8 ((𝜑𝑘 ∈ ℕ0) → 𝐶 ∈ ℂ)
5958, 56bcccl 41086 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → (𝐶C𝑐𝑘) ∈ ℂ)
6053, 55, 56, 59fvmptd 6753 . . . . . 6 ((𝜑𝑘 ∈ ℕ0) → (𝐹𝑘) = (𝐶C𝑐𝑘))
6160, 59eqeltrd 2890 . . . . 5 ((𝜑𝑘 ∈ ℕ0) → (𝐹𝑘) ∈ ℂ)
6250, 52, 61fmpt2d 6865 . . . 4 (𝜑𝐹:ℕ0⟶ℂ)
63 nfcv 2955 . . . . . . 7 𝑟
64 nfcv 2955 . . . . . . 7 𝑧
65 nfv 1915 . . . . . . 7 𝑧seq0( + , (𝑆𝑟)) ∈ dom ⇝
66 nfcv 2955 . . . . . . . . 9 𝑟0
67 nfcv 2955 . . . . . . . . 9 𝑟 +
68 nfcv 2955 . . . . . . . . . . 11 𝑟(𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑏𝑘))))
691, 68nfcxfr 2953 . . . . . . . . . 10 𝑟𝑆
70 nfcv 2955 . . . . . . . . . 10 𝑟𝑧
7169, 70nffv 6656 . . . . . . . . 9 𝑟(𝑆𝑧)
7266, 67, 71nfseq 13377 . . . . . . . 8 𝑟seq0( + , (𝑆𝑧))
7372nfel1 2971 . . . . . . 7 𝑟seq0( + , (𝑆𝑧)) ∈ dom ⇝
74 fveq2 6646 . . . . . . . . 9 (𝑟 = 𝑧 → (𝑆𝑟) = (𝑆𝑧))
7574seqeq3d 13375 . . . . . . . 8 (𝑟 = 𝑧 → seq0( + , (𝑆𝑟)) = seq0( + , (𝑆𝑧)))
7675eleq1d 2874 . . . . . . 7 (𝑟 = 𝑧 → (seq0( + , (𝑆𝑟)) ∈ dom ⇝ ↔ seq0( + , (𝑆𝑧)) ∈ dom ⇝ ))
7763, 64, 65, 73, 76cbvrabw 3437 . . . . . 6 {𝑟 ∈ ℝ ∣ seq0( + , (𝑆𝑟)) ∈ dom ⇝ } = {𝑧 ∈ ℝ ∣ seq0( + , (𝑆𝑧)) ∈ dom ⇝ }
7877supeq1i 8898 . . . . 5 sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑆𝑟)) ∈ dom ⇝ }, ℝ*, < ) = sup({𝑧 ∈ ℝ ∣ seq0( + , (𝑆𝑧)) ∈ dom ⇝ }, ℝ*, < )
797, 78eqtri 2821 . . . 4 𝑅 = sup({𝑧 ∈ ℝ ∣ seq0( + , (𝑆𝑧)) ∈ dom ⇝ }, ℝ*, < )
801fveq1i 6647 . . . . . . . . . . 11 (𝑆𝑧) = ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑏𝑘))))‘𝑧)
81 seqeq3 13372 . . . . . . . . . . 11 ((𝑆𝑧) = ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑏𝑘))))‘𝑧) → seq0( + , (𝑆𝑧)) = seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑏𝑘))))‘𝑧)))
8280, 81ax-mp 5 . . . . . . . . . 10 seq0( + , (𝑆𝑧)) = seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑏𝑘))))‘𝑧))
8382eleq1i 2880 . . . . . . . . 9 (seq0( + , (𝑆𝑧)) ∈ dom ⇝ ↔ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑏𝑘))))‘𝑧)) ∈ dom ⇝ )
8483rabbii 3420 . . . . . . . 8 {𝑧 ∈ ℝ ∣ seq0( + , (𝑆𝑧)) ∈ dom ⇝ } = {𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑏𝑘))))‘𝑧)) ∈ dom ⇝ }
8584supeq1i 8898 . . . . . . 7 sup({𝑧 ∈ ℝ ∣ seq0( + , (𝑆𝑧)) ∈ dom ⇝ }, ℝ*, < ) = sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑏𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < )
867, 78, 853eqtrri 2826 . . . . . 6 sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑏𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < ) = 𝑅
8786eleq1i 2880 . . . . 5 (sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑏𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < ) ∈ ℝ ↔ 𝑅 ∈ ℝ)
8886oveq2i 7147 . . . . . 6 ((abs‘𝑥) + sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑏𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < )) = ((abs‘𝑥) + 𝑅)
8988oveq1i 7146 . . . . 5 (((abs‘𝑥) + sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑏𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < )) / 2) = (((abs‘𝑥) + 𝑅) / 2)
90 eqid 2798 . . . . 5 ((abs‘𝑥) + 1) = ((abs‘𝑥) + 1)
9187, 89, 90ifbieq12i 4451 . . . 4 if(sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑏𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < ) ∈ ℝ, (((abs‘𝑥) + sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑏𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < )) / 2), ((abs‘𝑥) + 1)) = if(𝑅 ∈ ℝ, (((abs‘𝑥) + 𝑅) / 2), ((abs‘𝑥) + 1))
92 oveq1 7143 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑏 → (𝑤𝑘) = (𝑏𝑘))
9392oveq2d 7152 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑏 → ((𝐹𝑘) · (𝑤𝑘)) = ((𝐹𝑘) · (𝑏𝑘)))
9493mpteq2dv 5127 . . . . . . . . . . . . . . 15 (𝑤 = 𝑏 → (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑤𝑘))) = (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑏𝑘))))
9594cbvmptv 5134 . . . . . . . . . . . . . 14 (𝑤 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑤𝑘)))) = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑏𝑘))))
9695fveq1i 6647 . . . . . . . . . . . . 13 ((𝑤 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑤𝑘))))‘𝑧) = ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑏𝑘))))‘𝑧)
97 seqeq3 13372 . . . . . . . . . . . . 13 (((𝑤 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑤𝑘))))‘𝑧) = ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑏𝑘))))‘𝑧) → seq0( + , ((𝑤 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑤𝑘))))‘𝑧)) = seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑏𝑘))))‘𝑧)))
9896, 97ax-mp 5 . . . . . . . . . . . 12 seq0( + , ((𝑤 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑤𝑘))))‘𝑧)) = seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑏𝑘))))‘𝑧))
9998eleq1i 2880 . . . . . . . . . . 11 (seq0( + , ((𝑤 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑤𝑘))))‘𝑧)) ∈ dom ⇝ ↔ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑏𝑘))))‘𝑧)) ∈ dom ⇝ )
10099rabbii 3420 . . . . . . . . . 10 {𝑧 ∈ ℝ ∣ seq0( + , ((𝑤 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑤𝑘))))‘𝑧)) ∈ dom ⇝ } = {𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑏𝑘))))‘𝑧)) ∈ dom ⇝ }
101100supeq1i 8898 . . . . . . . . 9 sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑤 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑤𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < ) = sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑏𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < )
102101eleq1i 2880 . . . . . . . 8 (sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑤 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑤𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < ) ∈ ℝ ↔ sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑏𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < ) ∈ ℝ)
103101oveq2i 7147 . . . . . . . . 9 ((abs‘𝑥) + sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑤 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑤𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < )) = ((abs‘𝑥) + sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑏𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < ))
104103oveq1i 7146 . . . . . . . 8 (((abs‘𝑥) + sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑤 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑤𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < )) / 2) = (((abs‘𝑥) + sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑏𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < )) / 2)
105102, 104, 90ifbieq12i 4451 . . . . . . 7 if(sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑤 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑤𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < ) ∈ ℝ, (((abs‘𝑥) + sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑤 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑤𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < )) / 2), ((abs‘𝑥) + 1)) = if(sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑏𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < ) ∈ ℝ, (((abs‘𝑥) + sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑏𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < )) / 2), ((abs‘𝑥) + 1))
106105oveq2i 7147 . . . . . 6 ((abs‘𝑥) + if(sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑤 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑤𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < ) ∈ ℝ, (((abs‘𝑥) + sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑤 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑤𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < )) / 2), ((abs‘𝑥) + 1))) = ((abs‘𝑥) + if(sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑏𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < ) ∈ ℝ, (((abs‘𝑥) + sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑏𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < )) / 2), ((abs‘𝑥) + 1)))
107106oveq1i 7146 . . . . 5 (((abs‘𝑥) + if(sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑤 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑤𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < ) ∈ ℝ, (((abs‘𝑥) + sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑤 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑤𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < )) / 2), ((abs‘𝑥) + 1))) / 2) = (((abs‘𝑥) + if(sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑏𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < ) ∈ ℝ, (((abs‘𝑥) + sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑏𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < )) / 2), ((abs‘𝑥) + 1))) / 2)
108107oveq2i 7147 . . . 4 (0(ball‘(abs ∘ − ))(((abs‘𝑥) + if(sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑤 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑤𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < ) ∈ ℝ, (((abs‘𝑥) + sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑤 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑤𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < )) / 2), ((abs‘𝑥) + 1))) / 2)) = (0(ball‘(abs ∘ − ))(((abs‘𝑥) + if(sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑏𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < ) ∈ ℝ, (((abs‘𝑥) + sup({𝑧 ∈ ℝ ∣ seq0( + , ((𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑏𝑘))))‘𝑧)) ∈ dom ⇝ }, ℝ*, < )) / 2), ((abs‘𝑥) + 1))) / 2))
1091, 49, 62, 79, 3, 91, 108pserdv2 25035 . . 3 (𝜑 → (ℂ D 𝑃) = (𝑦𝐷 ↦ Σ𝑛 ∈ ℕ ((𝑛 · (𝐹𝑛)) · (𝑦↑(𝑛 − 1)))))
110 cnvimass 5917 . . . . . . . 8 (abs “ (0[,)𝑅)) ⊆ dom abs
1113, 110eqsstri 3949 . . . . . . 7 𝐷 ⊆ dom abs
112 absf 14692 . . . . . . . 8 abs:ℂ⟶ℝ
113112fdmi 6499 . . . . . . 7 dom abs = ℂ
114111, 113sseqtri 3951 . . . . . 6 𝐷 ⊆ ℂ
115114sseli 3911 . . . . 5 (𝑦𝐷𝑦 ∈ ℂ)
116 binomcxplem.e . . . . . . . . . 10 𝐸 = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹𝑘)) · (𝑏↑(𝑘 − 1)))))
117116a1i 11 . . . . . . . . 9 ((𝜑𝑦 ∈ ℂ) → 𝐸 = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹𝑘)) · (𝑏↑(𝑘 − 1))))))
118 simplr 768 . . . . . . . . . . . 12 ((((𝜑𝑦 ∈ ℂ) ∧ 𝑏 = 𝑦) ∧ 𝑘 ∈ ℕ) → 𝑏 = 𝑦)
119118oveq1d 7151 . . . . . . . . . . 11 ((((𝜑𝑦 ∈ ℂ) ∧ 𝑏 = 𝑦) ∧ 𝑘 ∈ ℕ) → (𝑏↑(𝑘 − 1)) = (𝑦↑(𝑘 − 1)))
120119oveq2d 7152 . . . . . . . . . 10 ((((𝜑𝑦 ∈ ℂ) ∧ 𝑏 = 𝑦) ∧ 𝑘 ∈ ℕ) → ((𝑘 · (𝐹𝑘)) · (𝑏↑(𝑘 − 1))) = ((𝑘 · (𝐹𝑘)) · (𝑦↑(𝑘 − 1))))
121120mpteq2dva 5126 . . . . . . . . 9 (((𝜑𝑦 ∈ ℂ) ∧ 𝑏 = 𝑦) → (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹𝑘)) · (𝑏↑(𝑘 − 1)))) = (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹𝑘)) · (𝑦↑(𝑘 − 1)))))
122 simpr 488 . . . . . . . . 9 ((𝜑𝑦 ∈ ℂ) → 𝑦 ∈ ℂ)
123 nnex 11634 . . . . . . . . . . 11 ℕ ∈ V
124123mptex 6964 . . . . . . . . . 10 (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹𝑘)) · (𝑦↑(𝑘 − 1)))) ∈ V
125124a1i 11 . . . . . . . . 9 ((𝜑𝑦 ∈ ℂ) → (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹𝑘)) · (𝑦↑(𝑘 − 1)))) ∈ V)
126117, 121, 122, 125fvmptd 6753 . . . . . . . 8 ((𝜑𝑦 ∈ ℂ) → (𝐸𝑦) = (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹𝑘)) · (𝑦↑(𝑘 − 1)))))
127126adantr 484 . . . . . . 7 (((𝜑𝑦 ∈ ℂ) ∧ 𝑛 ∈ ℕ) → (𝐸𝑦) = (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹𝑘)) · (𝑦↑(𝑘 − 1)))))
128 simpr 488 . . . . . . . . 9 ((((𝜑𝑦 ∈ ℂ) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 = 𝑛) → 𝑘 = 𝑛)
129128fveq2d 6650 . . . . . . . . 9 ((((𝜑𝑦 ∈ ℂ) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 = 𝑛) → (𝐹𝑘) = (𝐹𝑛))
130128, 129oveq12d 7154 . . . . . . . 8 ((((𝜑𝑦 ∈ ℂ) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 = 𝑛) → (𝑘 · (𝐹𝑘)) = (𝑛 · (𝐹𝑛)))
131128oveq1d 7151 . . . . . . . . 9 ((((𝜑𝑦 ∈ ℂ) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 = 𝑛) → (𝑘 − 1) = (𝑛 − 1))
132131oveq2d 7152 . . . . . . . 8 ((((𝜑𝑦 ∈ ℂ) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 = 𝑛) → (𝑦↑(𝑘 − 1)) = (𝑦↑(𝑛 − 1)))
133130, 132oveq12d 7154 . . . . . . 7 ((((𝜑𝑦 ∈ ℂ) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 = 𝑛) → ((𝑘 · (𝐹𝑘)) · (𝑦↑(𝑘 − 1))) = ((𝑛 · (𝐹𝑛)) · (𝑦↑(𝑛 − 1))))
134 simpr 488 . . . . . . 7 (((𝜑𝑦 ∈ ℂ) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
135 ovexd 7171 . . . . . . 7 (((𝜑𝑦 ∈ ℂ) ∧ 𝑛 ∈ ℕ) → ((𝑛 · (𝐹𝑛)) · (𝑦↑(𝑛 − 1))) ∈ V)
136127, 133, 134, 135fvmptd 6753 . . . . . 6 (((𝜑𝑦 ∈ ℂ) ∧ 𝑛 ∈ ℕ) → ((𝐸𝑦)‘𝑛) = ((𝑛 · (𝐹𝑛)) · (𝑦↑(𝑛 − 1))))
137136sumeq2dv 15055 . . . . 5 ((𝜑𝑦 ∈ ℂ) → Σ𝑛 ∈ ℕ ((𝐸𝑦)‘𝑛) = Σ𝑛 ∈ ℕ ((𝑛 · (𝐹𝑛)) · (𝑦↑(𝑛 − 1))))
138115, 137sylan2 595 . . . 4 ((𝜑𝑦𝐷) → Σ𝑛 ∈ ℕ ((𝐸𝑦)‘𝑛) = Σ𝑛 ∈ ℕ ((𝑛 · (𝐹𝑛)) · (𝑦↑(𝑛 − 1))))
139138mpteq2dva 5126 . . 3 (𝜑 → (𝑦𝐷 ↦ Σ𝑛 ∈ ℕ ((𝐸𝑦)‘𝑛)) = (𝑦𝐷 ↦ Σ𝑛 ∈ ℕ ((𝑛 · (𝐹𝑛)) · (𝑦↑(𝑛 − 1)))))
140109, 139eqtr4d 2836 . 2 (𝜑 → (ℂ D 𝑃) = (𝑦𝐷 ↦ Σ𝑛 ∈ ℕ ((𝐸𝑦)‘𝑛)))
141 nfcv 2955 . . . 4 𝑏
142 nfmpt1 5129 . . . . . . 7 𝑏(𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹𝑘)) · (𝑏↑(𝑘 − 1)))))
143116, 142nfcxfr 2953 . . . . . 6 𝑏𝐸
144143, 27nffv 6656 . . . . 5 𝑏(𝐸𝑦)
145 nfcv 2955 . . . . 5 𝑏𝑛
146144, 145nffv 6656 . . . 4 𝑏((𝐸𝑦)‘𝑛)
147141, 146nfsum 15042 . . 3 𝑏Σ𝑛 ∈ ℕ ((𝐸𝑦)‘𝑛)
148 nfcv 2955 . . 3 𝑦Σ𝑘 ∈ ℕ ((𝐸𝑏)‘𝑘)
149 simpl 486 . . . . . . 7 ((𝑦 = 𝑏𝑛 ∈ ℕ) → 𝑦 = 𝑏)
150149fveq2d 6650 . . . . . 6 ((𝑦 = 𝑏𝑛 ∈ ℕ) → (𝐸𝑦) = (𝐸𝑏))
151150fveq1d 6648 . . . . 5 ((𝑦 = 𝑏𝑛 ∈ ℕ) → ((𝐸𝑦)‘𝑛) = ((𝐸𝑏)‘𝑛))
152151sumeq2dv 15055 . . . 4 (𝑦 = 𝑏 → Σ𝑛 ∈ ℕ ((𝐸𝑦)‘𝑛) = Σ𝑛 ∈ ℕ ((𝐸𝑏)‘𝑛))
153 nfmpt1 5129 . . . . . . . . 9 𝑘(𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹𝑘)) · (𝑏↑(𝑘 − 1))))
15437, 153nfmpt 5128 . . . . . . . 8 𝑘(𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ ↦ ((𝑘 · (𝐹𝑘)) · (𝑏↑(𝑘 − 1)))))
155116, 154nfcxfr 2953 . . . . . . 7 𝑘𝐸
156 nfcv 2955 . . . . . . 7 𝑘𝑏
157155, 156nffv 6656 . . . . . 6 𝑘(𝐸𝑏)
158 nfcv 2955 . . . . . 6 𝑘𝑛
159157, 158nffv 6656 . . . . 5 𝑘((𝐸𝑏)‘𝑛)
160 nfcv 2955 . . . . 5 𝑛((𝐸𝑏)‘𝑘)
161 fveq2 6646 . . . . 5 (𝑛 = 𝑘 → ((𝐸𝑏)‘𝑛) = ((𝐸𝑏)‘𝑘))
162159, 160, 161cbvsumi 15049 . . . 4 Σ𝑛 ∈ ℕ ((𝐸𝑏)‘𝑛) = Σ𝑘 ∈ ℕ ((𝐸𝑏)‘𝑘)
163152, 162eqtrdi 2849 . . 3 (𝑦 = 𝑏 → Σ𝑛 ∈ ℕ ((𝐸𝑦)‘𝑛) = Σ𝑘 ∈ ℕ ((𝐸𝑏)‘𝑘))
16424, 23, 147, 148, 163cbvmptf 5130 . 2 (𝑦𝐷 ↦ Σ𝑛 ∈ ℕ ((𝐸𝑦)‘𝑛)) = (𝑏𝐷 ↦ Σ𝑘 ∈ ℕ ((𝐸𝑏)‘𝑘))
165140, 164eqtrdi 2849 1 (𝜑 → (ℂ D 𝑃) = (𝑏𝐷 ↦ Σ𝑘 ∈ ℕ ((𝐸𝑏)‘𝑘)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111  {crab 3110  Vcvv 3441  ifcif 4425   class class class wbr 5031   ↦ cmpt 5111  ◡ccnv 5519  dom cdm 5520   “ cima 5523   ∘ ccom 5524  ‘cfv 6325  (class class class)co 7136  supcsup 8891  ℂcc 10527  ℝcr 10528  0cc0 10529  1c1 10530   + caddc 10532   · cmul 10534  ℝ*cxr 10666   < clt 10667   − cmin 10862   / cdiv 11289  ℕcn 11628  2c2 11683  ℕ0cn0 11888  ℝ+crp 12380  [,)cico 12731  seqcseq 13367  ↑cexp 13428  abscabs 14588   ⇝ cli 14836  Σcsu 15037  ballcbl 20082   D cdv 24476  C𝑐cbcc 41083 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5155  ax-sep 5168  ax-nul 5175  ax-pow 5232  ax-pr 5296  ax-un 7444  ax-inf2 9091  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606  ax-pre-sup 10607  ax-addf 10608  ax-mulf 10609 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-int 4840  df-iun 4884  df-iin 4885  df-br 5032  df-opab 5094  df-mpt 5112  df-tr 5138  df-id 5426  df-eprel 5431  df-po 5439  df-so 5440  df-fr 5479  df-se 5480  df-we 5481  df-xp 5526  df-rel 5527  df-cnv 5528  df-co 5529  df-dm 5530  df-rn 5531  df-res 5532  df-ima 5533  df-pred 6117  df-ord 6163  df-on 6164  df-lim 6165  df-suc 6166  df-iota 6284  df-fun 6327  df-fn 6328  df-f 6329  df-f1 6330  df-fo 6331  df-f1o 6332  df-fv 6333  df-isom 6334  df-riota 7094  df-ov 7139  df-oprab 7140  df-mpo 7141  df-of 7391  df-om 7564  df-1st 7674  df-2nd 7675  df-supp 7817  df-wrecs 7933  df-recs 7994  df-rdg 8032  df-1o 8088  df-2o 8089  df-oadd 8092  df-er 8275  df-map 8394  df-pm 8395  df-ixp 8448  df-en 8496  df-dom 8497  df-sdom 8498  df-fin 8499  df-fsupp 8821  df-fi 8862  df-sup 8893  df-inf 8894  df-oi 8961  df-card 9355  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-div 11290  df-nn 11629  df-2 11691  df-3 11692  df-4 11693  df-5 11694  df-6 11695  df-7 11696  df-8 11697  df-9 11698  df-n0 11889  df-z 11973  df-dec 12090  df-uz 12235  df-q 12340  df-rp 12381  df-xneg 12498  df-xadd 12499  df-xmul 12500  df-ioo 12733  df-ico 12735  df-icc 12736  df-fz 12889  df-fzo 13032  df-fl 13160  df-seq 13368  df-exp 13429  df-fac 13633  df-hash 13690  df-shft 14421  df-cj 14453  df-re 14454  df-im 14455  df-sqrt 14589  df-abs 14590  df-limsup 14823  df-clim 14840  df-rlim 14841  df-sum 15038  df-prod 15255  df-fallfac 15356  df-struct 16480  df-ndx 16481  df-slot 16482  df-base 16484  df-sets 16485  df-ress 16486  df-plusg 16573  df-mulr 16574  df-starv 16575  df-sca 16576  df-vsca 16577  df-ip 16578  df-tset 16579  df-ple 16580  df-ds 16582  df-unif 16583  df-hom 16584  df-cco 16585  df-rest 16691  df-topn 16692  df-0g 16710  df-gsum 16711  df-topgen 16712  df-pt 16713  df-prds 16716  df-xrs 16770  df-qtop 16775  df-imas 16776  df-xps 16778  df-mre 16852  df-mrc 16853  df-acs 16855  df-mgm 17847  df-sgrp 17896  df-mnd 17907  df-submnd 17952  df-mulg 18221  df-cntz 18443  df-cmn 18904  df-psmet 20087  df-xmet 20088  df-met 20089  df-bl 20090  df-mopn 20091  df-fbas 20092  df-fg 20093  df-cnfld 20096  df-top 21509  df-topon 21526  df-topsp 21548  df-bases 21561  df-cld 21634  df-ntr 21635  df-cls 21636  df-nei 21713  df-lp 21751  df-perf 21752  df-cn 21842  df-cnp 21843  df-haus 21930  df-cmp 22002  df-tx 22177  df-hmeo 22370  df-fil 22461  df-fm 22553  df-flim 22554  df-flf 22555  df-xms 22937  df-ms 22938  df-tms 22939  df-cncf 23493  df-limc 24479  df-dv 24480  df-ulm 24982  df-bcc 41084 This theorem is referenced by:  binomcxplemnotnn0  41103
 Copyright terms: Public domain W3C validator