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 25695
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 25691 . 2 class coeff
2 vf . . 3 setvar ๐‘“
3 cc 11104 . . . 4 class โ„‚
4 cply 25689 . . . 4 class Poly
53, 4cfv 6540 . . 3 class (Polyโ€˜โ„‚)
6 va . . . . . . . . 9 setvar ๐‘Ž
76cv 1540 . . . . . . . 8 class ๐‘Ž
8 vn . . . . . . . . . . 11 setvar ๐‘›
98cv 1540 . . . . . . . . . 10 class ๐‘›
10 c1 11107 . . . . . . . . . 10 class 1
11 caddc 11109 . . . . . . . . . 10 class +
129, 10, 11co 7405 . . . . . . . . 9 class (๐‘› + 1)
13 cuz 12818 . . . . . . . . 9 class โ„คโ‰ฅ
1412, 13cfv 6540 . . . . . . . 8 class (โ„คโ‰ฅโ€˜(๐‘› + 1))
157, 14cima 5678 . . . . . . 7 class (๐‘Ž โ€œ (โ„คโ‰ฅโ€˜(๐‘› + 1)))
16 cc0 11106 . . . . . . . 8 class 0
1716csn 4627 . . . . . . 7 class {0}
1815, 17wceq 1541 . . . . . 6 wff (๐‘Ž โ€œ (โ„คโ‰ฅโ€˜(๐‘› + 1))) = {0}
192cv 1540 . . . . . . 7 class ๐‘“
20 vz . . . . . . . 8 setvar ๐‘ง
21 cfz 13480 . . . . . . . . . 10 class ...
2216, 9, 21co 7405 . . . . . . . . 9 class (0...๐‘›)
23 vk . . . . . . . . . . . 12 setvar ๐‘˜
2423cv 1540 . . . . . . . . . . 11 class ๐‘˜
2524, 7cfv 6540 . . . . . . . . . 10 class (๐‘Žโ€˜๐‘˜)
2620cv 1540 . . . . . . . . . . 11 class ๐‘ง
27 cexp 14023 . . . . . . . . . . 11 class โ†‘
2826, 24, 27co 7405 . . . . . . . . . 10 class (๐‘งโ†‘๐‘˜)
29 cmul 11111 . . . . . . . . . 10 class ยท
3025, 28, 29co 7405 . . . . . . . . 9 class ((๐‘Žโ€˜๐‘˜) ยท (๐‘งโ†‘๐‘˜))
3122, 30, 23csu 15628 . . . . . . . 8 class ฮฃ๐‘˜ โˆˆ (0...๐‘›)((๐‘Žโ€˜๐‘˜) ยท (๐‘งโ†‘๐‘˜))
3220, 3, 31cmpt 5230 . . . . . . 7 class (๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ๐‘˜ โˆˆ (0...๐‘›)((๐‘Žโ€˜๐‘˜) ยท (๐‘งโ†‘๐‘˜)))
3319, 32wceq 1541 . . . . . 6 wff ๐‘“ = (๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ๐‘˜ โˆˆ (0...๐‘›)((๐‘Žโ€˜๐‘˜) ยท (๐‘งโ†‘๐‘˜)))
3418, 33wa 396 . . . . 5 wff ((๐‘Ž โ€œ (โ„คโ‰ฅโ€˜(๐‘› + 1))) = {0} โˆง ๐‘“ = (๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ๐‘˜ โˆˆ (0...๐‘›)((๐‘Žโ€˜๐‘˜) ยท (๐‘งโ†‘๐‘˜))))
35 cn0 12468 . . . . 5 class โ„•0
3634, 8, 35wrex 3070 . . . 4 wff โˆƒ๐‘› โˆˆ โ„•0 ((๐‘Ž โ€œ (โ„คโ‰ฅโ€˜(๐‘› + 1))) = {0} โˆง ๐‘“ = (๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ๐‘˜ โˆˆ (0...๐‘›)((๐‘Žโ€˜๐‘˜) ยท (๐‘งโ†‘๐‘˜))))
37 cmap 8816 . . . . 5 class โ†‘m
383, 35, 37co 7405 . . . 4 class (โ„‚ โ†‘m โ„•0)
3936, 6, 38crio 7360 . . 3 class (โ„ฉ๐‘Ž โˆˆ (โ„‚ โ†‘m โ„•0)โˆƒ๐‘› โˆˆ โ„•0 ((๐‘Ž โ€œ (โ„คโ‰ฅโ€˜(๐‘› + 1))) = {0} โˆง ๐‘“ = (๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ๐‘˜ โˆˆ (0...๐‘›)((๐‘Žโ€˜๐‘˜) ยท (๐‘งโ†‘๐‘˜)))))
402, 5, 39cmpt 5230 . 2 class (๐‘“ โˆˆ (Polyโ€˜โ„‚) โ†ฆ (โ„ฉ๐‘Ž โˆˆ (โ„‚ โ†‘m โ„•0)โˆƒ๐‘› โˆˆ โ„•0 ((๐‘Ž โ€œ (โ„คโ‰ฅโ€˜(๐‘› + 1))) = {0} โˆง ๐‘“ = (๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ๐‘˜ โˆˆ (0...๐‘›)((๐‘Žโ€˜๐‘˜) ยท (๐‘งโ†‘๐‘˜))))))
411, 40wceq 1541 1 wff coeff = (๐‘“ โˆˆ (Polyโ€˜โ„‚) โ†ฆ (โ„ฉ๐‘Ž โˆˆ (โ„‚ โ†‘m โ„•0)โˆƒ๐‘› โˆˆ โ„•0 ((๐‘Ž โ€œ (โ„คโ‰ฅโ€˜(๐‘› + 1))) = {0} โˆง ๐‘“ = (๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ๐‘˜ โˆˆ (0...๐‘›)((๐‘Žโ€˜๐‘˜) ยท (๐‘งโ†‘๐‘˜))))))
Colors of variables: wff setvar class
This definition is referenced by:  coeval  25728
  Copyright terms: Public domain W3C validator