This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )