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

Proof

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

Metamath Proof Explorer

Theorem binomrisefac

Proof