binomfallfaclem2

Description: Lemma for binomfallfac . Inductive step. (Contributed by Scott Fenton, 13-Mar-2018)

	Ref	Expression
Hypotheses	binomfallfaclem.1	$⊢ φ \to A \in ℂ$
	binomfallfaclem.2	$⊢ φ \to B \in ℂ$
	binomfallfaclem.3	$⊢ φ \to N \in ℕ_{0}$
	binomfallfaclem.4	$⊢ ψ \to {(A + B)}^{\underline{N}} = \sum_{k = 0}^{N} (\binom{N}{k}) (A^{\underline{(N - k)}}) (B^{\underline{k}})$
Assertion	binomfallfaclem2	$⊢ (φ \land ψ) \to {(A + B)}^{\underline{(N + 1)}} = \sum_{k = 0}^{N + 1} (\binom{N + 1}{k}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}})$

Proof

Step	Hyp	Ref	Expression
1		binomfallfaclem.1	$⊢ φ \to A \in ℂ$
2		binomfallfaclem.2	$⊢ φ \to B \in ℂ$
3		binomfallfaclem.3	$⊢ φ \to N \in ℕ_{0}$
4		binomfallfaclem.4	$⊢ ψ \to {(A + B)}^{\underline{N}} = \sum_{k = 0}^{N} (\binom{N}{k}) (A^{\underline{(N - k)}}) (B^{\underline{k}})$
5		elfzelz	$⊢ k \in (0 \dots N) \to k \in ℤ$
6		bccl	$⊢ (N \in ℕ_{0} \land k \in ℤ) \to (\binom{N}{k}) \in ℕ_{0}$
7	3 5 6	syl2an	$⊢ (φ \land k \in (0 \dots N)) \to (\binom{N}{k}) \in ℕ_{0}$
8	7	nn0cnd	$⊢ (φ \land k \in (0 \dots N)) \to (\binom{N}{k}) \in ℂ$
9		fznn0sub	$⊢ k \in (0 \dots N) \to N - k \in ℕ_{0}$
10		fallfaccl	$⊢ (A \in ℂ \land N - k \in ℕ_{0}) \to A^{\underline{(N - k)}} \in ℂ$
11	1 9 10	syl2an	$⊢ (φ \land k \in (0 \dots N)) \to A^{\underline{(N - k)}} \in ℂ$
12		elfznn0	$⊢ k \in (0 \dots N) \to k \in ℕ_{0}$
13		fallfaccl	$⊢ (B \in ℂ \land k \in ℕ_{0}) \to B^{\underline{k}} \in ℂ$
14	2 12 13	syl2an	$⊢ (φ \land k \in (0 \dots N)) \to B^{\underline{k}} \in ℂ$
15	11 14	mulcld	$⊢ (φ \land k \in (0 \dots N)) \to (A^{\underline{(N - k)}}) (B^{\underline{k}}) \in ℂ$
16	1 2	addcld	$⊢ φ \to A + B \in ℂ$
17	3	nn0cnd	$⊢ φ \to N \in ℂ$
18	16 17	subcld	$⊢ φ \to A + B - N \in ℂ$
19	18	adantr	$⊢ (φ \land k \in (0 \dots N)) \to A + B - N \in ℂ$
20	8 15 19	mulassd	$⊢ (φ \land k \in (0 \dots N)) \to (\binom{N}{k}) (A^{\underline{(N - k)}}) (B^{\underline{k}}) (A + B - N) = (\binom{N}{k}) (A^{\underline{(N - k)}}) (B^{\underline{k}}) (A + B - N)$
21	9	nn0cnd	$⊢ k \in (0 \dots N) \to N - k \in ℂ$
22		subcl	$⊢ (A \in ℂ \land N - k \in ℂ) \to A - (N - k) \in ℂ$
23	1 21 22	syl2an	$⊢ (φ \land k \in (0 \dots N)) \to A - (N - k) \in ℂ$
24	12	nn0cnd	$⊢ k \in (0 \dots N) \to k \in ℂ$
25		subcl	$⊢ (B \in ℂ \land k \in ℂ) \to B - k \in ℂ$
26	2 24 25	syl2an	$⊢ (φ \land k \in (0 \dots N)) \to B - k \in ℂ$
27	15 23 26	adddid	$⊢ (φ \land k \in (0 \dots N)) \to (A^{\underline{(N - k)}}) (B^{\underline{k}}) ((A - (N - k)) + B - k) = (A^{\underline{(N - k)}}) (B^{\underline{k}}) (A - (N - k)) + (A^{\underline{(N - k)}}) (B^{\underline{k}}) (B - k)$
28	1	adantr	$⊢ (φ \land k \in (0 \dots N)) \to A \in ℂ$
29	17	adantr	$⊢ (φ \land k \in (0 \dots N)) \to N \in ℂ$
30	28 29	subcld	$⊢ (φ \land k \in (0 \dots N)) \to A - N \in ℂ$
31	24	adantl	$⊢ (φ \land k \in (0 \dots N)) \to k \in ℂ$
32	2	adantr	$⊢ (φ \land k \in (0 \dots N)) \to B \in ℂ$
33	30 31 32	ppncand	$⊢ (φ \land k \in (0 \dots N)) \to (A - N) + k + (B - k) = A - N + B$
34	28 29 31	subsubd	$⊢ (φ \land k \in (0 \dots N)) \to A - (N - k) = A - N + k$
35	34	oveq1d	$⊢ (φ \land k \in (0 \dots N)) \to (A - (N - k)) + B - k = (A - N) + k + (B - k)$
36	28 32 29	addsubd	$⊢ (φ \land k \in (0 \dots N)) \to A + B - N = A - N + B$
37	33 35 36	3eqtr4d	$⊢ (φ \land k \in (0 \dots N)) \to (A - (N - k)) + B - k = A + B - N$
38	37	oveq2d	$⊢ (φ \land k \in (0 \dots N)) \to (A^{\underline{(N - k)}}) (B^{\underline{k}}) ((A - (N - k)) + B - k) = (A^{\underline{(N - k)}}) (B^{\underline{k}}) (A + B - N)$
39	11 14 23	mul32d	$⊢ (φ \land k \in (0 \dots N)) \to (A^{\underline{(N - k)}}) (B^{\underline{k}}) (A - (N - k)) = (A^{\underline{(N - k)}}) (A - (N - k)) (B^{\underline{k}})$
40		1cnd	$⊢ (φ \land k \in (0 \dots N)) \to 1 \in ℂ$
41	29 40 31	addsubd	$⊢ (φ \land k \in (0 \dots N)) \to N + 1 - k = N - k + 1$
42	41	oveq2d	$⊢ (φ \land k \in (0 \dots N)) \to A^{\underline{(N + 1 - k)}} = A^{\underline{(N - k + 1)}}$
43		fallfacp1	$⊢ (A \in ℂ \land N - k \in ℕ_{0}) \to A^{\underline{(N - k + 1)}} = (A^{\underline{(N - k)}}) (A - (N - k))$
44	1 9 43	syl2an	$⊢ (φ \land k \in (0 \dots N)) \to A^{\underline{(N - k + 1)}} = (A^{\underline{(N - k)}}) (A - (N - k))$
45	42 44	eqtrd	$⊢ (φ \land k \in (0 \dots N)) \to A^{\underline{(N + 1 - k)}} = (A^{\underline{(N - k)}}) (A - (N - k))$
46	45	oveq1d	$⊢ (φ \land k \in (0 \dots N)) \to (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}}) = (A^{\underline{(N - k)}}) (A - (N - k)) (B^{\underline{k}})$
47	39 46	eqtr4d	$⊢ (φ \land k \in (0 \dots N)) \to (A^{\underline{(N - k)}}) (B^{\underline{k}}) (A - (N - k)) = (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}})$
48	11 14 26	mulassd	$⊢ (φ \land k \in (0 \dots N)) \to (A^{\underline{(N - k)}}) (B^{\underline{k}}) (B - k) = (A^{\underline{(N - k)}}) (B^{\underline{k}}) (B - k)$
49		fallfacp1	$⊢ (B \in ℂ \land k \in ℕ_{0}) \to B^{\underline{(k + 1)}} = (B^{\underline{k}}) (B - k)$
50	2 12 49	syl2an	$⊢ (φ \land k \in (0 \dots N)) \to B^{\underline{(k + 1)}} = (B^{\underline{k}}) (B - k)$
51	50	oveq2d	$⊢ (φ \land k \in (0 \dots N)) \to (A^{\underline{(N - k)}}) (B^{\underline{(k + 1)}}) = (A^{\underline{(N - k)}}) (B^{\underline{k}}) (B - k)$
52	48 51	eqtr4d	$⊢ (φ \land k \in (0 \dots N)) \to (A^{\underline{(N - k)}}) (B^{\underline{k}}) (B - k) = (A^{\underline{(N - k)}}) (B^{\underline{(k + 1)}})$
53	47 52	oveq12d	$⊢ (φ \land k \in (0 \dots N)) \to (A^{\underline{(N - k)}}) (B^{\underline{k}}) (A - (N - k)) + (A^{\underline{(N - k)}}) (B^{\underline{k}}) (B - k) = (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}}) + (A^{\underline{(N - k)}}) (B^{\underline{(k + 1)}})$
54	27 38 53	3eqtr3d	$⊢ (φ \land k \in (0 \dots N)) \to (A^{\underline{(N - k)}}) (B^{\underline{k}}) (A + B - N) = (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}}) + (A^{\underline{(N - k)}}) (B^{\underline{(k + 1)}})$
55	54	oveq2d	$⊢ (φ \land k \in (0 \dots N)) \to (\binom{N}{k}) (A^{\underline{(N - k)}}) (B^{\underline{k}}) (A + B - N) = (\binom{N}{k}) ((A^{\underline{(N + 1 - k)}}) (B^{\underline{k}}) + (A^{\underline{(N - k)}}) (B^{\underline{(k + 1)}}))$
56	3	nn0zd	$⊢ φ \to N \in ℤ$
57		uzid	$⊢ N \in ℤ \to N \in ℤ_{\geq N}$
58		peano2uz	$⊢ N \in ℤ_{\geq N} \to N + 1 \in ℤ_{\geq N}$
59		fzss2	$⊢ N + 1 \in ℤ_{\geq N} \to (0 \dots N) \subseteq (0 \dots N + 1)$
60	56 57 58 59	4syl	$⊢ φ \to (0 \dots N) \subseteq (0 \dots N + 1)$
61	60	sselda	$⊢ (φ \land k \in (0 \dots N)) \to k \in (0 \dots N + 1)$
62		fznn0sub	$⊢ k \in (0 \dots N + 1) \to N + 1 - k \in ℕ_{0}$
63		fallfaccl	$⊢ (A \in ℂ \land N + 1 - k \in ℕ_{0}) \to A^{\underline{(N + 1 - k)}} \in ℂ$
64	1 62 63	syl2an	$⊢ (φ \land k \in (0 \dots N + 1)) \to A^{\underline{(N + 1 - k)}} \in ℂ$
65	61 64	syldan	$⊢ (φ \land k \in (0 \dots N)) \to A^{\underline{(N + 1 - k)}} \in ℂ$
66	65 14	mulcld	$⊢ (φ \land k \in (0 \dots N)) \to (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}}) \in ℂ$
67		peano2nn0	$⊢ k \in ℕ_{0} \to k + 1 \in ℕ_{0}$
68	12 67	syl	$⊢ k \in (0 \dots N) \to k + 1 \in ℕ_{0}$
69		fallfaccl	$⊢ (B \in ℂ \land k + 1 \in ℕ_{0}) \to B^{\underline{(k + 1)}} \in ℂ$
70	2 68 69	syl2an	$⊢ (φ \land k \in (0 \dots N)) \to B^{\underline{(k + 1)}} \in ℂ$
71	11 70	mulcld	$⊢ (φ \land k \in (0 \dots N)) \to (A^{\underline{(N - k)}}) (B^{\underline{(k + 1)}}) \in ℂ$
72	8 66 71	adddid	$⊢ (φ \land k \in (0 \dots N)) \to (\binom{N}{k}) ((A^{\underline{(N + 1 - k)}}) (B^{\underline{k}}) + (A^{\underline{(N - k)}}) (B^{\underline{(k + 1)}})) = (\binom{N}{k}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}}) + (\binom{N}{k}) (A^{\underline{(N - k)}}) (B^{\underline{(k + 1)}})$
73	20 55 72	3eqtrd	$⊢ (φ \land k \in (0 \dots N)) \to (\binom{N}{k}) (A^{\underline{(N - k)}}) (B^{\underline{k}}) (A + B - N) = (\binom{N}{k}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}}) + (\binom{N}{k}) (A^{\underline{(N - k)}}) (B^{\underline{(k + 1)}})$
74	73	sumeq2dv	$⊢ φ \to \sum_{k = 0}^{N} (\binom{N}{k}) (A^{\underline{(N - k)}}) (B^{\underline{k}}) (A + B - N) = \sum_{k = 0}^{N} ((\binom{N}{k}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}}) + (\binom{N}{k}) (A^{\underline{(N - k)}}) (B^{\underline{(k + 1)}}))$
75	74	adantr	$⊢ (φ \land ψ) \to \sum_{k = 0}^{N} (\binom{N}{k}) (A^{\underline{(N - k)}}) (B^{\underline{k}}) (A + B - N) = \sum_{k = 0}^{N} ((\binom{N}{k}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}}) + (\binom{N}{k}) (A^{\underline{(N - k)}}) (B^{\underline{(k + 1)}}))$
76	16 3	fallfacp1d	$⊢ φ \to {(A + B)}^{\underline{(N + 1)}} = ({(A + B)}^{\underline{N}}) (A + B - N)$
77	4	oveq1d	$⊢ ψ \to ({(A + B)}^{\underline{N}}) (A + B - N) = \sum_{k = 0}^{N} (\binom{N}{k}) (A^{\underline{(N - k)}}) (B^{\underline{k}}) (A + B - N)$
78	76 77	sylan9eq	$⊢ (φ \land ψ) \to {(A + B)}^{\underline{(N + 1)}} = \sum_{k = 0}^{N} (\binom{N}{k}) (A^{\underline{(N - k)}}) (B^{\underline{k}}) (A + B - N)$
79		fzfid	$⊢ φ \to (0 \dots N) \in Fin$
80	8 15	mulcld	$⊢ (φ \land k \in (0 \dots N)) \to (\binom{N}{k}) (A^{\underline{(N - k)}}) (B^{\underline{k}}) \in ℂ$
81	79 18 80	fsummulc1	$⊢ φ \to \sum_{k = 0}^{N} (\binom{N}{k}) (A^{\underline{(N - k)}}) (B^{\underline{k}}) (A + B - N) = \sum_{k = 0}^{N} (\binom{N}{k}) (A^{\underline{(N - k)}}) (B^{\underline{k}}) (A + B - N)$
82	81	adantr	$⊢ (φ \land ψ) \to \sum_{k = 0}^{N} (\binom{N}{k}) (A^{\underline{(N - k)}}) (B^{\underline{k}}) (A + B - N) = \sum_{k = 0}^{N} (\binom{N}{k}) (A^{\underline{(N - k)}}) (B^{\underline{k}}) (A + B - N)$
83	78 82	eqtrd	$⊢ (φ \land ψ) \to {(A + B)}^{\underline{(N + 1)}} = \sum_{k = 0}^{N} (\binom{N}{k}) (A^{\underline{(N - k)}}) (B^{\underline{k}}) (A + B - N)$
84		elfzelz	$⊢ k \in (0 \dots N + 1) \to k \in ℤ$
85		bcpasc	$⊢ (N \in ℕ_{0} \land k \in ℤ) \to (\binom{N}{k}) + (\binom{N}{k - 1}) = (\binom{N + 1}{k})$
86	3 84 85	syl2an	$⊢ (φ \land k \in (0 \dots N + 1)) \to (\binom{N}{k}) + (\binom{N}{k - 1}) = (\binom{N + 1}{k})$
87	86	oveq1d	$⊢ (φ \land k \in (0 \dots N + 1)) \to ((\binom{N}{k}) + (\binom{N}{k - 1})) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}}) = (\binom{N + 1}{k}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}})$
88	3 84 6	syl2an	$⊢ (φ \land k \in (0 \dots N + 1)) \to (\binom{N}{k}) \in ℕ_{0}$
89	88	nn0cnd	$⊢ (φ \land k \in (0 \dots N + 1)) \to (\binom{N}{k}) \in ℂ$
90		peano2zm	$⊢ k \in ℤ \to k - 1 \in ℤ$
91	84 90	syl	$⊢ k \in (0 \dots N + 1) \to k - 1 \in ℤ$
92		bccl	$⊢ (N \in ℕ_{0} \land k - 1 \in ℤ) \to (\binom{N}{k - 1}) \in ℕ_{0}$
93	3 91 92	syl2an	$⊢ (φ \land k \in (0 \dots N + 1)) \to (\binom{N}{k - 1}) \in ℕ_{0}$
94	93	nn0cnd	$⊢ (φ \land k \in (0 \dots N + 1)) \to (\binom{N}{k - 1}) \in ℂ$
95		elfznn0	$⊢ k \in (0 \dots N + 1) \to k \in ℕ_{0}$
96	2 95 13	syl2an	$⊢ (φ \land k \in (0 \dots N + 1)) \to B^{\underline{k}} \in ℂ$
97	64 96	mulcld	$⊢ (φ \land k \in (0 \dots N + 1)) \to (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}}) \in ℂ$
98	89 94 97	adddird	$⊢ (φ \land k \in (0 \dots N + 1)) \to ((\binom{N}{k}) + (\binom{N}{k - 1})) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}}) = (\binom{N}{k}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}}) + (\binom{N}{k - 1}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}})$
99	87 98	eqtr3d	$⊢ (φ \land k \in (0 \dots N + 1)) \to (\binom{N + 1}{k}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}}) = (\binom{N}{k}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}}) + (\binom{N}{k - 1}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}})$
100	99	sumeq2dv	$⊢ φ \to \sum_{k = 0}^{N + 1} (\binom{N + 1}{k}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}}) = \sum_{k = 0}^{N + 1} ((\binom{N}{k}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}}) + (\binom{N}{k - 1}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}}))$
101		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
102	3 101	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq 0}$
103	89 97	mulcld	$⊢ (φ \land k \in (0 \dots N + 1)) \to (\binom{N}{k}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}}) \in ℂ$
104		oveq2	$⊢ k = N + 1 \to (\binom{N}{k}) = (\binom{N}{N + 1})$
105		oveq2	$⊢ k = N + 1 \to N + 1 - k = N + 1 - (N + 1)$
106	105	oveq2d	$⊢ k = N + 1 \to A^{\underline{(N + 1 - k)}} = A^{\underline{(N + 1 - (N + 1))}}$
107		oveq2	$⊢ k = N + 1 \to B^{\underline{k}} = B^{\underline{(N + 1)}}$
108	106 107	oveq12d	$⊢ k = N + 1 \to (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}}) = (A^{\underline{(N + 1 - (N + 1))}}) (B^{\underline{(N + 1)}})$
109	104 108	oveq12d	$⊢ k = N + 1 \to (\binom{N}{k}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}}) = (\binom{N}{N + 1}) (A^{\underline{(N + 1 - (N + 1))}}) (B^{\underline{(N + 1)}})$
110	102 103 109	fsump1	$⊢ φ \to \sum_{k = 0}^{N + 1} (\binom{N}{k}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}}) = \sum_{k = 0}^{N} (\binom{N}{k}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}}) + (\binom{N}{N + 1}) (A^{\underline{(N + 1 - (N + 1))}}) (B^{\underline{(N + 1)}})$
111		peano2nn0	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ_{0}$
112	3 111	syl	$⊢ φ \to N + 1 \in ℕ_{0}$
113	112	nn0zd	$⊢ φ \to N + 1 \in ℤ$
114	3	nn0red	$⊢ φ \to N \in ℝ$
115	114	ltp1d	$⊢ φ \to N < N + 1$
116	115	olcd	$⊢ φ \to (N + 1 < 0 \lor N < N + 1)$
117		bcval4	$⊢ (N \in ℕ_{0} \land N + 1 \in ℤ \land (N + 1 < 0 \lor N < N + 1)) \to (\binom{N}{N + 1}) = 0$
118	3 113 116 117	syl3anc	$⊢ φ \to (\binom{N}{N + 1}) = 0$
119	118	oveq1d	$⊢ φ \to (\binom{N}{N + 1}) (A^{\underline{(N + 1 - (N + 1))}}) (B^{\underline{(N + 1)}}) = 0 \cdot (A^{\underline{(N + 1 - (N + 1))}}) (B^{\underline{(N + 1)}})$
120	112	nn0cnd	$⊢ φ \to N + 1 \in ℂ$
121	120	subidd	$⊢ φ \to N + 1 - (N + 1) = 0$
122	121	oveq2d	$⊢ φ \to A^{\underline{(N + 1 - (N + 1))}} = A^{\underline{0}}$
123		0nn0	$⊢ 0 \in ℕ_{0}$
124		fallfaccl	$⊢ (A \in ℂ \land 0 \in ℕ_{0}) \to A^{\underline{0}} \in ℂ$
125	1 123 124	sylancl	$⊢ φ \to A^{\underline{0}} \in ℂ$
126	122 125	eqeltrd	$⊢ φ \to A^{\underline{(N + 1 - (N + 1))}} \in ℂ$
127		fallfaccl	$⊢ (B \in ℂ \land N + 1 \in ℕ_{0}) \to B^{\underline{(N + 1)}} \in ℂ$
128	2 112 127	syl2anc	$⊢ φ \to B^{\underline{(N + 1)}} \in ℂ$
129	126 128	mulcld	$⊢ φ \to (A^{\underline{(N + 1 - (N + 1))}}) (B^{\underline{(N + 1)}}) \in ℂ$
130	129	mul02d	$⊢ φ \to 0 \cdot (A^{\underline{(N + 1 - (N + 1))}}) (B^{\underline{(N + 1)}}) = 0$
131	119 130	eqtrd	$⊢ φ \to (\binom{N}{N + 1}) (A^{\underline{(N + 1 - (N + 1))}}) (B^{\underline{(N + 1)}}) = 0$
132	131	oveq2d	$⊢ φ \to \sum_{k = 0}^{N} (\binom{N}{k}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}}) + (\binom{N}{N + 1}) (A^{\underline{(N + 1 - (N + 1))}}) (B^{\underline{(N + 1)}}) = \sum_{k = 0}^{N} (\binom{N}{k}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}}) + 0$
133	61 103	syldan	$⊢ (φ \land k \in (0 \dots N)) \to (\binom{N}{k}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}}) \in ℂ$
134	79 133	fsumcl	$⊢ φ \to \sum_{k = 0}^{N} (\binom{N}{k}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}}) \in ℂ$
135	134	addid1d	$⊢ φ \to \sum_{k = 0}^{N} (\binom{N}{k}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}}) + 0 = \sum_{k = 0}^{N} (\binom{N}{k}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}})$
136	110 132 135	3eqtrd	$⊢ φ \to \sum_{k = 0}^{N + 1} (\binom{N}{k}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}}) = \sum_{k = 0}^{N} (\binom{N}{k}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}})$
137	112 101	eleqtrdi	$⊢ φ \to N + 1 \in ℤ_{\geq 0}$
138	94 97	mulcld	$⊢ (φ \land k \in (0 \dots N + 1)) \to (\binom{N}{k - 1}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}}) \in ℂ$
139		oveq1	$⊢ k = 0 \to k - 1 = 0 - 1$
140		df-neg	$⊢ - 1 = 0 - 1$
141	139 140	eqtr4di	$⊢ k = 0 \to k - 1 = - 1$
142	141	oveq2d	$⊢ k = 0 \to (\binom{N}{k - 1}) = (\binom{N}{- 1})$
143		oveq2	$⊢ k = 0 \to N + 1 - k = N + 1 - 0$
144	143	oveq2d	$⊢ k = 0 \to A^{\underline{(N + 1 - k)}} = A^{\underline{(N + 1 - 0)}}$
145		oveq2	$⊢ k = 0 \to B^{\underline{k}} = B^{\underline{0}}$
146	144 145	oveq12d	$⊢ k = 0 \to (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}}) = (A^{\underline{(N + 1 - 0)}}) (B^{\underline{0}})$
147	142 146	oveq12d	$⊢ k = 0 \to (\binom{N}{k - 1}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}}) = (\binom{N}{- 1}) (A^{\underline{(N + 1 - 0)}}) (B^{\underline{0}})$
148	137 138 147	fsum1p	$⊢ φ \to \sum_{k = 0}^{N + 1} (\binom{N}{k - 1}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}}) = (\binom{N}{- 1}) (A^{\underline{(N + 1 - 0)}}) (B^{\underline{0}}) + \sum_{k = 0 + 1}^{N + 1} (\binom{N}{k - 1}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}})$
149		neg1z	$⊢ - 1 \in ℤ$
150		neg1lt0	$⊢ - 1 < 0$
151	150	orci	$⊢ (- 1 < 0 \lor N < - 1)$
152		bcval4	$⊢ (N \in ℕ_{0} \land - 1 \in ℤ \land (- 1 < 0 \lor N < - 1)) \to (\binom{N}{- 1}) = 0$
153	149 151 152	mp3an23	$⊢ N \in ℕ_{0} \to (\binom{N}{- 1}) = 0$
154	3 153	syl	$⊢ φ \to (\binom{N}{- 1}) = 0$
155	154	oveq1d	$⊢ φ \to (\binom{N}{- 1}) (A^{\underline{(N + 1 - 0)}}) (B^{\underline{0}}) = 0 \cdot (A^{\underline{(N + 1 - 0)}}) (B^{\underline{0}})$
156	120	subid1d	$⊢ φ \to N + 1 - 0 = N + 1$
157	156	oveq2d	$⊢ φ \to A^{\underline{(N + 1 - 0)}} = A^{\underline{(N + 1)}}$
158		fallfaccl	$⊢ (A \in ℂ \land N + 1 \in ℕ_{0}) \to A^{\underline{(N + 1)}} \in ℂ$
159	1 112 158	syl2anc	$⊢ φ \to A^{\underline{(N + 1)}} \in ℂ$
160	157 159	eqeltrd	$⊢ φ \to A^{\underline{(N + 1 - 0)}} \in ℂ$
161		fallfaccl	$⊢ (B \in ℂ \land 0 \in ℕ_{0}) \to B^{\underline{0}} \in ℂ$
162	2 123 161	sylancl	$⊢ φ \to B^{\underline{0}} \in ℂ$
163	160 162	mulcld	$⊢ φ \to (A^{\underline{(N + 1 - 0)}}) (B^{\underline{0}}) \in ℂ$
164	163	mul02d	$⊢ φ \to 0 \cdot (A^{\underline{(N + 1 - 0)}}) (B^{\underline{0}}) = 0$
165	155 164	eqtrd	$⊢ φ \to (\binom{N}{- 1}) (A^{\underline{(N + 1 - 0)}}) (B^{\underline{0}}) = 0$
166		1zzd	$⊢ φ \to 1 \in ℤ$
167		0zd	$⊢ φ \to 0 \in ℤ$
168	1 2 3	binomfallfaclem1	$⊢ (φ \land j \in (0 \dots N)) \to (\binom{N}{j}) (A^{\underline{(N - j)}}) (B^{\underline{(j + 1)}}) \in ℂ$
169		oveq2	$⊢ j = k - 1 \to (\binom{N}{j}) = (\binom{N}{k - 1})$
170		oveq2	$⊢ j = k - 1 \to N - j = N - (k - 1)$
171	170	oveq2d	$⊢ j = k - 1 \to A^{\underline{(N - j)}} = A^{\underline{(N - (k - 1))}}$
172		oveq1	$⊢ j = k - 1 \to j + 1 = k - 1 + 1$
173	172	oveq2d	$⊢ j = k - 1 \to B^{\underline{(j + 1)}} = B^{\underline{(k - 1 + 1)}}$
174	171 173	oveq12d	$⊢ j = k - 1 \to (A^{\underline{(N - j)}}) (B^{\underline{(j + 1)}}) = (A^{\underline{(N - (k - 1))}}) (B^{\underline{(k - 1 + 1)}})$
175	169 174	oveq12d	$⊢ j = k - 1 \to (\binom{N}{j}) (A^{\underline{(N - j)}}) (B^{\underline{(j + 1)}}) = (\binom{N}{k - 1}) (A^{\underline{(N - (k - 1))}}) (B^{\underline{(k - 1 + 1)}})$
176	166 167 56 168 175	fsumshft	$⊢ φ \to \sum_{j = 0}^{N} (\binom{N}{j}) (A^{\underline{(N - j)}}) (B^{\underline{(j + 1)}}) = \sum_{k = 0 + 1}^{N + 1} (\binom{N}{k - 1}) (A^{\underline{(N - (k - 1))}}) (B^{\underline{(k - 1 + 1)}})$
177	17	adantr	$⊢ (φ \land k \in (0 + 1 \dots N + 1)) \to N \in ℂ$
178		elfzelz	$⊢ k \in (0 + 1 \dots N + 1) \to k \in ℤ$
179	178	adantl	$⊢ (φ \land k \in (0 + 1 \dots N + 1)) \to k \in ℤ$
180	179	zcnd	$⊢ (φ \land k \in (0 + 1 \dots N + 1)) \to k \in ℂ$
181		1cnd	$⊢ (φ \land k \in (0 + 1 \dots N + 1)) \to 1 \in ℂ$
182	177 180 181	subsub3d	$⊢ (φ \land k \in (0 + 1 \dots N + 1)) \to N - (k - 1) = N + 1 - k$
183	182	oveq2d	$⊢ (φ \land k \in (0 + 1 \dots N + 1)) \to A^{\underline{(N - (k - 1))}} = A^{\underline{(N + 1 - k)}}$
184	180 181	npcand	$⊢ (φ \land k \in (0 + 1 \dots N + 1)) \to k - 1 + 1 = k$
185	184	oveq2d	$⊢ (φ \land k \in (0 + 1 \dots N + 1)) \to B^{\underline{(k - 1 + 1)}} = B^{\underline{k}}$
186	183 185	oveq12d	$⊢ (φ \land k \in (0 + 1 \dots N + 1)) \to (A^{\underline{(N - (k - 1))}}) (B^{\underline{(k - 1 + 1)}}) = (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}})$
187	186	oveq2d	$⊢ (φ \land k \in (0 + 1 \dots N + 1)) \to (\binom{N}{k - 1}) (A^{\underline{(N - (k - 1))}}) (B^{\underline{(k - 1 + 1)}}) = (\binom{N}{k - 1}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}})$
188	187	sumeq2dv	$⊢ φ \to \sum_{k = 0 + 1}^{N + 1} (\binom{N}{k - 1}) (A^{\underline{(N - (k - 1))}}) (B^{\underline{(k - 1 + 1)}}) = \sum_{k = 0 + 1}^{N + 1} (\binom{N}{k - 1}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}})$
189	176 188	eqtr2d	$⊢ φ \to \sum_{k = 0 + 1}^{N + 1} (\binom{N}{k - 1}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}}) = \sum_{j = 0}^{N} (\binom{N}{j}) (A^{\underline{(N - j)}}) (B^{\underline{(j + 1)}})$
190		oveq2	$⊢ k = j \to (\binom{N}{k}) = (\binom{N}{j})$
191		oveq2	$⊢ k = j \to N - k = N - j$
192	191	oveq2d	$⊢ k = j \to A^{\underline{(N - k)}} = A^{\underline{(N - j)}}$
193		oveq1	$⊢ k = j \to k + 1 = j + 1$
194	193	oveq2d	$⊢ k = j \to B^{\underline{(k + 1)}} = B^{\underline{(j + 1)}}$
195	192 194	oveq12d	$⊢ k = j \to (A^{\underline{(N - k)}}) (B^{\underline{(k + 1)}}) = (A^{\underline{(N - j)}}) (B^{\underline{(j + 1)}})$
196	190 195	oveq12d	$⊢ k = j \to (\binom{N}{k}) (A^{\underline{(N - k)}}) (B^{\underline{(k + 1)}}) = (\binom{N}{j}) (A^{\underline{(N - j)}}) (B^{\underline{(j + 1)}})$
197	196	cbvsumv	$⊢ \sum_{k = 0}^{N} (\binom{N}{k}) (A^{\underline{(N - k)}}) (B^{\underline{(k + 1)}}) = \sum_{j = 0}^{N} (\binom{N}{j}) (A^{\underline{(N - j)}}) (B^{\underline{(j + 1)}})$
198	189 197	eqtr4di	$⊢ φ \to \sum_{k = 0 + 1}^{N + 1} (\binom{N}{k - 1}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}}) = \sum_{k = 0}^{N} (\binom{N}{k}) (A^{\underline{(N - k)}}) (B^{\underline{(k + 1)}})$
199	165 198	oveq12d	$⊢ φ \to (\binom{N}{- 1}) (A^{\underline{(N + 1 - 0)}}) (B^{\underline{0}}) + \sum_{k = 0 + 1}^{N + 1} (\binom{N}{k - 1}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}}) = 0 + \sum_{k = 0}^{N} (\binom{N}{k}) (A^{\underline{(N - k)}}) (B^{\underline{(k + 1)}})$
200	1 2 3	binomfallfaclem1	$⊢ (φ \land k \in (0 \dots N)) \to (\binom{N}{k}) (A^{\underline{(N - k)}}) (B^{\underline{(k + 1)}}) \in ℂ$
201	79 200	fsumcl	$⊢ φ \to \sum_{k = 0}^{N} (\binom{N}{k}) (A^{\underline{(N - k)}}) (B^{\underline{(k + 1)}}) \in ℂ$
202	201	addid2d	$⊢ φ \to 0 + \sum_{k = 0}^{N} (\binom{N}{k}) (A^{\underline{(N - k)}}) (B^{\underline{(k + 1)}}) = \sum_{k = 0}^{N} (\binom{N}{k}) (A^{\underline{(N - k)}}) (B^{\underline{(k + 1)}})$
203	148 199 202	3eqtrd	$⊢ φ \to \sum_{k = 0}^{N + 1} (\binom{N}{k - 1}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}}) = \sum_{k = 0}^{N} (\binom{N}{k}) (A^{\underline{(N - k)}}) (B^{\underline{(k + 1)}})$
204	136 203	oveq12d	$⊢ φ \to \sum_{k = 0}^{N + 1} (\binom{N}{k}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}}) + \sum_{k = 0}^{N + 1} (\binom{N}{k - 1}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}}) = \sum_{k = 0}^{N} (\binom{N}{k}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}}) + \sum_{k = 0}^{N} (\binom{N}{k}) (A^{\underline{(N - k)}}) (B^{\underline{(k + 1)}})$
205		fzfid	$⊢ φ \to (0 \dots N + 1) \in Fin$
206	205 103 138	fsumadd	$⊢ φ \to \sum_{k = 0}^{N + 1} ((\binom{N}{k}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}}) + (\binom{N}{k - 1}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}})) = \sum_{k = 0}^{N + 1} (\binom{N}{k}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}}) + \sum_{k = 0}^{N + 1} (\binom{N}{k - 1}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}})$
207	79 133 200	fsumadd	$⊢ φ \to \sum_{k = 0}^{N} ((\binom{N}{k}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}}) + (\binom{N}{k}) (A^{\underline{(N - k)}}) (B^{\underline{(k + 1)}})) = \sum_{k = 0}^{N} (\binom{N}{k}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}}) + \sum_{k = 0}^{N} (\binom{N}{k}) (A^{\underline{(N - k)}}) (B^{\underline{(k + 1)}})$
208	204 206 207	3eqtr4d	$⊢ φ \to \sum_{k = 0}^{N + 1} ((\binom{N}{k}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}}) + (\binom{N}{k - 1}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}})) = \sum_{k = 0}^{N} ((\binom{N}{k}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}}) + (\binom{N}{k}) (A^{\underline{(N - k)}}) (B^{\underline{(k + 1)}}))$
209	100 208	eqtrd	$⊢ φ \to \sum_{k = 0}^{N + 1} (\binom{N + 1}{k}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}}) = \sum_{k = 0}^{N} ((\binom{N}{k}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}}) + (\binom{N}{k}) (A^{\underline{(N - k)}}) (B^{\underline{(k + 1)}}))$
210	209	adantr	$⊢ (φ \land ψ) \to \sum_{k = 0}^{N + 1} (\binom{N + 1}{k}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}}) = \sum_{k = 0}^{N} ((\binom{N}{k}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}}) + (\binom{N}{k}) (A^{\underline{(N - k)}}) (B^{\underline{(k + 1)}}))$
211	75 83 210	3eqtr4d	$⊢ (φ \land ψ) \to {(A + B)}^{\underline{(N + 1)}} = \sum_{k = 0}^{N + 1} (\binom{N + 1}{k}) (A^{\underline{(N + 1 - k)}}) (B^{\underline{k}})$

Metamath Proof Explorer

Theorem binomfallfaclem2

Proof