Metamath Proof Explorer

Theorem fallrisefac

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

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

Proof

Step Hyp Ref Expression
1 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
2 1 2timesd 
 |-  ( N e. NN0 -> ( 2 x. N ) = ( N + N ) )
3 2 oveq2d 
 |-  ( N e. NN0 -> ( -u 1 ^ ( 2 x. N ) ) = ( -u 1 ^ ( N + N ) ) )
4 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
5 m1expeven 
 |-  ( N e. ZZ -> ( -u 1 ^ ( 2 x. N ) ) = 1 )
6 4 5 syl 
 |-  ( N e. NN0 -> ( -u 1 ^ ( 2 x. N ) ) = 1 )
7 neg1cn 
 |-  -u 1 e. CC
8 expadd 
 |-  ( ( -u 1 e. CC /\ N e. NN0 /\ N e. NN0 ) -> ( -u 1 ^ ( N + N ) ) = ( ( -u 1 ^ N ) x. ( -u 1 ^ N ) ) )
9 7 8 mp3an1 
 |-  ( ( N e. NN0 /\ N e. NN0 ) -> ( -u 1 ^ ( N + N ) ) = ( ( -u 1 ^ N ) x. ( -u 1 ^ N ) ) )
10 9 anidms 
 |-  ( N e. NN0 -> ( -u 1 ^ ( N + N ) ) = ( ( -u 1 ^ N ) x. ( -u 1 ^ N ) ) )
11 3 6 10 3eqtr3rd 
 |-  ( N e. NN0 -> ( ( -u 1 ^ N ) x. ( -u 1 ^ N ) ) = 1 )
12 11 adantl 
 |-  ( ( X e. CC /\ N e. NN0 ) -> ( ( -u 1 ^ N ) x. ( -u 1 ^ N ) ) = 1 )
13 negneg 
 |-  ( X e. CC -> -u -u X = X )
14 13 adantr 
 |-  ( ( X e. CC /\ N e. NN0 ) -> -u -u X = X )
15 14 oveq1d 
 |-  ( ( X e. CC /\ N e. NN0 ) -> ( -u -u X FallFac N ) = ( X FallFac N ) )
16 12 15 oveq12d 
 |-  ( ( X e. CC /\ N e. NN0 ) -> ( ( ( -u 1 ^ N ) x. ( -u 1 ^ N ) ) x. ( -u -u X FallFac N ) ) = ( 1 x. ( X FallFac N ) ) )
17 expcl 
 |-  ( ( -u 1 e. CC /\ N e. NN0 ) -> ( -u 1 ^ N ) e. CC )
18 7 17 mpan 
 |-  ( N e. NN0 -> ( -u 1 ^ N ) e. CC )
19 18 adantl 
 |-  ( ( X e. CC /\ N e. NN0 ) -> ( -u 1 ^ N ) e. CC )
20 negcl 
 |-  ( X e. CC -> -u X e. CC )
21 20 negcld 
 |-  ( X e. CC -> -u -u X e. CC )
22 fallfaccl 
 |-  ( ( -u -u X e. CC /\ N e. NN0 ) -> ( -u -u X FallFac N ) e. CC )
23 21 22 sylan 
 |-  ( ( X e. CC /\ N e. NN0 ) -> ( -u -u X FallFac N ) e. CC )
24 19 19 23 mulassd 
 |-  ( ( X e. CC /\ N e. NN0 ) -> ( ( ( -u 1 ^ N ) x. ( -u 1 ^ N ) ) x. ( -u -u X FallFac N ) ) = ( ( -u 1 ^ N ) x. ( ( -u 1 ^ N ) x. ( -u -u X FallFac N ) ) ) )
25 fallfaccl 
 |-  ( ( X e. CC /\ N e. NN0 ) -> ( X FallFac N ) e. CC )
26 25 mulid2d 
 |-  ( ( X e. CC /\ N e. NN0 ) -> ( 1 x. ( X FallFac N ) ) = ( X FallFac N ) )
27 16 24 26 3eqtr3rd 
 |-  ( ( X e. CC /\ N e. NN0 ) -> ( X FallFac N ) = ( ( -u 1 ^ N ) x. ( ( -u 1 ^ N ) x. ( -u -u X FallFac N ) ) ) )
28 risefallfac 
 |-  ( ( -u X e. CC /\ N e. NN0 ) -> ( -u X RiseFac N ) = ( ( -u 1 ^ N ) x. ( -u -u X FallFac N ) ) )
29 20 28 sylan 
 |-  ( ( X e. CC /\ N e. NN0 ) -> ( -u X RiseFac N ) = ( ( -u 1 ^ N ) x. ( -u -u X FallFac N ) ) )
30 29 oveq2d 
 |-  ( ( X e. CC /\ N e. NN0 ) -> ( ( -u 1 ^ N ) x. ( -u X RiseFac N ) ) = ( ( -u 1 ^ N ) x. ( ( -u 1 ^ N ) x. ( -u -u X FallFac N ) ) ) )
31 27 30 eqtr4d 
 |-  ( ( X e. CC /\ N e. NN0 ) -> ( X FallFac N ) = ( ( -u 1 ^ N ) x. ( -u X RiseFac N ) ) )