risefacval2

Description: One-based value of rising factorial. (Contributed by Scott Fenton, 15-Jan-2018)

		Ref	Expression
	Assertion	risefacval2	\|- ( ( A e. CC /\ N e. NN0 ) -> ( A RiseFac N ) = prod_ k e. ( 1 ... N ) ( A + ( k - 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		risefacval	\|- ( ( A e. CC /\ N e. NN0 ) -> ( A RiseFac N ) = prod_ n e. ( 0 ... ( N - 1 ) ) ( A + n ) )
2		1zzd	\|- ( ( A e. CC /\ N e. NN0 ) -> 1 e. ZZ )
3		0zd	\|- ( ( A e. CC /\ N e. NN0 ) -> 0 e. ZZ )
4		nn0z	\|- ( N e. NN0 -> N e. ZZ )
5		peano2zm	\|- ( N e. ZZ -> ( N - 1 ) e. ZZ )
6	4 5	syl	\|- ( N e. NN0 -> ( N - 1 ) e. ZZ )
7	6	adantl	\|- ( ( A e. CC /\ N e. NN0 ) -> ( N - 1 ) e. ZZ )
8		simpl	\|- ( ( A e. CC /\ N e. NN0 ) -> A e. CC )
9		elfznn0	\|- ( n e. ( 0 ... ( N - 1 ) ) -> n e. NN0 )
10	9	nn0cnd	\|- ( n e. ( 0 ... ( N - 1 ) ) -> n e. CC )
11		addcl	\|- ( ( A e. CC /\ n e. CC ) -> ( A + n ) e. CC )
12	8 10 11	syl2an	\|- ( ( ( A e. CC /\ N e. NN0 ) /\ n e. ( 0 ... ( N - 1 ) ) ) -> ( A + n ) e. CC )
13		oveq2	\|- ( n = ( k - 1 ) -> ( A + n ) = ( A + ( k - 1 ) ) )
14	2 3 7 12 13	fprodshft	\|- ( ( A e. CC /\ N e. NN0 ) -> prod_ n e. ( 0 ... ( N - 1 ) ) ( A + n ) = prod_ k e. ( ( 0 + 1 ) ... ( ( N - 1 ) + 1 ) ) ( A + ( k - 1 ) ) )
15		0p1e1	\|- ( 0 + 1 ) = 1
16	15	a1i	\|- ( ( A e. CC /\ N e. NN0 ) -> ( 0 + 1 ) = 1 )
17		nn0cn	\|- ( N e. NN0 -> N e. CC )
18		1cnd	\|- ( N e. NN0 -> 1 e. CC )
19	17 18	npcand	\|- ( N e. NN0 -> ( ( N - 1 ) + 1 ) = N )
20	19	adantl	\|- ( ( A e. CC /\ N e. NN0 ) -> ( ( N - 1 ) + 1 ) = N )
21	16 20	oveq12d	\|- ( ( A e. CC /\ N e. NN0 ) -> ( ( 0 + 1 ) ... ( ( N - 1 ) + 1 ) ) = ( 1 ... N ) )
22	21	prodeq1d	\|- ( ( A e. CC /\ N e. NN0 ) -> prod_ k e. ( ( 0 + 1 ) ... ( ( N - 1 ) + 1 ) ) ( A + ( k - 1 ) ) = prod_ k e. ( 1 ... N ) ( A + ( k - 1 ) ) )
23	1 14 22	3eqtrd	\|- ( ( A e. CC /\ N e. NN0 ) -> ( A RiseFac N ) = prod_ k e. ( 1 ... N ) ( A + ( k - 1 ) ) )

Metamath Proof Explorer

Theorem risefacval2

Proof