Theorem uzid 12750

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 12475	. . 3 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
3	2	leidd 11686	. 2 ⊢ (𝑀 ∈ ℤ → 𝑀 ≤ 𝑀)
4		eluz1 12739	. 2 ⊢ (𝑀 ∈ ℤ → (𝑀 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝑀)))
5	1, 3, 4	mpbir2and 713	1 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑀))

Syntax hints:   → wi 4   ∈ wcel 2109   class class class wbr 5092  ‘cfv 6482   ≤ cle 11150  ℤcz 12471  ℤ_≥cuz 12735

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-cnex 11065  ax-resscn 11066  ax-pre-lttri 11083

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-ov 7352  df-er 8625  df-en 8873  df-dom 8874  df-sdom 8875  df-pnf 11151  df-mnf 11152  df-xr 11153  df-ltxr 11154  df-le 11155  df-neg 11350  df-z 12472  df-uz 12736

This theorem is referenced by:  uzidd  12751  uzn0  12752  uz11  12760  uzinfi  12829  uzsupss  12841  eluzfz1  13434  eluzfz2  13435  elfz3  13437  elfz1end  13457  fzssp1  13470  fzpred  13475  fzp1ss  13478  fzpr  13482  fztp  13483  elfz0add  13529  fzolb  13568  zpnn0elfzo  13641  fzosplitsnm1  13643  fzofzp1  13667  fzosplitsn  13678  fzostep1  13686  om2uzuzi  13856  axdc4uzlem  13890  seqf  13930  seqfveq  13933  seq1p  13943  faclbnd3  14199  bcm1k  14222  bcn2  14226  seqcoll  14371  swrds1  14573  pfxccatpfx2  14643  rexuz3  15256  r19.2uz  15259  cau3lem  15262  caubnd2  15265  climconst  15450  climuni  15459  isercoll2  15576  climsup  15577  climcau  15578  serf0  15588  iseralt  15592  fsumcvg3  15636  fsumparts  15713  o1fsum  15720  abscvgcvg  15726  isum1p  15748  isumrpcl  15750  isumsup2  15753  climcndslem1  15756  climcndslem2  15757  climcnds  15758  cvgrat  15790  mertenslem1  15791  fprodabs  15881  binomfallfaclem2  15947  fprodefsum  16002  eftlub  16018  rpnnen2lem11  16133  bitsfzo  16346  bitsinv1  16353  smupval  16399  seq1st  16482  algr0  16483  eucalg  16498  2mulprm  16604  prmdvdsbc  16637  oddprm  16722  pcfac  16811  pcbc  16812  vdwlem6  16898  prmlem0  17017  gsumprval  18562  efgsres  19617  telgsumfzs  19868  lmconst  23146  lmmo  23265  zfbas  23781  uzrest  23782  iscau2  25175  iscau4  25177  caun0  25179  caussi  25195  equivcau  25198  lmcau  25211  mbfsup  25563  mbfinf  25564  mbflimsup  25565  plyco0  26095  dvply2g  26190  dvply2gOLD  26191  geolim3  26245  aaliou3lem2  26249  aaliou3lem3  26250  ulm2  26292  ulm0  26298  ulmcaulem  26301  ulmcau  26302  ulmss  26304  ulmcn  26306  ulmdvlem3  26309  ulmdv  26310  abelthlem7  26346  2logb9irr  26703  sqrt2cxp2logb9e3  26707  ppinprm  27060  chtnprm  27062  ppiublem1  27111  chtublem  27120  chtub  27121  bposlem6  27198  lgsqr  27260  lgseisenlem4  27287  lgsquadlem1  27289  lgsquad2  27295  pntpbnd1  27495  pntlemf  27514  ostth2lem2  27543  istrkg2ld  28409  axlowdimlem17  28907  clwwlkvbij  30061  2clwwlk2  30296  numclwlk2lem2f  30325  fzdif2  32742  esumcvg  34069  dya2ub  34254  dya2icoseg  34261  sseqmw  34375  sseqf  34376  ballotlemfp1  34476  iprodefisumlem  35733  poimirlem1  37621  poimirlem2  37622  poimirlem3  37623  poimirlem4  37624  poimirlem6  37626  poimirlem7  37627  poimirlem8  37628  poimirlem9  37629  poimirlem13  37633  poimirlem14  37634  poimirlem15  37635  poimirlem16  37636  poimirlem17  37637  poimirlem18  37638  poimirlem19  37639  poimirlem20  37640  poimirlem21  37641  poimirlem22  37642  poimirlem23  37643  poimirlem24  37644  poimirlem26  37646  poimirlem27  37647  poimirlem31  37651  poimirlem32  37652  mblfinlem2  37658  sdclem1  37743  fdc  37745  seqpo  37747  incsequz2  37749  geomcau  37759  bfplem2  37823  3lexlogpow2ineq1  42051  flt4lem2  42640  eq0rabdioph  42769  rexrabdioph  42787  jm3.1lem1  43010  dvgrat  44305  rexanuz3  45094  uzfissfz  45326  allbutfi  45392  uzid2  45404  fmul01lt1lem1  45585  climinf  45607  climsuse  45609  limsupvaluz2  45739  supcnvlimsup  45741  ioodvbdlimc1lem2  45933  ioodvbdlimc2lem  45935  iblspltprt  45974  stoweidlem7  46008  wallispilem1  46066  wallispilem4  46069  dirkertrigeqlem1  46099  sge0isum  46428  sge0reuzb  46449  carageniuncllem1  46522  caratheodorylem1  46527  smflimlem1  46772  smflimlem2  46773  smflim  46778  smfsuplem1  46812  smfsuplem3  46814  smflimsuplem1  46821  smflimsuplem2  46822  iccpartres  47422  iccelpart  47437  4fppr1  47739  pgnioedg1  48112  pgnioedg2  48113  pgnioedg3  48114  pgnioedg4  48115  pgnbgreunbgrlem1  48117  pgnbgreunbgrlem4  48123  fldivexpfllog2  48570  nnlog2ge0lt1  48571  logbpw2m1  48572  fllog2  48573  blennnelnn  48581  blenpw2  48583  blennnt2  48594  nnolog2flm1  48595  dig2nn0ld  48609  dig2nn1st  48610  0dig2pr01  48615  aacllem  49806