Theorem uzid 12883

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 12601	. . 3 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
3	2	leidd 11786	. 2 ⊢ (𝑀 ∈ ℤ → 𝑀 ≤ 𝑀)
4		eluz1 12872	. 2 ⊢ (𝑀 ∈ ℤ → (𝑀 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝑀)))
5	1, 3, 4	mpbir2and 725	1 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑀))

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2142   class class class wbr 5108  ‘cfv 6536   ≤ cle 11250  ℤcz 12597  ℤ_≥cuz 12868

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5256  ax-nul 5268  ax-pow 5335  ax-pr 5403  ax-un 7734  ax-cnex 11162  ax-resscn 11163  ax-pre-lttri 11180

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1103  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-nf 1813  df-sb 2096  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 3416  df-v 3456  df-sbc 3744  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-opab 5173  df-mpt 5192  df-id 5555  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-rn 5671  df-res 5672  df-ima 5673  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7415  df-er 8692  df-en 8942  df-dom 8943  df-sdom 8944  df-pnf 11251  df-mnf 11252  df-xr 11253  df-ltxr 11254  df-le 11255  df-neg 11450  df-z 12598  df-uz 12869

This theorem is used by:  uzidd  12884  uzn0  12885  uz11  12893  uzinfi  12958  uzsupss  12970  eluzfz1  13565  eluzfz2  13566  elfz3  13568  elfz1end  13589  fzssp1  13602  fzpred  13607  fzp1ss  13610  fzpr  13614  fztp  13615  elfz0add  13661  fzolb  13701  zpnn0elfzo  13774  fzosplitsnm1  13776  fzofzp1  13800  fzosplitsn  13812  fzostep1  13822  om2uzuzi  13992  axdc4uzlem  14026  seqf  14066  seqfveq  14069  seq1p  14079  faclbnd3  14335  bcm1k  14358  bcn2  14362  seqcoll  14508  swrds1  14711  pfxccatpfx2  14781  rexuz3  15407  r19.2uz  15410  cau3lem  15413  caubnd2  15416  climconst  15601  climuni  15610  isercoll2  15727  climsup  15728  climcau  15729  serf0  15739  iseralt  15743  fsumcvg3  15787  fsumparts  15865  o1fsum  15872  abscvgcvg  15878  isum1p  15902  isumrpcl  15904  isumsup2  15907  climcndslem1  15910  climcndslem2  15911  climcnds  15912  cvgrat  15944  mertenslem1  15945  fprodabs  16035  binomfallfaclem2  16100  fprodefsum  16155  eftlub  16171  rpnnen2lem11  16286  bitsfzo  16499  bitsinv1  16506  smupval  16552  seq1st  16635  algr0  16636  eucalg  16651  2mulprm  16757  prmdvdsbc  16791  oddprm  16876  pcfac  16965  pcbc  16966  vdwlem6  17052  prmlem0  17171  gsumprval  18752  efgsres  19814  telgsumfzs  20065  lmconst  23429  lmmo  23548  zfbas  24064  uzrest  24065  iscau2  25447  iscau4  25449  caun0  25451  caussi  25467  equivcau  25470  lmcau  25483  mbfsup  25834  mbfinf  25835  mbflimsup  25836  plyco0  26360  dvply2g  26457  geolim3  26513  aaliou3lem2  26517  aaliou3lem3  26518  ulm2  26559  ulm0  26565  ulmcaulem  26568  ulmcau  26569  ulmss  26571  ulmcn  26573  ulmdvlem3  26576  ulmdv  26577  abelthlem7  26612  2logb9irr  26971  sqrt2cxp2logb9e3  26975  ppinprm  27327  chtnprm  27329  ppiublem1  27377  chtublem  27386  chtub  27387  bposlem6  27464  lgsqr  27526  lgseisenlem4  27553  lgsquadlem1  27555  lgsquad2  27561  pntpbnd1  27761  pntlemf  27780  ostth2lem2  27809  istrkg2ld  28740  axlowdimlem17  29319  clwwlkvbij  30475  2clwwlk2  30710  numclwlk2lem2f  30739  fzdif2  33146  esumcvg  34485  dya2ub  34669  dya2icoseg  34676  sseqmw  34790  sseqf  34791  ballotlemfp1  34891  iprodefisumlem  36240  poimirlem1  38300  poimirlem2  38301  poimirlem3  38302  poimirlem4  38303  poimirlem6  38305  poimirlem7  38306  poimirlem8  38307  poimirlem9  38308  poimirlem13  38312  poimirlem14  38313  poimirlem15  38314  poimirlem16  38315  poimirlem17  38316  poimirlem18  38317  poimirlem19  38318  poimirlem20  38319  poimirlem21  38320  poimirlem22  38321  poimirlem23  38322  poimirlem24  38323  poimirlem26  38325  poimirlem27  38326  poimirlem31  38330  poimirlem32  38331  mblfinlem2  38337  sdclem1  38422  fdc  38424  seqpo  38426  incsequz2  38428  geomcau  38438  bfplem2  38502  3lexlogpow2ineq1  42853  flt4lem2  43407  eq0rabdioph  43535  rexrabdioph  43549  jm3.1lem1  43772  dvgrat  45050  rexanuz3  45842  uzfissfz  46070  allbutfi  46136  uzid2  46147  fmul01lt1lem1  46328  climinf  46350  climsuse  46352  limsupvaluz2  46480  supcnvlimsup  46482  ioodvbdlimc1lem2  46674  ioodvbdlimc2lem  46676  iblspltprt  46715  stoweidlem7  46749  wallispilem1  46807  wallispilem4  46810  dirkertrigeqlem1  46840  sge0isum  47169  sge0reuzb  47190  carageniuncllem1  47263  caratheodorylem1  47268  smflimlem1  47513  smflimlem2  47514  smflim  47519  smfsuplem1  47553  smfsuplem3  47555  smflimsuplem1  47562  smflimsuplem2  47563  iccpartres  48195  iccelpart  48210  4fppr1  48528  pgnioedg1  48901  pgnioedg2  48902  pgnioedg3  48903  pgnioedg4  48904  pgnbgreunbgrlem1  48906  pgnbgreunbgrlem4  48912  fldivexpfllog2  49373  nnlog2ge0lt1  49374  logbpw2m1  49375  fllog2  49376  blennnelnn  49384  blenpw2  49386  blennnt2  49397  nnolog2flm1  49398  dig2nn0ld  49412  dig2nn1st  49413  0dig2pr01  49418  aacllem  50649