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

Theorem elfzuz 11687
Description: A member of a finite set of sequential integers belongs to an upper set of integers. (Contributed by NM, 17-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
Assertion
Ref Expression
elfzuz  |-  ( K  e.  ( M ... N )  ->  K  e.  ( ZZ>= `  M )
)

Proof of Theorem elfzuz
StepHypRef Expression
1 elfzuzb 11685 . 2  |-  ( K  e.  ( M ... N )  <->  ( K  e.  ( ZZ>= `  M )  /\  N  e.  ( ZZ>=
`  K ) ) )
21simplbi 458 1  |-  ( K  e.  ( M ... N )  ->  K  e.  ( ZZ>= `  M )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1823   ` cfv 5570  (class class class)co 6270   ZZ>=cuz 11082   ...cfz 11675
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565  ax-cnex 9537  ax-resscn 9538
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-iun 4317  df-br 4440  df-opab 4498  df-mpt 4499  df-id 4784  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-fv 5578  df-ov 6273  df-oprab 6274  df-mpt2 6275  df-1st 6773  df-2nd 6774  df-neg 9799  df-z 10861  df-uz 11083  df-fz 11676
This theorem is referenced by:  elfzel1  11690  elfzelz  11691  elfzle1  11692  eluzfz2b  11698  fzsplit2  11713  fzsplit  11714  fzopth  11724  fzss1  11726  fzss2  11727  fzssuz  11728  fzp1elp1  11737  uzsplit  11754  elfzmlbm  11788  fzosplit  11835  seqf2  12111  seqfeq2  12115  seqfeq  12117  sermono  12124  seqf1olem2  12132  seqz  12140  seqfeq3  12142  ser0  12144  seqcoll  12499  swrdval2  12639  swrd0val  12640  swrdswrd  12679  swrdccatin12  12710  splid  12723  spllen  12724  splfv1  12725  limsupgre  13389  clim2ser  13562  clim2ser2  13563  isermulc2  13565  iserle  13567  climub  13569  isercolllem1  13572  isercolllem3  13574  isercoll2  13576  iseraltlem1  13589  fsumcvg  13619  fsumser  13637  isumclim3  13659  isumadd  13667  fsump1i  13669  fsum0diaglem  13676  o1fsum  13712  iserabs  13714  cvgcmp  13715  cvgcmpub  13716  cvgcmpce  13717  isumsplit  13737  isum1p  13738  isumsup2  13743  climcndslem1  13746  climcndslem2  13747  climcnds  13748  geoserg  13762  mertenslem1  13778  clim2div  13783  prodf1  13785  prodfn0  13788  ntrivcvgmullem  13795  fprodcvg  13822  fprodntriv  13834  fprodabs  13863  fprodeq0  13864  iprodclim3  13878  iprodmul  13881  fprodefsum  13915  prmind2  14315  pcfac  14505  prmreclem4  14524  prmreclem5  14525  efgtlen  16946  efgredleme  16963  efgredlemc  16965  frgpuplem  16992  ovolunlem1a  22076  ovolicc1  22096  uniioombllem3  22163  dvfsumrlimf  22595  dvfsumlem1  22596  dvfsumlem2  22597  dvfsumlem3  22598  dvfsumlem4  22599  dvfsum2  22604  coeidlem  22803  coeid3  22806  vieta1lem2  22876  mtest  22968  mtestbdd  22969  birthdaylem2  23483  wilth  23546  ftalem4  23550  ftalem5  23551  chtub  23688  mersenne  23703  bposlem6  23765  lgsdilem2  23807  rplogsumlem1  23870  rplogsumlem2  23871  dchrisumlem2  23876  dchrisum0lem1  23902  logdivbnd  23942  pntrsumbnd2  23953  pntrlog2bndlem1  23963  pntpbnd1  23972  pntpbnd2  23973  pntlemh  23985  pntlemj  23989  axlowdimlem17  24466  fzsplit3  27836  ballotlemfrci  28733  wrdsplex  28762  subfacp1lem3  28893  predfz  29526  mblfinlem2  30295  mettrifi  30493  geomcau  30495  elfzfzo  31701  fmulcl  31817  fmuldfeqlem1  31818  iblspltprt  32014  itgspltprt  32020  stoweidlem11  32035  stoweidlem17  32041  stirlinglem7  32104  fourierdlem15  32146  fourierdlem25  32156  pfxccatin12  32672  pfxccatpfx2  32675  ssfz12  32723
  Copyright terms: Public domain W3C validator