Theorem eluzelz 12773

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

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5100  ‘cfv 6500   ≤ cle 11179  ℤcz 12500  ℤ_≥cuz 12763

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 5243  ax-nul 5253  ax-pr 5379  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 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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-fv 6508  df-ov 7371  df-neg 11379  df-z 12501  df-uz 12764

This theorem is referenced by:  eluzelre  12774  uztrn  12781  uzneg  12783  uzss  12786  eluzp1l  12790  eluzadd  12792  eluzsub  12793  subeluzsub  12796  uzm1  12797  uzin  12799  uzind4  12831  uzwo  12836  uz2mulcl  12851  uzsupss  12865  elfz5  13444  elfzel2  13450  elfzelz  13452  eluzfz2  13460  peano2fzr  13465  fzsplit2  13477  fzopth  13489  ssfzunsn  13498  fzsuc  13499  elfz1uz  13522  uzsplit  13524  uzdisj  13525  fzm1  13535  uznfz  13538  nn0disj  13572  preduz  13578  elfzo3  13604  fzoss2  13615  fzouzsplit  13622  fzoun  13624  eluzgtdifelfzo  13655  fzosplitsnm1  13668  fzofzp1b  13693  elfzonelfzo  13697  fzosplitsn  13704  fzisfzounsn  13708  fldiv4lem1div2uz2  13768  m1modge3gt1  13853  modaddmodup  13869  om2uzlti  13885  om2uzf1oi  13888  uzrdgxfr  13902  fzen2  13904  seqfveq2  13959  seqfeq2  13960  seqshft2  13963  monoord  13967  monoord2  13968  sermono  13969  seqsplit  13970  seqf1olem1  13976  seqf1olem2  13977  seqid  13982  leexp2a  14107  expnlbnd2  14169  expmulnbnd  14170  hashfz  14362  fzsdom2  14363  hashfzo  14364  hashfzp1  14366  seqcoll  14399  swrdfv2  14597  pfxccatin12  14668  rexuz3  15284  r19.2uz  15287  rexuzre  15288  cau4  15292  caubnd2  15293  clim  15429  climrlim2  15482  climshft2  15517  climaddc1  15570  climmulc2  15572  climsubc1  15573  climsubc2  15574  clim2ser  15590  clim2ser2  15591  iserex  15592  climlec2  15594  climub  15597  isercolllem2  15601  isercoll  15603  isercoll2  15604  climcau  15606  caurcvg2  15613  caucvgb  15615  serf0  15616  iseraltlem1  15617  iseraltlem2  15618  iseralt  15620  sumrblem  15646  fsumcvg  15647  summolem2a  15650  fsumcvg2  15662  fsumm1  15686  fzosump1  15687  fsump1  15691  fsumrev2  15717  telfsumo  15737  fsumparts  15741  isumsplit  15775  isumrpcl  15778  isumsup2  15781  cvgrat  15818  mertenslem1  15819  clim2div  15824  prodeq2ii  15846  fprodcvg  15865  prodmolem2a  15869  zprod  15872  fprodntriv  15877  fprodser  15884  fprodm1  15902  fprodp1  15904  fprodeq0  15910  isprm3  16622  nprm  16627  dvdsprm  16642  exprmfct  16643  isprm5  16646  maxprmfct  16648  prmdvdsncoprmbd  16666  ncoprmlnprm  16667  phibndlem  16709  dfphi2  16713  hashdvds  16714  pcaddlem  16828  pcfac  16839  expnprm  16842  prmreclem4  16859  vdwlem8  16928  gsumval2a  18622  efgs1b  19680  telgsumfzs  19933  iscau4  25250  caucfil  25254  iscmet3lem3  25261  iscmet3lem1  25262  iscmet3lem2  25263  lmle  25272  uniioombllem3  25557  mbflimsup  25638  mbfi1fseqlem6  25692  dvfsumle  25997  dvfsumleOLD  25998  dvfsumge  25999  dvfsumabs  26000  aaliou3lem1  26321  aaliou3lem2  26322  ulmres  26368  ulmshftlem  26369  ulmshft  26370  ulmcaulem  26374  ulmcau  26375  ulmdvlem1  26380  radcnvlem1  26393  logblt  26765  logbgcd1irr  26775  muval1  27114  chtdif  27139  ppidif  27144  chtub  27194  bcmono  27259  bpos1lem  27264  lgsquad2lem2  27367  2sqlem6  27405  2sqlem8a  27407  2sqlem8  27408  chebbnd1lem1  27451  dchrisumlem2  27472  dchrisum0lem1  27498  ostthlem2  27610  ostth2  27619  axlowdimlem3  29033  axlowdimlem6  29036  axlowdimlem7  29037  axlowdimlem16  29046  axlowdimlem17  29047  axlowdim  29050  clwwnrepclwwn  30435  fzspl  32884  fzdif2  32885  supfz  35949  divcnvlin  35953  nn0prpwlem  36542  fdc  38000  mettrifi  38012  caushft  38016  aks4d1lem1  42436  aks4d1p1  42450  aks4d1p2  42451  aks4d1p3  42452  aks4d1p5  42454  aks4d1p6  42455  aks4d1p7d1  42456  aks4d1p7  42457  aks4d1p8  42461  aks4d1p9  42462  aks6d1c7lem1  42554  aks6d1c7lem2  42555  aks6d1c7  42558  aks5lem6  42566  aks5lem8  42575  aks5  42578  fzosumm1  42624  dffltz  42996  rmspecnonsq  43268  rmspecfund  43270  rmxyadd  43282  rmxy1  43283  jm2.18  43349  jm2.22  43356  jm2.15nn0  43364  jm2.16nn0  43365  jm2.27a  43366  jm2.27c  43368  jm3.1lem2  43379  jm3.1lem3  43380  jm3.1  43381  expdiophlem1  43382  dvgrat  44672  cvgdvgrat  44673  hashnzfz  44680  uzwo4  45417  ssinc  45450  ssdec  45451  rexanuz3  45459  monoords  45663  fzdifsuc2  45676  iuneqfzuzlem  45697  eluzelzd  45737  allbutfi  45755  eluzelz2  45765  uzid2  45767  monoordxrv  45843  monoord2xrv  45845  fmul01  45944  fmul01lt1lem1  45948  fmul01lt1lem2  45949  climsuselem1  45971  climsuse  45972  climf  45986  climresmpt  46021  climf2  46028  limsupequzlem  46084  limsupmnfuzlem  46088  limsupre3uzlem  46097  itgsinexp  46317  iblspltprt  46335  itgspltprt  46341  iundjiun  46822  smflimsuplem2  47183  smflimsuplem4  47185  smflimsuplem5  47186  fzopredsuc  47687  m1modmmod  47722  smonoord  47735  iccpartiltu  47786  fmtnoprmfac2lem1  47930  fmtnofac2lem  47932  lighneallem2  47970  lighneallem4a  47972  lighneallem4b  47973  fppr2odd  48095  fpprwpprb  48104  gboge9  48128  nnsum3primesle9  48158  nnsum4primesevenALTV  48165  wtgoldbnnsum4prm  48166  bgoldbnnsum3prm  48168  bgoldbtbndlem2  48170  gpgusgralem  48420  gpgprismgr4cycllem9  48467  fllogbd  48924  fllog2  48932  dignn0ldlem  48966  dignnld  48967  digexp  48971  dignn0flhalf  48982  nn0sumshdiglemB  48984