Metamath Proof Explorer

Theorem bcm1n

Description: The proportion of one binomial coefficient to another with N decreased by 1. (Contributed by Thierry Arnoux, 9-Nov-2016)

Ref Expression
Assertion bcm1n ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑁 − 1 ) C 𝐾 ) / ( 𝑁 C 𝐾 ) ) = ( ( 𝑁 − 𝐾 ) / 𝑁 ) )

Proof

Step Hyp Ref Expression
1 bcp1n ⊢ ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ( ( 𝑁 − 1 ) + 1 ) C 𝐾 ) = ( ( ( 𝑁 − 1 ) C 𝐾 ) · ( ( ( 𝑁 − 1 ) + 1 ) / ( ( ( 𝑁 − 1 ) + 1 ) − 𝐾 ) ) ) )
2 nnz ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
3 2 zcnd ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
4 3 adantl ⊢ ( ( 𝐾 ∈ ( 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 7 10 eqeq12d ⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( ( ( ( 𝑁 − 1 ) + 1 ) C 𝐾 ) = ( ( ( 𝑁 − 1 ) C 𝐾 ) · ( ( ( 𝑁 − 1 ) + 1 ) / ( ( ( 𝑁 − 1 ) + 1 ) − 𝐾 ) ) ) ↔ ( 𝑁 C 𝐾 ) = ( ( ( 𝑁 − 1 ) C 𝐾 ) · ( 𝑁 / ( 𝑁 − 𝐾 ) ) ) ) )
12 1 11 syl5ib ⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( 𝑁 C 𝐾 ) = ( ( ( 𝑁 − 1 ) C 𝐾 ) · ( 𝑁 / ( 𝑁 − 𝐾 ) ) ) ) )
13 12 3impia ⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑁 C 𝐾 ) = ( ( ( 𝑁 − 1 ) C 𝐾 ) · ( 𝑁 / ( 𝑁 − 𝐾 ) ) ) )
14 13 3anidm13 ⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝑁 C 𝐾 ) = ( ( ( 𝑁 − 1 ) C 𝐾 ) · ( 𝑁 / ( 𝑁 − 𝐾 ) ) ) )
15 elfznn0 ⊢ ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝐾 ∈ ℕ0 )
16 15 adantr ⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → 𝐾 ∈ ℕ0 )
17 simpr ⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℕ )
18 17 nnnn0d ⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℕ0 )
19 elfzelz ⊢ ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝐾 ∈ ℤ )
20 19 adantr ⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → 𝐾 ∈ ℤ )
21 20 zred ⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → 𝐾 ∈ ℝ )
22 2 adantl ⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℤ )
23 22 zred ⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℝ )
24 elfzle2 ⊢ ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝐾 ≤ ( 𝑁 − 1 ) )
25 24 adantr ⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → 𝐾 ≤ ( 𝑁 − 1 ) )
26 zltlem1 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 < 𝑁 ↔ 𝐾 ≤ ( 𝑁 − 1 ) ) )
27 19 2 26 syl2an ⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝐾 < 𝑁 ↔ 𝐾 ≤ ( 𝑁 − 1 ) ) )
28 25 27 mpbird ⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → 𝐾 < 𝑁 )
29 21 23 28 ltled ⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → 𝐾 ≤ 𝑁 )
30 elfz2nn0 ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) ↔ ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝐾 ≤ 𝑁 ) )
31 16 18 29 30 syl3anbrc ⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → 𝐾 ∈ ( 0 ... 𝑁 ) )
32 bcrpcl ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑁 C 𝐾 ) ∈ ℝ+ )
33 31 32 syl ⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝑁 C 𝐾 ) ∈ ℝ+ )
34 33 rpcnd ⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝑁 C 𝐾 ) ∈ ℂ )
35 19 zcnd ⊢ ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝐾 ∈ ℂ )
36 35 adantr ⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → 𝐾 ∈ ℂ )
37 4 36 subcld ⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝑁 − 𝐾 ) ∈ ℂ )
38 36 4 negsubdi2d ⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → - ( 𝐾 − 𝑁 ) = ( 𝑁 − 𝐾 ) )
39 21 23 resubcld ⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝐾 − 𝑁 ) ∈ ℝ )
40 39 recnd ⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝐾 − 𝑁 ) ∈ ℂ )
41 4 addid2d ⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( 0 + 𝑁 ) = 𝑁 )
42 28 41 breqtrrd ⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → 𝐾 < ( 0 + 𝑁 ) )
43 0red ⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → 0 ∈ ℝ )
44 21 23 43 ltsubaddd ⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( ( 𝐾 − 𝑁 ) < 0 ↔ 𝐾 < ( 0 + 𝑁 ) ) )
45 42 44 mpbird ⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝐾 − 𝑁 ) < 0 )
46 45 lt0ne0d ⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝐾 − 𝑁 ) ≠ 0 )
47 40 46 negne0d ⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → - ( 𝐾 − 𝑁 ) ≠ 0 )
48 38 47 eqnetrrd ⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝑁 − 𝐾 ) ≠ 0 )
49 4 37 48 divcld ⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝑁 / ( 𝑁 − 𝐾 ) ) ∈ ℂ )
50 bcrpcl ⊢ ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ( 𝑁 − 1 ) C 𝐾 ) ∈ ℝ+ )
51 50 adantr ⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( ( 𝑁 − 1 ) C 𝐾 ) ∈ ℝ+ )
52 51 rpcnne0d ⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑁 − 1 ) C 𝐾 ) ∈ ℂ ∧ ( ( 𝑁 − 1 ) C 𝐾 ) ≠ 0 ) )
53 divmul2 ⊢ ( ( ( 𝑁 C 𝐾 ) ∈ ℂ ∧ ( 𝑁 / ( 𝑁 − 𝐾 ) ) ∈ ℂ ∧ ( ( ( 𝑁 − 1 ) C 𝐾 ) ∈ ℂ ∧ ( ( 𝑁 − 1 ) C 𝐾 ) ≠ 0 ) ) → ( ( ( 𝑁 C 𝐾 ) / ( ( 𝑁 − 1 ) C 𝐾 ) ) = ( 𝑁 / ( 𝑁 − 𝐾 ) ) ↔ ( 𝑁 C 𝐾 ) = ( ( ( 𝑁 − 1 ) C 𝐾 ) · ( 𝑁 / ( 𝑁 − 𝐾 ) ) ) ) )
54 34 49 52 53 syl3anc ⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑁 C 𝐾 ) / ( ( 𝑁 − 1 ) C 𝐾 ) ) = ( 𝑁 / ( 𝑁 − 𝐾 ) ) ↔ ( 𝑁 C 𝐾 ) = ( ( ( 𝑁 − 1 ) C 𝐾 ) · ( 𝑁 / ( 𝑁 − 𝐾 ) ) ) ) )
55 14 54 mpbird ⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( ( 𝑁 C 𝐾 ) / ( ( 𝑁 − 1 ) C 𝐾 ) ) = ( 𝑁 / ( 𝑁 − 𝐾 ) ) )
56 55 oveq2d ⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( 1 / ( ( 𝑁 C 𝐾 ) / ( ( 𝑁 − 1 ) C 𝐾 ) ) ) = ( 1 / ( 𝑁 / ( 𝑁 − 𝐾 ) ) ) )
57 51 rpcnd ⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( ( 𝑁 − 1 ) C 𝐾 ) ∈ ℂ )
58 bccl2 ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑁 C 𝐾 ) ∈ ℕ )
59 31 58 syl ⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝑁 C 𝐾 ) ∈ ℕ )
60 59 nnne0d ⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝑁 C 𝐾 ) ≠ 0 )
61 bccl2 ⊢ ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ( 𝑁 − 1 ) C 𝐾 ) ∈ ℕ )
62 61 nnne0d ⊢ ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ( 𝑁 − 1 ) C 𝐾 ) ≠ 0 )
63 62 adantr ⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( ( 𝑁 − 1 ) C 𝐾 ) ≠ 0 )
64 34 57 60 63 recdivd ⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( 1 / ( ( 𝑁 C 𝐾 ) / ( ( 𝑁 − 1 ) C 𝐾 ) ) ) = ( ( ( 𝑁 − 1 ) C 𝐾 ) / ( 𝑁 C 𝐾 ) ) )
65 17 nnne0d ⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → 𝑁 ≠ 0 )
66 4 37 65 48 recdivd ⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( 1 / ( 𝑁 / ( 𝑁 − 𝐾 ) ) ) = ( ( 𝑁 − 𝐾 ) / 𝑁 ) )
67 56 64 66 3eqtr3d ⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑁 − 1 ) C 𝐾 ) / ( 𝑁 C 𝐾 ) ) = ( ( 𝑁 − 𝐾 ) / 𝑁 ) )