Metamath Proof Explorer

Theorem binomcxplemdvbinom

Description: Lemma for binomcxp . By the power and chain rules, calculate the derivative of ( ( 1 + b ) ^c -u C ) , with respect to b in the disk of convergence D . We later multiply the derivative in the later binomcxplemdvsum by this derivative to show that ( ( 1 + b ) ^c C ) (with a nonnegated C ) and the later sum, since both at b = 0 equal one, are the same. (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 ⇝ } , ℝ* , < )
binomcxplem.e ⊢ 𝐸 = ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ ↦ ( ( 𝑘 · ( 𝐹 ‘ 𝑘 ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) ) )
binomcxplem.d ⊢ 𝐷 = ( ◡ abs “ ( 0 [,) 𝑅 ) )
Assertion binomcxplemdvbinom ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ℂ D ( 𝑏 ∈ 𝐷 ↦ ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) ) = ( 𝑏 ∈ 𝐷 ↦ ( - 𝐶 · ( ( 1 + 𝑏 ) ↑𝑐 ( - 𝐶 − 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 binomcxplem.e ⊢ 𝐸 = ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ ↦ ( ( 𝑘 · ( 𝐹 ‘ 𝑘 ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) ) )
9 binomcxplem.d ⊢ 𝐷 = ( ◡ abs “ ( 0 [,) 𝑅 ) )
10 nfcv ⊢ Ⅎ 𝑏 ◡ abs
11 nfcv ⊢ Ⅎ 𝑏 0
12 nfcv ⊢ Ⅎ 𝑏 [,)
13 nfcv ⊢ Ⅎ 𝑏 +
14 nfmpt1 ⊢ Ⅎ 𝑏 ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹 ‘ 𝑘 ) · ( 𝑏 ↑ 𝑘 ) ) ) )
15 6 14 nfcxfr ⊢ Ⅎ 𝑏 𝑆
16 nfcv ⊢ Ⅎ 𝑏 𝑟
17 15 16 nffv ⊢ Ⅎ 𝑏 ( 𝑆 ‘ 𝑟 )
18 11 13 17 nfseq ⊢ Ⅎ 𝑏 seq 0 ( + , ( 𝑆 ‘ 𝑟 ) )
19 18 nfel1 ⊢ Ⅎ 𝑏 seq 0 ( + , ( 𝑆 ‘ 𝑟 ) ) ∈ dom ⇝
20 nfcv ⊢ Ⅎ 𝑏 ℝ
21 19 20 nfrabw ⊢ Ⅎ 𝑏 { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑆 ‘ 𝑟 ) ) ∈ dom ⇝ }
22 nfcv ⊢ Ⅎ 𝑏 ℝ*
23 nfcv ⊢ Ⅎ 𝑏 <
24 21 22 23 nfsup ⊢ Ⅎ 𝑏 sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑆 ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < )
25 7 24 nfcxfr ⊢ Ⅎ 𝑏 𝑅
26 11 12 25 nfov ⊢ Ⅎ 𝑏 ( 0 [,) 𝑅 )
27 10 26 nfima ⊢ Ⅎ 𝑏 ( ◡ abs “ ( 0 [,) 𝑅 ) )
28 9 27 nfcxfr ⊢ Ⅎ 𝑏 𝐷
29 nfcv ⊢ Ⅎ 𝑦 𝐷
30 nfcv ⊢ Ⅎ 𝑦 ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 )
31 nfcv ⊢ Ⅎ 𝑏 ( ( 1 + 𝑦 ) ↑𝑐 - 𝐶 )
32 oveq2 ⊢ ( 𝑏 = 𝑦 → ( 1 + 𝑏 ) = ( 1 + 𝑦 ) )
33 32 oveq1d ⊢ ( 𝑏 = 𝑦 → ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) = ( ( 1 + 𝑦 ) ↑𝑐 - 𝐶 ) )
34 28 29 30 31 33 cbvmptf ⊢ ( 𝑏 ∈ 𝐷 ↦ ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) = ( 𝑦 ∈ 𝐷 ↦ ( ( 1 + 𝑦 ) ↑𝑐 - 𝐶 ) )
35 34 oveq2i ⊢ ( ℂ D ( 𝑏 ∈ 𝐷 ↦ ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) ) = ( ℂ D ( 𝑦 ∈ 𝐷 ↦ ( ( 1 + 𝑦 ) ↑𝑐 - 𝐶 ) ) )
36 cnelprrecn ⊢ ℂ ∈ { ℝ , ℂ }
37 36 a1i ⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ℂ ∈ { ℝ , ℂ } )
38 1cnd ⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑦 ∈ 𝐷 ) → 1 ∈ ℂ )
39 cnvimass ⊢ ( ◡ abs “ ( 0 [,) 𝑅 ) ) ⊆ dom abs
40 9 39 eqsstri ⊢ 𝐷 ⊆ dom abs
41 absf ⊢ abs : ℂ ⟶ ℝ
42 41 fdmi ⊢ dom abs = ℂ
43 40 42 sseqtri ⊢ 𝐷 ⊆ ℂ
44 43 a1i ⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → 𝐷 ⊆ ℂ )
45 44 sselda ⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑦 ∈ 𝐷 ) → 𝑦 ∈ ℂ )
46 38 45 addcld ⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑦 ∈ 𝐷 ) → ( 1 + 𝑦 ) ∈ ℂ )
47 simpr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑦 ∈ 𝐷 ) ∧ ( 1 + 𝑦 ) ∈ ℝ ) → ( 1 + 𝑦 ) ∈ ℝ )
48 1cnd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑦 ∈ 𝐷 ) ∧ ( 1 + 𝑦 ) ∈ ℝ ) → 1 ∈ ℂ )
49 45 adantr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑦 ∈ 𝐷 ) ∧ ( 1 + 𝑦 ) ∈ ℝ ) → 𝑦 ∈ ℂ )
50 48 49 pncan2d ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑦 ∈ 𝐷 ) ∧ ( 1 + 𝑦 ) ∈ ℝ ) → ( ( 1 + 𝑦 ) − 1 ) = 𝑦 )
51 1red ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑦 ∈ 𝐷 ) ∧ ( 1 + 𝑦 ) ∈ ℝ ) → 1 ∈ ℝ )
52 47 51 resubcld ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑦 ∈ 𝐷 ) ∧ ( 1 + 𝑦 ) ∈ ℝ ) → ( ( 1 + 𝑦 ) − 1 ) ∈ ℝ )
53 50 52 eqeltrrd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑦 ∈ 𝐷 ) ∧ ( 1 + 𝑦 ) ∈ ℝ ) → 𝑦 ∈ ℝ )
54 1pneg1e0 ⊢ ( 1 + - 1 ) = 0
55 1red ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ℝ ) → 1 ∈ ℝ )
56 55 renegcld ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ℝ ) → - 1 ∈ ℝ )
57 simpr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℝ )
58 ffn ⊢ ( abs : ℂ ⟶ ℝ → abs Fn ℂ )
59 elpreima ⊢ ( abs Fn ℂ → ( 𝑦 ∈ ( ◡ abs “ ( 0 [,) 𝑅 ) ) ↔ ( 𝑦 ∈ ℂ ∧ ( abs ‘ 𝑦 ) ∈ ( 0 [,) 𝑅 ) ) ) )
60 41 58 59 mp2b ⊢ ( 𝑦 ∈ ( ◡ abs “ ( 0 [,) 𝑅 ) ) ↔ ( 𝑦 ∈ ℂ ∧ ( abs ‘ 𝑦 ) ∈ ( 0 [,) 𝑅 ) ) )
61 60 simprbi ⊢ ( 𝑦 ∈ ( ◡ abs “ ( 0 [,) 𝑅 ) ) → ( abs ‘ 𝑦 ) ∈ ( 0 [,) 𝑅 ) )
62 61 9 eleq2s ⊢ ( 𝑦 ∈ 𝐷 → ( abs ‘ 𝑦 ) ∈ ( 0 [,) 𝑅 ) )
63 0re ⊢ 0 ∈ ℝ
64 ssrab2 ⊢ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑆 ‘ 𝑟 ) ) ∈ dom ⇝ } ⊆ ℝ
65 ressxr ⊢ ℝ ⊆ ℝ*
66 64 65 sstri ⊢ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑆 ‘ 𝑟 ) ) ∈ dom ⇝ } ⊆ ℝ*
67 supxrcl ⊢ ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑆 ‘ 𝑟 ) ) ∈ dom ⇝ } ⊆ ℝ* → sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑆 ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ℝ* )
68 66 67 ax-mp ⊢ sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑆 ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ℝ*
69 7 68 eqeltri ⊢ 𝑅 ∈ ℝ*
70 elico2 ⊢ ( ( 0 ∈ ℝ ∧ 𝑅 ∈ ℝ* ) → ( ( abs ‘ 𝑦 ) ∈ ( 0 [,) 𝑅 ) ↔ ( ( abs ‘ 𝑦 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝑦 ) ∧ ( abs ‘ 𝑦 ) < 𝑅 ) ) )
71 63 69 70 mp2an ⊢ ( ( abs ‘ 𝑦 ) ∈ ( 0 [,) 𝑅 ) ↔ ( ( abs ‘ 𝑦 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝑦 ) ∧ ( abs ‘ 𝑦 ) < 𝑅 ) )
72 62 71 sylib ⊢ ( 𝑦 ∈ 𝐷 → ( ( abs ‘ 𝑦 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝑦 ) ∧ ( abs ‘ 𝑦 ) < 𝑅 ) )
73 72 simp3d ⊢ ( 𝑦 ∈ 𝐷 → ( abs ‘ 𝑦 ) < 𝑅 )
74 73 adantl ⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑦 ∈ 𝐷 ) → ( abs ‘ 𝑦 ) < 𝑅 )
75 1 2 3 4 5 6 7 binomcxplemradcnv ⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → 𝑅 = 1 )
76 75 adantr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑦 ∈ 𝐷 ) → 𝑅 = 1 )
77 74 76 breqtrd ⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑦 ∈ 𝐷 ) → ( abs ‘ 𝑦 ) < 1 )
78 77 adantr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ℝ ) → ( abs ‘ 𝑦 ) < 1 )
79 57 55 absltd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ℝ ) → ( ( abs ‘ 𝑦 ) < 1 ↔ ( - 1 < 𝑦 ∧ 𝑦 < 1 ) ) )
80 78 79 mpbid ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ℝ ) → ( - 1 < 𝑦 ∧ 𝑦 < 1 ) )
81 80 simpld ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ℝ ) → - 1 < 𝑦 )
82 56 57 55 81 ltadd2dd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ℝ ) → ( 1 + - 1 ) < ( 1 + 𝑦 ) )
83 54 82 eqbrtrrid ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑦 ∈ ℝ ) → 0 < ( 1 + 𝑦 ) )
84 53 83 syldan ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑦 ∈ 𝐷 ) ∧ ( 1 + 𝑦 ) ∈ ℝ ) → 0 < ( 1 + 𝑦 ) )
85 47 84 elrpd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑦 ∈ 𝐷 ) ∧ ( 1 + 𝑦 ) ∈ ℝ ) → ( 1 + 𝑦 ) ∈ ℝ+ )
86 85 ex ⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑦 ∈ 𝐷 ) → ( ( 1 + 𝑦 ) ∈ ℝ → ( 1 + 𝑦 ) ∈ ℝ+ ) )
87 eqid ⊢ ( ℂ ∖ ( -∞ (,] 0 ) ) = ( ℂ ∖ ( -∞ (,] 0 ) )
88 87 ellogdm ⊢ ( ( 1 + 𝑦 ) ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↔ ( ( 1 + 𝑦 ) ∈ ℂ ∧ ( ( 1 + 𝑦 ) ∈ ℝ → ( 1 + 𝑦 ) ∈ ℝ+ ) ) )
89 46 86 88 sylanbrc ⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑦 ∈ 𝐷 ) → ( 1 + 𝑦 ) ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) )
90 eldifi ⊢ ( 𝑥 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) → 𝑥 ∈ ℂ )
91 90 adantl ⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑥 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ) → 𝑥 ∈ ℂ )
92 4 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → 𝐶 ∈ ℂ )
93 92 negcld ⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → - 𝐶 ∈ ℂ )
94 93 adantr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑥 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ) → - 𝐶 ∈ ℂ )
95 91 94 cxpcld ⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑥 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ) → ( 𝑥 ↑𝑐 - 𝐶 ) ∈ ℂ )
96 ovexd ⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑥 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ) → ( - 𝐶 · ( 𝑥 ↑𝑐 ( - 𝐶 − 1 ) ) ) ∈ V )
97 1cnd ⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑥 ∈ ℂ ) → 1 ∈ ℂ )
98 simpr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑥 ∈ ℂ ) → 𝑥 ∈ ℂ )
99 97 98 addcld ⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑥 ∈ ℂ ) → ( 1 + 𝑥 ) ∈ ℂ )
100 c0ex ⊢ 0 ∈ V
101 100 a1i ⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑥 ∈ ℂ ) → 0 ∈ V )
102 1cnd ⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → 1 ∈ ℂ )
103 37 102 dvmptc ⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ℂ D ( 𝑥 ∈ ℂ ↦ 1 ) ) = ( 𝑥 ∈ ℂ ↦ 0 ) )
104 37 dvmptid ⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ℂ D ( 𝑥 ∈ ℂ ↦ 𝑥 ) ) = ( 𝑥 ∈ ℂ ↦ 1 ) )
105 37 97 101 103 98 97 104 dvmptadd ⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 1 + 𝑥 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 0 + 1 ) ) )
106 0p1e1 ⊢ ( 0 + 1 ) = 1
107 106 mpteq2i ⊢ ( 𝑥 ∈ ℂ ↦ ( 0 + 1 ) ) = ( 𝑥 ∈ ℂ ↦ 1 )
108 105 107 eqtrdi ⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 1 + 𝑥 ) ) ) = ( 𝑥 ∈ ℂ ↦ 1 ) )
109 fvex ⊢ ( TopOpen ‘ ℂfld ) ∈ V
110 cnfldtps ⊢ ℂfld ∈ TopSp
111 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
112 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
113 111 112 tpsuni ⊢ ( ℂfld ∈ TopSp → ℂ = ∪ ( TopOpen ‘ ℂfld ) )
114 110 113 ax-mp ⊢ ℂ = ∪ ( TopOpen ‘ ℂfld )
115 114 restid ⊢ ( ( TopOpen ‘ ℂfld ) ∈ V → ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) = ( TopOpen ‘ ℂfld ) )
116 109 115 ax-mp ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) = ( TopOpen ‘ ℂfld )
117 116 eqcomi ⊢ ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
118 112 cnfldtop ⊢ ( TopOpen ‘ ℂfld ) ∈ Top
119 eqid ⊢ ( abs ∘ − ) = ( abs ∘ − )
120 119 cnbl0 ⊢ ( 𝑅 ∈ ℝ* → ( ◡ abs “ ( 0 [,) 𝑅 ) ) = ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) )
121 69 120 ax-mp ⊢ ( ◡ abs “ ( 0 [,) 𝑅 ) ) = ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 )
122 9 121 eqtri ⊢ 𝐷 = ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 )
123 cnxmet ⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
124 0cn ⊢ 0 ∈ ℂ
125 112 cnfldtopn ⊢ ( TopOpen ‘ ℂfld ) = ( MetOpen ‘ ( abs ∘ − ) )
126 125 blopn ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 0 ∈ ℂ ∧ 𝑅 ∈ ℝ* ) → ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ∈ ( TopOpen ‘ ℂfld ) )
127 123 124 69 126 mp3an ⊢ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ∈ ( TopOpen ‘ ℂfld )
128 122 127 eqeltri ⊢ 𝐷 ∈ ( TopOpen ‘ ℂfld )
129 isopn3i ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ Top ∧ 𝐷 ∈ ( TopOpen ‘ ℂfld ) ) → ( ( int ‘ ( TopOpen ‘ ℂfld ) ) ‘ 𝐷 ) = 𝐷 )
130 118 128 129 mp2an ⊢ ( ( int ‘ ( TopOpen ‘ ℂfld ) ) ‘ 𝐷 ) = 𝐷
131 130 a1i ⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ( int ‘ ( TopOpen ‘ ℂfld ) ) ‘ 𝐷 ) = 𝐷 )
132 37 99 97 108 44 117 112 131 dvmptres2 ⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ℂ D ( 𝑥 ∈ 𝐷 ↦ ( 1 + 𝑥 ) ) ) = ( 𝑥 ∈ 𝐷 ↦ 1 ) )
133 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 1 + 𝑥 ) = ( 1 + 𝑦 ) )
134 133 cbvmptv ⊢ ( 𝑥 ∈ 𝐷 ↦ ( 1 + 𝑥 ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 1 + 𝑦 ) )
135 134 oveq2i ⊢ ( ℂ D ( 𝑥 ∈ 𝐷 ↦ ( 1 + 𝑥 ) ) ) = ( ℂ D ( 𝑦 ∈ 𝐷 ↦ ( 1 + 𝑦 ) ) )
136 eqidd ⊢ ( 𝑥 = 𝑦 → 1 = 1 )
137 136 cbvmptv ⊢ ( 𝑥 ∈ 𝐷 ↦ 1 ) = ( 𝑦 ∈ 𝐷 ↦ 1 )
138 132 135 137 3eqtr3g ⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ℂ D ( 𝑦 ∈ 𝐷 ↦ ( 1 + 𝑦 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ 1 ) )
139 87 dvcncxp1 ⊢ ( - 𝐶 ∈ ℂ → ( ℂ D ( 𝑥 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( 𝑥 ↑𝑐 - 𝐶 ) ) ) = ( 𝑥 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( - 𝐶 · ( 𝑥 ↑𝑐 ( - 𝐶 − 1 ) ) ) ) )
140 93 139 syl ⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ℂ D ( 𝑥 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( 𝑥 ↑𝑐 - 𝐶 ) ) ) = ( 𝑥 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( - 𝐶 · ( 𝑥 ↑𝑐 ( - 𝐶 − 1 ) ) ) ) )
141 oveq1 ⊢ ( 𝑥 = ( 1 + 𝑦 ) → ( 𝑥 ↑𝑐 - 𝐶 ) = ( ( 1 + 𝑦 ) ↑𝑐 - 𝐶 ) )
142 oveq1 ⊢ ( 𝑥 = ( 1 + 𝑦 ) → ( 𝑥 ↑𝑐 ( - 𝐶 − 1 ) ) = ( ( 1 + 𝑦 ) ↑𝑐 ( - 𝐶 − 1 ) ) )
143 142 oveq2d ⊢ ( 𝑥 = ( 1 + 𝑦 ) → ( - 𝐶 · ( 𝑥 ↑𝑐 ( - 𝐶 − 1 ) ) ) = ( - 𝐶 · ( ( 1 + 𝑦 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) )
144 37 37 89 38 95 96 138 140 141 143 dvmptco ⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ℂ D ( 𝑦 ∈ 𝐷 ↦ ( ( 1 + 𝑦 ) ↑𝑐 - 𝐶 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( ( - 𝐶 · ( ( 1 + 𝑦 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) · 1 ) ) )
145 92 adantr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑦 ∈ 𝐷 ) → 𝐶 ∈ ℂ )
146 145 negcld ⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑦 ∈ 𝐷 ) → - 𝐶 ∈ ℂ )
147 146 38 subcld ⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑦 ∈ 𝐷 ) → ( - 𝐶 − 1 ) ∈ ℂ )
148 46 147 cxpcld ⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑦 ∈ 𝐷 ) → ( ( 1 + 𝑦 ) ↑𝑐 ( - 𝐶 − 1 ) ) ∈ ℂ )
149 146 148 mulcld ⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑦 ∈ 𝐷 ) → ( - 𝐶 · ( ( 1 + 𝑦 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) ∈ ℂ )
150 149 mulid1d ⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑦 ∈ 𝐷 ) → ( ( - 𝐶 · ( ( 1 + 𝑦 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) · 1 ) = ( - 𝐶 · ( ( 1 + 𝑦 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) )
151 150 mpteq2dva ⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( 𝑦 ∈ 𝐷 ↦ ( ( - 𝐶 · ( ( 1 + 𝑦 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) · 1 ) ) = ( 𝑦 ∈ 𝐷 ↦ ( - 𝐶 · ( ( 1 + 𝑦 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) ) )
152 nfcv ⊢ Ⅎ 𝑏 ( - 𝐶 · ( ( 1 + 𝑦 ) ↑𝑐 ( - 𝐶 − 1 ) ) )
153 nfcv ⊢ Ⅎ 𝑦 ( - 𝐶 · ( ( 1 + 𝑏 ) ↑𝑐 ( - 𝐶 − 1 ) ) )
154 oveq2 ⊢ ( 𝑦 = 𝑏 → ( 1 + 𝑦 ) = ( 1 + 𝑏 ) )
155 154 oveq1d ⊢ ( 𝑦 = 𝑏 → ( ( 1 + 𝑦 ) ↑𝑐 ( - 𝐶 − 1 ) ) = ( ( 1 + 𝑏 ) ↑𝑐 ( - 𝐶 − 1 ) ) )
156 155 oveq2d ⊢ ( 𝑦 = 𝑏 → ( - 𝐶 · ( ( 1 + 𝑦 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) = ( - 𝐶 · ( ( 1 + 𝑏 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) )
157 29 28 152 153 156 cbvmptf ⊢ ( 𝑦 ∈ 𝐷 ↦ ( - 𝐶 · ( ( 1 + 𝑦 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) ) = ( 𝑏 ∈ 𝐷 ↦ ( - 𝐶 · ( ( 1 + 𝑏 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) )
158 157 a1i ⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( 𝑦 ∈ 𝐷 ↦ ( - 𝐶 · ( ( 1 + 𝑦 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) ) = ( 𝑏 ∈ 𝐷 ↦ ( - 𝐶 · ( ( 1 + 𝑏 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) ) )
159 144 151 158 3eqtrd ⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ℂ D ( 𝑦 ∈ 𝐷 ↦ ( ( 1 + 𝑦 ) ↑𝑐 - 𝐶 ) ) ) = ( 𝑏 ∈ 𝐷 ↦ ( - 𝐶 · ( ( 1 + 𝑏 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) ) )
160 35 159 syl5eq ⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ℂ D ( 𝑏 ∈ 𝐷 ↦ ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) ) = ( 𝑏 ∈ 𝐷 ↦ ( - 𝐶 · ( ( 1 + 𝑏 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) ) )