Metamath Proof Explorer

Theorem bcp1nk

Description: The proportion of one binomial coefficient to another with N and K increased by 1. (Contributed by Mario Carneiro, 16-Jan-2015)

Ref Expression
Assertion bcp1nk 
|- ( K e. ( 0 ... N ) -> ( ( N + 1 ) _C ( K + 1 ) ) = ( ( N _C K ) x. ( ( N + 1 ) / ( K + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 elfzel1 
 |-  ( K e. ( 0 ... N ) -> 0 e. ZZ )
2 elfzel2 
 |-  ( K e. ( 0 ... N ) -> N e. ZZ )
3 elfzelz 
 |-  ( K e. ( 0 ... N ) -> K e. ZZ )
4 1zzd 
 |-  ( K e. ( 0 ... N ) -> 1 e. ZZ )
5 fzaddel 
 |-  ( ( ( 0 e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ 1 e. ZZ ) ) -> ( K e. ( 0 ... N ) <-> ( K + 1 ) e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) )
6 1 2 3 4 5 syl22anc 
 |-  ( K e. ( 0 ... N ) -> ( K e. ( 0 ... N ) <-> ( K + 1 ) e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) )
7 6 ibi 
 |-  ( K e. ( 0 ... N ) -> ( K + 1 ) e. ( ( 0 + 1 ) ... ( N + 1 ) ) )
8 1e0p1 
 |-  1 = ( 0 + 1 )
9 8 oveq1i 
 |-  ( 1 ... ( N + 1 ) ) = ( ( 0 + 1 ) ... ( N + 1 ) )
10 7 9 eleqtrrdi 
 |-  ( K e. ( 0 ... N ) -> ( K + 1 ) e. ( 1 ... ( N + 1 ) ) )
11 bcm1k 
 |-  ( ( K + 1 ) e. ( 1 ... ( N + 1 ) ) -> ( ( N + 1 ) _C ( K + 1 ) ) = ( ( ( N + 1 ) _C ( ( K + 1 ) - 1 ) ) x. ( ( ( N + 1 ) - ( ( K + 1 ) - 1 ) ) / ( K + 1 ) ) ) )
12 10 11 syl 
 |-  ( K e. ( 0 ... N ) -> ( ( N + 1 ) _C ( K + 1 ) ) = ( ( ( N + 1 ) _C ( ( K + 1 ) - 1 ) ) x. ( ( ( N + 1 ) - ( ( K + 1 ) - 1 ) ) / ( K + 1 ) ) ) )
13 3 zcnd 
 |-  ( K e. ( 0 ... N ) -> K e. CC )
14 ax-1cn 
 |-  1 e. CC
15 pncan 
 |-  ( ( K e. CC /\ 1 e. CC ) -> ( ( K + 1 ) - 1 ) = K )
16 13 14 15 sylancl 
 |-  ( K e. ( 0 ... N ) -> ( ( K + 1 ) - 1 ) = K )
17 16 oveq2d 
 |-  ( K e. ( 0 ... N ) -> ( ( N + 1 ) _C ( ( K + 1 ) - 1 ) ) = ( ( N + 1 ) _C K ) )
18 bcp1n 
 |-  ( K e. ( 0 ... N ) -> ( ( N + 1 ) _C K ) = ( ( N _C K ) x. ( ( N + 1 ) / ( ( N + 1 ) - K ) ) ) )
19 17 18 eqtrd 
 |-  ( K e. ( 0 ... N ) -> ( ( N + 1 ) _C ( ( K + 1 ) - 1 ) ) = ( ( N _C K ) x. ( ( N + 1 ) / ( ( N + 1 ) - K ) ) ) )
20 16 oveq2d 
 |-  ( K e. ( 0 ... N ) -> ( ( N + 1 ) - ( ( K + 1 ) - 1 ) ) = ( ( N + 1 ) - K ) )
21 20 oveq1d 
 |-  ( K e. ( 0 ... N ) -> ( ( ( N + 1 ) - ( ( K + 1 ) - 1 ) ) / ( K + 1 ) ) = ( ( ( N + 1 ) - K ) / ( K + 1 ) ) )
22 19 21 oveq12d 
 |-  ( K e. ( 0 ... N ) -> ( ( ( N + 1 ) _C ( ( K + 1 ) - 1 ) ) x. ( ( ( N + 1 ) - ( ( K + 1 ) - 1 ) ) / ( K + 1 ) ) ) = ( ( ( N _C K ) x. ( ( N + 1 ) / ( ( N + 1 ) - K ) ) ) x. ( ( ( N + 1 ) - K ) / ( K + 1 ) ) ) )
23 bcrpcl 
 |-  ( K e. ( 0 ... N ) -> ( N _C K ) e. RR+ )
24 23 rpcnd 
 |-  ( K e. ( 0 ... N ) -> ( N _C K ) e. CC )
25 2 peano2zd 
 |-  ( K e. ( 0 ... N ) -> ( N + 1 ) e. ZZ )
26 25 zred 
 |-  ( K e. ( 0 ... N ) -> ( N + 1 ) e. RR )
27 3 zred 
 |-  ( K e. ( 0 ... N ) -> K e. RR )
28 2 zred 
 |-  ( K e. ( 0 ... N ) -> N e. RR )
29 elfzle2 
 |-  ( K e. ( 0 ... N ) -> K <_ N )
30 28 ltp1d 
 |-  ( K e. ( 0 ... N ) -> N < ( N + 1 ) )
31 27 28 26 29 30 lelttrd 
 |-  ( K e. ( 0 ... N ) -> K < ( N + 1 ) )
32 znnsub 
 |-  ( ( K e. ZZ /\ ( N + 1 ) e. ZZ ) -> ( K < ( N + 1 ) <-> ( ( N + 1 ) - K ) e. NN ) )
33 3 25 32 syl2anc 
 |-  ( K e. ( 0 ... N ) -> ( K < ( N + 1 ) <-> ( ( N + 1 ) - K ) e. NN ) )
34 31 33 mpbid 
 |-  ( K e. ( 0 ... N ) -> ( ( N + 1 ) - K ) e. NN )
35 26 34 nndivred 
 |-  ( K e. ( 0 ... N ) -> ( ( N + 1 ) / ( ( N + 1 ) - K ) ) e. RR )
36 35 recnd 
 |-  ( K e. ( 0 ... N ) -> ( ( N + 1 ) / ( ( N + 1 ) - K ) ) e. CC )
37 34 nnred 
 |-  ( K e. ( 0 ... N ) -> ( ( N + 1 ) - K ) e. RR )
38 elfznn0 
 |-  ( K e. ( 0 ... N ) -> K e. NN0 )
39 nn0p1nn 
 |-  ( K e. NN0 -> ( K + 1 ) e. NN )
40 38 39 syl 
 |-  ( K e. ( 0 ... N ) -> ( K + 1 ) e. NN )
41 37 40 nndivred 
 |-  ( K e. ( 0 ... N ) -> ( ( ( N + 1 ) - K ) / ( K + 1 ) ) e. RR )
42 41 recnd 
 |-  ( K e. ( 0 ... N ) -> ( ( ( N + 1 ) - K ) / ( K + 1 ) ) e. CC )
43 24 36 42 mulassd 
 |-  ( K e. ( 0 ... N ) -> ( ( ( N _C K ) x. ( ( N + 1 ) / ( ( N + 1 ) - K ) ) ) x. ( ( ( N + 1 ) - K ) / ( K + 1 ) ) ) = ( ( N _C K ) x. ( ( ( N + 1 ) / ( ( N + 1 ) - K ) ) x. ( ( ( N + 1 ) - K ) / ( K + 1 ) ) ) ) )
44 25 zcnd 
 |-  ( K e. ( 0 ... N ) -> ( N + 1 ) e. CC )
45 34 nncnd 
 |-  ( K e. ( 0 ... N ) -> ( ( N + 1 ) - K ) e. CC )
46 40 nncnd 
 |-  ( K e. ( 0 ... N ) -> ( K + 1 ) e. CC )
47 34 nnne0d 
 |-  ( K e. ( 0 ... N ) -> ( ( N + 1 ) - K ) =/= 0 )
48 40 nnne0d 
 |-  ( K e. ( 0 ... N ) -> ( K + 1 ) =/= 0 )
49 44 45 46 47 48 dmdcan2d 
 |-  ( K e. ( 0 ... N ) -> ( ( ( N + 1 ) / ( ( N + 1 ) - K ) ) x. ( ( ( N + 1 ) - K ) / ( K + 1 ) ) ) = ( ( N + 1 ) / ( K + 1 ) ) )
50 49 oveq2d 
 |-  ( K e. ( 0 ... N ) -> ( ( N _C K ) x. ( ( ( N + 1 ) / ( ( N + 1 ) - K ) ) x. ( ( ( N + 1 ) - K ) / ( K + 1 ) ) ) ) = ( ( N _C K ) x. ( ( N + 1 ) / ( K + 1 ) ) ) )
51 43 50 eqtrd 
 |-  ( K e. ( 0 ... N ) -> ( ( ( N _C K ) x. ( ( N + 1 ) / ( ( N + 1 ) - K ) ) ) x. ( ( ( N + 1 ) - K ) / ( K + 1 ) ) ) = ( ( N _C K ) x. ( ( N + 1 ) / ( K + 1 ) ) ) )
52 22 51 eqtrd 
 |-  ( K e. ( 0 ... N ) -> ( ( ( N + 1 ) _C ( ( K + 1 ) - 1 ) ) x. ( ( ( N + 1 ) - ( ( K + 1 ) - 1 ) ) / ( K + 1 ) ) ) = ( ( N _C K ) x. ( ( N + 1 ) / ( K + 1 ) ) ) )
53 12 52 eqtrd 
 |-  ( K e. ( 0 ... N ) -> ( ( N + 1 ) _C ( K + 1 ) ) = ( ( N _C K ) x. ( ( N + 1 ) / ( K + 1 ) ) ) )