Metamath Proof Explorer


Theorem risefac0

Description: The value of the rising factorial when N = 0 . (Contributed by Scott Fenton, 5-Jan-2018)

Ref Expression
Assertion risefac0 A A 0 = 1

Proof

Step Hyp Ref Expression
1 0nn0 0 0
2 risefacval A 0 0 A 0 = k = 0 0 1 A + k
3 1 2 mpan2 A A 0 = k = 0 0 1 A + k
4 risefall0lem 0 0 1 =
5 4 prodeq1i k = 0 0 1 A + k = k A + k
6 prod0 k A + k = 1
7 5 6 eqtri k = 0 0 1 A + k = 1
8 3 7 eqtrdi A A 0 = 1