Theorem uzid 12906

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 23	. 2 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℤ)
2		zre 12623	. . 3 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
3	2	leidd 11808	. 2 ⊢ (𝑀 ∈ ℤ → 𝑀 ≤ 𝑀)
4		eluz1 12895	. 2 ⊢ (𝑀 ∈ ℤ → (𝑀 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝑀)))
5	1, 3, 4	mpbir2and 726	1 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑀))

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   class class class wbr 5107  ‘cfv 6537   ≤ cle 11272  ℤcz 12619  ℤ_≥cuz 12891

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7740  ax-cnex 11184  ax-resscn 11185  ax-pre-lttri 11202

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7420  df-er 8700  df-en 8957  df-dom 8958  df-sdom 8959  df-pnf 11273  df-mnf 11274  df-xr 11275  df-ltxr 11276  df-le 11277  df-neg 11472  df-z 12620  df-uz 12892

This theorem is used by:  uzidd  12907  uzn0  12908  uz11  12916  uzinfi  12981  uzsupss  12993  eluzfz1  13589  eluzfz2  13590  elfz3  13592  elfz1end  13613  fzssp1  13626  fzpred  13631  fzp1ss  13634  fzpr  13638  fztp  13639  elfz0add  13685  fzolb  13725  zpnn0elfzo  13798  fzosplitsnm1  13800  fzofzp1  13824  fzosplitsn  13836  fzostep1  13846  om2uzuzi  14017  axdc4uzlem  14051  seqf  14091  seqfveq  14094  seq1p  14104  faclbnd3  14360  bcm1k  14383  bcn2  14387  seqcoll  14533  swrds1  14740  pfxccatpfx2  14810  rexuz3  15440  r19.2uz  15443  cau3lem  15446  caubnd2  15449  climconst  15634  climuni  15643  isercoll2  15760  climsup  15761  climcau  15762  serf0  15772  iseralt  15776  fsumcvg3  15819  fsumparts  15897  o1fsum  15904  abscvgcvg  15910  isum1p  15934  isumrpcl  15936  isumsup2  15939  climcndslem1  15942  climcndslem2  15943  climcnds  15944  cvgrat  15976  mertenslem1  15977  fprodabs  16067  binomfallfaclem2  16132  fprodefsum  16187  eftlub  16203  rpnnen2lem11  16318  bitsfzo  16531  bitsinv1  16538  smupval  16584  seq1st  16667  algr0  16668  eucalg  16683  2mulprm  16789  prmdvdsbc  16823  oddprm  16908  pcfac  16997  pcbc  16998  vdwlem6  17084  prmlem0  17203  gsumprval  18796  efgsres  19871  telgsumfzs  20122  lmconst  23492  lmmo  23611  zfbas  24128  uzrest  24129  iscau2  25511  iscau4  25513  caun0  25515  caussi  25531  equivcau  25534  lmcau  25547  mbfsup  25898  mbfinf  25899  mbflimsup  25900  plyco0  26424  dvply2g  26522  geolim3  26582  aaliou3lem2  26586  aaliou3lem3  26587  ulm2  26628  ulm0  26634  ulmcaulem  26637  ulmcau  26638  ulmss  26640  ulmcn  26642  ulmdvlem3  26645  ulmdv  26646  abelthlem7  26681  2logb9irr  27040  sqrt2cxp2logb9e3  27044  ppinprm  27396  chtnprm  27398  ppiublem1  27446  chtublem  27455  chtub  27456  bposlem6  27533  lgsqr  27595  lgseisenlem4  27622  lgsquadlem1  27624  lgsquad2  27630  pntpbnd1  27830  pntlemf  27849  ostth2lem2  27878  istrkg2ld  28809  axlowdimlem17  29423  clwwlkvbij  30591  2clwwlk2  30836  numclwlk2lem2f  30865  fzdif2  33269  esumcvg  34604  dya2ub  34789  dya2icoseg  34796  sseqmw  34910  sseqf  34911  ballotlemfp1  35011  iprodefisumlem  36327  poimirlem1  38378  poimirlem2  38379  poimirlem3  38380  poimirlem4  38381  poimirlem6  38383  poimirlem7  38384  poimirlem8  38385  poimirlem9  38386  poimirlem13  38390  poimirlem14  38391  poimirlem15  38392  poimirlem16  38393  poimirlem17  38394  poimirlem18  38395  poimirlem19  38396  poimirlem20  38397  poimirlem21  38398  poimirlem22  38399  poimirlem23  38400  poimirlem24  38401  poimirlem26  38403  poimirlem27  38404  poimirlem31  38408  poimirlem32  38409  mblfinlem2  38415  sdclem1  38501  fdc  38503  seqpo  38505  incsequz2  38507  geomcau  38517  bfplem2  38581  3lexlogpow2ineq1  42932  flt4lem2  43501  eq0rabdioph  43629  rexrabdioph  43643  jm3.1lem1  43866  dvgrat  45144  rexanuz3  45936  uzfissfz  46164  allbutfi  46230  uzid2  46241  fmul01lt1lem1  46422  climinf  46444  climsuse  46446  limsupvaluz2  46574  supcnvlimsup  46576  ioodvbdlimc1lem2  46768  ioodvbdlimc2lem  46770  iblspltprt  46809  stoweidlem7  46843  wallispilem1  46901  wallispilem4  46904  dirkertrigeqlem1  46934  sge0isum  47263  sge0reuzb  47284  carageniuncllem1  47357  caratheodorylem1  47362  smflimlem1  47607  smflimlem2  47608  smflim  47613  smfsuplem1  47647  smfsuplem3  47649  smflimsuplem1  47656  smflimsuplem2  47657  iccpartres  48326  iccelpart  48341  4fppr1  48659  pgnioedg1  49032  pgnioedg2  49033  pgnioedg3  49034  pgnioedg4  49035  pgnbgreunbgrlem1  49037  pgnbgreunbgrlem4  49043  fldivexpfllog2  49503  nnlog2ge0lt1  49504  logbpw2m1  49505  fllog2  49506  blennnelnn  49514  blenpw2  49516  blennnt2  49527  nnolog2flm1  49528  dig2nn0ld  49542  dig2nn1st  49543  0dig2pr01  49548  aacllem  50780