Metamath Proof Explorer


Theorem bcm1nt

Description: The proportion of one bionmial coefficient to another with N decreased by 1. (Contributed by Scott Fenton, 23-Jun-2020)

Ref Expression
Assertion bcm1nt ( ( ๐‘ โˆˆ โ„• โˆง ๐พ โˆˆ ( 0 ... ( ๐‘ โˆ’ 1 ) ) ) โ†’ ( ๐‘ C ๐พ ) = ( ( ( ๐‘ โˆ’ 1 ) C ๐พ ) ยท ( ๐‘ / ( ๐‘ โˆ’ ๐พ ) ) ) )

Proof

Step Hyp Ref Expression
1 bcp1n โŠข ( ๐พ โˆˆ ( 0 ... ( ๐‘ โˆ’ 1 ) ) โ†’ ( ( ( ๐‘ โˆ’ 1 ) + 1 ) C ๐พ ) = ( ( ( ๐‘ โˆ’ 1 ) C ๐พ ) ยท ( ( ( ๐‘ โˆ’ 1 ) + 1 ) / ( ( ( ๐‘ โˆ’ 1 ) + 1 ) โˆ’ ๐พ ) ) ) )
2 1 adantl โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐พ โˆˆ ( 0 ... ( ๐‘ โˆ’ 1 ) ) ) โ†’ ( ( ( ๐‘ โˆ’ 1 ) + 1 ) C ๐พ ) = ( ( ( ๐‘ โˆ’ 1 ) C ๐พ ) ยท ( ( ( ๐‘ โˆ’ 1 ) + 1 ) / ( ( ( ๐‘ โˆ’ 1 ) + 1 ) โˆ’ ๐พ ) ) ) )
3 simpl โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐พ โˆˆ ( 0 ... ( ๐‘ โˆ’ 1 ) ) ) โ†’ ๐‘ โˆˆ โ„• )
4 3 nncnd โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐พ โˆˆ ( 0 ... ( ๐‘ โˆ’ 1 ) ) ) โ†’ ๐‘ โˆˆ โ„‚ )
5 1cnd โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐พ โˆˆ ( 0 ... ( ๐‘ โˆ’ 1 ) ) ) โ†’ 1 โˆˆ โ„‚ )
6 4 5 npcand โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐พ โˆˆ ( 0 ... ( ๐‘ โˆ’ 1 ) ) ) โ†’ ( ( ๐‘ โˆ’ 1 ) + 1 ) = ๐‘ )
7 6 oveq1d โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐พ โˆˆ ( 0 ... ( ๐‘ โˆ’ 1 ) ) ) โ†’ ( ( ( ๐‘ โˆ’ 1 ) + 1 ) C ๐พ ) = ( ๐‘ C ๐พ ) )
8 6 oveq1d โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐พ โˆˆ ( 0 ... ( ๐‘ โˆ’ 1 ) ) ) โ†’ ( ( ( ๐‘ โˆ’ 1 ) + 1 ) โˆ’ ๐พ ) = ( ๐‘ โˆ’ ๐พ ) )
9 6 8 oveq12d โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐พ โˆˆ ( 0 ... ( ๐‘ โˆ’ 1 ) ) ) โ†’ ( ( ( ๐‘ โˆ’ 1 ) + 1 ) / ( ( ( ๐‘ โˆ’ 1 ) + 1 ) โˆ’ ๐พ ) ) = ( ๐‘ / ( ๐‘ โˆ’ ๐พ ) ) )
10 9 oveq2d โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐พ โˆˆ ( 0 ... ( ๐‘ โˆ’ 1 ) ) ) โ†’ ( ( ( ๐‘ โˆ’ 1 ) C ๐พ ) ยท ( ( ( ๐‘ โˆ’ 1 ) + 1 ) / ( ( ( ๐‘ โˆ’ 1 ) + 1 ) โˆ’ ๐พ ) ) ) = ( ( ( ๐‘ โˆ’ 1 ) C ๐พ ) ยท ( ๐‘ / ( ๐‘ โˆ’ ๐พ ) ) ) )
11 2 7 10 3eqtr3d โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐พ โˆˆ ( 0 ... ( ๐‘ โˆ’ 1 ) ) ) โ†’ ( ๐‘ C ๐พ ) = ( ( ( ๐‘ โˆ’ 1 ) C ๐พ ) ยท ( ๐‘ / ( ๐‘ โˆ’ ๐พ ) ) ) )