Theorem uzid 12877

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 23	. 2 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℤ)
2		zre 12595	. . 3 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
3	2	leidd 11780	. 2 ⊢ (𝑀 ∈ ℤ → 𝑀 ≤ 𝑀)
4		eluz1 12866	. 2 ⊢ (𝑀 ∈ ℤ → (𝑀 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝑀)))
5	1, 3, 4	mpbir2and 725	1 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑀))

Syntax hints:   → wi 4   ∈ wcel 2149   class class class wbr 5111  ‘cfv 6537   ≤ cle 11244  ℤcz 12591  ℤ_≥cuz 12862

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5259  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733  ax-cnex 11156  ax-resscn 11157  ax-pre-lttri 11174

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-rab 3423  df-v 3463  df-sbc 3752  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4491  df-pw 4567  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7414  df-er 8694  df-en 8944  df-dom 8945  df-sdom 8946  df-pnf 11245  df-mnf 11246  df-xr 11247  df-ltxr 11248  df-le 11249  df-neg 11444  df-z 12592  df-uz 12863

This theorem is referenced by:  uzidd  12878  uzn0  12879  uz11  12887  uzinfi  12952  uzsupss  12964  eluzfz1  13559  eluzfz2  13560  elfz3  13562  elfz1end  13582  fzssp1  13595  fzpred  13600  fzp1ss  13603  fzpr  13607  fztp  13608  elfz0add  13654  fzolb  13694  zpnn0elfzo  13767  fzosplitsnm1  13769  fzofzp1  13793  fzosplitsn  13805  fzostep1  13815  om2uzuzi  13985  axdc4uzlem  14019  seqf  14059  seqfveq  14062  seq1p  14072  faclbnd3  14328  bcm1k  14351  bcn2  14355  seqcoll  14501  swrds1  14704  pfxccatpfx2  14774  rexuz3  15400  r19.2uz  15403  cau3lem  15406  caubnd2  15409  climconst  15594  climuni  15603  isercoll2  15720  climsup  15721  climcau  15722  serf0  15732  iseralt  15736  fsumcvg3  15780  fsumparts  15858  o1fsum  15865  abscvgcvg  15871  isum1p  15895  isumrpcl  15897  isumsup2  15900  climcndslem1  15903  climcndslem2  15904  climcnds  15905  cvgrat  15937  mertenslem1  15938  fprodabs  16028  binomfallfaclem2  16094  fprodefsum  16149  eftlub  16165  rpnnen2lem11  16280  bitsfzo  16493  bitsinv1  16500  smupval  16546  seq1st  16629  algr0  16630  eucalg  16645  2mulprm  16751  prmdvdsbc  16785  oddprm  16870  pcfac  16959  pcbc  16960  vdwlem6  17046  prmlem0  17165  gsumprval  18746  efgsres  19808  telgsumfzs  20059  lmconst  23387  lmmo  23506  zfbas  24022  uzrest  24023  iscau2  25405  iscau4  25407  caun0  25409  caussi  25425  equivcau  25428  lmcau  25441  mbfsup  25792  mbfinf  25793  mbflimsup  25794  plyco0  26318  dvply2g  26415  geolim3  26469  aaliou3lem2  26473  aaliou3lem3  26474  ulm2  26514  ulm0  26520  ulmcaulem  26523  ulmcau  26524  ulmss  26526  ulmcn  26528  ulmdvlem3  26531  ulmdv  26532  abelthlem7  26567  2logb9irr  26926  sqrt2cxp2logb9e3  26930  ppinprm  27282  chtnprm  27284  ppiublem1  27332  chtublem  27341  chtub  27342  bposlem6  27419  lgsqr  27481  lgseisenlem4  27508  lgsquadlem1  27510  lgsquad2  27516  pntpbnd1  27716  pntlemf  27735  ostth2lem2  27764  istrkg2ld  28695  axlowdimlem17  29249  clwwlkvbij  30405  2clwwlk2  30640  numclwlk2lem2f  30669  fzdif2  33076  esumcvg  34421  dya2ub  34605  dya2icoseg  34612  sseqmw  34726  sseqf  34727  ballotlemfp1  34827  iprodefisumlem  36165  poimirlem1  38195  poimirlem2  38196  poimirlem3  38197  poimirlem4  38198  poimirlem6  38200  poimirlem7  38201  poimirlem8  38202  poimirlem9  38203  poimirlem13  38207  poimirlem14  38208  poimirlem15  38209  poimirlem16  38210  poimirlem17  38211  poimirlem18  38212  poimirlem19  38213  poimirlem20  38214  poimirlem21  38215  poimirlem22  38216  poimirlem23  38217  poimirlem24  38218  poimirlem26  38220  poimirlem27  38221  poimirlem31  38225  poimirlem32  38226  mblfinlem2  38232  sdclem1  38317  fdc  38319  seqpo  38321  incsequz2  38323  geomcau  38333  bfplem2  38397  3lexlogpow2ineq1  42750  flt4lem2  43306  eq0rabdioph  43434  rexrabdioph  43448  jm3.1lem1  43671  dvgrat  44949  rexanuz3  45741  uzfissfz  45969  allbutfi  46035  uzid2  46046  fmul01lt1lem1  46227  climinf  46249  climsuse  46251  limsupvaluz2  46379  supcnvlimsup  46381  ioodvbdlimc1lem2  46573  ioodvbdlimc2lem  46575  iblspltprt  46614  stoweidlem7  46648  wallispilem1  46706  wallispilem4  46709  dirkertrigeqlem1  46739  sge0isum  47068  sge0reuzb  47089  carageniuncllem1  47162  caratheodorylem1  47167  smflimlem1  47412  smflimlem2  47413  smflim  47418  smfsuplem1  47452  smfsuplem3  47454  smflimsuplem1  47461  smflimsuplem2  47462  iccpartres  48091  iccelpart  48106  4fppr1  48424  pgnioedg1  48797  pgnioedg2  48798  pgnioedg3  48799  pgnioedg4  48800  pgnbgreunbgrlem1  48802  pgnbgreunbgrlem4  48808  fldivexpfllog2  49265  nnlog2ge0lt1  49266  logbpw2m1  49267  fllog2  49268  blennnelnn  49276  blenpw2  49278  blennnt2  49289  nnolog2flm1  49290  dig2nn0ld  49304  dig2nn1st  49305  0dig2pr01  49310  aacllem  50510