# 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 )`
` |-  ( ( 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 ) )`
` |-  ( ( 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 )`
` |-  ( ( 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 )`
` |-  ( ( ( 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 ) ) )`