Theorem eluzelz 12789

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 12785	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))
2	1	simp2bi 1152	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2119   class class class wbr 5072  ‘cfv 6485   ≤ cle 11171  ℤcz 12515  ℤ_≥cuz 12779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pr 5362  ax-cnex 11085  ax-resscn 11086

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-fv 6493  df-ov 7359  df-neg 11371  df-z 12516  df-uz 12780

This theorem is referenced by:  eluzelre  12790  uztrn  12797  uzneg  12799  uzss  12802  eluzp1l  12806  eluzadd  12808  eluzsub  12809  subeluzsub  12812  uzm1  12813  uzin  12815  uzind4  12847  uzwo  12852  uz2mulcl  12867  uzsupss  12881  elfz5  13461  elfzel2  13467  elfzelz  13469  eluzfz2  13477  peano2fzr  13482  fzsplit2  13494  fzopth  13506  ssfzunsn  13515  fzsuc  13516  elfz1uz  13539  uzsplit  13541  uzdisj  13542  fzm1  13552  uznfz  13555  nn0disj  13589  preduz  13595  elfzo3  13622  fzoss2  13633  fzouzsplit  13640  fzoun  13642  eluzgtdifelfzo  13673  fzosplitsnm1  13686  fzofzp1b  13711  elfzonelfzo  13715  fzosplitsn  13722  fzisfzounsn  13726  fldiv4lem1div2uz2  13786  m1modge3gt1  13871  modaddmodup  13887  om2uzlti  13903  om2uzf1oi  13906  uzrdgxfr  13920  fzen2  13922  seqfveq2  13977  seqfeq2  13978  seqshft2  13981  monoord  13985  monoord2  13986  sermono  13987  seqsplit  13988  seqf1olem1  13994  seqf1olem2  13995  seqid  14000  leexp2a  14125  expnlbnd2  14187  expmulnbnd  14188  hashfz  14380  fzsdom2  14381  hashfzo  14382  hashfzp1  14384  seqcoll  14417  swrdfv2  14615  pfxccatin12  14686  rexuz3  15302  r19.2uz  15305  rexuzre  15306  cau4  15310  caubnd2  15311  clim  15447  climrlim2  15500  climshft2  15535  climaddc1  15588  climmulc2  15590  climsubc1  15591  climsubc2  15592  clim2ser  15608  clim2ser2  15609  iserex  15610  climlec2  15612  climub  15615  isercolllem2  15619  isercoll  15621  isercoll2  15622  climcau  15624  caurcvg2  15631  caucvgb  15633  serf0  15634  iseraltlem1  15635  iseraltlem2  15636  iseralt  15638  sumrblem  15664  fsumcvg  15665  summolem2a  15668  fsumcvg2  15680  fsumm1  15704  fzosump1  15705  fsump1  15709  fsumrev2  15735  telfsumo  15756  fsumparts  15760  isumsplit  15796  isumrpcl  15799  isumsup2  15802  cvgrat  15839  mertenslem1  15840  clim2div  15845  prodeq2ii  15867  fprodcvg  15886  prodmolem2a  15890  zprod  15893  fprodntriv  15898  fprodser  15905  fprodm1  15923  fprodp1  15925  fprodeq0  15931  isprm3  16643  nprm  16648  dvdsprm  16664  exprmfct  16665  isprm5  16668  maxprmfct  16670  prmdvdsncoprmbd  16688  ncoprmlnprm  16689  phibndlem  16731  dfphi2  16735  hashdvds  16736  pcaddlem  16850  pcfac  16861  expnprm  16864  prmreclem4  16881  vdwlem8  16950  gsumval2a  18644  efgs1b  19702  telgsumfzs  19955  iscau4  25264  caucfil  25268  iscmet3lem3  25275  iscmet3lem1  25276  iscmet3lem2  25277  lmle  25286  uniioombllem3  25570  mbflimsup  25651  mbfi1fseqlem6  25705  dvfsumle  26006  dvfsumge  26007  dvfsumabs  26008  aaliou3lem1  26326  aaliou3lem2  26327  ulmres  26371  ulmshftlem  26372  ulmshft  26373  ulmcaulem  26377  ulmcau  26378  ulmdvlem1  26383  radcnvlem1  26396  logblt  26766  logbgcd1irr  26776  muval1  27114  chtdif  27139  ppidif  27144  chtub  27193  bcmono  27258  bpos1lem  27263  lgsquad2lem2  27366  2sqlem6  27404  2sqlem8a  27406  2sqlem8  27407  chebbnd1lem1  27450  dchrisumlem2  27471  dchrisum0lem1  27497  ostthlem2  27609  ostth2  27618  axlowdimlem3  29031  axlowdimlem6  29034  axlowdimlem7  29035  axlowdimlem16  29044  axlowdimlem17  29045  axlowdim  29048  clwwnrepclwwn  30432  fzspl  32881  fzdif2  32882  supfz  35957  divcnvlin  35961  nn0prpwlem  36550  fdc  38112  mettrifi  38124  caushft  38128  aks4d1lem1  42547  aks4d1p1  42561  aks4d1p2  42562  aks4d1p3  42563  aks4d1p5  42565  aks4d1p6  42566  aks4d1p7d1  42567  aks4d1p7  42568  aks4d1p8  42572  aks4d1p9  42573  aks6d1c7lem1  42665  aks6d1c7lem2  42666  aks6d1c7  42669  aks5lem6  42677  aks5lem8  42686  aks5  42689  fzosumm1  42734  dffltz  43084  rmspecnonsq  43352  rmspecfund  43354  rmxyadd  43366  rmxy1  43367  jm2.18  43433  jm2.22  43440  jm2.15nn0  43448  jm2.16nn0  43449  jm2.27a  43450  jm2.27c  43452  jm3.1lem2  43463  jm3.1lem3  43464  jm3.1  43465  expdiophlem1  43466  dvgrat  44756  cvgdvgrat  44757  hashnzfz  44764  uzwo4  45501  ssinc  45534  ssdec  45535  rexanuz3  45543  monoords  45745  fzdifsuc2  45758  iuneqfzuzlem  45779  eluzelzd  45819  allbutfi  45837  eluzelz2  45846  uzid2  45848  monoordxrv  45924  monoord2xrv  45926  fmul01  46025  fmul01lt1lem1  46029  fmul01lt1lem2  46030  climsuselem1  46052  climsuse  46053  climf  46067  climresmpt  46102  climf2  46109  limsupequzlem  46165  limsupmnfuzlem  46169  limsupre3uzlem  46178  itgsinexp  46398  iblspltprt  46416  itgspltprt  46422  iundjiun  46903  smflimsuplem2  47264  smflimsuplem4  47266  smflimsuplem5  47267  fzopredsuc  47787  m1modmmod  47827  smonoord  47840  2timesltsq  47841  2timesltsqm1  47842  iccpartiltu  47897  nprmmul1  48002  fmtnoprmfac2lem1  48044  fmtnofac2lem  48046  lighneallem2  48084  lighneallem4a  48086  lighneallem4b  48087  nprmdvdsfacm1lem1  48098  nprmdvdsfacm1lem4  48101  ppivalnnprm  48103  ppivalnnnprmge6  48104  ppivalnn  48110  fppr2odd  48222  fpprwpprb  48231  gboge9  48255  nnsum3primesle9  48285  nnsum4primesevenALTV  48292  wtgoldbnnsum4prm  48293  bgoldbnnsum3prm  48295  bgoldbtbndlem2  48297  gpgusgralem  48547  gpgprismgr4cycllem9  48594  fllogbd  49051  fllog2  49059  dignn0ldlem  49093  dignnld  49094  digexp  49098  dignn0flhalf  49109  nn0sumshdiglemB  49111