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

Theorem uzid 10820
Description: Membership of the least member in a set of upper integers. (Contributed by NM, 2-Sep-2005.)
Assertion
Ref Expression
uzid

Proof of Theorem uzid
StepHypRef Expression
1 zre 10595 . . . 4
21leidd 9852 . . 3
32ancli 538 . 2
4 eluz1 10810 . 2
53, 4mpbird 226 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 362  e.wcel 1749   class class class wbr 4267  `cfv 5390   cle 9365   cz 10591   cuz 10806
This theorem is referenced by:  uzn0  10821  uz11  10828  uzinfmi  10879  uzsupss  10892  eluzfz1  11402  eluzfz2  11403  elfz3  11405  elfz1end  11423  fzssp1  11445  fzp1ss  11448  fzpr  11453  fztp  11454  fzolb  11499  fzosplitsnm1  11549  fzofzp1  11565  fzosplitsn  11574  fzostep1  11576  om2uzuzi  11713  axdc4uzlem  11745  seqf  11768  seqfveq  11771  seq1p  11781  faclbnd3  12009  bcm1k  12032  bcn2  12036  seqcoll  12157  ccatass  12227  swrds1  12286  swrdccat1  12292  swrdccat2  12293  splfv1  12338  splval2  12340  revccat  12347  rexuz3  12777  r19.2uz  12780  cau3lem  12783  caubnd2  12786  climconst  12962  climuni  12971  isercoll2  13087  climsup  13088  climcau  13089  serf0  13099  iseralt  13103  fsumcvg3  13147  fsumparts  13209  o1fsum  13216  abscvgcvg  13222  isum1p  13244  isumrpcl  13246  isumsup2  13249  climcndslem1  13252  climcndslem2  13253  climcnds  13254  cvgrat  13283  mertenslem1  13284  eftlub  13333  rpnnen2lem11  13447  bitsfzo  13571  bitsinv1  13578  smupval  13624  seq1st  13686  algr0  13687  eucalg  13702  oddprm  13822  pcfac  13901  pcbc  13902  vdwlem6  13987  prmlem0  14073  gsumprval  15451  gsumccat  15456  efginvrel2  16161  efgsres  16172  lmconst  18569  lmmo  18688  zfbas  19173  uzrest  19174  iscau2  20488  iscau4  20490  caun0  20492  caussi  20508  equivcau  20511  lmcau  20523  mbfsup  20842  mbfinf  20843  mbflimsup  20844  plyco0  21401  dvply2g  21492  geolim3  21546  aaliou3lem2  21550  aaliou3lem3  21551  ulm2  21591  ulm0  21597  ulmcaulem  21600  ulmcau  21601  ulmss  21603  ulmcn  21605  ulmdvlem3  21608  ulmdv  21609  abelthlem7  21644  ppinprm  22231  chtnprm  22233  ppiublem1  22282  chtublem  22291  chtub  22292  bposlem6  22369  lgsqr  22426  lgseisenlem4  22432  lgsquadlem1  22434  lgsquad2  22440  pntpbnd1  22576  pntlemf  22595  ostth2lem2  22624  axlowdimlem17  22883  3v3e3cycl1  23209  esumcvg  26244  dya2ub  26394  dya2icoseg  26401  sseqmw  26477  sseqf  26478  ballotlemfp1  26577  signstfvp  26675  ntrivcvgn0  27115  fprodabs  27186  fprodefsum  27187  iprodefisumlem  27206  binomfallfaclem2  27245  mblfinlem2  28100  sdclem1  28310  fdc  28312  seqpo  28314  incsequz2  28316  geomcau  28326  bfplem2  28393  eq0rabdioph  28788  rexrabdioph  28805  jm3.1lem1  29039  fmul01lt1lem1  29438  climinf  29453  climsuse  29455  stoweidlem7  29476  wallispilem1  29534  wallispilem4  29537  zpnn0elfzo  29895  clwwlkvbij  30137  numclwlk2lem2f  30370
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-8 1751  ax-9 1753  ax-10 1768  ax-11 1773  ax-12 1785  ax-13 1934  ax-ext 2403  ax-sep 4388  ax-nul 4396  ax-pow 4442  ax-pr 4503  ax-un 6342  ax-cnex 9284  ax-resscn 9285  ax-pre-lttri 9302
This theorem depends on definitions:  df-bi 179  df-or 363  df-an 364  df-3or 951  df-3an 952  df-tru 1355  df-ex 1582  df-nf 1585  df-sb 1694  df-eu 2248  df-mo 2249  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2547  df-ne 2587  df-nel 2588  df-ral 2699  df-rex 2700  df-rab 2703  df-v 2953  df-sbc 3165  df-csb 3266  df-dif 3308  df-un 3310  df-in 3312  df-ss 3319  df-nul 3615  df-if 3769  df-pw 3839  df-sn 3859  df-pr 3860  df-op 3862  df-uni 4067  df-br 4268  df-opab 4326  df-mpt 4327  df-id 4607  df-xp 4817  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-rn 4822  df-res 4823  df-ima 4824  df-iota 5353  df-fun 5392  df-fn 5393  df-f 5394  df-f1 5395  df-fo 5396  df-f1o 5397  df-fv 5398  df-ov 6064  df-er 7062  df-en 7270  df-dom 7271  df-sdom 7272  df-pnf 9366  df-mnf 9367  df-xr 9368  df-ltxr 9369  df-le 9370  df-neg 9544  df-z 10592  df-uz 10807
  Copyright terms: Public domain W3C validator