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

Theorem uzid 12246
Description: Membership of the least member in an upper set of integers. (Contributed by NM, 2-Sep-2005.)
Assertion
Ref Expression
uzid (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ𝑀))

Proof of Theorem uzid
StepHypRef Expression
1 zre 11973 . . . 4 (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
21leidd 11194 . . 3 (𝑀 ∈ ℤ → 𝑀𝑀)
32ancli 549 . 2 (𝑀 ∈ ℤ → (𝑀 ∈ ℤ ∧ 𝑀𝑀))
4 eluz1 12235 . 2 (𝑀 ∈ ℤ → (𝑀 ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑀𝑀)))
53, 4mpbird 258 1 (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ𝑀))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wcel 2105   class class class wbr 5057  cfv 6348  cle 10664  cz 11969  cuz 12231
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-cnex 10581  ax-resscn 10582  ax-pre-lttri 10599
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-ov 7148  df-er 8278  df-en 8498  df-dom 8499  df-sdom 8500  df-pnf 10665  df-mnf 10666  df-xr 10667  df-ltxr 10668  df-le 10669  df-neg 10861  df-z 11970  df-uz 12232
This theorem is referenced by:  uzidd  12247  uzn0  12248  uz11  12255  uzinfi  12316  uzsupss  12328  eluzfz1  12902  eluzfz2  12903  elfz3  12905  elfz1end  12925  fzssp1  12938  fzpred  12943  fzp1ss  12946  fzpr  12950  fztp  12951  elfz0add  12994  fzolb  13032  zpnn0elfzo  13098  fzosplitsnm1  13100  fzofzp1  13122  fzosplitsn  13133  fzostep1  13141  om2uzuzi  13305  axdc4uzlem  13339  seqf  13379  seqfveq  13382  seq1p  13392  faclbnd3  13640  bcm1k  13663  bcn2  13667  seqcoll  13810  swrds1  14016  pfxccatpfx2  14087  rexuz3  14696  r19.2uz  14699  cau3lem  14702  caubnd2  14705  climconst  14888  climuni  14897  isercoll2  15013  climsup  15014  climcau  15015  serf0  15025  iseralt  15029  fsumcvg3  15074  fsumparts  15149  o1fsum  15156  abscvgcvg  15162  isum1p  15184  isumrpcl  15186  isumsup2  15189  climcndslem1  15192  climcndslem2  15193  climcnds  15194  cvgrat  15227  mertenslem1  15228  ntrivcvgn0  15242  fprodabs  15316  binomfallfaclem2  15382  fprodefsum  15436  eftlub  15450  rpnnen2lem11  15565  bitsfzo  15772  bitsinv1  15779  smupval  15825  seq1st  15903  algr0  15904  eucalg  15919  2mulprm  16025  oddprm  16135  pcfac  16223  pcbc  16224  vdwlem6  16310  prmlem0  16427  gsumprval  17886  gsumccatOLD  17993  efgsres  18793  telgsumfzs  19038  lmconst  21797  lmmo  21916  zfbas  22432  uzrest  22433  iscau2  23807  iscau4  23809  caun0  23811  caussi  23827  equivcau  23830  lmcau  23843  mbfsup  24192  mbfinf  24193  mbflimsup  24194  plyco0  24709  dvply2g  24801  geolim3  24855  aaliou3lem2  24859  aaliou3lem3  24860  ulm2  24900  ulm0  24906  ulmcaulem  24909  ulmcau  24910  ulmss  24912  ulmcn  24914  ulmdvlem3  24917  ulmdv  24918  abelthlem7  24953  2logb9irr  25300  sqrt2cxp2logb9e3  25304  ppinprm  25656  chtnprm  25658  ppiublem1  25705  chtublem  25714  chtub  25715  bposlem6  25792  lgsqr  25854  lgseisenlem4  25881  lgsquadlem1  25883  lgsquad2  25889  pntpbnd1  26089  pntlemf  26108  ostth2lem2  26137  istrkg2ld  26173  axlowdimlem17  26671  clwwlkvbij  27819  2clwwlk2  28054  numclwlk2lem2f  28083  fzdif2  30440  prmdvdsbc  30458  esumcvg  31244  dya2ub  31427  dya2icoseg  31434  sseqmw  31548  sseqf  31549  ballotlemfp1  31648  iprodefisumlem  32869  poimirlem1  34774  poimirlem2  34775  poimirlem3  34776  poimirlem4  34777  poimirlem6  34779  poimirlem7  34780  poimirlem8  34781  poimirlem9  34782  poimirlem13  34786  poimirlem14  34787  poimirlem15  34788  poimirlem16  34789  poimirlem17  34790  poimirlem18  34791  poimirlem19  34792  poimirlem20  34793  poimirlem21  34794  poimirlem22  34795  poimirlem23  34796  poimirlem24  34797  poimirlem26  34799  poimirlem27  34800  poimirlem31  34804  poimirlem32  34805  mblfinlem2  34811  sdclem1  34899  fdc  34901  seqpo  34903  incsequz2  34905  geomcau  34915  bfplem2  34982  eq0rabdioph  39251  rexrabdioph  39269  jm3.1lem1  39492  dvgrat  40521  rexanuz3  41239  uzfissfz  41470  allbutfi  41541  uzid2  41554  fmul01lt1lem1  41741  climinf  41763  climsuse  41765  limsupvaluz2  41895  supcnvlimsup  41897  ioodvbdlimc1lem2  42093  ioodvbdlimc2lem  42095  iblspltprt  42134  stoweidlem7  42169  wallispilem1  42227  wallispilem4  42230  dirkertrigeqlem1  42260  sge0isum  42586  sge0reuzb  42607  carageniuncllem1  42680  caratheodorylem1  42685  smflimlem1  42924  smflimlem2  42925  smflim  42930  smfsuplem1  42962  smfsuplem3  42964  smflimsuplem1  42971  smflimsuplem2  42972  iccpartres  43455  iccelpart  43470  4fppr1  43777  fldivexpfllog2  44553  nnlog2ge0lt1  44554  logbpw2m1  44555  fllog2  44556  blennnelnn  44564  blenpw2  44566  blennnt2  44577  nnolog2flm1  44578  dig2nn0ld  44592  dig2nn1st  44593  0dig2pr01  44598  aacllem  44830
  Copyright terms: Public domain W3C validator