Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  binomfallfaclem2 Structured version   Visualization version   Unicode version

Theorem binomfallfaclem2 14170
 Description: Lemma for binomfallfac 14171. Inductive step. (Contributed by Scott Fenton, 13-Mar-2018.)
Hypotheses
Ref Expression
binomfallfaclem.1
binomfallfaclem.2
binomfallfaclem.3
binomfallfaclem.4 FallFac FallFac FallFac
Assertion
Ref Expression
binomfallfaclem2 FallFac FallFac FallFac
Distinct variable groups:   ,   ,   ,   ,
Allowed substitution hint:   ()

Proof of Theorem binomfallfaclem2
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 binomfallfaclem.3 . . . . . . . 8
2 elfzelz 11826 . . . . . . . 8
3 bccl 12545 . . . . . . . 8
41, 2, 3syl2an 485 . . . . . . 7
54nn0cnd 10951 . . . . . 6
6 binomfallfaclem.1 . . . . . . . 8
7 fznn0sub 11857 . . . . . . . 8
8 fallfaccl 14146 . . . . . . . 8 FallFac
96, 7, 8syl2an 485 . . . . . . 7 FallFac
10 binomfallfaclem.2 . . . . . . . 8
11 elfznn0 11913 . . . . . . . 8
12 fallfaccl 14146 . . . . . . . 8 FallFac
1310, 11, 12syl2an 485 . . . . . . 7 FallFac
149, 13mulcld 9681 . . . . . 6 FallFac FallFac
156, 10addcld 9680 . . . . . . . 8
161nn0cnd 10951 . . . . . . . 8
1715, 16subcld 10005 . . . . . . 7
1817adantr 472 . . . . . 6
195, 14, 18mulassd 9684 . . . . 5 FallFac FallFac FallFac FallFac
207nn0cnd 10951 . . . . . . . . 9
21 subcl 9894 . . . . . . . . 9
226, 20, 21syl2an 485 . . . . . . . 8
2311nn0cnd 10951 . . . . . . . . 9
24 subcl 9894 . . . . . . . . 9
2510, 23, 24syl2an 485 . . . . . . . 8
2614, 22, 25adddid 9685 . . . . . . 7 FallFac FallFac FallFac FallFac FallFac FallFac
276adantr 472 . . . . . . . . . . 11
2816adantr 472 . . . . . . . . . . 11
2927, 28subcld 10005 . . . . . . . . . 10
3023adantl 473 . . . . . . . . . 10
3110adantr 472 . . . . . . . . . 10
3229, 30, 31ppncand 10045 . . . . . . . . 9
3327, 28, 30subsubd 10033 . . . . . . . . . 10
3433oveq1d 6323 . . . . . . . . 9
3527, 31, 28addsubd 10026 . . . . . . . . 9
3632, 34, 353eqtr4d 2515 . . . . . . . 8
3736oveq2d 6324 . . . . . . 7 FallFac FallFac FallFac FallFac
389, 13, 22mul32d 9861 . . . . . . . . 9 FallFac FallFac FallFac FallFac
39 1cnd 9677 . . . . . . . . . . . . 13
4028, 39, 30addsubd 10026 . . . . . . . . . . . 12
4140oveq2d 6324 . . . . . . . . . . 11 FallFac FallFac
42 fallfacp1 14160 . . . . . . . . . . . 12 FallFac FallFac
436, 7, 42syl2an 485 . . . . . . . . . . 11 FallFac FallFac
4441, 43eqtrd 2505 . . . . . . . . . 10 FallFac FallFac
4544oveq1d 6323 . . . . . . . . 9 FallFac FallFac FallFac FallFac
4638, 45eqtr4d 2508 . . . . . . . 8 FallFac FallFac FallFac FallFac
479, 13, 25mulassd 9684 . . . . . . . . 9 FallFac FallFac FallFac FallFac
48 fallfacp1 14160 . . . . . . . . . . 11 FallFac FallFac
4910, 11, 48syl2an 485 . . . . . . . . . 10 FallFac FallFac
5049oveq2d 6324 . . . . . . . . 9 FallFac FallFac FallFac FallFac
5147, 50eqtr4d 2508 . . . . . . . 8 FallFac FallFac FallFac FallFac
5246, 51oveq12d 6326 . . . . . . 7 FallFac FallFac FallFac FallFac FallFac FallFac FallFac FallFac
5326, 37, 523eqtr3d 2513 . . . . . 6 FallFac FallFac FallFac FallFac FallFac FallFac
5453oveq2d 6324 . . . . 5 FallFac FallFac FallFac FallFac FallFac FallFac
551nn0zd 11061 . . . . . . . . . 10
56 uzid 11197 . . . . . . . . . 10
57 peano2uz 11235 . . . . . . . . . 10
58 fzss2 11864 . . . . . . . . . 10
5955, 56, 57, 584syl 19 . . . . . . . . 9
6059sselda 3418 . . . . . . . 8
61 fznn0sub 11857 . . . . . . . . 9
62 fallfaccl 14146 . . . . . . . . 9 FallFac
636, 61, 62syl2an 485 . . . . . . . 8 FallFac
6460, 63syldan 478 . . . . . . 7 FallFac
6564, 13mulcld 9681 . . . . . 6 FallFac FallFac
66 peano2nn0 10934 . . . . . . . . 9
6711, 66syl 17 . . . . . . . 8
68 fallfaccl 14146 . . . . . . . 8 FallFac
6910, 67, 68syl2an 485 . . . . . . 7 FallFac
709, 69mulcld 9681 . . . . . 6 FallFac FallFac
715, 65, 70adddid 9685 . . . . 5 FallFac FallFac FallFac FallFac FallFac FallFac FallFac FallFac
7219, 54, 713eqtrd 2509 . . . 4 FallFac FallFac FallFac FallFac FallFac FallFac
7372sumeq2dv 13846 . . 3 FallFac FallFac FallFac FallFac FallFac FallFac
7473adantr 472 . 2 FallFac FallFac FallFac FallFac FallFac FallFac
7515, 1fallfacp1d 14162 . . . 4 FallFac FallFac
76 binomfallfaclem.4 . . . . 5 FallFac FallFac FallFac
7776oveq1d 6323 . . . 4 FallFac FallFac FallFac
7875, 77sylan9eq 2525 . . 3 FallFac FallFac FallFac
79 fzfid 12224 . . . . 5
805, 14mulcld 9681 . . . . 5 FallFac FallFac
8179, 17, 80fsummulc1 13923 . . . 4 FallFac FallFac FallFac FallFac
8281adantr 472 . . 3 FallFac FallFac FallFac FallFac
8378, 82eqtrd 2505 . 2 FallFac FallFac FallFac
84 elfzelz 11826 . . . . . . . 8
85 bcpasc 12544 . . . . . . . 8
861, 84, 85syl2an 485 . . . . . . 7
8786oveq1d 6323 . . . . . 6 FallFac FallFac FallFac FallFac
881, 84, 3syl2an 485 . . . . . . . 8
8988nn0cnd 10951 . . . . . . 7
90 peano2zm 11004 . . . . . . . . . 10
9184, 90syl 17 . . . . . . . . 9
92 bccl 12545 . . . . . . . . 9
931, 91, 92syl2an 485 . . . . . . . 8
9493nn0cnd 10951 . . . . . . 7
95 elfznn0 11913 . . . . . . . . 9
9610, 95, 12syl2an 485 . . . . . . . 8 FallFac
9763, 96mulcld 9681 . . . . . . 7 FallFac FallFac
9889, 94, 97adddird 9686 . . . . . 6 FallFac FallFac FallFac FallFac FallFac FallFac
9987, 98eqtr3d 2507 . . . . 5 FallFac FallFac FallFac FallFac FallFac FallFac
10099sumeq2dv 13846 . . . 4 FallFac FallFac FallFac FallFac FallFac FallFac
101 nn0uz 11217 . . . . . . . . 9
1021, 101syl6eleq 2559 . . . . . . . 8
10389, 97mulcld 9681 . . . . . . . 8 FallFac FallFac
104 oveq2 6316 . . . . . . . . 9
105 oveq2 6316 . . . . . . . . . . 11
106105oveq2d 6324 . . . . . . . . . 10 FallFac FallFac
107 oveq2 6316 . . . . . . . . . 10 FallFac FallFac
108106, 107oveq12d 6326 . . . . . . . . 9 FallFac FallFac FallFac FallFac
109104, 108oveq12d 6326 . . . . . . . 8 FallFac FallFac FallFac FallFac
110102, 103, 109fsump1 13894 . . . . . . 7 FallFac FallFac FallFac FallFac FallFac FallFac
111 peano2nn0 10934 . . . . . . . . . . . . 13
1121, 111syl 17 . . . . . . . . . . . 12
113112nn0zd 11061 . . . . . . . . . . 11
1141nn0red 10950 . . . . . . . . . . . . 13
115114ltp1d 10559 . . . . . . . . . . . 12
116115olcd 400 . . . . . . . . . . 11
117 bcval4 12530 . . . . . . . . . . 11
1181, 113, 116, 117syl3anc 1292 . . . . . . . . . 10
119118oveq1d 6323 . . . . . . . . 9 FallFac FallFac FallFac FallFac
120112nn0cnd 10951 . . . . . . . . . . . . . 14
121120subidd 9993 . . . . . . . . . . . . 13
122121oveq2d 6324 . . . . . . . . . . . 12 FallFac FallFac
123 0nn0 10908 . . . . . . . . . . . . 13
124 fallfaccl 14146 . . . . . . . . . . . . 13 FallFac
1256, 123, 124sylancl 675 . . . . . . . . . . . 12 FallFac
126122, 125eqeltrd 2549 . . . . . . . . . . 11 FallFac
127 fallfaccl 14146 . . . . . . . . . . . 12 FallFac
12810, 112, 127syl2anc 673 . . . . . . . . . . 11 FallFac
129126, 128mulcld 9681 . . . . . . . . . 10 FallFac FallFac
130129mul02d 9849 . . . . . . . . 9 FallFac FallFac
131119, 130eqtrd 2505 . . . . . . . 8 FallFac FallFac
132131oveq2d 6324 . . . . . . 7 FallFac FallFac FallFac FallFac FallFac FallFac
13360, 103syldan 478 . . . . . . . . 9 FallFac FallFac
13479, 133fsumcl 13876 . . . . . . . 8 FallFac FallFac
135134addid1d 9851 . . . . . . 7 FallFac FallFac FallFac FallFac
136110, 132, 1353eqtrd 2509 . . . . . 6 FallFac FallFac FallFac FallFac
137112, 101syl6eleq 2559 . . . . . . . 8
13894, 97mulcld 9681 . . . . . . . 8 FallFac FallFac
139 oveq1 6315 . . . . . . . . . . 11
140 df-neg 9883 . . . . . . . . . . 11
141139, 140syl6eqr 2523 . . . . . . . . . 10
142141oveq2d 6324 . . . . . . . . 9
143 oveq2 6316 . . . . . . . . . . 11
144143oveq2d 6324 . . . . . . . . . 10 FallFac FallFac
145 oveq2 6316 . . . . . . . . . 10 FallFac FallFac
146144, 145oveq12d 6326 . . . . . . . . 9 FallFac FallFac FallFac FallFac
147142, 146oveq12d 6326 . . . . . . . 8 FallFac FallFac FallFac FallFac
148137, 138, 147fsum1p 13891 . . . . . . 7 FallFac FallFac FallFac FallFac FallFac FallFac
149 neg1z 10997 . . . . . . . . . . . 12
150 neg1lt0 10738 . . . . . . . . . . . . 13
151150orci 397 . . . . . . . . . . . 12
152 bcval4 12530 . . . . . . . . . . . 12
153149, 151, 152mp3an23 1382 . . . . . . . . . . 11
1541, 153syl 17 . . . . . . . . . 10
155154oveq1d 6323 . . . . . . . . 9 FallFac FallFac FallFac FallFac
156120subid1d 9994 . . . . . . . . . . . . 13
157156oveq2d 6324 . . . . . . . . . . . 12 FallFac FallFac
158 fallfaccl 14146 . . . . . . . . . . . . 13 FallFac
1596, 112, 158syl2anc 673 . . . . . . . . . . . 12 FallFac
160157, 159eqeltrd 2549 . . . . . . . . . . 11 FallFac
161 fallfaccl 14146 . . . . . . . . . . . 12 FallFac
16210, 123, 161sylancl 675 . . . . . . . . . . 11 FallFac
163160, 162mulcld 9681 . . . . . . . . . 10 FallFac FallFac
164163mul02d 9849 . . . . . . . . 9 FallFac FallFac
165155, 164eqtrd 2505 . . . . . . . 8 FallFac FallFac
166 1zzd 10992 . . . . . . . . . . 11
167 0zd 10973 . . . . . . . . . . 11
1686, 10, 1binomfallfaclem1 14169 . . . . . . . . . . 11 FallFac FallFac
169 oveq2 6316 . . . . . . . . . . . 12
170 oveq2 6316 . . . . . . . . . . . . . 14
171170oveq2d 6324 . . . . . . . . . . . . 13 FallFac FallFac
172 oveq1 6315 . . . . . . . . . . . . . 14
173172oveq2d 6324 . . . . . . . . . . . . 13 FallFac FallFac
174171, 173oveq12d 6326 . . . . . . . . . . . 12 FallFac FallFac FallFac FallFac
175169, 174oveq12d 6326 . . . . . . . . . . 11 FallFac FallFac FallFac FallFac
176166, 167, 55, 168, 175fsumshft 13918 . . . . . . . . . 10 FallFac FallFac FallFac FallFac
17716adantr 472 . . . . . . . . . . . . . . 15
178 elfzelz 11826 . . . . . . . . . . . . . . . . 17
179178adantl 473 . . . . . . . . . . . . . . . 16
180179zcnd 11064 . . . . . . . . . . . . . . 15
181 1cnd 9677 . . . . . . . . . . . . . . 15
182177, 180, 181subsub3d 10035 . . . . . . . . . . . . . 14
183182oveq2d 6324 . . . . . . . . . . . . 13 FallFac FallFac
184180, 181npcand 10009 . . . . . . . . . . . . . 14
185184oveq2d 6324 . . . . . . . . . . . . 13 FallFac FallFac
186183, 185oveq12d 6326 . . . . . . . . . . . 12 FallFac FallFac FallFac FallFac
187186oveq2d 6324 . . . . . . . . . . 11 FallFac FallFac FallFac FallFac
188187sumeq2dv 13846 . . . . . . . . . 10 FallFac FallFac FallFac FallFac
189176, 188eqtr2d 2506 . . . . . . . . 9 FallFac FallFac FallFac FallFac
190 oveq2 6316 . . . . . . . . . . 11
191 oveq2 6316 . . . . . . . . . . . . 13
192191oveq2d 6324 . . . . . . . . . . . 12 FallFac FallFac
193 oveq1 6315 . . . . . . . . . . . . 13
194193oveq2d 6324 . . . . . . . . . . . 12 FallFac FallFac
195192, 194oveq12d 6326 . . . . . . . . . . 11 FallFac FallFac FallFac FallFac
196190, 195oveq12d 6326 . . . . . . . . . 10 FallFac FallFac FallFac FallFac
197196cbvsumv 13839 . . . . . . . . 9 FallFac FallFac FallFac FallFac
198189, 197syl6eqr 2523 . . . . . . . 8 FallFac FallFac FallFac FallFac
199165, 198oveq12d 6326 . . . . . . 7 FallFac FallFac FallFac FallFac FallFac FallFac
2006, 10, 1binomfallfaclem1 14169 . . . . . . . . 9 FallFac FallFac
20179, 200fsumcl 13876 . . . . . . . 8 FallFac FallFac
202201addid2d 9852 . . . . . . 7 FallFac FallFac FallFac FallFac
203148, 199, 2023eqtrd 2509 . . . . . 6 FallFac FallFac FallFac FallFac
204136, 203oveq12d 6326 . . . . 5 FallFac FallFac FallFac FallFac FallFac FallFac FallFac FallFac
205 fzfid 12224 . . . . . 6
206205, 103, 138fsumadd 13882 . . . . 5 FallFac FallFac FallFac FallFac FallFac FallFac FallFac FallFac
20779, 133, 200fsumadd 13882 . . . . 5 FallFac FallFac FallFac FallFac FallFac FallFac FallFac FallFac
208204, 206, 2073eqtr4d 2515 . . . 4 FallFac FallFac FallFac FallFac FallFac FallFac FallFac FallFac
209100, 208eqtrd 2505 . . 3 FallFac FallFac FallFac FallFac FallFac FallFac
210209adantr 472 . 2 FallFac FallFac FallFac FallFac FallFac FallFac
21174, 83, 2103eqtr4d 2515 1 FallFac FallFac FallFac
 Colors of variables: wff setvar class Syntax hints:   wi 4   wo 375   wa 376   wceq 1452   wcel 1904   wss 3390   class class class wbr 4395  cfv 5589  (class class class)co 6308  cc 9555  cc0 9557  c1 9558   caddc 9560   cmul 9562   clt 9693   cmin 9880  cneg 9881  cn0 10893  cz 10961  cuz 11182  cfz 11810   cbc 12525  csu 13829   FallFac cfallfac 14134 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-inf2 8164  ax-cnex 9613  ax-resscn 9614  ax-1cn 9615  ax-icn 9616  ax-addcl 9617  ax-addrcl 9618  ax-mulcl 9619  ax-mulrcl 9620  ax-mulcom 9621  ax-addass 9622  ax-mulass 9623  ax-distr 9624  ax-i2m1 9625  ax-1ne0 9626  ax-1rid 9627  ax-rnegex 9628  ax-rrecex 9629  ax-cnre 9630  ax-pre-lttri 9631  ax-pre-lttrn 9632  ax-pre-ltadd 9633  ax-pre-mulgt0 9634  ax-pre-sup 9635 This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-fal 1458  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-int 4227  df-iun 4271  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-se 4799  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-isom 5598  df-riota 6270  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-om 6712  df-1st 6812  df-2nd 6813  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-1o 7200  df-oadd 7204  df-er 7381  df-en 7588  df-dom 7589  df-sdom 7590  df-fin 7591  df-sup 7974  df-oi 8043  df-card 8391  df-pnf 9695  df-mnf 9696  df-xr 9697  df-ltxr 9698  df-le 9699  df-sub 9882  df-neg 9883  df-div 10292  df-nn 10632  df-2 10690  df-3 10691  df-n0 10894  df-z 10962  df-uz 11183  df-rp 11326  df-fz 11811  df-fzo 11943  df-seq 12252  df-exp 12311  df-fac 12498  df-bc 12526  df-hash 12554  df-cj 13239  df-re 13240  df-im 13241  df-sqrt 13375  df-abs 13376  df-clim 13629  df-sum 13830  df-prod 14037  df-fallfac 14137 This theorem is referenced by:  binomfallfac  14171
 Copyright terms: Public domain W3C validator