Metamath Proof Explorer

Theorem fallfacfwd

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

Ref Expression
Assertion fallfacfwd 
|- ( ( A e. CC /\ N e. NN ) -> ( ( ( A + 1 ) FallFac N ) - ( A FallFac N ) ) = ( N x. ( A FallFac ( N - 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 peano2cn 
 |-  ( A e. CC -> ( A + 1 ) e. CC )
2 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
3 fallfacval 
 |-  ( ( ( A + 1 ) e. CC /\ N e. NN0 ) -> ( ( A + 1 ) FallFac N ) = prod_ k e. ( 0 ... ( N - 1 ) ) ( ( A + 1 ) - k ) )
4 1 2 3 syl2an 
 |-  ( ( A e. CC /\ N e. NN ) -> ( ( A + 1 ) FallFac N ) = prod_ k e. ( 0 ... ( N - 1 ) ) ( ( A + 1 ) - k ) )
5 0p1e1 
 |-  ( 0 + 1 ) = 1
6 5 oveq1i 
 |-  ( ( 0 + 1 ) ... ( N - 1 ) ) = ( 1 ... ( N - 1 ) )
7 6 prodeq1i 
 |-  prod_ k e. ( ( 0 + 1 ) ... ( N - 1 ) ) ( A - ( k - 1 ) ) = prod_ k e. ( 1 ... ( N - 1 ) ) ( A - ( k - 1 ) )
8 7 oveq2i 
 |-  ( ( A - -u 1 ) x. prod_ k e. ( ( 0 + 1 ) ... ( N - 1 ) ) ( A - ( k - 1 ) ) ) = ( ( A - -u 1 ) x. prod_ k e. ( 1 ... ( N - 1 ) ) ( A - ( k - 1 ) ) )
9 nnm1nn0 
 |-  ( N e. NN -> ( N - 1 ) e. NN0 )
10 9 adantl 
 |-  ( ( A e. CC /\ N e. NN ) -> ( N - 1 ) e. NN0 )
11 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
12 10 11 eleqtrdi 
 |-  ( ( A e. CC /\ N e. NN ) -> ( N - 1 ) e. ( ZZ>= ` 0 ) )
13 simpll 
 |-  ( ( ( A e. CC /\ N e. NN ) /\ k e. ( 0 ... ( N - 1 ) ) ) -> A e. CC )
14 elfzelz 
 |-  ( k e. ( 0 ... ( N - 1 ) ) -> k e. ZZ )
15 14 adantl 
 |-  ( ( ( A e. CC /\ N e. NN ) /\ k e. ( 0 ... ( N - 1 ) ) ) -> k e. ZZ )
16 peano2zm 
 |-  ( k e. ZZ -> ( k - 1 ) e. ZZ )
17 15 16 syl 
 |-  ( ( ( A e. CC /\ N e. NN ) /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( k - 1 ) e. ZZ )
18 17 zcnd 
 |-  ( ( ( A e. CC /\ N e. NN ) /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( k - 1 ) e. CC )
19 13 18 subcld 
 |-  ( ( ( A e. CC /\ N e. NN ) /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( A - ( k - 1 ) ) e. CC )
20 oveq1 
 |-  ( k = 0 -> ( k - 1 ) = ( 0 - 1 ) )
21 df-neg 
 |-  -u 1 = ( 0 - 1 )
22 20 21 eqtr4di 
 |-  ( k = 0 -> ( k - 1 ) = -u 1 )
23 22 oveq2d 
 |-  ( k = 0 -> ( A - ( k - 1 ) ) = ( A - -u 1 ) )
24 12 19 23 fprod1p 
 |-  ( ( A e. CC /\ N e. NN ) -> prod_ k e. ( 0 ... ( N - 1 ) ) ( A - ( k - 1 ) ) = ( ( A - -u 1 ) x. prod_ k e. ( ( 0 + 1 ) ... ( N - 1 ) ) ( A - ( k - 1 ) ) ) )
25 fallfacval2 
 |-  ( ( A e. CC /\ ( N - 1 ) e. NN0 ) -> ( A FallFac ( N - 1 ) ) = prod_ k e. ( 1 ... ( N - 1 ) ) ( A - ( k - 1 ) ) )
26 9 25 sylan2 
 |-  ( ( A e. CC /\ N e. NN ) -> ( A FallFac ( N - 1 ) ) = prod_ k e. ( 1 ... ( N - 1 ) ) ( A - ( k - 1 ) ) )
27 26 oveq2d 
 |-  ( ( A e. CC /\ N e. NN ) -> ( ( A - -u 1 ) x. ( A FallFac ( N - 1 ) ) ) = ( ( A - -u 1 ) x. prod_ k e. ( 1 ... ( N - 1 ) ) ( A - ( k - 1 ) ) ) )
28 8 24 27 3eqtr4a 
 |-  ( ( A e. CC /\ N e. NN ) -> prod_ k e. ( 0 ... ( N - 1 ) ) ( A - ( k - 1 ) ) = ( ( A - -u 1 ) x. ( A FallFac ( N - 1 ) ) ) )
29 elfznn0 
 |-  ( k e. ( 0 ... ( N - 1 ) ) -> k e. NN0 )
30 29 adantl 
 |-  ( ( ( A e. CC /\ N e. NN ) /\ k e. ( 0 ... ( N - 1 ) ) ) -> k e. NN0 )
31 30 nn0cnd 
 |-  ( ( ( A e. CC /\ N e. NN ) /\ k e. ( 0 ... ( N - 1 ) ) ) -> k e. CC )
32 1cnd 
 |-  ( ( ( A e. CC /\ N e. NN ) /\ k e. ( 0 ... ( N - 1 ) ) ) -> 1 e. CC )
33 13 31 32 subsub3d 
 |-  ( ( ( A e. CC /\ N e. NN ) /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( A - ( k - 1 ) ) = ( ( A + 1 ) - k ) )
34 33 prodeq2dv 
 |-  ( ( A e. CC /\ N e. NN ) -> prod_ k e. ( 0 ... ( N - 1 ) ) ( A - ( k - 1 ) ) = prod_ k e. ( 0 ... ( N - 1 ) ) ( ( A + 1 ) - k ) )
35 simpl 
 |-  ( ( A e. CC /\ N e. NN ) -> A e. CC )
36 1cnd 
 |-  ( ( A e. CC /\ N e. NN ) -> 1 e. CC )
37 35 36 subnegd 
 |-  ( ( A e. CC /\ N e. NN ) -> ( A - -u 1 ) = ( A + 1 ) )
38 37 oveq1d 
 |-  ( ( A e. CC /\ N e. NN ) -> ( ( A - -u 1 ) x. ( A FallFac ( N - 1 ) ) ) = ( ( A + 1 ) x. ( A FallFac ( N - 1 ) ) ) )
39 28 34 38 3eqtr3d 
 |-  ( ( A e. CC /\ N e. NN ) -> prod_ k e. ( 0 ... ( N - 1 ) ) ( ( A + 1 ) - k ) = ( ( A + 1 ) x. ( A FallFac ( N - 1 ) ) ) )
40 4 39 eqtrd 
 |-  ( ( A e. CC /\ N e. NN ) -> ( ( A + 1 ) FallFac N ) = ( ( A + 1 ) x. ( A FallFac ( N - 1 ) ) ) )
41 simpr 
 |-  ( ( A e. CC /\ N e. NN ) -> N e. NN )
42 41 nncnd 
 |-  ( ( A e. CC /\ N e. NN ) -> N e. CC )
43 42 36 npcand 
 |-  ( ( A e. CC /\ N e. NN ) -> ( ( N - 1 ) + 1 ) = N )
44 43 oveq2d 
 |-  ( ( A e. CC /\ N e. NN ) -> ( A FallFac ( ( N - 1 ) + 1 ) ) = ( A FallFac N ) )
45 fallfacp1 
 |-  ( ( A e. CC /\ ( N - 1 ) e. NN0 ) -> ( A FallFac ( ( N - 1 ) + 1 ) ) = ( ( A FallFac ( N - 1 ) ) x. ( A - ( N - 1 ) ) ) )
46 9 45 sylan2 
 |-  ( ( A e. CC /\ N e. NN ) -> ( A FallFac ( ( N - 1 ) + 1 ) ) = ( ( A FallFac ( N - 1 ) ) x. ( A - ( N - 1 ) ) ) )
47 44 46 eqtr3d 
 |-  ( ( A e. CC /\ N e. NN ) -> ( A FallFac N ) = ( ( A FallFac ( N - 1 ) ) x. ( A - ( N - 1 ) ) ) )
48 40 47 oveq12d 
 |-  ( ( A e. CC /\ N e. NN ) -> ( ( ( A + 1 ) FallFac N ) - ( A FallFac N ) ) = ( ( ( A + 1 ) x. ( A FallFac ( N - 1 ) ) ) - ( ( A FallFac ( N - 1 ) ) x. ( A - ( N - 1 ) ) ) ) )
49 fallfaccl 
 |-  ( ( A e. CC /\ ( N - 1 ) e. NN0 ) -> ( A FallFac ( N - 1 ) ) e. CC )
50 9 49 sylan2 
 |-  ( ( A e. CC /\ N e. NN ) -> ( A FallFac ( N - 1 ) ) e. CC )
51 10 nn0cnd 
 |-  ( ( A e. CC /\ N e. NN ) -> ( N - 1 ) e. CC )
52 35 51 subcld 
 |-  ( ( A e. CC /\ N e. NN ) -> ( A - ( N - 1 ) ) e. CC )
53 50 52 mulcomd 
 |-  ( ( A e. CC /\ N e. NN ) -> ( ( A FallFac ( N - 1 ) ) x. ( A - ( N - 1 ) ) ) = ( ( A - ( N - 1 ) ) x. ( A FallFac ( N - 1 ) ) ) )
54 53 oveq2d 
 |-  ( ( A e. CC /\ N e. NN ) -> ( ( ( A + 1 ) x. ( A FallFac ( N - 1 ) ) ) - ( ( A FallFac ( N - 1 ) ) x. ( A - ( N - 1 ) ) ) ) = ( ( ( A + 1 ) x. ( A FallFac ( N - 1 ) ) ) - ( ( A - ( N - 1 ) ) x. ( A FallFac ( N - 1 ) ) ) ) )
55 1 adantr 
 |-  ( ( A e. CC /\ N e. NN ) -> ( A + 1 ) e. CC )
56 55 52 50 subdird 
 |-  ( ( A e. CC /\ N e. NN ) -> ( ( ( A + 1 ) - ( A - ( N - 1 ) ) ) x. ( A FallFac ( N - 1 ) ) ) = ( ( ( A + 1 ) x. ( A FallFac ( N - 1 ) ) ) - ( ( A - ( N - 1 ) ) x. ( A FallFac ( N - 1 ) ) ) ) )
57 35 36 51 pnncand 
 |-  ( ( A e. CC /\ N e. NN ) -> ( ( A + 1 ) - ( A - ( N - 1 ) ) ) = ( 1 + ( N - 1 ) ) )
58 36 42 pncan3d 
 |-  ( ( A e. CC /\ N e. NN ) -> ( 1 + ( N - 1 ) ) = N )
59 57 58 eqtrd 
 |-  ( ( A e. CC /\ N e. NN ) -> ( ( A + 1 ) - ( A - ( N - 1 ) ) ) = N )
60 59 oveq1d 
 |-  ( ( A e. CC /\ N e. NN ) -> ( ( ( A + 1 ) - ( A - ( N - 1 ) ) ) x. ( A FallFac ( N - 1 ) ) ) = ( N x. ( A FallFac ( N - 1 ) ) ) )
61 54 56 60 3eqtr2d 
 |-  ( ( A e. CC /\ N e. NN ) -> ( ( ( A + 1 ) x. ( A FallFac ( N - 1 ) ) ) - ( ( A FallFac ( N - 1 ) ) x. ( A - ( N - 1 ) ) ) ) = ( N x. ( A FallFac ( N - 1 ) ) ) )
62 48 61 eqtrd 
 |-  ( ( A e. CC /\ N e. NN ) -> ( ( ( A + 1 ) FallFac N ) - ( A FallFac N ) ) = ( N x. ( A FallFac ( N - 1 ) ) ) )