Metamath Proof Explorer

Theorem fallfacfwd

Description: The forward difference of a falling factorial. (Contributed by Scott Fenton, 21-Jan-2018)

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

Proof

Step Hyp Ref Expression
1 peano2cn ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 + 1 ) ∈ ℂ )
2 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
3 fallfacval ⊢ ( ( ( 𝐴 + 1 ) ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 + 1 ) FallFac 𝑁 ) = ∏ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝐴 + 1 ) − 𝑘 ) )
4 1 2 3 syl2an ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 + 1 ) FallFac 𝑁 ) = ∏ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝐴 + 1 ) − 𝑘 ) )
5 0p1e1 ⊢ ( 0 + 1 ) = 1
6 5 oveq1i ⊢ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) = ( 1 ... ( 𝑁 − 1 ) )
7 6 prodeq1i ⊢ ∏ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( 𝐴 − ( 𝑘 − 1 ) ) = ∏ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( 𝐴 − ( 𝑘 − 1 ) )
8 7 oveq2i ⊢ ( ( 𝐴 − - 1 ) · ∏ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( 𝐴 − ( 𝑘 − 1 ) ) ) = ( ( 𝐴 − - 1 ) · ∏ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( 𝐴 − ( 𝑘 − 1 ) ) )
9 nnm1nn0 ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 )
10 9 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 − 1 ) ∈ ℕ0 )
11 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
12 10 11 eleqtrdi ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 0 ) )
13 simpll ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝐴 ∈ ℂ )
14 elfzelz ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑘 ∈ ℤ )
15 14 adantl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑘 ∈ ℤ )
16 peano2zm ⊢ ( 𝑘 ∈ ℤ → ( 𝑘 − 1 ) ∈ ℤ )
17 15 16 syl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑘 − 1 ) ∈ ℤ )
18 17 zcnd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑘 − 1 ) ∈ ℂ )
19 13 18 subcld ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝐴 − ( 𝑘 − 1 ) ) ∈ ℂ )
20 oveq1 ⊢ ( 𝑘 = 0 → ( 𝑘 − 1 ) = ( 0 − 1 ) )
21 df-neg ⊢ - 1 = ( 0 − 1 )
22 20 21 eqtr4di ⊢ ( 𝑘 = 0 → ( 𝑘 − 1 ) = - 1 )
23 22 oveq2d ⊢ ( 𝑘 = 0 → ( 𝐴 − ( 𝑘 − 1 ) ) = ( 𝐴 − - 1 ) )
24 12 19 23 fprod1p ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ∏ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 𝐴 − ( 𝑘 − 1 ) ) = ( ( 𝐴 − - 1 ) · ∏ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( 𝐴 − ( 𝑘 − 1 ) ) ) )
25 fallfacval2 ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑁 − 1 ) ∈ ℕ0 ) → ( 𝐴 FallFac ( 𝑁 − 1 ) ) = ∏ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( 𝐴 − ( 𝑘 − 1 ) ) )
26 9 25 sylan2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 FallFac ( 𝑁 − 1 ) ) = ∏ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( 𝐴 − ( 𝑘 − 1 ) ) )
27 26 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 − - 1 ) · ( 𝐴 FallFac ( 𝑁 − 1 ) ) ) = ( ( 𝐴 − - 1 ) · ∏ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ( 𝐴 − ( 𝑘 − 1 ) ) ) )
28 8 24 27 3eqtr4a ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ∏ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 𝐴 − ( 𝑘 − 1 ) ) = ( ( 𝐴 − - 1 ) · ( 𝐴 FallFac ( 𝑁 − 1 ) ) ) )
29 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑘 ∈ ℕ0 )
30 29 adantl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑘 ∈ ℕ0 )
31 30 nn0cnd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑘 ∈ ℂ )
32 1cnd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 1 ∈ ℂ )
33 13 31 32 subsub3d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝐴 − ( 𝑘 − 1 ) ) = ( ( 𝐴 + 1 ) − 𝑘 ) )
34 33 prodeq2dv ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ∏ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 𝐴 − ( 𝑘 − 1 ) ) = ∏ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝐴 + 1 ) − 𝑘 ) )
35 simpl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → 𝐴 ∈ ℂ )
36 1cnd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → 1 ∈ ℂ )
37 35 36 subnegd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 − - 1 ) = ( 𝐴 + 1 ) )
38 37 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 − - 1 ) · ( 𝐴 FallFac ( 𝑁 − 1 ) ) ) = ( ( 𝐴 + 1 ) · ( 𝐴 FallFac ( 𝑁 − 1 ) ) ) )
39 28 34 38 3eqtr3d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ∏ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝐴 + 1 ) − 𝑘 ) = ( ( 𝐴 + 1 ) · ( 𝐴 FallFac ( 𝑁 − 1 ) ) ) )
40 4 39 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 + 1 ) FallFac 𝑁 ) = ( ( 𝐴 + 1 ) · ( 𝐴 FallFac ( 𝑁 − 1 ) ) ) )
41 simpr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℕ )
42 41 nncnd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℂ )
43 42 36 npcand ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
44 43 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 FallFac ( ( 𝑁 − 1 ) + 1 ) ) = ( 𝐴 FallFac 𝑁 ) )
45 fallfacp1 ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑁 − 1 ) ∈ ℕ0 ) → ( 𝐴 FallFac ( ( 𝑁 − 1 ) + 1 ) ) = ( ( 𝐴 FallFac ( 𝑁 − 1 ) ) · ( 𝐴 − ( 𝑁 − 1 ) ) ) )
46 9 45 sylan2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 FallFac ( ( 𝑁 − 1 ) + 1 ) ) = ( ( 𝐴 FallFac ( 𝑁 − 1 ) ) · ( 𝐴 − ( 𝑁 − 1 ) ) ) )
47 44 46 eqtr3d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 FallFac 𝑁 ) = ( ( 𝐴 FallFac ( 𝑁 − 1 ) ) · ( 𝐴 − ( 𝑁 − 1 ) ) ) )
48 40 47 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 + 1 ) FallFac 𝑁 ) − ( 𝐴 FallFac 𝑁 ) ) = ( ( ( 𝐴 + 1 ) · ( 𝐴 FallFac ( 𝑁 − 1 ) ) ) − ( ( 𝐴 FallFac ( 𝑁 − 1 ) ) · ( 𝐴 − ( 𝑁 − 1 ) ) ) ) )
49 fallfaccl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑁 − 1 ) ∈ ℕ0 ) → ( 𝐴 FallFac ( 𝑁 − 1 ) ) ∈ ℂ )
50 9 49 sylan2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 FallFac ( 𝑁 − 1 ) ) ∈ ℂ )
51 10 nn0cnd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 − 1 ) ∈ ℂ )
52 35 51 subcld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 − ( 𝑁 − 1 ) ) ∈ ℂ )
53 50 52 mulcomd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 FallFac ( 𝑁 − 1 ) ) · ( 𝐴 − ( 𝑁 − 1 ) ) ) = ( ( 𝐴 − ( 𝑁 − 1 ) ) · ( 𝐴 FallFac ( 𝑁 − 1 ) ) ) )
54 53 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 + 1 ) · ( 𝐴 FallFac ( 𝑁 − 1 ) ) ) − ( ( 𝐴 FallFac ( 𝑁 − 1 ) ) · ( 𝐴 − ( 𝑁 − 1 ) ) ) ) = ( ( ( 𝐴 + 1 ) · ( 𝐴 FallFac ( 𝑁 − 1 ) ) ) − ( ( 𝐴 − ( 𝑁 − 1 ) ) · ( 𝐴 FallFac ( 𝑁 − 1 ) ) ) ) )
55 1 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 + 1 ) ∈ ℂ )
56 55 52 50 subdird ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 + 1 ) − ( 𝐴 − ( 𝑁 − 1 ) ) ) · ( 𝐴 FallFac ( 𝑁 − 1 ) ) ) = ( ( ( 𝐴 + 1 ) · ( 𝐴 FallFac ( 𝑁 − 1 ) ) ) − ( ( 𝐴 − ( 𝑁 − 1 ) ) · ( 𝐴 FallFac ( 𝑁 − 1 ) ) ) ) )
57 35 36 51 pnncand ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 + 1 ) − ( 𝐴 − ( 𝑁 − 1 ) ) ) = ( 1 + ( 𝑁 − 1 ) ) )
58 36 42 pncan3d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( 1 + ( 𝑁 − 1 ) ) = 𝑁 )
59 57 58 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 + 1 ) − ( 𝐴 − ( 𝑁 − 1 ) ) ) = 𝑁 )
60 59 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 + 1 ) − ( 𝐴 − ( 𝑁 − 1 ) ) ) · ( 𝐴 FallFac ( 𝑁 − 1 ) ) ) = ( 𝑁 · ( 𝐴 FallFac ( 𝑁 − 1 ) ) ) )
61 54 56 60 3eqtr2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 + 1 ) · ( 𝐴 FallFac ( 𝑁 − 1 ) ) ) − ( ( 𝐴 FallFac ( 𝑁 − 1 ) ) · ( 𝐴 − ( 𝑁 − 1 ) ) ) ) = ( 𝑁 · ( 𝐴 FallFac ( 𝑁 − 1 ) ) ) )
62 48 61 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 + 1 ) FallFac 𝑁 ) − ( 𝐴 FallFac 𝑁 ) ) = ( 𝑁 · ( 𝐴 FallFac ( 𝑁 − 1 ) ) ) )