Metamath Proof Explorer


Theorem bcval2

Description: Value of the binomial coefficient, N choose K , in its standard domain. (Contributed by NM, 9-Jun-2005) (Revised by Mario Carneiro, 7-Nov-2013)

Ref Expression
Assertion bcval2 ( ๐พ โˆˆ ( 0 ... ๐‘ ) โ†’ ( ๐‘ C ๐พ ) = ( ( ! โ€˜ ๐‘ ) / ( ( ! โ€˜ ( ๐‘ โˆ’ ๐พ ) ) ยท ( ! โ€˜ ๐พ ) ) ) )

Proof

Step Hyp Ref Expression
1 elfz3nn0 โŠข ( ๐พ โˆˆ ( 0 ... ๐‘ ) โ†’ ๐‘ โˆˆ โ„•0 )
2 elfzelz โŠข ( ๐พ โˆˆ ( 0 ... ๐‘ ) โ†’ ๐พ โˆˆ โ„ค )
3 bcval โŠข ( ( ๐‘ โˆˆ โ„•0 โˆง ๐พ โˆˆ โ„ค ) โ†’ ( ๐‘ C ๐พ ) = if ( ๐พ โˆˆ ( 0 ... ๐‘ ) , ( ( ! โ€˜ ๐‘ ) / ( ( ! โ€˜ ( ๐‘ โˆ’ ๐พ ) ) ยท ( ! โ€˜ ๐พ ) ) ) , 0 ) )
4 1 2 3 syl2anc โŠข ( ๐พ โˆˆ ( 0 ... ๐‘ ) โ†’ ( ๐‘ C ๐พ ) = if ( ๐พ โˆˆ ( 0 ... ๐‘ ) , ( ( ! โ€˜ ๐‘ ) / ( ( ! โ€˜ ( ๐‘ โˆ’ ๐พ ) ) ยท ( ! โ€˜ ๐พ ) ) ) , 0 ) )
5 iftrue โŠข ( ๐พ โˆˆ ( 0 ... ๐‘ ) โ†’ if ( ๐พ โˆˆ ( 0 ... ๐‘ ) , ( ( ! โ€˜ ๐‘ ) / ( ( ! โ€˜ ( ๐‘ โˆ’ ๐พ ) ) ยท ( ! โ€˜ ๐พ ) ) ) , 0 ) = ( ( ! โ€˜ ๐‘ ) / ( ( ! โ€˜ ( ๐‘ โˆ’ ๐พ ) ) ยท ( ! โ€˜ ๐พ ) ) ) )
6 4 5 eqtrd โŠข ( ๐พ โˆˆ ( 0 ... ๐‘ ) โ†’ ( ๐‘ C ๐พ ) = ( ( ! โ€˜ ๐‘ ) / ( ( ! โ€˜ ( ๐‘ โˆ’ ๐พ ) ) ยท ( ! โ€˜ ๐พ ) ) ) )