![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-coe | Structured version Visualization version Unicode version |
Description: Define the coefficient function for a polynomial. (Contributed by Mario Carneiro, 22-Jul-2014.) |
Ref | Expression |
---|---|
df-coe |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ccoe 23189 |
. 2
![]() | |
2 | vf |
. . 3
![]() ![]() | |
3 | cc 9563 |
. . . 4
![]() ![]() | |
4 | cply 23187 |
. . . 4
![]() | |
5 | 3, 4 | cfv 5601 |
. . 3
![]() ![]() ![]() ![]() ![]() |
6 | va |
. . . . . . . . 9
![]() ![]() | |
7 | 6 | cv 1454 |
. . . . . . . 8
![]() ![]() |
8 | vn |
. . . . . . . . . . 11
![]() ![]() | |
9 | 8 | cv 1454 |
. . . . . . . . . 10
![]() ![]() |
10 | c1 9566 |
. . . . . . . . . 10
![]() ![]() | |
11 | caddc 9568 |
. . . . . . . . . 10
![]() ![]() | |
12 | 9, 10, 11 | co 6315 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() |
13 | cuz 11188 |
. . . . . . . . 9
![]() ![]() | |
14 | 12, 13 | cfv 5601 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
15 | 7, 14 | cima 4856 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
16 | cc0 9565 |
. . . . . . . 8
![]() ![]() | |
17 | 16 | csn 3980 |
. . . . . . 7
![]() ![]() ![]() ![]() |
18 | 15, 17 | wceq 1455 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
19 | 2 | cv 1454 |
. . . . . . 7
![]() ![]() |
20 | vz |
. . . . . . . 8
![]() ![]() | |
21 | cfz 11813 |
. . . . . . . . . 10
![]() ![]() | |
22 | 16, 9, 21 | co 6315 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() |
23 | vk |
. . . . . . . . . . . 12
![]() ![]() | |
24 | 23 | cv 1454 |
. . . . . . . . . . 11
![]() ![]() |
25 | 24, 7 | cfv 5601 |
. . . . . . . . . 10
![]() ![]() ![]() ![]() ![]() ![]() |
26 | 20 | cv 1454 |
. . . . . . . . . . 11
![]() ![]() |
27 | cexp 12304 |
. . . . . . . . . . 11
![]() ![]() | |
28 | 26, 24, 27 | co 6315 |
. . . . . . . . . 10
![]() ![]() ![]() ![]() ![]() ![]() |
29 | cmul 9570 |
. . . . . . . . . 10
![]() ![]() | |
30 | 25, 28, 29 | co 6315 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
31 | 22, 30, 23 | csu 13801 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
32 | 20, 3, 31 | cmpt 4475 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
33 | 19, 32 | wceq 1455 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
34 | 18, 33 | wa 375 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
35 | cn0 10898 |
. . . . 5
![]() ![]() | |
36 | 34, 8, 35 | wrex 2750 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
37 | cmap 7498 |
. . . . 5
![]() ![]() | |
38 | 3, 35, 37 | co 6315 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() |
39 | 36, 6, 38 | crio 6276 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
40 | 2, 5, 39 | cmpt 4475 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
41 | 1, 40 | wceq 1455 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
This definition is referenced by: coeval 23226 |
Copyright terms: Public domain | W3C validator |