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

Theorem uzid 11740
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 11419 . . . 4 (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
21leidd 10632 . . 3 (𝑀 ∈ ℤ → 𝑀𝑀)
32ancli 573 . 2 (𝑀 ∈ ℤ → (𝑀 ∈ ℤ ∧ 𝑀𝑀))
4 eluz1 11729 . 2 (𝑀 ∈ ℤ → (𝑀 ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑀𝑀)))
53, 4mpbird 247 1 (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ𝑀))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 2030   class class class wbr 4685  cfv 5926  cle 10113  cz 11415  cuz 11725
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-pre-lttri 10048
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-ov 6693  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-neg 10307  df-z 11416  df-uz 11726
This theorem is referenced by:  uzn0  11741  uz11  11748  uzinfi  11806  uzsupss  11818  eluzfz1  12386  eluzfz2  12387  elfz3  12389  elfz1end  12409  fzssp1  12422  fzpred  12427  fzp1ss  12430  fzpr  12434  fztp  12435  elfz0add  12477  fzolb  12515  zpnn0elfzo  12580  fzosplitsnm1  12582  fzofzp1  12605  fzosplitsn  12616  fzostep1  12624  om2uzuzi  12788  axdc4uzlem  12822  seqf  12862  seqfveq  12865  seq1p  12875  faclbnd3  13119  bcm1k  13142  bcn2  13146  seqcoll  13286  ccatass  13406  ccatrn  13407  swrds1  13497  swrdccat1  13503  swrdccat2  13504  splfv1  13552  splval2  13554  revccat  13561  rexuz3  14132  r19.2uz  14135  cau3lem  14138  caubnd2  14141  climconst  14318  climuni  14327  isercoll2  14443  climsup  14444  climcau  14445  serf0  14455  iseralt  14459  fsumcvg3  14504  fsumparts  14582  o1fsum  14589  abscvgcvg  14595  isum1p  14617  isumrpcl  14619  isumsup2  14622  climcndslem1  14625  climcndslem2  14626  climcnds  14627  cvgrat  14659  mertenslem1  14660  ntrivcvgn0  14674  fprodabs  14748  binomfallfaclem2  14815  fprodefsum  14869  eftlub  14883  rpnnen2lem11  14997  bitsfzo  15204  bitsinv1  15211  smupval  15257  seq1st  15331  algr0  15332  eucalg  15347  oddprm  15562  pcfac  15650  pcbc  15651  vdwlem6  15737  prmlem0  15859  gsumprval  17328  gsumccat  17425  efginvrel2  18186  efgsres  18197  telgsumfzs  18432  lmconst  21113  lmmo  21232  zfbas  21747  uzrest  21748  iscau2  23121  iscau4  23123  caun0  23125  caussi  23141  equivcau  23144  lmcau  23157  mbfsup  23476  mbfinf  23477  mbflimsup  23478  plyco0  23993  dvply2g  24085  geolim3  24139  aaliou3lem2  24143  aaliou3lem3  24144  ulm2  24184  ulm0  24190  ulmcaulem  24193  ulmcau  24194  ulmss  24196  ulmcn  24198  ulmdvlem3  24201  ulmdv  24202  abelthlem7  24237  ppinprm  24923  chtnprm  24925  ppiublem1  24972  chtublem  24981  chtub  24982  bposlem6  25059  lgsqr  25121  lgseisenlem4  25148  lgsquadlem1  25150  lgsquad2  25156  pntpbnd1  25320  pntlemf  25339  ostth2lem2  25368  istrkg2ld  25404  axlowdimlem17  25883  clwwlkvbij  27088  clwwlkvbijOLD  27089  2clwwlk2  27336  numclwlk2lem2f  27357  numclwlk2lem2fOLD  27364  fzdif2  29679  esumcvg  30276  dya2ub  30460  dya2icoseg  30467  sseqmw  30581  sseqf  30582  ballotlemfp1  30681  signstfvp  30776  iprodefisumlem  31752  poimirlem1  33540  poimirlem2  33541  poimirlem3  33542  poimirlem4  33543  poimirlem6  33545  poimirlem7  33546  poimirlem8  33547  poimirlem9  33548  poimirlem13  33552  poimirlem14  33553  poimirlem15  33554  poimirlem16  33555  poimirlem17  33556  poimirlem18  33557  poimirlem19  33558  poimirlem20  33559  poimirlem21  33560  poimirlem22  33561  poimirlem23  33562  poimirlem24  33563  poimirlem26  33565  poimirlem27  33566  poimirlem31  33570  poimirlem32  33571  mblfinlem2  33577  sdclem1  33669  fdc  33671  seqpo  33673  incsequz2  33675  geomcau  33685  bfplem2  33752  eq0rabdioph  37657  rexrabdioph  37675  jm3.1lem1  37901  dvgrat  38828  rexanuz3  39589  uzfissfz  39855  allbutfi  39929  uzid2  39943  uzidd  39944  fmul01lt1lem1  40134  climinf  40156  climsuse  40158  limsupvaluz2  40288  supcnvlimsup  40290  ioodvbdlimc1lem2  40465  ioodvbdlimc2lem  40467  iblspltprt  40507  stoweidlem7  40542  wallispilem1  40600  wallispilem4  40603  dirkertrigeqlem1  40633  sge0isum  40962  sge0reuzb  40983  carageniuncllem1  41056  caratheodorylem1  41061  smflimlem1  41300  smflimlem2  41301  smflim  41306  smfsuplem1  41338  smfsuplem3  41340  smflimsuplem1  41347  smflimsuplem2  41348  iccpartres  41679  iccelpart  41694  pfxccat1  41735  pfxccatpfx2  41753  fldivexpfllog2  42684  nnlog2ge0lt1  42685  logbpw2m1  42686  fllog2  42687  blennnelnn  42695  blenpw2  42697  blennnt2  42708  nnolog2flm1  42709  dig2nn0ld  42723  dig2nn1st  42724  0dig2pr01  42729  aacllem  42875
  Copyright terms: Public domain W3C validator