Theorem uzid 12780

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

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5100  ‘cfv 6502   ≤ cle 11181  ℤcz 12502  ℤ_≥cuz 12765

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 2185  ax-ext 2709  ax-sep 5245  ax-nul 5255  ax-pow 5314  ax-pr 5381  ax-un 7692  ax-cnex 11096  ax-resscn 11097  ax-pre-lttri 11114

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5529  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6458  df-fun 6504  df-fn 6505  df-f 6506  df-f1 6507  df-fo 6508  df-f1o 6509  df-fv 6510  df-ov 7373  df-er 8647  df-en 8898  df-dom 8899  df-sdom 8900  df-pnf 11182  df-mnf 11183  df-xr 11184  df-ltxr 11185  df-le 11186  df-neg 11381  df-z 12503  df-uz 12766

This theorem is referenced by:  uzidd  12781  uzn0  12782  uz11  12790  uzinfi  12855  uzsupss  12867  eluzfz1  13461  eluzfz2  13462  elfz3  13464  elfz1end  13484  fzssp1  13497  fzpred  13502  fzp1ss  13505  fzpr  13509  fztp  13510  elfz0add  13556  fzolb  13595  zpnn0elfzo  13668  fzosplitsnm1  13670  fzofzp1  13694  fzosplitsn  13706  fzostep1  13716  om2uzuzi  13886  axdc4uzlem  13920  seqf  13960  seqfveq  13963  seq1p  13973  faclbnd3  14229  bcm1k  14252  bcn2  14256  seqcoll  14401  swrds1  14604  pfxccatpfx2  14674  rexuz3  15286  r19.2uz  15289  cau3lem  15292  caubnd2  15295  climconst  15480  climuni  15489  isercoll2  15606  climsup  15607  climcau  15608  serf0  15618  iseralt  15622  fsumcvg3  15666  fsumparts  15743  o1fsum  15750  abscvgcvg  15756  isum1p  15778  isumrpcl  15780  isumsup2  15783  climcndslem1  15786  climcndslem2  15787  climcnds  15788  cvgrat  15820  mertenslem1  15821  fprodabs  15911  binomfallfaclem2  15977  fprodefsum  16032  eftlub  16048  rpnnen2lem11  16163  bitsfzo  16376  bitsinv1  16383  smupval  16429  seq1st  16512  algr0  16513  eucalg  16528  2mulprm  16634  prmdvdsbc  16667  oddprm  16752  pcfac  16841  pcbc  16842  vdwlem6  16928  prmlem0  17047  gsumprval  18627  efgsres  19684  telgsumfzs  19935  lmconst  23222  lmmo  23341  zfbas  23857  uzrest  23858  iscau2  25250  iscau4  25252  caun0  25254  caussi  25270  equivcau  25273  lmcau  25286  mbfsup  25638  mbfinf  25639  mbflimsup  25640  plyco0  26170  dvply2g  26265  dvply2gOLD  26266  geolim3  26320  aaliou3lem2  26324  aaliou3lem3  26325  ulm2  26367  ulm0  26373  ulmcaulem  26376  ulmcau  26377  ulmss  26379  ulmcn  26381  ulmdvlem3  26384  ulmdv  26385  abelthlem7  26421  2logb9irr  26778  sqrt2cxp2logb9e3  26782  ppinprm  27135  chtnprm  27137  ppiublem1  27186  chtublem  27195  chtub  27196  bposlem6  27273  lgsqr  27335  lgseisenlem4  27362  lgsquadlem1  27364  lgsquad2  27370  pntpbnd1  27570  pntlemf  27589  ostth2lem2  27618  istrkg2ld  28549  istrkg2ldOLD  28550  axlowdimlem17  29049  clwwlkvbij  30206  2clwwlk2  30441  numclwlk2lem2f  30470  fzdif2  32887  esumcvg  34270  dya2ub  34454  dya2icoseg  34461  sseqmw  34575  sseqf  34576  ballotlemfp1  34676  iprodefisumlem  35962  poimirlem1  37901  poimirlem2  37902  poimirlem3  37903  poimirlem4  37904  poimirlem6  37906  poimirlem7  37907  poimirlem8  37908  poimirlem9  37909  poimirlem13  37913  poimirlem14  37914  poimirlem15  37915  poimirlem16  37916  poimirlem17  37917  poimirlem18  37918  poimirlem19  37919  poimirlem20  37920  poimirlem21  37921  poimirlem22  37922  poimirlem23  37923  poimirlem24  37924  poimirlem26  37926  poimirlem27  37927  poimirlem31  37931  poimirlem32  37932  mblfinlem2  37938  sdclem1  38023  fdc  38025  seqpo  38027  incsequz2  38029  geomcau  38039  bfplem2  38103  3lexlogpow2ineq1  42457  flt4lem2  43034  eq0rabdioph  43162  rexrabdioph  43180  jm3.1lem1  43403  dvgrat  44697  rexanuz3  45484  uzfissfz  45714  allbutfi  45780  uzid2  45792  fmul01lt1lem1  45973  climinf  45995  climsuse  45997  limsupvaluz2  46125  supcnvlimsup  46127  ioodvbdlimc1lem2  46319  ioodvbdlimc2lem  46321  iblspltprt  46360  stoweidlem7  46394  wallispilem1  46452  wallispilem4  46455  dirkertrigeqlem1  46485  sge0isum  46814  sge0reuzb  46835  carageniuncllem1  46908  caratheodorylem1  46913  smflimlem1  47158  smflimlem2  47159  smflim  47164  smfsuplem1  47198  smfsuplem3  47200  smflimsuplem1  47207  smflimsuplem2  47208  iccpartres  47807  iccelpart  47822  4fppr1  48124  pgnioedg1  48497  pgnioedg2  48498  pgnioedg3  48499  pgnioedg4  48500  pgnbgreunbgrlem1  48502  pgnbgreunbgrlem4  48508  fldivexpfllog2  48954  nnlog2ge0lt1  48955  logbpw2m1  48956  fllog2  48957  blennnelnn  48965  blenpw2  48967  blennnt2  48978  nnolog2flm1  48979  dig2nn0ld  48993  dig2nn1st  48994  0dig2pr01  48999  aacllem  50189