Theorem uzid 12935

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   class class class wbr 5103  ‘cfv 6528   ≤ cle 11301  ℤcz 12648  ℤ_≥cuz 12920

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 2213  ax-ext 2732  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7735  ax-cnex 11213  ax-resscn 11214  ax-pre-lttri 11231

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5543  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-iota 6484  df-fun 6530  df-fn 6531  df-f 6532  df-f1 6533  df-fo 6534  df-f1o 6535  df-fv 6536  df-ov 7412  df-er 8696  df-en 8953  df-dom 8954  df-sdom 8955  df-pnf 11302  df-mnf 11303  df-xr 11304  df-ltxr 11305  df-le 11306  df-neg 11501  df-z 12649  df-uz 12921

This theorem is used by:  uzidd  12936  uzn0  12937  uz11  12945  uzinfi  13010  uzsupss  13022  eluzfz1  13618  eluzfz2  13619  elfz3  13621  elfz1end  13642  fzssp1  13655  fzpred  13660  fzp1ss  13663  fzpr  13667  fztp  13668  elfz0add  13714  fzolb  13754  zpnn0elfzo  13827  fzosplitsnm1  13829  fzofzp1  13853  fzosplitsn  13865  fzostep1  13875  om2uzuzi  14046  axdc4uzlem  14080  seqf  14120  seqfveq  14123  seq1p  14133  faclbnd3  14389  bcm1k  14412  bcn2  14416  seqcoll  14562  swrds1  14769  pfxccatpfx2  14839  rexuz3  15469  r19.2uz  15472  cau3lem  15475  caubnd2  15478  climconst  15663  climuni  15672  isercoll2  15789  climsup  15790  climcau  15791  serf0  15801  iseralt  15805  fsumcvg3  15848  fsumparts  15926  o1fsum  15933  abscvgcvg  15939  isum1p  15963  isumrpcl  15965  isumsup2  15968  climcndslem1  15971  climcndslem2  15972  climcnds  15973  cvgrat  16005  mertenslem1  16006  fprodabs  16094  binomfallfaclem2  16159  fprodefsum  16214  eftlub  16230  rpnnen2lem11  16345  bitsfzo  16558  bitsinv1  16565  smupval  16611  seq1st  16694  algr0  16695  eucalg  16710  2mulprm  16816  prmdvdsbc  16850  oddprm  16935  pcfac  17024  pcbc  17025  vdwlem6  17111  prmlem0  17230  gsumprval  18824  efgsres  19899  telgsumfzs  20150  lmconst  23526  lmmo  23645  zfbas  24162  uzrest  24163  iscau2  25545  iscau4  25547  caun0  25549  caussi  25565  equivcau  25568  lmcau  25581  mbfsup  25932  mbfinf  25933  mbflimsup  25934  plyco0  26457  dvply2g  26555  geolim3  26615  aaliou3lem2  26619  aaliou3lem3  26620  ulm2  26661  ulm0  26667  ulmcaulem  26670  ulmcau  26671  ulmss  26673  ulmcn  26675  ulmdvlem3  26678  ulmdv  26679  abelthlem7  26714  2logb9irr  27072  sqrt2cxp2logb9e3  27076  ppinprm  27428  chtnprm  27430  ppiublem1  27478  chtublem  27487  chtub  27488  bposlem6  27565  lgsqr  27627  lgseisenlem4  27654  lgsquadlem1  27656  lgsquad2  27662  pntpbnd1  27862  pntlemf  27881  ostth2lem2  27910  istrkg2ld  28841  axlowdimlem17  29455  clwwlkvbij  30623  2clwwlk2  30868  numclwlk2lem2f  30897  fzdif2  33301  esumcvg  34637  dya2ub  34822  dya2icoseg  34829  sseqmw  34943  sseqf  34944  ballotlemfp1  35044  iprodefisumlem  36420  poimirlem1  38453  poimirlem2  38454  poimirlem3  38455  poimirlem4  38456  poimirlem6  38458  poimirlem7  38459  poimirlem8  38460  poimirlem9  38461  poimirlem13  38465  poimirlem14  38466  poimirlem15  38467  poimirlem16  38468  poimirlem17  38469  poimirlem18  38470  poimirlem19  38471  poimirlem20  38472  poimirlem21  38473  poimirlem22  38474  poimirlem23  38475  poimirlem24  38476  poimirlem26  38478  poimirlem27  38479  poimirlem31  38483  poimirlem32  38484  mblfinlem2  38490  sdclem1  38591  fdc  38593  seqpo  38595  incsequz2  38597  geomcau  38607  bfplem2  38671  3lexlogpow2ineq1  43022  flt4lem2  43591  eq0rabdioph  43719  rexrabdioph  43733  jm3.1lem1  43956  dvgrat  45234  rexanuz3  46026  uzfissfz  46254  allbutfi  46320  uzid2  46331  fmul01lt1lem1  46512  climinf  46534  climsuse  46536  limsupvaluz2  46664  supcnvlimsup  46666  ioodvbdlimc1lem2  46858  ioodvbdlimc2lem  46860  iblspltprt  46899  stoweidlem7  46933  wallispilem1  46991  wallispilem4  46994  dirkertrigeqlem1  47024  sge0isum  47353  sge0reuzb  47374  carageniuncllem1  47447  caratheodorylem1  47452  smflimlem1  47697  smflimlem2  47698  smflim  47703  smfsuplem1  47737  smfsuplem3  47739  smflimsuplem1  47746  smflimsuplem2  47747  iccpartres  48416  iccelpart  48431  4fppr1  48749  pgnioedg1  49122  pgnioedg2  49123  pgnioedg3  49124  pgnioedg4  49125  pgnbgreunbgrlem1  49127  pgnbgreunbgrlem4  49133  fldivexpfllog2  49593  nnlog2ge0lt1  49594  logbpw2m1  49595  fllog2  49596  blennnelnn  49604  blenpw2  49606  blennnt2  49617  nnolog2flm1  49618  dig2nn0ld  49632  dig2nn1st  49633  0dig2pr01  49638  aacllem  50855