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

Theorem binomcxplemdvbinom 41072
 Description: Lemma for binomcxp 41076. By the power and chain rules, calculate the derivative of ((1 + 𝑏)↑𝑐-𝐶), with respect to 𝑏 in the disk of convergence 𝐷. We later multiply the derivative in the later binomcxplemdvsum 41074 by this derivative to show that ((1 + 𝑏)↑𝑐𝐶) (with a nonnegated 𝐶) and the later sum, since both at 𝑏 = 0 equal one, are the same. (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[,)𝑅))
Assertion
Ref Expression
binomcxplemdvbinom ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → (ℂ D (𝑏𝐷 ↦ ((1 + 𝑏)↑𝑐-𝐶))) = (𝑏𝐷 ↦ (-𝐶 · ((1 + 𝑏)↑𝑐(-𝐶 − 1)))))
Distinct variable groups:   𝑗,𝑘,𝜑   𝑘,𝑏,𝐶   𝐶,𝑗   𝐹,𝑏,𝑘   𝑆,𝑟   𝑟,𝑏
Allowed substitution hints:   𝜑(𝑟,𝑏)   𝐴(𝑗,𝑘,𝑟,𝑏)   𝐵(𝑗,𝑘,𝑟,𝑏)   𝐶(𝑟)   𝐷(𝑗,𝑘,𝑟,𝑏)   𝑅(𝑗,𝑘,𝑟,𝑏)   𝑆(𝑗,𝑘,𝑏)   𝐸(𝑗,𝑘,𝑟,𝑏)   𝐹(𝑗,𝑟)

Proof of Theorem binomcxplemdvbinom
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 binomcxplem.d . . . . 5 𝐷 = (abs “ (0[,)𝑅))
2 nfcv 2955 . . . . . 6 𝑏abs
3 nfcv 2955 . . . . . . 7 𝑏0
4 nfcv 2955 . . . . . . 7 𝑏[,)
5 binomcxplem.r . . . . . . . 8 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑆𝑟)) ∈ dom ⇝ }, ℝ*, < )
6 nfcv 2955 . . . . . . . . . . . 12 𝑏 +
7 binomcxplem.s . . . . . . . . . . . . . 14 𝑆 = (𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑏𝑘))))
8 nfmpt1 5128 . . . . . . . . . . . . . 14 𝑏(𝑏 ∈ ℂ ↦ (𝑘 ∈ ℕ0 ↦ ((𝐹𝑘) · (𝑏𝑘))))
97, 8nfcxfr 2953 . . . . . . . . . . . . 13 𝑏𝑆
10 nfcv 2955 . . . . . . . . . . . . 13 𝑏𝑟
119, 10nffv 6655 . . . . . . . . . . . 12 𝑏(𝑆𝑟)
123, 6, 11nfseq 13376 . . . . . . . . . . 11 𝑏seq0( + , (𝑆𝑟))
1312nfel1 2971 . . . . . . . . . 10 𝑏seq0( + , (𝑆𝑟)) ∈ dom ⇝
14 nfcv 2955 . . . . . . . . . 10 𝑏
1513, 14nfrabw 3338 . . . . . . . . 9 𝑏{𝑟 ∈ ℝ ∣ seq0( + , (𝑆𝑟)) ∈ dom ⇝ }
16 nfcv 2955 . . . . . . . . 9 𝑏*
17 nfcv 2955 . . . . . . . . 9 𝑏 <
1815, 16, 17nfsup 8901 . . . . . . . 8 𝑏sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑆𝑟)) ∈ dom ⇝ }, ℝ*, < )
195, 18nfcxfr 2953 . . . . . . 7 𝑏𝑅
203, 4, 19nfov 7165 . . . . . 6 𝑏(0[,)𝑅)
212, 20nfima 5904 . . . . 5 𝑏(abs “ (0[,)𝑅))
221, 21nfcxfr 2953 . . . 4 𝑏𝐷
23 nfcv 2955 . . . 4 𝑦𝐷
24 nfcv 2955 . . . 4 𝑦((1 + 𝑏)↑𝑐-𝐶)
25 nfcv 2955 . . . 4 𝑏((1 + 𝑦)↑𝑐-𝐶)
26 oveq2 7143 . . . . 5 (𝑏 = 𝑦 → (1 + 𝑏) = (1 + 𝑦))
2726oveq1d 7150 . . . 4 (𝑏 = 𝑦 → ((1 + 𝑏)↑𝑐-𝐶) = ((1 + 𝑦)↑𝑐-𝐶))
2822, 23, 24, 25, 27cbvmptf 5129 . . 3 (𝑏𝐷 ↦ ((1 + 𝑏)↑𝑐-𝐶)) = (𝑦𝐷 ↦ ((1 + 𝑦)↑𝑐-𝐶))
2928oveq2i 7146 . 2 (ℂ D (𝑏𝐷 ↦ ((1 + 𝑏)↑𝑐-𝐶))) = (ℂ D (𝑦𝐷 ↦ ((1 + 𝑦)↑𝑐-𝐶)))
30 cnelprrecn 10621 . . . . 5 ℂ ∈ {ℝ, ℂ}
3130a1i 11 . . . 4 ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → ℂ ∈ {ℝ, ℂ})
32 1cnd 10627 . . . . . 6 (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦𝐷) → 1 ∈ ℂ)
33 cnvimass 5916 . . . . . . . . . 10 (abs “ (0[,)𝑅)) ⊆ dom abs
341, 33eqsstri 3949 . . . . . . . . 9 𝐷 ⊆ dom abs
35 absf 14691 . . . . . . . . . 10 abs:ℂ⟶ℝ
3635fdmi 6498 . . . . . . . . 9 dom abs = ℂ
3734, 36sseqtri 3951 . . . . . . . 8 𝐷 ⊆ ℂ
3837a1i 11 . . . . . . 7 ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → 𝐷 ⊆ ℂ)
3938sselda 3915 . . . . . 6 (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦𝐷) → 𝑦 ∈ ℂ)
4032, 39addcld 10651 . . . . 5 (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦𝐷) → (1 + 𝑦) ∈ ℂ)
41 simpr 488 . . . . . . 7 ((((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦𝐷) ∧ (1 + 𝑦) ∈ ℝ) → (1 + 𝑦) ∈ ℝ)
42 1cnd 10627 . . . . . . . . . 10 ((((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦𝐷) ∧ (1 + 𝑦) ∈ ℝ) → 1 ∈ ℂ)
4339adantr 484 . . . . . . . . . 10 ((((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦𝐷) ∧ (1 + 𝑦) ∈ ℝ) → 𝑦 ∈ ℂ)
4442, 43pncan2d 10990 . . . . . . . . 9 ((((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦𝐷) ∧ (1 + 𝑦) ∈ ℝ) → ((1 + 𝑦) − 1) = 𝑦)
45 1red 10633 . . . . . . . . . 10 ((((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦𝐷) ∧ (1 + 𝑦) ∈ ℝ) → 1 ∈ ℝ)
4641, 45resubcld 11059 . . . . . . . . 9 ((((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦𝐷) ∧ (1 + 𝑦) ∈ ℝ) → ((1 + 𝑦) − 1) ∈ ℝ)
4744, 46eqeltrrd 2891 . . . . . . . 8 ((((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦𝐷) ∧ (1 + 𝑦) ∈ ℝ) → 𝑦 ∈ ℝ)
48 1pneg1e0 11746 . . . . . . . . 9 (1 + -1) = 0
49 1red 10633 . . . . . . . . . . 11 ((((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦𝐷) ∧ 𝑦 ∈ ℝ) → 1 ∈ ℝ)
5049renegcld 11058 . . . . . . . . . 10 ((((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦𝐷) ∧ 𝑦 ∈ ℝ) → -1 ∈ ℝ)
51 simpr 488 . . . . . . . . . 10 ((((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦𝐷) ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
52 ffn 6487 . . . . . . . . . . . . . . . . . . . 20 (abs:ℂ⟶ℝ → abs Fn ℂ)
53 elpreima 6805 . . . . . . . . . . . . . . . . . . . 20 (abs Fn ℂ → (𝑦 ∈ (abs “ (0[,)𝑅)) ↔ (𝑦 ∈ ℂ ∧ (abs‘𝑦) ∈ (0[,)𝑅))))
5435, 52, 53mp2b 10 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ (abs “ (0[,)𝑅)) ↔ (𝑦 ∈ ℂ ∧ (abs‘𝑦) ∈ (0[,)𝑅)))
5554simprbi 500 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (abs “ (0[,)𝑅)) → (abs‘𝑦) ∈ (0[,)𝑅))
5655, 1eleq2s 2908 . . . . . . . . . . . . . . . . 17 (𝑦𝐷 → (abs‘𝑦) ∈ (0[,)𝑅))
57 0re 10634 . . . . . . . . . . . . . . . . . 18 0 ∈ ℝ
58 ssrab2 4007 . . . . . . . . . . . . . . . . . . . . 21 {𝑟 ∈ ℝ ∣ seq0( + , (𝑆𝑟)) ∈ dom ⇝ } ⊆ ℝ
59 ressxr 10676 . . . . . . . . . . . . . . . . . . . . 21 ℝ ⊆ ℝ*
6058, 59sstri 3924 . . . . . . . . . . . . . . . . . . . 20 {𝑟 ∈ ℝ ∣ seq0( + , (𝑆𝑟)) ∈ dom ⇝ } ⊆ ℝ*
61 supxrcl 12698 . . . . . . . . . . . . . . . . . . . 20 ({𝑟 ∈ ℝ ∣ seq0( + , (𝑆𝑟)) ∈ dom ⇝ } ⊆ ℝ* → sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑆𝑟)) ∈ dom ⇝ }, ℝ*, < ) ∈ ℝ*)
6260, 61ax-mp 5 . . . . . . . . . . . . . . . . . . 19 sup({𝑟 ∈ ℝ ∣ seq0( + , (𝑆𝑟)) ∈ dom ⇝ }, ℝ*, < ) ∈ ℝ*
635, 62eqeltri 2886 . . . . . . . . . . . . . . . . . 18 𝑅 ∈ ℝ*
64 elico2 12791 . . . . . . . . . . . . . . . . . 18 ((0 ∈ ℝ ∧ 𝑅 ∈ ℝ*) → ((abs‘𝑦) ∈ (0[,)𝑅) ↔ ((abs‘𝑦) ∈ ℝ ∧ 0 ≤ (abs‘𝑦) ∧ (abs‘𝑦) < 𝑅)))
6557, 63, 64mp2an 691 . . . . . . . . . . . . . . . . 17 ((abs‘𝑦) ∈ (0[,)𝑅) ↔ ((abs‘𝑦) ∈ ℝ ∧ 0 ≤ (abs‘𝑦) ∧ (abs‘𝑦) < 𝑅))
6656, 65sylib 221 . . . . . . . . . . . . . . . 16 (𝑦𝐷 → ((abs‘𝑦) ∈ ℝ ∧ 0 ≤ (abs‘𝑦) ∧ (abs‘𝑦) < 𝑅))
6766simp3d 1141 . . . . . . . . . . . . . . 15 (𝑦𝐷 → (abs‘𝑦) < 𝑅)
6867adantl 485 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦𝐷) → (abs‘𝑦) < 𝑅)
69 binomcxp.a . . . . . . . . . . . . . . . 16 (𝜑𝐴 ∈ ℝ+)
70 binomcxp.b . . . . . . . . . . . . . . . 16 (𝜑𝐵 ∈ ℝ)
71 binomcxp.lt . . . . . . . . . . . . . . . 16 (𝜑 → (abs‘𝐵) < (abs‘𝐴))
72 binomcxp.c . . . . . . . . . . . . . . . 16 (𝜑𝐶 ∈ ℂ)
73 binomcxplem.f . . . . . . . . . . . . . . . 16 𝐹 = (𝑗 ∈ ℕ0 ↦ (𝐶C𝑐𝑗))
7469, 70, 71, 72, 73, 7, 5binomcxplemradcnv 41071 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → 𝑅 = 1)
7574adantr 484 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦𝐷) → 𝑅 = 1)
7668, 75breqtrd 5056 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦𝐷) → (abs‘𝑦) < 1)
7776adantr 484 . . . . . . . . . . . 12 ((((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦𝐷) ∧ 𝑦 ∈ ℝ) → (abs‘𝑦) < 1)
7851, 49absltd 14783 . . . . . . . . . . . 12 ((((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦𝐷) ∧ 𝑦 ∈ ℝ) → ((abs‘𝑦) < 1 ↔ (-1 < 𝑦𝑦 < 1)))
7977, 78mpbid 235 . . . . . . . . . . 11 ((((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦𝐷) ∧ 𝑦 ∈ ℝ) → (-1 < 𝑦𝑦 < 1))
8079simpld 498 . . . . . . . . . 10 ((((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦𝐷) ∧ 𝑦 ∈ ℝ) → -1 < 𝑦)
8150, 51, 49, 80ltadd2dd 10790 . . . . . . . . 9 ((((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦𝐷) ∧ 𝑦 ∈ ℝ) → (1 + -1) < (1 + 𝑦))
8248, 81eqbrtrrid 5066 . . . . . . . 8 ((((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦𝐷) ∧ 𝑦 ∈ ℝ) → 0 < (1 + 𝑦))
8347, 82syldan 594 . . . . . . 7 ((((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦𝐷) ∧ (1 + 𝑦) ∈ ℝ) → 0 < (1 + 𝑦))
8441, 83elrpd 12418 . . . . . 6 ((((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦𝐷) ∧ (1 + 𝑦) ∈ ℝ) → (1 + 𝑦) ∈ ℝ+)
8584ex 416 . . . . 5 (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦𝐷) → ((1 + 𝑦) ∈ ℝ → (1 + 𝑦) ∈ ℝ+))
86 eqid 2798 . . . . . 6 (ℂ ∖ (-∞(,]0)) = (ℂ ∖ (-∞(,]0))
8786ellogdm 25237 . . . . 5 ((1 + 𝑦) ∈ (ℂ ∖ (-∞(,]0)) ↔ ((1 + 𝑦) ∈ ℂ ∧ ((1 + 𝑦) ∈ ℝ → (1 + 𝑦) ∈ ℝ+)))
8840, 85, 87sylanbrc 586 . . . 4 (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦𝐷) → (1 + 𝑦) ∈ (ℂ ∖ (-∞(,]0)))
89 eldifi 4054 . . . . . 6 (𝑥 ∈ (ℂ ∖ (-∞(,]0)) → 𝑥 ∈ ℂ)
9089adantl 485 . . . . 5 (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑥 ∈ (ℂ ∖ (-∞(,]0))) → 𝑥 ∈ ℂ)
9172adantr 484 . . . . . . 7 ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → 𝐶 ∈ ℂ)
9291negcld 10975 . . . . . 6 ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → -𝐶 ∈ ℂ)
9392adantr 484 . . . . 5 (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑥 ∈ (ℂ ∖ (-∞(,]0))) → -𝐶 ∈ ℂ)
9490, 93cxpcld 25306 . . . 4 (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑥 ∈ (ℂ ∖ (-∞(,]0))) → (𝑥𝑐-𝐶) ∈ ℂ)
95 ovexd 7170 . . . 4 (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑥 ∈ (ℂ ∖ (-∞(,]0))) → (-𝐶 · (𝑥𝑐(-𝐶 − 1))) ∈ V)
96 1cnd 10627 . . . . . . 7 (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑥 ∈ ℂ) → 1 ∈ ℂ)
97 simpr 488 . . . . . . 7 (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑥 ∈ ℂ) → 𝑥 ∈ ℂ)
9896, 97addcld 10651 . . . . . 6 (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑥 ∈ ℂ) → (1 + 𝑥) ∈ ℂ)
99 c0ex 10626 . . . . . . . . 9 0 ∈ V
10099a1i 11 . . . . . . . 8 (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑥 ∈ ℂ) → 0 ∈ V)
101 1cnd 10627 . . . . . . . . 9 ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → 1 ∈ ℂ)
10231, 101dvmptc 24568 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → (ℂ D (𝑥 ∈ ℂ ↦ 1)) = (𝑥 ∈ ℂ ↦ 0))
10331dvmptid 24567 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → (ℂ D (𝑥 ∈ ℂ ↦ 𝑥)) = (𝑥 ∈ ℂ ↦ 1))
10431, 96, 100, 102, 97, 96, 103dvmptadd 24570 . . . . . . 7 ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → (ℂ D (𝑥 ∈ ℂ ↦ (1 + 𝑥))) = (𝑥 ∈ ℂ ↦ (0 + 1)))
105 0p1e1 11749 . . . . . . . 8 (0 + 1) = 1
106105mpteq2i 5122 . . . . . . 7 (𝑥 ∈ ℂ ↦ (0 + 1)) = (𝑥 ∈ ℂ ↦ 1)
107104, 106eqtrdi 2849 . . . . . 6 ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → (ℂ D (𝑥 ∈ ℂ ↦ (1 + 𝑥))) = (𝑥 ∈ ℂ ↦ 1))
108 fvex 6658 . . . . . . . 8 (TopOpen‘ℂfld) ∈ V
109 cnfldtps 23390 . . . . . . . . . 10 fld ∈ TopSp
110 cnfldbas 20098 . . . . . . . . . . 11 ℂ = (Base‘ℂfld)
111 eqid 2798 . . . . . . . . . . 11 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
112110, 111tpsuni 21548 . . . . . . . . . 10 (ℂfld ∈ TopSp → ℂ = (TopOpen‘ℂfld))
113109, 112ax-mp 5 . . . . . . . . 9 ℂ = (TopOpen‘ℂfld)
114113restid 16701 . . . . . . . 8 ((TopOpen‘ℂfld) ∈ V → ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld))
115108, 114ax-mp 5 . . . . . . 7 ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld)
116115eqcomi 2807 . . . . . 6 (TopOpen‘ℂfld) = ((TopOpen‘ℂfld) ↾t ℂ)
117111cnfldtop 23396 . . . . . . . 8 (TopOpen‘ℂfld) ∈ Top
118 eqid 2798 . . . . . . . . . . . 12 (abs ∘ − ) = (abs ∘ − )
119118cnbl0 23386 . . . . . . . . . . 11 (𝑅 ∈ ℝ* → (abs “ (0[,)𝑅)) = (0(ball‘(abs ∘ − ))𝑅))
12063, 119ax-mp 5 . . . . . . . . . 10 (abs “ (0[,)𝑅)) = (0(ball‘(abs ∘ − ))𝑅)
1211, 120eqtri 2821 . . . . . . . . 9 𝐷 = (0(ball‘(abs ∘ − ))𝑅)
122 cnxmet 23385 . . . . . . . . . 10 (abs ∘ − ) ∈ (∞Met‘ℂ)
123 0cn 10624 . . . . . . . . . 10 0 ∈ ℂ
124111cnfldtopn 23394 . . . . . . . . . . 11 (TopOpen‘ℂfld) = (MetOpen‘(abs ∘ − ))
125124blopn 23114 . . . . . . . . . 10 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ ∧ 𝑅 ∈ ℝ*) → (0(ball‘(abs ∘ − ))𝑅) ∈ (TopOpen‘ℂfld))
126122, 123, 63, 125mp3an 1458 . . . . . . . . 9 (0(ball‘(abs ∘ − ))𝑅) ∈ (TopOpen‘ℂfld)
127121, 126eqeltri 2886 . . . . . . . 8 𝐷 ∈ (TopOpen‘ℂfld)
128 isopn3i 21694 . . . . . . . 8 (((TopOpen‘ℂfld) ∈ Top ∧ 𝐷 ∈ (TopOpen‘ℂfld)) → ((int‘(TopOpen‘ℂfld))‘𝐷) = 𝐷)
129117, 127, 128mp2an 691 . . . . . . 7 ((int‘(TopOpen‘ℂfld))‘𝐷) = 𝐷
130129a1i 11 . . . . . 6 ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → ((int‘(TopOpen‘ℂfld))‘𝐷) = 𝐷)
13131, 98, 96, 107, 38, 116, 111, 130dvmptres2 24572 . . . . 5 ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → (ℂ D (𝑥𝐷 ↦ (1 + 𝑥))) = (𝑥𝐷 ↦ 1))
132 oveq2 7143 . . . . . . 7 (𝑥 = 𝑦 → (1 + 𝑥) = (1 + 𝑦))
133132cbvmptv 5133 . . . . . 6 (𝑥𝐷 ↦ (1 + 𝑥)) = (𝑦𝐷 ↦ (1 + 𝑦))
134133oveq2i 7146 . . . . 5 (ℂ D (𝑥𝐷 ↦ (1 + 𝑥))) = (ℂ D (𝑦𝐷 ↦ (1 + 𝑦)))
135 eqidd 2799 . . . . . 6 (𝑥 = 𝑦 → 1 = 1)
136135cbvmptv 5133 . . . . 5 (𝑥𝐷 ↦ 1) = (𝑦𝐷 ↦ 1)
137131, 134, 1363eqtr3g 2856 . . . 4 ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → (ℂ D (𝑦𝐷 ↦ (1 + 𝑦))) = (𝑦𝐷 ↦ 1))
13886dvcncxp1 25339 . . . . 5 (-𝐶 ∈ ℂ → (ℂ D (𝑥 ∈ (ℂ ∖ (-∞(,]0)) ↦ (𝑥𝑐-𝐶))) = (𝑥 ∈ (ℂ ∖ (-∞(,]0)) ↦ (-𝐶 · (𝑥𝑐(-𝐶 − 1)))))
13992, 138syl 17 . . . 4 ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → (ℂ D (𝑥 ∈ (ℂ ∖ (-∞(,]0)) ↦ (𝑥𝑐-𝐶))) = (𝑥 ∈ (ℂ ∖ (-∞(,]0)) ↦ (-𝐶 · (𝑥𝑐(-𝐶 − 1)))))
140 oveq1 7142 . . . 4 (𝑥 = (1 + 𝑦) → (𝑥𝑐-𝐶) = ((1 + 𝑦)↑𝑐-𝐶))
141 oveq1 7142 . . . . 5 (𝑥 = (1 + 𝑦) → (𝑥𝑐(-𝐶 − 1)) = ((1 + 𝑦)↑𝑐(-𝐶 − 1)))
142141oveq2d 7151 . . . 4 (𝑥 = (1 + 𝑦) → (-𝐶 · (𝑥𝑐(-𝐶 − 1))) = (-𝐶 · ((1 + 𝑦)↑𝑐(-𝐶 − 1))))
14331, 31, 88, 32, 94, 95, 137, 139, 140, 142dvmptco 24582 . . 3 ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → (ℂ D (𝑦𝐷 ↦ ((1 + 𝑦)↑𝑐-𝐶))) = (𝑦𝐷 ↦ ((-𝐶 · ((1 + 𝑦)↑𝑐(-𝐶 − 1))) · 1)))
14491adantr 484 . . . . . . 7 (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦𝐷) → 𝐶 ∈ ℂ)
145144negcld 10975 . . . . . 6 (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦𝐷) → -𝐶 ∈ ℂ)
146145, 32subcld 10988 . . . . . . 7 (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦𝐷) → (-𝐶 − 1) ∈ ℂ)
14740, 146cxpcld 25306 . . . . . 6 (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦𝐷) → ((1 + 𝑦)↑𝑐(-𝐶 − 1)) ∈ ℂ)
148145, 147mulcld 10652 . . . . 5 (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦𝐷) → (-𝐶 · ((1 + 𝑦)↑𝑐(-𝐶 − 1))) ∈ ℂ)
149148mulid1d 10649 . . . 4 (((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) ∧ 𝑦𝐷) → ((-𝐶 · ((1 + 𝑦)↑𝑐(-𝐶 − 1))) · 1) = (-𝐶 · ((1 + 𝑦)↑𝑐(-𝐶 − 1))))
150149mpteq2dva 5125 . . 3 ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → (𝑦𝐷 ↦ ((-𝐶 · ((1 + 𝑦)↑𝑐(-𝐶 − 1))) · 1)) = (𝑦𝐷 ↦ (-𝐶 · ((1 + 𝑦)↑𝑐(-𝐶 − 1)))))
151 nfcv 2955 . . . . 5 𝑏(-𝐶 · ((1 + 𝑦)↑𝑐(-𝐶 − 1)))
152 nfcv 2955 . . . . 5 𝑦(-𝐶 · ((1 + 𝑏)↑𝑐(-𝐶 − 1)))
153 oveq2 7143 . . . . . . 7 (𝑦 = 𝑏 → (1 + 𝑦) = (1 + 𝑏))
154153oveq1d 7150 . . . . . 6 (𝑦 = 𝑏 → ((1 + 𝑦)↑𝑐(-𝐶 − 1)) = ((1 + 𝑏)↑𝑐(-𝐶 − 1)))
155154oveq2d 7151 . . . . 5 (𝑦 = 𝑏 → (-𝐶 · ((1 + 𝑦)↑𝑐(-𝐶 − 1))) = (-𝐶 · ((1 + 𝑏)↑𝑐(-𝐶 − 1))))
15623, 22, 151, 152, 155cbvmptf 5129 . . . 4 (𝑦𝐷 ↦ (-𝐶 · ((1 + 𝑦)↑𝑐(-𝐶 − 1)))) = (𝑏𝐷 ↦ (-𝐶 · ((1 + 𝑏)↑𝑐(-𝐶 − 1))))
157156a1i 11 . . 3 ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → (𝑦𝐷 ↦ (-𝐶 · ((1 + 𝑦)↑𝑐(-𝐶 − 1)))) = (𝑏𝐷 ↦ (-𝐶 · ((1 + 𝑏)↑𝑐(-𝐶 − 1)))))
158143, 150, 1573eqtrd 2837 . 2 ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → (ℂ D (𝑦𝐷 ↦ ((1 + 𝑦)↑𝑐-𝐶))) = (𝑏𝐷 ↦ (-𝐶 · ((1 + 𝑏)↑𝑐(-𝐶 − 1)))))
15929, 158syl5eq 2845 1 ((𝜑 ∧ ¬ 𝐶 ∈ ℕ0) → (ℂ D (𝑏𝐷 ↦ ((1 + 𝑏)↑𝑐-𝐶))) = (𝑏𝐷 ↦ (-𝐶 · ((1 + 𝑏)↑𝑐(-𝐶 − 1)))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111  {crab 3110  Vcvv 3441   ∖ cdif 3878   ⊆ wss 3881  {cpr 4527  ∪ cuni 4800   class class class wbr 5030   ↦ cmpt 5110  ◡ccnv 5518  dom cdm 5519   “ cima 5522   ∘ ccom 5523   Fn wfn 6319  ⟶wf 6320  ‘cfv 6324  (class class class)co 7135  supcsup 8890  ℂcc 10526  ℝcr 10527  0cc0 10528  1c1 10529   + caddc 10531   · cmul 10533  -∞cmnf 10664  ℝ*cxr 10665   < clt 10666   ≤ cle 10667   − cmin 10861  -cneg 10862  ℕcn 11627  ℕ0cn0 11887  ℝ+crp 12379  (,]cioc 12729  [,)cico 12730  seqcseq 13366  ↑cexp 13427  abscabs 14587   ⇝ cli 14835   ↾t crest 16688  TopOpenctopn 16689  ∞Metcxmet 20079  ballcbl 20081  ℂfldccnfld 20094  Topctop 21505  TopSpctps 21544  intcnt 21629   D cdv 24473  ↑𝑐ccxp 25154  C𝑐cbcc 41055 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 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7443  ax-inf2 9090  ax-cnex 10584  ax-resscn 10585  ax-1cn 10586  ax-icn 10587  ax-addcl 10588  ax-addrcl 10589  ax-mulcl 10590  ax-mulrcl 10591  ax-mulcom 10592  ax-addass 10593  ax-mulass 10594  ax-distr 10595  ax-i2m1 10596  ax-1ne0 10597  ax-1rid 10598  ax-rnegex 10599  ax-rrecex 10600  ax-cnre 10601  ax-pre-lttri 10602  ax-pre-lttrn 10603  ax-pre-ltadd 10604  ax-pre-mulgt0 10605  ax-pre-sup 10606  ax-addf 10607  ax-mulf 10608 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 4801  df-int 4839  df-iun 4883  df-iin 4884  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-se 5479  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-isom 6333  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-of 7390  df-om 7563  df-1st 7673  df-2nd 7674  df-supp 7816  df-wrecs 7932  df-recs 7993  df-rdg 8031  df-1o 8087  df-2o 8088  df-oadd 8091  df-er 8274  df-map 8393  df-pm 8394  df-ixp 8447  df-en 8495  df-dom 8496  df-sdom 8497  df-fin 8498  df-fsupp 8820  df-fi 8861  df-sup 8892  df-inf 8893  df-oi 8960  df-card 9354  df-pnf 10668  df-mnf 10669  df-xr 10670  df-ltxr 10671  df-le 10672  df-sub 10863  df-neg 10864  df-div 11289  df-nn 11628  df-2 11690  df-3 11691  df-4 11692  df-5 11693  df-6 11694  df-7 11695  df-8 11696  df-9 11697  df-n0 11888  df-z 11972  df-dec 12089  df-uz 12234  df-q 12339  df-rp 12380  df-xneg 12497  df-xadd 12498  df-xmul 12499  df-ioo 12732  df-ioc 12733  df-ico 12734  df-icc 12735  df-fz 12888  df-fzo 13031  df-fl 13159  df-mod 13235  df-seq 13367  df-exp 13428  df-fac 13632  df-bc 13661  df-hash 13689  df-shft 14420  df-cj 14452  df-re 14453  df-im 14454  df-sqrt 14588  df-abs 14589  df-limsup 14822  df-clim 14839  df-rlim 14840  df-sum 15037  df-prod 15254  df-fallfac 15355  df-ef 15415  df-sin 15417  df-cos 15418  df-tan 15419  df-pi 15420  df-struct 16479  df-ndx 16480  df-slot 16481  df-base 16483  df-sets 16484  df-ress 16485  df-plusg 16572  df-mulr 16573  df-starv 16574  df-sca 16575  df-vsca 16576  df-ip 16577  df-tset 16578  df-ple 16579  df-ds 16581  df-unif 16582  df-hom 16583  df-cco 16584  df-rest 16690  df-topn 16691  df-0g 16709  df-gsum 16710  df-topgen 16711  df-pt 16712  df-prds 16715  df-xrs 16769  df-qtop 16774  df-imas 16775  df-xps 16777  df-mre 16851  df-mrc 16852  df-acs 16854  df-mgm 17846  df-sgrp 17895  df-mnd 17906  df-submnd 17951  df-mulg 18220  df-cntz 18442  df-cmn 18903  df-psmet 20086  df-xmet 20087  df-met 20088  df-bl 20089  df-mopn 20090  df-fbas 20091  df-fg 20092  df-cnfld 20095  df-top 21506  df-topon 21523  df-topsp 21545  df-bases 21558  df-cld 21631  df-ntr 21632  df-cls 21633  df-nei 21710  df-lp 21748  df-perf 21749  df-cn 21839  df-cnp 21840  df-haus 21927  df-cmp 21999  df-tx 22174  df-hmeo 22367  df-fil 22458  df-fm 22550  df-flim 22551  df-flf 22552  df-xms 22934  df-ms 22935  df-tms 22936  df-cncf 23490  df-limc 24476  df-dv 24477  df-log 25155  df-cxp 25156  df-bcc 41056 This theorem is referenced by:  binomcxplemnotnn0  41075
 Copyright terms: Public domain W3C validator