Theorem uzid 12246

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 11973	. . . 4 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
2	1	leidd 11195	. . 3 ⊢ (𝑀 ∈ ℤ → 𝑀 ≤ 𝑀)
3	2	ancli 552	. 2 ⊢ (𝑀 ∈ ℤ → (𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝑀))
4		eluz1 12235	. 2 ⊢ (𝑀 ∈ ℤ → (𝑀 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝑀)))
5	3, 4	mpbird 260	1 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑀))

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2111   class class class wbr 5030  ‘cfv 6324   ≤ cle 10665  ℤcz 11969  ℤ_≥cuz 12231

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-cnex 10582  ax-resscn 10583  ax-pre-lttri 10600

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-ov 7138  df-er 8272  df-en 8493  df-dom 8494  df-sdom 8495  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-neg 10862  df-z 11970  df-uz 12232

This theorem is referenced by:  uzidd  12247  uzn0  12248  uz11  12255  uzinfi  12316  uzsupss  12328  eluzfz1  12909  eluzfz2  12910  elfz3  12912  elfz1end  12932  fzssp1  12945  fzpred  12950  fzp1ss  12953  fzpr  12957  fztp  12958  elfz0add  13001  fzolb  13039  zpnn0elfzo  13105  fzosplitsnm1  13107  fzofzp1  13129  fzosplitsn  13140  fzostep1  13148  om2uzuzi  13312  axdc4uzlem  13346  seqf  13387  seqfveq  13390  seq1p  13400  faclbnd3  13648  bcm1k  13671  bcn2  13675  seqcoll  13818  swrds1  14019  pfxccatpfx2  14090  rexuz3  14700  r19.2uz  14703  cau3lem  14706  caubnd2  14709  climconst  14892  climuni  14901  isercoll2  15017  climsup  15018  climcau  15019  serf0  15029  iseralt  15033  fsumcvg3  15078  fsumparts  15153  o1fsum  15160  abscvgcvg  15166  isum1p  15188  isumrpcl  15190  isumsup2  15193  climcndslem1  15196  climcndslem2  15197  climcnds  15198  cvgrat  15231  mertenslem1  15232  ntrivcvgn0  15246  fprodabs  15320  binomfallfaclem2  15386  fprodefsum  15440  eftlub  15454  rpnnen2lem11  15569  bitsfzo  15774  bitsinv1  15781  smupval  15827  seq1st  15905  algr0  15906  eucalg  15921  2mulprm  16027  oddprm  16137  pcfac  16225  pcbc  16226  vdwlem6  16312  prmlem0  16431  gsumprval  17890  gsumccatOLD  17997  efgsres  18856  telgsumfzs  19102  lmconst  21866  lmmo  21985  zfbas  22501  uzrest  22502  iscau2  23881  iscau4  23883  caun0  23885  caussi  23901  equivcau  23904  lmcau  23917  mbfsup  24268  mbfinf  24269  mbflimsup  24270  plyco0  24789  dvply2g  24881  geolim3  24935  aaliou3lem2  24939  aaliou3lem3  24940  ulm2  24980  ulm0  24986  ulmcaulem  24989  ulmcau  24990  ulmss  24992  ulmcn  24994  ulmdvlem3  24997  ulmdv  24998  abelthlem7  25033  2logb9irr  25381  sqrt2cxp2logb9e3  25385  ppinprm  25737  chtnprm  25739  ppiublem1  25786  chtublem  25795  chtub  25796  bposlem6  25873  lgsqr  25935  lgseisenlem4  25962  lgsquadlem1  25964  lgsquad2  25970  pntpbnd1  26170  pntlemf  26189  ostth2lem2  26218  istrkg2ld  26254  axlowdimlem17  26752  clwwlkvbij  27898  2clwwlk2  28133  numclwlk2lem2f  28162  fzdif2  30540  prmdvdsbc  30558  esumcvg  31455  dya2ub  31638  dya2icoseg  31645  sseqmw  31759  sseqf  31760  ballotlemfp1  31859  iprodefisumlem  33085  poimirlem1  35058  poimirlem2  35059  poimirlem3  35060  poimirlem4  35061  poimirlem6  35063  poimirlem7  35064  poimirlem8  35065  poimirlem9  35066  poimirlem13  35070  poimirlem14  35071  poimirlem15  35072  poimirlem16  35073  poimirlem17  35074  poimirlem18  35075  poimirlem19  35076  poimirlem20  35077  poimirlem21  35078  poimirlem22  35079  poimirlem23  35080  poimirlem24  35081  poimirlem26  35083  poimirlem27  35084  poimirlem31  35088  poimirlem32  35089  mblfinlem2  35095  sdclem1  35181  fdc  35183  seqpo  35185  incsequz2  35187  geomcau  35197  bfplem2  35261  eq0rabdioph  39717  rexrabdioph  39735  jm3.1lem1  39958  dvgrat  41016  rexanuz3  41732  uzfissfz  41958  allbutfi  42029  uzid2  42042  fmul01lt1lem1  42226  climinf  42248  climsuse  42250  limsupvaluz2  42380  supcnvlimsup  42382  ioodvbdlimc1lem2  42574  ioodvbdlimc2lem  42576  iblspltprt  42615  stoweidlem7  42649  wallispilem1  42707  wallispilem4  42710  dirkertrigeqlem1  42740  sge0isum  43066  sge0reuzb  43087  carageniuncllem1  43160  caratheodorylem1  43165  smflimlem1  43404  smflimlem2  43405  smflim  43410  smfsuplem1  43442  smfsuplem3  43444  smflimsuplem1  43451  smflimsuplem2  43452  iccpartres  43935  iccelpart  43950  4fppr1  44253  fldivexpfllog2  44979  nnlog2ge0lt1  44980  logbpw2m1  44981  fllog2  44982  blennnelnn  44990  blenpw2  44992  blennnt2  45003  nnolog2flm1  45004  dig2nn0ld  45018  dig2nn1st  45019  0dig2pr01  45024  aacllem  45329