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

Theorem uzid 10492
Description: Membership of the least member in a set of upper 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 10278 . . . 4  |-  ( M  e.  ZZ  ->  M  e.  RR )
21leidd 9585 . . 3  |-  ( M  e.  ZZ  ->  M  <_  M )
32ancli 535 . 2  |-  ( M  e.  ZZ  ->  ( M  e.  ZZ  /\  M  <_  M ) )
4 eluz1 10484 . 2  |-  ( M  e.  ZZ  ->  ( M  e.  ( ZZ>= `  M )  <->  ( M  e.  ZZ  /\  M  <_  M ) ) )
53, 4mpbird 224 1  |-  ( M  e.  ZZ  ->  M  e.  ( ZZ>= `  M )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1725   class class class wbr 4204   ` cfv 5446    <_ cle 9113   ZZcz 10274   ZZ>=cuz 10480
This theorem is referenced by:  uzn0  10493  uz11  10500  uzinfmi  10547  uzsupss  10560  eluzfz1  11056  eluzfz2  11057  elfz3  11059  elfz1end  11073  fzssp1  11087  fzp1ss  11090  fzpr  11093  fztp  11094  fzolb  11137  fzofzp1  11181  fzosplitsn  11187  fzostep1  11189  om2uzuzi  11281  axdc4uzlem  11313  seqf  11336  seqfveq  11339  seq1p  11349  faclbnd3  11575  bcm1k  11598  bcn2  11602  seqcoll  11704  ccatass  11742  swrdccat1  11766  swrdccat2  11767  splfv1  11776  splval2  11778  swrds1  11779  revccat  11790  rexuz3  12144  r19.2uz  12147  cau3lem  12150  caubnd2  12153  climconst  12329  climuni  12338  isercoll2  12454  climsup  12455  climcau  12456  serf0  12466  iseralt  12470  fsumcvg3  12515  fsumparts  12577  o1fsum  12584  abscvgcvg  12590  isum1p  12613  isumrpcl  12615  isumsup2  12618  climcndslem1  12621  climcndslem2  12622  climcnds  12623  cvgrat  12652  mertenslem1  12653  eftlub  12702  rpnnen2lem11  12816  bitsfzo  12939  bitsinv1  12946  smupval  12992  seq1st  13054  algr0  13055  eucalg  13070  oddprm  13181  pcfac  13260  pcbc  13261  vdwlem6  13346  prmlem0  13420  gsumccat  14779  efginvrel2  15351  efgsres  15362  lmconst  17317  lmmo  17436  zfbas  17920  uzrest  17921  iscau2  19222  iscau4  19224  caun0  19226  caussi  19242  equivcau  19245  lmcau  19257  mbfsup  19548  mbfinf  19549  mbflimsup  19550  plyco0  20103  dvply2g  20194  geolim3  20248  aaliou3lem2  20252  aaliou3lem3  20253  ulm2  20293  ulm0  20299  ulmcaulem  20302  ulmcau  20303  ulmss  20305  ulmcn  20307  ulmdvlem3  20310  ulmdv  20311  abelthlem7  20346  ppinprm  20927  chtnprm  20929  ppiublem1  20978  chtublem  20987  chtub  20988  bposlem6  21065  lgsqr  21122  lgseisenlem4  21128  lgsquadlem1  21130  lgsquad2  21136  pntpbnd1  21272  pntlemf  21291  ostth2lem2  21320  3v3e3cycl1  21623  esumcvg  24468  dya2ub  24612  dya2icoseg  24619  ballotlemfp1  24741  ntrivcvgn0  25218  fprodabs  25289  fprodefsum  25290  iprodefisumlem  25309  binomfallfaclem2  25348  axlowdimlem17  25889  mblfinlem  26234  sdclem1  26438  fdc  26440  seqpo  26442  incsequz2  26444  geomcau  26456  bfplem2  26523  eq0rabdioph  26826  rexrabdioph  26845  jm3.1lem1  27079  fmul01lt1lem1  27681  climinf  27699  climsuse  27701  stoweidlem7  27723  wallispilem1  27781  wallispilem4  27784  fzosplitsnm1  28114
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4693  ax-cnex 9038  ax-resscn 9039  ax-pre-lttri 9056
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-nel 2601  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-sbc 3154  df-csb 3244  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-br 4205  df-opab 4259  df-mpt 4260  df-id 4490  df-xp 4876  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-rn 4881  df-res 4882  df-ima 4883  df-iota 5410  df-fun 5448  df-fn 5449  df-f 5450  df-f1 5451  df-fo 5452  df-f1o 5453  df-fv 5454  df-ov 6076  df-er 6897  df-en 7102  df-dom 7103  df-sdom 7104  df-pnf 9114  df-mnf 9115  df-xr 9116  df-ltxr 9117  df-le 9118  df-neg 9286  df-z 10275  df-uz 10481
  Copyright terms: Public domain W3C validator