Theorem uzid 12526

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 12253	. . 3 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
3	2	leidd 11471	. 2 ⊢ (𝑀 ∈ ℤ → 𝑀 ≤ 𝑀)
4		eluz1 12515	. 2 ⊢ (𝑀 ∈ ℤ → (𝑀 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝑀)))
5	1, 3, 4	mpbir2and 709	1 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑀))

Syntax hints:   → wi 4   ∈ wcel 2108   class class class wbr 5070  ‘cfv 6418   ≤ cle 10941  ℤcz 12249  ℤ_≥cuz 12511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-cnex 10858  ax-resscn 10859  ax-pre-lttri 10876

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-ov 7258  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-pnf 10942  df-mnf 10943  df-xr 10944  df-ltxr 10945  df-le 10946  df-neg 11138  df-z 12250  df-uz 12512

This theorem is referenced by:  uzidd  12527  uzn0  12528  uz11  12536  uzinfi  12597  uzsupss  12609  eluzfz1  13192  eluzfz2  13193  elfz3  13195  elfz1end  13215  fzssp1  13228  fzpred  13233  fzp1ss  13236  fzpr  13240  fztp  13241  elfz0add  13284  fzolb  13322  zpnn0elfzo  13388  fzosplitsnm1  13390  fzofzp1  13412  fzosplitsn  13423  fzostep1  13431  om2uzuzi  13597  axdc4uzlem  13631  seqf  13672  seqfveq  13675  seq1p  13685  faclbnd3  13934  bcm1k  13957  bcn2  13961  seqcoll  14106  swrds1  14307  pfxccatpfx2  14378  rexuz3  14988  r19.2uz  14991  cau3lem  14994  caubnd2  14997  climconst  15180  climuni  15189  isercoll2  15308  climsup  15309  climcau  15310  serf0  15320  iseralt  15324  fsumcvg3  15369  fsumparts  15446  o1fsum  15453  abscvgcvg  15459  isum1p  15481  isumrpcl  15483  isumsup2  15486  climcndslem1  15489  climcndslem2  15490  climcnds  15491  cvgrat  15523  mertenslem1  15524  fprodabs  15612  binomfallfaclem2  15678  fprodefsum  15732  eftlub  15746  rpnnen2lem11  15861  bitsfzo  16070  bitsinv1  16077  smupval  16123  seq1st  16204  algr0  16205  eucalg  16220  2mulprm  16326  oddprm  16439  pcfac  16528  pcbc  16529  vdwlem6  16615  prmlem0  16735  gsumprval  18287  gsumccatOLD  18394  efgsres  19259  telgsumfzs  19505  lmconst  22320  lmmo  22439  zfbas  22955  uzrest  22956  iscau2  24346  iscau4  24348  caun0  24350  caussi  24366  equivcau  24369  lmcau  24382  mbfsup  24733  mbfinf  24734  mbflimsup  24735  plyco0  25258  dvply2g  25350  geolim3  25404  aaliou3lem2  25408  aaliou3lem3  25409  ulm2  25449  ulm0  25455  ulmcaulem  25458  ulmcau  25459  ulmss  25461  ulmcn  25463  ulmdvlem3  25466  ulmdv  25467  abelthlem7  25502  2logb9irr  25850  sqrt2cxp2logb9e3  25854  ppinprm  26206  chtnprm  26208  ppiublem1  26255  chtublem  26264  chtub  26265  bposlem6  26342  lgsqr  26404  lgseisenlem4  26431  lgsquadlem1  26433  lgsquad2  26439  pntpbnd1  26639  pntlemf  26658  ostth2lem2  26687  istrkg2ld  26725  axlowdimlem17  27229  clwwlkvbij  28378  2clwwlk2  28613  numclwlk2lem2f  28642  fzdif2  31014  prmdvdsbc  31032  esumcvg  31954  dya2ub  32137  dya2icoseg  32144  sseqmw  32258  sseqf  32259  ballotlemfp1  32358  iprodefisumlem  33612  poimirlem1  35705  poimirlem2  35706  poimirlem3  35707  poimirlem4  35708  poimirlem6  35710  poimirlem7  35711  poimirlem8  35712  poimirlem9  35713  poimirlem13  35717  poimirlem14  35718  poimirlem15  35719  poimirlem16  35720  poimirlem17  35721  poimirlem18  35722  poimirlem19  35723  poimirlem20  35724  poimirlem21  35725  poimirlem22  35726  poimirlem23  35727  poimirlem24  35728  poimirlem26  35730  poimirlem27  35731  poimirlem31  35735  poimirlem32  35736  mblfinlem2  35742  sdclem1  35828  fdc  35830  seqpo  35832  incsequz2  35834  geomcau  35844  bfplem2  35908  3lexlogpow2ineq1  39994  flt4lem2  40400  eq0rabdioph  40514  rexrabdioph  40532  jm3.1lem1  40755  dvgrat  41819  rexanuz3  42535  uzfissfz  42755  allbutfi  42823  uzid2  42835  fmul01lt1lem1  43015  climinf  43037  climsuse  43039  limsupvaluz2  43169  supcnvlimsup  43171  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  iblspltprt  43404  stoweidlem7  43438  wallispilem1  43496  wallispilem4  43499  dirkertrigeqlem1  43529  sge0isum  43855  sge0reuzb  43876  carageniuncllem1  43949  caratheodorylem1  43954  smflimlem1  44193  smflimlem2  44194  smflim  44199  smfsuplem1  44231  smfsuplem3  44233  smflimsuplem1  44240  smflimsuplem2  44241  iccpartres  44758  iccelpart  44773  4fppr1  45075  fldivexpfllog2  45799  nnlog2ge0lt1  45800  logbpw2m1  45801  fllog2  45802  blennnelnn  45810  blenpw2  45812  blennnt2  45823  nnolog2flm1  45824  dig2nn0ld  45838  dig2nn1st  45839  0dig2pr01  45844  aacllem  46391