Metamath Proof Explorer


Theorem fallfac1

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

Ref Expression
Assertion fallfac1 ( 𝐴 ∈ ℂ → ( 𝐴 FallFac 1 ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 0p1e1 ( 0 + 1 ) = 1
2 1 oveq2i ( 𝐴 FallFac ( 0 + 1 ) ) = ( 𝐴 FallFac 1 )
3 0nn0 0 ∈ ℕ0
4 fallfacp1 ( ( 𝐴 ∈ ℂ ∧ 0 ∈ ℕ0 ) → ( 𝐴 FallFac ( 0 + 1 ) ) = ( ( 𝐴 FallFac 0 ) · ( 𝐴 − 0 ) ) )
5 3 4 mpan2 ( 𝐴 ∈ ℂ → ( 𝐴 FallFac ( 0 + 1 ) ) = ( ( 𝐴 FallFac 0 ) · ( 𝐴 − 0 ) ) )
6 fallfac0 ( 𝐴 ∈ ℂ → ( 𝐴 FallFac 0 ) = 1 )
7 subid1 ( 𝐴 ∈ ℂ → ( 𝐴 − 0 ) = 𝐴 )
8 6 7 oveq12d ( 𝐴 ∈ ℂ → ( ( 𝐴 FallFac 0 ) · ( 𝐴 − 0 ) ) = ( 1 · 𝐴 ) )
9 mulid2 ( 𝐴 ∈ ℂ → ( 1 · 𝐴 ) = 𝐴 )
10 5 8 9 3eqtrd ( 𝐴 ∈ ℂ → ( 𝐴 FallFac ( 0 + 1 ) ) = 𝐴 )
11 2 10 eqtr3id ( 𝐴 ∈ ℂ → ( 𝐴 FallFac 1 ) = 𝐴 )