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 e. CC -> ( A FallFac 1 ) = A )

Proof

Step Hyp Ref Expression
1 0p1e1
 |-  ( 0 + 1 ) = 1
2 1 oveq2i
 |-  ( A FallFac ( 0 + 1 ) ) = ( A FallFac 1 )
3 0nn0
 |-  0 e. NN0
4 fallfacp1
 |-  ( ( A e. CC /\ 0 e. NN0 ) -> ( A FallFac ( 0 + 1 ) ) = ( ( A FallFac 0 ) x. ( A - 0 ) ) )
5 3 4 mpan2
 |-  ( A e. CC -> ( A FallFac ( 0 + 1 ) ) = ( ( A FallFac 0 ) x. ( A - 0 ) ) )
6 fallfac0
 |-  ( A e. CC -> ( A FallFac 0 ) = 1 )
7 subid1
 |-  ( A e. CC -> ( A - 0 ) = A )
8 6 7 oveq12d
 |-  ( A e. CC -> ( ( A FallFac 0 ) x. ( A - 0 ) ) = ( 1 x. A ) )
9 mulid2
 |-  ( A e. CC -> ( 1 x. A ) = A )
10 5 8 9 3eqtrd
 |-  ( A e. CC -> ( A FallFac ( 0 + 1 ) ) = A )
11 2 10 eqtr3id
 |-  ( A e. CC -> ( A FallFac 1 ) = A )