Theorem uzid 12980

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144   class class class wbr 5102  ‘cfv 6538   ≤ cle 11344  ℤcz 12693  ℤ_≥cuz 12965

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-cnex 11256  ax-resscn 11257  ax-pre-lttri 11274

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  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 3739  df-csb 3847  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7423  df-er 8717  df-en 8974  df-dom 8975  df-sdom 8976  df-pnf 11345  df-mnf 11346  df-xr 11347  df-ltxr 11348  df-le 11349  df-neg 11544  df-z 12694  df-uz 12966

This theorem is used by:  uzidd  12981  uzn0  12982  uz11  12990  uzinfi  13055  uzsupss  13067  eluzfz1  13664  eluzfz2  13665  elfz3  13667  elfz1end  13688  fzssp1  13701  fzpred  13706  fzp1ss  13709  fzpr  13713  fztp  13714  elfz0add  13760  fzolb  13800  zpnn0elfzo  13873  fzosplitsnm1  13875  fzofzp1  13899  fzosplitsn  13911  fzostep1  13921  om2uzuzi  14092  axdc4uzlem  14126  seqf  14166  seqfveq  14169  seq1p  14179  faclbnd3  14436  bcm1k  14459  bcn2  14463  seqcoll  14609  swrds1  14816  pfxccatpfx2  14886  rexuz3  15516  r19.2uz  15519  cau3lem  15522  caubnd2  15525  climconst  15710  climuni  15719  isercoll2  15836  climsup  15837  climcau  15838  serf0  15848  iseralt  15852  fsumcvg3  15895  fsumparts  15973  o1fsum  15980  abscvgcvg  15986  isum1p  16010  isumrpcl  16012  isumsup2  16015  climcndslem1  16018  climcndslem2  16019  climcnds  16020  cvgrat  16052  mertenslem1  16053  fprodabs  16141  binomfallfaclem2  16206  fprodefsum  16261  eftlub  16277  rpnnen2lem11  16392  bitsfzo  16605  bitsinv1  16612  smupval  16658  seq1st  16746  algr0  16747  eucalg  16762  2mulprm  16868  prmdvdsbc  16902  oddprm  16988  pcfac  17077  pcbc  17078  vdwlem6  17164  prmlem0  17283  gsumprval  18877  efgsres  19952  telgsumfzs  20203  lmconst  23579  lmmo  23698  zfbas  24215  uzrest  24216  iscau2  25598  iscau4  25600  caun0  25602  caussi  25618  equivcau  25621  lmcau  25634  mbfsup  25985  mbfinf  25986  mbflimsup  25987  plyco0  26510  dvply2g  26606  geolim3  26666  aaliou3lem2  26670  aaliou3lem3  26671  ulm2  26712  ulm0  26718  ulmcaulem  26721  ulmcau  26722  ulmss  26724  ulmcn  26726  ulmdvlem3  26729  ulmdv  26730  abelthlem7  26765  2logb9irr  27123  sqrt2cxp2logb9e3  27127  ppinprm  27479  chtnprm  27481  ppiublem1  27529  chtublem  27538  chtub  27539  bposlem6  27616  lgsqr  27678  lgseisenlem4  27705  lgsquadlem1  27707  lgsquad2  27713  pntpbnd1  27913  pntlemf  27932  ostth2lem2  27961  flt4lem2  27977  istrkg2ld  28922  axlowdimlem17  29536  clwwlkvbij  30704  2clwwlk2  30949  numclwlk2lem2f  30978  fzdif2  33382  esumcvg  34718  dya2ub  34902  dya2icoseg  34909  sseqmw  35023  sseqf  35024  ballotlemfp1  35124  iprodefisumlem  36505  poimirlem1  38540  poimirlem2  38541  poimirlem3  38542  poimirlem4  38543  poimirlem6  38545  poimirlem7  38546  poimirlem8  38547  poimirlem9  38548  poimirlem13  38552  poimirlem14  38553  poimirlem15  38554  poimirlem16  38555  poimirlem17  38556  poimirlem18  38557  poimirlem19  38558  poimirlem20  38559  poimirlem21  38560  poimirlem22  38561  poimirlem23  38562  poimirlem24  38563  poimirlem26  38565  poimirlem27  38566  poimirlem31  38570  poimirlem32  38571  mblfinlem2  38577  sdclem1  38678  fdc  38680  seqpo  38682  incsequz2  38684  geomcau  38694  bfplem2  38758  3lexlogpow2ineq1  43109  eq0rabdioph  43787  rexrabdioph  43801  jm3.1lem1  44024  dvgrat  45296  rexanuz3  46111  uzfissfz  46338  allbutfi  46404  uzid2  46415  fmul01lt1lem1  46596  climinf  46618  climsuse  46620  limsupvaluz2  46748  supcnvlimsup  46750  ioodvbdlimc1lem2  46942  ioodvbdlimc2lem  46944  iblspltprt  46983  stoweidlem7  47017  wallispilem1  47075  wallispilem4  47078  dirkertrigeqlem1  47108  sge0isum  47437  sge0reuzb  47458  carageniuncllem1  47531  caratheodorylem1  47536  smflimlem1  47781  smflimlem2  47782  smflim  47787  smfsuplem1  47821  smfsuplem3  47823  smflimsuplem1  47830  smflimsuplem2  47831  iccpartres  48500  iccelpart  48515  4fppr1  48833  pgnioedg1  49206  pgnioedg2  49207  pgnioedg3  49208  pgnioedg4  49209  pgnbgreunbgrlem1  49211  pgnbgreunbgrlem4  49217  fldivexpfllog2  49677  nnlog2ge0lt1  49678  logbpw2m1  49679  fllog2  49680  blennnelnn  49688  blenpw2  49690  blennnt2  49701  nnolog2flm1  49702  dig2nn0ld  49716  dig2nn1st  49717  0dig2pr01  49722  aacllem  50939