Theorem eluzelz 12798

Description: A member of an upper set of integers is an integer. (Contributed by NM, 6-Sep-2005.)

Assertion

Ref	Expression
eluzelz	⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ)

Proof of Theorem eluzelz

Step	Hyp	Ref	Expression
1		eluz2 12794	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))
2	1	simp2bi 1147	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5085  ‘cfv 6498   ≤ cle 11180  ℤcz 12524  ℤ_≥cuz 12788

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 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375  ax-cnex 11094  ax-resscn 11095

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-fv 6506  df-ov 7370  df-neg 11380  df-z 12525  df-uz 12789

This theorem is referenced by:  eluzelre  12799  uztrn  12806  uzneg  12808  uzss  12811  eluzp1l  12815  eluzadd  12817  eluzsub  12818  subeluzsub  12821  uzm1  12822  uzin  12824  uzind4  12856  uzwo  12861  uz2mulcl  12876  uzsupss  12890  elfz5  13470  elfzel2  13476  elfzelz  13478  eluzfz2  13486  peano2fzr  13491  fzsplit2  13503  fzopth  13515  ssfzunsn  13524  fzsuc  13525  elfz1uz  13548  uzsplit  13550  uzdisj  13551  fzm1  13561  uznfz  13564  nn0disj  13598  preduz  13604  elfzo3  13631  fzoss2  13642  fzouzsplit  13649  fzoun  13651  eluzgtdifelfzo  13682  fzosplitsnm1  13695  fzofzp1b  13720  elfzonelfzo  13724  fzosplitsn  13731  fzisfzounsn  13735  fldiv4lem1div2uz2  13795  m1modge3gt1  13880  modaddmodup  13896  om2uzlti  13912  om2uzf1oi  13915  uzrdgxfr  13929  fzen2  13931  seqfveq2  13986  seqfeq2  13987  seqshft2  13990  monoord  13994  monoord2  13995  sermono  13996  seqsplit  13997  seqf1olem1  14003  seqf1olem2  14004  seqid  14009  leexp2a  14134  expnlbnd2  14196  expmulnbnd  14197  hashfz  14389  fzsdom2  14390  hashfzo  14391  hashfzp1  14393  seqcoll  14426  swrdfv2  14624  pfxccatin12  14695  rexuz3  15311  r19.2uz  15314  rexuzre  15315  cau4  15319  caubnd2  15320  clim  15456  climrlim2  15509  climshft2  15544  climaddc1  15597  climmulc2  15599  climsubc1  15600  climsubc2  15601  clim2ser  15617  clim2ser2  15618  iserex  15619  climlec2  15621  climub  15624  isercolllem2  15628  isercoll  15630  isercoll2  15631  climcau  15633  caurcvg2  15640  caucvgb  15642  serf0  15643  iseraltlem1  15644  iseraltlem2  15645  iseralt  15647  sumrblem  15673  fsumcvg  15674  summolem2a  15677  fsumcvg2  15689  fsumm1  15713  fzosump1  15714  fsump1  15718  fsumrev2  15744  telfsumo  15765  fsumparts  15769  isumsplit  15805  isumrpcl  15808  isumsup2  15811  cvgrat  15848  mertenslem1  15849  clim2div  15854  prodeq2ii  15876  fprodcvg  15895  prodmolem2a  15899  zprod  15902  fprodntriv  15907  fprodser  15914  fprodm1  15932  fprodp1  15934  fprodeq0  15940  isprm3  16652  nprm  16657  dvdsprm  16673  exprmfct  16674  isprm5  16677  maxprmfct  16679  prmdvdsncoprmbd  16697  ncoprmlnprm  16698  phibndlem  16740  dfphi2  16744  hashdvds  16745  pcaddlem  16859  pcfac  16870  expnprm  16873  prmreclem4  16890  vdwlem8  16959  gsumval2a  18653  efgs1b  19711  telgsumfzs  19964  iscau4  25246  caucfil  25250  iscmet3lem3  25257  iscmet3lem1  25258  iscmet3lem2  25259  lmle  25268  uniioombllem3  25552  mbflimsup  25633  mbfi1fseqlem6  25687  dvfsumle  25988  dvfsumge  25989  dvfsumabs  25990  aaliou3lem1  26308  aaliou3lem2  26309  ulmres  26353  ulmshftlem  26354  ulmshft  26355  ulmcaulem  26359  ulmcau  26360  ulmdvlem1  26365  radcnvlem1  26378  logblt  26748  logbgcd1irr  26758  muval1  27096  chtdif  27121  ppidif  27126  chtub  27175  bcmono  27240  bpos1lem  27245  lgsquad2lem2  27348  2sqlem6  27386  2sqlem8a  27388  2sqlem8  27389  chebbnd1lem1  27432  dchrisumlem2  27453  dchrisum0lem1  27479  ostthlem2  27591  ostth2  27600  axlowdimlem3  29013  axlowdimlem6  29016  axlowdimlem7  29017  axlowdimlem16  29026  axlowdimlem17  29027  axlowdim  29030  clwwnrepclwwn  30414  fzspl  32862  fzdif2  32863  supfz  35911  divcnvlin  35915  nn0prpwlem  36504  fdc  38066  mettrifi  38078  caushft  38082  aks4d1lem1  42501  aks4d1p1  42515  aks4d1p2  42516  aks4d1p3  42517  aks4d1p5  42519  aks4d1p6  42520  aks4d1p7d1  42521  aks4d1p7  42522  aks4d1p8  42526  aks4d1p9  42527  aks6d1c7lem1  42619  aks6d1c7lem2  42620  aks6d1c7  42623  aks5lem6  42631  aks5lem8  42640  aks5  42643  fzosumm1  42689  dffltz  43067  rmspecnonsq  43335  rmspecfund  43337  rmxyadd  43349  rmxy1  43350  jm2.18  43416  jm2.22  43423  jm2.15nn0  43431  jm2.16nn0  43432  jm2.27a  43433  jm2.27c  43435  jm3.1lem2  43446  jm3.1lem3  43447  jm3.1  43448  expdiophlem1  43449  dvgrat  44739  cvgdvgrat  44740  hashnzfz  44747  uzwo4  45484  ssinc  45517  ssdec  45518  rexanuz3  45526  monoords  45730  fzdifsuc2  45743  iuneqfzuzlem  45764  eluzelzd  45804  allbutfi  45822  eluzelz2  45831  uzid2  45833  monoordxrv  45909  monoord2xrv  45911  fmul01  46010  fmul01lt1lem1  46014  fmul01lt1lem2  46015  climsuselem1  46037  climsuse  46038  climf  46052  climresmpt  46087  climf2  46094  limsupequzlem  46150  limsupmnfuzlem  46154  limsupre3uzlem  46163  itgsinexp  46383  iblspltprt  46401  itgspltprt  46407  iundjiun  46888  smflimsuplem2  47249  smflimsuplem4  47251  smflimsuplem5  47252  fzopredsuc  47772  m1modmmod  47812  smonoord  47825  2timesltsq  47826  2timesltsqm1  47827  iccpartiltu  47882  nprmmul1  47987  fmtnoprmfac2lem1  48029  fmtnofac2lem  48031  lighneallem2  48069  lighneallem4a  48071  lighneallem4b  48072  nprmdvdsfacm1lem1  48083  nprmdvdsfacm1lem4  48086  ppivalnnprm  48088  ppivalnnnprmge6  48089  ppivalnn  48095  fppr2odd  48207  fpprwpprb  48216  gboge9  48240  nnsum3primesle9  48270  nnsum4primesevenALTV  48277  wtgoldbnnsum4prm  48278  bgoldbnnsum3prm  48280  bgoldbtbndlem2  48282  gpgusgralem  48532  gpgprismgr4cycllem9  48579  fllogbd  49036  fllog2  49044  dignn0ldlem  49078  dignnld  49079  digexp  49083  dignn0flhalf  49094  nn0sumshdiglemB  49096