Metamath Proof Explorer

Theorem risefallfac

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

Ref Expression
Assertion risefallfac 
|- ( ( X e. CC /\ N e. NN0 ) -> ( X RiseFac N ) = ( ( -u 1 ^ N ) x. ( -u X FallFac N ) ) )

Proof

Step Hyp Ref Expression
1 negcl 
 |-  ( X e. CC -> -u X e. CC )
2 1 adantr 
 |-  ( ( X e. CC /\ N e. NN0 ) -> -u X e. CC )
3 elfznn 
 |-  ( k e. ( 1 ... N ) -> k e. NN )
4 nnm1nn0 
 |-  ( k e. NN -> ( k - 1 ) e. NN0 )
5 3 4 syl 
 |-  ( k e. ( 1 ... N ) -> ( k - 1 ) e. NN0 )
6 5 nn0cnd 
 |-  ( k e. ( 1 ... N ) -> ( k - 1 ) e. CC )
7 subcl 
 |-  ( ( -u X e. CC /\ ( k - 1 ) e. CC ) -> ( -u X - ( k - 1 ) ) e. CC )
8 2 6 7 syl2an 
 |-  ( ( ( X e. CC /\ N e. NN0 ) /\ k e. ( 1 ... N ) ) -> ( -u X - ( k - 1 ) ) e. CC )
9 8 mulm1d 
 |-  ( ( ( X e. CC /\ N e. NN0 ) /\ k e. ( 1 ... N ) ) -> ( -u 1 x. ( -u X - ( k - 1 ) ) ) = -u ( -u X - ( k - 1 ) ) )
10 simpll 
 |-  ( ( ( X e. CC /\ N e. NN0 ) /\ k e. ( 1 ... N ) ) -> X e. CC )
11 6 adantl 
 |-  ( ( ( X e. CC /\ N e. NN0 ) /\ k e. ( 1 ... N ) ) -> ( k - 1 ) e. CC )
12 10 11 negdi2d 
 |-  ( ( ( X e. CC /\ N e. NN0 ) /\ k e. ( 1 ... N ) ) -> -u ( X + ( k - 1 ) ) = ( -u X - ( k - 1 ) ) )
13 12 negeqd 
 |-  ( ( ( X e. CC /\ N e. NN0 ) /\ k e. ( 1 ... N ) ) -> -u -u ( X + ( k - 1 ) ) = -u ( -u X - ( k - 1 ) ) )
14 simpl 
 |-  ( ( X e. CC /\ N e. NN0 ) -> X e. CC )
15 addcl 
 |-  ( ( X e. CC /\ ( k - 1 ) e. CC ) -> ( X + ( k - 1 ) ) e. CC )
16 14 6 15 syl2an 
 |-  ( ( ( X e. CC /\ N e. NN0 ) /\ k e. ( 1 ... N ) ) -> ( X + ( k - 1 ) ) e. CC )
17 16 negnegd 
 |-  ( ( ( X e. CC /\ N e. NN0 ) /\ k e. ( 1 ... N ) ) -> -u -u ( X + ( k - 1 ) ) = ( X + ( k - 1 ) ) )
18 9 13 17 3eqtr2rd 
 |-  ( ( ( X e. CC /\ N e. NN0 ) /\ k e. ( 1 ... N ) ) -> ( X + ( k - 1 ) ) = ( -u 1 x. ( -u X - ( k - 1 ) ) ) )
19 18 prodeq2dv 
 |-  ( ( X e. CC /\ N e. NN0 ) -> prod_ k e. ( 1 ... N ) ( X + ( k - 1 ) ) = prod_ k e. ( 1 ... N ) ( -u 1 x. ( -u X - ( k - 1 ) ) ) )
20 risefacval2 
 |-  ( ( X e. CC /\ N e. NN0 ) -> ( X RiseFac N ) = prod_ k e. ( 1 ... N ) ( X + ( k - 1 ) ) )
21 fzfi 
 |-  ( 1 ... N ) e. Fin
22 neg1cn 
 |-  -u 1 e. CC
23 fprodconst 
 |-  ( ( ( 1 ... N ) e. Fin /\ -u 1 e. CC ) -> prod_ k e. ( 1 ... N ) -u 1 = ( -u 1 ^ ( # ` ( 1 ... N ) ) ) )
24 21 22 23 mp2an 
 |-  prod_ k e. ( 1 ... N ) -u 1 = ( -u 1 ^ ( # ` ( 1 ... N ) ) )
25 hashfz1 
 |-  ( N e. NN0 -> ( # ` ( 1 ... N ) ) = N )
26 25 oveq2d 
 |-  ( N e. NN0 -> ( -u 1 ^ ( # ` ( 1 ... N ) ) ) = ( -u 1 ^ N ) )
27 24 26 syl5req 
 |-  ( N e. NN0 -> ( -u 1 ^ N ) = prod_ k e. ( 1 ... N ) -u 1 )
28 27 adantl 
 |-  ( ( X e. CC /\ N e. NN0 ) -> ( -u 1 ^ N ) = prod_ k e. ( 1 ... N ) -u 1 )
29 fallfacval2 
 |-  ( ( -u X e. CC /\ N e. NN0 ) -> ( -u X FallFac N ) = prod_ k e. ( 1 ... N ) ( -u X - ( k - 1 ) ) )
30 1 29 sylan 
 |-  ( ( X e. CC /\ N e. NN0 ) -> ( -u X FallFac N ) = prod_ k e. ( 1 ... N ) ( -u X - ( k - 1 ) ) )
31 28 30 oveq12d 
 |-  ( ( X e. CC /\ N e. NN0 ) -> ( ( -u 1 ^ N ) x. ( -u X FallFac N ) ) = ( prod_ k e. ( 1 ... N ) -u 1 x. prod_ k e. ( 1 ... N ) ( -u X - ( k - 1 ) ) ) )
32 fzfid 
 |-  ( ( X e. CC /\ N e. NN0 ) -> ( 1 ... N ) e. Fin )
33 22 a1i 
 |-  ( ( ( X e. CC /\ N e. NN0 ) /\ k e. ( 1 ... N ) ) -> -u 1 e. CC )
34 32 33 8 fprodmul 
 |-  ( ( X e. CC /\ N e. NN0 ) -> prod_ k e. ( 1 ... N ) ( -u 1 x. ( -u X - ( k - 1 ) ) ) = ( prod_ k e. ( 1 ... N ) -u 1 x. prod_ k e. ( 1 ... N ) ( -u X - ( k - 1 ) ) ) )
35 31 34 eqtr4d 
 |-  ( ( X e. CC /\ N e. NN0 ) -> ( ( -u 1 ^ N ) x. ( -u X FallFac N ) ) = prod_ k e. ( 1 ... N ) ( -u 1 x. ( -u X - ( k - 1 ) ) ) )
36 19 20 35 3eqtr4d 
 |-  ( ( X e. CC /\ N e. NN0 ) -> ( X RiseFac N ) = ( ( -u 1 ^ N ) x. ( -u X FallFac N ) ) )