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

Theorem elfzuz 11796
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 11794 . 2  |-  ( K  e.  ( M ... N )  <->  ( K  e.  ( ZZ>= `  M )  /\  N  e.  ( ZZ>=
`  K ) ) )
21simplbi 461 1  |-  ( K  e.  ( M ... N )  ->  K  e.  ( ZZ>= `  M )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1868   ` cfv 5597  (class class class)co 6301   ZZ>=cuz 11159   ...cfz 11784
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593  ax-cnex 9595  ax-resscn 9596
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-id 4764  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-iota 5561  df-fun 5599  df-fn 5600  df-f 5601  df-fv 5605  df-ov 6304  df-oprab 6305  df-mpt2 6306  df-1st 6803  df-2nd 6804  df-neg 9863  df-z 10938  df-uz 11160  df-fz 11785
This theorem is referenced by:  elfzel1  11799  elfzelz  11800  elfzle1  11802  eluzfz2b  11808  fzsplit2  11824  fzsplit  11825  fzopth  11835  fzss1  11837  fzss2  11838  fzssuz  11839  fzp1elp1  11849  uzsplit  11866  elfzmlbm  11900  predfz  11914  fzosplit  11951  seqf2  12231  seqfeq2  12235  seqfeq  12237  sermono  12244  seqf1olem2  12252  seqz  12260  seqfeq3  12262  ser0  12264  seqcoll  12624  swrdval2  12766  swrd0val  12767  swrdswrd  12806  swrdccatin12  12837  splid  12850  spllen  12851  splfv1  12852  limsupgre  13529  limsupgreOLD  13530  clim2ser  13705  clim2ser2  13706  isermulc2  13708  iserle  13710  climub  13712  isercolllem1  13715  isercolllem3  13717  isercoll2  13719  iseraltlem1  13735  fsumcvg  13765  fsumser  13783  isumclim3  13807  isumadd  13815  fsump1i  13817  fsum0diaglem  13824  o1fsum  13860  iserabs  13862  cvgcmp  13863  cvgcmpub  13864  cvgcmpce  13865  isumsplit  13885  isum1p  13886  isumsup2  13891  climcndslem1  13894  climcndslem2  13895  climcnds  13896  geoserg  13911  mertenslem1  13927  clim2div  13932  prodf1  13934  prodfn0  13937  ntrivcvgmullem  13944  fprodcvg  13971  fprodntriv  13983  fprodabs  14015  fprodeq0  14016  iprodclim3  14040  iprodmul  14043  fprodefsum  14136  prmind2  14622  prmdvdsfz  14636  pcfac  14831  prmreclem4  14850  prmreclem5  14851  prmgaplem1  14994  prmgaplem2  14995  prmgaplcmlem2  14997  prmgaplcmlem2OLD  15000  prmgapprmorlemOLD  15004  prmgapprmolem  15019  efgtlen  17363  efgredleme  17380  efgredlemc  17382  frgpuplem  17409  ovolunlem1a  22435  ovolicc1  22455  uniioombllem3  22529  dvfsumrlimf  22963  dvfsumlem1  22964  dvfsumlem2  22965  dvfsumlem3  22966  dvfsumlem4  22967  dvfsum2  22972  coeidlem  23177  coeid3  23180  vieta1lem2  23250  mtest  23345  mtestbdd  23346  birthdaylem2  23864  wilth  23982  ftalem4  23986  ftalem5  23987  ftalem4OLD  23988  ftalem5OLD  23989  chtub  24126  mersenne  24141  bposlem6  24203  lgsdilem2  24245  rplogsumlem1  24308  rplogsumlem2  24309  dchrisumlem2  24314  dchrisum0lem1  24340  logdivbnd  24380  pntrsumbnd2  24391  pntrlog2bndlem1  24401  pntpbnd1  24410  pntpbnd2  24411  pntlemh  24423  pntlemj  24427  axlowdimlem17  24974  fzsplit3  28363  ballotlemfrci  29355  ballotlemfrciOLD  29393  wrdsplex  29422  subfacp1lem3  29900  poimirlem1  31854  poimirlem2  31855  poimirlem31  31884  poimirlem32  31885  mblfinlem2  31891  mettrifi  31999  geomcau  32001  elfzfzo  37327  fmulcl  37478  fmuldfeqlem1  37479  iblspltprt  37669  itgspltprt  37675  stoweidlem11  37690  stoweidlem17  37696  stirlinglem7  37761  fourierdlem15  37803  fourierdlem25  37813  sge0isum  38056  iundjiun  38076  carageniuncllem1  38120  carageniuncllem2  38121  caratheodorylem1  38125  iccpartgt  38452  pfxccatin12  38677  pfxccatpfx2  38680  ssfz12  38742
  Copyright terms: Public domain W3C validator