Theorem elfzle2 12345

Description: A member of a finite set of sequential integer is less than or equal to the upper bound. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)

Assertion

Ref	Expression
elfzle2	|- ( K e. ( M ... N ) -> K <_ N )

Proof of Theorem elfzle2

Step	Hyp	Ref	Expression
1		elfzuz3 12339	. 2 |- ( K e. ( M ... N ) -> N e. ( ZZ>= ` K ) )
2		eluzle 11700	. 2 |- ( N e. ( ZZ>= ` K ) -> K <_ N )
3	1, 2	syl 17	1 |- ( K e. ( M ... N ) -> K <_ N )

Syntax hints:   -> wi 4   e. wcel 1990   class class class wbr 4653   ` cfv 5888  (class class class)co 6650   <_ cle 10075   ZZ>=cuz 11687   ...cfz 12326

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-1st 7168  df-2nd 7169  df-neg 10269  df-z 11378  df-uz 11688  df-fz 12327

This theorem is referenced by:  elfz1eq  12352  fzdisj  12368  ssfzunsnext  12386  fznatpl1  12395  fzp1disj  12399  uzdisj  12413  fzneuz  12421  fznuz  12422  elfzmlbm  12449  difelfznle  12453  nn0disj  12455  seqf1olem1  12840  seqf1olem2  12841  bcval4  13094  bcp1nk  13104  hashf1  13241  seqcoll  13248  seqcoll2  13249  isercolllem2  14396  isercoll  14398  summolem2a  14446  fsum0diaglem  14508  mertenslem1  14616  prodmolem2a  14664  binomrisefac  14773  bpoly4  14790  fzm1ndvds  15044  prmind2  15398  prmdvdsfz  15417  isprm7  15420  hashdvds  15480  prmdiveq  15491  prmreclem3  15622  prmreclem5  15624  4sqlem11  15659  4sqlem12  15660  vdwlem1  15685  vdwlem3  15687  vdwlem6  15690  vdwlem9  15693  vdwlem10  15694  strlemor1OLD  15969  mndodconglem  17960  oddvds  17966  gexdvds  17999  coe1tmmul  19647  lebnumii  22765  ovolicc2lem4  23288  voliunlem1  23318  dvfsumle  23784  dvfsumge  23785  dvfsumabs  23786  dvfsumlem3  23791  elply2  23952  coeeq2  23998  aaliou3lem6  24103  birthdaylem2  24679  birthdaylem3  24680  wilthlem1  24794  ftalem5  24803  basellem1  24807  basellem3  24809  ppiprm  24877  chtprm  24879  logfac2  24942  lgsval2lem  25032  lgsqrlem2  25072  lgseisenlem1  25100  lgseisenlem2  25101  lgseisenlem3  25102  lgsquadlem1  25105  lgsquadlem2  25106  2lgslem1a  25116  chebbnd1lem1  25158  dchrvmasumiflem1  25190  mulog2sumlem2  25224  pntrlog2bndlem6  25272  pntpbnd1  25275  pntpbnd2  25276  pntlemh  25288  pntlemj  25292  pntlemf  25294  axlowdimlem16  25837  crctcshwlkn0lem2  26703  crctcshlem4  26712  bcm1n  29554  psgnfzto1stlem  29850  smatrcl  29862  submateqlem1  29873  madjusmdetlem2  29894  ballotlemimin  30567  ballotlemsdom  30573  ballotlemsel1i  30574  ballotlemsima  30577  ballotlemfrceq  30590  ballotlemfrcn0  30591  fsum2dsub  30685  reprgt  30699  breprexplemc  30710  erdszelem8  31180  cvmliftlem2  31268  cvmliftlem7  31273  supfz  31613  bcprod  31624  bccolsum  31625  poimirlem2  33411  poimirlem3  33412  poimirlem4  33413  poimirlem6  33415  poimirlem7  33416  poimirlem8  33417  poimirlem12  33421  poimirlem13  33422  poimirlem14  33423  poimirlem15  33424  poimirlem16  33425  poimirlem17  33426  poimirlem19  33428  poimirlem20  33429  poimirlem21  33430  poimirlem22  33431  poimirlem23  33432  poimirlem24  33433  poimirlem26  33435  poimirlem28  33437  poimirlem29  33438  poimirlem31  33440  poimirlem32  33441  mblfinlem2  33447  irrapxlem3  37388  irrapxlem4  37389  fzmaxdif  37548  jm2.23  37563  jm2.26lem3  37568  jm2.27dlem2  37577  binomcxplemnn0  38548  monoords  39511  elfzolem1  39537  fmul01lt1lem1  39816  fmul01lt1lem2  39817  sumnnodd  39862  dvnmul  40158  dvnprodlem1  40161  dvnprodlem2  40162  iblspltprt  40189  itgspltprt  40195  stoweidlem3  40220  stoweidlem17  40234  stoweidlem20  40237  stoweidlem26  40243  stoweidlem34  40251  fourierdlem11  40335  fourierdlem12  40336  fourierdlem15  40339  fourierdlem25  40349  fourierdlem41  40365  fourierdlem48  40371  fourierdlem49  40372  fourierdlem50  40373  fourierdlem52  40375  fourierdlem54  40377  fourierdlem79  40402  fourierdlem102  40425  fourierdlem114  40437  elaa2lem  40450  etransclem23  40474  etransclem28  40479  etransclem35  40486  etransclem38  40489  iundjiun  40677  2elfz2melfz  41328  elfzelfzlble  41331  iccpartgt  41363  fmtno4prm  41487  difmodm1lt  42317