Theorem fprodfac

Description: Factorial using product notation. (Contributed by Scott Fenton, 15-Dec-2017)

	Ref	Expression
Assertion	fprodfac	|- ( A e. NN0 -> ( ! ` A ) = prod_ k e. ( 1 ... A ) k )

Proof

Step	Hyp	Ref	Expression
1		elnn0	|- ( A e. NN0 <-> ( A e. NN \/ A = 0 ) )
2		facnn	|- ( A e. NN -> ( ! ` A ) = ( seq 1 ( x. , _I ) ` A ) )
3		vex	|- k e. _V
4		fvi	|- ( k e. _V -> ( _I ` k ) = k )
5	3 4	mp1i	|- ( ( A e. NN /\ k e. ( 1 ... A ) ) -> ( _I ` k ) = k )
6		elnnuz	|- ( A e. NN <-> A e. ( ZZ>= ` 1 ) )
7	6	biimpi	|- ( A e. NN -> A e. ( ZZ>= ` 1 ) )
8		elfznn	|- ( k e. ( 1 ... A ) -> k e. NN )
9	8	nncnd	|- ( k e. ( 1 ... A ) -> k e. CC )
10	9	adantl	|- ( ( A e. NN /\ k e. ( 1 ... A ) ) -> k e. CC )
11	5 7 10	fprodser	|- ( A e. NN -> prod_ k e. ( 1 ... A ) k = ( seq 1 ( x. , _I ) ` A ) )
12	2 11	eqtr4d	|- ( A e. NN -> ( ! ` A ) = prod_ k e. ( 1 ... A ) k )
13		prod0	|- prod_ k e. (/) k = 1
14	13	eqcomi	|- 1 = prod_ k e. (/) k
15		fveq2	|- ( A = 0 -> ( ! ` A ) = ( ! ` 0 ) )
16		fac0	|- ( ! ` 0 ) = 1
17	15 16	eqtrdi	|- ( A = 0 -> ( ! ` A ) = 1 )
18		oveq2	|- ( A = 0 -> ( 1 ... A ) = ( 1 ... 0 ) )
19		fz10	|- ( 1 ... 0 ) = (/)
20	18 19	eqtrdi	|- ( A = 0 -> ( 1 ... A ) = (/) )
21	20	prodeq1d	|- ( A = 0 -> prod_ k e. ( 1 ... A ) k = prod_ k e. (/) k )
22	14 17 21	3eqtr4a	|- ( A = 0 -> ( ! ` A ) = prod_ k e. ( 1 ... A ) k )
23	12 22	jaoi	|- ( ( A e. NN \/ A = 0 ) -> ( ! ` A ) = prod_ k e. ( 1 ... A ) k )
24	1 23	sylbi	|- ( A e. NN0 -> ( ! ` A ) = prod_ k e. ( 1 ... A ) k )