Theorem uzid 12918

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 12643	. . 3 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
3	2	leidd 11856	. 2 ⊢ (𝑀 ∈ ℤ → 𝑀 ≤ 𝑀)
4		eluz1 12907	. 2 ⊢ (𝑀 ∈ ℤ → (𝑀 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝑀)))
5	1, 3, 4	mpbir2and 712	1 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑀))

Syntax hints:   → wi 4   ∈ wcel 2108   class class class wbr 5166  ‘cfv 6573   ≤ cle 11325  ℤcz 12639  ℤ_≥cuz 12903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-cnex 11240  ax-resscn 11241  ax-pre-lttri 11258

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-ov 7451  df-er 8763  df-en 9004  df-dom 9005  df-sdom 9006  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-neg 11523  df-z 12640  df-uz 12904

This theorem is referenced by:  uzidd  12919  uzn0  12920  uz11  12928  uzinfi  12993  uzsupss  13005  eluzfz1  13591  eluzfz2  13592  elfz3  13594  elfz1end  13614  fzssp1  13627  fzpred  13632  fzp1ss  13635  fzpr  13639  fztp  13640  elfz0add  13683  fzolb  13722  zpnn0elfzo  13789  fzosplitsnm1  13791  fzofzp1  13814  fzosplitsn  13825  fzostep1  13833  om2uzuzi  14000  axdc4uzlem  14034  seqf  14074  seqfveq  14077  seq1p  14087  faclbnd3  14341  bcm1k  14364  bcn2  14368  seqcoll  14513  swrds1  14714  pfxccatpfx2  14785  rexuz3  15397  r19.2uz  15400  cau3lem  15403  caubnd2  15406  climconst  15589  climuni  15598  isercoll2  15717  climsup  15718  climcau  15719  serf0  15729  iseralt  15733  fsumcvg3  15777  fsumparts  15854  o1fsum  15861  abscvgcvg  15867  isum1p  15889  isumrpcl  15891  isumsup2  15894  climcndslem1  15897  climcndslem2  15898  climcnds  15899  cvgrat  15931  mertenslem1  15932  fprodabs  16022  binomfallfaclem2  16088  fprodefsum  16143  eftlub  16157  rpnnen2lem11  16272  bitsfzo  16481  bitsinv1  16488  smupval  16534  seq1st  16618  algr0  16619  eucalg  16634  2mulprm  16740  prmdvdsbc  16773  oddprm  16857  pcfac  16946  pcbc  16947  vdwlem6  17033  prmlem0  17153  gsumprval  18726  efgsres  19780  telgsumfzs  20031  lmconst  23290  lmmo  23409  zfbas  23925  uzrest  23926  iscau2  25330  iscau4  25332  caun0  25334  caussi  25350  equivcau  25353  lmcau  25366  mbfsup  25718  mbfinf  25719  mbflimsup  25720  plyco0  26251  dvply2g  26344  dvply2gOLD  26345  geolim3  26399  aaliou3lem2  26403  aaliou3lem3  26404  ulm2  26446  ulm0  26452  ulmcaulem  26455  ulmcau  26456  ulmss  26458  ulmcn  26460  ulmdvlem3  26463  ulmdv  26464  abelthlem7  26500  2logb9irr  26856  sqrt2cxp2logb9e3  26860  ppinprm  27213  chtnprm  27215  ppiublem1  27264  chtublem  27273  chtub  27274  bposlem6  27351  lgsqr  27413  lgseisenlem4  27440  lgsquadlem1  27442  lgsquad2  27448  pntpbnd1  27648  pntlemf  27667  ostth2lem2  27696  istrkg2ld  28486  axlowdimlem17  28991  clwwlkvbij  30145  2clwwlk2  30380  numclwlk2lem2f  30409  fzdif2  32796  esumcvg  34050  dya2ub  34235  dya2icoseg  34242  sseqmw  34356  sseqf  34357  ballotlemfp1  34456  iprodefisumlem  35702  poimirlem1  37581  poimirlem2  37582  poimirlem3  37583  poimirlem4  37584  poimirlem6  37586  poimirlem7  37587  poimirlem8  37588  poimirlem9  37589  poimirlem13  37593  poimirlem14  37594  poimirlem15  37595  poimirlem16  37596  poimirlem17  37597  poimirlem18  37598  poimirlem19  37599  poimirlem20  37600  poimirlem21  37601  poimirlem22  37602  poimirlem23  37603  poimirlem24  37604  poimirlem26  37606  poimirlem27  37607  poimirlem31  37611  poimirlem32  37612  mblfinlem2  37618  sdclem1  37703  fdc  37705  seqpo  37707  incsequz2  37709  geomcau  37719  bfplem2  37783  3lexlogpow2ineq1  42015  flt4lem2  42602  eq0rabdioph  42732  rexrabdioph  42750  jm3.1lem1  42974  dvgrat  44281  rexanuz3  44998  uzfissfz  45241  allbutfi  45308  uzid2  45320  fmul01lt1lem1  45505  climinf  45527  climsuse  45529  limsupvaluz2  45659  supcnvlimsup  45661  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  iblspltprt  45894  stoweidlem7  45928  wallispilem1  45986  wallispilem4  45989  dirkertrigeqlem1  46019  sge0isum  46348  sge0reuzb  46369  carageniuncllem1  46442  caratheodorylem1  46447  smflimlem1  46692  smflimlem2  46693  smflim  46698  smfsuplem1  46732  smfsuplem3  46734  smflimsuplem1  46741  smflimsuplem2  46742  iccpartres  47292  iccelpart  47307  4fppr1  47609  fldivexpfllog2  48299  nnlog2ge0lt1  48300  logbpw2m1  48301  fllog2  48302  blennnelnn  48310  blenpw2  48312  blennnt2  48323  nnolog2flm1  48324  dig2nn0ld  48338  dig2nn1st  48339  0dig2pr01  48344  aacllem  48895