Theorem uzid 12798

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 22	. 2 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℤ)
2		zre 12523	. . 3 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
3	2	leidd 11711	. 2 ⊢ (𝑀 ∈ ℤ → 𝑀 ≤ 𝑀)
4		eluz1 12787	. 2 ⊢ (𝑀 ∈ ℤ → (𝑀 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝑀)))
5	1, 3, 4	mpbir2and 720	1 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑀))

Syntax hints:   → wi 4   ∈ wcel 2121   class class class wbr 5075  ‘cfv 6489   ≤ cle 11175  ℤcz 12519  ℤ_≥cuz 12783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-sep 5221  ax-nul 5231  ax-pow 5297  ax-pr 5365  ax-un 7682  ax-cnex 11089  ax-resscn 11090  ax-pre-lttri 11107

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3or 1094  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-nel 3041  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4265  df-if 4458  df-pw 4534  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-br 5076  df-opab 5138  df-mpt 5157  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-ov 7363  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11176  df-mnf 11177  df-xr 11178  df-ltxr 11179  df-le 11180  df-neg 11375  df-z 12520  df-uz 12784

This theorem is referenced by:  uzidd  12799  uzn0  12800  uz11  12808  uzinfi  12873  uzsupss  12885  eluzfz1  13480  eluzfz2  13481  elfz3  13483  elfz1end  13503  fzssp1  13516  fzpred  13521  fzp1ss  13524  fzpr  13528  fztp  13529  elfz0add  13575  fzolb  13615  zpnn0elfzo  13688  fzosplitsnm1  13690  fzofzp1  13714  fzosplitsn  13726  fzostep1  13736  om2uzuzi  13906  axdc4uzlem  13940  seqf  13980  seqfveq  13983  seq1p  13993  faclbnd3  14249  bcm1k  14272  bcn2  14276  seqcoll  14421  swrds1  14624  pfxccatpfx2  14694  rexuz3  15306  r19.2uz  15309  cau3lem  15312  caubnd2  15315  climconst  15500  climuni  15509  isercoll2  15626  climsup  15627  climcau  15628  serf0  15638  iseralt  15642  fsumcvg3  15686  fsumparts  15764  o1fsum  15771  abscvgcvg  15777  isum1p  15801  isumrpcl  15803  isumsup2  15806  climcndslem1  15809  climcndslem2  15810  climcnds  15811  cvgrat  15843  mertenslem1  15844  fprodabs  15934  binomfallfaclem2  16000  fprodefsum  16055  eftlub  16071  rpnnen2lem11  16186  bitsfzo  16399  bitsinv1  16406  smupval  16452  seq1st  16535  algr0  16536  eucalg  16551  2mulprm  16657  prmdvdsbc  16691  oddprm  16776  pcfac  16865  pcbc  16866  vdwlem6  16952  prmlem0  17071  gsumprval  18651  efgsres  19708  telgsumfzs  19959  lmconst  23248  lmmo  23367  zfbas  23883  uzrest  23884  iscau2  25266  iscau4  25268  caun0  25270  caussi  25286  equivcau  25289  lmcau  25302  mbfsup  25653  mbfinf  25654  mbflimsup  25655  plyco0  26179  dvply2g  26273  geolim3  26327  aaliou3lem2  26331  aaliou3lem3  26332  ulm2  26372  ulm0  26378  ulmcaulem  26381  ulmcau  26382  ulmss  26384  ulmcn  26386  ulmdvlem3  26389  ulmdv  26390  abelthlem7  26425  2logb9irr  26781  sqrt2cxp2logb9e3  26785  ppinprm  27137  chtnprm  27139  ppiublem1  27187  chtublem  27196  chtub  27197  bposlem6  27274  lgsqr  27336  lgseisenlem4  27363  lgsquadlem1  27365  lgsquad2  27371  pntpbnd1  27571  pntlemf  27590  ostth2lem2  27619  istrkg2ld  28550  axlowdimlem17  29049  clwwlkvbij  30205  2clwwlk2  30440  numclwlk2lem2f  30469  fzdif2  32886  esumcvg  34282  dya2ub  34466  dya2icoseg  34473  sseqmw  34587  sseqf  34588  ballotlemfp1  34688  iprodefisumlem  35983  poimirlem1  38003  poimirlem2  38004  poimirlem3  38005  poimirlem4  38006  poimirlem6  38008  poimirlem7  38009  poimirlem8  38010  poimirlem9  38011  poimirlem13  38015  poimirlem14  38016  poimirlem15  38017  poimirlem16  38018  poimirlem17  38019  poimirlem18  38020  poimirlem19  38021  poimirlem20  38022  poimirlem21  38023  poimirlem22  38024  poimirlem23  38025  poimirlem24  38026  poimirlem26  38028  poimirlem27  38029  poimirlem31  38033  poimirlem32  38034  mblfinlem2  38040  sdclem1  38125  fdc  38127  seqpo  38129  incsequz2  38131  geomcau  38141  bfplem2  38205  3lexlogpow2ineq1  42558  flt4lem2  43112  eq0rabdioph  43240  rexrabdioph  43254  jm3.1lem1  43477  dvgrat  44771  rexanuz3  45557  uzfissfz  45785  allbutfi  45851  uzid2  45862  fmul01lt1lem1  46043  climinf  46065  climsuse  46067  limsupvaluz2  46195  supcnvlimsup  46197  ioodvbdlimc1lem2  46389  ioodvbdlimc2lem  46391  iblspltprt  46430  stoweidlem7  46464  wallispilem1  46522  wallispilem4  46525  dirkertrigeqlem1  46555  sge0isum  46884  sge0reuzb  46905  carageniuncllem1  46978  caratheodorylem1  46983  smflimlem1  47228  smflimlem2  47229  smflim  47234  smfsuplem1  47268  smfsuplem3  47270  smflimsuplem1  47277  smflimsuplem2  47278  iccpartres  47907  iccelpart  47922  4fppr1  48240  pgnioedg1  48613  pgnioedg2  48614  pgnioedg3  48615  pgnioedg4  48616  pgnbgreunbgrlem1  48618  pgnbgreunbgrlem4  48624  fldivexpfllog2  49070  nnlog2ge0lt1  49071  logbpw2m1  49072  fllog2  49073  blennnelnn  49081  blenpw2  49083  blennnt2  49094  nnolog2flm1  49095  dig2nn0ld  49109  dig2nn1st  49110  0dig2pr01  49115  aacllem  50305