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

Metamath Proof Explorer

Theorem fallfaccllem

Description: Lemma for falling factorial closure laws. (Contributed by Scott Fenton, 5-Jan-2018)

Ref Expression
Hypotheses risefallfaccllem.1 
|- S C_ CC
risefallfaccllem.2 
|- 1 e. S
risefallfaccllem.3 
|- ( ( x e. S /\ y e. S ) -> ( x x. y ) e. S )
fallfaccllem.4 
|- ( ( A e. S /\ k e. NN0 ) -> ( A - k ) e. S )
Assertion fallfaccllem 
|- ( ( A e. S /\ N e. NN0 ) -> ( A FallFac N ) e. S )

Proof

Step Hyp Ref Expression
1 risefallfaccllem.1 
 |-  S C_ CC
2 risefallfaccllem.2 
 |-  1 e. S
3 risefallfaccllem.3 
 |-  ( ( x e. S /\ y e. S ) -> ( x x. y ) e. S )
4 fallfaccllem.4 
 |-  ( ( A e. S /\ k e. NN0 ) -> ( A - k ) e. S )
5 1 sseli 
 |-  ( A e. S -> A e. CC )
6 fallfacval 
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( A FallFac N ) = prod_ k e. ( 0 ... ( N - 1 ) ) ( A - k ) )
7 5 6 sylan 
 |-  ( ( A e. S /\ N e. NN0 ) -> ( A FallFac N ) = prod_ k e. ( 0 ... ( N - 1 ) ) ( A - k ) )
8 1 a1i 
 |-  ( A e. S -> S C_ CC )
9 3 adantl 
 |-  ( ( A e. S /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S )
10 fzfid 
 |-  ( A e. S -> ( 0 ... ( N - 1 ) ) e. Fin )
11 elfznn0 
 |-  ( k e. ( 0 ... ( N - 1 ) ) -> k e. NN0 )
12 11 4 sylan2 
 |-  ( ( A e. S /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( A - k ) e. S )
13 2 a1i 
 |-  ( A e. S -> 1 e. S )
14 8 9 10 12 13 fprodcllem 
 |-  ( A e. S -> prod_ k e. ( 0 ... ( N - 1 ) ) ( A - k ) e. S )
15 14 adantr 
 |-  ( ( A e. S /\ N e. NN0 ) -> prod_ k e. ( 0 ... ( N - 1 ) ) ( A - k ) e. S )
16 7 15 eqeltrd 
 |-  ( ( A e. S /\ N e. NN0 ) -> ( A FallFac N ) e. S )