Metamath Proof Explorer

Theorem binomrisefac

Description: A version of the binomial theorem using rising factorials instead of exponentials. (Contributed by Scott Fenton, 16-Mar-2018)

Ref Expression
Assertion binomrisefac 
|- ( ( A e. CC /\ B e. CC /\ N e. NN0 ) -> ( ( A + B ) RiseFac N ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A RiseFac ( N - k ) ) x. ( B RiseFac k ) ) ) )

Proof

Step Hyp Ref Expression
1 negdi 
 |-  ( ( A e. CC /\ B e. CC ) -> -u ( A + B ) = ( -u A + -u B ) )
2 1 3adant3 
 |-  ( ( A e. CC /\ B e. CC /\ N e. NN0 ) -> -u ( A + B ) = ( -u A + -u B ) )
3 2 oveq1d 
 |-  ( ( A e. CC /\ B e. CC /\ N e. NN0 ) -> ( -u ( A + B ) FallFac N ) = ( ( -u A + -u B ) FallFac N ) )
4 negcl 
 |-  ( A e. CC -> -u A e. CC )
5 negcl 
 |-  ( B e. CC -> -u B e. CC )
6 id 
 |-  ( N e. NN0 -> N e. NN0 )
7 binomfallfac 
 |-  ( ( -u A e. CC /\ -u B e. CC /\ N e. NN0 ) -> ( ( -u A + -u B ) FallFac N ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( -u A FallFac ( N - k ) ) x. ( -u B FallFac k ) ) ) )
8 4 5 6 7 syl3an 
 |-  ( ( A e. CC /\ B e. CC /\ N e. NN0 ) -> ( ( -u A + -u B ) FallFac N ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( -u A FallFac ( N - k ) ) x. ( -u B FallFac k ) ) ) )
9 3 8 eqtrd 
 |-  ( ( A e. CC /\ B e. CC /\ N e. NN0 ) -> ( -u ( A + B ) FallFac N ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( -u A FallFac ( N - k ) ) x. ( -u B FallFac k ) ) ) )
10 9 oveq2d 
 |-  ( ( A e. CC /\ B e. CC /\ N e. NN0 ) -> ( ( -u 1 ^ N ) x. ( -u ( A + B ) FallFac N ) ) = ( ( -u 1 ^ N ) x. sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( -u A FallFac ( N - k ) ) x. ( -u B FallFac k ) ) ) ) )
11 fzfid 
 |-  ( ( A e. CC /\ B e. CC /\ N e. NN0 ) -> ( 0 ... N ) e. Fin )
12 neg1cn 
 |-  -u 1 e. CC
13 expcl 
 |-  ( ( -u 1 e. CC /\ N e. NN0 ) -> ( -u 1 ^ N ) e. CC )
14 12 13 mpan 
 |-  ( N e. NN0 -> ( -u 1 ^ N ) e. CC )
15 14 3ad2ant3 
 |-  ( ( A e. CC /\ B e. CC /\ N e. NN0 ) -> ( -u 1 ^ N ) e. CC )
16 simp3 
 |-  ( ( A e. CC /\ B e. CC /\ N e. NN0 ) -> N e. NN0 )
17 elfzelz 
 |-  ( k e. ( 0 ... N ) -> k e. ZZ )
18 bccl 
 |-  ( ( N e. NN0 /\ k e. ZZ ) -> ( N _C k ) e. NN0 )
19 16 17 18 syl2an 
 |-  ( ( ( A e. CC /\ B e. CC /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> ( N _C k ) e. NN0 )
20 19 nn0cnd 
 |-  ( ( ( A e. CC /\ B e. CC /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> ( N _C k ) e. CC )
21 simpl1 
 |-  ( ( ( A e. CC /\ B e. CC /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> A e. CC )
22 21 negcld 
 |-  ( ( ( A e. CC /\ B e. CC /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> -u A e. CC )
23 16 nn0zd 
 |-  ( ( A e. CC /\ B e. CC /\ N e. NN0 ) -> N e. ZZ )
24 zsubcl 
 |-  ( ( N e. ZZ /\ k e. ZZ ) -> ( N - k ) e. ZZ )
25 23 17 24 syl2an 
 |-  ( ( ( A e. CC /\ B e. CC /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> ( N - k ) e. ZZ )
26 elfzle2 
 |-  ( k e. ( 0 ... N ) -> k <_ N )
27 26 adantl 
 |-  ( ( ( A e. CC /\ B e. CC /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> k <_ N )
28 simpl3 
 |-  ( ( ( A e. CC /\ B e. CC /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> N e. NN0 )
29 28 nn0red 
 |-  ( ( ( A e. CC /\ B e. CC /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> N e. RR )
30 elfznn0 
 |-  ( k e. ( 0 ... N ) -> k e. NN0 )
31 30 adantl 
 |-  ( ( ( A e. CC /\ B e. CC /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> k e. NN0 )
32 31 nn0red 
 |-  ( ( ( A e. CC /\ B e. CC /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> k e. RR )
33 29 32 subge0d 
 |-  ( ( ( A e. CC /\ B e. CC /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> ( 0 <_ ( N - k ) <-> k <_ N ) )
34 27 33 mpbird 
 |-  ( ( ( A e. CC /\ B e. CC /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> 0 <_ ( N - k ) )
35 elnn0z 
 |-  ( ( N - k ) e. NN0 <-> ( ( N - k ) e. ZZ /\ 0 <_ ( N - k ) ) )
36 25 34 35 sylanbrc 
 |-  ( ( ( A e. CC /\ B e. CC /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> ( N - k ) e. NN0 )
37 fallfaccl 
 |-  ( ( -u A e. CC /\ ( N - k ) e. NN0 ) -> ( -u A FallFac ( N - k ) ) e. CC )
38 22 36 37 syl2anc 
 |-  ( ( ( A e. CC /\ B e. CC /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> ( -u A FallFac ( N - k ) ) e. CC )
39 simp2 
 |-  ( ( A e. CC /\ B e. CC /\ N e. NN0 ) -> B e. CC )
40 39 negcld 
 |-  ( ( A e. CC /\ B e. CC /\ N e. NN0 ) -> -u B e. CC )
41 fallfaccl 
 |-  ( ( -u B e. CC /\ k e. NN0 ) -> ( -u B FallFac k ) e. CC )
42 40 30 41 syl2an 
 |-  ( ( ( A e. CC /\ B e. CC /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> ( -u B FallFac k ) e. CC )
43 38 42 mulcld 
 |-  ( ( ( A e. CC /\ B e. CC /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> ( ( -u A FallFac ( N - k ) ) x. ( -u B FallFac k ) ) e. CC )
44 20 43 mulcld 
 |-  ( ( ( A e. CC /\ B e. CC /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> ( ( N _C k ) x. ( ( -u A FallFac ( N - k ) ) x. ( -u B FallFac k ) ) ) e. CC )
45 11 15 44 fsummulc2 
 |-  ( ( A e. CC /\ B e. CC /\ N e. NN0 ) -> ( ( -u 1 ^ N ) x. sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( -u A FallFac ( N - k ) ) x. ( -u B FallFac k ) ) ) ) = sum_ k e. ( 0 ... N ) ( ( -u 1 ^ N ) x. ( ( N _C k ) x. ( ( -u A FallFac ( N - k ) ) x. ( -u B FallFac k ) ) ) ) )
46 10 45 eqtrd 
 |-  ( ( A e. CC /\ B e. CC /\ N e. NN0 ) -> ( ( -u 1 ^ N ) x. ( -u ( A + B ) FallFac N ) ) = sum_ k e. ( 0 ... N ) ( ( -u 1 ^ N ) x. ( ( N _C k ) x. ( ( -u A FallFac ( N - k ) ) x. ( -u B FallFac k ) ) ) ) )
47 addcl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
48 risefallfac 
 |-  ( ( ( A + B ) e. CC /\ N e. NN0 ) -> ( ( A + B ) RiseFac N ) = ( ( -u 1 ^ N ) x. ( -u ( A + B ) FallFac N ) ) )
49 47 48 stoic3 
 |-  ( ( A e. CC /\ B e. CC /\ N e. NN0 ) -> ( ( A + B ) RiseFac N ) = ( ( -u 1 ^ N ) x. ( -u ( A + B ) FallFac N ) ) )
50 risefallfac 
 |-  ( ( A e. CC /\ ( N - k ) e. NN0 ) -> ( A RiseFac ( N - k ) ) = ( ( -u 1 ^ ( N - k ) ) x. ( -u A FallFac ( N - k ) ) ) )
51 21 36 50 syl2anc 
 |-  ( ( ( A e. CC /\ B e. CC /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> ( A RiseFac ( N - k ) ) = ( ( -u 1 ^ ( N - k ) ) x. ( -u A FallFac ( N - k ) ) ) )
52 simpl2 
 |-  ( ( ( A e. CC /\ B e. CC /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> B e. CC )
53 risefallfac 
 |-  ( ( B e. CC /\ k e. NN0 ) -> ( B RiseFac k ) = ( ( -u 1 ^ k ) x. ( -u B FallFac k ) ) )
54 52 31 53 syl2anc 
 |-  ( ( ( A e. CC /\ B e. CC /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> ( B RiseFac k ) = ( ( -u 1 ^ k ) x. ( -u B FallFac k ) ) )
55 51 54 oveq12d 
 |-  ( ( ( A e. CC /\ B e. CC /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> ( ( A RiseFac ( N - k ) ) x. ( B RiseFac k ) ) = ( ( ( -u 1 ^ ( N - k ) ) x. ( -u A FallFac ( N - k ) ) ) x. ( ( -u 1 ^ k ) x. ( -u B FallFac k ) ) ) )
56 expcl 
 |-  ( ( -u 1 e. CC /\ ( N - k ) e. NN0 ) -> ( -u 1 ^ ( N - k ) ) e. CC )
57 12 36 56 sylancr 
 |-  ( ( ( A e. CC /\ B e. CC /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> ( -u 1 ^ ( N - k ) ) e. CC )
58 expcl 
 |-  ( ( -u 1 e. CC /\ k e. NN0 ) -> ( -u 1 ^ k ) e. CC )
59 12 30 58 sylancr 
 |-  ( k e. ( 0 ... N ) -> ( -u 1 ^ k ) e. CC )
60 59 adantl 
 |-  ( ( ( A e. CC /\ B e. CC /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> ( -u 1 ^ k ) e. CC )
61 57 38 60 42 mul4d 
 |-  ( ( ( A e. CC /\ B e. CC /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> ( ( ( -u 1 ^ ( N - k ) ) x. ( -u A FallFac ( N - k ) ) ) x. ( ( -u 1 ^ k ) x. ( -u B FallFac k ) ) ) = ( ( ( -u 1 ^ ( N - k ) ) x. ( -u 1 ^ k ) ) x. ( ( -u A FallFac ( N - k ) ) x. ( -u B FallFac k ) ) ) )
62 12 a1i 
 |-  ( ( ( A e. CC /\ B e. CC /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> -u 1 e. CC )
63 62 31 36 expaddd 
 |-  ( ( ( A e. CC /\ B e. CC /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> ( -u 1 ^ ( ( N - k ) + k ) ) = ( ( -u 1 ^ ( N - k ) ) x. ( -u 1 ^ k ) ) )
64 16 nn0cnd 
 |-  ( ( A e. CC /\ B e. CC /\ N e. NN0 ) -> N e. CC )
65 30 nn0cnd 
 |-  ( k e. ( 0 ... N ) -> k e. CC )
66 npcan 
 |-  ( ( N e. CC /\ k e. CC ) -> ( ( N - k ) + k ) = N )
67 64 65 66 syl2an 
 |-  ( ( ( A e. CC /\ B e. CC /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> ( ( N - k ) + k ) = N )
68 67 oveq2d 
 |-  ( ( ( A e. CC /\ B e. CC /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> ( -u 1 ^ ( ( N - k ) + k ) ) = ( -u 1 ^ N ) )
69 63 68 eqtr3d 
 |-  ( ( ( A e. CC /\ B e. CC /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> ( ( -u 1 ^ ( N - k ) ) x. ( -u 1 ^ k ) ) = ( -u 1 ^ N ) )
70 69 oveq1d 
 |-  ( ( ( A e. CC /\ B e. CC /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> ( ( ( -u 1 ^ ( N - k ) ) x. ( -u 1 ^ k ) ) x. ( ( -u A FallFac ( N - k ) ) x. ( -u B FallFac k ) ) ) = ( ( -u 1 ^ N ) x. ( ( -u A FallFac ( N - k ) ) x. ( -u B FallFac k ) ) ) )
71 55 61 70 3eqtrd 
 |-  ( ( ( A e. CC /\ B e. CC /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> ( ( A RiseFac ( N - k ) ) x. ( B RiseFac k ) ) = ( ( -u 1 ^ N ) x. ( ( -u A FallFac ( N - k ) ) x. ( -u B FallFac k ) ) ) )
72 71 oveq2d 
 |-  ( ( ( A e. CC /\ B e. CC /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> ( ( N _C k ) x. ( ( A RiseFac ( N - k ) ) x. ( B RiseFac k ) ) ) = ( ( N _C k ) x. ( ( -u 1 ^ N ) x. ( ( -u A FallFac ( N - k ) ) x. ( -u B FallFac k ) ) ) ) )
73 15 adantr 
 |-  ( ( ( A e. CC /\ B e. CC /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> ( -u 1 ^ N ) e. CC )
74 20 73 43 mul12d 
 |-  ( ( ( A e. CC /\ B e. CC /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> ( ( N _C k ) x. ( ( -u 1 ^ N ) x. ( ( -u A FallFac ( N - k ) ) x. ( -u B FallFac k ) ) ) ) = ( ( -u 1 ^ N ) x. ( ( N _C k ) x. ( ( -u A FallFac ( N - k ) ) x. ( -u B FallFac k ) ) ) ) )
75 72 74 eqtrd 
 |-  ( ( ( A e. CC /\ B e. CC /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> ( ( N _C k ) x. ( ( A RiseFac ( N - k ) ) x. ( B RiseFac k ) ) ) = ( ( -u 1 ^ N ) x. ( ( N _C k ) x. ( ( -u A FallFac ( N - k ) ) x. ( -u B FallFac k ) ) ) ) )
76 75 sumeq2dv 
 |-  ( ( A e. CC /\ B e. CC /\ N e. NN0 ) -> sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A RiseFac ( N - k ) ) x. ( B RiseFac k ) ) ) = sum_ k e. ( 0 ... N ) ( ( -u 1 ^ N ) x. ( ( N _C k ) x. ( ( -u A FallFac ( N - k ) ) x. ( -u B FallFac k ) ) ) ) )
77 46 49 76 3eqtr4d 
 |-  ( ( A e. CC /\ B e. CC /\ N e. NN0 ) -> ( ( A + B ) RiseFac N ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A RiseFac ( N - k ) ) x. ( B RiseFac k ) ) ) )