Theorem fallfac0

Description: The value of the falling factorial when N = 0 . (Contributed by Scott Fenton, 5-Jan-2018)

	Ref	Expression
Assertion	fallfac0	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 FallFac 0 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		0nn0	⊢ 0 ∈ ℕ0
2		fallrisefac	⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ∈ ℕ0 ) → ( 𝐴 FallFac 0 ) = ( ( - 1 ↑ 0 ) · ( - 𝐴 RiseFac 0 ) ) )
3	1 2	mpan2	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 FallFac 0 ) = ( ( - 1 ↑ 0 ) · ( - 𝐴 RiseFac 0 ) ) )
4		neg1cn	⊢ - 1 ∈ ℂ
5		exp0	⊢ ( - 1 ∈ ℂ → ( - 1 ↑ 0 ) = 1 )
6	4 5	mp1i	⊢ ( 𝐴 ∈ ℂ → ( - 1 ↑ 0 ) = 1 )
7		negcl	⊢ ( 𝐴 ∈ ℂ → - 𝐴 ∈ ℂ )
8		risefac0	⊢ ( - 𝐴 ∈ ℂ → ( - 𝐴 RiseFac 0 ) = 1 )
9	7 8	syl	⊢ ( 𝐴 ∈ ℂ → ( - 𝐴 RiseFac 0 ) = 1 )
10	6 9	oveq12d	⊢ ( 𝐴 ∈ ℂ → ( ( - 1 ↑ 0 ) · ( - 𝐴 RiseFac 0 ) ) = ( 1 · 1 ) )
11		1t1e1	⊢ ( 1 · 1 ) = 1
12	10 11	eqtrdi	⊢ ( 𝐴 ∈ ℂ → ( ( - 1 ↑ 0 ) · ( - 𝐴 RiseFac 0 ) ) = 1 )
13	3 12	eqtrd	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 FallFac 0 ) = 1 )