This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bcm1k

Description: The proportion of one binomial coefficient to another with K decreased by 1. (Contributed by Mario Carneiro, 10-Mar-2014)

Ref Expression
Assertion bcm1k ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( 𝑁 C 𝐾 ) = ( ( 𝑁 C ( 𝐾 − 1 ) ) · ( ( 𝑁 − ( 𝐾 − 1 ) ) / 𝐾 ) ) )

Proof

Step Hyp Ref Expression
1 elfzuz2 ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
2 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
3 1 2 eleqtrrdi ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → 𝑁 ∈ ℕ )
4 3 nnnn0d ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → 𝑁 ∈ ℕ0 )
5 4 faccld ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ! ‘ 𝑁 ) ∈ ℕ )
6 5 nncnd ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ! ‘ 𝑁 ) ∈ ℂ )
7 fznn0sub ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( 𝑁 − 𝐾 ) ∈ ℕ0 )
8 nn0p1nn ⊢ ( ( 𝑁 − 𝐾 ) ∈ ℕ0 → ( ( 𝑁 − 𝐾 ) + 1 ) ∈ ℕ )
9 7 8 syl ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( 𝑁 − 𝐾 ) + 1 ) ∈ ℕ )
10 9 nncnd ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( 𝑁 − 𝐾 ) + 1 ) ∈ ℂ )
11 9 nnnn0d ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( 𝑁 − 𝐾 ) + 1 ) ∈ ℕ0 )
12 11 faccld ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) ∈ ℕ )
13 elfznn ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → 𝐾 ∈ ℕ )
14 nnm1nn0 ⊢ ( 𝐾 ∈ ℕ → ( 𝐾 − 1 ) ∈ ℕ0 )
15 faccl ⊢ ( ( 𝐾 − 1 ) ∈ ℕ0 → ( ! ‘ ( 𝐾 − 1 ) ) ∈ ℕ )
16 13 14 15 3syl ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ! ‘ ( 𝐾 − 1 ) ) ∈ ℕ )
17 12 16 nnmulcld ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) ∈ ℕ )
18 nncn ⊢ ( ( ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) ∈ ℕ → ( ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) ∈ ℂ )
19 nnne0 ⊢ ( ( ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) ∈ ℕ → ( ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) ≠ 0 )
20 18 19 jca ⊢ ( ( ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) ∈ ℕ → ( ( ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) ∈ ℂ ∧ ( ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) ≠ 0 ) )
21 17 20 syl ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) ∈ ℂ ∧ ( ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) ≠ 0 ) )
22 13 nncnd ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → 𝐾 ∈ ℂ )
23 13 nnne0d ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → 𝐾 ≠ 0 )
24 22 23 jca ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( 𝐾 ∈ ℂ ∧ 𝐾 ≠ 0 ) )
25 divmuldiv ⊢ ( ( ( ( ! ‘ 𝑁 ) ∈ ℂ ∧ ( ( 𝑁 − 𝐾 ) + 1 ) ∈ ℂ ) ∧ ( ( ( ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) ∈ ℂ ∧ ( ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) ≠ 0 ) ∧ ( 𝐾 ∈ ℂ ∧ 𝐾 ≠ 0 ) ) ) → ( ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) ) · ( ( ( 𝑁 − 𝐾 ) + 1 ) / 𝐾 ) ) = ( ( ( ! ‘ 𝑁 ) · ( ( 𝑁 − 𝐾 ) + 1 ) ) / ( ( ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) · 𝐾 ) ) )
26 6 10 21 24 25 syl22anc ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) ) · ( ( ( 𝑁 − 𝐾 ) + 1 ) / 𝐾 ) ) = ( ( ( ! ‘ 𝑁 ) · ( ( 𝑁 − 𝐾 ) + 1 ) ) / ( ( ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) · 𝐾 ) ) )
27 elfzel2 ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → 𝑁 ∈ ℤ )
28 27 zcnd ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → 𝑁 ∈ ℂ )
29 1cnd ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → 1 ∈ ℂ )
30 28 22 29 subsubd ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( 𝑁 − ( 𝐾 − 1 ) ) = ( ( 𝑁 − 𝐾 ) + 1 ) )
31 30 fveq2d ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ! ‘ ( 𝑁 − ( 𝐾 − 1 ) ) ) = ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) )
32 31 oveq1d ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ! ‘ ( 𝑁 − ( 𝐾 − 1 ) ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) = ( ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) )
33 32 oveq2d ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − ( 𝐾 − 1 ) ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) ) = ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) ) )
34 30 oveq1d ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( 𝑁 − ( 𝐾 − 1 ) ) / 𝐾 ) = ( ( ( 𝑁 − 𝐾 ) + 1 ) / 𝐾 ) )
35 33 34 oveq12d ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − ( 𝐾 − 1 ) ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) ) · ( ( 𝑁 − ( 𝐾 − 1 ) ) / 𝐾 ) ) = ( ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) ) · ( ( ( 𝑁 − 𝐾 ) + 1 ) / 𝐾 ) ) )
36 facp1 ⊢ ( ( 𝑁 − 𝐾 ) ∈ ℕ0 → ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) = ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ( 𝑁 − 𝐾 ) + 1 ) ) )
37 7 36 syl ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) = ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ( 𝑁 − 𝐾 ) + 1 ) ) )
38 37 eqcomd ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ( 𝑁 − 𝐾 ) + 1 ) ) = ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) )
39 facnn2 ⊢ ( 𝐾 ∈ ℕ → ( ! ‘ 𝐾 ) = ( ( ! ‘ ( 𝐾 − 1 ) ) · 𝐾 ) )
40 13 39 syl ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ! ‘ 𝐾 ) = ( ( ! ‘ ( 𝐾 − 1 ) ) · 𝐾 ) )
41 38 40 oveq12d ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ! ‘ 𝐾 ) ) = ( ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ( ! ‘ ( 𝐾 − 1 ) ) · 𝐾 ) ) )
42 7 faccld ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ! ‘ ( 𝑁 − 𝐾 ) ) ∈ ℕ )
43 42 nncnd ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ! ‘ ( 𝑁 − 𝐾 ) ) ∈ ℂ )
44 13 nnnn0d ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → 𝐾 ∈ ℕ0 )
45 44 faccld ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ! ‘ 𝐾 ) ∈ ℕ )
46 45 nncnd ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ! ‘ 𝐾 ) ∈ ℂ )
47 43 46 10 mul32d ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) · ( ( 𝑁 − 𝐾 ) + 1 ) ) = ( ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ! ‘ 𝐾 ) ) )
48 12 nncnd ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) ∈ ℂ )
49 16 nncnd ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ! ‘ ( 𝐾 − 1 ) ) ∈ ℂ )
50 48 49 22 mulassd ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) · 𝐾 ) = ( ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ( ! ‘ ( 𝐾 − 1 ) ) · 𝐾 ) ) )
51 41 47 50 3eqtr4d ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) · ( ( 𝑁 − 𝐾 ) + 1 ) ) = ( ( ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) · 𝐾 ) )
52 51 oveq2d ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ( ! ‘ 𝑁 ) · ( ( 𝑁 − 𝐾 ) + 1 ) ) / ( ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) · ( ( 𝑁 − 𝐾 ) + 1 ) ) ) = ( ( ( ! ‘ 𝑁 ) · ( ( 𝑁 − 𝐾 ) + 1 ) ) / ( ( ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) · 𝐾 ) ) )
53 26 35 52 3eqtr4d ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − ( 𝐾 − 1 ) ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) ) · ( ( 𝑁 − ( 𝐾 − 1 ) ) / 𝐾 ) ) = ( ( ( ! ‘ 𝑁 ) · ( ( 𝑁 − 𝐾 ) + 1 ) ) / ( ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) · ( ( 𝑁 − 𝐾 ) + 1 ) ) ) )
54 6 10 mulcomd ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ! ‘ 𝑁 ) · ( ( 𝑁 − 𝐾 ) + 1 ) ) = ( ( ( 𝑁 − 𝐾 ) + 1 ) · ( ! ‘ 𝑁 ) ) )
55 42 45 nnmulcld ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ∈ ℕ )
56 55 nncnd ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ∈ ℂ )
57 56 10 mulcomd ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) · ( ( 𝑁 − 𝐾 ) + 1 ) ) = ( ( ( 𝑁 − 𝐾 ) + 1 ) · ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) )
58 54 57 oveq12d ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ( ! ‘ 𝑁 ) · ( ( 𝑁 − 𝐾 ) + 1 ) ) / ( ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) · ( ( 𝑁 − 𝐾 ) + 1 ) ) ) = ( ( ( ( 𝑁 − 𝐾 ) + 1 ) · ( ! ‘ 𝑁 ) ) / ( ( ( 𝑁 − 𝐾 ) + 1 ) · ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) ) )
59 55 nnne0d ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ≠ 0 )
60 9 nnne0d ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( 𝑁 − 𝐾 ) + 1 ) ≠ 0 )
61 6 56 10 59 60 divcan5d ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ( ( 𝑁 − 𝐾 ) + 1 ) · ( ! ‘ 𝑁 ) ) / ( ( ( 𝑁 − 𝐾 ) + 1 ) · ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) ) = ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) )
62 53 58 61 3eqtrrd ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) = ( ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − ( 𝐾 − 1 ) ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) ) · ( ( 𝑁 − ( 𝐾 − 1 ) ) / 𝐾 ) ) )
63 fz1ssfz0 ⊢ ( 1 ... 𝑁 ) ⊆ ( 0 ... 𝑁 )
64 63 sseli ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → 𝐾 ∈ ( 0 ... 𝑁 ) )
65 bcval2 ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑁 C 𝐾 ) = ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) )
66 64 65 syl ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( 𝑁 C 𝐾 ) = ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) )
67 ax-1cn ⊢ 1 ∈ ℂ
68 npcan ⊢ ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
69 28 67 68 sylancl ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
70 peano2zm ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 − 1 ) ∈ ℤ )
71 uzid ⊢ ( ( 𝑁 − 1 ) ∈ ℤ → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) )
72 peano2uz ⊢ ( ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) )
73 27 70 71 72 4syl ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) )
74 69 73 eqeltrrd ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) )
75 fzss2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) → ( 0 ... ( 𝑁 − 1 ) ) ⊆ ( 0 ... 𝑁 ) )
76 74 75 syl ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( 0 ... ( 𝑁 − 1 ) ) ⊆ ( 0 ... 𝑁 ) )
77 elfzmlbm ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( 𝐾 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) )
78 76 77 sseldd ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( 𝐾 − 1 ) ∈ ( 0 ... 𝑁 ) )
79 bcval2 ⊢ ( ( 𝐾 − 1 ) ∈ ( 0 ... 𝑁 ) → ( 𝑁 C ( 𝐾 − 1 ) ) = ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − ( 𝐾 − 1 ) ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) ) )
80 78 79 syl ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( 𝑁 C ( 𝐾 − 1 ) ) = ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − ( 𝐾 − 1 ) ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) ) )
81 80 oveq1d ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( 𝑁 C ( 𝐾 − 1 ) ) · ( ( 𝑁 − ( 𝐾 − 1 ) ) / 𝐾 ) ) = ( ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − ( 𝐾 − 1 ) ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) ) · ( ( 𝑁 − ( 𝐾 − 1 ) ) / 𝐾 ) ) )
82 62 66 81 3eqtr4d ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( 𝑁 C 𝐾 ) = ( ( 𝑁 C ( 𝐾 − 1 ) ) · ( ( 𝑁 − ( 𝐾 − 1 ) ) / 𝐾 ) ) )