Theorem uzid 12890

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

Syntax hints:   → wi 4   ∈ wcel 2105   class class class wbr 5147  ‘cfv 6562   ≤ cle 11293  ℤcz 12610  ℤ_≥cuz 12875

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-resscn 11209  ax-pre-lttri 11226

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-ov 7433  df-er 8743  df-en 8984  df-dom 8985  df-sdom 8986  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-neg 11492  df-z 12611  df-uz 12876

This theorem is referenced by:  uzidd  12891  uzn0  12892  uz11  12900  uzinfi  12967  uzsupss  12979  eluzfz1  13567  eluzfz2  13568  elfz3  13570  elfz1end  13590  fzssp1  13603  fzpred  13608  fzp1ss  13611  fzpr  13615  fztp  13616  elfz0add  13662  fzolb  13701  zpnn0elfzo  13773  fzosplitsnm1  13775  fzofzp1  13799  fzosplitsn  13810  fzostep1  13818  om2uzuzi  13986  axdc4uzlem  14020  seqf  14060  seqfveq  14063  seq1p  14073  faclbnd3  14327  bcm1k  14350  bcn2  14354  seqcoll  14499  swrds1  14700  pfxccatpfx2  14771  rexuz3  15383  r19.2uz  15386  cau3lem  15389  caubnd2  15392  climconst  15575  climuni  15584  isercoll2  15701  climsup  15702  climcau  15703  serf0  15713  iseralt  15717  fsumcvg3  15761  fsumparts  15838  o1fsum  15845  abscvgcvg  15851  isum1p  15873  isumrpcl  15875  isumsup2  15878  climcndslem1  15881  climcndslem2  15882  climcnds  15883  cvgrat  15915  mertenslem1  15916  fprodabs  16006  binomfallfaclem2  16072  fprodefsum  16127  eftlub  16141  rpnnen2lem11  16256  bitsfzo  16468  bitsinv1  16475  smupval  16521  seq1st  16604  algr0  16605  eucalg  16620  2mulprm  16726  prmdvdsbc  16759  oddprm  16843  pcfac  16932  pcbc  16933  vdwlem6  17019  prmlem0  17139  gsumprval  18713  efgsres  19770  telgsumfzs  20021  lmconst  23284  lmmo  23403  zfbas  23919  uzrest  23920  iscau2  25324  iscau4  25326  caun0  25328  caussi  25344  equivcau  25347  lmcau  25360  mbfsup  25712  mbfinf  25713  mbflimsup  25714  plyco0  26245  dvply2g  26340  dvply2gOLD  26341  geolim3  26395  aaliou3lem2  26399  aaliou3lem3  26400  ulm2  26442  ulm0  26448  ulmcaulem  26451  ulmcau  26452  ulmss  26454  ulmcn  26456  ulmdvlem3  26459  ulmdv  26460  abelthlem7  26496  2logb9irr  26852  sqrt2cxp2logb9e3  26856  ppinprm  27209  chtnprm  27211  ppiublem1  27260  chtublem  27269  chtub  27270  bposlem6  27347  lgsqr  27409  lgseisenlem4  27436  lgsquadlem1  27438  lgsquad2  27444  pntpbnd1  27644  pntlemf  27663  ostth2lem2  27692  istrkg2ld  28482  axlowdimlem17  28987  clwwlkvbij  30141  2clwwlk2  30376  numclwlk2lem2f  30405  fzdif2  32798  esumcvg  34066  dya2ub  34251  dya2icoseg  34258  sseqmw  34372  sseqf  34373  ballotlemfp1  34472  iprodefisumlem  35719  poimirlem1  37607  poimirlem2  37608  poimirlem3  37609  poimirlem4  37610  poimirlem6  37612  poimirlem7  37613  poimirlem8  37614  poimirlem9  37615  poimirlem13  37619  poimirlem14  37620  poimirlem15  37621  poimirlem16  37622  poimirlem17  37623  poimirlem18  37624  poimirlem19  37625  poimirlem20  37626  poimirlem21  37627  poimirlem22  37628  poimirlem23  37629  poimirlem24  37630  poimirlem26  37632  poimirlem27  37633  poimirlem31  37637  poimirlem32  37638  mblfinlem2  37644  sdclem1  37729  fdc  37731  seqpo  37733  incsequz2  37735  geomcau  37745  bfplem2  37809  3lexlogpow2ineq1  42039  flt4lem2  42633  eq0rabdioph  42763  rexrabdioph  42781  jm3.1lem1  43005  dvgrat  44307  rexanuz3  45035  uzfissfz  45275  allbutfi  45342  uzid2  45354  fmul01lt1lem1  45539  climinf  45561  climsuse  45563  limsupvaluz2  45693  supcnvlimsup  45695  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  iblspltprt  45928  stoweidlem7  45962  wallispilem1  46020  wallispilem4  46023  dirkertrigeqlem1  46053  sge0isum  46382  sge0reuzb  46403  carageniuncllem1  46476  caratheodorylem1  46481  smflimlem1  46726  smflimlem2  46727  smflim  46732  smfsuplem1  46766  smfsuplem3  46768  smflimsuplem1  46775  smflimsuplem2  46776  iccpartres  47342  iccelpart  47357  4fppr1  47659  fldivexpfllog2  48414  nnlog2ge0lt1  48415  logbpw2m1  48416  fllog2  48417  blennnelnn  48425  blenpw2  48427  blennnt2  48438  nnolog2flm1  48439  dig2nn0ld  48453  dig2nn1st  48454  0dig2pr01  48459  aacllem  49031