Theorem uzid 12784

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

Syntax hints:   → wi 4   ∈ wcel 2109   class class class wbr 5102  ‘cfv 6499   ≤ cle 11185  ℤcz 12505  ℤ_≥cuz 12769

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-cnex 11100  ax-resscn 11101  ax-pre-lttri 11118

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-ov 7372  df-er 8648  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11186  df-mnf 11187  df-xr 11188  df-ltxr 11189  df-le 11190  df-neg 11384  df-z 12506  df-uz 12770

This theorem is referenced by:  uzidd  12785  uzn0  12786  uz11  12794  uzinfi  12863  uzsupss  12875  eluzfz1  13468  eluzfz2  13469  elfz3  13471  elfz1end  13491  fzssp1  13504  fzpred  13509  fzp1ss  13512  fzpr  13516  fztp  13517  elfz0add  13563  fzolb  13602  zpnn0elfzo  13675  fzosplitsnm1  13677  fzofzp1  13701  fzosplitsn  13712  fzostep1  13720  om2uzuzi  13890  axdc4uzlem  13924  seqf  13964  seqfveq  13967  seq1p  13977  faclbnd3  14233  bcm1k  14256  bcn2  14260  seqcoll  14405  swrds1  14607  pfxccatpfx2  14678  rexuz3  15291  r19.2uz  15294  cau3lem  15297  caubnd2  15300  climconst  15485  climuni  15494  isercoll2  15611  climsup  15612  climcau  15613  serf0  15623  iseralt  15627  fsumcvg3  15671  fsumparts  15748  o1fsum  15755  abscvgcvg  15761  isum1p  15783  isumrpcl  15785  isumsup2  15788  climcndslem1  15791  climcndslem2  15792  climcnds  15793  cvgrat  15825  mertenslem1  15826  fprodabs  15916  binomfallfaclem2  15982  fprodefsum  16037  eftlub  16053  rpnnen2lem11  16168  bitsfzo  16381  bitsinv1  16388  smupval  16434  seq1st  16517  algr0  16518  eucalg  16533  2mulprm  16639  prmdvdsbc  16672  oddprm  16757  pcfac  16846  pcbc  16847  vdwlem6  16933  prmlem0  17052  gsumprval  18597  efgsres  19652  telgsumfzs  19903  lmconst  23181  lmmo  23300  zfbas  23816  uzrest  23817  iscau2  25210  iscau4  25212  caun0  25214  caussi  25230  equivcau  25233  lmcau  25246  mbfsup  25598  mbfinf  25599  mbflimsup  25600  plyco0  26130  dvply2g  26225  dvply2gOLD  26226  geolim3  26280  aaliou3lem2  26284  aaliou3lem3  26285  ulm2  26327  ulm0  26333  ulmcaulem  26336  ulmcau  26337  ulmss  26339  ulmcn  26341  ulmdvlem3  26344  ulmdv  26345  abelthlem7  26381  2logb9irr  26738  sqrt2cxp2logb9e3  26742  ppinprm  27095  chtnprm  27097  ppiublem1  27146  chtublem  27155  chtub  27156  bposlem6  27233  lgsqr  27295  lgseisenlem4  27322  lgsquadlem1  27324  lgsquad2  27330  pntpbnd1  27530  pntlemf  27549  ostth2lem2  27578  istrkg2ld  28440  axlowdimlem17  28938  clwwlkvbij  30092  2clwwlk2  30327  numclwlk2lem2f  30356  fzdif2  32763  esumcvg  34069  dya2ub  34254  dya2icoseg  34261  sseqmw  34375  sseqf  34376  ballotlemfp1  34476  iprodefisumlem  35720  poimirlem1  37608  poimirlem2  37609  poimirlem3  37610  poimirlem4  37611  poimirlem6  37613  poimirlem7  37614  poimirlem8  37615  poimirlem9  37616  poimirlem13  37620  poimirlem14  37621  poimirlem15  37622  poimirlem16  37623  poimirlem17  37624  poimirlem18  37625  poimirlem19  37626  poimirlem20  37627  poimirlem21  37628  poimirlem22  37629  poimirlem23  37630  poimirlem24  37631  poimirlem26  37633  poimirlem27  37634  poimirlem31  37638  poimirlem32  37639  mblfinlem2  37645  sdclem1  37730  fdc  37732  seqpo  37734  incsequz2  37736  geomcau  37746  bfplem2  37810  3lexlogpow2ineq1  42039  flt4lem2  42628  eq0rabdioph  42757  rexrabdioph  42775  jm3.1lem1  42999  dvgrat  44294  rexanuz3  45083  uzfissfz  45315  allbutfi  45382  uzid2  45394  fmul01lt1lem1  45575  climinf  45597  climsuse  45599  limsupvaluz2  45729  supcnvlimsup  45731  ioodvbdlimc1lem2  45923  ioodvbdlimc2lem  45925  iblspltprt  45964  stoweidlem7  45998  wallispilem1  46056  wallispilem4  46059  dirkertrigeqlem1  46089  sge0isum  46418  sge0reuzb  46439  carageniuncllem1  46512  caratheodorylem1  46517  smflimlem1  46762  smflimlem2  46763  smflim  46768  smfsuplem1  46802  smfsuplem3  46804  smflimsuplem1  46811  smflimsuplem2  46812  iccpartres  47412  iccelpart  47427  4fppr1  47729  pgnioedg1  48091  pgnioedg2  48092  pgnioedg3  48093  pgnioedg4  48094  pgnbgreunbgrlem1  48096  pgnbgreunbgrlem4  48102  fldivexpfllog2  48547  nnlog2ge0lt1  48548  logbpw2m1  48549  fllog2  48550  blennnelnn  48558  blenpw2  48560  blennnt2  48571  nnolog2flm1  48572  dig2nn0ld  48586  dig2nn1st  48587  0dig2pr01  48592  aacllem  49783