Theorem eluzelz 12803

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

Syntax hints:   → wi 4   ∈ wcel 2109   class class class wbr 5107  ‘cfv 6511   ≤ cle 11209  ℤcz 12529  ℤ_≥cuz 12793

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-cnex 11124  ax-resscn 11125

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-fv 6519  df-ov 7390  df-neg 11408  df-z 12530  df-uz 12794

This theorem is referenced by:  eluzelre  12804  uztrn  12811  uzneg  12813  uzss  12816  eluzp1l  12820  eluzadd  12822  eluzsub  12823  eluzaddiOLD  12825  eluzsubiOLD  12827  subeluzsub  12830  uzm1  12831  uzin  12833  uzind4  12865  uzwo  12870  uz2mulcl  12885  uzsupss  12899  elfz5  13477  elfzel2  13483  elfzelz  13485  eluzfz2  13493  peano2fzr  13498  fzsplit2  13510  fzopth  13522  ssfzunsn  13531  fzsuc  13532  elfz1uz  13555  uzsplit  13557  uzdisj  13558  fzm1  13568  uznfz  13571  nn0disj  13605  preduz  13611  elfzo3  13637  fzoss2  13648  fzouzsplit  13655  fzoun  13657  eluzgtdifelfzo  13688  fzosplitsnm1  13701  fzofzp1b  13726  elfzonelfzo  13730  fzosplitsn  13736  fzisfzounsn  13740  fldiv4lem1div2uz2  13798  m1modge3gt1  13883  modaddmodup  13899  om2uzlti  13915  om2uzf1oi  13918  uzrdgxfr  13932  fzen2  13934  seqfveq2  13989  seqfeq2  13990  seqshft2  13993  monoord  13997  monoord2  13998  sermono  13999  seqsplit  14000  seqf1olem1  14006  seqf1olem2  14007  seqid  14012  leexp2a  14137  expnlbnd2  14199  expmulnbnd  14200  hashfz  14392  fzsdom2  14393  hashfzo  14394  hashfzp1  14396  seqcoll  14429  swrdfv2  14626  pfxccatin12  14698  rexuz3  15315  r19.2uz  15318  rexuzre  15319  cau4  15323  caubnd2  15324  clim  15460  climrlim2  15513  climshft2  15548  climaddc1  15601  climmulc2  15603  climsubc1  15604  climsubc2  15605  clim2ser  15621  clim2ser2  15622  iserex  15623  climlec2  15625  climub  15628  isercolllem2  15632  isercoll  15634  isercoll2  15635  climcau  15637  caurcvg2  15644  caucvgb  15646  serf0  15647  iseraltlem1  15648  iseraltlem2  15649  iseralt  15651  sumrblem  15677  fsumcvg  15678  summolem2a  15681  fsumcvg2  15693  fsumm1  15717  fzosump1  15718  fsump1  15722  fsumrev2  15748  telfsumo  15768  fsumparts  15772  isumsplit  15806  isumrpcl  15809  isumsup2  15812  cvgrat  15849  mertenslem1  15850  clim2div  15855  prodeq2ii  15877  fprodcvg  15896  prodmolem2a  15900  zprod  15903  fprodntriv  15908  fprodser  15915  fprodm1  15933  fprodp1  15935  fprodeq0  15941  isprm3  16653  nprm  16658  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  18612  efgs1b  19666  telgsumfzs  19919  iscau4  25179  caucfil  25183  iscmet3lem3  25190  iscmet3lem1  25191  iscmet3lem2  25192  lmle  25201  uniioombllem3  25486  mbflimsup  25567  mbfi1fseqlem6  25621  dvfsumle  25926  dvfsumleOLD  25927  dvfsumge  25928  dvfsumabs  25929  aaliou3lem1  26250  aaliou3lem2  26251  ulmres  26297  ulmshftlem  26298  ulmshft  26299  ulmcaulem  26303  ulmcau  26304  ulmdvlem1  26309  radcnvlem1  26322  logblt  26694  logbgcd1irr  26704  muval1  27043  chtdif  27068  ppidif  27073  chtub  27123  bcmono  27188  bpos1lem  27193  lgsquad2lem2  27296  2sqlem6  27334  2sqlem8a  27336  2sqlem8  27337  chebbnd1lem1  27380  dchrisumlem2  27401  dchrisum0lem1  27427  ostthlem2  27539  ostth2  27548  axlowdimlem3  28871  axlowdimlem6  28874  axlowdimlem7  28875  axlowdimlem16  28884  axlowdimlem17  28885  axlowdim  28888  clwwnrepclwwn  30273  fzspl  32712  fzdif2  32713  supfz  35716  divcnvlin  35720  nn0prpwlem  36310  fdc  37739  mettrifi  37751  caushft  37755  aks4d1lem1  42050  aks4d1p1  42064  aks4d1p2  42065  aks4d1p3  42066  aks4d1p5  42068  aks4d1p6  42069  aks4d1p7d1  42070  aks4d1p7  42071  aks4d1p8  42075  aks4d1p9  42076  aks6d1c7lem1  42168  aks6d1c7lem2  42169  aks6d1c7  42172  aks5lem6  42180  aks5lem8  42189  aks5  42192  fzosumm1  42238  dffltz  42622  rmspecnonsq  42895  rmspecfund  42897  rmxyadd  42910  rmxy1  42911  jm2.18  42977  jm2.22  42984  jm2.15nn0  42992  jm2.16nn0  42993  jm2.27a  42994  jm2.27c  42996  jm3.1lem2  43007  jm3.1lem3  43008  jm3.1  43009  expdiophlem1  43010  dvgrat  44301  cvgdvgrat  44302  hashnzfz  44309  uzwo4  45047  ssinc  45081  ssdec  45082  rexanuz3  45090  monoords  45295  fzdifsuc2  45308  iuneqfzuzlem  45330  eluzelzd  45371  allbutfi  45389  eluzelz2  45399  uzid2  45401  monoordxrv  45477  monoord2xrv  45479  fmul01  45578  fmul01lt1lem1  45582  fmul01lt1lem2  45583  climsuselem1  45605  climsuse  45606  climf  45620  climresmpt  45657  climf2  45664  limsupequzlem  45720  limsupmnfuzlem  45724  limsupre3uzlem  45733  itgsinexp  45953  iblspltprt  45971  itgspltprt  45977  iundjiun  46458  smflimsuplem2  46819  smflimsuplem4  46821  smflimsuplem5  46822  fzopredsuc  47324  m1modmmod  47359  smonoord  47372  iccpartiltu  47423  fmtnoprmfac2lem1  47567  fmtnofac2lem  47569  lighneallem2  47607  lighneallem4a  47609  lighneallem4b  47610  fppr2odd  47732  fpprwpprb  47741  gboge9  47765  nnsum3primesle9  47795  nnsum4primesevenALTV  47802  wtgoldbnnsum4prm  47803  bgoldbnnsum3prm  47805  bgoldbtbndlem2  47807  gpgusgralem  48047  gpgprismgr4cycllem9  48093  fllogbd  48549  fllog2  48557  dignn0ldlem  48591  dignnld  48592  digexp  48596  dignn0flhalf  48607  nn0sumshdiglemB  48609