risefallfac

Description: A relationship between rising and falling factorials. (Contributed by Scott Fenton, 15-Jan-2018)

		Ref	Expression
	Assertion	risefallfac	$⊢ (X \in ℂ \land N \in ℕ_{0}) \to X^{\overline{N}} = {(- 1)}^{N} ({(- X)}^{\underline{N}})$

Proof

Step	Hyp	Ref	Expression
1		negcl	$⊢ X \in ℂ \to - X \in ℂ$
2	1	adantr	$⊢ (X \in ℂ \land N \in ℕ_{0}) \to - X \in ℂ$
3		elfznn	$⊢ k \in (1 \dots N) \to k \in ℕ$
4		nnm1nn0	$⊢ k \in ℕ \to k - 1 \in ℕ_{0}$
5	3 4	syl	$⊢ k \in (1 \dots N) \to k - 1 \in ℕ_{0}$
6	5	nn0cnd	$⊢ k \in (1 \dots N) \to k - 1 \in ℂ$
7		subcl	$⊢ (- X \in ℂ \land k - 1 \in ℂ) \to - X - (k - 1) \in ℂ$
8	2 6 7	syl2an	$⊢ ((X \in ℂ \land N \in ℕ_{0}) \land k \in (1 \dots N)) \to - X - (k - 1) \in ℂ$
9	8	mulm1d	$⊢ ((X \in ℂ \land N \in ℕ_{0}) \land k \in (1 \dots N)) \to -1 (- X - (k - 1)) = - (- X - (k - 1))$
10		simpll	$⊢ ((X \in ℂ \land N \in ℕ_{0}) \land k \in (1 \dots N)) \to X \in ℂ$
11	6	adantl	$⊢ ((X \in ℂ \land N \in ℕ_{0}) \land k \in (1 \dots N)) \to k - 1 \in ℂ$
12	10 11	negdi2d	$⊢ ((X \in ℂ \land N \in ℕ_{0}) \land k \in (1 \dots N)) \to - (X + k - 1) = - X - (k - 1)$
13	12	negeqd	$⊢ ((X \in ℂ \land N \in ℕ_{0}) \land k \in (1 \dots N)) \to - (- (X + k - 1)) = - (- X - (k - 1))$
14		simpl	$⊢ (X \in ℂ \land N \in ℕ_{0}) \to X \in ℂ$
15		addcl	$⊢ (X \in ℂ \land k - 1 \in ℂ) \to X + k - 1 \in ℂ$
16	14 6 15	syl2an	$⊢ ((X \in ℂ \land N \in ℕ_{0}) \land k \in (1 \dots N)) \to X + k - 1 \in ℂ$
17	16	negnegd	$⊢ ((X \in ℂ \land N \in ℕ_{0}) \land k \in (1 \dots N)) \to - (- (X + k - 1)) = X + k - 1$
18	9 13 17	3eqtr2rd	$⊢ ((X \in ℂ \land N \in ℕ_{0}) \land k \in (1 \dots N)) \to X + k - 1 = -1 (- X - (k - 1))$
19	18	prodeq2dv	$⊢ (X \in ℂ \land N \in ℕ_{0}) \to \prod_{k = 1}^{N} (X + k - 1) = \prod_{k = 1}^{N} -1 (- X - (k - 1))$
20		risefacval2	$⊢ (X \in ℂ \land N \in ℕ_{0}) \to X^{\overline{N}} = \prod_{k = 1}^{N} (X + k - 1)$
21		fzfi	$⊢ (1 \dots N) \in Fin$
22		neg1cn	$⊢ - 1 \in ℂ$
23		fprodconst	$⊢ ((1 \dots N) \in Fin \land - 1 \in ℂ) \to \prod_{k = 1}^{N} -1 = {(- 1)}^{\|(1 \dots N)\|}$
24	21 22 23	mp2an	$⊢ \prod_{k = 1}^{N} -1 = {(- 1)}^{\|(1 \dots N)\|}$
25		hashfz1	$⊢ N \in ℕ_{0} \to \|(1 \dots N)\| = N$
26	25	oveq2d	$⊢ N \in ℕ_{0} \to {(- 1)}^{\|(1 \dots N)\|} = {(- 1)}^{N}$
27	24 26	syl5req	$⊢ N \in ℕ_{0} \to {(- 1)}^{N} = \prod_{k = 1}^{N} -1$
28	27	adantl	$⊢ (X \in ℂ \land N \in ℕ_{0}) \to {(- 1)}^{N} = \prod_{k = 1}^{N} -1$
29		fallfacval2	$⊢ (- X \in ℂ \land N \in ℕ_{0}) \to {(- X)}^{\underline{N}} = \prod_{k = 1}^{N} (- X - (k - 1))$
30	1 29	sylan	$⊢ (X \in ℂ \land N \in ℕ_{0}) \to {(- X)}^{\underline{N}} = \prod_{k = 1}^{N} (- X - (k - 1))$
31	28 30	oveq12d	$⊢ (X \in ℂ \land N \in ℕ_{0}) \to {(- 1)}^{N} ({(- X)}^{\underline{N}}) = \prod_{k = 1}^{N} -1 \prod_{k = 1}^{N} (- X - (k - 1))$
32		fzfid	$⊢ (X \in ℂ \land N \in ℕ_{0}) \to (1 \dots N) \in Fin$
33	22	a1i	$⊢ ((X \in ℂ \land N \in ℕ_{0}) \land k \in (1 \dots N)) \to - 1 \in ℂ$
34	32 33 8	fprodmul	$⊢ (X \in ℂ \land N \in ℕ_{0}) \to \prod_{k = 1}^{N} -1 (- X - (k - 1)) = \prod_{k = 1}^{N} -1 \prod_{k = 1}^{N} (- X - (k - 1))$
35	31 34	eqtr4d	$⊢ (X \in ℂ \land N \in ℕ_{0}) \to {(- 1)}^{N} ({(- X)}^{\underline{N}}) = \prod_{k = 1}^{N} -1 (- X - (k - 1))$
36	19 20 35	3eqtr4d	$⊢ (X \in ℂ \land N \in ℕ_{0}) \to X^{\overline{N}} = {(- 1)}^{N} ({(- X)}^{\underline{N}})$

Metamath Proof Explorer

Theorem risefallfac

Proof