Theorem uzid 12856

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 12574	. . 3 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
3	2	leidd 11755	. 2 ⊢ (𝑀 ∈ ℤ → 𝑀 ≤ 𝑀)
4		eluz1 12845	. 2 ⊢ (𝑀 ∈ ℤ → (𝑀 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝑀)))
5	1, 3, 4	mpbir2and 723	1 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑀))

Syntax hints:   → wi 4   ∈ wcel 2144   class class class wbr 5102  ‘cfv 6523   ≤ cle 11219  ℤcz 12570  ℤ_≥cuz 12841

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2214  ax-ext 2736  ax-sep 5248  ax-nul 5258  ax-pow 5324  ax-pr 5392  ax-un 7720  ax-cnex 11131  ax-resscn 11132  ax-pre-lttri 11149

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-nf 1806  df-sb 2093  df-mo 2568  df-eu 2598  df-clab 2743  df-cleq 2756  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3064  df-ral 3079  df-rex 3089  df-rab 3417  df-v 3458  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5544  df-xp 5655  df-rel 5656  df-cnv 5657  df-co 5658  df-dm 5659  df-rn 5660  df-res 5661  df-ima 5662  df-iota 6479  df-fun 6525  df-fn 6526  df-f 6527  df-f1 6528  df-fo 6529  df-f1o 6530  df-fv 6531  df-ov 7401  df-er 8680  df-en 8930  df-dom 8931  df-sdom 8932  df-pnf 11220  df-mnf 11221  df-xr 11222  df-ltxr 11223  df-le 11224  df-neg 11419  df-z 12571  df-uz 12842

This theorem is referenced by:  uzidd  12857  uzn0  12858  uz11  12866  uzinfi  12931  uzsupss  12943  eluzfz1  13538  eluzfz2  13539  elfz3  13541  elfz1end  13561  fzssp1  13574  fzpred  13579  fzp1ss  13582  fzpr  13586  fztp  13587  elfz0add  13633  fzolb  13673  zpnn0elfzo  13746  fzosplitsnm1  13748  fzofzp1  13772  fzosplitsn  13784  fzostep1  13794  om2uzuzi  13964  axdc4uzlem  13998  seqf  14038  seqfveq  14041  seq1p  14051  faclbnd3  14307  bcm1k  14330  bcn2  14334  seqcoll  14479  swrds1  14682  pfxccatpfx2  14752  rexuz3  15378  r19.2uz  15381  cau3lem  15384  caubnd2  15387  climconst  15572  climuni  15581  isercoll2  15698  climsup  15699  climcau  15700  serf0  15710  iseralt  15714  fsumcvg3  15758  fsumparts  15836  o1fsum  15843  abscvgcvg  15849  isum1p  15873  isumrpcl  15875  isumsup2  15878  climcndslem1  15881  climcndslem2  15882  climcnds  15883  cvgrat  15915  mertenslem1  15916  fprodabs  16006  binomfallfaclem2  16072  fprodefsum  16127  eftlub  16143  rpnnen2lem11  16258  bitsfzo  16471  bitsinv1  16478  smupval  16524  seq1st  16607  algr0  16608  eucalg  16623  2mulprm  16729  prmdvdsbc  16763  oddprm  16848  pcfac  16937  pcbc  16938  vdwlem6  17024  prmlem0  17143  gsumprval  18724  efgsres  19780  telgsumfzs  20031  lmconst  23323  lmmo  23442  zfbas  23958  uzrest  23959  iscau2  25341  iscau4  25343  caun0  25345  caussi  25361  equivcau  25364  lmcau  25377  mbfsup  25728  mbfinf  25729  mbflimsup  25730  plyco0  26254  dvply2g  26351  geolim3  26405  aaliou3lem2  26409  aaliou3lem3  26410  ulm2  26450  ulm0  26456  ulmcaulem  26459  ulmcau  26460  ulmss  26462  ulmcn  26464  ulmdvlem3  26467  ulmdv  26468  abelthlem7  26503  2logb9irr  26862  sqrt2cxp2logb9e3  26866  ppinprm  27218  chtnprm  27220  ppiublem1  27268  chtublem  27277  chtub  27278  bposlem6  27355  lgsqr  27417  lgseisenlem4  27444  lgsquadlem1  27446  lgsquad2  27452  pntpbnd1  27652  pntlemf  27671  ostth2lem2  27700  istrkg2ld  28631  axlowdimlem17  29161  clwwlkvbij  30317  2clwwlk2  30552  numclwlk2lem2f  30581  fzdif2  32994  esumcvg  34385  dya2ub  34569  dya2icoseg  34576  sseqmw  34690  sseqf  34691  ballotlemfp1  34791  iprodefisumlem  36095  poimirlem1  38125  poimirlem2  38126  poimirlem3  38127  poimirlem4  38128  poimirlem6  38130  poimirlem7  38131  poimirlem8  38132  poimirlem9  38133  poimirlem13  38137  poimirlem14  38138  poimirlem15  38139  poimirlem16  38140  poimirlem17  38141  poimirlem18  38142  poimirlem19  38143  poimirlem20  38144  poimirlem21  38145  poimirlem22  38146  poimirlem23  38147  poimirlem24  38148  poimirlem26  38150  poimirlem27  38151  poimirlem31  38155  poimirlem32  38156  mblfinlem2  38162  sdclem1  38247  fdc  38249  seqpo  38251  incsequz2  38253  geomcau  38263  bfplem2  38327  3lexlogpow2ineq1  42680  flt4lem2  43234  eq0rabdioph  43362  rexrabdioph  43376  jm3.1lem1  43599  dvgrat  44893  rexanuz3  45679  uzfissfz  45907  allbutfi  45973  uzid2  45984  fmul01lt1lem1  46165  climinf  46187  climsuse  46189  limsupvaluz2  46317  supcnvlimsup  46319  ioodvbdlimc1lem2  46511  ioodvbdlimc2lem  46513  iblspltprt  46552  stoweidlem7  46586  wallispilem1  46644  wallispilem4  46647  dirkertrigeqlem1  46677  sge0isum  47006  sge0reuzb  47027  carageniuncllem1  47100  caratheodorylem1  47105  smflimlem1  47350  smflimlem2  47351  smflim  47356  smfsuplem1  47390  smfsuplem3  47392  smflimsuplem1  47399  smflimsuplem2  47400  iccpartres  48029  iccelpart  48044  4fppr1  48362  pgnioedg1  48735  pgnioedg2  48736  pgnioedg3  48737  pgnioedg4  48738  pgnbgreunbgrlem1  48740  pgnbgreunbgrlem4  48746  fldivexpfllog2  49192  nnlog2ge0lt1  49193  logbpw2m1  49194  fllog2  49195  blennnelnn  49203  blenpw2  49205  blennnt2  49216  nnolog2flm1  49217  dig2nn0ld  49231  dig2nn1st  49232  0dig2pr01  49237  aacllem  50427