Theorem fallfacp1

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

	Ref	Expression
Assertion	fallfacp1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 FallFac ( 𝑁 + 1 ) ) = ( ( 𝐴 FallFac 𝑁 ) · ( 𝐴 − 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		nn0cn	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ )
2	1	adantl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℂ )
3		1cnd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → 1 ∈ ℂ )
4	2 3	pncand	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
5	4	oveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) = ( 0 ... 𝑁 ) )
6	5	prodeq1d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ∏ 𝑘 ∈ ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) ( 𝐴 − 𝑘 ) = ∏ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝐴 − 𝑘 ) )
7		elnn0uz	⊢ ( 𝑁 ∈ ℕ0 ↔ 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
8	7	biimpi	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
9	8	adantl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
10		elfznn0	⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℕ0 )
11	10	nn0cnd	⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℂ )
12		subcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( 𝐴 − 𝑘 ) ∈ ℂ )
13	11 12	sylan2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝐴 − 𝑘 ) ∈ ℂ )
14	13	adantlr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝐴 − 𝑘 ) ∈ ℂ )
15		oveq2	⊢ ( 𝑘 = 𝑁 → ( 𝐴 − 𝑘 ) = ( 𝐴 − 𝑁 ) )
16	9 14 15	fprodm1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ∏ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝐴 − 𝑘 ) = ( ∏ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 𝐴 − 𝑘 ) · ( 𝐴 − 𝑁 ) ) )
17	6 16	eqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ∏ 𝑘 ∈ ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) ( 𝐴 − 𝑘 ) = ( ∏ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 𝐴 − 𝑘 ) · ( 𝐴 − 𝑁 ) ) )
18		peano2nn0	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
19		fallfacval	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑁 + 1 ) ∈ ℕ0 ) → ( 𝐴 FallFac ( 𝑁 + 1 ) ) = ∏ 𝑘 ∈ ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) ( 𝐴 − 𝑘 ) )
20	18 19	sylan2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 FallFac ( 𝑁 + 1 ) ) = ∏ 𝑘 ∈ ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) ( 𝐴 − 𝑘 ) )
21		fallfacval	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 FallFac 𝑁 ) = ∏ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 𝐴 − 𝑘 ) )
22	21	oveq1d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 FallFac 𝑁 ) · ( 𝐴 − 𝑁 ) ) = ( ∏ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 𝐴 − 𝑘 ) · ( 𝐴 − 𝑁 ) ) )
23	17 20 22	3eqtr4d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 FallFac ( 𝑁 + 1 ) ) = ( ( 𝐴 FallFac 𝑁 ) · ( 𝐴 − 𝑁 ) ) )