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 syl5req ⊢ ( 𝑁 ∈ ℕ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 𝑁 ) ) )