Theorem eluzelz 12247

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

Syntax hints:   → wi 4   ∈ wcel 2110   class class class wbr 5058  ‘cfv 6349   ≤ cle 10670  ℤcz 11975  ℤ_≥cuz 12237

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-cnex 10587  ax-resscn 10588

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4561  df-pr 4563  df-op 4567  df-uni 4832  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-fv 6357  df-ov 7153  df-neg 10867  df-z 11976  df-uz 12238

This theorem is referenced by:  eluzelre  12248  uztrn  12255  uzneg  12257  uzss  12259  eluzp1l  12263  eluzaddi  12265  eluzsubi  12266  subeluzsub  12269  uzm1  12270  uzin  12272  uzind4  12300  uzwo  12305  uz2mulcl  12320  uzsupss  12334  elfz5  12894  elfzel2  12900  elfzelz  12902  eluzfz2  12909  peano2fzr  12914  fzsplit2  12926  fzopth  12938  ssfzunsn  12947  fzsuc  12948  elfz1uz  12971  uzsplit  12973  uzdisj  12974  fzm1  12981  uznfz  12984  nn0disj  13017  preduz  13023  elfzo3  13048  fzoss2  13059  fzouzsplit  13066  fzoun  13068  eluzgtdifelfzo  13093  fzosplitsnm1  13106  fzofzp1b  13129  elfzonelfzo  13133  fzosplitsn  13139  fzisfzounsn  13143  fldiv4lem1div2uz2  13200  m1modge3gt1  13280  modaddmodup  13296  om2uzlti  13312  om2uzf1oi  13315  uzrdgxfr  13329  fzen2  13331  seqfveq2  13386  seqfeq2  13387  seqshft2  13390  monoord  13394  monoord2  13395  sermono  13396  seqsplit  13397  seqf1olem1  13403  seqf1olem2  13404  seqid  13409  seqz  13412  leexp2a  13530  expnlbnd2  13589  expmulnbnd  13590  hashfz  13782  fzsdom2  13783  hashfzo  13784  hashfzp1  13786  seqcoll  13816  swrdfv2  14017  pfxccatin12  14089  rexuz3  14702  r19.2uz  14705  rexuzre  14706  cau4  14710  caubnd2  14711  clim  14845  climrlim2  14898  climshft2  14933  climaddc1  14985  climmulc2  14987  climsubc1  14988  climsubc2  14989  clim2ser  15005  clim2ser2  15006  iserex  15007  climlec2  15009  climub  15012  isercolllem2  15016  isercoll  15018  isercoll2  15019  climcau  15021  caurcvg2  15028  caucvgb  15030  serf0  15031  iseraltlem1  15032  iseraltlem2  15033  iseralt  15035  sumrblem  15062  fsumcvg  15063  summolem2a  15066  fsumcvg2  15078  fsumm1  15100  fzosump1  15101  fsump1  15105  fsumrev2  15131  telfsumo  15151  fsumparts  15155  isumsplit  15189  isumrpcl  15192  isumsup2  15195  cvgrat  15233  mertenslem1  15234  clim2div  15239  prodeq2ii  15261  fprodcvg  15278  prodmolem2a  15282  zprod  15285  fprodntriv  15290  fprodser  15297  fprodm1  15315  fprodp1  15317  fprodeq0  15323  isprm3  16021  nprm  16026  dvdsprm  16041  exprmfct  16042  isprm5  16045  maxprmfct  16047  ncoprmlnprm  16062  phibndlem  16101  dfphi2  16105  hashdvds  16106  pcaddlem  16218  pcfac  16229  expnprm  16232  prmreclem4  16249  vdwlem8  16318  gsumval2a  17889  efgs1b  18856  telgsumfzs  19103  iscau4  23876  caucfil  23880  iscmet3lem3  23887  iscmet3lem1  23888  iscmet3lem2  23889  lmle  23898  uniioombllem3  24180  mbflimsup  24261  mbfi1fseqlem6  24315  dvfsumle  24612  dvfsumge  24613  dvfsumabs  24614  aaliou3lem1  24925  aaliou3lem2  24926  ulmres  24970  ulmshftlem  24971  ulmshft  24972  ulmcaulem  24976  ulmcau  24977  ulmdvlem1  24982  radcnvlem1  24995  logblt  25356  logbgcd1irr  25366  muval1  25704  chtdif  25729  ppidif  25734  chtub  25782  bcmono  25847  bpos1lem  25852  lgsquad2lem2  25955  2sqlem6  25993  2sqlem8a  25995  2sqlem8  25996  chebbnd1lem1  26039  dchrisumlem2  26060  dchrisum0lem1  26086  ostthlem2  26198  ostth2  26207  axlowdimlem3  26724  axlowdimlem6  26727  axlowdimlem7  26728  axlowdimlem16  26737  axlowdimlem17  26738  axlowdim  26741  clwwnrepclwwn  28117  fzspl  30507  fzdif2  30508  supfz  32955  divcnvlin  32959  nn0prpwlem  33665  fdc  35014  mettrifi  35026  caushft  35030  fzosumm1  39119  dffltz  39264  fltne  39265  rmspecnonsq  39497  rmspecfund  39499  rmxyadd  39511  rmxy1  39512  jm2.18  39578  jm2.22  39585  jm2.15nn0  39593  jm2.16nn0  39594  jm2.27a  39595  jm2.27c  39597  jm3.1lem2  39608  jm3.1lem3  39609  jm3.1  39610  expdiophlem1  39611  dvgrat  40637  cvgdvgrat  40638  hashnzfz  40645  uzwo4  41308  ssinc  41346  ssdec  41347  rexanuz3  41355  monoords  41557  fzdifsuc2  41570  iuneqfzuzlem  41595  eluzelzd  41636  allbutfi  41658  eluzelz2  41669  uzid2  41671  monoordxrv  41751  monoord2xrv  41753  fmul01  41854  fmul01lt1lem1  41858  fmul01lt1lem2  41859  climsuselem1  41881  climsuse  41882  climf  41896  climresmpt  41933  climf2  41940  limsupequzlem  41996  limsupmnfuzlem  42000  limsupre3uzlem  42009  itgsinexp  42233  iblspltprt  42251  itgspltprt  42257  iundjiunlem  42735  iundjiun  42736  smflimsuplem2  43089  smflimsuplem4  43091  smflimsuplem5  43092  fzopredsuc  43517  smonoord  43525  iccpartiltu  43576  fmtnoprmfac2lem1  43722  fmtnofac2lem  43724  lighneallem2  43765  lighneallem4a  43767  lighneallem4b  43768  fppr2odd  43890  fpprwpprb  43899  gboge9  43923  nnsum3primesle9  43953  nnsum4primesevenALTV  43960  wtgoldbnnsum4prm  43961  bgoldbnnsum3prm  43963  bgoldbtbndlem2  43965  m1modmmod  44575  fllogbd  44614  fllog2  44622  dignn0ldlem  44656  dignnld  44657  digexp  44661  dignn0flhalf  44672  nn0sumshdiglemB  44674