Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-coe Structured version   Unicode version

Definition df-coe 20109
 Description: Define the coefficient function for a polynomial. (Contributed by Mario Carneiro, 22-Jul-2014.)
Assertion
Ref Expression
df-coe coeff Poly
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-coe
StepHypRef Expression
1 ccoe 20105 . 2 coeff
2 vf . . 3
3 cc 8988 . . . 4
4 cply 20103 . . . 4 Poly
53, 4cfv 5454 . . 3 Poly
6 va . . . . . . . . 9
76cv 1651 . . . . . . . 8
8 vn . . . . . . . . . . 11
98cv 1651 . . . . . . . . . 10
10 c1 8991 . . . . . . . . . 10
11 caddc 8993 . . . . . . . . . 10
129, 10, 11co 6081 . . . . . . . . 9
13 cuz 10488 . . . . . . . . 9
1412, 13cfv 5454 . . . . . . . 8
157, 14cima 4881 . . . . . . 7
16 cc0 8990 . . . . . . . 8
1716csn 3814 . . . . . . 7
1815, 17wceq 1652 . . . . . 6
192cv 1651 . . . . . . 7
20 vz . . . . . . . 8
21 cfz 11043 . . . . . . . . . 10
2216, 9, 21co 6081 . . . . . . . . 9
23 vk . . . . . . . . . . . 12
2423cv 1651 . . . . . . . . . . 11
2524, 7cfv 5454 . . . . . . . . . 10
2620cv 1651 . . . . . . . . . . 11
27 cexp 11382 . . . . . . . . . . 11
2826, 24, 27co 6081 . . . . . . . . . 10
29 cmul 8995 . . . . . . . . . 10
3025, 28, 29co 6081 . . . . . . . . 9
3122, 30, 23csu 12479 . . . . . . . 8
3220, 3, 31cmpt 4266 . . . . . . 7
3319, 32wceq 1652 . . . . . 6
3418, 33wa 359 . . . . 5
35 cn0 10221 . . . . 5
3634, 8, 35wrex 2706 . . . 4
37 cmap 7018 . . . . 5
383, 35, 37co 6081 . . . 4
3936, 6, 38crio 6542 . . 3
402, 5, 39cmpt 4266 . 2 Poly
411, 40wceq 1652 1 coeff Poly
 Colors of variables: wff set class This definition is referenced by:  coeval  20142
 Copyright terms: Public domain W3C validator