Theorem plymulx0 29432

Description: Coefficients of a polynomial multiplyed by Xp. (Contributed by Thierry Arnoux, 25-Sep-2018.)

Assertion

Ref	Expression
plymulx0	|- ( F e. ( (Poly ` RR ) \ { 0p } ) -> (coeff ` ( F oF x. Xp ) ) = ( n e. NN0 |-> if ( n = 0 , 0 , ( (coeff ` F ) ` ( n - 1 ) ) ) ) )

Distinct variable group:   n, F

Proof of Theorem plymulx0

Dummy variables i x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eldifi 3587	. . . . 5 |- ( F e. ( (Poly ` RR ) \ { 0p } ) -> F e. (Poly ` RR ) )
2		ax-resscn 9597	. . . . . . 7 |- RR C_ CC
3		1re 9643	. . . . . . 7 |- 1 e. RR
4		plyid 23150	. . . . . . 7 |- ( ( RR C_ CC /\ 1 e. RR ) -> Xp e. (Poly ` RR ) )
5	2, 3, 4	mp2an 676	. . . . . 6 |- Xp e. (Poly ` RR )
6	5	a1i 11	. . . . 5 |- ( F e. ( (Poly ` RR ) \ { 0p } ) -> Xp e. (Poly ` RR ) )
7		simprl 762	. . . . . 6 |- ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ ( x e. RR /\ y e. RR ) ) -> x e. RR )
8		simprr 764	. . . . . 6 |- ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ ( x e. RR /\ y e. RR ) ) -> y e. RR )
9	7, 8	readdcld 9671	. . . . 5 |- ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ ( x e. RR /\ y e. RR ) ) -> ( x + y ) e. RR )
10	7, 8	remulcld 9672	. . . . 5 |- ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ ( x e. RR /\ y e. RR ) ) -> ( x x. y ) e. RR )
11	1, 6, 9, 10	plymul 23159	. . . 4 |- ( F e. ( (Poly ` RR ) \ { 0p } ) -> ( F oF x. Xp ) e. (Poly ` RR ) )
12		0re 9644	. . . 4 |- 0 e. RR
13		eqid 2422	. . . . 5 |- (coeff ` ( F oF x. Xp ) ) = (coeff ` ( F oF x. Xp ) )
14	13	coef2 23172	. . . 4 |- ( ( ( F oF x. Xp ) e. (Poly ` RR ) /\ 0 e. RR ) -> (coeff ` ( F oF x. Xp ) ) : NN0 --> RR )
15	11, 12, 14	sylancl 666	. . 3 |- ( F e. ( (Poly ` RR ) \ { 0p } ) -> (coeff ` ( F oF x. Xp ) ) : NN0 --> RR )
16	15	feqmptd 5931	. 2 |- ( F e. ( (Poly ` RR ) \ { 0p } ) -> (coeff ` ( F oF x. Xp ) ) = ( n e. NN0 |-> ( (coeff ` ( F oF x. Xp ) ) ` n ) ) )
17		cnex 9621	. . . . . . . . 9 |- CC e. _V
18	17	a1i 11	. . . . . . . 8 |- ( F e. ( (Poly ` RR ) \ { 0p } ) -> CC e. _V )
19		plyf 23139	. . . . . . . . 9 |- ( F e. (Poly ` RR ) -> F : CC --> CC )
20	1, 19	syl 17	. . . . . . . 8 |- ( F e. ( (Poly ` RR ) \ { 0p } ) -> F : CC --> CC )
21		plyf 23139	. . . . . . . . . 10 |- ( Xp e. (Poly ` RR ) -> Xp : CC --> CC )
22	5, 21	ax-mp 5	. . . . . . . . 9 |- Xp : CC --> CC
23	22	a1i 11	. . . . . . . 8 |- ( F e. ( (Poly ` RR ) \ { 0p } ) -> Xp : CC --> CC )
24		simprl 762	. . . . . . . . 9 |- ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ ( x e. CC /\ y e. CC ) ) -> x e. CC )
25		simprr 764	. . . . . . . . 9 |- ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ ( x e. CC /\ y e. CC ) ) -> y e. CC )
26	24, 25	mulcomd 9665	. . . . . . . 8 |- ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ ( x e. CC /\ y e. CC ) ) -> ( x x. y ) = ( y x. x ) )
27	18, 20, 23, 26	caofcom 6574	. . . . . . 7 |- ( F e. ( (Poly ` RR ) \ { 0p } ) -> ( F oF x. Xp ) = ( Xp oF x. F ) )
28	27	fveq2d 5882	. . . . . 6 |- ( F e. ( (Poly ` RR ) \ { 0p } ) -> (coeff ` ( F oF x. Xp ) ) = (coeff ` ( Xp oF x. F ) ) )
29	28	fveq1d 5880	. . . . 5 |- ( F e. ( (Poly ` RR ) \ { 0p } ) -> ( (coeff ` ( F oF x. Xp ) ) ` n ) = ( (coeff ` ( Xp oF x. F ) ) ` n ) )
30	29	adantr 466	. . . 4 |- ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) -> ( (coeff ` ( F oF x. Xp ) ) ` n ) = ( (coeff ` ( Xp oF x. F ) ) ` n ) )
31	5	a1i 11	. . . . . 6 |- ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) -> Xp e. (Poly ` RR ) )
32	1	adantr 466	. . . . . 6 |- ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) -> F e. (Poly ` RR ) )
33		simpr 462	. . . . . 6 |- ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) -> n e. NN0 )
34		eqid 2422	. . . . . . 7 |- (coeff ` Xp ) = (coeff ` Xp )
35		eqid 2422	. . . . . . 7 |- (coeff ` F ) = (coeff ` F )
36	34, 35	coemul 23193	. . . . . 6 |- ( ( Xp e. (Poly ` RR ) /\ F e. (Poly ` RR ) /\ n e. NN0 ) -> ( (coeff ` ( Xp oF x. F ) ) ` n ) = sum_ i e. ( 0 ... n ) ( ( (coeff ` Xp ) ` i ) x. ( (coeff ` F ) ` ( n - i ) ) ) )
37	31, 32, 33, 36	syl3anc 1264	. . . . 5 |- ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) -> ( (coeff ` ( Xp oF x. F ) ) ` n ) = sum_ i e. ( 0 ... n ) ( ( (coeff ` Xp ) ` i ) x. ( (coeff ` F ) ` ( n - i ) ) ) )
38		elfznn0 11888	. . . . . . . . . 10 |- ( i e. ( 0 ... n ) -> i e. NN0 )
39		coeidp 23204	. . . . . . . . . 10 |- ( i e. NN0 -> ( (coeff ` Xp ) ` i ) = if ( i = 1 , 1 , 0 ) )
40	38, 39	syl 17	. . . . . . . . 9 |- ( i e. ( 0 ... n ) -> ( (coeff ` Xp ) ` i ) = if ( i = 1 , 1 , 0 ) )
41	40	oveq1d 6317	. . . . . . . 8 |- ( i e. ( 0 ... n ) -> ( ( (coeff ` Xp ) ` i ) x. ( (coeff ` F ) ` ( n - i ) ) ) = ( if ( i = 1 , 1 , 0 ) x. ( (coeff ` F ) ` ( n - i ) ) ) )
42		ovif 6384	. . . . . . . 8 |- ( if ( i = 1 , 1 , 0 ) x. ( (coeff ` F ) ` ( n - i ) ) ) = if ( i = 1 , ( 1 x. ( (coeff ` F ) ` ( n - i ) ) ) , ( 0 x. ( (coeff ` F ) ` ( n - i ) ) ) )
43	41, 42	syl6eq 2479	. . . . . . 7 |- ( i e. ( 0 ... n ) -> ( ( (coeff ` Xp ) ` i ) x. ( (coeff ` F ) ` ( n - i ) ) ) = if ( i = 1 , ( 1 x. ( (coeff ` F ) ` ( n - i ) ) ) , ( 0 x. ( (coeff ` F ) ` ( n - i ) ) ) ) )
44	43	adantl 467	. . . . . 6 |- ( ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) /\ i e. ( 0 ... n ) ) -> ( ( (coeff ` Xp ) ` i ) x. ( (coeff ` F ) ` ( n - i ) ) ) = if ( i = 1 , ( 1 x. ( (coeff ` F ) ` ( n - i ) ) ) , ( 0 x. ( (coeff ` F ) ` ( n - i ) ) ) ) )
45	44	sumeq2dv 13757	. . . . 5 |- ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) -> sum_ i e. ( 0 ... n ) ( ( (coeff ` Xp ) ` i ) x. ( (coeff ` F ) ` ( n - i ) ) ) = sum_ i e. ( 0 ... n ) if ( i = 1 , ( 1 x. ( (coeff ` F ) ` ( n - i ) ) ) , ( 0 x. ( (coeff ` F ) ` ( n - i ) ) ) ) )
46		elsn 4010	. . . . . . . . . 10 |- ( i e. { 1 } <-> i = 1 )
47	46	bicomi 205	. . . . . . . . 9 |- ( i = 1 <-> i e. { 1 } )
48	47	a1i 11	. . . . . . . 8 |- ( ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) /\ i e. ( 0 ... n ) ) -> ( i = 1 <-> i e. { 1 } ) )
49	35	coef2 23172	. . . . . . . . . . . . 13 |- ( ( F e. (Poly ` RR ) /\ 0 e. RR ) -> (coeff ` F ) : NN0 --> RR )
50	1, 12, 49	sylancl 666	. . . . . . . . . . . 12 |- ( F e. ( (Poly ` RR ) \ { 0p } ) -> (coeff ` F ) : NN0 --> RR )
51	50	ad2antrr 730	. . . . . . . . . . 11 |- ( ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) /\ i e. ( 0 ... n ) ) -> (coeff ` F ) : NN0 --> RR )
52		fznn0sub 11832	. . . . . . . . . . . 12 |- ( i e. ( 0 ... n ) -> ( n - i ) e. NN0 )
53	52	adantl 467	. . . . . . . . . . 11 |- ( ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) /\ i e. ( 0 ... n ) ) -> ( n - i ) e. NN0 )
54	51, 53	ffvelrnd 6035	. . . . . . . . . 10 |- ( ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) /\ i e. ( 0 ... n ) ) -> ( (coeff ` F ) ` ( n - i ) ) e. RR )
55	54	recnd 9670	. . . . . . . . 9 |- ( ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) /\ i e. ( 0 ... n ) ) -> ( (coeff ` F ) ` ( n - i ) ) e. CC )
56	55	mulid2d 9662	. . . . . . . 8 |- ( ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) /\ i e. ( 0 ... n ) ) -> ( 1 x. ( (coeff ` F ) ` ( n - i ) ) ) = ( (coeff ` F ) ` ( n - i ) ) )
57	55	mul02d 9832	. . . . . . . 8 |- ( ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) /\ i e. ( 0 ... n ) ) -> ( 0 x. ( (coeff ` F ) ` ( n - i ) ) ) = 0 )
58	48, 56, 57	ifbieq12d 3936	. . . . . . 7 |- ( ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) /\ i e. ( 0 ... n ) ) -> if ( i = 1 , ( 1 x. ( (coeff ` F ) ` ( n - i ) ) ) , ( 0 x. ( (coeff ` F ) ` ( n - i ) ) ) ) = if ( i e. { 1 } , ( (coeff ` F ) ` ( n - i ) ) , 0 ) )
59	58	sumeq2dv 13757	. . . . . 6 |- ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) -> sum_ i e. ( 0 ... n ) if ( i = 1 , ( 1 x. ( (coeff ` F ) ` ( n - i ) ) ) , ( 0 x. ( (coeff ` F ) ` ( n - i ) ) ) ) = sum_ i e. ( 0 ... n ) if ( i e. { 1 } , ( (coeff ` F ) ` ( n - i ) ) , 0 ) )
60		eqeq2 2437	. . . . . . 7 |- ( 0 = if ( n = 0 , 0 , ( (coeff ` F ) ` ( n - 1 ) ) ) -> ( sum_ i e. ( 0 ... n ) if ( i e. { 1 } , ( (coeff ` F ) ` ( n - i ) ) , 0 ) = 0 <-> sum_ i e. ( 0 ... n ) if ( i e. { 1 } , ( (coeff ` F ) ` ( n - i ) ) , 0 ) = if ( n = 0 , 0 , ( (coeff ` F ) ` ( n - 1 ) ) ) ) )
61		eqeq2 2437	. . . . . . 7 |- ( ( (coeff ` F ) ` ( n - 1 ) ) = if ( n = 0 , 0 , ( (coeff ` F ) ` ( n - 1 ) ) ) -> ( sum_ i e. ( 0 ... n ) if ( i e. { 1 } , ( (coeff ` F ) ` ( n - i ) ) , 0 ) = ( (coeff ` F ) ` ( n - 1 ) ) <-> sum_ i e. ( 0 ... n ) if ( i e. { 1 } , ( (coeff ` F ) ` ( n - i ) ) , 0 ) = if ( n = 0 , 0 , ( (coeff ` F ) ` ( n - 1 ) ) ) ) )
62		oveq2 6310	. . . . . . . . . . 11 |- ( n = 0 -> ( 0 ... n ) = ( 0 ... 0 ) )
63		0z 10949	. . . . . . . . . . . 12 |- 0 e. ZZ
64		fzsn 11841	. . . . . . . . . . . 12 |- ( 0 e. ZZ -> ( 0 ... 0 ) = { 0 } )
65	63, 64	ax-mp 5	. . . . . . . . . . 11 |- ( 0 ... 0 ) = { 0 }
66	62, 65	syl6eq 2479	. . . . . . . . . 10 |- ( n = 0 -> ( 0 ... n ) = { 0 } )
67		elsni 4021	. . . . . . . . . . . . 13 |- ( i e. { 0 } -> i = 0 )
68	67	adantl 467	. . . . . . . . . . . 12 |- ( ( n = 0 /\ i e. { 0 } ) -> i = 0 )
69		ax-1ne0 9609	. . . . . . . . . . . . . 14 |- 1 =/= 0
70	69	nesymi 2697	. . . . . . . . . . . . 13 |- -. 0 = 1
71		eqeq1 2426	. . . . . . . . . . . . 13 |- ( i = 0 -> ( i = 1 <-> 0 = 1 ) )
72	70, 71	mtbiri 304	. . . . . . . . . . . 12 |- ( i = 0 -> -. i = 1 )
73	68, 72	syl 17	. . . . . . . . . . 11 |- ( ( n = 0 /\ i e. { 0 } ) -> -. i = 1 )
74	47	notbii 297	. . . . . . . . . . . 12 |- ( -. i = 1 <-> -. i e. { 1 } )
75	74	biimpi 197	. . . . . . . . . . 11 |- ( -. i = 1 -> -. i e. { 1 } )
76		iffalse 3918	. . . . . . . . . . 11 |- ( -. i e. { 1 } -> if ( i e. { 1 } , ( (coeff ` F ) ` ( n - i ) ) , 0 ) = 0 )
77	73, 75, 76	3syl 18	. . . . . . . . . 10 |- ( ( n = 0 /\ i e. { 0 } ) -> if ( i e. { 1 } , ( (coeff ` F ) ` ( n - i ) ) , 0 ) = 0 )
78	66, 77	sumeq12rdv 13761	. . . . . . . . 9 |- ( n = 0 -> sum_ i e. ( 0 ... n ) if ( i e. { 1 } , ( (coeff ` F ) ` ( n - i ) ) , 0 ) = sum_ i e. { 0 } 0 )
79		snfi 7654	. . . . . . . . . . 11 |- { 0 } e. Fin
80	79	olci 392	. . . . . . . . . 10 |- ( { 0 } C_ ( ZZ>= ` 0 ) \/ { 0 } e. Fin )
81		sumz 13776	. . . . . . . . . 10 |- ( ( { 0 } C_ ( ZZ>= ` 0 ) \/ { 0 } e. Fin ) -> sum_ i e. { 0 } 0 = 0 )
82	80, 81	ax-mp 5	. . . . . . . . 9 |- sum_ i e. { 0 } 0 = 0
83	78, 82	syl6eq 2479	. . . . . . . 8 |- ( n = 0 -> sum_ i e. ( 0 ... n ) if ( i e. { 1 } , ( (coeff ` F ) ` ( n - i ) ) , 0 ) = 0 )
84	83	adantl 467	. . . . . . 7 |- ( ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) /\ n = 0 ) -> sum_ i e. ( 0 ... n ) if ( i e. { 1 } , ( (coeff ` F ) ` ( n - i ) ) , 0 ) = 0 )
85		simpll 758	. . . . . . . 8 |- ( ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) /\ -. n = 0 ) -> F e. ( (Poly ` RR ) \ { 0p } ) )
86	33	adantr 466	. . . . . . . . 9 |- ( ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) /\ -. n = 0 ) -> n e. NN0 )
87		simpr 462	. . . . . . . . . 10 |- ( ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) /\ -. n = 0 ) -> -. n = 0 )
88	87	neqned 2627	. . . . . . . . 9 |- ( ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) /\ -. n = 0 ) -> n =/= 0 )
89		elnnne0 10884	. . . . . . . . 9 |- ( n e. NN <-> ( n e. NN0 /\ n =/= 0 ) )
90	86, 88, 89	sylanbrc 668	. . . . . . . 8 |- ( ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) /\ -. n = 0 ) -> n e. NN )
91		1nn0 10886	. . . . . . . . . . . . 13 |- 1 e. NN0
92	91	a1i 11	. . . . . . . . . . . 12 |- ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ n e. NN ) -> 1 e. NN0 )
93		simpr 462	. . . . . . . . . . . . 13 |- ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ n e. NN ) -> n e. NN )
94	93	nnnn0d 10926	. . . . . . . . . . . 12 |- ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ n e. NN ) -> n e. NN0 )
95	93	nnge1d 10653	. . . . . . . . . . . 12 |- ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ n e. NN ) -> 1 <_ n )
96		elfz2nn0 11886	. . . . . . . . . . . 12 |- ( 1 e. ( 0 ... n ) <-> ( 1 e. NN0 /\ n e. NN0 /\ 1 <_ n ) )
97	92, 94, 95, 96	syl3anbrc 1189	. . . . . . . . . . 11 |- ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ n e. NN ) -> 1 e. ( 0 ... n ) )
98	97	snssd 4142	. . . . . . . . . 10 |- ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ n e. NN ) -> { 1 } C_ ( 0 ... n ) )
99	50	ad2antrr 730	. . . . . . . . . . . . 13 |- ( ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ n e. NN ) /\ i e. { 1 } ) -> (coeff ` F ) : NN0 --> RR )
100		oveq2 6310	. . . . . . . . . . . . . . . 16 |- ( i = 1 -> ( n - i ) = ( n - 1 ) )
101	46, 100	sylbi 198	. . . . . . . . . . . . . . 15 |- ( i e. { 1 } -> ( n - i ) = ( n - 1 ) )
102	101	adantl 467	. . . . . . . . . . . . . 14 |- ( ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ n e. NN ) /\ i e. { 1 } ) -> ( n - i ) = ( n - 1 ) )
103		nnm1nn0 10912	. . . . . . . . . . . . . . 15 |- ( n e. NN -> ( n - 1 ) e. NN0 )
104	103	ad2antlr 731	. . . . . . . . . . . . . 14 |- ( ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ n e. NN ) /\ i e. { 1 } ) -> ( n - 1 ) e. NN0 )
105	102, 104	eqeltrd 2510	. . . . . . . . . . . . 13 |- ( ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ n e. NN ) /\ i e. { 1 } ) -> ( n - i ) e. NN0 )
106	99, 105	ffvelrnd 6035	. . . . . . . . . . . 12 |- ( ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ n e. NN ) /\ i e. { 1 } ) -> ( (coeff ` F ) ` ( n - i ) ) e. RR )
107	106	recnd 9670	. . . . . . . . . . 11 |- ( ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ n e. NN ) /\ i e. { 1 } ) -> ( (coeff ` F ) ` ( n - i ) ) e. CC )
108	107	ralrimiva 2839	. . . . . . . . . 10 |- ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ n e. NN ) -> A. i e. { 1 } ( (coeff ` F ) ` ( n - i ) ) e. CC )
109		fzfi 12185	. . . . . . . . . . . 12 |- ( 0 ... n ) e. Fin
110	109	olci 392	. . . . . . . . . . 11 |- ( ( 0 ... n ) C_ ( ZZ>= ` 0 ) \/ ( 0 ... n ) e. Fin )
111	110	a1i 11	. . . . . . . . . 10 |- ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ n e. NN ) -> ( ( 0 ... n ) C_ ( ZZ>= ` 0 ) \/ ( 0 ... n ) e. Fin ) )
112		sumss2 13780	. . . . . . . . . 10 |- ( ( ( { 1 } C_ ( 0 ... n ) /\ A. i e. { 1 } ( (coeff ` F ) ` ( n - i ) ) e. CC ) /\ ( ( 0 ... n ) C_ ( ZZ>= ` 0 ) \/ ( 0 ... n ) e. Fin ) ) -> sum_ i e. { 1 } ( (coeff ` F ) ` ( n - i ) ) = sum_ i e. ( 0 ... n ) if ( i e. { 1 } , ( (coeff ` F ) ` ( n - i ) ) , 0 ) )
113	98, 108, 111, 112	syl21anc 1263	. . . . . . . . 9 |- ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ n e. NN ) -> sum_ i e. { 1 } ( (coeff ` F ) ` ( n - i ) ) = sum_ i e. ( 0 ... n ) if ( i e. { 1 } , ( (coeff ` F ) ` ( n - i ) ) , 0 ) )
114	50	adantr 466	. . . . . . . . . . . 12 |- ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ n e. NN ) -> (coeff ` F ) : NN0 --> RR )
115	103	adantl 467	. . . . . . . . . . . 12 |- ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ n e. NN ) -> ( n - 1 ) e. NN0 )
116	114, 115	ffvelrnd 6035	. . . . . . . . . . 11 |- ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ n e. NN ) -> ( (coeff ` F ) ` ( n - 1 ) ) e. RR )
117	116	recnd 9670	. . . . . . . . . 10 |- ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ n e. NN ) -> ( (coeff ` F ) ` ( n - 1 ) ) e. CC )
118	100	fveq2d 5882	. . . . . . . . . . 11 |- ( i = 1 -> ( (coeff ` F ) ` ( n - i ) ) = ( (coeff ` F ) ` ( n - 1 ) ) )
119	118	sumsn 13795	. . . . . . . . . 10 |- ( ( 1 e. RR /\ ( (coeff ` F ) ` ( n - 1 ) ) e. CC ) -> sum_ i e. { 1 } ( (coeff ` F ) ` ( n - i ) ) = ( (coeff ` F ) ` ( n - 1 ) ) )
120	3, 117, 119	sylancr 667	. . . . . . . . 9 |- ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ n e. NN ) -> sum_ i e. { 1 } ( (coeff ` F ) ` ( n - i ) ) = ( (coeff ` F ) ` ( n - 1 ) ) )
121	113, 120	eqtr3d 2465	. . . . . . . 8 |- ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ n e. NN ) -> sum_ i e. ( 0 ... n ) if ( i e. { 1 } , ( (coeff ` F ) ` ( n - i ) ) , 0 ) = ( (coeff ` F ) ` ( n - 1 ) ) )
122	85, 90, 121	syl2anc 665	. . . . . . 7 |- ( ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) /\ -. n = 0 ) -> sum_ i e. ( 0 ... n ) if ( i e. { 1 } , ( (coeff ` F ) ` ( n - i ) ) , 0 ) = ( (coeff ` F ) ` ( n - 1 ) ) )
123	60, 61, 84, 122	ifbothda 3944	. . . . . 6 |- ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) -> sum_ i e. ( 0 ... n ) if ( i e. { 1 } , ( (coeff ` F ) ` ( n - i ) ) , 0 ) = if ( n = 0 , 0 , ( (coeff ` F ) ` ( n - 1 ) ) ) )
124	59, 123	eqtrd 2463	. . . . 5 |- ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) -> sum_ i e. ( 0 ... n ) if ( i = 1 , ( 1 x. ( (coeff ` F ) ` ( n - i ) ) ) , ( 0 x. ( (coeff ` F ) ` ( n - i ) ) ) ) = if ( n = 0 , 0 , ( (coeff ` F ) ` ( n - 1 ) ) ) )
125	37, 45, 124	3eqtrd 2467	. . . 4 |- ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) -> ( (coeff ` ( Xp oF x. F ) ) ` n ) = if ( n = 0 , 0 , ( (coeff ` F ) ` ( n - 1 ) ) ) )
126	30, 125	eqtrd 2463	. . 3 |- ( ( F e. ( (Poly ` RR ) \ { 0p } ) /\ n e. NN0 ) -> ( (coeff ` ( F oF x. Xp ) ) ` n ) = if ( n = 0 , 0 , ( (coeff ` F ) ` ( n - 1 ) ) ) )
127	126	mpteq2dva 4507	. 2 |- ( F e. ( (Poly ` RR ) \ { 0p } ) -> ( n e. NN0 |-> ( (coeff ` ( F oF x. Xp ) ) ` n ) ) = ( n e. NN0 |-> if ( n = 0 , 0 , ( (coeff ` F ) ` ( n - 1 ) ) ) ) )
128	16, 127	eqtrd 2463	1 |- ( F e. ( (Poly ` RR ) \ { 0p } ) -> (coeff ` ( F oF x. Xp ) ) = ( n e. NN0 |-> if ( n = 0 , 0 , ( (coeff ` F ) ` ( n - 1 ) ) ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 187   \/ wo 369   /\ wa 370   = wceq 1437   e. wcel 1868   =/= wne 2618   A.wral 2775   _Vcvv 3081   \ cdif 3433   C_ wss 3436   ifcif 3909   {csn 3996   class class class wbr 4420   |-> cmpt 4479   -->wf 5594   ` cfv 5598  (class class class)co 6302   oFcof 6540   Fincfn 7574   CCcc 9538   RRcr 9539   0cc0 9540   1c1 9541   x. cmul 9545   <_ cle 9677   - cmin 9861   NNcn 10610   NN0cn0 10870   ZZcz 10938   ZZ>=cuz 11160   ...cfz 11785   sum_csu 13740   0pc0p 22614  Polycply 23125   Xpcidp 23126  coeffccoe 23127

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-rep 4533  ax-sep 4543  ax-nul 4552  ax-pow 4599  ax-pr 4657  ax-un 6594  ax-inf2 8149  ax-cnex 9596  ax-resscn 9597  ax-1cn 9598  ax-icn 9599  ax-addcl 9600  ax-addrcl 9601  ax-mulcl 9602  ax-mulrcl 9603  ax-mulcom 9604  ax-addass 9605  ax-mulass 9606  ax-distr 9607  ax-i2m1 9608  ax-1ne0 9609  ax-1rid 9610  ax-rnegex 9611  ax-rrecex 9612  ax-cnre 9613  ax-pre-lttri 9614  ax-pre-lttrn 9615  ax-pre-ltadd 9616  ax-pre-mulgt0 9617  ax-pre-sup 9618  ax-addf 9619

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-fal 1443  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-nel 2621  df-ral 2780  df-rex 2781  df-reu 2782  df-rmo 2783  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-uni 4217  df-int 4253  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-tr 4516  df-eprel 4761  df-id 4765  df-po 4771  df-so 4772  df-fr 4809  df-se 4810  df-we 4811  df-xp 4856  df-rel 4857  df-cnv 4858  df-co 4859  df-dm 4860  df-rn 4861  df-res 4862  df-ima 4863  df-pred 5396  df-ord 5442  df-on 5443  df-lim 5444  df-suc 5445  df-iota 5562  df-fun 5600  df-fn 5601  df-f 5602  df-f1 5603  df-fo 5604  df-f1o 5605  df-fv 5606  df-isom 5607  df-riota 6264  df-ov 6305  df-oprab 6306  df-mpt2 6307  df-of 6542  df-om 6704  df-1st 6804  df-2nd 6805  df-wrecs 7033  df-recs 7095  df-rdg 7133  df-1o 7187  df-oadd 7191  df-er 7368  df-map 7479  df-pm 7480  df-en 7575  df-dom 7576  df-sdom 7577  df-fin 7578  df-sup 7959  df-inf 7960  df-oi 8028  df-card 8375  df-pnf 9678  df-mnf 9679  df-xr 9680  df-ltxr 9681  df-le 9682  df-sub 9863  df-neg 9864  df-div 10271  df-nn 10611  df-2 10669  df-3 10670  df-n0 10871  df-z 10939  df-uz 11161  df-rp 11304  df-fz 11786  df-fzo 11917  df-fl 12028  df-seq 12214  df-exp 12273  df-hash 12516  df-cj 13151  df-re 13152  df-im 13153  df-sqrt 13287  df-abs 13288  df-clim 13540  df-rlim 13541  df-sum 13741  df-0p 22615  df-ply 23129  df-idp 23130  df-coe 23131  df-dgr 23132

This theorem is referenced by:  plymulx  29433