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

Definition df-coe 25938
Description: Define the coefficient function for a polynomial. (Contributed by Mario Carneiro, 22-Jul-2014.)
Assertion
Ref Expression
df-coe coeff = (๐‘“ โˆˆ (Polyโ€˜โ„‚) โ†ฆ (โ„ฉ๐‘Ž โˆˆ (โ„‚ โ†‘m โ„•0)โˆƒ๐‘› โˆˆ โ„•0 ((๐‘Ž โ€œ (โ„คโ‰ฅโ€˜(๐‘› + 1))) = {0} โˆง ๐‘“ = (๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ๐‘˜ โˆˆ (0...๐‘›)((๐‘Žโ€˜๐‘˜) ยท (๐‘งโ†‘๐‘˜))))))
Distinct variable group:   ๐‘“,๐‘Ž,๐‘˜,๐‘›,๐‘ง

Detailed syntax breakdown of Definition df-coe
StepHypRef Expression
1 ccoe 25934 . 2 class coeff
2 vf . . 3 setvar ๐‘“
3 cc 11112 . . . 4 class โ„‚
4 cply 25932 . . . 4 class Poly
53, 4cfv 6544 . . 3 class (Polyโ€˜โ„‚)
6 va . . . . . . . . 9 setvar ๐‘Ž
76cv 1538 . . . . . . . 8 class ๐‘Ž
8 vn . . . . . . . . . . 11 setvar ๐‘›
98cv 1538 . . . . . . . . . 10 class ๐‘›
10 c1 11115 . . . . . . . . . 10 class 1
11 caddc 11117 . . . . . . . . . 10 class +
129, 10, 11co 7413 . . . . . . . . 9 class (๐‘› + 1)
13 cuz 12828 . . . . . . . . 9 class โ„คโ‰ฅ
1412, 13cfv 6544 . . . . . . . 8 class (โ„คโ‰ฅโ€˜(๐‘› + 1))
157, 14cima 5680 . . . . . . 7 class (๐‘Ž โ€œ (โ„คโ‰ฅโ€˜(๐‘› + 1)))
16 cc0 11114 . . . . . . . 8 class 0
1716csn 4629 . . . . . . 7 class {0}
1815, 17wceq 1539 . . . . . 6 wff (๐‘Ž โ€œ (โ„คโ‰ฅโ€˜(๐‘› + 1))) = {0}
192cv 1538 . . . . . . 7 class ๐‘“
20 vz . . . . . . . 8 setvar ๐‘ง
21 cfz 13490 . . . . . . . . . 10 class ...
2216, 9, 21co 7413 . . . . . . . . 9 class (0...๐‘›)
23 vk . . . . . . . . . . . 12 setvar ๐‘˜
2423cv 1538 . . . . . . . . . . 11 class ๐‘˜
2524, 7cfv 6544 . . . . . . . . . 10 class (๐‘Žโ€˜๐‘˜)
2620cv 1538 . . . . . . . . . . 11 class ๐‘ง
27 cexp 14033 . . . . . . . . . . 11 class โ†‘
2826, 24, 27co 7413 . . . . . . . . . 10 class (๐‘งโ†‘๐‘˜)
29 cmul 11119 . . . . . . . . . 10 class ยท
3025, 28, 29co 7413 . . . . . . . . 9 class ((๐‘Žโ€˜๐‘˜) ยท (๐‘งโ†‘๐‘˜))
3122, 30, 23csu 15638 . . . . . . . 8 class ฮฃ๐‘˜ โˆˆ (0...๐‘›)((๐‘Žโ€˜๐‘˜) ยท (๐‘งโ†‘๐‘˜))
3220, 3, 31cmpt 5232 . . . . . . 7 class (๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ๐‘˜ โˆˆ (0...๐‘›)((๐‘Žโ€˜๐‘˜) ยท (๐‘งโ†‘๐‘˜)))
3319, 32wceq 1539 . . . . . 6 wff ๐‘“ = (๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ๐‘˜ โˆˆ (0...๐‘›)((๐‘Žโ€˜๐‘˜) ยท (๐‘งโ†‘๐‘˜)))
3418, 33wa 394 . . . . 5 wff ((๐‘Ž โ€œ (โ„คโ‰ฅโ€˜(๐‘› + 1))) = {0} โˆง ๐‘“ = (๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ๐‘˜ โˆˆ (0...๐‘›)((๐‘Žโ€˜๐‘˜) ยท (๐‘งโ†‘๐‘˜))))
35 cn0 12478 . . . . 5 class โ„•0
3634, 8, 35wrex 3068 . . . 4 wff โˆƒ๐‘› โˆˆ โ„•0 ((๐‘Ž โ€œ (โ„คโ‰ฅโ€˜(๐‘› + 1))) = {0} โˆง ๐‘“ = (๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ๐‘˜ โˆˆ (0...๐‘›)((๐‘Žโ€˜๐‘˜) ยท (๐‘งโ†‘๐‘˜))))
37 cmap 8824 . . . . 5 class โ†‘m
383, 35, 37co 7413 . . . 4 class (โ„‚ โ†‘m โ„•0)
3936, 6, 38crio 7368 . . 3 class (โ„ฉ๐‘Ž โˆˆ (โ„‚ โ†‘m โ„•0)โˆƒ๐‘› โˆˆ โ„•0 ((๐‘Ž โ€œ (โ„คโ‰ฅโ€˜(๐‘› + 1))) = {0} โˆง ๐‘“ = (๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ๐‘˜ โˆˆ (0...๐‘›)((๐‘Žโ€˜๐‘˜) ยท (๐‘งโ†‘๐‘˜)))))
402, 5, 39cmpt 5232 . 2 class (๐‘“ โˆˆ (Polyโ€˜โ„‚) โ†ฆ (โ„ฉ๐‘Ž โˆˆ (โ„‚ โ†‘m โ„•0)โˆƒ๐‘› โˆˆ โ„•0 ((๐‘Ž โ€œ (โ„คโ‰ฅโ€˜(๐‘› + 1))) = {0} โˆง ๐‘“ = (๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ๐‘˜ โˆˆ (0...๐‘›)((๐‘Žโ€˜๐‘˜) ยท (๐‘งโ†‘๐‘˜))))))
411, 40wceq 1539 1 wff coeff = (๐‘“ โˆˆ (Polyโ€˜โ„‚) โ†ฆ (โ„ฉ๐‘Ž โˆˆ (โ„‚ โ†‘m โ„•0)โˆƒ๐‘› โˆˆ โ„•0 ((๐‘Ž โ€œ (โ„คโ‰ฅโ€˜(๐‘› + 1))) = {0} โˆง ๐‘“ = (๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ๐‘˜ โˆˆ (0...๐‘›)((๐‘Žโ€˜๐‘˜) ยท (๐‘งโ†‘๐‘˜))))))
Colors of variables: wff setvar class
This definition is referenced by:  coeval  25971
  Copyright terms: Public domain W3C validator