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	sselid	\|- ( 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	mullidd	\|- ( ( 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		elfzle1	\|- ( k e. ( 0 ... i ) -> 0 <_ k )
211	210	adantl	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> 0 <_ k )
212	201	zred	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> k e. RR )
213	208	zred	\|- ( i e. ( 0 ..^ N ) -> N e. RR )
214	213	adantr	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> N e. RR )
215	187	nn0red	\|- ( i e. ( 0 ..^ N ) -> i e. RR )
216	215	adantr	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> i e. RR )
217		elfzle2	\|- ( k e. ( 0 ... i ) -> k <_ i )
218	217	adantl	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> k <_ i )
219		elfzolt2	\|- ( i e. ( 0 ..^ N ) -> i < N )
220	219	adantr	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> i < N )
221	212 216 214 218 220	lelttrd	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> k < N )
222	212 214 221	ltled	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> k <_ N )
223	207 209 201 211 222	elfzd	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> k e. ( 0 ... N ) )
224	223	adantll	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> k e. ( 0 ... N ) )
225	10	a1i	\|- ( ph -> C = ( k e. ( 0 ... N ) \|-> ( ( S Dn F ) ` k ) ) )
226		fvexd	\|- ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( S Dn F ) ` k ) e. _V )
227	225 226	fvmpt2d	\|- ( ( ph /\ k e. ( 0 ... N ) ) -> ( C ` k ) = ( ( S Dn F ) ` k ) )
228	227	feq1d	\|- ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( C ` k ) : X --> CC <-> ( ( S Dn F ) ` k ) : X --> CC ) )
229	8 228	mpbird	\|- ( ( ph /\ k e. ( 0 ... N ) ) -> ( C ` k ) : X --> CC )
230	206 224 229	syl2anc	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( C ` k ) : X --> CC )
231	230	3adant3	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) /\ x e. X ) -> ( C ` k ) : X --> CC )
232		simp3	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) /\ x e. X ) -> x e. X )
233	231 232	ffvelcdmd	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) /\ x e. X ) -> ( ( C ` k ) ` x ) e. CC )
234	187	nn0zd	\|- ( i e. ( 0 ..^ N ) -> i e. ZZ )
235	234	adantr	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> i e. ZZ )
236	235 201	zsubcld	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( i - k ) e. ZZ )
237		elfzel2	\|- ( k e. ( 0 ... i ) -> i e. ZZ )
238	237	zred	\|- ( k e. ( 0 ... i ) -> i e. RR )
239	200	zred	\|- ( k e. ( 0 ... i ) -> k e. RR )
240	238 239	subge0d	\|- ( k e. ( 0 ... i ) -> ( 0 <_ ( i - k ) <-> k <_ i ) )
241	217 240	mpbird	\|- ( k e. ( 0 ... i ) -> 0 <_ ( i - k ) )
242	241	adantl	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> 0 <_ ( i - k ) )
243	216 212	resubcld	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( i - k ) e. RR )
244	214 212	resubcld	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( N - k ) e. RR )
245	173	a1i	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> 0 e. RR )
246	214 245	jca	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( N e. RR /\ 0 e. RR ) )
247		resubcl	\|- ( ( N e. RR /\ 0 e. RR ) -> ( N - 0 ) e. RR )
248	246 247	syl	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( N - 0 ) e. RR )
249	216 214 212 220	ltsub1dd	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( i - k ) < ( N - k ) )
250	245 212 214 211	lesub2dd	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( N - k ) <_ ( N - 0 ) )
251	243 244 248 249 250	ltletrd	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( i - k ) < ( N - 0 ) )
252	213	recnd	\|- ( i e. ( 0 ..^ N ) -> N e. CC )
253	252	subid1d	\|- ( i e. ( 0 ..^ N ) -> ( N - 0 ) = N )
254	253	adantr	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( N - 0 ) = N )
255	251 254	breqtrd	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( i - k ) < N )
256	243 214 255	ltled	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( i - k ) <_ N )
257	207 209 236 242 256	elfzd	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( i - k ) e. ( 0 ... N ) )
258	257	adantll	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( i - k ) e. ( 0 ... N ) )
259		ovex	\|- ( i - k ) e. _V
260		eleq1	\|- ( j = ( i - k ) -> ( j e. ( 0 ... N ) <-> ( i - k ) e. ( 0 ... N ) ) )
261	260	anbi2d	\|- ( j = ( i - k ) -> ( ( ph /\ j e. ( 0 ... N ) ) <-> ( ph /\ ( i - k ) e. ( 0 ... N ) ) ) )
262		fveq2	\|- ( j = ( i - k ) -> ( ( S Dn G ) ` j ) = ( ( S Dn G ) ` ( i - k ) ) )
263	262	feq1d	\|- ( j = ( i - k ) -> ( ( ( S Dn G ) ` j ) : X --> CC <-> ( ( S Dn G ) ` ( i - k ) ) : X --> CC ) )
264	261 263	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 ) ) )
265		nfv	\|- F/ k ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( S Dn G ) ` j ) : X --> CC )
266		eleq1	\|- ( k = j -> ( k e. ( 0 ... N ) <-> j e. ( 0 ... N ) ) )
267	266	anbi2d	\|- ( k = j -> ( ( ph /\ k e. ( 0 ... N ) ) <-> ( ph /\ j e. ( 0 ... N ) ) ) )
268		fveq2	\|- ( k = j -> ( ( S Dn G ) ` k ) = ( ( S Dn G ) ` j ) )
269	268	feq1d	\|- ( k = j -> ( ( ( S Dn G ) ` k ) : X --> CC <-> ( ( S Dn G ) ` j ) : X --> CC ) )
270	267 269	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 ) ) )
271	265 270 9	chvarfv	\|- ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( S Dn G ) ` j ) : X --> CC )
272	259 264 271	vtocl	\|- ( ( ph /\ ( i - k ) e. ( 0 ... N ) ) -> ( ( S Dn G ) ` ( i - k ) ) : X --> CC )
273	206 258 272	syl2anc	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( S Dn G ) ` ( i - k ) ) : X --> CC )
274		fveq2	\|- ( n = ( i - k ) -> ( ( S Dn G ) ` n ) = ( ( S Dn G ) ` ( i - k ) ) )
275		fvexd	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( ( S Dn G ) ` ( i - k ) ) e. _V )
276	145 274 257 275	fvmptd3	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( D ` ( i - k ) ) = ( ( S Dn G ) ` ( i - k ) ) )
277	276	adantll	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( D ` ( i - k ) ) = ( ( S Dn G ) ` ( i - k ) ) )
278	277	feq1d	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( D ` ( i - k ) ) : X --> CC <-> ( ( S Dn G ) ` ( i - k ) ) : X --> CC ) )
279	273 278	mpbird	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( D ` ( i - k ) ) : X --> CC )
280	279	3adant3	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) /\ x e. X ) -> ( D ` ( i - k ) ) : X --> CC )
281	280 232	ffvelcdmd	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) /\ x e. X ) -> ( ( D ` ( i - k ) ) ` x ) e. CC )
282	233 281	mulcld	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) /\ x e. X ) -> ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) e. CC )
283	205 282	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 )
284	205	3expa	\|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( i _C k ) e. CC )
285	235	peano2zd	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( i + 1 ) e. ZZ )
286	285 201	zsubcld	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( ( i + 1 ) - k ) e. ZZ )
287		peano2re	\|- ( i e. RR -> ( i + 1 ) e. RR )
288	238 287	syl	\|- ( k e. ( 0 ... i ) -> ( i + 1 ) e. RR )
289		peano2re	\|- ( k e. RR -> ( k + 1 ) e. RR )
290	239 289	syl	\|- ( k e. ( 0 ... i ) -> ( k + 1 ) e. RR )
291	239	ltp1d	\|- ( k e. ( 0 ... i ) -> k < ( k + 1 ) )
292		1red	\|- ( k e. ( 0 ... i ) -> 1 e. RR )
293	239 238 292 217	leadd1dd	\|- ( k e. ( 0 ... i ) -> ( k + 1 ) <_ ( i + 1 ) )
294	239 290 288 291 293	ltletrd	\|- ( k e. ( 0 ... i ) -> k < ( i + 1 ) )
295	239 288 294	ltled	\|- ( k e. ( 0 ... i ) -> k <_ ( i + 1 ) )
296	295	adantl	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> k <_ ( i + 1 ) )
297	216 287	syl	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( i + 1 ) e. RR )
298	297 212	subge0d	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( 0 <_ ( ( i + 1 ) - k ) <-> k <_ ( i + 1 ) ) )
299	296 298	mpbird	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> 0 <_ ( ( i + 1 ) - k ) )
300	297 212	resubcld	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( ( i + 1 ) - k ) e. RR )
301		elfzop1le2	\|- ( i e. ( 0 ..^ N ) -> ( i + 1 ) <_ N )
302	301	adantr	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( i + 1 ) <_ N )
303	297 214 212 302	lesub1dd	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( ( i + 1 ) - k ) <_ ( N - k ) )
304	250 254	breqtrd	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( N - k ) <_ N )
305	300 244 214 303 304	letrd	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( ( i + 1 ) - k ) <_ N )
306	207 209 286 299 305	elfzd	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( ( i + 1 ) - k ) e. ( 0 ... N ) )
307	306	adantll	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( i + 1 ) - k ) e. ( 0 ... N ) )
308		ovex	\|- ( ( i + 1 ) - k ) e. _V
309		eleq1	\|- ( j = ( ( i + 1 ) - k ) -> ( j e. ( 0 ... N ) <-> ( ( i + 1 ) - k ) e. ( 0 ... N ) ) )
310	309	anbi2d	\|- ( j = ( ( i + 1 ) - k ) -> ( ( ph /\ j e. ( 0 ... N ) ) <-> ( ph /\ ( ( i + 1 ) - k ) e. ( 0 ... N ) ) ) )
311		fveq2	\|- ( j = ( ( i + 1 ) - k ) -> ( ( S Dn G ) ` j ) = ( ( S Dn G ) ` ( ( i + 1 ) - k ) ) )
312	311	feq1d	\|- ( j = ( ( i + 1 ) - k ) -> ( ( ( S Dn G ) ` j ) : X --> CC <-> ( ( S Dn G ) ` ( ( i + 1 ) - k ) ) : X --> CC ) )
313	310 312	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 ) ) )
314	308 313 271	vtocl	\|- ( ( ph /\ ( ( i + 1 ) - k ) e. ( 0 ... N ) ) -> ( ( S Dn G ) ` ( ( i + 1 ) - k ) ) : X --> CC )
315	206 307 314	syl2anc	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( S Dn G ) ` ( ( i + 1 ) - k ) ) : X --> CC )
316	145	a1i	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> D = ( n e. ( 0 ... N ) \|-> ( ( S Dn G ) ` n ) ) )
317		simpr	\|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ n = ( ( i + 1 ) - k ) ) -> n = ( ( i + 1 ) - k ) )
318	317	fveq2d	\|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ n = ( ( i + 1 ) - k ) ) -> ( ( S Dn G ) ` n ) = ( ( S Dn G ) ` ( ( i + 1 ) - k ) ) )
319		fvexd	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( S Dn G ) ` ( ( i + 1 ) - k ) ) e. _V )
320	316 318 307 319	fvmptd	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( D ` ( ( i + 1 ) - k ) ) = ( ( S Dn G ) ` ( ( i + 1 ) - k ) ) )
321	320	feq1d	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( D ` ( ( i + 1 ) - k ) ) : X --> CC <-> ( ( S Dn G ) ` ( ( i + 1 ) - k ) ) : X --> CC ) )
322	315 321	mpbird	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( D ` ( ( i + 1 ) - k ) ) : X --> CC )
323	322	ffvelcdmda	\|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( ( D ` ( ( i + 1 ) - k ) ) ` x ) e. CC )
324	233	3expa	\|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( ( C ` k ) ` x ) e. CC )
325	323 324	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 ) ) )
326	325	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 ) ) ) )
327	201	peano2zd	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( k + 1 ) e. ZZ )
328	173	a1i	\|- ( k e. ( 0 ... i ) -> 0 e. RR )
329	328 239 290 210 291	lelttrd	\|- ( k e. ( 0 ... i ) -> 0 < ( k + 1 ) )
330	328 290 329	ltled	\|- ( k e. ( 0 ... i ) -> 0 <_ ( k + 1 ) )
331	330	adantl	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> 0 <_ ( k + 1 ) )
332	212 289	syl	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( k + 1 ) e. RR )
333	293	adantl	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( k + 1 ) <_ ( i + 1 ) )
334	332 297 214 333 302	letrd	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( k + 1 ) <_ N )
335	207 209 327 331 334	elfzd	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( k + 1 ) e. ( 0 ... N ) )
336	335	adantll	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( k + 1 ) e. ( 0 ... N ) )
337		ovex	\|- ( k + 1 ) e. _V
338		eleq1	\|- ( j = ( k + 1 ) -> ( j e. ( 0 ... N ) <-> ( k + 1 ) e. ( 0 ... N ) ) )
339	338	anbi2d	\|- ( j = ( k + 1 ) -> ( ( ph /\ j e. ( 0 ... N ) ) <-> ( ph /\ ( k + 1 ) e. ( 0 ... N ) ) ) )
340		fveq2	\|- ( j = ( k + 1 ) -> ( C ` j ) = ( C ` ( k + 1 ) ) )
341	340	feq1d	\|- ( j = ( k + 1 ) -> ( ( C ` j ) : X --> CC <-> ( C ` ( k + 1 ) ) : X --> CC ) )
342	339 341	imbi12d	\|- ( j = ( k + 1 ) -> ( ( ( ph /\ j e. ( 0 ... N ) ) -> ( C ` j ) : X --> CC ) <-> ( ( ph /\ ( k + 1 ) e. ( 0 ... N ) ) -> ( C ` ( k + 1 ) ) : X --> CC ) ) )
343		nfv	\|- F/ k ( ph /\ j e. ( 0 ... N ) )
344		nfmpt1	\|- F/_ k ( k e. ( 0 ... N ) \|-> ( ( S Dn F ) ` k ) )
345	10 344	nfcxfr	\|- F/_ k C
346		nfcv	\|- F/_ k j
347	345 346	nffv	\|- F/_ k ( C ` j )
348		nfcv	\|- F/_ k X
349		nfcv	\|- F/_ k CC
350	347 348 349	nff	\|- F/ k ( C ` j ) : X --> CC
351	343 350	nfim	\|- F/ k ( ( ph /\ j e. ( 0 ... N ) ) -> ( C ` j ) : X --> CC )
352		fveq2	\|- ( k = j -> ( C ` k ) = ( C ` j ) )
353	352	feq1d	\|- ( k = j -> ( ( C ` k ) : X --> CC <-> ( C ` j ) : X --> CC ) )
354	267 353	imbi12d	\|- ( k = j -> ( ( ( ph /\ k e. ( 0 ... N ) ) -> ( C ` k ) : X --> CC ) <-> ( ( ph /\ j e. ( 0 ... N ) ) -> ( C ` j ) : X --> CC ) ) )
355	351 354 229	chvarfv	\|- ( ( ph /\ j e. ( 0 ... N ) ) -> ( C ` j ) : X --> CC )
356	337 342 355	vtocl	\|- ( ( ph /\ ( k + 1 ) e. ( 0 ... N ) ) -> ( C ` ( k + 1 ) ) : X --> CC )
357	206 336 356	syl2anc	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( C ` ( k + 1 ) ) : X --> CC )
358	357	ffvelcdmda	\|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( ( C ` ( k + 1 ) ) ` x ) e. CC )
359	281	3expa	\|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( ( D ` ( i - k ) ) ` x ) e. CC )
360	358 359	mulcld	\|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) e. CC )
361	323 324	mulcld	\|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( ( ( D ` ( ( i + 1 ) - k ) ) ` x ) x. ( ( C ` k ) ` x ) ) e. CC )
362	360 361	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 )
363	326 362	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 )
364	284 363	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 )
365	364	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 )
366	206 1	syl	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> S e. { RR , CC } )
367	173	a1i	\|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> 0 e. RR )
368	206 2	syl	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> X e. ( ( TopOpen ` CCfld ) \|`t S ) )
369	366 368 204	dvmptconst	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( S _D ( x e. X \|-> ( i _C k ) ) ) = ( x e. X \|-> 0 ) )
370	282	3expa	\|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) e. CC )
371	206 224 227	syl2anc	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( C ` k ) = ( ( S Dn F ) ` k ) )
372	371	eqcomd	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( S Dn F ) ` k ) = ( C ` k ) )
373	230	feqmptd	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( C ` k ) = ( x e. X \|-> ( ( C ` k ) ` x ) ) )
374	372 373	eqtr2d	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( x e. X \|-> ( ( C ` k ) ` x ) ) = ( ( S Dn F ) ` k ) )
375	374	oveq2d	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( S _D ( x e. X \|-> ( ( C ` k ) ` x ) ) ) = ( S _D ( ( S Dn F ) ` k ) ) )
376	366 84	syl	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> S C_ CC )
377	206 123	syl	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> F e. ( CC ^pm S ) )
378		elfznn0	\|- ( k e. ( 0 ... i ) -> k e. NN0 )
379	378	adantl	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> k e. NN0 )
380		dvnp1	\|- ( ( S C_ CC /\ F e. ( CC ^pm S ) /\ k e. NN0 ) -> ( ( S Dn F ) ` ( k + 1 ) ) = ( S _D ( ( S Dn F ) ` k ) ) )
381	376 377 379 380	syl3anc	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( S Dn F ) ` ( k + 1 ) ) = ( S _D ( ( S Dn F ) ` k ) ) )
382	381	eqcomd	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( S _D ( ( S Dn F ) ` k ) ) = ( ( S Dn F ) ` ( k + 1 ) ) )
383		fveq2	\|- ( n = ( k + 1 ) -> ( ( S Dn F ) ` n ) = ( ( S Dn F ) ` ( k + 1 ) ) )
384		fvexd	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( S Dn F ) ` ( k + 1 ) ) e. _V )
385	114 383 336 384	fvmptd3	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( C ` ( k + 1 ) ) = ( ( S Dn F ) ` ( k + 1 ) ) )
386	385	eqcomd	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( S Dn F ) ` ( k + 1 ) ) = ( C ` ( k + 1 ) ) )
387	357	feqmptd	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( C ` ( k + 1 ) ) = ( x e. X \|-> ( ( C ` ( k + 1 ) ) ` x ) ) )
388	386 387	eqtrd	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( S Dn F ) ` ( k + 1 ) ) = ( x e. X \|-> ( ( C ` ( k + 1 ) ) ` x ) ) )
389	375 382 388	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 ) ) )
390	277	eqcomd	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( S Dn G ) ` ( i - k ) ) = ( D ` ( i - k ) ) )
391	279	feqmptd	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( D ` ( i - k ) ) = ( x e. X \|-> ( ( D ` ( i - k ) ) ` x ) ) )
392	390 391	eqtr2d	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( x e. X \|-> ( ( D ` ( i - k ) ) ` x ) ) = ( ( S Dn G ) ` ( i - k ) ) )
393	392	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 ) ) ) )
394	206 152	syl	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> G e. ( CC ^pm S ) )
395		fznn0sub	\|- ( k e. ( 0 ... i ) -> ( i - k ) e. NN0 )
396	395	adantl	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( i - k ) e. NN0 )
397		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 ) ) ) )
398	376 394 396 397	syl3anc	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( S Dn G ) ` ( ( i - k ) + 1 ) ) = ( S _D ( ( S Dn G ) ` ( i - k ) ) ) )
399	398	eqcomd	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( S _D ( ( S Dn G ) ` ( i - k ) ) ) = ( ( S Dn G ) ` ( ( i - k ) + 1 ) ) )
400	216	recnd	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> i e. CC )
401		1cnd	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> 1 e. CC )
402	212	recnd	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> k e. CC )
403	400 401 402	addsubd	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( ( i + 1 ) - k ) = ( ( i - k ) + 1 ) )
404	403	eqcomd	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( ( i - k ) + 1 ) = ( ( i + 1 ) - k ) )
405	404	fveq2d	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( ( S Dn G ) ` ( ( i - k ) + 1 ) ) = ( ( S Dn G ) ` ( ( i + 1 ) - k ) ) )
406	405	adantll	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( S Dn G ) ` ( ( i - k ) + 1 ) ) = ( ( S Dn G ) ` ( ( i + 1 ) - k ) ) )
407	320	eqcomd	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( S Dn G ) ` ( ( i + 1 ) - k ) ) = ( D ` ( ( i + 1 ) - k ) ) )
408	322	feqmptd	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( D ` ( ( i + 1 ) - k ) ) = ( x e. X \|-> ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) )
409	406 407 408	3eqtrd	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( S Dn G ) ` ( ( i - k ) + 1 ) ) = ( x e. X \|-> ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) )
410	393 399 409	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 ) ) )
411	366 324 358 389 359 323 410	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 ) ) ) ) )
412	366 284 367 369 370 362 411	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 ) ) ) ) )
413	370	mul02d	\|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( 0 x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) ) = 0 )
414	326	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 ) ) )
415	363 284	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 ) ) ) ) )
416	414 415	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 ) ) ) ) )
417	413 416	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 ) ) ) ) ) )
418	364	addlidd	\|- ( ( ( ( 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 ) ) ) ) )
419	417 418	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 ) ) ) ) )
420	419	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 ) ) ) ) ) )
421	412 420	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 ) ) ) ) ) )
422	194 195 196 197 198 283 365 421	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 ) ) ) ) ) )
423	204	adantlr	\|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... i ) ) -> ( i _C k ) e. CC )
424	360	an32s	\|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... i ) ) -> ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) e. CC )
425		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 ) ) )
426		ancom	\|- ( ( k e. ( 0 ... i ) /\ x e. X ) <-> ( x e. X /\ k e. ( 0 ... i ) ) )
427	426	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 ) ) ) )
428		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 ) ) ) )
429	428	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 ) ) )
430	427 429	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 ) ) )
431	425 430	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 ) ) )
432	431	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 ) )
433	324 432	mpbi	\|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... i ) ) -> ( ( C ` k ) ` x ) e. CC )
434	431	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 ) )
435	323 434	mpbi	\|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... i ) ) -> ( ( D ` ( ( i + 1 ) - k ) ) ` x ) e. CC )
436	433 435	mulcld	\|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... i ) ) -> ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) e. CC )
437	423 424 436	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 ) ) ) ) )
438	437	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 ) ) ) ) )
439	198	adantr	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( 0 ... i ) e. Fin )
440	423 424	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 )
441	423 436	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 )
442	439 440 441	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 ) ) ) ) )
443		oveq2	\|- ( k = h -> ( i _C k ) = ( i _C h ) )
444		fvoveq1	\|- ( k = h -> ( C ` ( k + 1 ) ) = ( C ` ( h + 1 ) ) )
445	444	fveq1d	\|- ( k = h -> ( ( C ` ( k + 1 ) ) ` x ) = ( ( C ` ( h + 1 ) ) ` x ) )
446		oveq2	\|- ( k = h -> ( i - k ) = ( i - h ) )
447	446	fveq2d	\|- ( k = h -> ( D ` ( i - k ) ) = ( D ` ( i - h ) ) )
448	447	fveq1d	\|- ( k = h -> ( ( D ` ( i - k ) ) ` x ) = ( ( D ` ( i - h ) ) ` x ) )
449	445 448	oveq12d	\|- ( k = h -> ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) = ( ( ( C ` ( h + 1 ) ) ` x ) x. ( ( D ` ( i - h ) ) ` x ) ) )
450	443 449	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 ) ) ) )
451		nfcv	\|- F/_ h ( ( i _C k ) x. ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) )
452		nfcv	\|- F/_ k ( i _C h )
453		nfcv	\|- F/_ k x.
454		nfcv	\|- F/_ k ( h + 1 )
455	345 454	nffv	\|- F/_ k ( C ` ( h + 1 ) )
456		nfcv	\|- F/_ k x
457	455 456	nffv	\|- F/_ k ( ( C ` ( h + 1 ) ) ` x )
458		nfmpt1	\|- F/_ k ( k e. ( 0 ... N ) \|-> ( ( S Dn G ) ` k ) )
459	11 458	nfcxfr	\|- F/_ k D
460		nfcv	\|- F/_ k ( i - h )
461	459 460	nffv	\|- F/_ k ( D ` ( i - h ) )
462	461 456	nffv	\|- F/_ k ( ( D ` ( i - h ) ) ` x )
463	457 453 462	nfov	\|- F/_ k ( ( ( C ` ( h + 1 ) ) ` x ) x. ( ( D ` ( i - h ) ) ` x ) )
464	452 453 463	nfov	\|- F/_ k ( ( i _C h ) x. ( ( ( C ` ( h + 1 ) ) ` x ) x. ( ( D ` ( i - h ) ) ` x ) ) )
465	450 451 464	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 ) ) )
466	465	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 ) ) ) )
467		1zzd	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> 1 e. ZZ )
468	96	a1i	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> 0 e. ZZ )
469	234	ad2antlr	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> i e. ZZ )
470		nfv	\|- F/ k ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X )
471		nfcv	\|- F/_ k h
472		nfcv	\|- F/_ k ( 0 ... i )
473	471 472	nfel	\|- F/ k h e. ( 0 ... i )
474	470 473	nfan	\|- F/ k ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ h e. ( 0 ... i ) )
475	464 349	nfel	\|- F/ k ( ( i _C h ) x. ( ( ( C ` ( h + 1 ) ) ` x ) x. ( ( D ` ( i - h ) ) ` x ) ) ) e. CC
476	474 475	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 )
477		eleq1	\|- ( k = h -> ( k e. ( 0 ... i ) <-> h e. ( 0 ... i ) ) )
478	477	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 ) ) ) )
479	450	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 ) )
480	478 479	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 ) ) )
481	476 480 440	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 )
482		oveq2	\|- ( h = ( j - 1 ) -> ( i _C h ) = ( i _C ( j - 1 ) ) )
483		fvoveq1	\|- ( h = ( j - 1 ) -> ( C ` ( h + 1 ) ) = ( C ` ( ( j - 1 ) + 1 ) ) )
484	483	fveq1d	\|- ( h = ( j - 1 ) -> ( ( C ` ( h + 1 ) ) ` x ) = ( ( C ` ( ( j - 1 ) + 1 ) ) ` x ) )
485		oveq2	\|- ( h = ( j - 1 ) -> ( i - h ) = ( i - ( j - 1 ) ) )
486	485	fveq2d	\|- ( h = ( j - 1 ) -> ( D ` ( i - h ) ) = ( D ` ( i - ( j - 1 ) ) ) )
487	486	fveq1d	\|- ( h = ( j - 1 ) -> ( ( D ` ( i - h ) ) ` x ) = ( ( D ` ( i - ( j - 1 ) ) ) ` x ) )
488	484 487	oveq12d	\|- ( h = ( j - 1 ) -> ( ( ( C ` ( h + 1 ) ) ` x ) x. ( ( D ` ( i - h ) ) ` x ) ) = ( ( ( C ` ( ( j - 1 ) + 1 ) ) ` x ) x. ( ( D ` ( i - ( j - 1 ) ) ) ` x ) ) )
489	482 488	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 ) ) ) )
490	467 468 469 481 489	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 ) ) ) )
491	466 490	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 ) ) ) )
492		0p1e1	\|- ( 0 + 1 ) = 1
493	492	oveq1i	\|- ( ( 0 + 1 ) ... ( i + 1 ) ) = ( 1 ... ( i + 1 ) )
494	493	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 ) ) )
495	494	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 ) ) ) )
496		elfzelz	\|- ( j e. ( 1 ... ( i + 1 ) ) -> j e. ZZ )
497	496	zcnd	\|- ( j e. ( 1 ... ( i + 1 ) ) -> j e. CC )
498		1cnd	\|- ( j e. ( 1 ... ( i + 1 ) ) -> 1 e. CC )
499	497 498	npcand	\|- ( j e. ( 1 ... ( i + 1 ) ) -> ( ( j - 1 ) + 1 ) = j )
500	499	fveq2d	\|- ( j e. ( 1 ... ( i + 1 ) ) -> ( C ` ( ( j - 1 ) + 1 ) ) = ( C ` j ) )
501	500	fveq1d	\|- ( j e. ( 1 ... ( i + 1 ) ) -> ( ( C ` ( ( j - 1 ) + 1 ) ) ` x ) = ( ( C ` j ) ` x ) )
502	501	adantl	\|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( C ` ( ( j - 1 ) + 1 ) ) ` x ) = ( ( C ` j ) ` x ) )
503	215	recnd	\|- ( i e. ( 0 ..^ N ) -> i e. CC )
504	503	adantr	\|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> i e. CC )
505	497	adantl	\|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> j e. CC )
506	498	adantl	\|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> 1 e. CC )
507	504 505 506	subsub3d	\|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( i - ( j - 1 ) ) = ( ( i + 1 ) - j ) )
508	507	fveq2d	\|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( D ` ( i - ( j - 1 ) ) ) = ( D ` ( ( i + 1 ) - j ) ) )
509	508	fveq1d	\|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( D ` ( i - ( j - 1 ) ) ) ` x ) = ( ( D ` ( ( i + 1 ) - j ) ) ` x ) )
510	502 509	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 ) ) )
511	510	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 ) ) ) )
512	511	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 ) ) ) )
513	512	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 ) ) ) )
514		nfv	\|- F/ j ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X )
515		nfcv	\|- F/_ j ( ( i _C ( ( i + 1 ) - 1 ) ) x. ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) )
516		fzfid	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( 1 ... ( i + 1 ) ) e. Fin )
517	187	adantr	\|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> i e. NN0 )
518	496	adantl	\|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> j e. ZZ )
519		1zzd	\|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> 1 e. ZZ )
520	518 519	zsubcld	\|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( j - 1 ) e. ZZ )
521	517 520	bccld	\|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( i _C ( j - 1 ) ) e. NN0 )
522	521	nn0cnd	\|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( i _C ( j - 1 ) ) e. CC )
523	522	adantll	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( i _C ( j - 1 ) ) e. CC )
524	523	adantlr	\|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( i _C ( j - 1 ) ) e. CC )
525	12	ad2antrr	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ph )
526		0zd	\|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> 0 e. ZZ )
527	208	adantr	\|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> N e. ZZ )
528	173	a1i	\|- ( j e. ( 1 ... ( i + 1 ) ) -> 0 e. RR )
529	496	zred	\|- ( j e. ( 1 ... ( i + 1 ) ) -> j e. RR )
530		1red	\|- ( j e. ( 1 ... ( i + 1 ) ) -> 1 e. RR )
531		0lt1	\|- 0 < 1
532	531	a1i	\|- ( j e. ( 1 ... ( i + 1 ) ) -> 0 < 1 )
533		elfzle1	\|- ( j e. ( 1 ... ( i + 1 ) ) -> 1 <_ j )
534	528 530 529 532 533	ltletrd	\|- ( j e. ( 1 ... ( i + 1 ) ) -> 0 < j )
535	528 529 534	ltled	\|- ( j e. ( 1 ... ( i + 1 ) ) -> 0 <_ j )
536	535	adantl	\|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> 0 <_ j )
537	529	adantl	\|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> j e. RR )
538	215	adantr	\|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> i e. RR )
539		1red	\|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> 1 e. RR )
540	538 539	readdcld	\|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( i + 1 ) e. RR )
541	213	adantr	\|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> N e. RR )
542		elfzle2	\|- ( j e. ( 1 ... ( i + 1 ) ) -> j <_ ( i + 1 ) )
543	542	adantl	\|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> j <_ ( i + 1 ) )
544	301	adantr	\|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( i + 1 ) <_ N )
545	537 540 541 543 544	letrd	\|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> j <_ N )
546	526 527 518 536 545	elfzd	\|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> j e. ( 0 ... N ) )
547	546	adantll	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> j e. ( 0 ... N ) )
548	525 547 355	syl2anc	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( C ` j ) : X --> CC )
549	548	adantlr	\|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( C ` j ) : X --> CC )
550		simplr	\|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> x e. X )
551	549 550	ffvelcdmd	\|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( C ` j ) ` x ) e. CC )
552	234	adantr	\|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> i e. ZZ )
553	552	peano2zd	\|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( i + 1 ) e. ZZ )
554	553 518	zsubcld	\|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - j ) e. ZZ )
555	540 537	subge0d	\|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( 0 <_ ( ( i + 1 ) - j ) <-> j <_ ( i + 1 ) ) )
556	543 555	mpbird	\|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> 0 <_ ( ( i + 1 ) - j ) )
557	540 537	resubcld	\|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - j ) e. RR )
558	557	leidd	\|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - j ) <_ ( ( i + 1 ) - j ) )
559	529 534	elrpd	\|- ( j e. ( 1 ... ( i + 1 ) ) -> j e. RR+ )
560	559	adantl	\|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> j e. RR+ )
561	540 560	ltsubrpd	\|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - j ) < ( i + 1 ) )
562	557 540 541 561 544	ltletrd	\|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - j ) < N )
563	557 557 541 558 562	lelttrd	\|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - j ) < N )
564	557 541 563	ltled	\|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - j ) <_ N )
565	526 527 554 556 564	elfzd	\|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - j ) e. ( 0 ... N ) )
566	565	adantll	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - j ) e. ( 0 ... N ) )
567		nfv	\|- F/ k ( ph /\ ( ( i + 1 ) - j ) e. ( 0 ... N ) )
568		nfcv	\|- F/_ k ( ( i + 1 ) - j )
569	459 568	nffv	\|- F/_ k ( D ` ( ( i + 1 ) - j ) )
570	569 348 349	nff	\|- F/ k ( D ` ( ( i + 1 ) - j ) ) : X --> CC
571	567 570	nfim	\|- F/ k ( ( ph /\ ( ( i + 1 ) - j ) e. ( 0 ... N ) ) -> ( D ` ( ( i + 1 ) - j ) ) : X --> CC )
572		ovex	\|- ( ( i + 1 ) - j ) e. _V
573		eleq1	\|- ( k = ( ( i + 1 ) - j ) -> ( k e. ( 0 ... N ) <-> ( ( i + 1 ) - j ) e. ( 0 ... N ) ) )
574	573	anbi2d	\|- ( k = ( ( i + 1 ) - j ) -> ( ( ph /\ k e. ( 0 ... N ) ) <-> ( ph /\ ( ( i + 1 ) - j ) e. ( 0 ... N ) ) ) )
575		fveq2	\|- ( k = ( ( i + 1 ) - j ) -> ( D ` k ) = ( D ` ( ( i + 1 ) - j ) ) )
576	575	feq1d	\|- ( k = ( ( i + 1 ) - j ) -> ( ( D ` k ) : X --> CC <-> ( D ` ( ( i + 1 ) - j ) ) : X --> CC ) )
577	574 576	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 ) ) )
578	11	a1i	\|- ( ph -> D = ( k e. ( 0 ... N ) \|-> ( ( S Dn G ) ` k ) ) )
579		fvexd	\|- ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( S Dn G ) ` k ) e. _V )
580	578 579	fvmpt2d	\|- ( ( ph /\ k e. ( 0 ... N ) ) -> ( D ` k ) = ( ( S Dn G ) ` k ) )
581	580	feq1d	\|- ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( D ` k ) : X --> CC <-> ( ( S Dn G ) ` k ) : X --> CC ) )
582	9 581	mpbird	\|- ( ( ph /\ k e. ( 0 ... N ) ) -> ( D ` k ) : X --> CC )
583	571 572 577 582	vtoclf	\|- ( ( ph /\ ( ( i + 1 ) - j ) e. ( 0 ... N ) ) -> ( D ` ( ( i + 1 ) - j ) ) : X --> CC )
584	525 566 583	syl2anc	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( D ` ( ( i + 1 ) - j ) ) : X --> CC )
585	584	adantlr	\|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( D ` ( ( i + 1 ) - j ) ) : X --> CC )
586	585 550	ffvelcdmd	\|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... ( i + 1 ) ) ) -> ( ( D ` ( ( i + 1 ) - j ) ) ` x ) e. CC )
587	551 586	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 )
588	524 587	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 )
589		1zzd	\|- ( i e. ( 0 ..^ N ) -> 1 e. ZZ )
590	234	peano2zd	\|- ( i e. ( 0 ..^ N ) -> ( i + 1 ) e. ZZ )
591	492	eqcomi	\|- 1 = ( 0 + 1 )
592	591	a1i	\|- ( i e. ( 0 ..^ N ) -> 1 = ( 0 + 1 ) )
593	173	a1i	\|- ( i e. ( 0 ..^ N ) -> 0 e. RR )
594		1red	\|- ( i e. ( 0 ..^ N ) -> 1 e. RR )
595	187	nn0ge0d	\|- ( i e. ( 0 ..^ N ) -> 0 <_ i )
596	593 215 594 595	leadd1dd	\|- ( i e. ( 0 ..^ N ) -> ( 0 + 1 ) <_ ( i + 1 ) )
597	592 596	eqbrtrd	\|- ( i e. ( 0 ..^ N ) -> 1 <_ ( i + 1 ) )
598	589 590 597	3jca	\|- ( i e. ( 0 ..^ N ) -> ( 1 e. ZZ /\ ( i + 1 ) e. ZZ /\ 1 <_ ( i + 1 ) ) )
599		eluz2	\|- ( ( i + 1 ) e. ( ZZ>= ` 1 ) <-> ( 1 e. ZZ /\ ( i + 1 ) e. ZZ /\ 1 <_ ( i + 1 ) ) )
600	598 599	sylibr	\|- ( i e. ( 0 ..^ N ) -> ( i + 1 ) e. ( ZZ>= ` 1 ) )
601		eluzfz2	\|- ( ( i + 1 ) e. ( ZZ>= ` 1 ) -> ( i + 1 ) e. ( 1 ... ( i + 1 ) ) )
602	600 601	syl	\|- ( i e. ( 0 ..^ N ) -> ( i + 1 ) e. ( 1 ... ( i + 1 ) ) )
603	602	ad2antlr	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( i + 1 ) e. ( 1 ... ( i + 1 ) ) )
604		oveq1	\|- ( j = ( i + 1 ) -> ( j - 1 ) = ( ( i + 1 ) - 1 ) )
605	604	oveq2d	\|- ( j = ( i + 1 ) -> ( i _C ( j - 1 ) ) = ( i _C ( ( i + 1 ) - 1 ) ) )
606		fveq2	\|- ( j = ( i + 1 ) -> ( C ` j ) = ( C ` ( i + 1 ) ) )
607	606	fveq1d	\|- ( j = ( i + 1 ) -> ( ( C ` j ) ` x ) = ( ( C ` ( i + 1 ) ) ` x ) )
608		oveq2	\|- ( j = ( i + 1 ) -> ( ( i + 1 ) - j ) = ( ( i + 1 ) - ( i + 1 ) ) )
609	608	fveq2d	\|- ( j = ( i + 1 ) -> ( D ` ( ( i + 1 ) - j ) ) = ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) )
610	609	fveq1d	\|- ( j = ( i + 1 ) -> ( ( D ` ( ( i + 1 ) - j ) ) ` x ) = ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) )
611	607 610	oveq12d	\|- ( j = ( i + 1 ) -> ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) = ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) )
612	605 611	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 ) ) ) )
613	514 515 516 588 603 612	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 ) ) ) ) )
614		1cnd	\|- ( i e. ( 0 ..^ N ) -> 1 e. CC )
615	503 614	pncand	\|- ( i e. ( 0 ..^ N ) -> ( ( i + 1 ) - 1 ) = i )
616	615	oveq2d	\|- ( i e. ( 0 ..^ N ) -> ( i _C ( ( i + 1 ) - 1 ) ) = ( i _C i ) )
617		bcnn	\|- ( i e. NN0 -> ( i _C i ) = 1 )
618	187 617	syl	\|- ( i e. ( 0 ..^ N ) -> ( i _C i ) = 1 )
619	616 618	eqtrd	\|- ( i e. ( 0 ..^ N ) -> ( i _C ( ( i + 1 ) - 1 ) ) = 1 )
620	503 614	addcld	\|- ( i e. ( 0 ..^ N ) -> ( i + 1 ) e. CC )
621	620	subidd	\|- ( i e. ( 0 ..^ N ) -> ( ( i + 1 ) - ( i + 1 ) ) = 0 )
622	621	fveq2d	\|- ( i e. ( 0 ..^ N ) -> ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) = ( D ` 0 ) )
623	622	fveq1d	\|- ( i e. ( 0 ..^ N ) -> ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) = ( ( D ` 0 ) ` x ) )
624	623	oveq2d	\|- ( i e. ( 0 ..^ N ) -> ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) = ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) )
625	619 624	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 ) ) ) )
626	625	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 ) ) ) )
627		simpl	\|- ( ( ph /\ i e. ( 0 ..^ N ) ) -> ph )
628		fzofzp1	\|- ( i e. ( 0 ..^ N ) -> ( i + 1 ) e. ( 0 ... N ) )
629	628	adantl	\|- ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( i + 1 ) e. ( 0 ... N ) )
630		nfv	\|- F/ k ( ph /\ ( i + 1 ) e. ( 0 ... N ) )
631		nfcv	\|- F/_ k ( i + 1 )
632	345 631	nffv	\|- F/_ k ( C ` ( i + 1 ) )
633	632 348 349	nff	\|- F/ k ( C ` ( i + 1 ) ) : X --> CC
634	630 633	nfim	\|- F/ k ( ( ph /\ ( i + 1 ) e. ( 0 ... N ) ) -> ( C ` ( i + 1 ) ) : X --> CC )
635		ovex	\|- ( i + 1 ) e. _V
636		eleq1	\|- ( k = ( i + 1 ) -> ( k e. ( 0 ... N ) <-> ( i + 1 ) e. ( 0 ... N ) ) )
637	636	anbi2d	\|- ( k = ( i + 1 ) -> ( ( ph /\ k e. ( 0 ... N ) ) <-> ( ph /\ ( i + 1 ) e. ( 0 ... N ) ) ) )
638		fveq2	\|- ( k = ( i + 1 ) -> ( C ` k ) = ( C ` ( i + 1 ) ) )
639	638	feq1d	\|- ( k = ( i + 1 ) -> ( ( C ` k ) : X --> CC <-> ( C ` ( i + 1 ) ) : X --> CC ) )
640	637 639	imbi12d	\|- ( k = ( i + 1 ) -> ( ( ( ph /\ k e. ( 0 ... N ) ) -> ( C ` k ) : X --> CC ) <-> ( ( ph /\ ( i + 1 ) e. ( 0 ... N ) ) -> ( C ` ( i + 1 ) ) : X --> CC ) ) )
641	634 635 640 229	vtoclf	\|- ( ( ph /\ ( i + 1 ) e. ( 0 ... N ) ) -> ( C ` ( i + 1 ) ) : X --> CC )
642	627 629 641	syl2anc	\|- ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( C ` ( i + 1 ) ) : X --> CC )
643	642	ffvelcdmda	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( C ` ( i + 1 ) ) ` x ) e. CC )
644		nfv	\|- F/ k ( ph /\ 0 e. ( 0 ... N ) )
645		nfcv	\|- F/_ k 0
646	459 645	nffv	\|- F/_ k ( D ` 0 )
647	646 348 349	nff	\|- F/ k ( D ` 0 ) : X --> CC
648	644 647	nfim	\|- F/ k ( ( ph /\ 0 e. ( 0 ... N ) ) -> ( D ` 0 ) : X --> CC )
649		c0ex	\|- 0 e. _V
650		eleq1	\|- ( k = 0 -> ( k e. ( 0 ... N ) <-> 0 e. ( 0 ... N ) ) )
651	650	anbi2d	\|- ( k = 0 -> ( ( ph /\ k e. ( 0 ... N ) ) <-> ( ph /\ 0 e. ( 0 ... N ) ) ) )
652		fveq2	\|- ( k = 0 -> ( D ` k ) = ( D ` 0 ) )
653	652	feq1d	\|- ( k = 0 -> ( ( D ` k ) : X --> CC <-> ( D ` 0 ) : X --> CC ) )
654	651 653	imbi12d	\|- ( k = 0 -> ( ( ( ph /\ k e. ( 0 ... N ) ) -> ( D ` k ) : X --> CC ) <-> ( ( ph /\ 0 e. ( 0 ... N ) ) -> ( D ` 0 ) : X --> CC ) ) )
655	648 649 654 582	vtoclf	\|- ( ( ph /\ 0 e. ( 0 ... N ) ) -> ( D ` 0 ) : X --> CC )
656	12 117 655	syl2anc	\|- ( ph -> ( D ` 0 ) : X --> CC )
657	656	adantr	\|- ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( D ` 0 ) : X --> CC )
658	657	ffvelcdmda	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( D ` 0 ) ` x ) e. CC )
659	643 658	mulcld	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` 0 ) ` x ) ) e. CC )
660	659	mullidd	\|- ( ( ( 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 ) ) )
661	626 660	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 ) ) )
662		1m1e0	\|- ( 1 - 1 ) = 0
663	662	fveq2i	\|- ( ZZ>= ` ( 1 - 1 ) ) = ( ZZ>= ` 0 )
664	13	eqcomi	\|- ( ZZ>= ` 0 ) = NN0
665	663 664	eqtr2i	\|- NN0 = ( ZZ>= ` ( 1 - 1 ) )
666	665	a1i	\|- ( i e. ( 0 ..^ N ) -> NN0 = ( ZZ>= ` ( 1 - 1 ) ) )
667	187 666	eleqtrd	\|- ( i e. ( 0 ..^ N ) -> i e. ( ZZ>= ` ( 1 - 1 ) ) )
668		fzdifsuc2	\|- ( i e. ( ZZ>= ` ( 1 - 1 ) ) -> ( 1 ... i ) = ( ( 1 ... ( i + 1 ) ) \ { ( i + 1 ) } ) )
669	667 668	syl	\|- ( i e. ( 0 ..^ N ) -> ( 1 ... i ) = ( ( 1 ... ( i + 1 ) ) \ { ( i + 1 ) } ) )
670	669	eqcomd	\|- ( i e. ( 0 ..^ N ) -> ( ( 1 ... ( i + 1 ) ) \ { ( i + 1 ) } ) = ( 1 ... i ) )
671	670	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 ) ) ) )
672	671	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 ) ) ) )
673	661 672	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 ) ) ) ) )
674	513 613 673	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 ) ) ) ) )
675	491 495 674	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 ) ) ) ) )
676		nfcv	\|- F/_ k ( i _C 0 )
677	345 645	nffv	\|- F/_ k ( C ` 0 )
678	677 456	nffv	\|- F/_ k ( ( C ` 0 ) ` x )
679		nfcv	\|- F/_ k ( ( i + 1 ) - 0 )
680	459 679	nffv	\|- F/_ k ( D ` ( ( i + 1 ) - 0 ) )
681	680 456	nffv	\|- F/_ k ( ( D ` ( ( i + 1 ) - 0 ) ) ` x )
682	678 453 681	nfov	\|- F/_ k ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) )
683	676 453 682	nfov	\|- F/_ k ( ( i _C 0 ) x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) ) )
684	664	a1i	\|- ( i e. ( 0 ..^ N ) -> ( ZZ>= ` 0 ) = NN0 )
685	187 684	eleqtrrd	\|- ( i e. ( 0 ..^ N ) -> i e. ( ZZ>= ` 0 ) )
686		eluzfz1	\|- ( i e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... i ) )
687	685 686	syl	\|- ( i e. ( 0 ..^ N ) -> 0 e. ( 0 ... i ) )
688	687	ad2antlr	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> 0 e. ( 0 ... i ) )
689		oveq2	\|- ( k = 0 -> ( i _C k ) = ( i _C 0 ) )
690	110	fveq1d	\|- ( k = 0 -> ( ( C ` k ) ` x ) = ( ( C ` 0 ) ` x ) )
691		oveq2	\|- ( k = 0 -> ( ( i + 1 ) - k ) = ( ( i + 1 ) - 0 ) )
692	691	fveq2d	\|- ( k = 0 -> ( D ` ( ( i + 1 ) - k ) ) = ( D ` ( ( i + 1 ) - 0 ) ) )
693	692	fveq1d	\|- ( k = 0 -> ( ( D ` ( ( i + 1 ) - k ) ) ` x ) = ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) )
694	690 693	oveq12d	\|- ( k = 0 -> ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) = ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) ) )
695	689 694	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 ) ) ) )
696	470 683 439 441 688 695	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 ) ) ) ) )
697	620	subid1d	\|- ( i e. ( 0 ..^ N ) -> ( ( i + 1 ) - 0 ) = ( i + 1 ) )
698	697	fveq2d	\|- ( i e. ( 0 ..^ N ) -> ( D ` ( ( i + 1 ) - 0 ) ) = ( D ` ( i + 1 ) ) )
699	698	fveq1d	\|- ( i e. ( 0 ..^ N ) -> ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) = ( ( D ` ( i + 1 ) ) ` x ) )
700	699	oveq2d	\|- ( i e. ( 0 ..^ N ) -> ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) ) = ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) )
701	700	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 ) ) ) )
702	701	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 ) ) ) ) )
703	702	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 ) ) ) ) )
704		bcn0	\|- ( i e. NN0 -> ( i _C 0 ) = 1 )
705	187 704	syl	\|- ( i e. ( 0 ..^ N ) -> ( i _C 0 ) = 1 )
706	705	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 ) ) ) )
707	706	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 ) ) ) )
708	677 348 349	nff	\|- F/ k ( C ` 0 ) : X --> CC
709	644 708	nfim	\|- F/ k ( ( ph /\ 0 e. ( 0 ... N ) ) -> ( C ` 0 ) : X --> CC )
710	110	feq1d	\|- ( k = 0 -> ( ( C ` k ) : X --> CC <-> ( C ` 0 ) : X --> CC ) )
711	651 710	imbi12d	\|- ( k = 0 -> ( ( ( ph /\ k e. ( 0 ... N ) ) -> ( C ` k ) : X --> CC ) <-> ( ( ph /\ 0 e. ( 0 ... N ) ) -> ( C ` 0 ) : X --> CC ) ) )
712	709 649 711 229	vtoclf	\|- ( ( ph /\ 0 e. ( 0 ... N ) ) -> ( C ` 0 ) : X --> CC )
713	12 117 712	syl2anc	\|- ( ph -> ( C ` 0 ) : X --> CC )
714	713	adantr	\|- ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( C ` 0 ) : X --> CC )
715	714	ffvelcdmda	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( C ` 0 ) ` x ) e. CC )
716	459 631	nffv	\|- F/_ k ( D ` ( i + 1 ) )
717	716 348 349	nff	\|- F/ k ( D ` ( i + 1 ) ) : X --> CC
718	630 717	nfim	\|- F/ k ( ( ph /\ ( i + 1 ) e. ( 0 ... N ) ) -> ( D ` ( i + 1 ) ) : X --> CC )
719		fveq2	\|- ( k = ( i + 1 ) -> ( D ` k ) = ( D ` ( i + 1 ) ) )
720	719	feq1d	\|- ( k = ( i + 1 ) -> ( ( D ` k ) : X --> CC <-> ( D ` ( i + 1 ) ) : X --> CC ) )
721	637 720	imbi12d	\|- ( k = ( i + 1 ) -> ( ( ( ph /\ k e. ( 0 ... N ) ) -> ( D ` k ) : X --> CC ) <-> ( ( ph /\ ( i + 1 ) e. ( 0 ... N ) ) -> ( D ` ( i + 1 ) ) : X --> CC ) ) )
722	718 635 721 582	vtoclf	\|- ( ( ph /\ ( i + 1 ) e. ( 0 ... N ) ) -> ( D ` ( i + 1 ) ) : X --> CC )
723	627 629 722	syl2anc	\|- ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( D ` ( i + 1 ) ) : X --> CC )
724	723	ffvelcdmda	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( D ` ( i + 1 ) ) ` x ) e. CC )
725	715 724	mulcld	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( i + 1 ) ) ` x ) ) e. CC )
726	725	mullidd	\|- ( ( ( 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 ) ) )
727	707 726	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 ) ) )
728		nfv	\|- F/ j i e. ( 0 ..^ N )
729		1zzd	\|- ( ( i e. ( 0 ..^ N ) /\ j e. ( ( 0 ... i ) \ { 0 } ) ) -> 1 e. ZZ )
730	234	adantr	\|- ( ( i e. ( 0 ..^ N ) /\ j e. ( ( 0 ... i ) \ { 0 } ) ) -> i e. ZZ )
731		eldifi	\|- ( j e. ( ( 0 ... i ) \ { 0 } ) -> j e. ( 0 ... i ) )
732		elfzelz	\|- ( j e. ( 0 ... i ) -> j e. ZZ )
733	731 732	syl	\|- ( j e. ( ( 0 ... i ) \ { 0 } ) -> j e. ZZ )
734	733	adantl	\|- ( ( i e. ( 0 ..^ N ) /\ j e. ( ( 0 ... i ) \ { 0 } ) ) -> j e. ZZ )
735		elfznn0	\|- ( j e. ( 0 ... i ) -> j e. NN0 )
736	731 735	syl	\|- ( j e. ( ( 0 ... i ) \ { 0 } ) -> j e. NN0 )
737		eldifsni	\|- ( j e. ( ( 0 ... i ) \ { 0 } ) -> j =/= 0 )
738	736 737	jca	\|- ( j e. ( ( 0 ... i ) \ { 0 } ) -> ( j e. NN0 /\ j =/= 0 ) )
739		elnnne0	\|- ( j e. NN <-> ( j e. NN0 /\ j =/= 0 ) )
740	738 739	sylibr	\|- ( j e. ( ( 0 ... i ) \ { 0 } ) -> j e. NN )
741		nnge1	\|- ( j e. NN -> 1 <_ j )
742	740 741	syl	\|- ( j e. ( ( 0 ... i ) \ { 0 } ) -> 1 <_ j )
743	742	adantl	\|- ( ( i e. ( 0 ..^ N ) /\ j e. ( ( 0 ... i ) \ { 0 } ) ) -> 1 <_ j )
744		elfzle2	\|- ( j e. ( 0 ... i ) -> j <_ i )
745	731 744	syl	\|- ( j e. ( ( 0 ... i ) \ { 0 } ) -> j <_ i )
746	745	adantl	\|- ( ( i e. ( 0 ..^ N ) /\ j e. ( ( 0 ... i ) \ { 0 } ) ) -> j <_ i )
747	729 730 734 743 746	elfzd	\|- ( ( i e. ( 0 ..^ N ) /\ j e. ( ( 0 ... i ) \ { 0 } ) ) -> j e. ( 1 ... i ) )
748	747	ex	\|- ( i e. ( 0 ..^ N ) -> ( j e. ( ( 0 ... i ) \ { 0 } ) -> j e. ( 1 ... i ) ) )
749		0zd	\|- ( j e. ( 1 ... i ) -> 0 e. ZZ )
750		elfzel2	\|- ( j e. ( 1 ... i ) -> i e. ZZ )
751		elfzelz	\|- ( j e. ( 1 ... i ) -> j e. ZZ )
752	173	a1i	\|- ( j e. ( 1 ... i ) -> 0 e. RR )
753	751	zred	\|- ( j e. ( 1 ... i ) -> j e. RR )
754		1red	\|- ( j e. ( 1 ... i ) -> 1 e. RR )
755	531	a1i	\|- ( j e. ( 1 ... i ) -> 0 < 1 )
756		elfzle1	\|- ( j e. ( 1 ... i ) -> 1 <_ j )
757	752 754 753 755 756	ltletrd	\|- ( j e. ( 1 ... i ) -> 0 < j )
758	752 753 757	ltled	\|- ( j e. ( 1 ... i ) -> 0 <_ j )
759		elfzle2	\|- ( j e. ( 1 ... i ) -> j <_ i )
760	749 750 751 758 759	elfzd	\|- ( j e. ( 1 ... i ) -> j e. ( 0 ... i ) )
761	752 757	gtned	\|- ( j e. ( 1 ... i ) -> j =/= 0 )
762		nelsn	\|- ( j =/= 0 -> -. j e. { 0 } )
763	761 762	syl	\|- ( j e. ( 1 ... i ) -> -. j e. { 0 } )
764	760 763	eldifd	\|- ( j e. ( 1 ... i ) -> j e. ( ( 0 ... i ) \ { 0 } ) )
765	764	adantl	\|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... i ) ) -> j e. ( ( 0 ... i ) \ { 0 } ) )
766	765	ex	\|- ( i e. ( 0 ..^ N ) -> ( j e. ( 1 ... i ) -> j e. ( ( 0 ... i ) \ { 0 } ) ) )
767	748 766	impbid	\|- ( i e. ( 0 ..^ N ) -> ( j e. ( ( 0 ... i ) \ { 0 } ) <-> j e. ( 1 ... i ) ) )
768	728 767	alrimi	\|- ( i e. ( 0 ..^ N ) -> A. j ( j e. ( ( 0 ... i ) \ { 0 } ) <-> j e. ( 1 ... i ) ) )
769		dfcleq	\|- ( ( ( 0 ... i ) \ { 0 } ) = ( 1 ... i ) <-> A. j ( j e. ( ( 0 ... i ) \ { 0 } ) <-> j e. ( 1 ... i ) ) )
770	768 769	sylibr	\|- ( i e. ( 0 ..^ N ) -> ( ( 0 ... i ) \ { 0 } ) = ( 1 ... i ) )
771	770	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 ) ) ) )
772	771	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 ) ) ) )
773	727 772	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 ) ) ) ) )
774	696 703 773	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 ) ) ) ) )
775	675 774	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 ) ) ) ) ) )
776		fzfid	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( 1 ... i ) e. Fin )
777	187	adantr	\|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... i ) ) -> i e. NN0 )
778	765 733	syl	\|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... i ) ) -> j e. ZZ )
779		1zzd	\|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... i ) ) -> 1 e. ZZ )
780	778 779	zsubcld	\|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... i ) ) -> ( j - 1 ) e. ZZ )
781	777 780	bccld	\|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... i ) ) -> ( i _C ( j - 1 ) ) e. NN0 )
782	781	nn0cnd	\|- ( ( i e. ( 0 ..^ N ) /\ j e. ( 1 ... i ) ) -> ( i _C ( j - 1 ) ) e. CC )
783	782	adantll	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ j e. ( 1 ... i ) ) -> ( i _C ( j - 1 ) ) e. CC )
784	783	adantlr	\|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... i ) ) -> ( i _C ( j - 1 ) ) e. CC )
785		simpl	\|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... i ) ) -> ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) )
786		fzelp1	\|- ( j e. ( 1 ... i ) -> j e. ( 1 ... ( i + 1 ) ) )
787	786	adantl	\|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... i ) ) -> j e. ( 1 ... ( i + 1 ) ) )
788	785 787 551	syl2anc	\|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... i ) ) -> ( ( C ` j ) ` x ) e. CC )
789	787 586	syldan	\|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... i ) ) -> ( ( D ` ( ( i + 1 ) - j ) ) ` x ) e. CC )
790	788 789	mulcld	\|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ j e. ( 1 ... i ) ) -> ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) e. CC )
791	784 790	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 )
792	776 791	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 )
793	187	adantr	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> i e. NN0 )
794		elfzelz	\|- ( k e. ( 1 ... i ) -> k e. ZZ )
795	794	adantl	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> k e. ZZ )
796	793 795	bccld	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> ( i _C k ) e. NN0 )
797	796	nn0cnd	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> ( i _C k ) e. CC )
798	797	adantll	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 1 ... i ) ) -> ( i _C k ) e. CC )
799	798	adantlr	\|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 1 ... i ) ) -> ( i _C k ) e. CC )
800		simpll	\|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 1 ... i ) ) -> ( ph /\ i e. ( 0 ..^ N ) ) )
801		simplr	\|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 1 ... i ) ) -> x e. X )
802	760	ssriv	\|- ( 1 ... i ) C_ ( 0 ... i )
803		id	\|- ( k e. ( 1 ... i ) -> k e. ( 1 ... i ) )
804	802 803	sselid	\|- ( k e. ( 1 ... i ) -> k e. ( 0 ... i ) )
805	804	adantl	\|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 1 ... i ) ) -> k e. ( 0 ... i ) )
806	800 801 805 433	syl21anc	\|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 1 ... i ) ) -> ( ( C ` k ) ` x ) e. CC )
807	805 435	syldan	\|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 1 ... i ) ) -> ( ( D ` ( ( i + 1 ) - k ) ) ` x ) e. CC )
808	806 807	mulcld	\|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 1 ... i ) ) -> ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) e. CC )
809	799 808	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 )
810	776 809	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 )
811	659 792 725 810	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 ) ) ) ) ) )
812		oveq1	\|- ( j = k -> ( j - 1 ) = ( k - 1 ) )
813	812	oveq2d	\|- ( j = k -> ( i _C ( j - 1 ) ) = ( i _C ( k - 1 ) ) )
814		fveq2	\|- ( j = k -> ( C ` j ) = ( C ` k ) )
815	814	fveq1d	\|- ( j = k -> ( ( C ` j ) ` x ) = ( ( C ` k ) ` x ) )
816		oveq2	\|- ( j = k -> ( ( i + 1 ) - j ) = ( ( i + 1 ) - k ) )
817	816	fveq2d	\|- ( j = k -> ( D ` ( ( i + 1 ) - j ) ) = ( D ` ( ( i + 1 ) - k ) ) )
818	817	fveq1d	\|- ( j = k -> ( ( D ` ( ( i + 1 ) - j ) ) ` x ) = ( ( D ` ( ( i + 1 ) - k ) ) ` x ) )
819	815 818	oveq12d	\|- ( j = k -> ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) = ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) )
820	813 819	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 ) ) ) )
821		nfcv	\|- F/_ k ( i _C ( j - 1 ) )
822	347 456	nffv	\|- F/_ k ( ( C ` j ) ` x )
823	569 456	nffv	\|- F/_ k ( ( D ` ( ( i + 1 ) - j ) ) ` x )
824	822 453 823	nfov	\|- F/_ k ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) )
825	821 453 824	nfov	\|- F/_ k ( ( i _C ( j - 1 ) ) x. ( ( ( C ` j ) ` x ) x. ( ( D ` ( ( i + 1 ) - j ) ) ` x ) ) )
826		nfcv	\|- F/_ j ( ( i _C ( k - 1 ) ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) )
827	820 825 826	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 ) ) )
828	827	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 ) ) ) )
829	828	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 ) ) ) ) )
830		peano2zm	\|- ( k e. ZZ -> ( k - 1 ) e. ZZ )
831	795 830	syl	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> ( k - 1 ) e. ZZ )
832	793 831	bccld	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> ( i _C ( k - 1 ) ) e. NN0 )
833	832	nn0cnd	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> ( i _C ( k - 1 ) ) e. CC )
834	833	adantll	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 1 ... i ) ) -> ( i _C ( k - 1 ) ) e. CC )
835	834	adantlr	\|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 1 ... i ) ) -> ( i _C ( k - 1 ) ) e. CC )
836	835 808	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 )
837	776 836 809	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 ) ) ) ) )
838	837	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 ) ) ) ) )
839	833 797	addcomd	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> ( ( i _C ( k - 1 ) ) + ( i _C k ) ) = ( ( i _C k ) + ( i _C ( k - 1 ) ) ) )
840		bcpasc	\|- ( ( i e. NN0 /\ k e. ZZ ) -> ( ( i _C k ) + ( i _C ( k - 1 ) ) ) = ( ( i + 1 ) _C k ) )
841	793 795 840	syl2anc	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> ( ( i _C k ) + ( i _C ( k - 1 ) ) ) = ( ( i + 1 ) _C k ) )
842	839 841	eqtr2d	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> ( ( i + 1 ) _C k ) = ( ( i _C ( k - 1 ) ) + ( i _C k ) ) )
843	842	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 ) ) ) )
844	843	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 ) ) ) )
845	844	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 ) ) ) )
846	835 799 808	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 ) ) ) ) )
847	845 846	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 ) ) ) )
848	847	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 ) ) ) )
849	829 838 848	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 ) ) ) )
850	849	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 ) ) ) ) )
851		peano2nn0	\|- ( i e. NN0 -> ( i + 1 ) e. NN0 )
852	793 851	syl	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> ( i + 1 ) e. NN0 )
853	852 795	bccld	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> ( ( i + 1 ) _C k ) e. NN0 )
854	853	nn0cnd	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 1 ... i ) ) -> ( ( i + 1 ) _C k ) e. CC )
855	854	adantll	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 1 ... i ) ) -> ( ( i + 1 ) _C k ) e. CC )
856	855	adantlr	\|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 1 ... i ) ) -> ( ( i + 1 ) _C k ) e. CC )
857	856 808	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 )
858	776 857	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 )
859	659 725 858	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 ) ) ) ) ) )
860	187 851	syl	\|- ( i e. ( 0 ..^ N ) -> ( i + 1 ) e. NN0 )
861		bcn0	\|- ( ( i + 1 ) e. NN0 -> ( ( i + 1 ) _C 0 ) = 1 )
862	860 861	syl	\|- ( i e. ( 0 ..^ N ) -> ( ( i + 1 ) _C 0 ) = 1 )
863	862 700	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 ) ) ) )
864	863	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 ) ) ) )
865	864 726	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 ) ) ) )
866	770	ad2antlr	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( 0 ... i ) \ { 0 } ) = ( 1 ... i ) )
867	866	eqcomd	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( 1 ... i ) = ( ( 0 ... i ) \ { 0 } ) )
868	867	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 ) ) ) )
869	865 868	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 ) ) ) ) )
870		nfcv	\|- F/_ k ( ( i + 1 ) _C 0 )
871	870 453 682	nfov	\|- F/_ k ( ( ( i + 1 ) _C 0 ) x. ( ( ( C ` 0 ) ` x ) x. ( ( D ` ( ( i + 1 ) - 0 ) ) ` x ) ) )
872	199 851	syl	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( i + 1 ) e. NN0 )
873	872 201	bccld	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( ( i + 1 ) _C k ) e. NN0 )
874	873	nn0cnd	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... i ) ) -> ( ( i + 1 ) _C k ) e. CC )
875	874	adantll	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( i + 1 ) _C k ) e. CC )
876	875	adantlr	\|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... i ) ) -> ( ( i + 1 ) _C k ) e. CC )
877	876 436	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 )
878		oveq2	\|- ( k = 0 -> ( ( i + 1 ) _C k ) = ( ( i + 1 ) _C 0 ) )
879	878 694	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 ) ) ) )
880	470 871 439 877 688 879	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 ) ) ) ) )
881	880	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 ) ) ) )
882	869 881	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 ) ) ) )
883	882	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 ) ) ) ) )
884		bcnn	\|- ( ( i + 1 ) e. NN0 -> ( ( i + 1 ) _C ( i + 1 ) ) = 1 )
885	860 884	syl	\|- ( i e. ( 0 ..^ N ) -> ( ( i + 1 ) _C ( i + 1 ) ) = 1 )
886	885	ad2antlr	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( i + 1 ) _C ( i + 1 ) ) = 1 )
887	886	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 ) ) ) )
888	622	adantl	\|- ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) = ( D ` 0 ) )
889	888	feq1d	\|- ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) : X --> CC <-> ( D ` 0 ) : X --> CC ) )
890	657 889	mpbird	\|- ( ( ph /\ i e. ( 0 ..^ N ) ) -> ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) : X --> CC )
891	890	adantr	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) : X --> CC )
892		simpr	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> x e. X )
893	891 892	ffvelcdmd	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) e. CC )
894	643 893	mulcld	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) e. CC )
895	894	mullidd	\|- ( ( ( 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 ) ) )
896	624	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 ) ) )
897	887 895 896	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 ) ) ) )
898		fzdifsuc	\|- ( i e. ( ZZ>= ` 0 ) -> ( 0 ... i ) = ( ( 0 ... ( i + 1 ) ) \ { ( i + 1 ) } ) )
899	685 898	syl	\|- ( i e. ( 0 ..^ N ) -> ( 0 ... i ) = ( ( 0 ... ( i + 1 ) ) \ { ( i + 1 ) } ) )
900	899	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 ) ) ) )
901	900	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 ) ) ) )
902	897 901	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 ) ) ) ) )
903		nfcv	\|- F/_ k ( ( i + 1 ) _C ( i + 1 ) )
904	632 456	nffv	\|- F/_ k ( ( C ` ( i + 1 ) ) ` x )
905		nfcv	\|- F/_ k ( ( i + 1 ) - ( i + 1 ) )
906	459 905	nffv	\|- F/_ k ( D ` ( ( i + 1 ) - ( i + 1 ) ) )
907	906 456	nffv	\|- F/_ k ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x )
908	904 453 907	nfov	\|- F/_ k ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) )
909	903 453 908	nfov	\|- F/_ k ( ( ( i + 1 ) _C ( i + 1 ) ) x. ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) )
910		fzfid	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( 0 ... ( i + 1 ) ) e. Fin )
911	860	adantr	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( i + 1 ) e. NN0 )
912		elfzelz	\|- ( k e. ( 0 ... ( i + 1 ) ) -> k e. ZZ )
913	912	adantl	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> k e. ZZ )
914	911 913	bccld	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( i + 1 ) _C k ) e. NN0 )
915	914	nn0cnd	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( i + 1 ) _C k ) e. CC )
916	915	adantll	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( i + 1 ) _C k ) e. CC )
917	916	adantlr	\|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( i + 1 ) _C k ) e. CC )
918	627	adantr	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ph )
919	96	a1i	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> 0 e. ZZ )
920	208	adantr	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> N e. ZZ )
921		elfzle1	\|- ( k e. ( 0 ... ( i + 1 ) ) -> 0 <_ k )
922	921	adantl	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> 0 <_ k )
923	913	zred	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> k e. RR )
924	911	nn0red	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( i + 1 ) e. RR )
925	213	adantr	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> N e. RR )
926		elfzle2	\|- ( k e. ( 0 ... ( i + 1 ) ) -> k <_ ( i + 1 ) )
927	926	adantl	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> k <_ ( i + 1 ) )
928	301	adantr	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( i + 1 ) <_ N )
929	923 924 925 927 928	letrd	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> k <_ N )
930	919 920 913 922 929	elfzd	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> k e. ( 0 ... N ) )
931	930	adantll	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> k e. ( 0 ... N ) )
932	918 931 229	syl2anc	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( C ` k ) : X --> CC )
933	932	adantlr	\|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( C ` k ) : X --> CC )
934		simplr	\|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> x e. X )
935	933 934	ffvelcdmd	\|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( C ` k ) ` x ) e. CC )
936	918	adantlr	\|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ph )
937	590	adantr	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( i + 1 ) e. ZZ )
938	937 913	zsubcld	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - k ) e. ZZ )
939	924 923	subge0d	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( 0 <_ ( ( i + 1 ) - k ) <-> k <_ ( i + 1 ) ) )
940	927 939	mpbird	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> 0 <_ ( ( i + 1 ) - k ) )
941	924 923	resubcld	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - k ) e. RR )
942	925 923	resubcld	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( N - k ) e. RR )
943	925 173 247	sylancl	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( N - 0 ) e. RR )
944	924 925 923 928	lesub1dd	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - k ) <_ ( N - k ) )
945	173	a1i	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> 0 e. RR )
946	945 923 925 922	lesub2dd	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( N - k ) <_ ( N - 0 ) )
947	941 942 943 944 946	letrd	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - k ) <_ ( N - 0 ) )
948	253	adantr	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( N - 0 ) = N )
949	947 948	breqtrd	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - k ) <_ N )
950	919 920 938 940 949	elfzd	\|- ( ( i e. ( 0 ..^ N ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - k ) e. ( 0 ... N ) )
951	950	adantll	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - k ) e. ( 0 ... N ) )
952	951	adantlr	\|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( i + 1 ) - k ) e. ( 0 ... N ) )
953		fveq2	\|- ( j = ( ( i + 1 ) - k ) -> ( D ` j ) = ( D ` ( ( i + 1 ) - k ) ) )
954	953	feq1d	\|- ( j = ( ( i + 1 ) - k ) -> ( ( D ` j ) : X --> CC <-> ( D ` ( ( i + 1 ) - k ) ) : X --> CC ) )
955	310 954	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 ) ) )
956	459 346	nffv	\|- F/_ k ( D ` j )
957	956 348 349	nff	\|- F/ k ( D ` j ) : X --> CC
958	343 957	nfim	\|- F/ k ( ( ph /\ j e. ( 0 ... N ) ) -> ( D ` j ) : X --> CC )
959		fveq2	\|- ( k = j -> ( D ` k ) = ( D ` j ) )
960	959	feq1d	\|- ( k = j -> ( ( D ` k ) : X --> CC <-> ( D ` j ) : X --> CC ) )
961	267 960	imbi12d	\|- ( k = j -> ( ( ( ph /\ k e. ( 0 ... N ) ) -> ( D ` k ) : X --> CC ) <-> ( ( ph /\ j e. ( 0 ... N ) ) -> ( D ` j ) : X --> CC ) ) )
962	958 961 582	chvarfv	\|- ( ( ph /\ j e. ( 0 ... N ) ) -> ( D ` j ) : X --> CC )
963	308 955 962	vtocl	\|- ( ( ph /\ ( ( i + 1 ) - k ) e. ( 0 ... N ) ) -> ( D ` ( ( i + 1 ) - k ) ) : X --> CC )
964	936 952 963	syl2anc	\|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( D ` ( ( i + 1 ) - k ) ) : X --> CC )
965	964 934	ffvelcdmd	\|- ( ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( D ` ( ( i + 1 ) - k ) ) ` x ) e. CC )
966	935 965	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 )
967	917 966	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 )
968	860 684	eleqtrrd	\|- ( i e. ( 0 ..^ N ) -> ( i + 1 ) e. ( ZZ>= ` 0 ) )
969		eluzfz2	\|- ( ( i + 1 ) e. ( ZZ>= ` 0 ) -> ( i + 1 ) e. ( 0 ... ( i + 1 ) ) )
970	968 969	syl	\|- ( i e. ( 0 ..^ N ) -> ( i + 1 ) e. ( 0 ... ( i + 1 ) ) )
971	970	ad2antlr	\|- ( ( ( ph /\ i e. ( 0 ..^ N ) ) /\ x e. X ) -> ( i + 1 ) e. ( 0 ... ( i + 1 ) ) )
972		oveq2	\|- ( k = ( i + 1 ) -> ( ( i + 1 ) _C k ) = ( ( i + 1 ) _C ( i + 1 ) ) )
973	638	fveq1d	\|- ( k = ( i + 1 ) -> ( ( C ` k ) ` x ) = ( ( C ` ( i + 1 ) ) ` x ) )
974		oveq2	\|- ( k = ( i + 1 ) -> ( ( i + 1 ) - k ) = ( ( i + 1 ) - ( i + 1 ) ) )
975	974	fveq2d	\|- ( k = ( i + 1 ) -> ( D ` ( ( i + 1 ) - k ) ) = ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) )
976	975	fveq1d	\|- ( k = ( i + 1 ) -> ( ( D ` ( ( i + 1 ) - k ) ) ` x ) = ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) )
977	973 976	oveq12d	\|- ( k = ( i + 1 ) -> ( ( ( C ` k ) ` x ) x. ( ( D ` ( ( i + 1 ) - k ) ) ` x ) ) = ( ( ( C ` ( i + 1 ) ) ` x ) x. ( ( D ` ( ( i + 1 ) - ( i + 1 ) ) ) ` x ) ) )
978	972 977	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 ) ) ) )
979	470 909 910 967 971 978	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 ) ) ) ) )
980	979	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 ) ) ) )
981	883 902 980	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 ) ) ) )
982	850 859 981	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 ) ) ) )
983	775 811 982	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 ) ) ) )
984	438 442 983	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 ) ) ) )
985	984	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 ) ) ) ) )
986	422 985	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 ) ) ) ) )
987	986	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 ) ) ) ) )
988	191 193 987	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 ) ) ) ) )
989	180 181 184 988	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 ) ) ) ) )
990	989	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 ) ) ) ) ) ) )
991	44 57 70 83 179 990	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 ) ) ) ) ) )
992	31 991	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 ) ) ) ) ) ) )
993	5 16 992	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 ) ) ) ) ) )
994	12 993	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 ) ) ) ) )

Metamath Proof Explorer

Theorem dvnmul

Proof