Metamath Proof Explorer

Theorem binomfallfac

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

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

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( m = 0 -> ( ( A + B ) FallFac m ) = ( ( A + B ) FallFac 0 ) )
2 oveq2 
 |-  ( m = 0 -> ( 0 ... m ) = ( 0 ... 0 ) )
3 fz0sn 
 |-  ( 0 ... 0 ) = { 0 }
4 2 3 eqtrdi 
 |-  ( m = 0 -> ( 0 ... m ) = { 0 } )
5 oveq1 
 |-  ( m = 0 -> ( m _C k ) = ( 0 _C k ) )
6 oveq1 
 |-  ( m = 0 -> ( m - k ) = ( 0 - k ) )
7 6 oveq2d 
 |-  ( m = 0 -> ( A FallFac ( m - k ) ) = ( A FallFac ( 0 - k ) ) )
8 7 oveq1d 
 |-  ( m = 0 -> ( ( A FallFac ( m - k ) ) x. ( B FallFac k ) ) = ( ( A FallFac ( 0 - k ) ) x. ( B FallFac k ) ) )
9 5 8 oveq12d 
 |-  ( m = 0 -> ( ( m _C k ) x. ( ( A FallFac ( m - k ) ) x. ( B FallFac k ) ) ) = ( ( 0 _C k ) x. ( ( A FallFac ( 0 - k ) ) x. ( B FallFac k ) ) ) )
10 9 adantr 
 |-  ( ( m = 0 /\ k e. ( 0 ... m ) ) -> ( ( m _C k ) x. ( ( A FallFac ( m - k ) ) x. ( B FallFac k ) ) ) = ( ( 0 _C k ) x. ( ( A FallFac ( 0 - k ) ) x. ( B FallFac k ) ) ) )
11 4 10 sumeq12dv 
 |-  ( m = 0 -> sum_ k e. ( 0 ... m ) ( ( m _C k ) x. ( ( A FallFac ( m - k ) ) x. ( B FallFac k ) ) ) = sum_ k e. { 0 } ( ( 0 _C k ) x. ( ( A FallFac ( 0 - k ) ) x. ( B FallFac k ) ) ) )
12 1 11 eqeq12d 
 |-  ( m = 0 -> ( ( ( A + B ) FallFac m ) = sum_ k e. ( 0 ... m ) ( ( m _C k ) x. ( ( A FallFac ( m - k ) ) x. ( B FallFac k ) ) ) <-> ( ( A + B ) FallFac 0 ) = sum_ k e. { 0 } ( ( 0 _C k ) x. ( ( A FallFac ( 0 - k ) ) x. ( B FallFac k ) ) ) ) )
13 12 imbi2d 
 |-  ( m = 0 -> ( ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) FallFac m ) = sum_ k e. ( 0 ... m ) ( ( m _C k ) x. ( ( A FallFac ( m - k ) ) x. ( B FallFac k ) ) ) ) <-> ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) FallFac 0 ) = sum_ k e. { 0 } ( ( 0 _C k ) x. ( ( A FallFac ( 0 - k ) ) x. ( B FallFac k ) ) ) ) ) )
14 oveq2 
 |-  ( m = n -> ( ( A + B ) FallFac m ) = ( ( A + B ) FallFac n ) )
15 oveq2 
 |-  ( m = n -> ( 0 ... m ) = ( 0 ... n ) )
16 oveq1 
 |-  ( m = n -> ( m _C k ) = ( n _C k ) )
17 oveq1 
 |-  ( m = n -> ( m - k ) = ( n - k ) )
18 17 oveq2d 
 |-  ( m = n -> ( A FallFac ( m - k ) ) = ( A FallFac ( n - k ) ) )
19 18 oveq1d 
 |-  ( m = n -> ( ( A FallFac ( m - k ) ) x. ( B FallFac k ) ) = ( ( A FallFac ( n - k ) ) x. ( B FallFac k ) ) )
20 16 19 oveq12d 
 |-  ( m = n -> ( ( m _C k ) x. ( ( A FallFac ( m - k ) ) x. ( B FallFac k ) ) ) = ( ( n _C k ) x. ( ( A FallFac ( n - k ) ) x. ( B FallFac k ) ) ) )
21 20 adantr 
 |-  ( ( m = n /\ k e. ( 0 ... m ) ) -> ( ( m _C k ) x. ( ( A FallFac ( m - k ) ) x. ( B FallFac k ) ) ) = ( ( n _C k ) x. ( ( A FallFac ( n - k ) ) x. ( B FallFac k ) ) ) )
22 15 21 sumeq12dv 
 |-  ( m = n -> sum_ k e. ( 0 ... m ) ( ( m _C k ) x. ( ( A FallFac ( m - k ) ) x. ( B FallFac k ) ) ) = sum_ k e. ( 0 ... n ) ( ( n _C k ) x. ( ( A FallFac ( n - k ) ) x. ( B FallFac k ) ) ) )
23 14 22 eqeq12d 
 |-  ( m = n -> ( ( ( A + B ) FallFac m ) = sum_ k e. ( 0 ... m ) ( ( m _C k ) x. ( ( A FallFac ( m - k ) ) x. ( B FallFac k ) ) ) <-> ( ( A + B ) FallFac n ) = sum_ k e. ( 0 ... n ) ( ( n _C k ) x. ( ( A FallFac ( n - k ) ) x. ( B FallFac k ) ) ) ) )
24 23 imbi2d 
 |-  ( m = n -> ( ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) FallFac m ) = sum_ k e. ( 0 ... m ) ( ( m _C k ) x. ( ( A FallFac ( m - k ) ) x. ( B FallFac k ) ) ) ) <-> ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) FallFac n ) = sum_ k e. ( 0 ... n ) ( ( n _C k ) x. ( ( A FallFac ( n - k ) ) x. ( B FallFac k ) ) ) ) ) )
25 oveq2 
 |-  ( m = ( n + 1 ) -> ( ( A + B ) FallFac m ) = ( ( A + B ) FallFac ( n + 1 ) ) )
26 oveq2 
 |-  ( m = ( n + 1 ) -> ( 0 ... m ) = ( 0 ... ( n + 1 ) ) )
27 oveq1 
 |-  ( m = ( n + 1 ) -> ( m _C k ) = ( ( n + 1 ) _C k ) )
28 oveq1 
 |-  ( m = ( n + 1 ) -> ( m - k ) = ( ( n + 1 ) - k ) )
29 28 oveq2d 
 |-  ( m = ( n + 1 ) -> ( A FallFac ( m - k ) ) = ( A FallFac ( ( n + 1 ) - k ) ) )
30 29 oveq1d 
 |-  ( m = ( n + 1 ) -> ( ( A FallFac ( m - k ) ) x. ( B FallFac k ) ) = ( ( A FallFac ( ( n + 1 ) - k ) ) x. ( B FallFac k ) ) )
31 27 30 oveq12d 
 |-  ( m = ( n + 1 ) -> ( ( m _C k ) x. ( ( A FallFac ( m - k ) ) x. ( B FallFac k ) ) ) = ( ( ( n + 1 ) _C k ) x. ( ( A FallFac ( ( n + 1 ) - k ) ) x. ( B FallFac k ) ) ) )
32 31 adantr 
 |-  ( ( m = ( n + 1 ) /\ k e. ( 0 ... m ) ) -> ( ( m _C k ) x. ( ( A FallFac ( m - k ) ) x. ( B FallFac k ) ) ) = ( ( ( n + 1 ) _C k ) x. ( ( A FallFac ( ( n + 1 ) - k ) ) x. ( B FallFac k ) ) ) )
33 26 32 sumeq12dv 
 |-  ( m = ( n + 1 ) -> sum_ k e. ( 0 ... m ) ( ( m _C k ) x. ( ( A FallFac ( m - k ) ) x. ( B FallFac k ) ) ) = sum_ k e. ( 0 ... ( n + 1 ) ) ( ( ( n + 1 ) _C k ) x. ( ( A FallFac ( ( n + 1 ) - k ) ) x. ( B FallFac k ) ) ) )
34 25 33 eqeq12d 
 |-  ( m = ( n + 1 ) -> ( ( ( A + B ) FallFac m ) = sum_ k e. ( 0 ... m ) ( ( m _C k ) x. ( ( A FallFac ( m - k ) ) x. ( B FallFac k ) ) ) <-> ( ( A + B ) FallFac ( n + 1 ) ) = sum_ k e. ( 0 ... ( n + 1 ) ) ( ( ( n + 1 ) _C k ) x. ( ( A FallFac ( ( n + 1 ) - k ) ) x. ( B FallFac k ) ) ) ) )
35 34 imbi2d 
 |-  ( m = ( n + 1 ) -> ( ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) FallFac m ) = sum_ k e. ( 0 ... m ) ( ( m _C k ) x. ( ( A FallFac ( m - k ) ) x. ( B FallFac k ) ) ) ) <-> ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) FallFac ( n + 1 ) ) = sum_ k e. ( 0 ... ( n + 1 ) ) ( ( ( n + 1 ) _C k ) x. ( ( A FallFac ( ( n + 1 ) - k ) ) x. ( B FallFac k ) ) ) ) ) )
36 oveq2 
 |-  ( m = N -> ( ( A + B ) FallFac m ) = ( ( A + B ) FallFac N ) )
37 oveq2 
 |-  ( m = N -> ( 0 ... m ) = ( 0 ... N ) )
38 oveq1 
 |-  ( m = N -> ( m _C k ) = ( N _C k ) )
39 oveq1 
 |-  ( m = N -> ( m - k ) = ( N - k ) )
40 39 oveq2d 
 |-  ( m = N -> ( A FallFac ( m - k ) ) = ( A FallFac ( N - k ) ) )
41 40 oveq1d 
 |-  ( m = N -> ( ( A FallFac ( m - k ) ) x. ( B FallFac k ) ) = ( ( A FallFac ( N - k ) ) x. ( B FallFac k ) ) )
42 38 41 oveq12d 
 |-  ( m = N -> ( ( m _C k ) x. ( ( A FallFac ( m - k ) ) x. ( B FallFac k ) ) ) = ( ( N _C k ) x. ( ( A FallFac ( N - k ) ) x. ( B FallFac k ) ) ) )
43 42 adantr 
 |-  ( ( m = N /\ k e. ( 0 ... m ) ) -> ( ( m _C k ) x. ( ( A FallFac ( m - k ) ) x. ( B FallFac k ) ) ) = ( ( N _C k ) x. ( ( A FallFac ( N - k ) ) x. ( B FallFac k ) ) ) )
44 37 43 sumeq12dv 
 |-  ( m = N -> sum_ k e. ( 0 ... m ) ( ( m _C k ) x. ( ( A FallFac ( m - k ) ) x. ( B FallFac k ) ) ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A FallFac ( N - k ) ) x. ( B FallFac k ) ) ) )
45 36 44 eqeq12d 
 |-  ( m = N -> ( ( ( A + B ) FallFac m ) = sum_ k e. ( 0 ... m ) ( ( m _C k ) x. ( ( A FallFac ( m - k ) ) x. ( B FallFac k ) ) ) <-> ( ( A + B ) FallFac N ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A FallFac ( N - k ) ) x. ( B FallFac k ) ) ) ) )
46 45 imbi2d 
 |-  ( m = N -> ( ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) FallFac m ) = sum_ k e. ( 0 ... m ) ( ( m _C k ) x. ( ( A FallFac ( m - k ) ) x. ( B FallFac k ) ) ) ) <-> ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) FallFac N ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A FallFac ( N - k ) ) x. ( B FallFac k ) ) ) ) ) )
47 fallfac0 
 |-  ( A e. CC -> ( A FallFac 0 ) = 1 )
48 fallfac0 
 |-  ( B e. CC -> ( B FallFac 0 ) = 1 )
49 47 48 oveqan12d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A FallFac 0 ) x. ( B FallFac 0 ) ) = ( 1 x. 1 ) )
50 1t1e1 
 |-  ( 1 x. 1 ) = 1
51 49 50 eqtrdi 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A FallFac 0 ) x. ( B FallFac 0 ) ) = 1 )
52 51 oveq2d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( 1 x. ( ( A FallFac 0 ) x. ( B FallFac 0 ) ) ) = ( 1 x. 1 ) )
53 52 50 eqtrdi 
 |-  ( ( A e. CC /\ B e. CC ) -> ( 1 x. ( ( A FallFac 0 ) x. ( B FallFac 0 ) ) ) = 1 )
54 0cn 
 |-  0 e. CC
55 ax-1cn 
 |-  1 e. CC
56 53 55 eqeltrdi 
 |-  ( ( A e. CC /\ B e. CC ) -> ( 1 x. ( ( A FallFac 0 ) x. ( B FallFac 0 ) ) ) e. CC )
57 oveq2 
 |-  ( k = 0 -> ( 0 _C k ) = ( 0 _C 0 ) )
58 0nn0 
 |-  0 e. NN0
59 bcnn 
 |-  ( 0 e. NN0 -> ( 0 _C 0 ) = 1 )
60 58 59 ax-mp 
 |-  ( 0 _C 0 ) = 1
61 57 60 eqtrdi 
 |-  ( k = 0 -> ( 0 _C k ) = 1 )
62 oveq2 
 |-  ( k = 0 -> ( 0 - k ) = ( 0 - 0 ) )
63 0m0e0 
 |-  ( 0 - 0 ) = 0
64 62 63 eqtrdi 
 |-  ( k = 0 -> ( 0 - k ) = 0 )
65 64 oveq2d 
 |-  ( k = 0 -> ( A FallFac ( 0 - k ) ) = ( A FallFac 0 ) )
66 oveq2 
 |-  ( k = 0 -> ( B FallFac k ) = ( B FallFac 0 ) )
67 65 66 oveq12d 
 |-  ( k = 0 -> ( ( A FallFac ( 0 - k ) ) x. ( B FallFac k ) ) = ( ( A FallFac 0 ) x. ( B FallFac 0 ) ) )
68 61 67 oveq12d 
 |-  ( k = 0 -> ( ( 0 _C k ) x. ( ( A FallFac ( 0 - k ) ) x. ( B FallFac k ) ) ) = ( 1 x. ( ( A FallFac 0 ) x. ( B FallFac 0 ) ) ) )
69 68 sumsn 
 |-  ( ( 0 e. CC /\ ( 1 x. ( ( A FallFac 0 ) x. ( B FallFac 0 ) ) ) e. CC ) -> sum_ k e. { 0 } ( ( 0 _C k ) x. ( ( A FallFac ( 0 - k ) ) x. ( B FallFac k ) ) ) = ( 1 x. ( ( A FallFac 0 ) x. ( B FallFac 0 ) ) ) )
70 54 56 69 sylancr 
 |-  ( ( A e. CC /\ B e. CC ) -> sum_ k e. { 0 } ( ( 0 _C k ) x. ( ( A FallFac ( 0 - k ) ) x. ( B FallFac k ) ) ) = ( 1 x. ( ( A FallFac 0 ) x. ( B FallFac 0 ) ) ) )
71 addcl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
72 fallfac0 
 |-  ( ( A + B ) e. CC -> ( ( A + B ) FallFac 0 ) = 1 )
73 71 72 syl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) FallFac 0 ) = 1 )
74 53 70 73 3eqtr4rd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) FallFac 0 ) = sum_ k e. { 0 } ( ( 0 _C k ) x. ( ( A FallFac ( 0 - k ) ) x. ( B FallFac k ) ) ) )
75 simprl 
 |-  ( ( n e. NN0 /\ ( A e. CC /\ B e. CC ) ) -> A e. CC )
76 simprr 
 |-  ( ( n e. NN0 /\ ( A e. CC /\ B e. CC ) ) -> B e. CC )
77 simpl 
 |-  ( ( n e. NN0 /\ ( A e. CC /\ B e. CC ) ) -> n e. NN0 )
78 id 
 |-  ( ( ( A + B ) FallFac n ) = sum_ k e. ( 0 ... n ) ( ( n _C k ) x. ( ( A FallFac ( n - k ) ) x. ( B FallFac k ) ) ) -> ( ( A + B ) FallFac n ) = sum_ k e. ( 0 ... n ) ( ( n _C k ) x. ( ( A FallFac ( n - k ) ) x. ( B FallFac k ) ) ) )
79 75 76 77 78 binomfallfaclem2 
 |-  ( ( ( n e. NN0 /\ ( A e. CC /\ B e. CC ) ) /\ ( ( A + B ) FallFac n ) = sum_ k e. ( 0 ... n ) ( ( n _C k ) x. ( ( A FallFac ( n - k ) ) x. ( B FallFac k ) ) ) ) -> ( ( A + B ) FallFac ( n + 1 ) ) = sum_ k e. ( 0 ... ( n + 1 ) ) ( ( ( n + 1 ) _C k ) x. ( ( A FallFac ( ( n + 1 ) - k ) ) x. ( B FallFac k ) ) ) )
80 79 exp31 
 |-  ( n e. NN0 -> ( ( A e. CC /\ B e. CC ) -> ( ( ( A + B ) FallFac n ) = sum_ k e. ( 0 ... n ) ( ( n _C k ) x. ( ( A FallFac ( n - k ) ) x. ( B FallFac k ) ) ) -> ( ( A + B ) FallFac ( n + 1 ) ) = sum_ k e. ( 0 ... ( n + 1 ) ) ( ( ( n + 1 ) _C k ) x. ( ( A FallFac ( ( n + 1 ) - k ) ) x. ( B FallFac k ) ) ) ) ) )
81 80 a2d 
 |-  ( n e. NN0 -> ( ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) FallFac n ) = sum_ k e. ( 0 ... n ) ( ( n _C k ) x. ( ( A FallFac ( n - k ) ) x. ( B FallFac k ) ) ) ) -> ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) FallFac ( n + 1 ) ) = sum_ k e. ( 0 ... ( n + 1 ) ) ( ( ( n + 1 ) _C k ) x. ( ( A FallFac ( ( n + 1 ) - k ) ) x. ( B FallFac k ) ) ) ) ) )
82 13 24 35 46 74 81 nn0ind 
 |-  ( N e. NN0 -> ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) FallFac N ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A FallFac ( N - k ) ) x. ( B FallFac k ) ) ) ) )
83 82 com12 
 |-  ( ( A e. CC /\ B e. CC ) -> ( N e. NN0 -> ( ( A + B ) FallFac N ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A FallFac ( N - k ) ) x. ( B FallFac k ) ) ) ) )
84 83 3impia 
 |-  ( ( A e. CC /\ B e. CC /\ N e. NN0 ) -> ( ( A + B ) FallFac N ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A FallFac ( N - k ) ) x. ( B FallFac k ) ) ) )