Metamath Proof Explorer


Theorem fallfac1

Description: The value of falling factorial at one. (Contributed by Scott Fenton, 5-Jan-2018)

Ref Expression
Assertion fallfac1 A A 1 _ = A

Proof

Step Hyp Ref Expression
1 0p1e1 0 + 1 = 1
2 1 oveq2i A 0 + 1 _ = A 1 _
3 0nn0 0 0
4 fallfacp1 A 0 0 A 0 + 1 _ = A 0 _ A 0
5 3 4 mpan2 A A 0 + 1 _ = A 0 _ A 0
6 fallfac0 A A 0 _ = 1
7 subid1 A A 0 = A
8 6 7 oveq12d A A 0 _ A 0 = 1 A
9 mulid2 A 1 A = A
10 5 8 9 3eqtrd A A 0 + 1 _ = A
11 2 10 eqtr3id A A 1 _ = A