Theorem uzid 12007

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		zre 11732	. . . 4 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
2	1	leidd 10941	. . 3 ⊢ (𝑀 ∈ ℤ → 𝑀 ≤ 𝑀)
3	2	ancli 544	. 2 ⊢ (𝑀 ∈ ℤ → (𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝑀))
4		eluz1 11996	. 2 ⊢ (𝑀 ∈ ℤ → (𝑀 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝑀)))
5	3, 4	mpbird 249	1 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑀))

Syntax hints:   → wi 4   ∧ wa 386   ∈ wcel 2107   class class class wbr 4886  ‘cfv 6135   ≤ cle 10412  ℤcz 11728  ℤ_≥cuz 11992

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-cnex 10328  ax-resscn 10329  ax-pre-lttri 10346

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4672  df-br 4887  df-opab 4949  df-mpt 4966  df-id 5261  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-ov 6925  df-er 8026  df-en 8242  df-dom 8243  df-sdom 8244  df-pnf 10413  df-mnf 10414  df-xr 10415  df-ltxr 10416  df-le 10417  df-neg 10609  df-z 11729  df-uz 11993

This theorem is referenced by:  uzn0  12008  uz11  12015  uzinfi  12075  uzsupss  12087  eluzfz1  12665  eluzfz2  12666  elfz3  12668  elfz1end  12688  fzssp1  12701  fzpred  12706  fzp1ss  12709  fzpr  12713  fztp  12714  elfz0add  12757  fzolb  12795  zpnn0elfzo  12860  fzosplitsnm1  12862  fzofzp1  12884  fzosplitsn  12895  fzostep1  12903  om2uzuzi  13067  axdc4uzlem  13101  seqf  13140  seqfveq  13143  seq1p  13153  faclbnd3  13397  bcm1k  13420  bcn2  13424  seqcoll  13562  ccatass  13678  ccatrn  13679  swrds1  13771  swrdccat1OLD  13777  swrdccat2  13778  pfxccat1  13811  pfxccatpfx2  13868  splfv1  13898  splfv1OLD  13899  splval2  13902  splval2OLD  13903  revccat  13912  rexuz3  14495  r19.2uz  14498  cau3lem  14501  caubnd2  14504  climconst  14682  climuni  14691  isercoll2  14807  climsup  14808  climcau  14809  serf0  14819  iseralt  14823  fsumcvg3  14867  fsumparts  14942  o1fsum  14949  abscvgcvg  14955  isum1p  14977  isumrpcl  14979  isumsup2  14982  climcndslem1  14985  climcndslem2  14986  climcnds  14987  cvgrat  15018  mertenslem1  15019  ntrivcvgn0  15033  fprodabs  15107  binomfallfaclem2  15173  fprodefsum  15227  eftlub  15241  rpnnen2lem11  15357  bitsfzo  15563  bitsinv1  15570  smupval  15616  seq1st  15690  algr0  15691  eucalg  15706  oddprm  15919  pcfac  16007  pcbc  16008  vdwlem6  16094  prmlem0  16211  gsumprval  17667  gsumccat  17764  efginvrel2  18524  efgsres  18535  efgsresOLD  18536  telgsumfzs  18773  lmconst  21473  lmmo  21592  zfbas  22108  uzrest  22109  iscau2  23483  iscau4  23485  caun0  23487  caussi  23503  equivcau  23506  lmcau  23519  mbfsup  23868  mbfinf  23869  mbflimsup  23870  plyco0  24385  dvply2g  24477  geolim3  24531  aaliou3lem2  24535  aaliou3lem3  24536  ulm2  24576  ulm0  24582  ulmcaulem  24585  ulmcau  24586  ulmss  24588  ulmcn  24590  ulmdvlem3  24593  ulmdv  24594  abelthlem7  24629  2logb9irr  24973  sqrt2cxp2logb9e3  24977  ppinprm  25330  chtnprm  25332  ppiublem1  25379  chtublem  25388  chtub  25389  bposlem6  25466  lgsqr  25528  lgseisenlem4  25555  lgsquadlem1  25557  lgsquad2  25563  pntpbnd1  25727  pntlemf  25746  ostth2lem2  25775  istrkg2ld  25811  axlowdimlem17  26307  clwwlkvbij  27515  clwwlkvbijOLD  27516  2clwwlk2  27759  numclwlk2lem2f  27805  numclwlk2lem2fOLD  27808  fzdif2  30115  esumcvg  30746  dya2ub  30930  dya2icoseg  30937  sseqmw  31052  sseqf  31053  ballotlemfp1  31152  signstfvp  31249  iprodefisumlem  32220  poimirlem1  34038  poimirlem2  34039  poimirlem3  34040  poimirlem4  34041  poimirlem6  34043  poimirlem7  34044  poimirlem8  34045  poimirlem9  34046  poimirlem13  34050  poimirlem14  34051  poimirlem15  34052  poimirlem16  34053  poimirlem17  34054  poimirlem18  34055  poimirlem19  34056  poimirlem20  34057  poimirlem21  34058  poimirlem22  34059  poimirlem23  34060  poimirlem24  34061  poimirlem26  34063  poimirlem27  34064  poimirlem31  34068  poimirlem32  34069  mblfinlem2  34075  sdclem1  34165  fdc  34167  seqpo  34169  incsequz2  34171  geomcau  34181  bfplem2  34248  eq0rabdioph  38304  rexrabdioph  38322  jm3.1lem1  38547  dvgrat  39471  rexanuz3  40210  uzfissfz  40454  allbutfi  40526  uzid2  40540  uzidd  40541  fmul01lt1lem1  40728  climinf  40750  climsuse  40752  limsupvaluz2  40882  supcnvlimsup  40884  ioodvbdlimc1lem2  41079  ioodvbdlimc2lem  41081  iblspltprt  41120  stoweidlem7  41155  wallispilem1  41213  wallispilem4  41216  dirkertrigeqlem1  41246  sge0isum  41572  sge0reuzb  41593  carageniuncllem1  41666  caratheodorylem1  41671  smflimlem1  41910  smflimlem2  41911  smflim  41916  smfsuplem1  41948  smfsuplem3  41950  smflimsuplem1  41957  smflimsuplem2  41958  iccpartres  42390  iccelpart  42405  fldivexpfllog2  43378  nnlog2ge0lt1  43379  logbpw2m1  43380  fllog2  43381  blennnelnn  43389  blenpw2  43391  blennnt2  43402  nnolog2flm1  43403  dig2nn0ld  43417  dig2nn1st  43418  0dig2pr01  43423  aacllem  43657