Theorem dvnmul 37915

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

Hypotheses

Ref	Expression
dvnmul.s	|- ( ph -> S e. { RR , CC } )
dvnmul.x	|- ( ph -> X e. ( ( TopOpen ` ℂfld ) ↾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

Ref	Expression
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 ) ) ) ) )

Distinct variable groups:   A, k   B, k   x, C   x, D   k, F   k, G   k, N, x   S, k, x   k, X, x   ph, k, x

Allowed substitution hints:   A( x)   B( x)   C( k)   D( k)   F( x)   G( x)

Proof of Theorem dvnmul

Dummy variables i m n h j are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		id 22	. 2 |- ( ph -> ph )
2		dvnmul.n	. . 3 |- ( ph -> N e. NN0 )
3		nn0uz 11217	. . . . 5 |- NN0 = ( ZZ>= ` 0 )
4	2, 3	syl6eleq 2559	. . . 4 |- ( ph -> N e. ( ZZ>= ` 0 ) )
5		eluzfz2 11833	. . . 4 |- ( N e. ( ZZ>= ` 0 ) -> N e. ( 0 ... N ) )
6	4, 5	syl 17	. . 3 |- ( ph -> N e. ( 0 ... N ) )
7		eleq1 2537	. . . . 5 |- ( n = N -> ( n e. ( 0 ... N ) <-> N e. ( 0 ... N ) ) )
8		fveq2 5879	. . . . . . 7 |- ( n = N -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` n ) = ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` N ) )
9		oveq2 6316	. . . . . . . . . 10 |- ( n = N -> ( 0 ... n ) = ( 0 ... N ) )
10	9	sumeq1d 13844	. . . . . . . . 9 |- ( 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 ) ) ) )
11		oveq1 6315	. . . . . . . . . . 11 |- ( n = N -> ( n _C k ) = ( N _C k ) )
12		oveq1 6315	. . . . . . . . . . . . . 14 |- ( n = N -> ( n - k ) = ( N - k ) )
13	12	fveq2d 5883	. . . . . . . . . . . . 13 |- ( n = N -> ( D ` ( n - k ) ) = ( D ` ( N - k ) ) )
14	13	fveq1d 5881	. . . . . . . . . . . 12 |- ( n = N -> ( ( D ` ( n - k ) ) ` x ) = ( ( D ` ( N - k ) ) ` x ) )
15	14	oveq2d 6324	. . . . . . . . . . 11 |- ( n = N -> ( ( ( C ` k ) ` x ) x. ( ( D ` ( n - k ) ) ` x ) ) = ( ( ( C ` k ) ` x ) x. ( ( D ` ( N - k ) ) ` x ) ) )
16	11, 15	oveq12d 6326	. . . . . . . . . 10 |- ( 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 ) ) ) )
17	16	sumeq2ad 37740	. . . . . . . . 9 |- ( 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 ) ) ) )
18	10, 17	eqtrd 2505	. . . . . . . 8 |- ( 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 ) ) ) )
19	18	mpteq2dv 4483	. . . . . . 7 |- ( 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 ) ) ) ) )
20	8, 19	eqeq12d 2486	. . . . . 6 |- ( 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 ) ) ) ) ) )
21	20	imbi2d 323	. . . . 5 |- ( 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 ) ) ) ) ) ) )
22	7, 21	imbi12d 327	. . . 4 |- ( 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 ) ) ) ) ) ) ) )
23		fveq2 5879	. . . . . . 7 |- ( m = 0 -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` m ) = ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` 0 ) )
24		simpl 464	. . . . . . . . . 10 |- ( ( m = 0 /\ x e. X ) -> m = 0 )
25	24	oveq2d 6324	. . . . . . . . 9 |- ( ( m = 0 /\ x e. X ) -> ( 0 ... m ) = ( 0 ... 0 ) )
26		simpll 768	. . . . . . . . . . 11 |- ( ( ( m = 0 /\ x e. X ) /\ k e. ( 0 ... 0 ) ) -> m = 0 )
27	26	oveq1d 6323	. . . . . . . . . 10 |- ( ( ( m = 0 /\ x e. X ) /\ k e. ( 0 ... 0 ) ) -> ( m _C k ) = ( 0 _C k ) )
28	26	oveq1d 6323	. . . . . . . . . . . . 13 |- ( ( ( m = 0 /\ x e. X ) /\ k e. ( 0 ... 0 ) ) -> ( m - k ) = ( 0 - k ) )
29	28	fveq2d 5883	. . . . . . . . . . . 12 |- ( ( ( m = 0 /\ x e. X ) /\ k e. ( 0 ... 0 ) ) -> ( D ` ( m - k ) ) = ( D ` ( 0 - k ) ) )
30	29	fveq1d 5881	. . . . . . . . . . 11 |- ( ( ( m = 0 /\ x e. X ) /\ k e. ( 0 ... 0 ) ) -> ( ( D ` ( m - k ) ) ` x ) = ( ( D ` ( 0 - k ) ) ` x ) )
31	30	oveq2d 6324	. . . . . . . . . 10 |- ( ( ( 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 ) ) )
32	27, 31	oveq12d 6326	. . . . . . . . 9 |- ( ( ( 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 ) ) ) )
33	25, 32	sumeq12rdv 13850	. . . . . . . 8 |- ( ( 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 ) ) ) )
34	33	mpteq2dva 4482	. . . . . . 7 |- ( 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 ) ) ) ) )
35	23, 34	eqeq12d 2486	. . . . . 6 |- ( 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 ) ) ) ) ) )
36	35	imbi2d 323	. . . . 5 |- ( 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 ) ) ) ) ) ) )
37		fveq2 5879	. . . . . . 7 |- ( m = i -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` m ) = ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` i ) )
38		simpl 464	. . . . . . . . . 10 |- ( ( m = i /\ x e. X ) -> m = i )
39	38	oveq2d 6324	. . . . . . . . 9 |- ( ( m = i /\ x e. X ) -> ( 0 ... m ) = ( 0 ... i ) )
40		simpll 768	. . . . . . . . . . 11 |- ( ( ( m = i /\ x e. X ) /\ k e. ( 0 ... i ) ) -> m = i )
41	40	oveq1d 6323	. . . . . . . . . 10 |- ( ( ( m = i /\ x e. X ) /\ k e. ( 0 ... i ) ) -> ( m _C k ) = ( i _C k ) )
42	40	oveq1d 6323	. . . . . . . . . . . . 13 |- ( ( ( m = i /\ x e. X ) /\ k e. ( 0 ... i ) ) -> ( m - k ) = ( i - k ) )
43	42	fveq2d 5883	. . . . . . . . . . . 12 |- ( ( ( m = i /\ x e. X ) /\ k e. ( 0 ... i ) ) -> ( D ` ( m - k ) ) = ( D ` ( i - k ) ) )
44	43	fveq1d 5881	. . . . . . . . . . 11 |- ( ( ( m = i /\ x e. X ) /\ k e. ( 0 ... i ) ) -> ( ( D ` ( m - k ) ) ` x ) = ( ( D ` ( i - k ) ) ` x ) )
45	44	oveq2d 6324	. . . . . . . . . 10 |- ( ( ( 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 ) ) )
46	41, 45	oveq12d 6326	. . . . . . . . 9 |- ( ( ( 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 ) ) ) )
47	39, 46	sumeq12rdv 13850	. . . . . . . 8 |- ( ( 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 ) ) ) )
48	47	mpteq2dva 4482	. . . . . . 7 |- ( 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 ) ) ) ) )
49	37, 48	eqeq12d 2486	. . . . . 6 |- ( 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 ) ) ) ) ) )
50	49	imbi2d 323	. . . . 5 |- ( 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 ) ) ) ) ) ) )
51		fveq2 5879	. . . . . . 7 |- ( m = ( i + 1 ) -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` m ) = ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` ( i + 1 ) ) )
52		simpl 464	. . . . . . . . . 10 |- ( ( m = ( i + 1 ) /\ x e. X ) -> m = ( i + 1 ) )
53	52	oveq2d 6324	. . . . . . . . 9 |- ( ( m = ( i + 1 ) /\ x e. X ) -> ( 0 ... m ) = ( 0 ... ( i + 1 ) ) )
54		simpll 768	. . . . . . . . . . 11 |- ( ( ( m = ( i + 1 ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> m = ( i + 1 ) )
55	54	oveq1d 6323	. . . . . . . . . 10 |- ( ( ( m = ( i + 1 ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( m _C k ) = ( ( i + 1 ) _C k ) )
56	54	oveq1d 6323	. . . . . . . . . . . . 13 |- ( ( ( m = ( i + 1 ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( m - k ) = ( ( i + 1 ) - k ) )
57	56	fveq2d 5883	. . . . . . . . . . . 12 |- ( ( ( m = ( i + 1 ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( D ` ( m - k ) ) = ( D ` ( ( i + 1 ) - k ) ) )
58	57	fveq1d 5881	. . . . . . . . . . 11 |- ( ( ( m = ( i + 1 ) /\ x e. X ) /\ k e. ( 0 ... ( i + 1 ) ) ) -> ( ( D ` ( m - k ) ) ` x ) = ( ( D ` ( ( i + 1 ) - k ) ) ` x ) )
59	58	oveq2d 6324	. . . . . . . . . 10 |- ( ( ( 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 ) ) )
60	55, 59	oveq12d 6326	. . . . . . . . 9 |- ( ( ( 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 ) ) ) )
61	53, 60	sumeq12rdv 13850	. . . . . . . 8 |- ( ( 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 ) ) ) )
62	61	mpteq2dva 4482	. . . . . . 7 |- ( 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 ) ) ) ) )
63	51, 62	eqeq12d 2486	. . . . . 6 |- ( 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 ) ) ) ) ) )
64	63	imbi2d 323	. . . . 5 |- ( 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 ) ) ) ) ) ) )
65		fveq2 5879	. . . . . . 7 |- ( m = n -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` m ) = ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` n ) )
66		simpl 464	. . . . . . . . . 10 |- ( ( m = n /\ x e. X ) -> m = n )
67	66	oveq2d 6324	. . . . . . . . 9 |- ( ( m = n /\ x e. X ) -> ( 0 ... m ) = ( 0 ... n ) )
68		simpll 768	. . . . . . . . . . 11 |- ( ( ( m = n /\ x e. X ) /\ k e. ( 0 ... n ) ) -> m = n )
69	68	oveq1d 6323	. . . . . . . . . 10 |- ( ( ( m = n /\ x e. X ) /\ k e. ( 0 ... n ) ) -> ( m _C k ) = ( n _C k ) )
70	68	oveq1d 6323	. . . . . . . . . . . . 13 |- ( ( ( m = n /\ x e. X ) /\ k e. ( 0 ... n ) ) -> ( m - k ) = ( n - k ) )
71	70	fveq2d 5883	. . . . . . . . . . . 12 |- ( ( ( m = n /\ x e. X ) /\ k e. ( 0 ... n ) ) -> ( D ` ( m - k ) ) = ( D ` ( n - k ) ) )
72	71	fveq1d 5881	. . . . . . . . . . 11 |- ( ( ( m = n /\ x e. X ) /\ k e. ( 0 ... n ) ) -> ( ( D ` ( m - k ) ) ` x ) = ( ( D ` ( n - k ) ) ` x ) )
73	72	oveq2d 6324	. . . . . . . . . 10 |- ( ( ( 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 ) ) )
74	69, 73	oveq12d 6326	. . . . . . . . 9 |- ( ( ( 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 ) ) ) )
75	67, 74	sumeq12rdv 13850	. . . . . . . 8 |- ( ( 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 ) ) ) )
76	75	mpteq2dva 4482	. . . . . . 7 |- ( 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 ) ) ) ) )
77	65, 76	eqeq12d 2486	. . . . . 6 |- ( 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 ) ) ) ) ) )
78	77	imbi2d 323	. . . . 5 |- ( 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 ) ) ) ) ) ) )
79		dvnmul.s	. . . . . . . . 9 |- ( ph -> S e. { RR , CC } )
80		recnprss 22938	. . . . . . . . 9 |- ( S e. { RR , CC } -> S C_ CC )
81	79, 80	syl 17	. . . . . . . 8 |- ( ph -> S C_ CC )
82		dvnmul.a	. . . . . . . . . 10 |- ( ( ph /\ x e. X ) -> A e. CC )
83		dvnmul.cc	. . . . . . . . . 10 |- ( ( ph /\ x e. X ) -> B e. CC )
84	82, 83	mulcld 9681	. . . . . . . . 9 |- ( ( ph /\ x e. X ) -> ( A x. B ) e. CC )
85		restsspw 15408	. . . . . . . . . . 11 |- ( ( TopOpen ` ℂfld ) ↾t S ) C_ ~P S
86		dvnmul.x	. . . . . . . . . . 11 |- ( ph -> X e. ( ( TopOpen ` ℂfld ) ↾t S ) )
87	85, 86	sseldi 3416	. . . . . . . . . 10 |- ( ph -> X e. ~P S )
88		elpwi 3951	. . . . . . . . . 10 |- ( X e. ~P S -> X C_ S )
89	87, 88	syl 17	. . . . . . . . 9 |- ( ph -> X C_ S )
90		cnex 9638	. . . . . . . . . 10 |- CC e. _V
91	90	a1i 11	. . . . . . . . 9 |- ( ph -> CC e. _V )
92	84, 89, 91, 79	mptelpm 37514	. . . . . . . 8 |- ( ph -> ( x e. X |-> ( A x. B ) ) e. ( CC ^pm S ) )
93		dvn0 22957	. . . . . . . 8 |- ( ( 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 ) ) )
94	81, 92, 93	syl2anc 673	. . . . . . 7 |- ( ph -> ( ( S Dn ( x e. X |-> ( A x. B ) ) ) ` 0 ) = ( x e. X |-> ( A x. B ) ) )
95		0z 10972	. . . . . . . . . . . 12 |- 0 e. ZZ
96		fzsn 11866	. . . . . . . . . . . 12 |- ( 0 e. ZZ -> ( 0 ... 0 ) = { 0 } )
97	95, 96	ax-mp 5	. . . . . . . . . . 11 |- ( 0 ... 0 ) = { 0 }
98	97	sumeq1i 13841	. . . . . . . . . 10 |- 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 ) ) )
99	98	a1i 11	. . . . . . . . 9 |- ( ( 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 ) ) ) )
100		nfcvd 2613	. . . . . . . . . 10 |- ( ( ph /\ x e. X ) -> F/_ k ( A x. B ) )
101		nfv 1769	. . . . . . . . . 10 |- F/ k ( ph /\ x e. X )
102		oveq2 6316	. . . . . . . . . . . . . 14 |- ( k = 0 -> ( 0 _C k ) = ( 0 _C 0 ) )
103		0nn0 10908	. . . . . . . . . . . . . . . 16 |- 0 e. NN0
104		bcn0 12533	. . . . . . . . . . . . . . . 16 |- ( 0 e. NN0 -> ( 0 _C 0 ) = 1 )
105	103, 104	ax-mp 5	. . . . . . . . . . . . . . 15 |- ( 0 _C 0 ) = 1
106	105	a1i 11	. . . . . . . . . . . . . 14 |- ( k = 0 -> ( 0 _C 0 ) = 1 )
107	102, 106	eqtrd 2505	. . . . . . . . . . . . 13 |- ( k = 0 -> ( 0 _C k ) = 1 )
108	107	adantl 473	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. X ) /\ k = 0 ) -> ( 0 _C k ) = 1 )
109		fveq2 5879	. . . . . . . . . . . . . . . . . . 19 |- ( k = 0 -> ( C ` k ) = ( C ` 0 ) )
110	109	adantl 473	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ k = 0 ) -> ( C ` k ) = ( C ` 0 ) )
111		dvnmul.c	. . . . . . . . . . . . . . . . . . . . . 22 |- C = ( k e. ( 0 ... N ) |-> ( ( S Dn F ) ` k ) )
112		fveq2 5879	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( k = n -> ( ( S Dn F ) ` k ) = ( ( S Dn F ) ` n ) )
113	112	cbvmptv 4488	. . . . . . . . . . . . . . . . . . . . . 22 |- ( k e. ( 0 ... N ) |-> ( ( S Dn F ) ` k ) ) = ( n e. ( 0 ... N ) |-> ( ( S Dn F ) ` n ) )
114	111, 113	eqtri 2493	. . . . . . . . . . . . . . . . . . . . 21 |- C = ( n e. ( 0 ... N ) |-> ( ( S Dn F ) ` n ) )
115	114	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> C = ( n e. ( 0 ... N ) |-> ( ( S Dn F ) ` n ) ) )
116		fveq2 5879	. . . . . . . . . . . . . . . . . . . . 21 |- ( n = 0 -> ( ( S Dn F ) ` n ) = ( ( S Dn F ) ` 0 ) )
117	116	adantl 473	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ n = 0 ) -> ( ( S Dn F ) ` n ) = ( ( S Dn F ) ` 0 ) )
118		eluzfz1 11832	. . . . . . . . . . . . . . . . . . . . 21 |- ( N e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... N ) )
119	4, 118	syl 17	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> 0 e. ( 0 ... N ) )
120		fvex 5889	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( S Dn F ) ` 0 ) e. _V
121	120	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ( S Dn F ) ` 0 ) e. _V )
122	115, 117, 119, 121	fvmptd 5969	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( C ` 0 ) = ( ( S Dn F ) ` 0 ) )
123	122	adantr 472	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ k = 0 ) -> ( C ` 0 ) = ( ( S Dn F ) ` 0 ) )
124	110, 123	eqtrd 2505	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ k = 0 ) -> ( C ` k ) = ( ( S Dn F ) ` 0 ) )
125		dvnmulf	. . . . . . . . . . . . . . . . . . . 20 |- F = ( x e. X |-> A )
126	82, 89, 91, 79	mptelpm 37514	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( x e. X |-> A ) e. ( CC ^pm S ) )
127	125, 126	syl5eqel 2553	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> F e. ( CC ^pm S ) )
128		dvn0 22957	. . . . . . . . . . . . . . . . . . 19 |- ( ( S C_ CC /\ F e. ( CC ^pm S ) ) -> ( ( S Dn F ) ` 0 ) = F )
129	81, 127, 128	syl2anc 673	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( S Dn F ) ` 0 ) = F )
130	129	adantr 472	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ k = 0 ) -> ( ( S Dn F ) ` 0 ) = F )
131	124, 130	eqtrd 2505	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ k = 0 ) -> ( C ` k ) = F )
132	131	fveq1d 5881	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k = 0 ) -> ( ( C ` k ) ` x ) = ( F ` x ) )
133	132	adantlr 729	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. X ) /\ k = 0 ) -> ( ( C ` k ) ` x ) = ( F ` x ) )
134		simpr 468	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. X ) -> x e. X )
135	125	fvmpt2 5972	. . . . . . . . . . . . . . . 16 |- ( ( x e. X /\ A e. CC ) -> ( F ` x ) = A )
136	134, 82, 135	syl2anc 673	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. X ) -> ( F ` x ) = A )
137	136	adantr 472	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. X ) /\ k = 0 ) -> ( F ` x ) = A )
138	133, 137	eqtrd 2505	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. X ) /\ k = 0 ) -> ( ( C ` k ) ` x ) = A )
139		oveq2 6316	. . . . . . . . . . . . . . . . . . 19 |- ( k = 0 -> ( 0 - k ) = ( 0 - 0 ) )
140		0m0e0 10741	. . . . . . . . . . . . . . . . . . . 20 |- ( 0 - 0 ) = 0
141	140	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( k = 0 -> ( 0 - 0 ) = 0 )
142	139, 141	eqtrd 2505	. . . . . . . . . . . . . . . . . 18 |- ( k = 0 -> ( 0 - k ) = 0 )
143	142	fveq2d 5883	. . . . . . . . . . . . . . . . 17 |- ( k = 0 -> ( D ` ( 0 - k ) ) = ( D ` 0 ) )
144	143	fveq1d 5881	. . . . . . . . . . . . . . . 16 |- ( k = 0 -> ( ( D ` ( 0 - k ) ) ` x ) = ( ( D ` 0 ) ` x ) )
145	144	adantl 473	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k = 0 ) -> ( ( D ` ( 0 - k ) ) ` x ) = ( ( D ` 0 ) ` x ) )
146	145	adantlr 729	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. X ) /\ k = 0 ) -> ( ( D ` ( 0 - k ) ) ` x ) = ( ( D ` 0 ) ` x ) )
147		dvnmul.d	. . . . . . . . . . . . . . . . . . . 20 |- D = ( k e. ( 0 ... N ) |-> ( ( S Dn G ) ` k ) )
148		fveq2 5879	. . . . . . . . . . . . . . . . . . . . 21 |- ( k = n -> ( ( S Dn G ) ` k ) = ( ( S Dn G ) ` n ) )
149	148	cbvmptv 4488	. . . . . . . . . . . . . . . . . . . 20 |- ( k e. ( 0 ... N ) |-> ( ( S Dn G ) ` k ) ) = ( n e. ( 0 ... N ) |-> ( ( S Dn G ) ` n ) )
150	147, 149	eqtri 2493	. . . . . . . . . . . . . . . . . . 19 |- D = ( n e. ( 0 ... N ) |-> ( ( S Dn G ) ` n ) )
151	150	fveq1i 5880	. . . . . . . . . . . . . . . . . 18 |- ( D ` 0 ) = ( ( n e. ( 0 ... N ) |-> ( ( S Dn G ) ` n ) ) ` 0 )
152	151	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( D ` 0 ) = ( ( n e. ( 0 ... N ) |-> ( ( S Dn G ) ` n ) ) ` 0 ) )
153		eqidd 2472	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( n e. ( 0 ... N ) |-> ( ( S Dn G ) ` n ) ) = ( n e. ( 0 ... N ) |-> ( ( S Dn G ) ` n ) ) )
154		fveq2 5879	. . . . . . . . . . . . . . . . . . . 20 |- ( n = 0 -> ( ( S Dn G ) ` n ) = ( ( S Dn G ) ` 0 ) )
155	154	adantl 473	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ n = 0 ) -> ( ( S Dn G ) ` n ) = ( ( S Dn G ) ` 0 ) )
156		dvnmul.f	. . . . . . . . . . . . . . . . . . . . . 22 |- G = ( x e. X |-> B )
157	83, 89, 91, 79	mptelpm 37514	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( x e. X |-> B ) e. ( CC ^pm S ) )
158	156, 157	syl5eqel 2553	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> G e. ( CC ^pm S ) )
159		dvn0 22957	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( S C_ CC /\ G e. ( CC ^pm S ) ) -> ( ( S Dn G ) ` 0 ) = G )
160	81, 158, 159	syl2anc 673	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ( S Dn G ) ` 0 ) = G )
161	160	adantr 472	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ n = 0 ) -> ( ( S Dn G ) ` 0 ) = G )
162	155, 161	eqtrd 2505	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ n = 0 ) -> ( ( S Dn G ) ` n ) = G )
163	156	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> G = ( x e. X |-> B ) )
164		mptexg 6151	. . . . . . . . . . . . . . . . . . . 20 |- ( X e. ~P S -> ( x e. X |-> B ) e. _V )
165	87, 164	syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( x e. X |-> B ) e. _V )
166	163, 165	eqeltrd 2549	. . . . . . . . . . . . . . . . . 18 |- ( ph -> G e. _V )
167	153, 162, 119, 166	fvmptd 5969	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( n e. ( 0 ... N ) |-> ( ( S Dn G ) ` n ) ) ` 0 ) = G )
168	152, 167	eqtrd 2505	. . . . . . . . . . . . . . . 16 |- ( ph -> ( D ` 0 ) = G )
169	168	fveq1d 5881	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( D ` 0 ) ` x ) = ( G ` x ) )
170	169	ad2antrr 740	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. X ) /\ k = 0 ) -> ( ( D ` 0 ) ` x ) = ( G ` x ) )
171	163, 83	fvmpt2d 5974	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. X ) -> ( G ` x ) = B )
172	171	adantr 472	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. X ) /\ k = 0 ) -> ( G ` x ) = B )
173	146, 170, 172	3eqtrd 2509	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. X ) /\ k = 0 ) -> ( ( D ` ( 0 - k ) ) ` x ) = B )
174	138, 173	oveq12d 6326	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. X ) /\ k = 0 ) -> ( ( ( C ` k ) ` x ) x. ( ( D ` ( 0 - k ) ) ` x ) ) = ( A x. B ) )
175	108, 174	oveq12d 6326	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. X ) /\ k = 0 ) -> ( ( 0 _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( 0 - k ) ) ` x ) ) ) = ( 1 x. ( A x. B ) ) )
176	84	mulid2d 9679	. . . . . . . . . . . 12 |- ( ( ph /\ x e. X ) -> ( 1 x. ( A x. B ) ) = ( A x. B ) )
177	176	adantr 472	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. X ) /\ k = 0 ) -> ( 1 x. ( A x. B ) ) = ( A x. B ) )
178	175, 177	eqtrd 2505	. . . . . . . . . 10 |- ( ( ( ph /\ x e. X ) /\ k = 0 ) -> ( ( 0 _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( 0 - k ) ) ` x ) ) ) = ( A x. B ) )
179		0re 9661	. . . . . . . . . . 11 |- 0 e. RR
180	179	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ x e. X ) -> 0 e. RR )
181	100, 101, 178, 180, 84	sumsnd 37410	. . . . . . . . 9 |- ( ( ph /\ x e. X ) -> sum_ k e. { 0 } ( ( 0 _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( 0 - k ) ) ` x ) ) ) = ( A x. B ) )
182	99, 181	eqtr2d 2506	. . . . . . . 8 |- ( ( ph /\ x e. X ) -> ( A x. B ) = sum_ k e. ( 0 ... 0 ) ( ( 0 _C k ) x. ( ( ( C ` k ) ` x ) x. ( ( D ` ( 0 - k ) ) ` x ) ) ) )
183	182	mpteq2dva 4482	. . . . . . 7 |- ( 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 ) ) ) ) )
184	94, 183	eqtrd 2505	. . . . . 6 |- ( 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 ) ) ) ) )
185	184	a1i 11	. . . . 5 |- ( 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 ) ) ) ) ) )
186		simp3 1032	. . . . . . 7 |- ( ( 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 )
187		simp1 1030	. . . . . . 7 |- ( ( 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 ) )
188		simp2 1031	. . . . . . . 8 |- ( ( 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 ) ) ) ) ) )
189		pm3.35 597	. . . . . . . 8 |- ( ( 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 ) ) ) ) )
190	186, 188, 189	syl2anc 673	. . . . . . 7 |- ( ( 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 ) ) ) ) )
191	81	adantr 472	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ N ) ) -> S C_ CC )
192	92	adantr 472	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ N ) ) -> ( x e. X |-> ( A x. B ) ) e. ( CC ^pm S ) )
193		elfzonn0 11988	. . . . . . . . . . 11 |- ( i e. ( 0..^ N ) -> i e. NN0 )
194	193	adantl 473	. . . . . . . . . 10 |- ( ( ph /\ i e. ( 0..^ N ) ) -> i e. NN0 )
195		dvnp1 22958	. . . . . . . . . 10 |- ( ( 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 ) ) )
196	191, 192, 194, 195	syl3anc 1292	. . . . . . . . 9 |- ( ( 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 ) ) )
197	196	adantr 472	. . . . . . . 8 |- ( ( ( 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 ) ) )
198		simpr 468	. . . . . . . . 9 |- ( ( ( 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 ) ) ) ) )
199	198	oveq2d 6324	. . . . . . . 8 |- ( ( ( 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 ) ) ) ) ) )
200		eqid 2471	. . . . . . . . . . 11 |- ( ( TopOpen ` ℂfld ) ↾t S ) = ( ( TopOpen ` ℂfld ) ↾t S )
201		eqid 2471	. . . . . . . . . . 11 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
202	79	adantr 472	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ N ) ) -> S e. { RR , CC } )
203	86	adantr 472	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ N ) ) -> X e. ( ( TopOpen ` ℂfld ) ↾t S ) )
204		fzfid 12224	. . . . . . . . . . 11 |- ( ( ph /\ i e. ( 0..^ N ) ) -> ( 0 ... i ) e. Fin )
205	193	adantr 472	. . . . . . . . . . . . . . . 16 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> i e. NN0 )
206		elfzelz 11826	. . . . . . . . . . . . . . . . 17 |- ( k e. ( 0 ... i ) -> k e. ZZ )
207	206	adantl 473	. . . . . . . . . . . . . . . 16 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> k e. ZZ )
208	205, 207	bccld 37625	. . . . . . . . . . . . . . 15 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> ( i _C k ) e. NN0 )
209	208	nn0cnd 10951	. . . . . . . . . . . . . 14 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> ( i _C k ) e. CC )
210	209	adantll 728	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( i _C k ) e. CC )
211	210	3adant3 1050	. . . . . . . . . . . 12 |- ( ( ( ph /\ i e. ( 0..^ N ) ) /\ k e. ( 0 ... i ) /\ x e. X ) -> ( i _C k ) e. CC )
212		simpll 768	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ N ) ) /\ k e. ( 0 ... i ) ) -> ph )
213		0zd 10973	. . . . . . . . . . . . . . . . . . . 20 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> 0 e. ZZ )
214		elfzoel2 11946	. . . . . . . . . . . . . . . . . . . . 21 |- ( i e. ( 0..^ N ) -> N e. ZZ )
215	214	adantr 472	. . . . . . . . . . . . . . . . . . . 20 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> N e. ZZ )
216	213, 215, 207	3jca 1210	. . . . . . . . . . . . . . . . . . 19 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> ( 0 e. ZZ /\ N e. ZZ /\ k e. ZZ ) )
217		elfzle1 11828	. . . . . . . . . . . . . . . . . . . 20 |- ( k e. ( 0 ... i ) -> 0 <_ k )
218	217	adantl 473	. . . . . . . . . . . . . . . . . . 19 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> 0 <_ k )
219	207	zred 11063	. . . . . . . . . . . . . . . . . . . 20 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> k e. RR )
220	214	zred 11063	. . . . . . . . . . . . . . . . . . . . 21 |- ( i e. ( 0..^ N ) -> N e. RR )
221	220	adantr 472	. . . . . . . . . . . . . . . . . . . 20 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> N e. RR )
222	193	nn0red 10950	. . . . . . . . . . . . . . . . . . . . . 22 |- ( i e. ( 0..^ N ) -> i e. RR )
223	222	adantr 472	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> i e. RR )
224		elfzle2 11829	. . . . . . . . . . . . . . . . . . . . . 22 |- ( k e. ( 0 ... i ) -> k <_ i )
225	224	adantl 473	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> k <_ i )
226		elfzolt2 11956	. . . . . . . . . . . . . . . . . . . . . 22 |- ( i e. ( 0..^ N ) -> i < N )
227	226	adantr 472	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> i < N )
228	219, 223, 221, 225, 227	lelttrd 9810	. . . . . . . . . . . . . . . . . . . 20 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> k < N )
229	219, 221, 228	ltled 9800	. . . . . . . . . . . . . . . . . . 19 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> k <_ N )
230	216, 218, 229	jca32 544	. . . . . . . . . . . . . . . . . 18 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> ( ( 0 e. ZZ /\ N e. ZZ /\ k e. ZZ ) /\ ( 0 <_ k /\ k <_ N ) ) )
231		elfz2 11817	. . . . . . . . . . . . . . . . . 18 |- ( k e. ( 0 ... N ) <-> ( ( 0 e. ZZ /\ N e. ZZ /\ k e. ZZ ) /\ ( 0 <_ k /\ k <_ N ) ) )
232	230, 231	sylibr 217	. . . . . . . . . . . . . . . . 17 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> k e. ( 0 ... N ) )
233	232	adantll 728	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ N ) ) /\ k e. ( 0 ... i ) ) -> k e. ( 0 ... N ) )
234		dvnmul.dvnf	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( S Dn F ) ` k ) : X --> CC )
235	111	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> C = ( k e. ( 0 ... N ) |-> ( ( S Dn F ) ` k ) ) )
236		fvex 5889	. . . . . . . . . . . . . . . . . . . 20 |- ( ( S Dn F ) ` k ) e. _V
237	236	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( S Dn F ) ` k ) e. _V )
238	235, 237	fvmpt2d 5974	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ k e. ( 0 ... N ) ) -> ( C ` k ) = ( ( S Dn F ) ` k ) )
239	238	feq1d 5724	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( C ` k ) : X --> CC <-> ( ( S Dn F ) ` k ) : X --> CC ) )
240	234, 239	mpbird 240	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ k e. ( 0 ... N ) ) -> ( C ` k ) : X --> CC )
241	212, 233, 240	syl2anc 673	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( C ` k ) : X --> CC )
242	241	3adant3 1050	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ N ) ) /\ k e. ( 0 ... i ) /\ x e. X ) -> ( C ` k ) : X --> CC )
243		simp3 1032	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ N ) ) /\ k e. ( 0 ... i ) /\ x e. X ) -> x e. X )
244	242, 243	ffvelrnd 6038	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ N ) ) /\ k e. ( 0 ... i ) /\ x e. X ) -> ( ( C ` k ) ` x ) e. CC )
245	193	nn0zd 11061	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( i e. ( 0..^ N ) -> i e. ZZ )
246	245	adantr 472	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> i e. ZZ )
247	246, 207	zsubcld 11068	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> ( i - k ) e. ZZ )
248	213, 215, 247	3jca 1210	. . . . . . . . . . . . . . . . . . . 20 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> ( 0 e. ZZ /\ N e. ZZ /\ ( i - k ) e. ZZ ) )
249		elfzel2 11824	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( k e. ( 0 ... i ) -> i e. ZZ )
250	249	zred 11063	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( k e. ( 0 ... i ) -> i e. RR )
251	206	zred 11063	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( k e. ( 0 ... i ) -> k e. RR )
252	250, 251	subge0d 10224	. . . . . . . . . . . . . . . . . . . . . 22 |- ( k e. ( 0 ... i ) -> ( 0 <_ ( i - k ) <-> k <_ i ) )
253	224, 252	mpbird 240	. . . . . . . . . . . . . . . . . . . . 21 |- ( k e. ( 0 ... i ) -> 0 <_ ( i - k ) )
254	253	adantl 473	. . . . . . . . . . . . . . . . . . . 20 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> 0 <_ ( i - k ) )
255	223, 219	resubcld 10068	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> ( i - k ) e. RR )
256	221, 219	resubcld 10068	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> ( N - k ) e. RR )
257	179	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> 0 e. RR )
258	221, 257	jca 541	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> ( N e. RR /\ 0 e. RR ) )
259		resubcl 9958	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( N e. RR /\ 0 e. RR ) -> ( N - 0 ) e. RR )
260	258, 259	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> ( N - 0 ) e. RR )
261	223, 221, 219, 227	ltsub1dd 10246	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> ( i - k ) < ( N - k ) )
262	257, 219, 221, 218	lesub2dd 10251	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> ( N - k ) <_ ( N - 0 ) )
263	255, 256, 260, 261, 262	ltletrd 9812	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> ( i - k ) < ( N - 0 ) )
264	220	recnd 9687	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( i e. ( 0..^ N ) -> N e. CC )
265	264	subid1d 9994	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( i e. ( 0..^ N ) -> ( N - 0 ) = N )
266	265	adantr 472	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> ( N - 0 ) = N )
267	263, 266	breqtrd 4420	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> ( i - k ) < N )
268	255, 221, 267	ltled 9800	. . . . . . . . . . . . . . . . . . . 20 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> ( i - k ) <_ N )
269	248, 254, 268	jca32 544	. . . . . . . . . . . . . . . . . . 19 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> ( ( 0 e. ZZ /\ N e. ZZ /\ ( i - k ) e. ZZ ) /\ ( 0 <_ ( i - k ) /\ ( i - k ) <_ N ) ) )
270		elfz2 11817	. . . . . . . . . . . . . . . . . . 19 |- ( ( i - k ) e. ( 0 ... N ) <-> ( ( 0 e. ZZ /\ N e. ZZ /\ ( i - k ) e. ZZ ) /\ ( 0 <_ ( i - k ) /\ ( i - k ) <_ N ) ) )
271	269, 270	sylibr 217	. . . . . . . . . . . . . . . . . 18 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> ( i - k ) e. ( 0 ... N ) )
272	271	adantll 728	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( i - k ) e. ( 0 ... N ) )
273		ovex 6336	. . . . . . . . . . . . . . . . . 18 |- ( i - k ) e. _V
274		eleq1 2537	. . . . . . . . . . . . . . . . . . . 20 |- ( j = ( i - k ) -> ( j e. ( 0 ... N ) <-> ( i - k ) e. ( 0 ... N ) ) )
275	274	anbi2d 718	. . . . . . . . . . . . . . . . . . 19 |- ( j = ( i - k ) -> ( ( ph /\ j e. ( 0 ... N ) ) <-> ( ph /\ ( i - k ) e. ( 0 ... N ) ) ) )
276		fveq2 5879	. . . . . . . . . . . . . . . . . . . 20 |- ( j = ( i - k ) -> ( ( S Dn G ) ` j ) = ( ( S Dn G ) ` ( i - k ) ) )
277	276	feq1d 5724	. . . . . . . . . . . . . . . . . . 19 |- ( j = ( i - k ) -> ( ( ( S Dn G ) ` j ) : X --> CC <-> ( ( S Dn G ) ` ( i - k ) ) : X --> CC ) )
278	275, 277	imbi12d 327	. . . . . . . . . . . . . . . . . 18 |- ( 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 ) ) )
279		nfv 1769	. . . . . . . . . . . . . . . . . . 19 |- F/ k ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( S Dn G ) ` j ) : X --> CC )
280		eleq1 2537	. . . . . . . . . . . . . . . . . . . . 21 |- ( k = j -> ( k e. ( 0 ... N ) <-> j e. ( 0 ... N ) ) )
281	280	anbi2d 718	. . . . . . . . . . . . . . . . . . . 20 |- ( k = j -> ( ( ph /\ k e. ( 0 ... N ) ) <-> ( ph /\ j e. ( 0 ... N ) ) ) )
282		fveq2 5879	. . . . . . . . . . . . . . . . . . . . 21 |- ( k = j -> ( ( S Dn G ) ` k ) = ( ( S Dn G ) ` j ) )
283	282	feq1d 5724	. . . . . . . . . . . . . . . . . . . 20 |- ( k = j -> ( ( ( S Dn G ) ` k ) : X --> CC <-> ( ( S Dn G ) ` j ) : X --> CC ) )
284	281, 283	imbi12d 327	. . . . . . . . . . . . . . . . . . 19 |- ( k = j -> ( ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( S Dn G ) ` k ) : X --> CC ) <-> ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( S Dn G ) ` j ) : X --> CC ) ) )
285		dvnmul.dvng	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( S Dn G ) ` k ) : X --> CC )
286	279, 284, 285	chvar 2119	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( S Dn G ) ` j ) : X --> CC )
287	273, 278, 286	vtocl 3086	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( i - k ) e. ( 0 ... N ) ) -> ( ( S Dn G ) ` ( i - k ) ) : X --> CC )
288	212, 272, 287	syl2anc 673	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( S Dn G ) ` ( i - k ) ) : X --> CC )
289	150	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> D = ( n e. ( 0 ... N ) |-> ( ( S Dn G ) ` n ) ) )
290		fveq2 5879	. . . . . . . . . . . . . . . . . . . 20 |- ( n = ( i - k ) -> ( ( S Dn G ) ` n ) = ( ( S Dn G ) ` ( i - k ) ) )
291	290	adantl 473	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) /\ n = ( i - k ) ) -> ( ( S Dn G ) ` n ) = ( ( S Dn G ) ` ( i - k ) ) )
292		fvex 5889	. . . . . . . . . . . . . . . . . . . 20 |- ( ( S Dn G ) ` ( i - k ) ) e. _V
293	292	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> ( ( S Dn G ) ` ( i - k ) ) e. _V )
294	289, 291, 271, 293	fvmptd 5969	. . . . . . . . . . . . . . . . . 18 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> ( D ` ( i - k ) ) = ( ( S Dn G ) ` ( i - k ) ) )
295	294	adantll 728	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( D ` ( i - k ) ) = ( ( S Dn G ) ` ( i - k ) ) )
296	295	feq1d 5724	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ i e. ( 0..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( D ` ( i - k ) ) : X --> CC <-> ( ( S Dn G ) ` ( i - k ) ) : X --> CC ) )
297	288, 296	mpbird 240	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ i e. ( 0..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( D ` ( i - k ) ) : X --> CC )
298	297	3adant3 1050	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ i e. ( 0..^ N ) ) /\ k e. ( 0 ... i ) /\ x e. X ) -> ( D ` ( i - k ) ) : X --> CC )
299	298, 243	ffvelrnd 6038	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ N ) ) /\ k e. ( 0 ... i ) /\ x e. X ) -> ( ( D ` ( i - k ) ) ` x ) e. CC )
300	244, 299	mulcld 9681	. . . . . . . . . . . 12 |- ( ( ( ph /\ i e. ( 0..^ N ) ) /\ k e. ( 0 ... i ) /\ x e. X ) -> ( ( ( C ` k ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) e. CC )
301	211, 300	mulcld 9681	. . . . . . . . . . 11 |- ( ( ( 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 )
302	211	3expa 1231	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ i e. ( 0..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( i _C k ) e. CC )
303	246	peano2zd 11066	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> ( i + 1 ) e. ZZ )
304	303, 207	zsubcld 11068	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> ( ( i + 1 ) - k ) e. ZZ )
305	213, 215, 304	3jca 1210	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> ( 0 e. ZZ /\ N e. ZZ /\ ( ( i + 1 ) - k ) e. ZZ ) )
306		peano2re 9824	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( i e. RR -> ( i + 1 ) e. RR )
307	250, 306	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( k e. ( 0 ... i ) -> ( i + 1 ) e. RR )
308		peano2re 9824	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( k e. RR -> ( k + 1 ) e. RR )
309	251, 308	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( k e. ( 0 ... i ) -> ( k + 1 ) e. RR )
310	251	ltp1d 10559	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( k e. ( 0 ... i ) -> k < ( k + 1 ) )
311		1red 9676	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( k e. ( 0 ... i ) -> 1 e. RR )
312	251, 250, 311, 224	leadd1dd 10248	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( k e. ( 0 ... i ) -> ( k + 1 ) <_ ( i + 1 ) )
313	251, 309, 307, 310, 312	ltletrd 9812	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( k e. ( 0 ... i ) -> k < ( i + 1 ) )
314	251, 307, 313	ltled 9800	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( k e. ( 0 ... i ) -> k <_ ( i + 1 ) )
315	314	adantl 473	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> k <_ ( i + 1 ) )
316	223, 306	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> ( i + 1 ) e. RR )
317	316, 219	subge0d 10224	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> ( 0 <_ ( ( i + 1 ) - k ) <-> k <_ ( i + 1 ) ) )
318	315, 317	mpbird 240	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> 0 <_ ( ( i + 1 ) - k ) )
319	316, 219	resubcld 10068	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> ( ( i + 1 ) - k ) e. RR )
320		elfzop1le2 37592	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( i e. ( 0..^ N ) -> ( i + 1 ) <_ N )
321	320	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> ( i + 1 ) <_ N )
322	316, 221, 219, 321	lesub1dd 10250	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> ( ( i + 1 ) - k ) <_ ( N - k ) )
323	262, 266	breqtrd 4420	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> ( N - k ) <_ N )
324	319, 256, 221, 322, 323	letrd 9809	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> ( ( i + 1 ) - k ) <_ N )
325	305, 318, 324	jca32 544	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> ( ( 0 e. ZZ /\ N e. ZZ /\ ( ( i + 1 ) - k ) e. ZZ ) /\ ( 0 <_ ( ( i + 1 ) - k ) /\ ( ( i + 1 ) - k ) <_ N ) ) )
326		elfz2 11817	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( i + 1 ) - k ) e. ( 0 ... N ) <-> ( ( 0 e. ZZ /\ N e. ZZ /\ ( ( i + 1 ) - k ) e. ZZ ) /\ ( 0 <_ ( ( i + 1 ) - k ) /\ ( ( i + 1 ) - k ) <_ N ) ) )
327	325, 326	sylibr 217	. . . . . . . . . . . . . . . . . . . 20 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> ( ( i + 1 ) - k ) e. ( 0 ... N ) )
328	327	adantll 728	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 0..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( i + 1 ) - k ) e. ( 0 ... N ) )
329		ovex 6336	. . . . . . . . . . . . . . . . . . . 20 |- ( ( i + 1 ) - k ) e. _V
330		eleq1 2537	. . . . . . . . . . . . . . . . . . . . . 22 |- ( j = ( ( i + 1 ) - k ) -> ( j e. ( 0 ... N ) <-> ( ( i + 1 ) - k ) e. ( 0 ... N ) ) )
331	330	anbi2d 718	. . . . . . . . . . . . . . . . . . . . 21 |- ( j = ( ( i + 1 ) - k ) -> ( ( ph /\ j e. ( 0 ... N ) ) <-> ( ph /\ ( ( i + 1 ) - k ) e. ( 0 ... N ) ) ) )
332		fveq2 5879	. . . . . . . . . . . . . . . . . . . . . 22 |- ( j = ( ( i + 1 ) - k ) -> ( ( S Dn G ) ` j ) = ( ( S Dn G ) ` ( ( i + 1 ) - k ) ) )
333	332	feq1d 5724	. . . . . . . . . . . . . . . . . . . . 21 |- ( j = ( ( i + 1 ) - k ) -> ( ( ( S Dn G ) ` j ) : X --> CC <-> ( ( S Dn G ) ` ( ( i + 1 ) - k ) ) : X --> CC ) )
334	331, 333	imbi12d 327	. . . . . . . . . . . . . . . . . . . 20 |- ( 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 ) ) )
335	329, 334, 286	vtocl 3086	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( ( i + 1 ) - k ) e. ( 0 ... N ) ) -> ( ( S Dn G ) ` ( ( i + 1 ) - k ) ) : X --> CC )
336	212, 328, 335	syl2anc 673	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( S Dn G ) ` ( ( i + 1 ) - k ) ) : X --> CC )
337	150	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ i e. ( 0..^ N ) ) /\ k e. ( 0 ... i ) ) -> D = ( n e. ( 0 ... N ) |-> ( ( S Dn G ) ` n ) ) )
338		simpr 468	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ i e. ( 0..^ N ) ) /\ k e. ( 0 ... i ) ) /\ n = ( ( i + 1 ) - k ) ) -> n = ( ( i + 1 ) - k ) )
339	338	fveq2d 5883	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ i e. ( 0..^ N ) ) /\ k e. ( 0 ... i ) ) /\ n = ( ( i + 1 ) - k ) ) -> ( ( S Dn G ) ` n ) = ( ( S Dn G ) ` ( ( i + 1 ) - k ) ) )
340		fvex 5889	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( S Dn G ) ` ( ( i + 1 ) - k ) ) e. _V
341	340	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ i e. ( 0..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( S Dn G ) ` ( ( i + 1 ) - k ) ) e. _V )
342	337, 339, 328, 341	fvmptd 5969	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ i e. ( 0..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( D ` ( ( i + 1 ) - k ) ) = ( ( S Dn G ) ` ( ( i + 1 ) - k ) ) )
343	342	feq1d 5724	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( ( D ` ( ( i + 1 ) - k ) ) : X --> CC <-> ( ( S Dn G ) ` ( ( i + 1 ) - k ) ) : X --> CC ) )
344	336, 343	mpbird 240	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( D ` ( ( i + 1 ) - k ) ) : X --> CC )
345	344	ffvelrnda 6037	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ i e. ( 0..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( ( D ` ( ( i + 1 ) - k ) ) ` x ) e. CC )
346	244	3expa 1231	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ i e. ( 0..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( ( C ` k ) ` x ) e. CC )
347	345, 346	mulcomd 9682	. . . . . . . . . . . . . . 15 |- ( ( ( ( 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 ) ) )
348	347	oveq2d 6324	. . . . . . . . . . . . . 14 |- ( ( ( ( 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 ) ) ) )
349	207	peano2zd 11066	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> ( k + 1 ) e. ZZ )
350	213, 215, 349	3jca 1210	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> ( 0 e. ZZ /\ N e. ZZ /\ ( k + 1 ) e. ZZ ) )
351	179	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( k e. ( 0 ... i ) -> 0 e. RR )
352	351, 251, 309, 217, 310	lelttrd 9810	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( k e. ( 0 ... i ) -> 0 < ( k + 1 ) )
353	351, 309, 352	ltled 9800	. . . . . . . . . . . . . . . . . . . . . 22 |- ( k e. ( 0 ... i ) -> 0 <_ ( k + 1 ) )
354	353	adantl 473	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> 0 <_ ( k + 1 ) )
355	219, 308	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> ( k + 1 ) e. RR )
356	312	adantl 473	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> ( k + 1 ) <_ ( i + 1 ) )
357	355, 316, 221, 356, 321	letrd 9809	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> ( k + 1 ) <_ N )
358	350, 354, 357	jca32 544	. . . . . . . . . . . . . . . . . . . 20 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> ( ( 0 e. ZZ /\ N e. ZZ /\ ( k + 1 ) e. ZZ ) /\ ( 0 <_ ( k + 1 ) /\ ( k + 1 ) <_ N ) ) )
359		elfz2 11817	. . . . . . . . . . . . . . . . . . . 20 |- ( ( k + 1 ) e. ( 0 ... N ) <-> ( ( 0 e. ZZ /\ N e. ZZ /\ ( k + 1 ) e. ZZ ) /\ ( 0 <_ ( k + 1 ) /\ ( k + 1 ) <_ N ) ) )
360	358, 359	sylibr 217	. . . . . . . . . . . . . . . . . . 19 |- ( ( i e. ( 0..^ N ) /\ k e. ( 0 ... i ) ) -> ( k + 1 ) e. ( 0 ... N ) )
361	360	adantll 728	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ i e. ( 0..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( k + 1 ) e. ( 0 ... N ) )
362		ovex 6336	. . . . . . . . . . . . . . . . . . 19 |- ( k + 1 ) e. _V
363		eleq1 2537	. . . . . . . . . . . . . . . . . . . . 21 |- ( j = ( k + 1 ) -> ( j e. ( 0 ... N ) <-> ( k + 1 ) e. ( 0 ... N ) ) )
364	363	anbi2d 718	. . . . . . . . . . . . . . . . . . . 20 |- ( j = ( k + 1 ) -> ( ( ph /\ j e. ( 0 ... N ) ) <-> ( ph /\ ( k + 1 ) e. ( 0 ... N ) ) ) )
365		fveq2 5879	. . . . . . . . . . . . . . . . . . . . 21 |- ( j = ( k + 1 ) -> ( C ` j ) = ( C ` ( k + 1 ) ) )
366	365	feq1d 5724	. . . . . . . . . . . . . . . . . . . 20 |- ( j = ( k + 1 ) -> ( ( C ` j ) : X --> CC <-> ( C ` ( k + 1 ) ) : X --> CC ) )
367	364, 366	imbi12d 327	. . . . . . . . . . . . . . . . . . 19 |- ( j = ( k + 1 ) -> ( ( ( ph /\ j e. ( 0 ... N ) ) -> ( C ` j ) : X --> CC ) <-> ( ( ph /\ ( k + 1 ) e. ( 0 ... N ) ) -> ( C ` ( k + 1 ) ) : X --> CC ) ) )
368		nfv 1769	. . . . . . . . . . . . . . . . . . . . 21 |- F/ k ( ph /\ j e. ( 0 ... N ) )
369		nfmpt1 4485	. . . . . . . . . . . . . . . . . . . . . . . 24 |- F/_ k ( k e. ( 0 ... N ) |-> ( ( S Dn F ) ` k ) )
370	111, 369	nfcxfr 2610	. . . . . . . . . . . . . . . . . . . . . . 23 |- F/_ k C
371		nfcv 2612	. . . . . . . . . . . . . . . . . . . . . . 23 |- F/_ k j
372	370, 371	nffv 5886	. . . . . . . . . . . . . . . . . . . . . 22 |- F/_ k ( C ` j )
373		nfcv 2612	. . . . . . . . . . . . . . . . . . . . . 22 |- F/_ k X
374		nfcv 2612	. . . . . . . . . . . . . . . . . . . . . 22 |- F/_ k CC
375	372, 373, 374	nff 5735	. . . . . . . . . . . . . . . . . . . . 21 |- F/ k ( C ` j ) : X --> CC
376	368, 375	nfim 2023	. . . . . . . . . . . . . . . . . . . 20 |- F/ k ( ( ph /\ j e. ( 0 ... N ) ) -> ( C ` j ) : X --> CC )
377		fveq2 5879	. . . . . . . . . . . . . . . . . . . . . 22 |- ( k = j -> ( C ` k ) = ( C ` j ) )
378	377	feq1d 5724	. . . . . . . . . . . . . . . . . . . . 21 |- ( k = j -> ( ( C ` k ) : X --> CC <-> ( C ` j ) : X --> CC ) )
379	281, 378	imbi12d 327	. . . . . . . . . . . . . . . . . . . 20 |- ( k = j -> ( ( ( ph /\ k e. ( 0 ... N ) ) -> ( C ` k ) : X --> CC ) <-> ( ( ph /\ j e. ( 0 ... N ) ) -> ( C ` j ) : X --> CC ) ) )
380	376, 379, 240	chvar 2119	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ j e. ( 0 ... N ) ) -> ( C ` j ) : X --> CC )
381	362, 367, 380	vtocl 3086	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( k + 1 ) e. ( 0 ... N ) ) -> ( C ` ( k + 1 ) ) : X --> CC )
382	212, 361, 381	syl2anc 673	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ i e. ( 0..^ N ) ) /\ k e. ( 0 ... i ) ) -> ( C ` ( k + 1 ) ) : X --> CC )
383	382	ffvelrnda 6037	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ i e. ( 0..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( ( C ` ( k + 1 ) ) ` x ) e. CC )
384	299	3expa 1231	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ i e. ( 0..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( ( D ` ( i - k ) ) ` x ) e. CC )
385	383, 384	mulcld 9681	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ i e. ( 0..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( ( ( C ` ( k + 1 ) ) ` x ) x. ( ( D ` ( i - k ) ) ` x ) ) e. CC )
386	345, 346	mulcld 9681	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ i e. ( 0..^ N ) ) /\ k e. ( 0 ... i ) ) /\ x e. X ) -> ( ( ( D ` ( ( i + 1 ) - k ) ) ` x ) x. ( ( C ` k ) ` x ) ) e. CC )
387	385, 386	addcld 9680	. . . . . . . . . . . . . 14 |- ( ( ( ( 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 )
388	348, 387	eqeltrrd 2550	. . . . . . . . . . . . 13 |- ( ( ( ( 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 )
389	302, 388	mulcld 9681	. . . . . . . . . . . 12 |- ( ( ( ( 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 )
390	389	3impa 1226	. . . . . . . . . . 11 |- ( ( ( 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 )
391	212, 79	syl 17	. . . . . . . . . . . . 13 |- ( ( ( ph /\ i e. ( 0..^ N ) ) /\ k e. ( 0 ... i ) ) -> S e. { RR , CC } )
392	179	a1i 11	. . . . . . . . . . . . 13 |-