Metamath Proof Explorer

Theorem bcval5

Description: Write out the top and bottom parts of the binomial coefficient ( N _C K ) = ( N x. ( N - 1 ) x. ... x. ( ( N - K ) + 1 ) ) / K ! explicitly. In this form, it is valid even for N < K , although it is no longer valid for nonpositive K . (Contributed by Mario Carneiro, 22-May-2014)

Ref Expression
Assertion bcval5 ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) → ( 𝑁 C 𝐾 ) = ( ( seq ( ( 𝑁 − 𝐾 ) + 1 ) ( · , I ) ‘ 𝑁 ) / ( ! ‘ 𝐾 ) ) )

Proof

Step Hyp Ref Expression
1 bcval2 ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑁 C 𝐾 ) = ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) )
2 1 adantl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C 𝐾 ) = ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) )
3 mulcl ⊢ ( ( 𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 𝑘 · 𝑥 ) ∈ ℂ )
4 3 adantl ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑁 − 𝐾 ) ∈ ℕ ) ) ∧ ( 𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( 𝑘 · 𝑥 ) ∈ ℂ )
5 mulass ⊢ ( ( 𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( 𝑘 · 𝑥 ) · 𝑦 ) = ( 𝑘 · ( 𝑥 · 𝑦 ) ) )
6 5 adantl ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑁 − 𝐾 ) ∈ ℕ ) ) ∧ ( 𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → ( ( 𝑘 · 𝑥 ) · 𝑦 ) = ( 𝑘 · ( 𝑥 · 𝑦 ) ) )
7 simplr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → 𝐾 ∈ ℕ )
8 elfzuz3 ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) )
9 8 adantl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) )
10 eluznn ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝑁 ∈ ℕ )
11 7 9 10 syl2anc ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → 𝑁 ∈ ℕ )
12 11 adantrr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑁 − 𝐾 ) ∈ ℕ ) ) → 𝑁 ∈ ℕ )
13 simplr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑁 − 𝐾 ) ∈ ℕ ) ) → 𝐾 ∈ ℕ )
14 nnre ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
15 nnrp ⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ℝ+ )
16 ltsubrp ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝐾 ∈ ℝ+ ) → ( 𝑁 − 𝐾 ) < 𝑁 )
17 14 15 16 syl2an ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℕ ) → ( 𝑁 − 𝐾 ) < 𝑁 )
18 12 13 17 syl2anc ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑁 − 𝐾 ) ∈ ℕ ) ) → ( 𝑁 − 𝐾 ) < 𝑁 )
19 12 nnzd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑁 − 𝐾 ) ∈ ℕ ) ) → 𝑁 ∈ ℤ )
20 nnz ⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ℤ )
21 20 ad2antlr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑁 − 𝐾 ) ∈ ℕ ) ) → 𝐾 ∈ ℤ )
22 19 21 zsubcld ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑁 − 𝐾 ) ∈ ℕ ) ) → ( 𝑁 − 𝐾 ) ∈ ℤ )
23 zltp1le ⊢ ( ( ( 𝑁 − 𝐾 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑁 − 𝐾 ) < 𝑁 ↔ ( ( 𝑁 − 𝐾 ) + 1 ) ≤ 𝑁 ) )
24 22 19 23 syl2anc ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑁 − 𝐾 ) ∈ ℕ ) ) → ( ( 𝑁 − 𝐾 ) < 𝑁 ↔ ( ( 𝑁 − 𝐾 ) + 1 ) ≤ 𝑁 ) )
25 18 24 mpbid ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑁 − 𝐾 ) ∈ ℕ ) ) → ( ( 𝑁 − 𝐾 ) + 1 ) ≤ 𝑁 )
26 22 peano2zd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑁 − 𝐾 ) ∈ ℕ ) ) → ( ( 𝑁 − 𝐾 ) + 1 ) ∈ ℤ )
27 eluz ⊢ ( ( ( ( 𝑁 − 𝐾 ) + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ∈ ( ℤ≥ ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) ↔ ( ( 𝑁 − 𝐾 ) + 1 ) ≤ 𝑁 ) )
28 26 19 27 syl2anc ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑁 − 𝐾 ) ∈ ℕ ) ) → ( 𝑁 ∈ ( ℤ≥ ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) ↔ ( ( 𝑁 − 𝐾 ) + 1 ) ≤ 𝑁 ) )
29 25 28 mpbird ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑁 − 𝐾 ) ∈ ℕ ) ) → 𝑁 ∈ ( ℤ≥ ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) )
30 simprr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑁 − 𝐾 ) ∈ ℕ ) ) → ( 𝑁 − 𝐾 ) ∈ ℕ )
31 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
32 30 31 eleqtrdi ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑁 − 𝐾 ) ∈ ℕ ) ) → ( 𝑁 − 𝐾 ) ∈ ( ℤ≥ ‘ 1 ) )
33 fvi ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → ( I ‘ 𝑘 ) = 𝑘 )
34 elfzelz ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → 𝑘 ∈ ℤ )
35 34 zcnd ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → 𝑘 ∈ ℂ )
36 33 35 eqeltrd ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → ( I ‘ 𝑘 ) ∈ ℂ )
37 36 adantl ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑁 − 𝐾 ) ∈ ℕ ) ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( I ‘ 𝑘 ) ∈ ℂ )
38 4 6 29 32 37 seqsplit ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑁 − 𝐾 ) ∈ ℕ ) ) → ( seq 1 ( · , I ) ‘ 𝑁 ) = ( ( seq 1 ( · , I ) ‘ ( 𝑁 − 𝐾 ) ) · ( seq ( ( 𝑁 − 𝐾 ) + 1 ) ( · , I ) ‘ 𝑁 ) ) )
39 facnn ⊢ ( 𝑁 ∈ ℕ → ( ! ‘ 𝑁 ) = ( seq 1 ( · , I ) ‘ 𝑁 ) )
40 12 39 syl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑁 − 𝐾 ) ∈ ℕ ) ) → ( ! ‘ 𝑁 ) = ( seq 1 ( · , I ) ‘ 𝑁 ) )
41 facnn ⊢ ( ( 𝑁 − 𝐾 ) ∈ ℕ → ( ! ‘ ( 𝑁 − 𝐾 ) ) = ( seq 1 ( · , I ) ‘ ( 𝑁 − 𝐾 ) ) )
42 30 41 syl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑁 − 𝐾 ) ∈ ℕ ) ) → ( ! ‘ ( 𝑁 − 𝐾 ) ) = ( seq 1 ( · , I ) ‘ ( 𝑁 − 𝐾 ) ) )
43 42 oveq1d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑁 − 𝐾 ) ∈ ℕ ) ) → ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( seq ( ( 𝑁 − 𝐾 ) + 1 ) ( · , I ) ‘ 𝑁 ) ) = ( ( seq 1 ( · , I ) ‘ ( 𝑁 − 𝐾 ) ) · ( seq ( ( 𝑁 − 𝐾 ) + 1 ) ( · , I ) ‘ 𝑁 ) ) )
44 38 40 43 3eqtr4d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ( 𝐾 ∈ ( 0 ... 𝑁 ) ∧ ( 𝑁 − 𝐾 ) ∈ ℕ ) ) → ( ! ‘ 𝑁 ) = ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( seq ( ( 𝑁 − 𝐾 ) + 1 ) ( · , I ) ‘ 𝑁 ) ) )
45 44 expr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 − 𝐾 ) ∈ ℕ → ( ! ‘ 𝑁 ) = ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( seq ( ( 𝑁 − 𝐾 ) + 1 ) ( · , I ) ‘ 𝑁 ) ) ) )
46 simpll ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → 𝑁 ∈ ℕ0 )
47 faccl ⊢ ( 𝑁 ∈ ℕ0 → ( ! ‘ 𝑁 ) ∈ ℕ )
48 nncn ⊢ ( ( ! ‘ 𝑁 ) ∈ ℕ → ( ! ‘ 𝑁 ) ∈ ℂ )
49 46 47 48 3syl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ! ‘ 𝑁 ) ∈ ℂ )
50 49 mulid2d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 1 · ( ! ‘ 𝑁 ) ) = ( ! ‘ 𝑁 ) )
51 11 39 syl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ! ‘ 𝑁 ) = ( seq 1 ( · , I ) ‘ 𝑁 ) )
52 51 oveq2d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 1 · ( ! ‘ 𝑁 ) ) = ( 1 · ( seq 1 ( · , I ) ‘ 𝑁 ) ) )
53 50 52 eqtr3d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ! ‘ 𝑁 ) = ( 1 · ( seq 1 ( · , I ) ‘ 𝑁 ) ) )
54 fveq2 ⊢ ( ( 𝑁 − 𝐾 ) = 0 → ( ! ‘ ( 𝑁 − 𝐾 ) ) = ( ! ‘ 0 ) )
55 fac0 ⊢ ( ! ‘ 0 ) = 1
56 54 55 eqtrdi ⊢ ( ( 𝑁 − 𝐾 ) = 0 → ( ! ‘ ( 𝑁 − 𝐾 ) ) = 1 )
57 oveq1 ⊢ ( ( 𝑁 − 𝐾 ) = 0 → ( ( 𝑁 − 𝐾 ) + 1 ) = ( 0 + 1 ) )
58 0p1e1 ⊢ ( 0 + 1 ) = 1
59 57 58 eqtrdi ⊢ ( ( 𝑁 − 𝐾 ) = 0 → ( ( 𝑁 − 𝐾 ) + 1 ) = 1 )
60 59 seqeq1d ⊢ ( ( 𝑁 − 𝐾 ) = 0 → seq ( ( 𝑁 − 𝐾 ) + 1 ) ( · , I ) = seq 1 ( · , I ) )
61 60 fveq1d ⊢ ( ( 𝑁 − 𝐾 ) = 0 → ( seq ( ( 𝑁 − 𝐾 ) + 1 ) ( · , I ) ‘ 𝑁 ) = ( seq 1 ( · , I ) ‘ 𝑁 ) )
62 56 61 oveq12d ⊢ ( ( 𝑁 − 𝐾 ) = 0 → ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( seq ( ( 𝑁 − 𝐾 ) + 1 ) ( · , I ) ‘ 𝑁 ) ) = ( 1 · ( seq 1 ( · , I ) ‘ 𝑁 ) ) )
63 62 eqeq2d ⊢ ( ( 𝑁 − 𝐾 ) = 0 → ( ( ! ‘ 𝑁 ) = ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( seq ( ( 𝑁 − 𝐾 ) + 1 ) ( · , I ) ‘ 𝑁 ) ) ↔ ( ! ‘ 𝑁 ) = ( 1 · ( seq 1 ( · , I ) ‘ 𝑁 ) ) ) )
64 53 63 syl5ibrcom ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 − 𝐾 ) = 0 → ( ! ‘ 𝑁 ) = ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( seq ( ( 𝑁 − 𝐾 ) + 1 ) ( · , I ) ‘ 𝑁 ) ) ) )
65 fznn0sub ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑁 − 𝐾 ) ∈ ℕ0 )
66 65 adantl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 − 𝐾 ) ∈ ℕ0 )
67 elnn0 ⊢ ( ( 𝑁 − 𝐾 ) ∈ ℕ0 ↔ ( ( 𝑁 − 𝐾 ) ∈ ℕ ∨ ( 𝑁 − 𝐾 ) = 0 ) )
68 66 67 sylib ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 − 𝐾 ) ∈ ℕ ∨ ( 𝑁 − 𝐾 ) = 0 ) )
69 45 64 68 mpjaod ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ! ‘ 𝑁 ) = ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( seq ( ( 𝑁 − 𝐾 ) + 1 ) ( · , I ) ‘ 𝑁 ) ) )
70 69 oveq1d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) = ( ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( seq ( ( 𝑁 − 𝐾 ) + 1 ) ( · , I ) ‘ 𝑁 ) ) / ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) )
71 eqid ⊢ ( ℤ≥ ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) = ( ℤ≥ ‘ ( ( 𝑁 − 𝐾 ) + 1 ) )
72 nn0z ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
73 zsubcl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑁 − 𝐾 ) ∈ ℤ )
74 72 20 73 syl2an ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) → ( 𝑁 − 𝐾 ) ∈ ℤ )
75 74 peano2zd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) → ( ( 𝑁 − 𝐾 ) + 1 ) ∈ ℤ )
76 75 adantr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 − 𝐾 ) + 1 ) ∈ ℤ )
77 fvi ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) → ( I ‘ 𝑘 ) = 𝑘 )
78 eluzelcn ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) → 𝑘 ∈ ℂ )
79 77 78 eqeltrd ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) → ( I ‘ 𝑘 ) ∈ ℂ )
80 79 adantl ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) ) → ( I ‘ 𝑘 ) ∈ ℂ )
81 3 adantl ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( 𝑘 · 𝑥 ) ∈ ℂ )
82 71 76 80 81 seqf ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → seq ( ( 𝑁 − 𝐾 ) + 1 ) ( · , I ) : ( ℤ≥ ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) ⟶ ℂ )
83 11 7 17 syl2anc ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 − 𝐾 ) < 𝑁 )
84 74 adantr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 − 𝐾 ) ∈ ℤ )
85 11 nnzd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → 𝑁 ∈ ℤ )
86 84 85 23 syl2anc ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 − 𝐾 ) < 𝑁 ↔ ( ( 𝑁 − 𝐾 ) + 1 ) ≤ 𝑁 ) )
87 83 86 mpbid ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 − 𝐾 ) + 1 ) ≤ 𝑁 )
88 76 85 27 syl2anc ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 ∈ ( ℤ≥ ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) ↔ ( ( 𝑁 − 𝐾 ) + 1 ) ≤ 𝑁 ) )
89 87 88 mpbird ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → 𝑁 ∈ ( ℤ≥ ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) )
90 82 89 ffvelrnd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( seq ( ( 𝑁 − 𝐾 ) + 1 ) ( · , I ) ‘ 𝑁 ) ∈ ℂ )
91 elfznn0 ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝐾 ∈ ℕ0 )
92 91 adantl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → 𝐾 ∈ ℕ0 )
93 92 faccld ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ! ‘ 𝐾 ) ∈ ℕ )
94 93 nncnd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ! ‘ 𝐾 ) ∈ ℂ )
95 66 faccld ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ! ‘ ( 𝑁 − 𝐾 ) ) ∈ ℕ )
96 95 nncnd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ! ‘ ( 𝑁 − 𝐾 ) ) ∈ ℂ )
97 93 nnne0d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ! ‘ 𝐾 ) ≠ 0 )
98 95 nnne0d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ! ‘ ( 𝑁 − 𝐾 ) ) ≠ 0 )
99 90 94 96 97 98 divcan5d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( seq ( ( 𝑁 − 𝐾 ) + 1 ) ( · , I ) ‘ 𝑁 ) ) / ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) = ( ( seq ( ( 𝑁 − 𝐾 ) + 1 ) ( · , I ) ‘ 𝑁 ) / ( ! ‘ 𝐾 ) ) )
100 2 70 99 3eqtrd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C 𝐾 ) = ( ( seq ( ( 𝑁 − 𝐾 ) + 1 ) ( · , I ) ‘ 𝑁 ) / ( ! ‘ 𝐾 ) ) )
101 nnnn0 ⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ℕ0 )
102 101 ad2antlr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → 𝐾 ∈ ℕ0 )
103 faccl ⊢ ( 𝐾 ∈ ℕ0 → ( ! ‘ 𝐾 ) ∈ ℕ )
104 nncn ⊢ ( ( ! ‘ 𝐾 ) ∈ ℕ → ( ! ‘ 𝐾 ) ∈ ℂ )
105 nnne0 ⊢ ( ( ! ‘ 𝐾 ) ∈ ℕ → ( ! ‘ 𝐾 ) ≠ 0 )
106 104 105 div0d ⊢ ( ( ! ‘ 𝐾 ) ∈ ℕ → ( 0 / ( ! ‘ 𝐾 ) ) = 0 )
107 102 103 106 3syl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 0 / ( ! ‘ 𝐾 ) ) = 0 )
108 3 adantl ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( 𝑘 · 𝑥 ) ∈ ℂ )
109 fvi ⊢ ( 𝑘 ∈ ( ( ( 𝑁 − 𝐾 ) + 1 ) ... 𝑁 ) → ( I ‘ 𝑘 ) = 𝑘 )
110 elfzelz ⊢ ( 𝑘 ∈ ( ( ( 𝑁 − 𝐾 ) + 1 ) ... 𝑁 ) → 𝑘 ∈ ℤ )
111 110 zcnd ⊢ ( 𝑘 ∈ ( ( ( 𝑁 − 𝐾 ) + 1 ) ... 𝑁 ) → 𝑘 ∈ ℂ )
112 109 111 eqeltrd ⊢ ( 𝑘 ∈ ( ( ( 𝑁 − 𝐾 ) + 1 ) ... 𝑁 ) → ( I ‘ 𝑘 ) ∈ ℂ )
113 112 adantl ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 ∈ ( ( ( 𝑁 − 𝐾 ) + 1 ) ... 𝑁 ) ) → ( I ‘ 𝑘 ) ∈ ℂ )
114 mul02 ⊢ ( 𝑘 ∈ ℂ → ( 0 · 𝑘 ) = 0 )
115 114 adantl ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 ∈ ℂ ) → ( 0 · 𝑘 ) = 0 )
116 mul01 ⊢ ( 𝑘 ∈ ℂ → ( 𝑘 · 0 ) = 0 )
117 116 adantl ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 ∈ ℂ ) → ( 𝑘 · 0 ) = 0 )
118 simpr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ¬ 𝐾 ∈ ( 0 ... 𝑁 ) )
119 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
120 102 119 eleqtrdi ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → 𝐾 ∈ ( ℤ≥ ‘ 0 ) )
121 72 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → 𝑁 ∈ ℤ )
122 elfz5 ⊢ ( ( 𝐾 ∈ ( ℤ≥ ‘ 0 ) ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∈ ( 0 ... 𝑁 ) ↔ 𝐾 ≤ 𝑁 ) )
123 120 121 122 syl2anc ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝐾 ∈ ( 0 ... 𝑁 ) ↔ 𝐾 ≤ 𝑁 ) )
124 nn0re ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
125 124 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → 𝑁 ∈ ℝ )
126 nnre ⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ℝ )
127 126 ad2antlr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → 𝐾 ∈ ℝ )
128 125 127 subge0d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 0 ≤ ( 𝑁 − 𝐾 ) ↔ 𝐾 ≤ 𝑁 ) )
129 123 128 bitr4d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝐾 ∈ ( 0 ... 𝑁 ) ↔ 0 ≤ ( 𝑁 − 𝐾 ) ) )
130 118 129 mtbid ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ¬ 0 ≤ ( 𝑁 − 𝐾 ) )
131 74 adantr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 − 𝐾 ) ∈ ℤ )
132 131 zred ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 − 𝐾 ) ∈ ℝ )
133 0re ⊢ 0 ∈ ℝ
134 ltnle ⊢ ( ( ( 𝑁 − 𝐾 ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( 𝑁 − 𝐾 ) < 0 ↔ ¬ 0 ≤ ( 𝑁 − 𝐾 ) ) )
135 132 133 134 sylancl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 − 𝐾 ) < 0 ↔ ¬ 0 ≤ ( 𝑁 − 𝐾 ) ) )
136 130 135 mpbird ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 − 𝐾 ) < 0 )
137 0z ⊢ 0 ∈ ℤ
138 zltp1le ⊢ ( ( ( 𝑁 − 𝐾 ) ∈ ℤ ∧ 0 ∈ ℤ ) → ( ( 𝑁 − 𝐾 ) < 0 ↔ ( ( 𝑁 − 𝐾 ) + 1 ) ≤ 0 ) )
139 131 137 138 sylancl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 − 𝐾 ) < 0 ↔ ( ( 𝑁 − 𝐾 ) + 1 ) ≤ 0 ) )
140 136 139 mpbid ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 − 𝐾 ) + 1 ) ≤ 0 )
141 nn0ge0 ⊢ ( 𝑁 ∈ ℕ0 → 0 ≤ 𝑁 )
142 141 ad2antrr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → 0 ≤ 𝑁 )
143 0zd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → 0 ∈ ℤ )
144 75 adantr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 − 𝐾 ) + 1 ) ∈ ℤ )
145 elfz ⊢ ( ( 0 ∈ ℤ ∧ ( ( 𝑁 − 𝐾 ) + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 0 ∈ ( ( ( 𝑁 − 𝐾 ) + 1 ) ... 𝑁 ) ↔ ( ( ( 𝑁 − 𝐾 ) + 1 ) ≤ 0 ∧ 0 ≤ 𝑁 ) ) )
146 143 144 121 145 syl3anc ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 0 ∈ ( ( ( 𝑁 − 𝐾 ) + 1 ) ... 𝑁 ) ↔ ( ( ( 𝑁 − 𝐾 ) + 1 ) ≤ 0 ∧ 0 ≤ 𝑁 ) ) )
147 140 142 146 mpbir2and ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → 0 ∈ ( ( ( 𝑁 − 𝐾 ) + 1 ) ... 𝑁 ) )
148 simpll ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → 𝑁 ∈ ℕ0 )
149 0cn ⊢ 0 ∈ ℂ
150 fvi ⊢ ( 0 ∈ ℂ → ( I ‘ 0 ) = 0 )
151 149 150 mp1i ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( I ‘ 0 ) = 0 )
152 108 113 115 117 147 148 151 seqz ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( seq ( ( 𝑁 − 𝐾 ) + 1 ) ( · , I ) ‘ 𝑁 ) = 0 )
153 152 oveq1d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ( seq ( ( 𝑁 − 𝐾 ) + 1 ) ( · , I ) ‘ 𝑁 ) / ( ! ‘ 𝐾 ) ) = ( 0 / ( ! ‘ 𝐾 ) ) )
154 bcval3 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C 𝐾 ) = 0 )
155 20 154 syl3an2 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C 𝐾 ) = 0 )
156 155 3expa ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C 𝐾 ) = 0 )
157 107 153 156 3eqtr4rd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C 𝐾 ) = ( ( seq ( ( 𝑁 − 𝐾 ) + 1 ) ( · , I ) ‘ 𝑁 ) / ( ! ‘ 𝐾 ) ) )
158 100 157 pm2.61dan ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ ) → ( 𝑁 C 𝐾 ) = ( ( seq ( ( 𝑁 − 𝐾 ) + 1 ) ( · , I ) ‘ 𝑁 ) / ( ! ‘ 𝐾 ) ) )