Metamath Proof Explorer


Theorem binomfallfaclem2

Description: Lemma for binomfallfac . Inductive step. (Contributed by Scott Fenton, 13-Mar-2018)

Ref Expression
Hypotheses binomfallfaclem.1 φ A
binomfallfaclem.2 φ B
binomfallfaclem.3 φ N 0
binomfallfaclem.4 ψ A + B N _ = k = 0 N ( N k) A N k _ B k _
Assertion binomfallfaclem2 φ ψ A + B N + 1 _ = k = 0 N + 1 ( N + 1 k) A N + 1 - k _ B k _

Proof

Step Hyp Ref Expression
1 binomfallfaclem.1 φ A
2 binomfallfaclem.2 φ B
3 binomfallfaclem.3 φ N 0
4 binomfallfaclem.4 ψ A + B N _ = k = 0 N ( N k) A N k _ B k _
5 elfzelz k 0 N k
6 bccl N 0 k ( N k) 0
7 3 5 6 syl2an φ k 0 N ( N k) 0
8 7 nn0cnd φ k 0 N ( N k)
9 fznn0sub k 0 N N k 0
10 fallfaccl A N k 0 A N k _
11 1 9 10 syl2an φ k 0 N A N k _
12 elfznn0 k 0 N k 0
13 fallfaccl B k 0 B k _
14 2 12 13 syl2an φ k 0 N B k _
15 11 14 mulcld φ k 0 N A N k _ B k _
16 1 2 addcld φ A + B
17 3 nn0cnd φ N
18 16 17 subcld φ A + B - N
19 18 adantr φ k 0 N A + B - N
20 8 15 19 mulassd φ k 0 N ( N k) A N k _ B k _ A + B - N = ( N k) A N k _ B k _ A + B - N
21 9 nn0cnd k 0 N N k
22 subcl A N k A N k
23 1 21 22 syl2an φ k 0 N A N k
24 12 nn0cnd k 0 N k
25 subcl B k B k
26 2 24 25 syl2an φ k 0 N B k
27 15 23 26 adddid φ k 0 N A N k _ B k _ A N k + B - k = A N k _ B k _ A N k + A N k _ B k _ B k
28 1 adantr φ k 0 N A
29 17 adantr φ k 0 N N
30 28 29 subcld φ k 0 N A N
31 24 adantl φ k 0 N k
32 2 adantr φ k 0 N B
33 30 31 32 ppncand φ k 0 N A N + k + B k = A - N + B
34 28 29 31 subsubd φ k 0 N A N k = A - N + k
35 34 oveq1d φ k 0 N A N k + B - k = A N + k + B k
36 28 32 29 addsubd φ k 0 N A + B - N = A - N + B
37 33 35 36 3eqtr4d φ k 0 N A N k + B - k = A + B - N
38 37 oveq2d φ k 0 N A N k _ B k _ A N k + B - k = A N k _ B k _ A + B - N
39 11 14 23 mul32d φ k 0 N A N k _ B k _ A N k = A N k _ A N k B k _
40 1cnd φ k 0 N 1
41 29 40 31 addsubd φ k 0 N N + 1 - k = N - k + 1
42 41 oveq2d φ k 0 N A N + 1 - k _ = A N - k + 1 _
43 fallfacp1 A N k 0 A N - k + 1 _ = A N k _ A N k
44 1 9 43 syl2an φ k 0 N A N - k + 1 _ = A N k _ A N k
45 42 44 eqtrd φ k 0 N A N + 1 - k _ = A N k _ A N k
46 45 oveq1d φ k 0 N A N + 1 - k _ B k _ = A N k _ A N k B k _
47 39 46 eqtr4d φ k 0 N A N k _ B k _ A N k = A N + 1 - k _ B k _
48 11 14 26 mulassd φ k 0 N A N k _ B k _ B k = A N k _ B k _ B k
49 fallfacp1 B k 0 B k + 1 _ = B k _ B k
50 2 12 49 syl2an φ k 0 N B k + 1 _ = B k _ B k
51 50 oveq2d φ k 0 N A N k _ B k + 1 _ = A N k _ B k _ B k
52 48 51 eqtr4d φ k 0 N A N k _ B k _ B k = A N k _ B k + 1 _
53 47 52 oveq12d φ k 0 N A N k _ B k _ A N k + A N k _ B k _ B k = A N + 1 - k _ B k _ + A N k _ B k + 1 _
54 27 38 53 3eqtr3d φ k 0 N A N k _ B k _ A + B - N = A N + 1 - k _ B k _ + A N k _ B k + 1 _
55 54 oveq2d φ k 0 N ( N k) A N k _ B k _ A + B - N = ( N k) A N + 1 - k _ B k _ + A N k _ B k + 1 _
56 3 nn0zd φ N
57 uzid N N N
58 peano2uz N N N + 1 N
59 fzss2 N + 1 N 0 N 0 N + 1
60 56 57 58 59 4syl φ 0 N 0 N + 1
61 60 sselda φ k 0 N k 0 N + 1
62 fznn0sub k 0 N + 1 N + 1 - k 0
63 fallfaccl A N + 1 - k 0 A N + 1 - k _
64 1 62 63 syl2an φ k 0 N + 1 A N + 1 - k _
65 61 64 syldan φ k 0 N A N + 1 - k _
66 65 14 mulcld φ k 0 N A N + 1 - k _ B k _
67 peano2nn0 k 0 k + 1 0
68 12 67 syl k 0 N k + 1 0
69 fallfaccl B k + 1 0 B k + 1 _
70 2 68 69 syl2an φ k 0 N B k + 1 _
71 11 70 mulcld φ k 0 N A N k _ B k + 1 _
72 8 66 71 adddid φ k 0 N ( N k) A N + 1 - k _ B k _ + A N k _ B k + 1 _ = ( N k) A N + 1 - k _ B k _ + ( N k) A N k _ B k + 1 _
73 20 55 72 3eqtrd φ k 0 N ( N k) A N k _ B k _ A + B - N = ( N k) A N + 1 - k _ B k _ + ( N k) A N k _ B k + 1 _
74 73 sumeq2dv φ k = 0 N ( N k) A N k _ B k _ A + B - N = k = 0 N ( N k) A N + 1 - k _ B k _ + ( N k) A N k _ B k + 1 _
75 74 adantr φ ψ k = 0 N ( N k) A N k _ B k _ A + B - N = k = 0 N ( N k) A N + 1 - k _ B k _ + ( N k) A N k _ B k + 1 _
76 16 3 fallfacp1d φ A + B N + 1 _ = A + B N _ A + B - N
77 4 oveq1d ψ A + B N _ A + B - N = k = 0 N ( N k) A N k _ B k _ A + B - N
78 76 77 sylan9eq φ ψ A + B N + 1 _ = k = 0 N ( N k) A N k _ B k _ A + B - N
79 fzfid φ 0 N Fin
80 8 15 mulcld φ k 0 N ( N k) A N k _ B k _
81 79 18 80 fsummulc1 φ k = 0 N ( N k) A N k _ B k _ A + B - N = k = 0 N ( N k) A N k _ B k _ A + B - N
82 81 adantr φ ψ k = 0 N ( N k) A N k _ B k _ A + B - N = k = 0 N ( N k) A N k _ B k _ A + B - N
83 78 82 eqtrd φ ψ A + B N + 1 _ = k = 0 N ( N k) A N k _ B k _ A + B - N
84 elfzelz k 0 N + 1 k
85 bcpasc N 0 k ( N k) + ( N k 1 ) = ( N + 1 k)
86 3 84 85 syl2an φ k 0 N + 1 ( N k) + ( N k 1 ) = ( N + 1 k)
87 86 oveq1d φ k 0 N + 1 ( N k) + ( N k 1 ) A N + 1 - k _ B k _ = ( N + 1 k) A N + 1 - k _ B k _
88 3 84 6 syl2an φ k 0 N + 1 ( N k) 0
89 88 nn0cnd φ k 0 N + 1 ( N k)
90 peano2zm k k 1
91 84 90 syl k 0 N + 1 k 1
92 bccl N 0 k 1 ( N k 1 ) 0
93 3 91 92 syl2an φ k 0 N + 1 ( N k 1 ) 0
94 93 nn0cnd φ k 0 N + 1 ( N k 1 )
95 elfznn0 k 0 N + 1 k 0
96 2 95 13 syl2an φ k 0 N + 1 B k _
97 64 96 mulcld φ k 0 N + 1 A N + 1 - k _ B k _
98 89 94 97 adddird φ k 0 N + 1 ( N k) + ( N k 1 ) A N + 1 - k _ B k _ = ( N k) A N + 1 - k _ B k _ + ( N k 1 ) A N + 1 - k _ B k _
99 87 98 eqtr3d φ k 0 N + 1 ( N + 1 k) A N + 1 - k _ B k _ = ( N k) A N + 1 - k _ B k _ + ( N k 1 ) A N + 1 - k _ B k _
100 99 sumeq2dv φ k = 0 N + 1 ( N + 1 k) A N + 1 - k _ B k _ = k = 0 N + 1 ( N k) A N + 1 - k _ B k _ + ( N k 1 ) A N + 1 - k _ B k _
101 nn0uz 0 = 0
102 3 101 eleqtrdi φ N 0
103 89 97 mulcld φ k 0 N + 1 ( N k) A N + 1 - k _ B k _
104 oveq2 k = N + 1 ( N k) = ( N N + 1 )
105 oveq2 k = N + 1 N + 1 - k = N + 1 - N + 1
106 105 oveq2d k = N + 1 A N + 1 - k _ = A N + 1 - N + 1 _
107 oveq2 k = N + 1 B k _ = B N + 1 _
108 106 107 oveq12d k = N + 1 A N + 1 - k _ B k _ = A N + 1 - N + 1 _ B N + 1 _
109 104 108 oveq12d k = N + 1 ( N k) A N + 1 - k _ B k _ = ( N N + 1 ) A N + 1 - N + 1 _ B N + 1 _
110 102 103 109 fsump1 φ k = 0 N + 1 ( N k) A N + 1 - k _ B k _ = k = 0 N ( N k) A N + 1 - k _ B k _ + ( N N + 1 ) A N + 1 - N + 1 _ B N + 1 _
111 peano2nn0 N 0 N + 1 0
112 3 111 syl φ N + 1 0
113 112 nn0zd φ N + 1
114 3 nn0red φ N
115 114 ltp1d φ N < N + 1
116 115 olcd φ N + 1 < 0 N < N + 1
117 bcval4 N 0 N + 1 N + 1 < 0 N < N + 1 ( N N + 1 ) = 0
118 3 113 116 117 syl3anc φ ( N N + 1 ) = 0
119 118 oveq1d φ ( N N + 1 ) A N + 1 - N + 1 _ B N + 1 _ = 0 A N + 1 - N + 1 _ B N + 1 _
120 112 nn0cnd φ N + 1
121 120 subidd φ N + 1 - N + 1 = 0
122 121 oveq2d φ A N + 1 - N + 1 _ = A 0 _
123 0nn0 0 0
124 fallfaccl A 0 0 A 0 _
125 1 123 124 sylancl φ A 0 _
126 122 125 eqeltrd φ A N + 1 - N + 1 _
127 fallfaccl B N + 1 0 B N + 1 _
128 2 112 127 syl2anc φ B N + 1 _
129 126 128 mulcld φ A N + 1 - N + 1 _ B N + 1 _
130 129 mul02d φ 0 A N + 1 - N + 1 _ B N + 1 _ = 0
131 119 130 eqtrd φ ( N N + 1 ) A N + 1 - N + 1 _ B N + 1 _ = 0
132 131 oveq2d φ k = 0 N ( N k) A N + 1 - k _ B k _ + ( N N + 1 ) A N + 1 - N + 1 _ B N + 1 _ = k = 0 N ( N k) A N + 1 - k _ B k _ + 0
133 61 103 syldan φ k 0 N ( N k) A N + 1 - k _ B k _
134 79 133 fsumcl φ k = 0 N ( N k) A N + 1 - k _ B k _
135 134 addid1d φ k = 0 N ( N k) A N + 1 - k _ B k _ + 0 = k = 0 N ( N k) A N + 1 - k _ B k _
136 110 132 135 3eqtrd φ k = 0 N + 1 ( N k) A N + 1 - k _ B k _ = k = 0 N ( N k) A N + 1 - k _ B k _
137 112 101 eleqtrdi φ N + 1 0
138 94 97 mulcld φ k 0 N + 1 ( N k 1 ) A N + 1 - k _ B k _
139 oveq1 k = 0 k 1 = 0 1
140 df-neg 1 = 0 1
141 139 140 eqtr4di k = 0 k 1 = 1
142 141 oveq2d k = 0 ( N k 1 ) = ( N 1 )
143 oveq2 k = 0 N + 1 - k = N + 1 - 0
144 143 oveq2d k = 0 A N + 1 - k _ = A N + 1 - 0 _
145 oveq2 k = 0 B k _ = B 0 _
146 144 145 oveq12d k = 0 A N + 1 - k _ B k _ = A N + 1 - 0 _ B 0 _
147 142 146 oveq12d k = 0 ( N k 1 ) A N + 1 - k _ B k _ = ( N 1 ) A N + 1 - 0 _ B 0 _
148 137 138 147 fsum1p φ k = 0 N + 1 ( N k 1 ) A N + 1 - k _ B k _ = ( N 1 ) A N + 1 - 0 _ B 0 _ + k = 0 + 1 N + 1 ( N k 1 ) A N + 1 - k _ B k _
149 neg1z 1
150 neg1lt0 1 < 0
151 150 orci 1 < 0 N < 1
152 bcval4 N 0 1 1 < 0 N < 1 ( N 1 ) = 0
153 149 151 152 mp3an23 N 0 ( N 1 ) = 0
154 3 153 syl φ ( N 1 ) = 0
155 154 oveq1d φ ( N 1 ) A N + 1 - 0 _ B 0 _ = 0 A N + 1 - 0 _ B 0 _
156 120 subid1d φ N + 1 - 0 = N + 1
157 156 oveq2d φ A N + 1 - 0 _ = A N + 1 _
158 fallfaccl A N + 1 0 A N + 1 _
159 1 112 158 syl2anc φ A N + 1 _
160 157 159 eqeltrd φ A N + 1 - 0 _
161 fallfaccl B 0 0 B 0 _
162 2 123 161 sylancl φ B 0 _
163 160 162 mulcld φ A N + 1 - 0 _ B 0 _
164 163 mul02d φ 0 A N + 1 - 0 _ B 0 _ = 0
165 155 164 eqtrd φ ( N 1 ) A N + 1 - 0 _ B 0 _ = 0
166 1zzd φ 1
167 0zd φ 0
168 1 2 3 binomfallfaclem1 φ j 0 N ( N j) A N j _ B j + 1 _
169 oveq2 j = k 1 ( N j) = ( N k 1 )
170 oveq2 j = k 1 N j = N k 1
171 170 oveq2d j = k 1 A N j _ = A N k 1 _
172 oveq1 j = k 1 j + 1 = k - 1 + 1
173 172 oveq2d j = k 1 B j + 1 _ = B k - 1 + 1 _
174 171 173 oveq12d j = k 1 A N j _ B j + 1 _ = A N k 1 _ B k - 1 + 1 _
175 169 174 oveq12d j = k 1 ( N j) A N j _ B j + 1 _ = ( N k 1 ) A N k 1 _ B k - 1 + 1 _
176 166 167 56 168 175 fsumshft φ j = 0 N ( N j) A N j _ B j + 1 _ = k = 0 + 1 N + 1 ( N k 1 ) A N k 1 _ B k - 1 + 1 _
177 17 adantr φ k 0 + 1 N + 1 N
178 elfzelz k 0 + 1 N + 1 k
179 178 adantl φ k 0 + 1 N + 1 k
180 179 zcnd φ k 0 + 1 N + 1 k
181 1cnd φ k 0 + 1 N + 1 1
182 177 180 181 subsub3d φ k 0 + 1 N + 1 N k 1 = N + 1 - k
183 182 oveq2d φ k 0 + 1 N + 1 A N k 1 _ = A N + 1 - k _
184 180 181 npcand φ k 0 + 1 N + 1 k - 1 + 1 = k
185 184 oveq2d φ k 0 + 1 N + 1 B k - 1 + 1 _ = B k _
186 183 185 oveq12d φ k 0 + 1 N + 1 A N k 1 _ B k - 1 + 1 _ = A N + 1 - k _ B k _
187 186 oveq2d φ k 0 + 1 N + 1 ( N k 1 ) A N k 1 _ B k - 1 + 1 _ = ( N k 1 ) A N + 1 - k _ B k _
188 187 sumeq2dv φ k = 0 + 1 N + 1 ( N k 1 ) A N k 1 _ B k - 1 + 1 _ = k = 0 + 1 N + 1 ( N k 1 ) A N + 1 - k _ B k _
189 176 188 eqtr2d φ k = 0 + 1 N + 1 ( N k 1 ) A N + 1 - k _ B k _ = j = 0 N ( N j) A N j _ B j + 1 _
190 oveq2 k = j ( N k) = ( N j)
191 oveq2 k = j N k = N j
192 191 oveq2d k = j A N k _ = A N j _
193 oveq1 k = j k + 1 = j + 1
194 193 oveq2d k = j B k + 1 _ = B j + 1 _
195 192 194 oveq12d k = j A N k _ B k + 1 _ = A N j _ B j + 1 _
196 190 195 oveq12d k = j ( N k) A N k _ B k + 1 _ = ( N j) A N j _ B j + 1 _
197 196 cbvsumv k = 0 N ( N k) A N k _ B k + 1 _ = j = 0 N ( N j) A N j _ B j + 1 _
198 189 197 eqtr4di φ k = 0 + 1 N + 1 ( N k 1 ) A N + 1 - k _ B k _ = k = 0 N ( N k) A N k _ B k + 1 _
199 165 198 oveq12d φ ( N 1 ) A N + 1 - 0 _ B 0 _ + k = 0 + 1 N + 1 ( N k 1 ) A N + 1 - k _ B k _ = 0 + k = 0 N ( N k) A N k _ B k + 1 _
200 1 2 3 binomfallfaclem1 φ k 0 N ( N k) A N k _ B k + 1 _
201 79 200 fsumcl φ k = 0 N ( N k) A N k _ B k + 1 _
202 201 addid2d φ 0 + k = 0 N ( N k) A N k _ B k + 1 _ = k = 0 N ( N k) A N k _ B k + 1 _
203 148 199 202 3eqtrd φ k = 0 N + 1 ( N k 1 ) A N + 1 - k _ B k _ = k = 0 N ( N k) A N k _ B k + 1 _
204 136 203 oveq12d φ k = 0 N + 1 ( N k) A N + 1 - k _ B k _ + k = 0 N + 1 ( N k 1 ) A N + 1 - k _ B k _ = k = 0 N ( N k) A N + 1 - k _ B k _ + k = 0 N ( N k) A N k _ B k + 1 _
205 fzfid φ 0 N + 1 Fin
206 205 103 138 fsumadd φ k = 0 N + 1 ( N k) A N + 1 - k _ B k _ + ( N k 1 ) A N + 1 - k _ B k _ = k = 0 N + 1 ( N k) A N + 1 - k _ B k _ + k = 0 N + 1 ( N k 1 ) A N + 1 - k _ B k _
207 79 133 200 fsumadd φ k = 0 N ( N k) A N + 1 - k _ B k _ + ( N k) A N k _ B k + 1 _ = k = 0 N ( N k) A N + 1 - k _ B k _ + k = 0 N ( N k) A N k _ B k + 1 _
208 204 206 207 3eqtr4d φ k = 0 N + 1 ( N k) A N + 1 - k _ B k _ + ( N k 1 ) A N + 1 - k _ B k _ = k = 0 N ( N k) A N + 1 - k _ B k _ + ( N k) A N k _ B k + 1 _
209 100 208 eqtrd φ k = 0 N + 1 ( N + 1 k) A N + 1 - k _ B k _ = k = 0 N ( N k) A N + 1 - k _ B k _ + ( N k) A N k _ B k + 1 _
210 209 adantr φ ψ k = 0 N + 1 ( N + 1 k) A N + 1 - k _ B k _ = k = 0 N ( N k) A N + 1 - k _ B k _ + ( N k) A N k _ B k + 1 _
211 75 83 210 3eqtr4d φ ψ A + B N + 1 _ = k = 0 N + 1 ( N + 1 k) A N + 1 - k _ B k _