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

Theorem uzid 11106
Description: Membership of the least member in an upper set of integers. (Contributed by NM, 2-Sep-2005.)
Assertion
Ref Expression
uzid  |-  ( M  e.  ZZ  ->  M  e.  ( ZZ>= `  M )
)

Proof of Theorem uzid
StepHypRef Expression
1 zre 10875 . . . 4  |-  ( M  e.  ZZ  ->  M  e.  RR )
21leidd 10126 . . 3  |-  ( M  e.  ZZ  ->  M  <_  M )
32ancli 551 . 2  |-  ( M  e.  ZZ  ->  ( M  e.  ZZ  /\  M  <_  M ) )
4 eluz1 11096 . 2  |-  ( M  e.  ZZ  ->  ( M  e.  ( ZZ>= `  M )  <->  ( M  e.  ZZ  /\  M  <_  M ) ) )
53, 4mpbird 232 1  |-  ( M  e.  ZZ  ->  M  e.  ( ZZ>= `  M )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1804   class class class wbr 4437   ` cfv 5578    <_ cle 9632   ZZcz 10871   ZZ>=cuz 11092
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577  ax-cnex 9551  ax-resscn 9552  ax-pre-lttri 9569
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 975  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-nel 2641  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-opab 4496  df-mpt 4497  df-id 4785  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-fv 5586  df-ov 6284  df-er 7313  df-en 7519  df-dom 7520  df-sdom 7521  df-pnf 9633  df-mnf 9634  df-xr 9635  df-ltxr 9636  df-le 9637  df-neg 9813  df-z 10872  df-uz 11093
This theorem is referenced by:  uzn0  11107  uz11  11114  uzinfmi  11172  uzsupss  11185  eluzfz1  11704  eluzfz2  11705  elfz3  11707  elfz1end  11726  fzssp1  11737  fzpred  11739  fzp1ss  11742  fzpr  11746  fztp  11747  elfz0add  11786  fzolb  11816  zpnn0elfzo  11870  fzosplitsnm1  11872  fzofzp1  11891  fzosplitsn  11900  fzostep1  11904  om2uzuzi  12042  axdc4uzlem  12074  seqf  12110  seqfveq  12113  seq1p  12123  faclbnd3  12352  bcm1k  12375  bcn2  12379  seqcoll  12494  ccatass  12587  ccatrn  12588  swrds1  12658  swrdccat1  12664  swrdccat2  12665  splfv1  12713  splval2  12715  revccat  12722  rexuz3  13163  r19.2uz  13166  cau3lem  13169  caubnd2  13172  climconst  13348  climuni  13357  isercoll2  13473  climsup  13474  climcau  13475  serf0  13485  iseralt  13489  fsumcvg3  13533  fsumparts  13602  o1fsum  13609  abscvgcvg  13615  isum1p  13635  isumrpcl  13637  isumsup2  13640  climcndslem1  13643  climcndslem2  13644  climcnds  13645  cvgrat  13674  mertenslem1  13675  ntrivcvgn0  13689  fprodabs  13760  fprodefsum  13812  eftlub  13826  rpnnen2lem11  13940  bitsfzo  14067  bitsinv1  14074  smupval  14120  seq1st  14182  algr0  14183  eucalg  14198  oddprm  14321  pcfac  14400  pcbc  14401  vdwlem6  14486  prmlem0  14573  gsumprval  15887  gsumccat  15988  efginvrel2  16724  efgsres  16735  telgsumfzs  16997  lmconst  19740  lmmo  19859  zfbas  20375  uzrest  20376  iscau2  21694  iscau4  21696  caun0  21698  caussi  21714  equivcau  21717  lmcau  21729  mbfsup  22049  mbfinf  22050  mbflimsup  22051  plyco0  22567  dvply2g  22659  geolim3  22713  aaliou3lem2  22717  aaliou3lem3  22718  ulm2  22758  ulm0  22764  ulmcaulem  22767  ulmcau  22768  ulmss  22770  ulmcn  22772  ulmdvlem3  22775  ulmdv  22776  abelthlem7  22811  ppinprm  23404  chtnprm  23406  ppiublem1  23455  chtublem  23464  chtub  23465  bposlem6  23542  lgsqr  23599  lgseisenlem4  23605  lgsquadlem1  23607  lgsquad2  23613  pntpbnd1  23749  pntlemf  23768  ostth2lem2  23797  istrkg2ld  23836  axlowdimlem17  24239  3v3e3cycl1  24622  clwwlkvbij  24779  numclwlk2lem2f  25081  esumcvg  28070  dya2ub  28219  dya2icoseg  28226  sseqmw  28308  sseqf  28309  ballotlemfp1  28408  signstfvp  28506  iprodefisumlem  29099  binomfallfaclem2  29138  mblfinlem2  30028  sdclem1  30212  fdc  30214  seqpo  30216  incsequz2  30218  geomcau  30228  bfplem2  30295  eq0rabdioph  30686  rexrabdioph  30703  jm3.1lem1  30935  dvgrat  31169  fmul01lt1lem1  31532  climinf  31566  climsuse  31568  ioodvbdlimc1lem2  31683  ioodvbdlimc2lem  31685  iblspltprt  31726  stoweidlem7  31743  wallispilem1  31801  wallispilem4  31804  dirkertrigeqlem1  31834
  Copyright terms: Public domain W3C validator