Theorem uzid 12867

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

Syntax hints:   → wi 4   ∈ wcel 2108   class class class wbr 5119  ‘cfv 6531   ≤ cle 11270  ℤcz 12588  ℤ_≥cuz 12852

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7729  ax-cnex 11185  ax-resscn 11186  ax-pre-lttri 11203

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6484  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-ov 7408  df-er 8719  df-en 8960  df-dom 8961  df-sdom 8962  df-pnf 11271  df-mnf 11272  df-xr 11273  df-ltxr 11274  df-le 11275  df-neg 11469  df-z 12589  df-uz 12853

This theorem is referenced by:  uzidd  12868  uzn0  12869  uz11  12877  uzinfi  12944  uzsupss  12956  eluzfz1  13548  eluzfz2  13549  elfz3  13551  elfz1end  13571  fzssp1  13584  fzpred  13589  fzp1ss  13592  fzpr  13596  fztp  13597  elfz0add  13643  fzolb  13682  zpnn0elfzo  13754  fzosplitsnm1  13756  fzofzp1  13780  fzosplitsn  13791  fzostep1  13799  om2uzuzi  13967  axdc4uzlem  14001  seqf  14041  seqfveq  14044  seq1p  14054  faclbnd3  14310  bcm1k  14333  bcn2  14337  seqcoll  14482  swrds1  14684  pfxccatpfx2  14755  rexuz3  15367  r19.2uz  15370  cau3lem  15373  caubnd2  15376  climconst  15559  climuni  15568  isercoll2  15685  climsup  15686  climcau  15687  serf0  15697  iseralt  15701  fsumcvg3  15745  fsumparts  15822  o1fsum  15829  abscvgcvg  15835  isum1p  15857  isumrpcl  15859  isumsup2  15862  climcndslem1  15865  climcndslem2  15866  climcnds  15867  cvgrat  15899  mertenslem1  15900  fprodabs  15990  binomfallfaclem2  16056  fprodefsum  16111  eftlub  16127  rpnnen2lem11  16242  bitsfzo  16454  bitsinv1  16461  smupval  16507  seq1st  16590  algr0  16591  eucalg  16606  2mulprm  16712  prmdvdsbc  16745  oddprm  16830  pcfac  16919  pcbc  16920  vdwlem6  17006  prmlem0  17125  gsumprval  18666  efgsres  19719  telgsumfzs  19970  lmconst  23199  lmmo  23318  zfbas  23834  uzrest  23835  iscau2  25229  iscau4  25231  caun0  25233  caussi  25249  equivcau  25252  lmcau  25265  mbfsup  25617  mbfinf  25618  mbflimsup  25619  plyco0  26149  dvply2g  26244  dvply2gOLD  26245  geolim3  26299  aaliou3lem2  26303  aaliou3lem3  26304  ulm2  26346  ulm0  26352  ulmcaulem  26355  ulmcau  26356  ulmss  26358  ulmcn  26360  ulmdvlem3  26363  ulmdv  26364  abelthlem7  26400  2logb9irr  26757  sqrt2cxp2logb9e3  26761  ppinprm  27114  chtnprm  27116  ppiublem1  27165  chtublem  27174  chtub  27175  bposlem6  27252  lgsqr  27314  lgseisenlem4  27341  lgsquadlem1  27343  lgsquad2  27349  pntpbnd1  27549  pntlemf  27568  ostth2lem2  27597  istrkg2ld  28439  axlowdimlem17  28937  clwwlkvbij  30094  2clwwlk2  30329  numclwlk2lem2f  30358  fzdif2  32767  esumcvg  34117  dya2ub  34302  dya2icoseg  34309  sseqmw  34423  sseqf  34424  ballotlemfp1  34524  iprodefisumlem  35757  poimirlem1  37645  poimirlem2  37646  poimirlem3  37647  poimirlem4  37648  poimirlem6  37650  poimirlem7  37651  poimirlem8  37652  poimirlem9  37653  poimirlem13  37657  poimirlem14  37658  poimirlem15  37659  poimirlem16  37660  poimirlem17  37661  poimirlem18  37662  poimirlem19  37663  poimirlem20  37664  poimirlem21  37665  poimirlem22  37666  poimirlem23  37667  poimirlem24  37668  poimirlem26  37670  poimirlem27  37671  poimirlem31  37675  poimirlem32  37676  mblfinlem2  37682  sdclem1  37767  fdc  37769  seqpo  37771  incsequz2  37773  geomcau  37783  bfplem2  37847  3lexlogpow2ineq1  42071  flt4lem2  42670  eq0rabdioph  42799  rexrabdioph  42817  jm3.1lem1  43041  dvgrat  44336  rexanuz3  45120  uzfissfz  45353  allbutfi  45420  uzid2  45432  fmul01lt1lem1  45613  climinf  45635  climsuse  45637  limsupvaluz2  45767  supcnvlimsup  45769  ioodvbdlimc1lem2  45961  ioodvbdlimc2lem  45963  iblspltprt  46002  stoweidlem7  46036  wallispilem1  46094  wallispilem4  46097  dirkertrigeqlem1  46127  sge0isum  46456  sge0reuzb  46477  carageniuncllem1  46550  caratheodorylem1  46555  smflimlem1  46800  smflimlem2  46801  smflim  46806  smfsuplem1  46840  smfsuplem3  46842  smflimsuplem1  46849  smflimsuplem2  46850  iccpartres  47432  iccelpart  47447  4fppr1  47749  fldivexpfllog2  48545  nnlog2ge0lt1  48546  logbpw2m1  48547  fllog2  48548  blennnelnn  48556  blenpw2  48558  blennnt2  48569  nnolog2flm1  48570  dig2nn0ld  48584  dig2nn1st  48585  0dig2pr01  48590  aacllem  49665