Metamath Proof Explorer


Theorem binomcxplemnotnn0

Description: Lemma for binomcxp . When C is not a nonnegative integer, the generalized sum in binomcxplemnn0 —which we will call P —is a convergent power series: its base b is always of smaller absolute value than the radius of convergence.

pserdv2 gives the derivative of P , which by dvradcnv also converges in that radius. When A is fixed at one, ( A + b ) times that derivative equals ( C x. P ) and fraction ( P / ( ( A + b ) ^c C ) ) is always defined with derivative zero, so the fraction is a constant—specifically one, because ( ( 1 + 0 ) ^c C ) = 1 . Thus ( ( 1 + b ) ^c C ) = ( Pb ) .

Finally, let b be ( B / A ) , and multiply both the binomial ( ( 1 + ( B / A ) ) ^c C ) and the sum ( P( B / A ) ) by ( A ^c C ) to get the result. (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 [,) 𝑅 ) )
binomcxplem.p 𝑃 = ( 𝑏𝐷 ↦ Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) )
Assertion binomcxplemnotnn0 ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ( 𝐴 + 𝐵 ) ↑𝑐 𝐶 ) = Σ 𝑘 ∈ ℕ0 ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐴𝑐 ( 𝐶𝑘 ) ) · ( 𝐵𝑘 ) ) ) )

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 binomcxplem.p 𝑃 = ( 𝑏𝐷 ↦ Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) )
11 nfcv 𝑏 abs
12 nfcv 𝑏 0
13 nfcv 𝑏 [,)
14 nfcv 𝑏 +
15 nfmpt1 𝑏 ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹𝑘 ) · ( 𝑏𝑘 ) ) ) )
16 6 15 nfcxfr 𝑏 𝑆
17 nfcv 𝑏 𝑟
18 16 17 nffv 𝑏 ( 𝑆𝑟 )
19 12 14 18 nfseq 𝑏 seq 0 ( + , ( 𝑆𝑟 ) )
20 19 nfel1 𝑏 seq 0 ( + , ( 𝑆𝑟 ) ) ∈ dom ⇝
21 nfcv 𝑏
22 20 21 nfrabw 𝑏 { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑆𝑟 ) ) ∈ dom ⇝ }
23 nfcv 𝑏*
24 nfcv 𝑏 <
25 22 23 24 nfsup 𝑏 sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑆𝑟 ) ) ∈ dom ⇝ } , ℝ* , < )
26 7 25 nfcxfr 𝑏 𝑅
27 12 13 26 nfov 𝑏 ( 0 [,) 𝑅 )
28 11 27 nfima 𝑏 ( abs “ ( 0 [,) 𝑅 ) )
29 9 28 nfcxfr 𝑏 𝐷
30 nfcv 𝑥 𝐷
31 nfcv 𝑥 Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 )
32 nfcv 𝑏0
33 nfcv 𝑏 𝑥
34 16 33 nffv 𝑏 ( 𝑆𝑥 )
35 nfcv 𝑏 𝑘
36 34 35 nffv 𝑏 ( ( 𝑆𝑥 ) ‘ 𝑘 )
37 32 36 nfsum 𝑏 Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑥 ) ‘ 𝑘 )
38 simpl ( ( 𝑏 = 𝑥𝑘 ∈ ℕ0 ) → 𝑏 = 𝑥 )
39 38 fveq2d ( ( 𝑏 = 𝑥𝑘 ∈ ℕ0 ) → ( 𝑆𝑏 ) = ( 𝑆𝑥 ) )
40 39 fveq1d ( ( 𝑏 = 𝑥𝑘 ∈ ℕ0 ) → ( ( 𝑆𝑏 ) ‘ 𝑘 ) = ( ( 𝑆𝑥 ) ‘ 𝑘 ) )
41 40 sumeq2dv ( 𝑏 = 𝑥 → Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) = Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑥 ) ‘ 𝑘 ) )
42 29 30 31 37 41 cbvmptf ( 𝑏𝐷 ↦ Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) ) = ( 𝑥𝐷 ↦ Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑥 ) ‘ 𝑘 ) )
43 10 42 eqtri 𝑃 = ( 𝑥𝐷 ↦ Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑥 ) ‘ 𝑘 ) )
44 43 a1i ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → 𝑃 = ( 𝑥𝐷 ↦ Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑥 ) ‘ 𝑘 ) ) )
45 simplr ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑥 = ( 𝐵 / 𝐴 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑥 = ( 𝐵 / 𝐴 ) )
46 45 fveq2d ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑥 = ( 𝐵 / 𝐴 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑆𝑥 ) = ( 𝑆 ‘ ( 𝐵 / 𝐴 ) ) )
47 46 fveq1d ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑥 = ( 𝐵 / 𝐴 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆𝑥 ) ‘ 𝑘 ) = ( ( 𝑆 ‘ ( 𝐵 / 𝐴 ) ) ‘ 𝑘 ) )
48 47 sumeq2dv ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑥 = ( 𝐵 / 𝐴 ) ) → Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑥 ) ‘ 𝑘 ) = Σ 𝑘 ∈ ℕ0 ( ( 𝑆 ‘ ( 𝐵 / 𝐴 ) ) ‘ 𝑘 ) )
49 2 recnd ( 𝜑𝐵 ∈ ℂ )
50 49 adantr ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → 𝐵 ∈ ℂ )
51 1 rpcnd ( 𝜑𝐴 ∈ ℂ )
52 51 adantr ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → 𝐴 ∈ ℂ )
53 0red ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → 0 ∈ ℝ )
54 50 abscld ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( abs ‘ 𝐵 ) ∈ ℝ )
55 52 abscld ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( abs ‘ 𝐴 ) ∈ ℝ )
56 50 absge0d ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → 0 ≤ ( abs ‘ 𝐵 ) )
57 3 adantr ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( abs ‘ 𝐵 ) < ( abs ‘ 𝐴 ) )
58 53 54 55 56 57 lelttrd ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → 0 < ( abs ‘ 𝐴 ) )
59 58 gt0ne0d ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( abs ‘ 𝐴 ) ≠ 0 )
60 52 abs00ad ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ( abs ‘ 𝐴 ) = 0 ↔ 𝐴 = 0 ) )
61 60 necon3bid ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ( abs ‘ 𝐴 ) ≠ 0 ↔ 𝐴 ≠ 0 ) )
62 59 61 mpbid ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → 𝐴 ≠ 0 )
63 50 52 62 divcld ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( 𝐵 / 𝐴 ) ∈ ℂ )
64 63 abscld ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( abs ‘ ( 𝐵 / 𝐴 ) ) ∈ ℝ )
65 63 absge0d ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → 0 ≤ ( abs ‘ ( 𝐵 / 𝐴 ) ) )
66 55 recnd ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( abs ‘ 𝐴 ) ∈ ℂ )
67 66 mulid1d ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ( abs ‘ 𝐴 ) · 1 ) = ( abs ‘ 𝐴 ) )
68 57 67 breqtrrd ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( abs ‘ 𝐵 ) < ( ( abs ‘ 𝐴 ) · 1 ) )
69 1red ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → 1 ∈ ℝ )
70 55 58 elrpd ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( abs ‘ 𝐴 ) ∈ ℝ+ )
71 54 69 70 ltdivmuld ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ( ( abs ‘ 𝐵 ) / ( abs ‘ 𝐴 ) ) < 1 ↔ ( abs ‘ 𝐵 ) < ( ( abs ‘ 𝐴 ) · 1 ) ) )
72 68 71 mpbird ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ( abs ‘ 𝐵 ) / ( abs ‘ 𝐴 ) ) < 1 )
73 50 52 62 absdivd ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( abs ‘ ( 𝐵 / 𝐴 ) ) = ( ( abs ‘ 𝐵 ) / ( abs ‘ 𝐴 ) ) )
74 1 2 3 4 5 6 7 binomcxplemradcnv ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → 𝑅 = 1 )
75 72 73 74 3brtr4d ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( abs ‘ ( 𝐵 / 𝐴 ) ) < 𝑅 )
76 0re 0 ∈ ℝ
77 ssrab2 { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑆𝑟 ) ) ∈ dom ⇝ } ⊆ ℝ
78 ressxr ℝ ⊆ ℝ*
79 77 78 sstri { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑆𝑟 ) ) ∈ dom ⇝ } ⊆ ℝ*
80 supxrcl ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑆𝑟 ) ) ∈ dom ⇝ } ⊆ ℝ* → sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑆𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ℝ* )
81 79 80 ax-mp sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝑆𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ℝ*
82 7 81 eqeltri 𝑅 ∈ ℝ*
83 elico2 ( ( 0 ∈ ℝ ∧ 𝑅 ∈ ℝ* ) → ( ( abs ‘ ( 𝐵 / 𝐴 ) ) ∈ ( 0 [,) 𝑅 ) ↔ ( ( abs ‘ ( 𝐵 / 𝐴 ) ) ∈ ℝ ∧ 0 ≤ ( abs ‘ ( 𝐵 / 𝐴 ) ) ∧ ( abs ‘ ( 𝐵 / 𝐴 ) ) < 𝑅 ) ) )
84 76 82 83 mp2an ( ( abs ‘ ( 𝐵 / 𝐴 ) ) ∈ ( 0 [,) 𝑅 ) ↔ ( ( abs ‘ ( 𝐵 / 𝐴 ) ) ∈ ℝ ∧ 0 ≤ ( abs ‘ ( 𝐵 / 𝐴 ) ) ∧ ( abs ‘ ( 𝐵 / 𝐴 ) ) < 𝑅 ) )
85 64 65 75 84 syl3anbrc ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( abs ‘ ( 𝐵 / 𝐴 ) ) ∈ ( 0 [,) 𝑅 ) )
86 9 eleq2i ( ( 𝐵 / 𝐴 ) ∈ 𝐷 ↔ ( 𝐵 / 𝐴 ) ∈ ( abs “ ( 0 [,) 𝑅 ) ) )
87 absf abs : ℂ ⟶ ℝ
88 ffn ( abs : ℂ ⟶ ℝ → abs Fn ℂ )
89 elpreima ( abs Fn ℂ → ( ( 𝐵 / 𝐴 ) ∈ ( abs “ ( 0 [,) 𝑅 ) ) ↔ ( ( 𝐵 / 𝐴 ) ∈ ℂ ∧ ( abs ‘ ( 𝐵 / 𝐴 ) ) ∈ ( 0 [,) 𝑅 ) ) ) )
90 87 88 89 mp2b ( ( 𝐵 / 𝐴 ) ∈ ( abs “ ( 0 [,) 𝑅 ) ) ↔ ( ( 𝐵 / 𝐴 ) ∈ ℂ ∧ ( abs ‘ ( 𝐵 / 𝐴 ) ) ∈ ( 0 [,) 𝑅 ) ) )
91 86 90 bitri ( ( 𝐵 / 𝐴 ) ∈ 𝐷 ↔ ( ( 𝐵 / 𝐴 ) ∈ ℂ ∧ ( abs ‘ ( 𝐵 / 𝐴 ) ) ∈ ( 0 [,) 𝑅 ) ) )
92 63 85 91 sylanbrc ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( 𝐵 / 𝐴 ) ∈ 𝐷 )
93 sumex Σ 𝑘 ∈ ℕ0 ( ( 𝑆 ‘ ( 𝐵 / 𝐴 ) ) ‘ 𝑘 ) ∈ V
94 93 a1i ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → Σ 𝑘 ∈ ℕ0 ( ( 𝑆 ‘ ( 𝐵 / 𝐴 ) ) ‘ 𝑘 ) ∈ V )
95 44 48 92 94 fvmptd ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( 𝑃 ‘ ( 𝐵 / 𝐴 ) ) = Σ 𝑘 ∈ ℕ0 ( ( 𝑆 ‘ ( 𝐵 / 𝐴 ) ) ‘ 𝑘 ) )
96 eqid ( abs ∘ − ) = ( abs ∘ − )
97 96 cnbl0 ( 𝑅 ∈ ℝ* → ( abs “ ( 0 [,) 𝑅 ) ) = ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) )
98 82 97 ax-mp ( abs “ ( 0 [,) 𝑅 ) ) = ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 )
99 9 98 eqtri 𝐷 = ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 )
100 0cnd ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → 0 ∈ ℂ )
101 82 a1i ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → 𝑅 ∈ ℝ* )
102 mulcl ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 · 𝑦 ) ∈ ℂ )
103 102 adantl ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → ( 𝑥 · 𝑦 ) ∈ ℂ )
104 nfv 𝑏 ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 )
105 29 nfcri 𝑏 𝑥𝐷
106 104 105 nfan 𝑏 ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑥𝐷 )
107 37 nfel1 𝑏 Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑥 ) ‘ 𝑘 ) ∈ ℂ
108 106 107 nfim 𝑏 ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑥𝐷 ) → Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑥 ) ‘ 𝑘 ) ∈ ℂ )
109 eleq1 ( 𝑏 = 𝑥 → ( 𝑏𝐷𝑥𝐷 ) )
110 109 anbi2d ( 𝑏 = 𝑥 → ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ↔ ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑥𝐷 ) ) )
111 41 eleq1d ( 𝑏 = 𝑥 → ( Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) ∈ ℂ ↔ Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑥 ) ‘ 𝑘 ) ∈ ℂ ) )
112 110 111 imbi12d ( 𝑏 = 𝑥 → ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) ∈ ℂ ) ↔ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑥𝐷 ) → Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑥 ) ‘ 𝑘 ) ∈ ℂ ) ) )
113 nn0uz 0 = ( ℤ ‘ 0 )
114 0zd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → 0 ∈ ℤ )
115 eqidd ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆𝑏 ) ‘ 𝑘 ) = ( ( 𝑆𝑏 ) ‘ 𝑘 ) )
116 cnvimass ( abs “ ( 0 [,) 𝑅 ) ) ⊆ dom abs
117 9 116 eqsstri 𝐷 ⊆ dom abs
118 87 fdmi dom abs = ℂ
119 117 118 sseqtri 𝐷 ⊆ ℂ
120 119 sseli ( 𝑏𝐷𝑏 ∈ ℂ )
121 6 a1i ( 𝜑𝑆 = ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹𝑘 ) · ( 𝑏𝑘 ) ) ) ) )
122 nn0ex 0 ∈ V
123 122 mptex ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹𝑘 ) · ( 𝑏𝑘 ) ) ) ∈ V
124 123 a1i ( ( 𝜑𝑏 ∈ ℂ ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹𝑘 ) · ( 𝑏𝑘 ) ) ) ∈ V )
125 121 124 fvmpt2d ( ( 𝜑𝑏 ∈ ℂ ) → ( 𝑆𝑏 ) = ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹𝑘 ) · ( 𝑏𝑘 ) ) ) )
126 ovexd ( ( ( 𝜑𝑏 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐹𝑘 ) · ( 𝑏𝑘 ) ) ∈ V )
127 125 126 fvmpt2d ( ( ( 𝜑𝑏 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆𝑏 ) ‘ 𝑘 ) = ( ( 𝐹𝑘 ) · ( 𝑏𝑘 ) ) )
128 5 a1i ( ( 𝜑𝑘 ∈ ℕ0 ) → 𝐹 = ( 𝑗 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑗 ) ) )
129 simpr ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ 𝑗 = 𝑘 ) → 𝑗 = 𝑘 )
130 129 oveq2d ( ( ( 𝜑𝑘 ∈ ℕ0 ) ∧ 𝑗 = 𝑘 ) → ( 𝐶 C𝑐 𝑗 ) = ( 𝐶 C𝑐 𝑘 ) )
131 simpr ( ( 𝜑𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
132 ovexd ( ( 𝜑𝑘 ∈ ℕ0 ) → ( 𝐶 C𝑐 𝑘 ) ∈ V )
133 128 130 131 132 fvmptd ( ( 𝜑𝑘 ∈ ℕ0 ) → ( 𝐹𝑘 ) = ( 𝐶 C𝑐 𝑘 ) )
134 133 oveq1d ( ( 𝜑𝑘 ∈ ℕ0 ) → ( ( 𝐹𝑘 ) · ( 𝑏𝑘 ) ) = ( ( 𝐶 C𝑐 𝑘 ) · ( 𝑏𝑘 ) ) )
135 134 adantlr ( ( ( 𝜑𝑏 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐹𝑘 ) · ( 𝑏𝑘 ) ) = ( ( 𝐶 C𝑐 𝑘 ) · ( 𝑏𝑘 ) ) )
136 127 135 eqtrd ( ( ( 𝜑𝑏 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆𝑏 ) ‘ 𝑘 ) = ( ( 𝐶 C𝑐 𝑘 ) · ( 𝑏𝑘 ) ) )
137 120 136 sylanl2 ( ( ( 𝜑𝑏𝐷 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆𝑏 ) ‘ 𝑘 ) = ( ( 𝐶 C𝑐 𝑘 ) · ( 𝑏𝑘 ) ) )
138 4 ad2antrr ( ( ( 𝜑𝑏𝐷 ) ∧ 𝑘 ∈ ℕ0 ) → 𝐶 ∈ ℂ )
139 simpr ( ( ( 𝜑𝑏𝐷 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
140 138 139 bcccl ( ( ( 𝜑𝑏𝐷 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐶 C𝑐 𝑘 ) ∈ ℂ )
141 120 ad2antlr ( ( ( 𝜑𝑏𝐷 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑏 ∈ ℂ )
142 141 139 expcld ( ( ( 𝜑𝑏𝐷 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑏𝑘 ) ∈ ℂ )
143 140 142 mulcld ( ( ( 𝜑𝑏𝐷 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐶 C𝑐 𝑘 ) · ( 𝑏𝑘 ) ) ∈ ℂ )
144 137 143 eqeltrd ( ( ( 𝜑𝑏𝐷 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆𝑏 ) ‘ 𝑘 ) ∈ ℂ )
145 144 adantllr ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆𝑏 ) ‘ 𝑘 ) ∈ ℂ )
146 eleq1 ( 𝑥 = 𝑏 → ( 𝑥𝐷𝑏𝐷 ) )
147 146 anbi2d ( 𝑥 = 𝑏 → ( ( 𝜑𝑥𝐷 ) ↔ ( 𝜑𝑏𝐷 ) ) )
148 fveq2 ( 𝑥 = 𝑏 → ( 𝑆𝑥 ) = ( 𝑆𝑏 ) )
149 148 seqeq3d ( 𝑥 = 𝑏 → seq 0 ( + , ( 𝑆𝑥 ) ) = seq 0 ( + , ( 𝑆𝑏 ) ) )
150 149 eleq1d ( 𝑥 = 𝑏 → ( seq 0 ( + , ( 𝑆𝑥 ) ) ∈ dom ⇝ ↔ seq 0 ( + , ( 𝑆𝑏 ) ) ∈ dom ⇝ ) )
151 fveq2 ( 𝑥 = 𝑏 → ( 𝐸𝑥 ) = ( 𝐸𝑏 ) )
152 151 seqeq3d ( 𝑥 = 𝑏 → seq 1 ( + , ( 𝐸𝑥 ) ) = seq 1 ( + , ( 𝐸𝑏 ) ) )
153 152 eleq1d ( 𝑥 = 𝑏 → ( seq 1 ( + , ( 𝐸𝑥 ) ) ∈ dom ⇝ ↔ seq 1 ( + , ( 𝐸𝑏 ) ) ∈ dom ⇝ ) )
154 150 153 anbi12d ( 𝑥 = 𝑏 → ( ( seq 0 ( + , ( 𝑆𝑥 ) ) ∈ dom ⇝ ∧ seq 1 ( + , ( 𝐸𝑥 ) ) ∈ dom ⇝ ) ↔ ( seq 0 ( + , ( 𝑆𝑏 ) ) ∈ dom ⇝ ∧ seq 1 ( + , ( 𝐸𝑏 ) ) ∈ dom ⇝ ) ) )
155 147 154 imbi12d ( 𝑥 = 𝑏 → ( ( ( 𝜑𝑥𝐷 ) → ( seq 0 ( + , ( 𝑆𝑥 ) ) ∈ dom ⇝ ∧ seq 1 ( + , ( 𝐸𝑥 ) ) ∈ dom ⇝ ) ) ↔ ( ( 𝜑𝑏𝐷 ) → ( seq 0 ( + , ( 𝑆𝑏 ) ) ∈ dom ⇝ ∧ seq 1 ( + , ( 𝐸𝑏 ) ) ∈ dom ⇝ ) ) ) )
156 1 2 3 4 5 6 7 8 9 binomcxplemcvg ( ( 𝜑𝑥𝐷 ) → ( seq 0 ( + , ( 𝑆𝑥 ) ) ∈ dom ⇝ ∧ seq 1 ( + , ( 𝐸𝑥 ) ) ∈ dom ⇝ ) )
157 155 156 chvarvv ( ( 𝜑𝑏𝐷 ) → ( seq 0 ( + , ( 𝑆𝑏 ) ) ∈ dom ⇝ ∧ seq 1 ( + , ( 𝐸𝑏 ) ) ∈ dom ⇝ ) )
158 157 simpld ( ( 𝜑𝑏𝐷 ) → seq 0 ( + , ( 𝑆𝑏 ) ) ∈ dom ⇝ )
159 158 adantlr ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → seq 0 ( + , ( 𝑆𝑏 ) ) ∈ dom ⇝ )
160 113 114 115 145 159 isumcl ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) ∈ ℂ )
161 108 112 160 chvarfv ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑥𝐷 ) → Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑥 ) ‘ 𝑘 ) ∈ ℂ )
162 161 43 fmptd ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → 𝑃 : 𝐷 ⟶ ℂ )
163 1cnd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑥𝐷 ) → 1 ∈ ℂ )
164 119 sseli ( 𝑥𝐷𝑥 ∈ ℂ )
165 164 adantl ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑥𝐷 ) → 𝑥 ∈ ℂ )
166 163 165 addcld ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑥𝐷 ) → ( 1 + 𝑥 ) ∈ ℂ )
167 4 ad2antrr ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑥𝐷 ) → 𝐶 ∈ ℂ )
168 167 negcld ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑥𝐷 ) → - 𝐶 ∈ ℂ )
169 166 168 cxpcld ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑥𝐷 ) → ( ( 1 + 𝑥 ) ↑𝑐 - 𝐶 ) ∈ ℂ )
170 nfcv 𝑥 ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 )
171 nfcv 𝑏 ( ( 1 + 𝑥 ) ↑𝑐 - 𝐶 )
172 oveq2 ( 𝑏 = 𝑥 → ( 1 + 𝑏 ) = ( 1 + 𝑥 ) )
173 172 oveq1d ( 𝑏 = 𝑥 → ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) = ( ( 1 + 𝑥 ) ↑𝑐 - 𝐶 ) )
174 29 30 170 171 173 cbvmptf ( 𝑏𝐷 ↦ ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) = ( 𝑥𝐷 ↦ ( ( 1 + 𝑥 ) ↑𝑐 - 𝐶 ) )
175 169 174 fmptd ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( 𝑏𝐷 ↦ ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) : 𝐷 ⟶ ℂ )
176 cnex ℂ ∈ V
177 fex ( ( abs : ℂ ⟶ ℝ ∧ ℂ ∈ V ) → abs ∈ V )
178 87 176 177 mp2an abs ∈ V
179 178 cnvex abs ∈ V
180 imaexg ( abs ∈ V → ( abs “ ( 0 [,) 𝑅 ) ) ∈ V )
181 179 180 ax-mp ( abs “ ( 0 [,) 𝑅 ) ) ∈ V
182 9 181 eqeltri 𝐷 ∈ V
183 182 a1i ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → 𝐷 ∈ V )
184 inidm ( 𝐷𝐷 ) = 𝐷
185 103 162 175 183 183 184 off ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( 𝑃f · ( 𝑏𝐷 ↦ ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) ) : 𝐷 ⟶ ℂ )
186 1ex 1 ∈ V
187 186 fconst ( 𝐷 × { 1 } ) : 𝐷 ⟶ { 1 }
188 fconstmpt ( 𝐷 × { 1 } ) = ( 𝑥𝐷 ↦ 1 )
189 nfcv 𝑏 1
190 nfcv 𝑥 1
191 eqidd ( 𝑥 = 𝑏 → 1 = 1 )
192 30 29 189 190 191 cbvmptf ( 𝑥𝐷 ↦ 1 ) = ( 𝑏𝐷 ↦ 1 )
193 188 192 eqtri ( 𝐷 × { 1 } ) = ( 𝑏𝐷 ↦ 1 )
194 193 feq1i ( ( 𝐷 × { 1 } ) : 𝐷 ⟶ { 1 } ↔ ( 𝑏𝐷 ↦ 1 ) : 𝐷 ⟶ { 1 } )
195 187 194 mpbi ( 𝑏𝐷 ↦ 1 ) : 𝐷 ⟶ { 1 }
196 ax-1cn 1 ∈ ℂ
197 snssi ( 1 ∈ ℂ → { 1 } ⊆ ℂ )
198 196 197 ax-mp { 1 } ⊆ ℂ
199 fss ( ( ( 𝑏𝐷 ↦ 1 ) : 𝐷 ⟶ { 1 } ∧ { 1 } ⊆ ℂ ) → ( 𝑏𝐷 ↦ 1 ) : 𝐷 ⟶ ℂ )
200 195 198 199 mp2an ( 𝑏𝐷 ↦ 1 ) : 𝐷 ⟶ ℂ
201 200 a1i ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( 𝑏𝐷 ↦ 1 ) : 𝐷 ⟶ ℂ )
202 cnelprrecn ℂ ∈ { ℝ , ℂ }
203 202 a1i ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ℂ ∈ { ℝ , ℂ } )
204 1 2 3 4 5 6 7 8 9 10 binomcxplemdvsum ( 𝜑 → ( ℂ D 𝑃 ) = ( 𝑏𝐷 ↦ Σ 𝑘 ∈ ℕ ( ( 𝐸𝑏 ) ‘ 𝑘 ) ) )
205 204 adantr ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ℂ D 𝑃 ) = ( 𝑏𝐷 ↦ Σ 𝑘 ∈ ℕ ( ( 𝐸𝑏 ) ‘ 𝑘 ) ) )
206 nfcv 𝑥 Σ 𝑘 ∈ ℕ ( ( 𝐸𝑏 ) ‘ 𝑘 )
207 nfcv 𝑏
208 nfmpt1 𝑏 ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ ↦ ( ( 𝑘 · ( 𝐹𝑘 ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) ) )
209 8 208 nfcxfr 𝑏 𝐸
210 209 33 nffv 𝑏 ( 𝐸𝑥 )
211 210 35 nffv 𝑏 ( ( 𝐸𝑥 ) ‘ 𝑘 )
212 207 211 nfsum 𝑏 Σ 𝑘 ∈ ℕ ( ( 𝐸𝑥 ) ‘ 𝑘 )
213 simpl ( ( 𝑏 = 𝑥𝑘 ∈ ℕ ) → 𝑏 = 𝑥 )
214 213 fveq2d ( ( 𝑏 = 𝑥𝑘 ∈ ℕ ) → ( 𝐸𝑏 ) = ( 𝐸𝑥 ) )
215 214 fveq1d ( ( 𝑏 = 𝑥𝑘 ∈ ℕ ) → ( ( 𝐸𝑏 ) ‘ 𝑘 ) = ( ( 𝐸𝑥 ) ‘ 𝑘 ) )
216 215 sumeq2dv ( 𝑏 = 𝑥 → Σ 𝑘 ∈ ℕ ( ( 𝐸𝑏 ) ‘ 𝑘 ) = Σ 𝑘 ∈ ℕ ( ( 𝐸𝑥 ) ‘ 𝑘 ) )
217 29 30 206 212 216 cbvmptf ( 𝑏𝐷 ↦ Σ 𝑘 ∈ ℕ ( ( 𝐸𝑏 ) ‘ 𝑘 ) ) = ( 𝑥𝐷 ↦ Σ 𝑘 ∈ ℕ ( ( 𝐸𝑥 ) ‘ 𝑘 ) )
218 205 217 eqtrdi ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ℂ D 𝑃 ) = ( 𝑥𝐷 ↦ Σ 𝑘 ∈ ℕ ( ( 𝐸𝑥 ) ‘ 𝑘 ) ) )
219 sumex Σ 𝑘 ∈ ℕ ( ( 𝐸𝑥 ) ‘ 𝑘 ) ∈ V
220 219 a1i ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑥𝐷 ) → Σ 𝑘 ∈ ℕ ( ( 𝐸𝑥 ) ‘ 𝑘 ) ∈ V )
221 218 220 fmpt3d ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ℂ D 𝑃 ) : 𝐷 ⟶ V )
222 221 fdmd ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → dom ( ℂ D 𝑃 ) = 𝐷 )
223 1 2 3 4 5 6 7 8 9 binomcxplemdvbinom ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ℂ D ( 𝑏𝐷 ↦ ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) ) = ( 𝑏𝐷 ↦ ( - 𝐶 · ( ( 1 + 𝑏 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) ) )
224 nfcv 𝑥 ( - 𝐶 · ( ( 1 + 𝑏 ) ↑𝑐 ( - 𝐶 − 1 ) ) )
225 nfcv 𝑏 ( - 𝐶 · ( ( 1 + 𝑥 ) ↑𝑐 ( - 𝐶 − 1 ) ) )
226 172 oveq1d ( 𝑏 = 𝑥 → ( ( 1 + 𝑏 ) ↑𝑐 ( - 𝐶 − 1 ) ) = ( ( 1 + 𝑥 ) ↑𝑐 ( - 𝐶 − 1 ) ) )
227 226 oveq2d ( 𝑏 = 𝑥 → ( - 𝐶 · ( ( 1 + 𝑏 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) = ( - 𝐶 · ( ( 1 + 𝑥 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) )
228 29 30 224 225 227 cbvmptf ( 𝑏𝐷 ↦ ( - 𝐶 · ( ( 1 + 𝑏 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) ) = ( 𝑥𝐷 ↦ ( - 𝐶 · ( ( 1 + 𝑥 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) )
229 223 228 eqtrdi ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ℂ D ( 𝑏𝐷 ↦ ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) ) = ( 𝑥𝐷 ↦ ( - 𝐶 · ( ( 1 + 𝑥 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) ) )
230 168 163 subcld ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑥𝐷 ) → ( - 𝐶 − 1 ) ∈ ℂ )
231 166 230 cxpcld ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑥𝐷 ) → ( ( 1 + 𝑥 ) ↑𝑐 ( - 𝐶 − 1 ) ) ∈ ℂ )
232 168 231 mulcld ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑥𝐷 ) → ( - 𝐶 · ( ( 1 + 𝑥 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) ∈ ℂ )
233 229 232 fmpt3d ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ℂ D ( 𝑏𝐷 ↦ ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) ) : 𝐷 ⟶ ℂ )
234 233 fdmd ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → dom ( ℂ D ( 𝑏𝐷 ↦ ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) ) = 𝐷 )
235 203 162 175 222 234 dvmulf ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ℂ D ( 𝑃f · ( 𝑏𝐷 ↦ ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) ) ) = ( ( ( ℂ D 𝑃 ) ∘f · ( 𝑏𝐷 ↦ ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) ) ∘f + ( ( ℂ D ( 𝑏𝐷 ↦ ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) ) ∘f · 𝑃 ) ) )
236 4 ad2antrr ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → 𝐶 ∈ ℂ )
237 236 mulid1d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( 𝐶 · 1 ) = 𝐶 )
238 237 oveq1d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( 𝐶 · 1 ) + ( 𝐶 · Σ 𝑘 ∈ ℕ ( ( 𝐶 C𝑐 𝑘 ) · ( 𝑏𝑘 ) ) ) ) = ( 𝐶 + ( 𝐶 · Σ 𝑘 ∈ ℕ ( ( 𝐶 C𝑐 𝑘 ) · ( 𝑏𝑘 ) ) ) ) )
239 1cnd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → 1 ∈ ℂ )
240 nnuz ℕ = ( ℤ ‘ 1 )
241 1zzd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → 1 ∈ ℤ )
242 nnnn0 ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ0 )
243 242 137 sylan2 ( ( ( 𝜑𝑏𝐷 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑆𝑏 ) ‘ 𝑘 ) = ( ( 𝐶 C𝑐 𝑘 ) · ( 𝑏𝑘 ) ) )
244 243 adantllr ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑆𝑏 ) ‘ 𝑘 ) = ( ( 𝐶 C𝑐 𝑘 ) · ( 𝑏𝑘 ) ) )
245 4 ad3antrrr ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ0 ) → 𝐶 ∈ ℂ )
246 simpr ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
247 245 246 bcccl ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐶 C𝑐 𝑘 ) ∈ ℂ )
248 242 247 sylan2 ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ ) → ( 𝐶 C𝑐 𝑘 ) ∈ ℂ )
249 120 adantl ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → 𝑏 ∈ ℂ )
250 249 adantr ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑏 ∈ ℂ )
251 250 246 expcld ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑏𝑘 ) ∈ ℂ )
252 242 251 sylan2 ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ ) → ( 𝑏𝑘 ) ∈ ℂ )
253 248 252 mulcld ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝐶 C𝑐 𝑘 ) · ( 𝑏𝑘 ) ) ∈ ℂ )
254 1nn0 1 ∈ ℕ0
255 254 a1i ( ( 𝜑𝑏𝐷 ) → 1 ∈ ℕ0 )
256 113 255 144 iserex ( ( 𝜑𝑏𝐷 ) → ( seq 0 ( + , ( 𝑆𝑏 ) ) ∈ dom ⇝ ↔ seq 1 ( + , ( 𝑆𝑏 ) ) ∈ dom ⇝ ) )
257 158 256 mpbid ( ( 𝜑𝑏𝐷 ) → seq 1 ( + , ( 𝑆𝑏 ) ) ∈ dom ⇝ )
258 257 adantlr ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → seq 1 ( + , ( 𝑆𝑏 ) ) ∈ dom ⇝ )
259 240 241 244 253 258 isumcl ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → Σ 𝑘 ∈ ℕ ( ( 𝐶 C𝑐 𝑘 ) · ( 𝑏𝑘 ) ) ∈ ℂ )
260 236 239 259 adddid ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( 𝐶 · ( 1 + Σ 𝑘 ∈ ℕ ( ( 𝐶 C𝑐 𝑘 ) · ( 𝑏𝑘 ) ) ) ) = ( ( 𝐶 · 1 ) + ( 𝐶 · Σ 𝑘 ∈ ℕ ( ( 𝐶 C𝑐 𝑘 ) · ( 𝑏𝑘 ) ) ) ) )
261 8 a1i ( 𝜑𝐸 = ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ ↦ ( ( 𝑘 · ( 𝐹𝑘 ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) ) ) )
262 nnex ℕ ∈ V
263 262 mptex ( 𝑘 ∈ ℕ ↦ ( ( 𝑘 · ( 𝐹𝑘 ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) ) ∈ V
264 263 a1i ( ( 𝜑𝑏 ∈ ℂ ) → ( 𝑘 ∈ ℕ ↦ ( ( 𝑘 · ( 𝐹𝑘 ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) ) ∈ V )
265 261 264 fvmpt2d ( ( 𝜑𝑏 ∈ ℂ ) → ( 𝐸𝑏 ) = ( 𝑘 ∈ ℕ ↦ ( ( 𝑘 · ( 𝐹𝑘 ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) ) )
266 120 265 sylan2 ( ( 𝜑𝑏𝐷 ) → ( 𝐸𝑏 ) = ( 𝑘 ∈ ℕ ↦ ( ( 𝑘 · ( 𝐹𝑘 ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) ) )
267 266 adantlr ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( 𝐸𝑏 ) = ( 𝑘 ∈ ℕ ↦ ( ( 𝑘 · ( 𝐹𝑘 ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) ) )
268 ovexd ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑘 · ( 𝐹𝑘 ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) ∈ V )
269 267 268 fmpt3d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( 𝐸𝑏 ) : ℕ ⟶ V )
270 269 feqmptd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( 𝐸𝑏 ) = ( 𝑘 ∈ ℕ ↦ ( ( 𝐸𝑏 ) ‘ 𝑘 ) ) )
271 ovexd ( ( ( 𝜑𝑏 ∈ ℂ ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑘 · ( 𝐹𝑘 ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) ∈ V )
272 265 271 fvmpt2d ( ( ( 𝜑𝑏 ∈ ℂ ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝐸𝑏 ) ‘ 𝑘 ) = ( ( 𝑘 · ( 𝐹𝑘 ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) )
273 242 133 sylan2 ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝐹𝑘 ) = ( 𝐶 C𝑐 𝑘 ) )
274 273 oveq2d ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝑘 · ( 𝐹𝑘 ) ) = ( 𝑘 · ( 𝐶 C𝑐 𝑘 ) ) )
275 274 oveq1d ( ( 𝜑𝑘 ∈ ℕ ) → ( ( 𝑘 · ( 𝐹𝑘 ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) = ( ( 𝑘 · ( 𝐶 C𝑐 𝑘 ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) )
276 275 adantlr ( ( ( 𝜑𝑏 ∈ ℂ ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑘 · ( 𝐹𝑘 ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) = ( ( 𝑘 · ( 𝐶 C𝑐 𝑘 ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) )
277 272 276 eqtrd ( ( ( 𝜑𝑏 ∈ ℂ ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝐸𝑏 ) ‘ 𝑘 ) = ( ( 𝑘 · ( 𝐶 C𝑐 𝑘 ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) )
278 4 adantr ( ( 𝜑𝑘 ∈ ℕ ) → 𝐶 ∈ ℂ )
279 nnm1nn0 ( 𝑘 ∈ ℕ → ( 𝑘 − 1 ) ∈ ℕ0 )
280 279 adantl ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝑘 − 1 ) ∈ ℕ0 )
281 278 280 bccp1k ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝐶 C𝑐 ( ( 𝑘 − 1 ) + 1 ) ) = ( ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) · ( ( 𝐶 − ( 𝑘 − 1 ) ) / ( ( 𝑘 − 1 ) + 1 ) ) ) )
282 242 adantl ( ( 𝜑𝑘 ∈ ℕ ) → 𝑘 ∈ ℕ0 )
283 282 nn0cnd ( ( 𝜑𝑘 ∈ ℕ ) → 𝑘 ∈ ℂ )
284 1cnd ( ( 𝜑𝑘 ∈ ℕ ) → 1 ∈ ℂ )
285 283 284 npcand ( ( 𝜑𝑘 ∈ ℕ ) → ( ( 𝑘 − 1 ) + 1 ) = 𝑘 )
286 285 oveq2d ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝐶 C𝑐 ( ( 𝑘 − 1 ) + 1 ) ) = ( 𝐶 C𝑐 𝑘 ) )
287 285 oveq2d ( ( 𝜑𝑘 ∈ ℕ ) → ( ( 𝐶 − ( 𝑘 − 1 ) ) / ( ( 𝑘 − 1 ) + 1 ) ) = ( ( 𝐶 − ( 𝑘 − 1 ) ) / 𝑘 ) )
288 287 oveq2d ( ( 𝜑𝑘 ∈ ℕ ) → ( ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) · ( ( 𝐶 − ( 𝑘 − 1 ) ) / ( ( 𝑘 − 1 ) + 1 ) ) ) = ( ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) · ( ( 𝐶 − ( 𝑘 − 1 ) ) / 𝑘 ) ) )
289 281 286 288 3eqtr3d ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝐶 C𝑐 𝑘 ) = ( ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) · ( ( 𝐶 − ( 𝑘 − 1 ) ) / 𝑘 ) ) )
290 289 oveq2d ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝑘 · ( 𝐶 C𝑐 𝑘 ) ) = ( 𝑘 · ( ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) · ( ( 𝐶 − ( 𝑘 − 1 ) ) / 𝑘 ) ) ) )
291 278 280 bcccl ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ∈ ℂ )
292 283 284 subcld ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝑘 − 1 ) ∈ ℂ )
293 278 292 subcld ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝐶 − ( 𝑘 − 1 ) ) ∈ ℂ )
294 nnne0 ( 𝑘 ∈ ℕ → 𝑘 ≠ 0 )
295 294 adantl ( ( 𝜑𝑘 ∈ ℕ ) → 𝑘 ≠ 0 )
296 291 293 283 295 divassd ( ( 𝜑𝑘 ∈ ℕ ) → ( ( ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) · ( 𝐶 − ( 𝑘 − 1 ) ) ) / 𝑘 ) = ( ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) · ( ( 𝐶 − ( 𝑘 − 1 ) ) / 𝑘 ) ) )
297 296 oveq2d ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝑘 · ( ( ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) · ( 𝐶 − ( 𝑘 − 1 ) ) ) / 𝑘 ) ) = ( 𝑘 · ( ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) · ( ( 𝐶 − ( 𝑘 − 1 ) ) / 𝑘 ) ) ) )
298 291 293 mulcld ( ( 𝜑𝑘 ∈ ℕ ) → ( ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) · ( 𝐶 − ( 𝑘 − 1 ) ) ) ∈ ℂ )
299 298 283 295 divcan2d ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝑘 · ( ( ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) · ( 𝐶 − ( 𝑘 − 1 ) ) ) / 𝑘 ) ) = ( ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) · ( 𝐶 − ( 𝑘 − 1 ) ) ) )
300 290 297 299 3eqtr2d ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝑘 · ( 𝐶 C𝑐 𝑘 ) ) = ( ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) · ( 𝐶 − ( 𝑘 − 1 ) ) ) )
301 300 oveq1d ( ( 𝜑𝑘 ∈ ℕ ) → ( ( 𝑘 · ( 𝐶 C𝑐 𝑘 ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) = ( ( ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) · ( 𝐶 − ( 𝑘 − 1 ) ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) )
302 301 adantlr ( ( ( 𝜑𝑏 ∈ ℂ ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑘 · ( 𝐶 C𝑐 𝑘 ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) = ( ( ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) · ( 𝐶 − ( 𝑘 − 1 ) ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) )
303 291 adantlr ( ( ( 𝜑𝑏 ∈ ℂ ) ∧ 𝑘 ∈ ℕ ) → ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ∈ ℂ )
304 293 adantlr ( ( ( 𝜑𝑏 ∈ ℂ ) ∧ 𝑘 ∈ ℕ ) → ( 𝐶 − ( 𝑘 − 1 ) ) ∈ ℂ )
305 303 304 mulcomd ( ( ( 𝜑𝑏 ∈ ℂ ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) · ( 𝐶 − ( 𝑘 − 1 ) ) ) = ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) )
306 305 oveq1d ( ( ( 𝜑𝑏 ∈ ℂ ) ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) · ( 𝐶 − ( 𝑘 − 1 ) ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) = ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) )
307 277 302 306 3eqtrd ( ( ( 𝜑𝑏 ∈ ℂ ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝐸𝑏 ) ‘ 𝑘 ) = ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) )
308 120 307 sylanl2 ( ( ( 𝜑𝑏𝐷 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝐸𝑏 ) ‘ 𝑘 ) = ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) )
309 308 adantllr ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝐸𝑏 ) ‘ 𝑘 ) = ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) )
310 309 mpteq2dva ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( 𝑘 ∈ ℕ ↦ ( ( 𝐸𝑏 ) ‘ 𝑘 ) ) = ( 𝑘 ∈ ℕ ↦ ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) ) )
311 270 310 eqtrd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( 𝐸𝑏 ) = ( 𝑘 ∈ ℕ ↦ ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) ) )
312 311 oveq1d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( 𝐸𝑏 ) shift - 1 ) = ( ( 𝑘 ∈ ℕ ↦ ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) ) shift - 1 ) )
313 eqid ( 𝑘 ∈ ℕ ↦ ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) ) = ( 𝑘 ∈ ℕ ↦ ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) )
314 ovex ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) ∈ V
315 oveq1 ( 𝑘 = ( 𝑗 − - 1 ) → ( 𝑘 − 1 ) = ( ( 𝑗 − - 1 ) − 1 ) )
316 315 oveq2d ( 𝑘 = ( 𝑗 − - 1 ) → ( 𝐶 − ( 𝑘 − 1 ) ) = ( 𝐶 − ( ( 𝑗 − - 1 ) − 1 ) ) )
317 315 oveq2d ( 𝑘 = ( 𝑗 − - 1 ) → ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) = ( 𝐶 C𝑐 ( ( 𝑗 − - 1 ) − 1 ) ) )
318 316 317 oveq12d ( 𝑘 = ( 𝑗 − - 1 ) → ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) = ( ( 𝐶 − ( ( 𝑗 − - 1 ) − 1 ) ) · ( 𝐶 C𝑐 ( ( 𝑗 − - 1 ) − 1 ) ) ) )
319 315 oveq2d ( 𝑘 = ( 𝑗 − - 1 ) → ( 𝑏 ↑ ( 𝑘 − 1 ) ) = ( 𝑏 ↑ ( ( 𝑗 − - 1 ) − 1 ) ) )
320 318 319 oveq12d ( 𝑘 = ( 𝑗 − - 1 ) → ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) = ( ( ( 𝐶 − ( ( 𝑗 − - 1 ) − 1 ) ) · ( 𝐶 C𝑐 ( ( 𝑗 − - 1 ) − 1 ) ) ) · ( 𝑏 ↑ ( ( 𝑗 − - 1 ) − 1 ) ) ) )
321 1pneg1e0 ( 1 + - 1 ) = 0
322 321 fveq2i ( ℤ ‘ ( 1 + - 1 ) ) = ( ℤ ‘ 0 )
323 113 322 eqtr4i 0 = ( ℤ ‘ ( 1 + - 1 ) )
324 241 znegcld ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → - 1 ∈ ℤ )
325 313 314 320 240 323 241 324 uzmptshftfval ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( 𝑘 ∈ ℕ ↦ ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) ) shift - 1 ) = ( 𝑗 ∈ ℕ0 ↦ ( ( ( 𝐶 − ( ( 𝑗 − - 1 ) − 1 ) ) · ( 𝐶 C𝑐 ( ( 𝑗 − - 1 ) − 1 ) ) ) · ( 𝑏 ↑ ( ( 𝑗 − - 1 ) − 1 ) ) ) ) )
326 oveq1 ( 𝑗 = 𝑘 → ( 𝑗 − - 1 ) = ( 𝑘 − - 1 ) )
327 326 oveq1d ( 𝑗 = 𝑘 → ( ( 𝑗 − - 1 ) − 1 ) = ( ( 𝑘 − - 1 ) − 1 ) )
328 327 oveq2d ( 𝑗 = 𝑘 → ( 𝐶 − ( ( 𝑗 − - 1 ) − 1 ) ) = ( 𝐶 − ( ( 𝑘 − - 1 ) − 1 ) ) )
329 327 oveq2d ( 𝑗 = 𝑘 → ( 𝐶 C𝑐 ( ( 𝑗 − - 1 ) − 1 ) ) = ( 𝐶 C𝑐 ( ( 𝑘 − - 1 ) − 1 ) ) )
330 328 329 oveq12d ( 𝑗 = 𝑘 → ( ( 𝐶 − ( ( 𝑗 − - 1 ) − 1 ) ) · ( 𝐶 C𝑐 ( ( 𝑗 − - 1 ) − 1 ) ) ) = ( ( 𝐶 − ( ( 𝑘 − - 1 ) − 1 ) ) · ( 𝐶 C𝑐 ( ( 𝑘 − - 1 ) − 1 ) ) ) )
331 327 oveq2d ( 𝑗 = 𝑘 → ( 𝑏 ↑ ( ( 𝑗 − - 1 ) − 1 ) ) = ( 𝑏 ↑ ( ( 𝑘 − - 1 ) − 1 ) ) )
332 330 331 oveq12d ( 𝑗 = 𝑘 → ( ( ( 𝐶 − ( ( 𝑗 − - 1 ) − 1 ) ) · ( 𝐶 C𝑐 ( ( 𝑗 − - 1 ) − 1 ) ) ) · ( 𝑏 ↑ ( ( 𝑗 − - 1 ) − 1 ) ) ) = ( ( ( 𝐶 − ( ( 𝑘 − - 1 ) − 1 ) ) · ( 𝐶 C𝑐 ( ( 𝑘 − - 1 ) − 1 ) ) ) · ( 𝑏 ↑ ( ( 𝑘 − - 1 ) − 1 ) ) ) )
333 332 cbvmptv ( 𝑗 ∈ ℕ0 ↦ ( ( ( 𝐶 − ( ( 𝑗 − - 1 ) − 1 ) ) · ( 𝐶 C𝑐 ( ( 𝑗 − - 1 ) − 1 ) ) ) · ( 𝑏 ↑ ( ( 𝑗 − - 1 ) − 1 ) ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( ( 𝐶 − ( ( 𝑘 − - 1 ) − 1 ) ) · ( 𝐶 C𝑐 ( ( 𝑘 − - 1 ) − 1 ) ) ) · ( 𝑏 ↑ ( ( 𝑘 − - 1 ) − 1 ) ) ) )
334 333 a1i ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( 𝑗 ∈ ℕ0 ↦ ( ( ( 𝐶 − ( ( 𝑗 − - 1 ) − 1 ) ) · ( 𝐶 C𝑐 ( ( 𝑗 − - 1 ) − 1 ) ) ) · ( 𝑏 ↑ ( ( 𝑗 − - 1 ) − 1 ) ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( ( 𝐶 − ( ( 𝑘 − - 1 ) − 1 ) ) · ( 𝐶 C𝑐 ( ( 𝑘 − - 1 ) − 1 ) ) ) · ( 𝑏 ↑ ( ( 𝑘 − - 1 ) − 1 ) ) ) ) )
335 312 325 334 3eqtrd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( 𝐸𝑏 ) shift - 1 ) = ( 𝑘 ∈ ℕ0 ↦ ( ( ( 𝐶 − ( ( 𝑘 − - 1 ) − 1 ) ) · ( 𝐶 C𝑐 ( ( 𝑘 − - 1 ) − 1 ) ) ) · ( 𝑏 ↑ ( ( 𝑘 − - 1 ) − 1 ) ) ) ) )
336 nn0cn ( 𝑘 ∈ ℕ0𝑘 ∈ ℂ )
337 1cnd ( 𝑘 ∈ ℕ0 → 1 ∈ ℂ )
338 336 337 subnegd ( 𝑘 ∈ ℕ0 → ( 𝑘 − - 1 ) = ( 𝑘 + 1 ) )
339 338 oveq1d ( 𝑘 ∈ ℕ0 → ( ( 𝑘 − - 1 ) − 1 ) = ( ( 𝑘 + 1 ) − 1 ) )
340 336 337 pncand ( 𝑘 ∈ ℕ0 → ( ( 𝑘 + 1 ) − 1 ) = 𝑘 )
341 339 340 eqtrd ( 𝑘 ∈ ℕ0 → ( ( 𝑘 − - 1 ) − 1 ) = 𝑘 )
342 341 adantl ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑘 − - 1 ) − 1 ) = 𝑘 )
343 342 oveq2d ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐶 − ( ( 𝑘 − - 1 ) − 1 ) ) = ( 𝐶𝑘 ) )
344 342 oveq2d ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐶 C𝑐 ( ( 𝑘 − - 1 ) − 1 ) ) = ( 𝐶 C𝑐 𝑘 ) )
345 343 344 oveq12d ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐶 − ( ( 𝑘 − - 1 ) − 1 ) ) · ( 𝐶 C𝑐 ( ( 𝑘 − - 1 ) − 1 ) ) ) = ( ( 𝐶𝑘 ) · ( 𝐶 C𝑐 𝑘 ) ) )
346 342 oveq2d ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑏 ↑ ( ( 𝑘 − - 1 ) − 1 ) ) = ( 𝑏𝑘 ) )
347 345 346 oveq12d ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐶 − ( ( 𝑘 − - 1 ) − 1 ) ) · ( 𝐶 C𝑐 ( ( 𝑘 − - 1 ) − 1 ) ) ) · ( 𝑏 ↑ ( ( 𝑘 − - 1 ) − 1 ) ) ) = ( ( ( 𝐶𝑘 ) · ( 𝐶 C𝑐 𝑘 ) ) · ( 𝑏𝑘 ) ) )
348 347 mpteq2dva ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( ( 𝐶 − ( ( 𝑘 − - 1 ) − 1 ) ) · ( 𝐶 C𝑐 ( ( 𝑘 − - 1 ) − 1 ) ) ) · ( 𝑏 ↑ ( ( 𝑘 − - 1 ) − 1 ) ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( ( 𝐶𝑘 ) · ( 𝐶 C𝑐 𝑘 ) ) · ( 𝑏𝑘 ) ) ) )
349 335 348 eqtrd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( 𝐸𝑏 ) shift - 1 ) = ( 𝑘 ∈ ℕ0 ↦ ( ( ( 𝐶𝑘 ) · ( 𝐶 C𝑐 𝑘 ) ) · ( 𝑏𝑘 ) ) ) )
350 ovexd ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐶𝑘 ) · ( 𝐶 C𝑐 𝑘 ) ) · ( 𝑏𝑘 ) ) ∈ V )
351 349 350 fvmpt2d ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐸𝑏 ) shift - 1 ) ‘ 𝑘 ) = ( ( ( 𝐶𝑘 ) · ( 𝐶 C𝑐 𝑘 ) ) · ( 𝑏𝑘 ) ) )
352 242 351 sylan2 ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝐸𝑏 ) shift - 1 ) ‘ 𝑘 ) = ( ( ( 𝐶𝑘 ) · ( 𝐶 C𝑐 𝑘 ) ) · ( 𝑏𝑘 ) ) )
353 336 adantl ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℂ )
354 245 353 subcld ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐶𝑘 ) ∈ ℂ )
355 354 247 mulcld ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐶𝑘 ) · ( 𝐶 C𝑐 𝑘 ) ) ∈ ℂ )
356 355 251 mulcld ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐶𝑘 ) · ( 𝐶 C𝑐 𝑘 ) ) · ( 𝑏𝑘 ) ) ∈ ℂ )
357 242 356 sylan2 ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝐶𝑘 ) · ( 𝐶 C𝑐 𝑘 ) ) · ( 𝑏𝑘 ) ) ∈ ℂ )
358 fveq2 ( 𝑘 = 𝑗 → ( ( 𝐸𝑏 ) ‘ 𝑘 ) = ( ( 𝐸𝑏 ) ‘ 𝑗 ) )
359 358 oveq2d ( 𝑘 = 𝑗 → ( 𝑏 · ( ( 𝐸𝑏 ) ‘ 𝑘 ) ) = ( 𝑏 · ( ( 𝐸𝑏 ) ‘ 𝑗 ) ) )
360 359 cbvmptv ( 𝑘 ∈ ℕ ↦ ( 𝑏 · ( ( 𝐸𝑏 ) ‘ 𝑘 ) ) ) = ( 𝑗 ∈ ℕ ↦ ( 𝑏 · ( ( 𝐸𝑏 ) ‘ 𝑗 ) ) )
361 309 oveq2d ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ ) → ( 𝑏 · ( ( 𝐸𝑏 ) ‘ 𝑘 ) ) = ( 𝑏 · ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) ) )
362 249 adantr ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ ) → 𝑏 ∈ ℂ )
363 4 ad3antrrr ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ ) → 𝐶 ∈ ℂ )
364 nncn ( 𝑘 ∈ ℕ → 𝑘 ∈ ℂ )
365 364 adantl ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℂ )
366 1cnd ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ ) → 1 ∈ ℂ )
367 365 366 subcld ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ ) → ( 𝑘 − 1 ) ∈ ℂ )
368 363 367 subcld ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ ) → ( 𝐶 − ( 𝑘 − 1 ) ) ∈ ℂ )
369 279 adantl ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ ) → ( 𝑘 − 1 ) ∈ ℕ0 )
370 363 369 bcccl ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ ) → ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ∈ ℂ )
371 368 370 mulcld ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) ∈ ℂ )
372 362 369 expcld ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ ) → ( 𝑏 ↑ ( 𝑘 − 1 ) ) ∈ ℂ )
373 362 371 372 mul12d ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ ) → ( 𝑏 · ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) ) = ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏 · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) ) )
374 362 372 mulcomd ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ ) → ( 𝑏 · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) = ( ( 𝑏 ↑ ( 𝑘 − 1 ) ) · 𝑏 ) )
375 362 369 expp1d ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ ) → ( 𝑏 ↑ ( ( 𝑘 − 1 ) + 1 ) ) = ( ( 𝑏 ↑ ( 𝑘 − 1 ) ) · 𝑏 ) )
376 285 adantlr ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑘 − 1 ) + 1 ) = 𝑘 )
377 376 adantlr ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑘 − 1 ) + 1 ) = 𝑘 )
378 377 oveq2d ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ ) → ( 𝑏 ↑ ( ( 𝑘 − 1 ) + 1 ) ) = ( 𝑏𝑘 ) )
379 374 375 378 3eqtr2d ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ ) → ( 𝑏 · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) = ( 𝑏𝑘 ) )
380 379 oveq2d ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏 · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) ) = ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏𝑘 ) ) )
381 373 380 eqtrd ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ ) → ( 𝑏 · ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) ) = ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏𝑘 ) ) )
382 361 381 eqtrd ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ ) → ( 𝑏 · ( ( 𝐸𝑏 ) ‘ 𝑘 ) ) = ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏𝑘 ) ) )
383 382 mpteq2dva ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( 𝑘 ∈ ℕ ↦ ( 𝑏 · ( ( 𝐸𝑏 ) ‘ 𝑘 ) ) ) = ( 𝑘 ∈ ℕ ↦ ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏𝑘 ) ) ) )
384 360 383 eqtr3id ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( 𝑗 ∈ ℕ ↦ ( 𝑏 · ( ( 𝐸𝑏 ) ‘ 𝑗 ) ) ) = ( 𝑘 ∈ ℕ ↦ ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏𝑘 ) ) ) )
385 ovexd ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏𝑘 ) ) ∈ V )
386 384 385 fvmpt2d ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑗 ∈ ℕ ↦ ( 𝑏 · ( ( 𝐸𝑏 ) ‘ 𝑗 ) ) ) ‘ 𝑘 ) = ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏𝑘 ) ) )
387 371 252 mulcld ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏𝑘 ) ) ∈ ℂ )
388 climrel Rel ⇝
389 157 simprd ( ( 𝜑𝑏𝐷 ) → seq 1 ( + , ( 𝐸𝑏 ) ) ∈ dom ⇝ )
390 389 adantlr ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → seq 1 ( + , ( 𝐸𝑏 ) ) ∈ dom ⇝ )
391 climdm ( seq 1 ( + , ( 𝐸𝑏 ) ) ∈ dom ⇝ ↔ seq 1 ( + , ( 𝐸𝑏 ) ) ⇝ ( ⇝ ‘ seq 1 ( + , ( 𝐸𝑏 ) ) ) )
392 390 391 sylib ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → seq 1 ( + , ( 𝐸𝑏 ) ) ⇝ ( ⇝ ‘ seq 1 ( + , ( 𝐸𝑏 ) ) ) )
393 0z 0 ∈ ℤ
394 neg1z - 1 ∈ ℤ
395 fvex ( 𝐸𝑏 ) ∈ V
396 395 seqshft ( ( 0 ∈ ℤ ∧ - 1 ∈ ℤ ) → seq 0 ( + , ( ( 𝐸𝑏 ) shift - 1 ) ) = ( seq ( 0 − - 1 ) ( + , ( 𝐸𝑏 ) ) shift - 1 ) )
397 393 394 396 mp2an seq 0 ( + , ( ( 𝐸𝑏 ) shift - 1 ) ) = ( seq ( 0 − - 1 ) ( + , ( 𝐸𝑏 ) ) shift - 1 )
398 0cn 0 ∈ ℂ
399 398 196 subnegi ( 0 − - 1 ) = ( 0 + 1 )
400 0p1e1 ( 0 + 1 ) = 1
401 399 400 eqtri ( 0 − - 1 ) = 1
402 seqeq1 ( ( 0 − - 1 ) = 1 → seq ( 0 − - 1 ) ( + , ( 𝐸𝑏 ) ) = seq 1 ( + , ( 𝐸𝑏 ) ) )
403 401 402 ax-mp seq ( 0 − - 1 ) ( + , ( 𝐸𝑏 ) ) = seq 1 ( + , ( 𝐸𝑏 ) )
404 403 oveq1i ( seq ( 0 − - 1 ) ( + , ( 𝐸𝑏 ) ) shift - 1 ) = ( seq 1 ( + , ( 𝐸𝑏 ) ) shift - 1 )
405 397 404 eqtri seq 0 ( + , ( ( 𝐸𝑏 ) shift - 1 ) ) = ( seq 1 ( + , ( 𝐸𝑏 ) ) shift - 1 )
406 405 breq1i ( seq 0 ( + , ( ( 𝐸𝑏 ) shift - 1 ) ) ⇝ ( ⇝ ‘ seq 1 ( + , ( 𝐸𝑏 ) ) ) ↔ ( seq 1 ( + , ( 𝐸𝑏 ) ) shift - 1 ) ⇝ ( ⇝ ‘ seq 1 ( + , ( 𝐸𝑏 ) ) ) )
407 seqex seq 1 ( + , ( 𝐸𝑏 ) ) ∈ V
408 climshft ( ( - 1 ∈ ℤ ∧ seq 1 ( + , ( 𝐸𝑏 ) ) ∈ V ) → ( ( seq 1 ( + , ( 𝐸𝑏 ) ) shift - 1 ) ⇝ ( ⇝ ‘ seq 1 ( + , ( 𝐸𝑏 ) ) ) ↔ seq 1 ( + , ( 𝐸𝑏 ) ) ⇝ ( ⇝ ‘ seq 1 ( + , ( 𝐸𝑏 ) ) ) ) )
409 394 407 408 mp2an ( ( seq 1 ( + , ( 𝐸𝑏 ) ) shift - 1 ) ⇝ ( ⇝ ‘ seq 1 ( + , ( 𝐸𝑏 ) ) ) ↔ seq 1 ( + , ( 𝐸𝑏 ) ) ⇝ ( ⇝ ‘ seq 1 ( + , ( 𝐸𝑏 ) ) ) )
410 406 409 bitri ( seq 0 ( + , ( ( 𝐸𝑏 ) shift - 1 ) ) ⇝ ( ⇝ ‘ seq 1 ( + , ( 𝐸𝑏 ) ) ) ↔ seq 1 ( + , ( 𝐸𝑏 ) ) ⇝ ( ⇝ ‘ seq 1 ( + , ( 𝐸𝑏 ) ) ) )
411 392 410 sylibr ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → seq 0 ( + , ( ( 𝐸𝑏 ) shift - 1 ) ) ⇝ ( ⇝ ‘ seq 1 ( + , ( 𝐸𝑏 ) ) ) )
412 releldm ( ( Rel ⇝ ∧ seq 0 ( + , ( ( 𝐸𝑏 ) shift - 1 ) ) ⇝ ( ⇝ ‘ seq 1 ( + , ( 𝐸𝑏 ) ) ) ) → seq 0 ( + , ( ( 𝐸𝑏 ) shift - 1 ) ) ∈ dom ⇝ )
413 388 411 412 sylancr ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → seq 0 ( + , ( ( 𝐸𝑏 ) shift - 1 ) ) ∈ dom ⇝ )
414 254 a1i ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → 1 ∈ ℕ0 )
415 351 356 eqeltrd ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐸𝑏 ) shift - 1 ) ‘ 𝑘 ) ∈ ℂ )
416 113 414 415 iserex ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( seq 0 ( + , ( ( 𝐸𝑏 ) shift - 1 ) ) ∈ dom ⇝ ↔ seq 1 ( + , ( ( 𝐸𝑏 ) shift - 1 ) ) ∈ dom ⇝ ) )
417 413 416 mpbid ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → seq 1 ( + , ( ( 𝐸𝑏 ) shift - 1 ) ) ∈ dom ⇝ )
418 371 372 mulcld ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) ∈ ℂ )
419 309 418 eqeltrd ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝐸𝑏 ) ‘ 𝑘 ) ∈ ℂ )
420 386 382 eqtr4d ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑗 ∈ ℕ ↦ ( 𝑏 · ( ( 𝐸𝑏 ) ‘ 𝑗 ) ) ) ‘ 𝑘 ) = ( 𝑏 · ( ( 𝐸𝑏 ) ‘ 𝑘 ) ) )
421 240 241 249 392 419 420 isermulc2 ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → seq 1 ( + , ( 𝑗 ∈ ℕ ↦ ( 𝑏 · ( ( 𝐸𝑏 ) ‘ 𝑗 ) ) ) ) ⇝ ( 𝑏 · ( ⇝ ‘ seq 1 ( + , ( 𝐸𝑏 ) ) ) ) )
422 releldm ( ( Rel ⇝ ∧ seq 1 ( + , ( 𝑗 ∈ ℕ ↦ ( 𝑏 · ( ( 𝐸𝑏 ) ‘ 𝑗 ) ) ) ) ⇝ ( 𝑏 · ( ⇝ ‘ seq 1 ( + , ( 𝐸𝑏 ) ) ) ) ) → seq 1 ( + , ( 𝑗 ∈ ℕ ↦ ( 𝑏 · ( ( 𝐸𝑏 ) ‘ 𝑗 ) ) ) ) ∈ dom ⇝ )
423 388 421 422 sylancr ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → seq 1 ( + , ( 𝑗 ∈ ℕ ↦ ( 𝑏 · ( ( 𝐸𝑏 ) ‘ 𝑗 ) ) ) ) ∈ dom ⇝ )
424 240 241 352 357 386 387 417 423 isumadd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → Σ 𝑘 ∈ ℕ ( ( ( ( 𝐶𝑘 ) · ( 𝐶 C𝑐 𝑘 ) ) · ( 𝑏𝑘 ) ) + ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏𝑘 ) ) ) = ( Σ 𝑘 ∈ ℕ ( ( ( 𝐶𝑘 ) · ( 𝐶 C𝑐 𝑘 ) ) · ( 𝑏𝑘 ) ) + Σ 𝑘 ∈ ℕ ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏𝑘 ) ) ) )
425 424 oveq2d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( 𝐶 + Σ 𝑘 ∈ ℕ ( ( ( ( 𝐶𝑘 ) · ( 𝐶 C𝑐 𝑘 ) ) · ( 𝑏𝑘 ) ) + ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏𝑘 ) ) ) ) = ( 𝐶 + ( Σ 𝑘 ∈ ℕ ( ( ( 𝐶𝑘 ) · ( 𝐶 C𝑐 𝑘 ) ) · ( 𝑏𝑘 ) ) + Σ 𝑘 ∈ ℕ ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏𝑘 ) ) ) ) )
426 363 365 subcld ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ ) → ( 𝐶𝑘 ) ∈ ℂ )
427 426 248 mulcld ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝐶𝑘 ) · ( 𝐶 C𝑐 𝑘 ) ) ∈ ℂ )
428 427 371 252 adddird ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ ) → ( ( ( ( 𝐶𝑘 ) · ( 𝐶 C𝑐 𝑘 ) ) + ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) ) · ( 𝑏𝑘 ) ) = ( ( ( ( 𝐶𝑘 ) · ( 𝐶 C𝑐 𝑘 ) ) · ( 𝑏𝑘 ) ) + ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏𝑘 ) ) ) )
429 428 sumeq2dv ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → Σ 𝑘 ∈ ℕ ( ( ( ( 𝐶𝑘 ) · ( 𝐶 C𝑐 𝑘 ) ) + ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) ) · ( 𝑏𝑘 ) ) = Σ 𝑘 ∈ ℕ ( ( ( ( 𝐶𝑘 ) · ( 𝐶 C𝑐 𝑘 ) ) · ( 𝑏𝑘 ) ) + ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏𝑘 ) ) ) )
430 429 oveq2d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( 𝐶 + Σ 𝑘 ∈ ℕ ( ( ( ( 𝐶𝑘 ) · ( 𝐶 C𝑐 𝑘 ) ) + ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) ) · ( 𝑏𝑘 ) ) ) = ( 𝐶 + Σ 𝑘 ∈ ℕ ( ( ( ( 𝐶𝑘 ) · ( 𝐶 C𝑐 𝑘 ) ) · ( 𝑏𝑘 ) ) + ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏𝑘 ) ) ) ) )
431 307 sumeq2dv ( ( 𝜑𝑏 ∈ ℂ ) → Σ 𝑘 ∈ ℕ ( ( 𝐸𝑏 ) ‘ 𝑘 ) = Σ 𝑘 ∈ ℕ ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) )
432 431 oveq2d ( ( 𝜑𝑏 ∈ ℂ ) → ( ( 1 + 𝑏 ) · Σ 𝑘 ∈ ℕ ( ( 𝐸𝑏 ) ‘ 𝑘 ) ) = ( ( 1 + 𝑏 ) · Σ 𝑘 ∈ ℕ ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) ) )
433 120 432 sylan2 ( ( 𝜑𝑏𝐷 ) → ( ( 1 + 𝑏 ) · Σ 𝑘 ∈ ℕ ( ( 𝐸𝑏 ) ‘ 𝑘 ) ) = ( ( 1 + 𝑏 ) · Σ 𝑘 ∈ ℕ ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) ) )
434 433 adantlr ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( 1 + 𝑏 ) · Σ 𝑘 ∈ ℕ ( ( 𝐸𝑏 ) ‘ 𝑘 ) ) = ( ( 1 + 𝑏 ) · Σ 𝑘 ∈ ℕ ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) ) )
435 240 241 309 418 390 isumcl ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → Σ 𝑘 ∈ ℕ ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) ∈ ℂ )
436 239 249 435 adddird ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( 1 + 𝑏 ) · Σ 𝑘 ∈ ℕ ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) ) = ( ( 1 · Σ 𝑘 ∈ ℕ ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) ) + ( 𝑏 · Σ 𝑘 ∈ ℕ ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) ) ) )
437 435 mulid2d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( 1 · Σ 𝑘 ∈ ℕ ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) ) = Σ 𝑘 ∈ ℕ ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) )
438 240 241 309 418 390 249 isummulc2 ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( 𝑏 · Σ 𝑘 ∈ ℕ ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) ) = Σ 𝑘 ∈ ℕ ( 𝑏 · ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) ) )
439 381 sumeq2dv ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → Σ 𝑘 ∈ ℕ ( 𝑏 · ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) ) = Σ 𝑘 ∈ ℕ ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏𝑘 ) ) )
440 438 439 eqtrd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( 𝑏 · Σ 𝑘 ∈ ℕ ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) ) = Σ 𝑘 ∈ ℕ ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏𝑘 ) ) )
441 437 440 oveq12d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( 1 · Σ 𝑘 ∈ ℕ ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) ) + ( 𝑏 · Σ 𝑘 ∈ ℕ ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) ) ) = ( Σ 𝑘 ∈ ℕ ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) + Σ 𝑘 ∈ ℕ ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏𝑘 ) ) ) )
442 434 436 441 3eqtrd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( 1 + 𝑏 ) · Σ 𝑘 ∈ ℕ ( ( 𝐸𝑏 ) ‘ 𝑘 ) ) = ( Σ 𝑘 ∈ ℕ ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) + Σ 𝑘 ∈ ℕ ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏𝑘 ) ) ) )
443 400 fveq2i ( ℤ ‘ ( 0 + 1 ) ) = ( ℤ ‘ 1 )
444 240 443 eqtr4i ℕ = ( ℤ ‘ ( 0 + 1 ) )
445 oveq1 ( 𝑘 = ( 1 + 𝑗 ) → ( 𝑘 − 1 ) = ( ( 1 + 𝑗 ) − 1 ) )
446 445 oveq2d ( 𝑘 = ( 1 + 𝑗 ) → ( 𝐶 − ( 𝑘 − 1 ) ) = ( 𝐶 − ( ( 1 + 𝑗 ) − 1 ) ) )
447 445 oveq2d ( 𝑘 = ( 1 + 𝑗 ) → ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) = ( 𝐶 C𝑐 ( ( 1 + 𝑗 ) − 1 ) ) )
448 446 447 oveq12d ( 𝑘 = ( 1 + 𝑗 ) → ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) = ( ( 𝐶 − ( ( 1 + 𝑗 ) − 1 ) ) · ( 𝐶 C𝑐 ( ( 1 + 𝑗 ) − 1 ) ) ) )
449 445 oveq2d ( 𝑘 = ( 1 + 𝑗 ) → ( 𝑏 ↑ ( 𝑘 − 1 ) ) = ( 𝑏 ↑ ( ( 1 + 𝑗 ) − 1 ) ) )
450 448 449 oveq12d ( 𝑘 = ( 1 + 𝑗 ) → ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) = ( ( ( 𝐶 − ( ( 1 + 𝑗 ) − 1 ) ) · ( 𝐶 C𝑐 ( ( 1 + 𝑗 ) − 1 ) ) ) · ( 𝑏 ↑ ( ( 1 + 𝑗 ) − 1 ) ) ) )
451 113 444 450 241 114 418 isumshft ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → Σ 𝑘 ∈ ℕ ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) = Σ 𝑗 ∈ ℕ0 ( ( ( 𝐶 − ( ( 1 + 𝑗 ) − 1 ) ) · ( 𝐶 C𝑐 ( ( 1 + 𝑗 ) − 1 ) ) ) · ( 𝑏 ↑ ( ( 1 + 𝑗 ) − 1 ) ) ) )
452 oveq2 ( 𝑗 = 𝑘 → ( 1 + 𝑗 ) = ( 1 + 𝑘 ) )
453 452 oveq1d ( 𝑗 = 𝑘 → ( ( 1 + 𝑗 ) − 1 ) = ( ( 1 + 𝑘 ) − 1 ) )
454 453 oveq2d ( 𝑗 = 𝑘 → ( 𝐶 − ( ( 1 + 𝑗 ) − 1 ) ) = ( 𝐶 − ( ( 1 + 𝑘 ) − 1 ) ) )
455 453 oveq2d ( 𝑗 = 𝑘 → ( 𝐶 C𝑐 ( ( 1 + 𝑗 ) − 1 ) ) = ( 𝐶 C𝑐 ( ( 1 + 𝑘 ) − 1 ) ) )
456 454 455 oveq12d ( 𝑗 = 𝑘 → ( ( 𝐶 − ( ( 1 + 𝑗 ) − 1 ) ) · ( 𝐶 C𝑐 ( ( 1 + 𝑗 ) − 1 ) ) ) = ( ( 𝐶 − ( ( 1 + 𝑘 ) − 1 ) ) · ( 𝐶 C𝑐 ( ( 1 + 𝑘 ) − 1 ) ) ) )
457 453 oveq2d ( 𝑗 = 𝑘 → ( 𝑏 ↑ ( ( 1 + 𝑗 ) − 1 ) ) = ( 𝑏 ↑ ( ( 1 + 𝑘 ) − 1 ) ) )
458 456 457 oveq12d ( 𝑗 = 𝑘 → ( ( ( 𝐶 − ( ( 1 + 𝑗 ) − 1 ) ) · ( 𝐶 C𝑐 ( ( 1 + 𝑗 ) − 1 ) ) ) · ( 𝑏 ↑ ( ( 1 + 𝑗 ) − 1 ) ) ) = ( ( ( 𝐶 − ( ( 1 + 𝑘 ) − 1 ) ) · ( 𝐶 C𝑐 ( ( 1 + 𝑘 ) − 1 ) ) ) · ( 𝑏 ↑ ( ( 1 + 𝑘 ) − 1 ) ) ) )
459 458 cbvsumv Σ 𝑗 ∈ ℕ0 ( ( ( 𝐶 − ( ( 1 + 𝑗 ) − 1 ) ) · ( 𝐶 C𝑐 ( ( 1 + 𝑗 ) − 1 ) ) ) · ( 𝑏 ↑ ( ( 1 + 𝑗 ) − 1 ) ) ) = Σ 𝑘 ∈ ℕ0 ( ( ( 𝐶 − ( ( 1 + 𝑘 ) − 1 ) ) · ( 𝐶 C𝑐 ( ( 1 + 𝑘 ) − 1 ) ) ) · ( 𝑏 ↑ ( ( 1 + 𝑘 ) − 1 ) ) )
460 459 a1i ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → Σ 𝑗 ∈ ℕ0 ( ( ( 𝐶 − ( ( 1 + 𝑗 ) − 1 ) ) · ( 𝐶 C𝑐 ( ( 1 + 𝑗 ) − 1 ) ) ) · ( 𝑏 ↑ ( ( 1 + 𝑗 ) − 1 ) ) ) = Σ 𝑘 ∈ ℕ0 ( ( ( 𝐶 − ( ( 1 + 𝑘 ) − 1 ) ) · ( 𝐶 C𝑐 ( ( 1 + 𝑘 ) − 1 ) ) ) · ( 𝑏 ↑ ( ( 1 + 𝑘 ) − 1 ) ) ) )
461 1cnd ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ0 ) → 1 ∈ ℂ )
462 461 353 pncan2d ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 1 + 𝑘 ) − 1 ) = 𝑘 )
463 462 oveq2d ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐶 − ( ( 1 + 𝑘 ) − 1 ) ) = ( 𝐶𝑘 ) )
464 462 oveq2d ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐶 C𝑐 ( ( 1 + 𝑘 ) − 1 ) ) = ( 𝐶 C𝑐 𝑘 ) )
465 463 464 oveq12d ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐶 − ( ( 1 + 𝑘 ) − 1 ) ) · ( 𝐶 C𝑐 ( ( 1 + 𝑘 ) − 1 ) ) ) = ( ( 𝐶𝑘 ) · ( 𝐶 C𝑐 𝑘 ) ) )
466 462 oveq2d ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑏 ↑ ( ( 1 + 𝑘 ) − 1 ) ) = ( 𝑏𝑘 ) )
467 465 466 oveq12d ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐶 − ( ( 1 + 𝑘 ) − 1 ) ) · ( 𝐶 C𝑐 ( ( 1 + 𝑘 ) − 1 ) ) ) · ( 𝑏 ↑ ( ( 1 + 𝑘 ) − 1 ) ) ) = ( ( ( 𝐶𝑘 ) · ( 𝐶 C𝑐 𝑘 ) ) · ( 𝑏𝑘 ) ) )
468 467 sumeq2dv ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → Σ 𝑘 ∈ ℕ0 ( ( ( 𝐶 − ( ( 1 + 𝑘 ) − 1 ) ) · ( 𝐶 C𝑐 ( ( 1 + 𝑘 ) − 1 ) ) ) · ( 𝑏 ↑ ( ( 1 + 𝑘 ) − 1 ) ) ) = Σ 𝑘 ∈ ℕ0 ( ( ( 𝐶𝑘 ) · ( 𝐶 C𝑐 𝑘 ) ) · ( 𝑏𝑘 ) ) )
469 451 460 468 3eqtrd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → Σ 𝑘 ∈ ℕ ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) = Σ 𝑘 ∈ ℕ0 ( ( ( 𝐶𝑘 ) · ( 𝐶 C𝑐 𝑘 ) ) · ( 𝑏𝑘 ) ) )
470 113 114 351 356 413 isum1p ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → Σ 𝑘 ∈ ℕ0 ( ( ( 𝐶𝑘 ) · ( 𝐶 C𝑐 𝑘 ) ) · ( 𝑏𝑘 ) ) = ( ( ( ( 𝐸𝑏 ) shift - 1 ) ‘ 0 ) + Σ 𝑘 ∈ ( ℤ ‘ ( 0 + 1 ) ) ( ( ( 𝐶𝑘 ) · ( 𝐶 C𝑐 𝑘 ) ) · ( 𝑏𝑘 ) ) ) )
471 simpr ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 = 0 ) → 𝑘 = 0 )
472 471 oveq2d ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 = 0 ) → ( 𝐶𝑘 ) = ( 𝐶 − 0 ) )
473 471 oveq2d ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 = 0 ) → ( 𝐶 C𝑐 𝑘 ) = ( 𝐶 C𝑐 0 ) )
474 472 473 oveq12d ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 = 0 ) → ( ( 𝐶𝑘 ) · ( 𝐶 C𝑐 𝑘 ) ) = ( ( 𝐶 − 0 ) · ( 𝐶 C𝑐 0 ) ) )
475 471 oveq2d ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 = 0 ) → ( 𝑏𝑘 ) = ( 𝑏 ↑ 0 ) )
476 474 475 oveq12d ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 = 0 ) → ( ( ( 𝐶𝑘 ) · ( 𝐶 C𝑐 𝑘 ) ) · ( 𝑏𝑘 ) ) = ( ( ( 𝐶 − 0 ) · ( 𝐶 C𝑐 0 ) ) · ( 𝑏 ↑ 0 ) ) )
477 0nn0 0 ∈ ℕ0
478 477 a1i ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → 0 ∈ ℕ0 )
479 ovexd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( ( 𝐶 − 0 ) · ( 𝐶 C𝑐 0 ) ) · ( 𝑏 ↑ 0 ) ) ∈ V )
480 349 476 478 479 fvmptd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( ( 𝐸𝑏 ) shift - 1 ) ‘ 0 ) = ( ( ( 𝐶 − 0 ) · ( 𝐶 C𝑐 0 ) ) · ( 𝑏 ↑ 0 ) ) )
481 236 subid1d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( 𝐶 − 0 ) = 𝐶 )
482 236 bccn0 ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( 𝐶 C𝑐 0 ) = 1 )
483 481 482 oveq12d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( 𝐶 − 0 ) · ( 𝐶 C𝑐 0 ) ) = ( 𝐶 · 1 ) )
484 483 237 eqtrd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( 𝐶 − 0 ) · ( 𝐶 C𝑐 0 ) ) = 𝐶 )
485 249 exp0d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( 𝑏 ↑ 0 ) = 1 )
486 484 485 oveq12d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( ( 𝐶 − 0 ) · ( 𝐶 C𝑐 0 ) ) · ( 𝑏 ↑ 0 ) ) = ( 𝐶 · 1 ) )
487 480 486 237 3eqtrd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( ( 𝐸𝑏 ) shift - 1 ) ‘ 0 ) = 𝐶 )
488 444 eqcomi ( ℤ ‘ ( 0 + 1 ) ) = ℕ
489 488 sumeq1i Σ 𝑘 ∈ ( ℤ ‘ ( 0 + 1 ) ) ( ( ( 𝐶𝑘 ) · ( 𝐶 C𝑐 𝑘 ) ) · ( 𝑏𝑘 ) ) = Σ 𝑘 ∈ ℕ ( ( ( 𝐶𝑘 ) · ( 𝐶 C𝑐 𝑘 ) ) · ( 𝑏𝑘 ) )
490 489 a1i ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → Σ 𝑘 ∈ ( ℤ ‘ ( 0 + 1 ) ) ( ( ( 𝐶𝑘 ) · ( 𝐶 C𝑐 𝑘 ) ) · ( 𝑏𝑘 ) ) = Σ 𝑘 ∈ ℕ ( ( ( 𝐶𝑘 ) · ( 𝐶 C𝑐 𝑘 ) ) · ( 𝑏𝑘 ) ) )
491 487 490 oveq12d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( ( ( 𝐸𝑏 ) shift - 1 ) ‘ 0 ) + Σ 𝑘 ∈ ( ℤ ‘ ( 0 + 1 ) ) ( ( ( 𝐶𝑘 ) · ( 𝐶 C𝑐 𝑘 ) ) · ( 𝑏𝑘 ) ) ) = ( 𝐶 + Σ 𝑘 ∈ ℕ ( ( ( 𝐶𝑘 ) · ( 𝐶 C𝑐 𝑘 ) ) · ( 𝑏𝑘 ) ) ) )
492 469 470 491 3eqtrd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → Σ 𝑘 ∈ ℕ ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) = ( 𝐶 + Σ 𝑘 ∈ ℕ ( ( ( 𝐶𝑘 ) · ( 𝐶 C𝑐 𝑘 ) ) · ( 𝑏𝑘 ) ) ) )
493 492 oveq1d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( Σ 𝑘 ∈ ℕ ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) + Σ 𝑘 ∈ ℕ ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏𝑘 ) ) ) = ( ( 𝐶 + Σ 𝑘 ∈ ℕ ( ( ( 𝐶𝑘 ) · ( 𝐶 C𝑐 𝑘 ) ) · ( 𝑏𝑘 ) ) ) + Σ 𝑘 ∈ ℕ ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏𝑘 ) ) ) )
494 240 241 352 357 417 isumcl ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → Σ 𝑘 ∈ ℕ ( ( ( 𝐶𝑘 ) · ( 𝐶 C𝑐 𝑘 ) ) · ( 𝑏𝑘 ) ) ∈ ℂ )
495 249 435 mulcld ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( 𝑏 · Σ 𝑘 ∈ ℕ ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏 ↑ ( 𝑘 − 1 ) ) ) ) ∈ ℂ )
496 440 495 eqeltrrd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → Σ 𝑘 ∈ ℕ ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏𝑘 ) ) ∈ ℂ )
497 236 494 496 addassd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( 𝐶 + Σ 𝑘 ∈ ℕ ( ( ( 𝐶𝑘 ) · ( 𝐶 C𝑐 𝑘 ) ) · ( 𝑏𝑘 ) ) ) + Σ 𝑘 ∈ ℕ ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏𝑘 ) ) ) = ( 𝐶 + ( Σ 𝑘 ∈ ℕ ( ( ( 𝐶𝑘 ) · ( 𝐶 C𝑐 𝑘 ) ) · ( 𝑏𝑘 ) ) + Σ 𝑘 ∈ ℕ ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏𝑘 ) ) ) ) )
498 442 493 497 3eqtrd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( 1 + 𝑏 ) · Σ 𝑘 ∈ ℕ ( ( 𝐸𝑏 ) ‘ 𝑘 ) ) = ( 𝐶 + ( Σ 𝑘 ∈ ℕ ( ( ( 𝐶𝑘 ) · ( 𝐶 C𝑐 𝑘 ) ) · ( 𝑏𝑘 ) ) + Σ 𝑘 ∈ ℕ ( ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) · ( 𝑏𝑘 ) ) ) ) )
499 425 430 498 3eqtr4rd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( 1 + 𝑏 ) · Σ 𝑘 ∈ ℕ ( ( 𝐸𝑏 ) ‘ 𝑘 ) ) = ( 𝐶 + Σ 𝑘 ∈ ℕ ( ( ( ( 𝐶𝑘 ) · ( 𝐶 C𝑐 𝑘 ) ) + ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) ) · ( 𝑏𝑘 ) ) ) )
500 simpr ( ( 𝜑𝑘 ∈ ℕ ) → 𝑘 ∈ ℕ )
501 278 500 binomcxplemwb ( ( 𝜑𝑘 ∈ ℕ ) → ( ( ( 𝐶𝑘 ) · ( 𝐶 C𝑐 𝑘 ) ) + ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) ) = ( 𝐶 · ( 𝐶 C𝑐 𝑘 ) ) )
502 501 oveq1d ( ( 𝜑𝑘 ∈ ℕ ) → ( ( ( ( 𝐶𝑘 ) · ( 𝐶 C𝑐 𝑘 ) ) + ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) ) · ( 𝑏𝑘 ) ) = ( ( 𝐶 · ( 𝐶 C𝑐 𝑘 ) ) · ( 𝑏𝑘 ) ) )
503 502 sumeq2dv ( 𝜑 → Σ 𝑘 ∈ ℕ ( ( ( ( 𝐶𝑘 ) · ( 𝐶 C𝑐 𝑘 ) ) + ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) ) · ( 𝑏𝑘 ) ) = Σ 𝑘 ∈ ℕ ( ( 𝐶 · ( 𝐶 C𝑐 𝑘 ) ) · ( 𝑏𝑘 ) ) )
504 503 oveq2d ( 𝜑 → ( 𝐶 + Σ 𝑘 ∈ ℕ ( ( ( ( 𝐶𝑘 ) · ( 𝐶 C𝑐 𝑘 ) ) + ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) ) · ( 𝑏𝑘 ) ) ) = ( 𝐶 + Σ 𝑘 ∈ ℕ ( ( 𝐶 · ( 𝐶 C𝑐 𝑘 ) ) · ( 𝑏𝑘 ) ) ) )
505 504 ad2antrr ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( 𝐶 + Σ 𝑘 ∈ ℕ ( ( ( ( 𝐶𝑘 ) · ( 𝐶 C𝑐 𝑘 ) ) + ( ( 𝐶 − ( 𝑘 − 1 ) ) · ( 𝐶 C𝑐 ( 𝑘 − 1 ) ) ) ) · ( 𝑏𝑘 ) ) ) = ( 𝐶 + Σ 𝑘 ∈ ℕ ( ( 𝐶 · ( 𝐶 C𝑐 𝑘 ) ) · ( 𝑏𝑘 ) ) ) )
506 363 248 252 mulassd ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝐶 · ( 𝐶 C𝑐 𝑘 ) ) · ( 𝑏𝑘 ) ) = ( 𝐶 · ( ( 𝐶 C𝑐 𝑘 ) · ( 𝑏𝑘 ) ) ) )
507 506 sumeq2dv ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → Σ 𝑘 ∈ ℕ ( ( 𝐶 · ( 𝐶 C𝑐 𝑘 ) ) · ( 𝑏𝑘 ) ) = Σ 𝑘 ∈ ℕ ( 𝐶 · ( ( 𝐶 C𝑐 𝑘 ) · ( 𝑏𝑘 ) ) ) )
508 240 241 244 253 258 236 isummulc2 ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( 𝐶 · Σ 𝑘 ∈ ℕ ( ( 𝐶 C𝑐 𝑘 ) · ( 𝑏𝑘 ) ) ) = Σ 𝑘 ∈ ℕ ( 𝐶 · ( ( 𝐶 C𝑐 𝑘 ) · ( 𝑏𝑘 ) ) ) )
509 507 508 eqtr4d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → Σ 𝑘 ∈ ℕ ( ( 𝐶 · ( 𝐶 C𝑐 𝑘 ) ) · ( 𝑏𝑘 ) ) = ( 𝐶 · Σ 𝑘 ∈ ℕ ( ( 𝐶 C𝑐 𝑘 ) · ( 𝑏𝑘 ) ) ) )
510 509 oveq2d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( 𝐶 + Σ 𝑘 ∈ ℕ ( ( 𝐶 · ( 𝐶 C𝑐 𝑘 ) ) · ( 𝑏𝑘 ) ) ) = ( 𝐶 + ( 𝐶 · Σ 𝑘 ∈ ℕ ( ( 𝐶 C𝑐 𝑘 ) · ( 𝑏𝑘 ) ) ) ) )
511 499 505 510 3eqtrd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( 1 + 𝑏 ) · Σ 𝑘 ∈ ℕ ( ( 𝐸𝑏 ) ‘ 𝑘 ) ) = ( 𝐶 + ( 𝐶 · Σ 𝑘 ∈ ℕ ( ( 𝐶 C𝑐 𝑘 ) · ( 𝑏𝑘 ) ) ) ) )
512 238 260 511 3eqtr4rd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( 1 + 𝑏 ) · Σ 𝑘 ∈ ℕ ( ( 𝐸𝑏 ) ‘ 𝑘 ) ) = ( 𝐶 · ( 1 + Σ 𝑘 ∈ ℕ ( ( 𝐶 C𝑐 𝑘 ) · ( 𝑏𝑘 ) ) ) ) )
513 6 a1i ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → 𝑆 = ( 𝑏 ∈ ℂ ↦ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹𝑘 ) · ( 𝑏𝑘 ) ) ) ) )
514 123 a1i ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏 ∈ ℂ ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹𝑘 ) · ( 𝑏𝑘 ) ) ) ∈ V )
515 513 514 fvmpt2d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏 ∈ ℂ ) → ( 𝑆𝑏 ) = ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹𝑘 ) · ( 𝑏𝑘 ) ) ) )
516 120 515 sylan2 ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( 𝑆𝑏 ) = ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹𝑘 ) · ( 𝑏𝑘 ) ) ) )
517 ovexd ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐹𝑘 ) · ( 𝑏𝑘 ) ) ∈ V )
518 516 517 fvmpt2d ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆𝑏 ) ‘ 𝑘 ) = ( ( 𝐹𝑘 ) · ( 𝑏𝑘 ) ) )
519 518 sumeq2dv ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) = Σ 𝑘 ∈ ℕ0 ( ( 𝐹𝑘 ) · ( 𝑏𝑘 ) ) )
520 4 adantr ( ( 𝜑𝑘 ∈ ℕ0 ) → 𝐶 ∈ ℂ )
521 520 131 bcccl ( ( 𝜑𝑘 ∈ ℕ0 ) → ( 𝐶 C𝑐 𝑘 ) ∈ ℂ )
522 133 521 eqeltrd ( ( 𝜑𝑘 ∈ ℕ0 ) → ( 𝐹𝑘 ) ∈ ℂ )
523 522 adantlr ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹𝑘 ) ∈ ℂ )
524 523 adantlr ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹𝑘 ) ∈ ℂ )
525 524 251 mulcld ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐹𝑘 ) · ( 𝑏𝑘 ) ) ∈ ℂ )
526 113 114 518 525 159 isum1p ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → Σ 𝑘 ∈ ℕ0 ( ( 𝐹𝑘 ) · ( 𝑏𝑘 ) ) = ( ( ( 𝑆𝑏 ) ‘ 0 ) + Σ 𝑘 ∈ ( ℤ ‘ ( 0 + 1 ) ) ( ( 𝐹𝑘 ) · ( 𝑏𝑘 ) ) ) )
527 471 fveq2d ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 = 0 ) → ( 𝐹𝑘 ) = ( 𝐹 ‘ 0 ) )
528 527 475 oveq12d ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 = 0 ) → ( ( 𝐹𝑘 ) · ( 𝑏𝑘 ) ) = ( ( 𝐹 ‘ 0 ) · ( 𝑏 ↑ 0 ) ) )
529 ovexd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( 𝐹 ‘ 0 ) · ( 𝑏 ↑ 0 ) ) ∈ V )
530 516 528 478 529 fvmptd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( 𝑆𝑏 ) ‘ 0 ) = ( ( 𝐹 ‘ 0 ) · ( 𝑏 ↑ 0 ) ) )
531 5 a1i ( 𝜑𝐹 = ( 𝑗 ∈ ℕ0 ↦ ( 𝐶 C𝑐 𝑗 ) ) )
532 simpr ( ( 𝜑𝑗 = 0 ) → 𝑗 = 0 )
533 532 oveq2d ( ( 𝜑𝑗 = 0 ) → ( 𝐶 C𝑐 𝑗 ) = ( 𝐶 C𝑐 0 ) )
534 477 a1i ( 𝜑 → 0 ∈ ℕ0 )
535 ovexd ( 𝜑 → ( 𝐶 C𝑐 0 ) ∈ V )
536 531 533 534 535 fvmptd ( 𝜑 → ( 𝐹 ‘ 0 ) = ( 𝐶 C𝑐 0 ) )
537 536 ad2antrr ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( 𝐹 ‘ 0 ) = ( 𝐶 C𝑐 0 ) )
538 537 482 eqtrd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( 𝐹 ‘ 0 ) = 1 )
539 538 485 oveq12d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( 𝐹 ‘ 0 ) · ( 𝑏 ↑ 0 ) ) = ( 1 · 1 ) )
540 239 mulid1d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( 1 · 1 ) = 1 )
541 530 539 540 3eqtrd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( 𝑆𝑏 ) ‘ 0 ) = 1 )
542 488 sumeq1i Σ 𝑘 ∈ ( ℤ ‘ ( 0 + 1 ) ) ( ( 𝐹𝑘 ) · ( 𝑏𝑘 ) ) = Σ 𝑘 ∈ ℕ ( ( 𝐹𝑘 ) · ( 𝑏𝑘 ) )
543 134 adantlr ( ( ( 𝜑𝑏𝐷 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐹𝑘 ) · ( 𝑏𝑘 ) ) = ( ( 𝐶 C𝑐 𝑘 ) · ( 𝑏𝑘 ) ) )
544 242 543 sylan2 ( ( ( 𝜑𝑏𝐷 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝐹𝑘 ) · ( 𝑏𝑘 ) ) = ( ( 𝐶 C𝑐 𝑘 ) · ( 𝑏𝑘 ) ) )
545 544 adantllr ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝐹𝑘 ) · ( 𝑏𝑘 ) ) = ( ( 𝐶 C𝑐 𝑘 ) · ( 𝑏𝑘 ) ) )
546 545 sumeq2dv ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → Σ 𝑘 ∈ ℕ ( ( 𝐹𝑘 ) · ( 𝑏𝑘 ) ) = Σ 𝑘 ∈ ℕ ( ( 𝐶 C𝑐 𝑘 ) · ( 𝑏𝑘 ) ) )
547 542 546 syl5eq ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → Σ 𝑘 ∈ ( ℤ ‘ ( 0 + 1 ) ) ( ( 𝐹𝑘 ) · ( 𝑏𝑘 ) ) = Σ 𝑘 ∈ ℕ ( ( 𝐶 C𝑐 𝑘 ) · ( 𝑏𝑘 ) ) )
548 541 547 oveq12d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( ( 𝑆𝑏 ) ‘ 0 ) + Σ 𝑘 ∈ ( ℤ ‘ ( 0 + 1 ) ) ( ( 𝐹𝑘 ) · ( 𝑏𝑘 ) ) ) = ( 1 + Σ 𝑘 ∈ ℕ ( ( 𝐶 C𝑐 𝑘 ) · ( 𝑏𝑘 ) ) ) )
549 519 526 548 3eqtrrd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( 1 + Σ 𝑘 ∈ ℕ ( ( 𝐶 C𝑐 𝑘 ) · ( 𝑏𝑘 ) ) ) = Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) )
550 549 oveq2d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( 𝐶 · ( 1 + Σ 𝑘 ∈ ℕ ( ( 𝐶 C𝑐 𝑘 ) · ( 𝑏𝑘 ) ) ) ) = ( 𝐶 · Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) ) )
551 512 550 eqtrd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( 1 + 𝑏 ) · Σ 𝑘 ∈ ℕ ( ( 𝐸𝑏 ) ‘ 𝑘 ) ) = ( 𝐶 · Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) ) )
552 236 160 mulcld ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( 𝐶 · Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) ) ∈ ℂ )
553 239 249 addcld ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( 1 + 𝑏 ) ∈ ℂ )
554 eqidd ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝐸𝑏 ) ‘ 𝑘 ) = ( ( 𝐸𝑏 ) ‘ 𝑘 ) )
555 240 241 554 419 390 isumcl ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → Σ 𝑘 ∈ ℕ ( ( 𝐸𝑏 ) ‘ 𝑘 ) ∈ ℂ )
556 239 249 subnegd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( 1 − - 𝑏 ) = ( 1 + 𝑏 ) )
557 249 negcld ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → - 𝑏 ∈ ℂ )
558 elpreima ( abs Fn ℂ → ( 𝑏 ∈ ( abs “ ( 0 [,) 𝑅 ) ) ↔ ( 𝑏 ∈ ℂ ∧ ( abs ‘ 𝑏 ) ∈ ( 0 [,) 𝑅 ) ) ) )
559 87 88 558 mp2b ( 𝑏 ∈ ( abs “ ( 0 [,) 𝑅 ) ) ↔ ( 𝑏 ∈ ℂ ∧ ( abs ‘ 𝑏 ) ∈ ( 0 [,) 𝑅 ) ) )
560 559 simprbi ( 𝑏 ∈ ( abs “ ( 0 [,) 𝑅 ) ) → ( abs ‘ 𝑏 ) ∈ ( 0 [,) 𝑅 ) )
561 560 9 eleq2s ( 𝑏𝐷 → ( abs ‘ 𝑏 ) ∈ ( 0 [,) 𝑅 ) )
562 elico2 ( ( 0 ∈ ℝ ∧ 𝑅 ∈ ℝ* ) → ( ( abs ‘ 𝑏 ) ∈ ( 0 [,) 𝑅 ) ↔ ( ( abs ‘ 𝑏 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝑏 ) ∧ ( abs ‘ 𝑏 ) < 𝑅 ) ) )
563 76 82 562 mp2an ( ( abs ‘ 𝑏 ) ∈ ( 0 [,) 𝑅 ) ↔ ( ( abs ‘ 𝑏 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝑏 ) ∧ ( abs ‘ 𝑏 ) < 𝑅 ) )
564 563 simp3bi ( ( abs ‘ 𝑏 ) ∈ ( 0 [,) 𝑅 ) → ( abs ‘ 𝑏 ) < 𝑅 )
565 561 564 syl ( 𝑏𝐷 → ( abs ‘ 𝑏 ) < 𝑅 )
566 565 adantl ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( abs ‘ 𝑏 ) < 𝑅 )
567 249 absnegd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( abs ‘ - 𝑏 ) = ( abs ‘ 𝑏 ) )
568 567 eqcomd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( abs ‘ 𝑏 ) = ( abs ‘ - 𝑏 ) )
569 74 adantr ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → 𝑅 = 1 )
570 566 568 569 3brtr3d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( abs ‘ - 𝑏 ) < 1 )
571 1re 1 ∈ ℝ
572 abssubne0 ( ( - 𝑏 ∈ ℂ ∧ 1 ∈ ℝ ∧ ( abs ‘ - 𝑏 ) < 1 ) → ( 1 − - 𝑏 ) ≠ 0 )
573 571 572 mp3an2 ( ( - 𝑏 ∈ ℂ ∧ ( abs ‘ - 𝑏 ) < 1 ) → ( 1 − - 𝑏 ) ≠ 0 )
574 557 570 573 syl2anc ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( 1 − - 𝑏 ) ≠ 0 )
575 556 574 eqnetrrd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( 1 + 𝑏 ) ≠ 0 )
576 552 553 555 575 divmuld ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( ( 𝐶 · Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) ) / ( 1 + 𝑏 ) ) = Σ 𝑘 ∈ ℕ ( ( 𝐸𝑏 ) ‘ 𝑘 ) ↔ ( ( 1 + 𝑏 ) · Σ 𝑘 ∈ ℕ ( ( 𝐸𝑏 ) ‘ 𝑘 ) ) = ( 𝐶 · Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) ) ) )
577 551 576 mpbird ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( 𝐶 · Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) ) / ( 1 + 𝑏 ) ) = Σ 𝑘 ∈ ℕ ( ( 𝐸𝑏 ) ‘ 𝑘 ) )
578 236 160 553 575 div23d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( 𝐶 · Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) ) / ( 1 + 𝑏 ) ) = ( ( 𝐶 / ( 1 + 𝑏 ) ) · Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) ) )
579 577 578 eqtr3d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → Σ 𝑘 ∈ ℕ ( ( 𝐸𝑏 ) ‘ 𝑘 ) = ( ( 𝐶 / ( 1 + 𝑏 ) ) · Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) ) )
580 579 mpteq2dva ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( 𝑏𝐷 ↦ Σ 𝑘 ∈ ℕ ( ( 𝐸𝑏 ) ‘ 𝑘 ) ) = ( 𝑏𝐷 ↦ ( ( 𝐶 / ( 1 + 𝑏 ) ) · Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) ) ) )
581 ovexd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( 𝐶 / ( 1 + 𝑏 ) ) ∈ V )
582 sumex Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) ∈ V
583 582 a1i ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) ∈ V )
584 eqidd ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( 𝑏𝐷 ↦ ( 𝐶 / ( 1 + 𝑏 ) ) ) = ( 𝑏𝐷 ↦ ( 𝐶 / ( 1 + 𝑏 ) ) ) )
585 10 a1i ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → 𝑃 = ( 𝑏𝐷 ↦ Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) ) )
586 104 29 183 581 583 584 585 offval2f ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ( 𝑏𝐷 ↦ ( 𝐶 / ( 1 + 𝑏 ) ) ) ∘f · 𝑃 ) = ( 𝑏𝐷 ↦ ( ( 𝐶 / ( 1 + 𝑏 ) ) · Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) ) ) )
587 580 205 586 3eqtr4d ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ℂ D 𝑃 ) = ( ( 𝑏𝐷 ↦ ( 𝐶 / ( 1 + 𝑏 ) ) ) ∘f · 𝑃 ) )
588 587 oveq1d ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ( ℂ D 𝑃 ) ∘f · ( 𝑏𝐷 ↦ ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) ) = ( ( ( 𝑏𝐷 ↦ ( 𝐶 / ( 1 + 𝑏 ) ) ) ∘f · 𝑃 ) ∘f · ( 𝑏𝐷 ↦ ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) ) )
589 223 oveq1d ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ( ℂ D ( 𝑏𝐷 ↦ ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) ) ∘f · 𝑃 ) = ( ( 𝑏𝐷 ↦ ( - 𝐶 · ( ( 1 + 𝑏 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) ) ∘f · 𝑃 ) )
590 588 589 oveq12d ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ( ( ℂ D 𝑃 ) ∘f · ( 𝑏𝐷 ↦ ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) ) ∘f + ( ( ℂ D ( 𝑏𝐷 ↦ ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) ) ∘f · 𝑃 ) ) = ( ( ( ( 𝑏𝐷 ↦ ( 𝐶 / ( 1 + 𝑏 ) ) ) ∘f · 𝑃 ) ∘f · ( 𝑏𝐷 ↦ ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) ) ∘f + ( ( 𝑏𝐷 ↦ ( - 𝐶 · ( ( 1 + 𝑏 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) ) ∘f · 𝑃 ) ) )
591 ovexd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( ( 𝐶 / ( 1 + 𝑏 ) ) · Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) ) · ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) ∈ V )
592 ovexd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( - 𝐶 · ( ( 1 + 𝑏 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) · Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) ) ∈ V )
593 ovexd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( 𝐶 / ( 1 + 𝑏 ) ) · Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) ) ∈ V )
594 ovexd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ∈ V )
595 eqidd ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( 𝑏𝐷 ↦ ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) = ( 𝑏𝐷 ↦ ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) )
596 104 29 183 593 594 586 595 offval2f ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ( ( 𝑏𝐷 ↦ ( 𝐶 / ( 1 + 𝑏 ) ) ) ∘f · 𝑃 ) ∘f · ( 𝑏𝐷 ↦ ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) ) = ( 𝑏𝐷 ↦ ( ( ( 𝐶 / ( 1 + 𝑏 ) ) · Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) ) · ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) ) )
597 ovexd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( - 𝐶 · ( ( 1 + 𝑏 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) ∈ V )
598 eqidd ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( 𝑏𝐷 ↦ ( - 𝐶 · ( ( 1 + 𝑏 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) ) = ( 𝑏𝐷 ↦ ( - 𝐶 · ( ( 1 + 𝑏 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) ) )
599 104 29 183 597 583 598 585 offval2f ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ( 𝑏𝐷 ↦ ( - 𝐶 · ( ( 1 + 𝑏 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) ) ∘f · 𝑃 ) = ( 𝑏𝐷 ↦ ( ( - 𝐶 · ( ( 1 + 𝑏 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) · Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) ) ) )
600 104 29 183 591 592 596 599 offval2f ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ( ( ( 𝑏𝐷 ↦ ( 𝐶 / ( 1 + 𝑏 ) ) ) ∘f · 𝑃 ) ∘f · ( 𝑏𝐷 ↦ ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) ) ∘f + ( ( 𝑏𝐷 ↦ ( - 𝐶 · ( ( 1 + 𝑏 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) ) ∘f · 𝑃 ) ) = ( 𝑏𝐷 ↦ ( ( ( ( 𝐶 / ( 1 + 𝑏 ) ) · Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) ) · ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) + ( ( - 𝐶 · ( ( 1 + 𝑏 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) · Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) ) ) ) )
601 235 590 600 3eqtrd ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ℂ D ( 𝑃f · ( 𝑏𝐷 ↦ ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) ) ) = ( 𝑏𝐷 ↦ ( ( ( ( 𝐶 / ( 1 + 𝑏 ) ) · Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) ) · ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) + ( ( - 𝐶 · ( ( 1 + 𝑏 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) · Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) ) ) ) )
602 236 553 575 divcld ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( 𝐶 / ( 1 + 𝑏 ) ) ∈ ℂ )
603 236 negcld ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → - 𝐶 ∈ ℂ )
604 553 603 cxpcld ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ∈ ℂ )
605 602 160 604 mul32d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( ( 𝐶 / ( 1 + 𝑏 ) ) · Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) ) · ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) = ( ( ( 𝐶 / ( 1 + 𝑏 ) ) · ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) · Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) ) )
606 236 553 604 575 div32d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( 𝐶 / ( 1 + 𝑏 ) ) · ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) = ( 𝐶 · ( ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) / ( 1 + 𝑏 ) ) ) )
607 553 575 603 239 cxpsubd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( 1 + 𝑏 ) ↑𝑐 ( - 𝐶 − 1 ) ) = ( ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) / ( ( 1 + 𝑏 ) ↑𝑐 1 ) ) )
608 553 cxp1d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( 1 + 𝑏 ) ↑𝑐 1 ) = ( 1 + 𝑏 ) )
609 608 oveq2d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) / ( ( 1 + 𝑏 ) ↑𝑐 1 ) ) = ( ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) / ( 1 + 𝑏 ) ) )
610 607 609 eqtr2d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) / ( 1 + 𝑏 ) ) = ( ( 1 + 𝑏 ) ↑𝑐 ( - 𝐶 − 1 ) ) )
611 610 oveq2d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( 𝐶 · ( ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) / ( 1 + 𝑏 ) ) ) = ( 𝐶 · ( ( 1 + 𝑏 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) )
612 606 611 eqtrd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( 𝐶 / ( 1 + 𝑏 ) ) · ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) = ( 𝐶 · ( ( 1 + 𝑏 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) )
613 612 oveq1d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( ( 𝐶 / ( 1 + 𝑏 ) ) · ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) · Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) ) = ( ( 𝐶 · ( ( 1 + 𝑏 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) · Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) ) )
614 605 613 eqtrd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( ( 𝐶 / ( 1 + 𝑏 ) ) · Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) ) · ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) = ( ( 𝐶 · ( ( 1 + 𝑏 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) · Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) ) )
615 603 239 subcld ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( - 𝐶 − 1 ) ∈ ℂ )
616 553 615 cxpcld ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( 1 + 𝑏 ) ↑𝑐 ( - 𝐶 − 1 ) ) ∈ ℂ )
617 236 616 mulneg1d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( - 𝐶 · ( ( 1 + 𝑏 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) = - ( 𝐶 · ( ( 1 + 𝑏 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) )
618 617 oveq1d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( - 𝐶 · ( ( 1 + 𝑏 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) · Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) ) = ( - ( 𝐶 · ( ( 1 + 𝑏 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) · Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) ) )
619 236 616 mulcld ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( 𝐶 · ( ( 1 + 𝑏 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) ∈ ℂ )
620 619 160 mulneg1d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( - ( 𝐶 · ( ( 1 + 𝑏 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) · Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) ) = - ( ( 𝐶 · ( ( 1 + 𝑏 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) · Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) ) )
621 618 620 eqtrd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( - 𝐶 · ( ( 1 + 𝑏 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) · Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) ) = - ( ( 𝐶 · ( ( 1 + 𝑏 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) · Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) ) )
622 614 621 oveq12d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( ( ( 𝐶 / ( 1 + 𝑏 ) ) · Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) ) · ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) + ( ( - 𝐶 · ( ( 1 + 𝑏 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) · Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) ) ) = ( ( ( 𝐶 · ( ( 1 + 𝑏 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) · Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) ) + - ( ( 𝐶 · ( ( 1 + 𝑏 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) · Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) ) ) )
623 619 160 mulcld ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( 𝐶 · ( ( 1 + 𝑏 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) · Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) ) ∈ ℂ )
624 623 negidd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( ( 𝐶 · ( ( 1 + 𝑏 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) · Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) ) + - ( ( 𝐶 · ( ( 1 + 𝑏 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) · Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) ) ) = 0 )
625 622 624 eqtrd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( ( ( 𝐶 / ( 1 + 𝑏 ) ) · Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) ) · ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) + ( ( - 𝐶 · ( ( 1 + 𝑏 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) · Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) ) ) = 0 )
626 625 mpteq2dva ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( 𝑏𝐷 ↦ ( ( ( ( 𝐶 / ( 1 + 𝑏 ) ) · Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) ) · ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) + ( ( - 𝐶 · ( ( 1 + 𝑏 ) ↑𝑐 ( - 𝐶 − 1 ) ) ) · Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑏 ) ‘ 𝑘 ) ) ) ) = ( 𝑏𝐷 ↦ 0 ) )
627 601 626 eqtrd ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ℂ D ( 𝑃f · ( 𝑏𝐷 ↦ ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) ) ) = ( 𝑏𝐷 ↦ 0 ) )
628 nfcv 𝑥 0
629 eqidd ( 𝑥 = 𝑏 → 0 = 0 )
630 30 29 12 628 629 cbvmptf ( 𝑥𝐷 ↦ 0 ) = ( 𝑏𝐷 ↦ 0 )
631 627 630 eqtr4di ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ℂ D ( 𝑃f · ( 𝑏𝐷 ↦ ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) ) ) = ( 𝑥𝐷 ↦ 0 ) )
632 c0ex 0 ∈ V
633 632 snid 0 ∈ { 0 }
634 633 a1i ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑥𝐷 ) → 0 ∈ { 0 } )
635 631 634 fmpt3d ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ℂ D ( 𝑃f · ( 𝑏𝐷 ↦ ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) ) ) : 𝐷 ⟶ { 0 } )
636 635 fdmd ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → dom ( ℂ D ( 𝑃f · ( 𝑏𝐷 ↦ ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) ) ) = 𝐷 )
637 1cnd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑥 ∈ ℂ ) → 1 ∈ ℂ )
638 0cnd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑥 ∈ ℂ ) → 0 ∈ ℂ )
639 dvconst ( 1 ∈ ℂ → ( ℂ D ( ℂ × { 1 } ) ) = ( ℂ × { 0 } ) )
640 196 639 ax-mp ( ℂ D ( ℂ × { 1 } ) ) = ( ℂ × { 0 } )
641 fconstmpt ( ℂ × { 1 } ) = ( 𝑥 ∈ ℂ ↦ 1 )
642 641 oveq2i ( ℂ D ( ℂ × { 1 } ) ) = ( ℂ D ( 𝑥 ∈ ℂ ↦ 1 ) )
643 fconstmpt ( ℂ × { 0 } ) = ( 𝑥 ∈ ℂ ↦ 0 )
644 640 642 643 3eqtr3i ( ℂ D ( 𝑥 ∈ ℂ ↦ 1 ) ) = ( 𝑥 ∈ ℂ ↦ 0 )
645 644 a1i ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ℂ D ( 𝑥 ∈ ℂ ↦ 1 ) ) = ( 𝑥 ∈ ℂ ↦ 0 ) )
646 119 a1i ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → 𝐷 ⊆ ℂ )
647 fvex ( TopOpen ‘ ℂfld ) ∈ V
648 cnfldtps fld ∈ TopSp
649 cnfldbas ℂ = ( Base ‘ ℂfld )
650 eqid ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
651 649 650 tpsuni ( ℂfld ∈ TopSp → ℂ = ( TopOpen ‘ ℂfld ) )
652 648 651 ax-mp ℂ = ( TopOpen ‘ ℂfld )
653 652 restid ( ( TopOpen ‘ ℂfld ) ∈ V → ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) = ( TopOpen ‘ ℂfld ) )
654 647 653 ax-mp ( ( TopOpen ‘ ℂfld ) ↾t ℂ ) = ( TopOpen ‘ ℂfld )
655 654 eqcomi ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
656 650 cnfldtop ( TopOpen ‘ ℂfld ) ∈ Top
657 cnxmet ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
658 650 cnfldtopn ( TopOpen ‘ ℂfld ) = ( MetOpen ‘ ( abs ∘ − ) )
659 658 blopn ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 0 ∈ ℂ ∧ 𝑅 ∈ ℝ* ) → ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ∈ ( TopOpen ‘ ℂfld ) )
660 657 398 82 659 mp3an ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) ∈ ( TopOpen ‘ ℂfld )
661 99 660 eqeltri 𝐷 ∈ ( TopOpen ‘ ℂfld )
662 isopn3i ( ( ( TopOpen ‘ ℂfld ) ∈ Top ∧ 𝐷 ∈ ( TopOpen ‘ ℂfld ) ) → ( ( int ‘ ( TopOpen ‘ ℂfld ) ) ‘ 𝐷 ) = 𝐷 )
663 656 661 662 mp2an ( ( int ‘ ( TopOpen ‘ ℂfld ) ) ‘ 𝐷 ) = 𝐷
664 663 a1i ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ( int ‘ ( TopOpen ‘ ℂfld ) ) ‘ 𝐷 ) = 𝐷 )
665 203 637 638 645 646 655 650 664 dvmptres2 ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ℂ D ( 𝑥𝐷 ↦ 1 ) ) = ( 𝑥𝐷 ↦ 0 ) )
666 192 oveq2i ( ℂ D ( 𝑥𝐷 ↦ 1 ) ) = ( ℂ D ( 𝑏𝐷 ↦ 1 ) )
667 665 666 630 3eqtr3g ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ℂ D ( 𝑏𝐷 ↦ 1 ) ) = ( 𝑏𝐷 ↦ 0 ) )
668 626 601 667 3eqtr4d ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ℂ D ( 𝑃f · ( 𝑏𝐷 ↦ ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) ) ) = ( ℂ D ( 𝑏𝐷 ↦ 1 ) ) )
669 1rp 1 ∈ ℝ+
670 74 669 eqeltrdi ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → 𝑅 ∈ ℝ+ )
671 blcntr ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 0 ∈ ℂ ∧ 𝑅 ∈ ℝ+ ) → 0 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) )
672 657 398 671 mp3an12 ( 𝑅 ∈ ℝ+ → 0 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) )
673 670 672 syl ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → 0 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 𝑅 ) )
674 673 99 eleqtrrdi ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → 0 ∈ 𝐷 )
675 0zd ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → 0 ∈ ℤ )
676 eqidd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆 ‘ 0 ) ‘ 𝑘 ) = ( ( 𝑆 ‘ 0 ) ‘ 𝑘 ) )
677 nfv 𝑏 𝜑
678 29 nfel2 𝑏 0 ∈ 𝐷
679 677 678 nfan 𝑏 ( 𝜑 ∧ 0 ∈ 𝐷 )
680 nfv 𝑏 𝑘 ∈ ℕ0
681 679 680 nfan 𝑏 ( ( 𝜑 ∧ 0 ∈ 𝐷 ) ∧ 𝑘 ∈ ℕ0 )
682 16 12 nffv 𝑏 ( 𝑆 ‘ 0 )
683 682 35 nffv 𝑏 ( ( 𝑆 ‘ 0 ) ‘ 𝑘 )
684 683 nfel1 𝑏 ( ( 𝑆 ‘ 0 ) ‘ 𝑘 ) ∈ ℂ
685 681 684 nfim 𝑏 ( ( ( 𝜑 ∧ 0 ∈ 𝐷 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆 ‘ 0 ) ‘ 𝑘 ) ∈ ℂ )
686 eleq1 ( 𝑏 = 0 → ( 𝑏𝐷 ↔ 0 ∈ 𝐷 ) )
687 686 anbi2d ( 𝑏 = 0 → ( ( 𝜑𝑏𝐷 ) ↔ ( 𝜑 ∧ 0 ∈ 𝐷 ) ) )
688 687 anbi1d ( 𝑏 = 0 → ( ( ( 𝜑𝑏𝐷 ) ∧ 𝑘 ∈ ℕ0 ) ↔ ( ( 𝜑 ∧ 0 ∈ 𝐷 ) ∧ 𝑘 ∈ ℕ0 ) ) )
689 fveq2 ( 𝑏 = 0 → ( 𝑆𝑏 ) = ( 𝑆 ‘ 0 ) )
690 689 fveq1d ( 𝑏 = 0 → ( ( 𝑆𝑏 ) ‘ 𝑘 ) = ( ( 𝑆 ‘ 0 ) ‘ 𝑘 ) )
691 690 eleq1d ( 𝑏 = 0 → ( ( ( 𝑆𝑏 ) ‘ 𝑘 ) ∈ ℂ ↔ ( ( 𝑆 ‘ 0 ) ‘ 𝑘 ) ∈ ℂ ) )
692 688 691 imbi12d ( 𝑏 = 0 → ( ( ( ( 𝜑𝑏𝐷 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆𝑏 ) ‘ 𝑘 ) ∈ ℂ ) ↔ ( ( ( 𝜑 ∧ 0 ∈ 𝐷 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆 ‘ 0 ) ‘ 𝑘 ) ∈ ℂ ) ) )
693 685 632 692 144 vtoclf ( ( ( 𝜑 ∧ 0 ∈ 𝐷 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆 ‘ 0 ) ‘ 𝑘 ) ∈ ℂ )
694 674 693 syldanl ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆 ‘ 0 ) ‘ 𝑘 ) ∈ ℂ )
695 12 14 682 nfseq 𝑏 seq 0 ( + , ( 𝑆 ‘ 0 ) )
696 695 nfel1 𝑏 seq 0 ( + , ( 𝑆 ‘ 0 ) ) ∈ dom ⇝
697 679 696 nfim 𝑏 ( ( 𝜑 ∧ 0 ∈ 𝐷 ) → seq 0 ( + , ( 𝑆 ‘ 0 ) ) ∈ dom ⇝ )
698 689 seqeq3d ( 𝑏 = 0 → seq 0 ( + , ( 𝑆𝑏 ) ) = seq 0 ( + , ( 𝑆 ‘ 0 ) ) )
699 698 eleq1d ( 𝑏 = 0 → ( seq 0 ( + , ( 𝑆𝑏 ) ) ∈ dom ⇝ ↔ seq 0 ( + , ( 𝑆 ‘ 0 ) ) ∈ dom ⇝ ) )
700 687 699 imbi12d ( 𝑏 = 0 → ( ( ( 𝜑𝑏𝐷 ) → seq 0 ( + , ( 𝑆𝑏 ) ) ∈ dom ⇝ ) ↔ ( ( 𝜑 ∧ 0 ∈ 𝐷 ) → seq 0 ( + , ( 𝑆 ‘ 0 ) ) ∈ dom ⇝ ) ) )
701 697 632 700 158 vtoclf ( ( 𝜑 ∧ 0 ∈ 𝐷 ) → seq 0 ( + , ( 𝑆 ‘ 0 ) ) ∈ dom ⇝ )
702 674 701 syldan ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → seq 0 ( + , ( 𝑆 ‘ 0 ) ) ∈ dom ⇝ )
703 113 675 676 694 702 isum1p ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → Σ 𝑘 ∈ ℕ0 ( ( 𝑆 ‘ 0 ) ‘ 𝑘 ) = ( ( ( 𝑆 ‘ 0 ) ‘ 0 ) + Σ 𝑘 ∈ ( ℤ ‘ ( 0 + 1 ) ) ( ( 𝑆 ‘ 0 ) ‘ 𝑘 ) ) )
704 133 adantlr ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹𝑘 ) = ( 𝐶 C𝑐 𝑘 ) )
705 704 adantlr ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏 = 0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹𝑘 ) = ( 𝐶 C𝑐 𝑘 ) )
706 simplr ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏 = 0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑏 = 0 )
707 706 oveq1d ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏 = 0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑏𝑘 ) = ( 0 ↑ 𝑘 ) )
708 705 707 oveq12d ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏 = 0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐹𝑘 ) · ( 𝑏𝑘 ) ) = ( ( 𝐶 C𝑐 𝑘 ) · ( 0 ↑ 𝑘 ) ) )
709 708 mpteq2dva ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏 = 0 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹𝑘 ) · ( 𝑏𝑘 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐶 C𝑐 𝑘 ) · ( 0 ↑ 𝑘 ) ) ) )
710 122 mptex ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐶 C𝑐 𝑘 ) · ( 0 ↑ 𝑘 ) ) ) ∈ V
711 710 a1i ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐶 C𝑐 𝑘 ) · ( 0 ↑ 𝑘 ) ) ) ∈ V )
712 513 709 100 711 fvmptd ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( 𝑆 ‘ 0 ) = ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐶 C𝑐 𝑘 ) · ( 0 ↑ 𝑘 ) ) ) )
713 simpr ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 = 0 ) → 𝑘 = 0 )
714 713 oveq2d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 = 0 ) → ( 𝐶 C𝑐 𝑘 ) = ( 𝐶 C𝑐 0 ) )
715 713 oveq2d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 = 0 ) → ( 0 ↑ 𝑘 ) = ( 0 ↑ 0 ) )
716 714 715 oveq12d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 = 0 ) → ( ( 𝐶 C𝑐 𝑘 ) · ( 0 ↑ 𝑘 ) ) = ( ( 𝐶 C𝑐 0 ) · ( 0 ↑ 0 ) ) )
717 477 a1i ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → 0 ∈ ℕ0 )
718 ovexd ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ( 𝐶 C𝑐 0 ) · ( 0 ↑ 0 ) ) ∈ V )
719 712 716 717 718 fvmptd ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ( 𝑆 ‘ 0 ) ‘ 0 ) = ( ( 𝐶 C𝑐 0 ) · ( 0 ↑ 0 ) ) )
720 4 adantr ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → 𝐶 ∈ ℂ )
721 720 bccn0 ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( 𝐶 C𝑐 0 ) = 1 )
722 100 exp0d ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( 0 ↑ 0 ) = 1 )
723 721 722 oveq12d ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ( 𝐶 C𝑐 0 ) · ( 0 ↑ 0 ) ) = ( 1 · 1 ) )
724 1t1e1 ( 1 · 1 ) = 1
725 724 a1i ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( 1 · 1 ) = 1 )
726 719 723 725 3eqtrd ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ( 𝑆 ‘ 0 ) ‘ 0 ) = 1 )
727 ovexd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐶 C𝑐 𝑘 ) · ( 0 ↑ 𝑘 ) ) ∈ V )
728 712 727 fvmpt2d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆 ‘ 0 ) ‘ 𝑘 ) = ( ( 𝐶 C𝑐 𝑘 ) · ( 0 ↑ 𝑘 ) ) )
729 242 728 sylan2 ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑆 ‘ 0 ) ‘ 𝑘 ) = ( ( 𝐶 C𝑐 𝑘 ) · ( 0 ↑ 𝑘 ) ) )
730 simpr ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℕ )
731 730 0expd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ ) → ( 0 ↑ 𝑘 ) = 0 )
732 731 oveq2d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝐶 C𝑐 𝑘 ) · ( 0 ↑ 𝑘 ) ) = ( ( 𝐶 C𝑐 𝑘 ) · 0 ) )
733 521 adantlr ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐶 C𝑐 𝑘 ) ∈ ℂ )
734 242 733 sylan2 ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ ) → ( 𝐶 C𝑐 𝑘 ) ∈ ℂ )
735 734 mul01d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝐶 C𝑐 𝑘 ) · 0 ) = 0 )
736 729 732 735 3eqtrd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑆 ‘ 0 ) ‘ 𝑘 ) = 0 )
737 736 sumeq2dv ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → Σ 𝑘 ∈ ℕ ( ( 𝑆 ‘ 0 ) ‘ 𝑘 ) = Σ 𝑘 ∈ ℕ 0 )
738 444 sumeq1i Σ 𝑘 ∈ ℕ ( ( 𝑆 ‘ 0 ) ‘ 𝑘 ) = Σ 𝑘 ∈ ( ℤ ‘ ( 0 + 1 ) ) ( ( 𝑆 ‘ 0 ) ‘ 𝑘 )
739 240 eqimssi ℕ ⊆ ( ℤ ‘ 1 )
740 739 orci ( ℕ ⊆ ( ℤ ‘ 1 ) ∨ ℕ ∈ Fin )
741 sumz ( ( ℕ ⊆ ( ℤ ‘ 1 ) ∨ ℕ ∈ Fin ) → Σ 𝑘 ∈ ℕ 0 = 0 )
742 740 741 ax-mp Σ 𝑘 ∈ ℕ 0 = 0
743 737 738 742 3eqtr3g ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → Σ 𝑘 ∈ ( ℤ ‘ ( 0 + 1 ) ) ( ( 𝑆 ‘ 0 ) ‘ 𝑘 ) = 0 )
744 726 743 oveq12d ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ( ( 𝑆 ‘ 0 ) ‘ 0 ) + Σ 𝑘 ∈ ( ℤ ‘ ( 0 + 1 ) ) ( ( 𝑆 ‘ 0 ) ‘ 𝑘 ) ) = ( 1 + 0 ) )
745 703 744 eqtrd ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → Σ 𝑘 ∈ ℕ0 ( ( 𝑆 ‘ 0 ) ‘ 𝑘 ) = ( 1 + 0 ) )
746 1p0e1 ( 1 + 0 ) = 1
747 746 oveq1i ( ( 1 + 0 ) ↑𝑐 - 𝐶 ) = ( 1 ↑𝑐 - 𝐶 )
748 720 negcld ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → - 𝐶 ∈ ℂ )
749 748 1cxpd ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( 1 ↑𝑐 - 𝐶 ) = 1 )
750 747 749 syl5eq ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ( 1 + 0 ) ↑𝑐 - 𝐶 ) = 1 )
751 745 750 oveq12d ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( Σ 𝑘 ∈ ℕ0 ( ( 𝑆 ‘ 0 ) ‘ 𝑘 ) · ( ( 1 + 0 ) ↑𝑐 - 𝐶 ) ) = ( ( 1 + 0 ) · 1 ) )
752 746 oveq1i ( ( 1 + 0 ) · 1 ) = ( 1 · 1 )
753 752 724 eqtri ( ( 1 + 0 ) · 1 ) = 1
754 751 753 eqtrdi ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( Σ 𝑘 ∈ ℕ0 ( ( 𝑆 ‘ 0 ) ‘ 𝑘 ) · ( ( 1 + 0 ) ↑𝑐 - 𝐶 ) ) = 1 )
755 162 ffnd ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → 𝑃 Fn 𝐷 )
756 175 ffnd ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( 𝑏𝐷 ↦ ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) Fn 𝐷 )
757 43 a1i ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 0 ∈ 𝐷 ) → 𝑃 = ( 𝑥𝐷 ↦ Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑥 ) ‘ 𝑘 ) ) )
758 simplr ( ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 0 ∈ 𝐷 ) ∧ 𝑥 = 0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑥 = 0 )
759 758 fveq2d ( ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 0 ∈ 𝐷 ) ∧ 𝑥 = 0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑆𝑥 ) = ( 𝑆 ‘ 0 ) )
760 759 fveq1d ( ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 0 ∈ 𝐷 ) ∧ 𝑥 = 0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆𝑥 ) ‘ 𝑘 ) = ( ( 𝑆 ‘ 0 ) ‘ 𝑘 ) )
761 760 sumeq2dv ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 0 ∈ 𝐷 ) ∧ 𝑥 = 0 ) → Σ 𝑘 ∈ ℕ0 ( ( 𝑆𝑥 ) ‘ 𝑘 ) = Σ 𝑘 ∈ ℕ0 ( ( 𝑆 ‘ 0 ) ‘ 𝑘 ) )
762 simpr ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 0 ∈ 𝐷 ) → 0 ∈ 𝐷 )
763 sumex Σ 𝑘 ∈ ℕ0 ( ( 𝑆 ‘ 0 ) ‘ 𝑘 ) ∈ V
764 763 a1i ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 0 ∈ 𝐷 ) → Σ 𝑘 ∈ ℕ0 ( ( 𝑆 ‘ 0 ) ‘ 𝑘 ) ∈ V )
765 757 761 762 764 fvmptd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 0 ∈ 𝐷 ) → ( 𝑃 ‘ 0 ) = Σ 𝑘 ∈ ℕ0 ( ( 𝑆 ‘ 0 ) ‘ 𝑘 ) )
766 174 a1i ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 0 ∈ 𝐷 ) → ( 𝑏𝐷 ↦ ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) = ( 𝑥𝐷 ↦ ( ( 1 + 𝑥 ) ↑𝑐 - 𝐶 ) ) )
767 simpr ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 0 ∈ 𝐷 ) ∧ 𝑥 = 0 ) → 𝑥 = 0 )
768 767 oveq2d ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 0 ∈ 𝐷 ) ∧ 𝑥 = 0 ) → ( 1 + 𝑥 ) = ( 1 + 0 ) )
769 768 oveq1d ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 0 ∈ 𝐷 ) ∧ 𝑥 = 0 ) → ( ( 1 + 𝑥 ) ↑𝑐 - 𝐶 ) = ( ( 1 + 0 ) ↑𝑐 - 𝐶 ) )
770 ovexd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 0 ∈ 𝐷 ) → ( ( 1 + 0 ) ↑𝑐 - 𝐶 ) ∈ V )
771 766 769 762 770 fvmptd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 0 ∈ 𝐷 ) → ( ( 𝑏𝐷 ↦ ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) ‘ 0 ) = ( ( 1 + 0 ) ↑𝑐 - 𝐶 ) )
772 755 756 183 183 184 765 771 ofval ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 0 ∈ 𝐷 ) → ( ( 𝑃f · ( 𝑏𝐷 ↦ ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) ) ‘ 0 ) = ( Σ 𝑘 ∈ ℕ0 ( ( 𝑆 ‘ 0 ) ‘ 𝑘 ) · ( ( 1 + 0 ) ↑𝑐 - 𝐶 ) ) )
773 674 772 mpdan ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ( 𝑃f · ( 𝑏𝐷 ↦ ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) ) ‘ 0 ) = ( Σ 𝑘 ∈ ℕ0 ( ( 𝑆 ‘ 0 ) ‘ 𝑘 ) · ( ( 1 + 0 ) ↑𝑐 - 𝐶 ) ) )
774 193 fveq1i ( ( 𝐷 × { 1 } ) ‘ 0 ) = ( ( 𝑏𝐷 ↦ 1 ) ‘ 0 )
775 186 fvconst2 ( 0 ∈ 𝐷 → ( ( 𝐷 × { 1 } ) ‘ 0 ) = 1 )
776 674 775 syl ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ( 𝐷 × { 1 } ) ‘ 0 ) = 1 )
777 774 776 eqtr3id ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ( 𝑏𝐷 ↦ 1 ) ‘ 0 ) = 1 )
778 754 773 777 3eqtr4d ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ( 𝑃f · ( 𝑏𝐷 ↦ ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) ) ‘ 0 ) = ( ( 𝑏𝐷 ↦ 1 ) ‘ 0 ) )
779 99 100 101 185 201 636 668 674 778 dv11cn ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( 𝑃f · ( 𝑏𝐷 ↦ ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) ) = ( 𝑏𝐷 ↦ 1 ) )
780 779 oveq1d ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ( 𝑃f · ( 𝑏𝐷 ↦ ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) ) ∘f / ( 𝑏𝐷 ↦ ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) ) = ( ( 𝑏𝐷 ↦ 1 ) ∘f / ( 𝑏𝐷 ↦ ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) ) )
781 nfv 𝑏 ( 1 + 𝑥 ) ≠ 0
782 106 781 nfim 𝑏 ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑥𝐷 ) → ( 1 + 𝑥 ) ≠ 0 )
783 172 neeq1d ( 𝑏 = 𝑥 → ( ( 1 + 𝑏 ) ≠ 0 ↔ ( 1 + 𝑥 ) ≠ 0 ) )
784 110 783 imbi12d ( 𝑏 = 𝑥 → ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( 1 + 𝑏 ) ≠ 0 ) ↔ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑥𝐷 ) → ( 1 + 𝑥 ) ≠ 0 ) ) )
785 782 784 575 chvarfv ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑥𝐷 ) → ( 1 + 𝑥 ) ≠ 0 )
786 166 785 168 cxpne0d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑥𝐷 ) → ( ( 1 + 𝑥 ) ↑𝑐 - 𝐶 ) ≠ 0 )
787 eldifsn ( ( ( 1 + 𝑥 ) ↑𝑐 - 𝐶 ) ∈ ( ℂ ∖ { 0 } ) ↔ ( ( ( 1 + 𝑥 ) ↑𝑐 - 𝐶 ) ∈ ℂ ∧ ( ( 1 + 𝑥 ) ↑𝑐 - 𝐶 ) ≠ 0 ) )
788 169 786 787 sylanbrc ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑥𝐷 ) → ( ( 1 + 𝑥 ) ↑𝑐 - 𝐶 ) ∈ ( ℂ ∖ { 0 } ) )
789 788 174 fmptd ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( 𝑏𝐷 ↦ ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) : 𝐷 ⟶ ( ℂ ∖ { 0 } ) )
790 ofdivcan4 ( ( 𝐷 ∈ V ∧ 𝑃 : 𝐷 ⟶ ℂ ∧ ( 𝑏𝐷 ↦ ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) : 𝐷 ⟶ ( ℂ ∖ { 0 } ) ) → ( ( 𝑃f · ( 𝑏𝐷 ↦ ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) ) ∘f / ( 𝑏𝐷 ↦ ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) ) = 𝑃 )
791 183 162 789 790 syl3anc ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ( 𝑃f · ( 𝑏𝐷 ↦ ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) ) ∘f / ( 𝑏𝐷 ↦ ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) ) = 𝑃 )
792 eqidd ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( 𝑏𝐷 ↦ 1 ) = ( 𝑏𝐷 ↦ 1 ) )
793 104 29 183 239 604 792 595 offval2f ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ( 𝑏𝐷 ↦ 1 ) ∘f / ( 𝑏𝐷 ↦ ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) ) = ( 𝑏𝐷 ↦ ( 1 / ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) ) )
794 780 791 793 3eqtr3d ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → 𝑃 = ( 𝑏𝐷 ↦ ( 1 / ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) ) )
795 553 575 603 cxpnegd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( 1 + 𝑏 ) ↑𝑐 - - 𝐶 ) = ( 1 / ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) )
796 236 negnegd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → - - 𝐶 = 𝐶 )
797 796 oveq2d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( ( 1 + 𝑏 ) ↑𝑐 - - 𝐶 ) = ( ( 1 + 𝑏 ) ↑𝑐 𝐶 ) )
798 795 797 eqtr3d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏𝐷 ) → ( 1 / ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) = ( ( 1 + 𝑏 ) ↑𝑐 𝐶 ) )
799 798 mpteq2dva ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( 𝑏𝐷 ↦ ( 1 / ( ( 1 + 𝑏 ) ↑𝑐 - 𝐶 ) ) ) = ( 𝑏𝐷 ↦ ( ( 1 + 𝑏 ) ↑𝑐 𝐶 ) ) )
800 794 799 eqtrd ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → 𝑃 = ( 𝑏𝐷 ↦ ( ( 1 + 𝑏 ) ↑𝑐 𝐶 ) ) )
801 nfcv 𝑥 ( ( 1 + 𝑏 ) ↑𝑐 𝐶 )
802 nfcv 𝑏 ( ( 1 + 𝑥 ) ↑𝑐 𝐶 )
803 172 oveq1d ( 𝑏 = 𝑥 → ( ( 1 + 𝑏 ) ↑𝑐 𝐶 ) = ( ( 1 + 𝑥 ) ↑𝑐 𝐶 ) )
804 29 30 801 802 803 cbvmptf ( 𝑏𝐷 ↦ ( ( 1 + 𝑏 ) ↑𝑐 𝐶 ) ) = ( 𝑥𝐷 ↦ ( ( 1 + 𝑥 ) ↑𝑐 𝐶 ) )
805 800 804 eqtrdi ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → 𝑃 = ( 𝑥𝐷 ↦ ( ( 1 + 𝑥 ) ↑𝑐 𝐶 ) ) )
806 simpr ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑥 = ( 𝐵 / 𝐴 ) ) → 𝑥 = ( 𝐵 / 𝐴 ) )
807 806 oveq2d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑥 = ( 𝐵 / 𝐴 ) ) → ( 1 + 𝑥 ) = ( 1 + ( 𝐵 / 𝐴 ) ) )
808 807 oveq1d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑥 = ( 𝐵 / 𝐴 ) ) → ( ( 1 + 𝑥 ) ↑𝑐 𝐶 ) = ( ( 1 + ( 𝐵 / 𝐴 ) ) ↑𝑐 𝐶 ) )
809 1cnd ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → 1 ∈ ℂ )
810 809 63 addcld ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( 1 + ( 𝐵 / 𝐴 ) ) ∈ ℂ )
811 810 720 cxpcld ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ( 1 + ( 𝐵 / 𝐴 ) ) ↑𝑐 𝐶 ) ∈ ℂ )
812 805 808 92 811 fvmptd ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( 𝑃 ‘ ( 𝐵 / 𝐴 ) ) = ( ( 1 + ( 𝐵 / 𝐴 ) ) ↑𝑐 𝐶 ) )
813 704 adantlr ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏 = ( 𝐵 / 𝐴 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹𝑘 ) = ( 𝐶 C𝑐 𝑘 ) )
814 simplr ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏 = ( 𝐵 / 𝐴 ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑏 = ( 𝐵 / 𝐴 ) )
815 814 oveq1d ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏 = ( 𝐵 / 𝐴 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑏𝑘 ) = ( ( 𝐵 / 𝐴 ) ↑ 𝑘 ) )
816 813 815 oveq12d ( ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏 = ( 𝐵 / 𝐴 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐹𝑘 ) · ( 𝑏𝑘 ) ) = ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐵 / 𝐴 ) ↑ 𝑘 ) ) )
817 816 mpteq2dva ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑏 = ( 𝐵 / 𝐴 ) ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐹𝑘 ) · ( 𝑏𝑘 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐵 / 𝐴 ) ↑ 𝑘 ) ) ) )
818 122 mptex ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐵 / 𝐴 ) ↑ 𝑘 ) ) ) ∈ V
819 818 a1i ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐵 / 𝐴 ) ↑ 𝑘 ) ) ) ∈ V )
820 513 817 63 819 fvmptd ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( 𝑆 ‘ ( 𝐵 / 𝐴 ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐵 / 𝐴 ) ↑ 𝑘 ) ) ) )
821 ovexd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐵 / 𝐴 ) ↑ 𝑘 ) ) ∈ V )
822 820 821 fvmpt2d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑆 ‘ ( 𝐵 / 𝐴 ) ) ‘ 𝑘 ) = ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐵 / 𝐴 ) ↑ 𝑘 ) ) )
823 822 sumeq2dv ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → Σ 𝑘 ∈ ℕ0 ( ( 𝑆 ‘ ( 𝐵 / 𝐴 ) ) ‘ 𝑘 ) = Σ 𝑘 ∈ ℕ0 ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐵 / 𝐴 ) ↑ 𝑘 ) ) )
824 95 812 823 3eqtr3d ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ( 1 + ( 𝐵 / 𝐴 ) ) ↑𝑐 𝐶 ) = Σ 𝑘 ∈ ℕ0 ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐵 / 𝐴 ) ↑ 𝑘 ) ) )
825 824 oveq1d ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ( ( 1 + ( 𝐵 / 𝐴 ) ) ↑𝑐 𝐶 ) · ( 𝐴𝑐 𝐶 ) ) = ( Σ 𝑘 ∈ ℕ0 ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐵 / 𝐴 ) ↑ 𝑘 ) ) · ( 𝐴𝑐 𝐶 ) ) )
826 2 1 rerpdivcld ( 𝜑 → ( 𝐵 / 𝐴 ) ∈ ℝ )
827 826 adantr ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( 𝐵 / 𝐴 ) ∈ ℝ )
828 69 827 readdcld ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( 1 + ( 𝐵 / 𝐴 ) ) ∈ ℝ )
829 df-neg - ( 𝐵 / 𝐴 ) = ( 0 − ( 𝐵 / 𝐴 ) )
830 826 recnd ( 𝜑 → ( 𝐵 / 𝐴 ) ∈ ℂ )
831 830 negcld ( 𝜑 → - ( 𝐵 / 𝐴 ) ∈ ℂ )
832 831 abscld ( 𝜑 → ( abs ‘ - ( 𝐵 / 𝐴 ) ) ∈ ℝ )
833 1red ( 𝜑 → 1 ∈ ℝ )
834 830 absnegd ( 𝜑 → ( abs ‘ - ( 𝐵 / 𝐴 ) ) = ( abs ‘ ( 𝐵 / 𝐴 ) ) )
835 1 rpne0d ( 𝜑𝐴 ≠ 0 )
836 49 51 835 absdivd ( 𝜑 → ( abs ‘ ( 𝐵 / 𝐴 ) ) = ( ( abs ‘ 𝐵 ) / ( abs ‘ 𝐴 ) ) )
837 834 836 eqtrd ( 𝜑 → ( abs ‘ - ( 𝐵 / 𝐴 ) ) = ( ( abs ‘ 𝐵 ) / ( abs ‘ 𝐴 ) ) )
838 49 abscld ( 𝜑 → ( abs ‘ 𝐵 ) ∈ ℝ )
839 669 a1i ( 𝜑 → 1 ∈ ℝ+ )
840 51 835 absrpcld ( 𝜑 → ( abs ‘ 𝐴 ) ∈ ℝ+ )
841 838 recnd ( 𝜑 → ( abs ‘ 𝐵 ) ∈ ℂ )
842 841 div1d ( 𝜑 → ( ( abs ‘ 𝐵 ) / 1 ) = ( abs ‘ 𝐵 ) )
843 842 3 eqbrtrd ( 𝜑 → ( ( abs ‘ 𝐵 ) / 1 ) < ( abs ‘ 𝐴 ) )
844 838 839 840 843 ltdiv23d ( 𝜑 → ( ( abs ‘ 𝐵 ) / ( abs ‘ 𝐴 ) ) < 1 )
845 837 844 eqbrtrd ( 𝜑 → ( abs ‘ - ( 𝐵 / 𝐴 ) ) < 1 )
846 832 833 845 ltled ( 𝜑 → ( abs ‘ - ( 𝐵 / 𝐴 ) ) ≤ 1 )
847 826 renegcld ( 𝜑 → - ( 𝐵 / 𝐴 ) ∈ ℝ )
848 847 833 absled ( 𝜑 → ( ( abs ‘ - ( 𝐵 / 𝐴 ) ) ≤ 1 ↔ ( - 1 ≤ - ( 𝐵 / 𝐴 ) ∧ - ( 𝐵 / 𝐴 ) ≤ 1 ) ) )
849 846 848 mpbid ( 𝜑 → ( - 1 ≤ - ( 𝐵 / 𝐴 ) ∧ - ( 𝐵 / 𝐴 ) ≤ 1 ) )
850 849 simprd ( 𝜑 → - ( 𝐵 / 𝐴 ) ≤ 1 )
851 829 850 eqbrtrrid ( 𝜑 → ( 0 − ( 𝐵 / 𝐴 ) ) ≤ 1 )
852 0red ( 𝜑 → 0 ∈ ℝ )
853 852 826 833 lesubaddd ( 𝜑 → ( ( 0 − ( 𝐵 / 𝐴 ) ) ≤ 1 ↔ 0 ≤ ( 1 + ( 𝐵 / 𝐴 ) ) ) )
854 851 853 mpbid ( 𝜑 → 0 ≤ ( 1 + ( 𝐵 / 𝐴 ) ) )
855 854 adantr ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → 0 ≤ ( 1 + ( 𝐵 / 𝐴 ) ) )
856 1 adantr ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → 𝐴 ∈ ℝ+ )
857 856 rpred ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → 𝐴 ∈ ℝ )
858 856 rpge0d ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → 0 ≤ 𝐴 )
859 828 855 857 858 720 mulcxpd ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ( ( 1 + ( 𝐵 / 𝐴 ) ) · 𝐴 ) ↑𝑐 𝐶 ) = ( ( ( 1 + ( 𝐵 / 𝐴 ) ) ↑𝑐 𝐶 ) · ( 𝐴𝑐 𝐶 ) ) )
860 809 63 52 adddird ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ( 1 + ( 𝐵 / 𝐴 ) ) · 𝐴 ) = ( ( 1 · 𝐴 ) + ( ( 𝐵 / 𝐴 ) · 𝐴 ) ) )
861 52 mulid2d ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( 1 · 𝐴 ) = 𝐴 )
862 50 52 62 divcan1d ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ( 𝐵 / 𝐴 ) · 𝐴 ) = 𝐵 )
863 861 862 oveq12d ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ( 1 · 𝐴 ) + ( ( 𝐵 / 𝐴 ) · 𝐴 ) ) = ( 𝐴 + 𝐵 ) )
864 860 863 eqtrd ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ( 1 + ( 𝐵 / 𝐴 ) ) · 𝐴 ) = ( 𝐴 + 𝐵 ) )
865 864 oveq1d ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ( ( 1 + ( 𝐵 / 𝐴 ) ) · 𝐴 ) ↑𝑐 𝐶 ) = ( ( 𝐴 + 𝐵 ) ↑𝑐 𝐶 ) )
866 859 865 eqtr3d ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ( ( 1 + ( 𝐵 / 𝐴 ) ) ↑𝑐 𝐶 ) · ( 𝐴𝑐 𝐶 ) ) = ( ( 𝐴 + 𝐵 ) ↑𝑐 𝐶 ) )
867 63 adantr ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐵 / 𝐴 ) ∈ ℂ )
868 simpr ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
869 867 868 expcld ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐵 / 𝐴 ) ↑ 𝑘 ) ∈ ℂ )
870 733 869 mulcld ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐵 / 𝐴 ) ↑ 𝑘 ) ) ∈ ℂ )
871 1 2 3 4 5 6 7 8 9 binomcxplemcvg ( ( 𝜑 ∧ ( 𝐵 / 𝐴 ) ∈ 𝐷 ) → ( seq 0 ( + , ( 𝑆 ‘ ( 𝐵 / 𝐴 ) ) ) ∈ dom ⇝ ∧ seq 1 ( + , ( 𝐸 ‘ ( 𝐵 / 𝐴 ) ) ) ∈ dom ⇝ ) )
872 871 simpld ( ( 𝜑 ∧ ( 𝐵 / 𝐴 ) ∈ 𝐷 ) → seq 0 ( + , ( 𝑆 ‘ ( 𝐵 / 𝐴 ) ) ) ∈ dom ⇝ )
873 92 872 syldan ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → seq 0 ( + , ( 𝑆 ‘ ( 𝐵 / 𝐴 ) ) ) ∈ dom ⇝ )
874 52 720 cxpcld ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( 𝐴𝑐 𝐶 ) ∈ ℂ )
875 113 675 822 870 873 874 isummulc1 ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( Σ 𝑘 ∈ ℕ0 ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐵 / 𝐴 ) ↑ 𝑘 ) ) · ( 𝐴𝑐 𝐶 ) ) = Σ 𝑘 ∈ ℕ0 ( ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐵 / 𝐴 ) ↑ 𝑘 ) ) · ( 𝐴𝑐 𝐶 ) ) )
876 49 ad2antrr ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝐵 ∈ ℂ )
877 51 ad2antrr ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝐴 ∈ ℂ )
878 835 ad2antrr ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝐴 ≠ 0 )
879 876 877 878 divrecd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐵 / 𝐴 ) = ( 𝐵 · ( 1 / 𝐴 ) ) )
880 879 oveq1d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐵 / 𝐴 ) ↑ 𝑘 ) = ( ( 𝐵 · ( 1 / 𝐴 ) ) ↑ 𝑘 ) )
881 877 878 reccld ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 1 / 𝐴 ) ∈ ℂ )
882 876 881 868 mulexpd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐵 · ( 1 / 𝐴 ) ) ↑ 𝑘 ) = ( ( 𝐵𝑘 ) · ( ( 1 / 𝐴 ) ↑ 𝑘 ) ) )
883 880 882 eqtrd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐵 / 𝐴 ) ↑ 𝑘 ) = ( ( 𝐵𝑘 ) · ( ( 1 / 𝐴 ) ↑ 𝑘 ) ) )
884 883 oveq2d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐵 / 𝐴 ) ↑ 𝑘 ) ) = ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐵𝑘 ) · ( ( 1 / 𝐴 ) ↑ 𝑘 ) ) ) )
885 876 868 expcld ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐵𝑘 ) ∈ ℂ )
886 881 868 expcld ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 1 / 𝐴 ) ↑ 𝑘 ) ∈ ℂ )
887 733 885 886 mulassd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐶 C𝑐 𝑘 ) · ( 𝐵𝑘 ) ) · ( ( 1 / 𝐴 ) ↑ 𝑘 ) ) = ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐵𝑘 ) · ( ( 1 / 𝐴 ) ↑ 𝑘 ) ) ) )
888 884 887 eqtr4d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐵 / 𝐴 ) ↑ 𝑘 ) ) = ( ( ( 𝐶 C𝑐 𝑘 ) · ( 𝐵𝑘 ) ) · ( ( 1 / 𝐴 ) ↑ 𝑘 ) ) )
889 888 oveq1d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐵 / 𝐴 ) ↑ 𝑘 ) ) · ( 𝐴𝑐 𝐶 ) ) = ( ( ( ( 𝐶 C𝑐 𝑘 ) · ( 𝐵𝑘 ) ) · ( ( 1 / 𝐴 ) ↑ 𝑘 ) ) · ( 𝐴𝑐 𝐶 ) ) )
890 733 885 mulcld ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐶 C𝑐 𝑘 ) · ( 𝐵𝑘 ) ) ∈ ℂ )
891 874 adantr ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴𝑐 𝐶 ) ∈ ℂ )
892 890 886 891 mul32d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( ( 𝐶 C𝑐 𝑘 ) · ( 𝐵𝑘 ) ) · ( ( 1 / 𝐴 ) ↑ 𝑘 ) ) · ( 𝐴𝑐 𝐶 ) ) = ( ( ( ( 𝐶 C𝑐 𝑘 ) · ( 𝐵𝑘 ) ) · ( 𝐴𝑐 𝐶 ) ) · ( ( 1 / 𝐴 ) ↑ 𝑘 ) ) )
893 890 891 886 mulassd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( ( 𝐶 C𝑐 𝑘 ) · ( 𝐵𝑘 ) ) · ( 𝐴𝑐 𝐶 ) ) · ( ( 1 / 𝐴 ) ↑ 𝑘 ) ) = ( ( ( 𝐶 C𝑐 𝑘 ) · ( 𝐵𝑘 ) ) · ( ( 𝐴𝑐 𝐶 ) · ( ( 1 / 𝐴 ) ↑ 𝑘 ) ) ) )
894 889 892 893 3eqtrd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐵 / 𝐴 ) ↑ 𝑘 ) ) · ( 𝐴𝑐 𝐶 ) ) = ( ( ( 𝐶 C𝑐 𝑘 ) · ( 𝐵𝑘 ) ) · ( ( 𝐴𝑐 𝐶 ) · ( ( 1 / 𝐴 ) ↑ 𝑘 ) ) ) )
895 868 nn0cnd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℂ )
896 877 895 cxpcld ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴𝑐 𝑘 ) ∈ ℂ )
897 877 878 895 cxpne0d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴𝑐 𝑘 ) ≠ 0 )
898 891 896 897 divrecd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴𝑐 𝐶 ) / ( 𝐴𝑐 𝑘 ) ) = ( ( 𝐴𝑐 𝐶 ) · ( 1 / ( 𝐴𝑐 𝑘 ) ) ) )
899 4 ad2antrr ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝐶 ∈ ℂ )
900 877 878 899 895 cxpsubd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴𝑐 ( 𝐶𝑘 ) ) = ( ( 𝐴𝑐 𝐶 ) / ( 𝐴𝑐 𝑘 ) ) )
901 868 nn0zd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℤ )
902 877 878 901 exprecd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 1 / 𝐴 ) ↑ 𝑘 ) = ( 1 / ( 𝐴𝑘 ) ) )
903 cxpexp ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴𝑐 𝑘 ) = ( 𝐴𝑘 ) )
904 877 868 903 syl2anc ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴𝑐 𝑘 ) = ( 𝐴𝑘 ) )
905 904 oveq2d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 1 / ( 𝐴𝑐 𝑘 ) ) = ( 1 / ( 𝐴𝑘 ) ) )
906 902 905 eqtr4d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 1 / 𝐴 ) ↑ 𝑘 ) = ( 1 / ( 𝐴𝑐 𝑘 ) ) )
907 906 oveq2d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴𝑐 𝐶 ) · ( ( 1 / 𝐴 ) ↑ 𝑘 ) ) = ( ( 𝐴𝑐 𝐶 ) · ( 1 / ( 𝐴𝑐 𝑘 ) ) ) )
908 898 900 907 3eqtr4rd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴𝑐 𝐶 ) · ( ( 1 / 𝐴 ) ↑ 𝑘 ) ) = ( 𝐴𝑐 ( 𝐶𝑘 ) ) )
909 908 oveq2d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐶 C𝑐 𝑘 ) · ( 𝐵𝑘 ) ) · ( ( 𝐴𝑐 𝐶 ) · ( ( 1 / 𝐴 ) ↑ 𝑘 ) ) ) = ( ( ( 𝐶 C𝑐 𝑘 ) · ( 𝐵𝑘 ) ) · ( 𝐴𝑐 ( 𝐶𝑘 ) ) ) )
910 899 895 subcld ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐶𝑘 ) ∈ ℂ )
911 877 910 cxpcld ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴𝑐 ( 𝐶𝑘 ) ) ∈ ℂ )
912 733 885 911 mul32d ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐶 C𝑐 𝑘 ) · ( 𝐵𝑘 ) ) · ( 𝐴𝑐 ( 𝐶𝑘 ) ) ) = ( ( ( 𝐶 C𝑐 𝑘 ) · ( 𝐴𝑐 ( 𝐶𝑘 ) ) ) · ( 𝐵𝑘 ) ) )
913 894 909 912 3eqtrd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐵 / 𝐴 ) ↑ 𝑘 ) ) · ( 𝐴𝑐 𝐶 ) ) = ( ( ( 𝐶 C𝑐 𝑘 ) · ( 𝐴𝑐 ( 𝐶𝑘 ) ) ) · ( 𝐵𝑘 ) ) )
914 733 911 885 mulassd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐶 C𝑐 𝑘 ) · ( 𝐴𝑐 ( 𝐶𝑘 ) ) ) · ( 𝐵𝑘 ) ) = ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐴𝑐 ( 𝐶𝑘 ) ) · ( 𝐵𝑘 ) ) ) )
915 913 914 eqtrd ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐵 / 𝐴 ) ↑ 𝑘 ) ) · ( 𝐴𝑐 𝐶 ) ) = ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐴𝑐 ( 𝐶𝑘 ) ) · ( 𝐵𝑘 ) ) ) )
916 915 sumeq2dv ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → Σ 𝑘 ∈ ℕ0 ( ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐵 / 𝐴 ) ↑ 𝑘 ) ) · ( 𝐴𝑐 𝐶 ) ) = Σ 𝑘 ∈ ℕ0 ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐴𝑐 ( 𝐶𝑘 ) ) · ( 𝐵𝑘 ) ) ) )
917 875 916 eqtrd ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( Σ 𝑘 ∈ ℕ0 ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐵 / 𝐴 ) ↑ 𝑘 ) ) · ( 𝐴𝑐 𝐶 ) ) = Σ 𝑘 ∈ ℕ0 ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐴𝑐 ( 𝐶𝑘 ) ) · ( 𝐵𝑘 ) ) ) )
918 825 866 917 3eqtr3d ( ( 𝜑 ∧ ¬ 𝐶 ∈ ℕ0 ) → ( ( 𝐴 + 𝐵 ) ↑𝑐 𝐶 ) = Σ 𝑘 ∈ ℕ0 ( ( 𝐶 C𝑐 𝑘 ) · ( ( 𝐴𝑐 ( 𝐶𝑘 ) ) · ( 𝐵𝑘 ) ) ) )