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

Theorem uzid 12257
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 11984 . . . 4 (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
21leidd 11205 . . 3 (𝑀 ∈ ℤ → 𝑀𝑀)
32ancli 551 . 2 (𝑀 ∈ ℤ → (𝑀 ∈ ℤ ∧ 𝑀𝑀))
4 eluz1 12246 . 2 (𝑀 ∈ ℤ → (𝑀 ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑀𝑀)))
53, 4mpbird 259 1 (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ𝑀))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398  wcel 2110   class class class wbr 5065  cfv 6354  cle 10675  cz 11980  cuz 12242
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5202  ax-nul 5209  ax-pow 5265  ax-pr 5329  ax-un 7460  ax-cnex 10592  ax-resscn 10593  ax-pre-lttri 10610
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4838  df-br 5066  df-opab 5128  df-mpt 5146  df-id 5459  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-fv 6362  df-ov 7158  df-er 8288  df-en 8509  df-dom 8510  df-sdom 8511  df-pnf 10676  df-mnf 10677  df-xr 10678  df-ltxr 10679  df-le 10680  df-neg 10872  df-z 11981  df-uz 12243
This theorem is referenced by:  uzidd  12258  uzn0  12259  uz11  12266  uzinfi  12327  uzsupss  12339  eluzfz1  12913  eluzfz2  12914  elfz3  12916  elfz1end  12936  fzssp1  12949  fzpred  12954  fzp1ss  12957  fzpr  12961  fztp  12962  elfz0add  13005  fzolb  13043  zpnn0elfzo  13109  fzosplitsnm1  13111  fzofzp1  13133  fzosplitsn  13144  fzostep1  13152  om2uzuzi  13316  axdc4uzlem  13350  seqf  13390  seqfveq  13393  seq1p  13403  faclbnd3  13651  bcm1k  13674  bcn2  13678  seqcoll  13821  swrds1  14027  pfxccatpfx2  14098  rexuz3  14707  r19.2uz  14710  cau3lem  14713  caubnd2  14716  climconst  14899  climuni  14908  isercoll2  15024  climsup  15025  climcau  15026  serf0  15036  iseralt  15040  fsumcvg3  15085  fsumparts  15160  o1fsum  15167  abscvgcvg  15173  isum1p  15195  isumrpcl  15197  isumsup2  15200  climcndslem1  15203  climcndslem2  15204  climcnds  15205  cvgrat  15238  mertenslem1  15239  ntrivcvgn0  15253  fprodabs  15327  binomfallfaclem2  15393  fprodefsum  15447  eftlub  15461  rpnnen2lem11  15576  bitsfzo  15783  bitsinv1  15790  smupval  15836  seq1st  15914  algr0  15915  eucalg  15930  2mulprm  16036  oddprm  16146  pcfac  16234  pcbc  16235  vdwlem6  16321  prmlem0  16438  gsumprval  17897  gsumccatOLD  18004  efgsres  18863  telgsumfzs  19108  lmconst  21868  lmmo  21987  zfbas  22503  uzrest  22504  iscau2  23879  iscau4  23881  caun0  23883  caussi  23899  equivcau  23902  lmcau  23915  mbfsup  24264  mbfinf  24265  mbflimsup  24266  plyco0  24781  dvply2g  24873  geolim3  24927  aaliou3lem2  24931  aaliou3lem3  24932  ulm2  24972  ulm0  24978  ulmcaulem  24981  ulmcau  24982  ulmss  24984  ulmcn  24986  ulmdvlem3  24989  ulmdv  24990  abelthlem7  25025  2logb9irr  25372  sqrt2cxp2logb9e3  25376  ppinprm  25728  chtnprm  25730  ppiublem1  25777  chtublem  25786  chtub  25787  bposlem6  25864  lgsqr  25926  lgseisenlem4  25953  lgsquadlem1  25955  lgsquad2  25961  pntpbnd1  26161  pntlemf  26180  ostth2lem2  26209  istrkg2ld  26245  axlowdimlem17  26743  clwwlkvbij  27891  2clwwlk2  28126  numclwlk2lem2f  28155  fzdif2  30513  prmdvdsbc  30531  esumcvg  31345  dya2ub  31528  dya2icoseg  31535  sseqmw  31649  sseqf  31650  ballotlemfp1  31749  iprodefisumlem  32972  poimirlem1  34892  poimirlem2  34893  poimirlem3  34894  poimirlem4  34895  poimirlem6  34897  poimirlem7  34898  poimirlem8  34899  poimirlem9  34900  poimirlem13  34904  poimirlem14  34905  poimirlem15  34906  poimirlem16  34907  poimirlem17  34908  poimirlem18  34909  poimirlem19  34910  poimirlem20  34911  poimirlem21  34912  poimirlem22  34913  poimirlem23  34914  poimirlem24  34915  poimirlem26  34917  poimirlem27  34918  poimirlem31  34922  poimirlem32  34923  mblfinlem2  34929  sdclem1  35017  fdc  35019  seqpo  35021  incsequz2  35023  geomcau  35033  bfplem2  35100  eq0rabdioph  39371  rexrabdioph  39389  jm3.1lem1  39612  dvgrat  40642  rexanuz3  41360  uzfissfz  41592  allbutfi  41663  uzid2  41676  fmul01lt1lem1  41863  climinf  41885  climsuse  41887  limsupvaluz2  42017  supcnvlimsup  42019  ioodvbdlimc1lem2  42215  ioodvbdlimc2lem  42217  iblspltprt  42256  stoweidlem7  42291  wallispilem1  42349  wallispilem4  42352  dirkertrigeqlem1  42382  sge0isum  42708  sge0reuzb  42729  carageniuncllem1  42802  caratheodorylem1  42807  smflimlem1  43046  smflimlem2  43047  smflim  43052  smfsuplem1  43084  smfsuplem3  43086  smflimsuplem1  43093  smflimsuplem2  43094  iccpartres  43577  iccelpart  43592  4fppr1  43899  fldivexpfllog2  44624  nnlog2ge0lt1  44625  logbpw2m1  44626  fllog2  44627  blennnelnn  44635  blenpw2  44637  blennnt2  44648  nnolog2flm1  44649  dig2nn0ld  44663  dig2nn1st  44664  0dig2pr01  44669  aacllem  44901
  Copyright terms: Public domain W3C validator