Theorem uzid 12893

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 12617	. . 3 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
3	2	leidd 11829	. 2 ⊢ (𝑀 ∈ ℤ → 𝑀 ≤ 𝑀)
4		eluz1 12882	. 2 ⊢ (𝑀 ∈ ℤ → (𝑀 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝑀)))
5	1, 3, 4	mpbir2and 713	1 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑀))

Syntax hints:   → wi 4   ∈ wcel 2108   class class class wbr 5143  ‘cfv 6561   ≤ cle 11296  ℤcz 12613  ℤ_≥cuz 12878

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-pre-lttri 11229

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-neg 11495  df-z 12614  df-uz 12879

This theorem is referenced by:  uzidd  12894  uzn0  12895  uz11  12903  uzinfi  12970  uzsupss  12982  eluzfz1  13571  eluzfz2  13572  elfz3  13574  elfz1end  13594  fzssp1  13607  fzpred  13612  fzp1ss  13615  fzpr  13619  fztp  13620  elfz0add  13666  fzolb  13705  zpnn0elfzo  13777  fzosplitsnm1  13779  fzofzp1  13803  fzosplitsn  13814  fzostep1  13822  om2uzuzi  13990  axdc4uzlem  14024  seqf  14064  seqfveq  14067  seq1p  14077  faclbnd3  14331  bcm1k  14354  bcn2  14358  seqcoll  14503  swrds1  14704  pfxccatpfx2  14775  rexuz3  15387  r19.2uz  15390  cau3lem  15393  caubnd2  15396  climconst  15579  climuni  15588  isercoll2  15705  climsup  15706  climcau  15707  serf0  15717  iseralt  15721  fsumcvg3  15765  fsumparts  15842  o1fsum  15849  abscvgcvg  15855  isum1p  15877  isumrpcl  15879  isumsup2  15882  climcndslem1  15885  climcndslem2  15886  climcnds  15887  cvgrat  15919  mertenslem1  15920  fprodabs  16010  binomfallfaclem2  16076  fprodefsum  16131  eftlub  16145  rpnnen2lem11  16260  bitsfzo  16472  bitsinv1  16479  smupval  16525  seq1st  16608  algr0  16609  eucalg  16624  2mulprm  16730  prmdvdsbc  16763  oddprm  16848  pcfac  16937  pcbc  16938  vdwlem6  17024  prmlem0  17143  gsumprval  18701  efgsres  19756  telgsumfzs  20007  lmconst  23269  lmmo  23388  zfbas  23904  uzrest  23905  iscau2  25311  iscau4  25313  caun0  25315  caussi  25331  equivcau  25334  lmcau  25347  mbfsup  25699  mbfinf  25700  mbflimsup  25701  plyco0  26231  dvply2g  26326  dvply2gOLD  26327  geolim3  26381  aaliou3lem2  26385  aaliou3lem3  26386  ulm2  26428  ulm0  26434  ulmcaulem  26437  ulmcau  26438  ulmss  26440  ulmcn  26442  ulmdvlem3  26445  ulmdv  26446  abelthlem7  26482  2logb9irr  26838  sqrt2cxp2logb9e3  26842  ppinprm  27195  chtnprm  27197  ppiublem1  27246  chtublem  27255  chtub  27256  bposlem6  27333  lgsqr  27395  lgseisenlem4  27422  lgsquadlem1  27424  lgsquad2  27430  pntpbnd1  27630  pntlemf  27649  ostth2lem2  27678  istrkg2ld  28468  axlowdimlem17  28973  clwwlkvbij  30132  2clwwlk2  30367  numclwlk2lem2f  30396  fzdif2  32792  esumcvg  34087  dya2ub  34272  dya2icoseg  34279  sseqmw  34393  sseqf  34394  ballotlemfp1  34494  iprodefisumlem  35740  poimirlem1  37628  poimirlem2  37629  poimirlem3  37630  poimirlem4  37631  poimirlem6  37633  poimirlem7  37634  poimirlem8  37635  poimirlem9  37636  poimirlem13  37640  poimirlem14  37641  poimirlem15  37642  poimirlem16  37643  poimirlem17  37644  poimirlem18  37645  poimirlem19  37646  poimirlem20  37647  poimirlem21  37648  poimirlem22  37649  poimirlem23  37650  poimirlem24  37651  poimirlem26  37653  poimirlem27  37654  poimirlem31  37658  poimirlem32  37659  mblfinlem2  37665  sdclem1  37750  fdc  37752  seqpo  37754  incsequz2  37756  geomcau  37766  bfplem2  37830  3lexlogpow2ineq1  42059  flt4lem2  42657  eq0rabdioph  42787  rexrabdioph  42805  jm3.1lem1  43029  dvgrat  44331  rexanuz3  45101  uzfissfz  45337  allbutfi  45404  uzid2  45416  fmul01lt1lem1  45599  climinf  45621  climsuse  45623  limsupvaluz2  45753  supcnvlimsup  45755  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  iblspltprt  45988  stoweidlem7  46022  wallispilem1  46080  wallispilem4  46083  dirkertrigeqlem1  46113  sge0isum  46442  sge0reuzb  46463  carageniuncllem1  46536  caratheodorylem1  46541  smflimlem1  46786  smflimlem2  46787  smflim  46792  smfsuplem1  46826  smfsuplem3  46828  smflimsuplem1  46835  smflimsuplem2  46836  iccpartres  47405  iccelpart  47420  4fppr1  47722  fldivexpfllog2  48486  nnlog2ge0lt1  48487  logbpw2m1  48488  fllog2  48489  blennnelnn  48497  blenpw2  48499  blennnt2  48510  nnolog2flm1  48511  dig2nn0ld  48525  dig2nn1st  48526  0dig2pr01  48531  aacllem  49320