Metamath Proof Explorer

Theorem bcpasc

Description: Pascal's rule for the binomial coefficient, generalized to all integers K . Equation 2 of Gleason p. 295. (Contributed by NM, 13-Jul-2005) (Revised by Mario Carneiro, 10-Mar-2014)

Ref Expression
Assertion bcpasc ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) → ( ( 𝑁 C 𝐾 ) + ( 𝑁 C ( 𝐾 − 1 ) ) ) = ( ( 𝑁 + 1 ) C 𝐾 ) )

Proof

Step Hyp Ref Expression
1 peano2nn0 ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
2 elfzp12 ⊢ ( ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 0 ) → ( 𝐾 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↔ ( 𝐾 = 0 ∨ 𝐾 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) ) )
3 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
4 2 3 eleq2s ⊢ ( ( 𝑁 + 1 ) ∈ ℕ0 → ( 𝐾 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↔ ( 𝐾 = 0 ∨ 𝐾 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) ) )
5 1 4 syl ⊢ ( 𝑁 ∈ ℕ0 → ( 𝐾 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↔ ( 𝐾 = 0 ∨ 𝐾 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) ) )
6 1p0e1 ⊢ ( 1 + 0 ) = 1
7 bcn0 ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 C 0 ) = 1 )
8 0z ⊢ 0 ∈ ℤ
9 1z ⊢ 1 ∈ ℤ
10 zsubcl ⊢ ( ( 0 ∈ ℤ ∧ 1 ∈ ℤ ) → ( 0 − 1 ) ∈ ℤ )
11 8 9 10 mp2an ⊢ ( 0 − 1 ) ∈ ℤ
12 0re ⊢ 0 ∈ ℝ
13 ltm1 ⊢ ( 0 ∈ ℝ → ( 0 − 1 ) < 0 )
14 12 13 ax-mp ⊢ ( 0 − 1 ) < 0
15 14 orci ⊢ ( ( 0 − 1 ) < 0 ∨ 𝑁 < ( 0 − 1 ) )
16 bcval4 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 0 − 1 ) ∈ ℤ ∧ ( ( 0 − 1 ) < 0 ∨ 𝑁 < ( 0 − 1 ) ) ) → ( 𝑁 C ( 0 − 1 ) ) = 0 )
17 11 15 16 mp3an23 ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 C ( 0 − 1 ) ) = 0 )
18 7 17 oveq12d ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 C 0 ) + ( 𝑁 C ( 0 − 1 ) ) ) = ( 1 + 0 ) )
19 bcn0 ⊢ ( ( 𝑁 + 1 ) ∈ ℕ0 → ( ( 𝑁 + 1 ) C 0 ) = 1 )
20 1 19 syl ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) C 0 ) = 1 )
21 6 18 20 3eqtr4a ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 C 0 ) + ( 𝑁 C ( 0 − 1 ) ) ) = ( ( 𝑁 + 1 ) C 0 ) )
22 oveq2 ⊢ ( 𝐾 = 0 → ( 𝑁 C 𝐾 ) = ( 𝑁 C 0 ) )
23 oveq1 ⊢ ( 𝐾 = 0 → ( 𝐾 − 1 ) = ( 0 − 1 ) )
24 23 oveq2d ⊢ ( 𝐾 = 0 → ( 𝑁 C ( 𝐾 − 1 ) ) = ( 𝑁 C ( 0 − 1 ) ) )
25 22 24 oveq12d ⊢ ( 𝐾 = 0 → ( ( 𝑁 C 𝐾 ) + ( 𝑁 C ( 𝐾 − 1 ) ) ) = ( ( 𝑁 C 0 ) + ( 𝑁 C ( 0 − 1 ) ) ) )
26 oveq2 ⊢ ( 𝐾 = 0 → ( ( 𝑁 + 1 ) C 𝐾 ) = ( ( 𝑁 + 1 ) C 0 ) )
27 25 26 eqeq12d ⊢ ( 𝐾 = 0 → ( ( ( 𝑁 C 𝐾 ) + ( 𝑁 C ( 𝐾 − 1 ) ) ) = ( ( 𝑁 + 1 ) C 𝐾 ) ↔ ( ( 𝑁 C 0 ) + ( 𝑁 C ( 0 − 1 ) ) ) = ( ( 𝑁 + 1 ) C 0 ) ) )
28 21 27 syl5ibrcom ⊢ ( 𝑁 ∈ ℕ0 → ( 𝐾 = 0 → ( ( 𝑁 C 𝐾 ) + ( 𝑁 C ( 𝐾 − 1 ) ) ) = ( ( 𝑁 + 1 ) C 𝐾 ) ) )
29 simpr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → 𝐾 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) )
30 0p1e1 ⊢ ( 0 + 1 ) = 1
31 30 oveq1i ⊢ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) = ( 1 ... ( 𝑁 + 1 ) )
32 29 31 eleqtrdi ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → 𝐾 ∈ ( 1 ... ( 𝑁 + 1 ) ) )
33 nn0p1nn ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ )
34 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
35 33 34 eleqtrdi ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
36 fzm1 ⊢ ( ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 1 ) → ( 𝐾 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↔ ( 𝐾 ∈ ( 1 ... ( ( 𝑁 + 1 ) − 1 ) ) ∨ 𝐾 = ( 𝑁 + 1 ) ) ) )
37 36 biimpa ⊢ ( ( ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 1 ) ∧ 𝐾 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( 𝐾 ∈ ( 1 ... ( ( 𝑁 + 1 ) − 1 ) ) ∨ 𝐾 = ( 𝑁 + 1 ) ) )
38 35 37 sylan ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( 𝐾 ∈ ( 1 ... ( ( 𝑁 + 1 ) − 1 ) ) ∨ 𝐾 = ( 𝑁 + 1 ) ) )
39 nn0cn ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ )
40 ax-1cn ⊢ 1 ∈ ℂ
41 pncan ⊢ ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
42 39 40 41 sylancl ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
43 42 oveq2d ⊢ ( 𝑁 ∈ ℕ0 → ( 1 ... ( ( 𝑁 + 1 ) − 1 ) ) = ( 1 ... 𝑁 ) )
44 43 eleq2d ⊢ ( 𝑁 ∈ ℕ0 → ( 𝐾 ∈ ( 1 ... ( ( 𝑁 + 1 ) − 1 ) ) ↔ 𝐾 ∈ ( 1 ... 𝑁 ) ) )
45 44 biimpa ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ( 1 ... ( ( 𝑁 + 1 ) − 1 ) ) ) → 𝐾 ∈ ( 1 ... 𝑁 ) )
46 fz1ssfz0 ⊢ ( 1 ... 𝑁 ) ⊆ ( 0 ... 𝑁 )
47 46 sseli ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → 𝐾 ∈ ( 0 ... 𝑁 ) )
48 bcp1n ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( 𝑁 + 1 ) C 𝐾 ) = ( ( 𝑁 C 𝐾 ) · ( ( 𝑁 + 1 ) / ( ( 𝑁 + 1 ) − 𝐾 ) ) ) )
49 47 48 syl ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( 𝑁 + 1 ) C 𝐾 ) = ( ( 𝑁 C 𝐾 ) · ( ( 𝑁 + 1 ) / ( ( 𝑁 + 1 ) − 𝐾 ) ) ) )
50 bcrpcl ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑁 C 𝐾 ) ∈ ℝ+ )
51 47 50 syl ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( 𝑁 C 𝐾 ) ∈ ℝ+ )
52 51 rpcnd ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( 𝑁 C 𝐾 ) ∈ ℂ )
53 elfzuz2 ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
54 53 34 eleqtrrdi ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → 𝑁 ∈ ℕ )
55 54 peano2nnd ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( 𝑁 + 1 ) ∈ ℕ )
56 55 nncnd ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( 𝑁 + 1 ) ∈ ℂ )
57 54 nncnd ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → 𝑁 ∈ ℂ )
58 1cnd ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → 1 ∈ ℂ )
59 elfzelz ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → 𝐾 ∈ ℤ )
60 59 zcnd ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → 𝐾 ∈ ℂ )
61 57 58 60 addsubd ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( 𝑁 + 1 ) − 𝐾 ) = ( ( 𝑁 − 𝐾 ) + 1 ) )
62 fznn0sub ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( 𝑁 − 𝐾 ) ∈ ℕ0 )
63 nn0p1nn ⊢ ( ( 𝑁 − 𝐾 ) ∈ ℕ0 → ( ( 𝑁 − 𝐾 ) + 1 ) ∈ ℕ )
64 62 63 syl ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( 𝑁 − 𝐾 ) + 1 ) ∈ ℕ )
65 61 64 eqeltrd ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( 𝑁 + 1 ) − 𝐾 ) ∈ ℕ )
66 65 nncnd ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( 𝑁 + 1 ) − 𝐾 ) ∈ ℂ )
67 65 nnne0d ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( 𝑁 + 1 ) − 𝐾 ) ≠ 0 )
68 52 56 66 67 div12d ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( 𝑁 C 𝐾 ) · ( ( 𝑁 + 1 ) / ( ( 𝑁 + 1 ) − 𝐾 ) ) ) = ( ( 𝑁 + 1 ) · ( ( 𝑁 C 𝐾 ) / ( ( 𝑁 + 1 ) − 𝐾 ) ) ) )
69 65 nnrpd ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( 𝑁 + 1 ) − 𝐾 ) ∈ ℝ+ )
70 51 69 rpdivcld ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( 𝑁 C 𝐾 ) / ( ( 𝑁 + 1 ) − 𝐾 ) ) ∈ ℝ+ )
71 70 rpcnd ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( 𝑁 C 𝐾 ) / ( ( 𝑁 + 1 ) − 𝐾 ) ) ∈ ℂ )
72 56 71 mulcomd ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( 𝑁 + 1 ) · ( ( 𝑁 C 𝐾 ) / ( ( 𝑁 + 1 ) − 𝐾 ) ) ) = ( ( ( 𝑁 C 𝐾 ) / ( ( 𝑁 + 1 ) − 𝐾 ) ) · ( 𝑁 + 1 ) ) )
73 68 72 eqtrd ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( 𝑁 C 𝐾 ) · ( ( 𝑁 + 1 ) / ( ( 𝑁 + 1 ) − 𝐾 ) ) ) = ( ( ( 𝑁 C 𝐾 ) / ( ( 𝑁 + 1 ) − 𝐾 ) ) · ( 𝑁 + 1 ) ) )
74 56 60 npcand ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ( 𝑁 + 1 ) − 𝐾 ) + 𝐾 ) = ( 𝑁 + 1 ) )
75 74 oveq2d ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ( 𝑁 C 𝐾 ) / ( ( 𝑁 + 1 ) − 𝐾 ) ) · ( ( ( 𝑁 + 1 ) − 𝐾 ) + 𝐾 ) ) = ( ( ( 𝑁 C 𝐾 ) / ( ( 𝑁 + 1 ) − 𝐾 ) ) · ( 𝑁 + 1 ) ) )
76 71 66 60 adddid ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ( 𝑁 C 𝐾 ) / ( ( 𝑁 + 1 ) − 𝐾 ) ) · ( ( ( 𝑁 + 1 ) − 𝐾 ) + 𝐾 ) ) = ( ( ( ( 𝑁 C 𝐾 ) / ( ( 𝑁 + 1 ) − 𝐾 ) ) · ( ( 𝑁 + 1 ) − 𝐾 ) ) + ( ( ( 𝑁 C 𝐾 ) / ( ( 𝑁 + 1 ) − 𝐾 ) ) · 𝐾 ) ) )
77 73 75 76 3eqtr2d ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( 𝑁 C 𝐾 ) · ( ( 𝑁 + 1 ) / ( ( 𝑁 + 1 ) − 𝐾 ) ) ) = ( ( ( ( 𝑁 C 𝐾 ) / ( ( 𝑁 + 1 ) − 𝐾 ) ) · ( ( 𝑁 + 1 ) − 𝐾 ) ) + ( ( ( 𝑁 C 𝐾 ) / ( ( 𝑁 + 1 ) − 𝐾 ) ) · 𝐾 ) ) )
78 52 66 67 divcan1d ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ( 𝑁 C 𝐾 ) / ( ( 𝑁 + 1 ) − 𝐾 ) ) · ( ( 𝑁 + 1 ) − 𝐾 ) ) = ( 𝑁 C 𝐾 ) )
79 elfznn ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → 𝐾 ∈ ℕ )
80 79 nnne0d ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → 𝐾 ≠ 0 )
81 52 66 60 67 80 divdiv2d ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( 𝑁 C 𝐾 ) / ( ( ( 𝑁 + 1 ) − 𝐾 ) / 𝐾 ) ) = ( ( ( 𝑁 C 𝐾 ) · 𝐾 ) / ( ( 𝑁 + 1 ) − 𝐾 ) ) )
82 bcm1k ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( 𝑁 C 𝐾 ) = ( ( 𝑁 C ( 𝐾 − 1 ) ) · ( ( 𝑁 − ( 𝐾 − 1 ) ) / 𝐾 ) ) )
83 57 60 58 subsub3d ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( 𝑁 − ( 𝐾 − 1 ) ) = ( ( 𝑁 + 1 ) − 𝐾 ) )
84 83 oveq1d ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( 𝑁 − ( 𝐾 − 1 ) ) / 𝐾 ) = ( ( ( 𝑁 + 1 ) − 𝐾 ) / 𝐾 ) )
85 84 oveq2d ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( 𝑁 C ( 𝐾 − 1 ) ) · ( ( 𝑁 − ( 𝐾 − 1 ) ) / 𝐾 ) ) = ( ( 𝑁 C ( 𝐾 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝐾 ) / 𝐾 ) ) )
86 82 85 eqtrd ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( 𝑁 C 𝐾 ) = ( ( 𝑁 C ( 𝐾 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝐾 ) / 𝐾 ) ) )
87 fzelp1 ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → 𝐾 ∈ ( 1 ... ( 𝑁 + 1 ) ) )
88 55 nnzd ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( 𝑁 + 1 ) ∈ ℤ )
89 elfzm1b ⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝑁 + 1 ) ∈ ℤ ) → ( 𝐾 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↔ ( 𝐾 − 1 ) ∈ ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) ) )
90 59 88 89 syl2anc ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( 𝐾 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↔ ( 𝐾 − 1 ) ∈ ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) ) )
91 87 90 mpbid ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( 𝐾 − 1 ) ∈ ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) )
92 57 40 41 sylancl ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
93 92 oveq2d ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) = ( 0 ... 𝑁 ) )
94 91 93 eleqtrd ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( 𝐾 − 1 ) ∈ ( 0 ... 𝑁 ) )
95 bcrpcl ⊢ ( ( 𝐾 − 1 ) ∈ ( 0 ... 𝑁 ) → ( 𝑁 C ( 𝐾 − 1 ) ) ∈ ℝ+ )
96 94 95 syl ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( 𝑁 C ( 𝐾 − 1 ) ) ∈ ℝ+ )
97 96 rpcnd ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( 𝑁 C ( 𝐾 − 1 ) ) ∈ ℂ )
98 79 nnrpd ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → 𝐾 ∈ ℝ+ )
99 69 98 rpdivcld ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ( 𝑁 + 1 ) − 𝐾 ) / 𝐾 ) ∈ ℝ+ )
100 99 rpcnd ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ( 𝑁 + 1 ) − 𝐾 ) / 𝐾 ) ∈ ℂ )
101 99 rpne0d ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ( 𝑁 + 1 ) − 𝐾 ) / 𝐾 ) ≠ 0 )
102 52 97 100 101 divmul3d ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ( 𝑁 C 𝐾 ) / ( ( ( 𝑁 + 1 ) − 𝐾 ) / 𝐾 ) ) = ( 𝑁 C ( 𝐾 − 1 ) ) ↔ ( 𝑁 C 𝐾 ) = ( ( 𝑁 C ( 𝐾 − 1 ) ) · ( ( ( 𝑁 + 1 ) − 𝐾 ) / 𝐾 ) ) ) )
103 86 102 mpbird ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( 𝑁 C 𝐾 ) / ( ( ( 𝑁 + 1 ) − 𝐾 ) / 𝐾 ) ) = ( 𝑁 C ( 𝐾 − 1 ) ) )
104 52 60 66 67 div23d ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ( 𝑁 C 𝐾 ) · 𝐾 ) / ( ( 𝑁 + 1 ) − 𝐾 ) ) = ( ( ( 𝑁 C 𝐾 ) / ( ( 𝑁 + 1 ) − 𝐾 ) ) · 𝐾 ) )
105 81 103 104 3eqtr3rd ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ( 𝑁 C 𝐾 ) / ( ( 𝑁 + 1 ) − 𝐾 ) ) · 𝐾 ) = ( 𝑁 C ( 𝐾 − 1 ) ) )
106 78 105 oveq12d ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ( ( 𝑁 C 𝐾 ) / ( ( 𝑁 + 1 ) − 𝐾 ) ) · ( ( 𝑁 + 1 ) − 𝐾 ) ) + ( ( ( 𝑁 C 𝐾 ) / ( ( 𝑁 + 1 ) − 𝐾 ) ) · 𝐾 ) ) = ( ( 𝑁 C 𝐾 ) + ( 𝑁 C ( 𝐾 − 1 ) ) ) )
107 49 77 106 3eqtrrd ⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( 𝑁 C 𝐾 ) + ( 𝑁 C ( 𝐾 − 1 ) ) ) = ( ( 𝑁 + 1 ) C 𝐾 ) )
108 45 107 syl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ( 1 ... ( ( 𝑁 + 1 ) − 1 ) ) ) → ( ( 𝑁 C 𝐾 ) + ( 𝑁 C ( 𝐾 − 1 ) ) ) = ( ( 𝑁 + 1 ) C 𝐾 ) )
109 oveq2 ⊢ ( 𝐾 = ( 𝑁 + 1 ) → ( 𝑁 C 𝐾 ) = ( 𝑁 C ( 𝑁 + 1 ) ) )
110 33 nnzd ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℤ )
111 nn0re ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
112 111 ltp1d ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 < ( 𝑁 + 1 ) )
113 112 olcd ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) < 0 ∨ 𝑁 < ( 𝑁 + 1 ) ) )
114 bcval4 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑁 + 1 ) ∈ ℤ ∧ ( ( 𝑁 + 1 ) < 0 ∨ 𝑁 < ( 𝑁 + 1 ) ) ) → ( 𝑁 C ( 𝑁 + 1 ) ) = 0 )
115 110 113 114 mpd3an23 ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 C ( 𝑁 + 1 ) ) = 0 )
116 109 115 sylan9eqr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 = ( 𝑁 + 1 ) ) → ( 𝑁 C 𝐾 ) = 0 )
117 oveq1 ⊢ ( 𝐾 = ( 𝑁 + 1 ) → ( 𝐾 − 1 ) = ( ( 𝑁 + 1 ) − 1 ) )
118 117 42 sylan9eqr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 = ( 𝑁 + 1 ) ) → ( 𝐾 − 1 ) = 𝑁 )
119 118 oveq2d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 = ( 𝑁 + 1 ) ) → ( 𝑁 C ( 𝐾 − 1 ) ) = ( 𝑁 C 𝑁 ) )
120 bcnn ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 C 𝑁 ) = 1 )
121 120 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 = ( 𝑁 + 1 ) ) → ( 𝑁 C 𝑁 ) = 1 )
122 119 121 eqtrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 = ( 𝑁 + 1 ) ) → ( 𝑁 C ( 𝐾 − 1 ) ) = 1 )
123 116 122 oveq12d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 = ( 𝑁 + 1 ) ) → ( ( 𝑁 C 𝐾 ) + ( 𝑁 C ( 𝐾 − 1 ) ) ) = ( 0 + 1 ) )
124 oveq2 ⊢ ( 𝐾 = ( 𝑁 + 1 ) → ( ( 𝑁 + 1 ) C 𝐾 ) = ( ( 𝑁 + 1 ) C ( 𝑁 + 1 ) ) )
125 bcnn ⊢ ( ( 𝑁 + 1 ) ∈ ℕ0 → ( ( 𝑁 + 1 ) C ( 𝑁 + 1 ) ) = 1 )
126 1 125 syl ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) C ( 𝑁 + 1 ) ) = 1 )
127 124 126 sylan9eqr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 = ( 𝑁 + 1 ) ) → ( ( 𝑁 + 1 ) C 𝐾 ) = 1 )
128 30 123 127 3eqtr4a ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 = ( 𝑁 + 1 ) ) → ( ( 𝑁 C 𝐾 ) + ( 𝑁 C ( 𝐾 − 1 ) ) ) = ( ( 𝑁 + 1 ) C 𝐾 ) )
129 108 128 jaodan ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐾 ∈ ( 1 ... ( ( 𝑁 + 1 ) − 1 ) ) ∨ 𝐾 = ( 𝑁 + 1 ) ) ) → ( ( 𝑁 C 𝐾 ) + ( 𝑁 C ( 𝐾 − 1 ) ) ) = ( ( 𝑁 + 1 ) C 𝐾 ) )
130 38 129 syldan ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 C 𝐾 ) + ( 𝑁 C ( 𝐾 − 1 ) ) ) = ( ( 𝑁 + 1 ) C 𝐾 ) )
131 32 130 syldan ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 C 𝐾 ) + ( 𝑁 C ( 𝐾 − 1 ) ) ) = ( ( 𝑁 + 1 ) C 𝐾 ) )
132 131 ex ⊢ ( 𝑁 ∈ ℕ0 → ( 𝐾 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) → ( ( 𝑁 C 𝐾 ) + ( 𝑁 C ( 𝐾 − 1 ) ) ) = ( ( 𝑁 + 1 ) C 𝐾 ) ) )
133 28 132 jaod ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝐾 = 0 ∨ 𝐾 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 C 𝐾 ) + ( 𝑁 C ( 𝐾 − 1 ) ) ) = ( ( 𝑁 + 1 ) C 𝐾 ) ) )
134 5 133 sylbid ⊢ ( 𝑁 ∈ ℕ0 → ( 𝐾 ∈ ( 0 ... ( 𝑁 + 1 ) ) → ( ( 𝑁 C 𝐾 ) + ( 𝑁 C ( 𝐾 − 1 ) ) ) = ( ( 𝑁 + 1 ) C 𝐾 ) ) )
135 134 imp ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 C 𝐾 ) + ( 𝑁 C ( 𝐾 − 1 ) ) ) = ( ( 𝑁 + 1 ) C 𝐾 ) )
136 135 adantlr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) ∧ 𝐾 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 C 𝐾 ) + ( 𝑁 C ( 𝐾 − 1 ) ) ) = ( ( 𝑁 + 1 ) C 𝐾 ) )
137 00id ⊢ ( 0 + 0 ) = 0
138 fzelp1 ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝐾 ∈ ( 0 ... ( 𝑁 + 1 ) ) )
139 138 con3i ⊢ ( ¬ 𝐾 ∈ ( 0 ... ( 𝑁 + 1 ) ) → ¬ 𝐾 ∈ ( 0 ... 𝑁 ) )
140 bcval3 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C 𝐾 ) = 0 )
141 140 3expa ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) ∧ ¬ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C 𝐾 ) = 0 )
142 139 141 sylan2 ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) ∧ ¬ 𝐾 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 𝑁 C 𝐾 ) = 0 )
143 simpll ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) ∧ ¬ 𝐾 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → 𝑁 ∈ ℕ0 )
144 simplr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) ∧ ¬ 𝐾 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → 𝐾 ∈ ℤ )
145 peano2zm ⊢ ( 𝐾 ∈ ℤ → ( 𝐾 − 1 ) ∈ ℤ )
146 144 145 syl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) ∧ ¬ 𝐾 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 𝐾 − 1 ) ∈ ℤ )
147 39 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) → 𝑁 ∈ ℂ )
148 147 40 41 sylancl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
149 148 oveq2d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) → ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) = ( 0 ... 𝑁 ) )
150 149 eleq2d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) → ( ( 𝐾 − 1 ) ∈ ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) ↔ ( 𝐾 − 1 ) ∈ ( 0 ... 𝑁 ) ) )
151 id ⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℤ )
152 1 nn0zd ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℤ )
153 151 152 89 syl2anr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) → ( 𝐾 ∈ ( 1 ... ( 𝑁 + 1 ) ) ↔ ( 𝐾 − 1 ) ∈ ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) ) )
154 fz1ssfz0 ⊢ ( 1 ... ( 𝑁 + 1 ) ) ⊆ ( 0 ... ( 𝑁 + 1 ) )
155 154 sseli ⊢ ( 𝐾 ∈ ( 1 ... ( 𝑁 + 1 ) ) → 𝐾 ∈ ( 0 ... ( 𝑁 + 1 ) ) )
156 153 155 syl6bir ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) → ( ( 𝐾 − 1 ) ∈ ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) → 𝐾 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) )
157 150 156 sylbird ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) → ( ( 𝐾 − 1 ) ∈ ( 0 ... 𝑁 ) → 𝐾 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) )
158 157 con3dimp ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) ∧ ¬ 𝐾 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ¬ ( 𝐾 − 1 ) ∈ ( 0 ... 𝑁 ) )
159 bcval3 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐾 − 1 ) ∈ ℤ ∧ ¬ ( 𝐾 − 1 ) ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C ( 𝐾 − 1 ) ) = 0 )
160 143 146 158 159 syl3anc ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) ∧ ¬ 𝐾 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 𝑁 C ( 𝐾 − 1 ) ) = 0 )
161 142 160 oveq12d ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) ∧ ¬ 𝐾 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 C 𝐾 ) + ( 𝑁 C ( 𝐾 − 1 ) ) ) = ( 0 + 0 ) )
162 143 1 syl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) ∧ ¬ 𝐾 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 𝑁 + 1 ) ∈ ℕ0 )
163 simpr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) ∧ ¬ 𝐾 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ¬ 𝐾 ∈ ( 0 ... ( 𝑁 + 1 ) ) )
164 bcval3 ⊢ ( ( ( 𝑁 + 1 ) ∈ ℕ0 ∧ 𝐾 ∈ ℤ ∧ ¬ 𝐾 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 + 1 ) C 𝐾 ) = 0 )
165 162 144 163 164 syl3anc ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) ∧ ¬ 𝐾 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 + 1 ) C 𝐾 ) = 0 )
166 137 161 165 3eqtr4a ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) ∧ ¬ 𝐾 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 C 𝐾 ) + ( 𝑁 C ( 𝐾 − 1 ) ) ) = ( ( 𝑁 + 1 ) C 𝐾 ) )
167 136 166 pm2.61dan ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) → ( ( 𝑁 C 𝐾 ) + ( 𝑁 C ( 𝐾 − 1 ) ) ) = ( ( 𝑁 + 1 ) C 𝐾 ) )