Theorem uzid 12252

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 11979	. . . 4 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
2	1	leidd 11200	. . 3 ⊢ (𝑀 ∈ ℤ → 𝑀 ≤ 𝑀)
3	2	ancli 551	. 2 ⊢ (𝑀 ∈ ℤ → (𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝑀))
4		eluz1 12241	. 2 ⊢ (𝑀 ∈ ℤ → (𝑀 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝑀)))
5	3, 4	mpbird 259	1 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑀))

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2110   class class class wbr 5058  ‘cfv 6349   ≤ cle 10670  ℤcz 11975  ℤ_≥cuz 12237

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7455  ax-cnex 10587  ax-resscn 10588  ax-pre-lttri 10605

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4561  df-pr 4563  df-op 4567  df-uni 4832  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-ov 7153  df-er 8283  df-en 8504  df-dom 8505  df-sdom 8506  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-neg 10867  df-z 11976  df-uz 12238

This theorem is referenced by:  uzidd  12253  uzn0  12254  uz11  12261  uzinfi  12322  uzsupss  12334  eluzfz1  12908  eluzfz2  12909  elfz3  12911  elfz1end  12931  fzssp1  12944  fzpred  12949  fzp1ss  12952  fzpr  12956  fztp  12957  elfz0add  13000  fzolb  13038  zpnn0elfzo  13104  fzosplitsnm1  13106  fzofzp1  13128  fzosplitsn  13139  fzostep1  13147  om2uzuzi  13311  axdc4uzlem  13345  seqf  13385  seqfveq  13388  seq1p  13398  faclbnd3  13646  bcm1k  13669  bcn2  13673  seqcoll  13816  swrds1  14022  pfxccatpfx2  14093  rexuz3  14702  r19.2uz  14705  cau3lem  14708  caubnd2  14711  climconst  14894  climuni  14903  isercoll2  15019  climsup  15020  climcau  15021  serf0  15031  iseralt  15035  fsumcvg3  15080  fsumparts  15155  o1fsum  15162  abscvgcvg  15168  isum1p  15190  isumrpcl  15192  isumsup2  15195  climcndslem1  15198  climcndslem2  15199  climcnds  15200  cvgrat  15233  mertenslem1  15234  ntrivcvgn0  15248  fprodabs  15322  binomfallfaclem2  15388  fprodefsum  15442  eftlub  15456  rpnnen2lem11  15571  bitsfzo  15778  bitsinv1  15785  smupval  15831  seq1st  15909  algr0  15910  eucalg  15925  2mulprm  16031  oddprm  16141  pcfac  16229  pcbc  16230  vdwlem6  16316  prmlem0  16433  gsumprval  17892  gsumccatOLD  17999  efgsres  18858  telgsumfzs  19103  lmconst  21863  lmmo  21982  zfbas  22498  uzrest  22499  iscau2  23874  iscau4  23876  caun0  23878  caussi  23894  equivcau  23897  lmcau  23910  mbfsup  24259  mbfinf  24260  mbflimsup  24261  plyco0  24776  dvply2g  24868  geolim3  24922  aaliou3lem2  24926  aaliou3lem3  24927  ulm2  24967  ulm0  24973  ulmcaulem  24976  ulmcau  24977  ulmss  24979  ulmcn  24981  ulmdvlem3  24984  ulmdv  24985  abelthlem7  25020  2logb9irr  25367  sqrt2cxp2logb9e3  25371  ppinprm  25723  chtnprm  25725  ppiublem1  25772  chtublem  25781  chtub  25782  bposlem6  25859  lgsqr  25921  lgseisenlem4  25948  lgsquadlem1  25950  lgsquad2  25956  pntpbnd1  26156  pntlemf  26175  ostth2lem2  26204  istrkg2ld  26240  axlowdimlem17  26738  clwwlkvbij  27886  2clwwlk2  28121  numclwlk2lem2f  28150  fzdif2  30508  prmdvdsbc  30526  esumcvg  31340  dya2ub  31523  dya2icoseg  31530  sseqmw  31644  sseqf  31645  ballotlemfp1  31744  iprodefisumlem  32967  poimirlem1  34887  poimirlem2  34888  poimirlem3  34889  poimirlem4  34890  poimirlem6  34892  poimirlem7  34893  poimirlem8  34894  poimirlem9  34895  poimirlem13  34899  poimirlem14  34900  poimirlem15  34901  poimirlem16  34902  poimirlem17  34903  poimirlem18  34904  poimirlem19  34905  poimirlem20  34906  poimirlem21  34907  poimirlem22  34908  poimirlem23  34909  poimirlem24  34910  poimirlem26  34912  poimirlem27  34913  poimirlem31  34917  poimirlem32  34918  mblfinlem2  34924  sdclem1  35012  fdc  35014  seqpo  35016  incsequz2  35018  geomcau  35028  bfplem2  35095  eq0rabdioph  39366  rexrabdioph  39384  jm3.1lem1  39607  dvgrat  40637  rexanuz3  41355  uzfissfz  41587  allbutfi  41658  uzid2  41671  fmul01lt1lem1  41858  climinf  41880  climsuse  41882  limsupvaluz2  42012  supcnvlimsup  42014  ioodvbdlimc1lem2  42210  ioodvbdlimc2lem  42212  iblspltprt  42251  stoweidlem7  42286  wallispilem1  42344  wallispilem4  42347  dirkertrigeqlem1  42377  sge0isum  42703  sge0reuzb  42724  carageniuncllem1  42797  caratheodorylem1  42802  smflimlem1  43041  smflimlem2  43042  smflim  43047  smfsuplem1  43079  smfsuplem3  43081  smflimsuplem1  43088  smflimsuplem2  43089  iccpartres  43572  iccelpart  43587  4fppr1  43894  fldivexpfllog2  44619  nnlog2ge0lt1  44620  logbpw2m1  44621  fllog2  44622  blennnelnn  44630  blenpw2  44632  blennnt2  44643  nnolog2flm1  44644  dig2nn0ld  44658  dig2nn1st  44659  0dig2pr01  44664  aacllem  44896