fallrisefac

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

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

Proof

Step	Hyp	Ref	Expression
1		nn0cn	$⊢ N \in ℕ_{0} \to N \in ℂ$
2	1	2timesd	$⊢ N \in ℕ_{0} \to 2 \cdot N = N + N$
3	2	oveq2d	$⊢ N \in ℕ_{0} \to {(- 1)}^{2 \cdot N} = {(- 1)}^{N + N}$
4		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
5		m1expeven	$⊢ N \in ℤ \to {(- 1)}^{2 \cdot N} = 1$
6	4 5	syl	$⊢ N \in ℕ_{0} \to {(- 1)}^{2 \cdot N} = 1$
7		neg1cn	$⊢ - 1 \in ℂ$
8		expadd	$⊢ (- 1 \in ℂ \land N \in ℕ_{0} \land N \in ℕ_{0}) \to {(- 1)}^{N + N} = {(- 1)}^{N} {(- 1)}^{N}$
9	7 8	mp3an1	$⊢ (N \in ℕ_{0} \land N \in ℕ_{0}) \to {(- 1)}^{N + N} = {(- 1)}^{N} {(- 1)}^{N}$
10	9	anidms	$⊢ N \in ℕ_{0} \to {(- 1)}^{N + N} = {(- 1)}^{N} {(- 1)}^{N}$
11	3 6 10	3eqtr3rd	$⊢ N \in ℕ_{0} \to {(- 1)}^{N} {(- 1)}^{N} = 1$
12	11	adantl	$⊢ (X \in ℂ \land N \in ℕ_{0}) \to {(- 1)}^{N} {(- 1)}^{N} = 1$
13		negneg	$⊢ X \in ℂ \to - (- X) = X$
14	13	adantr	$⊢ (X \in ℂ \land N \in ℕ_{0}) \to - (- X) = X$
15	14	oveq1d	$⊢ (X \in ℂ \land N \in ℕ_{0}) \to {(- (- X))}^{\underline{N}} = X^{\underline{N}}$
16	12 15	oveq12d	$⊢ (X \in ℂ \land N \in ℕ_{0}) \to {(- 1)}^{N} {(- 1)}^{N} ({(- (- X))}^{\underline{N}}) = 1 (X^{\underline{N}})$
17		expcl	$⊢ (- 1 \in ℂ \land N \in ℕ_{0}) \to {(- 1)}^{N} \in ℂ$
18	7 17	mpan	$⊢ N \in ℕ_{0} \to {(- 1)}^{N} \in ℂ$
19	18	adantl	$⊢ (X \in ℂ \land N \in ℕ_{0}) \to {(- 1)}^{N} \in ℂ$
20		negcl	$⊢ X \in ℂ \to - X \in ℂ$
21	20	negcld	$⊢ X \in ℂ \to - (- X) \in ℂ$
22		fallfaccl	$⊢ (- (- X) \in ℂ \land N \in ℕ_{0}) \to {(- (- X))}^{\underline{N}} \in ℂ$
23	21 22	sylan	$⊢ (X \in ℂ \land N \in ℕ_{0}) \to {(- (- X))}^{\underline{N}} \in ℂ$
24	19 19 23	mulassd	$⊢ (X \in ℂ \land N \in ℕ_{0}) \to {(- 1)}^{N} {(- 1)}^{N} ({(- (- X))}^{\underline{N}}) = {(- 1)}^{N} {(- 1)}^{N} ({(- (- X))}^{\underline{N}})$
25		fallfaccl	$⊢ (X \in ℂ \land N \in ℕ_{0}) \to X^{\underline{N}} \in ℂ$
26	25	mullidd	$⊢ (X \in ℂ \land N \in ℕ_{0}) \to 1 (X^{\underline{N}}) = X^{\underline{N}}$
27	16 24 26	3eqtr3rd	$⊢ (X \in ℂ \land N \in ℕ_{0}) \to X^{\underline{N}} = {(- 1)}^{N} {(- 1)}^{N} ({(- (- X))}^{\underline{N}})$
28		risefallfac	$⊢ (- X \in ℂ \land N \in ℕ_{0}) \to {(- X)}^{\overline{N}} = {(- 1)}^{N} ({(- (- X))}^{\underline{N}})$
29	20 28	sylan	$⊢ (X \in ℂ \land N \in ℕ_{0}) \to {(- X)}^{\overline{N}} = {(- 1)}^{N} ({(- (- X))}^{\underline{N}})$
30	29	oveq2d	$⊢ (X \in ℂ \land N \in ℕ_{0}) \to {(- 1)}^{N} ({(- X)}^{\overline{N}}) = {(- 1)}^{N} {(- 1)}^{N} ({(- (- X))}^{\underline{N}})$
31	27 30	eqtr4d	$⊢ (X \in ℂ \land N \in ℕ_{0}) \to X^{\underline{N}} = {(- 1)}^{N} ({(- X)}^{\overline{N}})$

Metamath Proof Explorer

Theorem fallrisefac

Proof