Metamath Proof Explorer


Theorem fallfaccl

Description: Closure law for falling factorial. (Contributed by Scott Fenton, 5-Jan-2018)

Ref Expression
Assertion fallfaccl ( ( ๐ด โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„•0 ) โ†’ ( ๐ด FallFac ๐‘ ) โˆˆ โ„‚ )

Proof

Step Hyp Ref Expression
1 ssid โŠข โ„‚ โŠ† โ„‚
2 ax-1cn โŠข 1 โˆˆ โ„‚
3 mulcl โŠข ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚ ) โ†’ ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ โ„‚ )
4 nn0cn โŠข ( ๐‘˜ โˆˆ โ„•0 โ†’ ๐‘˜ โˆˆ โ„‚ )
5 subcl โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐‘˜ โˆˆ โ„‚ ) โ†’ ( ๐ด โˆ’ ๐‘˜ ) โˆˆ โ„‚ )
6 4 5 sylan2 โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ( ๐ด โˆ’ ๐‘˜ ) โˆˆ โ„‚ )
7 1 2 3 6 fallfaccllem โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„•0 ) โ†’ ( ๐ด FallFac ๐‘ ) โˆˆ โ„‚ )