Metamath Proof Explorer


Theorem fallfacp1

Description: The value of the falling factorial at a successor. (Contributed by Scott Fenton, 5-Jan-2018)

Ref Expression
Assertion fallfacp1
|- ( ( A e. CC /\ N e. NN0 ) -> ( A FallFac ( N + 1 ) ) = ( ( A FallFac N ) x. ( A - N ) ) )

Proof

Step Hyp Ref Expression
1 nn0cn
 |-  ( N e. NN0 -> N e. CC )
2 1 adantl
 |-  ( ( A e. CC /\ N e. NN0 ) -> N e. CC )
3 1cnd
 |-  ( ( A e. CC /\ N e. NN0 ) -> 1 e. CC )
4 2 3 pncand
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( ( N + 1 ) - 1 ) = N )
5 4 oveq2d
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( 0 ... ( ( N + 1 ) - 1 ) ) = ( 0 ... N ) )
6 5 prodeq1d
 |-  ( ( A e. CC /\ N e. NN0 ) -> prod_ k e. ( 0 ... ( ( N + 1 ) - 1 ) ) ( A - k ) = prod_ k e. ( 0 ... N ) ( A - k ) )
7 elnn0uz
 |-  ( N e. NN0 <-> N e. ( ZZ>= ` 0 ) )
8 7 biimpi
 |-  ( N e. NN0 -> N e. ( ZZ>= ` 0 ) )
9 8 adantl
 |-  ( ( A e. CC /\ N e. NN0 ) -> N e. ( ZZ>= ` 0 ) )
10 elfznn0
 |-  ( k e. ( 0 ... N ) -> k e. NN0 )
11 10 nn0cnd
 |-  ( k e. ( 0 ... N ) -> k e. CC )
12 subcl
 |-  ( ( A e. CC /\ k e. CC ) -> ( A - k ) e. CC )
13 11 12 sylan2
 |-  ( ( A e. CC /\ k e. ( 0 ... N ) ) -> ( A - k ) e. CC )
14 13 adantlr
 |-  ( ( ( A e. CC /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> ( A - k ) e. CC )
15 oveq2
 |-  ( k = N -> ( A - k ) = ( A - N ) )
16 9 14 15 fprodm1
 |-  ( ( A e. CC /\ N e. NN0 ) -> prod_ k e. ( 0 ... N ) ( A - k ) = ( prod_ k e. ( 0 ... ( N - 1 ) ) ( A - k ) x. ( A - N ) ) )
17 6 16 eqtrd
 |-  ( ( A e. CC /\ N e. NN0 ) -> prod_ k e. ( 0 ... ( ( N + 1 ) - 1 ) ) ( A - k ) = ( prod_ k e. ( 0 ... ( N - 1 ) ) ( A - k ) x. ( A - N ) ) )
18 peano2nn0
 |-  ( N e. NN0 -> ( N + 1 ) e. NN0 )
19 fallfacval
 |-  ( ( A e. CC /\ ( N + 1 ) e. NN0 ) -> ( A FallFac ( N + 1 ) ) = prod_ k e. ( 0 ... ( ( N + 1 ) - 1 ) ) ( A - k ) )
20 18 19 sylan2
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( A FallFac ( N + 1 ) ) = prod_ k e. ( 0 ... ( ( N + 1 ) - 1 ) ) ( A - k ) )
21 fallfacval
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( A FallFac N ) = prod_ k e. ( 0 ... ( N - 1 ) ) ( A - k ) )
22 21 oveq1d
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( ( A FallFac N ) x. ( A - N ) ) = ( prod_ k e. ( 0 ... ( N - 1 ) ) ( A - k ) x. ( A - N ) ) )
23 17 20 22 3eqtr4d
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( A FallFac ( N + 1 ) ) = ( ( A FallFac N ) x. ( A - N ) ) )