Metamath Proof Explorer

Theorem risefac1

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

Ref Expression
Assertion risefac1 
|- ( A e. CC -> ( A RiseFac 1 ) = A )

Proof

Step Hyp Ref Expression
1 0p1e1 
 |-  ( 0 + 1 ) = 1
2 1 oveq2i 
 |-  ( A RiseFac ( 0 + 1 ) ) = ( A RiseFac 1 )
3 0nn0 
 |-  0 e. NN0
4 risefacp1 
 |-  ( ( A e. CC /\ 0 e. NN0 ) -> ( A RiseFac ( 0 + 1 ) ) = ( ( A RiseFac 0 ) x. ( A + 0 ) ) )
5 3 4 mpan2 
 |-  ( A e. CC -> ( A RiseFac ( 0 + 1 ) ) = ( ( A RiseFac 0 ) x. ( A + 0 ) ) )
6 risefac0 
 |-  ( A e. CC -> ( A RiseFac 0 ) = 1 )
7 addrid 
 |-  ( A e. CC -> ( A + 0 ) = A )
8 6 7 oveq12d 
 |-  ( A e. CC -> ( ( A RiseFac 0 ) x. ( A + 0 ) ) = ( 1 x. A ) )
9 mullid 
 |-  ( A e. CC -> ( 1 x. A ) = A )
10 5 8 9 3eqtrd 
 |-  ( A e. CC -> ( A RiseFac ( 0 + 1 ) ) = A )
11 2 10 eqtr3id 
 |-  ( A e. CC -> ( A RiseFac 1 ) = A )