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

Theorem elfzuz 11803
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 11801 . 2  |-  ( K  e.  ( M ... N )  <->  ( K  e.  ( ZZ>= `  M )  /\  N  e.  ( ZZ>=
`  K ) ) )
21simplbi 462 1  |-  ( K  e.  ( M ... N )  ->  K  e.  ( ZZ>= `  M )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1889   ` cfv 5585  (class class class)co 6295   ZZ>=cuz 11166   ...cfz 11791
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-8 1891  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-sep 4528  ax-nul 4537  ax-pow 4584  ax-pr 4642  ax-un 6588  ax-cnex 9600  ax-resscn 9601
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 987  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-eu 2305  df-mo 2306  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-ral 2744  df-rex 2745  df-rab 2748  df-v 3049  df-sbc 3270  df-csb 3366  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3734  df-if 3884  df-pw 3955  df-sn 3971  df-pr 3973  df-op 3977  df-uni 4202  df-iun 4283  df-br 4406  df-opab 4465  df-mpt 4466  df-id 4752  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5549  df-fun 5587  df-fn 5588  df-f 5589  df-fv 5593  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-1st 6798  df-2nd 6799  df-neg 9868  df-z 10945  df-uz 11167  df-fz 11792
This theorem is referenced by:  elfzel1  11806  elfzelz  11807  elfzle1  11809  eluzfz2b  11815  fzsplit2  11831  fzsplit  11832  fzopth  11842  fzss1  11844  fzss2  11845  fzssuz  11846  fzp1elp1  11856  uzsplit  11873  elfzmlbm  11907  predfz  11921  fzosplit  11958  seqf2  12239  seqfeq2  12243  seqfeq  12245  sermono  12252  seqf1olem2  12260  seqz  12268  seqfeq3  12270  ser0  12272  seqcoll  12634  swrdval2  12783  swrd0val  12784  swrdswrd  12823  swrdccatin12  12854  splid  12867  spllen  12868  splfv1  12869  limsupgre  13554  limsupgreOLD  13555  clim2ser  13730  clim2ser2  13731  isermulc2  13733  iserle  13735  climub  13737  isercolllem1  13740  isercolllem3  13742  isercoll2  13744  iseraltlem1  13760  fsumcvg  13790  fsumser  13808  isumclim3  13832  isumadd  13840  fsump1i  13842  fsum0diaglem  13849  o1fsum  13885  iserabs  13887  cvgcmp  13888  cvgcmpub  13889  cvgcmpce  13890  isumsplit  13910  isum1p  13911  isumsup2  13916  climcndslem1  13919  climcndslem2  13920  climcnds  13921  geoserg  13936  mertenslem1  13952  clim2div  13957  prodf1  13959  prodfn0  13962  ntrivcvgmullem  13969  fprodcvg  13996  fprodntriv  14008  fprodabs  14040  fprodeq0  14041  iprodclim3  14065  iprodmul  14068  fprodefsum  14161  prmind2  14647  prmdvdsfz  14661  pcfac  14856  prmreclem4  14875  prmreclem5  14876  prmgaplem1  15019  prmgaplem2  15020  prmgaplcmlem2  15022  prmgaplcmlem2OLD  15025  prmgapprmorlemOLD  15029  prmgapprmolem  15044  efgtlen  17388  efgredleme  17405  efgredlemc  17407  frgpuplem  17434  ovolunlem1a  22461  ovolicc1  22481  uniioombllem3  22555  dvfsumrlimf  22989  dvfsumlem1  22990  dvfsumlem2  22991  dvfsumlem3  22992  dvfsumlem4  22993  dvfsum2  22998  coeidlem  23203  coeid3  23206  vieta1lem2  23276  mtest  23371  mtestbdd  23372  birthdaylem2  23890  wilth  24008  ftalem4  24012  ftalem5  24013  ftalem4OLD  24014  ftalem5OLD  24015  chtub  24152  mersenne  24167  bposlem6  24229  lgsdilem2  24271  rplogsumlem1  24334  rplogsumlem2  24335  dchrisumlem2  24340  dchrisum0lem1  24366  logdivbnd  24406  pntrsumbnd2  24417  pntrlog2bndlem1  24427  pntpbnd1  24436  pntpbnd2  24437  pntlemh  24449  pntlemj  24453  axlowdimlem17  25000  fzsplit3  28382  ballotlemfrci  29372  ballotlemfrciOLD  29410  wrdsplex  29439  subfacp1lem3  29917  poimirlem1  31953  poimirlem2  31954  poimirlem31  31983  poimirlem32  31984  mblfinlem2  31990  mettrifi  32098  geomcau  32100  elfzfzo  37496  fmulcl  37669  fmuldfeqlem1  37670  iblspltprt  37860  itgspltprt  37866  stoweidlem11  37881  stoweidlem17  37887  stirlinglem7  37952  fourierdlem15  37994  fourierdlem25  38004  sge0isum  38279  iundjiun  38308  carageniuncllem1  38352  carageniuncllem2  38353  caratheodorylem1  38357  iccpartgt  38751  pfxccatin12  38976  pfxccatpfx2  38979  ssfz12  39064
  Copyright terms: Public domain W3C validator