fallfacfwd

Description: The forward difference of a falling factorial. (Contributed by Scott Fenton, 21-Jan-2018)

		Ref	Expression
	Assertion	fallfacfwd	$⊢ (A \in ℂ \land N \in ℕ) \to ({(A + 1)}^{\underline{N}}) - (A^{\underline{N}}) = N (A^{\underline{(N - 1)}})$

Proof

Step	Hyp	Ref	Expression
1		peano2cn	$⊢ A \in ℂ \to A + 1 \in ℂ$
2		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
3		fallfacval	$⊢ (A + 1 \in ℂ \land N \in ℕ_{0}) \to {(A + 1)}^{\underline{N}} = \prod_{k = 0}^{N - 1} (A + 1 - k)$
4	1 2 3	syl2an	$⊢ (A \in ℂ \land N \in ℕ) \to {(A + 1)}^{\underline{N}} = \prod_{k = 0}^{N - 1} (A + 1 - k)$
5		0p1e1	$⊢ 0 + 1 = 1$
6	5	oveq1i	$⊢ (0 + 1 \dots N - 1) = (1 \dots N - 1)$
7	6	prodeq1i	$⊢ \prod_{k = 0 + 1}^{N - 1} (A - (k - 1)) = \prod_{k = 1}^{N - 1} (A - (k - 1))$
8	7	oveq2i	$⊢ (A - -1) \prod_{k = 0 + 1}^{N - 1} (A - (k - 1)) = (A - -1) \prod_{k = 1}^{N - 1} (A - (k - 1))$
9		nnm1nn0	$⊢ N \in ℕ \to N - 1 \in ℕ_{0}$
10	9	adantl	$⊢ (A \in ℂ \land N \in ℕ) \to N - 1 \in ℕ_{0}$
11		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
12	10 11	eleqtrdi	$⊢ (A \in ℂ \land N \in ℕ) \to N - 1 \in ℤ_{\geq 0}$
13		simpll	$⊢ ((A \in ℂ \land N \in ℕ) \land k \in (0 \dots N - 1)) \to A \in ℂ$
14		elfzelz	$⊢ k \in (0 \dots N - 1) \to k \in ℤ$
15	14	adantl	$⊢ ((A \in ℂ \land N \in ℕ) \land k \in (0 \dots N - 1)) \to k \in ℤ$
16		peano2zm	$⊢ k \in ℤ \to k - 1 \in ℤ$
17	15 16	syl	$⊢ ((A \in ℂ \land N \in ℕ) \land k \in (0 \dots N - 1)) \to k - 1 \in ℤ$
18	17	zcnd	$⊢ ((A \in ℂ \land N \in ℕ) \land k \in (0 \dots N - 1)) \to k - 1 \in ℂ$
19	13 18	subcld	$⊢ ((A \in ℂ \land N \in ℕ) \land k \in (0 \dots N - 1)) \to A - (k - 1) \in ℂ$
20		oveq1	$⊢ k = 0 \to k - 1 = 0 - 1$
21		df-neg	$⊢ - 1 = 0 - 1$
22	20 21	eqtr4di	$⊢ k = 0 \to k - 1 = - 1$
23	22	oveq2d	$⊢ k = 0 \to A - (k - 1) = A - -1$
24	12 19 23	fprod1p	$⊢ (A \in ℂ \land N \in ℕ) \to \prod_{k = 0}^{N - 1} (A - (k - 1)) = (A - -1) \prod_{k = 0 + 1}^{N - 1} (A - (k - 1))$
25		fallfacval2	$⊢ (A \in ℂ \land N - 1 \in ℕ_{0}) \to A^{\underline{(N - 1)}} = \prod_{k = 1}^{N - 1} (A - (k - 1))$
26	9 25	sylan2	$⊢ (A \in ℂ \land N \in ℕ) \to A^{\underline{(N - 1)}} = \prod_{k = 1}^{N - 1} (A - (k - 1))$
27	26	oveq2d	$⊢ (A \in ℂ \land N \in ℕ) \to (A - -1) (A^{\underline{(N - 1)}}) = (A - -1) \prod_{k = 1}^{N - 1} (A - (k - 1))$
28	8 24 27	3eqtr4a	$⊢ (A \in ℂ \land N \in ℕ) \to \prod_{k = 0}^{N - 1} (A - (k - 1)) = (A - -1) (A^{\underline{(N - 1)}})$
29		elfznn0	$⊢ k \in (0 \dots N - 1) \to k \in ℕ_{0}$
30	29	adantl	$⊢ ((A \in ℂ \land N \in ℕ) \land k \in (0 \dots N - 1)) \to k \in ℕ_{0}$
31	30	nn0cnd	$⊢ ((A \in ℂ \land N \in ℕ) \land k \in (0 \dots N - 1)) \to k \in ℂ$
32		1cnd	$⊢ ((A \in ℂ \land N \in ℕ) \land k \in (0 \dots N - 1)) \to 1 \in ℂ$
33	13 31 32	subsub3d	$⊢ ((A \in ℂ \land N \in ℕ) \land k \in (0 \dots N - 1)) \to A - (k - 1) = A + 1 - k$
34	33	prodeq2dv	$⊢ (A \in ℂ \land N \in ℕ) \to \prod_{k = 0}^{N - 1} (A - (k - 1)) = \prod_{k = 0}^{N - 1} (A + 1 - k)$
35		simpl	$⊢ (A \in ℂ \land N \in ℕ) \to A \in ℂ$
36		1cnd	$⊢ (A \in ℂ \land N \in ℕ) \to 1 \in ℂ$
37	35 36	subnegd	$⊢ (A \in ℂ \land N \in ℕ) \to A - -1 = A + 1$
38	37	oveq1d	$⊢ (A \in ℂ \land N \in ℕ) \to (A - -1) (A^{\underline{(N - 1)}}) = (A + 1) (A^{\underline{(N - 1)}})$
39	28 34 38	3eqtr3d	$⊢ (A \in ℂ \land N \in ℕ) \to \prod_{k = 0}^{N - 1} (A + 1 - k) = (A + 1) (A^{\underline{(N - 1)}})$
40	4 39	eqtrd	$⊢ (A \in ℂ \land N \in ℕ) \to {(A + 1)}^{\underline{N}} = (A + 1) (A^{\underline{(N - 1)}})$
41		simpr	$⊢ (A \in ℂ \land N \in ℕ) \to N \in ℕ$
42	41	nncnd	$⊢ (A \in ℂ \land N \in ℕ) \to N \in ℂ$
43	42 36	npcand	$⊢ (A \in ℂ \land N \in ℕ) \to N - 1 + 1 = N$
44	43	oveq2d	$⊢ (A \in ℂ \land N \in ℕ) \to A^{\underline{(N - 1 + 1)}} = A^{\underline{N}}$
45		fallfacp1	$⊢ (A \in ℂ \land N - 1 \in ℕ_{0}) \to A^{\underline{(N - 1 + 1)}} = (A^{\underline{(N - 1)}}) (A - (N - 1))$
46	9 45	sylan2	$⊢ (A \in ℂ \land N \in ℕ) \to A^{\underline{(N - 1 + 1)}} = (A^{\underline{(N - 1)}}) (A - (N - 1))$
47	44 46	eqtr3d	$⊢ (A \in ℂ \land N \in ℕ) \to A^{\underline{N}} = (A^{\underline{(N - 1)}}) (A - (N - 1))$
48	40 47	oveq12d	$⊢ (A \in ℂ \land N \in ℕ) \to ({(A + 1)}^{\underline{N}}) - (A^{\underline{N}}) = (A + 1) (A^{\underline{(N - 1)}}) - (A^{\underline{(N - 1)}}) (A - (N - 1))$
49		fallfaccl	$⊢ (A \in ℂ \land N - 1 \in ℕ_{0}) \to A^{\underline{(N - 1)}} \in ℂ$
50	9 49	sylan2	$⊢ (A \in ℂ \land N \in ℕ) \to A^{\underline{(N - 1)}} \in ℂ$
51	10	nn0cnd	$⊢ (A \in ℂ \land N \in ℕ) \to N - 1 \in ℂ$
52	35 51	subcld	$⊢ (A \in ℂ \land N \in ℕ) \to A - (N - 1) \in ℂ$
53	50 52	mulcomd	$⊢ (A \in ℂ \land N \in ℕ) \to (A^{\underline{(N - 1)}}) (A - (N - 1)) = (A - (N - 1)) (A^{\underline{(N - 1)}})$
54	53	oveq2d	$⊢ (A \in ℂ \land N \in ℕ) \to (A + 1) (A^{\underline{(N - 1)}}) - (A^{\underline{(N - 1)}}) (A - (N - 1)) = (A + 1) (A^{\underline{(N - 1)}}) - (A - (N - 1)) (A^{\underline{(N - 1)}})$
55	1	adantr	$⊢ (A \in ℂ \land N \in ℕ) \to A + 1 \in ℂ$
56	55 52 50	subdird	$⊢ (A \in ℂ \land N \in ℕ) \to (A + 1 - (A - (N - 1))) (A^{\underline{(N - 1)}}) = (A + 1) (A^{\underline{(N - 1)}}) - (A - (N - 1)) (A^{\underline{(N - 1)}})$
57	35 36 51	pnncand	$⊢ (A \in ℂ \land N \in ℕ) \to A + 1 - (A - (N - 1)) = 1 + N - 1$
58	36 42	pncan3d	$⊢ (A \in ℂ \land N \in ℕ) \to 1 + N - 1 = N$
59	57 58	eqtrd	$⊢ (A \in ℂ \land N \in ℕ) \to A + 1 - (A - (N - 1)) = N$
60	59	oveq1d	$⊢ (A \in ℂ \land N \in ℕ) \to (A + 1 - (A - (N - 1))) (A^{\underline{(N - 1)}}) = N (A^{\underline{(N - 1)}})$
61	54 56 60	3eqtr2d	$⊢ (A \in ℂ \land N \in ℕ) \to (A + 1) (A^{\underline{(N - 1)}}) - (A^{\underline{(N - 1)}}) (A - (N - 1)) = N (A^{\underline{(N - 1)}})$
62	48 61	eqtrd	$⊢ (A \in ℂ \land N \in ℕ) \to ({(A + 1)}^{\underline{N}}) - (A^{\underline{N}}) = N (A^{\underline{(N - 1)}})$

Metamath Proof Explorer

Theorem fallfacfwd

Proof