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 \in ℂ \land B \in ℂ \land N \in ℕ_{0}) \to {(A + B)}^{\underline{N}} = \sum_{k = 0}^{N} (\binom{N}{k}) (A^{\underline{(N - k)}}) (B^{\underline{k}})$

Proof

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

Metamath Proof Explorer

Theorem binomfallfac

Proof