Theorem eluzelz 12885

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

Syntax hints:   → wi 4   ∈ wcel 2105   class class class wbr 5147  ‘cfv 6562   ≤ cle 11293  ℤcz 12610  ℤ_≥cuz 12875

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437  ax-cnex 11208  ax-resscn 11209

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-fv 6570  df-ov 7433  df-neg 11492  df-z 12611  df-uz 12876

This theorem is referenced by:  eluzelre  12886  uztrn  12893  uzneg  12895  uzss  12898  eluzp1l  12902  eluzadd  12904  eluzsub  12905  eluzaddiOLD  12907  eluzsubiOLD  12909  subeluzsub  12912  uzm1  12913  uzin  12915  uzind4  12945  uzwo  12950  uz2mulcl  12965  uzsupss  12979  elfz5  13552  elfzel2  13558  elfzelz  13560  eluzfz2  13568  peano2fzr  13573  fzsplit2  13585  fzopth  13597  ssfzunsn  13606  fzsuc  13607  elfz1uz  13630  uzsplit  13632  uzdisj  13633  fzm1  13643  uznfz  13646  nn0disj  13680  preduz  13686  elfzo3  13712  fzoss2  13723  fzouzsplit  13730  fzoun  13732  eluzgtdifelfzo  13762  fzosplitsnm1  13775  fzofzp1b  13800  elfzonelfzo  13804  fzosplitsn  13810  fzisfzounsn  13814  fldiv4lem1div2uz2  13872  m1modge3gt1  13955  modaddmodup  13971  om2uzlti  13987  om2uzf1oi  13990  uzrdgxfr  14004  fzen2  14006  seqfveq2  14061  seqfeq2  14062  seqshft2  14065  monoord  14069  monoord2  14070  sermono  14071  seqsplit  14072  seqf1olem1  14078  seqf1olem2  14079  seqid  14084  leexp2a  14208  expnlbnd2  14269  expmulnbnd  14270  hashfz  14462  fzsdom2  14463  hashfzo  14464  hashfzp1  14466  seqcoll  14499  swrdfv2  14695  pfxccatin12  14767  rexuz3  15383  r19.2uz  15386  rexuzre  15387  cau4  15391  caubnd2  15392  clim  15526  climrlim2  15579  climshft2  15614  climaddc1  15667  climmulc2  15669  climsubc1  15670  climsubc2  15671  clim2ser  15687  clim2ser2  15688  iserex  15689  climlec2  15691  climub  15694  isercolllem2  15698  isercoll  15700  isercoll2  15701  climcau  15703  caurcvg2  15710  caucvgb  15712  serf0  15713  iseraltlem1  15714  iseraltlem2  15715  iseralt  15717  sumrblem  15743  fsumcvg  15744  summolem2a  15747  fsumcvg2  15759  fsumm1  15783  fzosump1  15784  fsump1  15788  fsumrev2  15814  telfsumo  15834  fsumparts  15838  isumsplit  15872  isumrpcl  15875  isumsup2  15878  cvgrat  15915  mertenslem1  15916  clim2div  15921  prodeq2ii  15943  fprodcvg  15962  prodmolem2a  15966  zprod  15969  fprodntriv  15974  fprodser  15981  fprodm1  15999  fprodp1  16001  fprodeq0  16007  isprm3  16716  nprm  16721  dvdsprm  16736  exprmfct  16737  isprm5  16740  maxprmfct  16742  prmdvdsncoprmbd  16760  ncoprmlnprm  16761  phibndlem  16803  dfphi2  16807  hashdvds  16808  pcaddlem  16921  pcfac  16932  expnprm  16935  prmreclem4  16952  vdwlem8  17021  gsumval2a  18710  efgs1b  19768  telgsumfzs  20021  iscau4  25326  caucfil  25330  iscmet3lem3  25337  iscmet3lem1  25338  iscmet3lem2  25339  lmle  25348  uniioombllem3  25633  mbflimsup  25714  mbfi1fseqlem6  25769  dvfsumle  26074  dvfsumleOLD  26075  dvfsumge  26076  dvfsumabs  26077  aaliou3lem1  26398  aaliou3lem2  26399  ulmres  26445  ulmshftlem  26446  ulmshft  26447  ulmcaulem  26451  ulmcau  26452  ulmdvlem1  26457  radcnvlem1  26470  logblt  26841  logbgcd1irr  26851  muval1  27190  chtdif  27215  ppidif  27220  chtub  27270  bcmono  27335  bpos1lem  27340  lgsquad2lem2  27443  2sqlem6  27481  2sqlem8a  27483  2sqlem8  27484  chebbnd1lem1  27527  dchrisumlem2  27548  dchrisum0lem1  27574  ostthlem2  27686  ostth2  27695  axlowdimlem3  28973  axlowdimlem6  28976  axlowdimlem7  28977  axlowdimlem16  28986  axlowdimlem17  28987  axlowdim  28990  clwwnrepclwwn  30372  fzspl  32797  fzdif2  32798  supfz  35708  divcnvlin  35712  nn0prpwlem  36304  fdc  37731  mettrifi  37743  caushft  37747  aks4d1lem1  42043  aks4d1p1  42057  aks4d1p2  42058  aks4d1p3  42059  aks4d1p5  42061  aks4d1p6  42062  aks4d1p7d1  42063  aks4d1p7  42064  aks4d1p8  42068  aks4d1p9  42069  aks6d1c7lem1  42161  aks6d1c7lem2  42162  aks6d1c7  42165  aks5lem6  42173  aks5lem8  42182  aks5  42185  fzosumm1  42269  dffltz  42620  rmspecnonsq  42894  rmspecfund  42896  rmxyadd  42909  rmxy1  42910  jm2.18  42976  jm2.22  42983  jm2.15nn0  42991  jm2.16nn0  42992  jm2.27a  42993  jm2.27c  42995  jm3.1lem2  43006  jm3.1lem3  43007  jm3.1  43008  expdiophlem1  43009  dvgrat  44307  cvgdvgrat  44308  hashnzfz  44315  uzwo4  44992  ssinc  45026  ssdec  45027  rexanuz3  45035  monoords  45247  fzdifsuc2  45260  iuneqfzuzlem  45283  eluzelzd  45324  allbutfi  45342  eluzelz2  45352  uzid2  45354  monoordxrv  45431  monoord2xrv  45433  fmul01  45535  fmul01lt1lem1  45539  fmul01lt1lem2  45540  climsuselem1  45562  climsuse  45563  climf  45577  climresmpt  45614  climf2  45621  limsupequzlem  45677  limsupmnfuzlem  45681  limsupre3uzlem  45690  itgsinexp  45910  iblspltprt  45928  itgspltprt  45934  iundjiun  46415  smflimsuplem2  46776  smflimsuplem4  46778  smflimsuplem5  46779  fzopredsuc  47272  smonoord  47295  iccpartiltu  47346  fmtnoprmfac2lem1  47490  fmtnofac2lem  47492  lighneallem2  47530  lighneallem4a  47532  lighneallem4b  47533  fppr2odd  47655  fpprwpprb  47664  gboge9  47688  nnsum3primesle9  47718  nnsum4primesevenALTV  47725  wtgoldbnnsum4prm  47726  bgoldbnnsum3prm  47728  bgoldbtbndlem2  47730  gpgusgralem  47945  m1modmmod  48370  fllogbd  48409  fllog2  48417  dignn0ldlem  48451  dignnld  48452  digexp  48456  dignn0flhalf  48467  nn0sumshdiglemB  48469