This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑁 ) · ( 𝐴 − 𝑁 ) ) )