Metamath Proof Explorer


Theorem fallfacfac

Description: Relate falling factorial to factorial. (Contributed by Scott Fenton, 5-Jan-2018)

Ref Expression
Assertion fallfacfac N 0 N N _ = N !

Proof

Step Hyp Ref Expression
1 nn0fz0 N 0 N 0 N
2 fallfacval4 N 0 N N N _ = N ! N N !
3 1 2 sylbi N 0 N N _ = N ! N N !
4 nn0cn N 0 N
5 4 subidd N 0 N N = 0
6 5 fveq2d N 0 N N ! = 0 !
7 fac0 0 ! = 1
8 6 7 eqtrdi N 0 N N ! = 1
9 8 oveq2d N 0 N ! N N ! = N ! 1
10 faccl N 0 N !
11 10 nncnd N 0 N !
12 11 div1d N 0 N ! 1 = N !
13 3 9 12 3eqtrd N 0 N N _ = N !