Theorem uzid 12768

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 12494	. . 3 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
3	2	leidd 11705	. 2 ⊢ (𝑀 ∈ ℤ → 𝑀 ≤ 𝑀)
4		eluz1 12757	. 2 ⊢ (𝑀 ∈ ℤ → (𝑀 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝑀)))
5	1, 3, 4	mpbir2and 714	1 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑀))

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5097  ‘cfv 6491   ≤ cle 11169  ℤcz 12490  ℤ_≥cuz 12753

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2183  ax-ext 2707  ax-sep 5240  ax-nul 5250  ax-pow 5309  ax-pr 5376  ax-un 7680  ax-cnex 11084  ax-resscn 11085  ax-pre-lttri 11102

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2538  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3060  df-rab 3399  df-v 3441  df-sbc 3740  df-csb 3849  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-nul 4285  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-iota 6447  df-fun 6493  df-fn 6494  df-f 6495  df-f1 6496  df-fo 6497  df-f1o 6498  df-fv 6499  df-ov 7361  df-er 8635  df-en 8886  df-dom 8887  df-sdom 8888  df-pnf 11170  df-mnf 11171  df-xr 11172  df-ltxr 11173  df-le 11174  df-neg 11369  df-z 12491  df-uz 12754

This theorem is referenced by:  uzidd  12769  uzn0  12770  uz11  12778  uzinfi  12843  uzsupss  12855  eluzfz1  13449  eluzfz2  13450  elfz3  13452  elfz1end  13472  fzssp1  13485  fzpred  13490  fzp1ss  13493  fzpr  13497  fztp  13498  elfz0add  13544  fzolb  13583  zpnn0elfzo  13656  fzosplitsnm1  13658  fzofzp1  13682  fzosplitsn  13694  fzostep1  13704  om2uzuzi  13874  axdc4uzlem  13908  seqf  13948  seqfveq  13951  seq1p  13961  faclbnd3  14217  bcm1k  14240  bcn2  14244  seqcoll  14389  swrds1  14592  pfxccatpfx2  14662  rexuz3  15274  r19.2uz  15277  cau3lem  15280  caubnd2  15283  climconst  15468  climuni  15477  isercoll2  15594  climsup  15595  climcau  15596  serf0  15606  iseralt  15610  fsumcvg3  15654  fsumparts  15731  o1fsum  15738  abscvgcvg  15744  isum1p  15766  isumrpcl  15768  isumsup2  15771  climcndslem1  15774  climcndslem2  15775  climcnds  15776  cvgrat  15808  mertenslem1  15809  fprodabs  15899  binomfallfaclem2  15965  fprodefsum  16020  eftlub  16036  rpnnen2lem11  16151  bitsfzo  16364  bitsinv1  16371  smupval  16417  seq1st  16500  algr0  16501  eucalg  16516  2mulprm  16622  prmdvdsbc  16655  oddprm  16740  pcfac  16829  pcbc  16830  vdwlem6  16916  prmlem0  17035  gsumprval  18615  efgsres  19669  telgsumfzs  19920  lmconst  23207  lmmo  23326  zfbas  23842  uzrest  23843  iscau2  25235  iscau4  25237  caun0  25239  caussi  25255  equivcau  25258  lmcau  25271  mbfsup  25623  mbfinf  25624  mbflimsup  25625  plyco0  26155  dvply2g  26250  dvply2gOLD  26251  geolim3  26305  aaliou3lem2  26309  aaliou3lem3  26310  ulm2  26352  ulm0  26358  ulmcaulem  26361  ulmcau  26362  ulmss  26364  ulmcn  26366  ulmdvlem3  26369  ulmdv  26370  abelthlem7  26406  2logb9irr  26763  sqrt2cxp2logb9e3  26767  ppinprm  27120  chtnprm  27122  ppiublem1  27171  chtublem  27180  chtub  27181  bposlem6  27258  lgsqr  27320  lgseisenlem4  27347  lgsquadlem1  27349  lgsquad2  27355  pntpbnd1  27555  pntlemf  27574  ostth2lem2  27603  istrkg2ld  28513  axlowdimlem17  29012  clwwlkvbij  30169  2clwwlk2  30404  numclwlk2lem2f  30433  fzdif2  32849  esumcvg  34222  dya2ub  34406  dya2icoseg  34413  sseqmw  34527  sseqf  34528  ballotlemfp1  34628  iprodefisumlem  35913  poimirlem1  37791  poimirlem2  37792  poimirlem3  37793  poimirlem4  37794  poimirlem6  37796  poimirlem7  37797  poimirlem8  37798  poimirlem9  37799  poimirlem13  37803  poimirlem14  37804  poimirlem15  37805  poimirlem16  37806  poimirlem17  37807  poimirlem18  37808  poimirlem19  37809  poimirlem20  37810  poimirlem21  37811  poimirlem22  37812  poimirlem23  37813  poimirlem24  37814  poimirlem26  37816  poimirlem27  37817  poimirlem31  37821  poimirlem32  37822  mblfinlem2  37828  sdclem1  37913  fdc  37915  seqpo  37917  incsequz2  37919  geomcau  37929  bfplem2  37993  3lexlogpow2ineq1  42347  flt4lem2  42927  eq0rabdioph  43055  rexrabdioph  43073  jm3.1lem1  43296  dvgrat  44590  rexanuz3  45377  uzfissfz  45608  allbutfi  45674  uzid2  45686  fmul01lt1lem1  45867  climinf  45889  climsuse  45891  limsupvaluz2  46019  supcnvlimsup  46021  ioodvbdlimc1lem2  46213  ioodvbdlimc2lem  46215  iblspltprt  46254  stoweidlem7  46288  wallispilem1  46346  wallispilem4  46349  dirkertrigeqlem1  46379  sge0isum  46708  sge0reuzb  46729  carageniuncllem1  46802  caratheodorylem1  46807  smflimlem1  47052  smflimlem2  47053  smflim  47058  smfsuplem1  47092  smfsuplem3  47094  smflimsuplem1  47101  smflimsuplem2  47102  iccpartres  47701  iccelpart  47716  4fppr1  48018  pgnioedg1  48391  pgnioedg2  48392  pgnioedg3  48393  pgnioedg4  48394  pgnbgreunbgrlem1  48396  pgnbgreunbgrlem4  48402  fldivexpfllog2  48848  nnlog2ge0lt1  48849  logbpw2m1  48850  fllog2  48851  blennnelnn  48859  blenpw2  48861  blennnt2  48872  nnolog2flm1  48873  dig2nn0ld  48887  dig2nn1st  48888  0dig2pr01  48893  aacllem  50083