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
risefallfaccllem.2 1 S
risefallfaccllem.3 x S y S x y S
fallfaccllem.4 A S k 0 A k S
Assertion fallfaccllem A S N 0 A N _ S

Proof

Step Hyp Ref Expression
1 risefallfaccllem.1 S
2 risefallfaccllem.2 1 S
3 risefallfaccllem.3 x S y S x y S
4 fallfaccllem.4 A S k 0 A k S
5 1 sseli A S A
6 fallfacval A N 0 A N _ = k = 0 N 1 A k
7 5 6 sylan A S N 0 A N _ = k = 0 N 1 A k
8 1 a1i A S S
9 3 adantl A S x S y S x y S
10 fzfid A S 0 N 1 Fin
11 elfznn0 k 0 N 1 k 0
12 11 4 sylan2 A S k 0 N 1 A k S
13 2 a1i A S 1 S
14 8 9 10 12 13 fprodcllem A S k = 0 N 1 A k S
15 14 adantr A S N 0 k = 0 N 1 A k S
16 7 15 eqeltrd A S N 0 A N _ S