Theorem uzid 12837

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

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℤ)
2		zre 12562	. . 3 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
3	2	leidd 11780	. 2 ⊢ (𝑀 ∈ ℤ → 𝑀 ≤ 𝑀)
4		eluz1 12826	. 2 ⊢ (𝑀 ∈ ℤ → (𝑀 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝑀)))
5	1, 3, 4	mpbir2and 712	1 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑀))

Syntax hints:   → wi 4   ∈ wcel 2107   class class class wbr 5149  ‘cfv 6544   ≤ cle 11249  ℤcz 12558  ℤ_≥cuz 12822

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-cnex 11166  ax-resscn 11167  ax-pre-lttri 11184

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7412  df-er 8703  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-neg 11447  df-z 12559  df-uz 12823

This theorem is referenced by:  uzidd  12838  uzn0  12839  uz11  12847  uzinfi  12912  uzsupss  12924  eluzfz1  13508  eluzfz2  13509  elfz3  13511  elfz1end  13531  fzssp1  13544  fzpred  13549  fzp1ss  13552  fzpr  13556  fztp  13557  elfz0add  13600  fzolb  13638  zpnn0elfzo  13705  fzosplitsnm1  13707  fzofzp1  13729  fzosplitsn  13740  fzostep1  13748  om2uzuzi  13914  axdc4uzlem  13948  seqf  13989  seqfveq  13992  seq1p  14002  faclbnd3  14252  bcm1k  14275  bcn2  14279  seqcoll  14425  swrds1  14616  pfxccatpfx2  14687  rexuz3  15295  r19.2uz  15298  cau3lem  15301  caubnd2  15304  climconst  15487  climuni  15496  isercoll2  15615  climsup  15616  climcau  15617  serf0  15627  iseralt  15631  fsumcvg3  15675  fsumparts  15752  o1fsum  15759  abscvgcvg  15765  isum1p  15787  isumrpcl  15789  isumsup2  15792  climcndslem1  15795  climcndslem2  15796  climcnds  15797  cvgrat  15829  mertenslem1  15830  fprodabs  15918  binomfallfaclem2  15984  fprodefsum  16038  eftlub  16052  rpnnen2lem11  16167  bitsfzo  16376  bitsinv1  16383  smupval  16429  seq1st  16508  algr0  16509  eucalg  16524  2mulprm  16630  oddprm  16743  pcfac  16832  pcbc  16833  vdwlem6  16919  prmlem0  17039  gsumprval  18607  efgsres  19606  telgsumfzs  19857  lmconst  22765  lmmo  22884  zfbas  23400  uzrest  23401  iscau2  24794  iscau4  24796  caun0  24798  caussi  24814  equivcau  24817  lmcau  24830  mbfsup  25181  mbfinf  25182  mbflimsup  25183  plyco0  25706  dvply2g  25798  geolim3  25852  aaliou3lem2  25856  aaliou3lem3  25857  ulm2  25897  ulm0  25903  ulmcaulem  25906  ulmcau  25907  ulmss  25909  ulmcn  25911  ulmdvlem3  25914  ulmdv  25915  abelthlem7  25950  2logb9irr  26300  sqrt2cxp2logb9e3  26304  ppinprm  26656  chtnprm  26658  ppiublem1  26705  chtublem  26714  chtub  26715  bposlem6  26792  lgsqr  26854  lgseisenlem4  26881  lgsquadlem1  26883  lgsquad2  26889  pntpbnd1  27089  pntlemf  27108  ostth2lem2  27137  istrkg2ld  27711  axlowdimlem17  28216  clwwlkvbij  29366  2clwwlk2  29601  numclwlk2lem2f  29630  fzdif2  32002  prmdvdsbc  32022  esumcvg  33084  dya2ub  33269  dya2icoseg  33276  sseqmw  33390  sseqf  33391  ballotlemfp1  33490  iprodefisumlem  34710  poimirlem1  36489  poimirlem2  36490  poimirlem3  36491  poimirlem4  36492  poimirlem6  36494  poimirlem7  36495  poimirlem8  36496  poimirlem9  36497  poimirlem13  36501  poimirlem14  36502  poimirlem15  36503  poimirlem16  36504  poimirlem17  36505  poimirlem18  36506  poimirlem19  36507  poimirlem20  36508  poimirlem21  36509  poimirlem22  36510  poimirlem23  36511  poimirlem24  36512  poimirlem26  36514  poimirlem27  36515  poimirlem31  36519  poimirlem32  36520  mblfinlem2  36526  sdclem1  36611  fdc  36613  seqpo  36615  incsequz2  36617  geomcau  36627  bfplem2  36691  3lexlogpow2ineq1  40923  flt4lem2  41389  eq0rabdioph  41514  rexrabdioph  41532  jm3.1lem1  41756  dvgrat  43071  rexanuz3  43785  uzfissfz  44036  allbutfi  44103  uzid2  44115  fmul01lt1lem1  44300  climinf  44322  climsuse  44324  limsupvaluz2  44454  supcnvlimsup  44456  ioodvbdlimc1lem2  44648  ioodvbdlimc2lem  44650  iblspltprt  44689  stoweidlem7  44723  wallispilem1  44781  wallispilem4  44784  dirkertrigeqlem1  44814  sge0isum  45143  sge0reuzb  45164  carageniuncllem1  45237  caratheodorylem1  45242  smflimlem1  45487  smflimlem2  45488  smflim  45493  smfsuplem1  45527  smfsuplem3  45529  smflimsuplem1  45536  smflimsuplem2  45537  iccpartres  46086  iccelpart  46101  4fppr1  46403  fldivexpfllog2  47251  nnlog2ge0lt1  47252  logbpw2m1  47253  fllog2  47254  blennnelnn  47262  blenpw2  47264  blennnt2  47275  nnolog2flm1  47276  dig2nn0ld  47290  dig2nn1st  47291  0dig2pr01  47296  aacllem  47848