Metamath Proof Explorer


Theorem risefallfac

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

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

Proof

Step Hyp Ref Expression
1 negcl ( 𝑋 ∈ ℂ → - 𝑋 ∈ ℂ )
2 1 adantr ( ( 𝑋 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → - 𝑋 ∈ ℂ )
3 elfznn ( 𝑘 ∈ ( 1 ... 𝑁 ) → 𝑘 ∈ ℕ )
4 nnm1nn0 ( 𝑘 ∈ ℕ → ( 𝑘 − 1 ) ∈ ℕ0 )
5 3 4 syl ( 𝑘 ∈ ( 1 ... 𝑁 ) → ( 𝑘 − 1 ) ∈ ℕ0 )
6 5 nn0cnd ( 𝑘 ∈ ( 1 ... 𝑁 ) → ( 𝑘 − 1 ) ∈ ℂ )
7 subcl ( ( - 𝑋 ∈ ℂ ∧ ( 𝑘 − 1 ) ∈ ℂ ) → ( - 𝑋 − ( 𝑘 − 1 ) ) ∈ ℂ )
8 2 6 7 syl2an ( ( ( 𝑋 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( - 𝑋 − ( 𝑘 − 1 ) ) ∈ ℂ )
9 8 mulm1d ( ( ( 𝑋 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( - 1 · ( - 𝑋 − ( 𝑘 − 1 ) ) ) = - ( - 𝑋 − ( 𝑘 − 1 ) ) )
10 simpll ( ( ( 𝑋 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑋 ∈ ℂ )
11 6 adantl ( ( ( 𝑋 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝑘 − 1 ) ∈ ℂ )
12 10 11 negdi2d ( ( ( 𝑋 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → - ( 𝑋 + ( 𝑘 − 1 ) ) = ( - 𝑋 − ( 𝑘 − 1 ) ) )
13 12 negeqd ( ( ( 𝑋 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → - - ( 𝑋 + ( 𝑘 − 1 ) ) = - ( - 𝑋 − ( 𝑘 − 1 ) ) )
14 simpl ( ( 𝑋 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → 𝑋 ∈ ℂ )
15 addcl ( ( 𝑋 ∈ ℂ ∧ ( 𝑘 − 1 ) ∈ ℂ ) → ( 𝑋 + ( 𝑘 − 1 ) ) ∈ ℂ )
16 14 6 15 syl2an ( ( ( 𝑋 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝑋 + ( 𝑘 − 1 ) ) ∈ ℂ )
17 16 negnegd ( ( ( 𝑋 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → - - ( 𝑋 + ( 𝑘 − 1 ) ) = ( 𝑋 + ( 𝑘 − 1 ) ) )
18 9 13 17 3eqtr2rd ( ( ( 𝑋 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝑋 + ( 𝑘 − 1 ) ) = ( - 1 · ( - 𝑋 − ( 𝑘 − 1 ) ) ) )
19 18 prodeq2dv ( ( 𝑋 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ∏ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝑋 + ( 𝑘 − 1 ) ) = ∏ 𝑘 ∈ ( 1 ... 𝑁 ) ( - 1 · ( - 𝑋 − ( 𝑘 − 1 ) ) ) )
20 risefacval2 ( ( 𝑋 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑋 RiseFac 𝑁 ) = ∏ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝑋 + ( 𝑘 − 1 ) ) )
21 fzfi ( 1 ... 𝑁 ) ∈ Fin
22 neg1cn - 1 ∈ ℂ
23 fprodconst ( ( ( 1 ... 𝑁 ) ∈ Fin ∧ - 1 ∈ ℂ ) → ∏ 𝑘 ∈ ( 1 ... 𝑁 ) - 1 = ( - 1 ↑ ( ♯ ‘ ( 1 ... 𝑁 ) ) ) )
24 21 22 23 mp2an 𝑘 ∈ ( 1 ... 𝑁 ) - 1 = ( - 1 ↑ ( ♯ ‘ ( 1 ... 𝑁 ) ) )
25 hashfz1 ( 𝑁 ∈ ℕ0 → ( ♯ ‘ ( 1 ... 𝑁 ) ) = 𝑁 )
26 25 oveq2d ( 𝑁 ∈ ℕ0 → ( - 1 ↑ ( ♯ ‘ ( 1 ... 𝑁 ) ) ) = ( - 1 ↑ 𝑁 ) )
27 24 26 eqtr2id ( 𝑁 ∈ ℕ0 → ( - 1 ↑ 𝑁 ) = ∏ 𝑘 ∈ ( 1 ... 𝑁 ) - 1 )
28 27 adantl ( ( 𝑋 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( - 1 ↑ 𝑁 ) = ∏ 𝑘 ∈ ( 1 ... 𝑁 ) - 1 )
29 fallfacval2 ( ( - 𝑋 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( - 𝑋 FallFac 𝑁 ) = ∏ 𝑘 ∈ ( 1 ... 𝑁 ) ( - 𝑋 − ( 𝑘 − 1 ) ) )
30 1 29 sylan ( ( 𝑋 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( - 𝑋 FallFac 𝑁 ) = ∏ 𝑘 ∈ ( 1 ... 𝑁 ) ( - 𝑋 − ( 𝑘 − 1 ) ) )
31 28 30 oveq12d ( ( 𝑋 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑁 ) · ( - 𝑋 FallFac 𝑁 ) ) = ( ∏ 𝑘 ∈ ( 1 ... 𝑁 ) - 1 · ∏ 𝑘 ∈ ( 1 ... 𝑁 ) ( - 𝑋 − ( 𝑘 − 1 ) ) ) )
32 fzfid ( ( 𝑋 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 1 ... 𝑁 ) ∈ Fin )
33 22 a1i ( ( ( 𝑋 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → - 1 ∈ ℂ )
34 32 33 8 fprodmul ( ( 𝑋 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ∏ 𝑘 ∈ ( 1 ... 𝑁 ) ( - 1 · ( - 𝑋 − ( 𝑘 − 1 ) ) ) = ( ∏ 𝑘 ∈ ( 1 ... 𝑁 ) - 1 · ∏ 𝑘 ∈ ( 1 ... 𝑁 ) ( - 𝑋 − ( 𝑘 − 1 ) ) ) )
35 31 34 eqtr4d ( ( 𝑋 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑁 ) · ( - 𝑋 FallFac 𝑁 ) ) = ∏ 𝑘 ∈ ( 1 ... 𝑁 ) ( - 1 · ( - 𝑋 − ( 𝑘 − 1 ) ) ) )
36 19 20 35 3eqtr4d ( ( 𝑋 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑋 RiseFac 𝑁 ) = ( ( - 1 ↑ 𝑁 ) · ( - 𝑋 FallFac 𝑁 ) ) )