Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-fwddifn Structured version   Visualization version   GIF version

Definition df-fwddifn 34799
Description: Define the nth forward difference operator. This works out to be the forward difference operator iterated ๐‘› times. (Contributed by Scott Fenton, 28-May-2020.)
Assertion
Ref Expression
df-fwddifn โ–ณn = (๐‘› โˆˆ โ„•0, ๐‘“ โˆˆ (โ„‚ โ†‘pm โ„‚) โ†ฆ (๐‘ฅ โˆˆ {๐‘ฆ โˆˆ โ„‚ โˆฃ โˆ€๐‘˜ โˆˆ (0...๐‘›)(๐‘ฆ + ๐‘˜) โˆˆ dom ๐‘“} โ†ฆ ฮฃ๐‘˜ โˆˆ (0...๐‘›)((๐‘›C๐‘˜) ยท ((-1โ†‘(๐‘› โˆ’ ๐‘˜)) ยท (๐‘“โ€˜(๐‘ฅ + ๐‘˜))))))
Distinct variable group:   ๐‘“,๐‘›,๐‘ฅ,๐‘ฆ,๐‘˜

Detailed syntax breakdown of Definition df-fwddifn
StepHypRef Expression
1 cfwddifn 34798 . 2 class โ–ณn
2 vn . . 3 setvar ๐‘›
3 vf . . 3 setvar ๐‘“
4 cn0 12421 . . 3 class โ„•0
5 cc 11057 . . . 4 class โ„‚
6 cpm 8772 . . . 4 class โ†‘pm
75, 5, 6co 7361 . . 3 class (โ„‚ โ†‘pm โ„‚)
8 vx . . . 4 setvar ๐‘ฅ
9 vy . . . . . . . . 9 setvar ๐‘ฆ
109cv 1541 . . . . . . . 8 class ๐‘ฆ
11 vk . . . . . . . . 9 setvar ๐‘˜
1211cv 1541 . . . . . . . 8 class ๐‘˜
13 caddc 11062 . . . . . . . 8 class +
1410, 12, 13co 7361 . . . . . . 7 class (๐‘ฆ + ๐‘˜)
153cv 1541 . . . . . . . 8 class ๐‘“
1615cdm 5637 . . . . . . 7 class dom ๐‘“
1714, 16wcel 2107 . . . . . 6 wff (๐‘ฆ + ๐‘˜) โˆˆ dom ๐‘“
18 cc0 11059 . . . . . . 7 class 0
192cv 1541 . . . . . . 7 class ๐‘›
20 cfz 13433 . . . . . . 7 class ...
2118, 19, 20co 7361 . . . . . 6 class (0...๐‘›)
2217, 11, 21wral 3061 . . . . 5 wff โˆ€๐‘˜ โˆˆ (0...๐‘›)(๐‘ฆ + ๐‘˜) โˆˆ dom ๐‘“
2322, 9, 5crab 3406 . . . 4 class {๐‘ฆ โˆˆ โ„‚ โˆฃ โˆ€๐‘˜ โˆˆ (0...๐‘›)(๐‘ฆ + ๐‘˜) โˆˆ dom ๐‘“}
24 cbc 14211 . . . . . . 7 class C
2519, 12, 24co 7361 . . . . . 6 class (๐‘›C๐‘˜)
26 c1 11060 . . . . . . . . 9 class 1
2726cneg 11394 . . . . . . . 8 class -1
28 cmin 11393 . . . . . . . . 9 class โˆ’
2919, 12, 28co 7361 . . . . . . . 8 class (๐‘› โˆ’ ๐‘˜)
30 cexp 13976 . . . . . . . 8 class โ†‘
3127, 29, 30co 7361 . . . . . . 7 class (-1โ†‘(๐‘› โˆ’ ๐‘˜))
328cv 1541 . . . . . . . . 9 class ๐‘ฅ
3332, 12, 13co 7361 . . . . . . . 8 class (๐‘ฅ + ๐‘˜)
3433, 15cfv 6500 . . . . . . 7 class (๐‘“โ€˜(๐‘ฅ + ๐‘˜))
35 cmul 11064 . . . . . . 7 class ยท
3631, 34, 35co 7361 . . . . . 6 class ((-1โ†‘(๐‘› โˆ’ ๐‘˜)) ยท (๐‘“โ€˜(๐‘ฅ + ๐‘˜)))
3725, 36, 35co 7361 . . . . 5 class ((๐‘›C๐‘˜) ยท ((-1โ†‘(๐‘› โˆ’ ๐‘˜)) ยท (๐‘“โ€˜(๐‘ฅ + ๐‘˜))))
3821, 37, 11csu 15579 . . . 4 class ฮฃ๐‘˜ โˆˆ (0...๐‘›)((๐‘›C๐‘˜) ยท ((-1โ†‘(๐‘› โˆ’ ๐‘˜)) ยท (๐‘“โ€˜(๐‘ฅ + ๐‘˜))))
398, 23, 38cmpt 5192 . . 3 class (๐‘ฅ โˆˆ {๐‘ฆ โˆˆ โ„‚ โˆฃ โˆ€๐‘˜ โˆˆ (0...๐‘›)(๐‘ฆ + ๐‘˜) โˆˆ dom ๐‘“} โ†ฆ ฮฃ๐‘˜ โˆˆ (0...๐‘›)((๐‘›C๐‘˜) ยท ((-1โ†‘(๐‘› โˆ’ ๐‘˜)) ยท (๐‘“โ€˜(๐‘ฅ + ๐‘˜)))))
402, 3, 4, 7, 39cmpo 7363 . 2 class (๐‘› โˆˆ โ„•0, ๐‘“ โˆˆ (โ„‚ โ†‘pm โ„‚) โ†ฆ (๐‘ฅ โˆˆ {๐‘ฆ โˆˆ โ„‚ โˆฃ โˆ€๐‘˜ โˆˆ (0...๐‘›)(๐‘ฆ + ๐‘˜) โˆˆ dom ๐‘“} โ†ฆ ฮฃ๐‘˜ โˆˆ (0...๐‘›)((๐‘›C๐‘˜) ยท ((-1โ†‘(๐‘› โˆ’ ๐‘˜)) ยท (๐‘“โ€˜(๐‘ฅ + ๐‘˜))))))
411, 40wceq 1542 1 wff โ–ณn = (๐‘› โˆˆ โ„•0, ๐‘“ โˆˆ (โ„‚ โ†‘pm โ„‚) โ†ฆ (๐‘ฅ โˆˆ {๐‘ฆ โˆˆ โ„‚ โˆฃ โˆ€๐‘˜ โˆˆ (0...๐‘›)(๐‘ฆ + ๐‘˜) โˆˆ dom ๐‘“} โ†ฆ ฮฃ๐‘˜ โˆˆ (0...๐‘›)((๐‘›C๐‘˜) ยท ((-1โ†‘(๐‘› โˆ’ ๐‘˜)) ยท (๐‘“โ€˜(๐‘ฅ + ๐‘˜))))))
Colors of variables: wff setvar class
This definition is referenced by:  fwddifnval  34801
  Copyright terms: Public domain W3C validator