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 ) ) )