Theorem eluzelz 12792

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

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5086  ‘cfv 6493   ≤ cle 11174  ℤcz 12518  ℤ_≥cuz 12782

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 2709  ax-sep 5232  ax-nul 5242  ax-pr 5371  ax-cnex 11088  ax-resscn 11089

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-fv 6501  df-ov 7364  df-neg 11374  df-z 12519  df-uz 12783

This theorem is referenced by:  eluzelre  12793  uztrn  12800  uzneg  12802  uzss  12805  eluzp1l  12809  eluzadd  12811  eluzsub  12812  subeluzsub  12815  uzm1  12816  uzin  12818  uzind4  12850  uzwo  12855  uz2mulcl  12870  uzsupss  12884  elfz5  13464  elfzel2  13470  elfzelz  13472  eluzfz2  13480  peano2fzr  13485  fzsplit2  13497  fzopth  13509  ssfzunsn  13518  fzsuc  13519  elfz1uz  13542  uzsplit  13544  uzdisj  13545  fzm1  13555  uznfz  13558  nn0disj  13592  preduz  13598  elfzo3  13625  fzoss2  13636  fzouzsplit  13643  fzoun  13645  eluzgtdifelfzo  13676  fzosplitsnm1  13689  fzofzp1b  13714  elfzonelfzo  13718  fzosplitsn  13725  fzisfzounsn  13729  fldiv4lem1div2uz2  13789  m1modge3gt1  13874  modaddmodup  13890  om2uzlti  13906  om2uzf1oi  13909  uzrdgxfr  13923  fzen2  13925  seqfveq2  13980  seqfeq2  13981  seqshft2  13984  monoord  13988  monoord2  13989  sermono  13990  seqsplit  13991  seqf1olem1  13997  seqf1olem2  13998  seqid  14003  leexp2a  14128  expnlbnd2  14190  expmulnbnd  14191  hashfz  14383  fzsdom2  14384  hashfzo  14385  hashfzp1  14387  seqcoll  14420  swrdfv2  14618  pfxccatin12  14689  rexuz3  15305  r19.2uz  15308  rexuzre  15309  cau4  15313  caubnd2  15314  clim  15450  climrlim2  15503  climshft2  15538  climaddc1  15591  climmulc2  15593  climsubc1  15594  climsubc2  15595  clim2ser  15611  clim2ser2  15612  iserex  15613  climlec2  15615  climub  15618  isercolllem2  15622  isercoll  15624  isercoll2  15625  climcau  15627  caurcvg2  15634  caucvgb  15636  serf0  15637  iseraltlem1  15638  iseraltlem2  15639  iseralt  15641  sumrblem  15667  fsumcvg  15668  summolem2a  15671  fsumcvg2  15683  fsumm1  15707  fzosump1  15708  fsump1  15712  fsumrev2  15738  telfsumo  15759  fsumparts  15763  isumsplit  15799  isumrpcl  15802  isumsup2  15805  cvgrat  15842  mertenslem1  15843  clim2div  15848  prodeq2ii  15870  fprodcvg  15889  prodmolem2a  15893  zprod  15896  fprodntriv  15901  fprodser  15908  fprodm1  15926  fprodp1  15928  fprodeq0  15934  isprm3  16646  nprm  16651  dvdsprm  16667  exprmfct  16668  isprm5  16671  maxprmfct  16673  prmdvdsncoprmbd  16691  ncoprmlnprm  16692  phibndlem  16734  dfphi2  16738  hashdvds  16739  pcaddlem  16853  pcfac  16864  expnprm  16867  prmreclem4  16884  vdwlem8  16953  gsumval2a  18647  efgs1b  19705  telgsumfzs  19958  iscau4  25259  caucfil  25263  iscmet3lem3  25270  iscmet3lem1  25271  iscmet3lem2  25272  lmle  25281  uniioombllem3  25565  mbflimsup  25646  mbfi1fseqlem6  25700  dvfsumle  26001  dvfsumge  26002  dvfsumabs  26003  aaliou3lem1  26322  aaliou3lem2  26323  ulmres  26369  ulmshftlem  26370  ulmshft  26371  ulmcaulem  26375  ulmcau  26376  ulmdvlem1  26381  radcnvlem1  26394  logblt  26764  logbgcd1irr  26774  muval1  27113  chtdif  27138  ppidif  27143  chtub  27192  bcmono  27257  bpos1lem  27262  lgsquad2lem2  27365  2sqlem6  27403  2sqlem8a  27405  2sqlem8  27406  chebbnd1lem1  27449  dchrisumlem2  27470  dchrisum0lem1  27496  ostthlem2  27608  ostth2  27617  axlowdimlem3  29030  axlowdimlem6  29033  axlowdimlem7  29034  axlowdimlem16  29043  axlowdimlem17  29044  axlowdim  29047  clwwnrepclwwn  30432  fzspl  32880  fzdif2  32881  supfz  35930  divcnvlin  35934  nn0prpwlem  36523  fdc  38083  mettrifi  38095  caushft  38099  aks4d1lem1  42518  aks4d1p1  42532  aks4d1p2  42533  aks4d1p3  42534  aks4d1p5  42536  aks4d1p6  42537  aks4d1p7d1  42538  aks4d1p7  42539  aks4d1p8  42543  aks4d1p9  42544  aks6d1c7lem1  42636  aks6d1c7lem2  42637  aks6d1c7  42640  aks5lem6  42648  aks5lem8  42657  aks5  42660  fzosumm1  42706  dffltz  43084  rmspecnonsq  43356  rmspecfund  43358  rmxyadd  43370  rmxy1  43371  jm2.18  43437  jm2.22  43444  jm2.15nn0  43452  jm2.16nn0  43453  jm2.27a  43454  jm2.27c  43456  jm3.1lem2  43467  jm3.1lem3  43468  jm3.1  43469  expdiophlem1  43470  dvgrat  44760  cvgdvgrat  44761  hashnzfz  44768  uzwo4  45505  ssinc  45538  ssdec  45539  rexanuz3  45547  monoords  45751  fzdifsuc2  45764  iuneqfzuzlem  45785  eluzelzd  45825  allbutfi  45843  eluzelz2  45852  uzid2  45854  monoordxrv  45930  monoord2xrv  45932  fmul01  46031  fmul01lt1lem1  46035  fmul01lt1lem2  46036  climsuselem1  46058  climsuse  46059  climf  46073  climresmpt  46108  climf2  46115  limsupequzlem  46171  limsupmnfuzlem  46175  limsupre3uzlem  46184  itgsinexp  46404  iblspltprt  46422  itgspltprt  46428  iundjiun  46909  smflimsuplem2  47270  smflimsuplem4  47272  smflimsuplem5  47273  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