This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 mullidd ⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑁 ∈ ℕ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 𝑁 ) ) )