Theorem dvnmul

Description: Function-builder for the N -th derivative, product rule. (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	dvnmul.s	|- ( ph -> S e. { RR , CC } )
	dvnmul.x	|- ( ph -> X e. ( ( TopOpen ` CCfld ) |`t S ) )
	dvnmul.a	|- ( ( ph /\ x e. X ) -> A e. CC )
	dvnmul.cc	|- ( ( ph /\ x e. X ) -> B e. CC )
	dvnmul.n	|- ( ph -> N e. NN0 )
	dvnmulf	|- F = ( x e. X |-> A )
	dvnmul.f	|- G = ( x e. X |-> B )
	dvnmul.dvnf	|- ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( S Dn F ) ` k ) : X --> CC )
	dvnmul.dvng	|- ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( S Dn G ) ` k ) : X --> CC )
	dvnmul.c	|- C = ( k e. ( 0 ... N ) |-> ( ( S Dn F ) ` k ) )
	dvnmul.d	|- D = ( k e. ( 0 ... N ) |-> ( ( S Dn G ) ` k ) )
Assertion	dvnmul	|- ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` N ) = ( x e. X |-> sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( N - k ) ) ` x ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		dvnmul.s	|- ( ph -> S e. { RR , CC } )
2		dvnmul.x	|- ( ph -> X e. ( ( TopOpen ` CCfld ) |`t S ) )
3		dvnmul.a	|- ( ( ph /\ x e. X ) -> A e. CC )
4		dvnmul.cc	|- ( ( ph /\ x e. X ) -> B e. CC )
5		dvnmul.n	|- ( ph -> N e. NN0 )
6		dvnmulf	|- F = ( x e. X |-> A )
7		dvnmul.f	|- G = ( x e. X |-> B )
8		dvnmul.dvnf	|- ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( S Dn F ) ` k ) : X --> CC )
9		dvnmul.dvng	|- ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( S Dn G ) ` k ) : X --> CC )
10		dvnmul.c	|- C = ( k e. ( 0 ... N ) |-> ( ( S Dn F ) ` k ) )
11		dvnmul.d	|- D = ( k e. ( 0 ... N ) |-> ( ( S Dn G ) ` k ) )
12		id	|- ( ph -> ph )
13		nn0uz	|- NN0 = ( ZZ>= ` 0 )
14	5 13	eleqtrdi	|- ( ph -> N e. ( ZZ>= ` 0 ) )
15		eluzfz2	|- ( N e. ( ZZ>= ` 0 ) -> N e. ( 0 ... N ) )
16	14 15	syl	|- ( ph -> N e. ( 0 ... N ) )
17		eleq1	|- ( n = N -> ( n e. ( 0 ... N ) <-> N e. ( 0 ... N ) ) )
18		fveq2	|- ( n = N -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` n ) = ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` N ) )
19		oveq2	|- ( n = N -> ( 0 ... n ) = ( 0 ... N ) )
20	19	sumeq1d	|- ( n = N -> sum_ k e. ( 0 ... n ) ( ( n _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( n - k ) ) ` x ) ) ) = sum_ k e. ( 0 ... N ) ( ( n _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( n - k ) ) ` x ) ) ) )
21		oveq1	|- ( n = N -> ( n _C k ) = ( N _C k ) )
22		fvoveq1	|- ( n = N -> ( D ` ( n - k ) ) = ( D ` ( N - k ) ) )
23	22	fveq1d	|- ( n = N -> ( ( D ` ( n - k ) ) ` x ) = ( ( D ` ( N - k ) ) ` x ) )
24	23	oveq2d	|- ( n = N -> ( ( ( C ` k ) ` x ) x. ( ( D ` ( n - k ) ) ` x ) ) = ( ( ( C ` k ) ` x ) x. ( ( D ` ( N - k ) ) ` x ) ) )
25	21 24	oveq12d	|- ( n = N -> ( ( n _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( n - k ) ) ` x ) ) ) = ( ( N _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( N - k ) ) ` x ) ) ) )
26	25	sumeq2sdv	|- ( n = N -> sum_ k e. ( 0 ... N ) ( ( n _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( n - k ) ) ` x ) ) ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( N - k ) ) ` x ) ) ) )
27	20 26	eqtrd	|- ( n = N -> sum_ k e. ( 0 ... n ) ( ( n _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( n - k ) ) ` x ) ) ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( N - k ) ) ` x ) ) ) )
28	27	mpteq2dv	|- ( n = N -> ( x e. X |-> sum_ k e. ( 0 ... n ) ( ( n _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( n - k ) ) ` x ) ) ) ) = ( x e. X |-> sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( N - k ) ) ` x ) ) ) ) )
29	18 28	eqeq12d	|- ( n = N -> ( ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` n ) = ( x e. X |-> sum_ k e. ( 0 ... n ) ( ( n _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( n - k ) ) ` x ) ) ) ) <-> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` N ) = ( x e. X |-> sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( N - k ) ) ` x ) ) ) ) ) )
30	29	imbi2d	|- ( n = N -> ( ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` n ) = ( x e. X |-> sum_ k e. ( 0 ... n ) ( ( n _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( n - k ) ) ` x ) ) ) ) ) <-> ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` N ) = ( x e. X |-> sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( N - k ) ) ` x ) ) ) ) ) ) )
31	17 30	imbi12d	|- ( n = N -> ( ( n e. ( 0 ... N ) -> ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` n ) = ( x e. X |-> sum_ k e. ( 0 ... n ) ( ( n _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( n - k ) ) ` x ) ) ) ) ) ) <-> ( N e. ( 0 ... N ) -> ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` N ) = ( x e. X |-> sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( N - k ) ) ` x ) ) ) ) ) ) ) )
32		fveq2	|- ( m = 0 -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` m ) = ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` 0 ) )
33		simpl	|- ( ( m = 0 /\ x e. X ) -> m = 0 )
34	33	oveq2d	|- ( ( m = 0 /\ x e. X ) -> ( 0 ... m ) = ( 0 ... 0 ) )
35		simpll	|- ( ( ( m = 0 /\ x e. X ) /\ k e. ( 0 ... 0 ) ) -> m = 0 )
36	35	oveq1d	|- ( ( ( m = 0 /\ x e. X ) /\ k e. ( 0 ... 0 ) ) -> ( m _C k ) = ( 0 _C k ) )
37	35	fvoveq1d	|- ( ( ( m = 0 /\ x e. X ) /\ k e. ( 0 ... 0 ) ) -> ( D ` ( m - k ) ) = ( D ` ( 0 - k ) ) )
38	37	fveq1d	|- ( ( ( m = 0 /\ x e. X ) /\ k e. ( 0 ... 0 ) ) -> ( ( D ` ( m - k ) ) ` x ) = ( ( D ` ( 0 - k ) ) ` x ) )
39	38	oveq2d	|- ( ( ( m = 0 /\ x e. X ) /\ k e. ( 0 ... 0 ) ) -> ( ( ( C ` k ) ` x ) x. ( ( D ` ( m - k ) ) ` x ) ) = ( ( ( C ` k ) ` x ) x. ( ( D ` ( 0 - k ) ) ` x ) ) )
40	36 39	oveq12d	|- ( ( ( m = 0 /\ x e. X ) /\ k e. ( 0 ... 0 ) ) -> ( ( m _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( m - k ) ) ` x ) ) ) = ( ( 0 _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( 0 - k ) ) ` x ) ) ) )
41	34 40	sumeq12rdv	|- ( ( m = 0 /\ x e. X ) -> sum_ k e. ( 0 ... m ) ( ( m _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( m - k ) ) ` x ) ) ) = sum_ k e. ( 0 ... 0 ) ( ( 0 _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( 0 - k ) ) ` x ) ) ) )
42	41	mpteq2dva	|- ( m = 0 -> ( x e. X |-> sum_ k e. ( 0 ... m ) ( ( m _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( m - k ) ) ` x ) ) ) ) = ( x e. X |-> sum_ k e. ( 0 ... 0 ) ( ( 0 _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( 0 - k ) ) ` x ) ) ) ) )
43	32 42	eqeq12d	|- ( m = 0 -> ( ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` m ) = ( x e. X |-> sum_ k e. ( 0 ... m ) ( ( m _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( m - k ) ) ` x ) ) ) ) <-> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` 0 ) = ( x e. X |-> sum_ k e. ( 0 ... 0 ) ( ( 0 _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( 0 - k ) ) ` x ) ) ) ) ) )
44	43	imbi2d	|- ( m = 0 -> ( ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` m ) = ( x e. X |-> sum_ k e. ( 0 ... m ) ( ( m _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( m - k ) ) ` x ) ) ) ) ) <-> ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` 0 ) = ( x e. X |-> sum_ k e. ( 0 ... 0 ) ( ( 0 _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( 0 - k ) ) ` x ) ) ) ) ) ) )
45		fveq2	|- ( m = i -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` m ) = ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` i ) )
46		simpl	|- ( ( m = i /\ x e. X ) -> m = i )
47	46	oveq2d	|- ( ( m = i /\ x e. X ) -> ( 0 ... m ) = ( 0 ... i ) )
48		simpll	|- ( ( ( m = i /\ x e. X ) /\ k e. ( 0 ... i ) ) -> m = i )
49	48	oveq1d	|- ( ( ( m = i /\ x e. X ) /\ k e. ( 0 ... i ) ) -> ( m _C k ) = ( i _C k ) )
50	48	fvoveq1d	|- ( ( ( m = i /\ x e. X ) /\ k e. ( 0 ... i ) ) -> ( D ` ( m - k ) ) = ( D ` ( i - k ) ) )
51	50	fveq1d	|- ( ( ( m = i /\ x e. X ) /\ k e. ( 0 ... i ) ) -> ( ( D ` ( m - k ) ) ` x ) = ( ( D ` ( i - k ) ) ` x ) )
52	51	oveq2d	|- ( ( ( m = i /\ x e. X ) /\ k e. ( 0 ... i ) ) -> ( ( ( C ` k ) ` x ) x. ( ( D ` ( m - k ) ) ` x ) ) = ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) )
53	49 52	oveq12d	|- ( ( ( m = i /\ x e. X ) /\ k e. ( 0 ... i ) ) -> ( ( m _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( m - k ) ) ` x ) ) ) = ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) )
54	47 53	sumeq12rdv	|- ( ( m = i /\ x e. X ) -> sum_ k e. ( 0 ... m ) ( ( m _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( m - k ) ) ` x ) ) ) = sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) )
55	54	mpteq2dva	|- ( m = i -> ( x e. X |-> sum_ k e. ( 0 ... m ) ( ( m _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( m - k ) ) ` x ) ) ) ) = ( x e. X |-> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) )
56	45 55	eqeq12d	|- ( m = i -> ( ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` m ) = ( x e. X |-> sum_ k e. ( 0 ... m ) ( ( m _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( m - k ) ) ` x ) ) ) ) <-> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` i ) = ( x e. X |-> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) ) )
57	56	imbi2d	|- ( m = i -> ( ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` m ) = ( x e. X |-> sum_ k e. ( 0 ... m ) ( ( m _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( m - k ) ) ` x ) ) ) ) ) <-> ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` i ) = ( x e. X |-> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) ) ) )
58		fveq2	|- ( m = ( i + 1 ) -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` m ) = ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` ( i + 1 ) ) )
59		simpl	|- ( ( m = ( i + 1 ) /\ x e. X ) -> m = ( i + 1 ) )
60	59	oveq2d	|- ( ( m = ( i + 1 ) /\ x e. X ) -> ( 0 ... m ) = ( 0 ... ( i + 1 ) ) )
61		simpll	|- ( ( ( m = ( i + 1 ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> m = ( i + 1 ) )
62	61	oveq1d	|- ( ( ( m = ( i + 1 ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( m _C k ) = ( ( i + 1 ) _C k ) )
63	61	fvoveq1d	|- ( ( ( m = ( i + 1 ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( D ` ( m - k ) ) = ( D ` ( ( i + 1 ) - k ) ) )
64	63	fveq1d	|- ( ( ( m = ( i + 1 ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( D ` ( m - k ) ) ` x ) = ( ( D ` ( ( i + 1 ) - k ) ) ` x ) )
65	64	oveq2d	|- ( ( ( m = ( i + 1 ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( ( C ` k ) ` x ) x. ( ( D ` ( m - k ) ) ` x ) ) = ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) )
66	62 65	oveq12d	|- ( ( ( m = ( i + 1 ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( m _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( m - k ) ) ` x ) ) ) = ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) )
67	60 66	sumeq12rdv	|- ( ( m = ( i + 1 ) /\ x e. X ) -> sum_ k e. ( 0 ... m ) ( ( m _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( m - k ) ) ` x ) ) ) = sum_ k e. ( 0 ... ( i + 1 ) ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) )
68	67	mpteq2dva	|- ( m = ( i + 1 ) -> ( x e. X |-> sum_ k e. ( 0 ... m ) ( ( m _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( m - k ) ) ` x ) ) ) ) = ( x e. X |-> sum_ k e. ( 0 ... ( i + 1 ) ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
69	58 68	eqeq12d	|- ( m = ( i + 1 ) -> ( ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` m ) = ( x e. X |-> sum_ k e. ( 0 ... m ) ( ( m _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( m - k ) ) ` x ) ) ) ) <-> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` ( i + 1 ) ) = ( x e. X |-> sum_ k e. ( 0 ... ( i + 1 ) ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) ) )
70	69	imbi2d	|- ( m = ( i + 1 ) -> ( ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` m ) = ( x e. X |-> sum_ k e. ( 0 ... m ) ( ( m _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( m - k ) ) ` x ) ) ) ) ) <-> ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` ( i + 1 ) ) = ( x e. X |-> sum_ k e. ( 0 ... ( i + 1 ) ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) ) ) )
71		fveq2	|- ( m = n -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` m ) = ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` n ) )
72		simpl	|- ( ( m = n /\ x e. X ) -> m = n )
73	72	oveq2d	|- ( ( m = n /\ x e. X ) -> ( 0 ... m ) = ( 0 ... n ) )
74		simpll	|- ( ( ( m = n /\ x e. X ) /\ k e. ( 0 ... n ) ) -> m = n )
75	74	oveq1d	|- ( ( ( m = n /\ x e. X ) /\ k e. ( 0 ... n ) ) -> ( m _C k ) = ( n _C k ) )
76	74	fvoveq1d	|- ( ( ( m = n /\ x e. X ) /\ k e. ( 0 ... n ) ) -> ( D ` ( m - k ) ) = ( D ` ( n - k ) ) )
77	76	fveq1d	|- ( ( ( m = n /\ x e. X ) /\ k e. ( 0 ... n ) ) -> ( ( D ` ( m - k ) ) ` x ) = ( ( D ` ( n - k ) ) ` x ) )
78	77	oveq2d	|- ( ( ( m = n /\ x e. X ) /\ k e. ( 0 ... n ) ) -> ( ( ( C ` k ) ` x ) x. ( ( D ` ( m - k ) ) ` x ) ) = ( ( ( C ` k ) ` x ) x. ( ( D ` ( n - k ) ) ` x ) ) )
79	75 78	oveq12d	|- ( ( ( m = n /\ x e. X ) /\ k e. ( 0 ... n ) ) -> ( ( m _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( m - k ) ) ` x ) ) ) = ( ( n _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( n - k ) ) ` x ) ) ) )
80	73 79	sumeq12rdv	|- ( ( m = n /\ x e. X ) -> sum_ k e. ( 0 ... m ) ( ( m _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( m - k ) ) ` x ) ) ) = sum_ k e. ( 0 ... n ) ( ( n _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( n - k ) ) ` x ) ) ) )
81	80	mpteq2dva	|- ( m = n -> ( x e. X |-> sum_ k e. ( 0 ... m ) ( ( m _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( m - k ) ) ` x ) ) ) ) = ( x e. X |-> sum_ k e. ( 0 ... n ) ( ( n _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( n - k ) ) ` x ) ) ) ) )
82	71 81	eqeq12d	|- ( m = n -> ( ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` m ) = ( x e. X |-> sum_ k e. ( 0 ... m ) ( ( m _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( m - k ) ) ` x ) ) ) ) <-> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` n ) = ( x e. X |-> sum_ k e. ( 0 ... n ) ( ( n _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( n - k ) ) ` x ) ) ) ) ) )
83	82	imbi2d	|- ( m = n -> ( ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` m ) = ( x e. X |-> sum_ k e. ( 0 ... m ) ( ( m _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( m - k ) ) ` x ) ) ) ) ) <-> ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` n ) = ( x e. X |-> sum_ k e. ( 0 ... n ) ( ( n _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( n - k ) ) ` x ) ) ) ) ) ) )
84		recnprss	|- ( S e. { RR , CC } -> S C_ CC )
85	1 84	syl	|- ( ph -> S C_ CC )
86	3 4	mulcld	|- ( ( ph /\ x e. X ) -> ( A x. B ) e. CC )
87		restsspw	|- ( ( TopOpen ` CCfld ) |`t S ) C_ ~P S
88	87 2	sseldi	|- ( ph -> X e. ~P S )
89		elpwi	|- ( X e. ~P S -> X C_ S )
90	88 89	syl	|- ( ph -> X C_ S )
91		cnex	|- CC e. _V
92	91	a1i	|- ( ph -> CC e. _V )
93	86 90 92 1	mptelpm	|- ( ph -> ( x e. X |-> ( A x. B ) ) e. ( CC ^pm S ) )
94		dvn0	|- ( ( S C_ CC /\ ( x e. X |-> ( A x. B ) ) e. ( CC ^pm S ) ) -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` 0 ) = ( x e. X |-> ( A x. B ) ) )
95	85 93 94	syl2anc	|- ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` 0 ) = ( x e. X |-> ( A x. B ) ) )
96		0z	|- 0 e. ZZ
97		fzsn	|- ( 0 e. ZZ -> ( 0 ... 0 ) = { 0 } )
98	96 97	ax-mp	|- ( 0 ... 0 ) = { 0 }
99	98	sumeq1i	|- sum_ k e. ( 0 ... 0 ) ( ( 0 _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( 0 - k ) ) ` x ) ) ) = sum_ k e. { 0 } ( ( 0 _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( 0 - k ) ) ` x ) ) )
100	99	a1i	|- ( ( ph /\ x e. X ) -> sum_ k e. ( 0 ... 0 ) ( ( 0 _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( 0 - k ) ) ` x ) ) ) = sum_ k e. { 0 } ( ( 0 _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( 0 - k ) ) ` x ) ) ) )
101		nfcvd	|- ( ( ph /\ x e. X ) -> F/_ k ( A x. B ) )
102		nfv	|- F/ k ( ph /\ x e. X )
103		oveq2	|- ( k = 0 -> ( 0 _C k ) = ( 0 _C 0 ) )
104		0nn0	|- 0 e. NN0
105		bcn0	|- ( 0 e. NN0 -> ( 0 _C 0 ) = 1 )
106	104 105	ax-mp	|- ( 0 _C 0 ) = 1
107	106	a1i	|- ( k = 0 -> ( 0 _C 0 ) = 1 )
108	103 107	eqtrd	|- ( k = 0 -> ( 0 _C k ) = 1 )
109	108	adantl	|- ( ( ( ph /\ x e. X ) /\ k = 0 ) -> ( 0 _C k ) = 1 )
110		fveq2	|- ( k = 0 -> ( C ` k ) = ( C ` 0 ) )
111	110	adantl	|- ( ( ph /\ k = 0 ) -> ( C ` k ) = ( C ` 0 ) )
112		fveq2	|- ( k = n -> ( ( S Dn F ) ` k ) = ( ( S Dn F ) ` n ) )
113	112	cbvmptv	|- ( k e. ( 0 ... N ) |-> ( ( S Dn F ) ` k ) ) = ( n e. ( 0 ... N ) |-> ( ( S Dn F ) ` n ) )
114	10 113	eqtri	|- C = ( n e. ( 0 ... N ) |-> ( ( S Dn F ) ` n ) )
115		fveq2	|- ( n = 0 -> ( ( S Dn F ) ` n ) = ( ( S Dn F ) ` 0 ) )
116		eluzfz1	|- ( N e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... N ) )
117	14 116	syl	|- ( ph -> 0 e. ( 0 ... N ) )
118		fvexd	|- ( ph -> ( ( S Dn F ) ` 0 ) e. _V )
119	114 115 117 118	fvmptd3	|- ( ph -> ( C ` 0 ) = ( ( S Dn F ) ` 0 ) )
120	119	adantr	|- ( ( ph /\ k = 0 ) -> ( C ` 0 ) = ( ( S Dn F ) ` 0 ) )
121	111 120	eqtrd	|- ( ( ph /\ k = 0 ) -> ( C ` k ) = ( ( S Dn F ) ` 0 ) )
122	3 90 92 1	mptelpm	|- ( ph -> ( x e. X |-> A ) e. ( CC ^pm S ) )
123	6 122	eqeltrid	|- ( ph -> F e. ( CC ^pm S ) )
124		dvn0	|- ( ( S C_ CC /\ F e. ( CC ^pm S ) ) -> ( ( S Dn F ) ` 0 ) = F )
125	85 123 124	syl2anc	|- ( ph -> ( ( S Dn F ) ` 0 ) = F )
126	125	adantr	|- ( ( ph /\ k = 0 ) -> ( ( S Dn F ) ` 0 ) = F )
127	121 126	eqtrd	|- ( ( ph /\ k = 0 ) -> ( C ` k ) = F )
128	127	fveq1d	|- ( ( ph /\ k = 0 ) -> ( ( C ` k ) ` x ) = ( F ` x ) )
129	128	adantlr	|- ( ( ( ph /\ x e. X ) /\ k = 0 ) -> ( ( C ` k ) ` x ) = ( F ` x ) )
130		simpr	|- ( ( ph /\ x e. X ) -> x e. X )
131	6	fvmpt2	|- ( ( x e. X /\ A e. CC ) -> ( F ` x ) = A )
132	130 3 131	syl2anc	|- ( ( ph /\ x e. X ) -> ( F ` x ) = A )
133	132	adantr	|- ( ( ( ph /\ x e. X ) /\ k = 0 ) -> ( F ` x ) = A )
134	129 133	eqtrd	|- ( ( ( ph /\ x e. X ) /\ k = 0 ) -> ( ( C ` k ) ` x ) = A )
135		oveq2	|- ( k = 0 -> ( 0 - k ) = ( 0 - 0 ) )
136		0m0e0	|- ( 0 - 0 ) = 0
137	136	a1i	|- ( k = 0 -> ( 0 - 0 ) = 0 )
138	135 137	eqtrd	|- ( k = 0 -> ( 0 - k ) = 0 )
139	138	fveq2d	|- ( k = 0 -> ( D ` ( 0 - k ) ) = ( D ` 0 ) )
140	139	fveq1d	|- ( k = 0 -> ( ( D ` ( 0 - k ) ) ` x ) = ( ( D ` 0 ) ` x ) )
141	140	adantl	|- ( ( ph /\ k = 0 ) -> ( ( D ` ( 0 - k ) ) ` x ) = ( ( D ` 0 ) ` x ) )
142	141	adantlr	|- ( ( ( ph /\ x e. X ) /\ k = 0 ) -> ( ( D ` ( 0 - k ) ) ` x ) = ( ( D ` 0 ) ` x ) )
143		fveq2	|- ( k = n -> ( ( S Dn G ) ` k ) = ( ( S Dn G ) ` n ) )
144	143	cbvmptv	|- ( k e. ( 0 ... N ) |-> ( ( S Dn G ) ` k ) ) = ( n e. ( 0 ... N ) |-> ( ( S Dn G ) ` n ) )
145	11 144	eqtri	|- D = ( n e. ( 0 ... N ) |-> ( ( S Dn G ) ` n ) )
146	145	fveq1i	|- ( D ` 0 ) = ( ( n e. ( 0 ... N ) |-> ( ( S Dn G ) ` n ) ) ` 0 )
147	146	a1i	|- ( ph -> ( D ` 0 ) = ( ( n e. ( 0 ... N ) |-> ( ( S Dn G ) ` n ) ) ` 0 ) )
148		eqidd	|- ( ph -> ( n e. ( 0 ... N ) |-> ( ( S Dn G ) ` n ) ) = ( n e. ( 0 ... N ) |-> ( ( S Dn G ) ` n ) ) )
149		fveq2	|- ( n = 0 -> ( ( S Dn G ) ` n ) = ( ( S Dn G ) ` 0 ) )
150	149	adantl	|- ( ( ph /\ n = 0 ) -> ( ( S Dn G ) ` n ) = ( ( S Dn G ) ` 0 ) )
151	4 90 92 1	mptelpm	|- ( ph -> ( x e. X |-> B ) e. ( CC ^pm S ) )
152	7 151	eqeltrid	|- ( ph -> G e. ( CC ^pm S ) )
153		dvn0	|- ( ( S C_ CC /\ G e. ( CC ^pm S ) ) -> ( ( S Dn G ) ` 0 ) = G )
154	85 152 153	syl2anc	|- ( ph -> ( ( S Dn G ) ` 0 ) = G )
155	154	adantr	|- ( ( ph /\ n = 0 ) -> ( ( S Dn G ) ` 0 ) = G )
156	150 155	eqtrd	|- ( ( ph /\ n = 0 ) -> ( ( S Dn G ) ` n ) = G )
157	7	a1i	|- ( ph -> G = ( x e. X |-> B ) )
158		mptexg	|- ( X e. ~P S -> ( x e. X |-> B ) e. _V )
159	88 158	syl	|- ( ph -> ( x e. X |-> B ) e. _V )
160	157 159	eqeltrd	|- ( ph -> G e. _V )
161	148 156 117 160	fvmptd	|- ( ph -> ( ( n e. ( 0 ... N ) |-> ( ( S Dn G ) ` n ) ) ` 0 ) = G )
162	147 161	eqtrd	|- ( ph -> ( D ` 0 ) = G )
163	162	fveq1d	|- ( ph -> ( ( D ` 0 ) ` x ) = ( G ` x ) )
164	163	ad2antrr	|- ( ( ( ph /\ x e. X ) /\ k = 0 ) -> ( ( D ` 0 ) ` x ) = ( G ` x ) )
165	157 4	fvmpt2d	|- ( ( ph /\ x e. X ) -> ( G ` x ) = B )
166	165	adantr	|- ( ( ( ph /\ x e. X ) /\ k = 0 ) -> ( G ` x ) = B )
167	142 164 166	3eqtrd	|- ( ( ( ph /\ x e. X ) /\ k = 0 ) -> ( ( D ` ( 0 - k ) ) ` x ) = B )
168	134 167	oveq12d	|- ( ( ( ph /\ x e. X ) /\ k = 0 ) -> ( ( ( C ` k ) ` x ) x. ( ( D ` ( 0 - k ) ) ` x ) ) = ( A x. B ) )
169	109 168	oveq12d	|- ( ( ( ph /\ x e. X ) /\ k = 0 ) -> ( ( 0 _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( 0 - k ) ) ` x ) ) ) = ( 1 x. ( A x. B ) ) )
170	86	mulid2d	|- ( ( ph /\ x e. X ) -> ( 1 x. ( A x. B ) ) = ( A x. B ) )
171	170	adantr	|- ( ( ( ph /\ x e. X ) /\ k = 0 ) -> ( 1 x. ( A x. B ) ) = ( A x. B ) )
172	169 171	eqtrd	|- ( ( ( ph /\ x e. X ) /\ k = 0 ) -> ( ( 0 _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( 0 - k ) ) ` x ) ) ) = ( A x. B ) )
173		0re	|- 0 e. RR
174	173	a1i	|- ( ( ph /\ x e. X ) -> 0 e. RR )
175	101 102 172 174 86	sumsnd	|- ( ( ph /\ x e. X ) -> sum_ k e. { 0 } ( ( 0 _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( 0 - k ) ) ` x ) ) ) = ( A x. B ) )
176	100 175	eqtr2d	|- ( ( ph /\ x e. X ) -> ( A x. B ) = sum_ k e. ( 0 ... 0 ) ( ( 0 _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( 0 - k ) ) ` x ) ) ) )
177	176	mpteq2dva	|- ( ph -> ( x e. X |-> ( A x. B ) ) = ( x e. X |-> sum_ k e. ( 0 ... 0 ) ( ( 0 _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( 0 - k ) ) ` x ) ) ) ) )
178	95 177	eqtrd	|- ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` 0 ) = ( x e. X |-> sum_ k e. ( 0 ... 0 ) ( ( 0 _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( 0 - k ) ) ` x ) ) ) ) )
179	178	a1i	|- ( N e. ( ZZ>= ` 0 ) -> ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` 0 ) = ( x e. X |-> sum_ k e. ( 0 ... 0 ) ( ( 0 _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( 0 - k ) ) ` x ) ) ) ) ) )
180		simp3	|- ( ( i e. ( 0 ..^ N ) /\ ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` i ) = ( x e. X |-> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) ) /\ ph ) -> ph )
181		simp1	|- ( ( i e. ( 0 ..^ N ) /\ ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` i ) = ( x e. X |-> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) ) /\ ph ) -> i e. ( 0 ..^ N ) )
182		simp2	|- ( ( i e. ( 0 ..^ N ) /\ ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` i ) = ( x e. X |-> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) ) /\ ph ) -> ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` i ) = ( x e. X |-> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) ) )
183		pm3.35	|- ( ( ph /\ ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` i ) = ( x e. X |-> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) ) ) -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` i ) = ( x e. X |-> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) )
184	180 182 183	syl2anc	|- ( ( i e. ( 0 ..^ N ) /\ ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` i ) = ( x e. X |-> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) ) /\ ph ) -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` i ) = ( x e. X |-> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) )
185	85	adantr	|- ( ( ph /\ i e. ( 0 ..^ N ) ) -> S C_ CC )
186	93	adantr	|- ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( x e. X |-> ( A x. B ) ) e. ( CC ^pm S ) )
187		elfzonn0	|- ( i e. ( 0 ..^ N ) -> i e. NN0 )
188	187	adantl	|- ( ( ph /\ i e. ( 0 ..^ N ) ) -> i e. NN0 )
189		dvnp1	|- ( ( S C_ CC /\ ( x e. X |-> ( A x. B ) ) e. ( CC ^pm S ) /\ i e. NN0 ) -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` ( i + 1 ) ) = ( S _D ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` i ) ) )
190	185 186 188 189	syl3anc	|- ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` ( i + 1 ) ) = ( S _D ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` i ) ) )
191	190	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` i ) = ( x e. X |-> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) ) -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` ( i + 1 ) ) = ( S _D ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` i ) ) )
192		simpr	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` i ) = ( x e. X |-> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) ) -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` i ) = ( x e. X |-> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) )
193	192	oveq2d	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` i ) = ( x e. X |-> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) ) -> ( S _D ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` i ) ) = ( S _D ( x e. X |-> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) ) )
194		eqid	|- ( ( TopOpen ` CCfld ) |`t S ) = ( ( TopOpen ` CCfld ) |`t S )
195		eqid	|- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
196	1	adantr	|- ( ( ph /\ i e. ( 0 ..^ N ) ) -> S e. { RR , CC } )
197	2	adantr	|- ( ( ph /\ i e. ( 0 ..^ N ) ) -> X e. ( ( TopOpen ` CCfld ) |`t S ) )
198		fzfid	|- ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( 0 ... i ) e. Fin )
199	187	adantr	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> i e. NN0 )
200		elfzelz	|- ( k e. ( 0 ... i ) -> k e. ZZ )
201	200	adantl	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> k e. ZZ )
202	199 201	bccld	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( i _C k ) e. NN0 )
203	202	nn0cnd	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( i _C k ) e. CC )
204	203	adantll	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( i _C k ) e. CC )
205	204	3adant3	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) /\ x e. X ) -> ( i _C k ) e. CC )
206		simpll	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ph )
207		0zd	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> 0 e. ZZ )
208		elfzoel2	|- ( i e. ( 0 ..^ N ) -> N e. ZZ )
209	208	adantr	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> N e. ZZ )
210	207 209 201	3jca	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( 0 e. ZZ /\ N e. ZZ /\ k e. ZZ ) )
211		elfzle1	|- ( k e. ( 0 ... i ) -> 0 <_ k )
212	211	adantl	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> 0 <_ k )
213	201	zred	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> k e. RR )
214	208	zred	|- ( i e. ( 0 ..^ N ) -> N e. RR )
215	214	adantr	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> N e. RR )
216	187	nn0red	|- ( i e. ( 0 ..^ N ) -> i e. RR )
217	216	adantr	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> i e. RR )
218		elfzle2	|- ( k e. ( 0 ... i ) -> k <_ i )
219	218	adantl	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> k <_ i )
220		elfzolt2	|- ( i e. ( 0 ..^ N ) -> i < N )
221	220	adantr	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> i < N )
222	213 217 215 219 221	lelttrd	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> k < N )
223	213 215 222	ltled	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> k <_ N )
224	210 212 223	jca32	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( ( 0 e. ZZ /\ N e. ZZ /\ k e. ZZ ) /\ ( 0 <_ k /\ k <_ N ) ) )
225		elfz2	|- ( k e. ( 0 ... N ) <-> ( ( 0 e. ZZ /\ N e. ZZ /\ k e. ZZ ) /\ ( 0 <_ k /\ k <_ N ) ) )
226	224 225	sylibr	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> k e. ( 0 ... N ) )
227	226	adantll	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> k e. ( 0 ... N ) )
228	10	a1i	|- ( ph -> C = ( k e. ( 0 ... N ) |-> ( ( S Dn F ) ` k ) ) )
229		fvexd	|- ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( S Dn F ) ` k ) e. _V )
230	228 229	fvmpt2d	|- ( ( ph /\ k e. ( 0 ... N ) ) -> ( C ` k ) = ( ( S Dn F ) ` k ) )
231	230	feq1d	|- ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( C ` k ) : X --> CC <-> ( ( S Dn F ) ` k ) : X --> CC ) )
232	8 231	mpbird	|- ( ( ph /\ k e. ( 0 ... N ) ) -> ( C ` k ) : X --> CC )
233	206 227 232	syl2anc	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( C ` k ) : X --> CC )
234	233	3adant3	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) /\ x e. X ) -> ( C ` k ) : X --> CC )
235		simp3	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) /\ x e. X ) -> x e. X )
236	234 235	ffvelrnd	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) /\ x e. X ) -> ( ( C ` k ) ` x ) e. CC )
237	187	nn0zd	|- ( i e. ( 0 ..^ N ) -> i e. ZZ )
238	237	adantr	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> i e. ZZ )
239	238 201	zsubcld	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( i - k ) e. ZZ )
240	207 209 239	3jca	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( 0 e. ZZ /\ N e. ZZ /\ ( i - k ) e. ZZ ) )
241		elfzel2	|- ( k e. ( 0 ... i ) -> i e. ZZ )
242	241	zred	|- ( k e. ( 0 ... i ) -> i e. RR )
243	200	zred	|- ( k e. ( 0 ... i ) -> k e. RR )
244	242 243	subge0d	|- ( k e. ( 0 ... i ) -> ( 0 <_ ( i - k ) <-> k <_ i ) )
245	218 244	mpbird	|- ( k e. ( 0 ... i ) -> 0 <_ ( i - k ) )
246	245	adantl	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> 0 <_ ( i - k ) )
247	217 213	resubcld	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( i - k ) e. RR )
248	215 213	resubcld	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( N - k ) e. RR )
249	173	a1i	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> 0 e. RR )
250	215 249	jca	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( N e. RR /\ 0 e. RR ) )
251		resubcl	|- ( ( N e. RR /\ 0 e. RR ) -> ( N - 0 ) e. RR )
252	250 251	syl	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( N - 0 ) e. RR )
253	217 215 213 221	ltsub1dd	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( i - k ) < ( N - k ) )
254	249 213 215 212	lesub2dd	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( N - k ) <_ ( N - 0 ) )
255	247 248 252 253 254	ltletrd	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( i - k ) < ( N - 0 ) )
256	214	recnd	|- ( i e. ( 0 ..^ N ) -> N e. CC )
257	256	subid1d	|- ( i e. ( 0 ..^ N ) -> ( N - 0 ) = N )
258	257	adantr	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( N - 0 ) = N )
259	255 258	breqtrd	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( i - k ) < N )
260	247 215 259	ltled	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( i - k ) <_ N )
261	240 246 260	jca32	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( ( 0 e. ZZ /\ N e. ZZ /\ ( i - k ) e. ZZ ) /\ ( 0 <_ ( i - k ) /\ ( i - k ) <_ N ) ) )
262		elfz2	|- ( ( i - k ) e. ( 0 ... N ) <-> ( ( 0 e. ZZ /\ N e. ZZ /\ ( i - k ) e. ZZ ) /\ ( 0 <_ ( i - k ) /\ ( i - k ) <_ N ) ) )
263	261 262	sylibr	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( i - k ) e. ( 0 ... N ) )
264	263	adantll	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( i - k ) e. ( 0 ... N ) )
265		ovex	|- ( i - k ) e. _V
266		eleq1	|- ( j = ( i - k ) -> ( j e. ( 0 ... N ) <-> ( i - k ) e. ( 0 ... N ) ) )
267	266	anbi2d	|- ( j = ( i - k ) -> ( ( ph /\ j e. ( 0 ... N ) ) <-> ( ph /\ ( i - k ) e. ( 0 ... N ) ) ) )
268		fveq2	|- ( j = ( i - k ) -> ( ( S Dn G ) ` j ) = ( ( S Dn G ) ` ( i - k ) ) )
269	268	feq1d	|- ( j = ( i - k ) -> ( ( ( S Dn G ) ` j ) : X --> CC <-> ( ( S Dn G ) ` ( i - k ) ) : X --> CC ) )
270	267 269	imbi12d	|- ( j = ( i - k ) -> ( ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( S Dn G ) ` j ) : X --> CC ) <-> ( ( ph /\ ( i - k ) e. ( 0 ... N ) ) -> ( ( S Dn G ) ` ( i - k ) ) : X --> CC ) ) )
271		nfv	|- F/ k ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( S Dn G ) ` j ) : X --> CC )
272		eleq1	|- ( k = j -> ( k e. ( 0 ... N ) <-> j e. ( 0 ... N ) ) )
273	272	anbi2d	|- ( k = j -> ( ( ph /\ k e. ( 0 ... N ) ) <-> ( ph /\ j e. ( 0 ... N ) ) ) )
274		fveq2	|- ( k = j -> ( ( S Dn G ) ` k ) = ( ( S Dn G ) ` j ) )
275	274	feq1d	|- ( k = j -> ( ( ( S Dn G ) ` k ) : X --> CC <-> ( ( S Dn G ) ` j ) : X --> CC ) )
276	273 275	imbi12d	|- ( k = j -> ( ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( S Dn G ) ` k ) : X --> CC ) <-> ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( S Dn G ) ` j ) : X --> CC ) ) )
277	271 276 9	chvarfv	|- ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( S Dn G ) ` j ) : X --> CC )
278	265 270 277	vtocl	|- ( ( ph /\ ( i - k ) e. ( 0 ... N ) ) -> ( ( S Dn G ) ` ( i - k ) ) : X --> CC )
279	206 264 278	syl2anc	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( S Dn G ) ` ( i - k ) ) : X --> CC )
280		fveq2	|- ( n = ( i - k ) -> ( ( S Dn G ) ` n ) = ( ( S Dn G ) ` ( i - k ) ) )
281		fvexd	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( ( S Dn G ) ` ( i - k ) ) e. _V )
282	145 280 263 281	fvmptd3	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( D ` ( i - k ) ) = ( ( S Dn G ) ` ( i - k ) ) )
283	282	adantll	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( D ` ( i - k ) ) = ( ( S Dn G ) ` ( i - k ) ) )
284	283	feq1d	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( D ` ( i - k ) ) : X --> CC <-> ( ( S Dn G ) ` ( i - k ) ) : X --> CC ) )
285	279 284	mpbird	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( D ` ( i - k ) ) : X --> CC )
286	285	3adant3	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) /\ x e. X ) -> ( D ` ( i - k ) ) : X --> CC )
287	286 235	ffvelrnd	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) /\ x e. X ) -> ( ( D ` ( i - k ) ) ` x ) e. CC )
288	236 287	mulcld	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) /\ x e. X ) -> ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) e. CC )
289	205 288	mulcld	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) /\ x e. X ) -> ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) e. CC )
290	205	3expa	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( i _C k ) e. CC )
291	238	peano2zd	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( i + 1 ) e. ZZ )
292	291 201	zsubcld	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( ( i + 1 ) - k ) e. ZZ )
293	207 209 292	3jca	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( 0 e. ZZ /\ N e. ZZ /\ ( ( i + 1 ) - k ) e. ZZ ) )
294		peano2re	|- ( i e. RR -> ( i + 1 ) e. RR )
295	242 294	syl	|- ( k e. ( 0 ... i ) -> ( i + 1 ) e. RR )
296		peano2re	|- ( k e. RR -> ( k + 1 ) e. RR )
297	243 296	syl	|- ( k e. ( 0 ... i ) -> ( k + 1 ) e. RR )
298	243	ltp1d	|- ( k e. ( 0 ... i ) -> k < ( k + 1 ) )
299		1red	|- ( k e. ( 0 ... i ) -> 1 e. RR )
300	243 242 299 218	leadd1dd	|- ( k e. ( 0 ... i ) -> ( k + 1 ) <_ ( i + 1 ) )
301	243 297 295 298 300	ltletrd	|- ( k e. ( 0 ... i ) -> k < ( i + 1 ) )
302	243 295 301	ltled	|- ( k e. ( 0 ... i ) -> k <_ ( i + 1 ) )
303	302	adantl	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> k <_ ( i + 1 ) )
304	217 294	syl	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( i + 1 ) e. RR )
305	304 213	subge0d	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( 0 <_ ( ( i + 1 ) - k ) <-> k <_ ( i + 1 ) ) )
306	303 305	mpbird	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> 0 <_ ( ( i + 1 ) - k ) )
307	304 213	resubcld	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( ( i + 1 ) - k ) e. RR )
308		elfzop1le2	|- ( i e. ( 0 ..^ N ) -> ( i + 1 ) <_ N )
309	308	adantr	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( i + 1 ) <_ N )
310	304 215 213 309	lesub1dd	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( ( i + 1 ) - k ) <_ ( N - k ) )
311	254 258	breqtrd	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( N - k ) <_ N )
312	307 248 215 310 311	letrd	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( ( i + 1 ) - k ) <_ N )
313	293 306 312	jca32	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( ( 0 e. ZZ /\ N e. ZZ /\ ( ( i + 1 ) - k ) e. ZZ ) /\ ( 0 <_ ( ( i + 1 ) - k ) /\ ( ( i + 1 ) - k ) <_ N ) ) )
314		elfz2	|- ( ( ( i + 1 ) - k ) e. ( 0 ... N ) <-> ( ( 0 e. ZZ /\ N e. ZZ /\ ( ( i + 1 ) - k ) e. ZZ ) /\ ( 0 <_ ( ( i + 1 ) - k ) /\ ( ( i + 1 ) - k ) <_ N ) ) )
315	313 314	sylibr	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( ( i + 1 ) - k ) e. ( 0 ... N ) )
316	315	adantll	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( i + 1 ) - k ) e. ( 0 ... N ) )
317		ovex	|- ( ( i + 1 ) - k ) e. _V
318		eleq1	|- ( j = ( ( i + 1 ) - k ) -> ( j e. ( 0 ... N ) <-> ( ( i + 1 ) - k ) e. ( 0 ... N ) ) )
319	318	anbi2d	|- ( j = ( ( i + 1 ) - k ) -> ( ( ph /\ j e. ( 0 ... N ) ) <-> ( ph /\ ( ( i + 1 ) - k ) e. ( 0 ... N ) ) ) )
320		fveq2	|- ( j = ( ( i + 1 ) - k ) -> ( ( S Dn G ) ` j ) = ( ( S Dn G ) ` ( ( i + 1 ) - k ) ) )
321	320	feq1d	|- ( j = ( ( i + 1 ) - k ) -> ( ( ( S Dn G ) ` j ) : X --> CC <-> ( ( S Dn G ) ` ( ( i + 1 ) - k ) ) : X --> CC ) )
322	319 321	imbi12d	|- ( j = ( ( i + 1 ) - k ) -> ( ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( S Dn G ) ` j ) : X --> CC ) <-> ( ( ph /\ ( ( i + 1 ) - k ) e. ( 0 ... N ) ) -> ( ( S Dn G ) ` ( ( i + 1 ) - k ) ) : X --> CC ) ) )
323	317 322 277	vtocl	|- ( ( ph /\ ( ( i + 1 ) - k ) e. ( 0 ... N ) ) -> ( ( S Dn G ) ` ( ( i + 1 ) - k ) ) : X --> CC )
324	206 316 323	syl2anc	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( S Dn G ) ` ( ( i + 1 ) - k ) ) : X --> CC )
325	145	a1i	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> D = ( n e. ( 0 ... N ) |-> ( ( S Dn G ) ` n ) ) )
326		simpr	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ n = ( ( i + 1 ) - k ) ) -> n = ( ( i + 1 ) - k ) )
327	326	fveq2d	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ n = ( ( i + 1 ) - k ) ) -> ( ( S Dn G ) ` n ) = ( ( S Dn G ) ` ( ( i + 1 ) - k ) ) )
328		fvexd	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( S Dn G ) ` ( ( i + 1 ) - k ) ) e. _V )
329	325 327 316 328	fvmptd	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( D ` ( ( i + 1 ) - k ) ) = ( ( S Dn G ) ` ( ( i + 1 ) - k ) ) )
330	329	feq1d	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( D ` ( ( i + 1 ) - k ) ) : X --> CC <-> ( ( S Dn G ) ` ( ( i + 1 ) - k ) ) : X --> CC ) )
331	324 330	mpbird	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( D ` ( ( i + 1 ) - k ) ) : X --> CC )
332	331	ffvelrnda	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( ( D ` ( ( i + 1 ) - k ) ) ` x ) e. CC )
333	236	3expa	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( ( C ` k ) ` x ) e. CC )
334	332 333	mulcomd	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( ( ( D ` ( ( i + 1 ) - k ) ) ` x ) x. ( ( C ` k ) ` x ) ) = ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) )
335	334	oveq2d	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( D ` ( ( i + 1 ) - k ) ) ` x ) x. ( ( C ` k ) ` x ) ) ) = ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) )
336	201	peano2zd	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( k + 1 ) e. ZZ )
337	207 209 336	3jca	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( 0 e. ZZ /\ N e. ZZ /\ ( k + 1 ) e. ZZ ) )
338	173	a1i	|- ( k e. ( 0 ... i ) -> 0 e. RR )
339	338 243 297 211 298	lelttrd	|- ( k e. ( 0 ... i ) -> 0 < ( k + 1 ) )
340	338 297 339	ltled	|- ( k e. ( 0 ... i ) -> 0 <_ ( k + 1 ) )
341	340	adantl	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> 0 <_ ( k + 1 ) )
342	213 296	syl	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( k + 1 ) e. RR )
343	300	adantl	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( k + 1 ) <_ ( i + 1 ) )
344	342 304 215 343 309	letrd	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( k + 1 ) <_ N )
345	337 341 344	jca32	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( ( 0 e. ZZ /\ N e. ZZ /\ ( k + 1 ) e. ZZ ) /\ ( 0 <_ ( k + 1 ) /\ ( k + 1 ) <_ N ) ) )
346		elfz2	|- ( ( k + 1 ) e. ( 0 ... N ) <-> ( ( 0 e. ZZ /\ N e. ZZ /\ ( k + 1 ) e. ZZ ) /\ ( 0 <_ ( k + 1 ) /\ ( k + 1 ) <_ N ) ) )
347	345 346	sylibr	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( k + 1 ) e. ( 0 ... N ) )
348	347	adantll	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( k + 1 ) e. ( 0 ... N ) )
349		ovex	|- ( k + 1 ) e. _V
350		eleq1	|- ( j = ( k + 1 ) -> ( j e. ( 0 ... N ) <-> ( k + 1 ) e. ( 0 ... N ) ) )
351	350	anbi2d	|- ( j = ( k + 1 ) -> ( ( ph /\ j e. ( 0 ... N ) ) <-> ( ph /\ ( k + 1 ) e. ( 0 ... N ) ) ) )
352		fveq2	|- ( j = ( k + 1 ) -> ( C ` j ) = ( C ` ( k + 1 ) ) )
353	352	feq1d	|- ( j = ( k + 1 ) -> ( ( C ` j ) : X --> CC <-> ( C ` ( k + 1 ) ) : X --> CC ) )
354	351 353	imbi12d	|- ( j = ( k + 1 ) -> ( ( ( ph /\ j e. ( 0 ... N ) ) -> ( C ` j ) : X --> CC ) <-> ( ( ph /\ ( k + 1 ) e. ( 0 ... N ) ) -> ( C ` ( k + 1 ) ) : X --> CC ) ) )
355		nfv	|- F/ k ( ph /\ j e. ( 0 ... N ) )
356		nfmpt1	|- F/_ k ( k e. ( 0 ... N ) |-> ( ( S Dn F ) ` k ) )
357	10 356	nfcxfr	|- F/_ k C
358		nfcv	|- F/_ k j
359	357 358	nffv	|- F/_ k ( C ` j )
360		nfcv	|- F/_ k X
361		nfcv	|- F/_ k CC
362	359 360 361	nff	|- F/ k ( C ` j ) : X --> CC
363	355 362	nfim	|- F/ k ( ( ph /\ j e. ( 0 ... N ) ) -> ( C ` j ) : X --> CC )
364		fveq2	|- ( k = j -> ( C ` k ) = ( C ` j ) )
365	364	feq1d	|- ( k = j -> ( ( C ` k ) : X --> CC <-> ( C ` j ) : X --> CC ) )
366	273 365	imbi12d	|- ( k = j -> ( ( ( ph /\ k e. ( 0 ... N ) ) -> ( C ` k ) : X --> CC ) <-> ( ( ph /\ j e. ( 0 ... N ) ) -> ( C ` j ) : X --> CC ) ) )
367	363 366 232	chvarfv	|- ( ( ph /\ j e. ( 0 ... N ) ) -> ( C ` j ) : X --> CC )
368	349 354 367	vtocl	|- ( ( ph /\ ( k + 1 ) e. ( 0 ... N ) ) -> ( C ` ( k + 1 ) ) : X --> CC )
369	206 348 368	syl2anc	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( C ` ( k + 1 ) ) : X --> CC )
370	369	ffvelrnda	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( ( C ` ( k + 1 ) ) ` x ) e. CC )
371	287	3expa	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( ( D ` ( i - k ) ) ` x ) e. CC )
372	370 371	mulcld	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) e. CC )
373	332 333	mulcld	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( ( ( D ` ( ( i + 1 ) - k ) ) ` x ) x. ( ( C ` k ) ` x ) ) e. CC )
374	372 373	addcld	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( D ` ( ( i + 1 ) - k ) ) ` x ) x. ( ( C ` k ) ` x ) ) ) e. CC )
375	335 374	eqeltrrd	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) e. CC )
376	290 375	mulcld	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( ( i _C k ) x. ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) e. CC )
377	376	3impa	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) /\ x e. X ) -> ( ( i _C k ) x. ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) e. CC )
378	206 1	syl	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> S e. { RR , CC } )
379	173	a1i	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> 0 e. RR )
380	206 2	syl	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> X e. ( ( TopOpen ` CCfld ) |`t S ) )
381	378 380 204	dvmptconst	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( S _D ( x e. X |-> ( i _C k ) ) ) = ( x e. X |-> 0 ) )
382	288	3expa	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) e. CC )
383	206 227 230	syl2anc	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( C ` k ) = ( ( S Dn F ) ` k ) )
384	383	eqcomd	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( S Dn F ) ` k ) = ( C ` k ) )
385	233	feqmptd	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( C ` k ) = ( x e. X |-> ( ( C ` k ) ` x ) ) )
386	384 385	eqtr2d	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( x e. X |-> ( ( C ` k ) ` x ) ) = ( ( S Dn F ) ` k ) )
387	386	oveq2d	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( S _D ( x e. X |-> ( ( C ` k ) ` x ) ) ) = ( S _D ( ( S Dn F ) ` k ) ) )
388	378 84	syl	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> S C_ CC )
389	206 123	syl	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> F e. ( CC ^pm S ) )
390		elfznn0	|- ( k e. ( 0 ... i ) -> k e. NN0 )
391	390	adantl	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> k e. NN0 )
392		dvnp1	|- ( ( S C_ CC /\ F e. ( CC ^pm S ) /\ k e. NN0 ) -> ( ( S Dn F ) ` ( k + 1 ) ) = ( S _D ( ( S Dn F ) ` k ) ) )
393	388 389 391 392	syl3anc	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( S Dn F ) ` ( k + 1 ) ) = ( S _D ( ( S Dn F ) ` k ) ) )
394	393	eqcomd	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( S _D ( ( S Dn F ) ` k ) ) = ( ( S Dn F ) ` ( k + 1 ) ) )
395		fveq2	|- ( n = ( k + 1 ) -> ( ( S Dn F ) ` n ) = ( ( S Dn F ) ` ( k + 1 ) ) )
396		fvexd	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( S Dn F ) ` ( k + 1 ) ) e. _V )
397	114 395 348 396	fvmptd3	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( C ` ( k + 1 ) ) = ( ( S Dn F ) ` ( k + 1 ) ) )
398	397	eqcomd	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( S Dn F ) ` ( k + 1 ) ) = ( C ` ( k + 1 ) ) )
399	369	feqmptd	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( C ` ( k + 1 ) ) = ( x e. X |-> ( ( C ` ( k + 1 ) ) ` x ) ) )
400	398 399	eqtrd	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( S Dn F ) ` ( k + 1 ) ) = ( x e. X |-> ( ( C ` ( k + 1 ) ) ` x ) ) )
401	387 394 400	3eqtrd	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( S _D ( x e. X |-> ( ( C ` k ) ` x ) ) ) = ( x e. X |-> ( ( C ` ( k + 1 ) ) ` x ) ) )
402	283	eqcomd	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( S Dn G ) ` ( i - k ) ) = ( D ` ( i - k ) ) )
403	285	feqmptd	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( D ` ( i - k ) ) = ( x e. X |-> ( ( D ` ( i - k ) ) ` x ) ) )
404	402 403	eqtr2d	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( x e. X |-> ( ( D ` ( i - k ) ) ` x ) ) = ( ( S Dn G ) ` ( i - k ) ) )
405	404	oveq2d	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( S _D ( x e. X |-> ( ( D ` ( i - k ) ) ` x ) ) ) = ( S _D ( ( S Dn G ) ` ( i - k ) ) ) )
406	206 152	syl	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> G e. ( CC ^pm S ) )
407		fznn0sub	|- ( k e. ( 0 ... i ) -> ( i - k ) e. NN0 )
408	407	adantl	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( i - k ) e. NN0 )
409		dvnp1	|- ( ( S C_ CC /\ G e. ( CC ^pm S ) /\ ( i - k ) e. NN0 ) -> ( ( S Dn G ) ` ( ( i - k ) + 1 ) ) = ( S _D ( ( S Dn G ) ` ( i - k ) ) ) )
410	388 406 408 409	syl3anc	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( S Dn G ) ` ( ( i - k ) + 1 ) ) = ( S _D ( ( S Dn G ) ` ( i - k ) ) ) )
411	410	eqcomd	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( S _D ( ( S Dn G ) ` ( i - k ) ) ) = ( ( S Dn G ) ` ( ( i - k ) + 1 ) ) )
412	217	recnd	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> i e. CC )
413		1cnd	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> 1 e. CC )
414	213	recnd	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> k e. CC )
415	412 413 414	addsubd	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( ( i + 1 ) - k ) = ( ( i - k ) + 1 ) )
416	415	eqcomd	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( ( i - k ) + 1 ) = ( ( i + 1 ) - k ) )
417	416	fveq2d	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( ( S Dn G ) ` ( ( i - k ) + 1 ) ) = ( ( S Dn G ) ` ( ( i + 1 ) - k ) ) )
418	417	adantll	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( S Dn G ) ` ( ( i - k ) + 1 ) ) = ( ( S Dn G ) ` ( ( i + 1 ) - k ) ) )
419	329	eqcomd	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( S Dn G ) ` ( ( i + 1 ) - k ) ) = ( D ` ( ( i + 1 ) - k ) ) )
420	331	feqmptd	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( D ` ( ( i + 1 ) - k ) ) = ( x e. X |-> ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) )
421	418 419 420	3eqtrd	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( S Dn G ) ` ( ( i - k ) + 1 ) ) = ( x e. X |-> ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) )
422	405 411 421	3eqtrd	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( S _D ( x e. X |-> ( ( D ` ( i - k ) ) ` x ) ) ) = ( x e. X |-> ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) )
423	378 333 370 401 371 332 422	dvmptmul	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( S _D ( x e. X |-> ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) = ( x e. X |-> ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( D ` ( ( i + 1 ) - k ) ) ` x ) x. ( ( C ` k ) ` x ) ) ) ) )
424	378 290 379 381 382 374 423	dvmptmul	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( S _D ( x e. X |-> ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) ) = ( x e. X |-> ( ( 0 x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) + ( ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( D ` ( ( i + 1 ) - k ) ) ` x ) x. ( ( C ` k ) ` x ) ) ) x. ( i _C k ) ) ) ) )
425	382	mul02d	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( 0 x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) = 0 )
426	335	oveq1d	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( D ` ( ( i + 1 ) - k ) ) ` x ) x. ( ( C ` k ) ` x ) ) ) x. ( i _C k ) ) = ( ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) x. ( i _C k ) ) )
427	375 290	mulcomd	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) x. ( i _C k ) ) = ( ( i _C k ) x. ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
428	426 427	eqtrd	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( D ` ( ( i + 1 ) - k ) ) ` x ) x. ( ( C ` k ) ` x ) ) ) x. ( i _C k ) ) = ( ( i _C k ) x. ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
429	425 428	oveq12d	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( ( 0 x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) + ( ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( D ` ( ( i + 1 ) - k ) ) ` x ) x. ( ( C ` k ) ` x ) ) ) x. ( i _C k ) ) ) = ( 0 + ( ( i _C k ) x. ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) ) )
430	376	addid2d	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( 0 + ( ( i _C k ) x. ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) ) = ( ( i _C k ) x. ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
431	429 430	eqtrd	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( ( 0 x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) + ( ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( D ` ( ( i + 1 ) - k ) ) ` x ) x. ( ( C ` k ) ` x ) ) ) x. ( i _C k ) ) ) = ( ( i _C k ) x. ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
432	431	mpteq2dva	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( x e. X |-> ( ( 0 x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) + ( ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( D ` ( ( i + 1 ) - k ) ) ` x ) x. ( ( C ` k ) ` x ) ) ) x. ( i _C k ) ) ) ) = ( x e. X |-> ( ( i _C k ) x. ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) ) )
433	424 432	eqtrd	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( S _D ( x e. X |-> ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) ) = ( x e. X |-> ( ( i _C k ) x. ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) ) )
434	194 195 196 197 198 289 377 433	dvmptfsum	|- ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( S _D ( x e. X |-> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) ) = ( x e. X |-> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) ) )
435	204	adantlr	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... i ) ) -> ( i _C k ) e. CC )
436	372	an32s	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... i ) ) -> ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) e. CC )
437		anass	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) <-> ( ( ph /\ i e. ( 0 ..^ N ) ) /\ ( k e. ( 0 ... i ) /\ x e. X ) ) )
438		ancom	|- ( ( k e. ( 0 ... i ) /\ x e. X ) <-> ( x e. X /\ k e. ( 0 ... i ) ) )
439	438	anbi2i	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ ( k e. ( 0 ... i ) /\ x e. X ) ) <-> ( ( ph /\ i e. ( 0 ..^ N ) ) /\ ( x e. X /\ k e. ( 0 ... i ) ) ) )
440		anass	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... i ) ) <-> ( ( ph /\ i e. ( 0 ..^ N ) ) /\ ( x e. X /\ k e. ( 0 ... i ) ) ) )
441	440	bicomi	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ ( x e. X /\ k e. ( 0 ... i ) ) ) <-> ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... i ) ) )
442	439 441	bitri	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ ( k e. ( 0 ... i ) /\ x e. X ) ) <-> ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... i ) ) )
443	437 442	bitri	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) <-> ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... i ) ) )
444	443	imbi1i	|- ( ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( ( C ` k ) ` x ) e. CC ) <-> ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... i ) ) -> ( ( C ` k ) ` x ) e. CC ) )
445	333 444	mpbi	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... i ) ) -> ( ( C ` k ) ` x ) e. CC )
446	443	imbi1i	|- ( ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( ( D ` ( ( i + 1 ) - k ) ) ` x ) e. CC ) <-> ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... i ) ) -> ( ( D ` ( ( i + 1 ) - k ) ) ` x ) e. CC ) )
447	332 446	mpbi	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... i ) ) -> ( ( D ` ( ( i + 1 ) - k ) ) ` x ) e. CC )
448	445 447	mulcld	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... i ) ) -> ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) e. CC )
449	435 436 448	adddid	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... i ) ) -> ( ( i _C k ) x. ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) = ( ( ( i _C k ) x. ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) + ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
450	449	sumeq2dv	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) = sum_ k e. ( 0 ... i ) ( ( ( i _C k ) x. ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) + ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
451	198	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( 0 ... i ) e. Fin )
452	435 436	mulcld	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... i ) ) -> ( ( i _C k ) x. ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) e. CC )
453	435 448	mulcld	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... i ) ) -> ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) e. CC )
454	451 452 453	fsumadd	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> sum_ k e. ( 0 ... i ) ( ( ( i _C k ) x. ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) + ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) = ( sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) + sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
455		oveq2	|- ( k = h -> ( i _C k ) = ( i _C h ) )
456		fvoveq1	|- ( k = h -> ( C ` ( k + 1 ) ) = ( C ` ( h + 1 ) ) )
457	456	fveq1d	|- ( k = h -> ( ( C ` ( k + 1 ) ) ` x ) = ( ( C ` ( h + 1 ) ) ` x ) )
458		oveq2	|- ( k = h -> ( i - k ) = ( i - h ) )
459	458	fveq2d	|- ( k = h -> ( D ` ( i - k ) ) = ( D ` ( i - h ) ) )
460	459	fveq1d	|- ( k = h -> ( ( D ` ( i - k ) ) ` x ) = ( ( D ` ( i - h ) ) ` x ) )
461	457 460	oveq12d	|- ( k = h -> ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) = ( ( ( C ` ( h + 1 ) ) ` x ) x. ( ( D ` ( i - h ) ) ` x ) ) )
462	455 461	oveq12d	|- ( k = h -> ( ( i _C k ) x. ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) = ( ( i _C h ) x. ( ( ( C ` ( h + 1 ) ) ` x ) x. ( ( D ` ( i - h ) ) ` x ) ) ) )
463		nfcv	|- F/_ h ( 0 ... i )
464		nfcv	|- F/_ k ( 0 ... i )
465		nfcv	|- F/_ h ( ( i _C k ) x. ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) )
466		nfcv	|- F/_ k ( i _C h )
467		nfcv	|- F/_ k x.
468		nfcv	|- F/_ k ( h + 1 )
469	357 468	nffv	|- F/_ k ( C ` ( h + 1 ) )
470		nfcv	|- F/_ k x
471	469 470	nffv	|- F/_ k ( ( C ` ( h + 1 ) ) ` x )
472		nfmpt1	|- F/_ k ( k e. ( 0 ... N ) |-> ( ( S Dn G ) ` k ) )
473	11 472	nfcxfr	|- F/_ k D
474		nfcv	|- F/_ k ( i - h )
475	473 474	nffv	|- F/_ k ( D ` ( i - h ) )
476	475 470	nffv	|- F/_ k ( ( D ` ( i - h ) ) ` x )
477	471 467 476	nfov	|- F/_ k ( ( ( C ` ( h + 1 ) ) ` x ) x. ( ( D ` ( i - h ) ) ` x ) )
478	466 467 477	nfov	|- F/_ k ( ( i _C h ) x. ( ( ( C ` ( h + 1 ) ) ` x ) x. ( ( D ` ( i - h ) ) ` x ) ) )
479	462 463 464 465 478	cbvsum	|- sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) = sum_ h e. ( 0 ... i ) ( ( i _C h ) x. ( ( ( C ` ( h + 1 ) ) ` x ) x. ( ( D ` ( i - h ) ) ` x ) ) )
480	479	a1i	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) = sum_ h e. ( 0 ... i ) ( ( i _C h ) x. ( ( ( C ` ( h + 1 ) ) ` x ) x. ( ( D ` ( i - h ) ) ` x ) ) ) )
481		1zzd	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> 1 e. ZZ )
482	96	a1i	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> 0 e. ZZ )
483	237	ad2antlr	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> i e. ZZ )
484		nfv	|- F/ k ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X )
485		nfcv	|- F/_ k h
486	485 464	nfel	|- F/ k h e. ( 0 ... i )
487	484 486	nfan	|- F/ k ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ h e. ( 0 ... i ) )
488	478 361	nfel	|- F/ k ( ( i _C h ) x. ( ( ( C ` ( h + 1 ) ) ` x ) x. ( ( D ` ( i - h ) ) ` x ) ) ) e. CC
489	487 488	nfim	|- F/ k ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ h e. ( 0 ... i ) ) -> ( ( i _C h ) x. ( ( ( C ` ( h + 1 ) ) ` x ) x. ( ( D ` ( i - h ) ) ` x ) ) ) e. CC )
490		eleq1	|- ( k = h -> ( k e. ( 0 ... i ) <-> h e. ( 0 ... i ) ) )
491	490	anbi2d	|- ( k = h -> ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... i ) ) <-> ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ h e. ( 0 ... i ) ) ) )
492	462	eleq1d	|- ( k = h -> ( ( ( i _C k ) x. ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) e. CC <-> ( ( i _C h ) x. ( ( ( C ` ( h + 1 ) ) ` x ) x. ( ( D ` ( i - h ) ) ` x ) ) ) e. CC ) )
493	491 492	imbi12d	|- ( k = h -> ( ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... i ) ) -> ( ( i _C k ) x. ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) e. CC ) <-> ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ h e. ( 0 ... i ) ) -> ( ( i _C h ) x. ( ( ( C ` ( h + 1 ) ) ` x ) x. ( ( D ` ( i - h ) ) ` x ) ) ) e. CC ) ) )
494	489 493 452	chvarfv	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ h e. ( 0 ... i ) ) -> ( ( i _C h ) x. ( ( ( C ` ( h + 1 ) ) ` x ) x. ( ( D ` ( i - h ) ) ` x ) ) ) e. CC )
495		oveq2	|- ( h = ( j - 1 ) -> ( i _C h ) = ( i _C ( j - 1 ) ) )
496		fvoveq1	|- ( h = ( j - 1 ) -> ( C ` ( h + 1 ) ) = ( C ` ( ( j - 1 ) + 1 ) ) )
497	496	fveq1d	|- ( h = ( j - 1 ) -> ( ( C ` ( h + 1 ) ) ` x ) = ( ( C ` ( ( j - 1 ) + 1 ) ) ` x ) )
498		oveq2	|- ( h = ( j - 1 ) -> ( i - h ) = ( i - ( j - 1 ) ) )
499	498	fveq2d	|- ( h = ( j - 1 ) -> ( D ` ( i - h ) ) = ( D ` ( i - ( j - 1 ) ) ) )
500	499	fveq1d	|- ( h = ( j - 1 ) -> ( ( D ` ( i - h ) ) ` x ) = ( ( D ` ( i - ( j - 1 ) ) ) ` x ) )
501	497 500	oveq12d	|- ( h = ( j - 1 ) -> ( ( ( C ` ( h + 1 ) ) ` x ) x. ( ( D ` ( i - h ) ) ` x ) ) = ( ( ( C ` ( ( j - 1 ) + 1 ) ) ` x ) x. ( ( D ` ( i - ( j - 1 ) ) ) ` x ) ) )
502	495 501	oveq12d	|- ( h = ( j - 1 ) -> ( ( i _C h ) x. ( ( ( C ` ( h + 1 ) ) ` x ) x. ( ( D ` ( i - h ) ) ` x ) ) ) = ( ( i _C ( j - 1 ) ) x. ( ( ( C ` ( ( j - 1 ) + 1 ) ) ` x ) x. ( ( D ` ( i - ( j - 1 ) ) ) ` x ) ) ) )
503	481 482 483 494 502	fsumshft	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> sum_ h e. ( 0 ... i ) ( ( i _C h ) x. ( ( ( C ` ( h + 1 ) ) ` x ) x. ( ( D ` ( i - h ) ) ` x ) ) ) = sum_ j e. ( ( 0 + 1 ) ... ( i + 1 ) ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` ( ( j - 1 ) + 1 ) ) ` x ) x. ( ( D ` ( i - ( j - 1 ) ) ) ` x ) ) ) )
504	480 503	eqtrd	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) = sum_ j e. ( ( 0 + 1 ) ... ( i + 1 ) ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` ( ( j - 1 ) + 1 ) ) ` x ) x. ( ( D ` ( i - ( j - 1 ) ) ) ` x ) ) ) )
505		0p1e1	|- ( 0 + 1 ) = 1
506	505	oveq1i	|- ( ( 0 + 1 ) ... ( i + 1 ) ) = ( 1 ... ( i + 1 ) )
507	506	sumeq1i	|- sum_ j e. ( ( 0 + 1 ) ... ( i + 1 ) ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` ( ( j - 1 ) + 1 ) ) ` x ) x. ( ( D ` ( i - ( j - 1 ) ) ) ` x ) ) ) = sum_ j e. ( 1 ... ( i + 1 ) ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` ( ( j - 1 ) + 1 ) ) ` x ) x. ( ( D ` ( i - ( j - 1 ) ) ) ` x ) ) )
508	507	a1i	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> sum_ j e. ( ( 0 + 1 ) ... ( i + 1 ) ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` ( ( j - 1 ) + 1 ) ) ` x ) x. ( ( D ` ( i - ( j - 1 ) ) ) ` x ) ) ) = sum_ j e. ( 1 ... ( i + 1 ) ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` ( ( j - 1 ) + 1 ) ) ` x ) x. ( ( D ` ( i - ( j - 1 ) ) ) ` x ) ) ) )
509		elfzelz	|- ( j e. ( 1 ... ( i + 1 ) ) -> j e. ZZ )
510	509	zcnd	|- ( j e. ( 1 ... ( i + 1 ) ) -> j e. CC )
511		1cnd	|- ( j e. ( 1 ... ( i + 1 ) ) -> 1 e. CC )
512	510 511	npcand	|- ( j e. ( 1 ... ( i + 1 ) ) -> ( ( j - 1 ) + 1 ) = j )
513	512	fveq2d	|- ( j e. ( 1 ... ( i + 1 ) ) -> ( C ` ( ( j - 1 ) + 1 ) ) = ( C ` j ) )
514	513	fveq1d	|- ( j e. ( 1 ... ( i + 1 ) ) -> ( ( C ` ( ( j - 1 ) + 1 ) ) ` x ) = ( ( C ` j ) ` x ) )
515	514	adantl	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( C ` ( ( j - 1 ) + 1 ) ) ` x ) = ( ( C ` j ) ` x ) )
516	216	recnd	|- ( i e. ( 0 ..^ N ) -> i e. CC )
517	516	adantr	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> i e. CC )
518	510	adantl	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> j e. CC )
519	511	adantl	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> 1 e. CC )
520	517 518 519	subsub3d	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( i - ( j - 1 ) ) = ( ( i + 1 ) - j ) )
521	520	fveq2d	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( D ` ( i - ( j - 1 ) ) ) = ( D ` ( ( i + 1 ) - j ) ) )
522	521	fveq1d	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( D ` ( i - ( j - 1 ) ) ) ` x ) = ( ( D ` ( ( i + 1 ) - j ) ) ` x ) )
523	515 522	oveq12d	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( ( C ` ( ( j - 1 ) + 1 ) ) ` x ) x. ( ( D ` ( i - ( j - 1 ) ) ) ` x ) ) = ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) )
524	523	oveq2d	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( i _C ( j - 1 ) ) x. ( ( ( C ` ( ( j - 1 ) + 1 ) ) ` x ) x. ( ( D ` ( i - ( j - 1 ) ) ) ` x ) ) ) = ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) )
525	524	sumeq2dv	|- ( i e. ( 0 ..^ N ) -> sum_ j e. ( 1 ... ( i + 1 ) ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` ( ( j - 1 ) + 1 ) ) ` x ) x. ( ( D ` ( i - ( j - 1 ) ) ) ` x ) ) ) = sum_ j e. ( 1 ... ( i + 1 ) ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) )
526	525	ad2antlr	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> sum_ j e. ( 1 ... ( i + 1 ) ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` ( ( j - 1 ) + 1 ) ) ` x ) x. ( ( D ` ( i - ( j - 1 ) ) ) ` x ) ) ) = sum_ j e. ( 1 ... ( i + 1 ) ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) )
527		nfv	|- F/ j ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X )
528		nfcv	|- F/_ j ( ( i _C ( ( i + 1 ) - 1 ) ) x. ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) )
529		fzfid	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( 1 ... ( i + 1 ) ) e. Fin )
530	187	adantr	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> i e. NN0 )
531	509	adantl	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> j e. ZZ )
532		1zzd	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> 1 e. ZZ )
533	531 532	zsubcld	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( j - 1 ) e. ZZ )
534	530 533	bccld	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( i _C ( j - 1 ) ) e. NN0 )
535	534	nn0cnd	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( i _C ( j - 1 ) ) e. CC )
536	535	adantll	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( i _C ( j - 1 ) ) e. CC )
537	536	adantlr	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( i _C ( j - 1 ) ) e. CC )
538	12	ad2antrr	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ph )
539		0zd	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> 0 e. ZZ )
540	208	adantr	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> N e. ZZ )
541	539 540 531	3jca	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( 0 e. ZZ /\ N e. ZZ /\ j e. ZZ ) )
542	173	a1i	|- ( j e. ( 1 ... ( i + 1 ) ) -> 0 e. RR )
543	509	zred	|- ( j e. ( 1 ... ( i + 1 ) ) -> j e. RR )
544		1red	|- ( j e. ( 1 ... ( i + 1 ) ) -> 1 e. RR )
545		0lt1	|- 0 < 1
546	545	a1i	|- ( j e. ( 1 ... ( i + 1 ) ) -> 0 < 1 )
547		elfzle1	|- ( j e. ( 1 ... ( i + 1 ) ) -> 1 <_ j )
548	542 544 543 546 547	ltletrd	|- ( j e. ( 1 ... ( i + 1 ) ) -> 0 < j )
549	542 543 548	ltled	|- ( j e. ( 1 ... ( i + 1 ) ) -> 0 <_ j )
550	549	adantl	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> 0 <_ j )
551	543	adantl	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> j e. RR )
552	216	adantr	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> i e. RR )
553		1red	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> 1 e. RR )
554	552 553	readdcld	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( i + 1 ) e. RR )
555	214	adantr	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> N e. RR )
556		elfzle2	|- ( j e. ( 1 ... ( i + 1 ) ) -> j <_ ( i + 1 ) )
557	556	adantl	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> j <_ ( i + 1 ) )
558	308	adantr	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( i + 1 ) <_ N )
559	551 554 555 557 558	letrd	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> j <_ N )
560	541 550 559	jca32	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( 0 e. ZZ /\ N e. ZZ /\ j e. ZZ ) /\ ( 0 <_ j /\ j <_ N ) ) )
561		elfz2	|- ( j e. ( 0 ... N ) <-> ( ( 0 e. ZZ /\ N e. ZZ /\ j e. ZZ ) /\ ( 0 <_ j /\ j <_ N ) ) )
562	560 561	sylibr	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> j e. ( 0 ... N ) )
563	562	adantll	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> j e. ( 0 ... N ) )
564	538 563 367	syl2anc	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( C ` j ) : X --> CC )
565	564	adantlr	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( C ` j ) : X --> CC )
566		simplr	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> x e. X )
567	565 566	ffvelrnd	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( C ` j ) ` x ) e. CC )
568	237	adantr	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> i e. ZZ )
569	568	peano2zd	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( i + 1 ) e. ZZ )
570	569 531	zsubcld	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - j ) e. ZZ )
571	539 540 570	3jca	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( 0 e. ZZ /\ N e. ZZ /\ ( ( i + 1 ) - j ) e. ZZ ) )
572	554 551	subge0d	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( 0 <_ ( ( i + 1 ) - j ) <-> j <_ ( i + 1 ) ) )
573	557 572	mpbird	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> 0 <_ ( ( i + 1 ) - j ) )
574	554 551	resubcld	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - j ) e. RR )
575	574	leidd	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - j ) <_ ( ( i + 1 ) - j ) )
576	543 548	elrpd	|- ( j e. ( 1 ... ( i + 1 ) ) -> j e. RR+ )
577	576	adantl	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> j e. RR+ )
578	554 577	ltsubrpd	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - j ) < ( i + 1 ) )
579	574 554 555 578 558	ltletrd	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - j ) < N )
580	574 574 555 575 579	lelttrd	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - j ) < N )
581	574 555 580	ltled	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - j ) <_ N )
582	571 573 581	jca32	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( 0 e. ZZ /\ N e. ZZ /\ ( ( i + 1 ) - j ) e. ZZ ) /\ ( 0 <_ ( ( i + 1 ) - j ) /\ ( ( i + 1 ) - j ) <_ N ) ) )
583		elfz2	|- ( ( ( i + 1 ) - j ) e. ( 0 ... N ) <-> ( ( 0 e. ZZ /\ N e. ZZ /\ ( ( i + 1 ) - j ) e. ZZ ) /\ ( 0 <_ ( ( i + 1 ) - j ) /\ ( ( i + 1 ) - j ) <_ N ) ) )
584	582 583	sylibr	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - j ) e. ( 0 ... N ) )
585	584	adantll	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - j ) e. ( 0 ... N ) )
586		nfv	|- F/ k ( ph /\ ( ( i + 1 ) - j ) e. ( 0 ... N ) )
587		nfcv	|- F/_ k ( ( i + 1 ) - j )
588	473 587	nffv	|- F/_ k ( D ` ( ( i + 1 ) - j ) )
589	588 360 361	nff	|- F/ k ( D ` ( ( i + 1 ) - j ) ) : X --> CC
590	586 589	nfim	|- F/ k ( ( ph /\ ( ( i + 1 ) - j ) e. ( 0 ... N ) ) -> ( D ` ( ( i + 1 ) - j ) ) : X --> CC )
591		ovex	|- ( ( i + 1 ) - j ) e. _V
592		eleq1	|- ( k = ( ( i + 1 ) - j ) -> ( k e. ( 0 ... N ) <-> ( ( i + 1 ) - j ) e. ( 0 ... N ) ) )
593	592	anbi2d	|- ( k = ( ( i + 1 ) - j ) -> ( ( ph /\ k e. ( 0 ... N ) ) <-> ( ph /\ ( ( i + 1 ) - j ) e. ( 0 ... N ) ) ) )
594		fveq2	|- ( k = ( ( i + 1 ) - j ) -> ( D ` k ) = ( D ` ( ( i + 1 ) - j ) ) )
595	594	feq1d	|- ( k = ( ( i + 1 ) - j ) -> ( ( D ` k ) : X --> CC <-> ( D ` ( ( i + 1 ) - j ) ) : X --> CC ) )
596	593 595	imbi12d	|- ( k = ( ( i + 1 ) - j ) -> ( ( ( ph /\ k e. ( 0 ... N ) ) -> ( D ` k ) : X --> CC ) <-> ( ( ph /\ ( ( i + 1 ) - j ) e. ( 0 ... N ) ) -> ( D ` ( ( i + 1 ) - j ) ) : X --> CC ) ) )
597	11	a1i	|- ( ph -> D = ( k e. ( 0 ... N ) |-> ( ( S Dn G ) ` k ) ) )
598		fvexd	|- ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( S Dn G ) ` k ) e. _V )
599	597 598	fvmpt2d	|- ( ( ph /\ k e. ( 0 ... N ) ) -> ( D ` k ) = ( ( S Dn G ) ` k ) )
600	599	feq1d	|- ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( D ` k ) : X --> CC <-> ( ( S Dn G ) ` k ) : X --> CC ) )
601	9 600	mpbird	|- ( ( ph /\ k e. ( 0 ... N ) ) -> ( D ` k ) : X --> CC )
602	590 591 596 601	vtoclf	|- ( ( ph /\ ( ( i + 1 ) - j ) e. ( 0 ... N ) ) -> ( D ` ( ( i + 1 ) - j ) ) : X --> CC )
603	538 585 602	syl2anc	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( D ` ( ( i + 1 ) - j ) ) : X --> CC )
604	603	adantlr	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( D ` ( ( i + 1 ) - j ) ) : X --> CC )
605	604 566	ffvelrnd	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( D ` ( ( i + 1 ) - j ) ) ` x ) e. CC )
606	567 605	mulcld	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) e. CC )
607	537 606	mulcld	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) e. CC )
608		1zzd	|- ( i e. ( 0 ..^ N ) -> 1 e. ZZ )
609	237	peano2zd	|- ( i e. ( 0 ..^ N ) -> ( i + 1 ) e. ZZ )
610	505	eqcomi	|- 1 = ( 0 + 1 )
611	610	a1i	|- ( i e. ( 0 ..^ N ) -> 1 = ( 0 + 1 ) )
612	173	a1i	|- ( i e. ( 0 ..^ N ) -> 0 e. RR )
613		1red	|- ( i e. ( 0 ..^ N ) -> 1 e. RR )
614	187	nn0ge0d	|- ( i e. ( 0 ..^ N ) -> 0 <_ i )
615	612 216 613 614	leadd1dd	|- ( i e. ( 0 ..^ N ) -> ( 0 + 1 ) <_ ( i + 1 ) )
616	611 615	eqbrtrd	|- ( i e. ( 0 ..^ N ) -> 1 <_ ( i + 1 ) )
617	608 609 616	3jca	|- ( i e. ( 0 ..^ N ) -> ( 1 e. ZZ /\ ( i + 1 ) e. ZZ /\ 1 <_ ( i + 1 ) ) )
618		eluz2	|- ( ( i + 1 ) e. ( ZZ>= ` 1 ) <-> ( 1 e. ZZ /\ ( i + 1 ) e. ZZ /\ 1 <_ ( i + 1 ) ) )
619	617 618	sylibr	|- ( i e. ( 0 ..^ N ) -> ( i + 1 ) e. ( ZZ>= ` 1 ) )
620		eluzfz2	|- ( ( i + 1 ) e. ( ZZ>= ` 1 ) -> ( i + 1 ) e. ( 1 ... ( i + 1 ) ) )
621	619 620	syl	|- ( i e. ( 0 ..^ N ) -> ( i + 1 ) e. ( 1 ... ( i + 1 ) ) )
622	621	ad2antlr	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( i + 1 ) e. ( 1 ... ( i + 1 ) ) )
623		oveq1	|- ( j = ( i + 1 ) -> ( j - 1 ) = ( ( i + 1 ) - 1 ) )
624	623	oveq2d	|- ( j = ( i + 1 ) -> ( i _C ( j - 1 ) ) = ( i _C ( ( i + 1 ) - 1 ) ) )
625		fveq2	|- ( j = ( i + 1 ) -> ( C ` j ) = ( C ` ( i + 1 ) ) )
626	625	fveq1d	|- ( j = ( i + 1 ) -> ( ( C ` j ) ` x ) = ( ( C ` ( i + 1 ) ) ` x ) )
627		oveq2	|- ( j = ( i + 1 ) -> ( ( i + 1 ) - j ) = ( ( i + 1 ) - ( i + 1 ) ) )
628	627	fveq2d	|- ( j = ( i + 1 ) -> ( D ` ( ( i + 1 ) - j ) ) = ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) )
629	628	fveq1d	|- ( j = ( i + 1 ) -> ( ( D ` ( ( i + 1 ) - j ) ) ` x ) = ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) )
630	626 629	oveq12d	|- ( j = ( i + 1 ) -> ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) = ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) )
631	624 630	oveq12d	|- ( j = ( i + 1 ) -> ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) = ( ( i _C ( ( i + 1 ) - 1 ) ) x. ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) ) )
632	527 528 529 607 622 631	fsumsplit1	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> sum_ j e. ( 1 ... ( i + 1 ) ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) = ( ( ( i _C ( ( i + 1 ) - 1 ) ) x. ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) ) + sum_ j e. ( ( 1 ... ( i + 1 ) ) \ { ( i + 1 ) } ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) ) )
633		1cnd	|- ( i e. ( 0 ..^ N ) -> 1 e. CC )
634	516 633	pncand	|- ( i e. ( 0 ..^ N ) -> ( ( i + 1 ) - 1 ) = i )
635	634	oveq2d	|- ( i e. ( 0 ..^ N ) -> ( i _C ( ( i + 1 ) - 1 ) ) = ( i _C i ) )
636		bcnn	|- ( i e. NN0 -> ( i _C i ) = 1 )
637	187 636	syl	|- ( i e. ( 0 ..^ N ) -> ( i _C i ) = 1 )
638	635 637	eqtrd	|- ( i e. ( 0 ..^ N ) -> ( i _C ( ( i + 1 ) - 1 ) ) = 1 )
639	516 633	addcld	|- ( i e. ( 0 ..^ N ) -> ( i + 1 ) e. CC )
640	639	subidd	|- ( i e. ( 0 ..^ N ) -> ( ( i + 1 ) - ( i + 1 ) ) = 0 )
641	640	fveq2d	|- ( i e. ( 0 ..^ N ) -> ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) = ( D ` 0 ) )
642	641	fveq1d	|- ( i e. ( 0 ..^ N ) -> ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) = ( ( D ` 0 ) ` x ) )
643	642	oveq2d	|- ( i e. ( 0 ..^ N ) -> ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) = ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) )
644	638 643	oveq12d	|- ( i e. ( 0 ..^ N ) -> ( ( i _C ( ( i + 1 ) - 1 ) ) x. ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) ) = ( 1 x. ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) ) )
645	644	ad2antlr	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( i _C ( ( i + 1 ) - 1 ) ) x. ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) ) = ( 1 x. ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) ) )
646		simpl	|- ( ( ph /\ i e. ( 0 ..^ N ) ) -> ph )
647		fzofzp1	|- ( i e. ( 0 ..^ N ) -> ( i + 1 ) e. ( 0 ... N ) )
648	647	adantl	|- ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( i + 1 ) e. ( 0 ... N ) )
649		nfv	|- F/ k ( ph /\ ( i + 1 ) e. ( 0 ... N ) )
650		nfcv	|- F/_ k ( i + 1 )
651	357 650	nffv	|- F/_ k ( C ` ( i + 1 ) )
652	651 360 361	nff	|- F/ k ( C ` ( i + 1 ) ) : X --> CC
653	649 652	nfim	|- F/ k ( ( ph /\ ( i + 1 ) e. ( 0 ... N ) ) -> ( C ` ( i + 1 ) ) : X --> CC )
654		ovex	|- ( i + 1 ) e. _V
655		eleq1	|- ( k = ( i + 1 ) -> ( k e. ( 0 ... N ) <-> ( i + 1 ) e. ( 0 ... N ) ) )
656	655	anbi2d	|- ( k = ( i + 1 ) -> ( ( ph /\ k e. ( 0 ... N ) ) <-> ( ph /\ ( i + 1 ) e. ( 0 ... N ) ) ) )
657		fveq2	|- ( k = ( i + 1 ) -> ( C ` k ) = ( C ` ( i + 1 ) ) )
658	657	feq1d	|- ( k = ( i + 1 ) -> ( ( C ` k ) : X --> CC <-> ( C ` ( i + 1 ) ) : X --> CC ) )
659	656 658	imbi12d	|- ( k = ( i + 1 ) -> ( ( ( ph /\ k e. ( 0 ... N ) ) -> ( C ` k ) : X --> CC ) <-> ( ( ph /\ ( i + 1 ) e. ( 0 ... N ) ) -> ( C ` ( i + 1 ) ) : X --> CC ) ) )
660	653 654 659 232	vtoclf	|- ( ( ph /\ ( i + 1 ) e. ( 0 ... N ) ) -> ( C ` ( i + 1 ) ) : X --> CC )
661	646 648 660	syl2anc	|- ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( C ` ( i + 1 ) ) : X --> CC )
662	661	ffvelrnda	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( C ` ( i + 1 ) ) ` x ) e. CC )
663		nfv	|- F/ k ( ph /\ 0 e. ( 0 ... N ) )
664		nfcv	|- F/_ k 0
665	473 664	nffv	|- F/_ k ( D ` 0 )
666	665 360 361	nff	|- F/ k ( D ` 0 ) : X --> CC
667	663 666	nfim	|- F/ k ( ( ph /\ 0 e. ( 0 ... N ) ) -> ( D ` 0 ) : X --> CC )
668		c0ex	|- 0 e. _V
669		eleq1	|- ( k = 0 -> ( k e. ( 0 ... N ) <-> 0 e. ( 0 ... N ) ) )
670	669	anbi2d	|- ( k = 0 -> ( ( ph /\ k e. ( 0 ... N ) ) <-> ( ph /\ 0 e. ( 0 ... N ) ) ) )
671		fveq2	|- ( k = 0 -> ( D ` k ) = ( D ` 0 ) )
672	671	feq1d	|- ( k = 0 -> ( ( D ` k ) : X --> CC <-> ( D ` 0 ) : X --> CC ) )
673	670 672	imbi12d	|- ( k = 0 -> ( ( ( ph /\ k e. ( 0 ... N ) ) -> ( D ` k ) : X --> CC ) <-> ( ( ph /\ 0 e. ( 0 ... N ) ) -> ( D ` 0 ) : X --> CC ) ) )
674	667 668 673 601	vtoclf	|- ( ( ph /\ 0 e. ( 0 ... N ) ) -> ( D ` 0 ) : X --> CC )
675	12 117 674	syl2anc	|- ( ph -> ( D ` 0 ) : X --> CC )
676	675	adantr	|- ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( D ` 0 ) : X --> CC )
677	676	ffvelrnda	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( D ` 0 ) ` x ) e. CC )
678	662 677	mulcld	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) e. CC )
679	678	mulid2d	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( 1 x. ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) ) = ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) )
680	645 679	eqtrd	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( i _C ( ( i + 1 ) - 1 ) ) x. ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) ) = ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) )
681		1m1e0	|- ( 1 - 1 ) = 0
682	681	fveq2i	|- ( ZZ>= ` ( 1 - 1 ) ) = ( ZZ>= ` 0 )
683	13	eqcomi	|- ( ZZ>= ` 0 ) = NN0
684	682 683	eqtr2i	|- NN0 = ( ZZ>= ` ( 1 - 1 ) )
685	684	a1i	|- ( i e. ( 0 ..^ N ) -> NN0 = ( ZZ>= ` ( 1 - 1 ) ) )
686	187 685	eleqtrd	|- ( i e. ( 0 ..^ N ) -> i e. ( ZZ>= ` ( 1 - 1 ) ) )
687		fzdifsuc2	|- ( i e. ( ZZ>= ` ( 1 - 1 ) ) -> ( 1 ... i ) = ( ( 1 ... ( i + 1 ) ) \ { ( i + 1 ) } ) )
688	686 687	syl	|- ( i e. ( 0 ..^ N ) -> ( 1 ... i ) = ( ( 1 ... ( i + 1 ) ) \ { ( i + 1 ) } ) )
689	688	eqcomd	|- ( i e. ( 0 ..^ N ) -> ( ( 1 ... ( i + 1 ) ) \ { ( i + 1 ) } ) = ( 1 ... i ) )
690	689	sumeq1d	|- ( i e. ( 0 ..^ N ) -> sum_ j e. ( ( 1 ... ( i + 1 ) ) \ { ( i + 1 ) } ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) = sum_ j e. ( 1 ... i ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) )
691	690	ad2antlr	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> sum_ j e. ( ( 1 ... ( i + 1 ) ) \ { ( i + 1 ) } ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) = sum_ j e. ( 1 ... i ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) )
692	680 691	oveq12d	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( ( i _C ( ( i + 1 ) - 1 ) ) x. ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) ) + sum_ j e. ( ( 1 ... ( i + 1 ) ) \ { ( i + 1 ) } ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) ) = ( ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) + sum_ j e. ( 1 ... i ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) ) )
693	526 632 692	3eqtrd	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> sum_ j e. ( 1 ... ( i + 1 ) ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` ( ( j - 1 ) + 1 ) ) ` x ) x. ( ( D ` ( i - ( j - 1 ) ) ) ` x ) ) ) = ( ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) + sum_ j e. ( 1 ... i ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) ) )
694	504 508 693	3eqtrd	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) = ( ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) + sum_ j e. ( 1 ... i ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) ) )
695		nfcv	|- F/_ k ( i _C 0 )
696	357 664	nffv	|- F/_ k ( C ` 0 )
697	696 470	nffv	|- F/_ k ( ( C ` 0 ) ` x )
698		nfcv	|- F/_ k ( ( i + 1 ) - 0 )
699	473 698	nffv	|- F/_ k ( D ` ( ( i + 1 ) - 0 ) )
700	699 470	nffv	|- F/_ k ( ( D ` ( ( i + 1 ) - 0 ) ) ` x )
701	697 467 700	nfov	|- F/_ k ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) )
702	695 467 701	nfov	|- F/_ k ( ( i _C 0 ) x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) ) )
703	683	a1i	|- ( i e. ( 0 ..^ N ) -> ( ZZ>= ` 0 ) = NN0 )
704	187 703	eleqtrrd	|- ( i e. ( 0 ..^ N ) -> i e. ( ZZ>= ` 0 ) )
705		eluzfz1	|- ( i e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... i ) )
706	704 705	syl	|- ( i e. ( 0 ..^ N ) -> 0 e. ( 0 ... i ) )
707	706	ad2antlr	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> 0 e. ( 0 ... i ) )
708		oveq2	|- ( k = 0 -> ( i _C k ) = ( i _C 0 ) )
709	110	fveq1d	|- ( k = 0 -> ( ( C ` k ) ` x ) = ( ( C ` 0 ) ` x ) )
710		oveq2	|- ( k = 0 -> ( ( i + 1 ) - k ) = ( ( i + 1 ) - 0 ) )
711	710	fveq2d	|- ( k = 0 -> ( D ` ( ( i + 1 ) - k ) ) = ( D ` ( ( i + 1 ) - 0 ) ) )
712	711	fveq1d	|- ( k = 0 -> ( ( D ` ( ( i + 1 ) - k ) ) ` x ) = ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) )
713	709 712	oveq12d	|- ( k = 0 -> ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) = ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) ) )
714	708 713	oveq12d	|- ( k = 0 -> ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) = ( ( i _C 0 ) x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) ) ) )
715	484 702 451 453 707 714	fsumsplit1	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) = ( ( ( i _C 0 ) x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) ) ) + sum_ k e. ( ( 0 ... i ) \ { 0 } ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
716	639	subid1d	|- ( i e. ( 0 ..^ N ) -> ( ( i + 1 ) - 0 ) = ( i + 1 ) )
717	716	fveq2d	|- ( i e. ( 0 ..^ N ) -> ( D ` ( ( i + 1 ) - 0 ) ) = ( D ` ( i + 1 ) ) )
718	717	fveq1d	|- ( i e. ( 0 ..^ N ) -> ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) = ( ( D ` ( i + 1 ) ) ` x ) )
719	718	oveq2d	|- ( i e. ( 0 ..^ N ) -> ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) ) = ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) )
720	719	oveq2d	|- ( i e. ( 0 ..^ N ) -> ( ( i _C 0 ) x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) ) ) = ( ( i _C 0 ) x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) ) )
721	720	oveq1d	|- ( i e. ( 0 ..^ N ) -> ( ( ( i _C 0 ) x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) ) ) + sum_ k e. ( ( 0 ... i ) \ { 0 } ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) = ( ( ( i _C 0 ) x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) ) + sum_ k e. ( ( 0 ... i ) \ { 0 } ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
722	721	ad2antlr	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( ( i _C 0 ) x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) ) ) + sum_ k e. ( ( 0 ... i ) \ { 0 } ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) = ( ( ( i _C 0 ) x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) ) + sum_ k e. ( ( 0 ... i ) \ { 0 } ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
723		bcn0	|- ( i e. NN0 -> ( i _C 0 ) = 1 )
724	187 723	syl	|- ( i e. ( 0 ..^ N ) -> ( i _C 0 ) = 1 )
725	724	oveq1d	|- ( i e. ( 0 ..^ N ) -> ( ( i _C 0 ) x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) ) = ( 1 x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) ) )
726	725	ad2antlr	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( i _C 0 ) x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) ) = ( 1 x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) ) )
727	696 360 361	nff	|- F/ k ( C ` 0 ) : X --> CC
728	663 727	nfim	|- F/ k ( ( ph /\ 0 e. ( 0 ... N ) ) -> ( C ` 0 ) : X --> CC )
729	110	feq1d	|- ( k = 0 -> ( ( C ` k ) : X --> CC <-> ( C ` 0 ) : X --> CC ) )
730	670 729	imbi12d	|- ( k = 0 -> ( ( ( ph /\ k e. ( 0 ... N ) ) -> ( C ` k ) : X --> CC ) <-> ( ( ph /\ 0 e. ( 0 ... N ) ) -> ( C ` 0 ) : X --> CC ) ) )
731	728 668 730 232	vtoclf	|- ( ( ph /\ 0 e. ( 0 ... N ) ) -> ( C ` 0 ) : X --> CC )
732	12 117 731	syl2anc	|- ( ph -> ( C ` 0 ) : X --> CC )
733	732	adantr	|- ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( C ` 0 ) : X --> CC )
734	733	ffvelrnda	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( C ` 0 ) ` x ) e. CC )
735	473 650	nffv	|- F/_ k ( D ` ( i + 1 ) )
736	735 360 361	nff	|- F/ k ( D ` ( i + 1 ) ) : X --> CC
737	649 736	nfim	|- F/ k ( ( ph /\ ( i + 1 ) e. ( 0 ... N ) ) -> ( D ` ( i + 1 ) ) : X --> CC )
738		fveq2	|- ( k = ( i + 1 ) -> ( D ` k ) = ( D ` ( i + 1 ) ) )
739	738	feq1d	|- ( k = ( i + 1 ) -> ( ( D ` k ) : X --> CC <-> ( D ` ( i + 1 ) ) : X --> CC ) )
740	656 739	imbi12d	|- ( k = ( i + 1 ) -> ( ( ( ph /\ k e. ( 0 ... N ) ) -> ( D ` k ) : X --> CC ) <-> ( ( ph /\ ( i + 1 ) e. ( 0 ... N ) ) -> ( D ` ( i + 1 ) ) : X --> CC ) ) )
741	737 654 740 601	vtoclf	|- ( ( ph /\ ( i + 1 ) e. ( 0 ... N ) ) -> ( D ` ( i + 1 ) ) : X --> CC )
742	646 648 741	syl2anc	|- ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( D ` ( i + 1 ) ) : X --> CC )
743	742	ffvelrnda	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( D ` ( i + 1 ) ) ` x ) e. CC )
744	734 743	mulcld	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) e. CC )
745	744	mulid2d	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( 1 x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) ) = ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) )
746	726 745	eqtrd	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( i _C 0 ) x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) ) = ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) )
747		nfv	|- F/ j i e. ( 0 ..^ N )
748		1zzd	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( ( 0 ... i ) \ { 0 } ) ) -> 1 e. ZZ )
749	237	adantr	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( ( 0 ... i ) \ { 0 } ) ) -> i e. ZZ )
750		eldifi	|- ( j e. ( ( 0 ... i ) \ { 0 } ) -> j e. ( 0 ... i ) )
751		elfzelz	|- ( j e. ( 0 ... i ) -> j e. ZZ )
752	750 751	syl	|- ( j e. ( ( 0 ... i ) \ { 0 } ) -> j e. ZZ )
753	752	adantl	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( ( 0 ... i ) \ { 0 } ) ) -> j e. ZZ )
754	748 749 753	3jca	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( ( 0 ... i ) \ { 0 } ) ) -> ( 1 e. ZZ /\ i e. ZZ /\ j e. ZZ ) )
755		elfznn0	|- ( j e. ( 0 ... i ) -> j e. NN0 )
756	750 755	syl	|- ( j e. ( ( 0 ... i ) \ { 0 } ) -> j e. NN0 )
757		eldifsni	|- ( j e. ( ( 0 ... i ) \ { 0 } ) -> j =/= 0 )
758	756 757	jca	|- ( j e. ( ( 0 ... i ) \ { 0 } ) -> ( j e. NN0 /\ j =/= 0 ) )
759		elnnne0	|- ( j e. NN <-> ( j e. NN0 /\ j =/= 0 ) )
760	758 759	sylibr	|- ( j e. ( ( 0 ... i ) \ { 0 } ) -> j e. NN )
761		nnge1	|- ( j e. NN -> 1 <_ j )
762	760 761	syl	|- ( j e. ( ( 0 ... i ) \ { 0 } ) -> 1 <_ j )
763	762	adantl	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( ( 0 ... i ) \ { 0 } ) ) -> 1 <_ j )
764		elfzle2	|- ( j e. ( 0 ... i ) -> j <_ i )
765	750 764	syl	|- ( j e. ( ( 0 ... i ) \ { 0 } ) -> j <_ i )
766	765	adantl	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( ( 0 ... i ) \ { 0 } ) ) -> j <_ i )
767	754 763 766	jca32	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( ( 0 ... i ) \ { 0 } ) ) -> ( ( 1 e. ZZ /\ i e. ZZ /\ j e. ZZ ) /\ ( 1 <_ j /\ j <_ i ) ) )
768		elfz2	|- ( j e. ( 1 ... i ) <-> ( ( 1 e. ZZ /\ i e. ZZ /\ j e. ZZ ) /\ ( 1 <_ j /\ j <_ i ) ) )
769	767 768	sylibr	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( ( 0 ... i ) \ { 0 } ) ) -> j e. ( 1 ... i ) )
770	769	ex	|- ( i e. ( 0 ..^ N ) -> ( j e. ( ( 0 ... i ) \ { 0 } ) -> j e. ( 1 ... i ) ) )
771		0zd	|- ( j e. ( 1 ... i ) -> 0 e. ZZ )
772		elfzel2	|- ( j e. ( 1 ... i ) -> i e. ZZ )
773		elfzelz	|- ( j e. ( 1 ... i ) -> j e. ZZ )
774	771 772 773	3jca	|- ( j e. ( 1 ... i ) -> ( 0 e. ZZ /\ i e. ZZ /\ j e. ZZ ) )
775	173	a1i	|- ( j e. ( 1 ... i ) -> 0 e. RR )
776	773	zred	|- ( j e. ( 1 ... i ) -> j e. RR )
777		1red	|- ( j e. ( 1 ... i ) -> 1 e. RR )
778	545	a1i	|- ( j e. ( 1 ... i ) -> 0 < 1 )
779		elfzle1	|- ( j e. ( 1 ... i ) -> 1 <_ j )
780	775 777 776 778 779	ltletrd	|- ( j e. ( 1 ... i ) -> 0 < j )
781	775 776 780	ltled	|- ( j e. ( 1 ... i ) -> 0 <_ j )
782		elfzle2	|- ( j e. ( 1 ... i ) -> j <_ i )
783	774 781 782	jca32	|- ( j e. ( 1 ... i ) -> ( ( 0 e. ZZ /\ i e. ZZ /\ j e. ZZ ) /\ ( 0 <_ j /\ j <_ i ) ) )
784		elfz2	|- ( j e. ( 0 ... i ) <-> ( ( 0 e. ZZ /\ i e. ZZ /\ j e. ZZ ) /\ ( 0 <_ j /\ j <_ i ) ) )
785	783 784	sylibr	|- ( j e. ( 1 ... i ) -> j e. ( 0 ... i ) )
786	775 780	gtned	|- ( j e. ( 1 ... i ) -> j =/= 0 )
787		nelsn	|- ( j =/= 0 -> -. j e. { 0 } )
788	786 787	syl	|- ( j e. ( 1 ... i ) -> -. j e. { 0 } )
789	785 788	eldifd	|- ( j e. ( 1 ... i ) -> j e. ( ( 0 ... i ) \ { 0 } ) )
790	789	adantl	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... i ) ) -> j e. ( ( 0 ... i ) \ { 0 } ) )
791	790	ex	|- ( i e. ( 0 ..^ N ) -> ( j e. ( 1 ... i ) -> j e. ( ( 0 ... i ) \ { 0 } ) ) )
792	770 791	impbid	|- ( i e. ( 0 ..^ N ) -> ( j e. ( ( 0 ... i ) \ { 0 } ) <-> j e. ( 1 ... i ) ) )
793	747 792	alrimi	|- ( i e. ( 0 ..^ N ) -> A. j ( j e. ( ( 0 ... i ) \ { 0 } ) <-> j e. ( 1 ... i ) ) )
794		dfcleq	|- ( ( ( 0 ... i ) \ { 0 } ) = ( 1 ... i ) <-> A. j ( j e. ( ( 0 ... i ) \ { 0 } ) <-> j e. ( 1 ... i ) ) )
795	793 794	sylibr	|- ( i e. ( 0 ..^ N ) -> ( ( 0 ... i ) \ { 0 } ) = ( 1 ... i ) )
796	795	sumeq1d	|- ( i e. ( 0 ..^ N ) -> sum_ k e. ( ( 0 ... i ) \ { 0 } ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) = sum_ k e. ( 1 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) )
797	796	ad2antlr	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> sum_ k e. ( ( 0 ... i ) \ { 0 } ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) = sum_ k e. ( 1 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) )
798	746 797	oveq12d	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( ( i _C 0 ) x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) ) + sum_ k e. ( ( 0 ... i ) \ { 0 } ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) = ( ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) + sum_ k e. ( 1 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
799	715 722 798	3eqtrd	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) = ( ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) + sum_ k e. ( 1 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
800	694 799	oveq12d	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) + sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) = ( ( ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) + sum_ j e. ( 1 ... i ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) ) + ( ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) + sum_ k e. ( 1 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) ) )
801		fzfid	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( 1 ... i ) e. Fin )
802	187	adantr	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... i ) ) -> i e. NN0 )
803	790 752	syl	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... i ) ) -> j e. ZZ )
804		1zzd	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... i ) ) -> 1 e. ZZ )
805	803 804	zsubcld	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... i ) ) -> ( j - 1 ) e. ZZ )
806	802 805	bccld	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... i ) ) -> ( i _C ( j - 1 ) ) e. NN0 )
807	806	nn0cnd	|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... i ) ) -> ( i _C ( j - 1 ) ) e. CC )
808	807	adantll	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ j e. ( 1 ... i ) ) -> ( i _C ( j - 1 ) ) e. CC )
809	808	adantlr	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... i ) ) -> ( i _C ( j - 1 ) ) e. CC )
810		simpl	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... i ) ) -> ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) )
811		fzelp1	|- ( j e. ( 1 ... i ) -> j e. ( 1 ... ( i + 1 ) ) )
812	811	adantl	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... i ) ) -> j e. ( 1 ... ( i + 1 ) ) )
813	810 812 567	syl2anc	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... i ) ) -> ( ( C ` j ) ` x ) e. CC )
814	812 605	syldan	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... i ) ) -> ( ( D ` ( ( i + 1 ) - j ) ) ` x ) e. CC )
815	813 814	mulcld	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... i ) ) -> ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) e. CC )
816	809 815	mulcld	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... i ) ) -> ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) e. CC )
817	801 816	fsumcl	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> sum_ j e. ( 1 ... i ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) e. CC )
818	187	adantr	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> i e. NN0 )
819		elfzelz	|- ( k e. ( 1 ... i ) -> k e. ZZ )
820	819	adantl	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> k e. ZZ )
821	818 820	bccld	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> ( i _C k ) e. NN0 )
822	821	nn0cnd	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> ( i _C k ) e. CC )
823	822	adantll	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 1 ... i ) ) -> ( i _C k ) e. CC )
824	823	adantlr	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 1 ... i ) ) -> ( i _C k ) e. CC )
825		simpll	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 1 ... i ) ) -> ( ph /\ i e. ( 0 ..^ N ) ) )
826		simplr	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 1 ... i ) ) -> x e. X )
827	785	ssriv	|- ( 1 ... i ) C_ ( 0 ... i )
828		id	|- ( k e. ( 1 ... i ) -> k e. ( 1 ... i ) )
829	827 828	sseldi	|- ( k e. ( 1 ... i ) -> k e. ( 0 ... i ) )
830	829	adantl	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 1 ... i ) ) -> k e. ( 0 ... i ) )
831	825 826 830 445	syl21anc	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 1 ... i ) ) -> ( ( C ` k ) ` x ) e. CC )
832	830 447	syldan	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 1 ... i ) ) -> ( ( D ` ( ( i + 1 ) - k ) ) ` x ) e. CC )
833	831 832	mulcld	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 1 ... i ) ) -> ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) e. CC )
834	824 833	mulcld	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 1 ... i ) ) -> ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) e. CC )
835	801 834	fsumcl	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> sum_ k e. ( 1 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) e. CC )
836	678 817 744 835	add4d	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) + sum_ j e. ( 1 ... i ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) ) + ( ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) + sum_ k e. ( 1 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) ) = ( ( ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) + ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) ) + ( sum_ j e. ( 1 ... i ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) + sum_ k e. ( 1 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) ) )
837		oveq1	|- ( j = k -> ( j - 1 ) = ( k - 1 ) )
838	837	oveq2d	|- ( j = k -> ( i _C ( j - 1 ) ) = ( i _C ( k - 1 ) ) )
839		fveq2	|- ( j = k -> ( C ` j ) = ( C ` k ) )
840	839	fveq1d	|- ( j = k -> ( ( C ` j ) ` x ) = ( ( C ` k ) ` x ) )
841		oveq2	|- ( j = k -> ( ( i + 1 ) - j ) = ( ( i + 1 ) - k ) )
842	841	fveq2d	|- ( j = k -> ( D ` ( ( i + 1 ) - j ) ) = ( D ` ( ( i + 1 ) - k ) ) )
843	842	fveq1d	|- ( j = k -> ( ( D ` ( ( i + 1 ) - j ) ) ` x ) = ( ( D ` ( ( i + 1 ) - k ) ) ` x ) )
844	840 843	oveq12d	|- ( j = k -> ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) = ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) )
845	838 844	oveq12d	|- ( j = k -> ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) = ( ( i _C ( k - 1 ) ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) )
846		nfcv	|- F/_ k ( 1 ... i )
847		nfcv	|- F/_ j ( 1 ... i )
848		nfcv	|- F/_ k ( i _C ( j - 1 ) )
849	359 470	nffv	|- F/_ k ( ( C ` j ) ` x )
850	588 470	nffv	|- F/_ k ( ( D ` ( ( i + 1 ) - j ) ) ` x )
851	849 467 850	nfov	|- F/_ k ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) )
852	848 467 851	nfov	|- F/_ k ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) )
853		nfcv	|- F/_ j ( ( i _C ( k - 1 ) ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) )
854	845 846 847 852 853	cbvsum	|- sum_ j e. ( 1 ... i ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) = sum_ k e. ( 1 ... i ) ( ( i _C ( k - 1 ) ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) )
855	854	a1i	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> sum_ j e. ( 1 ... i ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) = sum_ k e. ( 1 ... i ) ( ( i _C ( k - 1 ) ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) )
856	855	oveq1d	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( sum_ j e. ( 1 ... i ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) + sum_ k e. ( 1 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) = ( sum_ k e. ( 1 ... i ) ( ( i _C ( k - 1 ) ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) + sum_ k e. ( 1 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
857		peano2zm	|- ( k e. ZZ -> ( k - 1 ) e. ZZ )
858	820 857	syl	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> ( k - 1 ) e. ZZ )
859	818 858	bccld	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> ( i _C ( k - 1 ) ) e. NN0 )
860	859	nn0cnd	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> ( i _C ( k - 1 ) ) e. CC )
861	860	adantll	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 1 ... i ) ) -> ( i _C ( k - 1 ) ) e. CC )
862	861	adantlr	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 1 ... i ) ) -> ( i _C ( k - 1 ) ) e. CC )
863	862 833	mulcld	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 1 ... i ) ) -> ( ( i _C ( k - 1 ) ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) e. CC )
864	801 863 834	fsumadd	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> sum_ k e. ( 1 ... i ) ( ( ( i _C ( k - 1 ) ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) + ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) = ( sum_ k e. ( 1 ... i ) ( ( i _C ( k - 1 ) ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) + sum_ k e. ( 1 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
865	864	eqcomd	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( sum_ k e. ( 1 ... i ) ( ( i _C ( k - 1 ) ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) + sum_ k e. ( 1 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) = sum_ k e. ( 1 ... i ) ( ( ( i _C ( k - 1 ) ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) + ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
866	860 822	addcomd	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> ( ( i _C ( k - 1 ) ) + ( i _C k ) ) = ( ( i _C k ) + ( i _C ( k - 1 ) ) ) )
867		bcpasc	|- ( ( i e. NN0 /\ k e. ZZ ) -> ( ( i _C k ) + ( i _C ( k - 1 ) ) ) = ( ( i + 1 ) _C k ) )
868	818 820 867	syl2anc	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> ( ( i _C k ) + ( i _C ( k - 1 ) ) ) = ( ( i + 1 ) _C k ) )
869	866 868	eqtr2d	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> ( ( i + 1 ) _C k ) = ( ( i _C ( k - 1 ) ) + ( i _C k ) ) )
870	869	oveq1d	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) = ( ( ( i _C ( k - 1 ) ) + ( i _C k ) ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) )
871	870	adantll	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 1 ... i ) ) -> ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) = ( ( ( i _C ( k - 1 ) ) + ( i _C k ) ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) )
872	871	adantlr	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 1 ... i ) ) -> ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) = ( ( ( i _C ( k - 1 ) ) + ( i _C k ) ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) )
873	862 824 833	adddird	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 1 ... i ) ) -> ( ( ( i _C ( k - 1 ) ) + ( i _C k ) ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) = ( ( ( i _C ( k - 1 ) ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) + ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
874	872 873	eqtr2d	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 1 ... i ) ) -> ( ( ( i _C ( k - 1 ) ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) + ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) = ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) )
875	874	sumeq2dv	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> sum_ k e. ( 1 ... i ) ( ( ( i _C ( k - 1 ) ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) + ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) = sum_ k e. ( 1 ... i ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) )
876	856 865 875	3eqtrd	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( sum_ j e. ( 1 ... i ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) + sum_ k e. ( 1 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) = sum_ k e. ( 1 ... i ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) )
877	876	oveq2d	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) + ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) ) + ( sum_ j e. ( 1 ... i ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) + sum_ k e. ( 1 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) ) = ( ( ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) + ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) ) + sum_ k e. ( 1 ... i ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
878		peano2nn0	|- ( i e. NN0 -> ( i + 1 ) e. NN0 )
879	818 878	syl	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> ( i + 1 ) e. NN0 )
880	879 820	bccld	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> ( ( i + 1 ) _C k ) e. NN0 )
881	880	nn0cnd	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> ( ( i + 1 ) _C k ) e. CC )
882	881	adantll	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 1 ... i ) ) -> ( ( i + 1 ) _C k ) e. CC )
883	882	adantlr	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 1 ... i ) ) -> ( ( i + 1 ) _C k ) e. CC )
884	883 833	mulcld	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 1 ... i ) ) -> ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) e. CC )
885	801 884	fsumcl	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> sum_ k e. ( 1 ... i ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) e. CC )
886	678 744 885	addassd	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) + ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) ) + sum_ k e. ( 1 ... i ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) = ( ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) + ( ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) + sum_ k e. ( 1 ... i ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) ) )
887	187 878	syl	|- ( i e. ( 0 ..^ N ) -> ( i + 1 ) e. NN0 )
888		bcn0	|- ( ( i + 1 ) e. NN0 -> ( ( i + 1 ) _C 0 ) = 1 )
889	887 888	syl	|- ( i e. ( 0 ..^ N ) -> ( ( i + 1 ) _C 0 ) = 1 )
890	889 719	oveq12d	|- ( i e. ( 0 ..^ N ) -> ( ( ( i + 1 ) _C 0 ) x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) ) ) = ( 1 x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) ) )
891	890	ad2antlr	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( ( i + 1 ) _C 0 ) x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) ) ) = ( 1 x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) ) )
892	891 745	eqtr2d	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) = ( ( ( i + 1 ) _C 0 ) x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) ) ) )
893	795	ad2antlr	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( 0 ... i ) \ { 0 } ) = ( 1 ... i ) )
894	893	eqcomd	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( 1 ... i ) = ( ( 0 ... i ) \ { 0 } ) )
895	894	sumeq1d	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> sum_ k e. ( 1 ... i ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) = sum_ k e. ( ( 0 ... i ) \ { 0 } ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) )
896	892 895	oveq12d	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) + sum_ k e. ( 1 ... i ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) = ( ( ( ( i + 1 ) _C 0 ) x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) ) ) + sum_ k e. ( ( 0 ... i ) \ { 0 } ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
897		nfcv	|- F/_ k ( ( i + 1 ) _C 0 )
898	897 467 701	nfov	|- F/_ k ( ( ( i + 1 ) _C 0 ) x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) ) )
899	199 878	syl	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( i + 1 ) e. NN0 )
900	899 201	bccld	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( ( i + 1 ) _C k ) e. NN0 )
901	900	nn0cnd	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( ( i + 1 ) _C k ) e. CC )
902	901	adantll	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( i + 1 ) _C k ) e. CC )
903	902	adantlr	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... i ) ) -> ( ( i + 1 ) _C k ) e. CC )
904	903 448	mulcld	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... i ) ) -> ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) e. CC )
905		oveq2	|- ( k = 0 -> ( ( i + 1 ) _C k ) = ( ( i + 1 ) _C 0 ) )
906	905 713	oveq12d	|- ( k = 0 -> ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) = ( ( ( i + 1 ) _C 0 ) x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) ) ) )
907	484 898 451 904 707 906	fsumsplit1	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> sum_ k e. ( 0 ... i ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) = ( ( ( ( i + 1 ) _C 0 ) x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) ) ) + sum_ k e. ( ( 0 ... i ) \ { 0 } ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
908	907	eqcomd	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( ( ( i + 1 ) _C 0 ) x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) ) ) + sum_ k e. ( ( 0 ... i ) \ { 0 } ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) = sum_ k e. ( 0 ... i ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) )
909	896 908	eqtrd	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) + sum_ k e. ( 1 ... i ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) = sum_ k e. ( 0 ... i ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) )
910	909	oveq2d	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) + ( ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) + sum_ k e. ( 1 ... i ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) ) = ( ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) + sum_ k e. ( 0 ... i ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
911		bcnn	|- ( ( i + 1 ) e. NN0 -> ( ( i + 1 ) _C ( i + 1 ) ) = 1 )
912	887 911	syl	|- ( i e. ( 0 ..^ N ) -> ( ( i + 1 ) _C ( i + 1 ) ) = 1 )
913	912	ad2antlr	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( i + 1 ) _C ( i + 1 ) ) = 1 )
914	913	oveq1d	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( ( i + 1 ) _C ( i + 1 ) ) x. ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) ) = ( 1 x. ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) ) )
915	641	adantl	|- ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) = ( D ` 0 ) )
916	915	feq1d	|- ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) : X --> CC <-> ( D ` 0 ) : X --> CC ) )
917	676 916	mpbird	|- ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) : X --> CC )
918	917	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) : X --> CC )
919		simpr	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> x e. X )
920	918 919	ffvelrnd	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) e. CC )
921	662 920	mulcld	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) e. CC )
922	921	mulid2d	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( 1 x. ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) ) = ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) )
923	643	ad2antlr	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) = ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) )
924	914 922 923	3eqtrrd	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) = ( ( ( i + 1 ) _C ( i + 1 ) ) x. ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) ) )
925		fzdifsuc	|- ( i e. ( ZZ>= ` 0 ) -> ( 0 ... i ) = ( ( 0 ... ( i + 1 ) ) \ { ( i + 1 ) } ) )
926	704 925	syl	|- ( i e. ( 0 ..^ N ) -> ( 0 ... i ) = ( ( 0 ... ( i + 1 ) ) \ { ( i + 1 ) } ) )
927	926	sumeq1d	|- ( i e. ( 0 ..^ N ) -> sum_ k e. ( 0 ... i ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) = sum_ k e. ( ( 0 ... ( i + 1 ) ) \ { ( i + 1 ) } ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) )
928	927	ad2antlr	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> sum_ k e. ( 0 ... i ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) = sum_ k e. ( ( 0 ... ( i + 1 ) ) \ { ( i + 1 ) } ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) )
929	924 928	oveq12d	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) + sum_ k e. ( 0 ... i ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) = ( ( ( ( i + 1 ) _C ( i + 1 ) ) x. ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) ) + sum_ k e. ( ( 0 ... ( i + 1 ) ) \ { ( i + 1 ) } ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
930		nfcv	|- F/_ k ( ( i + 1 ) _C ( i + 1 ) )
931	651 470	nffv	|- F/_ k ( ( C ` ( i + 1 ) ) ` x )
932		nfcv	|- F/_ k ( ( i + 1 ) - ( i + 1 ) )
933	473 932	nffv	|- F/_ k ( D ` ( ( i + 1 ) - ( i + 1 ) ) )
934	933 470	nffv	|- F/_ k ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x )
935	931 467 934	nfov	|- F/_ k ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) )
936	930 467 935	nfov	|- F/_ k ( ( ( i + 1 ) _C ( i + 1 ) ) x. ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) )
937		fzfid	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( 0 ... ( i + 1 ) ) e. Fin )
938	887	adantr	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( i + 1 ) e. NN0 )
939		elfzelz	|- ( k e. ( 0 ... ( i + 1 ) ) -> k e. ZZ )
940	939	adantl	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> k e. ZZ )
941	938 940	bccld	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( i + 1 ) _C k ) e. NN0 )
942	941	nn0cnd	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( i + 1 ) _C k ) e. CC )
943	942	adantll	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( i + 1 ) _C k ) e. CC )
944	943	adantlr	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( i + 1 ) _C k ) e. CC )
945	646	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ph )
946	96	a1i	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> 0 e. ZZ )
947	208	adantr	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> N e. ZZ )
948	946 947 940	3jca	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( 0 e. ZZ /\ N e. ZZ /\ k e. ZZ ) )
949		elfzle1	|- ( k e. ( 0 ... ( i + 1 ) ) -> 0 <_ k )
950	949	adantl	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> 0 <_ k )
951	940	zred	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> k e. RR )
952	938	nn0red	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( i + 1 ) e. RR )
953	214	adantr	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> N e. RR )
954		elfzle2	|- ( k e. ( 0 ... ( i + 1 ) ) -> k <_ ( i + 1 ) )
955	954	adantl	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> k <_ ( i + 1 ) )
956	308	adantr	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( i + 1 ) <_ N )
957	951 952 953 955 956	letrd	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> k <_ N )
958	948 950 957	jca32	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( 0 e. ZZ /\ N e. ZZ /\ k e. ZZ ) /\ ( 0 <_ k /\ k <_ N ) ) )
959	958 225	sylibr	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> k e. ( 0 ... N ) )
960	959	adantll	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> k e. ( 0 ... N ) )
961	945 960 232	syl2anc	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( C ` k ) : X --> CC )
962	961	adantlr	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( C ` k ) : X --> CC )
963		simplr	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> x e. X )
964	962 963	ffvelrnd	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( C ` k ) ` x ) e. CC )
965	945	adantlr	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ph )
966	609	adantr	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( i + 1 ) e. ZZ )
967	966 940	zsubcld	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - k ) e. ZZ )
968	946 947 967	3jca	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( 0 e. ZZ /\ N e. ZZ /\ ( ( i + 1 ) - k ) e. ZZ ) )
969	952 951	subge0d	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( 0 <_ ( ( i + 1 ) - k ) <-> k <_ ( i + 1 ) ) )
970	955 969	mpbird	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> 0 <_ ( ( i + 1 ) - k ) )
971	952 951	resubcld	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - k ) e. RR )
972	953 951	resubcld	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( N - k ) e. RR )
973	953 173 251	sylancl	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( N - 0 ) e. RR )
974	952 953 951 956	lesub1dd	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - k ) <_ ( N - k ) )
975	173	a1i	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> 0 e. RR )
976	975 951 953 950	lesub2dd	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( N - k ) <_ ( N - 0 ) )
977	971 972 973 974 976	letrd	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - k ) <_ ( N - 0 ) )
978	257	adantr	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( N - 0 ) = N )
979	977 978	breqtrd	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - k ) <_ N )
980	968 970 979	jca32	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( 0 e. ZZ /\ N e. ZZ /\ ( ( i + 1 ) - k ) e. ZZ ) /\ ( 0 <_ ( ( i + 1 ) - k ) /\ ( ( i + 1 ) - k ) <_ N ) ) )
981	980 314	sylibr	|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - k ) e. ( 0 ... N ) )
982	981	adantll	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - k ) e. ( 0 ... N ) )
983	982	adantlr	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - k ) e. ( 0 ... N ) )
984		fveq2	|- ( j = ( ( i + 1 ) - k ) -> ( D ` j ) = ( D ` ( ( i + 1 ) - k ) ) )
985	984	feq1d	|- ( j = ( ( i + 1 ) - k ) -> ( ( D ` j ) : X --> CC <-> ( D ` ( ( i + 1 ) - k ) ) : X --> CC ) )
986	319 985	imbi12d	|- ( j = ( ( i + 1 ) - k ) -> ( ( ( ph /\ j e. ( 0 ... N ) ) -> ( D ` j ) : X --> CC ) <-> ( ( ph /\ ( ( i + 1 ) - k ) e. ( 0 ... N ) ) -> ( D ` ( ( i + 1 ) - k ) ) : X --> CC ) ) )
987	473 358	nffv	|- F/_ k ( D ` j )
988	987 360 361	nff	|- F/ k ( D ` j ) : X --> CC
989	355 988	nfim	|- F/ k ( ( ph /\ j e. ( 0 ... N ) ) -> ( D ` j ) : X --> CC )
990		fveq2	|- ( k = j -> ( D ` k ) = ( D ` j ) )
991	990	feq1d	|- ( k = j -> ( ( D ` k ) : X --> CC <-> ( D ` j ) : X --> CC ) )
992	273 991	imbi12d	|- ( k = j -> ( ( ( ph /\ k e. ( 0 ... N ) ) -> ( D ` k ) : X --> CC ) <-> ( ( ph /\ j e. ( 0 ... N ) ) -> ( D ` j ) : X --> CC ) ) )
993	989 992 601	chvarfv	|- ( ( ph /\ j e. ( 0 ... N ) ) -> ( D ` j ) : X --> CC )
994	317 986 993	vtocl	|- ( ( ph /\ ( ( i + 1 ) - k ) e. ( 0 ... N ) ) -> ( D ` ( ( i + 1 ) - k ) ) : X --> CC )
995	965 983 994	syl2anc	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( D ` ( ( i + 1 ) - k ) ) : X --> CC )
996	995 963	ffvelrnd	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( D ` ( ( i + 1 ) - k ) ) ` x ) e. CC )
997	964 996	mulcld	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) e. CC )
998	944 997	mulcld	|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) e. CC )
999	887 703	eleqtrrd	|- ( i e. ( 0 ..^ N ) -> ( i + 1 ) e. ( ZZ>= ` 0 ) )
1000		eluzfz2	|- ( ( i + 1 ) e. ( ZZ>= ` 0 ) -> ( i + 1 ) e. ( 0 ... ( i + 1 ) ) )
1001	999 1000	syl	|- ( i e. ( 0 ..^ N ) -> ( i + 1 ) e. ( 0 ... ( i + 1 ) ) )
1002	1001	ad2antlr	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( i + 1 ) e. ( 0 ... ( i + 1 ) ) )
1003		oveq2	|- ( k = ( i + 1 ) -> ( ( i + 1 ) _C k ) = ( ( i + 1 ) _C ( i + 1 ) ) )
1004	657	fveq1d	|- ( k = ( i + 1 ) -> ( ( C ` k ) ` x ) = ( ( C ` ( i + 1 ) ) ` x ) )
1005		oveq2	|- ( k = ( i + 1 ) -> ( ( i + 1 ) - k ) = ( ( i + 1 ) - ( i + 1 ) ) )
1006	1005	fveq2d	|- ( k = ( i + 1 ) -> ( D ` ( ( i + 1 ) - k ) ) = ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) )
1007	1006	fveq1d	|- ( k = ( i + 1 ) -> ( ( D ` ( ( i + 1 ) - k ) ) ` x ) = ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) )
1008	1004 1007	oveq12d	|- ( k = ( i + 1 ) -> ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) = ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) )
1009	1003 1008	oveq12d	|- ( k = ( i + 1 ) -> ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) = ( ( ( i + 1 ) _C ( i + 1 ) ) x. ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) ) )
1010	484 936 937 998 1002 1009	fsumsplit1	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> sum_ k e. ( 0 ... ( i + 1 ) ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) = ( ( ( ( i + 1 ) _C ( i + 1 ) ) x. ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) ) + sum_ k e. ( ( 0 ... ( i + 1 ) ) \ { ( i + 1 ) } ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
1011	1010	eqcomd	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( ( ( i + 1 ) _C ( i + 1 ) ) x. ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) ) + sum_ k e. ( ( 0 ... ( i + 1 ) ) \ { ( i + 1 ) } ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) = sum_ k e. ( 0 ... ( i + 1 ) ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) )
1012	910 929 1011	3eqtrd	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) + ( ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) + sum_ k e. ( 1 ... i ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) ) = sum_ k e. ( 0 ... ( i + 1 ) ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) )
1013	877 886 1012	3eqtrd	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) + ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) ) + ( sum_ j e. ( 1 ... i ) ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) ) + sum_ k e. ( 1 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) ) = sum_ k e. ( 0 ... ( i + 1 ) ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) )
1014	800 836 1013	3eqtrd	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) + sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) = sum_ k e. ( 0 ... ( i + 1 ) ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) )
1015	450 454 1014	3eqtrd	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) = sum_ k e. ( 0 ... ( i + 1 ) ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) )
1016	1015	mpteq2dva	|- ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( x e. X |-> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) + ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) ) = ( x e. X |-> sum_ k e. ( 0 ... ( i + 1 ) ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
1017	434 1016	eqtrd	|- ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( S _D ( x e. X |-> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) ) = ( x e. X |-> sum_ k e. ( 0 ... ( i + 1 ) ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
1018	1017	adantr	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` i ) = ( x e. X |-> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) ) -> ( S _D ( x e. X |-> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) ) = ( x e. X |-> sum_ k e. ( 0 ... ( i + 1 ) ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
1019	191 193 1018	3eqtrd	|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` i ) = ( x e. X |-> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) ) -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` ( i + 1 ) ) = ( x e. X |-> sum_ k e. ( 0 ... ( i + 1 ) ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
1020	180 181 184 1019	syl21anc	|- ( ( i e. ( 0 ..^ N ) /\ ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` i ) = ( x e. X |-> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) ) /\ ph ) -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` ( i + 1 ) ) = ( x e. X |-> sum_ k e. ( 0 ... ( i + 1 ) ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) )
1021	1020	3exp	|- ( i e. ( 0 ..^ N ) -> ( ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` i ) = ( x e. X |-> sum_ k e. ( 0 ... i ) ( ( i _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) ) ) -> ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` ( i + 1 ) ) = ( x e. X |-> sum_ k e. ( 0 ... ( i + 1 ) ) ( ( ( i + 1 ) _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) ) ) ) ) )
1022	44 57 70 83 179 1021	fzind2	|- ( n e. ( 0 ... N ) -> ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` n ) = ( x e. X |-> sum_ k e. ( 0 ... n ) ( ( n _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( n - k ) ) ` x ) ) ) ) ) )
1023	31 1022	vtoclg	|- ( N e. NN0 -> ( N e. ( 0 ... N ) -> ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` N ) = ( x e. X |-> sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( N - k ) ) ` x ) ) ) ) ) ) )
1024	5 16 1023	sylc	|- ( ph -> ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` N ) = ( x e. X |-> sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( N - k ) ) ` x ) ) ) ) ) )
1025	12 1024	mpd	|- ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` N ) = ( x e. X |-> sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( N - k ) ) ` x ) ) ) ) )