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		mullid	⊢ ( 𝐴 ∈ ℂ → ( 1 · 𝐴 ) = 𝐴 )
10	5 8 9	3eqtrd	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 FallFac ( 0 + 1 ) ) = 𝐴 )
11	2 10	eqtr3id	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 FallFac 1 ) = 𝐴 )