Theorem uzid 12833

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 12558	. . 3 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
3	2	leidd 11776	. 2 ⊢ (𝑀 ∈ ℤ → 𝑀 ≤ 𝑀)
4		eluz1 12822	. 2 ⊢ (𝑀 ∈ ℤ → (𝑀 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝑀)))
5	1, 3, 4	mpbir2and 711	1 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑀))

Syntax hints:   → wi 4   ∈ wcel 2106   class class class wbr 5147  ‘cfv 6540   ≤ cle 11245  ℤcz 12554  ℤ_≥cuz 12818

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-cnex 11162  ax-resscn 11163  ax-pre-lttri 11180

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7408  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-neg 11443  df-z 12555  df-uz 12819

This theorem is referenced by:  uzidd  12834  uzn0  12835  uz11  12843  uzinfi  12908  uzsupss  12920  eluzfz1  13504  eluzfz2  13505  elfz3  13507  elfz1end  13527  fzssp1  13540  fzpred  13545  fzp1ss  13548  fzpr  13552  fztp  13553  elfz0add  13596  fzolb  13634  zpnn0elfzo  13701  fzosplitsnm1  13703  fzofzp1  13725  fzosplitsn  13736  fzostep1  13744  om2uzuzi  13910  axdc4uzlem  13944  seqf  13985  seqfveq  13988  seq1p  13998  faclbnd3  14248  bcm1k  14271  bcn2  14275  seqcoll  14421  swrds1  14612  pfxccatpfx2  14683  rexuz3  15291  r19.2uz  15294  cau3lem  15297  caubnd2  15300  climconst  15483  climuni  15492  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  15914  binomfallfaclem2  15980  fprodefsum  16034  eftlub  16048  rpnnen2lem11  16163  bitsfzo  16372  bitsinv1  16379  smupval  16425  seq1st  16504  algr0  16505  eucalg  16520  2mulprm  16626  oddprm  16739  pcfac  16828  pcbc  16829  vdwlem6  16915  prmlem0  17035  gsumprval  18603  efgsres  19600  telgsumfzs  19851  lmconst  22756  lmmo  22875  zfbas  23391  uzrest  23392  iscau2  24785  iscau4  24787  caun0  24789  caussi  24805  equivcau  24808  lmcau  24821  mbfsup  25172  mbfinf  25173  mbflimsup  25174  plyco0  25697  dvply2g  25789  geolim3  25843  aaliou3lem2  25847  aaliou3lem3  25848  ulm2  25888  ulm0  25894  ulmcaulem  25897  ulmcau  25898  ulmss  25900  ulmcn  25902  ulmdvlem3  25905  ulmdv  25906  abelthlem7  25941  2logb9irr  26289  sqrt2cxp2logb9e3  26293  ppinprm  26645  chtnprm  26647  ppiublem1  26694  chtublem  26703  chtub  26704  bposlem6  26781  lgsqr  26843  lgseisenlem4  26870  lgsquadlem1  26872  lgsquad2  26878  pntpbnd1  27078  pntlemf  27097  ostth2lem2  27126  istrkg2ld  27700  axlowdimlem17  28205  clwwlkvbij  29355  2clwwlk2  29590  numclwlk2lem2f  29619  fzdif2  31989  prmdvdsbc  32009  esumcvg  33072  dya2ub  33257  dya2icoseg  33264  sseqmw  33378  sseqf  33379  ballotlemfp1  33478  iprodefisumlem  34698  poimirlem1  36477  poimirlem2  36478  poimirlem3  36479  poimirlem4  36480  poimirlem6  36482  poimirlem7  36483  poimirlem8  36484  poimirlem9  36485  poimirlem13  36489  poimirlem14  36490  poimirlem15  36491  poimirlem16  36492  poimirlem17  36493  poimirlem18  36494  poimirlem19  36495  poimirlem20  36496  poimirlem21  36497  poimirlem22  36498  poimirlem23  36499  poimirlem24  36500  poimirlem26  36502  poimirlem27  36503  poimirlem31  36507  poimirlem32  36508  mblfinlem2  36514  sdclem1  36599  fdc  36601  seqpo  36603  incsequz2  36605  geomcau  36615  bfplem2  36679  3lexlogpow2ineq1  40911  flt4lem2  41385  eq0rabdioph  41499  rexrabdioph  41517  jm3.1lem1  41741  dvgrat  43056  rexanuz3  43770  uzfissfz  44022  allbutfi  44089  uzid2  44101  fmul01lt1lem1  44286  climinf  44308  climsuse  44310  limsupvaluz2  44440  supcnvlimsup  44442  ioodvbdlimc1lem2  44634  ioodvbdlimc2lem  44636  iblspltprt  44675  stoweidlem7  44709  wallispilem1  44767  wallispilem4  44770  dirkertrigeqlem1  44800  sge0isum  45129  sge0reuzb  45150  carageniuncllem1  45223  caratheodorylem1  45228  smflimlem1  45473  smflimlem2  45474  smflim  45479  smfsuplem1  45513  smfsuplem3  45515  smflimsuplem1  45522  smflimsuplem2  45523  iccpartres  46072  iccelpart  46087  4fppr1  46389  fldivexpfllog2  47204  nnlog2ge0lt1  47205  logbpw2m1  47206  fllog2  47207  blennnelnn  47215  blenpw2  47217  blennnt2  47228  nnolog2flm1  47229  dig2nn0ld  47243  dig2nn1st  47244  0dig2pr01  47249  aacllem  47801