Theorem uzid 12792

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 12517	. . 3 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
3	2	leidd 11705	. 2 ⊢ (𝑀 ∈ ℤ → 𝑀 ≤ 𝑀)
4		eluz1 12781	. 2 ⊢ (𝑀 ∈ ℤ → (𝑀 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝑀)))
5	1, 3, 4	mpbir2and 714	1 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑀))

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5074  ‘cfv 6487   ≤ cle 11169  ℤcz 12513  ℤ_≥cuz 12777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2184  ax-ext 2707  ax-sep 5220  ax-nul 5230  ax-pow 5296  ax-pr 5364  ax-un 7678  ax-cnex 11083  ax-resscn 11084  ax-pre-lttri 11101

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2538  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-ne 2931  df-nel 3035  df-ral 3050  df-rex 3060  df-rab 3388  df-v 3429  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4264  df-if 4457  df-pw 4533  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-br 5075  df-opab 5137  df-mpt 5156  df-id 5515  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-iota 6443  df-fun 6489  df-fn 6490  df-f 6491  df-f1 6492  df-fo 6493  df-f1o 6494  df-fv 6495  df-ov 7359  df-er 8632  df-en 8883  df-dom 8884  df-sdom 8885  df-pnf 11170  df-mnf 11171  df-xr 11172  df-ltxr 11173  df-le 11174  df-neg 11369  df-z 12514  df-uz 12778

This theorem is referenced by:  uzidd  12793  uzn0  12794  uz11  12802  uzinfi  12867  uzsupss  12879  eluzfz1  13474  eluzfz2  13475  elfz3  13477  elfz1end  13497  fzssp1  13510  fzpred  13515  fzp1ss  13518  fzpr  13522  fztp  13523  elfz0add  13569  fzolb  13609  zpnn0elfzo  13682  fzosplitsnm1  13684  fzofzp1  13708  fzosplitsn  13720  fzostep1  13730  om2uzuzi  13900  axdc4uzlem  13934  seqf  13974  seqfveq  13977  seq1p  13987  faclbnd3  14243  bcm1k  14266  bcn2  14270  seqcoll  14415  swrds1  14618  pfxccatpfx2  14688  rexuz3  15300  r19.2uz  15303  cau3lem  15306  caubnd2  15309  climconst  15494  climuni  15503  isercoll2  15620  climsup  15621  climcau  15622  serf0  15632  iseralt  15636  fsumcvg3  15680  fsumparts  15758  o1fsum  15765  abscvgcvg  15771  isum1p  15795  isumrpcl  15797  isumsup2  15800  climcndslem1  15803  climcndslem2  15804  climcnds  15805  cvgrat  15837  mertenslem1  15838  fprodabs  15928  binomfallfaclem2  15994  fprodefsum  16049  eftlub  16065  rpnnen2lem11  16180  bitsfzo  16393  bitsinv1  16400  smupval  16446  seq1st  16529  algr0  16530  eucalg  16545  2mulprm  16651  prmdvdsbc  16685  oddprm  16770  pcfac  16859  pcbc  16860  vdwlem6  16946  prmlem0  17065  gsumprval  18645  efgsres  19702  telgsumfzs  19953  lmconst  23214  lmmo  23333  zfbas  23849  uzrest  23850  iscau2  25232  iscau4  25234  caun0  25236  caussi  25252  equivcau  25255  lmcau  25268  mbfsup  25619  mbfinf  25620  mbflimsup  25621  plyco0  26145  dvply2g  26239  geolim3  26293  aaliou3lem2  26297  aaliou3lem3  26298  ulm2  26338  ulm0  26344  ulmcaulem  26347  ulmcau  26348  ulmss  26350  ulmcn  26352  ulmdvlem3  26355  ulmdv  26356  abelthlem7  26391  2logb9irr  26747  sqrt2cxp2logb9e3  26751  ppinprm  27103  chtnprm  27105  ppiublem1  27153  chtublem  27162  chtub  27163  bposlem6  27240  lgsqr  27302  lgseisenlem4  27329  lgsquadlem1  27331  lgsquad2  27337  pntpbnd1  27537  pntlemf  27556  ostth2lem2  27585  istrkg2ld  28516  axlowdimlem17  29015  clwwlkvbij  30171  2clwwlk2  30406  numclwlk2lem2f  30435  fzdif2  32851  esumcvg  34218  dya2ub  34402  dya2icoseg  34409  sseqmw  34523  sseqf  34524  ballotlemfp1  34624  iprodefisumlem  35910  poimirlem1  37930  poimirlem2  37931  poimirlem3  37932  poimirlem4  37933  poimirlem6  37935  poimirlem7  37936  poimirlem8  37937  poimirlem9  37938  poimirlem13  37942  poimirlem14  37943  poimirlem15  37944  poimirlem16  37945  poimirlem17  37946  poimirlem18  37947  poimirlem19  37948  poimirlem20  37949  poimirlem21  37950  poimirlem22  37951  poimirlem23  37952  poimirlem24  37953  poimirlem26  37955  poimirlem27  37956  poimirlem31  37960  poimirlem32  37961  mblfinlem2  37967  sdclem1  38052  fdc  38054  seqpo  38056  incsequz2  38058  geomcau  38068  bfplem2  38132  3lexlogpow2ineq1  42485  flt4lem2  43068  eq0rabdioph  43196  rexrabdioph  43210  jm3.1lem1  43433  dvgrat  44727  rexanuz3  45514  uzfissfz  45744  allbutfi  45810  uzid2  45821  fmul01lt1lem1  46002  climinf  46024  climsuse  46026  limsupvaluz2  46154  supcnvlimsup  46156  ioodvbdlimc1lem2  46348  ioodvbdlimc2lem  46350  iblspltprt  46389  stoweidlem7  46423  wallispilem1  46481  wallispilem4  46484  dirkertrigeqlem1  46514  sge0isum  46843  sge0reuzb  46864  carageniuncllem1  46937  caratheodorylem1  46942  smflimlem1  47187  smflimlem2  47188  smflim  47193  smfsuplem1  47227  smfsuplem3  47229  smflimsuplem1  47236  smflimsuplem2  47237  iccpartres  47866  iccelpart  47881  4fppr1  48199  pgnioedg1  48572  pgnioedg2  48573  pgnioedg3  48574  pgnioedg4  48575  pgnbgreunbgrlem1  48577  pgnbgreunbgrlem4  48583  fldivexpfllog2  49029  nnlog2ge0lt1  49030  logbpw2m1  49031  fllog2  49032  blennnelnn  49040  blenpw2  49042  blennnt2  49053  nnolog2flm1  49054  dig2nn0ld  49068  dig2nn1st  49069  0dig2pr01  49074  aacllem  50264