Theorem fallrisefac

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

	Ref	Expression
Assertion	fallrisefac	⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑋 FallFac 𝑁 ) = ( ( - 1 ↑ 𝑁 ) · ( - 𝑋 RiseFac 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		nn0cn	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ )
2	1	2timesd	⊢ ( 𝑁 ∈ ℕ0 → ( 2 · 𝑁 ) = ( 𝑁 + 𝑁 ) )
3	2	oveq2d	⊢ ( 𝑁 ∈ ℕ0 → ( - 1 ↑ ( 2 · 𝑁 ) ) = ( - 1 ↑ ( 𝑁 + 𝑁 ) ) )
4		nn0z	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
5		m1expeven	⊢ ( 𝑁 ∈ ℤ → ( - 1 ↑ ( 2 · 𝑁 ) ) = 1 )
6	4 5	syl	⊢ ( 𝑁 ∈ ℕ0 → ( - 1 ↑ ( 2 · 𝑁 ) ) = 1 )
7		neg1cn	⊢ - 1 ∈ ℂ
8		expadd	⊢ ( ( - 1 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( - 1 ↑ ( 𝑁 + 𝑁 ) ) = ( ( - 1 ↑ 𝑁 ) · ( - 1 ↑ 𝑁 ) ) )
9	7 8	mp3an1	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( - 1 ↑ ( 𝑁 + 𝑁 ) ) = ( ( - 1 ↑ 𝑁 ) · ( - 1 ↑ 𝑁 ) ) )
10	9	anidms	⊢ ( 𝑁 ∈ ℕ0 → ( - 1 ↑ ( 𝑁 + 𝑁 ) ) = ( ( - 1 ↑ 𝑁 ) · ( - 1 ↑ 𝑁 ) ) )
11	3 6 10	3eqtr3rd	⊢ ( 𝑁 ∈ ℕ0 → ( ( - 1 ↑ 𝑁 ) · ( - 1 ↑ 𝑁 ) ) = 1 )
12	11	adantl	⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑁 ) · ( - 1 ↑ 𝑁 ) ) = 1 )
13		negneg	⊢ ( 𝑋 ∈ ℂ → - - 𝑋 = 𝑋 )
14	13	adantr	⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → - - 𝑋 = 𝑋 )
15	14	oveq1d	⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( - - 𝑋 FallFac 𝑁 ) = ( 𝑋 FallFac 𝑁 ) )
16	12 15	oveq12d	⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( ( - 1 ↑ 𝑁 ) · ( - 1 ↑ 𝑁 ) ) · ( - - 𝑋 FallFac 𝑁 ) ) = ( 1 · ( 𝑋 FallFac 𝑁 ) ) )
17		expcl	⊢ ( ( - 1 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( - 1 ↑ 𝑁 ) ∈ ℂ )
18	7 17	mpan	⊢ ( 𝑁 ∈ ℕ0 → ( - 1 ↑ 𝑁 ) ∈ ℂ )
19	18	adantl	⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( - 1 ↑ 𝑁 ) ∈ ℂ )
20		negcl	⊢ ( 𝑋 ∈ ℂ → - 𝑋 ∈ ℂ )
21	20	negcld	⊢ ( 𝑋 ∈ ℂ → - - 𝑋 ∈ ℂ )
22		fallfaccl	⊢ ( ( - - 𝑋 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( - - 𝑋 FallFac 𝑁 ) ∈ ℂ )
23	21 22	sylan	⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( - - 𝑋 FallFac 𝑁 ) ∈ ℂ )
24	19 19 23	mulassd	⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( ( - 1 ↑ 𝑁 ) · ( - 1 ↑ 𝑁 ) ) · ( - - 𝑋 FallFac 𝑁 ) ) = ( ( - 1 ↑ 𝑁 ) · ( ( - 1 ↑ 𝑁 ) · ( - - 𝑋 FallFac 𝑁 ) ) ) )
25		fallfaccl	⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑋 FallFac 𝑁 ) ∈ ℂ )
26	25	mulid2d	⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 1 · ( 𝑋 FallFac 𝑁 ) ) = ( 𝑋 FallFac 𝑁 ) )
27	16 24 26	3eqtr3rd	⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑋 FallFac 𝑁 ) = ( ( - 1 ↑ 𝑁 ) · ( ( - 1 ↑ 𝑁 ) · ( - - 𝑋 FallFac 𝑁 ) ) ) )
28		risefallfac	⊢ ( ( - 𝑋 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( - 𝑋 RiseFac 𝑁 ) = ( ( - 1 ↑ 𝑁 ) · ( - - 𝑋 FallFac 𝑁 ) ) )
29	20 28	sylan	⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( - 𝑋 RiseFac 𝑁 ) = ( ( - 1 ↑ 𝑁 ) · ( - - 𝑋 FallFac 𝑁 ) ) )
30	29	oveq2d	⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑁 ) · ( - 𝑋 RiseFac 𝑁 ) ) = ( ( - 1 ↑ 𝑁 ) · ( ( - 1 ↑ 𝑁 ) · ( - - 𝑋 FallFac 𝑁 ) ) ) )
31	27 30	eqtr4d	⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑋 FallFac 𝑁 ) = ( ( - 1 ↑ 𝑁 ) · ( - 𝑋 RiseFac 𝑁 ) ) )