Theorem uzid 12905

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 23	. 2 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℤ)
2		zre 12622	. . 3 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
3	2	leidd 11807	. 2 ⊢ (𝑀 ∈ ℤ → 𝑀 ≤ 𝑀)
4		eluz1 12894	. 2 ⊢ (𝑀 ∈ ℤ → (𝑀 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝑀)))
5	1, 3, 4	mpbir2and 726	1 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑀))

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   class class class wbr 5107  ‘cfv 6537   ≤ cle 11271  ℤcz 12618  ℤ_≥cuz 12890

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7739  ax-cnex 11183  ax-resscn 11184  ax-pre-lttri 11201

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7419  df-er 8699  df-en 8956  df-dom 8957  df-sdom 8958  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-neg 11471  df-z 12619  df-uz 12891

This theorem is used by:  uzidd  12906  uzn0  12907  uz11  12915  uzinfi  12980  uzsupss  12992  eluzfz1  13587  eluzfz2  13588  elfz3  13590  elfz1end  13611  fzssp1  13624  fzpred  13629  fzp1ss  13632  fzpr  13636  fztp  13637  elfz0add  13683  fzolb  13723  zpnn0elfzo  13796  fzosplitsnm1  13798  fzofzp1  13822  fzosplitsn  13834  fzostep1  13844  om2uzuzi  14015  axdc4uzlem  14049  seqf  14089  seqfveq  14092  seq1p  14102  faclbnd3  14358  bcm1k  14381  bcn2  14385  seqcoll  14531  swrds1  14738  pfxccatpfx2  14808  rexuz3  15438  r19.2uz  15441  cau3lem  15444  caubnd2  15447  climconst  15632  climuni  15641  isercoll2  15758  climsup  15759  climcau  15760  serf0  15770  iseralt  15774  fsumcvg3  15817  fsumparts  15895  o1fsum  15902  abscvgcvg  15908  isum1p  15932  isumrpcl  15934  isumsup2  15937  climcndslem1  15940  climcndslem2  15941  climcnds  15942  cvgrat  15974  mertenslem1  15975  fprodabs  16065  binomfallfaclem2  16130  fprodefsum  16185  eftlub  16201  rpnnen2lem11  16316  bitsfzo  16529  bitsinv1  16536  smupval  16582  seq1st  16665  algr0  16666  eucalg  16681  2mulprm  16787  prmdvdsbc  16821  oddprm  16906  pcfac  16995  pcbc  16996  vdwlem6  17082  prmlem0  17201  gsumprval  18792  efgsres  19866  telgsumfzs  20117  lmconst  23487  lmmo  23606  zfbas  24123  uzrest  24124  iscau2  25506  iscau4  25508  caun0  25510  caussi  25526  equivcau  25529  lmcau  25542  mbfsup  25893  mbfinf  25894  mbflimsup  25895  plyco0  26419  dvply2g  26516  geolim3  26572  aaliou3lem2  26576  aaliou3lem3  26577  ulm2  26618  ulm0  26624  ulmcaulem  26627  ulmcau  26628  ulmss  26630  ulmcn  26632  ulmdvlem3  26635  ulmdv  26636  abelthlem7  26671  2logb9irr  27030  sqrt2cxp2logb9e3  27034  ppinprm  27386  chtnprm  27388  ppiublem1  27436  chtublem  27445  chtub  27446  bposlem6  27523  lgsqr  27585  lgseisenlem4  27612  lgsquadlem1  27614  lgsquad2  27620  pntpbnd1  27820  pntlemf  27839  ostth2lem2  27868  istrkg2ld  28799  axlowdimlem17  29401  clwwlkvbij  30569  2clwwlk2  30814  numclwlk2lem2f  30843  fzdif2  33248  esumcvg  34583  dya2ub  34768  dya2icoseg  34775  sseqmw  34889  sseqf  34890  ballotlemfp1  34990  iprodefisumlem  36306  poimirlem1  38357  poimirlem2  38358  poimirlem3  38359  poimirlem4  38360  poimirlem6  38362  poimirlem7  38363  poimirlem8  38364  poimirlem9  38365  poimirlem13  38369  poimirlem14  38370  poimirlem15  38371  poimirlem16  38372  poimirlem17  38373  poimirlem18  38374  poimirlem19  38375  poimirlem20  38376  poimirlem21  38377  poimirlem22  38378  poimirlem23  38379  poimirlem24  38380  poimirlem26  38382  poimirlem27  38383  poimirlem31  38387  poimirlem32  38388  mblfinlem2  38394  sdclem1  38480  fdc  38482  seqpo  38484  incsequz2  38486  geomcau  38496  bfplem2  38560  3lexlogpow2ineq1  42911  flt4lem2  43480  eq0rabdioph  43608  rexrabdioph  43622  jm3.1lem1  43845  dvgrat  45123  rexanuz3  45915  uzfissfz  46143  allbutfi  46209  uzid2  46220  fmul01lt1lem1  46401  climinf  46423  climsuse  46425  limsupvaluz2  46553  supcnvlimsup  46555  ioodvbdlimc1lem2  46747  ioodvbdlimc2lem  46749  iblspltprt  46788  stoweidlem7  46822  wallispilem1  46880  wallispilem4  46883  dirkertrigeqlem1  46913  sge0isum  47242  sge0reuzb  47263  carageniuncllem1  47336  caratheodorylem1  47341  smflimlem1  47586  smflimlem2  47587  smflim  47592  smfsuplem1  47626  smfsuplem3  47628  smflimsuplem1  47635  smflimsuplem2  47636  iccpartres  48305  iccelpart  48320  4fppr1  48638  pgnioedg1  49011  pgnioedg2  49012  pgnioedg3  49013  pgnioedg4  49014  pgnbgreunbgrlem1  49016  pgnbgreunbgrlem4  49022  fldivexpfllog2  49482  nnlog2ge0lt1  49483  logbpw2m1  49484  fllog2  49485  blennnelnn  49493  blenpw2  49495  blennnt2  49506  nnolog2flm1  49507  dig2nn0ld  49521  dig2nn1st  49522  0dig2pr01  49527  aacllem  50759