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 )