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 𝐾 ) )