pserdvlem2

	Ref	Expression
Hypotheses	pserf.g	\|- G = ( x e. CC \|-> ( n e. NN0 \|-> ( ( A ` n ) x. ( x ^ n ) ) ) )
	pserf.f	\|- F = ( y e. S \|-> sum_ j e. NN0 ( ( G ` y ) ` j ) )
	pserf.a	\|- ( ph -> A : NN0 --> CC )
	pserf.r	\|- R = sup ( { r e. RR \| seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < )
	psercn.s	\|- S = ( `' abs " ( 0 [,) R ) )
	psercn.m	\|- M = if ( R e. RR , ( ( ( abs ` a ) + R ) / 2 ) , ( ( abs ` a ) + 1 ) )
	pserdv.b	\|- B = ( 0 ( ball ` ( abs o. - ) ) ( ( ( abs ` a ) + M ) / 2 ) )
Assertion	pserdvlem2	\|- ( ( ph /\ a e. S ) -> ( CC _D ( F \|` B ) ) = ( y e. B \|-> sum_ k e. NN0 ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		pserf.g	\|- G = ( x e. CC \|-> ( n e. NN0 \|-> ( ( A ` n ) x. ( x ^ n ) ) ) )
2		pserf.f	\|- F = ( y e. S \|-> sum_ j e. NN0 ( ( G ` y ) ` j ) )
3		pserf.a	\|- ( ph -> A : NN0 --> CC )
4		pserf.r	\|- R = sup ( { r e. RR \| seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < )
5		psercn.s	\|- S = ( `' abs " ( 0 [,) R ) )
6		psercn.m	\|- M = if ( R e. RR , ( ( ( abs ` a ) + R ) / 2 ) , ( ( abs ` a ) + 1 ) )
7		pserdv.b	\|- B = ( 0 ( ball ` ( abs o. - ) ) ( ( ( abs ` a ) + M ) / 2 ) )
8		nn0uz	\|- NN0 = ( ZZ>= ` 0 )
9		cnelprrecn	\|- CC e. { RR , CC }
10	9	a1i	\|- ( ( ph /\ a e. S ) -> CC e. { RR , CC } )
11		0zd	\|- ( ( ph /\ a e. S ) -> 0 e. ZZ )
12		fzfid	\|- ( ( ( ( ph /\ a e. S ) /\ k e. NN0 ) /\ y e. B ) -> ( 0 ... k ) e. Fin )
13	3	ad3antrrr	\|- ( ( ( ( ph /\ a e. S ) /\ k e. NN0 ) /\ y e. B ) -> A : NN0 --> CC )
14		cnxmet	\|- ( abs o. - ) e. ( *Met ` CC )
15		0cnd	\|- ( ( ph /\ a e. S ) -> 0 e. CC )
16	1 2 3 4 5 6	pserdvlem1	\|- ( ( ph /\ a e. S ) -> ( ( ( ( abs ` a ) + M ) / 2 ) e. RR+ /\ ( abs ` a ) < ( ( ( abs ` a ) + M ) / 2 ) /\ ( ( ( abs ` a ) + M ) / 2 ) < R ) )
17	16	simp1d	\|- ( ( ph /\ a e. S ) -> ( ( ( abs ` a ) + M ) / 2 ) e. RR+ )
18	17	rpxrd	\|- ( ( ph /\ a e. S ) -> ( ( ( abs ` a ) + M ) / 2 ) e. RR* )
19		blssm	\|- ( ( ( abs o. - ) e. ( Met ` CC ) /\ 0 e. CC /\ ( ( ( abs ` a ) + M ) / 2 ) e. RR ) -> ( 0 ( ball ` ( abs o. - ) ) ( ( ( abs ` a ) + M ) / 2 ) ) C_ CC )
20	14 15 18 19	mp3an2i	\|- ( ( ph /\ a e. S ) -> ( 0 ( ball ` ( abs o. - ) ) ( ( ( abs ` a ) + M ) / 2 ) ) C_ CC )
21	7 20	eqsstrid	\|- ( ( ph /\ a e. S ) -> B C_ CC )
22	21	adantr	\|- ( ( ( ph /\ a e. S ) /\ k e. NN0 ) -> B C_ CC )
23	22	sselda	\|- ( ( ( ( ph /\ a e. S ) /\ k e. NN0 ) /\ y e. B ) -> y e. CC )
24	1 13 23	psergf	\|- ( ( ( ( ph /\ a e. S ) /\ k e. NN0 ) /\ y e. B ) -> ( G ` y ) : NN0 --> CC )
25		elfznn0	\|- ( i e. ( 0 ... k ) -> i e. NN0 )
26		ffvelcdm	\|- ( ( ( G ` y ) : NN0 --> CC /\ i e. NN0 ) -> ( ( G ` y ) ` i ) e. CC )
27	24 25 26	syl2an	\|- ( ( ( ( ( ph /\ a e. S ) /\ k e. NN0 ) /\ y e. B ) /\ i e. ( 0 ... k ) ) -> ( ( G ` y ) ` i ) e. CC )
28	12 27	fsumcl	\|- ( ( ( ( ph /\ a e. S ) /\ k e. NN0 ) /\ y e. B ) -> sum_ i e. ( 0 ... k ) ( ( G ` y ) ` i ) e. CC )
29	28	fmpttd	\|- ( ( ( ph /\ a e. S ) /\ k e. NN0 ) -> ( y e. B \|-> sum_ i e. ( 0 ... k ) ( ( G ` y ) ` i ) ) : B --> CC )
30		cnex	\|- CC e. _V
31	7	ovexi	\|- B e. _V
32	30 31	elmap	\|- ( ( y e. B \|-> sum_ i e. ( 0 ... k ) ( ( G ` y ) ` i ) ) e. ( CC ^m B ) <-> ( y e. B \|-> sum_ i e. ( 0 ... k ) ( ( G ` y ) ` i ) ) : B --> CC )
33	29 32	sylibr	\|- ( ( ( ph /\ a e. S ) /\ k e. NN0 ) -> ( y e. B \|-> sum_ i e. ( 0 ... k ) ( ( G ` y ) ` i ) ) e. ( CC ^m B ) )
34	33	fmpttd	\|- ( ( ph /\ a e. S ) -> ( k e. NN0 \|-> ( y e. B \|-> sum_ i e. ( 0 ... k ) ( ( G ` y ) ` i ) ) ) : NN0 --> ( CC ^m B ) )
35	1 2 3 4 5 6	psercn	\|- ( ph -> F e. ( S -cn-> CC ) )
36		cncff	\|- ( F e. ( S -cn-> CC ) -> F : S --> CC )
37	35 36	syl	\|- ( ph -> F : S --> CC )
38	37	adantr	\|- ( ( ph /\ a e. S ) -> F : S --> CC )
39	1 2 3 4 5 16	psercnlem2	\|- ( ( ph /\ a e. S ) -> ( a e. ( 0 ( ball ` ( abs o. - ) ) ( ( ( abs ` a ) + M ) / 2 ) ) /\ ( 0 ( ball ` ( abs o. - ) ) ( ( ( abs ` a ) + M ) / 2 ) ) C_ ( `' abs " ( 0 [,] ( ( ( abs ` a ) + M ) / 2 ) ) ) /\ ( `' abs " ( 0 [,] ( ( ( abs ` a ) + M ) / 2 ) ) ) C_ S ) )
40	39	simp2d	\|- ( ( ph /\ a e. S ) -> ( 0 ( ball ` ( abs o. - ) ) ( ( ( abs ` a ) + M ) / 2 ) ) C_ ( `' abs " ( 0 [,] ( ( ( abs ` a ) + M ) / 2 ) ) ) )
41	7 40	eqsstrid	\|- ( ( ph /\ a e. S ) -> B C_ ( `' abs " ( 0 [,] ( ( ( abs ` a ) + M ) / 2 ) ) ) )
42	39	simp3d	\|- ( ( ph /\ a e. S ) -> ( `' abs " ( 0 [,] ( ( ( abs ` a ) + M ) / 2 ) ) ) C_ S )
43	41 42	sstrd	\|- ( ( ph /\ a e. S ) -> B C_ S )
44	38 43	fssresd	\|- ( ( ph /\ a e. S ) -> ( F \|` B ) : B --> CC )
45		0zd	\|- ( ( ( ph /\ a e. S ) /\ z e. B ) -> 0 e. ZZ )
46		eqidd	\|- ( ( ( ( ph /\ a e. S ) /\ z e. B ) /\ j e. NN0 ) -> ( ( G ` z ) ` j ) = ( ( G ` z ) ` j ) )
47	3	ad2antrr	\|- ( ( ( ph /\ a e. S ) /\ z e. B ) -> A : NN0 --> CC )
48	21	sselda	\|- ( ( ( ph /\ a e. S ) /\ z e. B ) -> z e. CC )
49	1 47 48	psergf	\|- ( ( ( ph /\ a e. S ) /\ z e. B ) -> ( G ` z ) : NN0 --> CC )
50	49	ffvelcdmda	\|- ( ( ( ( ph /\ a e. S ) /\ z e. B ) /\ j e. NN0 ) -> ( ( G ` z ) ` j ) e. CC )
51	48	abscld	\|- ( ( ( ph /\ a e. S ) /\ z e. B ) -> ( abs ` z ) e. RR )
52	51	rexrd	\|- ( ( ( ph /\ a e. S ) /\ z e. B ) -> ( abs ` z ) e. RR* )
53	18	adantr	\|- ( ( ( ph /\ a e. S ) /\ z e. B ) -> ( ( ( abs ` a ) + M ) / 2 ) e. RR* )
54		iccssxr	\|- ( 0 [,] +oo ) C_ RR*
55	1 3 4	radcnvcl	\|- ( ph -> R e. ( 0 [,] +oo ) )
56	54 55	sselid	\|- ( ph -> R e. RR* )
57	56	ad2antrr	\|- ( ( ( ph /\ a e. S ) /\ z e. B ) -> R e. RR* )
58		0cn	\|- 0 e. CC
59		eqid	\|- ( abs o. - ) = ( abs o. - )
60	59	cnmetdval	\|- ( ( z e. CC /\ 0 e. CC ) -> ( z ( abs o. - ) 0 ) = ( abs ` ( z - 0 ) ) )
61	48 58 60	sylancl	\|- ( ( ( ph /\ a e. S ) /\ z e. B ) -> ( z ( abs o. - ) 0 ) = ( abs ` ( z - 0 ) ) )
62	48	subid1d	\|- ( ( ( ph /\ a e. S ) /\ z e. B ) -> ( z - 0 ) = z )
63	62	fveq2d	\|- ( ( ( ph /\ a e. S ) /\ z e. B ) -> ( abs ` ( z - 0 ) ) = ( abs ` z ) )
64	61 63	eqtrd	\|- ( ( ( ph /\ a e. S ) /\ z e. B ) -> ( z ( abs o. - ) 0 ) = ( abs ` z ) )
65		simpr	\|- ( ( ( ph /\ a e. S ) /\ z e. B ) -> z e. B )
66	65 7	eleqtrdi	\|- ( ( ( ph /\ a e. S ) /\ z e. B ) -> z e. ( 0 ( ball ` ( abs o. - ) ) ( ( ( abs ` a ) + M ) / 2 ) ) )
67	14	a1i	\|- ( ( ( ph /\ a e. S ) /\ z e. B ) -> ( abs o. - ) e. ( *Met ` CC ) )
68		0cnd	\|- ( ( ( ph /\ a e. S ) /\ z e. B ) -> 0 e. CC )
69		elbl3	\|- ( ( ( ( abs o. - ) e. ( Met ` CC ) /\ ( ( ( abs ` a ) + M ) / 2 ) e. RR ) /\ ( 0 e. CC /\ z e. CC ) ) -> ( z e. ( 0 ( ball ` ( abs o. - ) ) ( ( ( abs ` a ) + M ) / 2 ) ) <-> ( z ( abs o. - ) 0 ) < ( ( ( abs ` a ) + M ) / 2 ) ) )
70	67 53 68 48 69	syl22anc	\|- ( ( ( ph /\ a e. S ) /\ z e. B ) -> ( z e. ( 0 ( ball ` ( abs o. - ) ) ( ( ( abs ` a ) + M ) / 2 ) ) <-> ( z ( abs o. - ) 0 ) < ( ( ( abs ` a ) + M ) / 2 ) ) )
71	66 70	mpbid	\|- ( ( ( ph /\ a e. S ) /\ z e. B ) -> ( z ( abs o. - ) 0 ) < ( ( ( abs ` a ) + M ) / 2 ) )
72	64 71	eqbrtrrd	\|- ( ( ( ph /\ a e. S ) /\ z e. B ) -> ( abs ` z ) < ( ( ( abs ` a ) + M ) / 2 ) )
73	16	simp3d	\|- ( ( ph /\ a e. S ) -> ( ( ( abs ` a ) + M ) / 2 ) < R )
74	73	adantr	\|- ( ( ( ph /\ a e. S ) /\ z e. B ) -> ( ( ( abs ` a ) + M ) / 2 ) < R )
75	52 53 57 72 74	xrlttrd	\|- ( ( ( ph /\ a e. S ) /\ z e. B ) -> ( abs ` z ) < R )
76	1 47 4 48 75	radcnvlt2	\|- ( ( ( ph /\ a e. S ) /\ z e. B ) -> seq 0 ( + , ( G ` z ) ) e. dom ~~> )
77	8 45 46 50 76	isumclim2	\|- ( ( ( ph /\ a e. S ) /\ z e. B ) -> seq 0 ( + , ( G ` z ) ) ~~> sum_ j e. NN0 ( ( G ` z ) ` j ) )
78	43	sselda	\|- ( ( ( ph /\ a e. S ) /\ z e. B ) -> z e. S )
79		fveq2	\|- ( y = z -> ( G ` y ) = ( G ` z ) )
80	79	fveq1d	\|- ( y = z -> ( ( G ` y ) ` j ) = ( ( G ` z ) ` j ) )
81	80	sumeq2sdv	\|- ( y = z -> sum_ j e. NN0 ( ( G ` y ) ` j ) = sum_ j e. NN0 ( ( G ` z ) ` j ) )
82		sumex	\|- sum_ j e. NN0 ( ( G ` z ) ` j ) e. _V
83	81 2 82	fvmpt	\|- ( z e. S -> ( F ` z ) = sum_ j e. NN0 ( ( G ` z ) ` j ) )
84	78 83	syl	\|- ( ( ( ph /\ a e. S ) /\ z e. B ) -> ( F ` z ) = sum_ j e. NN0 ( ( G ` z ) ` j ) )
85	77 84	breqtrrd	\|- ( ( ( ph /\ a e. S ) /\ z e. B ) -> seq 0 ( + , ( G ` z ) ) ~~> ( F ` z ) )
86		oveq2	\|- ( k = m -> ( 0 ... k ) = ( 0 ... m ) )
87	86	sumeq1d	\|- ( k = m -> sum_ i e. ( 0 ... k ) ( ( G ` y ) ` i ) = sum_ i e. ( 0 ... m ) ( ( G ` y ) ` i ) )
88	87	mpteq2dv	\|- ( k = m -> ( y e. B \|-> sum_ i e. ( 0 ... k ) ( ( G ` y ) ` i ) ) = ( y e. B \|-> sum_ i e. ( 0 ... m ) ( ( G ` y ) ` i ) ) )
89		eqid	\|- ( k e. NN0 \|-> ( y e. B \|-> sum_ i e. ( 0 ... k ) ( ( G ` y ) ` i ) ) ) = ( k e. NN0 \|-> ( y e. B \|-> sum_ i e. ( 0 ... k ) ( ( G ` y ) ` i ) ) )
90	31	mptex	\|- ( y e. B \|-> sum_ i e. ( 0 ... m ) ( ( G ` y ) ` i ) ) e. _V
91	88 89 90	fvmpt	\|- ( m e. NN0 -> ( ( k e. NN0 \|-> ( y e. B \|-> sum_ i e. ( 0 ... k ) ( ( G ` y ) ` i ) ) ) ` m ) = ( y e. B \|-> sum_ i e. ( 0 ... m ) ( ( G ` y ) ` i ) ) )
92	91	adantl	\|- ( ( ( ( ph /\ a e. S ) /\ z e. B ) /\ m e. NN0 ) -> ( ( k e. NN0 \|-> ( y e. B \|-> sum_ i e. ( 0 ... k ) ( ( G ` y ) ` i ) ) ) ` m ) = ( y e. B \|-> sum_ i e. ( 0 ... m ) ( ( G ` y ) ` i ) ) )
93	92	fveq1d	\|- ( ( ( ( ph /\ a e. S ) /\ z e. B ) /\ m e. NN0 ) -> ( ( ( k e. NN0 \|-> ( y e. B \|-> sum_ i e. ( 0 ... k ) ( ( G ` y ) ` i ) ) ) ` m ) ` z ) = ( ( y e. B \|-> sum_ i e. ( 0 ... m ) ( ( G ` y ) ` i ) ) ` z ) )
94	79	fveq1d	\|- ( y = z -> ( ( G ` y ) ` i ) = ( ( G ` z ) ` i ) )
95	94	sumeq2sdv	\|- ( y = z -> sum_ i e. ( 0 ... m ) ( ( G ` y ) ` i ) = sum_ i e. ( 0 ... m ) ( ( G ` z ) ` i ) )
96		eqid	\|- ( y e. B \|-> sum_ i e. ( 0 ... m ) ( ( G ` y ) ` i ) ) = ( y e. B \|-> sum_ i e. ( 0 ... m ) ( ( G ` y ) ` i ) )
97		sumex	\|- sum_ i e. ( 0 ... m ) ( ( G ` z ) ` i ) e. _V
98	95 96 97	fvmpt	\|- ( z e. B -> ( ( y e. B \|-> sum_ i e. ( 0 ... m ) ( ( G ` y ) ` i ) ) ` z ) = sum_ i e. ( 0 ... m ) ( ( G ` z ) ` i ) )
99	98	ad2antlr	\|- ( ( ( ( ph /\ a e. S ) /\ z e. B ) /\ m e. NN0 ) -> ( ( y e. B \|-> sum_ i e. ( 0 ... m ) ( ( G ` y ) ` i ) ) ` z ) = sum_ i e. ( 0 ... m ) ( ( G ` z ) ` i ) )
100		eqidd	\|- ( ( ( ( ( ph /\ a e. S ) /\ z e. B ) /\ m e. NN0 ) /\ i e. ( 0 ... m ) ) -> ( ( G ` z ) ` i ) = ( ( G ` z ) ` i ) )
101		simpr	\|- ( ( ( ( ph /\ a e. S ) /\ z e. B ) /\ m e. NN0 ) -> m e. NN0 )
102	101 8	eleqtrdi	\|- ( ( ( ( ph /\ a e. S ) /\ z e. B ) /\ m e. NN0 ) -> m e. ( ZZ>= ` 0 ) )
103	49	adantr	\|- ( ( ( ( ph /\ a e. S ) /\ z e. B ) /\ m e. NN0 ) -> ( G ` z ) : NN0 --> CC )
104		elfznn0	\|- ( i e. ( 0 ... m ) -> i e. NN0 )
105		ffvelcdm	\|- ( ( ( G ` z ) : NN0 --> CC /\ i e. NN0 ) -> ( ( G ` z ) ` i ) e. CC )
106	103 104 105	syl2an	\|- ( ( ( ( ( ph /\ a e. S ) /\ z e. B ) /\ m e. NN0 ) /\ i e. ( 0 ... m ) ) -> ( ( G ` z ) ` i ) e. CC )
107	100 102 106	fsumser	\|- ( ( ( ( ph /\ a e. S ) /\ z e. B ) /\ m e. NN0 ) -> sum_ i e. ( 0 ... m ) ( ( G ` z ) ` i ) = ( seq 0 ( + , ( G ` z ) ) ` m ) )
108	93 99 107	3eqtrd	\|- ( ( ( ( ph /\ a e. S ) /\ z e. B ) /\ m e. NN0 ) -> ( ( ( k e. NN0 \|-> ( y e. B \|-> sum_ i e. ( 0 ... k ) ( ( G ` y ) ` i ) ) ) ` m ) ` z ) = ( seq 0 ( + , ( G ` z ) ) ` m ) )
109	108	mpteq2dva	\|- ( ( ( ph /\ a e. S ) /\ z e. B ) -> ( m e. NN0 \|-> ( ( ( k e. NN0 \|-> ( y e. B \|-> sum_ i e. ( 0 ... k ) ( ( G ` y ) ` i ) ) ) ` m ) ` z ) ) = ( m e. NN0 \|-> ( seq 0 ( + , ( G ` z ) ) ` m ) ) )
110		0z	\|- 0 e. ZZ
111		seqfn	\|- ( 0 e. ZZ -> seq 0 ( + , ( G ` z ) ) Fn ( ZZ>= ` 0 ) )
112	110 111	ax-mp	\|- seq 0 ( + , ( G ` z ) ) Fn ( ZZ>= ` 0 )
113	8	fneq2i	\|- ( seq 0 ( + , ( G ` z ) ) Fn NN0 <-> seq 0 ( + , ( G ` z ) ) Fn ( ZZ>= ` 0 ) )
114	112 113	mpbir	\|- seq 0 ( + , ( G ` z ) ) Fn NN0
115		dffn5	\|- ( seq 0 ( + , ( G ` z ) ) Fn NN0 <-> seq 0 ( + , ( G ` z ) ) = ( m e. NN0 \|-> ( seq 0 ( + , ( G ` z ) ) ` m ) ) )
116	114 115	mpbi	\|- seq 0 ( + , ( G ` z ) ) = ( m e. NN0 \|-> ( seq 0 ( + , ( G ` z ) ) ` m ) )
117	109 116	eqtr4di	\|- ( ( ( ph /\ a e. S ) /\ z e. B ) -> ( m e. NN0 \|-> ( ( ( k e. NN0 \|-> ( y e. B \|-> sum_ i e. ( 0 ... k ) ( ( G ` y ) ` i ) ) ) ` m ) ` z ) ) = seq 0 ( + , ( G ` z ) ) )
118		fvres	\|- ( z e. B -> ( ( F \|` B ) ` z ) = ( F ` z ) )
119	118	adantl	\|- ( ( ( ph /\ a e. S ) /\ z e. B ) -> ( ( F \|` B ) ` z ) = ( F ` z ) )
120	85 117 119	3brtr4d	\|- ( ( ( ph /\ a e. S ) /\ z e. B ) -> ( m e. NN0 \|-> ( ( ( k e. NN0 \|-> ( y e. B \|-> sum_ i e. ( 0 ... k ) ( ( G ` y ) ` i ) ) ) ` m ) ` z ) ) ~~> ( ( F \|` B ) ` z ) )
121	91	adantl	\|- ( ( ( ph /\ a e. S ) /\ m e. NN0 ) -> ( ( k e. NN0 \|-> ( y e. B \|-> sum_ i e. ( 0 ... k ) ( ( G ` y ) ` i ) ) ) ` m ) = ( y e. B \|-> sum_ i e. ( 0 ... m ) ( ( G ` y ) ` i ) ) )
122	121	oveq2d	\|- ( ( ( ph /\ a e. S ) /\ m e. NN0 ) -> ( CC _D ( ( k e. NN0 \|-> ( y e. B \|-> sum_ i e. ( 0 ... k ) ( ( G ` y ) ` i ) ) ) ` m ) ) = ( CC _D ( y e. B \|-> sum_ i e. ( 0 ... m ) ( ( G ` y ) ` i ) ) ) )
123		eqid	\|- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
124	123	cnfldtopon	\|- ( TopOpen ` CCfld ) e. ( TopOn ` CC )
125	124	toponrestid	\|- ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) \|`t CC )
126	9	a1i	\|- ( ( ( ph /\ a e. S ) /\ m e. NN0 ) -> CC e. { RR , CC } )
127	123	cnfldtopn	\|- ( TopOpen ` CCfld ) = ( MetOpen ` ( abs o. - ) )
128	127	blopn	\|- ( ( ( abs o. - ) e. ( Met ` CC ) /\ 0 e. CC /\ ( ( ( abs ` a ) + M ) / 2 ) e. RR ) -> ( 0 ( ball ` ( abs o. - ) ) ( ( ( abs ` a ) + M ) / 2 ) ) e. ( TopOpen ` CCfld ) )
129	14 15 18 128	mp3an2i	\|- ( ( ph /\ a e. S ) -> ( 0 ( ball ` ( abs o. - ) ) ( ( ( abs ` a ) + M ) / 2 ) ) e. ( TopOpen ` CCfld ) )
130	7 129	eqeltrid	\|- ( ( ph /\ a e. S ) -> B e. ( TopOpen ` CCfld ) )
131	130	adantr	\|- ( ( ( ph /\ a e. S ) /\ m e. NN0 ) -> B e. ( TopOpen ` CCfld ) )
132		fzfid	\|- ( ( ( ph /\ a e. S ) /\ m e. NN0 ) -> ( 0 ... m ) e. Fin )
133	3	ad2antrr	\|- ( ( ( ph /\ a e. S ) /\ m e. NN0 ) -> A : NN0 --> CC )
134	133	3ad2ant1	\|- ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ i e. ( 0 ... m ) /\ y e. B ) -> A : NN0 --> CC )
135	21	adantr	\|- ( ( ( ph /\ a e. S ) /\ m e. NN0 ) -> B C_ CC )
136	135	sselda	\|- ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ y e. B ) -> y e. CC )
137	136	3adant2	\|- ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ i e. ( 0 ... m ) /\ y e. B ) -> y e. CC )
138	1 134 137	psergf	\|- ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ i e. ( 0 ... m ) /\ y e. B ) -> ( G ` y ) : NN0 --> CC )
139	104	3ad2ant2	\|- ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ i e. ( 0 ... m ) /\ y e. B ) -> i e. NN0 )
140	138 139	ffvelcdmd	\|- ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ i e. ( 0 ... m ) /\ y e. B ) -> ( ( G ` y ) ` i ) e. CC )
141	9	a1i	\|- ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ i e. ( 0 ... m ) ) -> CC e. { RR , CC } )
142		ffvelcdm	\|- ( ( A : NN0 --> CC /\ i e. NN0 ) -> ( A ` i ) e. CC )
143	133 104 142	syl2an	\|- ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ i e. ( 0 ... m ) ) -> ( A ` i ) e. CC )
144	143	adantr	\|- ( ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ i e. ( 0 ... m ) ) /\ y e. B ) -> ( A ` i ) e. CC )
145	136	adantlr	\|- ( ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ i e. ( 0 ... m ) ) /\ y e. B ) -> y e. CC )
146		id	\|- ( y e. CC -> y e. CC )
147	104	adantl	\|- ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ i e. ( 0 ... m ) ) -> i e. NN0 )
148		expcl	\|- ( ( y e. CC /\ i e. NN0 ) -> ( y ^ i ) e. CC )
149	146 147 148	syl2anr	\|- ( ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ i e. ( 0 ... m ) ) /\ y e. CC ) -> ( y ^ i ) e. CC )
150	145 149	syldan	\|- ( ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ i e. ( 0 ... m ) ) /\ y e. B ) -> ( y ^ i ) e. CC )
151	144 150	mulcld	\|- ( ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ i e. ( 0 ... m ) ) /\ y e. B ) -> ( ( A ` i ) x. ( y ^ i ) ) e. CC )
152		ovexd	\|- ( ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ i e. ( 0 ... m ) ) /\ y e. B ) -> ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) e. _V )
153		c0ex	\|- 0 e. _V
154		ovex	\|- ( i x. ( y ^ ( i - 1 ) ) ) e. _V
155	153 154	ifex	\|- if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) e. _V
156	155	a1i	\|- ( ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ i e. ( 0 ... m ) ) /\ y e. B ) -> if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) e. _V )
157	155	a1i	\|- ( ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ i e. ( 0 ... m ) ) /\ y e. CC ) -> if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) e. _V )
158		dvexp2	\|- ( i e. NN0 -> ( CC _D ( y e. CC \|-> ( y ^ i ) ) ) = ( y e. CC \|-> if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) )
159	147 158	syl	\|- ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ i e. ( 0 ... m ) ) -> ( CC _D ( y e. CC \|-> ( y ^ i ) ) ) = ( y e. CC \|-> if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) )
160	21	ad2antrr	\|- ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ i e. ( 0 ... m ) ) -> B C_ CC )
161	130	ad2antrr	\|- ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ i e. ( 0 ... m ) ) -> B e. ( TopOpen ` CCfld ) )
162	141 149 157 159 160 125 123 161	dvmptres	\|- ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ i e. ( 0 ... m ) ) -> ( CC _D ( y e. B \|-> ( y ^ i ) ) ) = ( y e. B \|-> if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) )
163	141 150 156 162 143	dvmptcmul	\|- ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ i e. ( 0 ... m ) ) -> ( CC _D ( y e. B \|-> ( ( A ` i ) x. ( y ^ i ) ) ) ) = ( y e. B \|-> ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) ) )
164	141 151 152 163	dvmptcl	\|- ( ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ i e. ( 0 ... m ) ) /\ y e. B ) -> ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) e. CC )
165	164	3impa	\|- ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ i e. ( 0 ... m ) /\ y e. B ) -> ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) e. CC )
166	104	ad2antlr	\|- ( ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ i e. ( 0 ... m ) ) /\ y e. B ) -> i e. NN0 )
167	1	pserval2	\|- ( ( y e. CC /\ i e. NN0 ) -> ( ( G ` y ) ` i ) = ( ( A ` i ) x. ( y ^ i ) ) )
168	145 166 167	syl2anc	\|- ( ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ i e. ( 0 ... m ) ) /\ y e. B ) -> ( ( G ` y ) ` i ) = ( ( A ` i ) x. ( y ^ i ) ) )
169	168	mpteq2dva	\|- ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ i e. ( 0 ... m ) ) -> ( y e. B \|-> ( ( G ` y ) ` i ) ) = ( y e. B \|-> ( ( A ` i ) x. ( y ^ i ) ) ) )
170	169	oveq2d	\|- ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ i e. ( 0 ... m ) ) -> ( CC _D ( y e. B \|-> ( ( G ` y ) ` i ) ) ) = ( CC _D ( y e. B \|-> ( ( A ` i ) x. ( y ^ i ) ) ) ) )
171	170 163	eqtrd	\|- ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ i e. ( 0 ... m ) ) -> ( CC _D ( y e. B \|-> ( ( G ` y ) ` i ) ) ) = ( y e. B \|-> ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) ) )
172	125 123 126 131 132 140 165 171	dvmptfsum	\|- ( ( ( ph /\ a e. S ) /\ m e. NN0 ) -> ( CC _D ( y e. B \|-> sum_ i e. ( 0 ... m ) ( ( G ` y ) ` i ) ) ) = ( y e. B \|-> sum_ i e. ( 0 ... m ) ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) ) )
173	122 172	eqtrd	\|- ( ( ( ph /\ a e. S ) /\ m e. NN0 ) -> ( CC _D ( ( k e. NN0 \|-> ( y e. B \|-> sum_ i e. ( 0 ... k ) ( ( G ` y ) ` i ) ) ) ` m ) ) = ( y e. B \|-> sum_ i e. ( 0 ... m ) ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) ) )
174	173	mpteq2dva	\|- ( ( ph /\ a e. S ) -> ( m e. NN0 \|-> ( CC _D ( ( k e. NN0 \|-> ( y e. B \|-> sum_ i e. ( 0 ... k ) ( ( G ` y ) ` i ) ) ) ` m ) ) ) = ( m e. NN0 \|-> ( y e. B \|-> sum_ i e. ( 0 ... m ) ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) ) ) )
175		nnssnn0	\|- NN C_ NN0
176		resmpt	\|- ( NN C_ NN0 -> ( ( m e. NN0 \|-> ( y e. B \|-> sum_ i e. ( 0 ... m ) ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) ) ) \|` NN ) = ( m e. NN \|-> ( y e. B \|-> sum_ i e. ( 0 ... m ) ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) ) ) )
177	175 176	ax-mp	\|- ( ( m e. NN0 \|-> ( y e. B \|-> sum_ i e. ( 0 ... m ) ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) ) ) \|` NN ) = ( m e. NN \|-> ( y e. B \|-> sum_ i e. ( 0 ... m ) ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) ) )
178		oveq1	\|- ( a = x -> ( a ^ i ) = ( x ^ i ) )
179	178	oveq2d	\|- ( a = x -> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) = ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( x ^ i ) ) )
180	179	mpteq2dv	\|- ( a = x -> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) = ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( x ^ i ) ) ) )
181		oveq1	\|- ( i = n -> ( i + 1 ) = ( n + 1 ) )
182		fvoveq1	\|- ( i = n -> ( A ` ( i + 1 ) ) = ( A ` ( n + 1 ) ) )
183	181 182	oveq12d	\|- ( i = n -> ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) = ( ( n + 1 ) x. ( A ` ( n + 1 ) ) ) )
184		oveq2	\|- ( i = n -> ( x ^ i ) = ( x ^ n ) )
185	183 184	oveq12d	\|- ( i = n -> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( x ^ i ) ) = ( ( ( n + 1 ) x. ( A ` ( n + 1 ) ) ) x. ( x ^ n ) ) )
186	185	cbvmptv	\|- ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( x ^ i ) ) ) = ( n e. NN0 \|-> ( ( ( n + 1 ) x. ( A ` ( n + 1 ) ) ) x. ( x ^ n ) ) )
187		oveq1	\|- ( m = n -> ( m + 1 ) = ( n + 1 ) )
188		fvoveq1	\|- ( m = n -> ( A ` ( m + 1 ) ) = ( A ` ( n + 1 ) ) )
189	187 188	oveq12d	\|- ( m = n -> ( ( m + 1 ) x. ( A ` ( m + 1 ) ) ) = ( ( n + 1 ) x. ( A ` ( n + 1 ) ) ) )
190		eqid	\|- ( m e. NN0 \|-> ( ( m + 1 ) x. ( A ` ( m + 1 ) ) ) ) = ( m e. NN0 \|-> ( ( m + 1 ) x. ( A ` ( m + 1 ) ) ) )
191		ovex	\|- ( ( n + 1 ) x. ( A ` ( n + 1 ) ) ) e. _V
192	189 190 191	fvmpt	\|- ( n e. NN0 -> ( ( m e. NN0 \|-> ( ( m + 1 ) x. ( A ` ( m + 1 ) ) ) ) ` n ) = ( ( n + 1 ) x. ( A ` ( n + 1 ) ) ) )
193	192	oveq1d	\|- ( n e. NN0 -> ( ( ( m e. NN0 \|-> ( ( m + 1 ) x. ( A ` ( m + 1 ) ) ) ) ` n ) x. ( x ^ n ) ) = ( ( ( n + 1 ) x. ( A ` ( n + 1 ) ) ) x. ( x ^ n ) ) )
194	193	mpteq2ia	\|- ( n e. NN0 \|-> ( ( ( m e. NN0 \|-> ( ( m + 1 ) x. ( A ` ( m + 1 ) ) ) ) ` n ) x. ( x ^ n ) ) ) = ( n e. NN0 \|-> ( ( ( n + 1 ) x. ( A ` ( n + 1 ) ) ) x. ( x ^ n ) ) )
195	186 194	eqtr4i	\|- ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( x ^ i ) ) ) = ( n e. NN0 \|-> ( ( ( m e. NN0 \|-> ( ( m + 1 ) x. ( A ` ( m + 1 ) ) ) ) ` n ) x. ( x ^ n ) ) )
196	180 195	eqtrdi	\|- ( a = x -> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) = ( n e. NN0 \|-> ( ( ( m e. NN0 \|-> ( ( m + 1 ) x. ( A ` ( m + 1 ) ) ) ) ` n ) x. ( x ^ n ) ) ) )
197	196	cbvmptv	\|- ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) = ( x e. CC \|-> ( n e. NN0 \|-> ( ( ( m e. NN0 \|-> ( ( m + 1 ) x. ( A ` ( m + 1 ) ) ) ) ` n ) x. ( x ^ n ) ) ) )
198		fveq2	\|- ( y = z -> ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) = ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` z ) )
199	198	fveq1d	\|- ( y = z -> ( ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ` k ) = ( ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` z ) ` k ) )
200	199	sumeq2sdv	\|- ( y = z -> sum_ k e. NN0 ( ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ` k ) = sum_ k e. NN0 ( ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` z ) ` k ) )
201	200	cbvmptv	\|- ( y e. B \|-> sum_ k e. NN0 ( ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ` k ) ) = ( z e. B \|-> sum_ k e. NN0 ( ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` z ) ` k ) )
202		peano2nn0	\|- ( m e. NN0 -> ( m + 1 ) e. NN0 )
203	202	adantl	\|- ( ( ( ph /\ a e. S ) /\ m e. NN0 ) -> ( m + 1 ) e. NN0 )
204	203	nn0cnd	\|- ( ( ( ph /\ a e. S ) /\ m e. NN0 ) -> ( m + 1 ) e. CC )
205	133 203	ffvelcdmd	\|- ( ( ( ph /\ a e. S ) /\ m e. NN0 ) -> ( A ` ( m + 1 ) ) e. CC )
206	204 205	mulcld	\|- ( ( ( ph /\ a e. S ) /\ m e. NN0 ) -> ( ( m + 1 ) x. ( A ` ( m + 1 ) ) ) e. CC )
207	206	fmpttd	\|- ( ( ph /\ a e. S ) -> ( m e. NN0 \|-> ( ( m + 1 ) x. ( A ` ( m + 1 ) ) ) ) : NN0 --> CC )
208		fveq2	\|- ( r = j -> ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` r ) = ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` j ) )
209	208	seqeq3d	\|- ( r = j -> seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` r ) ) = seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` j ) ) )
210	209	eleq1d	\|- ( r = j -> ( seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` r ) ) e. dom ~~> <-> seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` j ) ) e. dom ~~> ) )
211	210	cbvrabv	\|- { r e. RR \| seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` r ) ) e. dom ~~> } = { j e. RR \| seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` j ) ) e. dom ~~> }
212	211	supeq1i	\|- sup ( { r e. RR \| seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) = sup ( { j e. RR \| seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` j ) ) e. dom ~~> } , RR* , < )
213	198	seqeq3d	\|- ( y = z -> seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ) = seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` z ) ) )
214	213	fveq1d	\|- ( y = z -> ( seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ) ` j ) = ( seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` z ) ) ` j ) )
215	214	cbvmptv	\|- ( y e. B \|-> ( seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ) ` j ) ) = ( z e. B \|-> ( seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` z ) ) ` j ) )
216		fveq2	\|- ( j = m -> ( seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` z ) ) ` j ) = ( seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` z ) ) ` m ) )
217	216	mpteq2dv	\|- ( j = m -> ( z e. B \|-> ( seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` z ) ) ` j ) ) = ( z e. B \|-> ( seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` z ) ) ` m ) ) )
218	215 217	eqtrid	\|- ( j = m -> ( y e. B \|-> ( seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ) ` j ) ) = ( z e. B \|-> ( seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` z ) ) ` m ) ) )
219	218	cbvmptv	\|- ( j e. NN0 \|-> ( y e. B \|-> ( seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ) ` j ) ) ) = ( m e. NN0 \|-> ( z e. B \|-> ( seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` z ) ) ` m ) ) )
220	17	rpred	\|- ( ( ph /\ a e. S ) -> ( ( ( abs ` a ) + M ) / 2 ) e. RR )
221	1 2 3 4 5 6	psercnlem1	\|- ( ( ph /\ a e. S ) -> ( M e. RR+ /\ ( abs ` a ) < M /\ M < R ) )
222	221	simp1d	\|- ( ( ph /\ a e. S ) -> M e. RR+ )
223	222	rpxrd	\|- ( ( ph /\ a e. S ) -> M e. RR* )
224	197 207 212	radcnvcl	\|- ( ( ph /\ a e. S ) -> sup ( { r e. RR \| seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) e. ( 0 [,] +oo ) )
225	54 224	sselid	\|- ( ( ph /\ a e. S ) -> sup ( { r e. RR \| seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) e. RR* )
226	221	simp2d	\|- ( ( ph /\ a e. S ) -> ( abs ` a ) < M )
227		cnvimass	\|- ( `' abs " ( 0 [,) R ) ) C_ dom abs
228		absf	\|- abs : CC --> RR
229	228	fdmi	\|- dom abs = CC
230	227 229	sseqtri	\|- ( `' abs " ( 0 [,) R ) ) C_ CC
231	5 230	eqsstri	\|- S C_ CC
232	231	a1i	\|- ( ph -> S C_ CC )
233	232	sselda	\|- ( ( ph /\ a e. S ) -> a e. CC )
234	233	abscld	\|- ( ( ph /\ a e. S ) -> ( abs ` a ) e. RR )
235	222	rpred	\|- ( ( ph /\ a e. S ) -> M e. RR )
236		avglt2	\|- ( ( ( abs ` a ) e. RR /\ M e. RR ) -> ( ( abs ` a ) < M <-> ( ( ( abs ` a ) + M ) / 2 ) < M ) )
237	234 235 236	syl2anc	\|- ( ( ph /\ a e. S ) -> ( ( abs ` a ) < M <-> ( ( ( abs ` a ) + M ) / 2 ) < M ) )
238	226 237	mpbid	\|- ( ( ph /\ a e. S ) -> ( ( ( abs ` a ) + M ) / 2 ) < M )
239	222	rpge0d	\|- ( ( ph /\ a e. S ) -> 0 <_ M )
240	235 239	absidd	\|- ( ( ph /\ a e. S ) -> ( abs ` M ) = M )
241	222	rpcnd	\|- ( ( ph /\ a e. S ) -> M e. CC )
242		oveq1	\|- ( w = M -> ( w ^ i ) = ( M ^ i ) )
243	242	oveq2d	\|- ( w = M -> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( w ^ i ) ) = ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( M ^ i ) ) )
244	243	mpteq2dv	\|- ( w = M -> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( w ^ i ) ) ) = ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( M ^ i ) ) ) )
245		oveq1	\|- ( a = w -> ( a ^ i ) = ( w ^ i ) )
246	245	oveq2d	\|- ( a = w -> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) = ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( w ^ i ) ) )
247	246	mpteq2dv	\|- ( a = w -> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) = ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( w ^ i ) ) ) )
248	247	cbvmptv	\|- ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) = ( w e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( w ^ i ) ) ) )
249		nn0ex	\|- NN0 e. _V
250	249	mptex	\|- ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( M ^ i ) ) ) e. _V
251	244 248 250	fvmpt	\|- ( M e. CC -> ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` M ) = ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( M ^ i ) ) ) )
252	241 251	syl	\|- ( ( ph /\ a e. S ) -> ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` M ) = ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( M ^ i ) ) ) )
253	252	seqeq3d	\|- ( ( ph /\ a e. S ) -> seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` M ) ) = seq 0 ( + , ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( M ^ i ) ) ) ) )
254		fveq2	\|- ( n = i -> ( A ` n ) = ( A ` i ) )
255		oveq2	\|- ( n = i -> ( x ^ n ) = ( x ^ i ) )
256	254 255	oveq12d	\|- ( n = i -> ( ( A ` n ) x. ( x ^ n ) ) = ( ( A ` i ) x. ( x ^ i ) ) )
257	256	cbvmptv	\|- ( n e. NN0 \|-> ( ( A ` n ) x. ( x ^ n ) ) ) = ( i e. NN0 \|-> ( ( A ` i ) x. ( x ^ i ) ) )
258		oveq1	\|- ( x = y -> ( x ^ i ) = ( y ^ i ) )
259	258	oveq2d	\|- ( x = y -> ( ( A ` i ) x. ( x ^ i ) ) = ( ( A ` i ) x. ( y ^ i ) ) )
260	259	mpteq2dv	\|- ( x = y -> ( i e. NN0 \|-> ( ( A ` i ) x. ( x ^ i ) ) ) = ( i e. NN0 \|-> ( ( A ` i ) x. ( y ^ i ) ) ) )
261	257 260	eqtrid	\|- ( x = y -> ( n e. NN0 \|-> ( ( A ` n ) x. ( x ^ n ) ) ) = ( i e. NN0 \|-> ( ( A ` i ) x. ( y ^ i ) ) ) )
262	261	cbvmptv	\|- ( x e. CC \|-> ( n e. NN0 \|-> ( ( A ` n ) x. ( x ^ n ) ) ) ) = ( y e. CC \|-> ( i e. NN0 \|-> ( ( A ` i ) x. ( y ^ i ) ) ) )
263	1 262	eqtri	\|- G = ( y e. CC \|-> ( i e. NN0 \|-> ( ( A ` i ) x. ( y ^ i ) ) ) )
264		fveq2	\|- ( r = s -> ( G ` r ) = ( G ` s ) )
265	264	seqeq3d	\|- ( r = s -> seq 0 ( + , ( G ` r ) ) = seq 0 ( + , ( G ` s ) ) )
266	265	eleq1d	\|- ( r = s -> ( seq 0 ( + , ( G ` r ) ) e. dom ~~> <-> seq 0 ( + , ( G ` s ) ) e. dom ~~> ) )
267	266	cbvrabv	\|- { r e. RR \| seq 0 ( + , ( G ` r ) ) e. dom ~~> } = { s e. RR \| seq 0 ( + , ( G ` s ) ) e. dom ~~> }
268	267	supeq1i	\|- sup ( { r e. RR \| seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < ) = sup ( { s e. RR \| seq 0 ( + , ( G ` s ) ) e. dom ~~> } , RR* , < )
269	4 268	eqtri	\|- R = sup ( { s e. RR \| seq 0 ( + , ( G ` s ) ) e. dom ~~> } , RR* , < )
270		eqid	\|- ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( M ^ i ) ) ) = ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( M ^ i ) ) )
271	3	adantr	\|- ( ( ph /\ a e. S ) -> A : NN0 --> CC )
272	221	simp3d	\|- ( ( ph /\ a e. S ) -> M < R )
273	240 272	eqbrtrd	\|- ( ( ph /\ a e. S ) -> ( abs ` M ) < R )
274	263 269 270 271 241 273	dvradcnv	\|- ( ( ph /\ a e. S ) -> seq 0 ( + , ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( M ^ i ) ) ) ) e. dom ~~> )
275	253 274	eqeltrd	\|- ( ( ph /\ a e. S ) -> seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` M ) ) e. dom ~~> )
276	197 207 212 241 275	radcnvle	\|- ( ( ph /\ a e. S ) -> ( abs ` M ) <_ sup ( { r e. RR \| seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) )
277	240 276	eqbrtrrd	\|- ( ( ph /\ a e. S ) -> M <_ sup ( { r e. RR \| seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) )
278	18 223 225 238 277	xrltletrd	\|- ( ( ph /\ a e. S ) -> ( ( ( abs ` a ) + M ) / 2 ) < sup ( { r e. RR \| seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` r ) ) e. dom ~~> } , RR* , < ) )
279	197 201 207 212 219 220 278 41	pserulm	\|- ( ( ph /\ a e. S ) -> ( j e. NN0 \|-> ( y e. B \|-> ( seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ) ` j ) ) ) ( ~~>u ` B ) ( y e. B \|-> sum_ k e. NN0 ( ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ` k ) ) )
280	21	sselda	\|- ( ( ( ph /\ a e. S ) /\ y e. B ) -> y e. CC )
281		oveq1	\|- ( a = y -> ( a ^ i ) = ( y ^ i ) )
282	281	oveq2d	\|- ( a = y -> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) = ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( y ^ i ) ) )
283	282	mpteq2dv	\|- ( a = y -> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) = ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( y ^ i ) ) ) )
284		eqid	\|- ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) = ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) )
285	249	mptex	\|- ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( y ^ i ) ) ) e. _V
286	283 284 285	fvmpt	\|- ( y e. CC -> ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) = ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( y ^ i ) ) ) )
287	280 286	syl	\|- ( ( ( ph /\ a e. S ) /\ y e. B ) -> ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) = ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( y ^ i ) ) ) )
288	287	adantr	\|- ( ( ( ( ph /\ a e. S ) /\ y e. B ) /\ k e. NN0 ) -> ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) = ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( y ^ i ) ) ) )
289	288	fveq1d	\|- ( ( ( ( ph /\ a e. S ) /\ y e. B ) /\ k e. NN0 ) -> ( ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ` k ) = ( ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( y ^ i ) ) ) ` k ) )
290		oveq1	\|- ( i = k -> ( i + 1 ) = ( k + 1 ) )
291		fvoveq1	\|- ( i = k -> ( A ` ( i + 1 ) ) = ( A ` ( k + 1 ) ) )
292	290 291	oveq12d	\|- ( i = k -> ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) = ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) )
293		oveq2	\|- ( i = k -> ( y ^ i ) = ( y ^ k ) )
294	292 293	oveq12d	\|- ( i = k -> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( y ^ i ) ) = ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) )
295		eqid	\|- ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( y ^ i ) ) ) = ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( y ^ i ) ) )
296		ovex	\|- ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) e. _V
297	294 295 296	fvmpt	\|- ( k e. NN0 -> ( ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( y ^ i ) ) ) ` k ) = ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) )
298	297	adantl	\|- ( ( ( ( ph /\ a e. S ) /\ y e. B ) /\ k e. NN0 ) -> ( ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( y ^ i ) ) ) ` k ) = ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) )
299	289 298	eqtrd	\|- ( ( ( ( ph /\ a e. S ) /\ y e. B ) /\ k e. NN0 ) -> ( ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ` k ) = ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) )
300	299	sumeq2dv	\|- ( ( ( ph /\ a e. S ) /\ y e. B ) -> sum_ k e. NN0 ( ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ` k ) = sum_ k e. NN0 ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) )
301	300	mpteq2dva	\|- ( ( ph /\ a e. S ) -> ( y e. B \|-> sum_ k e. NN0 ( ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ` k ) ) = ( y e. B \|-> sum_ k e. NN0 ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) ) )
302	279 301	breqtrd	\|- ( ( ph /\ a e. S ) -> ( j e. NN0 \|-> ( y e. B \|-> ( seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ) ` j ) ) ) ( ~~>u ` B ) ( y e. B \|-> sum_ k e. NN0 ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) ) )
303		nnuz	\|- NN = ( ZZ>= ` 1 )
304		1e0p1	\|- 1 = ( 0 + 1 )
305	304	fveq2i	\|- ( ZZ>= ` 1 ) = ( ZZ>= ` ( 0 + 1 ) )
306	303 305	eqtri	\|- NN = ( ZZ>= ` ( 0 + 1 ) )
307		1zzd	\|- ( ( ph /\ a e. S ) -> 1 e. ZZ )
308		0zd	\|- ( ( ( ph /\ a e. S ) /\ y e. B ) -> 0 e. ZZ )
309		peano2nn0	\|- ( i e. NN0 -> ( i + 1 ) e. NN0 )
310	309	nn0cnd	\|- ( i e. NN0 -> ( i + 1 ) e. CC )
311	310	adantl	\|- ( ( ( ( ph /\ a e. S ) /\ y e. B ) /\ i e. NN0 ) -> ( i + 1 ) e. CC )
312	3	ad2antrr	\|- ( ( ( ph /\ a e. S ) /\ y e. B ) -> A : NN0 --> CC )
313		ffvelcdm	\|- ( ( A : NN0 --> CC /\ ( i + 1 ) e. NN0 ) -> ( A ` ( i + 1 ) ) e. CC )
314	312 309 313	syl2an	\|- ( ( ( ( ph /\ a e. S ) /\ y e. B ) /\ i e. NN0 ) -> ( A ` ( i + 1 ) ) e. CC )
315	311 314	mulcld	\|- ( ( ( ( ph /\ a e. S ) /\ y e. B ) /\ i e. NN0 ) -> ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) e. CC )
316	280 148	sylan	\|- ( ( ( ( ph /\ a e. S ) /\ y e. B ) /\ i e. NN0 ) -> ( y ^ i ) e. CC )
317	315 316	mulcld	\|- ( ( ( ( ph /\ a e. S ) /\ y e. B ) /\ i e. NN0 ) -> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( y ^ i ) ) e. CC )
318	287 317	fmpt3d	\|- ( ( ( ph /\ a e. S ) /\ y e. B ) -> ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) : NN0 --> CC )
319	318	ffvelcdmda	\|- ( ( ( ( ph /\ a e. S ) /\ y e. B ) /\ m e. NN0 ) -> ( ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ` m ) e. CC )
320	8 308 319	serf	\|- ( ( ( ph /\ a e. S ) /\ y e. B ) -> seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ) : NN0 --> CC )
321	320	ffvelcdmda	\|- ( ( ( ( ph /\ a e. S ) /\ y e. B ) /\ j e. NN0 ) -> ( seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ) ` j ) e. CC )
322	321	an32s	\|- ( ( ( ( ph /\ a e. S ) /\ j e. NN0 ) /\ y e. B ) -> ( seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ) ` j ) e. CC )
323	322	fmpttd	\|- ( ( ( ph /\ a e. S ) /\ j e. NN0 ) -> ( y e. B \|-> ( seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ) ` j ) ) : B --> CC )
324	30 31	elmap	\|- ( ( y e. B \|-> ( seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ) ` j ) ) e. ( CC ^m B ) <-> ( y e. B \|-> ( seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ) ` j ) ) : B --> CC )
325	323 324	sylibr	\|- ( ( ( ph /\ a e. S ) /\ j e. NN0 ) -> ( y e. B \|-> ( seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ) ` j ) ) e. ( CC ^m B ) )
326	325	fmpttd	\|- ( ( ph /\ a e. S ) -> ( j e. NN0 \|-> ( y e. B \|-> ( seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ) ` j ) ) ) : NN0 --> ( CC ^m B ) )
327		elfznn	\|- ( i e. ( 1 ... m ) -> i e. NN )
328	327	nnne0d	\|- ( i e. ( 1 ... m ) -> i =/= 0 )
329	328	neneqd	\|- ( i e. ( 1 ... m ) -> -. i = 0 )
330	329	iffalsed	\|- ( i e. ( 1 ... m ) -> if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) = ( i x. ( y ^ ( i - 1 ) ) ) )
331	330	oveq2d	\|- ( i e. ( 1 ... m ) -> ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) = ( ( A ` i ) x. ( i x. ( y ^ ( i - 1 ) ) ) ) )
332	331	sumeq2i	\|- sum_ i e. ( 1 ... m ) ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) = sum_ i e. ( 1 ... m ) ( ( A ` i ) x. ( i x. ( y ^ ( i - 1 ) ) ) )
333		1zzd	\|- ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) -> 1 e. ZZ )
334		nnz	\|- ( m e. NN -> m e. ZZ )
335	334	ad2antlr	\|- ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) -> m e. ZZ )
336	271	ad2antrr	\|- ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) -> A : NN0 --> CC )
337	327	nnnn0d	\|- ( i e. ( 1 ... m ) -> i e. NN0 )
338	336 337 142	syl2an	\|- ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ i e. ( 1 ... m ) ) -> ( A ` i ) e. CC )
339	327	adantl	\|- ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ i e. ( 1 ... m ) ) -> i e. NN )
340	339	nncnd	\|- ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ i e. ( 1 ... m ) ) -> i e. CC )
341	280	adantlr	\|- ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) -> y e. CC )
342		nnm1nn0	\|- ( i e. NN -> ( i - 1 ) e. NN0 )
343	327 342	syl	\|- ( i e. ( 1 ... m ) -> ( i - 1 ) e. NN0 )
344		expcl	\|- ( ( y e. CC /\ ( i - 1 ) e. NN0 ) -> ( y ^ ( i - 1 ) ) e. CC )
345	341 343 344	syl2an	\|- ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ i e. ( 1 ... m ) ) -> ( y ^ ( i - 1 ) ) e. CC )
346	340 345	mulcld	\|- ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ i e. ( 1 ... m ) ) -> ( i x. ( y ^ ( i - 1 ) ) ) e. CC )
347	338 346	mulcld	\|- ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ i e. ( 1 ... m ) ) -> ( ( A ` i ) x. ( i x. ( y ^ ( i - 1 ) ) ) ) e. CC )
348		fveq2	\|- ( i = ( k + 1 ) -> ( A ` i ) = ( A ` ( k + 1 ) ) )
349		id	\|- ( i = ( k + 1 ) -> i = ( k + 1 ) )
350		oveq1	\|- ( i = ( k + 1 ) -> ( i - 1 ) = ( ( k + 1 ) - 1 ) )
351	350	oveq2d	\|- ( i = ( k + 1 ) -> ( y ^ ( i - 1 ) ) = ( y ^ ( ( k + 1 ) - 1 ) ) )
352	349 351	oveq12d	\|- ( i = ( k + 1 ) -> ( i x. ( y ^ ( i - 1 ) ) ) = ( ( k + 1 ) x. ( y ^ ( ( k + 1 ) - 1 ) ) ) )
353	348 352	oveq12d	\|- ( i = ( k + 1 ) -> ( ( A ` i ) x. ( i x. ( y ^ ( i - 1 ) ) ) ) = ( ( A ` ( k + 1 ) ) x. ( ( k + 1 ) x. ( y ^ ( ( k + 1 ) - 1 ) ) ) ) )
354	333 333 335 347 353	fsumshftm	\|- ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) -> sum_ i e. ( 1 ... m ) ( ( A ` i ) x. ( i x. ( y ^ ( i - 1 ) ) ) ) = sum_ k e. ( ( 1 - 1 ) ... ( m - 1 ) ) ( ( A ` ( k + 1 ) ) x. ( ( k + 1 ) x. ( y ^ ( ( k + 1 ) - 1 ) ) ) ) )
355	332 354	eqtrid	\|- ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) -> sum_ i e. ( 1 ... m ) ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) = sum_ k e. ( ( 1 - 1 ) ... ( m - 1 ) ) ( ( A ` ( k + 1 ) ) x. ( ( k + 1 ) x. ( y ^ ( ( k + 1 ) - 1 ) ) ) ) )
356		fz1ssfz0	\|- ( 1 ... m ) C_ ( 0 ... m )
357	356	a1i	\|- ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) -> ( 1 ... m ) C_ ( 0 ... m ) )
358	331	adantl	\|- ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ i e. ( 1 ... m ) ) -> ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) = ( ( A ` i ) x. ( i x. ( y ^ ( i - 1 ) ) ) ) )
359	358 347	eqeltrd	\|- ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ i e. ( 1 ... m ) ) -> ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) e. CC )
360		eldif	\|- ( i e. ( ( 0 ... m ) \ ( ( 0 + 1 ) ... m ) ) <-> ( i e. ( 0 ... m ) /\ -. i e. ( ( 0 + 1 ) ... m ) ) )
361		elfzuz2	\|- ( i e. ( 0 ... m ) -> m e. ( ZZ>= ` 0 ) )
362		elfzp12	\|- ( m e. ( ZZ>= ` 0 ) -> ( i e. ( 0 ... m ) <-> ( i = 0 \/ i e. ( ( 0 + 1 ) ... m ) ) ) )
363	361 362	syl	\|- ( i e. ( 0 ... m ) -> ( i e. ( 0 ... m ) <-> ( i = 0 \/ i e. ( ( 0 + 1 ) ... m ) ) ) )
364	363	ibi	\|- ( i e. ( 0 ... m ) -> ( i = 0 \/ i e. ( ( 0 + 1 ) ... m ) ) )
365	364	ord	\|- ( i e. ( 0 ... m ) -> ( -. i = 0 -> i e. ( ( 0 + 1 ) ... m ) ) )
366	365	con1d	\|- ( i e. ( 0 ... m ) -> ( -. i e. ( ( 0 + 1 ) ... m ) -> i = 0 ) )
367	366	imp	\|- ( ( i e. ( 0 ... m ) /\ -. i e. ( ( 0 + 1 ) ... m ) ) -> i = 0 )
368	360 367	sylbi	\|- ( i e. ( ( 0 ... m ) \ ( ( 0 + 1 ) ... m ) ) -> i = 0 )
369	304	oveq1i	\|- ( 1 ... m ) = ( ( 0 + 1 ) ... m )
370	369	difeq2i	\|- ( ( 0 ... m ) \ ( 1 ... m ) ) = ( ( 0 ... m ) \ ( ( 0 + 1 ) ... m ) )
371	368 370	eleq2s	\|- ( i e. ( ( 0 ... m ) \ ( 1 ... m ) ) -> i = 0 )
372	371	adantl	\|- ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ i e. ( ( 0 ... m ) \ ( 1 ... m ) ) ) -> i = 0 )
373	372	iftrued	\|- ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ i e. ( ( 0 ... m ) \ ( 1 ... m ) ) ) -> if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) = 0 )
374	373	oveq2d	\|- ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ i e. ( ( 0 ... m ) \ ( 1 ... m ) ) ) -> ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) = ( ( A ` i ) x. 0 ) )
375		eldifi	\|- ( i e. ( ( 0 ... m ) \ ( 1 ... m ) ) -> i e. ( 0 ... m ) )
376	375 104	syl	\|- ( i e. ( ( 0 ... m ) \ ( 1 ... m ) ) -> i e. NN0 )
377	336 376 142	syl2an	\|- ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ i e. ( ( 0 ... m ) \ ( 1 ... m ) ) ) -> ( A ` i ) e. CC )
378	377	mul01d	\|- ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ i e. ( ( 0 ... m ) \ ( 1 ... m ) ) ) -> ( ( A ` i ) x. 0 ) = 0 )
379	374 378	eqtrd	\|- ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ i e. ( ( 0 ... m ) \ ( 1 ... m ) ) ) -> ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) = 0 )
380		fzfid	\|- ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) -> ( 0 ... m ) e. Fin )
381	357 359 379 380	fsumss	\|- ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) -> sum_ i e. ( 1 ... m ) ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) = sum_ i e. ( 0 ... m ) ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) )
382		1m1e0	\|- ( 1 - 1 ) = 0
383	382	oveq1i	\|- ( ( 1 - 1 ) ... ( m - 1 ) ) = ( 0 ... ( m - 1 ) )
384	383	sumeq1i	\|- sum_ k e. ( ( 1 - 1 ) ... ( m - 1 ) ) ( ( A ` ( k + 1 ) ) x. ( ( k + 1 ) x. ( y ^ ( ( k + 1 ) - 1 ) ) ) ) = sum_ k e. ( 0 ... ( m - 1 ) ) ( ( A ` ( k + 1 ) ) x. ( ( k + 1 ) x. ( y ^ ( ( k + 1 ) - 1 ) ) ) )
385		elfznn0	\|- ( k e. ( 0 ... ( m - 1 ) ) -> k e. NN0 )
386	385	adantl	\|- ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ k e. ( 0 ... ( m - 1 ) ) ) -> k e. NN0 )
387	386 297	syl	\|- ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ k e. ( 0 ... ( m - 1 ) ) ) -> ( ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( y ^ i ) ) ) ` k ) = ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) )
388	341	adantr	\|- ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ k e. ( 0 ... ( m - 1 ) ) ) -> y e. CC )
389	388 286	syl	\|- ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ k e. ( 0 ... ( m - 1 ) ) ) -> ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) = ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( y ^ i ) ) ) )
390	389	fveq1d	\|- ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ k e. ( 0 ... ( m - 1 ) ) ) -> ( ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ` k ) = ( ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( y ^ i ) ) ) ` k ) )
391	336	adantr	\|- ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ k e. ( 0 ... ( m - 1 ) ) ) -> A : NN0 --> CC )
392		peano2nn0	\|- ( k e. NN0 -> ( k + 1 ) e. NN0 )
393	386 392	syl	\|- ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ k e. ( 0 ... ( m - 1 ) ) ) -> ( k + 1 ) e. NN0 )
394	391 393	ffvelcdmd	\|- ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ k e. ( 0 ... ( m - 1 ) ) ) -> ( A ` ( k + 1 ) ) e. CC )
395	393	nn0cnd	\|- ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ k e. ( 0 ... ( m - 1 ) ) ) -> ( k + 1 ) e. CC )
396		expcl	\|- ( ( y e. CC /\ k e. NN0 ) -> ( y ^ k ) e. CC )
397	341 385 396	syl2an	\|- ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ k e. ( 0 ... ( m - 1 ) ) ) -> ( y ^ k ) e. CC )
398	394 395 397	mul12d	\|- ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ k e. ( 0 ... ( m - 1 ) ) ) -> ( ( A ` ( k + 1 ) ) x. ( ( k + 1 ) x. ( y ^ k ) ) ) = ( ( k + 1 ) x. ( ( A ` ( k + 1 ) ) x. ( y ^ k ) ) ) )
399	386	nn0cnd	\|- ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ k e. ( 0 ... ( m - 1 ) ) ) -> k e. CC )
400		ax-1cn	\|- 1 e. CC
401		pncan	\|- ( ( k e. CC /\ 1 e. CC ) -> ( ( k + 1 ) - 1 ) = k )
402	399 400 401	sylancl	\|- ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ k e. ( 0 ... ( m - 1 ) ) ) -> ( ( k + 1 ) - 1 ) = k )
403	402	oveq2d	\|- ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ k e. ( 0 ... ( m - 1 ) ) ) -> ( y ^ ( ( k + 1 ) - 1 ) ) = ( y ^ k ) )
404	403	oveq2d	\|- ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ k e. ( 0 ... ( m - 1 ) ) ) -> ( ( k + 1 ) x. ( y ^ ( ( k + 1 ) - 1 ) ) ) = ( ( k + 1 ) x. ( y ^ k ) ) )
405	404	oveq2d	\|- ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ k e. ( 0 ... ( m - 1 ) ) ) -> ( ( A ` ( k + 1 ) ) x. ( ( k + 1 ) x. ( y ^ ( ( k + 1 ) - 1 ) ) ) ) = ( ( A ` ( k + 1 ) ) x. ( ( k + 1 ) x. ( y ^ k ) ) ) )
406	395 394 397	mulassd	\|- ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ k e. ( 0 ... ( m - 1 ) ) ) -> ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) = ( ( k + 1 ) x. ( ( A ` ( k + 1 ) ) x. ( y ^ k ) ) ) )
407	398 405 406	3eqtr4d	\|- ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ k e. ( 0 ... ( m - 1 ) ) ) -> ( ( A ` ( k + 1 ) ) x. ( ( k + 1 ) x. ( y ^ ( ( k + 1 ) - 1 ) ) ) ) = ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) )
408	387 390 407	3eqtr4d	\|- ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ k e. ( 0 ... ( m - 1 ) ) ) -> ( ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ` k ) = ( ( A ` ( k + 1 ) ) x. ( ( k + 1 ) x. ( y ^ ( ( k + 1 ) - 1 ) ) ) ) )
409		nnm1nn0	\|- ( m e. NN -> ( m - 1 ) e. NN0 )
410	409	adantl	\|- ( ( ( ph /\ a e. S ) /\ m e. NN ) -> ( m - 1 ) e. NN0 )
411	410	adantr	\|- ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) -> ( m - 1 ) e. NN0 )
412	411 8	eleqtrdi	\|- ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) -> ( m - 1 ) e. ( ZZ>= ` 0 ) )
413	403 397	eqeltrd	\|- ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ k e. ( 0 ... ( m - 1 ) ) ) -> ( y ^ ( ( k + 1 ) - 1 ) ) e. CC )
414	395 413	mulcld	\|- ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ k e. ( 0 ... ( m - 1 ) ) ) -> ( ( k + 1 ) x. ( y ^ ( ( k + 1 ) - 1 ) ) ) e. CC )
415	394 414	mulcld	\|- ( ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) /\ k e. ( 0 ... ( m - 1 ) ) ) -> ( ( A ` ( k + 1 ) ) x. ( ( k + 1 ) x. ( y ^ ( ( k + 1 ) - 1 ) ) ) ) e. CC )
416	408 412 415	fsumser	\|- ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) -> sum_ k e. ( 0 ... ( m - 1 ) ) ( ( A ` ( k + 1 ) ) x. ( ( k + 1 ) x. ( y ^ ( ( k + 1 ) - 1 ) ) ) ) = ( seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ) ` ( m - 1 ) ) )
417	384 416	eqtrid	\|- ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) -> sum_ k e. ( ( 1 - 1 ) ... ( m - 1 ) ) ( ( A ` ( k + 1 ) ) x. ( ( k + 1 ) x. ( y ^ ( ( k + 1 ) - 1 ) ) ) ) = ( seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ) ` ( m - 1 ) ) )
418	355 381 417	3eqtr3d	\|- ( ( ( ( ph /\ a e. S ) /\ m e. NN ) /\ y e. B ) -> sum_ i e. ( 0 ... m ) ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) = ( seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ) ` ( m - 1 ) ) )
419	418	mpteq2dva	\|- ( ( ( ph /\ a e. S ) /\ m e. NN ) -> ( y e. B \|-> sum_ i e. ( 0 ... m ) ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) ) = ( y e. B \|-> ( seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ) ` ( m - 1 ) ) ) )
420		fveq2	\|- ( j = ( m - 1 ) -> ( seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ) ` j ) = ( seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ) ` ( m - 1 ) ) )
421	420	mpteq2dv	\|- ( j = ( m - 1 ) -> ( y e. B \|-> ( seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ) ` j ) ) = ( y e. B \|-> ( seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ) ` ( m - 1 ) ) ) )
422		eqid	\|- ( j e. NN0 \|-> ( y e. B \|-> ( seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ) ` j ) ) ) = ( j e. NN0 \|-> ( y e. B \|-> ( seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ) ` j ) ) )
423	31	mptex	\|- ( y e. B \|-> ( seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ) ` ( m - 1 ) ) ) e. _V
424	421 422 423	fvmpt	\|- ( ( m - 1 ) e. NN0 -> ( ( j e. NN0 \|-> ( y e. B \|-> ( seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ) ` j ) ) ) ` ( m - 1 ) ) = ( y e. B \|-> ( seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ) ` ( m - 1 ) ) ) )
425	410 424	syl	\|- ( ( ( ph /\ a e. S ) /\ m e. NN ) -> ( ( j e. NN0 \|-> ( y e. B \|-> ( seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ) ` j ) ) ) ` ( m - 1 ) ) = ( y e. B \|-> ( seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ) ` ( m - 1 ) ) ) )
426	419 425	eqtr4d	\|- ( ( ( ph /\ a e. S ) /\ m e. NN ) -> ( y e. B \|-> sum_ i e. ( 0 ... m ) ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) ) = ( ( j e. NN0 \|-> ( y e. B \|-> ( seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ) ` j ) ) ) ` ( m - 1 ) ) )
427	426	mpteq2dva	\|- ( ( ph /\ a e. S ) -> ( m e. NN \|-> ( y e. B \|-> sum_ i e. ( 0 ... m ) ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) ) ) = ( m e. NN \|-> ( ( j e. NN0 \|-> ( y e. B \|-> ( seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ) ` j ) ) ) ` ( m - 1 ) ) ) )
428	8 306 11 307 326 427	ulmshft	\|- ( ( ph /\ a e. S ) -> ( ( j e. NN0 \|-> ( y e. B \|-> ( seq 0 ( + , ( ( a e. CC \|-> ( i e. NN0 \|-> ( ( ( i + 1 ) x. ( A ` ( i + 1 ) ) ) x. ( a ^ i ) ) ) ) ` y ) ) ` j ) ) ) ( ~~>u ` B ) ( y e. B \|-> sum_ k e. NN0 ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) ) <-> ( m e. NN \|-> ( y e. B \|-> sum_ i e. ( 0 ... m ) ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) ) ) ( ~~>u ` B ) ( y e. B \|-> sum_ k e. NN0 ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) ) ) )
429	302 428	mpbid	\|- ( ( ph /\ a e. S ) -> ( m e. NN \|-> ( y e. B \|-> sum_ i e. ( 0 ... m ) ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) ) ) ( ~~>u ` B ) ( y e. B \|-> sum_ k e. NN0 ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) ) )
430	177 429	eqbrtrid	\|- ( ( ph /\ a e. S ) -> ( ( m e. NN0 \|-> ( y e. B \|-> sum_ i e. ( 0 ... m ) ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) ) ) \|` NN ) ( ~~>u ` B ) ( y e. B \|-> sum_ k e. NN0 ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) ) )
431		1nn0	\|- 1 e. NN0
432	431	a1i	\|- ( ( ph /\ a e. S ) -> 1 e. NN0 )
433		fzfid	\|- ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ y e. B ) -> ( 0 ... m ) e. Fin )
434	164	an32s	\|- ( ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ y e. B ) /\ i e. ( 0 ... m ) ) -> ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) e. CC )
435	433 434	fsumcl	\|- ( ( ( ( ph /\ a e. S ) /\ m e. NN0 ) /\ y e. B ) -> sum_ i e. ( 0 ... m ) ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) e. CC )
436	435	fmpttd	\|- ( ( ( ph /\ a e. S ) /\ m e. NN0 ) -> ( y e. B \|-> sum_ i e. ( 0 ... m ) ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) ) : B --> CC )
437	30 31	elmap	\|- ( ( y e. B \|-> sum_ i e. ( 0 ... m ) ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) ) e. ( CC ^m B ) <-> ( y e. B \|-> sum_ i e. ( 0 ... m ) ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) ) : B --> CC )
438	436 437	sylibr	\|- ( ( ( ph /\ a e. S ) /\ m e. NN0 ) -> ( y e. B \|-> sum_ i e. ( 0 ... m ) ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) ) e. ( CC ^m B ) )
439	438	fmpttd	\|- ( ( ph /\ a e. S ) -> ( m e. NN0 \|-> ( y e. B \|-> sum_ i e. ( 0 ... m ) ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) ) ) : NN0 --> ( CC ^m B ) )
440	8 303 432 439	ulmres	\|- ( ( ph /\ a e. S ) -> ( ( m e. NN0 \|-> ( y e. B \|-> sum_ i e. ( 0 ... m ) ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) ) ) ( ~~>u ` B ) ( y e. B \|-> sum_ k e. NN0 ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) ) <-> ( ( m e. NN0 \|-> ( y e. B \|-> sum_ i e. ( 0 ... m ) ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) ) ) \|` NN ) ( ~~>u ` B ) ( y e. B \|-> sum_ k e. NN0 ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) ) ) )
441	430 440	mpbird	\|- ( ( ph /\ a e. S ) -> ( m e. NN0 \|-> ( y e. B \|-> sum_ i e. ( 0 ... m ) ( ( A ` i ) x. if ( i = 0 , 0 , ( i x. ( y ^ ( i - 1 ) ) ) ) ) ) ) ( ~~>u ` B ) ( y e. B \|-> sum_ k e. NN0 ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) ) )
442	174 441	eqbrtrd	\|- ( ( ph /\ a e. S ) -> ( m e. NN0 \|-> ( CC _D ( ( k e. NN0 \|-> ( y e. B \|-> sum_ i e. ( 0 ... k ) ( ( G ` y ) ` i ) ) ) ` m ) ) ) ( ~~>u ` B ) ( y e. B \|-> sum_ k e. NN0 ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) ) )
443	8 10 11 34 44 120 442	ulmdv	\|- ( ( ph /\ a e. S ) -> ( CC _D ( F \|` B ) ) = ( y e. B \|-> sum_ k e. NN0 ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( y ^ k ) ) ) )

Metamath Proof Explorer

Theorem pserdvlem2

Proof