Metamath Proof Explorer

Theorem risefacp1

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

Ref Expression
Assertion risefacp1 
|- ( ( A e. CC /\ N e. NN0 ) -> ( A RiseFac ( N + 1 ) ) = ( ( A RiseFac 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 addcl 
 |-  ( ( 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 risefacval 
 |-  ( ( A e. CC /\ ( N + 1 ) e. NN0 ) -> ( A RiseFac ( N + 1 ) ) = prod_ k e. ( 0 ... ( ( N + 1 ) - 1 ) ) ( A + k ) )
20 18 19 sylan2 
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( A RiseFac ( N + 1 ) ) = prod_ k e. ( 0 ... ( ( N + 1 ) - 1 ) ) ( A + k ) )
21 risefacval 
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( A RiseFac N ) = prod_ k e. ( 0 ... ( N - 1 ) ) ( A + k ) )
22 21 oveq1d 
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( ( A RiseFac 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 RiseFac ( N + 1 ) ) = ( ( A RiseFac N ) x. ( A + N ) ) )