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	|- ( ph -> A e. RR+ )
	binomcxp.b	|- ( ph -> B e. RR )
	binomcxp.lt	|- ( ph -> ( abs ` B ) < ( abs ` A ) )
	binomcxp.c	|- ( ph -> C e. CC )
	binomcxplem.f	|- F = ( j e. NN0 |-> ( C _Cc j ) )
	binomcxplem.s	|- S = ( b e. CC |-> ( k e. NN0 |-> ( ( F ` k ) x. ( b ^ k ) ) ) )
	binomcxplem.r	|- R = sup ( { r e. RR | seq 0 ( + , ( S ` r ) ) e. dom ~~> } , RR* , < )
	binomcxplem.e	|- E = ( b e. CC |-> ( k e. NN |-> ( ( k x. ( F ` k ) ) x. ( b ^ ( k - 1 ) ) ) ) )
	binomcxplem.d	|- D = ( `' abs " ( 0 [,) R ) )
	binomcxplem.p	|- P = ( b e. D |-> sum_ k e. NN0 ( ( S ` b ) ` k ) )
Assertion	binomcxplemnotnn0	|- ( ( ph /\ -. C e. NN0 ) -> ( ( A + B ) ^c C ) = sum_ k e. NN0 ( ( C _Cc k ) x. ( ( A ^c ( C - k ) ) x. ( B ^ k ) ) ) )

Proof

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