Metamath Proof Explorer


Theorem fallfaccllem

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

Ref Expression
Hypotheses risefallfaccllem.1 โŠข ๐‘† โŠ† โ„‚
risefallfaccllem.2 โŠข 1 โˆˆ ๐‘†
risefallfaccllem.3 โŠข ( ( ๐‘ฅ โˆˆ ๐‘† โˆง ๐‘ฆ โˆˆ ๐‘† ) โ†’ ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘† )
fallfaccllem.4 โŠข ( ( ๐ด โˆˆ ๐‘† โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ( ๐ด โˆ’ ๐‘˜ ) โˆˆ ๐‘† )
Assertion fallfaccllem ( ( ๐ด โˆˆ ๐‘† โˆง ๐‘ โˆˆ โ„•0 ) โ†’ ( ๐ด FallFac ๐‘ ) โˆˆ ๐‘† )

Proof

Step Hyp Ref Expression
1 risefallfaccllem.1 โŠข ๐‘† โŠ† โ„‚
2 risefallfaccllem.2 โŠข 1 โˆˆ ๐‘†
3 risefallfaccllem.3 โŠข ( ( ๐‘ฅ โˆˆ ๐‘† โˆง ๐‘ฆ โˆˆ ๐‘† ) โ†’ ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘† )
4 fallfaccllem.4 โŠข ( ( ๐ด โˆˆ ๐‘† โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ( ๐ด โˆ’ ๐‘˜ ) โˆˆ ๐‘† )
5 1 sseli โŠข ( ๐ด โˆˆ ๐‘† โ†’ ๐ด โˆˆ โ„‚ )
6 fallfacval โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„•0 ) โ†’ ( ๐ด FallFac ๐‘ ) = โˆ ๐‘˜ โˆˆ ( 0 ... ( ๐‘ โˆ’ 1 ) ) ( ๐ด โˆ’ ๐‘˜ ) )
7 5 6 sylan โŠข ( ( ๐ด โˆˆ ๐‘† โˆง ๐‘ โˆˆ โ„•0 ) โ†’ ( ๐ด FallFac ๐‘ ) = โˆ ๐‘˜ โˆˆ ( 0 ... ( ๐‘ โˆ’ 1 ) ) ( ๐ด โˆ’ ๐‘˜ ) )
8 1 a1i โŠข ( ๐ด โˆˆ ๐‘† โ†’ ๐‘† โŠ† โ„‚ )
9 3 adantl โŠข ( ( ๐ด โˆˆ ๐‘† โˆง ( ๐‘ฅ โˆˆ ๐‘† โˆง ๐‘ฆ โˆˆ ๐‘† ) ) โ†’ ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘† )
10 fzfid โŠข ( ๐ด โˆˆ ๐‘† โ†’ ( 0 ... ( ๐‘ โˆ’ 1 ) ) โˆˆ Fin )
11 elfznn0 โŠข ( ๐‘˜ โˆˆ ( 0 ... ( ๐‘ โˆ’ 1 ) ) โ†’ ๐‘˜ โˆˆ โ„•0 )
12 11 4 sylan2 โŠข ( ( ๐ด โˆˆ ๐‘† โˆง ๐‘˜ โˆˆ ( 0 ... ( ๐‘ โˆ’ 1 ) ) ) โ†’ ( ๐ด โˆ’ ๐‘˜ ) โˆˆ ๐‘† )
13 2 a1i โŠข ( ๐ด โˆˆ ๐‘† โ†’ 1 โˆˆ ๐‘† )
14 8 9 10 12 13 fprodcllem โŠข ( ๐ด โˆˆ ๐‘† โ†’ โˆ ๐‘˜ โˆˆ ( 0 ... ( ๐‘ โˆ’ 1 ) ) ( ๐ด โˆ’ ๐‘˜ ) โˆˆ ๐‘† )
15 14 adantr โŠข ( ( ๐ด โˆˆ ๐‘† โˆง ๐‘ โˆˆ โ„•0 ) โ†’ โˆ ๐‘˜ โˆˆ ( 0 ... ( ๐‘ โˆ’ 1 ) ) ( ๐ด โˆ’ ๐‘˜ ) โˆˆ ๐‘† )
16 7 15 eqeltrd โŠข ( ( ๐ด โˆˆ ๐‘† โˆง ๐‘ โˆˆ โ„•0 ) โ†’ ( ๐ด FallFac ๐‘ ) โˆˆ ๐‘† )