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 
|- ( ( N e. NN0 /\ K e. ZZ ) -> ( ( N _C K ) + ( N _C ( K - 1 ) ) ) = ( ( N + 1 ) _C K ) )

Proof

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