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